Update to LocationVariable is ignored after pruning

[gewitternacht]

Description

Sometimes the simplifyUpdate1/simplifyUpdate2 rules ignore updates, specifically to LoctionVaribales. This seems to be caused by preceding pruning.
In my case something like { ... || heapBefore_foo:=heap || ... }heapBefore_foo was "simplified" to heapBefore_foo instead of heap.

Reproducible

always

Steps to reproduce

1. load the foo()-Method from Updates.java into KeY
2. execute Full Auto Pilot→ the proof is closed
3. prune the whole proof tree
4. execute Full Auto Pilot again → the proof is not closed
5. apply One Step Simplification on the remaining goal (Validity of the assertion)
   → the resulting formula contains self.modelMethod()@heapBefore_foo, which should be self.modelMethod() – the update heapBefore_foo:=heap should have been applied, but was ignored
6. save the proof in its current state
7. relaod the previously saved proof and go to the remaining goal
   → now the formula correctly contains self.modelMethod()

Updates.java.zip

---

• Commit: 69fd947

[gewitternacht]

#1418 seems to be somewhat similar.

[mattulbrich]

Is that reprocucible if pruned not from a closed but from an unfinished proof?

[gewitternacht]

Is that reprocucible if pruned not from a closed but from an unfinished proof?

Yes, this was the case for me when I first noticed the issue.
It can also be observed by executing "Auto Pilot (Preparation Only)" instead of "Full Auto Pilot" in step 2 from above. This way in step 3 an unfinished proof is pruned.

[mattulbrich]

The problem is that during symbolic execution the jml assertions within method bodies are rewritten to refer to intermediate heap variables. Unfortunately, this is incompatible with pruning since these heap variables are different in a second run.

Program data structures are designed immutable and this behaviour violates this fundamental design principle leading to this bug.

A suggested solution is:

1. JmlAssert.updateVars does not change fields in the object, but returns a fresh copy with modified variables.
2. The class PrestateVariablesUpdater is changed such that it does not modify statements but reconstructs statements. To do this, the method performActionOnJmlAssert might collect replacement pairs which are then replaced if needed in the visitor entry method; or make the class extend CreatingASTVisitor