diff options
| -rw-r--r-- | abstract/abs_interp.ml | 29 | ||||
| -rw-r--r-- | main.ml | 13 |
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; @@ -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 |