• Johannes Kanig's avatar
    N127-001 improve performance on fastWP · 2afdad2c
    Johannes Kanig authored
    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
    2afdad2c
Name
Last commit
Last update
..
mlw_decl.ml Loading commit data...
mlw_decl.mli Loading commit data...
mlw_dexpr.ml Loading commit data...
mlw_dexpr.mli Loading commit data...
mlw_driver.ml Loading commit data...
mlw_driver.mli Loading commit data...
mlw_exec.ml Loading commit data...
mlw_exec.mli Loading commit data...
mlw_expr.ml Loading commit data...
mlw_expr.mli Loading commit data...
mlw_interp.ml Loading commit data...
mlw_interp.mli Loading commit data...
mlw_main.ml Loading commit data...
mlw_main.mli Loading commit data...
mlw_module.ml Loading commit data...
mlw_module.mli Loading commit data...
mlw_ocaml.ml Loading commit data...
mlw_ocaml.mli Loading commit data...
mlw_pretty.ml Loading commit data...
mlw_pretty.mli Loading commit data...
mlw_ty.ml Loading commit data...
mlw_ty.mli Loading commit data...
mlw_typing.ml Loading commit data...
mlw_typing.mli Loading commit data...
mlw_wp.ml Loading commit data...
mlw_wp.mli Loading commit data...