Skip to content

Commit ed6f332

Browse files
unp1unp1
committed
Feature: If possible save the last selected node in the proof, to reselect it upon loading (issue #3297).
1 parent 6a06061 commit ed6f332

File tree

24 files changed

+176
-85
lines changed

24 files changed

+176
-85
lines changed

‎key.core.symbolic_execution/src/test/java/de/uka/ilkd/key/symbolic_execution/testcase/AbstractSymbolicExecutionTestCase.java‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1678,7 +1678,7 @@ protected void assertSaveAndReload(File baseDir, String javaPathInBaseDir,
16781678
KeYEnvironment<DefaultUserInterfaceControl> reloadedEnv = null;
16791679
SymbolicExecutionTreeBuilder reloadedBuilder = null;
16801680
try {
1681-
ProofSaver saver = new ProofSaver(env.getProof(), tempFile.getAbsolutePath(),
1681+
ProofSaver saver = new ProofSaver(env.getProof(), null, tempFile.getAbsolutePath(),
16821682
KeYConstants.INTERNAL_VERSION);
16831683
assertNull(saver.save());
16841684
// Load proof from saved *.proof file

‎key.core/src/main/java/de/uka/ilkd/key/proof/Proof.java‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1344,7 +1344,7 @@ public void setProofFile(File proofFile) {
13441344
}
13451345

13461346
public void saveToFile(File file) throws IOException {
1347-
ProofSaver saver = new ProofSaver(this, file);
1347+
ProofSaver saver = new ProofSaver(this, null, file);
13481348
saver.save();
13491349
}
13501350

@@ -1356,7 +1356,7 @@ public void saveToFile(File file) throws IOException {
13561356
* @throws IOException on any I/O error
13571357
*/
13581358
public void saveProofObligationToFile(File file) throws IOException {
1359-
ProofSaver saver = new ProofSaver(this, file, false);
1359+
ProofSaver saver = new ProofSaver(this, null, file, false);
13601360
saver.save();
13611361
}
13621362

‎key.core/src/main/java/de/uka/ilkd/key/proof/io/AbstractProblemLoader.java‎

Lines changed: 9 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -740,15 +740,17 @@ private ReplayResult replayProof(Proof proof) {
740740
replayResult =
741741
replayer.replay(problemInitializer.getListener(), problemInitializer.getProgMon());
742742

743-
lastTouchedNode = replayResult.getLastSelectedGoal() != null
744-
? replayResult.getLastSelectedGoal().node()
745-
: proof.root();
743+
lastTouchedNode =
744+
replayResult.savedSelectedNode() != null ? replayResult.savedSelectedNode()
745+
: replayResult.lastSelectedGoal() != null
746+
? replayResult.lastSelectedGoal().node()
747+
: proof.root();
746748

747749
} catch (Exception e) {
748750
if (parserResult == null || parserResult.errors() == null
749751
|| parserResult.errors().isEmpty() || replayer == null
750-
|| replayResult == null || replayResult.getErrors() == null
751-
|| replayResult.getErrors().isEmpty()) {
752+
|| replayResult == null || replayResult.errors() == null
753+
|| replayResult.errors().isEmpty()) {
752754
// this exception was something unexpected
753755
errors.add(e);
754756
}
@@ -758,10 +760,10 @@ private ReplayResult replayProof(Proof proof) {
758760
errors.addAll(parserResult.errors());
759761
}
760762
status += (status.isEmpty() ? "Proof replayed successfully." : "\n\n")
761-
+ (replayResult != null ? replayResult.getStatus()
763+
+ (replayResult != null ? replayResult.status()
762764
: "Error while loading proof.");
763765
if (replayResult != null) {
764-
errors.addAll(replayResult.getErrors());
766+
errors.addAll(replayResult.errors());
765767
}
766768

767769
StrategyProperties newProps =

‎key.core/src/main/java/de/uka/ilkd/key/proof/io/AutoSaver.java‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -147,7 +147,7 @@ private void save(final String filename, final Proof proof) {
147147
// there may be concurrent changes to the proof... whatever
148148
final Runnable r = () -> {
149149
try {
150-
new ProofSaver(proof, filename, KeYConstants.INTERNAL_VERSION).save();
150+
new ProofSaver(proof, null, filename, KeYConstants.INTERNAL_VERSION).save();
151151
LOGGER.info("File saved: {}", filename);
152152
} catch (Exception e) {
153153
LOGGER.error("Autosaving file {} failed.", filename, e);

‎key.core/src/main/java/de/uka/ilkd/key/proof/io/GZipProofSaver.java‎

Lines changed: 5 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -8,6 +8,7 @@
88
import java.io.IOException;
99
import java.util.zip.GZIPOutputStream;
1010

11+
import de.uka.ilkd.key.proof.Node;
1112
import de.uka.ilkd.key.proof.Proof;
1213

1314
/**
@@ -22,11 +23,13 @@ public class GZipProofSaver extends ProofSaver {
2223
* Instantiates a new proof saver.
2324
*
2425
* @param proof the non-<code>null</code> proof to save
26+
* @param selectedNode the Node selected at time of saving or <code>null</code> if no
27+
* information available
2528
* @param fileName the name of the file to write to
2629
* @param internalVersion the internal version
2730
*/
28-
public GZipProofSaver(Proof proof, String fileName, String internalVersion) {
29-
super(proof, fileName, internalVersion);
31+
public GZipProofSaver(Proof proof, Node selectedNode, String fileName, String internalVersion) {
32+
super(proof, selectedNode, fileName, internalVersion);
3033
}
3134

3235
/**

‎key.core/src/main/java/de/uka/ilkd/key/proof/io/IProofFileParser.java‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -34,7 +34,7 @@ enum ProofElementID {
3434
USER_INTERACTION("userinteraction"), PROOF_SCRIPT("proofscript"), NEW_NAMES("newnames"),
3535
AUTOMODE_TIME("autoModeTime"), KeY_LOG("keyLog"), KeY_USER("keyUser"),
3636
KeY_VERSION("keyVersion"), KeY_SETTINGS("keySettings"), OPEN_GOAL("opengoal"),
37-
NOTES("notes"), SOLVERTYPE("solverType"), MODALITY("modality");
37+
NOTES("notes"), SOLVERTYPE("solverType"), MODALITY("modality"), SELECTED_NODE("selected");
3838

3939
private final String rawName;
4040

‎key.core/src/main/java/de/uka/ilkd/key/proof/io/IntermediatePresentationProofFileParser.java‎

Lines changed: 25 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -74,6 +74,7 @@ public class IntermediatePresentationProofFileParser implements IProofFileParser
7474
private BranchNodeIntermediate root = null; // the "dummy ID" branch
7575
private NodeIntermediate currNode;
7676
private final LinkedList<Throwable> errors = new LinkedList<>();
77+
private boolean parsingOpenGoal = false;
7778

7879
/**
7980
* @param proof Proof object for storing meta information about the parsed proof.
@@ -220,6 +221,9 @@ public void beginExpr(ProofElementID eid, String str) {
220221
}
221222
}
222223
case SOLVERTYPE -> ((BuiltinRuleInformation) ruleInfo).solver = str;
224+
case OPEN_GOAL -> {
225+
parsingOpenGoal = true;
226+
}
223227
default -> {
224228
}
225229
}
@@ -235,6 +239,24 @@ public void endExpr(ProofElementID eid, int lineNr) {
235239
((AppNodeIntermediate) currNode).setInteractiveRuleApplication(true);
236240
}
237241
}
242+
case SELECTED_NODE -> {
243+
int openGoalChildSelected = -1;
244+
if (parsingOpenGoal) {
245+
if (currNode instanceof BranchNodeIntermediate branchNode) {
246+
if (!stack.isEmpty()) {
247+
if (stack.peek() instanceof AppNodeIntermediate parentAppNode) {
248+
openGoalChildSelected = parentAppNode.getChildren().size() - 1;
249+
parentAppNode.setSelectedNode(true, openGoalChildSelected);
250+
}
251+
}
252+
} else {
253+
openGoalChildSelected = 0;
254+
}
255+
}
256+
if (currNode != null && currNode instanceof AppNodeIntermediate appNode) {
257+
appNode.setSelectedNode(true, openGoalChildSelected);
258+
}
259+
}
238260
case PROOF_SCRIPT -> {
239261
if (currNode != null) {
240262
((AppNodeIntermediate) currNode).setScriptRuleApplication(true);
@@ -254,6 +276,9 @@ public void endExpr(ProofElementID eid, int lineNr) {
254276
builtinInfo.builtinIfInsts.append(new Pair<>(
255277
builtinInfo.currIfInstFormula, builtinInfo.currIfInstPosInTerm));
256278
}
279+
case OPEN_GOAL -> {
280+
parsingOpenGoal = false;
281+
}
257282
default -> {
258283
}
259284
}

‎key.core/src/main/java/de/uka/ilkd/key/proof/io/IntermediateProofReplayer.java‎

Lines changed: 25 additions & 27 deletions
Original file line numberDiff line numberDiff line change
@@ -116,12 +116,15 @@ public class IntermediateProofReplayer {
116116
/** The current open goal */
117117
private Goal currGoal = null;
118118

119+
/** the node selected at time of saving, or null if information is not available */
120+
private Node savedSelectedNode = null;
121+
119122
/**
120123
* Constructs a new {@link IntermediateProofReplayer}.
121124
*
122-
* @param loader The problem loader, for reporting errors.
123-
* @param proof The proof object into which to load the replayed proof.
124-
* @param parserResult the result of the proof file parser to be replayed
125+
* @param loader the problem loader, for reporting errors.
126+
* @param proof the proof object into which to load the replayed proof.
127+
* @param parserResult the result of the intermediate parser to be replayed
125128
*/
126129
public IntermediateProofReplayer(AbstractProblemLoader loader, Proof proof,
127130
IntermediatePresentationProofFileParser.Result parserResult) {
@@ -223,6 +226,7 @@ public Result replay(ProblemInitializer.ProblemInitializerListener listener,
223226
proof.getServices().getNameRecorder()
224227
.setProposals(currInterm.getIntermediateRuleApp().getNewNames());
225228

229+
226230
if (currInterm.getIntermediateRuleApp() instanceof TacletAppIntermediate) {
227231
TacletAppIntermediate appInterm =
228232
(TacletAppIntermediate) currInterm.getIntermediateRuleApp();
@@ -358,6 +362,21 @@ public Result replay(ProblemInitializer.ProblemInitializerListener listener,
358362
}
359363
}
360364
}
365+
// set information if this node was the last selected node at the time of saving
366+
// the
367+
// proof
368+
if (currInterm.getSelectedNode()) {
369+
// check whether the node itself was selected or a child that is an open
370+
// goal
371+
int openChildSelected = currInterm.getOpenChildSelected();
372+
if (openChildSelected < 0
373+
|| openChildSelected >= currNode.childrenCount()) {
374+
savedSelectedNode = currNode;
375+
} else {
376+
savedSelectedNode = currNode.child(openChildSelected);
377+
}
378+
}
379+
361380
}
362381
} catch (Throwable throwable) {
363382
// Default exception catcher -- proof should not stop loading
@@ -374,7 +393,7 @@ public Result replay(ProblemInitializer.ProblemInitializerListener listener,
374393
progressMonitor.setProgress(max);
375394
}
376395
LOGGER.debug("Proof replay took " + PerfScope.formatTime(System.nanoTime() - time));
377-
return new Result(status, errors, currGoal);
396+
return new Result(status, errors, currGoal, savedSelectedNode);
378397
}
379398

380399
/**
@@ -1057,27 +1076,6 @@ static class SkipSMTRuleException extends Exception {
10571076
*
10581077
* @author Dominic Scheurer
10591078
*/
1060-
public static class Result {
1061-
private final String status;
1062-
private final List<Throwable> errors;
1063-
private Goal lastSelectedGoal = null;
1064-
1065-
public Result(String status, List<Throwable> errors, Goal lastSelectedGoal) {
1066-
this.status = status;
1067-
this.errors = errors;
1068-
this.lastSelectedGoal = lastSelectedGoal;
1069-
}
1070-
1071-
public String getStatus() {
1072-
return status;
1073-
}
1074-
1075-
public List<Throwable> getErrors() {
1076-
return errors;
1077-
}
1078-
1079-
public Goal getLastSelectedGoal() {
1080-
return lastSelectedGoal;
1081-
}
1082-
}
1079+
public record Result(String status, List<Throwable> errors, Goal lastSelectedGoal,
1080+
Node savedSelectedNode) {}
10831081
}

‎key.core/src/main/java/de/uka/ilkd/key/proof/io/OutputStreamProofSaver.java‎

Lines changed: 22 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -74,6 +74,10 @@ public class OutputStreamProofSaver {
7474
*/
7575
protected final boolean saveProofSteps;
7676

77+
/**
78+
* The currently selected node if available, otherwise null
79+
*/
80+
protected final Node selectedNode;
7781

7882
/**
7983
* Extracts java source directory from {@link Proof#header()}, if it exists.
@@ -95,27 +99,28 @@ public static File getJavaSourceLocation(Proof proof) {
9599
return null;
96100
}
97101

98-
public OutputStreamProofSaver(Proof proof) {
99-
this(proof, KeYConstants.INTERNAL_VERSION);
102+
public OutputStreamProofSaver(Proof proof, Node selectedNode) {
103+
this(proof, selectedNode, KeYConstants.INTERNAL_VERSION);
100104
}
101105

102-
public OutputStreamProofSaver(Proof proof, String internalVersion) {
103-
this.proof = proof;
104-
this.internalVersion = internalVersion;
105-
this.saveProofSteps = true;
106+
public OutputStreamProofSaver(Proof proof, Node selectedNode, String internalVersion) {
107+
this(proof, selectedNode, internalVersion, true);
106108
}
107109

108110
/**
109111
* Create a new OutputStreamProofSaver.
110112
*
111113
* @param proof the proof to save
114+
* @param selectedNode the Node selected at time of saving or null if no information available
112115
* @param internalVersion currently running KeY version
113116
* @param saveProofSteps whether to save the performed proof steps
114117
*/
115-
public OutputStreamProofSaver(Proof proof, String internalVersion, boolean saveProofSteps) {
118+
public OutputStreamProofSaver(Proof proof, Node selectedNode, String internalVersion,
119+
boolean saveProofSteps) {
116120
this.proof = proof;
117121
this.internalVersion = internalVersion;
118122
this.saveProofSteps = saveProofSteps;
123+
this.selectedNode = selectedNode;
119124
}
120125

121126
/**
@@ -589,7 +594,11 @@ private void printSingleNode(Node node, String prefix, Appendable output) throws
589594

590595
printer.printSequent(node.sequent());
591596
output.append(escapeCharacters(printer.result().replace('\n', ' ')));
592-
output.append("\")\n");
597+
output.append("\"");
598+
if (node == selectedNode) {
599+
output.append(" (" + ProofElementID.SELECTED_NODE.getRawName() + ")");
600+
}
601+
output.append(")\n");
593602
return;
594603
}
595604

@@ -653,10 +662,13 @@ private void collectProof(Node node, String prefix, Appendable output) throws IO
653662
*/
654663
private void userInteraction2Proof(Node node, Appendable output) throws IOException {
655664
if (node.getNodeInfo().getInteractiveRuleApplication()) {
656-
output.append(" (userinteraction)");
665+
output.append(" (" + ProofElementID.USER_INTERACTION.getRawName() + ")");
666+
}
667+
if (node == selectedNode) {
668+
output.append(" (" + ProofElementID.SELECTED_NODE.getRawName() + ")");
657669
}
658670
if (node.getNodeInfo().getScriptRuleApplication()) {
659-
output.append(" (proofscript)");
671+
output.append(" (" + ProofElementID.PROOF_SCRIPT.getRawName() + ")");
660672
}
661673
}
662674

‎key.core/src/main/java/de/uka/ilkd/key/proof/io/ProofBundleSaver.java‎

Lines changed: 4 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -7,6 +7,7 @@
77
import java.io.IOException;
88
import java.nio.file.Paths;
99

10+
import de.uka.ilkd.key.proof.Node;
1011
import de.uka.ilkd.key.proof.Proof;
1112
import de.uka.ilkd.key.proof.io.consistency.AbstractFileRepo;
1213
import de.uka.ilkd.key.proof.io.consistency.FileRepo;
@@ -30,10 +31,11 @@ public class ProofBundleSaver extends ProofSaver {
3031
* Creates a new ProofBundleSaver.
3132
*
3233
* @param proof the proof to save
34+
* @param selectedNode the Node selected at time of saving or null if no information available
3335
* @param saveFile the target filename
3436
*/
35-
public ProofBundleSaver(Proof proof, File saveFile) {
36-
super(proof, saveFile);
37+
public ProofBundleSaver(Proof proof, Node selectedNode, File saveFile) {
38+
super(proof, selectedNode, saveFile);
3739
}
3840

3941
@Override

0 commit comments

Comments
 (0)