Changes to parser ; EDD optimisations ; test cases.

1 files changed, 80 insertions, 71 deletions

diff --git a/abstract/abs_interp_edd.ml b/abstract/abs_interp_edd.ml
index fd31670..6220a0a 100644
--- a/abstract/abs_interp_edd.ml
+++ b/abstract/abs_interp_edd.ml
@@ -280,78 +280,86 @@ end = struct
       edd_meet : edd_v -> edd_v -> edd_v
     *)
     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 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 ve na < rank ve nb ->
-            let kl = List.map (fun (k, ca) -> k, f_rec ca nb) la in
-            dq va kl
-          | _, DChoice(_, vb, lb) when rank ve nb < rank ve na ->
-            let kl = List.map (fun (k, cb) -> k, f_rec 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
-          | DVal(u, _), DBot ->
-            get_leaf (Hashtbl.find a.leaves u)
-          | DBot, DVal(v, _) ->
-            get_leaf (Hashtbl.find b.leaves v)
-
-          | _ -> assert false (* so that OCaml won't complain ; all cases ARE handled *)
-        in
-          { leaves; ve; root = time "join" (fun () -> memo2 f a.root b.root) }
+        if a.root = DBot then b else
+        if b.root = DBot then a else
+        if a.root = DTop || b.root = DTop then edd_top a.ve else begin
+          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
+            | 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 ve na < rank ve nb ->
+              let kl = List.map (fun (k, ca) -> k, f_rec ca nb) la in
+              dq va kl
+            | _, DChoice(_, vb, lb) when rank ve nb < rank ve na ->
+              let kl = List.map (fun (k, cb) -> k, f_rec 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
+            | DVal(u, _), DBot ->
+              get_leaf (Hashtbl.find a.leaves u)
+            | DBot, DVal(v, _) ->
+              get_leaf (Hashtbl.find b.leaves v)
+
+            | _ -> assert false (* so that OCaml won't complain ; all cases ARE handled *)
+          in
+            { leaves; ve; root = time "join" (fun () -> memo2 f a.root b.root) }
+        end
 
     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
-          | 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 ve na < rank ve nb ->
-            let kl = List.map (fun (k, ca) -> k, f_rec ca nb) la in
-            dq va kl
-          | _, DChoice(_, vb, lb) when rank ve nb < rank ve na ->
-            let kl = List.map (fun (k, cb) -> k, f_rec na cb) lb in
-            dq vb kl
-
-          | DVal (u, _) , DVal (v, _) ->
-            let x = ND.meet (Hashtbl.find a.leaves u) (Hashtbl.find b.leaves v) in
-            get_leaf x
-          | DVal(u, _), DTop ->
-            get_leaf (Hashtbl.find a.leaves u)
-          | DTop, DVal(v, _) ->
-            get_leaf (Hashtbl.find b.leaves v)
-
-          | _ -> assert false (* see above *)
-        in
-          { leaves; ve; root = time "meet" (fun () -> memo2 f a.root b.root) }
+        if a.root = DTop then b else
+        if b.root = DTop then a else
+        if a.root = DBot || b.root = DBot then edd_bot a.ve else begin
+          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
+            | 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 ve na < rank ve nb ->
+              let kl = List.map (fun (k, ca) -> k, f_rec ca nb) la in
+              dq va kl
+            | _, DChoice(_, vb, lb) when rank ve nb < rank ve na ->
+              let kl = List.map (fun (k, cb) -> k, f_rec na cb) lb in
+              dq vb kl
+
+            | DVal (u, _) , DVal (v, _) ->
+              let x = ND.meet (Hashtbl.find a.leaves u) (Hashtbl.find b.leaves v) in
+              get_leaf x
+            | DVal(u, _), DTop ->
+              get_leaf (Hashtbl.find a.leaves u)
+            | DTop, DVal(v, _) ->
+              get_leaf (Hashtbl.find b.leaves v)
+
+            | _ -> assert false (* see above *)
+          in
+            { leaves; ve; root = time "meet" (fun () -> memo2 f a.root b.root) }
+        end
 
 
 
@@ -407,7 +415,8 @@ end = struct
         | CLFalse -> edd_bot v.ve
         | CLAnd (a, b) ->
           let v = edd_apply_cl v ([], nc, a) in
-          edd_apply_cl v ([], nc, b)
+          if v.root = DBot then v else
+            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))