Add command line option : verbose chaotic iterations.

2 files changed, 28 insertions, 14 deletions

diff --git a/abstract/abs_interp.ml b/abstract/abs_interp.ml
index 8d5f1c9..f526095 100644
--- a/abstract/abs_interp.ml
+++ b/abstract/abs_interp.ml
@@ -7,12 +7,18 @@ open Util
 open Num_domain
 open Enum_domain
 
+type cmdline_opt = {
+    widen_delay       : int;
+    disjunct          : (id -> bool);
+    verbose_ci        : bool;
+}
+
 
 module I (ED : ENUM_ENVIRONMENT_DOMAIN) (ND : NUMERICAL_ENVIRONMENT_DOMAIN) : sig
 
     type st
 
-    val do_prog     : int -> (id -> bool) -> rooted_prog -> unit
+    val do_prog : cmdline_opt -> rooted_prog -> unit
 
 end = struct
 
@@ -161,7 +167,7 @@ end = struct
 
     type st = {
         rp          : rooted_prog;
-        widen_delay : int;
+        opt         : cmdline_opt;
 
         enum_vars   : (id * ED.item list) list;
         num_vars    : (id * bool) list;
@@ -199,7 +205,7 @@ end = struct
             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.widen_delay then ND.join else ND.widen 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 ->
@@ -225,7 +231,7 @@ end = struct
     (*
       init_state : int -> rooted_prog -> st
     *)
-    let init_state widen_delay disj rp =
+    let init_state opt rp =
       Format.printf "Vars: @[<hov>%a@]@.@."
           (Ast_printer.print_list Ast_printer.print_typed_var ", ")
           rp.all_vars;
@@ -253,8 +259,6 @@ end = struct
       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;
-      Format.printf "Cycle formula with guarantees:@.%a@.@."
-          Formula_printer.print_expr f_g;
 
       let cl = Formula.conslist_of_f f in
       let cl_g = Formula.conslist_of_f f_g in
@@ -288,7 +292,7 @@ end = struct
       in
       let d_vars_0 = calculate_dvars init_cl in
       let d_vars_1 = List.filter
-          (fun id -> disj id && not (List.mem id d_vars_0) && id.[0] <> 'N')
+          (fun id -> opt.disjunct id && not (List.mem id d_vars_0) && id.[0] <> 'N')
           (List.map (fun (id, _) -> id) enum_vars) in
       let d_vars = d_vars_0 @ d_vars_1 in
 
@@ -310,7 +314,7 @@ end = struct
       let env = env_dd.data in
       
       let st = 
-      { rp; widen_delay; enum_vars; num_vars;
+      { rp; opt; enum_vars; num_vars;
         f; cl; f_g; cl_g; guarantees;
         cycle; forget; d_vars; top;
         env; delta; widen } in
@@ -372,8 +376,8 @@ end = struct
     (*
       do_prog : rooted_prog -> unit
     *)
-    let do_prog widen_delay disj rp =
-      let st = init_state widen_delay disj rp in
+    let do_prog opt rp =
+      let st = init_state opt rp in
 
       Format.printf "Init: %a@." print_st st;
 
@@ -400,7 +404,7 @@ end = struct
         let rec iter n (i_enum, i_num) =
           let fi_enum, fi_num = f (i_enum, i_num) in
           let j_enum, j_num =
-            if n < st.widen_delay then
+            if n < st.opt.widen_delay then
               ED.join i_enum fi_enum, ND.join i_num fi_num
             else
               ED.join i_enum fi_enum, ND.widen i_num fi_num
@@ -425,7 +429,8 @@ end = struct
 
         st.delta <- List.filter ((<>) case) st.delta;
 
-        (* Format.printf "Final: %a@." print_st st; *)
+        if st.opt.verbose_ci then
+          Format.printf "-> @[<hov>%a@]@." print_st st;
 
       done;
 
diff --git a/main.ml b/main.ml
index 1de08be..2e4eb49 100644
--- a/main.ml
+++ b/main.ml
@@ -3,6 +3,7 @@ open Ast
 open Num_domain
 open Nonrelational
 open Apron_domain
+open Abs_interp
 
 module Interpret = Interpret.I
 
@@ -23,6 +24,7 @@ let ai_widen_delay = ref 3
 let ai_no_time_scopes = ref ""
 let ai_init_scopes = ref ""
 let ai_disj_v = ref ""
+let ai_vci = ref false
 let ifile = ref ""
 
 let usage = "usage: analyzer [options] file.scade"
@@ -34,6 +36,7 @@ let options = [
     "--test", Arg.Set test, "Simple testing (direct interpret).";
     "--ai-itv", Arg.Set ai_itv, "Do abstract analysis using intervals.";
     "--ai-rel", Arg.Set ai_rel, "Do abstract analysis using Apron.";
+    "--ai-vci", Arg.Set ai_vci, "Verbose chaotic iterations (show state at each iteration)";
     "--wd", Arg.Set_int ai_widen_delay, "Widening delay in abstract analysis of loops (default: 3).";
     "--root", Arg.Set_string ai_root, "Root node for abstract analysis (default: test).";
     "--no-time", Arg.Set_string ai_no_time_scopes, "Scopes for which not to introduce a 'time' variable in analysis.";
@@ -99,9 +102,15 @@ let () =
               (select_f !ai_init_scopes) in
 
           let disj = select_f !ai_disj_v in
+
+          let opt = {
+              widen_delay = !ai_widen_delay;
+              disjunct = disj;
+              verbose_ci = !ai_vci
+          } in
           
-          if !ai_itv then AI_Itv.do_prog !ai_widen_delay disj rp;
-          if !ai_rel then AI_Rel.do_prog !ai_widen_delay disj rp;
+          if !ai_itv then AI_Itv.do_prog opt rp;
+          if !ai_rel then AI_Rel.do_prog opt rp;
       end;
 
       if !vtest then do_test_interpret prog true