Adapt abs_interp to use ENUM_DOMAIN2 (this is a test...)

2 files changed, 109 insertions, 71 deletions

diff --git a/abstract/abs_interp.ml b/abstract/abs_interp.ml
index cb5ae9c..10bd33f 100644
--- a/abstract/abs_interp.ml
+++ b/abstract/abs_interp.ml
@@ -7,10 +7,11 @@ open Cmdline
 open Util
 open Num_domain
 open Enum_domain
+open Enum_domain_edd
 
 
 
-module I (ED : ENUM_ENVIRONMENT_DOMAIN) (ND : NUMERICAL_ENVIRONMENT_DOMAIN) : sig
+module I (ED : ENUM_ENVIRONMENT_DOMAIN2) (ND : NUMERICAL_ENVIRONMENT_DOMAIN) : sig
 
     type st
 
@@ -56,21 +57,22 @@ end = struct
       dd_add_case : dd_v -> case_v -> unit
     *)
     let dd_add_case env (enum, num) =
-      let rec aux enum vals = function
-        | [] ->
-          let case = List.rev vals in
-          begin try let e0, n0 = Hashtbl.find env.data case in
-            Hashtbl.replace env.data case (ED.join enum e0, ND.join num n0);
-          with Not_found ->
-            Hashtbl.add env.data case (enum, num);
-          end
-        | p::q ->
-          List.iter
-            (fun v -> match ED.apply_cons enum (E_EQ, p, EItem v) with
-              | [en] -> aux en (v::vals) q
-              | _ -> assert false)
-            (ED.project enum p)
-      in aux enum [] env.d_vars
+      if not (ED.is_bot enum || ND.is_bot num) then
+        let rec aux enum vals = function
+          | [] ->
+            let case = List.rev vals in
+            begin try let e0, n0 = Hashtbl.find env.data case in
+              Hashtbl.replace env.data case (ED.join enum e0, ND.join num n0);
+            with Not_found ->
+              Hashtbl.add env.data case (enum, num);
+            end
+          | p::q ->
+            List.iter
+              (fun v -> let en = ED.apply_cons enum (E_EQ, p, EItem v) in 
+                assert (not (ED.is_bot en));
+                aux en (v::vals) q)
+              (ED.project enum p)
+        in aux enum [] env.d_vars
 
     (*
       dd_singleton : id list -> case_v -> dd_v
@@ -101,14 +103,12 @@ end = struct
         vv
 
     (*
-      dd_apply_econs : dd_v -> enum_cons -> dd_v
+      dd_apply_ecl : dd_v -> enum_cons list -> dd_v
     *)
-    let dd_apply_econs v cons =
+    let dd_apply_ecl v cons =
         let vv = dd_bot v.d_vars in
         Hashtbl.iter (fun case (enum, num) ->
-            List.iter
-              (fun enum -> dd_add_case vv (enum, num))
-              (ED.apply_cons enum cons))
+            dd_add_case vv (ED.apply_cl enum cons, num))
           v.data;
         vv
 
@@ -133,7 +133,7 @@ end = struct
             try let e2, n2 = Hashtbl.find b.data case in
               let en, nn = ED.meet enum e2, ND.meet n2 num in
               if not (ND.is_bot nn) then Hashtbl.add vv.data case (en, nn)
-            with _ -> ())
+            with Not_found -> ())
           a.data;
         vv
 
@@ -143,10 +143,8 @@ end = struct
     let rec apply_cl env (ec, nc, r) =
         match r with
         | CLTrue ->
-          let env_ec = List.fold_left dd_apply_econs env ec in
+          let env_ec = dd_apply_ecl env ec in
           let env_nc = dd_apply_ncl env_ec nc in
-          (* Format.printf "[[ %a -> %a ]]@."
-              print_dd env print_dd env_nc; *)
           env_nc
         | CLFalse -> dd_bot env.d_vars
         | CLAnd(a, b) ->
@@ -194,33 +192,34 @@ end = struct
       add_case : st -> case_v -> unit
     *)
     let add_case st (enum, num) =
-      let rec aux enum vals = function
-        | [] ->
-          let case = List.rev vals in
-          begin try let e0, n0 = Hashtbl.find st.env case in
-            if (not (ED.subset enum e0)) || (not (ND.subset num n0)) then begin
-              begin try
-                let n = Hashtbl.find st.widen case in
-                let jw = if n < st.opt.widen_delay then ND.join else ND.widen in
-                Hashtbl.replace st.env case (ED.join e0 enum, jw n0 num);
-                Hashtbl.replace st.widen case (n+1);
-              with Not_found ->
-                Hashtbl.replace st.env case (ED.join enum e0, ND.join num n0);
-                Hashtbl.add st.widen case 0;
-              end;
+      if not (ED.is_bot enum || ND.is_bot num) then
+        let rec aux enum vals = function
+          | [] ->
+            let case = List.rev vals in
+            begin try let e0, n0 = Hashtbl.find st.env case in
+              if (not (ED.subset enum e0)) || (not (ND.subset num n0)) then begin
+                begin try
+                  let n = Hashtbl.find st.widen case in
+                  let jw = if n < st.opt.widen_delay then ND.join else ND.widen in
+                  Hashtbl.replace st.env case (ED.join e0 enum, jw n0 num);
+                  Hashtbl.replace st.widen case (n+1);
+                with Not_found ->
+                  Hashtbl.replace st.env case (ED.join enum e0, ND.join num n0);
+                  Hashtbl.add st.widen case 0;
+                end;
+                if not (List.mem case st.delta) then st.delta <- case::st.delta
+              end
+            with Not_found ->
+              Hashtbl.add st.env case (enum, num);
               if not (List.mem case st.delta) then st.delta <- case::st.delta
             end
-          with Not_found ->
-            Hashtbl.add st.env case (enum, num);
-            if not (List.mem case st.delta) then st.delta <- case::st.delta
-          end
-        | p::q ->
-          List.iter
-            (fun v -> match ED.apply_cons enum (E_EQ, p, EItem v) with
-              | [en] -> aux en (v::vals) q
-              | _ -> assert false)
-            (ED.project enum p)
-      in aux enum [] st.acc_d_vars
+          | p::q ->
+            List.iter
+              (fun v -> let en = ED.apply_cons enum (E_EQ, p, EItem v) in
+                assert (not (ED.is_bot en));
+                aux en (v::vals) q)
+              (ED.project enum p)
+        in aux enum [] st.acc_d_vars
 
   
     (*
@@ -229,10 +228,8 @@ end = struct
     let rec apply_cl_get_all_cases (enum, num) (ec, nc, r) =
         match r with
         | CLTrue ->
-          let enums = List.fold_left
-            (fun enums ec -> List.flatten
-              (List.map (fun e -> ED.apply_cons e ec) enums))
-            [enum] ec in
+          let enum = ED.apply_cl enum ec in
+          let enums = if ED.is_bot enum then [] else [enum] in
           let num = ND.apply_cl num nc in
           List.map (fun ec -> ec, num) enums
         | CLFalse -> []
@@ -257,13 +254,12 @@ end = struct
         let enum = ED.assign enum assign_e in
         let num = ND.assign num assign_n in
 
-        List.fold_left
-            (fun (enum, num) (var, t) ->
-              let e, n = match t with
-              | TEnum _ -> ED.forgetvar enum var, num
-              | TReal | TInt -> enum, ND.forgetvar num var
-              in e, n)
-            (enum, num) st.forget
+        let ef, nf = List.fold_left
+            (fun (ef, nf) (var, t) -> match t with
+              | TEnum _ -> var::ef, nf
+              | TReal | TInt -> ef, var::nf)
+            ([], []) st.forget in
+        ED.forgetvars enum ef, List.fold_left ND.forgetvar num nf
 
     let dd_pass_cycle st (v : dd_v) =
       let vv = dd_bot st.acc_d_vars in
@@ -363,12 +359,14 @@ end = struct
       set_target_case : st -> dd_v -> case -> dd_v
     *)
     let set_target_case st env case =
-      List.fold_left2
-        (fun env id v ->
-          if List.exists (fun (id2, _) -> id2 = "L"^id) st.enum_vars then
-            dd_apply_econs env (E_EQ, id, EItem v)
-          else env)
-        env st.acc_d_vars case
+      let cl =
+        List.fold_left2
+          (fun cl id v ->
+            if List.exists (fun (id2, _) -> id2 = "L"^id) st.enum_vars then
+              (E_EQ, id, EItem v)::cl
+            else cl)
+        [] st.acc_d_vars case
+      in dd_apply_ecl env cl
 
     (*
       do_prog : rooted_prog -> unit
diff --git a/abstract/enum_domain_edd.ml b/abstract/enum_domain_edd.ml
index 60f2d3b..a372772 100644
--- a/abstract/enum_domain_edd.ml
+++ b/abstract/enum_domain_edd.ml
@@ -1,9 +1,41 @@
 open Ast
 open Formula
 open Util
-open Enum_domain
 
-module EDD : ENUM_ENVIRONMENT_DOMAIN = struct
+module type ENUM_ENVIRONMENT_DOMAIN2 = sig
+    type t
+
+    type item = string
+
+    (* construction *)
+    val top           : (id * item list) list -> t
+    val bot           : (id * item list) list -> t
+    val is_bot        : t -> bool
+
+    (* variable management *)
+    val vars          : t -> (id * item list) list
+
+    val forgetvar     : t -> id -> t
+    val forgetvars    : t -> id list -> t
+    val project       : t -> id -> item list
+
+    (* set-theoretic operations *)
+    val join          : t -> t -> t   (* union *)
+    val meet          : t -> t -> t   (* intersection *)
+
+    val subset        : t -> t -> bool
+    val eq            : t -> t -> bool
+
+    (* abstract operations *)
+    val apply_cons    : t -> enum_cons -> t
+    val apply_cl      : t -> enum_cons list -> t
+    val assign        : t -> (id * id) list -> t
+
+    (* pretty-printing *)
+    val print         : Format.formatter -> t -> unit
+end
+
+module EDD : ENUM_ENVIRONMENT_DOMAIN2 = struct
     exception Top
 
     type item = string
@@ -132,11 +164,19 @@ module EDD : ENUM_ENVIRONMENT_DOMAIN = struct
 
     (*
       top : (id * item list) list -> t
+      bot : (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 }
+    let bot vars = let t = top vars in { t with root = DBot }
+
+    (*
+      is_bot : t -> bool
+    *)
+    let is_bot x = (x.root = DBot)
+
     (*
       vars : t -> (id * item list) list
     *)
@@ -243,8 +283,8 @@ module EDD : ENUM_ENVIRONMENT_DOMAIN = struct
       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]
+      meet v (of_cons v x)
+
     let apply_cl v ec =
         let rec cl_k = function
           | [] -> { v with root = DTop }