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..1cdbd787f8f 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 @@ -25,7 +25,6 @@ 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 +86,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 +133,7 @@ protected static SequentFormula replace(PosInOccurrence pio, Term newTerm, Servi public boolean isApplicableOnSubTerms() { return false; } + + 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/rule/ModalitySideProofRule.java b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/rule/ModalitySideProofRule.java index 6c1a1fa4212..ae8e2bf013c 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 @@ -3,36 +3,23 @@ * SPDX-License-Identifier: GPL-2.0-only */ package de.uka.ilkd.key.symbolic_execution.rule; -import java.util.LinkedHashSet; -import java.util.List; -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.jspecify.annotations.NonNull; import org.key_project.logic.Name; import org.key_project.util.collection.ImmutableArray; import org.key_project.util.collection.ImmutableList; import org.key_project.util.collection.Pair; -import org.jspecify.annotations.NonNull; +import java.util.LinkedHashSet; +import java.util.List; +import java.util.Set; /** *

@@ -182,7 +169,7 @@ public ImmutableList apply(Goal goal, Services services, RuleApp ruleApp) .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 @@ -191,10 +178,10 @@ public ImmutableList apply(Goal goal, Services services, RuleApp ruleApp) 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 727b69d9f19..a88b20100c3 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; @@ -229,7 +226,7 @@ public ImmutableList apply(Goal goal, Services services, RuleApp ruleApp) 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 @@ -238,10 +235,10 @@ public ImmutableList apply(Goal goal, Services services, RuleApp ruleApp) 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) { @@ -257,11 +254,11 @@ public ImmutableList apply(Goal goal, Services services, RuleApp ruleApp) 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/util/SymbolicExecutionSideProofUtil.java b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/util/SymbolicExecutionSideProofUtil.java index 766547c958c..f26b338c655 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 @@ -3,8 +3,6 @@ * SPDX-License-Identifier: GPL-2.0-only */ package de.uka.ilkd.key.symbolic_execution.util; -import java.util.*; - import de.uka.ilkd.key.java.Services; import de.uka.ilkd.key.java.abstraction.KeYJavaType; import de.uka.ilkd.key.ldt.HeapLDT; @@ -32,10 +30,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.AbstractSideProofRule.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; import org.key_project.util.collection.ImmutableList; @@ -43,6 +40,8 @@ import org.key_project.util.collection.Pair; import org.key_project.util.java.CollectionUtil; +import java.util.*; + /** * Provides utility methods for side proofs. * @@ -65,7 +64,7 @@ private SymbolicExecutionSideProofUtil() { * @return The general initial {@link Sequent}. */ public static Sequent computeGeneralSequentToProve(Sequent goalSequent, - SequentFormula currentSF) { + SequentFormula currentSF) { Sequent sequentToProve = Sequent.EMPTY_SEQUENT; for (SequentFormula sf : goalSequent.antecedent()) { if (sf != currentSF) { @@ -106,12 +105,12 @@ public static Sequent computeGeneralSequentToProve(Sequent goalSequent, * @throws ProofInputException Occurred Exception. */ public static List> computeResults(Services services, Proof proof, - ProofEnvironment sideProofEnvironment, Sequent sequentToProve, TermLabel label, - String description, String methodTreatment, String loopTreatment, String queryTreatment, - String splittingOption, boolean addNamesToServices) throws ProofInputException { + ProofEnvironment sideProofEnvironment, Sequent sequentToProve, TermLabel label, + String description, String methodTreatment, String loopTreatment, String queryTreatment, + String splittingOption, boolean addNamesToServices) throws ProofInputException { // Execute side proof ApplyStrategyInfo info = startSideProof(proof, sideProofEnvironment, sequentToProve, - methodTreatment, loopTreatment, queryTreatment, splittingOption); + methodTreatment, loopTreatment, queryTreatment, splittingOption); try { // Extract results and conditions from side proof List> conditionsAndResultsMap = new LinkedList<>(); @@ -169,21 +168,21 @@ 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) throws ProofInputException { // Execute side proof ApplyStrategyInfo info = startSideProof(proof, sideProofEnvironment, sequentToProve, - methodTreatment, loopTreatment, queryTreatment, splittingOption); + methodTreatment, loopTreatment, queryTreatment, splittingOption); try { // Extract relevant things Set relevantThingsInSequentToProve = - extractRelevantThings(info.getProof().getServices(), sequentToProve); + 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."); @@ -196,18 +195,18 @@ public static List, Node>> computeResultsAndConditions(Se if (newPredicateIsSequentFormula) { if (Operator.opEquals(sf.formula().op(), operator)) { throw new IllegalStateException( - "Result predicate found in antecedent."); + "Result predicate found in antecedent."); } else { Term constructedResult = - constructResultIfContained(services, sf, operator); + constructResultIfContained(services, sf, operator); if (constructedResult != null) { throw new IllegalStateException( - "Result predicate found in antecedent."); + "Result predicate found in antecedent."); } } } if (!isIrrelevantCondition(services, sequentToProve, - relevantThingsInSequentToProve, sf)) { + relevantThingsInSequentToProve, sf)) { if (resultConditions.add(sf.formula()) && addNamesToServices) { addNewNamesToNamespace(services, sf.formula()); } @@ -218,7 +217,7 @@ public static List, Node>> computeResultsAndConditions(Se if (Operator.opEquals(sf.formula().op(), operator)) { if (result != null) { throw new IllegalStateException( - "Result predicate found multiple times in succedent."); + "Result predicate found multiple times in succedent."); } result = sf.formula().sub(0); } @@ -227,14 +226,14 @@ public static List, Node>> computeResultsAndConditions(Se if (constructedResult != null) { if (result != null) { throw new IllegalStateException( - "Result predicate found multiple times in succedent."); + "Result predicate found multiple times in succedent."); } result = constructedResult; } } if (result == null) { if (!isIrrelevantCondition(services, sequentToProve, - relevantThingsInSequentToProve, sf)) { + relevantThingsInSequentToProve, sf)) { if (resultConditions.add(services.getTermBuilder().not(sf.formula())) && addNamesToServices) { addNewNamesToNamespace(services, sf.formula()); @@ -245,8 +244,7 @@ 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 { @@ -255,12 +253,12 @@ public static List, Node>> computeResultsAndConditions(Se } private static Term constructResultIfContained(Services services, SequentFormula sf, - Operator operator) { + Operator operator) { return constructResultIfContained(services, sf.formula(), operator); } private static Term constructResultIfContained(Services services, Term term, - Operator operator) { + Operator operator) { if (Operator.opEquals(term.op(), operator)) { return term.sub(0); } else { @@ -280,8 +278,8 @@ private static Term constructResultIfContained(Services services, Term term, } } result = services.getTermFactory().createTerm(term.op(), - new ImmutableArray<>(newSubs), term.boundVars(), - term.getLabels()); + new ImmutableArray<>(newSubs), term.boundVars(), + term.getLabels()); } return result; } @@ -289,7 +287,7 @@ private static Term constructResultIfContained(Services services, Term term, private static boolean isOperatorASequentFormula(Sequent sequent, final Operator operator) { return CollectionUtil.search(sequent, - element -> Operator.opEquals(element.formula().op(), operator)) != null; + element -> Operator.opEquals(element.formula().op(), operator)) != null; } /** @@ -303,14 +301,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()); } }); } @@ -382,15 +377,12 @@ public boolean isContainsModalityOrQuery() { * @return The found relevant things. */ public static Set extractRelevantThings(final Services services, - Sequent sequentToProve) { + 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()); } }); } @@ -437,7 +429,7 @@ private static boolean isRelevantThing(Services services, Term term) { * {@link SequentFormula} is not a relevant condition. */ public static boolean isIrrelevantCondition(Services services, Sequent initialSequent, - Set relevantThingsInSequentToProve, SequentFormula sf) { + Set relevantThingsInSequentToProve, SequentFormula sf) { return initialSequent.antecedent().contains(sf) || initialSequent.succedent().contains(sf) || containsModalityOrQuery(sf) // isInOrOfAntecedent(initialSequent, sf) || || containsIrrelevantThings(services, sf, relevantThingsInSequentToProve); @@ -481,9 +473,9 @@ public static boolean isIrrelevantCondition(Services services, Sequent initialSe * {@link SequentFormula} contains no irrelevant things. */ public static boolean containsIrrelevantThings(Services services, SequentFormula sf, - Set relevantThings) { + Set relevantThings) { ContainsIrrelevantThingsVisitor visitor = - new ContainsIrrelevantThingsVisitor(services, relevantThings); + new ContainsIrrelevantThingsVisitor(services, relevantThings); sf.formula().execPostOrder(visitor); return visitor.isContainsIrrelevantThings(); } @@ -558,11 +550,11 @@ public boolean isContainsIrrelevantThings() { * @throws ProofInputException Occurred Exception */ public static ApplyStrategyInfo startSideProof(Proof proof, - ProofEnvironment sideProofEnvironment, Sequent sequentToProve) + ProofEnvironment sideProofEnvironment, Sequent sequentToProve) throws ProofInputException { return startSideProof(proof, sideProofEnvironment, sequentToProve, - StrategyProperties.METHOD_NONE, StrategyProperties.LOOP_NONE, - StrategyProperties.QUERY_OFF, StrategyProperties.SPLITTING_OFF); + StrategyProperties.METHOD_NONE, StrategyProperties.LOOP_NONE, + StrategyProperties.QUERY_OFF, StrategyProperties.SPLITTING_OFF); } /** @@ -575,12 +567,12 @@ public static ApplyStrategyInfo startSideProof(Proof proof, * @throws ProofInputException Occurred Exception */ public static ApplyStrategyInfo startSideProof(Proof proof, - ProofEnvironment sideProofEnvironment, Sequent sequentToProve, String methodTreatment, - String loopTreatment, String queryTreatment, String splittingOption) + ProofEnvironment sideProofEnvironment, Sequent sequentToProve, String methodTreatment, + String loopTreatment, String queryTreatment, String splittingOption) throws ProofInputException { ProofStarter starter = createSideProof(sideProofEnvironment, sequentToProve, null); return startSideProof(proof, starter, methodTreatment, loopTreatment, queryTreatment, - splittingOption); + splittingOption); } /** @@ -594,7 +586,7 @@ public static ApplyStrategyInfo startSideProof(Proof proof, * @throws ProofInputException Occurred Exception. */ public static ProofStarter createSideProof(ProofEnvironment sideProofEnvironment, - Sequent sequentToProve, String proofName) throws ProofInputException { + Sequent sequentToProve, String proofName) throws ProofInputException { return SideProofUtil.createSideProof(sideProofEnvironment, sequentToProve, proofName); } @@ -607,8 +599,8 @@ public static ProofStarter createSideProof(ProofEnvironment sideProofEnvironment * @return The site proof result. */ public static ApplyStrategyInfo startSideProof(Proof proof, ProofStarter starter, - String methodTreatment, String loopTreatment, String queryTreatment, - String splittingOption) { + String methodTreatment, String loopTreatment, String queryTreatment, + String splittingOption) { assert starter != null; starter.setMaxRuleApplications(10000); StrategyProperties sp = proof != null && !proof.isDisposed() @@ -621,7 +613,7 @@ public static ApplyStrategyInfo startSideProof(Proof proof, ProofStarter starter sp.setProperty(StrategyProperties.QUERY_OPTIONS_KEY, queryTreatment); sp.setProperty(StrategyProperties.SPLITTING_OPTIONS_KEY, splittingOption); sp.setProperty(StrategyProperties.QUANTIFIERS_OPTIONS_KEY, - StrategyProperties.QUANTIFIERS_NON_SPLITTING); + StrategyProperties.QUANTIFIERS_NON_SPLITTING); starter.setStrategyProperties(sp); // Execute proof in the current thread return starter.start(); @@ -668,8 +660,8 @@ public static Term extractOperatorTerm(ApplyStrategyInfo info, Operator operator assert info != null; if (info.getProof().openGoals().size() != 1) { throw new ProofInputException( - "Assumption that return value extraction has one goal does not hold because " - + info.getProof().openGoals().size() + " goals are available."); + "Assumption that return value extraction has one goal does not hold because " + + info.getProof().openGoals().size() + " goals are available."); } // Get node of open goal return extractOperatorTerm(info.getProof().openGoals().head(), operator); @@ -723,11 +715,11 @@ public static Term extractOperatorTerm(Node node, final Operator operator) { * {@link Proof} but with its own {@link OneStepSimplifier} instance. */ public static ProofEnvironment cloneProofEnvironmentWithOwnOneStepSimplifier(final Proof source, - final boolean useSimplifyTermProfile) { + final boolean useSimplifyTermProfile) { assert source != null; assert !source.isDisposed(); return cloneProofEnvironmentWithOwnOneStepSimplifier(source.getInitConfig(), - useSimplifyTermProfile); + useSimplifyTermProfile); } /** @@ -753,13 +745,13 @@ protected ImmutableList computeTermLabelConfiguration() Profile sourceProfile = sourceInitConfig.getProfile(); if (sourceProfile instanceof SymbolicExecutionJavaProfile) { ImmutableList result = - super.computeTermLabelConfiguration(); + super.computeTermLabelConfiguration(); // Make sure that the term labels of symbolic execution are also supported // by the new environment. result = result.prepend(SymbolicExecutionJavaProfile .getSymbolicExecutionTermLabelConfigurations( - SymbolicExecutionJavaProfile - .isTruthValueEvaluationEnabled(sourceInitConfig))); + SymbolicExecutionJavaProfile + .isTruthValueEvaluationEnabled(sourceInitConfig))); return result; } else { return super.computeTermLabelConfiguration(); @@ -773,13 +765,13 @@ protected ImmutableList computeTermLabelConfiguration() Profile sourceProfile = sourceInitConfig.getProfile(); if (sourceProfile instanceof SymbolicExecutionJavaProfile) { ImmutableList result = - super.computeTermLabelConfiguration(); + super.computeTermLabelConfiguration(); // Make sure that the term labels of symbolic execution are also supported // by the new environment. result = result.prepend(SymbolicExecutionJavaProfile .getSymbolicExecutionTermLabelConfigurations( - SymbolicExecutionJavaProfile - .isTruthValueEvaluationEnabled(sourceInitConfig))); + SymbolicExecutionJavaProfile + .isTruthValueEvaluationEnabled(sourceInitConfig))); return result; } else { return super.computeTermLabelConfiguration(); @@ -789,7 +781,7 @@ protected ImmutableList computeTermLabelConfiguration() } // Create new InitConfig final InitConfig initConfig = - new InitConfig(sourceInitConfig.getServices().copy(profile, false)); + new InitConfig(sourceInitConfig.getServices().copy(profile, false)); // Set modified taclet options in which runtime exceptions are banned. Choice runtimeExceptionTreatment = new Choice("ban", "runtimeExceptions"); ImmutableSet choices = SideProofUtil @@ -801,14 +793,14 @@ protected ImmutableList computeTermLabelConfiguration() : null; initConfig.setSettings(clonedSettings); initConfig.setTaclet2Builder( - (HashMap>) sourceInitConfig.getTaclet2Builder() - .clone()); + (HashMap>) sourceInitConfig.getTaclet2Builder() + .clone()); initConfig.setTaclets(sourceInitConfig.getTaclets()); // Create new ProofEnvironment and initialize it with values from initial one. ProofEnvironment env = new ProofEnvironment(initConfig); for (Taclet taclet : initConfig.activatedTaclets()) { initConfig.getJustifInfo().addJustification(taclet, - sourceJustiInfo.getJustification(taclet)); + sourceJustiInfo.getJustification(taclet)); } for (BuiltInRule rule : initConfig.builtInRules()) { RuleJustification origJusti = sourceJustiInfo.getJustification(rule); 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..23a70913479 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 6dde2f9ba5e..ed7bc2fa1f5 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,14 @@ public static class File extends KeyAst { return settings; } - public @Nullable Triple findProofScript() { + 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/proof/init/KeYUserProblemFile.java b/key.core/src/main/java/de/uka/ilkd/key/proof/init/KeYUserProblemFile.java index af88fe91224..0f5cae49926 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; @@ -22,8 +20,8 @@ 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.jspecify.annotations.Nullable; import org.key_project.util.collection.DefaultImmutableSet; import org.key_project.util.collection.ImmutableSet; @@ -174,11 +172,12 @@ public boolean implies(ProofOblInput po) { public boolean hasProofScript() { - return getParseContext().findProofScript() != null; + return readProofScript() != null; } - public Triple readProofScript() { - return getParseContext().findProofScript(); + 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 8417e0fbbc3..a637f5fa1e9 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 @@ -3,25 +3,9 @@ * SPDX-License-Identifier: GPL-2.0-only */ package de.uka.ilkd.key.proof.io; -import java.io.ByteArrayInputStream; -import java.io.File; -import java.io.FileNotFoundException; -import java.io.IOException; -import java.lang.reflect.InvocationTargetException; -import java.lang.reflect.Method; -import java.net.URI; -import java.nio.charset.StandardCharsets; -import java.nio.file.*; -import java.util.*; -import java.util.function.Consumer; -import java.util.stream.Collectors; -import java.util.stream.Stream; -import java.util.zip.ZipFile; - -import de.uka.ilkd.key.java.Position; import de.uka.ilkd.key.java.Services; import de.uka.ilkd.key.nparser.KeYLexer; -import de.uka.ilkd.key.parser.Location; +import de.uka.ilkd.key.nparser.ProofScriptEntry; import de.uka.ilkd.key.proof.Node; import de.uka.ilkd.key.proof.Proof; import de.uka.ilkd.key.proof.ProofAggregate; @@ -38,16 +22,28 @@ 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.antlr.runtime.MismatchedTokenException; +import org.jspecify.annotations.Nullable; import org.key_project.util.collection.Pair; import org.key_project.util.java.IOUtil; import org.key_project.util.reflection.ClassLoaderUtil; - -import org.antlr.runtime.MismatchedTokenException; import org.slf4j.Logger; import org.slf4j.LoggerFactory; +import java.io.ByteArrayInputStream; +import java.io.File; +import java.io.FileNotFoundException; +import java.io.IOException; +import java.lang.reflect.InvocationTargetException; +import java.lang.reflect.Method; +import java.nio.charset.StandardCharsets; +import java.nio.file.*; +import java.util.*; +import java.util.function.Consumer; +import java.util.stream.Collectors; +import java.util.stream.Stream; +import java.util.zip.ZipFile; + /** *

* This class provides the basic functionality to load something in KeY. The loading process is done @@ -200,7 +196,7 @@ public boolean hasErrors() { // format: (expected, found) mismatchErrors = new HashMap<>(); mismatchErrors.put(new Pair<>(KeYLexer.SEMI, KeYLexer.COMMA), - "there may be only one declaration per line"); + "there may be only one declaration per line"); missedErrors = new HashMap<>(); missedErrors.put(KeYLexer.RPAREN, "closing parenthesis"); @@ -226,19 +222,19 @@ public boolean hasErrors() { * the loaded {@link InitConfig}. */ public AbstractProblemLoader(File file, List classPath, File bootClassPath, - List includes, Profile profileOfNewProofs, boolean forceNewProfileOfNewProofs, - ProblemLoaderControl control, - boolean askUiToSelectAProofObligationIfNotDefinedByLoadedFile, - Properties poPropertiesToForce) { + List includes, Profile profileOfNewProofs, boolean forceNewProfileOfNewProofs, + ProblemLoaderControl control, + boolean askUiToSelectAProofObligationIfNotDefinedByLoadedFile, + Properties poPropertiesToForce) { this.file = file; this.classPath = classPath; this.bootClassPath = bootClassPath; this.control = control; this.profileOfNewProofs = - profileOfNewProofs != null ? profileOfNewProofs : AbstractProfile.getDefaultProfile(); + profileOfNewProofs != null ? profileOfNewProofs : AbstractProfile.getDefaultProfile(); this.forceNewProfileOfNewProofs = forceNewProfileOfNewProofs; this.askUiToSelectAProofObligationIfNotDefinedByLoadedFile = - askUiToSelectAProofObligationIfNotDefinedByLoadedFile; + askUiToSelectAProofObligationIfNotDefinedByLoadedFile; this.poPropertiesToForce = poPropertiesToForce; this.includes = includes; } @@ -312,14 +308,14 @@ protected void loadEnvironment() throws ProofInputException, IOException { LOGGER.info("Loading environment from " + file); envInput = createEnvInput(fileRepo); LOGGER.debug( - "Environment load took " + PerfScope.formatTime(System.nanoTime() - timeBeforeEnv)); + "Environment load took " + PerfScope.formatTime(System.nanoTime() - timeBeforeEnv)); problemInitializer = createProblemInitializer(fileRepo); var beforeInitConfig = System.nanoTime(); LOGGER.info("Creating init config"); initConfig = createInitConfig(); initConfig.setFileRepo(fileRepo); LOGGER.debug( - "Init config took " + PerfScope.formatTime(System.nanoTime() - beforeInitConfig)); + "Init config took " + PerfScope.formatTime(System.nanoTime() - beforeInitConfig)); if (!problemInitializer.getWarnings().isEmpty() && !ignoreWarnings) { control.reportWarnings(problemInitializer.getWarnings()); } @@ -347,7 +343,7 @@ protected void selectAndLoadProof(ProblemLoaderControl control, InitConfig initC * @see AbstractProblemLoader#load() */ protected void loadSelectedProof(LoadedPOContainer poContainer, ProofAggregate proofList, - Consumer callbackProofLoaded) + Consumer callbackProofLoaded) throws ProofInputException, ProblemLoaderException { // try to replay first proof proof = proofList.getProof(poContainer.getProofNum()); @@ -385,23 +381,23 @@ protected ProblemLoaderException recoverParserErrorMessage(Exception e) { if (c0 instanceof org.antlr.runtime.MismatchedTokenException) { if (c0 instanceof org.antlr.runtime.MissingTokenException) { final org.antlr.runtime.MissingTokenException mte = - (org.antlr.runtime.MissingTokenException) c0; + (org.antlr.runtime.MissingTokenException) c0; // TODO: other commonly missed tokens final String readable = missedErrors.get(mte.expecting); final String token = readable == null ? "token id " + mte.expecting : readable; final String msg = "Syntax error: missing " + token - + (occurrence == null ? "" : " at " + occurrence.getText()) + " statement (" - + mte.input.getSourceName() + ":" + mte.line + ")"; + + (occurrence == null ? "" : " at " + occurrence.getText()) + " statement (" + + mte.input.getSourceName() + ":" + mte.line + ")"; return new ProblemLoaderException(this, msg, mte); // TODO other ANTLR exceptions } else { final org.antlr.runtime.MismatchedTokenException mte = - (MismatchedTokenException) c0; + (MismatchedTokenException) c0; final String genericMsg = "expected " + mte.expecting + ", but found " + mte.c; final String readable = - mismatchErrors.get(new Pair<>(mte.expecting, mte.c)); + mismatchErrors.get(new Pair<>(mte.expecting, mte.c)); final String msg = "Syntax error: " + (readable == null ? genericMsg : readable) - + " (" + mte.input.getSourceName() + ":" + mte.line + ")"; + + " (" + mte.input.getSourceName() + ":" + mte.line + ")"; return new ProblemLoaderException(this, msg, mte); } } @@ -450,7 +446,7 @@ protected EnvInput createEnvInput(FileRepo fileRepo) throws IOException { ret = new SLEnvInput(".", classPath, bootClassPath, profileOfNewProofs, includes); } else { ret = new SLEnvInput(file.getParentFile().getAbsolutePath(), classPath, - bootClassPath, profileOfNewProofs, includes); + bootClassPath, profileOfNewProofs, includes); } ret.setJavaFile(file.getAbsolutePath()); ret.setIgnoreOtherJavaFiles(loadSingleJavaFile); @@ -510,26 +506,26 @@ protected EnvInput createEnvInput(FileRepo fileRepo) throws IOException { Path unzippedProof = tmpDir.resolve(proofFilename.toPath()); return new KeYUserProblemFile(unzippedProof.toString(), unzippedProof.toFile(), - fileRepo, control, profileOfNewProofs, false); + fileRepo, control, profileOfNewProofs, false); } else if (filename.endsWith(".key") || filename.endsWith(".proof") || filename.endsWith(".proof.gz")) { // KeY problem specification or saved proof return new KeYUserProblemFile(filename, file, fileRepo, control, profileOfNewProofs, - filename.endsWith(".proof.gz")); + filename.endsWith(".proof.gz")); } else if (file.isDirectory()) { // directory containing java sources, probably enriched // by specifications return new SLEnvInput(file.getPath(), classPath, bootClassPath, profileOfNewProofs, - includes); + includes); } else { if (filename.lastIndexOf('.') != -1) { throw new IllegalArgumentException("Unsupported file extension '" - + filename.substring(filename.lastIndexOf('.')) + "' of read-in file " - + filename + ". Allowed extensions are: .key, .proof, .java or " - + "complete directories."); + + filename.substring(filename.lastIndexOf('.')) + "' of read-in file " + + filename + ". Allowed extensions are: .key, .proof, .java or " + + "complete directories."); } else { throw new FileNotFoundException( - "File or directory\n\t " + filename + "\n not found."); + "File or directory\n\t " + filename + "\n not found."); } } } @@ -606,7 +602,7 @@ protected LoadedPOContainer createProofObligationContainer() throws IOException // Load proof obligation settings final Properties properties = new Properties(); properties.load( - new ByteArrayInputStream(proofObligation.getBytes(StandardCharsets.UTF_8))); + new ByteArrayInputStream(proofObligation.getBytes(StandardCharsets.UTF_8))); properties.setProperty(IPersistablePO.PROPERTY_FILENAME, file.getAbsolutePath()); if (poPropertiesToForce != null) { properties.putAll(poPropertiesToForce); @@ -614,7 +610,7 @@ protected LoadedPOContainer createProofObligationContainer() throws IOException String poClass = properties.getProperty(IPersistablePO.PROPERTY_CLASS); if (poClass == null || poClass.isEmpty()) { throw new IOException("Proof obligation class property \"" - + IPersistablePO.PROPERTY_CLASS + "\" is not defiend or empty."); + + IPersistablePO.PROPERTY_CLASS + "\" is not defiend or empty."); } try { // Try to instantiate proof obligation by calling static method: public static @@ -622,13 +618,13 @@ protected LoadedPOContainer createProofObligationContainer() throws IOException // IOException Class poClassInstance = ClassLoaderUtil.getClassforName(poClass); Method loadMethod = - poClassInstance.getMethod("loadFrom", InitConfig.class, Properties.class); + poClassInstance.getMethod("loadFrom", InitConfig.class, Properties.class); return (LoadedPOContainer) loadMethod.invoke(null, initConfig, properties); } catch (NoSuchMethodException | IllegalAccessException | IllegalArgumentException - | ClassNotFoundException e) { + | ClassNotFoundException e) { throw new IOException( - "Can't call static factory method \"loadFrom\" on class \"" + poClass + "\".", - e); + "Can't call static factory method \"loadFrom\" on class \"" + poClass + "\".", + e); } catch (InvocationTargetException e) { // Try to unwrap the inner exception as good as possible if (e.getCause() instanceof IOException) { @@ -656,7 +652,7 @@ protected LoadedPOContainer createProofObligationContainer() throws IOException protected ProofAggregate createProof(LoadedPOContainer poContainer) throws ProofInputException { ProofAggregate proofList = - problemInitializer.startProver(initConfig, poContainer.getProofOblInput()); + problemInitializer.startProver(initConfig, poContainer.getProofOblInput()); for (Proof p : proofList.getProofs()) { // register proof @@ -680,26 +676,17 @@ public boolean hasProofScript() { return false; } - public Pair readProofScript() throws ProofInputException { + public @Nullable ProofScriptEntry readProofScript() throws ProofInputException { assert envInput instanceof KeYUserProblemFile; KeYUserProblemFile kupf = (KeYUserProblemFile) envInput; - - Triple script = kupf.readProofScript(); - URI url = kupf.getInitialFile().toURI(); - Location location = new Location(url, Position.newOneBased(script.second, script.third)); - - return new Pair<>(script.first, location); + return kupf.readProofScript(); } - public Pair getProofScript() throws ProblemLoaderException { - if (hasProofScript()) { - try { - return readProofScript(); - } catch (ProofInputException e) { - throw new ProblemLoaderException(this, e); - } - } else { - return null; + public @Nullable ProofScriptEntry getProofScript() throws ProblemLoaderException { + try { + return readProofScript(); + } catch (ProofInputException e) { + throw new ProblemLoaderException(this, e); } } @@ -720,7 +707,7 @@ private ReplayResult replayProof(Proof proof) { assert envInput instanceof KeYUserProblemFile; IntermediatePresentationProofFileParser parser = - new IntermediatePresentationProofFileParser(proof); + new IntermediatePresentationProofFileParser(proof); problemInitializer.tryReadProof(parser, (KeYUserProblemFile) envInput); parserResult = parser.getResult(); @@ -731,14 +718,14 @@ private ReplayResult replayProof(Proof proof) { // able to load proofs that used it even if the user has currently // turned OSS off. StrategyProperties newProps = - proof.getSettings().getStrategySettings().getActiveStrategyProperties(); + proof.getSettings().getStrategySettings().getActiveStrategyProperties(); newProps.setProperty(StrategyProperties.OSS_OPTIONS_KEY, StrategyProperties.OSS_ON); Strategy.updateStrategySettings(proof, newProps); OneStepSimplifier.refreshOSS(proof); replayer = new IntermediateProofReplayer(this, proof, parserResult); replayResult = - replayer.replay(problemInitializer.getListener(), problemInitializer.getProgMon()); + replayer.replay(problemInitializer.getListener(), problemInitializer.getProgMon()); lastTouchedNode = replayResult.getLastSelectedGoal() != null ? replayResult.getLastSelectedGoal().node() @@ -759,13 +746,13 @@ private ReplayResult replayProof(Proof proof) { } status += (status.isEmpty() ? "Proof replayed successfully." : "\n\n") + (replayResult != null ? replayResult.getStatus() - : "Error while loading proof."); + : "Error while loading proof."); if (replayResult != null) { errors.addAll(replayResult.getErrors()); } StrategyProperties newProps = - proof.getSettings().getStrategySettings().getActiveStrategyProperties(); + proof.getSettings().getStrategySettings().getActiveStrategyProperties(); newProps.setProperty(StrategyProperties.OSS_OPTIONS_KEY, ossStatus); Strategy.updateStrategySettings(proof, newProps); OneStepSimplifier.refreshOSS(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 8581cdeec9e..70d6ea8dbdd 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,7 +48,6 @@ 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 org.key_project.logic.Name; @@ -112,9 +111,10 @@ public class IntermediateProofReplayer { private final LinkedList> queue = new LinkedList<>(); + public record PartnerNode(Node first, PosInOccurrence second, NodeIntermediate third){} + /** 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,8 +264,8 @@ public Result replay(ProblemInitializer.ProblemInitializerListener listener, (BuiltInAppIntermediate) currInterm.getIntermediateRuleApp(); if (appInterm instanceof MergeAppIntermediate joinAppInterm) { - HashSet> partnerNodesInfo = - joinPartnerNodes.get(((MergeAppIntermediate) appInterm).getId()); + HashSet partnerNodesInfo = + joinPartnerNodes.get(((MergeAppIntermediate) appInterm).getId()); if (partnerNodesInfo == null || partnerNodesInfo.size() < joinAppInterm.getNrPartners()) { @@ -309,7 +309,7 @@ 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(); LinkedList intermChildren = @@ -327,11 +327,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 +713,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,14 +802,14 @@ private MergeRuleBuiltInRuleApp instantiateJoinApp(final MergeAppIntermediate jo } ImmutableList joinPartners = ImmutableSLList.nil(); - for (Triple partnerNodeInfo : partnerNodesInfo) { + for (PartnerNode partnerNodeInfo : partnerNodesInfo) { - final Triple ownSEState = + var ownSEState = sequentToSETriple(currNode, joinApp.posInOccurrence(), services); - final Triple partnerSEState = + var partnerSEState = sequentToSETriple(partnerNodeInfo.first, partnerNodeInfo.second, services); - assert ownSEState.third.equals(partnerSEState.third) + assert ownSEState.third().equals(partnerSEState.third()) : "Cannot merge incompatible program counters"; joinPartners = joinPartners.append( 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 f588dc929b0..8748007d5de 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 @@ -3,11 +3,6 @@ * SPDX-License-Identifier: GPL-2.0-only */ package de.uka.ilkd.key.proof.mgt; -import java.net.URI; -import java.util.*; -import java.util.Map.Entry; -import java.util.function.UnaryOperator; - import de.uka.ilkd.key.java.JavaInfo; import de.uka.ilkd.key.java.Services; import de.uka.ilkd.key.java.Statement; @@ -34,20 +29,18 @@ 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.jspecify.annotations.Nullable; 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.jspecify.annotations.Nullable; +import org.key_project.util.collection.*; import org.slf4j.Logger; import org.slf4j.LoggerFactory; +import java.net.URI; +import java.util.*; +import java.util.Map.Entry; +import java.util.function.UnaryOperator; + /** * Central storage for all specification elements, such as contracts, class axioms, and loop * invariants. Provides methods for adding such elements to the repository, and for retrieving them @@ -68,38 +61,29 @@ public final class SpecificationRepository { private final ContractFactory cf; private final Map, ImmutableSet> contracts = - new LinkedHashMap<>(); + new LinkedHashMap<>(); private final Map, ImmutableSet> operationContracts = - new LinkedHashMap<>(); + new LinkedHashMap<>(); private final Map, ImmutableSet> wdChecks = - new LinkedHashMap<>(); + new LinkedHashMap<>(); private final Map contractsByName = new LinkedHashMap<>(); - private final Map> contractTargets = - new LinkedHashMap<>(); + private final Map> contractTargets = new LinkedHashMap<>(); private final Map> invs = new LinkedHashMap<>(); private final Map> axioms = new LinkedHashMap<>(); - private final Map> initiallyClauses = - new LinkedHashMap<>(); + private final Map> initiallyClauses = new LinkedHashMap<>(); private final Map> proofs = new LinkedHashMap<>(); - private final Map, LoopSpecification> loopInvs = - new LinkedHashMap<>(); - private final Map, ImmutableSet> blockContracts = - new LinkedHashMap<>(); - private final Map, ImmutableSet> loopContracts = - new LinkedHashMap<>(); + private final Map, LoopSpecification> loopInvs = new LinkedHashMap<>(); + private final Map> blockContracts = new LinkedHashMap<>(); + private final Map> loopContracts = new LinkedHashMap<>(); + /** * A map which relates each loop statement its starting line number and set of loop contracts. */ - private final Map, ImmutableSet> loopContractsOnLoops = - new LinkedHashMap<>(); - private final Map> mergeContracts = - new LinkedHashMap<>(); - private final Map unlimitedToLimited = - new LinkedHashMap<>(); - private final Map limitedToUnlimited = - new LinkedHashMap<>(); - private final Map> unlimitedToLimitTaclets = - new LinkedHashMap<>(); + private final Map, ImmutableSet> loopContractsOnLoops = new LinkedHashMap<>(); + private final Map> mergeContracts = new LinkedHashMap<>(); + private final Map unlimitedToLimited = new LinkedHashMap<>(); + private final Map limitedToUnlimited = new LinkedHashMap<>(); + private final Map> unlimitedToLimitTaclets = new LinkedHashMap<>(); /** *

@@ -114,13 +98,13 @@ public final class SpecificationRepository { *

*/ private final Map> allClassAxiomsCache = - new LinkedHashMap<>(); + new LinkedHashMap<>(); private final Services services; private final TermBuilder tb; private final Map contractCounters = - new de.uka.ilkd.key.util.LinkedHashMap<>(); + new de.uka.ilkd.key.util.LinkedHashMap<>(); public SpecificationRepository(Services services) { this.services = services; @@ -147,7 +131,7 @@ private static String getUniqueNameForObserver(IObserverFunction obs) { } private static Taclet getLimitedToUnlimitedTaclet(IObserverFunction limited, - IObserverFunction unlimited, TermServices services) { + IObserverFunction unlimited, TermServices services) { final TermBuilder tb = services.getTermBuilder(); assert limited.arity() == unlimited.arity(); @@ -155,7 +139,7 @@ private static Taclet getLimitedToUnlimitedTaclet(IObserverFunction limited, final Term[] subs = new Term[limited.arity()]; for (int i = 0; i < subs.length; i++) { final SchemaVariable argSV = SchemaVariableFactory.createTermSV(new Name("t" + i), - limited.argSort(i), false, false); + limited.argSort(i), false, false); subs[i] = tb.var(argSV); } final Term limitedTerm = tb.func(limited, subs); @@ -165,14 +149,14 @@ private static Taclet getLimitedToUnlimitedTaclet(IObserverFunction limited, final RewriteTacletBuilder tacletBuilder = new RewriteTacletBuilder<>(); tacletBuilder.setFind(limitedTerm); tacletBuilder.addTacletGoalTemplate(new RewriteTacletGoalTemplate(Sequent.EMPTY_SEQUENT, - ImmutableSLList.nil(), unlimitedTerm)); + ImmutableSLList.nil(), unlimitedTerm)); tacletBuilder.setName( - MiscTools.toValidTacletName("unlimit " + getUniqueNameForObserver(unlimited))); + MiscTools.toValidTacletName("unlimit " + getUniqueNameForObserver(unlimited))); return tacletBuilder.getTaclet(); } private static Taclet getUnlimitedToLimitedTaclet(IObserverFunction limited, - IObserverFunction unlimited, TermServices services) { + IObserverFunction unlimited, TermServices services) { assert limited.arity() == unlimited.arity(); final TermBuilder tb = services.getTermBuilder(); @@ -180,7 +164,7 @@ private static Taclet getUnlimitedToLimitedTaclet(IObserverFunction limited, final Term[] subs = new Term[limited.arity()]; for (int i = 0; i < subs.length; i++) { final SchemaVariable argSV = SchemaVariableFactory.createTermSV(new Name("t" + i), - limited.argSort(i), false, false); + limited.argSort(i), false, false); subs[i] = tb.var(argSV); } final Term limitedTerm = tb.func(limited, subs); @@ -191,12 +175,12 @@ private static Taclet getUnlimitedToLimitedTaclet(IObserverFunction limited, tacletBuilder.setFind(tb.func(unlimited, subs)); final SequentFormula cf = new SequentFormula(tb.equals(limitedTerm, unlimitedTerm)); final Sequent addedSeq = - Sequent.createAnteSequent(Semisequent.EMPTY_SEMISEQUENT.insertFirst(cf).semisequent()); + Sequent.createAnteSequent(Semisequent.EMPTY_SEMISEQUENT.insertFirst(cf).semisequent()); tacletBuilder.addTacletGoalTemplate(new RewriteTacletGoalTemplate(addedSeq, - ImmutableSLList.nil(), tb.func(unlimited, subs))); + ImmutableSLList.nil(), tb.func(unlimited, subs))); tacletBuilder.setApplicationRestriction(RewriteTaclet.IN_SEQUENT_STATE); tacletBuilder.setName( - MiscTools.toValidTacletName("limit " + getUniqueNameForObserver(unlimited))); + MiscTools.toValidTacletName("limit " + getUniqueNameForObserver(unlimited))); tacletBuilder.addRuleSet(new RuleSet(new Name("limitObserver"))); return tacletBuilder.getTaclet(); @@ -227,8 +211,9 @@ private IObserverFunction getCanonicalFormForKJT(IObserverFunction obs, KeYJavaT final String name = pm.getMethodDeclaration().getName(); final int numParams = pm.getParameterDeclarationCount(); final ImmutableList candidatePMs = - services.getJavaInfo().getAllProgramMethods(kjt); - outer: for (IProgramMethod candidatePM : candidatePMs) { + services.getJavaInfo().getAllProgramMethods(kjt); + outer: + for (IProgramMethod candidatePM : candidatePMs) { if (candidatePM.getMethodDeclaration().getName().equals(name) && candidatePM.getParameterDeclarationCount() == numParams) { for (int i = 0; i < numParams; i++) { @@ -255,7 +240,7 @@ private IObserverFunction getCanonicalFormForKJT(IObserverFunction obs, KeYJavaT } private ImmutableSet> getOverridingMethods(KeYJavaType kjt, - IProgramMethod pm) { + IProgramMethod pm) { ImmutableList> result = ImmutableSLList.nil(); // static methods and constructors are not overriden @@ -275,7 +260,7 @@ private ImmutableSet> getOverridingMethods( } public ImmutableSet> getOverridingTargets(KeYJavaType kjt, - IObserverFunction target) { + IObserverFunction target) { if (target instanceof IProgramMethod) { return getOverridingMethods(kjt, (IProgramMethod) target); } else { @@ -366,19 +351,19 @@ assert getCanonicalFormForKJT(contract.getTarget(), contract.getKJT()) private void registerContract(Contract contract) { final Pair target = - new Pair<>(contract.getKJT(), contract.getTarget()); + new Pair<>(contract.getKJT(), contract.getTarget()); registerContract(contract, target); } private void registerContract(Contract contract, - final ImmutableSet> targets) { + final ImmutableSet> targets) { for (Pair impl : targets) { registerContract(contract, impl); } } private void registerContract(Contract contract, - Pair targetPair) { + Pair targetPair) { LOGGER.trace("Contract registered {}", contract); if (!WellDefinednessCheck.isOn() && contract instanceof WellDefinednessCheck) { return; @@ -391,30 +376,30 @@ private void registerContract(Contract contract, : "Tried to add a contract with a non-unique name: " + name; assert !name.contains(CONTRACT_COMBINATION_MARKER) : "Tried to add a contract with a name containing the" + " reserved character " - + CONTRACT_COMBINATION_MARKER + ": " + name; + + CONTRACT_COMBINATION_MARKER + ": " + name; assert contract.id() != Contract.INVALID_ID : "Tried to add a contract with an invalid id!"; contracts.put(targetPair, getContracts(targetKJT, targetMethod).add(contract)); if (contract instanceof FunctionalOperationContract) { operationContracts.put(new Pair<>(targetKJT, (IProgramMethod) targetMethod), - getOperationContracts(targetKJT, (IProgramMethod) targetMethod) - .add((FunctionalOperationContract) contract)); + getOperationContracts(targetKJT, (IProgramMethod) targetMethod) + .add((FunctionalOperationContract) contract)); // Create new well-definedness check final MethodWellDefinedness mwd = - new MethodWellDefinedness((FunctionalOperationContract) contract, services); + new MethodWellDefinedness((FunctionalOperationContract) contract, services); registerContract(mwd); } else if (contract instanceof DependencyContract && contract.getOrigVars().atPres.isEmpty() && targetMethod.getContainerType() - .equals(services.getJavaInfo().getJavaLangObject())) { + .equals(services.getJavaInfo().getJavaLangObject())) { // Create or extend a well-definedness check for a class invariant final Term deps = - contract.getAccessible(services.getTypeConverter().getHeapLDT().getHeap()); + contract.getAccessible(services.getTypeConverter().getHeapLDT().getHeap()); final Term mby = contract.getMby(); final String invName = "JML model class invariant in " + targetKJT.getName(); final ClassInvariant inv = new ClassInvariantImpl(invName, invName, targetKJT, - contract.getVisibility(), tb.tt(), contract.getOrigVars().self); + contract.getVisibility(), tb.tt(), contract.getOrigVars().self); ClassWellDefinedness cwd = - new ClassWellDefinedness(inv, targetMethod, deps, mby, services); + new ClassWellDefinedness(inv, targetMethod, deps, mby, services); final ImmutableSet cwds = getWdClassChecks(targetKJT); if (!cwds.isEmpty()) { assert cwds.size() == 1; @@ -428,9 +413,9 @@ private void registerContract(Contract contract, && contract.getOrigVars().atPres.isEmpty()) { // Create or extend a well-definedness check for a model field MethodWellDefinedness mwd = - new MethodWellDefinedness((DependencyContract) contract, services); + new MethodWellDefinedness((DependencyContract) contract, services); final ImmutableSet mwds = - getWdMethodChecks(targetKJT, targetMethod); + getWdMethodChecks(targetKJT, targetMethod); if (!mwds.isEmpty()) { assert mwds.size() == 1; final MethodWellDefinedness oldMwd = mwds.iterator().next(); @@ -456,12 +441,12 @@ private void unregisterContract(Contract contract) { contracts.put(tp, contracts.get(tp).remove(contract)); if (contract instanceof FunctionalOperationContract) { final Pair tp2 = - new Pair<>(tp.first, (IProgramMethod) tp.second); + new Pair<>(tp.first, (IProgramMethod) tp.second); operationContracts.put(tp2, - operationContracts.get(tp2).remove((FunctionalOperationContract) contract)); + operationContracts.get(tp2).remove((FunctionalOperationContract) contract)); if (!getWdChecks(contract.getKJT(), contract.getTarget()).isEmpty()) { ImmutableSet wdcs = - getWdChecks(contract.getKJT(), contract.getTarget()); + getWdChecks(contract.getKJT(), contract.getTarget()); for (WellDefinednessCheck wdc : wdcs) { if (wdc instanceof MethodWellDefinedness && ((MethodWellDefinedness) wdc).getMethodContract().equals(contract)) { @@ -493,7 +478,7 @@ private void createContractsFromInitiallyClause(InitiallyClause inv, KeYJavaType if (!JMLInfoExtractor.isHelper(pm)) { final ImmutableSet oldContracts = getContracts(kjt, pm); ImmutableSet oldFuncContracts = - DefaultImmutableSet.nil(); + DefaultImmutableSet.nil(); for (Contract old : oldContracts) { if (old instanceof FunctionalOperationContract) { oldFuncContracts = oldFuncContracts.add((FunctionalOperationContract) old); @@ -545,7 +530,7 @@ private static ImmutableSet removeWdChecks(ImmutableSet cont */ private void registerWdCheck(WellDefinednessCheck check) { ImmutableSet checks = - getWdChecks(check.getKJT(), check.getTarget()).add(check); + getWdChecks(check.getKJT(), check.getTarget()).add(check); wdChecks.put(new Pair<>(check.getKJT(), check.getTarget()), checks); } @@ -557,7 +542,7 @@ private void registerWdCheck(WellDefinednessCheck check) { */ private void unregisterWdCheck(WellDefinednessCheck check) { wdChecks.put(new Pair<>(check.getKJT(), check.getTarget()), - getWdChecks(check.getKJT(), check.getTarget()).remove(check)); + getWdChecks(check.getKJT(), check.getTarget()).remove(check)); } /** @@ -578,7 +563,7 @@ private ImmutableSet getWdChecks(KeYJavaType kjt) { * Returns all registered (atomic) well-definedness checks for the passed target and kjt. */ private ImmutableSet getWdChecks(KeYJavaType kjt, - IObserverFunction target) { + IObserverFunction target) { assert kjt != null; assert target != null; target = getCanonicalFormForKJT(target, kjt); @@ -618,7 +603,7 @@ private ImmutableSet getWdMethodChecks(KeYJavaType kjt) { * Returns all registered (atomic) well-definedness method checks for the passed target and kjt. */ private ImmutableSet getWdMethodChecks(KeYJavaType kjt, - IObserverFunction target) { + IObserverFunction target) { assert kjt != null; assert target != null; ImmutableSet result = DefaultImmutableSet.nil(); @@ -653,7 +638,7 @@ private ImmutableSet getWdClassChecks(KeYJavaType kjt) { */ @SuppressWarnings("unchecked") private void mapValueSets(Map> map, - UnaryOperator op, Services services) { + UnaryOperator op, Services services) { for (Entry> entry : map.entrySet()) { final K key = entry.getKey(); final ImmutableSet oldSet = entry.getValue(); @@ -684,7 +669,7 @@ private void mapValueSets(Map void mapValues(Map map, - UnaryOperator op, Services services) { + UnaryOperator op, Services services) { for (Entry entry : map.entrySet()) { final K key = entry.getKey(); final V oldContract = entry.getValue(); @@ -740,10 +725,10 @@ public ImmutableSet getAllContracts() { */ public ImmutableSet getContracts(KeYJavaType kjt, IObserverFunction target) { target = - getCanonicalFormForKJT(Objects.requireNonNull(target), Objects.requireNonNull(kjt)); + getCanonicalFormForKJT(Objects.requireNonNull(target), Objects.requireNonNull(kjt)); final Pair pair = new Pair<>(kjt, target); final ImmutableSet result = - WellDefinednessCheck.isOn() ? contracts.get(pair) : removeWdChecks(contracts.get(pair)); + WellDefinednessCheck.isOn() ? contracts.get(pair) : removeWdChecks(contracts.get(pair)); return result == null ? DefaultImmutableSet.nil() : result; } @@ -751,7 +736,7 @@ public ImmutableSet getContracts(KeYJavaType kjt, IObserverFunction ta * Returns all registered (atomic) operation contracts for the passed operation. */ public ImmutableSet getOperationContracts(KeYJavaType kjt, - IProgramMethod pm) { + IProgramMethod pm) { pm = (IProgramMethod) getCanonicalFormForKJT(pm, kjt); final Pair pair = new Pair<>(kjt, pm); final ImmutableSet result = operationContracts.get(pair); @@ -763,14 +748,14 @@ public ImmutableSet getOperationContracts(KeYJavaTy * the passed modality. */ public ImmutableSet getOperationContracts(KeYJavaType kjt, - IProgramMethod pm, Modality.JavaModalityKind modalityKind) { + IProgramMethod pm, Modality.JavaModalityKind modalityKind) { ImmutableSet result = getOperationContracts(kjt, pm); final boolean transactionModality = - modalityKind.transaction(); + modalityKind.transaction(); final Modality.JavaModalityKind matchModality = transactionModality ? ((modalityKind == Modality.JavaModalityKind.DIA_TRANSACTION) - ? Modality.JavaModalityKind.DIA - : Modality.JavaModalityKind.BOX) + ? Modality.JavaModalityKind.DIA + : Modality.JavaModalityKind.BOX) : modalityKind; for (FunctionalOperationContract contract : result) { if (!contract.getModalityKind().equals(matchModality) @@ -797,7 +782,7 @@ public Contract getContractByName(String name) { ImmutableSet baseContracts = DefaultImmutableSet.nil(); for (String baseName : baseNames) { FunctionalOperationContract baseContract = - (FunctionalOperationContract) contractsByName.get(baseName); + (FunctionalOperationContract) contractsByName.get(baseName); if (baseContract == null) { return null; } @@ -814,7 +799,7 @@ public Contract getContractByName(String name) { public ImmutableSet getInheritedContracts(Contract contract) { ImmutableSet result = DefaultImmutableSet.nil().add(contract); final ImmutableSet> subs = - getOverridingTargets(contract.getKJT(), contract.getTarget()); + getOverridingTargets(contract.getKJT(), contract.getTarget()); for (Pair sub : subs) { for (Contract subContract : getContracts(sub.first, sub.second)) { if (subContract.id() == contract.id()) { @@ -854,13 +839,13 @@ public void addContract(Contract contract) { // register and inherit final ImmutableSet> impls = - getOverridingTargets(contract.getKJT(), contract.getTarget()) - .add(new Pair<>(contract.getKJT(), contract.getTarget())); + getOverridingTargets(contract.getKJT(), contract.getTarget()) + .add(new Pair<>(contract.getKJT(), contract.getTarget())); registerContract(contract, impls); if (!contractTargets.get(contract.getKJT()).contains(contract.getTarget())) { throw new IllegalStateException( - "target " + contract.getTarget() + " missing for contract " + contract); + "target " + contract.getTarget() + " missing for contract " + contract); } } @@ -893,7 +878,7 @@ public FunctionalOperationContract combineOperationContracts( // sort contracts alphabetically (for determinism) FunctionalOperationContract[] contractsArray = - toCombine.toArray(new FunctionalOperationContract[toCombine.size()]); + toCombine.toArray(new FunctionalOperationContract[toCombine.size()]); Arrays.sort(contractsArray, Comparator.comparing(SpecificationElement::getName)); return cf.union(contractsArray); @@ -940,7 +925,7 @@ public void addClassInvariant(ClassInvariant inv) { ClassWellDefinedness cwd = cwds.iterator().next(); unregisterContract(cwd); cwd = cwd.combine(new ClassWellDefinedness(inv, cwd.getTarget(), null, null, services), - services); + services); registerContract(cwd); } @@ -956,13 +941,13 @@ public void addClassInvariant(ClassInvariant inv) { for (KeYJavaType sub : subs) { ClassInvariant subInv = inv.setKJT(sub); final IObserverFunction subTarget = - subInv.isStatic() ? services.getJavaInfo().getStaticInv(sub) - : services.getJavaInfo().getInv(); + subInv.isStatic() ? services.getJavaInfo().getStaticInv(sub) + : services.getJavaInfo().getInv(); invs.put(sub, getClassInvariants(sub).add(subInv)); final ImmutableSet subCwds = getWdClassChecks(sub); if (subCwds.isEmpty()) { registerContract( - new ClassWellDefinedness(subInv, subTarget, null, null, services)); + new ClassWellDefinedness(subInv, subTarget, null, null, services)); } else { for (ClassWellDefinedness cwd : subCwds) { unregisterContract(cwd); @@ -995,7 +980,7 @@ public void createContractsFromInitiallyClauses() throws SLTranslationException createContractsFromInitiallyClause(inv, kjt); if (VisibilityModifier.allowsInheritance(inv.getVisibility())) { final ImmutableList subs = - services.getJavaInfo().getAllSubtypes(kjt); + services.getJavaInfo().getAllSubtypes(kjt); for (KeYJavaType sub : subs) { createContractsFromInitiallyClause(inv, sub); } @@ -1077,7 +1062,7 @@ public ImmutableSet getClassAxioms(KeYJavaType selfKjt) { staticInvDef = tb.and(staticInvDef, inv.getInv(null, services)); } else { freeStaticInvDef = - tb.and(freeStaticInvDef, inv.getInv(selfVar, services)); + tb.and(freeStaticInvDef, inv.getInv(selfVar, services)); } } } @@ -1085,9 +1070,9 @@ public ImmutableSet getClassAxioms(KeYJavaType selfKjt) { invDef = tb.tf().createTerm(Equality.EQV, tb.inv(tb.var(selfVar)), invDef); staticInvDef = tb.tf().createTerm(Equality.EQV, tb.staticInv(kjt), staticInvDef); freeInvDef = tb.tf().createTerm(Equality.EQV, - tb.invFree(tb.var(selfVar)), freeInvDef); + tb.invFree(tb.var(selfVar)), freeInvDef); freeStaticInvDef = tb.tf().createTerm(Equality.EQV, - tb.staticInvFree(kjt), freeStaticInvDef); + tb.staticInvFree(kjt), freeStaticInvDef); final IObserverFunction invSymbol = services.getJavaInfo().getInv(); final IObserverFunction staticInvSymbol = services.getJavaInfo().getStaticInv(kjt); @@ -1096,24 +1081,24 @@ public ImmutableSet getClassAxioms(KeYJavaType selfKjt) { .getStaticInvFree(kjt); final ClassAxiom invRepresentsAxiom = - new RepresentsAxiom("Class invariant axiom for " + kjt.getFullName(), invSymbol, - kjt, new Private(), null, invDef, selfVar, ImmutableSLList.nil(), null); + new RepresentsAxiom("Class invariant axiom for " + kjt.getFullName(), invSymbol, + kjt, new Private(), null, invDef, selfVar, ImmutableSLList.nil(), null); result = result.add(invRepresentsAxiom); final ClassAxiom staticInvRepresentsAxiom = new RepresentsAxiom( - "Static class invariant axiom for " + kjt.getFullName(), staticInvSymbol, kjt, - new Private(), null, staticInvDef, null, ImmutableSLList.nil(), null); + "Static class invariant axiom for " + kjt.getFullName(), staticInvSymbol, kjt, + new Private(), null, staticInvDef, null, ImmutableSLList.nil(), null); result = result.add(staticInvRepresentsAxiom); final ClassAxiom invFreeRepresentsAxiom = new RepresentsAxiom( - "Free class invariant axiom for " + kjt.getFullName(), freeInvSymbol, kjt, - new Private(), null, freeInvDef, selfVar, ImmutableSLList.nil(), null); + "Free class invariant axiom for " + kjt.getFullName(), freeInvSymbol, kjt, + new Private(), null, freeInvDef, selfVar, ImmutableSLList.nil(), null); result = result.add(invFreeRepresentsAxiom); final ClassAxiom staticFreeInvRepresentsAxiom = new RepresentsAxiom( - "Free static class invariant axiom for " + kjt.getFullName(), - freeStaticInvSymbol, kjt, new Private(), null, freeStaticInvDef, null, - ImmutableSLList.nil(), null); + "Free static class invariant axiom for " + kjt.getFullName(), + freeStaticInvSymbol, kjt, new Private(), null, freeStaticInvDef, null, + ImmutableSLList.nil(), null); result = result.add(staticFreeInvRepresentsAxiom); } @@ -1129,7 +1114,7 @@ freeStaticInvSymbol, kjt, new Private(), null, freeStaticInvDef, null, } final ClassAxiom queryAxiom = new QueryAxiom("Query axiom for " + pm.getName() - + "_" + sb + " in " + selfKjt.getFullName(), pm, selfKjt); + + "_" + sb + " in " + selfKjt.getFullName(), pm, selfKjt); result = result.add(queryAxiom); } } @@ -1158,7 +1143,7 @@ private ImmutableSet getModelMethodAxioms() { List heaps = HeapContext.getModHeaps(services, false); for (LocationVariable heap : heaps) { atPreVars.put(heap, - tb.atPreVar(heap.name().toString(), heap.sort(), false)); + tb.atPreVar(heap.name().toString(), heap.sort(), false)); } ProgramVariable resultVar = tb.resultVar(pm, false); @@ -1167,10 +1152,10 @@ private ImmutableSet getModelMethodAxioms() { // We need to construct an inheritance chain of contracts // starting at the bottom ImmutableList lookupContracts = - ImmutableSLList.nil(); + ImmutableSLList.nil(); ImmutableSet cs = getOperationContracts(kjt, pm); ImmutableList superTypes = - services.getJavaInfo().getAllSupertypes(kjt); + services.getJavaInfo().getAllSupertypes(kjt); for (KeYJavaType superType : superTypes) { for (FunctionalOperationContract fop : cs) { if (fop.getSpecifiedIn().equals(superType)) { @@ -1180,9 +1165,9 @@ private ImmutableSet getModelMethodAxioms() { } for (FunctionalOperationContract fop : lookupContracts) { Term representsFromContract = fop.getRepresentsAxiom(heaps.get(0), selfVar, - paramVars, tb.resultVar(pm, false), atPreVars, services); + paramVars, tb.resultVar(pm, false), atPreVars, services); Term preContract = - fop.getPre(heaps, selfVar, paramVars, atPreVars, services); + fop.getPre(heaps, selfVar, paramVars, atPreVars, services); if (preContract == null) { preContract = tb.tt(); } @@ -1194,11 +1179,11 @@ private ImmutableSet getModelMethodAxioms() { // (pm.isProtected() ? new Protected() : // (pm.isPublic() ? new Public() : null)); final ClassAxiom modelMethodRepresentsAxiom = - new RepresentsAxiom( - "Definition axiom for " + pm.getName() + " in " - + kjt.getFullName(), - pm, kjt, new Private(), preContract, representsFromContract, - selfVar, paramVars, atPreVars); + new RepresentsAxiom( + "Definition axiom for " + pm.getName() + " in " + + kjt.getFullName(), + pm, kjt, new Private(), preContract, representsFromContract, + selfVar, paramVars, atPreVars); result = result.add(modelMethodRepresentsAxiom); break; } @@ -1208,24 +1193,24 @@ pm, kjt, new Private(), preContract, representsFromContract, continue; } Term preFromContract = - fop.getPre(heaps, selfVar, paramVars, atPreVars, services); + fop.getPre(heaps, selfVar, paramVars, atPreVars, services); Term freePreFromContract = - fop.getFreePre(heaps, selfVar, paramVars, atPreVars, services); + fop.getFreePre(heaps, selfVar, paramVars, atPreVars, services); Term postFromContract = fop.getPost(heaps, selfVar, paramVars, resultVar, - null, atPreVars, services); + null, atPreVars, services); Term freePostFromContract = fop.getFreePost(heaps, selfVar, paramVars, - resultVar, null, atPreVars, services); + resultVar, null, atPreVars, services); if (preFromContract != null && ((postFromContract != null && postFromContract != tb.tt()) - || (freePostFromContract != null - && freePostFromContract != tb.tt()))) { + || (freePostFromContract != null + && freePostFromContract != tb.tt()))) { Term mbyFromContract = - fop.hasMby() ? fop.getMby(selfVar, paramVars, services) : null; + fop.hasMby() ? fop.getMby(selfVar, paramVars, services) : null; final ClassAxiom modelMethodContractAxiom = new ContractAxiom( - "Contract axiom for " + pm.getName() + " in " + kjt.getName(), pm, - kjt, new Private(), preFromContract, freePreFromContract, - postFromContract, freePostFromContract, mbyFromContract, atPreVars, - selfVar, resultVar, paramVars); + "Contract axiom for " + pm.getName() + " in " + kjt.getName(), pm, + kjt, new Private(), preFromContract, freePreFromContract, + postFromContract, freePostFromContract, mbyFromContract, atPreVars, + selfVar, resultVar, paramVars); result = result.add(modelMethodContractAxiom); } } @@ -1326,7 +1311,7 @@ public ImmutableSet getProofs(Contract atomicContract) { */ public ImmutableSet getProofs(KeYJavaType kjt, IObserverFunction target) { final ImmutableSet> targets = - getOverridingTargets(kjt, target).add(new Pair<>(kjt, target)); + getOverridingTargets(kjt, target).add(new Pair<>(kjt, target)); ImmutableSet result = DefaultImmutableSet.nil(); for (Map.Entry> entry : proofs.entrySet()) { final ProofOblInput po = entry.getKey(); @@ -1334,7 +1319,7 @@ public ImmutableSet getProofs(KeYJavaType kjt, IObserverFunction target) if (po instanceof ContractPO) { final Contract contract = ((ContractPO) po).getContract(); final Pair pair = - new Pair<>(contract.getKJT(), contract.getTarget()); + new Pair<>(contract.getKJT(), contract.getTarget()); if (targets.contains(pair)) { result = result.union(sop); } @@ -1493,8 +1478,7 @@ 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 +1494,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(); @@ -1552,7 +1535,7 @@ public ImmutableSet getMergeContracts(MergePointStatement mps) { * @param modalityKind the given modality. */ public ImmutableSet getBlockContracts(final StatementBlock block, - final Modality.JavaModalityKind modalityKind) { + final Modality.JavaModalityKind modalityKind) { ImmutableSet result = getBlockContracts(block); final Modality.JavaModalityKind matchModality = getMatchModalityKind(modalityKind); for (BlockContract contract : result) { @@ -1565,7 +1548,7 @@ public ImmutableSet getBlockContracts(final StatementBlock block, } public ImmutableSet getLoopContracts(final StatementBlock block, - final Modality.JavaModalityKind modalityKind) { + final Modality.JavaModalityKind modalityKind) { ImmutableSet result = getLoopContracts(block); final Modality.JavaModalityKind matchModality = getMatchModalityKind(modalityKind); for (LoopContract contract : result) { @@ -1585,7 +1568,7 @@ public ImmutableSet getLoopContracts(final StatementBlock block, * @return the set of resulting loop statements. */ public ImmutableSet getLoopContracts(final LoopStatement loop, - final Modality.JavaModalityKind modalityKind) { + final Modality.JavaModalityKind modalityKind) { ImmutableSet result = getLoopContracts(loop); final Modality.JavaModalityKind matchModality = getMatchModalityKind(modalityKind); for (LoopContract contract : result) { @@ -1615,8 +1598,7 @@ 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 +1619,9 @@ 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,13 +1643,12 @@ 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(); final Pair b = - new Pair<>(loop, loop.getStartPosition().line()); + new Pair<>(loop, loop.getStartPosition().line()); loopContractsOnLoops.put(b, getLoopContracts(loop).add(contract)); } @@ -1696,18 +1675,15 @@ 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()); + 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)); } } @@ -1771,11 +1747,11 @@ public Pair> limitObs(IObserverFunction if (limited == null) { final String baseName = - ((ProgramElementName) obs.name()).getProgramName() + LIMIT_SUFFIX; + ((ProgramElementName) obs.name()).getProgramName() + LIMIT_SUFFIX; final Sort heapSort = services.getTypeConverter().getHeapLDT().targetSort(); limited = new ObserverFunction(baseName, obs.sort(), obs.getType(), heapSort, - obs.getContainerType(), obs.isStatic(), obs.getParamTypes(), - obs.getHeapCount(services), obs.getStateCount()); + obs.getContainerType(), obs.isStatic(), obs.getParamTypes(), + obs.getHeapCount(services), obs.getStateCount()); unlimitedToLimited.put(obs, limited); limitedToUnlimited.put(limited, obs); @@ -1890,7 +1866,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}. @@ -1944,5 +1920,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 ec13b8c4c9c..c82f3103c63 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,13 +561,12 @@ private Term useCaseFormula(TermLabelState termLabelState, Services services, Ru Term restPsi = tb.prog(mod.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, - final KeYJavaType booleanKJT, LoopInvariantBuiltInRuleApp loopRuleApp, - final TermServices services) { + private Guard prepareGuard(final Instantiation inst, + final KeYJavaType booleanKJT, LoopInvariantBuiltInRuleApp loopRuleApp, + final TermServices services) { final TermBuilder tb = services.getTermBuilder(); final ProgramElementName guardVarName = new ProgramElementName(tb.newName("b")); final LocationVariable guardVar = new LocationVariable(guardVarName, booleanKJT); @@ -592,9 +583,11 @@ 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); } + private record Guard(JavaBlock first, Term second, Term third) {} + private void prepareInvInitiallyValidBranch(TermLabelState termLabelState, Services services, RuleApp ruleApp, Instantiation inst, final Term invTerm, Term reachableState, Goal initGoal) { @@ -751,7 +744,7 @@ public ImmutableList apply(Goal goal, Services services, final RuleApp rul 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; @@ -991,48 +984,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 8b3ad769444..db812dda262 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; @@ -166,7 +165,7 @@ public final ImmutableList apply(Goal goal, final Services services, RuleA // The merge loop SymbolicExecutionState mergedState = - new SymbolicExecutionState(thisSEState.first, thisSEState.second, newGoal.node()); + new SymbolicExecutionState(thisSEState.first(), thisSEState.second(), newGoal.node()); LinkedHashSet newNames = new LinkedHashSet<>(); LinkedHashSet sideConditionsToProve = new LinkedHashSet<>(); HashMap mergePartnerNodesToStates = new HashMap<>(); @@ -183,8 +182,8 @@ public final ImmutableList apply(Goal goal, final Services services, RuleA mergePartnerNodesToStates.put(state.getCorrespondingNode(), state); - Triple, LinkedHashSet> mergeResult = - mergeStates(mergeRule, mergedState, state, thisSEState.third, + MergeStateEntry mergeResult = + mergeStates(mergeRule, mergedState, state, thisSEState.third(), mergeRuleApp.getDistinguishingFormula(), services); newNames.addAll(mergeResult.second); sideConditionsToProve.addAll(mergeResult.third); @@ -207,7 +206,7 @@ public final ImmutableList apply(Goal goal, final Services services, RuleA for (MergePartner mergePartner : mergePartners) { closeMergePartnerGoal(newGoal.node(), mergePartner.getGoal(), mergePartner.getPio(), mergedState, mergePartnerNodesToStates.get(mergePartner.getGoal().node()), - thisSEState.third, newNames); + thisSEState.third(), newNames); } // Delete previous sequents @@ -240,7 +239,7 @@ public final ImmutableList apply(Goal goal, final Services services, RuleA } // Add new succedent (symbolic state & program counter) - final Term succedentFormula = tb.apply(mergedState.first, thisSEState.third); + final Term succedentFormula = tb.apply(mergedState.first, thisSEState.third()); final SequentFormula newSuccedent = new SequentFormula(succedentFormula); newGoal.addFormula(newSuccedent, new PosInOccurrence(newSuccedent, PosInTerm.getTopLevel(), false)); @@ -258,7 +257,7 @@ public final ImmutableList apply(Goal goal, final Services services, RuleA } // 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,22 +291,22 @@ public final ImmutableList apply(Goal goal, final Services services, RuleA * 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. - * @param state1 First state to merge. - * @param state2 Second state to merge. - * @param programCounter The formula \<{ ... }\> phi consisting of the common program - * counter and the post condition. + * @param mergeRule The merge procedure to use for the merge. + * @param state1 First state to merge. + * @param state2 Second state to merge. + * @param programCounter The formula \<{ ... }\> phi consisting of the common program + * counter and the post condition. * @param distinguishingFormula The user-specified distinguishing formula. May be null (for - * automatic generation). - * @param services The services object. + * automatic generation). + * @param services The services object. * @return A new merged SE state (U*,C*) which is a weakening of the original states. */ @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) { @@ -438,7 +437,7 @@ protected Triple, LinkedHashSet( + return new MergeStateEntry( new SymbolicExecutionState(newSymbolicState, newAdditionalConstraints == null ? newPathCondition : tb.and(newPathCondition, @@ -648,7 +647,7 @@ public static boolean isOfAdmissibleForm(Goal goal, PosInOccurrence pio, return false; } - return !doMergePartnerCheck || findPotentialMergePartners(goal, pio).size() > 0; + return !doMergePartnerCheck || !findPotentialMergePartners(goal, pio).isEmpty(); } @@ -676,7 +675,7 @@ 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 +691,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.third().equals(partnerSEState.third())) { potentialPartners = potentialPartners.prepend(new MergePartner(g, gPio)); @@ -714,4 +713,6 @@ public interface MergeRuleProgressListener { void signalProgress(int progress); } + public record MergeStateEntry(SymbolicExecutionState first, LinkedHashSet second, + LinkedHashSet third) {} } 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 8e1c587feba..17d64a0d76a 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 @@ -20,9 +20,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; @@ -193,22 +193,22 @@ public DependencyContract dep(KeYJavaType containerType, IObserverFunction pm, } public DependencyContract dep(KeYJavaType kjt, LocationVariable targetHeap, - Triple dep, ProgramVariable selfVar) { - final ImmutableList paramVars = tb.paramVars(dep.first, false); - assert (selfVar == null) == dep.first.isStatic(); + TranslatedDependencyContract dep, ProgramVariable selfVar) { + final ImmutableList paramVars = tb.paramVars(dep.first(), false); + assert (selfVar == null) == dep.first().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 (LocationVariable heap : HeapContext.getModHeaps(services, false)) { if (heap == targetHeap) { - accessibles.put(heap, dep.second); + accessibles.put(heap, dep.second()); } 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.first(), dep.first().getContainerType(), pres, dep.third(), 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 e1bbae2f358..8371394e48a 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; @@ -195,9 +194,11 @@ public void addRequires(LabeledParserRuleContext label) { addClause(REQUIRES, label); } - public Triple[] getAbbreviations() { + public record Abbreviation(LabeledParserRuleContext first, LabeledParserRuleContext second, LabeledParserRuleContext thrid){} + + 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 f80ff858970..9cf9d03a442 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; @@ -827,7 +826,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)); } 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 288c7a061d9..5c8d2a0f189 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 @@ -19,7 +19,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; @@ -303,9 +302,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); } /** @@ -315,8 +313,7 @@ public Triple translateDependencyContract( * * @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 c04b662a9e7..2547e1f32aa 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; @@ -1031,8 +1030,7 @@ public Pair represents(SLExpression lhs, Term t) { return new Pair<>((IObserverFunction) lhs.getTerm().op(), t); } - public Triple depends(SLExpression lhs, Term rhs, - SLExpression mby) { + public TranslatedDependencyContract depends(SLExpression lhs, Term rhs, SLExpression mby) { LocationVariable heap = services.getTypeConverter().getHeapLDT().getHeap(); if (!lhs.isTerm()) { 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..983d03b0f7f --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/TranslatedDependencyContract.java @@ -0,0 +1,12 @@ +package de.uka.ilkd.key.speclang.njml; + +import de.uka.ilkd.key.logic.Term; +import de.uka.ilkd.key.logic.op.IObserverFunction; + +/** + * + * @author Alexander Weigl + * @version 1 (23.04.24) + */ +public record TranslatedDependencyContract(IObserverFunction first, Term second, Term third) { +} 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..5e1ba42bb90 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,9 @@ * @see StrategyPropertyValueDefinition */ public class StrategySettingsDefinition { + public record StategySettingEntry(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 +74,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 StategySettingEntry( "Java verif. std.", 7000, () -> { final StrategyProperties newProps = IDefaultStrategyPropertiesFactory.DEFAULT_FACTORY @@ -124,7 +123,7 @@ public class StrategySettingsDefinition { })); // Simplification preset - STD_FURTHER_DEFAULTS.add(new Triple<>( + STD_FURTHER_DEFAULTS.add(new StategySettingEntry( "Simplification", 5000, () -> { final StrategyProperties newProps = IDefaultStrategyPropertiesFactory.DEFAULT_FACTORY @@ -197,7 +196,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 +271,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/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 a3750cf89e5..9059d07e207 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; @@ -652,7 +651,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()) { @@ -1096,11 +1095,11 @@ 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.first(), partnerSEState.second(), node)); } return result; @@ -1375,7 +1374,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..f4ec6a50bd3 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,7 +7,7 @@ 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 @@ -17,10 +17,8 @@ * * @author Dominic Scheurer */ -public class SymbolicExecutionStateWithProgCnt extends Triple { - - private Node correspondingNode = null; - +public record SymbolicExecutionStateWithProgCnt(Term first, Term second, Term third, + @Nullable Node correspondingNode) { /** * @param symbolicState The symbolic state (parallel update). * @param pathCondition The path condition (formula). 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 400c0bf393a..3d1a1d7aaef 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 @@ -69,9 +69,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..8966026c803 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,6 +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.nparser.ProofScriptEntry; import de.uka.ilkd.key.parser.Location; import de.uka.ilkd.key.proof.Proof; import de.uka.ilkd.key.proof.io.AbstractProblemLoader; @@ -197,7 +198,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..d7aa7c78ee0 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..25d5dedd8fc 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..b17ae902c0b 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,8 @@ private JPanel createDefaultPanel(StrategySelectionComponents components) { existingPredefs[0] = "Defaults"; int i = 1; - for (Triple furtherDefault : DEFINITION - .getFurtherDefaults()) { - existingPredefs[i] = furtherDefault.first; + for (StrategySettingsDefinition.StategySettingEntry furtherDefault : DEFINITION.getFurtherDefaults()) { + existingPredefs[i] = furtherDefault.name(); i++; } @@ -425,10 +423,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 f9066745de7..8f8e4f96993 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/WindowUserInterfaceControl.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/WindowUserInterfaceControl.java @@ -24,7 +24,7 @@ import de.uka.ilkd.key.gui.notification.events.NotificationEvent; import de.uka.ilkd.key.macros.ProofMacro; import de.uka.ilkd.key.macros.ProofMacroFinishedInfo; -import de.uka.ilkd.key.parser.Location; +import de.uka.ilkd.key.nparser.ProofScriptEntry; import de.uka.ilkd.key.proof.Goal; import de.uka.ilkd.key.proof.Proof; import de.uka.ilkd.key.proof.ProofAggregate; @@ -237,11 +237,11 @@ private void taskFinishedInternal(TaskFinishedInfo info) { KeYMediator mediator = mainWindow.getMediator(); mediator.getNotationInfo().refresh(mediator.getServices()); if (problemLoader.hasProofScript()) { - Pair scriptAndLoc; + ProofScriptEntry scriptAndLoc; try { scriptAndLoc = problemLoader.readProofScript(); ProofScriptWorker psw = new ProofScriptWorker(mainWindow.getMediator(), - scriptAndLoc.first, scriptAndLoc.second); + scriptAndLoc.script(), scriptAndLoc.location()); psw.init(); psw.execute(); } catch (ProofInputException e) { 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..02385e81654 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,33 @@ static String findAndPopNearestMatch(String l, List right) { return current; } + public 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 (!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/keyext.slicing/src/main/java/org/key_project/slicing/RuleStatistics.java b/keyext.slicing/src/main/java/org/key_project/slicing/RuleStatistics.java index f011f4e5601..30ada1c137a 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 @@ -4,7 +4,6 @@ package org.key_project.slicing; import de.uka.ilkd.key.rule.Rule; -import de.uka.ilkd.key.util.Triple; import java.util.Comparator; import java.util.HashMap; @@ -23,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. */ @@ -39,9 +38,9 @@ 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)); } /** @@ -54,9 +53,9 @@ 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)); } /** @@ -69,9 +68,9 @@ 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)); } /** @@ -84,8 +83,8 @@ public void addInitialUselessApplication(Rule rule, boolean branches) { */ public List sortBy(Comparator comparator) { return map.entrySet().stream() - .map(entry -> new RuleStatisticEntry(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()); } @@ -100,6 +99,9 @@ public boolean branches(String 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 @@ -107,4 +109,12 @@ public boolean branches(String rule) { */ 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/graph/DependencyGraph.java b/keyext.slicing/src/main/java/org/key_project/slicing/graph/DependencyGraph.java index 02f109322a2..320c5d43756 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; @@ -120,16 +119,18 @@ public Stream incomingEdgesOf(GraphNode node) { return graph.incomingEdgesOf(node).stream().map(AnnotatedEdge::getProofStep); } + public record IncomingEdge(Node first, GraphNode second, AnnotatedEdge third){} + /** * @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 IncomingEdge(edge.getProofStep(), graph.getEdgeSource(edge), edge)); } /** @@ -147,12 +148,12 @@ public Stream outgoingEdgesOf(GraphNode 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 IncomingEdge(edge.getProofStep(), graph.getEdgeTarget(edge), edge)); } /** 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..320042ea01b 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,12 @@ 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; +import org.key_project.slicing.graph.DependencyGraph.IncomingEdge; import org.key_project.slicing.graph.GraphNode; import org.key_project.util.collection.Pair; @@ -72,17 +73,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.first()); + graphNodes.add(n.second()); + var ruleName = n.first().getAppliedRuleApp().rule().displayName(); return List.of( - Integer.toString(n.first.serialNr()), - analysisResults != null && !analysisResults.usefulSteps.contains(n.first) + Integer.toString(n.first().serialNr()), + analysisResults != null && !analysisResults.usefulSteps.contains(n.first()) ? "" + ruleName + "" : ruleName, - n.third.replacesInputNode() ? "yes" : "no", - n.second.toString(false, false)); + n.third().replacesInputNode() ? "yes" : "no", + n.second().toString(false, false)); }; var idxFactory = new IndexFactory(); @@ -99,7 +100,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.first())).count() : -1; var extraInfo = useful != -1 ? "

" + useful + " useful rule apps

" : ""; var previousDerivations = 0;