Skip to content

Commit 0bb9c02

Browse files
unp1unp1
committed
This commit addresses issue #3297. Feature: If possible save the last selected node in the proof, to reselect it upon loading.
1 parent 9d102b5 commit 0bb9c02

File tree

24 files changed

+175
-84
lines changed

24 files changed

+175
-84
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
@@ -742,15 +742,17 @@ private ReplayResult replayProof(Proof proof) {
742742
replayResult =
743743
replayer.replay(problemInitializer.getListener(), problemInitializer.getProgMon());
744744

745-
lastTouchedNode = replayResult.getLastSelectedGoal() != null
746-
? replayResult.getLastSelectedGoal().node()
747-
: proof.root();
745+
lastTouchedNode =
746+
replayResult.savedSelectedNode() != null ? replayResult.savedSelectedNode()
747+
: replayResult.lastSelectedGoal() != null
748+
? replayResult.lastSelectedGoal().node()
749+
: proof.root();
748750

749751
} catch (Exception e) {
750752
if (parserResult == null || parserResult.errors() == null
751753
|| parserResult.errors().isEmpty() || replayer == null
752-
|| replayResult == null || replayResult.getErrors() == null
753-
|| replayResult.getErrors().isEmpty()) {
754+
|| replayResult == null || replayResult.errors() == null
755+
|| replayResult.errors().isEmpty()) {
754756
// this exception was something unexpected
755757
errors.add(e);
756758
}
@@ -760,10 +762,10 @@ private ReplayResult replayProof(Proof proof) {
760762
errors.addAll(parserResult.errors());
761763
}
762764
status += (status.isEmpty() ? "Proof replayed successfully." : "\n\n")
763-
+ (replayResult != null ? replayResult.getStatus()
765+
+ (replayResult != null ? replayResult.status()
764766
: "Error while loading proof.");
765767
if (replayResult != null) {
766-
errors.addAll(replayResult.getErrors());
768+
errors.addAll(replayResult.errors());
767769
}
768770

769771
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
@@ -146,7 +146,7 @@ private void save(final String filename, final Proof proof) {
146146
// there may be concurrent changes to the proof... whatever
147147
final Runnable r = () -> {
148148
try {
149-
new ProofSaver(proof, filename, KeYConstants.INTERNAL_VERSION).save();
149+
new ProofSaver(proof, null, filename, KeYConstants.INTERNAL_VERSION).save();
150150
LOGGER.info("File saved: {}", filename);
151151
} catch (Exception e) {
152152
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
@@ -33,7 +33,7 @@ enum ProofElementID {
3333
USER_INTERACTION("userinteraction"), PROOF_SCRIPT("proofscript"), NEW_NAMES("newnames"),
3434
AUTOMODE_TIME("autoModeTime"), KeY_LOG("keyLog"), KeY_USER("keyUser"),
3535
KeY_VERSION("keyVersion"), KeY_SETTINGS("keySettings"), OPEN_GOAL("opengoal"),
36-
NOTES("notes"), SOLVERTYPE("solverType"), MODALITY("modality");
36+
NOTES("notes"), SOLVERTYPE("solverType"), MODALITY("modality"), SELECTED_NODE("selected");
3737

3838
private final String rawName;
3939

‎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
@@ -72,6 +72,7 @@ public class IntermediatePresentationProofFileParser implements IProofFileParser
7272
private BranchNodeIntermediate root = null; // the "dummy ID" branch
7373
private NodeIntermediate currNode;
7474
private final LinkedList<Throwable> errors = new LinkedList<>();
75+
private boolean parsingOpenGoal = false;
7576

7677
/**
7778
* @param proof Proof object for storing meta information about the parsed proof.
@@ -218,6 +219,9 @@ public void beginExpr(ProofElementID eid, String str) {
218219
}
219220
}
220221
case SOLVERTYPE -> ((BuiltinRuleInformation) ruleInfo).solver = str;
222+
case OPEN_GOAL -> {
223+
parsingOpenGoal = true;
224+
}
221225
default -> {
222226
}
223227
}
@@ -233,6 +237,24 @@ public void endExpr(ProofElementID eid, int lineNr) {
233237
((AppNodeIntermediate) currNode).setInteractiveRuleApplication(true);
234238
}
235239
}
240+
case SELECTED_NODE -> {
241+
int openGoalChildSelected = -1;
242+
if (parsingOpenGoal) {
243+
if (currNode instanceof BranchNodeIntermediate branchNode) {
244+
if (!stack.isEmpty()) {
245+
if (stack.peek() instanceof AppNodeIntermediate parentAppNode) {
246+
openGoalChildSelected = parentAppNode.getChildren().size() - 1;
247+
parentAppNode.setSelectedNode(true, openGoalChildSelected);
248+
}
249+
}
250+
} else {
251+
openGoalChildSelected = 0;
252+
}
253+
}
254+
if (currNode != null && currNode instanceof AppNodeIntermediate appNode) {
255+
appNode.setSelectedNode(true, openGoalChildSelected);
256+
}
257+
}
236258
case PROOF_SCRIPT -> {
237259
if (currNode != null) {
238260
((AppNodeIntermediate) currNode).setScriptRuleApplication(true);
@@ -252,6 +274,9 @@ public void endExpr(ProofElementID eid, int lineNr) {
252274
builtinInfo.builtinIfInsts.append(new Pair<>(
253275
builtinInfo.currIfInstFormula, builtinInfo.currIfInstPosInTerm));
254276
}
277+
case OPEN_GOAL -> {
278+
parsingOpenGoal = false;
279+
}
255280
default -> {
256281
}
257282
}

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

Lines changed: 23 additions & 25 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
*
122125
* @param loader The problem loader, for reporting errors.
123126
* @param proof The proof object into which to load the replayed proof.
124-
* @param intermediate
127+
* @param parserResult 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: 23 additions & 11 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 selectedNodeNr;
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.selectedNodeNr = 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 == selectedNodeNr) {
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 == selectedNodeNr) {
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

@@ -716,7 +728,7 @@ public static String posInTerm2Proof(PosInTerm pos) {
716728
/**
717729
* Get the "interesting" instantiations of the provided object.
718730
*
719-
* @see SVInstantiations#interesting
731+
* @see SVInstantiations#interesting()
720732
* @param inst instantiations
721733
* @return the "interesting" instantiations (serialized)
722734
*/

‎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)