From 067ff852cd2429ef7e9a96ec4fcb72cadecc2374 Mon Sep 17 00:00:00 2001 From: Alexander Weigl Date: Thu, 28 Dec 2023 03:14:14 +0100 Subject: [PATCH 1/3] select last node --- .../java/de/uka/ilkd/key/nparser/KeyAst.java | 12 +- .../main/java/de/uka/ilkd/key/proof/Node.java | 115 ++++++++----- .../key/proof/init/KeYUserProblemFile.java | 12 ++ .../key/proof/io/OutputStreamProofSaver.java | 156 ++++++++++++------ .../ilkd/key/proof/io/ProofBundleSaver.java | 4 +- .../uka/ilkd/key/settings/Configuration.java | 15 +- .../uka/ilkd/key/settings/ProofSettings.java | 59 ++++--- .../key/gui/WindowUserInterfaceControl.java | 20 ++- .../util/collection/KeYCollections.java | 118 ++++++++++++- .../util/collection/KeYCollectionsTest.java | 57 +++++++ 10 files changed, 447 insertions(+), 121 deletions(-) create mode 100644 key.util/src/test/java/org/key_project/util/collection/KeYCollectionsTest.java diff --git a/key.core/src/main/java/de/uka/ilkd/key/nparser/KeyAst.java b/key.core/src/main/java/de/uka/ilkd/key/nparser/KeyAst.java index e3e50418712..3a4925082c3 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/nparser/KeyAst.java +++ b/key.core/src/main/java/de/uka/ilkd/key/nparser/KeyAst.java @@ -123,10 +123,20 @@ public static class File extends KeyAst { } else { return new KeyAst.ProofScript(pctx.proofScript()); } + /** + * Returns the raw settings within a {@link de.uka.ilkd.key.proof.io.KeYFile}. + */ + public Configuration findSettings() { + final var cfg = new ConfigurationBuilder(); + if (ctx.preferences() == null || ctx.preferences().cvalue() == null) { + return new Configuration(); } - return null; + + var c = ctx.preferences().cvalue(); + return (Configuration) c.accept(cfg); } + /// Returns the includes (possible empty but not null) computed from the underlying parse /// tree. public Includes getIncludes(URL base) { diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/Node.java b/key.core/src/main/java/de/uka/ilkd/key/proof/Node.java index 93c58da43ce..5421fa70a17 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/Node.java +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/Node.java @@ -3,16 +3,6 @@ * SPDX-License-Identifier: GPL-2.0-only */ package de.uka.ilkd.key.proof; -import java.util.ArrayList; -import java.util.Collection; -import java.util.Collections; -import java.util.HashSet; -import java.util.Iterator; -import java.util.LinkedHashSet; -import java.util.LinkedList; -import java.util.List; -import java.util.ListIterator; - import de.uka.ilkd.key.logic.RenamingTable; import de.uka.ilkd.key.logic.op.IProgramVariable; import de.uka.ilkd.key.proof.calculus.JavaDLSequentKit; @@ -24,6 +14,9 @@ import org.key_project.prover.rules.RuleApp; import org.key_project.prover.sequent.Sequent; import org.key_project.prover.sequent.SequentChangeInfo; +import de.uka.ilkd.key.util.Pair; +import org.jspecify.annotations.NonNull; +import org.jspecify.annotations.Nullable; import org.key_project.util.collection.DefaultImmutableSet; import org.key_project.util.collection.ImmutableList; import org.key_project.util.collection.ImmutableSLList; @@ -31,8 +24,7 @@ import org.key_project.util.collection.Pair; import org.key_project.util.lookup.Lookup; -import org.jspecify.annotations.NonNull; -import org.jspecify.annotations.Nullable; +import java.util.*; public class Node implements Iterable { private static final String RULE_WITHOUT_NAME = "rule without name"; @@ -50,10 +42,14 @@ public class Node implements Iterable { private static final String NODES = "nodes"; - /** the proof the node belongs to */ + /** + * the proof the node belongs to + */ private final Proof proof; - /** The parent node. **/ + /** + * The parent node. + **/ private @Nullable Node parent = null; /** * The branch location of this proof node. @@ -82,7 +78,9 @@ public class Node implements Iterable { private boolean closed = false; - /** contains non-logical content, used for user feedback */ + /** + * contains non-logical content, used for user feedback + */ private NodeInfo nodeInfo; /** @@ -118,7 +116,7 @@ public class Node implements Iterable { * taclet with an addrule section on this node, then these taclets are stored in this list */ private ImmutableSet localIntroducedRules = - DefaultImmutableSet.nil(); + DefaultImmutableSet.nil(); /** * Holds the undo methods for the information added by rules to the {@code Goal.strategyInfos}. @@ -161,7 +159,9 @@ public void setSequent(Sequent seq) { this.seq = seq; } - /** returns the sequent of this node */ + /** + * returns the sequent of this node + */ public Sequent sequent() { return seq; } @@ -175,7 +175,9 @@ public NodeInfo getNodeInfo() { return nodeInfo; } - /** returns the proof the Node belongs to */ + /** + * returns the proof the Node belongs to + */ public Proof proof() { return proof; } @@ -225,7 +227,9 @@ public RuleApp getAppliedRuleApp() { return appliedRuleApp; } - /** Returns the set of NoPosTacletApps at this node */ + /** + * Returns the set of NoPosTacletApps at this node + */ public Iterable getLocalIntroducedRules() { return localIntroducedRules; } @@ -249,7 +253,7 @@ public void addLocalProgVars(Iterable elements) { /** * Returns the set of freshly created function symbols known to this node. - * + *

* In the resulting list, the newest additions come first. * * @return a non-null immutable list of function symbols. @@ -444,7 +448,7 @@ List getLeaves() { /** * @return an iterator for the leaves of the subtree below this node. The computation is called - * at every call! + * at every call! */ public Iterator leavesIterator() { return new NodeIterator(getLeaves().iterator()); @@ -471,13 +475,14 @@ public Iterator subtreeIterator() { return new SubtreeIterator(this); } - /** @return number of children */ + /** + * @return number of children + */ public int childrenCount() { return children.size(); } /** - * * @param i an index (starting at 0). * @return the i-th child of this node. */ @@ -488,7 +493,7 @@ public Node child(int i) { /** * @param child a child of this node. * @return the number of the node child, if it is a child of this node (starting - * with 0), -1 otherwise + * with 0), -1 otherwise */ public int getChildNr(Node child) { int res = 0; @@ -528,16 +533,16 @@ public StringBuffer getUniqueTacletId() { * Helper for {@link #toString()} * * @param prefix needed to keep track if a line has to be printed - * @param tree the tree representation we want to add this subtree " @param preEnumeration the - * enumeration of the parent without the last number + * @param tree the tree representation we want to add this subtree " @param preEnumeration the + * enumeration of the parent without the last number * @param postNr the last number of the parents enumeration - * @param maxNr the number of nodes at this level - * @param ownNr the place of this node at this level + * @param maxNr the number of nodes at this level + * @param ownNr the place of this node at this level * @return the string representation of this node. */ private StringBuffer toString(String prefix, StringBuffer tree, String preEnumeration, - int postNr, int maxNr, int ownNr) { + int postNr, int maxNr, int ownNr) { Iterator childrenIt = childrenIterator(); // Some constants String frontIndent = (maxNr > 1 ? " " : ""); @@ -588,7 +593,7 @@ private StringBuffer toString(String prefix, StringBuffer tree, String preEnumer while (childrenIt.hasNext()) { childId++; childrenIt.next().toString(prefix, tree, newEnumeration, newPostNr, children.size(), - childId); + childId); } return tree; @@ -645,7 +650,7 @@ public String name() { * this node. * * @return true iff the parent of this node has this node as child and this condition holds also - * for the own children. + * for the own children. */ public boolean sanityCheckDoubleLinks() { if (!root()) { @@ -667,7 +672,9 @@ public boolean sanityCheckDoubleLinks() { return true; } - /** marks a node as closed */ + /** + * marks a node as closed + */ Node close() { closed = true; Node tmp = parent; @@ -684,7 +691,7 @@ Node close() { /** * Opens a previously closed node and all its closed parents. *

- * + *

* This is, for instance, needed for the {@link MergeRule}: In a situation where a merge node * and its associated partners have been closed and the merge node is then pruned away, the * partners have to be reopened again. Otherwise, we have a soundness issue. @@ -699,7 +706,9 @@ void reopen() { clearNameCache(); } - /** @return true iff this inner node is closeable */ + /** + * @return true iff this inner node is closeable + */ private boolean isCloseable() { assert childrenCount() > 0; for (Node child : children) { @@ -768,7 +777,7 @@ public void addStrategyInfoUndoMethod(StrategyInfoUndoMethod undoMethod) { /** * Register a user-defined data in this node info. * - * @param obj an object to be registered + * @param obj an object to be registered * @param service the key under it should be registered * @param the type of the object to be registered */ @@ -779,9 +788,9 @@ public void register(T obj, Class service) { /** * Remove a previous registered user-defined data. * - * @param obj registered object + * @param obj registered object * @param service the key under which the data was registered - * @param arbitray object + * @param arbitray object */ public void deregister(T obj, Class service) { if (userData != null) { @@ -838,4 +847,36 @@ public int getStepIndex() { void setStepIndex(int stepIndex) { this.stepIndex = stepIndex; } + + /** + * Calculates an array is the path from root node to this node. Each entry defines the child to be selected. + * + * @see #traversePath(Iterator) + */ + public int[] getPosInProof() { + // collect the path from the current to node to the root of the proof. + // each entry is the children position + var path = new LinkedList(); + var current = this; + while (current.parent != null) { + path.add(0, current.parent.getChildNr(current)); + current = current.parent; + } + return path.stream().mapToInt(it -> it).toArray(); + } + + + /** + * Traverses a given iterator (child selection). + * + * @param traverse non-null + */ + public Node traversePath(Iterator traverse) { + var current = this; + while (traverse.hasNext()) { + int child = traverse.next(); + current = current.child(child); + } + return current; + } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/init/KeYUserProblemFile.java b/key.core/src/main/java/de/uka/ilkd/key/proof/init/KeYUserProblemFile.java index 7e9e1fe64b9..9c2bb61f73c 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/init/KeYUserProblemFile.java +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/init/KeYUserProblemFile.java @@ -9,6 +9,7 @@ import de.uka.ilkd.key.java.abstraction.KeYJavaType; import de.uka.ilkd.key.nparser.*; +import de.uka.ilkd.key.nparser.builder.ProblemFinder; import de.uka.ilkd.key.proof.Proof; import de.uka.ilkd.key.proof.ProofAggregate; import de.uka.ilkd.key.proof.io.IProofFileParser; @@ -34,8 +35,12 @@ * obligation. */ public final class KeYUserProblemFile extends KeYFile implements ProofOblInput { + @Nullable private Sequent problem = null; + @Nullable + private Configuration settings; + // ------------------------------------------------------------------------- // constructors // ------------------------------------------------------------------------- @@ -119,6 +124,13 @@ public ImmutableSet read() throws ProofInputException { return warnings; } + public Configuration readSettings() { + if(settings==null){ + settings = getParseContext().findSettings(); + } + return settings; + } + @Override public void readProblem() throws ProofInputException { if (initConfig == null) { 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..fd23ed04092 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 @@ -62,26 +62,39 @@ import org.slf4j.Logger; import org.slf4j.LoggerFactory; +import java.io.*; +import java.nio.charset.StandardCharsets; +import java.util.*; + /** * Saves a proof to a given {@link OutputStream}. * * @author Kai Wallisch */ +@NullMarked public class OutputStreamProofSaver { private static final Logger LOGGER = LoggerFactory.getLogger(OutputStreamProofSaver.class); + public static final String KEY_LAST_SELECTED_NODE = "lastSelectedNode"; /** * The proof to save. */ - protected final Proof proof; + private Proof proof; + /** * Currently running KeY version (usually a git commit hash). */ - protected final String internalVersion; + private String internalVersion; + /** * Whether the proof steps should be output (usually true). */ - protected final boolean saveProofSteps; + private boolean saveProofSteps; + + /** + * Last selected node in this proof + */ + private int @Nullable [] pathToLastSelectedNode = null; /** @@ -90,6 +103,7 @@ public class OutputStreamProofSaver { * @param proof the Proof * @return the location of the java source code or null if no such exists */ + @Nullable public static File getJavaSourceLocation(Proof proof) { final String header = proof.header(); final int i = header.indexOf("\\javaSource"); @@ -97,7 +111,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); } } @@ -117,9 +131,9 @@ public OutputStreamProofSaver(Proof proof, String internalVersion) { /** * Create a new OutputStreamProofSaver. * - * @param proof the proof to save + * @param proof the proof to save * @param internalVersion currently running KeY version - * @param saveProofSteps whether to save the performed proof steps + * @param saveProofSteps whether to save the performed proof steps */ public OutputStreamProofSaver(Proof proof, String internalVersion, boolean saveProofSteps) { this.proof = proof; @@ -157,14 +171,20 @@ public String writeProfile(Profile profile) { } public String writeSettings(ProofSettings ps) { - return String.format("\\settings %s \n", ps.settingsToString()); + // inject the last selected node + var additionalInformation = new TreeMap(); + if(pathToLastSelectedNode!=null) { + var lastSelectedNode = KeYCollections.runLengthEncoding(pathToLastSelectedNode); + additionalInformation.put(KEY_LAST_SELECTED_NODE, lastSelectedNode); + } + return String.format("\\settings %s \n", ps.settingsToString(additionalInformation)); } public void save(OutputStream out) throws IOException { CopyReferenceResolver.copyCachedGoals(proof, null, null, null); try (var ps = new PrintWriter(out, true, StandardCharsets.UTF_8)) { final ProofOblInput po = - proof.getServices().getSpecificationRepository().getProofOblInput(proof); + proof.getServices().getSpecificationRepository().getProofOblInput(proof); LogicPrinter printer = createLogicPrinter(proof.getServices(), false); // profile @@ -173,11 +193,11 @@ public void save(OutputStream out) throws IOException { // settings final StrategySettings strategySettings = proof.getSettings().getStrategySettings(); final StrategyProperties strategyProperties = - strategySettings.getActiveStrategyProperties(); + strategySettings.getActiveStrategyProperties(); if (po instanceof AbstractInfFlowPO && (po instanceof InfFlowCompositePO || !((InfFlowProof) proof).getIFSymbols().isFreshContract())) { strategyProperties.put(StrategyProperties.INF_FLOW_CHECK_PROPERTY, - StrategyProperties.INF_FLOW_CHECK_TRUE); + StrategyProperties.INF_FLOW_CHECK_TRUE); strategySettings.setActiveStrategyProperties(strategyProperties); for (final SequentFormula s : proof.root().sequent() .succedent().asList()) { @@ -185,7 +205,7 @@ public void save(OutputStream out) throws IOException { } } else { strategyProperties.put(StrategyProperties.INF_FLOW_CHECK_PROPERTY, - StrategyProperties.INF_FLOW_CHECK_FALSE); + StrategyProperties.INF_FLOW_CHECK_FALSE); strategySettings.setActiveStrategyProperties(strategyProperties); } ps.println(writeSettings(proof.getSettings())); @@ -193,7 +213,7 @@ public void save(OutputStream out) throws IOException { if (po instanceof AbstractInfFlowPO && (po instanceof InfFlowCompositePO || !((InfFlowProof) proof).getIFSymbols().isFreshContract())) { strategyProperties.put(StrategyProperties.INF_FLOW_CHECK_PROPERTY, - StrategyProperties.INF_FLOW_CHECK_FALSE); + StrategyProperties.INF_FLOW_CHECK_FALSE); strategySettings.setActiveStrategyProperties(strategyProperties); } @@ -205,7 +225,7 @@ public void save(OutputStream out) throws IOException { // \problem or \proofObligation if (po instanceof IPersistablePO ppo && (!(po instanceof AbstractInfFlowPO) || (!(po instanceof InfFlowCompositePO) - && ((InfFlowProof) proof).getIFSymbols().isFreshContract()))) { + && ((InfFlowProof) proof).getIFSymbols().isFreshContract()))) { var loadingConfig = ppo.createLoaderConfig(); ps.println("\\proofObligation "); loadingConfig.save(ps, ""); @@ -239,6 +259,7 @@ public void save(OutputStream out) throws IOException { } } + @Nullable protected Path getBasePath() throws IOException { File javaSourceLocation = getJavaSourceLocation(proof); if (javaSourceLocation != null) { @@ -261,8 +282,8 @@ protected Path getBasePath() throws IOException { */ private String makePathsRelative(String header) { final String[] search = - { "\\javaSource", "\\bootclasspath", "\\classpath", "\\include" }; - final String basePath; + {"\\javaSource", "\\bootclasspath", "\\classpath", "\\include"}; + String basePath; String tmp = header; try { basePath = getBasePath().toString(); @@ -342,13 +363,13 @@ private String newNames2Proof(Node n) { * 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 prefix a string which the printed rule is concatenated to + * @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 { + Appendable output) throws IOException { output.append(prefix); output.append("(rule \""); @@ -372,11 +393,11 @@ private void printSingleTacletApp(TacletApp appliedRuleApp, Node node, String pr * Print predicates for applied merge rule application into the passed writer. * * @param predAbstrRule the rule application with the predicates to be printed - * @param output the writer in which the rule is printed + * @param output the writer in which the rule is printed * @throws IOException an exception thrown when printing fails */ private void printPredicatesForSingleMergeRuleApp(MergeWithPredicateAbstraction predAbstrRule, - Appendable output) throws IOException { + Appendable output) throws IOException { output.append("(").append(ProofElementID.MERGE_ABSTRACTION_PREDICATES.getRawName()) .append(" \""); boolean first = true; @@ -407,13 +428,13 @@ private void printPredicatesForSingleMergeRuleApp(MergeWithPredicateAbstraction * Print predicates for applied merge rule application into the passed writer. * * @param concreteRule the rule application with the abstract domain to be printed - * @param output the writer in which the rule is printed + * @param output the writer in which the rule is printed * @throws IOException an exception thrown when printing fails */ private void printLatticeAbstractionForSingleMergeRuleApp( MergeWithLatticeAbstraction concreteRule, Appendable output) throws IOException { final Map userChoices = - concreteRule.getUserChoices(); + concreteRule.getUserChoices(); if (!userChoices.isEmpty()) { output.append(" (").append(ProofElementID.MERGE_USER_CHOICES.getRawName()) @@ -441,12 +462,12 @@ private void printLatticeAbstractionForSingleMergeRuleApp( * Print applied merge rule for a single merge rule application into the passed writer. * * @param mergeApp 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 prefix a string which the printed rule is concatenated to + * @param output the writer in which the rule is printed * @throws IOException an exception thrown when printing fails */ private void printSingleMergeRuleApp(MergeRuleBuiltInRuleApp mergeApp, Node node, String prefix, - Appendable output) throws IOException { + Appendable output) throws IOException { final MergeProcedure concreteRule = mergeApp.getConcreteRule(); output.append(" (").append(ProofElementID.MERGE_PROCEDURE.getRawName()).append(" \""); @@ -465,8 +486,8 @@ private void printSingleMergeRuleApp(MergeRuleBuiltInRuleApp mergeApp, Node node output.append(" (").append(ProofElementID.MERGE_DIST_FORMULA.getRawName()) .append(" \""); output.append(escapeCharacters( - printAnything(mergeApp.getDistinguishingFormula(), proof.getServices(), false) - .trim().replaceAll("(\\r|\\n|\\r\\n)+", ""))); + printAnything(mergeApp.getDistinguishingFormula(), proof.getServices(), false) + .trim().replaceAll("(\\r|\\n|\\r\\n)+", ""))); output.append("\")"); } @@ -475,12 +496,12 @@ private void printSingleMergeRuleApp(MergeRuleBuiltInRuleApp mergeApp, Node node && ((MergeWithPredicateAbstraction) concreteRule).getPredicates().size() > 0) { printPredicatesForSingleMergeRuleApp((MergeWithPredicateAbstraction) concreteRule, - output); + output); } if (concreteRule instanceof MergeWithLatticeAbstraction) { printLatticeAbstractionForSingleMergeRuleApp((MergeWithLatticeAbstraction) concreteRule, - output); + output); } } @@ -498,7 +519,7 @@ private void printSingleMergeRuleApp(MergeRuleBuiltInRuleApp mergeApp, Node node * @throws IOException an exception thrown when printing fails */ private void printSingleCloseAfterMergeRuleApp(CloseAfterMergeRuleBuiltInRuleApp closeApp, - Node node, String prefix, Appendable output) throws IOException { + Node node, String prefix, Appendable output) throws IOException { // TODO (DS): There may be problems here if the merge node is // pruned away. Need to test some cases and either check for @@ -509,7 +530,7 @@ private void printSingleCloseAfterMergeRuleApp(CloseAfterMergeRuleBuiltInRuleApp } private void printSingleSMTRuleApp(SMTRuleApp smtApp, Node node, String prefix, - Appendable output) throws IOException { + Appendable output) throws IOException { output.append(" (").append(ProofElementID.SOLVERTYPE.getRawName()) .append(" \"").append(smtApp.getSuccessfulSolverName()).append("\")"); } @@ -518,7 +539,7 @@ private void printSingleSMTRuleApp(SMTRuleApp smtApp, Node node, String prefix, * Print rule justification for applied built-in rule application into the passed writer. * * @param appliedRuleApp the rule application to be printed - * @param output the writer in which the rule is printed + * @param output the writer in which the rule is printed * @throws IOException an exception thrown when printing fails */ private void printRuleJustification(IBuiltInRuleApp appliedRuleApp, Appendable output) @@ -539,12 +560,12 @@ private void printRuleJustification(IBuiltInRuleApp appliedRuleApp, Appendable o * Print applied built-in rule for a single built-in 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 prefix a string which the printed rule is concatenated to + * @param output the writer in which the rule is printed * @throws IOException an exception thrown when printing fails */ private void printSingleBuiltInRuleApp(IBuiltInRuleApp appliedRuleApp, Node node, String prefix, - Appendable output) throws IOException { + Appendable output) throws IOException { output.append(prefix); output.append(" (builtin \""); output.append(appliedRuleApp.rule().name().toString()); @@ -575,7 +596,7 @@ private void printSingleBuiltInRuleApp(IBuiltInRuleApp appliedRuleApp, Node node if (appliedRuleApp instanceof CloseAfterMergeRuleBuiltInRuleApp) { printSingleCloseAfterMergeRuleApp((CloseAfterMergeRuleBuiltInRuleApp) appliedRuleApp, - node, prefix, output); + node, prefix, output); } else if (appliedRuleApp instanceof SMTRuleApp) { printSingleSMTRuleApp((SMTRuleApp) appliedRuleApp, node, prefix, output); } @@ -589,7 +610,7 @@ private void printSingleBuiltInRuleApp(IBuiltInRuleApp appliedRuleApp, Node node /** * Print applied rule (s) for a single proof node into the passed writer. * - * @param node the proof node to be printed + * @param node the proof node to be printed * @param prefix a string which the printed rules are concatenated to * @param output the writer in which the rule(s) is /are printed * @throws IOException an exception thrown when printing fails @@ -618,7 +639,7 @@ private void printSingleNode(Node node, String prefix, Appendable output) throws /** * Print applied rule(s) for a proof node and its decendants into the passed writer. * - * @param node the proof node from which to be printed + * @param node the proof node from which to be printed * @param prefix a string which the printed rules are concatenated to * @param output the writer in which the rule(s) is/are printed * @throws IOException an exception thrown when printing fails @@ -662,7 +683,7 @@ private void collectProof(Node node, String prefix, Appendable output) throws IO * Check whether the applied rule of the passed proof node was performed interactively. If this * is the case, a user interaction label is appended. * - * @param node the proof node to be checked + * @param node the proof node to be checked * @param output the writer to which the label should be appended * @throws IOException an exception thrown in case printing fails */ @@ -678,7 +699,7 @@ private void userInteraction2Proof(Node node, Appendable output) throws IOExcept /** * Saves user provided notes to the proof if present. * - * @param node the node to check for notes + * @param node the node to check for notes * @param output the writer to which to append the notes * @throws IOException if printing fails */ @@ -699,7 +720,7 @@ private void notes2Proof(Node node, Appendable output) throws IOException { * can be loaded again as a proof. * * @param node the proof node from which to be printed - * @param ps the writer in which the rule(s) is/are printed + * @param ps the writer in which the rule(s) is/are printed * @throws IOException an exception thrown when printing fails */ public void node2Proof(Node node, Appendable ps) throws IOException { @@ -708,14 +729,13 @@ public void node2Proof(Node node, Appendable ps) throws IOException { ps.append(")\n"); } - public static String posInOccurrence2Proof(Sequent seq, - PosInOccurrence pos) { + public static String posInOccurrence2Proof(Sequent seq, @Nullable PosInOccurrence pos) { if (pos == null) { return ""; } return " (formula \"" + seq.formulaNumberInSequent(pos.isInAntec(), pos.sequentFormula()) - + "\")" + posInTerm2Proof(pos.posInTerm()); + + "\")" + posInTerm2Proof(pos.posInTerm()); } public static String posInTerm2Proof(PosInTerm pos) { @@ -733,9 +753,9 @@ public static String posInTerm2Proof(PosInTerm pos) { /** * Get the "interesting" instantiations of the provided object. * - * @see SVInstantiations#interesting() * @param inst instantiations * @return the "interesting" instantiations (serialized) + * @see SVInstantiations#interesting() */ public Collection getInterestingInstantiations(SVInstantiations inst) { Collection s = new ArrayList<>(); @@ -748,11 +768,11 @@ public Collection getInterestingInstantiations(SVInstantiations inst) { if (!(value instanceof JTerm || value instanceof ProgramElement || value instanceof Name)) { throw new IllegalStateException("Saving failed.\n" - + "FIXME: Unhandled instantiation type: " + value.getClass()); + + "FIXME: Unhandled instantiation type: " + value.getClass()); } String singleInstantiation = - var.name() + "=" + printAnything(value, proof.getServices(), false); + var.name() + "=" + printAnything(value, proof.getServices(), false); s.add(singleInstantiation); } @@ -844,8 +864,9 @@ public static String printAnything(Object val, Services services) { return printAnything(val, services, true); } - public static String printAnything(Object val, Services services, - boolean shortAttrNotation) { + @Nullable + public static String printAnything(@Nullable Object val, Services services, + boolean shortAttrNotation) { if (val instanceof ProgramElement) { return printProgramElement((ProgramElement) val); } else if (val instanceof JTerm) { @@ -865,17 +886,46 @@ public static String printAnything(Object val, Services services, } } - private static String printSequent(Sequent val, Services services) { + private static String printSequent(Sequent val, @Nullable Services services) { final LogicPrinter printer = createLogicPrinter(services, services == null); printer.printSequent(val); return printer.result(); } - private static LogicPrinter createLogicPrinter(Services serv, boolean shortAttrNotation) { - + private static LogicPrinter createLogicPrinter(@Nullable Services serv, boolean shortAttrNotation) { final NotationInfo ni = new NotationInfo(); - return LogicPrinter.purePrinter(ni, (shortAttrNotation ? serv : null)); } + public String getInternalVersion() { + return internalVersion; + } + + public void setInternalVersion(String internalVersion) { + this.internalVersion = internalVersion; + } + + public boolean isSaveProofSteps() { + return saveProofSteps; + } + + public void setSaveProofSteps(boolean saveProofSteps) { + this.saveProofSteps = saveProofSteps; + } + + public Proof getProof() { + return proof; + } + + public void setProof(Proof proof) { + this.proof = proof; + } + + public int @Nullable [] getPathToLastSelectedNode() { + return pathToLastSelectedNode; + } + + public void setPathToLastSelectedNode(int[] pathToLastSelectedNode) { + this.pathToLastSelectedNode = pathToLastSelectedNode; + } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/io/ProofBundleSaver.java b/key.core/src/main/java/de/uka/ilkd/key/proof/io/ProofBundleSaver.java index a40390cd13c..8b508a2eb12 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/io/ProofBundleSaver.java +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/io/ProofBundleSaver.java @@ -39,7 +39,7 @@ public ProofBundleSaver(Proof proof, Path saveFile) { @Override protected void save(Path file) throws IOException { // get the FileRepo from the InitConfig of the Proof - FileRepo repo = proof.getInitConfig().getFileRepo(); + FileRepo repo = getProof().getInitConfig().getFileRepo(); // this ProofSaver can not be used with TrivialFileRepo if (!(repo instanceof AbstractFileRepo)) { @@ -51,7 +51,7 @@ protected void save(Path file) throws IOException { * create a filename for the actual proof file in the FileRepo: We always use the contract * name here (preparation for proof bundle -> saving multiple proofs). */ - String proofFileName = MiscTools.toValidFileName(proof.name() + ".proof"); + String proofFileName = MiscTools.toValidFileName(getProof().name() + ".proof"); // save the proof file to the FileRepo (stream is closed by the save method!) save(repo.createOutputStream(Paths.get(proofFileName))); diff --git a/key.core/src/main/java/de/uka/ilkd/key/settings/Configuration.java b/key.core/src/main/java/de/uka/ilkd/key/settings/Configuration.java index 8efef1a3e1b..43b7209cdf0 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/settings/Configuration.java +++ b/key.core/src/main/java/de/uka/ilkd/key/settings/Configuration.java @@ -288,6 +288,17 @@ public List getList(String name) { return (List) result; } + /** + * Returns a list of integer values given by the name. + */ + @Nullable + public List getIntList(String name) { + var seq = get(name, List.class); + if (seq == null) return null; + if (!seq.stream().allMatch(it -> it instanceof Integer)) throw new ClassCastException(); + return seq; + } + /** * Returns string array for the requested entry. {@code defaultValue} is returned if no such * entry exists. @@ -332,7 +343,7 @@ public String[] getStringArray(String name, @NonNull String[] defaultValue) { } /** - * Returns the meta data corresponding to the given entry. + * Returns the meta-data corresponding to the given entry. */ @Nullable public ConfigurationMeta getMeta(String name) { @@ -502,6 +513,8 @@ public ConfigurationWriter printValue(Object value) { printValue(value.toString()); } else if (value == null) { printValue("null"); + } else if (value instanceof int[] array) { + printSeq(array); } else { throw new IllegalArgumentException("Unexpected object: " + value); } diff --git a/key.core/src/main/java/de/uka/ilkd/key/settings/ProofSettings.java b/key.core/src/main/java/de/uka/ilkd/key/settings/ProofSettings.java index b06d2307847..5459f8c9fe8 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/settings/ProofSettings.java +++ b/key.core/src/main/java/de/uka/ilkd/key/settings/ProofSettings.java @@ -3,20 +3,19 @@ * SPDX-License-Identifier: GPL-2.0-only */ package de.uka.ilkd.key.settings; -import java.beans.PropertyChangeListener; -import java.io.*; -import java.net.URL; -import java.nio.charset.StandardCharsets; -import java.util.LinkedList; -import java.util.List; -import java.util.Properties; - import de.uka.ilkd.key.util.KeYResourceManager; - import org.antlr.v4.runtime.CharStreams; +import org.jspecify.annotations.NullMarked; +import org.jspecify.annotations.Nullable; import org.slf4j.Logger; import org.slf4j.LoggerFactory; +import java.beans.PropertyChangeListener; +import java.io.*; +import java.net.URL; +import java.nio.charset.StandardCharsets; +import java.util.*; + /** * This class is used to load and save settings for proofs such as which data type models are used * to represent the java types. Which heuristics have to be loaded and so on. The class loads the @@ -32,19 +31,21 @@ * @see Properties * @see Settings */ +@NullMarked public class ProofSettings { private static final Logger LOGGER = LoggerFactory.getLogger(ProofSettings.class); public static final File PROVER_CONFIG_FILE = - new File(PathConfig.getKeyConfigDir(), "proof-settings.props"); + new File(PathConfig.getKeyConfigDir(), "proof-settings.props"); public static final File PROVER_CONFIG_FILE_NEW = - new File(PathConfig.getKeyConfigDir(), "proof-settings.json"); + new File(PathConfig.getKeyConfigDir(), "proof-settings.json"); public static final URL PROVER_CONFIG_FILE_TEMPLATE = KeYResourceManager.getManager() .getResourceFile(ProofSettings.class, "default-proof-settings.json"); public static final ProofSettings DEFAULT_SETTINGS = loadedSettings(); + public static final String KEY_ADDITIONAL_DATA = "additionalInformation"; private static ProofSettings loadedSettings() { @@ -66,12 +67,12 @@ private static ProofSettings loadedSettings() { private final StrategySettings strategySettings = new StrategySettings(); private final ChoiceSettings choiceSettings = new ChoiceSettings(); private final ProofDependentSMTSettings smtSettings = - ProofDependentSMTSettings.getDefaultSettingsData(); + ProofDependentSMTSettings.getDefaultSettingsData(); private final NewSMTTranslationSettings newSMTSettings = new NewSMTTranslationSettings(); private final TermLabelSettings termLabelSettings = new TermLabelSettings(); - private Properties lastLoadedProperties = null; - private Configuration lastLoadedConfiguration = null; + private @Nullable Properties lastLoadedProperties = null; + private @Nullable Configuration lastLoadedConfiguration = null; /** * create a proof settings object. When you add a new settings object, PLEASE UPDATE THE LIST @@ -133,10 +134,26 @@ public Configuration getConfiguration() { } /** - * Used by saveSettings() and settingsToString() + * Write the settings to the given stream w/o additional information. + * + * @see #settingsToStream(Writer, Map) */ public void settingsToStream(Writer out) { - getConfiguration().save(out, "Proof-Settings-Config-File"); + settingsToStream(out, null); + } + + /** + * Writes the settings to the given stream storing additional data into {@link #KEY_ADDITIONAL_DATA}. + * + * @param out a output destination + * @param additionalInformation a nullable map of additional information + */ + public void settingsToStream(Writer out, @Nullable Map additionalInformation) { + var config = getConfiguration(); + if (additionalInformation != null) { + config.set(KEY_ADDITIONAL_DATA, new Configuration(additionalInformation)); + } + config.save(out, "Proof-Settings-Config-File"); } /** @@ -148,7 +165,7 @@ public void saveSettings() { PROVER_CONFIG_FILE.getParentFile().mkdirs(); } try (Writer out = new BufferedWriter( - new FileWriter(PROVER_CONFIG_FILE_NEW, StandardCharsets.UTF_8))) { + new FileWriter(PROVER_CONFIG_FILE_NEW, StandardCharsets.UTF_8))) { settingsToStream(out); } } catch (IOException e) { @@ -157,8 +174,12 @@ public void saveSettings() { } public String settingsToString() { + return settingsToString(new HashMap<>()); + } + + public String settingsToString(Map additionalInformation) { StringWriter out = new StringWriter(); - settingsToStream(out); + settingsToStream(out, additionalInformation); return out.getBuffer().toString(); } @@ -170,7 +191,7 @@ public void loadSettingsFromJSONStream(Reader in) throws IOException { public void loadDefaultJSONSettings() { if (PROVER_CONFIG_FILE_TEMPLATE == null) { LOGGER.warn( - "default proof-settings file 'default-proof-settings.json' could not be found."); + "default proof-settings file 'default-proof-settings.json' could not be found."); } else { try (var in = new InputStreamReader(PROVER_CONFIG_FILE_TEMPLATE.openStream())) { loadSettingsFromJSONStream(in); diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/WindowUserInterfaceControl.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/WindowUserInterfaceControl.java index 8f738947e82..df726eedb11 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/WindowUserInterfaceControl.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/WindowUserInterfaceControl.java @@ -35,6 +35,7 @@ import de.uka.ilkd.key.proof.io.AbstractProblemLoader.ReplayResult; import de.uka.ilkd.key.rule.IBuiltInRuleApp; import de.uka.ilkd.key.settings.ProofIndependentSettings; +import de.uka.ilkd.key.settings.ProofSettings; import de.uka.ilkd.key.settings.ViewSettings; import de.uka.ilkd.key.speclang.PositionedString; import de.uka.ilkd.key.strategy.StrategyProperties; @@ -392,6 +393,11 @@ public Path saveProof(Proof proof, String fileExtension) { } else { saver = new ProofSaver(proof, filename, KeYConstants.INTERNAL_VERSION); } + + if(getMediator().getSelectedProof() == proof) { + saver.setPathToLastSelectedNode(getMediator().getSelectedNode().getPosInProof()); + } + String errorMsg; try { getMediator().stopInterface(true); @@ -523,8 +529,18 @@ public void loadingFinished(AbstractProblemLoader loader, LoadedPOContainer poCo } } getMediator().resetNrGoalsClosedByHeuristics(); - if (poContainer != null && poContainer.getProofOblInput() instanceof KeYUserProblemFile) { - ((KeYUserProblemFile) poContainer.getProofOblInput()).close(); + if (poContainer != null && poContainer.getProofOblInput() instanceof KeYUserProblemFile file) { + //TODO weigl not triggered + var settings = file.readSettings(); + var addInfo = settings.getSection(ProofSettings.KEY_ADDITIONAL_DATA); + if(addInfo!=null){ + var lastSelectedNodePath = settings.getIntList(OutputStreamProofSaver.KEY_LAST_SELECTED_NODE); + if (lastSelectedNodePath != null && proofList != null) { + var proof = proofList.getFirstProof(); + proof.root().traversePath(lastSelectedNodePath.iterator()); + } + } + file.close(); } } diff --git a/key.util/src/main/java/org/key_project/util/collection/KeYCollections.java b/key.util/src/main/java/org/key_project/util/collection/KeYCollections.java index e6193c17e99..234fbd1686e 100644 --- a/key.util/src/main/java/org/key_project/util/collection/KeYCollections.java +++ b/key.util/src/main/java/org/key_project/util/collection/KeYCollections.java @@ -3,10 +3,7 @@ * SPDX-License-Identifier: GPL-2.0-only */ package org.key_project.util.collection; -import java.util.Arrays; -import java.util.HashMap; -import java.util.Map; -import java.util.Objects; +import java.util.*; import java.util.stream.Collectors; import java.util.stream.StreamSupport; @@ -81,7 +78,7 @@ public static Map apply(Map m0, Map m1) { * {@link Object#toString()} is used to turn the objects into strings. * * @param collection an arbitrary non-null collection - * @param delimiter a non-null string which is put between the elements. + * @param delimiter a non-null string which is put between the elements. * @return the concatenation of all string representations separated by the delimiter */ public static String join(Iterable collection, String delimiter) { @@ -96,7 +93,7 @@ public static String join(Iterable collection, String delimiter) { * {@link Object#toString()} is used to turn the objects into strings. * * @param collection an arbitrary non-null array of objects - * @param delimiter a non-null string which is put between the elements. + * @param delimiter a non-null string which is put between the elements. * @return the concatenation of all string representations separated by the delimiter */ public static String join(Object[] collection, String delimiter) { @@ -125,4 +122,113 @@ public static String join(Object[] collection, String delimiter) { } return res.toString(); } + + /** + * Creates a run-length encoding from the given positive integer array. The return array has the following form: + * every positive entry stands for its own. Every negative integer describes the repetition + * of the following positive integer. + *

+ * For example {@code [1, -5, 2, 1]} stands for {@code [1,2,2,2,2,2,1]}. + * + * @param array an integer array where + */ + public static int[] runLengthEncoding(int[] array) { + int len = array.length; + int[] target = new int[2 * len]; + int used = 0; + for (int i = 0; i < len; i++) { + // Count occurrences of current character + int count = 1; + int symbol = array[i]; + while (i < len - 1 && symbol == array[i + 1]) { + count++; + i++; + } + if (count != 1) { + target[used++] = -count; + } + target[used++] = symbol; + } + + return Arrays.copyOf(target, used); + } + + + public static int[] runLengthEncoding(Collection array) { + var iter = array.iterator(); + class PushbackIterator implements Iterator { + private int pushedBack=-1; + @Override + public boolean hasNext() { + return pushedBack >= 0 || iter.hasNext(); + } + + @Override + public Integer next() { + if(pushedBack>=0){ + var v = pushedBack; + pushedBack=-1; + return v; + } + return iter.next(); + } + + public void pushBack(int last) { + pushedBack = last; + } + } + var piter = new PushbackIterator(); + int len = array.size(); + int[] target = new int[2 * len]; + int used = 0; + + while (piter.hasNext()) { + // Count occurrences of current character + int count = 1; + int symbol = piter.next(); + int last = symbol; + while (iter.hasNext() && (symbol == (last = piter.next()))) { + count++; + } + if(last!=symbol) { + piter.pushBack(last); + } + if (count != 1) { + target[used++] = -count; + } + target[used++] = symbol; + } + return Arrays.copyOf(target, used); + } + + + /** + * Creates a lazy decoding for the given run-length encoding. + */ + public static Iterator runLengthDecoding(int[] rleArray) { + return new Iterator<>() { + int pos = 0; + int count = 0; + int value = -1; + + @Override + public boolean hasNext() { + return count > 0 || pos < rleArray.length; + } + + @Override + public Integer next() { + if (count == 0) { + value = rleArray[pos++]; + if (value < 0) { + count = (-value) - 1; + value = rleArray[pos++]; + } + } else { + count--; + } + return value; + } + }; + } } diff --git a/key.util/src/test/java/org/key_project/util/collection/KeYCollectionsTest.java b/key.util/src/test/java/org/key_project/util/collection/KeYCollectionsTest.java new file mode 100644 index 00000000000..6e09f70ab74 --- /dev/null +++ b/key.util/src/test/java/org/key_project/util/collection/KeYCollectionsTest.java @@ -0,0 +1,57 @@ +package org.key_project.util.collection; + +import org.junit.jupiter.api.Test; + +import java.lang.constant.Constable; +import java.util.List; +import java.util.Spliterator; +import java.util.Spliterators; +import java.util.function.Consumer; +import java.util.stream.StreamSupport; + +import static org.junit.jupiter.api.Assertions.assertArrayEquals; +import static org.key_project.util.collection.KeYCollections.runLengthDecoding; +import static org.key_project.util.collection.KeYCollections.runLengthEncoding; + +/** + * @author Alexander Weigl + * @version 1 (28.12.23) + */ +class KeYCollectionsTest { + + @Test + void runLengthEncoding_test() { + assertArrayEquals(new int[]{1, -5, 2, 1}, runLengthEncoding(new int[]{1, 2, 2, 2, 2, 2, 1})); + assertArrayEquals(new int[]{-5, 2}, runLengthEncoding(new int[]{2, 2, 2, 2, 2})); + assertArrayEquals(new int[]{}, runLengthEncoding(new int[]{})); + assertArrayEquals(new int[]{-5, 2, -5, 1}, runLengthEncoding(new int[]{2, 2, 2, 2, 2, 1, 1, 1, 1, 1})); + } + + @Test + void runLengthEncoding_test2() { + assertArrayEquals(new int[]{}, runLengthEncoding(List.of())); + assertArrayEquals(new int[]{1, -5, 2, 1}, runLengthEncoding(List.of(1, 2, 2, 2, 2, 2, 1))); + assertArrayEquals(new int[]{-5, 2}, runLengthEncoding(List.of(2, 2, 2, 2, 2))); + assertArrayEquals(new int[]{-5, 2, -5, 1}, runLengthEncoding(List.of(2, 2, 2, 2, 2, 1, 1, 1, 1, 1))); + } + + + @Test + void runLengthDecoding_test() { + Consumer tester = original -> { + final var rle = runLengthEncoding(original); + final var iter = runLengthDecoding(rle); + var stream = StreamSupport.stream(Spliterators.spliteratorUnknownSize(iter, Spliterator.ORDERED), false) + .mapToInt(it -> it) + .toArray(); + System.out.println(stream); + assertArrayEquals(original, stream); + }; + tester.accept(new int[]{1, 2, 2, 2, 2, 2, 1}); + tester.accept(new int[]{2, 2, 2, 2, 2}); + tester.accept(new int[]{}); + tester.accept(new int[]{2, 2, 2, 2, 2, 1, 1, 1, 1, 1}); + } + + +} From 05f079acbc077e121efb4f8f9fd4bef23593db68 Mon Sep 17 00:00:00 2001 From: Alexander Weigl Date: Sat, 3 Feb 2024 17:46:36 +0100 Subject: [PATCH 2/3] change in the listener delivers settings now --- .../control/AbstractUserInterfaceControl.java | 3 +- .../java/de/uka/ilkd/key/nparser/KeyAst.java | 12 +-- .../main/java/de/uka/ilkd/key/proof/Node.java | 38 ++++---- .../key/proof/init/KeYUserProblemFile.java | 6 +- .../key/proof/io/AbstractProblemLoader.java | 7 +- .../key/proof/io/OutputStreamProofSaver.java | 88 +++++++++---------- .../key/proof/io/ProblemLoaderControl.java | 5 +- .../uka/ilkd/key/settings/Configuration.java | 8 +- .../uka/ilkd/key/settings/ProofSettings.java | 28 +++--- .../key/gui/WindowUserInterfaceControl.java | 12 +-- .../util/collection/KeYCollections.java | 16 ++-- .../util/collection/KeYCollectionsTest.java | 39 ++++---- 12 files changed, 135 insertions(+), 127 deletions(-) diff --git a/key.core/src/main/java/de/uka/ilkd/key/control/AbstractUserInterfaceControl.java b/key.core/src/main/java/de/uka/ilkd/key/control/AbstractUserInterfaceControl.java index c8a26ca1100..67bccc1a181 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/control/AbstractUserInterfaceControl.java +++ b/key.core/src/main/java/de/uka/ilkd/key/control/AbstractUserInterfaceControl.java @@ -257,7 +257,8 @@ public void loadingStarted(AbstractProblemLoader loader) { @Override public void loadingFinished(AbstractProblemLoader loader, LoadedPOContainer poContainer, - ProofAggregate proofList, ReplayResult result) throws ProblemLoaderException { + ProofAggregate proofList, ReplayResult result, Configuration settings) + throws ProblemLoaderException { if (proofList != null) { // avoid double registration at spec repos as that is done already earlier in // createProof diff --git a/key.core/src/main/java/de/uka/ilkd/key/nparser/KeyAst.java b/key.core/src/main/java/de/uka/ilkd/key/nparser/KeyAst.java index 3a4925082c3..e3e50418712 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/nparser/KeyAst.java +++ b/key.core/src/main/java/de/uka/ilkd/key/nparser/KeyAst.java @@ -123,20 +123,10 @@ public static class File extends KeyAst { } else { return new KeyAst.ProofScript(pctx.proofScript()); } - /** - * Returns the raw settings within a {@link de.uka.ilkd.key.proof.io.KeYFile}. - */ - public Configuration findSettings() { - final var cfg = new ConfigurationBuilder(); - if (ctx.preferences() == null || ctx.preferences().cvalue() == null) { - return new Configuration(); } - - var c = ctx.preferences().cvalue(); - return (Configuration) c.accept(cfg); + return null; } - /// Returns the includes (possible empty but not null) computed from the underlying parse /// tree. public Includes getIncludes(URL base) { diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/Node.java b/key.core/src/main/java/de/uka/ilkd/key/proof/Node.java index 5421fa70a17..8da653ad7c8 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/Node.java +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/Node.java @@ -3,20 +3,20 @@ * SPDX-License-Identifier: GPL-2.0-only */ package de.uka.ilkd.key.proof; +import java.util.*; + import de.uka.ilkd.key.logic.RenamingTable; import de.uka.ilkd.key.logic.op.IProgramVariable; import de.uka.ilkd.key.proof.calculus.JavaDLSequentKit; import de.uka.ilkd.key.proof.reference.ClosedBy; import de.uka.ilkd.key.rule.NoPosTacletApp; import de.uka.ilkd.key.rule.merge.MergeRule; +import de.uka.ilkd.key.util.Pair; import org.key_project.logic.op.Function; import org.key_project.prover.rules.RuleApp; import org.key_project.prover.sequent.Sequent; import org.key_project.prover.sequent.SequentChangeInfo; -import de.uka.ilkd.key.util.Pair; -import org.jspecify.annotations.NonNull; -import org.jspecify.annotations.Nullable; import org.key_project.util.collection.DefaultImmutableSet; import org.key_project.util.collection.ImmutableList; import org.key_project.util.collection.ImmutableSLList; @@ -24,7 +24,8 @@ import org.key_project.util.collection.Pair; import org.key_project.util.lookup.Lookup; -import java.util.*; +import org.jspecify.annotations.NonNull; +import org.jspecify.annotations.Nullable; public class Node implements Iterable { private static final String RULE_WITHOUT_NAME = "rule without name"; @@ -116,7 +117,7 @@ public class Node implements Iterable { * taclet with an addrule section on this node, then these taclets are stored in this list */ private ImmutableSet localIntroducedRules = - DefaultImmutableSet.nil(); + DefaultImmutableSet.nil(); /** * Holds the undo methods for the information added by rules to the {@code Goal.strategyInfos}. @@ -448,7 +449,7 @@ List getLeaves() { /** * @return an iterator for the leaves of the subtree below this node. The computation is called - * at every call! + * at every call! */ public Iterator leavesIterator() { return new NodeIterator(getLeaves().iterator()); @@ -493,7 +494,7 @@ public Node child(int i) { /** * @param child a child of this node. * @return the number of the node child, if it is a child of this node (starting - * with 0), -1 otherwise + * with 0), -1 otherwise */ public int getChildNr(Node child) { int res = 0; @@ -533,16 +534,16 @@ public StringBuffer getUniqueTacletId() { * Helper for {@link #toString()} * * @param prefix needed to keep track if a line has to be printed - * @param tree the tree representation we want to add this subtree " @param preEnumeration the - * enumeration of the parent without the last number + * @param tree the tree representation we want to add this subtree " @param preEnumeration the + * enumeration of the parent without the last number * @param postNr the last number of the parents enumeration - * @param maxNr the number of nodes at this level - * @param ownNr the place of this node at this level + * @param maxNr the number of nodes at this level + * @param ownNr the place of this node at this level * @return the string representation of this node. */ private StringBuffer toString(String prefix, StringBuffer tree, String preEnumeration, - int postNr, int maxNr, int ownNr) { + int postNr, int maxNr, int ownNr) { Iterator childrenIt = childrenIterator(); // Some constants String frontIndent = (maxNr > 1 ? " " : ""); @@ -593,7 +594,7 @@ private StringBuffer toString(String prefix, StringBuffer tree, String preEnumer while (childrenIt.hasNext()) { childId++; childrenIt.next().toString(prefix, tree, newEnumeration, newPostNr, children.size(), - childId); + childId); } return tree; @@ -650,7 +651,7 @@ public String name() { * this node. * * @return true iff the parent of this node has this node as child and this condition holds also - * for the own children. + * for the own children. */ public boolean sanityCheckDoubleLinks() { if (!root()) { @@ -777,7 +778,7 @@ public void addStrategyInfoUndoMethod(StrategyInfoUndoMethod undoMethod) { /** * Register a user-defined data in this node info. * - * @param obj an object to be registered + * @param obj an object to be registered * @param service the key under it should be registered * @param the type of the object to be registered */ @@ -788,9 +789,9 @@ public void register(T obj, Class service) { /** * Remove a previous registered user-defined data. * - * @param obj registered object + * @param obj registered object * @param service the key under which the data was registered - * @param arbitray object + * @param arbitray object */ public void deregister(T obj, Class service) { if (userData != null) { @@ -849,7 +850,8 @@ void setStepIndex(int stepIndex) { } /** - * Calculates an array is the path from root node to this node. Each entry defines the child to be selected. + * Calculates an array is the path from root node to this node. Each entry defines the child to + * be selected. * * @see #traversePath(Iterator) */ diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/init/KeYUserProblemFile.java b/key.core/src/main/java/de/uka/ilkd/key/proof/init/KeYUserProblemFile.java index 9c2bb61f73c..064363db938 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/init/KeYUserProblemFile.java +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/init/KeYUserProblemFile.java @@ -9,7 +9,6 @@ import de.uka.ilkd.key.java.abstraction.KeYJavaType; import de.uka.ilkd.key.nparser.*; -import de.uka.ilkd.key.nparser.builder.ProblemFinder; import de.uka.ilkd.key.proof.Proof; import de.uka.ilkd.key.proof.ProofAggregate; import de.uka.ilkd.key.proof.io.IProofFileParser; @@ -124,8 +123,8 @@ public ImmutableSet read() throws ProofInputException { return warnings; } - public Configuration readSettings() { - if(settings==null){ + public Configuration readSettings() { + if (settings == null) { settings = getParseContext().findSettings(); } return settings; @@ -282,4 +281,5 @@ private Profile getDefaultProfile() { public KeYJavaType getContainerType() { return null; } + } diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/io/AbstractProblemLoader.java b/key.core/src/main/java/de/uka/ilkd/key/proof/io/AbstractProblemLoader.java index 03c43de3c17..b343ad4b8b2 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/io/AbstractProblemLoader.java +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/io/AbstractProblemLoader.java @@ -279,7 +279,9 @@ public final void load(Consumer callbackProofLoaded) loadSelectedProof(poContainer, proofList, callbackProofLoaded); } } finally { - control.loadingFinished(this, poContainer, proofList, result); + var settings = (envInput instanceof KeYUserProblemFile kupf) ? kupf.readSettings() + : new Configuration(); + control.loadingFinished(this, poContainer, proofList, result, settings); } } @@ -646,9 +648,6 @@ private ReplayResult replayProof(Proof proof) { problemInitializer.tryReadProof(parser, (KeYUserProblemFile) envInput); parserResult = parser.getResult(); - // Parser is no longer needed, set it to null to free memory. - parser = null; - // For loading, we generally turn on one step simplification to be // able to load proofs that used it even if the user has currently // turned OSS off. 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 fd23ed04092..354b5889c22 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 @@ -58,14 +58,11 @@ import org.key_project.prover.sequent.Sequent; import org.key_project.prover.sequent.SequentFormula; import org.key_project.util.collection.ImmutableList; +import org.key_project.util.collection.KeYCollections; import org.slf4j.Logger; import org.slf4j.LoggerFactory; -import java.io.*; -import java.nio.charset.StandardCharsets; -import java.util.*; - /** * Saves a proof to a given {@link OutputStream}. * @@ -131,9 +128,9 @@ public OutputStreamProofSaver(Proof proof, String internalVersion) { /** * Create a new OutputStreamProofSaver. * - * @param proof the proof to save + * @param proof the proof to save * @param internalVersion currently running KeY version - * @param saveProofSteps whether to save the performed proof steps + * @param saveProofSteps whether to save the performed proof steps */ public OutputStreamProofSaver(Proof proof, String internalVersion, boolean saveProofSteps) { this.proof = proof; @@ -173,7 +170,7 @@ public String writeProfile(Profile profile) { public String writeSettings(ProofSettings ps) { // inject the last selected node var additionalInformation = new TreeMap(); - if(pathToLastSelectedNode!=null) { + if (pathToLastSelectedNode != null) { var lastSelectedNode = KeYCollections.runLengthEncoding(pathToLastSelectedNode); additionalInformation.put(KEY_LAST_SELECTED_NODE, lastSelectedNode); } @@ -184,7 +181,7 @@ public void save(OutputStream out) throws IOException { CopyReferenceResolver.copyCachedGoals(proof, null, null, null); try (var ps = new PrintWriter(out, true, StandardCharsets.UTF_8)) { final ProofOblInput po = - proof.getServices().getSpecificationRepository().getProofOblInput(proof); + proof.getServices().getSpecificationRepository().getProofOblInput(proof); LogicPrinter printer = createLogicPrinter(proof.getServices(), false); // profile @@ -193,11 +190,11 @@ public void save(OutputStream out) throws IOException { // settings final StrategySettings strategySettings = proof.getSettings().getStrategySettings(); final StrategyProperties strategyProperties = - strategySettings.getActiveStrategyProperties(); + strategySettings.getActiveStrategyProperties(); if (po instanceof AbstractInfFlowPO && (po instanceof InfFlowCompositePO || !((InfFlowProof) proof).getIFSymbols().isFreshContract())) { strategyProperties.put(StrategyProperties.INF_FLOW_CHECK_PROPERTY, - StrategyProperties.INF_FLOW_CHECK_TRUE); + StrategyProperties.INF_FLOW_CHECK_TRUE); strategySettings.setActiveStrategyProperties(strategyProperties); for (final SequentFormula s : proof.root().sequent() .succedent().asList()) { @@ -205,7 +202,7 @@ public void save(OutputStream out) throws IOException { } } else { strategyProperties.put(StrategyProperties.INF_FLOW_CHECK_PROPERTY, - StrategyProperties.INF_FLOW_CHECK_FALSE); + StrategyProperties.INF_FLOW_CHECK_FALSE); strategySettings.setActiveStrategyProperties(strategyProperties); } ps.println(writeSettings(proof.getSettings())); @@ -213,7 +210,7 @@ public void save(OutputStream out) throws IOException { if (po instanceof AbstractInfFlowPO && (po instanceof InfFlowCompositePO || !((InfFlowProof) proof).getIFSymbols().isFreshContract())) { strategyProperties.put(StrategyProperties.INF_FLOW_CHECK_PROPERTY, - StrategyProperties.INF_FLOW_CHECK_FALSE); + StrategyProperties.INF_FLOW_CHECK_FALSE); strategySettings.setActiveStrategyProperties(strategyProperties); } @@ -225,7 +222,7 @@ public void save(OutputStream out) throws IOException { // \problem or \proofObligation if (po instanceof IPersistablePO ppo && (!(po instanceof AbstractInfFlowPO) || (!(po instanceof InfFlowCompositePO) - && ((InfFlowProof) proof).getIFSymbols().isFreshContract()))) { + && ((InfFlowProof) proof).getIFSymbols().isFreshContract()))) { var loadingConfig = ppo.createLoaderConfig(); ps.println("\\proofObligation "); loadingConfig.save(ps, ""); @@ -282,7 +279,7 @@ protected Path getBasePath() throws IOException { */ private String makePathsRelative(String header) { final String[] search = - {"\\javaSource", "\\bootclasspath", "\\classpath", "\\include"}; + { "\\javaSource", "\\bootclasspath", "\\classpath", "\\include" }; String basePath; String tmp = header; try { @@ -363,13 +360,13 @@ private String newNames2Proof(Node n) { * 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 prefix a string which the printed rule is concatenated to + * @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 { + Appendable output) throws IOException { output.append(prefix); output.append("(rule \""); @@ -393,11 +390,11 @@ private void printSingleTacletApp(TacletApp appliedRuleApp, Node node, String pr * Print predicates for applied merge rule application into the passed writer. * * @param predAbstrRule the rule application with the predicates to be printed - * @param output the writer in which the rule is printed + * @param output the writer in which the rule is printed * @throws IOException an exception thrown when printing fails */ private void printPredicatesForSingleMergeRuleApp(MergeWithPredicateAbstraction predAbstrRule, - Appendable output) throws IOException { + Appendable output) throws IOException { output.append("(").append(ProofElementID.MERGE_ABSTRACTION_PREDICATES.getRawName()) .append(" \""); boolean first = true; @@ -428,13 +425,13 @@ private void printPredicatesForSingleMergeRuleApp(MergeWithPredicateAbstraction * Print predicates for applied merge rule application into the passed writer. * * @param concreteRule the rule application with the abstract domain to be printed - * @param output the writer in which the rule is printed + * @param output the writer in which the rule is printed * @throws IOException an exception thrown when printing fails */ private void printLatticeAbstractionForSingleMergeRuleApp( MergeWithLatticeAbstraction concreteRule, Appendable output) throws IOException { final Map userChoices = - concreteRule.getUserChoices(); + concreteRule.getUserChoices(); if (!userChoices.isEmpty()) { output.append(" (").append(ProofElementID.MERGE_USER_CHOICES.getRawName()) @@ -462,12 +459,12 @@ private void printLatticeAbstractionForSingleMergeRuleApp( * Print applied merge rule for a single merge rule application into the passed writer. * * @param mergeApp 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 prefix a string which the printed rule is concatenated to + * @param output the writer in which the rule is printed * @throws IOException an exception thrown when printing fails */ private void printSingleMergeRuleApp(MergeRuleBuiltInRuleApp mergeApp, Node node, String prefix, - Appendable output) throws IOException { + Appendable output) throws IOException { final MergeProcedure concreteRule = mergeApp.getConcreteRule(); output.append(" (").append(ProofElementID.MERGE_PROCEDURE.getRawName()).append(" \""); @@ -486,8 +483,8 @@ private void printSingleMergeRuleApp(MergeRuleBuiltInRuleApp mergeApp, Node node output.append(" (").append(ProofElementID.MERGE_DIST_FORMULA.getRawName()) .append(" \""); output.append(escapeCharacters( - printAnything(mergeApp.getDistinguishingFormula(), proof.getServices(), false) - .trim().replaceAll("(\\r|\\n|\\r\\n)+", ""))); + printAnything(mergeApp.getDistinguishingFormula(), proof.getServices(), false) + .trim().replaceAll("(\\r|\\n|\\r\\n)+", ""))); output.append("\")"); } @@ -496,12 +493,12 @@ private void printSingleMergeRuleApp(MergeRuleBuiltInRuleApp mergeApp, Node node && ((MergeWithPredicateAbstraction) concreteRule).getPredicates().size() > 0) { printPredicatesForSingleMergeRuleApp((MergeWithPredicateAbstraction) concreteRule, - output); + output); } if (concreteRule instanceof MergeWithLatticeAbstraction) { printLatticeAbstractionForSingleMergeRuleApp((MergeWithLatticeAbstraction) concreteRule, - output); + output); } } @@ -519,7 +516,7 @@ private void printSingleMergeRuleApp(MergeRuleBuiltInRuleApp mergeApp, Node node * @throws IOException an exception thrown when printing fails */ private void printSingleCloseAfterMergeRuleApp(CloseAfterMergeRuleBuiltInRuleApp closeApp, - Node node, String prefix, Appendable output) throws IOException { + Node node, String prefix, Appendable output) throws IOException { // TODO (DS): There may be problems here if the merge node is // pruned away. Need to test some cases and either check for @@ -530,7 +527,7 @@ private void printSingleCloseAfterMergeRuleApp(CloseAfterMergeRuleBuiltInRuleApp } private void printSingleSMTRuleApp(SMTRuleApp smtApp, Node node, String prefix, - Appendable output) throws IOException { + Appendable output) throws IOException { output.append(" (").append(ProofElementID.SOLVERTYPE.getRawName()) .append(" \"").append(smtApp.getSuccessfulSolverName()).append("\")"); } @@ -539,7 +536,7 @@ private void printSingleSMTRuleApp(SMTRuleApp smtApp, Node node, String prefix, * Print rule justification for applied built-in rule application into the passed writer. * * @param appliedRuleApp the rule application to be printed - * @param output the writer in which the rule is printed + * @param output the writer in which the rule is printed * @throws IOException an exception thrown when printing fails */ private void printRuleJustification(IBuiltInRuleApp appliedRuleApp, Appendable output) @@ -560,12 +557,12 @@ private void printRuleJustification(IBuiltInRuleApp appliedRuleApp, Appendable o * Print applied built-in rule for a single built-in 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 prefix a string which the printed rule is concatenated to + * @param output the writer in which the rule is printed * @throws IOException an exception thrown when printing fails */ private void printSingleBuiltInRuleApp(IBuiltInRuleApp appliedRuleApp, Node node, String prefix, - Appendable output) throws IOException { + Appendable output) throws IOException { output.append(prefix); output.append(" (builtin \""); output.append(appliedRuleApp.rule().name().toString()); @@ -596,7 +593,7 @@ private void printSingleBuiltInRuleApp(IBuiltInRuleApp appliedRuleApp, Node node if (appliedRuleApp instanceof CloseAfterMergeRuleBuiltInRuleApp) { printSingleCloseAfterMergeRuleApp((CloseAfterMergeRuleBuiltInRuleApp) appliedRuleApp, - node, prefix, output); + node, prefix, output); } else if (appliedRuleApp instanceof SMTRuleApp) { printSingleSMTRuleApp((SMTRuleApp) appliedRuleApp, node, prefix, output); } @@ -610,7 +607,7 @@ private void printSingleBuiltInRuleApp(IBuiltInRuleApp appliedRuleApp, Node node /** * Print applied rule (s) for a single proof node into the passed writer. * - * @param node the proof node to be printed + * @param node the proof node to be printed * @param prefix a string which the printed rules are concatenated to * @param output the writer in which the rule(s) is /are printed * @throws IOException an exception thrown when printing fails @@ -639,7 +636,7 @@ private void printSingleNode(Node node, String prefix, Appendable output) throws /** * Print applied rule(s) for a proof node and its decendants into the passed writer. * - * @param node the proof node from which to be printed + * @param node the proof node from which to be printed * @param prefix a string which the printed rules are concatenated to * @param output the writer in which the rule(s) is/are printed * @throws IOException an exception thrown when printing fails @@ -683,7 +680,7 @@ private void collectProof(Node node, String prefix, Appendable output) throws IO * Check whether the applied rule of the passed proof node was performed interactively. If this * is the case, a user interaction label is appended. * - * @param node the proof node to be checked + * @param node the proof node to be checked * @param output the writer to which the label should be appended * @throws IOException an exception thrown in case printing fails */ @@ -699,7 +696,7 @@ private void userInteraction2Proof(Node node, Appendable output) throws IOExcept /** * Saves user provided notes to the proof if present. * - * @param node the node to check for notes + * @param node the node to check for notes * @param output the writer to which to append the notes * @throws IOException if printing fails */ @@ -720,7 +717,7 @@ private void notes2Proof(Node node, Appendable output) throws IOException { * can be loaded again as a proof. * * @param node the proof node from which to be printed - * @param ps the writer in which the rule(s) is/are printed + * @param ps the writer in which the rule(s) is/are printed * @throws IOException an exception thrown when printing fails */ public void node2Proof(Node node, Appendable ps) throws IOException { @@ -735,7 +732,7 @@ public static String posInOccurrence2Proof(Sequent seq, @Nullable PosInOccurrenc } return " (formula \"" + seq.formulaNumberInSequent(pos.isInAntec(), pos.sequentFormula()) - + "\")" + posInTerm2Proof(pos.posInTerm()); + + "\")" + posInTerm2Proof(pos.posInTerm()); } public static String posInTerm2Proof(PosInTerm pos) { @@ -768,11 +765,11 @@ public Collection getInterestingInstantiations(SVInstantiations inst) { if (!(value instanceof JTerm || value instanceof ProgramElement || value instanceof Name)) { throw new IllegalStateException("Saving failed.\n" - + "FIXME: Unhandled instantiation type: " + value.getClass()); + + "FIXME: Unhandled instantiation type: " + value.getClass()); } String singleInstantiation = - var.name() + "=" + printAnything(value, proof.getServices(), false); + var.name() + "=" + printAnything(value, proof.getServices(), false); s.add(singleInstantiation); } @@ -866,7 +863,7 @@ public static String printAnything(Object val, Services services) { @Nullable public static String printAnything(@Nullable Object val, Services services, - boolean shortAttrNotation) { + boolean shortAttrNotation) { if (val instanceof ProgramElement) { return printProgramElement((ProgramElement) val); } else if (val instanceof JTerm) { @@ -892,7 +889,8 @@ private static String printSequent(Sequent val, @Nullable Services services) { return printer.result(); } - private static LogicPrinter createLogicPrinter(@Nullable Services serv, boolean shortAttrNotation) { + private static LogicPrinter createLogicPrinter(@Nullable Services serv, + boolean shortAttrNotation) { final NotationInfo ni = new NotationInfo(); return LogicPrinter.purePrinter(ni, (shortAttrNotation ? serv : null)); } diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/io/ProblemLoaderControl.java b/key.core/src/main/java/de/uka/ilkd/key/proof/io/ProblemLoaderControl.java index 01bc5fcb2dc..7c1d313d994 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/io/ProblemLoaderControl.java +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/io/ProblemLoaderControl.java @@ -8,6 +8,7 @@ import de.uka.ilkd.key.proof.init.InitConfig; import de.uka.ilkd.key.proof.init.ProblemInitializer.ProblemInitializerListener; import de.uka.ilkd.key.proof.io.AbstractProblemLoader.ReplayResult; +import de.uka.ilkd.key.settings.Configuration; import de.uka.ilkd.key.speclang.PositionedString; import de.uka.ilkd.key.util.ProgressMonitor; @@ -33,10 +34,12 @@ public interface ProblemLoaderControl extends ProblemInitializerListener, Progre * @param poContainer The loaded {@link LoadedPOContainer}. * @param proofList The created {@link ProofAggregate}. * @param result The occurred {@link ReplayResult}. + * @param settings * @throws ProblemLoaderException Occurred Exception. */ void loadingFinished(AbstractProblemLoader loader, LoadedPOContainer poContainer, - ProofAggregate proofList, ReplayResult result) throws ProblemLoaderException; + ProofAggregate proofList, ReplayResult result, + Configuration settings) throws ProblemLoaderException; /** * This method is called if no {@link LoadedPOContainer} was created via diff --git a/key.core/src/main/java/de/uka/ilkd/key/settings/Configuration.java b/key.core/src/main/java/de/uka/ilkd/key/settings/Configuration.java index 43b7209cdf0..0d434d8bf3b 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/settings/Configuration.java +++ b/key.core/src/main/java/de/uka/ilkd/key/settings/Configuration.java @@ -292,10 +292,12 @@ public List getList(String name) { * Returns a list of integer values given by the name. */ @Nullable - public List getIntList(String name) { + public List getIntList(String name) { var seq = get(name, List.class); - if (seq == null) return null; - if (!seq.stream().allMatch(it -> it instanceof Integer)) throw new ClassCastException(); + if (seq == null) + return null; + if (!seq.stream().allMatch(it -> it instanceof Long)) + throw new ClassCastException(); return seq; } diff --git a/key.core/src/main/java/de/uka/ilkd/key/settings/ProofSettings.java b/key.core/src/main/java/de/uka/ilkd/key/settings/ProofSettings.java index 5459f8c9fe8..61f4ec77964 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/settings/ProofSettings.java +++ b/key.core/src/main/java/de/uka/ilkd/key/settings/ProofSettings.java @@ -3,19 +3,20 @@ * SPDX-License-Identifier: GPL-2.0-only */ package de.uka.ilkd.key.settings; +import java.beans.PropertyChangeListener; +import java.io.*; +import java.net.URL; +import java.nio.charset.StandardCharsets; +import java.util.*; + import de.uka.ilkd.key.util.KeYResourceManager; + import org.antlr.v4.runtime.CharStreams; import org.jspecify.annotations.NullMarked; import org.jspecify.annotations.Nullable; import org.slf4j.Logger; import org.slf4j.LoggerFactory; -import java.beans.PropertyChangeListener; -import java.io.*; -import java.net.URL; -import java.nio.charset.StandardCharsets; -import java.util.*; - /** * This class is used to load and save settings for proofs such as which data type models are used * to represent the java types. Which heuristics have to be loaded and so on. The class loads the @@ -36,10 +37,10 @@ public class ProofSettings { private static final Logger LOGGER = LoggerFactory.getLogger(ProofSettings.class); public static final File PROVER_CONFIG_FILE = - new File(PathConfig.getKeyConfigDir(), "proof-settings.props"); + new File(PathConfig.getKeyConfigDir(), "proof-settings.props"); public static final File PROVER_CONFIG_FILE_NEW = - new File(PathConfig.getKeyConfigDir(), "proof-settings.json"); + new File(PathConfig.getKeyConfigDir(), "proof-settings.json"); public static final URL PROVER_CONFIG_FILE_TEMPLATE = KeYResourceManager.getManager() .getResourceFile(ProofSettings.class, "default-proof-settings.json"); @@ -67,7 +68,7 @@ private static ProofSettings loadedSettings() { private final StrategySettings strategySettings = new StrategySettings(); private final ChoiceSettings choiceSettings = new ChoiceSettings(); private final ProofDependentSMTSettings smtSettings = - ProofDependentSMTSettings.getDefaultSettingsData(); + ProofDependentSMTSettings.getDefaultSettingsData(); private final NewSMTTranslationSettings newSMTSettings = new NewSMTTranslationSettings(); private final TermLabelSettings termLabelSettings = new TermLabelSettings(); @@ -143,9 +144,10 @@ public void settingsToStream(Writer out) { } /** - * Writes the settings to the given stream storing additional data into {@link #KEY_ADDITIONAL_DATA}. + * Writes the settings to the given stream storing additional data into + * {@link #KEY_ADDITIONAL_DATA}. * - * @param out a output destination + * @param out a output destination * @param additionalInformation a nullable map of additional information */ public void settingsToStream(Writer out, @Nullable Map additionalInformation) { @@ -165,7 +167,7 @@ public void saveSettings() { PROVER_CONFIG_FILE.getParentFile().mkdirs(); } try (Writer out = new BufferedWriter( - new FileWriter(PROVER_CONFIG_FILE_NEW, StandardCharsets.UTF_8))) { + new FileWriter(PROVER_CONFIG_FILE_NEW, StandardCharsets.UTF_8))) { settingsToStream(out); } } catch (IOException e) { @@ -191,7 +193,7 @@ public void loadSettingsFromJSONStream(Reader in) throws IOException { public void loadDefaultJSONSettings() { if (PROVER_CONFIG_FILE_TEMPLATE == null) { LOGGER.warn( - "default proof-settings file 'default-proof-settings.json' could not be found."); + "default proof-settings file 'default-proof-settings.json' could not be found."); } else { try (var in = new InputStreamReader(PROVER_CONFIG_FILE_TEMPLATE.openStream())) { loadSettingsFromJSONStream(in); diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/WindowUserInterfaceControl.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/WindowUserInterfaceControl.java index df726eedb11..5f0d5a06085 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/WindowUserInterfaceControl.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/WindowUserInterfaceControl.java @@ -394,7 +394,7 @@ public Path saveProof(Proof proof, String fileExtension) { saver = new ProofSaver(proof, filename, KeYConstants.INTERNAL_VERSION); } - if(getMediator().getSelectedProof() == proof) { + if (getMediator().getSelectedProof() == proof) { saver.setPathToLastSelectedNode(getMediator().getSelectedNode().getPosInProof()); } @@ -529,12 +529,14 @@ public void loadingFinished(AbstractProblemLoader loader, LoadedPOContainer poCo } } getMediator().resetNrGoalsClosedByHeuristics(); - if (poContainer != null && poContainer.getProofOblInput() instanceof KeYUserProblemFile file) { - //TODO weigl not triggered + if (poContainer != null + && poContainer.getProofOblInput() instanceof KeYUserProblemFile file) { + // TODO weigl not triggered var settings = file.readSettings(); var addInfo = settings.getSection(ProofSettings.KEY_ADDITIONAL_DATA); - if(addInfo!=null){ - var lastSelectedNodePath = settings.getIntList(OutputStreamProofSaver.KEY_LAST_SELECTED_NODE); + if (addInfo != null) { + var lastSelectedNodePath = + settings.getIntList(OutputStreamProofSaver.KEY_LAST_SELECTED_NODE); if (lastSelectedNodePath != null && proofList != null) { var proof = proofList.getFirstProof(); proof.root().traversePath(lastSelectedNodePath.iterator()); diff --git a/key.util/src/main/java/org/key_project/util/collection/KeYCollections.java b/key.util/src/main/java/org/key_project/util/collection/KeYCollections.java index 234fbd1686e..676ebc50adb 100644 --- a/key.util/src/main/java/org/key_project/util/collection/KeYCollections.java +++ b/key.util/src/main/java/org/key_project/util/collection/KeYCollections.java @@ -78,7 +78,7 @@ public static Map apply(Map m0, Map m1) { * {@link Object#toString()} is used to turn the objects into strings. * * @param collection an arbitrary non-null collection - * @param delimiter a non-null string which is put between the elements. + * @param delimiter a non-null string which is put between the elements. * @return the concatenation of all string representations separated by the delimiter */ public static String join(Iterable collection, String delimiter) { @@ -93,7 +93,7 @@ public static String join(Iterable collection, String delimiter) { * {@link Object#toString()} is used to turn the objects into strings. * * @param collection an arbitrary non-null array of objects - * @param delimiter a non-null string which is put between the elements. + * @param delimiter a non-null string which is put between the elements. * @return the concatenation of all string representations separated by the delimiter */ public static String join(Object[] collection, String delimiter) { @@ -124,7 +124,8 @@ public static String join(Object[] collection, String delimiter) { } /** - * Creates a run-length encoding from the given positive integer array. The return array has the following form: + * Creates a run-length encoding from the given positive integer array. The return array has the + * following form: * every positive entry stands for its own. Every negative integer describes the repetition * of the following positive integer. *

@@ -157,7 +158,8 @@ public static int[] runLengthEncoding(int[] array) { public static int[] runLengthEncoding(Collection array) { var iter = array.iterator(); class PushbackIterator implements Iterator { - private int pushedBack=-1; + private int pushedBack = -1; + @Override public boolean hasNext() { return pushedBack >= 0 || iter.hasNext(); @@ -165,9 +167,9 @@ public boolean hasNext() { @Override public Integer next() { - if(pushedBack>=0){ + if (pushedBack >= 0) { var v = pushedBack; - pushedBack=-1; + pushedBack = -1; return v; } return iter.next(); @@ -190,7 +192,7 @@ public void pushBack(int last) { while (iter.hasNext() && (symbol == (last = piter.next()))) { count++; } - if(last!=symbol) { + if (last != symbol) { piter.pushBack(last); } if (count != 1) { diff --git a/key.util/src/test/java/org/key_project/util/collection/KeYCollectionsTest.java b/key.util/src/test/java/org/key_project/util/collection/KeYCollectionsTest.java index 6e09f70ab74..f76b9b3e0e4 100644 --- a/key.util/src/test/java/org/key_project/util/collection/KeYCollectionsTest.java +++ b/key.util/src/test/java/org/key_project/util/collection/KeYCollectionsTest.java @@ -1,14 +1,16 @@ +/* This file is part of KeY - https://key-project.org + * KeY is licensed under the GNU General Public License Version 2 + * SPDX-License-Identifier: GPL-2.0-only */ package org.key_project.util.collection; -import org.junit.jupiter.api.Test; - -import java.lang.constant.Constable; import java.util.List; import java.util.Spliterator; import java.util.Spliterators; import java.util.function.Consumer; import java.util.stream.StreamSupport; +import org.junit.jupiter.api.Test; + import static org.junit.jupiter.api.Assertions.assertArrayEquals; import static org.key_project.util.collection.KeYCollections.runLengthDecoding; import static org.key_project.util.collection.KeYCollections.runLengthEncoding; @@ -21,18 +23,22 @@ class KeYCollectionsTest { @Test void runLengthEncoding_test() { - assertArrayEquals(new int[]{1, -5, 2, 1}, runLengthEncoding(new int[]{1, 2, 2, 2, 2, 2, 1})); - assertArrayEquals(new int[]{-5, 2}, runLengthEncoding(new int[]{2, 2, 2, 2, 2})); - assertArrayEquals(new int[]{}, runLengthEncoding(new int[]{})); - assertArrayEquals(new int[]{-5, 2, -5, 1}, runLengthEncoding(new int[]{2, 2, 2, 2, 2, 1, 1, 1, 1, 1})); + assertArrayEquals(new int[] { 1, -5, 2, 1 }, + runLengthEncoding(new int[] { 1, 2, 2, 2, 2, 2, 1 })); + assertArrayEquals(new int[] { -5, 2 }, runLengthEncoding(new int[] { 2, 2, 2, 2, 2 })); + assertArrayEquals(new int[] {}, runLengthEncoding(new int[] {})); + assertArrayEquals(new int[] { -5, 2, -5, 1 }, + runLengthEncoding(new int[] { 2, 2, 2, 2, 2, 1, 1, 1, 1, 1 })); } @Test void runLengthEncoding_test2() { - assertArrayEquals(new int[]{}, runLengthEncoding(List.of())); - assertArrayEquals(new int[]{1, -5, 2, 1}, runLengthEncoding(List.of(1, 2, 2, 2, 2, 2, 1))); - assertArrayEquals(new int[]{-5, 2}, runLengthEncoding(List.of(2, 2, 2, 2, 2))); - assertArrayEquals(new int[]{-5, 2, -5, 1}, runLengthEncoding(List.of(2, 2, 2, 2, 2, 1, 1, 1, 1, 1))); + assertArrayEquals(new int[] {}, runLengthEncoding(List.of())); + assertArrayEquals(new int[] { 1, -5, 2, 1 }, + runLengthEncoding(List.of(1, 2, 2, 2, 2, 2, 1))); + assertArrayEquals(new int[] { -5, 2 }, runLengthEncoding(List.of(2, 2, 2, 2, 2))); + assertArrayEquals(new int[] { -5, 2, -5, 1 }, + runLengthEncoding(List.of(2, 2, 2, 2, 2, 1, 1, 1, 1, 1))); } @@ -41,16 +47,17 @@ void runLengthDecoding_test() { Consumer tester = original -> { final var rle = runLengthEncoding(original); final var iter = runLengthDecoding(rle); - var stream = StreamSupport.stream(Spliterators.spliteratorUnknownSize(iter, Spliterator.ORDERED), false) + var stream = StreamSupport + .stream(Spliterators.spliteratorUnknownSize(iter, Spliterator.ORDERED), false) .mapToInt(it -> it) .toArray(); System.out.println(stream); assertArrayEquals(original, stream); }; - tester.accept(new int[]{1, 2, 2, 2, 2, 2, 1}); - tester.accept(new int[]{2, 2, 2, 2, 2}); - tester.accept(new int[]{}); - tester.accept(new int[]{2, 2, 2, 2, 2, 1, 1, 1, 1, 1}); + tester.accept(new int[] { 1, 2, 2, 2, 2, 2, 1 }); + tester.accept(new int[] { 2, 2, 2, 2, 2 }); + tester.accept(new int[] {}); + tester.accept(new int[] { 2, 2, 2, 2, 2, 1, 1, 1, 1, 1 }); } From 48b5e70473d6f7a0ebd4c92d5c2cd5779a0f277d Mon Sep 17 00:00:00 2001 From: Alexander Weigl Date: Wed, 10 Sep 2025 23:16:40 +0200 Subject: [PATCH 3/3] fix errors from rebasing --- .../control/AbstractUserInterfaceControl.java | 1 + .../java/de/uka/ilkd/key/nparser/KeyAst.java | 11 +++++++++ .../main/java/de/uka/ilkd/key/proof/Node.java | 1 - .../key/proof/io/OutputStreamProofSaver.java | 2 ++ .../uka/ilkd/key/settings/Configuration.java | 24 ++++++++++++++++--- .../key/gui/WindowUserInterfaceControl.java | 14 ++++++----- 6 files changed, 43 insertions(+), 10 deletions(-) diff --git a/key.core/src/main/java/de/uka/ilkd/key/control/AbstractUserInterfaceControl.java b/key.core/src/main/java/de/uka/ilkd/key/control/AbstractUserInterfaceControl.java index 67bccc1a181..19cb701e060 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/control/AbstractUserInterfaceControl.java +++ b/key.core/src/main/java/de/uka/ilkd/key/control/AbstractUserInterfaceControl.java @@ -22,6 +22,7 @@ import de.uka.ilkd.key.proof.io.ProblemLoaderException; import de.uka.ilkd.key.proof.io.SingleThreadProblemLoader; import de.uka.ilkd.key.proof.mgt.ProofEnvironment; +import de.uka.ilkd.key.settings.Configuration; import org.key_project.prover.engine.ProverCore; import org.key_project.prover.engine.ProverTaskListener; diff --git a/key.core/src/main/java/de/uka/ilkd/key/nparser/KeyAst.java b/key.core/src/main/java/de/uka/ilkd/key/nparser/KeyAst.java index e3e50418712..c21de3859ab 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/nparser/KeyAst.java +++ b/key.core/src/main/java/de/uka/ilkd/key/nparser/KeyAst.java @@ -185,6 +185,17 @@ public String getProblemHeader() { } return ""; } + + /// Returns the raw settings within a [de.uka.ilkd.key.proof.io.KeYFile]. + public Configuration findSettings() { + final var cfg = new ConfigurationBuilder(); + if (ctx.preferences() == null || ctx.preferences().cvalue() == null) { + return new Configuration(); + } + + var c = ctx.preferences().cvalue(); + return (Configuration) c.accept(cfg); + } } public static class ConfigurationFile extends KeyAst { diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/Node.java b/key.core/src/main/java/de/uka/ilkd/key/proof/Node.java index 8da653ad7c8..6c7a5079394 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/Node.java +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/Node.java @@ -11,7 +11,6 @@ import de.uka.ilkd.key.proof.reference.ClosedBy; import de.uka.ilkd.key.rule.NoPosTacletApp; import de.uka.ilkd.key.rule.merge.MergeRule; -import de.uka.ilkd.key.util.Pair; import org.key_project.logic.op.Function; import org.key_project.prover.rules.RuleApp; 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 354b5889c22..e314a52c437 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 @@ -60,6 +60,8 @@ import org.key_project.util.collection.ImmutableList; import org.key_project.util.collection.KeYCollections; +import org.jspecify.annotations.NullMarked; +import org.jspecify.annotations.Nullable; import org.slf4j.Logger; import org.slf4j.LoggerFactory; diff --git a/key.core/src/main/java/de/uka/ilkd/key/settings/Configuration.java b/key.core/src/main/java/de/uka/ilkd/key/settings/Configuration.java index 0d434d8bf3b..736eea251de 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/settings/Configuration.java +++ b/key.core/src/main/java/de/uka/ilkd/key/settings/Configuration.java @@ -268,7 +268,7 @@ public List getList(String name) { /** * Returns a list of strings for the given name. - * + *

* In contrast to the other methods, this method does not throw an exception if the entry does * not * exist in the configuration. Instead, it returns an empty list. @@ -433,14 +433,19 @@ public void overwriteWith(Configuration other) { } // TODO Add documentation for this. + /** * POJO for metadata of configuration entries. */ public static class ConfigurationMeta { - /** Position of declaration within a file */ + /** + * Position of declaration within a file + */ private Position position; - /** documentation given in the file */ + /** + * documentation given in the file + */ private String documentation; public Position getPosition() { @@ -550,6 +555,19 @@ private ConfigurationWriter print(String s) { return this; } + private ConfigurationWriter printSeq(int[] values) { + out.format("["); + for (var i = 0; i < values.length; i++) { + int o = values[i]; + printValue(o); + if (i + 1 < values.length) { + print(", "); + } + } + out.format("]"); + return this; + } + private ConfigurationWriter printSeq(Collection value) { out.format("[ "); indent += 4; diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/WindowUserInterfaceControl.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/WindowUserInterfaceControl.java index 5f0d5a06085..5813343e333 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/WindowUserInterfaceControl.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/WindowUserInterfaceControl.java @@ -34,6 +34,7 @@ import de.uka.ilkd.key.proof.io.*; import de.uka.ilkd.key.proof.io.AbstractProblemLoader.ReplayResult; import de.uka.ilkd.key.rule.IBuiltInRuleApp; +import de.uka.ilkd.key.settings.Configuration; import de.uka.ilkd.key.settings.ProofIndependentSettings; import de.uka.ilkd.key.settings.ProofSettings; import de.uka.ilkd.key.settings.ViewSettings; @@ -509,8 +510,10 @@ public void loadingStarted(AbstractProblemLoader loader) { @Override public void loadingFinished(AbstractProblemLoader loader, LoadedPOContainer poContainer, - ProofAggregate proofList, ReplayResult result) throws ProblemLoaderException { - super.loadingFinished(loader, poContainer, proofList, result); + ProofAggregate proofList, ReplayResult result, Configuration settings) + throws ProblemLoaderException { + + super.loadingFinished(loader, poContainer, proofList, result, settings); if (proofList != null) { if (result != null) { if ("".equals(result.getStatus())) { @@ -532,22 +535,21 @@ public void loadingFinished(AbstractProblemLoader loader, LoadedPOContainer poCo if (poContainer != null && poContainer.getProofOblInput() instanceof KeYUserProblemFile file) { // TODO weigl not triggered - var settings = file.readSettings(); var addInfo = settings.getSection(ProofSettings.KEY_ADDITIONAL_DATA); if (addInfo != null) { var lastSelectedNodePath = settings.getIntList(OutputStreamProofSaver.KEY_LAST_SELECTED_NODE); if (lastSelectedNodePath != null && proofList != null) { var proof = proofList.getFirstProof(); - proof.root().traversePath(lastSelectedNodePath.iterator()); + var selectedNode = proof.root().traversePath( + lastSelectedNodePath.stream().map(Long::intValue).iterator()); + getMediator().getSelectionModel().setSelectedNode(selectedNode); } } file.close(); } } - - /** * Loads the given location and returns all required references as {@link KeYEnvironment} with * KeY's {@link MainWindow}.