From 2afdad2c0410a1b4d39331f0e84e462965ff7a6f Mon Sep 17 00:00:00 2001 From: Johannes Kanig Date: Thu, 4 Feb 2016 18:27:42 +0900 Subject: [PATCH] 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 --- src/whyml/mlw_wp.ml | 45 +++++++++++++++++++++++++++++---------------- 1 file changed, 29 insertions(+), 16 deletions(-) diff --git a/src/whyml/mlw_wp.ml b/src/whyml/mlw_wp.ml index f8ccfa351..9c74e92ef 100644 --- a/src/whyml/mlw_wp.ml +++ b/src/whyml/mlw_wp.ml @@ -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)) -- 2.26.2