KeY proofs cannot be replayed if certain labels are present

[mattulbrich]

Description

If certain labels are present on a term and a find-and-add taclet is applied, stored proofs cannot be replayed/loaded.

The problem is that the recomputation of the labels modifies the sequent (although there is no replacewith-term). The place for inserting a formula, on the other hand, is determined by the PosInOccurrence of the find term. But that is no longer on the sequent. So finding it on the sequent fails.

This occurred in a 160k+ steps proof, but can be reduced to a minimal example.

Reproducible

always. Minimal example identified and attached.

Steps to reproduce

1. Load a .key file with the content below.
2. Apply the rule r on (2)<<origin("ensures (implicit)", "[]")>>.
3. Save the proof.
4. Try to reload it.
5. Observe the exception.

The file content is

\rules {
   r {
     \find(2)
     \add(2+2=4 ==>)
   };
}

\problem{ 2<<origin("ensures (implicit)", "[]")>> + 3 = 5 ==> 1+1=2 }

It makes sense to switch on term labels if you deactivated them.

Additional information

In the original situation, the error was slightly different. ...

Stacktrace:

Proof could only be loaded partially.
In summary 1 not loadable rule application(s) have been detected.
The first one:
Error loading proof.
Line 94, goal 0, rule r not available or not applicable in this context. (file: /tmp/.quicksave.key; caused by: Error loading proof.
Line 94, goal 0, rule r not available or not applicable in this context. (file: /tmp/.quicksave.key; caused by: de.uka.ilkd.key.proof.io.IntermediateProofReplayer$TacletAppConstructionException: Wrong position information: Term subterm: [0,0] of equals(add(Z(1(#)),Z(1(#))),Z(2(#)))))
	at de.uka.ilkd.key.gui.WindowUserInterfaceControl.loadingFinished(WindowUserInterfaceControl.java:533)
	at de.uka.ilkd.key.proof.io.AbstractProblemLoader.load(AbstractProblemLoader.java:297)
	at de.uka.ilkd.key.proof.io.ProblemLoader.doWork(ProblemLoader.java:74)
	at de.uka.ilkd.key.proof.io.ProblemLoader$1.doInBackground(ProblemLoader.java:124)
	at de.uka.ilkd.key.proof.io.ProblemLoader$1.doInBackground(ProblemLoader.java:117)
	at java.desktop/javax.swing.SwingWorker$1.call(SwingWorker.java:304)
	at java.base/java.util.concurrent.FutureTask.run$$$capture(FutureTask.java:264)
	at java.base/java.util.concurrent.FutureTask.run(FutureTask.java)
	at java.desktop/javax.swing.SwingWorker.run(SwingWorker.java:343)
	at java.base/java.util.concurrent.ThreadPoolExecutor.runWorker(ThreadPoolExecutor.java:1136)
	at java.base/java.util.concurrent.ThreadPoolExecutor$Worker.run(ThreadPoolExecutor.java:635)
	at java.base/java.lang.Thread.run(Thread.java:840)
Caused by: Error loading proof.
Line 94, goal 0, rule r not available or not applicable in this context. (file: /tmp/.quicksave.key; caused by: de.uka.ilkd.key.proof.io.IntermediateProofReplayer$TacletAppConstructionException: Wrong position information: Term subterm: [0,0] of equals(add(Z(1(#)),Z(1(#))),Z(2(#))))
	at de.uka.ilkd.key.proof.io.IntermediateProofReplayer.reportError(IntermediateProofReplayer.java:835)
	at de.uka.ilkd.key.proof.io.IntermediateProofReplayer.replay(IntermediateProofReplayer.java:256)
	at de.uka.ilkd.key.proof.io.IntermediateProofReplayer.replay(IntermediateProofReplayer.java:170)
	at de.uka.ilkd.key.proof.io.AbstractProblemLoader.replayProof(AbstractProblemLoader.java:741)
	at de.uka.ilkd.key.proof.io.AbstractProblemLoader.loadSelectedProof(AbstractProblemLoader.java:361)
	at de.uka.ilkd.key.proof.io.AbstractProblemLoader.load(AbstractProblemLoader.java:289)
	... 10 more
Caused by: de.uka.ilkd.key.proof.io.IntermediateProofReplayer$TacletAppConstructionException: Wrong position information: Term subterm: [0,0] of equals(add(Z(1(#)),Z(1(#))),Z(2(#)))
	at de.uka.ilkd.key.proof.io.IntermediateProofReplayer.constructTacletApp(IntermediateProofReplayer.java:480)
	at de.uka.ilkd.key.proof.io.IntermediateProofReplayer.replay(IntermediateProofReplayer.java:234)
	... 14 more
Caused by: java.lang.NullPointerException: Cannot invoke "de.uka.ilkd.key.rule.TacletApp.setPosInOccurrence(de.uka.ilkd.key.logic.PosInOccurrence, de.uka.ilkd.key.java.Services)" because "ourApp" is null
	at de.uka.ilkd.key.proof.io.IntermediateProofReplayer.constructTacletApp(IntermediateProofReplayer.java:476)
	... 15 more

---

• Commit: c8b5d84

[mattulbrich]

One relatively cheap fix is to simply ignore the position in case it is no longer there and add it to the beginning. But then (when loading) follow-up rules may not be applicable.

[flo2702]

The problem in this case seems to be somewhere else: The problem parser discards the antecedent and only parses the succedent.

@wadoon is parsing problems with a non-empty antecedent supposed to be supported or not? If not, is this documented?

@mattulbrich I don't quite remember the conversation we had. In the original situation, was there also a non-empty antecent or is there in fact another problem? If it's the latter, can you send me the example?

[mattulbrich]

Being able to specify a sequent in the problem section is a relatively new feature in key. I think it is quite relevant. I assume that because of its novelty the feature had not been used for saving files yet. It should probably get a bug report on its own.I can send you the original problem file -- but it has a few 10k proof steps.

[mi-ki]

@flo2702 I just wanted to take a look at the bug and the patch or fix you mentioned. However, I cannot find the proposed patch, so could you maybe give me a pointer?

[mattulbrich]

@flo2702 I just wanted to take a look at the bug and the patch or fix you mentioned. However, I cannot find the proposed patch, so could you maybe give me a pointer?

@mi-ki I sent you the material by e-mail.