• 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
mlw_wp.ml 82.6 KB