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 ef7a1e8c6fa..d1cdaf985f1 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 @@ -26,6 +26,7 @@ import de.uka.ilkd.key.prover.ProverTaskListener; import de.uka.ilkd.key.prover.TaskFinishedInfo; import de.uka.ilkd.key.prover.TaskStartedInfo; +import de.uka.ilkd.key.settings.Configuration; import org.slf4j.LoggerFactory; @@ -255,7 +256,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/control/KeYEnvironment.java b/key.core/src/main/java/de/uka/ilkd/key/control/KeYEnvironment.java index 370527fb280..73d1fd6b3ae 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/control/KeYEnvironment.java +++ b/key.core/src/main/java/de/uka/ilkd/key/control/KeYEnvironment.java @@ -10,7 +10,7 @@ import de.uka.ilkd.key.java.JavaInfo; import de.uka.ilkd.key.java.Services; -import de.uka.ilkd.key.parser.Location; +import de.uka.ilkd.key.nparser.KeyAst; import de.uka.ilkd.key.proof.Proof; import de.uka.ilkd.key.proof.init.InitConfig; import de.uka.ilkd.key.proof.init.Profile; @@ -20,7 +20,6 @@ import de.uka.ilkd.key.proof.io.AbstractProblemLoader.ReplayResult; import de.uka.ilkd.key.proof.io.ProblemLoaderException; import de.uka.ilkd.key.proof.mgt.SpecificationRepository; -import de.uka.ilkd.key.util.Pair; /** * Instances of this class are used to collect and access all relevant information for verification @@ -47,7 +46,7 @@ public class KeYEnvironment { /** * An optional field denoting a script contained in the proof file. */ - private final Pair proofScript; + private final KeyAst.ProofScriptEntry proofScript; /** * Indicates that this {@link KeYEnvironment} is disposed. @@ -76,7 +75,7 @@ public KeYEnvironment(U ui, InitConfig initConfig) { * @param initConfig The loaded project. */ public KeYEnvironment(U ui, InitConfig initConfig, Proof loadedProof, - Pair proofScript, ReplayResult replayResult) { + KeyAst.ProofScriptEntry proofScript, ReplayResult replayResult) { this.ui = ui; this.initConfig = initConfig; this.loadedProof = loadedProof; @@ -316,7 +315,7 @@ public boolean isDisposed() { return disposed; } - public Pair getProofScript() { + public KeyAst.ProofScriptEntry getProofScript() { return proofScript; } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/ProofScriptEngine.java b/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/ProofScriptEngine.java index f5dabe1d5e1..6458cd9c422 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/ProofScriptEngine.java +++ b/key.core/src/main/java/de/uka/ilkd/key/macros/scripts/ProofScriptEngine.java @@ -14,6 +14,7 @@ import de.uka.ilkd.key.control.AbstractUserInterfaceControl; import de.uka.ilkd.key.java.Position; +import de.uka.ilkd.key.nparser.KeyAst; import de.uka.ilkd.key.parser.Location; import de.uka.ilkd.key.proof.Goal; import de.uka.ilkd.key.proof.Node; @@ -67,6 +68,10 @@ public ProofScriptEngine(String script, Location initLocation, Goal initiallySel this.initiallySelectedGoal = initiallySelectedGoal; } + public ProofScriptEngine(KeyAst.ProofScriptEntry script) { + this(script.code(), script.getLocation()); + } + private static Map> loadCommands() { Map> result = new HashMap<>(); var loader = ServiceLoader.load(ProofScriptCommand.class); 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 c5dc159aa8e..d81da231dd0 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 @@ -3,17 +3,19 @@ * SPDX-License-Identifier: GPL-2.0-only */ package de.uka.ilkd.key.nparser; +import java.net.URI; import java.net.URL; import java.util.List; +import de.uka.ilkd.key.java.Position; import de.uka.ilkd.key.nparser.builder.BuilderHelpers; import de.uka.ilkd.key.nparser.builder.ChoiceFinder; import de.uka.ilkd.key.nparser.builder.FindProblemInformation; import de.uka.ilkd.key.nparser.builder.IncludeFinder; +import de.uka.ilkd.key.parser.Location; import de.uka.ilkd.key.proof.init.Includes; import de.uka.ilkd.key.settings.Configuration; import de.uka.ilkd.key.settings.ProofSettings; -import de.uka.ilkd.key.util.Triple; import org.key_project.util.java.StringUtil; @@ -73,11 +75,28 @@ public static class File extends KeyAst { return settings; } - public @Nullable Triple findProofScript() { + /** + * 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); + } + + + public @Nullable ProofScriptEntry findProofScript() { if (ctx.problem() != null && ctx.problem().proofScript() != null) { KeYParser.ProofScriptContext pctx = ctx.problem().proofScript(); String text = pctx.ps.getText(); - return new Triple<>(StringUtil.trim(text, '"'), pctx.ps.getLine(), + return new ProofScriptEntry( + StringUtil.trim(text, '"'), + URI.create(pctx.start.getInputStream().getSourceName()), + pctx.ps.getLine(), pctx.ps.getCharPositionInLine()); } return null; @@ -167,4 +186,17 @@ public Taclet(KeYParser.TacletContext taclet) { super(taclet); } } + + /** + * This class represents the entry of a proof script within a KeY file. + * + * @param code non-null string containing the proof script + * @param line line number of the entry + * @param charPositionInLine starting offset position in the line + */ + public record ProofScriptEntry(@NonNull String code, URI source, int line, int charPositionInLine) { + public Location getLocation() { + return new Location(source, Position.newOneBased(this.line(), this.charPositionInLine())); + } + } } 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 533828bb803..7f9716420c2 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,15 +3,7 @@ * 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 java.util.*; import de.uka.ilkd.key.logic.RenamingTable; import de.uka.ilkd.key.logic.Sequent; @@ -49,10 +41,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 Node parent = null; /** * The branch location of this proof node. @@ -81,7 +77,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; /** @@ -162,7 +160,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; } @@ -176,7 +176,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,14 +227,16 @@ 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; } /** * Returns the set of created program variables known in this node. - * + *

* In the resulting list, the newest additions come first. * * @returns a non-null immutable list of program variables. @@ -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. @@ -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. */ @@ -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) { @@ -837,4 +846,37 @@ 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 af88fe91224..a4db0e29baf 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 @@ -18,18 +18,18 @@ import de.uka.ilkd.key.proof.io.IProofFileParser; import de.uka.ilkd.key.proof.io.KeYFile; import de.uka.ilkd.key.proof.io.consistency.FileRepo; +import de.uka.ilkd.key.settings.Configuration; import de.uka.ilkd.key.settings.ProofSettings; import de.uka.ilkd.key.speclang.PositionedString; import de.uka.ilkd.key.speclang.SLEnvInput; import de.uka.ilkd.key.util.ProgressMonitor; -import de.uka.ilkd.key.util.Triple; import org.key_project.util.collection.DefaultImmutableSet; import org.key_project.util.collection.ImmutableSet; import org.antlr.v4.runtime.CharStream; import org.antlr.v4.runtime.Token; -import org.jspecify.annotations.NonNull; +import org.jspecify.annotations.Nullable; /** @@ -37,8 +37,12 @@ * obligation. */ public final class KeYUserProblemFile extends KeYFile implements ProofOblInput { + @Nullable private Sequent problem = null; + @Nullable + private Configuration settings; + // ------------------------------------------------------------------------- // constructors // ------------------------------------------------------------------------- @@ -122,6 +126,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) { @@ -177,7 +188,7 @@ public boolean hasProofScript() { return getParseContext().findProofScript() != null; } - public Triple readProofScript() { + public KeyAst.ProofScriptEntry readProofScript() { return getParseContext().findProofScript(); } @@ -238,7 +249,6 @@ public Profile getProfile() { * is defined by the file. */ private Profile readProfileFromFile() { - @NonNull ProblemInformation pi = getProblemInformation(); String profileName = pi.getProfile(); if (profileName != null && !profileName.isEmpty()) { @@ -264,4 +274,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 ae83793a678..7c502f52cf8 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 @@ -9,19 +9,16 @@ import java.io.IOException; import java.lang.reflect.InvocationTargetException; import java.lang.reflect.Method; -import java.net.URI; import java.nio.charset.StandardCharsets; import java.nio.file.*; import java.util.*; import java.util.function.Consumer; -import java.util.stream.Collectors; import java.util.stream.Stream; import java.util.zip.ZipFile; -import de.uka.ilkd.key.java.Position; import de.uka.ilkd.key.java.Services; import de.uka.ilkd.key.nparser.KeYLexer; -import de.uka.ilkd.key.parser.Location; +import de.uka.ilkd.key.nparser.KeyAst; import de.uka.ilkd.key.proof.Node; import de.uka.ilkd.key.proof.Proof; import de.uka.ilkd.key.proof.ProofAggregate; @@ -32,6 +29,7 @@ import de.uka.ilkd.key.proof.io.consistency.SimpleFileRepo; import de.uka.ilkd.key.prover.impl.PerfScope; import de.uka.ilkd.key.rule.OneStepSimplifier; +import de.uka.ilkd.key.settings.Configuration; import de.uka.ilkd.key.settings.ProofIndependentSettings; import de.uka.ilkd.key.speclang.Contract; import de.uka.ilkd.key.speclang.SLEnvInput; @@ -39,7 +37,6 @@ import de.uka.ilkd.key.strategy.StrategyProperties; import de.uka.ilkd.key.util.ExceptionHandlerException; import de.uka.ilkd.key.util.Pair; -import de.uka.ilkd.key.util.Triple; import org.key_project.util.java.IOUtil; import org.key_project.util.reflection.ClassLoaderUtil; @@ -288,13 +285,10 @@ public final void load(Consumer callbackProofLoaded) proofList = createProof(poContainer); loadSelectedProof(poContainer, proofList, callbackProofLoaded); } - } catch (Throwable t) { - // Throw this exception; otherwise, it can for instance occur - // that "result" will be null (if replayProof(...) fails) and - // we get a NullPointerException that is hard to analyze. - throw t; } finally { - control.loadingFinished(this, poContainer, proofList, result); + var settings = (envInput instanceof KeYUserProblemFile kupf) ? kupf.readSettings() + : new Configuration(); + control.loadingFinished(this, poContainer, proofList, result, settings); } } @@ -342,13 +336,10 @@ protected void selectAndLoadProof(ProblemLoaderControl control, InitConfig initC * @param poContainer the container created by {@link #createProofObligationContainer()}. * @param proofList the proof list containing the proof to load. * @param callbackProofLoaded optional callback, called before the proof is replayed - * @throws ProofInputException Occurred Exception. - * @throws ProblemLoaderException Occurred Exception. * @see AbstractProblemLoader#load() */ protected void loadSelectedProof(LoadedPOContainer poContainer, ProofAggregate proofList, - Consumer callbackProofLoaded) - throws ProofInputException, ProblemLoaderException { + Consumer callbackProofLoaded) { // try to replay first proof proof = proofList.getProof(poContainer.getProofNum()); @@ -470,7 +461,7 @@ protected EnvInput createEnvInput(FileRepo fileRepo) throws IOException { try (ZipFile bundle = new ZipFile(file)) { proofs = bundle.stream().filter(e -> !e.isDirectory()) .filter(e -> e.getName().endsWith(".proof")) - .map(e -> Paths.get(e.getName())).collect(Collectors.toList()); + .map(e -> Paths.get(e.getName())).toList(); } if (!proofs.isEmpty()) { // load first proof found in file @@ -680,18 +671,13 @@ public boolean hasProofScript() { return false; } - public Pair readProofScript() throws ProofInputException { + public KeyAst.ProofScriptEntry readProofScript() throws ProofInputException { assert envInput instanceof KeYUserProblemFile; KeYUserProblemFile kupf = (KeYUserProblemFile) envInput; - - Triple script = kupf.readProofScript(); - URI url = kupf.getInitialFile().toURI(); - Location location = new Location(url, Position.newOneBased(script.second, script.third)); - - return new Pair<>(script.first, location); + return kupf.readProofScript(); } - public Pair getProofScript() throws ProblemLoaderException { + public KeyAst.ProofScriptEntry getProofScript() throws ProblemLoaderException { if (hasProofScript()) { try { return readProofScript(); @@ -724,9 +710,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 1939b925ec6..7e9b01b74d5 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 @@ -50,7 +50,10 @@ import org.key_project.util.collection.ImmutableList; import org.key_project.util.collection.ImmutableMapEntry; +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; @@ -59,21 +62,30 @@ * * @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; /** @@ -82,6 +94,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"); @@ -89,7 +102,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); } } @@ -149,7 +162,13 @@ 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 { @@ -229,6 +248,7 @@ public void save(OutputStream out) throws IOException { } } + @Nullable protected String getBasePath() throws IOException { File javaSourceLocation = getJavaSourceLocation(proof); if (javaSourceLocation != null) { @@ -245,7 +265,7 @@ protected String getBasePath() throws IOException { private String makePathsRelative(String header) { final String[] search = new String[] { "\\javaSource", "\\bootclasspath", "\\classpath", "\\include" }; - final String basePath; + String basePath; String tmp = header; try { basePath = getBasePath(); @@ -270,7 +290,7 @@ private String makePathsRelative(String header) { // there may be more than one path while (0 <= tmp.indexOf('"', i) && tmp.indexOf('"', i) < l) { - if (relPathString.length() > 0) { + if (!relPathString.isEmpty()) { relPathString.append(", "); } @@ -694,7 +714,7 @@ 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 ""; } @@ -717,9 +737,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<>(); @@ -826,7 +846,8 @@ public static String printAnything(Object val, Services services) { return printAnything(val, services, true); } - public static String printAnything(Object val, Services services, + @Nullable + public static String printAnything(@Nullable Object val, Services services, boolean shortAttrNotation) { if (val instanceof ProgramElement) { return printProgramElement((ProgramElement) val); @@ -847,17 +868,47 @@ 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/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/proof/io/ProofBundleSaver.java b/key.core/src/main/java/de/uka/ilkd/key/proof/io/ProofBundleSaver.java index 32e54ea77ba..81e500a88e6 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, File saveFile) { @Override protected void save(File 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(File 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().toString() + ".proof"); + String proofFileName = MiscTools.toValidFileName(getProof().name().toString() + ".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 7785598b50a..b2598276d1d 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 @@ -54,7 +54,7 @@ public static Configuration load(File file) throws IOException { /** * Loads a configuration using the given char stream. * - * @param file existsing file path + * @param input existing file path * @return a configuration based on the file contents * @throws IOException i/o error on the steram */ @@ -129,8 +129,8 @@ public Object get(String name) { * Returns an integer or {@code null} if not such entry exists. * * @param name property name - * @throw ClassCastException if the entry is not an {@link #Long} - * @throw NullPointerException if no such value entry exists + * @throws ClassCastException if the entry is not an {@link #Long} + * @throws NullPointerException if no such value entry exists */ public int getInt(String name) { return (int) getLong(name); @@ -141,8 +141,8 @@ public int getInt(String name) { * present. * * @param name property name - * @throw ClassCastException if the entry is not an {@link #Long} - * @throw NullPointerException if no such value entry exists + * @throws ClassCastException if the entry is not an {@link #Long} + * @throws NullPointerException if no such value entry exists */ public int getInt(String name, int defaultValue) { return (int) getLong(name, defaultValue); @@ -152,8 +152,8 @@ public int getInt(String name, int defaultValue) { * Returns a long value for the given name. {@code null} if no such value is present. * * @param name property name - * @throw ClassCastException if the entry is not an {@link #Long} - * @throw NullPointerException if no such value entry exists + * @throws ClassCastException if the entry is not an {@link #Long} + * @throws NullPointerException if no such value entry exists */ public long getLong(String name) { return get(name, Long.class); @@ -163,8 +163,8 @@ public long getLong(String name) { * Returns a long value for the given name. {@code defaultValue} if no such value is present. * * @param name property name - * @throw ClassCastException if the entry is not an {@link #Long} - * @throw NullPointerException if no such value entry exists + * @throws ClassCastException if the entry is not an {@link #Long} + * @throws NullPointerException if no such value entry exists */ public long getLong(String name, long defaultValue) { var value = get(name, Long.class); @@ -175,8 +175,8 @@ public long getLong(String name, long defaultValue) { * Returns a boolean value for the given name. * * @param name property name - * @throw ClassCastException if the entry is not an {@link #Long} - * @throw NullPointerException if no such value entry exists + * @throws ClassCastException if the entry is not an {@link #Long} + * @throws NullPointerException if no such value entry exists */ public boolean getBool(String name) { return get(name, Boolean.class); @@ -186,8 +186,8 @@ public boolean getBool(String name) { * Returns a boolean value for the given name. {@code defaultValue} if no such value is present. * * @param name property name - * @throw ClassCastException if the entry is not an {@link #Long} - * @throw NullPointerException if no such value entry exists + * @throws ClassCastException if the entry is not an {@link #Long} + * @throws NullPointerException if no such value entry exists */ public boolean getBool(String name, boolean defaultValue) { return get(name, defaultValue); @@ -198,15 +198,15 @@ public boolean getBool(String name, boolean defaultValue) { * present. * * @param name property name - * @throw ClassCastException if the entry is not an {@link #Long} - * @throw NullPointerException if no such value entry exists + * @throws ClassCastException if the entry is not an {@link #Long} + * @throws NullPointerException if no such value entry exists */ public double getDouble(String name) { return get(name, Double.class); } /** - * Returns an string value for the given name. {@code null} if no such value is present. + * Returns a string value for the given name. {@code null} if no such value is present. * * @param name property name */ @@ -216,7 +216,7 @@ public String getString(String name) { } /** - * Returns an string value for the given name. {@code defaultValue} if no such value is present. + * Returns a string value for the given name. {@code defaultValue} if no such value is present. * * @param name property name */ @@ -225,7 +225,7 @@ public String getString(String name, String defaultValue) { } /** - * Returns an sub configuration for the given name. {@code null} if no such value is present. + * Returns a sub configuration for the given name. {@code null} if no such value is present. * * @param name property name */ @@ -260,6 +260,19 @@ public List getStringList(String name) { return seq; } + /** + * 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 Long)) + throw new ClassCastException(); + return seq; + } + /** * Returns string array for the requested entry. {@code defaultValue} is returned if no such * entry exists. @@ -277,7 +290,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) { @@ -376,6 +389,7 @@ public void save(Writer writer, String comment) { new ConfigurationWriter(writer).printComment(comment).printMap(this.data); } + /** * POJO for metadata of configuration entries. */ @@ -457,12 +471,15 @@ 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); } return this; } + private ConfigurationWriter printMap(Map value) { out.format("{ "); indent += 4; @@ -490,12 +507,16 @@ private ConfigurationWriter print(String s) { return this; } - private ConfigurationWriter printSeq(Collection value) { + private void printSeq(int[] array) { + printSeq(Arrays.stream(array).boxed().toList()); + } + + private ConfigurationWriter printSeq(Collection value) { out.format("[ "); indent += 4; newline(); printIndent(); - for (Iterator iterator = value.iterator(); iterator.hasNext();) { + for (var iterator = value.iterator(); iterator.hasNext();) { Object o = iterator.next(); printValue(o); if (iterator.hasNext()) { 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 319df9a2b2e..baa6e0a7b3a 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 @@ -7,13 +7,13 @@ 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 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; @@ -32,6 +32,7 @@ * @see Properties * @see Settings */ +@NullMarked public class ProofSettings { private static final Logger LOGGER = LoggerFactory.getLogger(ProofSettings.class); @@ -45,6 +46,7 @@ public class ProofSettings { .getResourceFile(ProofSettings.class, "default-proof-settings.json"); public static final ProofSettings DEFAULT_SETTINGS = ProofSettings.loadedSettings(); + public static final String KEY_ADDITIONAL_DATA = "additionalInformation"; private static ProofSettings loadedSettings() { @@ -70,8 +72,8 @@ private static ProofSettings loadedSettings() { 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 +135,27 @@ 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"); } /** @@ -157,8 +176,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(); } diff --git a/key.core/src/test/java/de/uka/ilkd/key/logic/TestLocalSymbols.java b/key.core/src/test/java/de/uka/ilkd/key/logic/TestLocalSymbols.java index 00c2b3ffa33..97d12069907 100644 --- a/key.core/src/test/java/de/uka/ilkd/key/logic/TestLocalSymbols.java +++ b/key.core/src/test/java/de/uka/ilkd/key/logic/TestLocalSymbols.java @@ -127,7 +127,7 @@ public void testDoubleInstantiation() throws Exception { KeYEnvironment env = loadProof("doubleSkolem.key"); Proof proof = env.getLoadedProof(); - String script = env.getProofScript().first; + String script = env.getProofScript().code(); ProofScriptEngine pse = new ProofScriptEngine(script, new Location(null, Position.newOneBased(1, 1))); diff --git a/key.core/src/test/java/de/uka/ilkd/key/proof/proverules/ProveRulesTest.java b/key.core/src/test/java/de/uka/ilkd/key/proof/proverules/ProveRulesTest.java index 527b27e7e36..b49b0bcfdec 100644 --- a/key.core/src/test/java/de/uka/ilkd/key/proof/proverules/ProveRulesTest.java +++ b/key.core/src/test/java/de/uka/ilkd/key/proof/proverules/ProveRulesTest.java @@ -10,7 +10,6 @@ import de.uka.ilkd.key.control.DefaultUserInterfaceControl; import de.uka.ilkd.key.control.KeYEnvironment; import de.uka.ilkd.key.macros.scripts.ProofScriptEngine; -import de.uka.ilkd.key.parser.Location; import de.uka.ilkd.key.proof.Proof; import de.uka.ilkd.key.proof.init.Profile; import de.uka.ilkd.key.proof.io.ProblemLoaderException; @@ -18,7 +17,6 @@ import de.uka.ilkd.key.rule.Taclet; import de.uka.ilkd.key.util.HelperClassForTests; import de.uka.ilkd.key.util.LinkedHashMap; -import de.uka.ilkd.key.util.Pair; import org.key_project.util.helper.FindResources; @@ -69,9 +67,9 @@ public void loadTacletProof(String tacletName, Taclet taclet, File proofFile) th KeYEnvironment env = KeYEnvironment.load(proofFile); Proof proof = env.getLoadedProof(); - Pair script = env.getProofScript(); + var script = env.getProofScript(); if (script != null) { - ProofScriptEngine pse = new ProofScriptEngine(script.first, script.second); + ProofScriptEngine pse = new ProofScriptEngine(script.code(), script.getLocation()); pse.execute(env.getUi(), proof); } diff --git a/key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/ProveTest.java b/key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/ProveTest.java index 6c0696f47c2..110350ce492 100644 --- a/key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/ProveTest.java +++ b/key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/ProveTest.java @@ -10,7 +10,7 @@ import de.uka.ilkd.key.control.DefaultUserInterfaceControl; import de.uka.ilkd.key.control.KeYEnvironment; import de.uka.ilkd.key.macros.scripts.ProofScriptEngine; -import de.uka.ilkd.key.parser.Location; +import de.uka.ilkd.key.nparser.KeyAst; import de.uka.ilkd.key.proof.Proof; import de.uka.ilkd.key.proof.io.AbstractProblemLoader; import de.uka.ilkd.key.proof.io.ProblemLoaderException; @@ -93,10 +93,9 @@ private void runKey(String file, TestProperty testProperty) throws Exception { boolean success; try { // Initialize KeY environment and load proof. - Pair, Pair> pair = - load(keyFile); + var pair = load(keyFile); env = pair.first; - Pair script = pair.second; + var script = pair.second; loadedProof = env.getLoadedProof(); AbstractProblemLoader.ReplayResult replayResult = env.getReplayResult(); @@ -168,14 +167,14 @@ private void reload(File proofFile, Proof loadedProof) throws Exception { * want to use a different strategy. */ private void autoMode(KeYEnvironment env, Proof loadedProof, - Pair script) throws Exception { + KeyAst.ProofScriptEntry script) throws Exception { // Run KeY prover. if (script == null) { // auto mode env.getProofControl().startAndWaitForAutoMode(loadedProof); } else { // ... script - ProofScriptEngine pse = new ProofScriptEngine(script.first, script.second); + ProofScriptEngine pse = new ProofScriptEngine(script); pse.execute(env.getUi(), env.getLoadedProof()); } } @@ -183,7 +182,7 @@ private void autoMode(KeYEnvironment env, Proof loa /* * has resemblances with KeYEnvironment.load ... */ - private Pair, Pair> load( + private Pair, KeyAst.ProofScriptEntry> load( File keyFile) throws ProblemLoaderException { KeYEnvironment env = KeYEnvironment.load(keyFile); return new Pair<>(env, env.getProofScript()); diff --git a/key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/performance/DataRecordingTestFile.java b/key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/performance/DataRecordingTestFile.java index af574c0ccbf..317fc985fda 100644 --- a/key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/performance/DataRecordingTestFile.java +++ b/key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/performance/DataRecordingTestFile.java @@ -8,7 +8,7 @@ import de.uka.ilkd.key.control.DefaultUserInterfaceControl; import de.uka.ilkd.key.control.KeYEnvironment; -import de.uka.ilkd.key.parser.Location; +import de.uka.ilkd.key.nparser.KeyAst; import de.uka.ilkd.key.proof.Proof; import de.uka.ilkd.key.proof.runallproofs.proofcollection.ProofCollectionSettings; import de.uka.ilkd.key.proof.runallproofs.proofcollection.TestFile; @@ -16,7 +16,6 @@ import de.uka.ilkd.key.prover.impl.ApplyStrategy; import de.uka.ilkd.key.prover.impl.ApplyStrategyInfo; import de.uka.ilkd.key.strategy.Strategy; -import de.uka.ilkd.key.util.Pair; class DataRecordingTestFile extends TestFile { public final ProfilingDirectories directories; @@ -29,7 +28,7 @@ public DataRecordingTestFile(TestProperty testProperty, String path, @Override protected void autoMode(KeYEnvironment env, Proof loadedProof, - Pair script) throws Exception { + KeyAst.ProofScriptEntry script) throws Exception { // Run KeY prover. if (script == null) { DataRecordingStrategy strategy = new DataRecordingStrategy(loadedProof, this); diff --git a/key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/proofcollection/TestFile.java b/key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/proofcollection/TestFile.java index 00b4b408f49..2f362dcf9ba 100644 --- a/key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/proofcollection/TestFile.java +++ b/key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/proofcollection/TestFile.java @@ -13,7 +13,7 @@ import de.uka.ilkd.key.control.DefaultUserInterfaceControl; import de.uka.ilkd.key.control.KeYEnvironment; import de.uka.ilkd.key.macros.scripts.ProofScriptEngine; -import de.uka.ilkd.key.parser.Location; +import de.uka.ilkd.key.nparser.KeyAst; import de.uka.ilkd.key.proof.Proof; import de.uka.ilkd.key.proof.io.AbstractProblemLoader.ReplayResult; import de.uka.ilkd.key.proof.io.ProblemLoaderException; @@ -160,10 +160,9 @@ public TestResult runKey() throws Exception { boolean success; try { // Initialize KeY environment and load proof. - Pair, Pair> pair = - load(keyFile); + var pair = load(keyFile); env = pair.first; - Pair script = pair.second; + var script = pair.second; loadedProof = env.getLoadedProof(); ReplayResult replayResult; @@ -262,14 +261,14 @@ protected void reload(boolean verbose, File proofFile, Proof loadedProof, boolea * want to use a different strategy. */ protected void autoMode(KeYEnvironment env, Proof loadedProof, - Pair script) throws Exception { + KeyAst.ProofScriptEntry script) throws Exception { // Run KeY prover. if (script == null) { // auto mode env.getProofControl().startAndWaitForAutoMode(loadedProof); } else { // ... script - ProofScriptEngine pse = new ProofScriptEngine(script.first, script.second); + ProofScriptEngine pse = new ProofScriptEngine(script.code(), script.getLocation()); pse.execute(env.getUi(), env.getLoadedProof()); } } @@ -277,7 +276,7 @@ protected void autoMode(KeYEnvironment env, Proof l /* * has resemblances with KeYEnvironment.load ... */ - private Pair, Pair> load( + private Pair, KeyAst.ProofScriptEntry> load( File keyFile) throws ProblemLoaderException { KeYEnvironment env = KeYEnvironment.load(keyFile); return new Pair<>(env, env.getProofScript()); 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 88d8f7c46ba..bbcf41cfba2 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 @@ -24,7 +24,7 @@ import de.uka.ilkd.key.gui.notification.events.NotificationEvent; import de.uka.ilkd.key.macros.ProofMacro; import de.uka.ilkd.key.macros.ProofMacroFinishedInfo; -import de.uka.ilkd.key.parser.Location; +import de.uka.ilkd.key.nparser.KeyAst; import de.uka.ilkd.key.proof.Goal; import de.uka.ilkd.key.proof.Proof; import de.uka.ilkd.key.proof.ProofAggregate; @@ -38,7 +38,9 @@ import de.uka.ilkd.key.prover.TaskStartedInfo; import de.uka.ilkd.key.prover.impl.ApplyStrategyInfo; 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; import de.uka.ilkd.key.speclang.PositionedString; import de.uka.ilkd.key.strategy.StrategyProperties; @@ -50,6 +52,7 @@ import de.uka.ilkd.key.util.ThreadUtilities; import org.key_project.util.collection.ImmutableSet; +import org.key_project.util.collection.KeYCollections; import org.key_project.util.java.SwingUtil; import org.slf4j.Logger; @@ -233,11 +236,11 @@ private void taskFinishedInternal(TaskFinishedInfo info) { KeYMediator mediator = mainWindow.getMediator(); mediator.getNotationInfo().refresh(mediator.getServices()); if (problemLoader.hasProofScript()) { - Pair scriptAndLoc; + KeyAst.ProofScriptEntry scriptAndLoc; try { scriptAndLoc = problemLoader.readProofScript(); ProofScriptWorker psw = new ProofScriptWorker(mainWindow.getMediator(), - scriptAndLoc.first, scriptAndLoc.second); + scriptAndLoc.code(), scriptAndLoc.getLocation()); psw.init(); psw.execute(); } catch (ProofInputException e) { @@ -404,6 +407,11 @@ public File 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); @@ -515,28 +523,47 @@ 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); - if (proofList != null) { - if (result != null) { - if ("".equals(result.getStatus())) { - this.resetStatus(this); - } else { - this.reportStatus(this, result.getStatus()); - } - if (result.hasErrors()) { - throw new ProblemLoaderException(loader, - "Proof could only be loaded partially.\n" + "In summary " - + result.getErrorList().size() - + " not loadable rule application(s) have been detected.\n" - + "The first one:\n" + result.getErrorList().get(0).getMessage(), - result.getErrorList().get(0)); - } + ProofAggregate proofList, ReplayResult result, Configuration settings) + throws ProblemLoaderException { + super.loadingFinished(loader, poContainer, proofList, result, settings); + if (proofList != null && result != null) { + if ("".equals(result.getStatus())) { + this.resetStatus(this); + } else { + this.reportStatus(this, result.getStatus()); + } + if (result.hasErrors()) { + throw new ProblemLoaderException(loader, + "Proof could only be loaded partially.\n" + "In summary " + + result.getErrorList().size() + + " not loadable rule application(s) have been detected.\n" + + "The first one:\n" + result.getErrorList().get(0).getMessage(), + result.getErrorList().get(0)); } } getMediator().resetNrGoalsClosedByHeuristics(); - if (poContainer != null && poContainer.getProofOblInput() instanceof KeYUserProblemFile) { - ((KeYUserProblemFile) poContainer.getProofOblInput()).close(); + if (settings != null) { + // TODO weigl not triggered + var addInfo = settings.getSection(ProofSettings.KEY_ADDITIONAL_DATA); + if (addInfo != null) { + var lastSelectedNodePath = + addInfo.getIntList(OutputStreamProofSaver.KEY_LAST_SELECTED_NODE); + if (lastSelectedNodePath != null && proofList != null) { + var proof = proofList.getFirstProof(); + var compressed = + lastSelectedNodePath.stream().mapToInt(Long::intValue).toArray(); + var path = KeYCollections.runLengthDecoding(compressed); + try { + var node = proof.root().traversePath(path); + getMediator().nonGoalNodeChosen(node); + } catch (ArrayIndexOutOfBoundsException e) { + LOGGER.warn( + "Invalid proof tree path detected in KeYUserProblemFile. Not able to select last" + + + " selected proof node."); + } + } + } } } diff --git a/key.ui/src/main/java/de/uka/ilkd/key/ui/ConsoleUserInterfaceControl.java b/key.ui/src/main/java/de/uka/ilkd/key/ui/ConsoleUserInterfaceControl.java index 1d80903ff68..e2bbe84657f 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/ui/ConsoleUserInterfaceControl.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/ui/ConsoleUserInterfaceControl.java @@ -20,7 +20,6 @@ import de.uka.ilkd.key.macros.ProofMacroFinishedInfo; import de.uka.ilkd.key.macros.SkipMacro; import de.uka.ilkd.key.macros.scripts.ProofScriptEngine; -import de.uka.ilkd.key.parser.Location; import de.uka.ilkd.key.proof.Goal; import de.uka.ilkd.key.proof.Proof; import de.uka.ilkd.key.proof.ProofAggregate; @@ -40,7 +39,6 @@ import de.uka.ilkd.key.rule.IBuiltInRuleApp; import de.uka.ilkd.key.speclang.PositionedString; import de.uka.ilkd.key.util.MiscTools; -import de.uka.ilkd.key.util.Pair; import org.key_project.util.collection.ImmutableList; import org.key_project.util.collection.ImmutableSLList; @@ -67,13 +65,13 @@ public class ConsoleUserInterfaceControl extends AbstractMediatorUserInterfaceCo int progressMax = 0; - // flag to indicate that a file should merely be loaded not proved. (for - // "reload" testing) + // flag to indicate that a file should merely be loaded isn't proved. + // (for "reload" testing) private final boolean loadOnly; /** - * Current key problem file that is attempted to be proven. + * The current key problem file that is attempted to be proven. */ private File keyProblemFile = null; @@ -114,7 +112,7 @@ private void printResults(final int openGoals, TaskFinishedInfo info, final Obje * It is assumed that this part of the code is never reached, unless a value has been * assigned to keyProblemFile in method loadProblem(File). */ - assert keyProblemFile != null : "Unexcpected null pointer. Trying to" + assert keyProblemFile != null : "Unexpected null pointer. Trying to" + " save a proof but no corresponding key problem file is " + "available."; allProofsSuccessful &= saveProof(result2, info.getProof(), keyProblemFile); /* @@ -159,12 +157,12 @@ public void taskFinished(TaskFinishedInfo info) { ProblemLoader problemLoader = (ProblemLoader) info.getSource(); if (problemLoader.hasProofScript()) { try { - Pair script = problemLoader.readProofScript(); - ProofScriptEngine pse = new ProofScriptEngine(script.first, script.second); + var script = problemLoader.readProofScript(); + ProofScriptEngine pse = new ProofScriptEngine(script.code(), script.getLocation()); this.taskStarted(new DefaultTaskStartedInfo(TaskKind.Macro, "Script started", 0)); pse.execute(this, proof); // The start and end messages are fake to persuade the system ... - // All this here should refactored anyway ... + // All this here should be refactored anyway ... this.taskFinished(new ProofMacroFinishedInfo(new SkipMacro(), proof)); } catch (Exception e) { LOGGER.debug("", e); @@ -192,8 +190,9 @@ public void taskStarted(TaskStartedInfo info) { @Override public void loadProblem(File file) { /* - * Current file is stored in a private field. It will be used in method printResults() to - * determine file names, in which proofs will be written. + * The current file is stored in a private field. + * It will be used in method printResults() to determine file names, in which proofs will be + * written. */ keyProblemFile = file; getProblemLoader(file, null, null, null, mediator).runSynchronously(); @@ -249,7 +248,7 @@ public final void progressStopped(Object sender) { @Override public final void reportException(Object sender, ProofOblInput input, Exception e) { - LOGGER.debug("ConsoleUserInterfaceControl.reportException({},{},{})", sender, input, e); + LOGGER.debug("ConsoleUserInterfaceControl.reportException({},{})", sender, input, e); } @Override @@ -295,7 +294,7 @@ public void completeAndApplyTacletMatch(TacletInstantiationModel[] models, Goal @Override public final void openExamples() { - LOGGER.info("Open Examples not suported by console UI."); + LOGGER.info("Open Examples not supported by console UI."); } @Override @@ -306,6 +305,7 @@ public final ProblemInitializer createProblemInitializer(Profile profile) { /** * {@inheritDoc} */ + @SuppressWarnings("StatementWithEmptyBody") @Override public void proofDisposing(ProofDisposedEvent e) { super.proofDisposing(e); @@ -316,7 +316,7 @@ public void proofDisposing(ProofDisposedEvent e) { mediator.getSelectionModel().setSelectedProof(proofStack.head()); } else { // proofStack might be empty, though proof != null. This can - // happen for symbolic execution tests, if proofCreated was not + // happen for symbolic execution tests if proofCreated was not // called by the test setup. } } @@ -363,7 +363,7 @@ public void reportWarnings(ImmutableSet warnings) { */ public static boolean saveProof(Object result, Proof proof, File keyProblemFile) { if (result instanceof Throwable) { - throw new RuntimeException("Error in batchmode.", (Throwable) result); + throw new RuntimeException("Error in batch mode.", (Throwable) result); } // Save the proof before exit. @@ -400,7 +400,7 @@ public static boolean saveProof(Object result, Proof proof, File keyProblemFile) } // Says true if all Proofs have succeeded, // or false if there is at least one open Proof - return proof.openGoals().size() == 0; + return proof.openGoals().isEmpty(); } @Override 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 d7e1e6fcc46..9ff072a5f18 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,17 +3,13 @@ * 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; /** * Utilities for Collections. * - * * @author Alexander Weigl * @version 1 (29.03.19) */ @@ -118,4 +114,115 @@ 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..f76b9b3e0e4 --- /dev/null +++ b/key.util/src/test/java/org/key_project/util/collection/KeYCollectionsTest.java @@ -0,0 +1,64 @@ +/* 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 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; + +/** + * @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 }); + } + + +}