Reached interesting point in BDD implementation.

5 files changed, 121 insertions, 111 deletions

diff --git a/abstract/abs_interp_edd.ml b/abstract/abs_interp_edd.ml
index 863a22d..ebf7549 100644
--- a/abstract/abs_interp_edd.ml
+++ b/abstract/abs_interp_edd.ml
@@ -13,6 +13,9 @@ let time id f =
   Format.printf "] @?";
   r
 
+
+exception Top
+
 module I (ND : NUMERICAL_ENVIRONMENT_DOMAIN) : sig
 
     val do_prog : cmdline_opt -> rooted_prog -> unit
@@ -39,6 +42,7 @@ end = struct
 
     type edd =
         | DBot
+        | DTop
         | DVal of int
         | DChoice of int * id * (item * edd) list
 
@@ -60,9 +64,10 @@ end = struct
       Where 'a = 'b = 'c = edd, but it can be adapted.
     *)
     let key = function
-        | DBot -> None
-        | DVal i -> Some (Left i)
-        | DChoice(i, _, _) -> Some (Right i)
+        | DBot -> 0
+        | DTop -> 1
+        | DVal i -> 2 * i + 2
+        | DChoice(i, _, _) -> 2 * i + 3
 
     let memo f =
         let memo = Hashtbl.create 12 in
@@ -84,6 +89,7 @@ end = struct
 
     let edd_node_eq = function
         | DBot, DBot -> true
+        | DTop, DTop -> true
         | DVal i, DVal j when i = j -> true
         | DChoice(i, _, _), DChoice(j, _, _) when i = j -> true
         | _ -> false
@@ -108,6 +114,7 @@ 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;
           | DChoice(n, _, _) -> Format.fprintf fmt "n%d" n
@@ -140,10 +147,7 @@ end = struct
     (*
       edd_top : evar list -> nvar list -> edd_v
     *)
-    let edd_top ve =
-        let leaves = Hashtbl.create 1 in
-        Hashtbl.add leaves 0 (ND.top ve.nvars);
-        { ve; root = DVal 0; leaves }
+    let edd_top ve = { ve; root = DTop; leaves = Hashtbl.create 1 }
 
     (*
       edd_of_cons : varenv -> enum_cons -> edd_v
@@ -152,14 +156,11 @@ end = struct
         let op = match op with | E_EQ -> (=) | E_NE -> (<>) in
 
         let leaves = Hashtbl.create 1 in
-        Hashtbl.add leaves 0 (ND.top ve.nvars);
-
-        let bot, top = DBot, DVal 0 in
 
         let root = match r with
         | EItem x ->
           DChoice(0, vid,
-              List.map (fun v -> if op v x then v, top else v, bot)
+              List.map (fun v -> if op v x then v, DTop else v, DBot)
                 (List.assoc vid ve.evars))      
         | EIdent vid2 ->
             let a, b =
@@ -171,7 +172,7 @@ end = struct
             let nb x =
               incr n;
               DChoice(!n, b,
-                    List.map (fun v -> if op v x then v, top else v, bot)
+                    List.map (fun v -> if op v x then v, DTop else v, DBot)
                       (List.assoc b ve.evars))
             in
             DChoice(0, a, List.map (fun x -> x, nb x) (List.assoc a ve.evars))
@@ -179,44 +180,49 @@ 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 a b =
+    let edd_join_meet op a b =
         let ve = a.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)
+          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 f f_rec na nb =
-          let dq v l =
-            let _, x0 = List.hd l in
-            if List.exists (fun (_, x) -> not (edd_node_eq (x, x0))) l
-              then begin
-                incr nc; DChoice(!nc, v, l)
-              end else x0
-          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 =
           match na, nb with
+          | DTop, _ | _, DTop -> DTop
           | DBot, DBot -> DBot
-          | 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 x = ND.join (Hashtbl.find a.leaves u) (Hashtbl.find b.leaves v) in
-            get_leaf x
 
           | DChoice(_, va, la), DChoice(_, vb, lb) when va = vb ->
             let kl = List.map2
@@ -234,6 +240,14 @@ end = struct
             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 x = 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
@@ -241,44 +255,11 @@ 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) }
-
-    (*
-      edd_meet : edd_v -> edd_v -> edd_v
-    *)
-    let edd_meet a b =
-        let ve = a.ve in
 
-        let lc = 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 lc;
-              Hashtbl.add leaves !lc x;
-              DVal (!lc)
-          end
-        in
-
-        let nc = ref 0 in
-        let f f_rec na nb =
-          let dq v l =
-            let _, x0 = List.hd l in
-            if List.exists (fun (_, x) -> not (edd_node_eq (x, x0))) l
-              then begin
-                incr nc; DChoice(!nc, v, l)
-              end else x0
-          in
+        let f_meet f_rec na nb =
           match na, nb with
           | DBot, _ | _, DBot -> DBot
-          | DVal u, DVal v ->
-            let x = ND.meet (Hashtbl.find a.leaves u) (Hashtbl.find b.leaves v) in
-            get_leaf x
+          | DTop, DTop -> DTop
 
           | DChoice(_, va, la), DChoice(_, vb, lb) when va = vb ->
             let kl = List.map2
@@ -295,6 +276,15 @@ end = struct
                 vb, List.map (fun (k, cb) -> k, f_rec na cb) lb
             in
             dq v kl
+
+          | DTop, DVal i ->
+            get_leaf (Hashtbl.find b.leaves i)
+          | DVal i, DTop ->
+            get_leaf (Hashtbl.find a.leaves i)
+          | DVal u, DVal v ->
+            let x = ND.meet (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
@@ -302,7 +292,16 @@ end = struct
             let kl = List.map (fun (k, cb) -> k, f_rec na cb) lb in
             dq vb kl
         in
-        { leaves; ve; root = time "meet" (fun () -> memo2 f a.root b.root) }
+
+        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
+
+
 
     (*
       edd_num_apply : edd_v -> (ND.t -> ND.t) -> edd_v
@@ -330,6 +329,7 @@ end = struct
         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))
           | DChoice(n, var, l) ->
             let l = List.map (fun (k, v) -> k, f_rec v) l in
@@ -357,6 +357,7 @@ end = struct
         in
         let cons_edd = cl_k ec in
         edd_meet v cons_edd
+        (*List.fold_left (fun v c -> edd_meet v (edd_of_cons v.ve c)) v ec*)
 
     (*
       edd_apply_cl : edd_v -> conslist -> edd_v
@@ -381,6 +382,7 @@ end = struct
         let f f_rec na nb =
           match na, nb with
           | DBot, DBot -> true
+          | DTop, DTop -> 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 ->
@@ -417,45 +419,48 @@ end = struct
             let kl = List.sort Pervasives.compare (List.map key l) in
             try Hashtbl.find memo kl
             with Not_found -> let r =
-              let cn, fn = List.fold_left
-                (fun (cn, fn) node -> match node with
-                  | DBot -> cn, fn
-                  | DVal i -> cn, i::fn
-                  | DChoice (n, v, l) -> (n, v, l)::cn, fn)
-                ([], []) l in
-              let cn = List.sort
-                (fun (n, v1, _) (n, v2, _) -> Pervasives.compare
-                    (Hashtbl.find ve.ev_order v1) (Hashtbl.find ve.ev_order v2))
-                cn in
-              if cn = [] then
-                if fn = [] then DBot
-                else
-                  let x = list_fold_op ND.join
-                      (List.map (Hashtbl.find v.leaves) fn)
-                  in get_leaf x
-              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
-                let ch2 = List.map (fun i -> DVal i) fn in
-                if List.mem dv vars then
-                  (* Do union of all branches branching from nodes on variable dv *)
-                  let ch3 = List.flatten
-                    (List.map (fun (_, _, c) -> List.map snd c) d) in
-                  f (ch1@ch2@ch3)
+              try
+                let cn, fn = List.fold_left
+                  (fun (cn, fn) node -> match node with
+                    | DBot -> cn, fn
+                    | DTop -> raise Top
+                    | DVal i -> cn, i::fn
+                    | DChoice (n, v, l) -> (n, v, l)::cn, fn)
+                  ([], []) l in
+                let cn = List.sort
+                  (fun (n, v1, _) (n, v2, _) -> Pervasives.compare
+                      (Hashtbl.find ve.ev_order v1) (Hashtbl.find ve.ev_order v2))
+                  cn in
+                if cn = [] then
+                  if fn = [] then DBot
+                  else
+                    let x = list_fold_op ND.join
+                        (List.map (Hashtbl.find v.leaves) fn)
+                    in get_leaf x
                 else
-                  (* Keep disjunction on variable dv *)
+                  let _, dv, cl = List.hd cn in
                   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
-                      c, f (ch1@ch2@ch3))
-                    cl in
-                  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)
-                  end else x0
+                  let ch1 = List.map (fun (a, b, c) -> DChoice(a, b, c)) nd in
+                  let ch2 = List.map (fun i -> DVal i) fn in
+                  if List.mem dv vars then
+                    (* Do union of all branches branching from nodes on variable dv *)
+                    let ch3 = List.flatten
+                      (List.map (fun (_, _, c) -> List.map snd c) d) in
+                    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
+                        c, f (ch1@ch2@ch3))
+                      cl in
+                    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)
+                    end else x0
+              with | Top -> DTop
             in Hashtbl.add memo kl r; r
         in
         { leaves; ve; root = f [v.root] }
diff --git a/abstract/apron_domain.ml b/abstract/apron_domain.ml
index 7a823db..45803fc 100644
--- a/abstract/apron_domain.ml
+++ b/abstract/apron_domain.ml
@@ -71,6 +71,7 @@ module ND : NUMERICAL_ENVIRONMENT_DOMAIN = struct
       Abstract1.top manager (v_env vars)
     let bottom vars = Abstract1.bottom manager (v_env vars)
     let is_bot = Abstract1.is_bottom manager
+    let is_top = Abstract1.is_top manager
 
     let forgetvar x id =
         let v = [| Var.of_string id |] in
diff --git a/abstract/nonrelational.ml b/abstract/nonrelational.ml
index b3129c0..7a83303 100644
--- a/abstract/nonrelational.ml
+++ b/abstract/nonrelational.ml
@@ -57,6 +57,9 @@ module ND (V : VALUE_DOMAIN) : NUMERICAL_ENVIRONMENT_DOMAIN = struct
     let is_bot env = match env with
         | Bot -> true
         | Env env -> strict env = Bot
+    let is_top env = match env with
+        | Bot -> false
+        | Env e -> VarMap.for_all (fun _ v -> v = V.top) e
 
     let forgetvar x id = strict_apply (fun y -> Env (VarMap.add id V.top y)) x
 
diff --git a/abstract/num_domain.ml b/abstract/num_domain.ml
index 96de8bc..285b3c4 100644
--- a/abstract/num_domain.ml
+++ b/abstract/num_domain.ml
@@ -10,6 +10,7 @@ module type NUMERICAL_ENVIRONMENT_DOMAIN = sig
     val bottom      : (id * bool) list -> t
     val vbottom     : t -> t       (* bottom value with same variables *)
     val is_bot      : t -> bool
+    val is_top      : t -> bool
 
     (* variable management *)
     val vars        : t -> (id * bool) list
diff --git a/tests/source/uturn.scade b/tests/source/uturn.scade
index 84c9b51..97c2fdb 100644
--- a/tests/source/uturn.scade
+++ b/tests/source/uturn.scade
@@ -64,8 +64,8 @@ let
   assume h3: empty_section -> true;
   assume h4: true -> implies(edge(not empty_section), pre grant_access);
   assume h5: true -> implies(edge(on_C), pre grant_exit);
-  assume h6: implies(edge(not on_A), on_B);
-  assume h7: implies(edge(not on_B), on_A or on_C);
+  assume h6: true -> implies(edge(not on_A), on_B);
+  assume h7: true -> implies(edge(not on_B), on_A or on_C);
 
   grant_access, grant_exit, do_AB, do_BC = UMS(on_A, on_B, on_C, ack_AB, ack_BC);