Implement a few things. Tomorrow: optimizations.

2 files changed, 138 insertions, 51 deletions

diff --git a/abstract/abs_interp_edd.ml b/abstract/abs_interp_edd.ml
index a9ecc07..3ff91a6 100644
--- a/abstract/abs_interp_edd.ml
+++ b/abstract/abs_interp_edd.ml
@@ -65,14 +65,18 @@ end = struct
           | DChoice _ as x -> Format.fprintf fmt "n%d" (Hashtbl.find ids x)
         in
         Format.fprintf fmt "Root: %a@." print_n v.root;
-        Hashtbl.iter
-            (fun x id -> match x with
+        for id = 1 to !n do
+          let c = ref None in
+          Hashtbl.iter (fun u i -> if i = id then c := Some u) ids;
+          let x = match !c with | Some x -> x | None -> assert false in
+          match x with
               | DChoice (var, l) ->
                 let p fmt (c, l) = Format.fprintf fmt "%s → %a" c print_n l in
-                Format.fprintf fmt "n%d: %s ? @[<hov>%a@]@." id var
+                Format.fprintf fmt "n%d: %a ? @[<hov>%a@]@."
+                    id Formula_printer.print_id var
                     (print_list p ", ") l
-              | _ -> assert false)
-            ids;
+              | _ -> assert false
+        done;
         Hashtbl.iter
             (fun id v -> Format.fprintf fmt "v%d: %a@." id ND.print v)
             v.leaves
@@ -262,22 +266,80 @@ end = struct
         { leaves; ve; root = f (a.root, b.root) }
 
     (*
-      edd_of_conslist : varenv -> enum_cons list -> edd_v
-
-      Does this by dichotomy so that the EDD meets are done mostly on
-      small sized EDDs.
+      edd_apply_ncl : edd_v -> num_cons list -> edd_v
     *)
-    let rec edd_of_conslist ve = function
-      | [] -> edd_top ve
-      | [a] -> edd_of_cons ve a
-      | l ->
-        let rec split = function
-          | [] -> [], []
-          | [a] -> [a], []
-          | a::b::q -> let u, v = split q in a::u, b::v
+    let edd_apply_ncl v ncl =
+        let ve = v.ve in
+
+        let n = ref 0 in
+        let leaves = Hashtbl.create 12 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 n;
+              Hashtbl.add leaves !n x;
+              DVal (!n)
+          end
+        in
+
+        let memo = Hashtbl.create 12 in
+        let rec f n =
+          try Hashtbl.find memo n
+          with Not_found -> let r =
+            match n with
+            | DBot -> DBot
+            | DVal i -> get_leaf (ND.apply_cl (Hashtbl.find v.leaves i) ncl)
+            | DChoice(var, l) ->
+              let l = List.map (fun (k, v) -> k, f v) l in
+              let _, x0 = List.hd l in
+              if List.exists (fun (_, x) -> x <> x0) l
+                then DChoice(var, l)
+                else x0
+          in Hashtbl.add memo n r; r
         in
-        let u, v = split l in
-        edd_meet (edd_of_conslist ve u) (edd_of_conslist ve v)
+        { leaves; ve; root = f v.root }
+
+    (*
+      edd_apply_cl : edd_v -> conslist -> edd_v
+    *)
+    let rec edd_apply_cl v (ec, nc, r) =
+        let v = List.fold_left
+            (fun v cons -> edd_meet v (edd_of_cons v.ve cons))
+            v ec in
+        match r with
+        | CLTrue ->
+          edd_apply_ncl v nc
+        | CLFalse -> edd_bot v.ve
+        | CLAnd (a, b) ->
+          let v = edd_apply_cl v ([], nc, a) in
+          edd_apply_cl v ([], nc, b)
+        | CLOr((eca, nca, ra), (ecb, ncb, rb)) ->
+          edd_join (edd_apply_cl v (eca, nc@nca, ra))
+                   (edd_apply_cl v (ecb, nc@ncb, rb))
+
+    (*
+      edd_eq : edd_v -> edd_v -> bool
+    *)
+    let edd_eq a b =
+        let memo = Hashtbl.create 12 in
+        let rec f (na, nb) =
+          try Hashtbl.find memo (na, nb)
+          with Not_found -> let r =
+            match na, nb with
+            | DBot, DBot -> true
+            | 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 (na, nb))
+                  la lb
+            | _ -> false
+          in Hashtbl.add memo (na, nb) r; r
+        in f (a.root, b.root)
 
 
     let test () =
@@ -303,21 +365,22 @@ end = struct
       ******************************* *)
     
     type env = {
-        rp          : rooted_prog;
-        opt         : cmdline_opt;
+        rp            : rooted_prog;
+        opt           : cmdline_opt;
 
-        ve          : varenv;
+        ve            : varenv;
 
         (* program expressions *)
-        f           : bool_expr;
-        cl          : conslist;
-        f_g         : bool_expr;
-        cl_g        : conslist;
-        guarantees  : (id * bool_expr) list;
+        f             : bool_expr;
+        cl            : conslist;
+        f_g           : bool_expr;
+        cl_g          : conslist;
+        guarantees    : (id * bool_expr) list;
 
         (* abstract interpretation *)
-        cycle       : (id * id * typ) list;     (* s'(x) = s(y) *)
-        forget      : (id * typ) list;          (* s'(x) not specified *)
+        cycle         : (id * id * typ) list;     (* s'(x) = s(y) *)
+        forget        : (id * typ) list;          (* s'(x) not specified *)
+        mutable data  : edd_v;
     }
 
     (*
@@ -328,7 +391,16 @@ end = struct
 
       A couple may appear several times in the result.
     *)
-    let rec extract_linked_evars (ecl, _, r) =
+    let rec extract_linked_evars_root (ecl, _, r) =
+        let v_ecl = List.fold_left
+            (fun c (_, x, v) -> match v with
+                | EIdent y -> (x, y)::c
+                | _ -> c)
+            [] ecl
+        in
+        v_ecl
+
+    let rec extract_linked_evars(ecl, _, r) =
         let v_ecl = List.fold_left
             (fun c (_, x, v) -> match v with
                 | EIdent y -> (x, y)::c
@@ -343,6 +415,7 @@ end = struct
           in
           match q with
           | [x; y] -> [x, y]
+          | [x; y; z] -> [x, y; y, z; z, x]
           | _ -> []
         in
         let rec aux = function
@@ -457,10 +530,15 @@ end = struct
 
         let lv0 = List.map (fun x -> x, "N"^x)
             (List.filter (fun x -> List.exists (fun y -> y = "N"^x) evars) evars) in
-        let lv = lv0 @ extract_linked_evars init_cl @ extract_linked_evars cl_g in
-        let lv = uniq_sorted
-             (List.sort Pervasives.compare (List.map ord_couple lv)) in
-        let evars_ord = scope_constrict evars (lv0 @ lv) in
+        let lv1 = extract_linked_evars_root init_cl
+            @ extract_linked_evars_root cl_g in
+        let lv2 = extract_linked_evars init_cl @ extract_linked_evars cl_g in
+
+        let lv1 = uniq_sorted
+             (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 = scope_constrict evars (lv0 @ lv1 @ lv2) in
 
         let ev_order = Hashtbl.create (List.length evars) in
         List.iteri (fun i x -> Hashtbl.add ev_order x i) evars_ord;
@@ -484,16 +562,21 @@ end = struct
               rp.all_vars)
         in
 
+        (* calculate initial environment *)
+        let data = edd_apply_cl (edd_top ve) init_cl in
+        Format.printf "Init: @[<hov>%a@]@." edd_print data;
+
         { rp; opt; ve;
           f; cl; f_g; cl_g; guarantees;
-          cycle; forget }
+          cycle; forget; data }
 
           
 
 
     let do_prog opt rp =
         let e = init_env opt rp in
-        ()
+        let d2 = edd_apply_cl e.data e.cl in
+        Format.printf " -> @[<hov>%a@]@." edd_print d2
 
 end
 
diff --git a/abstract/nonrelational.ml b/abstract/nonrelational.ml
index 3e978ce..b3129c0 100644
--- a/abstract/nonrelational.ml
+++ b/abstract/nonrelational.ml
@@ -201,21 +201,25 @@ module ND (V : VALUE_DOMAIN) : NUMERICAL_ENVIRONMENT_DOMAIN = struct
               | _::q -> bl q
             in
             let sbl = bl s in
-            Format.fprintf fmt "@[<v 2>{ ";
-            List.iteri
-              (fun j (v, ids) ->
-                if j > 0 then Format.fprintf fmt "@ ";
-                Format.fprintf fmt "@[<hov 4>";
-                List.iteri
-                  (fun i id ->
-                    if i > 0 then Format.fprintf fmt ",@ ";
-                    Format.fprintf fmt "%a" Formula_printer.print_id id)
-                  ids;
-                match V.as_const v with
-                | Some i -> Format.fprintf fmt " = %d@]" i
-                | _ -> Format.fprintf fmt " ∊ %s@]" (V.to_string v))
-              sbl;
-            Format.fprintf fmt " }@]"
+            if sbl = [] then
+              Format.fprintf fmt "⊤"
+            else begin
+              Format.fprintf fmt "@[<v 2>{ ";
+              List.iteri
+                (fun j (v, ids) ->
+                  if j > 0 then Format.fprintf fmt "@ ";
+                  Format.fprintf fmt "@[<hov 4>";
+                  List.iteri
+                    (fun i id ->
+                      if i > 0 then Format.fprintf fmt ",@ ";
+                      Format.fprintf fmt "%a" Formula_printer.print_id id)
+                    ids;
+                  match V.as_const v with
+                  | Some i -> Format.fprintf fmt " = %d@]" i
+                  | _ -> Format.fprintf fmt " ∊ %s@]" (V.to_string v))
+                sbl;
+              Format.fprintf fmt " }@]"
+            end
 
     let print fmt x =
         print_vars fmt x (List.map fst (vars x))