Adapt domain with non-EDD disjunctions ; it doesn't work very well !

1 files changed, 103 insertions, 93 deletions

diff --git a/abstract/abs_interp.ml b/abstract/abs_interp.ml
index 26b788b..787c6d6 100644
--- a/abstract/abs_interp.ml
+++ b/abstract/abs_interp.ml
@@ -165,6 +165,7 @@ end = struct
         rp          : rooted_prog;
         opt         : cmdline_opt;
 
+        all_vars    : (bool * id * typ) list;
         enum_vars   : (id * ED.item list) list;
         num_vars    : (id * bool) list;
 
@@ -220,27 +221,68 @@ end = struct
             (ED.project enum p)
       in aux enum [] st.d_vars
 
+  
+    (*
+      dd_apply_cl : dd_v -> conslist -> dd_v
+    *)
+    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 num = ND.apply_cl num nc in
+          List.map (fun ec -> ec, num) enums
+        | CLFalse -> []
+        | CLAnd(a, b) ->
+          let envs = apply_cl_get_all_cases (enum, num) (ec, nc, a) in
+          List.flatten
+            (List.map (fun e -> apply_cl_get_all_cases e (ec, nc, b)) envs)
+        | CLOr((eca, nca, ra), (ecb, ncb, rb)) ->
+          apply_cl_get_all_cases (enum, num) (ec@eca, nc@nca, ra) @
+          apply_cl_get_all_cases (enum, num) (ec@ecb, nc@ncb, rb)
+
+    (*
+      pass_cycle : st -> case_v -> case_v
+    *)
+    let pass_cycle st (enum, num) =
+        let assign_e, assign_n = List.fold_left
+          (fun (ae, an) (a, b, t) -> match t with
+            | TEnum _ -> (a, b)::ae, an
+            | TInt | TReal -> ae, (a, NIdent b)::an)
+          ([], []) st.cycle in
+
+        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 dd_pass_cycle st (v : dd_v) =
+      let vv = dd_bot v.d_vars in
+      Hashtbl.iter (fun _ x -> dd_add_case vv (pass_cycle st x)) v.data;
+      vv
 
     (*
       init_state : int -> rooted_prog -> st
     *)
     let init_state opt rp =
-      Format.printf "Vars: @[<hov>%a@]@.@."
-          (print_list Ast_printer.print_typed_var ", ")
-          rp.all_vars;
-
-      let num_vars, enum_vars = List.fold_left
-          (fun (nv, ev) (_, id, t) -> match t with
-              | TEnum ch -> nv, (id, ch)::ev
-              | TInt -> (id, false)::nv, ev
-              | TReal -> (id, true)::nv, ev)
-          ([], []) rp.all_vars in
-
-      let init_f = Transform.init_f_of_prog rp in
+      let init_f, f = Transform.f_of_prog rp false in
+      let _, f_g = Transform.f_of_prog rp true in
       Format.printf "Init formula: %a@.@." Formula_printer.print_expr init_f;
-      let init_cl = conslist_of_f init_f in
+      Format.printf "Cycle formula:@.%a@.@." Formula_printer.print_expr f;
 
+      let init_cl = conslist_of_f init_f in
+      let cl = Formula.conslist_of_f f in
+      let cl_g = Formula.conslist_of_f f_g in
+      Format.printf "Cycle conslist:@.%a@.@." Formula_printer.print_conslist cl;
+      
       let guarantees = Transform.guarantees_of_prog rp in
       Format.printf "Guarantees:@.";
       List.iter (fun (id, f) ->
@@ -248,46 +290,42 @@ end = struct
         guarantees;
       Format.printf "@.";
 
-      let f = Formula.eliminate_not (Transform.f_of_prog rp false) in
-      let f_g = Formula.eliminate_not (Transform.f_of_prog rp true) in
-      Format.printf "Cycle formula:@.%a@.@." Formula_printer.print_expr f;
 
-      let cl = Formula.conslist_of_f f in
-      let cl_g = Formula.conslist_of_f f_g in
-      Format.printf "Cycle conslist:@.%a@.@." Formula_printer.print_conslist cl;
+      (* add variables from LASTs *)
+      let last_vars = uniq_sorted
+        (List.sort compare (Transform.extract_last_vars f_g)) in
+      let last_vars = List.map
+        (fun id ->
+          let (_, _, ty) = List.find (fun (_, u, _) -> id = "L"^u) rp.all_vars
+            in false, id, ty)
+        last_vars in
+      let all_vars = last_vars @ rp.all_vars in
+
+      Format.printf "Vars: @[<hov>%a@]@.@."
+          (print_list Ast_printer.print_typed_var ", ")
+          all_vars;
+
+      let num_vars, enum_vars = List.fold_left
+          (fun (nv, ev) (_, id, t) -> match t with
+              | TEnum ch -> nv, (id, ch)::ev
+              | TInt -> (id, false)::nv, ev
+              | TReal -> (id, true)::nv, ev)
+          ([], []) all_vars in
 
       (* calculate cycle variables and forget variables *)
       let cycle = List.fold_left
         (fun q (_, id, ty) ->
-            if id.[0] = 'N' then
-              (String.sub id 1 (String.length id - 1), id, ty)::q
+            if id.[0] = 'L' then
+              (id, String.sub id 1 (String.length id - 1), ty)::q
             else q)
-        [] rp.all_vars
-      in
-      let forget = List.map (fun (_, id, ty) -> (id, ty))
-          (List.filter
-            (fun (_, id, _) ->
-              not (List.exists (fun (_, id2, _) -> id2 = "N"^id) rp.all_vars))
-            rp.all_vars)
+        [] all_vars
       in
+      let forget = List.map (fun (_, id, ty) -> (id, ty)) rp.all_vars in
 
       (* calculate disjunction variables *)
-      (* first approximation : use all enum variables appearing in init formula *)
-      let rec calculate_dvars (ec, _, r) =
-          let a = List.map (fun (_, id, _) -> id) ec in
-          let rec aux = function
-          | CLTrue | CLFalse -> []
-          | CLAnd(u, v) ->
-              aux u @ aux v
-          | CLOr(u, v) ->
-              calculate_dvars u @ calculate_dvars v
-          in a @ aux r
-      in
-      let d_vars_0 = calculate_dvars init_cl in
-      let d_vars_1 = List.filter
-          (fun id -> opt.disjunct id && not (List.mem id d_vars_0) && id.[0] <> 'N')
+      (* actually, don't calculate them, rely on user input *)
+      let d_vars = List.filter (fun k -> k <> "/init" && opt.disjunct k)
           (List.map (fun (id, _) -> id) enum_vars) in
-      let d_vars = d_vars_0 @ d_vars_1 in
 
       (* setup abstract data *)
       let top = ED.top enum_vars, ND.top num_vars in
@@ -297,51 +335,26 @@ end = struct
       (* calculate initial state and environment *)
       let init_s = dd_bot d_vars in
 
-      let init_ec, _, _ = init_cl in
-      let init_ed = List.fold_left
-          (fun ed cons ->
-            List.flatten (List.map (fun x -> ED.apply_cons x cons) ed))
-          [ED.top enum_vars] (init_ec) in
-      List.iter (fun ed -> dd_add_case init_s (ed, ND.top num_vars)) init_ed;
-      let env_dd = apply_cl init_s init_cl in
-      let env = env_dd.data in
-      
+      List.iter (fun ed -> dd_add_case init_s ed)
+        (apply_cl_get_all_cases top init_cl);
+
+      let env_dd = apply_cl init_s init_cl in (* useless refinement ? *)
+
       let st = 
-      { rp; opt; enum_vars; num_vars;
+      { rp; opt; enum_vars; num_vars; all_vars;
          cl; cl_g; guarantees;
         cycle; forget; d_vars; top;
-        env; delta; widen } in
+        env = Hashtbl.create 1; delta; widen } in
+
+      let env_dd_pass = dd_pass_cycle st env_dd in
 
+      let st = { st with env = env_dd_pass.data } in
       Hashtbl.iter (fun case _ -> st.delta <- case::st.delta) st.env;
 
       st
 
 
     (*
-      pass_cycle : st -> case_v -> case_v
-    *)
-    let pass_cycle st (enum, num) =
-        let assign_e, assign_n = List.fold_left
-          (fun (ae, an) (a, b, t) -> match t with
-            | TEnum _ -> (a, b)::ae, an
-            | TInt | TReal -> ae, (a, NIdent b)::an)
-          ([], []) st.cycle in
-
-        let enum = ED.assign enum assign_e in
-        let num = ND.assign num assign_n in
-
-        List.fold_left
-            (fun (enum, num) (var, t) -> match t with
-              | TEnum _ -> ED.forgetvar enum var, num
-              | TReal | TInt -> enum, ND.forgetvar num var)
-            (enum, num) st.forget
-
-    let dd_pass_cycle st (v : dd_v) =
-      let vv = dd_bot v.d_vars in
-      Hashtbl.iter (fun _ x -> dd_add_case vv (pass_cycle st x)) v.data;
-      vv
-
-    (*
       cycle : st -> cl -> dd_v -> dd_v
     *)
     let cycle st cl env =
@@ -407,23 +420,20 @@ end = struct
 
         let i = dd_singleton st.d_vars z in
         let j = cycle st st.cl i in
-        if Hashtbl.length j.data = 0 then
-          Format.printf "@.WARNING: contradictory hypotheses!@.@."
-        else begin
-          let cases = ref [] in
-          Hashtbl.iter (fun case _ -> cases := case::(!cases)) j.data;
-          List.iter
-              (fun case ->
-                let i' = set_target_case st i case in
-                let j = cycle st st.cl i' in
-                Hashtbl.iter (fun _ q -> add_case st q) j.data)
-              !cases;
 
-          st.delta <- List.filter ((<>) case) st.delta;
+        let cases = ref [] in
+        Hashtbl.iter (fun case _ -> cases := case::(!cases)) j.data;
+        List.iter
+            (fun case ->
+              let i' = set_target_case st i case in
+              let j = cycle st st.cl i' in
+              Hashtbl.iter (fun _ q -> add_case st q) j.data)
+            !cases;
+
+        if st.opt.verbose_ci then
+          Format.printf "-> @[<hov>%a@]@." print_st st;
 
-          if st.opt.verbose_ci then
-            Format.printf "-> @[<hov>%a@]@." print_st st;
-        end
+        st.delta <- List.filter ((<>) case) st.delta;
 
       done;