Use LAST instead of NEXT (only EDD implementation works at the moment)

1 files changed, 36 insertions, 37 deletions

diff --git a/abstract/abs_interp_edd.ml b/abstract/abs_interp_edd.ml
index 6220a0a..c1fb905 100644
--- a/abstract/abs_interp_edd.ml
+++ b/abstract/abs_interp_edd.ml
@@ -2,10 +2,10 @@ open Ast
 open Ast_util
 open Formula
 open Typing
+open Cmdline
 
 open Util
 open Num_domain
-open Abs_interp
 
 
 
@@ -592,9 +592,12 @@ end = struct
         rp            : rooted_prog;
         opt           : cmdline_opt;
 
+        last_vars     : (bool * id * typ) list;
+        all_vars      : (bool * id * typ) list;
         ve            : varenv;
 
         (* program expressions *)
+        init_f        : bool_expr;
         cl            : conslist;
         cl_g          : conslist;
         guarantees    : (id * bool_expr) list;
@@ -602,7 +605,6 @@ end = struct
         (* abstract interpretation *)
         cycle         : (id * id * typ) list;     (* s'(x) = s(y) *)
         forget        : (id * typ) list;          (* s'(x) not specified *)
-        mutable data  : edd_v;
     }
 
 
@@ -924,20 +926,33 @@ end = struct
       init_env : cmdline_opt -> rooted_prog -> env
     *)
     let init_env opt rp =
+        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;
+        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;
+
+        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 ", ")
-            rp.all_vars;
+            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
-        Format.printf "Init formula: %a@.@." Formula_printer.print_expr init_f;
-        let init_cl = conslist_of_f init_f in
+            ([], []) all_vars in
 
         let guarantees = Transform.guarantees_of_prog rp in
         Format.printf "Guarantees:@.";
@@ -946,19 +961,10 @@ 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;
-
         (* calculate order for enumerated variables *)
         let evars = List.map fst enum_vars in
 
-        let lv = extract_linked_evars_root init_cl
-            @ extract_linked_evars_root cl_g in
+        let lv = extract_linked_evars_root cl_g in
         let lv = uniq_sorted
              (List.sort Pervasives.compare (List.map ord_couple lv)) in
 
@@ -995,25 +1001,17 @@ end = struct
         (* 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)
+          [] last_vars
         in
+        let forget = List.map (fun (_, id, ty) -> (id, ty)) rp.all_vars in
 
-        (* calculate initial environment *)
-        let data = edd_apply_cl (edd_top ve) init_cl in
-        Format.printf "Init: @[<hov>%a@]@." edd_print data;
 
-        { rp; opt; ve;
-          cl; cl_g; guarantees;
-          cycle; forget; data }
+        { rp; opt; ve; last_vars; all_vars;
+          init_f; cl; cl_g; guarantees;
+          cycle; forget }
 
           
 
@@ -1094,7 +1092,8 @@ end = struct
             end
         in
 
-        let init_acc = edd_star_new (edd_bot e.data.ve) e.data in
+        let init_acc = edd_star_new (edd_bot e.ve)
+            (pass_cycle e (edd_apply_cl (edd_top e.ve) (conslist_of_f e.init_f))) in
         
         (* Dump final state *)
         let acc = ch_it 0 init_acc in
@@ -1124,13 +1123,13 @@ end = struct
         end;
 
         (* Examine probes *)
-        if List.exists (fun (p, _, _) -> p) e.rp.all_vars then begin
+        if List.exists (fun (p, _, _) -> p) e.all_vars then begin
           let final_flat = edd_forget_vars final
             (List.fold_left
               (fun l (_, id, ty) -> match ty with
                 | TInt | TReal -> l
                 | TEnum _ -> id::l)
-              [] e.rp.all_vars) in
+              [] e.all_vars) in
           let final_flat = match final_flat.root with
             | DTop -> ND.top e.ve.nvars
             | DBot -> ND.bottom e.ve.nvars
@@ -1146,7 +1145,7 @@ end = struct
                 ND.print_itv (ND.project final_flat id)
             | TEnum _ -> Format.printf "%a : enum variable@."
                 Formula_printer.print_id id)
-            e.rp.all_vars;
+            e.all_vars;
           Format.printf "@]@."
         end