diff --git a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/rule/AbstractSideProofRule.java b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/rule/AbstractSideProofRule.java index b4f25f305e1..e9178d692a2 100644 --- a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/rule/AbstractSideProofRule.java +++ b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/rule/AbstractSideProofRule.java @@ -6,7 +6,6 @@ import java.util.Deque; import java.util.LinkedList; import java.util.List; -import java.util.Set; import de.uka.ilkd.key.java.Services; import de.uka.ilkd.key.ldt.JavaDLTheory; @@ -18,14 +17,12 @@ import de.uka.ilkd.key.logic.Term; import de.uka.ilkd.key.logic.op.JFunction; import de.uka.ilkd.key.proof.Goal; -import de.uka.ilkd.key.proof.Node; import de.uka.ilkd.key.proof.Proof; import de.uka.ilkd.key.proof.init.ProofInputException; import de.uka.ilkd.key.proof.mgt.ProofEnvironment; import de.uka.ilkd.key.rule.BuiltInRule; import de.uka.ilkd.key.strategy.StrategyProperties; import de.uka.ilkd.key.symbolic_execution.util.SymbolicExecutionSideProofUtil; -import de.uka.ilkd.key.util.Triple; import org.key_project.logic.Name; import org.key_project.logic.sort.Sort; @@ -87,7 +84,7 @@ protected JFunction createResultFunction(Services services, Sort sort) { * @return The found result {@link Term} and the conditions. * @throws ProofInputException Occurred Exception. */ - protected List, Node>> computeResultsAndConditions(Services services, + protected List computeResultsAndConditions(Services services, Goal goal, ProofEnvironment sideProofEnvironment, Sequent sequentToProve, JFunction newPredicate) throws ProofInputException { return SymbolicExecutionSideProofUtil.computeResultsAndConditions(services, goal.proof(), @@ -134,4 +131,5 @@ protected static SequentFormula replace(PosInOccurrence pio, Term newTerm, Servi public boolean isApplicableOnSubTerms() { return false; } + } diff --git a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/rule/ModalitySideProofRule.java b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/rule/ModalitySideProofRule.java index 6c1fc13fb94..18f87c546f0 100644 --- a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/rule/ModalitySideProofRule.java +++ b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/rule/ModalitySideProofRule.java @@ -8,24 +8,13 @@ import java.util.Set; import de.uka.ilkd.key.java.Services; -import de.uka.ilkd.key.logic.PosInOccurrence; -import de.uka.ilkd.key.logic.Sequent; -import de.uka.ilkd.key.logic.SequentFormula; -import de.uka.ilkd.key.logic.Term; -import de.uka.ilkd.key.logic.TermBuilder; -import de.uka.ilkd.key.logic.TermServices; +import de.uka.ilkd.key.logic.*; import de.uka.ilkd.key.logic.op.*; import de.uka.ilkd.key.proof.Goal; -import de.uka.ilkd.key.proof.Node; import de.uka.ilkd.key.proof.mgt.ProofEnvironment; -import de.uka.ilkd.key.rule.BuiltInRule; -import de.uka.ilkd.key.rule.DefaultBuiltInRuleApp; -import de.uka.ilkd.key.rule.IBuiltInRuleApp; -import de.uka.ilkd.key.rule.RuleAbortException; -import de.uka.ilkd.key.rule.RuleApp; +import de.uka.ilkd.key.rule.*; import de.uka.ilkd.key.symbolic_execution.util.SymbolicExecutionSideProofUtil; import de.uka.ilkd.key.symbolic_execution.util.SymbolicExecutionUtil; -import de.uka.ilkd.key.util.Triple; import org.key_project.logic.Name; import org.key_project.util.collection.ImmutableArray; @@ -181,7 +170,7 @@ public IBuiltInRuleApp createApp(PosInOccurrence pos, TermServices services) { .addFormula(new SequentFormula(newModalityWithUpdatesTerm), false, false) .sequent(); // Compute results and their conditions - List, Node>> conditionsAndResultsMap = + List conditionsAndResultsMap = computeResultsAndConditions(services, goal, sideProofEnv, sequentToProve, newPredicate); // Create new single goal in which the query is replaced by the possible results @@ -190,10 +179,11 @@ public IBuiltInRuleApp createApp(PosInOccurrence pos, TermServices services) { resultGoal.removeFormula(pio); // Create results Set resultTerms = new LinkedHashSet<>(); - for (Triple, Node> conditionsAndResult : conditionsAndResultsMap) { - Term conditionTerm = tb.and(conditionsAndResult.second); - Term resultEqualityTerm = varFirst ? tb.equals(conditionsAndResult.first, otherTerm) - : tb.equals(otherTerm, conditionsAndResult.first); + for (ResultsAndCondition conditionsAndResult : conditionsAndResultsMap) { + Term conditionTerm = tb.and(conditionsAndResult.conditions()); + Term resultEqualityTerm = + varFirst ? tb.equals(conditionsAndResult.result(), otherTerm) + : tb.equals(otherTerm, conditionsAndResult.result()); Term resultTerm = pio.isInAntec() ? tb.imp(conditionTerm, resultEqualityTerm) : tb.and(conditionTerm, resultEqualityTerm); resultTerms.add(resultTerm); diff --git a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/rule/QuerySideProofRule.java b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/rule/QuerySideProofRule.java index 2f00a4a8941..a4bfda8eab7 100644 --- a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/rule/QuerySideProofRule.java +++ b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/rule/QuerySideProofRule.java @@ -4,7 +4,6 @@ package de.uka.ilkd.key.symbolic_execution.rule; import java.util.List; -import java.util.Set; import de.uka.ilkd.key.java.Services; import de.uka.ilkd.key.logic.PIOPathIterator; @@ -16,7 +15,6 @@ import de.uka.ilkd.key.logic.TermServices; import de.uka.ilkd.key.logic.op.*; import de.uka.ilkd.key.proof.Goal; -import de.uka.ilkd.key.proof.Node; import de.uka.ilkd.key.proof.mgt.ProofEnvironment; import de.uka.ilkd.key.rule.BuiltInRule; import de.uka.ilkd.key.rule.DefaultBuiltInRuleApp; @@ -25,7 +23,6 @@ import de.uka.ilkd.key.rule.RuleAbortException; import de.uka.ilkd.key.rule.RuleApp; import de.uka.ilkd.key.symbolic_execution.util.SymbolicExecutionSideProofUtil; -import de.uka.ilkd.key.util.Triple; import org.key_project.logic.Name; import org.key_project.logic.sort.Sort; @@ -228,7 +225,7 @@ public IBuiltInRuleApp createApp(PosInOccurrence pos, TermServices services) { sequentToProve = sequentToProve.addFormula(new SequentFormula(newTerm), false, false).sequent(); // Compute results and their conditions - List, Node>> conditionsAndResultsMap = + List conditionsAndResultsMap = computeResultsAndConditions(services, goal, sideProofEnv, sequentToProve, newPredicate); // Create new single goal in which the query is replaced by the possible results @@ -237,10 +234,11 @@ public IBuiltInRuleApp createApp(PosInOccurrence pos, TermServices services) { final TermBuilder tb = services.getTermBuilder(); resultGoal.removeFormula(pio); if (pio.isTopLevel() || queryConditionTerm != null) { - for (Triple, Node> conditionsAndResult : conditionsAndResultsMap) { - Term conditionTerm = tb.and(conditionsAndResult.second); - Term newEqualityTerm = varFirst ? tb.equals(varTerm, conditionsAndResult.first) - : tb.equals(conditionsAndResult.first, varTerm); + for (ResultsAndCondition conditionsAndResult : conditionsAndResultsMap) { + Term conditionTerm = tb.and(conditionsAndResult.conditions()); + Term newEqualityTerm = + varFirst ? tb.equals(varTerm, conditionsAndResult.result()) + : tb.equals(conditionsAndResult.result(), varTerm); Term resultTerm = pio.isInAntec() ? tb.imp(conditionTerm, newEqualityTerm) : tb.and(conditionTerm, newEqualityTerm); if (queryConditionTerm != null) { @@ -256,11 +254,11 @@ public IBuiltInRuleApp createApp(PosInOccurrence pos, TermServices services) { tb.equals(resultFunctionTerm, varTerm), services), pio.isInAntec(), false); - for (Triple, Node> conditionsAndResult : conditionsAndResultsMap) { - Term conditionTerm = tb.and(conditionsAndResult.second); + for (ResultsAndCondition conditionsAndResult : conditionsAndResultsMap) { + Term conditionTerm = tb.and(conditionsAndResult.conditions()); Term resultTerm = tb.imp(conditionTerm, - varFirst ? tb.equals(resultFunctionTerm, conditionsAndResult.first) - : tb.equals(conditionsAndResult.first, resultFunctionTerm)); + varFirst ? tb.equals(resultFunctionTerm, conditionsAndResult.result()) + : tb.equals(conditionsAndResult.result(), resultFunctionTerm)); resultGoal.addFormula(new SequentFormula(resultTerm), true, false); } } diff --git a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/rule/ResultsAndCondition.java b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/rule/ResultsAndCondition.java new file mode 100644 index 00000000000..9a14b9852cb --- /dev/null +++ b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/rule/ResultsAndCondition.java @@ -0,0 +1,19 @@ +/* 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 de.uka.ilkd.key.symbolic_execution.rule; + +import java.util.Set; + +import de.uka.ilkd.key.logic.Term; +import de.uka.ilkd.key.proof.Node; + +/** + * The return value of a side proof. + * + * @param result a term representing the result (first formula of succedent) + * @param conditions formulas of the antecedent + * @param node the final node of the side proof + */ +public record ResultsAndCondition(Term result, Set conditions, Node node) { +} diff --git a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/util/SymbolicExecutionSideProofUtil.java b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/util/SymbolicExecutionSideProofUtil.java index 766547c958c..079bf2aed6b 100644 --- a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/util/SymbolicExecutionSideProofUtil.java +++ b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/util/SymbolicExecutionSideProofUtil.java @@ -32,9 +32,9 @@ import de.uka.ilkd.key.strategy.StrategyProperties; import de.uka.ilkd.key.symbolic_execution.profile.SimplifyTermProfile; import de.uka.ilkd.key.symbolic_execution.profile.SymbolicExecutionJavaProfile; +import de.uka.ilkd.key.symbolic_execution.rule.ResultsAndCondition; import de.uka.ilkd.key.util.ProofStarter; import de.uka.ilkd.key.util.SideProofUtil; -import de.uka.ilkd.key.util.Triple; import org.key_project.logic.Name; import org.key_project.util.collection.ImmutableArray; @@ -169,7 +169,8 @@ public static List> computeResults(Services services, Proof pro * @return The found result {@link Term} and the conditions. * @throws ProofInputException Occurred Exception. */ - public static List, Node>> computeResultsAndConditions(Services services, + public static List computeResultsAndConditions( + Services services, Proof proof, ProofEnvironment sideProofEnvironment, Sequent sequentToProve, Operator operator, String description, String methodTreatment, String loopTreatment, String queryTreatment, String splittingOption, boolean addNamesToServices) @@ -182,8 +183,7 @@ public static List, Node>> computeResultsAndConditions(Se Set relevantThingsInSequentToProve = extractRelevantThings(info.getProof().getServices(), sequentToProve); // Extract results and conditions from side proof - List, Node>> conditionsAndResultsMap = - new LinkedList<>(); + List conditionsAndResultsMap = new LinkedList<>(); for (Goal resultGoal : info.getProof().openGoals()) { if (SymbolicExecutionUtil.hasApplicableRules(resultGoal)) { throw new IllegalStateException("Not all applicable rules are applied."); @@ -245,8 +245,8 @@ public static List, Node>> computeResultsAndConditions(Se if (result == null) { result = services.getTermBuilder().ff(); } - conditionsAndResultsMap.add( - new Triple<>(result, resultConditions, resultGoal.node())); + conditionsAndResultsMap + .add(new ResultsAndCondition(result, resultConditions, resultGoal.node())); } return conditionsAndResultsMap; } finally { @@ -303,14 +303,11 @@ public static void addNewNamesToNamespace(Services services, Term term) { final Namespace functions = services.getNamespaces().functions(); final Namespace progVars = services.getNamespaces().programVariables(); // LogicVariables are always local bound - term.execPreOrder(new DefaultVisitor() { - @Override - public void visit(Term visited) { - if (visited.op() instanceof JFunction) { - functions.add((JFunction) visited.op()); - } else if (visited.op() instanceof IProgramVariable) { - progVars.add((IProgramVariable) visited.op()); - } + term.execPreOrder((DefaultVisitor) visited -> { + if (visited.op() instanceof JFunction) { + functions.add((JFunction) visited.op()); + } else if (visited.op() instanceof IProgramVariable) { + progVars.add((IProgramVariable) visited.op()); } }); } @@ -385,12 +382,9 @@ public static Set extractRelevantThings(final Services services, Sequent sequentToProve) { final Set result = new HashSet<>(); for (SequentFormula sf : sequentToProve) { - sf.formula().execPreOrder(new DefaultVisitor() { - @Override - public void visit(Term visited) { - if (isRelevantThing(services, visited)) { - result.add(visited.op()); - } + sf.formula().execPreOrder((DefaultVisitor) visited -> { + if (isRelevantThing(services, visited)) { + result.add(visited.op()); } }); } 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 7e502b50096..bc34b6eaf8a 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.ProofScriptEntry; import de.uka.ilkd.key.proof.Proof; import de.uka.ilkd.key.proof.init.InitConfig; import de.uka.ilkd.key.proof.init.Profile; @@ -21,7 +21,7 @@ import de.uka.ilkd.key.proof.io.ProblemLoaderException; import de.uka.ilkd.key.proof.mgt.SpecificationRepository; -import org.key_project.util.collection.Pair; +import org.jspecify.annotations.Nullable; /** * Instances of this class are used to collect and access all relevant information for verification @@ -48,7 +48,7 @@ public class KeYEnvironment { /** * An optional field denoting a script contained in the proof file. */ - private final Pair proofScript; + private final @Nullable ProofScriptEntry proofScript; /** * Indicates that this {@link KeYEnvironment} is disposed. @@ -77,7 +77,7 @@ public KeYEnvironment(U ui, InitConfig initConfig) { * @param initConfig The loaded project. */ public KeYEnvironment(U ui, InitConfig initConfig, Proof loadedProof, - Pair proofScript, ReplayResult replayResult) { + @Nullable ProofScriptEntry proofScript, ReplayResult replayResult) { this.ui = ui; this.initConfig = initConfig; this.loadedProof = loadedProof; @@ -317,7 +317,7 @@ public boolean isDisposed() { return disposed; } - public Pair getProofScript() { + public @Nullable ProofScriptEntry getProofScript() { return proofScript; } } 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 9eb702a8327..095e3ca921a 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,9 +3,11 @@ * 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; @@ -15,7 +17,6 @@ import de.uka.ilkd.key.settings.Configuration; import de.uka.ilkd.key.settings.ProofSettings; import de.uka.ilkd.key.speclang.njml.JmlParser; -import de.uka.ilkd.key.util.Triple; import org.key_project.util.java.StringUtil; @@ -84,12 +85,24 @@ public static class File extends KeyAst { return settings; } - public @Nullable Triple findProofScript() { + /** + * Returns the a {@link ProofScriptEntry} from the underlying AST if an {@code \proofscript} + * entry is present. + * The {@code url} is used as the source of input and might be later used for error message, + * or including + * other files. + * + * @param url location pointing to the source of the AST + * @return a {@link ProofScriptEntry} if {@code \proofscript} is present + */ + public @Nullable ProofScriptEntry findProofScript(URI url) { if (ctx.problem() != null && ctx.problem().proofScript() != null) { KeYParser.ProofScriptContext pctx = ctx.problem().proofScript(); + Location location = new Location(url, + Position.newOneBased(pctx.ps.getLine(), pctx.ps.getCharPositionInLine())); + String text = pctx.ps.getText(); - return new Triple<>(StringUtil.trim(text, '"'), pctx.ps.getLine(), - pctx.ps.getCharPositionInLine()); + return new ProofScriptEntry(StringUtil.trim(text, '"'), location); } return null; } diff --git a/key.core/src/main/java/de/uka/ilkd/key/nparser/ProofScriptEntry.java b/key.core/src/main/java/de/uka/ilkd/key/nparser/ProofScriptEntry.java new file mode 100644 index 00000000000..18120539a39 --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/nparser/ProofScriptEntry.java @@ -0,0 +1,19 @@ +/* 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 de.uka.ilkd.key.nparser; + +import de.uka.ilkd.key.parser.Location; + +import org.jspecify.annotations.NonNull; + +/** + * This struct encapsulate the information of a proofscript found in key files. + * + * @param script the content of the script + * @param location location of the content + * @author Alexander Weigl + * @version 1 (23.04.24) + */ +public record ProofScriptEntry(@NonNull String script, @NonNull Location location) { +} 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 cd394dee308..2cd7f1a89da 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 @@ -5,14 +5,12 @@ import java.io.File; import java.io.IOException; +import java.net.URI; import java.net.URISyntaxException; import de.uka.ilkd.key.java.abstraction.KeYJavaType; import de.uka.ilkd.key.logic.Sequent; -import de.uka.ilkd.key.nparser.ChoiceInformation; -import de.uka.ilkd.key.nparser.KeyAst; -import de.uka.ilkd.key.nparser.ProblemInformation; -import de.uka.ilkd.key.nparser.ProofReplayer; +import de.uka.ilkd.key.nparser.*; import de.uka.ilkd.key.proof.Proof; import de.uka.ilkd.key.proof.ProofAggregate; import de.uka.ilkd.key.proof.io.IProofFileParser; @@ -23,7 +21,6 @@ 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; @@ -31,6 +28,7 @@ import org.antlr.v4.runtime.CharStream; import org.antlr.v4.runtime.Token; import org.jspecify.annotations.NonNull; +import org.jspecify.annotations.Nullable; /** @@ -174,12 +172,24 @@ public boolean implies(ProofOblInput po) { } + /** + * True iff a {@link ProofScriptEntry} is present + * + * @see #readProofScript() + */ public boolean hasProofScript() { - return getParseContext().findProofScript() != null; + return readProofScript() != null; } - public Triple readProofScript() { - return getParseContext().findProofScript(); + /** + * Returns the {@link ProofScriptEntry} in this resource + * + * @return {@link ProofScriptEntry} if present otherwise null + * @see KeyAst.File#findProofScript(URI) + */ + public @Nullable ProofScriptEntry readProofScript() { + URI url = getInitialFile().toURI(); + return getParseContext().findProofScript(url); } /** 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 84cdbaf5706..a7d6c940c57 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 @@ -6,7 +6,6 @@ import java.io.File; import java.io.FileNotFoundException; import java.io.IOException; -import java.net.URI; import java.nio.file.*; import java.util.*; import java.util.function.Consumer; @@ -14,10 +13,9 @@ 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.ProofScriptEntry; import de.uka.ilkd.key.proof.Node; import de.uka.ilkd.key.proof.Proof; import de.uka.ilkd.key.proof.ProofAggregate; @@ -36,12 +34,12 @@ import de.uka.ilkd.key.strategy.Strategy; import de.uka.ilkd.key.strategy.StrategyProperties; import de.uka.ilkd.key.util.ExceptionHandlerException; -import de.uka.ilkd.key.util.Triple; import org.key_project.util.collection.Pair; import org.key_project.util.java.IOUtil; import org.antlr.runtime.MismatchedTokenException; +import org.jspecify.annotations.Nullable; import org.slf4j.Logger; import org.slf4j.LoggerFactory; @@ -262,7 +260,6 @@ public final void load() throws Exception { * * @param callbackProofLoaded optional callback, called when the proof is loaded but not yet * replayed - * * @throws ProofInputException Occurred Exception. * @throws IOException Occurred Exception. * @throws ProblemLoaderException Occurred Exception. @@ -661,27 +658,15 @@ public boolean hasProofScript() { return false; } - public Pair 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); - } - - public Pair getProofScript() throws ProblemLoaderException { - if (hasProofScript()) { - try { - return readProofScript(); - } catch (ProofInputException e) { - throw new ProblemLoaderException(this, e); - } - } else { + /** + * Returns a {@link ProofScriptEntry} if {@code \proofscript} is given with the problem. + */ + public @Nullable ProofScriptEntry getProofScript() { + if (!hasProofScript()) { return null; } + KeYUserProblemFile kupf = (KeYUserProblemFile) envInput; + return kupf.readProofScript(); } private ReplayResult replayProof(Proof proof) { diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/io/IntermediateProofReplayer.java b/key.core/src/main/java/de/uka/ilkd/key/proof/io/IntermediateProofReplayer.java index b40ef0409c1..7dce2562e06 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/io/IntermediateProofReplayer.java +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/io/IntermediateProofReplayer.java @@ -48,8 +48,8 @@ import de.uka.ilkd.key.speclang.Contract; import de.uka.ilkd.key.speclang.OperationContract; import de.uka.ilkd.key.util.ProgressMonitor; -import de.uka.ilkd.key.util.Triple; import de.uka.ilkd.key.util.mergerule.MergeRuleUtils; +import de.uka.ilkd.key.util.mergerule.SymbolicExecutionStateWithProgCnt; import org.key_project.logic.Name; import org.key_project.logic.Named; @@ -112,9 +112,18 @@ public class IntermediateProofReplayer { private final LinkedList> queue = new LinkedList<>(); + /** + * Used by the node merging during the proof replay. + * + * @param node the other node to be merged with + * @param pio pio of ??? (ask Dominic Steinhöfel) + * @param intermediate representation of the node during the replay + * @see MergePartnerAppIntermediate + */ + private record PartnerNode(Node node, PosInOccurrence pio, NodeIntermediate intermediate) {} + /** Maps join node IDs to previously seen join partners */ - private final HashMap>> joinPartnerNodes = - new HashMap<>(); + private final HashMap> joinPartnerNodes = new HashMap<>(); /** The current open goal */ private Goal currGoal = null; @@ -264,7 +273,7 @@ public Result replay(ProblemInitializer.ProblemInitializerListener listener, (BuiltInAppIntermediate) currInterm.getIntermediateRuleApp(); if (appInterm instanceof MergeAppIntermediate joinAppInterm) { - HashSet> partnerNodesInfo = + HashSet partnerNodesInfo = joinPartnerNodes.get(((MergeAppIntermediate) appInterm).getId()); if (partnerNodesInfo == null @@ -309,11 +318,11 @@ public Result replay(ProblemInitializer.ProblemInitializerListener listener, } // Now add children of partner nodes - for (Triple partnerNodeInfo : partnerNodesInfo) { + for (PartnerNode partnerNodeInfo : partnerNodesInfo) { Iterator children = - partnerNodeInfo.first.childrenIterator(); + partnerNodeInfo.node.childrenIterator(); LinkedList intermChildren = - partnerNodeInfo.third.getChildren(); + partnerNodeInfo.intermediate.getChildren(); addChildren(children, intermChildren); } @@ -327,11 +336,11 @@ public Result replay(ProblemInitializer.ProblemInitializerListener listener, } } else if (appInterm instanceof MergePartnerAppIntermediate joinPartnerApp) { // Register this partner node - HashSet> partnerNodeInfo = + HashSet partnerNodeInfo = joinPartnerNodes.computeIfAbsent(joinPartnerApp.getMergeNodeId(), k -> new HashSet<>()); - partnerNodeInfo.add(new Triple<>( + partnerNodeInfo.add(new PartnerNode( currNode, PosInOccurrence.findInSequent(currGoal.sequent(), appInterm.getPosInfo().first, appInterm.getPosInfo().second), @@ -713,7 +722,7 @@ private IBuiltInRuleApp constructBuiltinApp(BuiltInAppIntermediate currInterm, G */ private MergeRuleBuiltInRuleApp instantiateJoinApp(final MergeAppIntermediate joinAppInterm, final Node currNode, - final Set> partnerNodesInfo, + final HashSet partnerNodesInfo, final Services services) throws SkipSMTRuleException, BuiltInConstructionException { final MergeRuleBuiltInRuleApp joinApp = (MergeRuleBuiltInRuleApp) constructBuiltinApp(joinAppInterm, currGoal); @@ -802,18 +811,18 @@ private MergeRuleBuiltInRuleApp instantiateJoinApp(final MergeAppIntermediate jo } ImmutableList joinPartners = ImmutableSLList.nil(); - for (Triple partnerNodeInfo : partnerNodesInfo) { + for (PartnerNode partnerNodeInfo : partnerNodesInfo) { - final Triple ownSEState = + SymbolicExecutionStateWithProgCnt ownSEState = sequentToSETriple(currNode, joinApp.posInOccurrence(), services); - final Triple partnerSEState = - sequentToSETriple(partnerNodeInfo.first, partnerNodeInfo.second, services); + var partnerSEState = + sequentToSETriple(partnerNodeInfo.node, partnerNodeInfo.pio, services); - assert ownSEState.third.equals(partnerSEState.third) + assert ownSEState.programCounter().equals(partnerSEState.programCounter()) : "Cannot merge incompatible program counters"; joinPartners = joinPartners.append( - new MergePartner(proof.getOpenGoal(partnerNodeInfo.first), partnerNodeInfo.second)); + new MergePartner(proof.getOpenGoal(partnerNodeInfo.node), partnerNodeInfo.pio)); } joinApp.setMergeNode(currNode); diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/mgt/ProofCorrectnessMgt.java b/key.core/src/main/java/de/uka/ilkd/key/proof/mgt/ProofCorrectnessMgt.java index 9e6b585c458..5a56e9992d1 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/mgt/ProofCorrectnessMgt.java +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/mgt/ProofCorrectnessMgt.java @@ -266,14 +266,6 @@ public ProofStatus getStatus() { return proofStatus; } - @Override - protected void finalize() throws Throwable { - removeProofListener(); - super.finalize(); - } - - - // ------------------------------------------------------------------------- // inner classes // ------------------------------------------------------------------------- diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/mgt/SpecificationRepository.java b/key.core/src/main/java/de/uka/ilkd/key/proof/mgt/SpecificationRepository.java index ac8404f0b4e..95b4a37b93d 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/mgt/SpecificationRepository.java +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/mgt/SpecificationRepository.java @@ -34,15 +34,10 @@ import de.uka.ilkd.key.speclang.jml.translation.ProgramVariableCollection; import de.uka.ilkd.key.speclang.translation.SLTranslationException; import de.uka.ilkd.key.util.MiscTools; -import de.uka.ilkd.key.util.Triple; import org.key_project.logic.Name; import org.key_project.logic.sort.Sort; -import org.key_project.util.collection.DefaultImmutableSet; -import org.key_project.util.collection.ImmutableList; -import org.key_project.util.collection.ImmutableSLList; -import org.key_project.util.collection.ImmutableSet; -import org.key_project.util.collection.Pair; +import org.key_project.util.collection.*; import org.jspecify.annotations.Nullable; import org.slf4j.Logger; @@ -83,10 +78,11 @@ public final class SpecificationRepository { private final Map> proofs = new LinkedHashMap<>(); private final Map, LoopSpecification> loopInvs = new LinkedHashMap<>(); - private final Map, ImmutableSet> blockContracts = + private final Map> blockContracts = new LinkedHashMap<>(); - private final Map, ImmutableSet> loopContracts = + private final Map> loopContracts = new LinkedHashMap<>(); + /** * A map which relates each loop statement its starting line number and set of loop contracts. */ @@ -1493,8 +1489,8 @@ public void addLoopInvariant(final LoopSpecification inv) { * @return all block contracts for the specified block. */ public ImmutableSet getBlockContracts(StatementBlock block) { - final Triple b = - new Triple<>(block, block.getParentClass(), block.getStartPosition().line()); + var b = + new BlockContractKey(block, block.getParentClass(), block.getStartPosition().line()); final ImmutableSet contracts = blockContracts.get(b); if (contracts == null) { return DefaultImmutableSet.nil(); @@ -1510,8 +1506,7 @@ public ImmutableSet getBlockContracts(StatementBlock block) { * @return all loop contracts for the specified block. */ public ImmutableSet getLoopContracts(StatementBlock block) { - final Triple b = - new Triple<>(block, block.getParentClass(), block.getStartPosition().line()); + var b = new LoopContractKey(block, block.getParentClass(), block.getStartPosition().line()); final ImmutableSet contracts = loopContracts.get(b); if (contracts == null) { return DefaultImmutableSet.nil(); @@ -1615,8 +1610,8 @@ public void addBlockContract(final BlockContract contract) { */ public void addBlockContract(final BlockContract contract, boolean addFunctionalContract) { final StatementBlock block = contract.getBlock(); - final Triple b = - new Triple<>(block, block.getParentClass(), block.getStartPosition().line()); + var b = + new BlockContractKey(block, block.getParentClass(), block.getStartPosition().line()); blockContracts.put(b, getBlockContracts(block).add(contract)); if (addFunctionalContract) { @@ -1637,11 +1632,10 @@ public void addBlockContract(final BlockContract contract, boolean addFunctional */ public void removeBlockContract(final BlockContract contract) { final StatementBlock block = contract.getBlock(); - final Triple b = - new Triple<>(block, block.getParentClass(), block.getStartPosition().line()); + var b = + new BlockContractKey(block, block.getParentClass(), block.getStartPosition().line()); - ImmutableSet set = blockContracts.get(b); - blockContracts.put(b, set.remove(contract)); + blockContracts.compute(b, (k, set) -> set.remove(contract)); } /** @@ -1663,8 +1657,8 @@ public void addLoopContract(final LoopContract contract) { public void addLoopContract(final LoopContract contract, boolean addFunctionalContract) { if (contract.isOnBlock()) { final StatementBlock block = contract.getBlock(); - final Triple b = - new Triple<>(block, block.getParentClass(), block.getStartPosition().line()); + var b = + new LoopContractKey(block, block.getParentClass(), block.getStartPosition().line()); loopContracts.put(b, getLoopContracts(block).add(contract)); } else { final LoopStatement loop = contract.getLoop(); @@ -1696,18 +1690,16 @@ public void addLoopContract(final LoopContract contract, boolean addFunctionalCo public void removeLoopContract(final LoopContract contract) { if (contract.isOnBlock()) { final StatementBlock block = contract.getBlock(); - final Triple b = - new Triple<>(block, block.getParentClass(), block.getStartPosition().line()); + var b = + new LoopContractKey(block, block.getParentClass(), block.getStartPosition().line()); - ImmutableSet set = loopContracts.get(b); - loopContracts.put(b, set.remove(contract)); + loopContracts.compute(b, (k, set) -> set.remove(contract)); } else { final LoopStatement loop = contract.getLoop(); final Pair b = new Pair<>(loop, loop.getStartPosition().line()); - ImmutableSet set = loopContractsOnLoops.get(b); - loopContractsOnLoops.put(b, set.remove(contract)); + loopContractsOnLoops.compute(b, (k, set) -> set.remove(contract)); } } @@ -1889,7 +1881,7 @@ public JmlStatementSpec addStatementSpec(Statement statement, JmlStatementSpec s public record JmlStatementSpec( ProgramVariableCollection vars, ImmutableList terms - ){ + ) { /** * Retrieve a term * @param index a index to the list of {@code terms}. @@ -1943,5 +1935,11 @@ public JmlStatementSpec updateVariables(Map atPres, Serv newTerms); } } + + private record BlockContractKey(StatementBlock block, URI file, Integer pos) { + } + + private record LoopContractKey(StatementBlock block, URI file, Integer pos) { + } // endregion } diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/WhileInvariantRule.java b/key.core/src/main/java/de/uka/ilkd/key/rule/WhileInvariantRule.java index 4ed438b1b8a..217965523f0 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/WhileInvariantRule.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/WhileInvariantRule.java @@ -52,7 +52,6 @@ import de.uka.ilkd.key.speclang.LoopWellDefinedness; import de.uka.ilkd.key.speclang.WellDefinednessCheck; import de.uka.ilkd.key.util.MiscTools; -import de.uka.ilkd.key.util.Triple; import org.key_project.logic.Name; import org.key_project.util.collection.ImmutableArray; @@ -163,10 +162,9 @@ private static InfFlowData prepareSetUpOfInfFlowValidityGoal(final Goal infFlowG final Taclet informationFlowInvariantApp = ifInvariantBuilder.buildTaclet(infFlowGoal); // return information flow data - InfFlowData infFlowData = new InfFlowData(instantiationVars, guardAtPre, guardAtPost, + return new InfFlowData(instantiationVars, guardAtPre, guardAtPost, guardJb, guardTerm, localOutTerms, localOutsAtPre, localOutsAtPost, updates, loopInvApplPredTerm, informationFlowInvariantApp); - return infFlowData; } @@ -221,9 +219,7 @@ private static Instantiation instantiate(final LoopInvariantBuiltInRuleApp app, services.getSpecificationRepository().addLoopInvariant(spec); // cache and return result - final Instantiation result = - new Instantiation(u, progPost, loop, spec, selfTerm, innermostExecutionContext); - return result; + return new Instantiation(u, progPost, loop, spec, selfTerm, innermostExecutionContext); } private static Term createLocalAnonUpdate(ImmutableSet localOuts, @@ -294,8 +290,7 @@ private static Term buildAtPostVar(Term varTerm, String suffix, Services service final LocationVariable varAtPostVar = new LocationVariable(new ProgramElementName(name), resultType); register(varAtPostVar, services); - final Term varAtPost = tb.var(varAtPostVar); - return varAtPost; + return tb.var(varAtPostVar); } private static Term buildBeforeVar(Term varTerm, Services services) { @@ -310,8 +305,7 @@ private static Term buildBeforeVar(Term varTerm, Services services) { final LocationVariable varAtPreVar = new LocationVariable(new ProgramElementName(name), resultType); register(varAtPreVar, services); - final Term varAtPre = tb.var(varAtPreVar); - return varAtPre; + return tb.var(varAtPreVar); } private static Term buildAfterVar(Term varTerm, Services services) { @@ -326,8 +320,7 @@ private static Term buildAfterVar(Term varTerm, Services services) { final LocationVariable varAtPostVar = new LocationVariable(new ProgramElementName(name), resultType); register(varAtPostVar, services); - final Term varAtPost = tb.var(varAtPostVar); - return varAtPost; + return tb.var(varAtPostVar); } private static ImmutableList buildLocalOutsAtPre(ImmutableList varTerms, @@ -540,8 +533,7 @@ private Term bodyTerm(TermLabelState termLabelState, Services services, RuleApp this, bodyGoal, FULL_INVARIANT_TERM_HINT, null); Term bodyTerm = wir.transform(termLabelState, this, ruleApp, bodyGoal, applicationSequent, ruleApp.posInOccurrence(), inst.progPost, fullInvariant, svInst, services); - final Term guardTrueBody = tb.imp(tb.box(guardJb, guardTrueTerm), bodyTerm); - return guardTrueBody; + return tb.imp(tb.box(guardJb, guardTrueTerm), bodyTerm); } @@ -569,11 +561,10 @@ private Term useCaseFormula(TermLabelState termLabelState, Services services, Ru Term restPsi = tb.prog(modality.kind(), useJavaBlock, inst.progPost.sub(0), instantiateLabels); - Term guardFalseRestPsi = tb.box(guardJb, tb.imp(guardFalseTerm, restPsi)); - return guardFalseRestPsi; + return tb.box(guardJb, tb.imp(guardFalseTerm, restPsi)); } - private Triple prepareGuard(final Instantiation inst, + private Guard prepareGuard(final Instantiation inst, final KeYJavaType booleanKJT, LoopInvariantBuiltInRuleApp loopRuleApp, final TermServices services) { final TermBuilder tb = services.getTermBuilder(); @@ -592,9 +583,18 @@ private Triple prepareGuard(final Instantiation inst, JavaBlock.createJavaBlock(new StatementBlock(guardVarMethodFrame)); final Term guardTrueTerm = tb.equals(tb.var(guardVar), tb.TRUE()); final Term guardFalseTerm = tb.equals(tb.var(guardVar), tb.FALSE()); - return new Triple<>(guardJb, guardTrueTerm, guardFalseTerm); + return new Guard(guardJb, guardTrueTerm, guardFalseTerm); } + /** + * Represents a {@code javaBlock} which is executed if the {@code trueTerm} is true. + * + * @param javaBlock a block of java code + * @param trueTerm a boolean term + * @param falseTerm the negation (at least semantically) of {@code trueTerm} + */ + private record Guard(JavaBlock javaBlock, Term trueTerm, Term falseTerm) {} + private void prepareInvInitiallyValidBranch(TermLabelState termLabelState, Services services, RuleApp ruleApp, Instantiation inst, final Term invTerm, Term reachableState, Goal initGoal) { @@ -752,11 +752,11 @@ private void setupWdGoal(final Goal goal, final LoopSpecification inv, final Ter final Term variantPO = variantPair.second; // prepare guard - final Triple guardStuff = + final Guard guardStuff = prepareGuard(inst, booleanKJT, loopRuleApp, services); - final JavaBlock guardJb = guardStuff.first; - final Term guardTrueTerm = guardStuff.second; - final Term guardFalseTerm = guardStuff.third; + final JavaBlock guardJb = guardStuff.javaBlock; + final Term guardTrueTerm = guardStuff.trueTerm; + final Term guardFalseTerm = guardStuff.falseTerm; Term beforeLoopUpdate = null; @@ -995,48 +995,39 @@ public AnonUpdateData(Term anonUpdate, Term loopHeap, Term loopHeapAtPre, Term a } } - private static final class InfFlowData { - public final ProofObligationVars symbExecVars; - public final Term guardAtPre; - public final Term guardAtPost; - public final JavaBlock guardJb; - public final Term guardTerm; - public final ImmutableList localOuts; - public final ImmutableList localOutsAtPre; - public final ImmutableList localOutsAtPost; - public final Pair updates; - public final Term applPredTerm; - public final Taclet infFlowApp; - - private InfFlowData(ProofObligationVars symbExecVars, Term guardAtPre, Term guardAtPost, - JavaBlock guardJb, Term guardTerm, ImmutableList localOuts, - ImmutableList localOutsAtPre, ImmutableList localOutsAtPost, - Pair updates, Term applPredTerm, Taclet infFlowApp) { - this.symbExecVars = symbExecVars; - this.guardAtPre = guardAtPre; - this.guardAtPost = guardAtPost; - this.guardJb = guardJb; - this.guardTerm = guardTerm; - this.localOuts = localOuts; - this.localOutsAtPre = localOutsAtPre; - this.localOutsAtPost = localOutsAtPost; - this.updates = updates; - this.infFlowApp = infFlowApp; - this.applPredTerm = applPredTerm; - - assert symbExecVars != null; - assert guardAtPre != null; - assert guardAtPost != null; - assert guardJb != null; - assert guardTerm != null; - assert localOuts != null; - assert localOutsAtPre != null; - assert localOutsAtPost != null; - assert updates != null; - assert applPredTerm != null; - assert infFlowApp != null; + private record InfFlowData(ProofObligationVars symbExecVars, Term guardAtPre, Term guardAtPost, JavaBlock guardJb, + Term guardTerm, ImmutableList localOuts, ImmutableList localOutsAtPre, + ImmutableList localOutsAtPost, Pair updates, Term applPredTerm, + Taclet infFlowApp) { + private InfFlowData(ProofObligationVars symbExecVars, Term guardAtPre, Term guardAtPost, + JavaBlock guardJb, Term guardTerm, ImmutableList localOuts, + ImmutableList localOutsAtPre, ImmutableList localOutsAtPost, + Pair updates, Term applPredTerm, Taclet infFlowApp) { + this.symbExecVars = symbExecVars; + this.guardAtPre = guardAtPre; + this.guardAtPost = guardAtPost; + this.guardJb = guardJb; + this.guardTerm = guardTerm; + this.localOuts = localOuts; + this.localOutsAtPre = localOutsAtPre; + this.localOutsAtPost = localOutsAtPost; + this.updates = updates; + this.infFlowApp = infFlowApp; + this.applPredTerm = applPredTerm; + + assert symbExecVars != null; + assert guardAtPre != null; + assert guardAtPost != null; + assert guardJb != null; + assert guardTerm != null; + assert localOuts != null; + assert localOutsAtPre != null; + assert localOutsAtPost != null; + assert updates != null; + assert applPredTerm != null; + assert infFlowApp != null; + } } - } /** * {@inheritDoc} diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/merge/MergeRule.java b/key.core/src/main/java/de/uka/ilkd/key/rule/merge/MergeRule.java index 3fb35b67e79..b7a0cd56ab4 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/merge/MergeRule.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/merge/MergeRule.java @@ -32,7 +32,6 @@ import de.uka.ilkd.key.rule.merge.procedures.MergeTotalWeakening; import de.uka.ilkd.key.rule.merge.procedures.MergeWithLatticeAbstraction; import de.uka.ilkd.key.rule.merge.procedures.MergeWithPredicateAbstraction; -import de.uka.ilkd.key.util.Triple; import de.uka.ilkd.key.util.mergerule.MergeRuleUtils; import de.uka.ilkd.key.util.mergerule.SymbolicExecutionState; import de.uka.ilkd.key.util.mergerule.SymbolicExecutionStateWithProgCnt; @@ -63,16 +62,15 @@ * Base for implementing merge rules. Extend this class, implement method mergeValuesInStates(...) * and register in class JavaProfile. *

- * + *

* The rule is applicable if the chosen subterm has the form { x := v || ... } PHI and there are * potential merge candidates. *

- * + *

* Any rule application returned will be incomplete; completion is handled by * de.uka.ilkd.key.gui.mergerule.MergeRuleCompletion. * * @author Dominic Scheurer - * * @see MergeRuleUtils * @see MergeTotalWeakening * @see MergeByIfThenElse @@ -96,7 +94,7 @@ public class MergeRule implements BuiltInRule { /** * Thresholds the maximum depth of right sides in updates for which an equivalence proof is * started. - * + *

* We skip the check for equal valuation of this variable if the depth threshold is exceeded by * one of the right sides. Experiments show a very big time overhead from a depth of about 8-10 * on, or sometimes even earlier. @@ -166,7 +164,8 @@ public String toString() { // The merge loop SymbolicExecutionState mergedState = - new SymbolicExecutionState(thisSEState.first, thisSEState.second, newGoal.node()); + new SymbolicExecutionState(thisSEState.symbolicState(), thisSEState.pathCondition(), + newGoal.node()); LinkedHashSet newNames = new LinkedHashSet<>(); LinkedHashSet sideConditionsToProve = new LinkedHashSet<>(); HashMap mergePartnerNodesToStates = new HashMap<>(); @@ -183,13 +182,13 @@ public String toString() { mergePartnerNodesToStates.put(state.getCorrespondingNode(), state); - Triple, LinkedHashSet> mergeResult = - mergeStates(mergeRule, mergedState, state, thisSEState.third, + MergeStateEntry mergeResult = + mergeStates(mergeRule, mergedState, state, thisSEState.programCounter(), mergeRuleApp.getDistinguishingFormula(), services); - newNames.addAll(mergeResult.second); - sideConditionsToProve.addAll(mergeResult.third); + newNames.addAll(mergeResult.newIntroducedNames); + sideConditionsToProve.addAll(mergeResult.sideConditionsToProve); - mergedState = mergeResult.first; + mergedState = mergeResult.newSymbolicState; mergedState.setCorrespondingNode(newGoal.node()); } @@ -207,7 +206,7 @@ public String toString() { for (MergePartner mergePartner : mergePartners) { closeMergePartnerGoal(newGoal.node(), mergePartner.getGoal(), mergePartner.getPio(), mergedState, mergePartnerNodesToStates.get(mergePartner.getGoal().node()), - thisSEState.third, newNames); + thisSEState.programCounter(), newNames); } // Delete previous sequents @@ -240,7 +239,7 @@ public String toString() { } // Add new succedent (symbolic state & program counter) - final Term succedentFormula = tb.apply(mergedState.first, thisSEState.third); + final Term succedentFormula = tb.apply(mergedState.first, thisSEState.programCounter()); final SequentFormula newSuccedent = new SequentFormula(succedentFormula); newGoal.addFormula(newSuccedent, new PosInOccurrence(newSuccedent, PosInTerm.getTopLevel(), false)); @@ -258,7 +257,7 @@ public String toString() { } // Add new goals for side conditions that have to be proven - if (sideConditionsToProve.size() > 0) { + if (!sideConditionsToProve.isEmpty()) { final Iterator sideCondIt = sideConditionsToProve.iterator(); int i = 0; @@ -292,7 +291,7 @@ public String toString() { * The programCounter must be the same in both states, so it is supplied * separately. *

- * + *

* Override this method for special merge procedures. * * @param mergeRule The merge procedure to use for the merge. @@ -307,7 +306,7 @@ public String toString() { */ @SuppressWarnings("unused") /* For deactivated equiv check */ - protected Triple, LinkedHashSet> mergeStates( + protected MergeStateEntry mergeStates( MergeProcedure mergeRule, SymbolicExecutionState state1, SymbolicExecutionState state2, Term programCounter, Term distinguishingFormula, Services services) { @@ -378,7 +377,7 @@ protected Triple, LinkedHashSet, LinkedHashSet( + return new MergeStateEntry( new SymbolicExecutionState(newSymbolicState, newAdditionalConstraints == null ? newPathCondition : tb.and(newPathCondition, @@ -451,7 +450,7 @@ protected Triple, LinkedHashSet - * + *

* Override this method for specialized heap merge procedures. * * @param heapVar The heap variable for which the values should be merged. @@ -460,8 +459,8 @@ protected Triple, LinkedHashSet 0; + return !doMergePartnerCheck || !findPotentialMergePartners(goal, pio).isEmpty(); } @@ -676,7 +675,8 @@ public static ImmutableList findPotentialMergePartners(Goal goal, final ImmutableList allGoals = services.getProof().openGoals(); - final Triple ownSEState = sequentToSETriple(goal.node(), pio, services); + final SymbolicExecutionStateWithProgCnt ownSEState = + sequentToSETriple(goal.node(), pio, services); // Find potential partners -- for which isApplicable is true and // they have the same program counter (and post condition). @@ -692,10 +692,10 @@ public static ImmutableList findPotentialMergePartners(Goal goal, final PosInOccurrence gPio = new PosInOccurrence(f, pit, false); if (isOfAdmissibleForm(g, gPio, false)) { - final Triple partnerSEState = + final SymbolicExecutionStateWithProgCnt partnerSEState = sequentToSETriple(g.node(), gPio, services); - if (ownSEState.third.equals(partnerSEState.third)) { + if (ownSEState.programCounter().equals(partnerSEState.programCounter())) { potentialPartners = potentialPartners.prepend(new MergePartner(g, gPio)); @@ -714,4 +714,17 @@ public interface MergeRuleProgressListener { void signalProgress(int progress); } + /** + * Represents the result for merging to states. + * + * @param newSymbolicState the new state + * @param newIntroducedNames newly introduced names + * @param sideConditionsToProve side condition required for merging + * @see #mergeStates(MergeProcedure, SymbolicExecutionState, SymbolicExecutionState, Term, Term, + * Services) + */ + public record MergeStateEntry(SymbolicExecutionState newSymbolicState, + LinkedHashSet newIntroducedNames, + LinkedHashSet sideConditionsToProve) { + } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/merge/procedures/MergeByIfThenElse.java b/key.core/src/main/java/de/uka/ilkd/key/rule/merge/procedures/MergeByIfThenElse.java index 2ad185845f0..d9b85da0719 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/merge/procedures/MergeByIfThenElse.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/merge/procedures/MergeByIfThenElse.java @@ -12,7 +12,6 @@ import de.uka.ilkd.key.logic.op.LocationVariable; import de.uka.ilkd.key.rule.merge.MergeProcedure; import de.uka.ilkd.key.rule.merge.MergeRule; -import de.uka.ilkd.key.util.Quadruple; import de.uka.ilkd.key.util.mergerule.SymbolicExecutionState; import org.key_project.util.collection.DefaultImmutableSet; @@ -108,12 +107,12 @@ public static Term createIfThenElseTerm(final SymbolicExecutionState state1, Term cond, ifForm, elseForm; if (distinguishingFormula == null) { - Quadruple distFormAndRightSidesForITEUpd = + DistanceFormRightSide distFormAndRightSidesForITEUpd = createDistFormAndRightSidesForITEUpd(state1, state2, ifTerm, elseTerm, services); - cond = distFormAndRightSidesForITEUpd.first(); - ifForm = distFormAndRightSidesForITEUpd.second(); - elseForm = distFormAndRightSidesForITEUpd.third(); + cond = distFormAndRightSidesForITEUpd.distinguishingFormula(); + ifForm = distFormAndRightSidesForITEUpd.ifTerm(); + elseForm = distFormAndRightSidesForITEUpd.elseTerm(); } else { cond = distinguishingFormula; ifForm = ifTerm; @@ -147,7 +146,7 @@ public static Term createIfThenElseTerm(final SymbolicExecutionState state1, * second (fourth component = true) state was used as a basis for the condition (first * component). */ - static Quadruple createDistFormAndRightSidesForITEUpd( + static DistanceFormRightSide createDistFormAndRightSidesForITEUpd( LocationVariable v, SymbolicExecutionState state1, SymbolicExecutionState state2, Services services) { @@ -169,7 +168,8 @@ static Quadruple createDistFormAndRightSidesForITEUpd } /** - * Creates the input for an if-then-else update. The elements of the resulting quadruple can be + * Creates the input for an if-then-else update. The elements of the resulting + * {@link DistanceFormRightSide} can be * used to construct an elementary update corresponding to * { v := \if (c1) \then (ifTerm) \else (elseTerm) }, where c1 is the path * condition of state1. However, the method also tries an optimization: The path condition c2 of @@ -190,7 +190,7 @@ static Quadruple createDistFormAndRightSidesForITEUpd * second (fourth component = true) state was used as a basis for the condition (first * component). */ - static Quadruple createDistFormAndRightSidesForITEUpd( + static DistanceFormRightSide createDistFormAndRightSidesForITEUpd( SymbolicExecutionState state1, SymbolicExecutionState state2, Term ifTerm, Term elseTerm, Services services) { @@ -246,7 +246,7 @@ static Quadruple createDistFormAndRightSidesForITEUpd distinguishingFormula = trySimplify(services.getProof(), distinguishingFormula, true, SIMPLIFICATION_TIMEOUT_MS); - return new Quadruple<>(distinguishingFormula, + return new DistanceFormRightSide(distinguishingFormula, commuteSides ? elseTerm : ifTerm, commuteSides ? ifTerm : elseTerm, commuteSides); } @@ -255,4 +255,27 @@ static Quadruple createDistFormAndRightSidesForITEUpd public String toString() { return DISPLAY_NAME; } + + /** + * Represents the distance between formulas for an if-then-else update. + * Input to construct an elementary update like + * { v := \if (distinguishingFormula) \then (ifTerm) \else (elseTerm) }, where + * distinguishingFormula, ifTerm + * and elseTerm are the respective components of the returned triple. The sideCommuted component + * indicates whether the path condition of the distinguishingFormula (sideCommuted component = + * false) or the + * ifTerm (sideCommuted component = true) state was used as a basis for the condition + * (distinguishingFormula + * component). + * + * @param distinguishingFormula a formula + * @param ifTerm a term + * @param elseTerm a term + * @param sideCommuted true if ifTerm and elseTerm have been swapped. + * @see #createDistFormAndRightSidesForITEUpd(SymbolicExecutionState, SymbolicExecutionState, + * Term, Term, Services) + */ + public record DistanceFormRightSide(Term distinguishingFormula, Term ifTerm, Term elseTerm, + boolean sideCommuted) { + } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/merge/procedures/MergeIfThenElseAntecedent.java b/key.core/src/main/java/de/uka/ilkd/key/rule/merge/procedures/MergeIfThenElseAntecedent.java index 18d456f3509..a403f227f4a 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/merge/procedures/MergeIfThenElseAntecedent.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/merge/procedures/MergeIfThenElseAntecedent.java @@ -11,7 +11,6 @@ import de.uka.ilkd.key.logic.op.JFunction; import de.uka.ilkd.key.rule.merge.MergeProcedure; import de.uka.ilkd.key.rule.merge.MergeRule; -import de.uka.ilkd.key.util.Quadruple; import de.uka.ilkd.key.util.mergerule.MergeRuleUtils; import de.uka.ilkd.key.util.mergerule.SymbolicExecutionState; @@ -103,14 +102,14 @@ private static ImmutableSet getIfThenElseConstraints(Term constrained, Ter ImmutableSet result = DefaultImmutableSet.nil(); if (distinguishingFormula == null) { - final Quadruple distFormAndRightSidesForITEUpd = + final MergeByIfThenElse.DistanceFormRightSide distFormAndRightSidesForITEUpd = MergeByIfThenElse.createDistFormAndRightSidesForITEUpd(state1, state2, ifTerm, elseTerm, services); - final Term cond = distFormAndRightSidesForITEUpd.first(); - final Term ifForm = distFormAndRightSidesForITEUpd.second(); - final Term elseForm = distFormAndRightSidesForITEUpd.third(); - final boolean isSwapped = distFormAndRightSidesForITEUpd.fourth(); + final Term cond = distFormAndRightSidesForITEUpd.distinguishingFormula(); + final Term ifForm = distFormAndRightSidesForITEUpd.ifTerm(); + final Term elseForm = distFormAndRightSidesForITEUpd.elseTerm(); + final boolean isSwapped = distFormAndRightSidesForITEUpd.sideCommuted(); final Term varEqualsIfForm = tb.equals(constrained, ifForm); final Term varEqualsElseForm = tb.equals(constrained, elseForm); diff --git a/key.core/src/main/java/de/uka/ilkd/key/speclang/ContractFactory.java b/key.core/src/main/java/de/uka/ilkd/key/speclang/ContractFactory.java index a524843a1b7..83058d0b741 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/speclang/ContractFactory.java +++ b/key.core/src/main/java/de/uka/ilkd/key/speclang/ContractFactory.java @@ -16,9 +16,9 @@ import de.uka.ilkd.key.proof.OpReplacer; import de.uka.ilkd.key.speclang.jml.translation.JMLSpecFactory; import de.uka.ilkd.key.speclang.jml.translation.ProgramVariableCollection; +import de.uka.ilkd.key.speclang.njml.TranslatedDependencyContract; import de.uka.ilkd.key.speclang.translation.SLTranslationException; import de.uka.ilkd.key.util.InfFlowSpec; -import de.uka.ilkd.key.util.Triple; import org.key_project.util.collection.ImmutableArray; import org.key_project.util.collection.ImmutableList; @@ -192,22 +192,24 @@ public DependencyContract dep(KeYJavaType containerType, IObserverFunction pm, } public DependencyContract dep(KeYJavaType kjt, LocationVariable targetHeap, - Triple dep, LocationVariable selfVar) { - final ImmutableList paramVars = tb.paramVars(dep.first, false); - assert (selfVar == null) == dep.first.isStatic(); + TranslatedDependencyContract dep, LocationVariable selfVar) { + final ImmutableList paramVars = + tb.paramVars(dep.observerFunction(), false); + assert (selfVar == null) == dep.observerFunction().isStatic(); Map pres = new LinkedHashMap<>(); pres.put(services.getTypeConverter().getHeapLDT().getHeap(), selfVar == null ? tb.tt() : tb.inv(tb.var(selfVar))); Map accessibles = new LinkedHashMap<>(); for (final LocationVariable heap : HeapContext.getModifiableHeaps(services, false)) { if (heap == targetHeap) { - accessibles.put(heap, dep.second); + accessibles.put(heap, dep.rhs()); } else { accessibles.put(heap, tb.allLocs()); } } // TODO: insert static invariant?? - return dep(kjt, dep.first, dep.first.getContainerType(), pres, dep.third, accessibles, + return dep(kjt, dep.observerFunction(), dep.observerFunction().getContainerType(), pres, + dep.mby(), accessibles, selfVar, paramVars, null, null); } diff --git a/key.core/src/main/java/de/uka/ilkd/key/speclang/jml/pretranslation/TextualJMLSpecCase.java b/key.core/src/main/java/de/uka/ilkd/key/speclang/jml/pretranslation/TextualJMLSpecCase.java index 83db0781c77..f7ed59b9f03 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/speclang/jml/pretranslation/TextualJMLSpecCase.java +++ b/key.core/src/main/java/de/uka/ilkd/key/speclang/jml/pretranslation/TextualJMLSpecCase.java @@ -10,7 +10,6 @@ import de.uka.ilkd.key.ldt.HeapLDT; import de.uka.ilkd.key.speclang.njml.LabeledParserRuleContext; -import de.uka.ilkd.key.util.Triple; import org.key_project.logic.Name; import org.key_project.util.collection.ImmutableList; @@ -205,9 +204,21 @@ public void addRequires(LabeledParserRuleContext label) { addClause(REQUIRES, label); } - public Triple[] getAbbreviations() { + /** + * An abbreviation is a short-name for a term. Currently unused during the JML translation. + * A relict from older days ({@link #getAbbreviations()}. + * + * @param typeName name of the type + * @param abbrevName the short-representation of the term + * @param abbreviatedTerm the term to be abbreviated. + */ + public record Abbreviation(LabeledParserRuleContext typeName, + LabeledParserRuleContext abbrevName, + LabeledParserRuleContext abbreviatedTerm) {} + + public Abbreviation[] getAbbreviations() { /* weigl: prepare for future use of generated abbreviations from JML specifications */ - return new Triple[0]; + return new Abbreviation[0]; } public ImmutableList getInfFlowSpecs() { diff --git a/key.core/src/main/java/de/uka/ilkd/key/speclang/jml/translation/JMLSpecFactory.java b/key.core/src/main/java/de/uka/ilkd/key/speclang/jml/translation/JMLSpecFactory.java index 5c65044189b..64696bfbaed 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/speclang/jml/translation/JMLSpecFactory.java +++ b/key.core/src/main/java/de/uka/ilkd/key/speclang/jml/translation/JMLSpecFactory.java @@ -46,7 +46,6 @@ import de.uka.ilkd.key.speclang.translation.SLWarningException; import de.uka.ilkd.key.util.InfFlowSpec; import de.uka.ilkd.key.util.MiscTools; -import de.uka.ilkd.key.util.Triple; import de.uka.ilkd.key.util.mergerule.MergeParamsSpec; import org.key_project.logic.Name; @@ -606,12 +605,11 @@ private void translateAssignable(Context context, ProgramVariableCollection prog */ private ImmutableList registerAbbreviationVariables(TextualJMLSpecCase textualSpecCase, Context context, ProgramVariableCollection progVars, ContractClauses clauses) { - for (Triple abbrv : textualSpecCase - .getAbbreviations()) { + for (TextualJMLSpecCase.Abbreviation abbrv : textualSpecCase.getAbbreviations()) { final KeYJavaType abbrKJT = - services.getJavaInfo().getKeYJavaType(abbrv.first.first.getText()); + services.getJavaInfo().getKeYJavaType(abbrv.typeName().first.getText()); final ProgramElementName abbrVarName = - new ProgramElementName(abbrv.second.first.getText()); + new ProgramElementName(abbrv.abbrevName().first.getText()); final LocationVariable abbrVar = new LocationVariable(abbrVarName, abbrKJT, true, true); assert abbrVar.isGhost() : "specification parameter not ghost"; services.getNamespaces().programVariables().addSafely(abbrVar); @@ -620,7 +618,7 @@ private ImmutableList registerAbbreviationVariables(TextualJMLSpecCase tex // parameter Term rhs = new JmlIO(services).context(context).parameters(progVars.paramVars) .atPres(progVars.atPres).atBefore(progVars.atBefores) - .translateTerm(abbrv.third); + .translateTerm(abbrv.abbreviatedTerm()); clauses.abbreviations = clauses.abbreviations.append(tb.elementary(tb.var(abbrVar), rhs)); } @@ -899,7 +897,7 @@ public String generateName(IProgramMethod pm, TextualJMLSpecCase textualSpecCase } public String generateName(IProgramMethod pm, Behavior originalBehavior, String customName) { - return ((!(customName == null) && customName.length() > 0) ? customName + return ((!(customName == null) && !customName.isEmpty()) ? customName : getContractName(pm, originalBehavior)); } @@ -1233,9 +1231,10 @@ public Contract createJMLDependencyContract(KeYJavaType kjt, LocationVariable ta var context = Context.inClass(kjt, false, tb); // translateToTerm expression - Triple dep = + TranslatedDependencyContract dep = new JmlIO(services).context(context).translateDependencyContract(originalDep); - return cf.dep(kjt, targetHeap, dep, dep.first.isStatic() ? null : context.selfVar()); + return cf.dep(kjt, targetHeap, dep, + dep.observerFunction().isStatic() ? null : context.selfVar()); } public Contract createJMLDependencyContract(KeYJavaType kjt, TextualJMLDepends textualDep) { @@ -1508,8 +1507,7 @@ public void translateJmlAssertCondition(final JmlAssert jmlAssert, final IProgra } public @Nullable String checkSetStatementAssignee(Term assignee) { - if (assignee.op() instanceof LocationVariable) { - var variable = (LocationVariable) assignee.op(); + if (assignee.op() instanceof LocationVariable variable) { if (variable.isGhost()) { return null; } else { diff --git a/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/JmlIO.java b/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/JmlIO.java index effb006af91..3fdab8fa401 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/JmlIO.java +++ b/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/JmlIO.java @@ -18,7 +18,6 @@ import de.uka.ilkd.key.speclang.jml.translation.Context; import de.uka.ilkd.key.speclang.translation.SLExpression; import de.uka.ilkd.key.util.InfFlowSpec; -import de.uka.ilkd.key.util.Triple; import de.uka.ilkd.key.util.mergerule.MergeParamsSpec; import org.key_project.util.collection.ImmutableList; @@ -295,9 +294,8 @@ public InfFlowSpec translateInfFlow(LabeledParserRuleContext expr) { * @throws ClassCastException if the {@code ctx} is not suitable */ @SuppressWarnings("unchecked") - public Triple translateDependencyContract( - ParserRuleContext ctx) { - return (Triple) interpret(ctx); + public TranslatedDependencyContract translateDependencyContract(ParserRuleContext ctx) { + return (TranslatedDependencyContract) interpret(ctx); } /** @@ -305,10 +303,11 @@ public Triple translateDependencyContract( *

* Note (weigl): No label is currently attached. * + * @param ctx a context + * @return {@link #translateDependencyContract(ParserRuleContext)} * @throws ClassCastException if the {@code ctx} is not suitable */ - public Triple translateDependencyContract( - LabeledParserRuleContext ctx) { + public TranslatedDependencyContract translateDependencyContract(LabeledParserRuleContext ctx) { return translateDependencyContract(ctx.first); } // endregion diff --git a/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/JmlTermFactory.java b/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/JmlTermFactory.java index 968913112a5..baedf9d073c 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/JmlTermFactory.java +++ b/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/JmlTermFactory.java @@ -27,7 +27,6 @@ import de.uka.ilkd.key.speclang.translation.SLExpression; import de.uka.ilkd.key.speclang.translation.SLTranslationException; import de.uka.ilkd.key.util.MiscTools; -import de.uka.ilkd.key.util.Triple; import org.key_project.logic.Name; import org.key_project.logic.Named; @@ -1030,8 +1029,16 @@ public Pair represents(SLExpression lhs, Term t) { return new Pair<>((IObserverFunction) lhs.getTerm().op(), t); } - public Triple depends(SLExpression lhs, Term rhs, - SLExpression mby) { + /** + * Translates the dependency clause ({@code accessible rhs := mby \measured_by mby}) into a + * dependency contract. + * + * @param lhs left-hand side of the clause + * @param rhs right-hand side of the clause + * @param mby measured by term, can be omitted + * @return {@link TranslatedDependencyContract} + */ + public TranslatedDependencyContract depends(SLExpression lhs, Term rhs, SLExpression mby) { LocationVariable heap = services.getTypeConverter().getHeapLDT().getHeap(); if (!lhs.isTerm()) { @@ -1050,7 +1057,7 @@ public Triple depends(SLExpression lhs, Term rhs, + ", given" + lhs.getTerm().sub(0).op()); } - return new Triple<>((IObserverFunction) lhs.getTerm().op(), rhs, + return new TranslatedDependencyContract((IObserverFunction) lhs.getTerm().op(), rhs, mby == null ? null : mby.getTerm()); } diff --git a/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/TranslatedDependencyContract.java b/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/TranslatedDependencyContract.java new file mode 100644 index 00000000000..5e3582459b4 --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/TranslatedDependencyContract.java @@ -0,0 +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 de.uka.ilkd.key.speclang.njml; + +import de.uka.ilkd.key.logic.Term; +import de.uka.ilkd.key.logic.op.IObserverFunction; + +/** + * The information obtain from an JML accessible clause. + * + * @author Alexander Weigl + * @version 1 (23.04.24) + */ +public record TranslatedDependencyContract(IObserverFunction observerFunction, Term rhs, Term mby) { +} diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/definition/StrategySettingsDefinition.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/definition/StrategySettingsDefinition.java index db1c5c7b10f..a15f94f9ecc 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/strategy/definition/StrategySettingsDefinition.java +++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/definition/StrategySettingsDefinition.java @@ -9,7 +9,6 @@ import de.uka.ilkd.key.strategy.Strategy; import de.uka.ilkd.key.strategy.StrategyFactory; import de.uka.ilkd.key.strategy.StrategyProperties; -import de.uka.ilkd.key.util.Triple; import org.key_project.util.collection.ImmutableArray; @@ -36,8 +35,17 @@ * @see StrategyPropertyValueDefinition */ public class StrategySettingsDefinition { + /** + * This class represents an attribute in the strategy settings. + * + * @param name name of the attribute + * @param order precedence for sorting + * @param factory factory for creating new settings + */ + public record StrategySettingEntry(String name, int order, + IDefaultStrategyPropertiesFactory factory) {} - private static final ArrayList> STD_FURTHER_DEFAULTS; + private static final ArrayList STD_FURTHER_DEFAULTS; /** * Defines if a user interface control is shown to edit {@link StrategySettings#getMaxSteps()}. @@ -74,14 +82,13 @@ public class StrategySettingsDefinition { * Further default settings, for example suitable for simplification. Consists of triples * (DEFAULT_NAME, MAX_RULE_APPS, PROPERTIES). */ - private final ArrayList> furtherDefaults; + private final ArrayList furtherDefaults; static { - STD_FURTHER_DEFAULTS = - new ArrayList<>(); + STD_FURTHER_DEFAULTS = new ArrayList<>(); // Java verification standard preset (tested in TimSort case study) - STD_FURTHER_DEFAULTS.add(new Triple<>( + STD_FURTHER_DEFAULTS.add(new StrategySettingEntry( "Java verif. std.", 7000, () -> { final StrategyProperties newProps = IDefaultStrategyPropertiesFactory.DEFAULT_FACTORY @@ -124,7 +131,7 @@ public class StrategySettingsDefinition { })); // Simplification preset - STD_FURTHER_DEFAULTS.add(new Triple<>( + STD_FURTHER_DEFAULTS.add(new StrategySettingEntry( "Simplification", 5000, () -> { final StrategyProperties newProps = IDefaultStrategyPropertiesFactory.DEFAULT_FACTORY @@ -197,7 +204,7 @@ public StrategySettingsDefinition(String propertiesTitle, public StrategySettingsDefinition(boolean showMaxRuleApplications, String maxRuleApplicationsLabel, int defaultMaxRuleApplications, String propertiesTitle, IDefaultStrategyPropertiesFactory defaultPropertiesFactory, - ArrayList> furtherDefaults, + ArrayList furtherDefaults, AbstractStrategyPropertyDefinition... properties) { assert defaultPropertiesFactory != null; this.showMaxRuleApplications = showMaxRuleApplications; @@ -272,7 +279,7 @@ public IDefaultStrategyPropertiesFactory getDefaultPropertiesFactory() { /** * @return Further default settings, e.g. for simplification. */ - public ArrayList> getFurtherDefaults() { + public ArrayList getFurtherDefaults() { return furtherDefaults; } diff --git a/key.core/src/main/java/de/uka/ilkd/key/util/Quadruple.java b/key.core/src/main/java/de/uka/ilkd/key/util/Quadruple.java deleted file mode 100644 index 3a18b0a7558..00000000000 --- a/key.core/src/main/java/de/uka/ilkd/key/util/Quadruple.java +++ /dev/null @@ -1,35 +0,0 @@ -/* 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 de.uka.ilkd.key.util; - -import java.util.Comparator; - -/** - * Simple 4-tuple data object. - * - * @param type of first element - * @param type of second element - * @param type of third element - * @param type of fourth element - * @author Dominic Scheurer - */ -public record Quadruple(T1 first, T2 second, T3 third, T4 fourth) { - - /** - * Constructs a comparator for a {@link Quadruple} with arbitrary comparable arguments. - */ - public static , T2 extends Comparable, - T3 extends Comparable, T4 extends Comparable> - Comparator> getComparator() { - Comparator> t1 = Comparator.comparing(it -> it.first); - Comparator> t2 = Comparator.comparing(it -> it.second); - Comparator> t3 = Comparator.comparing(it -> it.third); - Comparator> t4 = Comparator.comparing(it -> it.fourth); - return t1.thenComparing(t2).thenComparing(t3).thenComparing(t4); - } - - public String toString() { - return "(" + first + ", " + second + ", " + third + ", " + fourth + ")"; - } -} diff --git a/key.core/src/main/java/de/uka/ilkd/key/util/Triple.java b/key.core/src/main/java/de/uka/ilkd/key/util/Triple.java deleted file mode 100644 index aec99618b43..00000000000 --- a/key.core/src/main/java/de/uka/ilkd/key/util/Triple.java +++ /dev/null @@ -1,62 +0,0 @@ -/* 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 de.uka.ilkd.key.util; - - -import java.util.Objects; - -/** - * Simple value object to hold three values. - * - * @param type of first element - * @param type of second element - * @param type of third element - */ -public class Triple { - /** - * First element. - */ - public final T1 first; - /** - * Second element. - */ - public final T2 second; - /** - * Third element. - */ - public final T3 third; - - - /** - * Construct a new triple containing the provided values. - * - * @param first first element - * @param second second element - * @param third third element - */ - public Triple(T1 first, T2 second, T3 third) { - this.first = first; - this.second = second; - this.third = third; - } - - - public String toString() { - return "(" + first + ", " + second + ", " + third + ")"; - } - - - public boolean equals(Object o) { - if (!(o instanceof Triple p)) { - return false; - } - return Objects.equals(first, p.first) && Objects.equals(second, p.second) - && Objects.equals(third, p.third); - } - - - public int hashCode() { - return Objects.hash(first, second, third); - } -} diff --git a/key.core/src/main/java/de/uka/ilkd/key/util/mergerule/MergeRuleUtils.java b/key.core/src/main/java/de/uka/ilkd/key/util/mergerule/MergeRuleUtils.java index 4d3fe3dfc6d..332988a3461 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/util/mergerule/MergeRuleUtils.java +++ b/key.core/src/main/java/de/uka/ilkd/key/util/mergerule/MergeRuleUtils.java @@ -32,7 +32,6 @@ import de.uka.ilkd.key.strategy.StrategyProperties; import de.uka.ilkd.key.util.ProofStarter; import de.uka.ilkd.key.util.SideProofUtil; -import de.uka.ilkd.key.util.Triple; import org.key_project.logic.Name; import org.key_project.logic.Named; @@ -653,7 +652,7 @@ public static JavaBlock getJavaBlockRecursive(Term term) { return JavaBlock.EMPTY_JAVABLOCK; } - if (term.subs().size() == 0 || !term.javaBlock().isEmpty()) { + if (term.subs().isEmpty() || !term.javaBlock().isEmpty()) { return term.javaBlock(); } else { for (Term sub : term.subs()) { @@ -1032,7 +1031,7 @@ public static SymbolicExecutionState sequentToSEPair(Node node, PosInOccurrence SymbolicExecutionStateWithProgCnt triple = sequentToSETriple(node, pio, services); - return new SymbolicExecutionState(triple.first, triple.second, node); + return new SymbolicExecutionState(triple.symbolicState(), triple.pathCondition(), node); } /** @@ -1099,11 +1098,12 @@ public static ImmutableList sequentsToSEPairs( final Node node = sequentInfo.getGoal().node(); final Services services = sequentInfo.getGoal().proof().getServices(); - Triple partnerSEState = + SymbolicExecutionStateWithProgCnt partnerSEState = sequentToSETriple(node, sequentInfo.getPio(), services); result = result.prepend( - new SymbolicExecutionState(partnerSEState.first, partnerSEState.second, node)); + new SymbolicExecutionState(partnerSEState.symbolicState(), + partnerSEState.pathCondition(), node)); } return result; @@ -1378,7 +1378,7 @@ public static LocationVariable rename(Name newName, LocationVariable lv) { */ private static Term joinListToAndTerm(ImmutableList formulae, Services services) { - if (formulae.size() == 0) { + if (formulae.isEmpty()) { return services.getTermBuilder().tt(); } else if (formulae.size() == 1) { return formulae.head().formula(); diff --git a/key.core/src/main/java/de/uka/ilkd/key/util/mergerule/SymbolicExecutionStateWithProgCnt.java b/key.core/src/main/java/de/uka/ilkd/key/util/mergerule/SymbolicExecutionStateWithProgCnt.java index 6aa291423f9..b8c04ecece2 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/util/mergerule/SymbolicExecutionStateWithProgCnt.java +++ b/key.core/src/main/java/de/uka/ilkd/key/util/mergerule/SymbolicExecutionStateWithProgCnt.java @@ -7,63 +7,42 @@ import de.uka.ilkd.key.logic.Term; import de.uka.ilkd.key.pp.LogicPrinter; import de.uka.ilkd.key.proof.Node; -import de.uka.ilkd.key.util.Triple; + +import org.jspecify.annotations.Nullable; /** * A symbolic execution state with program counter is a triple of a symbolic state in form of a * parallel update, a path condition in form of a JavaDL formula, and a program counter in form of a * JavaDL formula with non-empty Java Block (and a possible post condition as first, and only, sub * term). - * + * @param symbolicState The symbolic state (parallel update). + * @param pathCondition The path condition (formula). + * @param programCounter The program counter: Formula with non-empty Java block and post + * condition as only sub term. + * @param correspondingNode The node corresponding to this SE state. * @author Dominic Scheurer */ -public class SymbolicExecutionStateWithProgCnt extends Triple { - - private Node correspondingNode = null; - - /** - * @param symbolicState The symbolic state (parallel update). - * @param pathCondition The path condition (formula). - * @param programCounter The program counter: Formula with non-empty Java block and post - * condition as only sub term. - */ - public SymbolicExecutionStateWithProgCnt(Term symbolicState, Term pathCondition, - Term programCounter) { - super(symbolicState, pathCondition, programCounter); - } - - /** - * @param symbolicState The symbolic state (parallel update). - * @param pathCondition The path condition (formula). - * @param programCounter The program counter: Formula with non-empty Java block and post - * condition as only sub term. - * @param correspondingNode The node corresponding to this SE state. - */ - public SymbolicExecutionStateWithProgCnt(Term symbolicState, Term pathCondition, - Term programCounter, Node correspondingNode) { - this(symbolicState, pathCondition, programCounter); - this.correspondingNode = correspondingNode; - } - +public record SymbolicExecutionStateWithProgCnt(Term symbolicState, Term pathCondition, Term programCounter, + @Nullable Node correspondingNode) { /** * @return The symbolic state. */ public Term getSymbolicState() { - return first; + return symbolicState; } /** * @return The path condition. */ public Term getPathCondition() { - return second; + return pathCondition; } /** * @return The program counter (and post condition). */ public Term getProgramCounter() { - return third; + return programCounter; } /** @@ -73,18 +52,11 @@ public Node getCorrespondingNode() { return correspondingNode; } - /** - * @param correspondingNode The node corresponding to this SE state. - */ - public void setCorrespondingNode(Node correspondingNode) { - this.correspondingNode = correspondingNode; - } - /** * @return The corresponding SE state (without the program counter). */ public SymbolicExecutionState toSymbolicExecutionState() { - return new SymbolicExecutionState(first, second); + return new SymbolicExecutionState(symbolicState, pathCondition); } @Override 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..69234d167b4 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().script(); 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 94864222674..c71823dc978 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; @@ -19,7 +18,6 @@ import de.uka.ilkd.key.util.HelperClassForTests; import de.uka.ilkd.key.util.LinkedHashMap; -import org.key_project.util.collection.Pair; import org.key_project.util.helper.FindResources; import org.junit.jupiter.api.DynamicTest; @@ -68,9 +66,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.script(), script.location()); 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 dba91626680..87d614a794b 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.ProofScriptEntry; import de.uka.ilkd.key.proof.Proof; import de.uka.ilkd.key.proof.io.AbstractProblemLoader; import de.uka.ilkd.key.proof.io.ProblemLoaderException; @@ -103,12 +103,12 @@ private void runKey(String file, TestProperty testProperty) throws Exception { try { LOGGER.info("({}) Start proving", caseId); // Initialize KeY environment and load proof. - Pair, Pair> pair = + Pair, ProofScriptEntry> pair = load(keyFile); LOGGER.info("({}) Proving done", caseId); env = pair.first; - Pair script = pair.second; + ProofScriptEntry script = pair.second; loadedProof = env.getLoadedProof(); AbstractProblemLoader.ReplayResult replayResult = env.getReplayResult(); @@ -182,14 +182,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 { + 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.script(), script.location()); pse.execute(env.getUi(), env.getLoadedProof()); } } @@ -197,7 +197,7 @@ private void autoMode(KeYEnvironment env, Proof loa /* * has resemblances with KeYEnvironment.load ... */ - private Pair, Pair> load( + private Pair, 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 3617cbc09c9..c48a8afeb85 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.ProofScriptEntry; 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; @@ -17,8 +17,6 @@ import de.uka.ilkd.key.prover.impl.ApplyStrategyInfo; import de.uka.ilkd.key.strategy.Strategy; -import org.key_project.util.collection.Pair; - class DataRecordingTestFile extends TestFile { public final ProfilingDirectories directories; @@ -30,7 +28,7 @@ public DataRecordingTestFile(TestProperty testProperty, String path, @Override protected void autoMode(KeYEnvironment env, Proof loadedProof, - Pair script) throws Exception { + 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 e8a476b06e7..af762f4e45a 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.ProofScriptEntry; import de.uka.ilkd.key.proof.Proof; import de.uka.ilkd.key.proof.io.AbstractProblemLoader.ReplayResult; import de.uka.ilkd.key.proof.io.ProblemLoaderException; @@ -161,10 +161,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; + ProofScriptEntry script = pair.second; loadedProof = env.getLoadedProof(); ReplayResult replayResult; @@ -263,14 +262,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 { + 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.script(), script.location()); pse.execute(env.getUi(), env.getLoadedProof()); } } @@ -278,7 +277,7 @@ protected void autoMode(KeYEnvironment env, Proof l /* * has resemblances with KeYEnvironment.load ... */ - private Pair, Pair> load( + private Pair, 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/StrategySelectionView.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/StrategySelectionView.java index ca11ccaa58e..9a833bd94eb 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/StrategySelectionView.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/StrategySelectionView.java @@ -25,7 +25,6 @@ import de.uka.ilkd.key.strategy.StrategyFactory; import de.uka.ilkd.key.strategy.StrategyProperties; import de.uka.ilkd.key.strategy.definition.*; -import de.uka.ilkd.key.util.Triple; import org.slf4j.Logger; import org.slf4j.LoggerFactory; @@ -405,9 +404,9 @@ private JPanel createDefaultPanel(StrategySelectionComponents components) { existingPredefs[0] = "Defaults"; int i = 1; - for (Triple furtherDefault : DEFINITION + for (StrategySettingsDefinition.StrategySettingEntry furtherDefault : DEFINITION .getFurtherDefaults()) { - existingPredefs[i] = furtherDefault.first; + existingPredefs[i] = furtherDefault.name(); i++; } @@ -425,10 +424,9 @@ private JPanel createDefaultPanel(StrategySelectionComponents components) { newProps = DEFINITION.getDefaultPropertiesFactory().createDefaultStrategyProperties(); } else { - Triple chosenDefault = - DEFINITION.getFurtherDefaults().get(selIndex - 1); - newMaxSteps = chosenDefault.second; - newProps = chosenDefault.third.createDefaultStrategyProperties(); + var chosenDefault = DEFINITION.getFurtherDefaults().get(selIndex - 1); + newMaxSteps = chosenDefault.order(); + newProps = chosenDefault.factory().createDefaultStrategyProperties(); } mediator.getSelectedProof().getSettings().getStrategySettings() 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 fa0578538d8..33dbfeed86a 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 @@ -23,7 +23,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.ProofScriptEntry; import de.uka.ilkd.key.proof.Goal; import de.uka.ilkd.key.proof.Proof; import de.uka.ilkd.key.proof.ProofAggregate; @@ -221,17 +221,12 @@ private void taskFinishedInternal(TaskFinishedInfo info) { } else { KeYMediator mediator = mainWindow.getMediator(); mediator.getNotationInfo().refresh(mediator.getServices()); - if (problemLoader.hasProofScript()) { - Pair scriptAndLoc; - try { - scriptAndLoc = problemLoader.readProofScript(); - ProofScriptWorker psw = new ProofScriptWorker(mainWindow.getMediator(), - scriptAndLoc.first, scriptAndLoc.second); - psw.init(); - psw.execute(); - } catch (ProofInputException e) { - LOGGER.warn("Failed to load proof", e); - } + ProofScriptEntry scriptAndLoc = problemLoader.getProofScript(); + if (scriptAndLoc != null) { + ProofScriptWorker psw = new ProofScriptWorker(mainWindow.getMediator(), + scriptAndLoc.script(), scriptAndLoc.location()); + psw.init(); + psw.execute(); } else if (macroChosen()) { applyMacro(); } diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/nodeviews/SequentView.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/nodeviews/SequentView.java index 8dd79d96681..c617b595e6a 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/nodeviews/SequentView.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/nodeviews/SequentView.java @@ -242,11 +242,6 @@ public void removeNotify() { unregisterListener(); } - @Override - protected void finalize() { - dispose(); - } - /** * Dispose this SequentView. * Before calling this method, the view should be removed from the UI. @@ -257,12 +252,6 @@ public void dispose() { printer = null; } catch (Throwable e) { mainWindow.notify(new GeneralFailureEvent(e.getMessage())); - } finally { - try { - super.finalize(); - } catch (Throwable e) { - mainWindow.notify(new GeneralFailureEvent(e.getMessage())); - } } } diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/proofdiff/ProofDifference.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/proofdiff/ProofDifference.java index abcbed2365a..73bca44ed19 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/proofdiff/ProofDifference.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/proofdiff/ProofDifference.java @@ -12,7 +12,6 @@ import de.uka.ilkd.key.logic.Term; import de.uka.ilkd.key.pp.LogicPrinter; import de.uka.ilkd.key.proof.Node; -import de.uka.ilkd.key.util.Triple; /** * @author Alexander Weigl @@ -84,31 +83,40 @@ static String findAndPopNearestMatch(String l, List right) { return current; } + /** + * Entry in the search queue. + * + * @param idxLeft index of the left candidate + * @param idxRight index of the right candidate + * @param distance measure of difference between candidates + */ + private record QueueEntry(int idxLeft, int idxRight, int distance) {} + static List findPairs(List left, List right) { List pairs = new ArrayList<>(left.size() + right.size()); int initCap = Math.max(8, Math.max(left.size() * right.size(), Math.max(left.size(), right.size()))); - PriorityQueue> queue = - new PriorityQueue<>(initCap, Comparator.comparingInt((t) -> t.third)); + PriorityQueue queue = + new PriorityQueue<>(initCap, Comparator.comparingInt(QueueEntry::distance)); for (int i = 0; i < left.size(); i++) { for (int j = 0; j < right.size(); j++) { - queue.add(new Triple<>(i, j, Levensthein.calculate(left.get(i), right.get(j)))); + queue.add(new QueueEntry(i, j, Levensthein.calculate(left.get(i), right.get(j)))); } } boolean[] matchedLeft = new boolean[left.size()]; boolean[] matchedRight = new boolean[right.size()]; while (!queue.isEmpty()) { - Triple t = queue.poll(); + QueueEntry t = queue.poll(); /* - * if(t.third>=THRESHOLD) { break; } + * if(t.elseTerm>=THRESHOLD) { break; } */ - if (!matchedLeft[t.first] && !matchedRight[t.second]) { - String l = left.get(t.first); - String r = right.get(t.second); - pairs.add(new Matching(l, r, t.third)); - matchedLeft[t.first] = true; - matchedRight[t.second] = true; + if (!matchedLeft[t.idxLeft] && !matchedRight[t.idxRight]) { + String l = left.get(t.idxLeft); + String r = right.get(t.idxRight); + pairs.add(new Matching(l, r, t.distance)); + matchedLeft[t.idxLeft] = true; + matchedRight[t.idxRight] = true; } } diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/ProofTreeView.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/ProofTreeView.java index 45fe758240f..8b5c4718711 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/ProofTreeView.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/ProofTreeView.java @@ -327,9 +327,7 @@ public void setExpandOSSNodes(boolean expandOSSNodes) { this.expandOSSNodes = expandOSSNodes; } - @Override - protected void finalize() throws Throwable { - super.finalize(); + protected void dispose() throws Throwable { Config.DEFAULT.removeConfigChangeListener(configChangeListener); NodeInfoVisualizer.removeListener(nodeInfoVisListener); } 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 c0cf68fe6c7..8edea689cd6 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,7 @@ 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.nparser.ProofScriptEntry; import de.uka.ilkd.key.proof.Goal; import de.uka.ilkd.key.proof.Proof; import de.uka.ilkd.key.proof.ProofAggregate; @@ -44,7 +44,6 @@ import org.key_project.util.collection.ImmutableList; import org.key_project.util.collection.ImmutableSLList; import org.key_project.util.collection.ImmutableSet; -import org.key_project.util.collection.Pair; import org.slf4j.Logger; import org.slf4j.LoggerFactory; @@ -159,13 +158,17 @@ 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); - 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 ... - this.taskFinished(new ProofMacroFinishedInfo(new SkipMacro(), proof)); + ProofScriptEntry script = problemLoader.getProofScript(); + if (script != null) { + ProofScriptEngine pse = + new ProofScriptEngine(script.script(), script.location()); + 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 ... + this.taskFinished(new ProofMacroFinishedInfo(new SkipMacro(), proof)); + } } catch (Exception e) { LOGGER.debug("", e); System.exit(-1); diff --git a/keyext.slicing/src/main/java/org/key_project/slicing/RuleStatistics.java b/keyext.slicing/src/main/java/org/key_project/slicing/RuleStatistics.java index 2a2ee3d8ddb..95d7ebc8509 100644 --- a/keyext.slicing/src/main/java/org/key_project/slicing/RuleStatistics.java +++ b/keyext.slicing/src/main/java/org/key_project/slicing/RuleStatistics.java @@ -10,8 +10,6 @@ import java.util.stream.Collectors; import de.uka.ilkd.key.rule.Rule; -import de.uka.ilkd.key.util.Quadruple; -import de.uka.ilkd.key.util.Triple; /** * Simple data object to store a mapping of rules to various counters. @@ -24,7 +22,7 @@ public class RuleStatistics { * that used this rule and didn't contribute to the proof ("useless" proof steps), and the * number of "useless" proof steps that initiate a chain of further (useless) proof steps. */ - private final Map> map = new HashMap<>(); + private final Map map = new HashMap<>(); /** * Mapping of rule name to whether this rule introduces new proof branches. */ @@ -40,9 +38,10 @@ public void addApplication(Rule rule, boolean branches) { String name = rule.displayName(); ruleBranched.put(name, branches); - Triple entry = - map.computeIfAbsent(name, it -> new Triple<>(0, 0, 0)); - map.put(name, new Triple<>(entry.first + 1, entry.second, entry.third)); + StatisticEntry entry = + map.computeIfAbsent(name, it -> new StatisticEntry(0, 0, 0)); + map.put(name, new StatisticEntry(entry.numberOfApplications + 1, + entry.numberOfUselessApplications, entry.numberOfInitialUselessApplications)); } /** @@ -55,9 +54,10 @@ public void addUselessApplication(Rule rule, boolean branches) { String name = rule.displayName(); ruleBranched.put(name, branches); - Triple entry = - map.computeIfAbsent(name, it -> new Triple<>(0, 0, 0)); - map.put(name, new Triple<>(entry.first + 1, entry.second + 1, entry.third)); + StatisticEntry entry = + map.computeIfAbsent(name, it -> new StatisticEntry(0, 0, 0)); + map.put(name, new StatisticEntry(entry.numberOfApplications + 1, + entry.numberOfUselessApplications + 1, entry.numberOfInitialUselessApplications)); } /** @@ -70,9 +70,10 @@ public void addInitialUselessApplication(Rule rule, boolean branches) { String name = rule.displayName(); ruleBranched.put(name, branches); - Triple entry = - map.computeIfAbsent(name, it -> new Triple<>(0, 0, 0)); - map.put(name, new Triple<>(entry.first + 1, entry.second + 1, entry.third + 1)); + StatisticEntry entry = + map.computeIfAbsent(name, it -> new StatisticEntry(0, 0, 0)); + map.put(name, new StatisticEntry(entry.numberOfApplications + 1, + entry.numberOfUselessApplications + 1, entry.numberOfInitialUselessApplications + 1)); } /** @@ -83,11 +84,12 @@ public void addInitialUselessApplication(Rule rule, boolean branches) { * @param comparator custom comparator * @return list of rule names + counters */ - public List> sortBy( - Comparator> comparator) { + public List sortBy(Comparator comparator) { return map.entrySet().stream() - .map(entry -> new Quadruple<>(entry.getKey(), entry.getValue().first, - entry.getValue().second, entry.getValue().third)) + .map(entry -> new RuleStatisticEntry(entry.getKey(), + entry.getValue().numberOfApplications, + entry.getValue().numberOfUselessApplications, + entry.getValue().numberOfInitialUselessApplications)) .sorted(comparator) .collect(Collectors.toList()); } @@ -99,4 +101,29 @@ public List> sortBy( public boolean branches(String rule) { return ruleBranched.get(rule); } + + /** + * Usage statistic of a rule. + *

+ * TODO weigl: refactoring task, combine {@link RuleStatisticEntry} with {@link StatisticEntry} + * to avoid repetition. + * + * @param ruleName + * @param numberOfApplications + * @param numberOfUselessApplications + * @param numberOfInitialUselessApplications + */ + public record RuleStatisticEntry(String ruleName, int numberOfApplications, + int numberOfUselessApplications, int numberOfInitialUselessApplications) { + } + + /** + * Usage statistic of a rule. + * + * @param numberOfApplications + * @param numberOfUselessApplications + * @param numberOfInitialUselessApplications + */ + public record StatisticEntry(int numberOfApplications, int numberOfUselessApplications, + int numberOfInitialUselessApplications) {} } diff --git a/keyext.slicing/src/main/java/org/key_project/slicing/analysis/DependencyAnalyzer.java b/keyext.slicing/src/main/java/org/key_project/slicing/analysis/DependencyAnalyzer.java index f01a9de6985..df768c0f273 100644 --- a/keyext.slicing/src/main/java/org/key_project/slicing/analysis/DependencyAnalyzer.java +++ b/keyext.slicing/src/main/java/org/key_project/slicing/analysis/DependencyAnalyzer.java @@ -444,7 +444,7 @@ private void deduplicateRuleApps() { // (for obvious reasons, we don't care about origin labels here -> wrapper) Map, Set> foundDupes = new HashMap<>(); graph.outgoingGraphEdgesOf(node).forEach(t -> { - Node proofNode = t.first; + Node proofNode = t.fromNode(); // this analysis algorithm does not support proofs with State Merging if (proofNode.getAppliedRuleApp() instanceof MergeRuleBuiltInRuleApp @@ -465,7 +465,7 @@ private void deduplicateRuleApps() { } // Only try to deduplicate the addition of new formulas. // It is unlikely that two closed goals are derived using the same formula. - GraphNode produced = t.second; + GraphNode produced = t.toNode(); if (!(produced instanceof TrackedFormula)) { return; } @@ -473,7 +473,7 @@ private void deduplicateRuleApps() { .computeIfAbsent( new EqualsModProofIrrelevancyWrapper<>(proofNode.getAppliedRuleApp()), _a -> new LinkedHashSet<>()) - .add(t.third.getProofStep()); + .add(t.annotation().getProofStep()); }); // scan dupes, try to find a set of mergable rule applications diff --git a/keyext.slicing/src/main/java/org/key_project/slicing/graph/DependencyGraph.java b/keyext.slicing/src/main/java/org/key_project/slicing/graph/DependencyGraph.java index 02f109322a2..220bcc22a3d 100644 --- a/keyext.slicing/src/main/java/org/key_project/slicing/graph/DependencyGraph.java +++ b/keyext.slicing/src/main/java/org/key_project/slicing/graph/DependencyGraph.java @@ -11,7 +11,6 @@ import de.uka.ilkd.key.proof.BranchLocation; import de.uka.ilkd.key.proof.Node; import de.uka.ilkd.key.proof.Proof; -import de.uka.ilkd.key.util.Triple; import org.key_project.slicing.DependencyNodeData; import org.key_project.slicing.DependencyTracker; @@ -121,15 +120,27 @@ public Stream incomingEdgesOf(GraphNode node) { } /** + * Represents an edge in the dependency graph. + * + * @param fromNode the outgoing node of the edge + * @param toNode the incoming node of the edge + * @param annotation annotation associated to the edge + */ + public record Edge(Node fromNode, GraphNode toNode, AnnotatedEdge annotation) {} + + /** + * Returns the incoming edges of the given node. + * * @param node a graph node * @return the incoming (graph edges, graph sources) of that node */ - public Stream> incomingGraphEdgesOf(GraphNode node) { + public Stream incomingGraphEdgesOf(GraphNode node) { if (!graph.containsVertex(node)) { return Stream.of(); } return graph.incomingEdgesOf(node).stream() - .map(edge -> new Triple<>(edge.getProofStep(), graph.getEdgeSource(edge), edge)); + .map( + edge -> new Edge(edge.getProofStep(), graph.getEdgeSource(edge), edge)); } /** @@ -144,15 +155,18 @@ public Stream outgoingEdgesOf(GraphNode node) { } /** + * Returns the outgoing edges of the given node. + * * @param node a graph node * @return the outgoing (graph edges, graph targets) of that node */ - public Stream> outgoingGraphEdgesOf(GraphNode node) { + public Stream outgoingGraphEdgesOf(GraphNode node) { if (!graph.containsVertex(node)) { return Stream.of(); } return graph.outgoingEdgesOf(node).stream() - .map(edge -> new Triple<>(edge.getProofStep(), graph.getEdgeTarget(edge), edge)); + .map( + edge -> new Edge(edge.getProofStep(), graph.getEdgeTarget(edge), edge)); } /** @@ -280,7 +294,7 @@ public Stream inputsConsumedBy(Node proofStep) { * @return the outgoing edges of that node */ public Stream edgesUsing(GraphNode node) { - return outgoingGraphEdgesOf(node).map(it -> it.third); + return outgoingGraphEdgesOf(node).map(it -> it.annotation); } /** @@ -289,8 +303,8 @@ public Stream edgesUsing(GraphNode node) { */ public Stream edgesConsuming(GraphNode node) { return outgoingGraphEdgesOf(node) - .filter(it -> it.third.replacesInputNode()) - .map(it -> it.third); + .filter(it -> it.annotation.replacesInputNode()) + .map(it -> it.annotation); } /** @@ -299,7 +313,7 @@ public Stream edgesConsuming(GraphNode node) { */ public Stream edgesProducing(GraphNode node) { return incomingGraphEdgesOf(node) - .map(it -> it.third); + .map(it -> it.annotation); } /** @@ -392,12 +406,12 @@ public DependencyGraph removeChains() { // whose hyperedge should not connect more nodes // (otherwise we cannot remove the edge without // making the graph inconsistent) - Node startNode = incoming.get(0).first; + Node startNode = incoming.get(0).fromNode; if (edgesOf(startNode).size() != 1) { continue; } - GraphNode startGraphNode = incoming.get(0).second; - AnnotatedEdge edge = incoming.get(0).third; + GraphNode startGraphNode = incoming.get(0).toNode; + AnnotatedEdge edge = incoming.get(0).annotation; // get real initial node // (in case of repeated shortenings) @@ -411,9 +425,9 @@ public DependencyGraph removeChains() { // whose hyperedge should not connect more nodes // (otherwise we cannot remove the edge without // making the graph inconsistent) - Node endNode = outgoing.get(0).first; - GraphNode endGraphNode = outgoing.get(0).second; - var edge2 = outgoing.get(0).third; + Node endNode = outgoing.get(0).fromNode; + GraphNode endGraphNode = outgoing.get(0).toNode; + var edge2 = outgoing.get(0).annotation; if (edgesOf(endNode).size() != 1) { continue; } diff --git a/keyext.slicing/src/main/java/org/key_project/slicing/ui/RuleStatisticsDialog.java b/keyext.slicing/src/main/java/org/key_project/slicing/ui/RuleStatisticsDialog.java index 9358166f5cb..ca39d883a20 100644 --- a/keyext.slicing/src/main/java/org/key_project/slicing/ui/RuleStatisticsDialog.java +++ b/keyext.slicing/src/main/java/org/key_project/slicing/ui/RuleStatisticsDialog.java @@ -12,9 +12,9 @@ import de.uka.ilkd.key.gui.MainWindow; import de.uka.ilkd.key.gui.configuration.Config; -import de.uka.ilkd.key.util.Quadruple; import org.key_project.slicing.RuleStatistics; +import org.key_project.slicing.RuleStatistics.RuleStatisticEntry; import org.key_project.slicing.analysis.AnalysisResults; /** @@ -87,8 +87,7 @@ private void createUI(Window window) { statisticsPane.setText(genTable( statistics.sortBy( - Comparator - .comparing((Quadruple it) -> it.second()) + Comparator.comparing(RuleStatisticEntry::numberOfApplications) .reversed()))); statisticsPane.setCaretPosition(0); setLocationRelativeTo(window); @@ -111,36 +110,28 @@ private JPanel constructButtonPanel(JEditorPane statisticsPane) { JButton sortButton1 = new JButton("Sort by name"); sortButton1.addActionListener(event -> { statisticsPane.setText(genTable( - statistics.sortBy(Comparator.comparing(Quadruple::first)))); + statistics.sortBy(Comparator.comparing(RuleStatisticEntry::ruleName)))); statisticsPane.setCaretPosition(0); }); JButton sortButton2 = new JButton("Sort by total"); sortButton2.addActionListener(event -> { statisticsPane.setText(genTable( statistics.sortBy( - Comparator - .comparing( - (Quadruple it) -> it.second()) - .reversed()))); + Comparator.comparing(RuleStatisticEntry::numberOfApplications).reversed()))); statisticsPane.setCaretPosition(0); }); JButton sortButton3 = new JButton("Sort by useless"); sortButton3.addActionListener(event -> { statisticsPane.setText(genTable( - statistics.sortBy( - Comparator - .comparing( - (Quadruple it) -> it.third()) - .reversed()))); + statistics.sortBy(Comparator + .comparing(RuleStatisticEntry::numberOfUselessApplications).reversed()))); statisticsPane.setCaretPosition(0); }); JButton sortButton4 = new JButton("Sort by initial useless"); sortButton4.addActionListener(event -> { statisticsPane.setText(genTable( statistics.sortBy( - Comparator - .comparing( - (Quadruple it) -> it.fourth()) + Comparator.comparing(RuleStatisticEntry::numberOfInitialUselessApplications) .reversed()))); statisticsPane.setCaretPosition(0); }); @@ -170,33 +161,38 @@ public void keyTyped(KeyEvent e) { * @param rules statistics on rule apps (see {@link RuleStatistics}) * @return HTML */ - private String genTable(List> rules) { + private String genTable(List rules) { List columns = List.of("Rule name", "Total applications", "Useless applications", "Initial useless applications"); List> rows = new ArrayList<>(); // summary row int uniqueRules = rules.size(); - int totalSteps = rules.stream().mapToInt(Quadruple::second).sum(); - int uselessSteps = rules.stream().mapToInt(Quadruple::third).sum(); - int initialUseless = rules.stream().mapToInt(Quadruple::fourth).sum(); + int totalSteps = rules.stream().mapToInt(RuleStatisticEntry::numberOfApplications).sum(); + int uselessSteps = + rules.stream().mapToInt(RuleStatisticEntry::numberOfUselessApplications).sum(); + int initialUseless = + rules.stream().mapToInt(RuleStatisticEntry::numberOfInitialUselessApplications).sum(); rows.add(List.of(String.format("(all %d rules)", uniqueRules), Integer.toString(totalSteps), Integer.toString(uselessSteps), Integer.toString(initialUseless))); // next summary row - List> rulesBranching = - rules.stream().filter(it -> statistics.branches(it.first())).toList(); + List rulesBranching = + rules.stream().filter(it -> statistics.branches(it.ruleName())).toList(); int uniqueRules2 = rulesBranching.size(); - totalSteps = rulesBranching.stream().mapToInt(Quadruple::second).sum(); - uselessSteps = rulesBranching.stream().mapToInt(Quadruple::third).sum(); - initialUseless = rulesBranching.stream().mapToInt(Quadruple::fourth).sum(); + totalSteps = + rulesBranching.stream().mapToInt(RuleStatisticEntry::numberOfApplications).sum(); + uselessSteps = + rulesBranching.stream().mapToInt(RuleStatisticEntry::numberOfUselessApplications).sum(); + initialUseless = rulesBranching.stream() + .mapToInt(RuleStatisticEntry::numberOfInitialUselessApplications).sum(); rows.add(List.of(String.format("(%d branching rules)", uniqueRules2), Integer.toString(totalSteps), Integer.toString(uselessSteps), Integer.toString(initialUseless))); rules.forEach(a -> { - String name = a.first(); - Integer all = a.second(); - Integer useless = a.third(); - Integer iua = a.fourth(); + String name = a.ruleName(); + Integer all = a.numberOfApplications(); + Integer useless = a.numberOfUselessApplications(); + Integer iua = a.numberOfInitialUselessApplications(); rows.add(List.of(name, all.toString(), useless.toString(), iua.toString())); }); diff --git a/keyext.slicing/src/main/java/org/key_project/slicing/ui/ShowNodeInfoAction.java b/keyext.slicing/src/main/java/org/key_project/slicing/ui/ShowNodeInfoAction.java index 1066b77a47d..930ea88a5b8 100644 --- a/keyext.slicing/src/main/java/org/key_project/slicing/ui/ShowNodeInfoAction.java +++ b/keyext.slicing/src/main/java/org/key_project/slicing/ui/ShowNodeInfoAction.java @@ -15,11 +15,10 @@ import de.uka.ilkd.key.gui.MainWindow; import de.uka.ilkd.key.gui.actions.MainWindowAction; import de.uka.ilkd.key.proof.Node; -import de.uka.ilkd.key.util.Triple; import org.key_project.slicing.DependencyTracker; import org.key_project.slicing.analysis.AnalysisResults; -import org.key_project.slicing.graph.AnnotatedEdge; +import org.key_project.slicing.graph.DependencyGraph.Edge; import org.key_project.slicing.graph.GraphNode; import org.key_project.util.collection.Pair; @@ -72,17 +71,17 @@ private void showDialog(Window parentWindow) { List graphNodes = new ArrayList<>(); List proofSteps = new ArrayList<>(); AnalysisResults analysisResults = tracker.getAnalysisResults(); - Function, Collection> nodeToTableRow = n -> { - proofSteps.add(n.first); - graphNodes.add(n.second); - var ruleName = n.first.getAppliedRuleApp().rule().displayName(); + Function> nodeToTableRow = n -> { + proofSteps.add(n.fromNode()); + graphNodes.add(n.toNode()); + var ruleName = n.fromNode().getAppliedRuleApp().rule().displayName(); return List.of( - Integer.toString(n.first.serialNr()), - analysisResults != null && !analysisResults.usefulSteps.contains(n.first) + Integer.toString(n.fromNode().serialNr()), + analysisResults != null && !analysisResults.usefulSteps.contains(n.fromNode()) ? "" + ruleName + "" : ruleName, - n.third.replacesInputNode() ? "yes" : "no", - n.second.toString(false, false)); + n.annotation().replacesInputNode() ? "yes" : "no", + n.toNode().toString(false, false)); }; var idxFactory = new IndexFactory(); @@ -99,7 +98,7 @@ private void showDialog(Window parentWindow) { HtmlFactory.generateTable(headers2, clickable, Optional.empty(), outgoing, idxFactory); var useful = analysisResults != null ? tracker.getDependencyGraph().outgoingGraphEdgesOf(node) - .filter(t -> analysisResults.usefulSteps.contains(t.first)).count() + .filter(t -> analysisResults.usefulSteps.contains(t.fromNode())).count() : -1; var extraInfo = useful != -1 ? "

" + useful + " useful rule apps

" : ""; var previousDerivations = 0; diff --git a/keyext.slicing/src/test/java/org/key_project/slicing/DependencyGraphTest.java b/keyext.slicing/src/test/java/org/key_project/slicing/DependencyGraphTest.java index f2b7adc37ff..2b2769523ea 100644 --- a/keyext.slicing/src/test/java/org/key_project/slicing/DependencyGraphTest.java +++ b/keyext.slicing/src/test/java/org/key_project/slicing/DependencyGraphTest.java @@ -58,14 +58,14 @@ void basicTest() { var incomingClosedGoal = graph.incomingGraphEdgesOf(closedGoal).toList(); assertEquals(1, incomingClosedGoal.size()); - assertEquals(formB, incomingClosedGoal.get(0).second); + assertEquals(formB, incomingClosedGoal.get(0).toNode()); var incomingFormB = graph.incomingGraphEdgesOf(formB).toList(); assertEquals(2, incomingFormB.size()); - if (incomingFormB.get(0).second.equals(formA)) { - assertEquals(formC, incomingFormB.get(1).second); + if (incomingFormB.get(0).toNode().equals(formA)) { + assertEquals(formC, incomingFormB.get(1).toNode()); } else { - assertEquals(formA, incomingFormB.get(1).second); + assertEquals(formA, incomingFormB.get(1).toNode()); } assertTrue(graph.containsNode(formA));