From fc5ec0030c77bd66d8dda8a78b259f10c5c276e9 Mon Sep 17 00:00:00 2001 From: Drodt Date: Thu, 8 Jan 2026 14:01:45 +0100 Subject: [PATCH 1/2] Expand OSS apps when saving proof --- .../TruthValueTracingUtil.java | 2 +- .../key/proof/io/OutputStreamProofSaver.java | 38 ++++++++++++++++--- .../de/uka/ilkd/key/proof/io/ProofSaver.java | 16 +++++--- .../uka/ilkd/key/rule/OneStepSimplifier.java | 5 +-- 4 files changed, 46 insertions(+), 15 deletions(-) diff --git a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/TruthValueTracingUtil.java b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/TruthValueTracingUtil.java index bcf25617392..62d018da038 100644 --- a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/TruthValueTracingUtil.java +++ b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/TruthValueTracingUtil.java @@ -261,7 +261,7 @@ private static void evaluateNode( } } else if (parent.getAppliedRuleApp() instanceof OneStepSimplifierRuleApp app) { PosInOccurrence parentPio = null; - for (RuleApp protocolApp : app.getProtocol()) { + for (var protocolApp : app.getProtocol()) { if (parentPio != null) { updatePredicateResultBasedOnNewMinorIdsOSS(protocolApp.posInOccurrence(), parentPio, termLabelName, services.getTermBuilder(), nodeResult); diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/io/OutputStreamProofSaver.java b/key.core/src/main/java/de/uka/ilkd/key/proof/io/OutputStreamProofSaver.java index 0db5b7fd9f5..35d344cffca 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/io/OutputStreamProofSaver.java +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/io/OutputStreamProofSaver.java @@ -82,7 +82,8 @@ public class OutputStreamProofSaver { * Whether the proof steps should be output (usually true). */ protected final boolean saveProofSteps; - + /// Whether steps by the [OneStepSimplifier] should be expanded. + protected final boolean expandOneStepSimplifier; /** * Extracts java source directory from {@link Proof#header()}, if it exists. @@ -97,7 +98,7 @@ public static File getJavaSourceLocation(Proof proof) { final int begin = header.indexOf('\"', i); final int end = header.indexOf('\"', begin + 1); final String sourceLocation = header.substring(begin + 1, end); - if (sourceLocation.length() > 0) { + if (!sourceLocation.isEmpty()) { return new File(sourceLocation); } } @@ -112,6 +113,7 @@ public OutputStreamProofSaver(Proof proof, String internalVersion) { this.proof = proof; this.internalVersion = internalVersion; this.saveProofSteps = true; + this.expandOneStepSimplifier = true; } /** @@ -121,10 +123,12 @@ public OutputStreamProofSaver(Proof proof, String internalVersion) { * @param internalVersion currently running KeY version * @param saveProofSteps whether to save the performed proof steps */ - public OutputStreamProofSaver(Proof proof, String internalVersion, boolean saveProofSteps) { + public OutputStreamProofSaver(Proof proof, String internalVersion, boolean saveProofSteps, + boolean expandOneStepSimplifier) { this.proof = proof; this.internalVersion = internalVersion; this.saveProofSteps = saveProofSteps; + this.expandOneStepSimplifier = expandOneStepSimplifier; } /** @@ -349,7 +353,6 @@ private String newNames2Proof(Node n) { private void printSingleTacletApp(TacletApp appliedRuleApp, Node node, String prefix, Appendable output) throws IOException { - output.append(prefix); output.append("(rule \""); output.append(appliedRuleApp.rule().name().toString()); @@ -546,7 +549,7 @@ private void printRuleJustification(IBuiltInRuleApp appliedRuleApp, Appendable o private void printSingleBuiltInRuleApp(IBuiltInRuleApp appliedRuleApp, Node node, String prefix, Appendable output) throws IOException { output.append(prefix); - output.append(" (builtin \""); + output.append("(builtin \""); output.append(appliedRuleApp.rule().name().toString()); output.append("\""); output.append(posInOccurrence2Proof(node.sequent(), appliedRuleApp.posInOccurrence())); @@ -610,11 +613,35 @@ private void printSingleNode(Node node, String prefix, Appendable output) throws if (appliedRuleApp instanceof TacletApp) { printSingleTacletApp((TacletApp) appliedRuleApp, node, prefix, output); + } else if (expandOneStepSimplifier + && appliedRuleApp instanceof OneStepSimplifierRuleApp ossa) { + printExpandedOneStepSimplifierRuleApp(ossa, node, prefix, output); } else if (appliedRuleApp instanceof IBuiltInRuleApp) { printSingleBuiltInRuleApp((IBuiltInRuleApp) appliedRuleApp, node, prefix, output); } } + private void printExpandedOneStepSimplifierRuleApp(OneStepSimplifierRuleApp ossa, Node node, + String prefix, Appendable output) throws IOException { + OneStepSimplifier.Protocol protocol = ossa.getProtocol(); + for (int i = 0; i < protocol.size(); i++) { + var app = protocol.get(i); + Node n = new Node(node.proof()); + if (i == 0) { + n.setNameRecorder(node.getNameRecorder()); + } + int seqFNum = node.sequent().formulaNumberInSequent(ossa.posInOccurrence()); + Sequent seq = node.sequent() + .replaceFormula(seqFNum, app.posInOccurrence().sequentFormula()).sequent(); + n.setSequent(seq); + if (app instanceof TacletApp ta) { + printSingleTacletApp(ta, n, prefix, output); + } else if (app instanceof IBuiltInRuleApp ba) { + printSingleBuiltInRuleApp(ba, n, prefix, output); + } + } + } + /** * Print applied rule(s) for a proof node and its decendants into the passed writer. * @@ -624,7 +651,6 @@ private void printSingleNode(Node node, String prefix, Appendable output) throws * @throws IOException an exception thrown when printing fails */ private void collectProof(Node node, String prefix, Appendable output) throws IOException { - printSingleNode(node, prefix, output); Iterator childrenIt; diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/io/ProofSaver.java b/key.core/src/main/java/de/uka/ilkd/key/proof/io/ProofSaver.java index 48148ff405a..f3a1516ab6f 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/io/ProofSaver.java +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/io/ProofSaver.java @@ -50,7 +50,7 @@ public static void saveToFile(Path file, Proof proof) throws IOException { * @throws IOException on any I/O error */ public static void saveProofObligationToFile(Path file, Proof proof) throws IOException { - ProofSaver saver = new ProofSaver(proof, file, false); + ProofSaver saver = new ProofSaver(proof, file, false, false); saver.save(); } @@ -88,9 +88,12 @@ public ProofSaver(Proof proof, Path file, String internalVersion) { * @param proof proof to save * @param file file to save proof into * @param saveProofSteps whether to save proof steps (false -> only proof obligation) + * @param expandOneStepSimplifier whether to expand + * {@link de.uka.ilkd.key.rule.OneStepSimplifier} rule apps */ - public ProofSaver(Proof proof, Path file, boolean saveProofSteps) { - this(proof, file, KeYConstants.INTERNAL_VERSION, saveProofSteps); + public ProofSaver(Proof proof, Path file, boolean saveProofSteps, + boolean expandOneStepSimplifier) { + this(proof, file, KeYConstants.INTERNAL_VERSION, saveProofSteps, expandOneStepSimplifier); } /** @@ -100,9 +103,12 @@ public ProofSaver(Proof proof, Path file, boolean saveProofSteps) { * @param file file to save proof into * @param internalVersion version of KeY to add to the proof log * @param saveProofSteps whether to save proof steps (false -> only proof obligation) + * @param expandOneStepSimplifier whether to expand + * {@link de.uka.ilkd.key.rule.OneStepSimplifier} rule apps */ - public ProofSaver(Proof proof, Path file, String internalVersion, boolean saveProofSteps) { - super(proof, internalVersion, saveProofSteps); + public ProofSaver(Proof proof, Path file, String internalVersion, boolean saveProofSteps, + boolean expandOneStepSimplifier) { + super(proof, internalVersion, saveProofSteps, expandOneStepSimplifier); this.file = file; } diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/OneStepSimplifier.java b/key.core/src/main/java/de/uka/ilkd/key/rule/OneStepSimplifier.java index 5f5d6cb4986..a405ea2862c 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/OneStepSimplifier.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/OneStepSimplifier.java @@ -419,7 +419,7 @@ private RuleApp makeReplaceKnownTacletApp(JTerm formula, SVInstantiations svi = SVInstantiations.EMPTY_SVINSTANTIATIONS; FormulaSV sv = SchemaVariableFactory.createFormulaSV(new Name("b")); - svi.add(sv, (JTerm) pio.sequentFormula().formula(), lastProof.getServices()); + svi.add(sv, pio.sequentFormula().formula(), lastProof.getServices()); PosInOccurrence applicatinPIO = new PosInOccurrence(new SequentFormula(formula), PosInTerm.getTopLevel(), // TODO: This @@ -431,9 +431,8 @@ private RuleApp makeReplaceKnownTacletApp(JTerm formula, // renamings and term labels ImmutableList ifInst = ImmutableSLList.nil(); ifInst = ifInst.append(new AssumesFormulaInstDirect(pio.sequentFormula())); - TacletApp ta = PosTacletApp.createPosTacletApp(taclet, svi, ifInst, applicatinPIO, + return PosTacletApp.createPosTacletApp(taclet, svi, ifInst, applicatinPIO, lastProof.getServices()); - return ta; } /** From 0e769f9e134a94ceec15a1beb3ab43748b6e781a Mon Sep 17 00:00:00 2001 From: Drodt Date: Thu, 8 Jan 2026 14:17:40 +0100 Subject: [PATCH 2/2] Print whether a node is an OSS step --- .../ilkd/key/proof/io/IProofFileParser.java | 2 +- .../key/proof/io/OutputStreamProofSaver.java | 22 +++++++++++++++++-- 2 files changed, 21 insertions(+), 3 deletions(-) diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/io/IProofFileParser.java b/key.core/src/main/java/de/uka/ilkd/key/proof/io/IProofFileParser.java index aa958b4efe6..b0b09fb1f39 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/io/IProofFileParser.java +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/io/IProofFileParser.java @@ -34,7 +34,7 @@ enum ProofElementID { USER_INTERACTION("userinteraction"), PROOF_SCRIPT("proofscript"), NEW_NAMES("newnames"), AUTOMODE_TIME("autoModeTime"), KeY_LOG("keyLog"), KeY_USER("keyUser"), KeY_VERSION("keyVersion"), KeY_SETTINGS("keySettings"), OPEN_GOAL("opengoal"), - NOTES("notes"), SOLVERTYPE("solverType"), MODALITY("modality"); + NOTES("notes"), SOLVERTYPE("solverType"), MODALITY("modality"), OSS_STEP("ossStep"); private final String rawName; diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/io/OutputStreamProofSaver.java b/key.core/src/main/java/de/uka/ilkd/key/proof/io/OutputStreamProofSaver.java index 35d344cffca..ac5a5d65826 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/io/OutputStreamProofSaver.java +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/io/OutputStreamProofSaver.java @@ -350,9 +350,22 @@ private String newNames2Proof(Node n) { * @param output the writer in which the rule is printed * @throws IOException an exception thrown when printing fails */ - private void printSingleTacletApp(TacletApp appliedRuleApp, Node node, String prefix, Appendable output) throws IOException { + printSingleTacletApp(appliedRuleApp, node, prefix, output, false); + } + + /** + * Print applied taclet rule for a single taclet rule application into the passed writer. + * + * @param appliedRuleApp the rule application to be printed + * @param prefix a string which the printed rule is concatenated to + * @param output the writer in which the rule is printed + * @param isOSSStep whether this node is an expanded OSS rule app step + * @throws IOException an exception thrown when printing fails + */ + private void printSingleTacletApp(TacletApp appliedRuleApp, Node node, String prefix, + Appendable output, boolean isOSSStep) throws IOException { output.append(prefix); output.append("(rule \""); output.append(appliedRuleApp.rule().name().toString()); @@ -367,6 +380,9 @@ private void printSingleTacletApp(TacletApp appliedRuleApp, Node node, String pr } output.append(""); userInteraction2Proof(node, output); + if (isOSSStep) { + output.append(" (ossStep)"); + } notes2Proof(node, output); output.append(")\n"); } @@ -635,8 +651,10 @@ private void printExpandedOneStepSimplifierRuleApp(OneStepSimplifierRuleApp ossa .replaceFormula(seqFNum, app.posInOccurrence().sequentFormula()).sequent(); n.setSequent(seq); if (app instanceof TacletApp ta) { - printSingleTacletApp(ta, n, prefix, output); + printSingleTacletApp(ta, n, prefix, output, true); } else if (app instanceof IBuiltInRuleApp ba) { + // This case does not currently happen, but just in case any built-ins get added to + // the OSS... printSingleBuiltInRuleApp(ba, n, prefix, output); } }