1 files changed, 101 insertions, 85 deletions

diff --git a/abstract/abs_interp_edd.ml b/abstract/abs_interp_edd.ml
index 3ff91a6..4f2ad81 100644
--- a/abstract/abs_interp_edd.ml
+++ b/abstract/abs_interp_edd.ml
@@ -11,8 +11,6 @@ module I (ND : NUMERICAL_ENVIRONMENT_DOMAIN) : sig
 
     val do_prog : cmdline_opt -> rooted_prog -> unit
 
-    val test : unit -> unit
-
 end = struct
 
 
@@ -31,10 +29,11 @@ end = struct
         ev_order      : (id, int) Hashtbl.t;
     }
 
-    type edd =
+    type edd_node =
         | DBot
         | DVal of int
         | DChoice of id * (item * edd) list
+    and edd = int * edd_node
 
     type edd_v = {
         ve            : varenv;
@@ -43,40 +42,66 @@ end = struct
         (* add here eventual annotations *)
     }
 
+    (*
+      Utility functions for memoization
+
+      memo : (((int * 'a) -> (int * 'b)) -> 'a -> 'b) -> (int * 'a) -> (int * 'b)
+      memo2 : (((int * 'a) -> (int * 'b) -> (int * 'c)) -> 'a -> 'b -> 'c) -> (int * 'a) -> (int * 'b) -> (int * 'c)
+    *)
+    let memo f =
+        let n = ref 0 in
+        let memo = Hashtbl.create 12 in
+        let rec ff (id, v) =
+          try Hashtbl.find memo id
+          with Not_found ->
+            let r = f ff v in
+            incr n;
+            Hashtbl.add memo id (n, r);
+            n, r
+        in ff
           
+    let memo2 f =
+        let n = ref 0 in
+        let memo = Hashtbl.create 12 in
+        let rec ff (id1, v1) (id2, v2) =
+          try Hashtbl.find memo (id1, id2)
+          with Not_found ->
+            let r = f ff v1 v2 in
+            incr n;
+            Hashtbl.add memo (id1, id2) (n, r);
+            n, r
+        in ff
 
     (*
       edd_print : Format.formatter -> edd_v -> unit
     *)
     let edd_print fmt v =
-        let ids = Hashtbl.create 12 in
-        let n = ref 0 in
-        let rec mkid = function
-            | DChoice(_, l) as x ->
-              if not (Hashtbl.mem ids x) then begin
-                incr n; Hashtbl.add ids x !n;
-                List.iter (fun (_, x) -> mkid x) l
+        let c_nodes = Hashtbl.create 12 in
+        let rec add = function
+            | n, (DChoice(_, l) as x) ->
+              if not (Hashtbl.mem c_nodes n) then begin
+                Hashtbl.add c_nodes n x;
+                List.iter (fun (_, y) -> add y) l
               end
             | _ -> ()
-        in mkid v.root;
+        in add v.root;
+
         let print_n fmt = function
-          | DBot -> Format.fprintf fmt "⊥";
-          | DVal i -> Format.fprintf fmt "v%d" i;
-          | DChoice _ as x -> Format.fprintf fmt "n%d" (Hashtbl.find ids x)
+          | (_, DBot) -> Format.fprintf fmt "⊥";
+          | (_, DVal i) -> Format.fprintf fmt "v%d" i;
+          | (n, DChoice _) -> Format.fprintf fmt "n%d" n
         in
         Format.fprintf fmt "Root: %a@." print_n v.root;
-        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
+
+        Hashtbl.iter
+          (fun id x -> 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: %a ? @[<hov>%a@]@."
                     id Formula_printer.print_id var
                     (print_list p ", ") l
-              | _ -> assert false
-        done;
+              | _ -> assert false)
+          c_nodes;
         Hashtbl.iter
             (fun id v -> Format.fprintf fmt "v%d: %a@." id ND.print v)
             v.leaves
@@ -86,7 +111,7 @@ end = struct
     (*
       edd_bot : varenv -> edd_v
     *)
-    let edd_bot ve = { ve; root = DBot; leaves = Hashtbl.create 1 }
+    let edd_bot ve = { ve; root = (0, DBot); leaves = Hashtbl.create 1 }
 
     (*
       edd_top : evar list -> nvar list -> edd_v
@@ -94,7 +119,7 @@ end = struct
     let edd_top ve =
         let leaves = Hashtbl.create 1 in
         Hashtbl.add leaves 0 (ND.top ve.nvars);
-        { ve; root = DVal 0; leaves }
+        { ve; root = (1, DVal 0); leaves }
 
     (*
       edd_of_cons : varenv -> enum_cons -> edd_v
@@ -105,23 +130,27 @@ end = struct
         let leaves = Hashtbl.create 1 in
         Hashtbl.add leaves 0 (ND.top ve.nvars);
 
+        let bot, top = (0, DBot), (1, DVal 0) in
+
         let root = match r with
         | EItem x ->
-          DChoice(vid,
-            List.map (fun v -> if op v x then v, DVal 0 else v, DBot)
-              (List.assoc vid ve.evars))      
+          2, DChoice(vid,
+              List.map (fun v -> if op v x then v, bot else v, top)
+                (List.assoc vid ve.evars))      
         | EIdent vid2 ->
             let a, b =
                 if Hashtbl.find ve.ev_order vid < Hashtbl.find ve.ev_order vid2
                   then vid, vid2
                   else vid2, vid
             in
+            let n = ref 2 in
             let nb x =
-              DChoice(b,
-                List.map (fun v -> if op v x then v, DVal 0 else v, DBot)
-                  (List.assoc b ve.evars))
+              incr n;
+              !n, DChoice(b,
+                    List.map (fun v -> if op v x then v, top else v, bot)
+                      (List.assoc b ve.evars))
             in
-            DChoice(a, List.map (fun x -> x, nb x) (List.assoc a ve.evars))
+            2, DChoice(a, List.map (fun x -> x, nb x) (List.assoc a ve.evars))
         in
         { ve; root; leaves }
 
@@ -131,10 +160,9 @@ end = struct
     let edd_join a b =
         let ve = a.ve in
 
-        let leaves = Hashtbl.copy a.leaves in
-        let n = ref 0 in
-        Hashtbl.iter (fun i _ -> if i > !n then n := i) leaves;
+        let leaves = Hashtbl.create 12 in
 
+        let n = 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;
@@ -147,61 +175,47 @@ end = struct
           end
         in
 
-        let memo_bcopy = Hashtbl.create 12 in
-        let rec bcopy nb =
-          try Hashtbl.find memo_bcopy nb
-          with Not_found -> let r =
-            match nb with
-            | DBot -> DBot
-            | DVal i -> get_leaf (Hashtbl.find b.leaves i)
-            | DChoice (v, x) ->
-              DChoice(v, List.map (fun (c, n) -> c, bcopy n) x)
-          in Hashtbl.add memo_bcopy nb r; r
-        in
 
-        let memo = Hashtbl.create 12 in
-        let rec f (na, nb) =
-          try Hashtbl.find memo (na, nb)
-          with Not_found -> let r =
-            let dq v l =
-              let _, x0 = List.hd l in
-              if List.exists (fun (_, x) -> x <> x0) l
-                then DChoice(v, l)
-                else x0
+        let f f_rec na nb =
+          let dq v l =
+            let _, (i, x0) = List.hd l in
+            if List.exists (fun (_, (j, x)) -> j <> i || x <> x0) l
+              then DChoice(v, l)
+              else x0
+          in
+          match na, nb with
+          | DBot, DBot -> DBot
+          | DBot, DVal i -> get_leaf (Hashtbl.find b.leaves i)
+          | x, DBot -> x
+
+          | DChoice(va, la), DChoice(vb, lb) when va = vb ->
+            let kl = List.map2
+                (fun (ta, ba) (tb, bb) -> assert (ta = tb);
+                  ta, f (ba, bb))
+                la lb
             in
-            match na, nb with
-            | DBot, x -> bcopy x
-            | x, DBot -> x
-
-            | DChoice(va, la), DChoice(vb, lb) when va = vb ->
-              let kl = List.map2
-                  (fun (ta, ba) (tb, bb) -> assert (ta = tb);
-                    ta, f (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 (ca, nb)) la
-                else
-                  vb, List.map (fun (k, cb) -> k, f (na, cb)) lb
-              in
-              dq v kl
-
-            | DChoice(va, la), _ ->
-              let kl = List.map (fun (k, ca) -> k, f (ca, nb)) la in
-              dq va kl
-            | _, DChoice(vb, lb) ->
-              let kl = List.map (fun (k, cb) -> k, f (na, cb)) lb in
-              dq vb kl
-
-            | DVal u, DVal v ->
-              let x = ND.join (Hashtbl.find a.leaves u) (Hashtbl.find b.leaves v) in
-              get_leaf x
-          in Hashtbl.add memo (na, nb) r; r
+            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 (ca, nb)) la
+              else
+                vb, List.map (fun (k, cb) -> k, f (na, cb)) lb
+            in
+            dq v kl
+
+          | DChoice(va, la), _ ->
+            let kl = List.map (fun (k, ca) -> k, f (ca, nb)) la in
+            dq va kl
+          | _, DChoice(vb, lb) ->
+            let kl = List.map (fun (k, cb) -> k, f (na, cb)) lb in
+            dq vb kl
+
+          | DVal u, DVal v ->
+            let x = ND.join (Hashtbl.find a.leaves u) (Hashtbl.find b.leaves v) in
+            get_leaf x
         in
-        { leaves; ve; root = f (a.root, b.root) }
+        { leaves; ve; root = memo2 f a.root b.root }
 
     (*
       edd_meet : edd_v -> edd_v -> edd_v
@@ -342,6 +356,7 @@ end = struct
         in f (a.root, b.root)
 
 
+    (*
     let test () =
         let ve = {
             evars = ["x", ["tt"; "ff"]; "y", ["tt"; "ff"]; "z", ["tt"; "ff"]];
@@ -358,6 +373,7 @@ end = struct
         Format.printf "x = y && y != z : @[%a@]@." edd_print w;
         let t = edd_join u v in
         Format.printf "x = y || y != z : @[%a@]@." edd_print t
+    *)
 
 
     (* ******************************