diff options
Diffstat (limited to 'abstract/abs_interp.ml')
| -rw-r--r-- | abstract/abs_interp.ml | 66 |
1 files changed, 48 insertions, 18 deletions
diff --git a/abstract/abs_interp.ml b/abstract/abs_interp.ml index feaf037..d706f35 100644 --- a/abstract/abs_interp.ml +++ b/abstract/abs_interp.ml @@ -21,6 +21,9 @@ end = struct env : E.t; f : bool_expr; cl : conslist; + f_g : bool_expr; + cl_g : conslist; + guarantees : (id * bool_expr) list; } @@ -73,8 +76,11 @@ end = struct let init_state widen_delay p root = let root_scope = get_root_scope p root in - let f = Formula.eliminate_not (Transform.f_of_prog p root) in + let f = Formula.eliminate_not (Transform.f_of_prog p root false) in let cl = Formula.conslist_of_f f in + let f_g = Formula.eliminate_not (Transform.f_of_prog p root true) in + let cl_g = Formula.conslist_of_f f_g in + let all_vars = node_vars p root "" @ extract_all_vars p root_scope in let env = List.fold_left (fun env (_, id, ty) -> @@ -83,15 +89,25 @@ end = struct all_vars in let init_f = Transform.init_f_of_prog p root in + let guarantees = Transform.guarantees_of_prog p root in Format.printf "Init formula: %a@.@." Formula_printer.print_expr init_f; - Format.printf "Cycle formula: %a@.@." Formula_printer.print_expr f; + Format.printf "Cycle formula:@.%a@.@." Formula_printer.print_expr f; + Format.printf "Cycle formula with guarantees:@.%a@.@." Formula_printer.print_expr f_g; Format.printf "Vars: @[<hov>%a@]@.@." (Ast_printer.print_list Ast_printer.print_var_decl ", ") all_vars; + Format.printf "Guarantees:@."; + List.iter (fun (id, f) -> + Format.printf " %s: %a@." id Formula_printer.print_expr f) + guarantees; + Format.printf "@."; + let env = E.apply_f env init_f in - { p; root_scope; widen_delay; f; cl; all_vars; env } + { p; root_scope; widen_delay; + f; cl; f_g; cl_g; + guarantees; all_vars; env } (* pass_cycle : var_def list -> E.t -> E.t @@ -125,35 +141,36 @@ end = struct (pass_cycle st.all_vars (E.apply_cl i cl)) (* - loop : st -> cl -> env -> env -> env + loop : st -> env -> env -> env *) - let loop st cycle_cl pnew stay = + let loop st pnew stay = Format.printf "Loop @[<hv>%a@]@.New @[<hv>%a@]@.Stay @[<hv>%a@]@." - Formula_printer.print_conslist cycle_cl + Formula_printer.print_conslist st.cl E.print_all pnew E.print_all stay; - let add_stay = cycle st cycle_cl pnew in + let add_stay = cycle st st.cl pnew in let acc0 = E.join stay add_stay in - let fsharp i = + let fsharp cl i = Format.printf "Acc @[<hv>%a@]@." E.print_all i; - let j = cycle st cycle_cl i in + let j = cycle st cl i in E.join acc0 j in let rec iter n i = let i' = if n < st.widen_delay - then E.join i (fsharp i) - else E.widen i (fsharp i) + then E.join i (fsharp st.cl_g i) + else E.widen i (fsharp st.cl_g i) in if E.eq i i' then i else iter (n+1) i' in let x = iter 0 acc0 in - fix E.eq fsharp x (* decreasing iteration *) - + let y = fix E.eq (fsharp st.cl_g) x in (* decreasing iteration *) + let z = E.apply_cl y st.cl in + y, z (* do_prog : prog -> id -> unit @@ -163,16 +180,29 @@ end = struct let pnew = st.env in - let stay = loop st st.cl pnew (E.vbottom pnew) in + let stay, stay_c = loop st pnew (E.vbottom pnew) in - let final = E.join (E.apply_cl pnew st.cl) (E.apply_cl stay st.cl) in + let final = E.join (E.apply_cl pnew st.cl) stay_c in - Format.printf "@[<hov>Final %a@]@." + Format.printf "@[<hov>Final %a@]@.@." E.print_all final; - Format.printf "Probes:@[<hov>"; + let check_guarantee (id, f) = + Format.printf "@[<hv>%s:@ %a@ " + id Formula_printer.print_expr f; + let z = E.apply_f final (BAnd(f, st.f)) in + if E.is_bot z then + Format.printf "OK@]@ " + else + Format.printf "FAIL@]@ " + in + Format.printf "Guarantees: @[<v 0>"; + List.iter check_guarantee st.guarantees; + Format.printf "@]@."; + + Format.printf "Probes:@[<v>"; List.iter (fun (p, id, _) -> - if p then Format.printf "@ %a ∊ %a," + if p then Format.printf " %a ∊ %a@ " Formula_printer.print_id id E.print_itv (E.var_itv final id)) st.all_vars; |