Implement stand-alone EDDs

5 files changed, 372 insertions, 232 deletions

diff --git a/Makefile b/Makefile
index 3e5d01a..a6cc2d8 100644
--- a/Makefile
+++ b/Makefile
@@ -18,6 +18,7 @@ SRC= 	main.ml \
 		abstract/apron_domain.ml \
 		abstract/num_domain.ml \
 		abstract/enum_domain.ml \
+		abstract/enum_domain_edd.ml \
 		\
 		abstract/formula.ml \
 		abstract/formula_printer.ml \
diff --git a/abstract/abs_interp_edd.ml b/abstract/abs_interp_edd.ml
index 8ea0012..1b3bb39 100644
--- a/abstract/abs_interp_edd.ml
+++ b/abstract/abs_interp_edd.ml
@@ -47,7 +47,6 @@ end = struct
         ve            : varenv;
         root          : edd;
         leaves        : (int, ND.t) Hashtbl.t;
-        (* add here eventual annotations *)
     }
 
     (*
@@ -529,7 +528,6 @@ end = struct
                     f (ch1@ch2@ch3)
                   else
                     (* Keep disjunction on variable dv *)
-                    let d, nd = List.partition (fun (_, v, _) -> v = dv) cn in
                     let cc = List.map
                       (fun (c, _) ->
                         let ch3 = List.map (fun (_, _, cl) -> List.assoc c cl) d in
diff --git a/abstract/enum_domain.ml b/abstract/enum_domain.ml
index d216276..ea2b053 100644
--- a/abstract/enum_domain.ml
+++ b/abstract/enum_domain.ml
@@ -264,233 +264,3 @@ module MultiValuation : ENUM_ENVIRONMENT_DOMAIN = struct
 end
 
 
-(*
-    Complicated domain : a set of values for each variables, plus some
-    constraints on couples of variables
-      (eg. (x, y) in [ tt, tt ; ff, ff ]
-
-    WARNING : This domain is not proved to be safe. In particular, it may represent
-    a set of contraints that imply Bot (ie that are impossible) without raising the
-    Bot exception. (there is potentially exponential cost in the checking that all
-    the constraints are coherent, and I have no idea of an algorithm for doing that
-    check.)
-
-    Therefore, do not use this domain unless you know what you are doing (which is
-    probably not the case anyway).
-*)
-
-module MultiValuationCCons : ENUM_ENVIRONMENT_DOMAIN = struct
-
-    module VarC = struct
-        type t = id * id
-        let compare = Pervasives.compare
-    end
-    module VarCMap = Mapext.Make(VarC)
-
-    type item = string
-
-    type t = {
-        vars      : (id * item list) list;
-        value     : item list VarMap.t;
-
-        (* in ccond (x, y) -> l, must have x < y (textual order on identifiers) -> unicity *)
-        ccons     : (item * item) list VarCMap.t;
-    }
-
-    let sort = List.sort Pervasives.compare
-    let uniq x = uniq_sorted (sort x)
-    let list_inter x y = List.filter (fun k -> List.mem k y) x
-
-    let all_couples l1 l2 =
-        List.flatten
-          (List.map (fun x -> List.map (fun y -> x, y) l2) l1)
-
-    let top vars = { vars; value = VarMap.empty; ccons = VarCMap.empty }
-
-    let vars x = x.vars
-
-    let forgetvar x id =
-        (* TODO : try to find a substitution variable so that some contraints can be propagated.
-                  this is important so that cycle passing can be done correctly ! *)
-        { x with
-          value = VarMap.remove id x.value;
-          ccons = VarCMap.filter (fun (a, b) _ -> a <> id && b <> id) x.ccons }
-
-    let project x id =
-        try VarMap.find id x.value
-        with Not_found -> List.assoc id x.vars
-
-    let project2 x id1 id2 =
-        try
-          let id1', id2' = ord_couple (id1, id2) in
-          if id1' = id1 then
-            VarCMap.find (id1, id2) x.ccons
-          else
-            List.map (fun (a, b) -> b, a) (VarCMap.find (id1', id2') x.ccons)
-        with _ ->
-          let v1, v2 = project x id1, project x id2 in
-          all_couples v1 v2
-
-    let strict x =
-        let rec f x =
-          (*
-              - if (x, y) in [ a, b1 ; a, b2 ; ... ; a, bn ],
-                  replace this by x = a and y in { b1, ..., bn }
-              - filter (x, y) in [ ... ] with x in specified itv, y in specified itv
-          *)
-          let usefull, vv, cc =
-            VarCMap.fold
-              (fun (x, y) l (usefull, vv, cc) ->
-                  let p1, p2 = uniq (List.map fst l), uniq (List.map snd l) in
-                  let p1 = try list_inter p1 (VarMap.find x vv) with _ -> p1 in
-                  let p2 = try list_inter p2 (VarMap.find y vv) with _ -> p2 in
-
-                  if p1 = [] || p2 = [] then raise Bot;
-                  let vv = VarMap.add x p1 (VarMap.add y p2 vv) in
-
-                  if List.length p1 = 1 || List.length p2 = 1
-                  then
-                    true, vv, cc
-                  else
-                    match List.filter (fun (u, v) -> List.mem u p1 && List.mem v p2) l with
-                    | [] -> raise Bot
-                    | l2 -> List.length l2 < List.length l, vv, VarCMap.add (x, y) l2 cc)
-              x.ccons (false, x.value, VarCMap.empty) in
-
-          let x = { x with value = vv; ccons = cc } in
-          if usefull then f x else x
-        in
-        f x
-
-    let join x1 x2 =
-        let v = VarMap.merge
-          (fun _ a b -> match a, b with
-            | Some a, Some b -> Some (uniq (a@b))
-            | _ -> None)
-          x1.value x2.value in
-        let x = { x1 with value = v } in
-
-        let cc = VarCMap.merge
-          (fun (id1, id2) l1 l2 ->
-              let v1, v2 = project x1 id1, project x id2 in
-              let ac = all_couples v1 v2 in
-              let c = List.filter
-                  (fun q ->
-                    (match l1 with Some l -> List.mem q l | _ -> true) ||
-                    (match l2 with Some l -> List.mem q l | _ -> true))
-                  ac in 
-              if List.length c < List.length ac then Some c else None)
-          x1.ccons x2.ccons in
-
-        strict { x with ccons = cc }
-
-    let meet x1 x2 =
-        let v = VarMap.merge
-          (fun _ a b -> match a, b with
-            | Some a, None | None, Some a -> Some a
-            | Some a, Some b ->
-              begin match list_inter a b with
-              | [] -> raise Bot | l -> Some l end
-            | _ -> None)
-          x1.value x2.value in
-        let x = { x1 with value = v } in 
-
-        let cc = VarCMap.merge
-          (fun (id1, id2) l1 l2 ->
-              let v1, v2 = project x id1, project x id2 in
-              let ac = all_couples v1 v2 in
-              let c1 = match l1 with Some l -> list_inter l ac | None -> ac in
-              let c2 = match l2 with Some l -> list_inter l ac | None -> ac in
-              match list_inter c1 c2 with
-              | [] -> raise Bot
-              | l -> if List.length l < List.length ac then Some l else None)
-          x1.ccons x2.ccons in
-
-        strict { x with ccons = cc }
-
-    let subset a b =
-        VarMap.for_all
-          (fun id v ->
-              let vs = project a id in
-              List.for_all (fun c -> List.mem c vs) v)
-          b.value
-        &&
-        VarCMap.for_all
-          (fun (id1, id2) l ->
-              let l2 = project2 a id1 id2 in
-              List.for_all (fun c -> List.mem c l) l2)
-          b.ccons
-    let eq a b =
-      subset a b && subset b a
-
-    let apply_cons x (op, id, e) =
-        let op = match op with | E_EQ -> (=) | E_NE -> (<>) in
-        
-        match e with
-        | EItem s ->
-          let pv = project x id in
-          begin match List.filter (op s) pv with
-          | [] -> []
-          | vals -> try [strict { x with value = VarMap.add id vals x.value }] with Bot -> []
-          end
-        | EIdent id2 ->
-          let id, id2 = ord_couple (id, id2) in
-          let c = project2 x id id2 in
-          let ok_c = List.filter (fun (a, b) -> op a b) c in
-          try
-            [match uniq (List.map fst ok_c), uniq (List.map snd ok_c) with
-              | [], _ | _, [] -> raise Bot
-              | [a], q -> strict { x with value = VarMap.add id [a] (VarMap.add id2 q x.value) }
-              | q, [b] -> strict { x with value = VarMap.add id q (VarMap.add id2 [b] x.value) }
-              | _ -> strict { x with ccons = VarCMap.add (id, id2) ok_c x.ccons}
-            ]
-          with Bot -> []
-    
-    let assign x idl =
-        let x2 = List.fold_left (fun x (v, _) -> forgetvar x v) x idl in
-        let v = List.fold_left
-            (fun v (id, id2) ->
-                try VarMap.add id (VarMap.find id2 x.value) v
-                with Not_found -> v)
-            x2.value idl in
-        let c = VarCMap.fold
-            (fun (v1, v2) l c ->
-                let v1' = try List.assoc v1 idl with _ -> v1 in
-                let v2' = try List.assoc v2 idl with _ -> v2 in
-                VarCMap.add (v1', v2') l c)
-            x.ccons x2.ccons in
-        strict { x with value = v; ccons = c }
-
-
-    let print fmt x =
-        let b = List.map (fun (x, y) -> y, x) (VarMap.bindings x.value) in
-        let s = List.sort Pervasives.compare b in
-        let rec bl = function
-          | [] -> []
-          | (v, id)::q ->
-            let v = sort v in
-            if v <> sort (List.assoc id x.vars) then
-              match bl q with
-              | (vv, ids)::q when vv = v -> (v, id::ids)::q
-              | r -> (v, [id])::r
-            else
-              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 with
-            | [v0] -> Format.fprintf fmt " ≡ %s@]" v0
-            | l -> Format.fprintf fmt " ∊ @[<hov>{ %a }@]@]" (print_list Format.pp_print_string ", ") l)
-          sbl;
-        Format.fprintf fmt " }@]"
-
-end
diff --git a/abstract/enum_domain_edd.ml b/abstract/enum_domain_edd.ml
new file mode 100644
index 0000000..60f2d3b
--- /dev/null
+++ b/abstract/enum_domain_edd.ml
@@ -0,0 +1,371 @@
+open Ast
+open Formula
+open Util
+open Enum_domain
+
+module EDD : ENUM_ENVIRONMENT_DOMAIN = struct
+    exception Top
+
+    type item = string
+
+    type edd =
+        | DBot
+        | DTop
+        | DChoice of int * id * (item * edd) list
+
+    type t = {
+      vars      : (id * item list) list;
+      order     : (id, int) Hashtbl.t;
+      root      : edd;
+    }
+
+    (* Utility functions for memoization *)
+    let key = function
+        | DBot -> -1
+        | DTop -> -2
+        | DChoice(i, _, _) -> i
+    
+    let memo f =
+        let memo = Hashtbl.create 12 in
+        let rec ff v =
+          try Hashtbl.find memo (key v)
+          with Not_found ->
+            let r = f ff v in
+            Hashtbl.add memo (key v) r; r
+        in ff
+          
+    let memo2 f =
+        let memo = Hashtbl.create 12 in
+        let rec ff v1 v2 =
+          try Hashtbl.find memo (key v1, key v2)
+          with Not_found ->
+            let r = f ff v1 v2 in
+            Hashtbl.add memo (key v1, key v2) r; r
+        in ff
+    
+    let edd_node_eq = function
+        | DBot, DBot -> true
+        | DTop, DTop -> true
+        | DChoice(i, _, _), DChoice(j, _, _) -> i = j
+        | _ -> 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 rank v = function
+        | DChoice(_, x, _) -> Hashtbl.find v.order x
+        | _ -> 10000000
+
+
+    (*
+      print : Format.formatter -> t -> unit
+    *)
+    let print fmt v =
+        let print_nodes = Queue.create () in
+        let a = Hashtbl.create 12 in
+
+        let node_pc = Hashtbl.create 12 in
+        let f f_rec = function
+          | DChoice(_, _, l) ->
+            List.iter
+              (fun (_, c) -> match c with
+                  | DChoice(n, _, _) ->
+                      begin try Hashtbl.add node_pc n (Hashtbl.find node_pc n + 1)
+                      with Not_found -> Hashtbl.add node_pc n 1 end
+                  | _ -> ())
+            l;
+            List.iter (fun (_, c) -> f_rec c) l
+          | _ -> ()
+        in memo f v.root;
+
+        let rec print_n fmt = function
+          | DBot -> Format.fprintf fmt "⊥";
+          | DTop -> Format.fprintf fmt "⊤";
+          | DChoice(_, v, l) ->
+            match List.filter (fun (_, x) -> x <> DBot) l with
+            | [(c, nn)] ->
+              let aux fmt = function
+                | DChoice(nn, _, _) as i when Hashtbl.find node_pc nn >= 2 ->
+                  if Hashtbl.mem a nn then () else begin
+                    Queue.push i print_nodes;
+                    Hashtbl.add a nn ()
+                  end;
+                  Format.fprintf fmt "n%d" nn
+                | x -> print_n fmt x
+              in
+              Format.fprintf fmt "%a = %s,@ %a" Formula_printer.print_id v c aux nn
+            | _ ->
+              Format.fprintf fmt "%a ? " Formula_printer.print_id v;
+              let print_u fmt (c, i) =
+                Format.fprintf fmt "%s → " c;
+                match i with
+                | DChoice(nn, v, l) ->
+                  if Hashtbl.mem a nn then () else begin
+                    Queue.push i print_nodes;
+                    Hashtbl.add a nn ()
+                  end;
+                  Format.fprintf fmt "n%d" nn
+                | _ -> Format.fprintf fmt "%a" print_n i
+              in
+              Format.fprintf fmt "@[<h>%a@]" (print_list print_u ", ") l;
+        in
+        Format.fprintf fmt "@[<v 4>{ @[<hov>%a@]" print_n v.root;
+        while not (Queue.is_empty print_nodes) do
+          match Queue.pop print_nodes with
+          | DChoice(n, v, l) as x ->
+            Format.fprintf fmt "@ n%d: @[<hov>%a@]" n print_n x
+          | _ -> assert false
+        done;
+        Format.fprintf fmt " }@]"
+
+    (*
+      top : (id * item list) list -> t
+    *)
+    let top vars =
+        let order = Hashtbl.create 12 in
+        List.iteri (fun i (id, _) -> Hashtbl.add order id i) vars;
+        { vars; order; root = DTop }
+    (*
+      vars : t -> (id * item list) list
+    *)
+    let vars x = x.vars
+         
+    (*
+      of_cons : t -> enum_cons -> t
+      The first t is NOT used as a decision function, here we only use
+      the variable ordering it provides.
+    *)
+    let of_cons v0 (op, vid, r) =
+        let op = match op with | E_EQ -> (=) | E_NE -> (<>) in
+
+        let root = match r with
+        | EItem x ->
+          DChoice(0, vid,
+              List.map (fun v -> if op v x then v, DTop else v, DBot)
+                (List.assoc vid v0.vars))      
+        | EIdent vid2 ->
+            let a, b =
+                if Hashtbl.find v0.order vid < Hashtbl.find v0.order vid2
+                  then vid, vid2
+                  else vid2, vid
+            in
+            let nc = ref 0 in
+            let nb x =
+              incr nc;
+              DChoice(!nc, b,
+                    List.map (fun v -> if op v x then v, DTop else v, DBot)
+                      (List.assoc b v0.vars))
+            in
+            DChoice(0, a, List.map (fun x -> x, nb x) (List.assoc a v0.vars))
+        in
+        { v0 with root = root }
+
+    (*
+      join : t -> t -> t
+      meet : t -> t -> t
+    *)
+    let join a b =
+        if a.root = DBot then b else
+        if b.root = DBot then a else
+        if a.root = DTop || b.root = DTop then { a with root = DTop } else begin
+          let dq = new_node_fun () in
+
+          let f f_rec na nb =
+            match na, nb with
+            | 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
+
+            | DTop, _ | _, DTop -> DTop
+            | DBot, DBot -> DBot
+
+            | DChoice(_,va, la), _ when rank a na < rank a nb ->
+              let kl = List.map (fun (k, ca) -> k, f_rec ca nb) la in
+              dq va kl
+            | _, DChoice(_, vb, lb) when rank a nb < rank a na ->
+              let kl = List.map (fun (k, cb) -> k, f_rec na cb) lb in
+              dq vb kl
+
+            | _ -> assert false
+          in
+            { a with root = memo2 f a.root b.root }
+        end
+
+    let meet a b =
+        if a.root = DTop then b else
+        if b.root = DTop then a else
+        if a.root = DBot || b.root = DBot then { a with root = DBot } else begin
+          let dq = new_node_fun () in
+
+          let f f_rec na nb =
+            match na, nb with
+            | 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
+
+            | DBot, _ | _, DBot -> DBot
+            | DTop, DTop -> DTop
+
+            | DChoice(_, va, la), _ when rank a na < rank a nb ->
+              let kl = List.map (fun (k, ca) -> k, f_rec ca nb) la in
+              dq va kl
+            | _, DChoice(_, vb, lb) when rank a nb < rank a na ->
+              let kl = List.map (fun (k, cb) -> k, f_rec na cb) lb in
+              dq vb kl
+
+            | _ -> assert false
+          in
+            {a with root = memo2 f a.root b.root }
+        end
+
+    (*
+      apply_cons : t -> enum_cons -> t
+      apply_cl : t -> enum_cons list -> t
+    *)
+    let apply_cons v x =
+      let v = meet v (of_cons v x) in
+      if v.root = DBot then [] else [v]
+    let apply_cl v ec =
+        let rec cl_k = function
+          | [] -> { v with root = DTop }
+          | [a] -> of_cons v a
+          | l ->
+            let n = ref 0 in
+            let la, lb = List.partition (fun _ -> incr n; !n mod 2 = 0) l in
+            meet (cl_k la) (cl_k lb)
+        in
+        let cons_edd = cl_k ec in
+        meet v cons_edd
+
+    (*
+      eq : edd_v -> edd_v -> bool
+    *)
+    let eq a b =
+        let f f_rec na nb =
+          match na, nb with
+          | DBot, DBot -> true
+          | DTop, DTop -> true
+          | DChoice(_, va, la), DChoice(_, vb, lb) when va = vb ->
+            List.for_all2 (fun (ca, na) (cb, nb) -> assert (ca = cb); f_rec na nb)
+                la lb
+          | _ -> false
+        in memo2 f a.root b.root
+
+    (*
+      subset : edd_v -> edd_v -> bool
+    *)
+    let subset a b =
+        let rank = rank a in
+        let f f_rec na nb =
+          match na, nb with
+          | DBot, _ -> true
+          | _, DTop -> true
+          | DTop, DBot -> false
+
+          | DChoice(_, va, la), DChoice(_, vb, lb) when va = vb ->
+            List.for_all2 (fun (ca, na) (cb, nb) -> assert (ca = cb); f_rec na nb)
+              la lb
+          | DChoice(_, va, la), _ when rank na < rank nb ->
+            List.for_all (fun (c, n) -> f_rec n nb) la
+          | _, DChoice(_, vb, lb) when rank na > rank nb ->
+            List.for_all (fun (c, n) -> f_rec na n) lb
+          | _ -> assert false
+        in memo2 f a.root b.root
+
+    (*
+      forgetvars : t -> id list -> t
+    *)
+    let forgetvars v vars =
+        let dq = new_node_fun () in
+
+        let 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
+            with Not_found -> let r =
+              try
+                let cn = List.fold_left
+                  (fun cn node -> match node with
+                    | DBot -> cn
+                    | DTop -> raise Top
+                    | DChoice (n, v, l) -> (n, v, l)::cn)
+                  [] l in
+                let cn = List.sort
+                  (fun (n, v1, _) (n, v2, _) -> Pervasives.compare
+                      (Hashtbl.find v.order v1) (Hashtbl.find v.order v2))
+                  cn in
+                if cn = [] then
+                  DBot
+                else
+                  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
+                  if List.mem dv vars then
+                    (* Do union of all branches branching from nodes on variable dv *)
+                    let ch2 = List.flatten
+                      (List.map (fun (_, _, c) -> List.map snd c) d) in
+                    f (ch1@ch2)
+                  else
+                    (* Keep disjunction on variable dv *)
+                    let cc = List.map
+                      (fun (c, _) ->
+                        let ch2 = List.map (fun (_, _, cl) -> List.assoc c cl) d in
+                        c, f (ch1@ch2))
+                      cl in
+                    dq dv cc
+              with | Top -> DTop
+            in Hashtbl.add memo kl r; r
+        in
+        { v with root = f [v.root] }
+
+    let forgetvar v x = forgetvars v [x]
+
+    (*
+      project : t -> id -> item list
+    *)
+    let project v x =
+      try
+        let vals = ref [] in
+        let f f_rec = function
+          | DBot -> ()
+          | DChoice(_, var, l) when
+              Hashtbl.find v.order var < Hashtbl.find v.order x ->
+            List.iter (fun (_, c) -> f_rec c) l
+          | DChoice(_, var, l) when var = x ->
+            List.iter
+              (fun (v, l) ->
+                if l <> DBot && not (List.mem v !vals) then vals := v::(!vals))
+              l
+          | _ -> raise Top
+        in
+        memo f v.root; !vals
+      with Top -> List.assoc x v.vars
+
+    (*
+      assign : t -> (id * id) list -> t
+    *)
+    let assign v ids =
+      let v = forgetvars v (List.map fst ids) in
+      apply_cl v (List.map (fun (x, y) -> (E_EQ, x, EIdent y)) ids)
+
+end
diff --git a/tests/source/counters.scade b/tests/source/counters.scade
index 334bca1..334bca1 100755..100644
--- a/tests/source/counters.scade
+++ b/tests/source/counters.scade