Implement chaotic iterations on EDDs. Global widening is missing.

1 files changed, 329 insertions, 109 deletions

diff --git a/abstract/abs_interp_edd.ml b/abstract/abs_interp_edd.ml
index ebf7549..0dfc6f3 100644
--- a/abstract/abs_interp_edd.ml
+++ b/abstract/abs_interp_edd.ml
@@ -7,15 +7,12 @@ open Util
 open Num_domain
 open Abs_interp
 
-let time id f =
-  Format.printf "%s[@?" id;
-  let r = f () in
-  Format.printf "] @?";
-  r
 
 
 exception Top
 
+exception Found_int of int
+
 module I (ND : NUMERICAL_ENVIRONMENT_DOMAIN) : sig
 
     val do_prog : cmdline_opt -> rooted_prog -> unit
@@ -43,7 +40,7 @@ end = struct
     type edd =
         | DBot
         | DTop
-        | DVal of int
+        | DVal of int * bool   (* bool : new case ? *)
         | DChoice of int * id * (item * edd) list
 
     type edd_v = {
@@ -66,7 +63,7 @@ end = struct
     let key = function
         | DBot -> 0
         | DTop -> 1
-        | DVal i -> 2 * i + 2
+        | DVal (i, _) -> 2 * i + 2
         | DChoice(i, _, _) -> 2 * i + 3
 
     let memo f =
@@ -90,10 +87,43 @@ end = struct
     let edd_node_eq = function
         | DBot, DBot -> true
         | DTop, DTop -> true
-        | DVal i, DVal j when i = j -> true
+        | DVal (i, _), DVal (j, _) when i = j -> true
         | DChoice(i, _, _), DChoice(j, _, _) when i = j -> true
         | _ -> false
 
+    let new_node_fun () =
+        let nc = ref 0 in
+        let node_memo = Hashtbl.create 12 in
+        fun v l ->
+          let _, x0 = List.hd l in
+          if List.exists (fun (_, x) -> not (edd_node_eq (x, x0))) l
+            then begin
+              let k = (v, List.map (fun (a, b) -> a, key b) l) in
+              let n =
+                try Hashtbl.find node_memo k
+                with _ -> (incr nc; Hashtbl.add node_memo k !nc; !nc)
+              in
+              DChoice(n, v, l)
+            end else x0
+
+    let get_leaf_fun_st () =
+        let leaves = Hashtbl.create 12 in
+        let lc = ref 0 in
+        let get_leaf st x = 
+          if ND.is_top x then DTop else
+          if ND.is_bot x then DBot else
+            try
+              Hashtbl.iter (fun i v -> if ND.eq v x then raise (Found_int i)) leaves;
+              incr lc;
+              Hashtbl.add leaves !lc x;
+              DVal (!lc, st)
+            with Found_int i -> DVal (i, st)
+        in leaves, get_leaf
+
+    let get_leaf_fun () =
+        let leaves, get_leaf = get_leaf_fun_st () in
+        leaves, get_leaf false
+
     (*
       edd_print : Format.formatter -> edd_v -> unit
     *)
@@ -115,11 +145,11 @@ end = struct
         let print_n fmt = function
           | DBot -> Format.fprintf fmt "⊥";
           | DTop -> Format.fprintf fmt "⊤";
-          | DVal i -> if i > !max_v then max_v := i;
-                    Format.fprintf fmt "v%d" i;
+          | DVal (i, s) -> if i > !max_v then max_v := i;
+                    Format.fprintf fmt "v%d%s" i (if s then "*" else "");
           | DChoice(n, _, _) -> Format.fprintf fmt "n%d" n
         in
-        Format.fprintf fmt "Root: %a@." print_n v.root;
+        Format.fprintf fmt "%a where:@." print_n v.root;
 
         for id = !max_n downto 0 do
           try match Hashtbl.find c_nodes id with
@@ -180,46 +210,15 @@ end = struct
         { ve; root; leaves }
 
     (*
-      edd_join_meet : bool -> edd_v -> edd_v -> edd_v
       edd_join : edd_v -> edd_v -> edd_v
       edd_meet : edd_v -> edd_v -> edd_v
     *)
-    let edd_join_meet op a b =
+    let edd_join a b =
         let ve = a.ve in
+        let leaves, get_leaf = get_leaf_fun () in
+        let dq = new_node_fun () in
 
-        let leaves = Hashtbl.create 12 in
-        let lc = ref 0 in
-
-        let get_leaf x = 
-          if ND.is_top x then DTop else
-          if ND.is_bot x then DBot else begin
-            let id = ref None in
-            Hashtbl.iter (fun i v -> if ND.eq v x then id := Some i) leaves;
-            match !id with
-            | Some i -> DVal i
-            | None ->
-              incr lc;
-              Hashtbl.add leaves !lc x;
-              DVal (!lc)
-          end
-        in
-
-        let nc = ref 0 in
-        let node_memo = Hashtbl.create 12 in
-        let dq v l =
-          let _, x0 = List.hd l in
-          if List.exists (fun (_, x) -> not (edd_node_eq (x, x0))) l
-            then begin
-              let k = (v, List.map (fun (a, b) -> a, key b) l) in
-              let n =
-                try Hashtbl.find node_memo k
-                with _ -> (incr nc; Hashtbl.add node_memo k !nc; !nc)
-              in
-              DChoice(n, v, l)
-            end else x0
-        in
-
-        let f_join f_rec na nb =
+        let f f_rec na nb =
           match na, nb with
           | DTop, _ | _, DTop -> DTop
           | DBot, DBot -> DBot
@@ -240,11 +239,11 @@ end = struct
             in
             dq v kl
 
-          | DBot, DVal i ->
+          | DBot, DVal (i, _) ->
               get_leaf (Hashtbl.find b.leaves i)
-          | DVal i, DBot ->
+          | DVal (i, _), DBot ->
               get_leaf (Hashtbl.find a.leaves i)
-          | DVal u, DVal v ->
+          | DVal (u, _), DVal (v, _) ->
             let x = ND.join (Hashtbl.find a.leaves u) (Hashtbl.find b.leaves v) in
             get_leaf x
 
@@ -255,8 +254,14 @@ end = struct
             let kl = List.map (fun (k, cb) -> k, f_rec na cb) lb in
             dq vb kl
         in
+          { leaves; ve; root = time "join" (fun () -> memo2 f a.root b.root) }
 
-        let f_meet f_rec na nb =
+    let edd_meet a b =
+        let ve = a.ve in
+        let leaves, get_leaf = get_leaf_fun () in
+        let dq = new_node_fun () in
+
+        let f f_rec na nb =
           match na, nb with
           | DBot, _ | _, DBot -> DBot
           | DTop, DTop -> DTop
@@ -277,11 +282,11 @@ end = struct
             in
             dq v kl
 
-          | DTop, DVal i ->
+          | DTop, DVal (i, _) ->
             get_leaf (Hashtbl.find b.leaves i)
-          | DVal i, DTop ->
+          | DVal (i, _), DTop ->
             get_leaf (Hashtbl.find a.leaves i)
-          | DVal u, DVal v ->
+          | DVal (u, _) , DVal (v, _) ->
             let x = ND.meet (Hashtbl.find a.leaves u) (Hashtbl.find b.leaves v) in
             get_leaf x
 
@@ -292,14 +297,7 @@ end = struct
             let kl = List.map (fun (k, cb) -> k, f_rec na cb) lb in
             dq vb kl
         in
-
-        if op then
-          { leaves; ve; root = time "join" (fun () -> memo2 f_join a.root b.root) }
-        else
-          { leaves; ve; root = time "meet" (fun () -> memo2 f_meet a.root b.root) }
-
-    let edd_join = edd_join_meet true
-    let edd_meet = edd_join_meet false
+          { leaves; ve; root = time "meet" (fun () -> memo2 f a.root b.root) }
 
 
 
@@ -310,33 +308,18 @@ end = struct
     let edd_num_apply v nfun =
         let ve = v.ve in
 
-        let lc = ref 0 in
-        let leaves = Hashtbl.create 12 in
+        let leaves, get_leaf = get_leaf_fun () in
 
-        let get_leaf x = 
-          if ND.is_bot x then DBot else begin
-            let id = ref None in
-            Hashtbl.iter (fun i v -> if ND.eq v x then id := Some i) leaves;
-            match !id with
-            | Some i -> DVal i
-            | None ->
-              incr lc;
-              Hashtbl.add leaves !lc x;
-              DVal (!lc)
-          end
-        in
+        let dq = new_node_fun () in
 
         let f f_rec n =
           match n with
           | DBot -> DBot
           | DTop -> get_leaf (nfun (ND.top ve.nvars))
-          | DVal i -> get_leaf (nfun (Hashtbl.find v.leaves i))
+          | DVal (i, _) -> get_leaf (nfun (Hashtbl.find v.leaves i))
           | DChoice(n, var, l) ->
             let l = List.map (fun (k, v) -> k, f_rec v) l in
-            let _, x0 = List.hd l in
-            if List.exists (fun (_, x) -> not (edd_node_eq (x, x0))) l
-              then DChoice(n, var, l)
-              else x0
+            dq var l
         in
         { leaves; ve; root = memo f v.root }
 
@@ -375,6 +358,25 @@ end = struct
           edd_join (edd_apply_cl v (eca, nc@nca, ra))
                    (edd_apply_cl v (ecb, nc@ncb, rb))
 
+
+    (*
+      edd_extract_path : edd_v -> id -> edd_v
+    *)
+    let edd_extract_path v leaf_id =
+        let ve = v.ve in
+
+        let dq = new_node_fun () in
+
+        let f f_rec n =
+          match n with
+          | DVal (i, _) when i = leaf_id -> DTop
+          | DChoice(n, var, l) ->
+            let l = List.map (fun (k, v) -> k, f_rec v) l in
+            dq var l
+          | _ -> DBot
+        in
+        { leaves = Hashtbl.create 1; ve; root = memo f v.root }
+
     (*
       edd_eq : edd_v -> edd_v -> bool
     *)
@@ -383,7 +385,7 @@ end = struct
           match na, nb with
           | DBot, DBot -> true
           | DTop, DTop -> true
-          | DVal i, DVal j ->
+          | DVal (i, _), DVal (j, _) ->
             ND.eq (Hashtbl.find a.leaves i) (Hashtbl.find b.leaves j)
           | DChoice(_, va, la), DChoice(_, vb, lb) when va = vb ->
             List.for_all2 (fun (ca, na) (cb, nb) -> assert (ca = cb); f_rec na nb)
@@ -398,23 +400,11 @@ end = struct
     let edd_forget_vars v vars =
         let ve = v.ve in
 
-        let leaves = Hashtbl.create 12 in
-        let lc = ref 0 in
-
-        let get_leaf x = 
-          let id = ref None in
-          Hashtbl.iter (fun i v -> if ND.eq v x then id := Some i) leaves;
-          begin match !id with
-          | Some i -> DVal i
-          | None ->
-            incr lc;
-            Hashtbl.add leaves !lc x;
-            DVal (!lc)
-          end
-        in
+        let leaves, get_leaf = get_leaf_fun () in
 
         let nc = ref 0 in
         let memo = Hashtbl.create 12 in
+        let node_memo = Hashtbl.create 12 in
         let rec f l =
             let kl = List.sort Pervasives.compare (List.map key l) in
             try Hashtbl.find memo kl
@@ -424,7 +414,7 @@ end = struct
                   (fun (cn, fn) node -> match node with
                     | DBot -> cn, fn
                     | DTop -> raise Top
-                    | DVal i -> cn, i::fn
+                    | DVal (i, _) -> cn, i::fn
                     | DChoice (n, v, l) -> (n, v, l)::cn, fn)
                   ([], []) l in
                 let cn = List.sort
@@ -441,7 +431,7 @@ end = struct
                   let _, dv, cl = List.hd cn in
                   let d, nd = List.partition (fun (_, v, _) -> v = dv) cn in
                   let ch1 = List.map (fun (a, b, c) -> DChoice(a, b, c)) nd in
-                  let ch2 = List.map (fun i -> DVal i) fn in
+                  let ch2 = List.map (fun i -> DVal (i, false)) fn in
                   if List.mem dv vars then
                     (* Do union of all branches branching from nodes on variable dv *)
                     let ch3 = List.flatten
@@ -458,7 +448,12 @@ end = struct
                     let _, x0 = List.hd cc in
                     if List.exists (fun (_, x) -> not (edd_node_eq (x, x0))) cc
                     then begin
-                      incr nc; DChoice(!nc, dv, cc)
+                      let k = (dv, List.map (fun (a, b) -> a, key b) cc) in
+                      let n =
+                        try Hashtbl.find node_memo k
+                        with _ -> (incr nc; Hashtbl.add node_memo k !nc; !nc)
+                      in
+                      DChoice(n, dv, cc)
                     end else x0
               with | Top -> DTop
             in Hashtbl.add memo kl r; r
@@ -524,7 +519,134 @@ end = struct
 
 
     (*
+      edd_find_starred : edd_v -> int option
+      edd_unstar : edd_v -> int -> edd_v
+    *)
+    let edd_find_starred v =
+        let f f_rec = function
+          | DVal (i, true) -> raise (Found_int i)
+          | DChoice(_, _, l) -> List.iter (fun (_, x) -> f_rec x) l
+          | _ -> ()
+        in
+        try memo f v.root; None
+        with Found_int i -> Some i
+
+    let edd_unstar v i =
+        let f f_rec = function
+          | DChoice(a, b, l) -> DChoice(a, b, List.map (fun (c, x) -> c, f_rec x) l)
+          | DVal(j, n) when i = j -> DVal(i, false)
+          | x -> x
+        in
+        { v with root = memo f v.root }
+
+
+    (*
+      edd_join_widen : edd_v -> edd_v -> edd_v
+    *)
+    let edd_join_widen (a:edd_v) (b:edd_v) =
+        let ve = a.ve in
+        let leaves, get_leaf = get_leaf_fun () in
+        let dq = new_node_fun () in
+
+        let f f_rec na nb =
+          match na, nb with
+          | DTop, _ | _, DTop -> DTop
+          | DBot, DBot -> DBot
+
+          | DChoice(_, va, la), DChoice(_, vb, lb) when va = vb ->
+            let kl = List.map2
+                (fun (ta, ba) (tb, bb) -> assert (ta = tb);
+                  ta, f_rec ba bb)
+                la lb
+            in
+            dq va kl
+          | DChoice(_, va, la), DChoice(_, vb, lb) ->
+            let v, kl =
+              if Hashtbl.find ve.ev_order va < Hashtbl.find ve.ev_order vb then
+                va, List.map (fun (k, ca) -> k, f_rec ca nb) la
+              else
+                vb, List.map (fun (k, cb) -> k, f_rec na cb) lb
+            in
+            dq v kl
+
+          | DBot, DVal (i, _) ->
+              get_leaf (Hashtbl.find b.leaves i)
+          | DVal (i, _), DBot ->
+              get_leaf (Hashtbl.find a.leaves i)
+          | DVal (u, _), DVal (v, _) ->
+            let p1, p2 = edd_extract_path a u, edd_extract_path b v in
+            let widen = 
+              if edd_eq p1 p2 then true else false
+            in
+            let x = (if widen then ND.widen else ND.join)
+                 (Hashtbl.find a.leaves u) (Hashtbl.find b.leaves v) in
+            get_leaf x
+
+          | DChoice(_,va, la), _ ->
+            let kl = List.map (fun (k, ca) -> k, f_rec ca nb) la in
+            dq va kl
+          | _, DChoice(_, vb, lb) ->
+            let kl = List.map (fun (k, cb) -> k, f_rec na cb) lb in
+            dq vb kl
+        in
+        { leaves; ve; root = time "join/W" (fun () -> memo2 f a.root b.root) }
+
+    (*
+      edd_join_star : edd_v -> edd_v -> edd_v
+
+      Star in A all things that are in B and not in A.
+    *)
+    let edd_join_star (a:edd_v) (b:edd_v) =
+        let ve = a.ve in
+        let leaves, get_leaf = get_leaf_fun_st () in
+        let dq = new_node_fun () in
+
+        let f f_rec na nb =
+          match na, nb with
+          | DTop, _ | _, DTop -> DTop
+          | DBot, DBot -> DBot
+
+          | DChoice(_, va, la), DChoice(_, vb, lb) when va = vb ->
+            let kl = List.map2
+                (fun (ta, ba) (tb, bb) -> assert (ta = tb);
+                  ta, f_rec ba bb)
+                la lb
+            in
+            dq va kl
+          | DChoice(_, va, la), DChoice(_, vb, lb) ->
+            let v, kl =
+              if Hashtbl.find ve.ev_order va < Hashtbl.find ve.ev_order vb then
+                va, List.map (fun (k, ca) -> k, f_rec ca nb) la
+              else
+                vb, List.map (fun (k, cb) -> k, f_rec na cb) lb
+            in
+            dq v kl
+
+          | DBot, DVal (i, _) ->
+              get_leaf true (Hashtbl.find b.leaves i)
+          | DVal (i, s), DBot ->
+              get_leaf s (Hashtbl.find a.leaves i)
+          | DVal (u, s1), DVal (v, _) ->
+            let p1, p2 = edd_extract_path a u, edd_extract_path b v in
+            let d1, d2 = Hashtbl.find a.leaves u, Hashtbl.find b.leaves v in
+            let star = 
+              s1 || not (edd_eq p1 p2) || not (ND.subset d2 d1)
+            in
+            let x = ND.join d1 d2 in
+            get_leaf star x
+
+          | DChoice(_,va, la), _ ->
+            let kl = List.map (fun (k, ca) -> k, f_rec ca nb) la in
+            dq va kl
+          | _, DChoice(_, vb, lb) ->
+            let kl = List.map (fun (k, cb) -> k, f_rec na cb) lb in
+            dq vb kl
+        in
+        { leaves; ve; root = time "join/*" (fun () -> memo2 f a.root b.root) }
+
+    (*
       pass_cycle : env -> edd_v -> edd_v
+      unpass_cycle : env -> edd_v -> edd_v
     *)
     let pass_cycle env v =
         let assign_e, assign_n = List.fold_left
@@ -545,6 +667,28 @@ end = struct
         let v = edd_forget_vars v ef in
         edd_num_apply v (fun nv -> List.fold_left ND.forgetvar nv nf)
 
+    let unpass_cycle env v =
+        let assign_e, assign_n = List.fold_left
+          (fun (ae, an) (a, b, t) -> match t with
+            | TEnum _ -> (b, a)::ae, an
+            | TInt | TReal -> ae, (b, NIdent a)::an)
+          ([], []) env.cycle in
+
+        let v = edd_eassign v assign_e in
+        let v = edd_num_apply v (fun nv -> ND.assign nv assign_n) in
+
+        let ef, nf = List.fold_left
+            (fun (ef, nf) (_, var, t) ->
+              if var.[0] <> 'N' then
+                match t with
+                | TEnum _ -> var::ef, nf
+                | TReal | TInt -> ef, var::nf
+              else ef, nf)
+            ([], []) env.rp.all_vars in
+
+        let v = edd_forget_vars v ef in
+        edd_num_apply v (fun nv -> List.fold_left ND.forgetvar nv nf)
+
     (*
       extract_linked_evars : conslist -> (id * id) list
 
@@ -700,7 +844,7 @@ end = struct
              (List.sort Pervasives.compare (List.map ord_couple lv1)) in
         let lv2 = uniq_sorted
              (List.sort Pervasives.compare (List.map ord_couple lv2)) in
-        let evars_ord = List.rev @@  scope_constrict evars ( lv1 ) in
+        let evars_ord = List.rev @@  time "SCA" (fun () -> scope_constrict evars ( lv1 )) in
 
         let ev_order = Hashtbl.create (List.length evars) in
         List.iteri (fun i x -> Hashtbl.add ev_order x i) evars_ord;
@@ -737,20 +881,69 @@ end = struct
 
     let do_prog opt rp =
         let e = init_env opt rp in
-        let rec f x =
-          Format.printf "Apply formula...@.";
-          let d2 = edd_apply_cl x e.cl in
-          Format.printf "Pass cycle...@.";
-          let dc = pass_cycle e d2 in
-          Format.printf "Join with init...@.";
-          let dcc = edd_join dc e.data in
-          Format.printf "@[<hov>%a@]@.@." edd_print dcc;
-          if not (edd_eq x dcc) then f dcc else dcc
+
+        (* Do iterations until fixpoint is reached *)
+        let rec ch_it n x =
+          match edd_find_starred x with
+          | None ->
+            Format.printf "Chaotic iteration %d : full iteration.@." n;
+
+            let d2 = edd_apply_cl x e.cl in
+            let dc = pass_cycle e d2 in
+            let y = edd_join_star x dc in
+
+            if e.opt.verbose_ci then
+              Format.printf " -> %a@." edd_print y;
+
+            if not (edd_eq x y) then ch_it (n+1) y else y
+
+          | Some i ->
+            let path = edd_extract_path x i in
+            let x = edd_unstar x i in
+            Format.printf "Chaotic iteration %d: @[<hov>%a@]@." n edd_print path;
+
+            let path_target = unpass_cycle e path in
+            let start = edd_meet path x in
+
+            let f i =
+              let i = edd_meet path i in
+              let i' = edd_meet i path_target in
+              let q = edd_join start (pass_cycle e (edd_apply_cl i' e.cl)) in
+              edd_meet path q
+            in
+
+            let rec iter n i =
+              let fi = f i in
+              let j =
+                if n < e.opt.widen_delay then
+                  edd_join i fi
+                else
+                  edd_join_widen i fi
+              in
+              if edd_eq i j then j else iter (n+1) j
+            in
+            let y = iter 0 start in
+            let z = fix edd_eq f y in
+
+
+            let j = pass_cycle e (edd_apply_cl z e.cl) in
+            let r = edd_join_star x j in
+
+            if e.opt.verbose_ci then
+              Format.printf " -> %a@." edd_print r;
+
+            ch_it (n+1) r
         in
+
+        let init_acc = edd_join_star (edd_bot e.data.ve) e.data in
         
-        let final = edd_apply_cl (f e.data) e.cl in
+        (* Dump final state *)
+        let acc = ch_it 0 init_acc in
+        Format.printf "Finishing up...@.";
+        let final = edd_apply_cl acc e.cl in
         (*Format.printf "@.Final:@.@[<hov>%a@]@." edd_print final;*)
 
+        (* Check guarantees *)
         let check_guarantee (id, f) =
           let cl = Formula.conslist_of_f f in
           Format.printf "@[<hv 4>%s:@ %a ⇒ ⊥  @ "
@@ -767,6 +960,33 @@ end = struct
           Format.printf "@]@."
         end;
 
+        (* Examine probes *)
+        if List.exists (fun (p, _, _) -> p) e.rp.all_vars then begin
+          let final_flat = edd_forget_vars final
+            (List.fold_left
+              (fun l (_, id, ty) -> match ty with
+                | TInt | TReal -> l
+                | TEnum _ -> id::l)
+              [] e.rp.all_vars) in
+          let final_flat = match final_flat.root with
+            | DTop -> ND.top e.ve.nvars
+            | DBot -> ND.bottom e.ve.nvars
+            | DVal(i, _) -> Hashtbl.find final_flat.leaves i
+            | DChoice _ -> assert false
+          in
+
+          Format.printf "Probes: @[<v 0>";
+          List.iter (fun (p, id, ty) ->
+            if p then match ty with
+            | TInt | TReal ->
+              Format.printf "%a ∊ %a@." Formula_printer.print_id id
+                ND.print_itv (ND.project final_flat id)
+            | TEnum _ -> Format.printf "%a : enum variable@."
+                Formula_printer.print_id id)
+            e.rp.all_vars;
+          Format.printf "@]@."
+        end
+
 end