Commit 2afdad2c authored by Johannes Kanig's avatar Johannes Kanig

N127-001 improve performance on fastWP

On N121-024 we fixed a bug where a state was incorrectly reused during
merge. The fix was to never reuse state when merging. This resulted in a
performance drop.

The new fix now marks states which should not be reused - basically
states that come from raise - and when such a state is present during
merging, we don't reuse. Otherwise, we reuse.  This seems to get us the
performance and passes all tests.

Marking is implemented simply by a flag in states

* mlw_wp.ml:
(mark) allows to set the marked flag of a state
(empty) empty state is not marked
(havoc) havoc doesn't change marked state
(merge_vars, merge_regs) new argument "marked", only create a new
  variable when marked is true, otherwise reuse
(fast_wp) in the case of Eraise, mark the used state

M415-042 pass labels down to conjunctions

Why3 parser groups the loop invariants into a single formula. This patch
allows to have the VC labels on every conjunct

mlw_wp.ml
(fastwp) call wp_expl instead of t_label
parent b48ec445
......@@ -1139,6 +1139,8 @@ module Subst : sig
(* the initial substitution for a program which mentions the given program
variables *)
val mark : t -> t
val havoc : model_data option -> wp_env -> Sreg.t -> t -> t * term
(* [havoc md env regions s] generates a new state in which all regions in
[regions] are touched and all other regions unchanged. The result pair
......@@ -1192,6 +1194,7 @@ end = struct
{ now : subst;
other : subst Mvs.t;
reg_names : vsymbol Mreg.t;
marked : bool;
}
(* the reg_names field is a simple name hint; a mapping reg |-> name means
that [name] should be used as a base for new variables in region [reg].
......@@ -1239,6 +1242,7 @@ end = struct
in
{ other = s.other;
reg_names = reg_names;
marked = s.marked;
now =
{ subst_vars = vars;
subst_regions =
......@@ -1252,10 +1256,13 @@ end = struct
let empty =
{ other = Mvs.empty;
reg_names = Mreg.empty;
marked = false;
now = { subst_regions = Mreg.empty;
subst_vars = Mvs.empty; }
}
let mark s = { s with marked = true }
(* (* debugging code *)
let print_state fmt s =
Format.fprintf fmt "{ ";
......@@ -1299,9 +1306,10 @@ end = struct
acc
end) s.now.subst_vars (s.now.subst_vars, t_true) in
{ s with now =
{ subst_regions = regs;
subst_vars = vars;
} }, f
{ subst_regions = regs;
subst_vars = vars;
};
marked = s.marked }, f
let rec term s t =
(* apply a substitution to a formula. This is straightforward, we only need
......@@ -1367,25 +1375,27 @@ end = struct
let first_different_vars base l = first_different base vs_equal l
let first_different_terms base l = first_different base t_equal l
let merge_vars md base domain mapl =
let merge_vars md marked base domain mapl =
Mvs.fold (fun k _ (map , fl) ->
let all_terms = List.map (fun m -> Mvs.find k m) mapl in
match first_different_terms (Mvs.find k base) all_terms with
| None -> Mvs.add k (List.hd all_terms) map, fl
| Some _ ->
let new_ = t_var (fresh_var_from_var md k) in
| Some new_ ->
let new_ =
if marked then t_var (fresh_var_from_var md k) else new_ in
Mvs.add k new_ map,
List.map2 (fun old f ->
t_and_simp (t_equ new_ old) f) all_terms fl)
domain (Mvs.empty, List.map (fun _ -> t_true) mapl)
let merge_regs md names base domain mapl =
let merge_regs md names marked base domain mapl =
Mreg.fold (fun k _ (map, fl) ->
let all_vars = List.map (fun m -> Mreg.find k m) mapl in
match first_different_vars (Mreg.find k base) all_vars with
| None -> Mreg.add k (List.hd all_vars) map, fl
| Some _ ->
let new_ = fresh_var_from_region md names k in
| Some new_ ->
let new_ =
if marked then fresh_var_from_region md names k else new_ in
Mreg.add k new_ map,
List.map2 (fun old f ->
if vs_equal old new_ then f
......@@ -1401,17 +1411,20 @@ end = struct
program variables/regions should be present in all of them. *)
let domain =
List.fold_left (fun acc s -> subst_inter acc s.now) base.now sl in
let marked = List.exists (fun x -> x.marked) sl in
let vars, fl1 =
merge_vars md base.now.subst_vars domain.subst_vars
merge_vars md marked base.now.subst_vars domain.subst_vars
(List.map (fun x -> x.now.subst_vars) sl)
in
let regs, fl2 =
merge_regs md base.reg_names base.now.subst_regions domain.subst_regions
merge_regs md base.reg_names marked base.now.subst_regions
domain.subst_regions
(List.map (fun x -> x.now.subst_regions) sl)
in
{ base with now =
{ subst_vars = vars;
subst_regions = regs }
{ subst_vars = vars;
subst_regions = regs };
marked = false;
},
List.map2 t_and_simp fl1 fl2
......@@ -1772,7 +1785,7 @@ and fast_wp_desc (env : wp_env) (s : Subst.t) (r : res_type) (e : expr)
s, ne
with Not_found ->
wp1.post.s, t_and_simp wp1.post.ne rpost in
let expost = { s = s; ne = wp_label e ne } in
let expost = { s = Subst.mark s; ne = wp_label e ne } in
let xne = Mexn.add ex expost wp1.exn in
{ ok = wp1.ok;
post = { ne = t_false; s = wp1.post.s };
......@@ -1881,12 +1894,12 @@ and fast_wp_desc (env : wp_env) (s : Subst.t) (r : res_type) (e : expr)
(* EX: ex(e1)[r -> r'] *)
let md = create_model_data_opt ~loc:e1.e_loc ~context_labels:e1.e_label "loop" in
let havoc_state, glue = Subst.havoc md env (regs_of_writes e1.e_effect) s in
let init_inv = t_label_add expl_loop_init (Subst.term s inv) in
let init_inv = wp_expl expl_loop_init (Subst.term s inv) in
let inv_hypo =
t_and_simp glue (Subst.term havoc_state inv) in
let wp1 = fast_wp_expr env havoc_state r e1 in
let post_inv =
t_label_add expl_loop_keep (Subst.term wp1.post.s inv) in
wp_expl expl_loop_keep (Subst.term wp1.post.s inv) in
(* preservation also includes the "OK" of the loop body, the overall
form is:
I => (OK /\ (NE => I' /\ V))
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment