diff --git a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/rule/label/BlockContractValidityTermLabelUpdate.java b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/rule/label/BlockContractValidityTermLabelUpdate.java index 88408fc4a4f..973d0456e8d 100644 --- a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/rule/label/BlockContractValidityTermLabelUpdate.java +++ b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/rule/label/BlockContractValidityTermLabelUpdate.java @@ -5,19 +5,15 @@ import java.util.Set; -import de.uka.ilkd.key.java.Services; import de.uka.ilkd.key.logic.JTerm; import de.uka.ilkd.key.logic.label.BlockContractValidityTermLabel; import de.uka.ilkd.key.logic.label.TermLabel; -import de.uka.ilkd.key.logic.label.TermLabelState; +import de.uka.ilkd.key.logic.label.TermLabelContext; import de.uka.ilkd.key.rule.BlockContractInternalRule; import de.uka.ilkd.key.rule.LoopContractInternalRule; import de.uka.ilkd.key.symbolic_execution.util.SymbolicExecutionUtil; import org.key_project.logic.Name; -import org.key_project.prover.rules.Rule; -import org.key_project.prover.rules.RuleApp; -import org.key_project.prover.sequent.PosInOccurrence; import org.key_project.util.collection.ImmutableList; import org.key_project.util.java.CollectionUtil; @@ -40,18 +36,17 @@ public ImmutableList getSupportedRuleNames() { * {@inheritDoc} */ @Override - public void updateLabels(TermLabelState state, Services services, - PosInOccurrence applicationPosInOccurrence, JTerm applicationTerm, JTerm modalityTerm, - Rule rule, RuleApp ruleApp, Object hint, JTerm tacletTerm, JTerm newTerm, - Set labels) { - if ((rule instanceof BlockContractInternalRule || rule instanceof LoopContractInternalRule) - && ((BlockContractInternalRule.BlockContractHint) hint) + public void updateLabels(TermLabelContext context, JTerm newTerm, Set labels) { + if ((context.rule() instanceof BlockContractInternalRule + || context.rule() instanceof LoopContractInternalRule) + && ((BlockContractInternalRule.BlockContractHint) context.hint()) .getExceptionalVariable() != null - && SymbolicExecutionUtil.hasSymbolicExecutionLabel(modalityTerm)) { + && SymbolicExecutionUtil.hasSymbolicExecutionLabel(context.modalityTerm())) { if (CollectionUtil.search(labels, element -> element instanceof BlockContractValidityTermLabel) == null) { labels.add(new BlockContractValidityTermLabel( - ((BlockContractInternalRule.BlockContractHint) hint).getExceptionalVariable())); + ((BlockContractInternalRule.BlockContractHint) context.hint()) + .getExceptionalVariable())); } } } diff --git a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/rule/label/FormulaTermLabelRefactoring.java b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/rule/label/FormulaTermLabelRefactoring.java index c9607d88c29..e9c48f72845 100644 --- a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/rule/label/FormulaTermLabelRefactoring.java +++ b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/rule/label/FormulaTermLabelRefactoring.java @@ -10,6 +10,7 @@ import de.uka.ilkd.key.logic.label.FormulaTermLabel; import de.uka.ilkd.key.logic.label.LabelCollection; import de.uka.ilkd.key.logic.label.TermLabel; +import de.uka.ilkd.key.logic.label.TermLabelContext; import de.uka.ilkd.key.logic.label.TermLabelState; import de.uka.ilkd.key.proof.Goal; import de.uka.ilkd.key.proof.Proof; @@ -112,19 +113,17 @@ public ImmutableList getSupportedRuleNames() { * {@inheritDoc} */ @Override - public RefactoringScope defineRefactoringScope(TermLabelState state, Services services, - PosInOccurrence applicationPosInOccurrence, - JTerm applicationTerm, Rule rule, Goal goal, - Object hint, JTerm tacletTerm) { - if (shouldRefactorSpecificationApplication(rule, goal, hint)) { + public RefactoringScope defineRefactoringScope(TermLabelContext context) { + if (shouldRefactorSpecificationApplication(context.rule(), context.goal(), + context.hint())) { return RefactoringScope.APPLICATION_CHILDREN_AND_GRANDCHILDREN_SUBTREE; - } else if (isParentRefactoringRequired(state)) { + } else if (isParentRefactoringRequired(context.state())) { return RefactoringScope.APPLICATION_CHILDREN_AND_GRANDCHILDREN_SUBTREE_AND_PARENTS; - } else if (isUpdateRefactoringRequired(state)) { + } else if (isUpdateRefactoringRequired(context.state())) { return RefactoringScope.APPLICATION_BELOW_UPDATES; - } else if (containsSequentFormulasToRefactor(state)) { + } else if (containsSequentFormulasToRefactor(context.state())) { return RefactoringScope.SEQUENT; - } else if (SyntacticalReplaceVisitor.SUBSTITUTION_WITH_LABELS_HINT.equals(hint)) { + } else if (SyntacticalReplaceVisitor.SUBSTITUTION_WITH_LABELS_HINT.equals(context.hint())) { return RefactoringScope.APPLICATION_BELOW_UPDATES; } else { return RefactoringScope.NONE; @@ -147,20 +146,19 @@ private boolean shouldRefactorSpecificationApplication(Rule rule, Goal goal, Obj * {@inheritDoc} */ @Override - public void refactorLabels(TermLabelState state, Services services, - PosInOccurrence applicationPosInOccurrence, - JTerm applicationTerm, Rule rule, Goal goal, - Object hint, JTerm tacletTerm, JTerm term, LabelCollection labels) { - if (shouldRefactorSpecificationApplication(rule, goal, hint)) { - refactorSpecificationApplication(term, services, labels, hint); - } else if (isParentRefactoringRequired(state)) { - refactorInCaseOfNewIdRequired(state, goal, term, services, labels); - } else if (isUpdateRefactoringRequired(state)) { - refactorBelowUpdates(applicationPosInOccurrence, term, labels); - } else if (containsSequentFormulasToRefactor(state)) { - refactorSequentFormulas(state, services, term, labels); - } else if (SyntacticalReplaceVisitor.SUBSTITUTION_WITH_LABELS_HINT.equals(hint)) { - refactorSubstitution(term, tacletTerm, labels); + public void refactorLabels(TermLabelContext context, JTerm term, LabelCollection labels) { + if (shouldRefactorSpecificationApplication(context.rule(), context.goal(), + context.hint())) { + refactorSpecificationApplication(term, context.services(), labels, context.hint()); + } else if (isParentRefactoringRequired(context.state())) { + refactorInCaseOfNewIdRequired(context.state(), context.goal(), term, context.services(), + labels); + } else if (isUpdateRefactoringRequired(context.state())) { + refactorBelowUpdates(context.applicationPosInOccurrence(), term, labels); + } else if (containsSequentFormulasToRefactor(context.state())) { + refactorSequentFormulas(context.state(), context.services(), term, labels); + } else if (SyntacticalReplaceVisitor.SUBSTITUTION_WITH_LABELS_HINT.equals(context.hint())) { + refactorSubstitution(term, context.tacletTerm(), labels); } } diff --git a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/rule/label/FormulaTermLabelUpdate.java b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/rule/label/FormulaTermLabelUpdate.java index d80e5fe0a9f..147c4acce62 100644 --- a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/rule/label/FormulaTermLabelUpdate.java +++ b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/rule/label/FormulaTermLabelUpdate.java @@ -9,22 +9,18 @@ import java.util.Map.Entry; import java.util.Set; -import de.uka.ilkd.key.java.Services; import de.uka.ilkd.key.logic.*; import de.uka.ilkd.key.logic.label.FormulaTermLabel; import de.uka.ilkd.key.logic.label.TermLabel; +import de.uka.ilkd.key.logic.label.TermLabelContext; import de.uka.ilkd.key.logic.label.TermLabelManager; -import de.uka.ilkd.key.logic.label.TermLabelState; import de.uka.ilkd.key.rule.Taclet.TacletLabelHint; import de.uka.ilkd.key.rule.Taclet.TacletLabelHint.TacletOperation; import de.uka.ilkd.key.rule.TacletApp; import de.uka.ilkd.key.symbolic_execution.TruthValueTracingUtil; import org.key_project.logic.Name; -import org.key_project.prover.rules.Rule; -import org.key_project.prover.rules.RuleApp; import org.key_project.prover.rules.instantiation.AssumesFormulaInstantiation; -import org.key_project.prover.sequent.PosInOccurrence; import org.key_project.prover.sequent.SequentFormula; import org.key_project.util.collection.ImmutableList; import org.key_project.util.java.CollectionUtil; @@ -48,12 +44,8 @@ public ImmutableList getSupportedRuleNames() { * {@inheritDoc} */ @Override - public void updateLabels(TermLabelState state, Services services, - PosInOccurrence applicationPosInOccurrence, - JTerm applicationTerm, JTerm modalityTerm, - Rule rule, RuleApp ruleApp, Object hint, JTerm tacletTerm, JTerm newTerm, - Set labels) { - if (hint instanceof TacletLabelHint tacletHint) { + public void updateLabels(TermLabelContext context, JTerm newTerm, Set labels) { + if (context.hint() instanceof TacletLabelHint tacletHint) { if ((TacletOperation.ADD_ANTECEDENT.equals(tacletHint.getTacletOperation()) || TacletOperation.ADD_SUCCEDENT.equals(tacletHint.getTacletOperation())) && (TruthValueTracingUtil.isPredicate(newTerm) @@ -61,20 +53,22 @@ public void updateLabels(TermLabelState state, Services services, newTerm.subs()))) { if (getTermLabel(labels, FormulaTermLabel.NAME) == null) { TermLabel label = TermLabelManager.findInnerMostParentLabel( - applicationPosInOccurrence, FormulaTermLabel.NAME); + context.applicationPosInOccurrence(), FormulaTermLabel.NAME); if (label instanceof FormulaTermLabel oldLabel) { - int labelSubID = FormulaTermLabel.newLabelSubID(services, oldLabel); + int labelSubID = + FormulaTermLabel.newLabelSubID(context.services(), oldLabel); FormulaTermLabel newLabel = new FormulaTermLabel(oldLabel.getMajorId(), labelSubID, Collections.singletonList(oldLabel.getId())); labels.add(newLabel); // Let the PredicateTermLabelRefactoring perform the refactoring, see also // PredicateTermLabelRefactoring#PARENT_REFACTORING_REQUIRED - FormulaTermLabelRefactoring.setParentRefactoringRequired(state, true); + FormulaTermLabelRefactoring.setParentRefactoringRequired(context.state(), + true); } } } } - if (ruleApp instanceof TacletApp ta) { + if (context.ruleApp() instanceof TacletApp ta) { if (ta.assumesInstantionsComplete() && ta.assumesFormulaInstantiations() != null) { Map ifLabels = new LinkedHashMap<>(); @@ -92,11 +86,12 @@ public void updateLabels(TermLabelState state, Services services, for (Entry ifEntry : ifLabels .entrySet()) { FormulaTermLabel ifLabel = ifEntry.getValue(); - int labelSubID = FormulaTermLabel.newLabelSubID(services, ifLabel); + int labelSubID = + FormulaTermLabel.newLabelSubID(context.services(), ifLabel); FormulaTermLabel newLabel = new FormulaTermLabel(ifLabel.getMajorId(), labelSubID, Collections.singletonList(ifLabel.getId())); labels.add(newLabel); - FormulaTermLabelRefactoring.addSequentFormulaToRefactor(state, + FormulaTermLabelRefactoring.addSequentFormulaToRefactor(context.state(), ifEntry.getKey()); } } diff --git a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/rule/label/LoopBodyTermLabelUpdate.java b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/rule/label/LoopBodyTermLabelUpdate.java index 70faae66f69..097d368dc88 100644 --- a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/rule/label/LoopBodyTermLabelUpdate.java +++ b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/rule/label/LoopBodyTermLabelUpdate.java @@ -5,17 +5,13 @@ import java.util.Set; -import de.uka.ilkd.key.java.Services; import de.uka.ilkd.key.logic.JTerm; import de.uka.ilkd.key.logic.label.TermLabel; -import de.uka.ilkd.key.logic.label.TermLabelState; +import de.uka.ilkd.key.logic.label.TermLabelContext; import de.uka.ilkd.key.rule.WhileInvariantRule; import de.uka.ilkd.key.symbolic_execution.util.SymbolicExecutionUtil; import org.key_project.logic.Name; -import org.key_project.prover.rules.Rule; -import org.key_project.prover.rules.RuleApp; -import org.key_project.prover.sequent.PosInOccurrence; import org.key_project.util.collection.ImmutableList; /** @@ -37,12 +33,10 @@ public ImmutableList getSupportedRuleNames() { * {@inheritDoc} */ @Override - public void updateLabels(TermLabelState state, Services services, - PosInOccurrence applicationPosInOccurrence, JTerm applicationTerm, JTerm modalityTerm, - Rule rule, RuleApp ruleApp, Object hint, JTerm tacletTerm, JTerm newTerm, - Set labels) { - if (rule instanceof WhileInvariantRule && "LoopBodyModality".equals(hint) - && SymbolicExecutionUtil.hasSymbolicExecutionLabel(modalityTerm)) { + public void updateLabels(TermLabelContext context, JTerm newTerm, Set labels) { + if (context.rule() instanceof WhileInvariantRule + && "LoopBodyModality".equals(context.hint()) + && SymbolicExecutionUtil.hasSymbolicExecutionLabel(context.modalityTerm())) { labels.add(SymbolicExecutionUtil.LOOP_BODY_LABEL); } } diff --git a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/rule/label/LoopInvariantNormalBehaviorTermLabelUpdate.java b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/rule/label/LoopInvariantNormalBehaviorTermLabelUpdate.java index d5022ed9661..307c316f5ee 100644 --- a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/rule/label/LoopInvariantNormalBehaviorTermLabelUpdate.java +++ b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/rule/label/LoopInvariantNormalBehaviorTermLabelUpdate.java @@ -5,17 +5,13 @@ import java.util.Set; -import de.uka.ilkd.key.java.Services; import de.uka.ilkd.key.logic.JTerm; import de.uka.ilkd.key.logic.label.TermLabel; -import de.uka.ilkd.key.logic.label.TermLabelState; +import de.uka.ilkd.key.logic.label.TermLabelContext; import de.uka.ilkd.key.rule.WhileInvariantRule; import de.uka.ilkd.key.symbolic_execution.util.SymbolicExecutionUtil; import org.key_project.logic.Name; -import org.key_project.prover.rules.Rule; -import org.key_project.prover.rules.RuleApp; -import org.key_project.prover.sequent.PosInOccurrence; import org.key_project.util.collection.ImmutableList; /** @@ -37,12 +33,10 @@ public ImmutableList getSupportedRuleNames() { * {@inheritDoc} */ @Override - public void updateLabels(TermLabelState state, Services services, - PosInOccurrence applicationPosInOccurrence, JTerm applicationTerm, JTerm modalityTerm, - Rule rule, RuleApp ruleApp, Object hint, JTerm tacletTerm, JTerm newTerm, - Set labels) { - if (rule instanceof WhileInvariantRule && "LoopBodyImplication".equals(hint) - && SymbolicExecutionUtil.hasSymbolicExecutionLabel(modalityTerm)) { + public void updateLabels(TermLabelContext context, JTerm newTerm, Set labels) { + if (context.rule() instanceof WhileInvariantRule + && "LoopBodyImplication".equals(context.hint()) + && SymbolicExecutionUtil.hasSymbolicExecutionLabel(context.modalityTerm())) { labels.add(SymbolicExecutionUtil.LOOP_INVARIANT_NORMAL_BEHAVIOR_LABEL); } } diff --git a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/rule/label/RemoveInCheckBranchesTermLabelRefactoring.java b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/rule/label/RemoveInCheckBranchesTermLabelRefactoring.java index 17064ef97bc..a40839c1dc2 100644 --- a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/rule/label/RemoveInCheckBranchesTermLabelRefactoring.java +++ b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/rule/label/RemoveInCheckBranchesTermLabelRefactoring.java @@ -3,12 +3,10 @@ * SPDX-License-Identifier: GPL-2.0-only */ package de.uka.ilkd.key.rule.label; -import de.uka.ilkd.key.java.Services; import de.uka.ilkd.key.logic.JTerm; import de.uka.ilkd.key.logic.label.LabelCollection; import de.uka.ilkd.key.logic.label.TermLabel; -import de.uka.ilkd.key.logic.label.TermLabelState; -import de.uka.ilkd.key.proof.Goal; +import de.uka.ilkd.key.logic.label.TermLabelContext; import de.uka.ilkd.key.rule.AbstractAuxiliaryContractRule; import de.uka.ilkd.key.rule.BlockContractExternalRule; import de.uka.ilkd.key.rule.BlockContractInternalRule; @@ -18,8 +16,6 @@ import de.uka.ilkd.key.rule.WhileInvariantRule; import org.key_project.logic.Name; -import org.key_project.prover.rules.Rule; -import org.key_project.prover.sequent.PosInOccurrence; import org.key_project.util.collection.ImmutableList; /** @@ -67,13 +63,10 @@ public ImmutableList getSupportedRuleNames() { * {@inheritDoc} */ @Override - public RefactoringScope defineRefactoringScope(TermLabelState state, Services services, - PosInOccurrence applicationPosInOccurrence, - JTerm applicationTerm, Rule rule, Goal goal, - Object hint, JTerm tacletTerm) { - if (goal != null) { - final String branchLabel = goal.node().getNodeInfo().getBranchLabel(); - return switch (rule) { + public RefactoringScope defineRefactoringScope(TermLabelContext context) { + if (context.goal() != null) { + final String branchLabel = context.goal().node().getNodeInfo().getBranchLabel(); + return switch (context.rule()) { case UseOperationContractRule ignored when (branchLabel.startsWith("Pre") || branchLabel.startsWith("Null reference")) -> RefactoringScope.SEQUENT; @@ -94,9 +87,7 @@ case UseOperationContractRule ignored when (branchLabel.startsWith("Pre") || * {@inheritDoc} */ @Override - public void refactorLabels(TermLabelState state, Services services, - PosInOccurrence applicationPosInOccurrence, JTerm applicationTerm, Rule rule, Goal goal, - Object hint, JTerm tacletTerm, JTerm term, LabelCollection labels) { + public void refactorLabels(TermLabelContext context, JTerm term, LabelCollection labels) { labels.removeIf(next -> termLabelNameToRemove.equals(next.name())); } } diff --git a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/rule/label/StayOnFormulaTermLabelPolicy.java b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/rule/label/StayOnFormulaTermLabelPolicy.java index 58c2c392fb2..25e755faec4 100644 --- a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/rule/label/StayOnFormulaTermLabelPolicy.java +++ b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/rule/label/StayOnFormulaTermLabelPolicy.java @@ -7,19 +7,15 @@ import java.util.LinkedHashSet; import java.util.Set; -import de.uka.ilkd.key.java.Services; import de.uka.ilkd.key.logic.JTerm; import de.uka.ilkd.key.logic.label.FormulaTermLabel; import de.uka.ilkd.key.logic.label.TermLabel; -import de.uka.ilkd.key.logic.label.TermLabelState; +import de.uka.ilkd.key.logic.label.TermLabelContext; import de.uka.ilkd.key.logic.op.*; -import de.uka.ilkd.key.proof.Goal; import de.uka.ilkd.key.rule.Taclet.TacletLabelHint; import de.uka.ilkd.key.rule.Taclet.TacletLabelHint.TacletOperation; import de.uka.ilkd.key.symbolic_execution.TruthValueTracingUtil; -import org.key_project.prover.rules.Rule; -import org.key_project.prover.sequent.PosInOccurrence; import org.key_project.util.collection.ImmutableArray; import org.key_project.util.java.CollectionUtil; @@ -33,10 +29,8 @@ public class StayOnFormulaTermLabelPolicy implements TermLabelPolicy { * {@inheritDoc} */ @Override - public TermLabel keepLabel(TermLabelState state, Services services, - PosInOccurrence applicationPosInOccurrence, JTerm applicationTerm, Rule rule, Goal goal, - Object hint, JTerm tacletTerm, - JTerm newTerm, TermLabel label) { + public TermLabel keepLabel(TermLabelContext context, JTerm sourceTerm, JTerm newTerm, + TermLabel label) { // Maintain label if new Term is a predicate if (TruthValueTracingUtil.isPredicate(newTerm.op()) || TruthValueTracingUtil.isLogicOperator(newTerm.op(), newTerm.subs())) { @@ -48,7 +42,7 @@ public TermLabel keepLabel(TermLabelState state, Services services, // May change sub ID if logical operators like junctors are used boolean newLabelIdRequired = false; Set originalLabelIds = new LinkedHashSet<>(); - if (hint instanceof TacletLabelHint tacletHint) { + if (context.hint() instanceof TacletLabelHint tacletHint) { if (isBelowIfThenElse(tacletHint.getTacletTermStack())) { return null; // Do not label children of if-then-else. They are labeled when a // rule rewrites them outside of the if-then-else. @@ -74,7 +68,7 @@ public TermLabel keepLabel(TermLabelState state, Services services, newLabelIdRequired = true; } } else if (tacletHint.getTerm() != null) { - boolean topLevel = isTopLevel(tacletHint, tacletTerm); + boolean topLevel = isTopLevel(tacletHint, context.tacletTerm()); if (!topLevel && !TruthValueTracingUtil.isPredicate(tacletHint.getTerm())) { newLabelIdRequired = true; } @@ -91,7 +85,8 @@ public TermLabel keepLabel(TermLabelState state, Services services, if (originalLabel != null) { originalLabelIds.add(originalLabel.getId()); } - int labelSubID = FormulaTermLabel.newLabelSubID(services, mostImportantLabel); + int labelSubID = + FormulaTermLabel.newLabelSubID(context.services(), mostImportantLabel); if (!originalLabelIds.isEmpty()) { return new FormulaTermLabel(mostImportantLabel.getMajorId(), labelSubID, originalLabelIds); @@ -110,13 +105,14 @@ public TermLabel keepLabel(TermLabelState state, Services services, JTerm target = newTerm.subs().get(UpdateApplication.targetPos()); TermLabel targetLabel = target.getLabel(FormulaTermLabel.NAME); if (targetLabel instanceof FormulaTermLabel) { - if (applicationPosInOccurrence != null) { - JTerm appliationTerm = (JTerm) applicationPosInOccurrence.subTerm(); + if (context.applicationPosInOccurrence() != null) { + JTerm appliationTerm = (JTerm) context.applicationPosInOccurrence().subTerm(); TermLabel applicationLabel = appliationTerm.getLabel(FormulaTermLabel.NAME); if (applicationLabel instanceof FormulaTermLabel) { // Let the PredicateTermLabelRefactoring perform the refactoring, see also // PredicateTermLabelRefactoring#UPDATE_REFACTORING_REQUIRED - FormulaTermLabelRefactoring.setUpdateRefactoringRequired(state, true); + FormulaTermLabelRefactoring.setUpdateRefactoringRequired(context.state(), + true); } } } diff --git a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/rule/label/SymbolicExecutionTermLabelUpdate.java b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/rule/label/SymbolicExecutionTermLabelUpdate.java index 381dada7ebe..f5398644b82 100644 --- a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/rule/label/SymbolicExecutionTermLabelUpdate.java +++ b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/rule/label/SymbolicExecutionTermLabelUpdate.java @@ -5,17 +5,13 @@ import java.util.Set; -import de.uka.ilkd.key.java.Services; import de.uka.ilkd.key.logic.JTerm; import de.uka.ilkd.key.logic.label.SymbolicExecutionTermLabel; import de.uka.ilkd.key.logic.label.TermLabel; -import de.uka.ilkd.key.logic.label.TermLabelState; +import de.uka.ilkd.key.logic.label.TermLabelContext; import de.uka.ilkd.key.rule.*; import org.key_project.logic.Name; -import org.key_project.prover.rules.Rule; -import org.key_project.prover.rules.RuleApp; -import org.key_project.prover.sequent.PosInOccurrence; import org.key_project.util.collection.ImmutableList; import org.key_project.util.java.CollectionUtil; @@ -42,20 +38,18 @@ public ImmutableList getSupportedRuleNames() { * {@inheritDoc} */ @Override - public void updateLabels(TermLabelState state, Services services, - PosInOccurrence applicationPosInOccurrence, JTerm applicationTerm, JTerm modalityTerm, - Rule rule, RuleApp ruleApp, Object hint, JTerm tacletTerm, - JTerm newTerm, - Set labels) { - if (rule instanceof WhileInvariantRule && "LoopBodyModality".equals(hint) - || (rule instanceof AbstractAuxiliaryContractRule - && ((AbstractBlockContractRule.BlockContractHint) hint) + public void updateLabels(TermLabelContext context, JTerm newTerm, Set labels) { + if (context.rule() instanceof WhileInvariantRule + && "LoopBodyModality".equals(context.hint()) + || (context.rule() instanceof AbstractAuxiliaryContractRule + && ((AbstractBlockContractRule.BlockContractHint) context.hint()) .getExceptionalVariable() != null)) { TermLabel label = CollectionUtil.searchAndRemove(labels, element -> element instanceof SymbolicExecutionTermLabel); if (label instanceof SymbolicExecutionTermLabel) { - int labelID = services.getCounter(SymbolicExecutionTermLabel.PROOF_COUNTER_NAME) - .getCountPlusPlus(); + int labelID = + context.services().getCounter(SymbolicExecutionTermLabel.PROOF_COUNTER_NAME) + .getCountPlusPlus(); labels.add(new SymbolicExecutionTermLabel(labelID)); } } diff --git a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/profile/SimplifyTermProfile.java b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/profile/SimplifyTermProfile.java index 00f9e5f051f..20af2c594a5 100644 --- a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/profile/SimplifyTermProfile.java +++ b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/profile/SimplifyTermProfile.java @@ -61,12 +61,10 @@ protected ImmutableList computeTermLabelConfiguration() ImmutableList result = super.computeTermLabelConfiguration(); ImmutableList symExcPolicies = ImmutableList.nil() - .prepend((state, services, applicationPosInOccurrence, applicationTerm, rule, - goal, hint, tacletTerm, - newTerm, label) -> label); + .prepend((context, sourceTerm, newTerm, label) -> label); result = result.prepend(new TermLabelConfiguration(SymbolicExecutionUtil.RESULT_LABEL_NAME, new SingletonLabelFactory<>(SymbolicExecutionUtil.RESULT_LABEL), null, - symExcPolicies, null, null, null, null, null)); + symExcPolicies, null, null, null)); return result; } diff --git a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/profile/SymbolicExecutionJavaProfile.java b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/profile/SymbolicExecutionJavaProfile.java index 021dd65a003..cac2c5d6f4a 100644 --- a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/profile/SymbolicExecutionJavaProfile.java +++ b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/profile/SymbolicExecutionJavaProfile.java @@ -168,19 +168,19 @@ public static ImmutableList getSymbolicExecutionTermLabe ImmutableList result = ImmutableList.nil(); result = result.prepend(new TermLabelConfiguration(BlockContractValidityTermLabel.NAME, - new BlockContractValidityTermLabelFactory(), null, symExcPolicies, null, null, bcUps, + new BlockContractValidityTermLabelFactory(), null, symExcPolicies, bcUps, bcRefs, null)); result = result.prepend(new TermLabelConfiguration(SymbolicExecutionUtil.LOOP_BODY_LABEL_NAME, new SingletonLabelFactory<>(SymbolicExecutionUtil.LOOP_BODY_LABEL), null, - symExcPolicies, null, null, lbUps, lbRefs, null)); + symExcPolicies, lbUps, lbRefs, null)); result = result.prepend(new TermLabelConfiguration( SymbolicExecutionUtil.LOOP_INVARIANT_NORMAL_BEHAVIOR_LABEL_NAME, new SingletonLabelFactory<>( SymbolicExecutionUtil.LOOP_INVARIANT_NORMAL_BEHAVIOR_LABEL), - null, symExcPolicies, null, null, nbUps, nbRefs, null)); + null, symExcPolicies, nbUps, nbRefs, null)); result = result.prepend(new TermLabelConfiguration(SymbolicExecutionTermLabel.NAME, - new SymbolicExecutionTermLabelFactory(), null, symExcPolicies, null, null, seUps, + new SymbolicExecutionTermLabelFactory(), null, symExcPolicies, seUps, seRefs, null)); if (predicateEvaluationEnabled) { ImmutableList predPolicies = @@ -190,7 +190,7 @@ public static ImmutableList getSymbolicExecutionTermLabe ImmutableList predRefs = ImmutableList .nil().prepend(new FormulaTermLabelRefactoring()); result = result.prepend(new TermLabelConfiguration(FormulaTermLabel.NAME, - new FormulaTermLabelFactory(), null, predPolicies, null, null, predUpdates, + new FormulaTermLabelFactory(), null, predPolicies, predUpdates, predRefs, new FormulaTermLabelMerger())); } return result; diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/ServiceCaches.java b/key.core/src/main/java/de/uka/ilkd/key/java/ServiceCaches.java index d8e7739c803..8e05563e558 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/ServiceCaches.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/ServiceCaches.java @@ -8,6 +8,7 @@ import java.util.WeakHashMap; import de.uka.ilkd.key.logic.JTerm; +import de.uka.ilkd.key.logic.StrictTermKey; import de.uka.ilkd.key.logic.label.OriginTermLabel.Origin; import de.uka.ilkd.key.proof.Node; import de.uka.ilkd.key.proof.PrefixTermTacletAppIndexCacheImpl.CacheKey; @@ -117,9 +118,11 @@ public class ServiceCaches implements SessionCaches { private final Map graphCache = new LRUCache<>(1000); /** - * Cache used by the TermFactory to avoid unnecessary creation of terms + * Cache used by the TermFactory to avoid unnecessary creation of terms. Keyed on + * {@link StrictTermKey} (label-sensitive equality) so that term labels are preserved and + * label variants are interned separately. */ - private final Map termCache = new LRUCache<>(20000); + private final Map termCache = new LRUCache<>(20000); /** * Cache used by TypeComparisonCondition @@ -162,9 +165,10 @@ public class ServiceCaches implements SessionCaches { /** * Cache used by {@link de.uka.ilkd.key.rule.label.OriginTermLabelRefactoring}: the * origins of a term and all its subterms. Terms are immutable, so the set never - * changes for a given term. + * changes for a given term. The key is label-sensitive ({@link StrictTermKey}) as the + * cached value is derived from the term's labels. */ - private final Map> subtermOriginsCache = new LRUCache<>(20000); + private final Map> subtermOriginsCache = new LRUCache<>(20000); /** @@ -182,7 +186,7 @@ public final Map getTermTacletAppIndexCache() { * * @return map from a term to the origins of the term and all its subterms */ - public final Map> getSubtermOriginsCache() { + public final Map> getSubtermOriginsCache() { return subtermOriginsCache; } @@ -214,7 +218,7 @@ public final Map getGraphCache() { return graphCache; } - public final Map getTermFactoryCache() { + public final Map getTermFactoryCache() { return termCache; } diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/JTerm.java b/key.core/src/main/java/de/uka/ilkd/key/logic/JTerm.java index 621b2b335e7..b201ee7e433 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/logic/JTerm.java +++ b/key.core/src/main/java/de/uka/ilkd/key/logic/JTerm.java @@ -118,6 +118,36 @@ public interface JTerm */ boolean containsJavaBlockRecursive(); + /** + * Checks if this {@link JTerm} or one of its direct or indirect children carries a + * {@link TermLabel}. Cached; used as a cheap guard by label-sensitive consumers since + * {@link #equals(Object)} ignores term labels. + * + * @return {@code true} iff a term label occurs anywhere in the term tree + */ + boolean containsLabelsRecursive(); + + /** + * Checks term equality including {@link TermLabel}s on this term and all subterms + * (labels compared as sets). This is the label-sensitive counterpart of + * {@link #equals(Object)}. + * + * @param o the object to compare with + * @return {@code true} iff {@code o} is a term syntactically equal to this one with equal + * label sets on all subterms + */ + boolean equalsIncludingLabels(Object o); + + /** + * A hash code consistent with {@link #equalsIncludingLabels(Object)}: two terms that are + * equal including labels have the same labeled hash code. Cached. This is the label-sensitive + * counterpart of {@link #hashCode()} and is used to key the term-factory cache so that label + * variants are interned separately (and hence still shared via {@code ==}). + * + * @return the label-sensitive hash code + */ + int labeledHashCode(); + /** * Checks if this {@link JTerm} or one of its direct or indirect children has a * {@link de.uka.ilkd.key.logic.op.Transformer} operator. Cached; used by diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/LabeledTermImpl.java b/key.core/src/main/java/de/uka/ilkd/key/logic/LabeledTermImpl.java deleted file mode 100644 index 4f1dba590ea..00000000000 --- a/key.core/src/main/java/de/uka/ilkd/key/logic/LabeledTermImpl.java +++ /dev/null @@ -1,170 +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.logic; - -import java.util.Objects; -import java.util.stream.Collectors; - -import de.uka.ilkd.key.logic.equality.EqualsModProperty; -import de.uka.ilkd.key.logic.equality.RenamingTermProperty; -import de.uka.ilkd.key.logic.label.TermLabel; - -import org.key_project.logic.Name; -import org.key_project.logic.Property; -import org.key_project.logic.op.Operator; -import org.key_project.logic.op.QuantifiableVariable; -import org.key_project.util.collection.ImmutableArray; -import org.key_project.util.java.CollectionUtil; - -/** - *

- * The labeled term class is used for terms that have a label attached. - *

- * - * Two labeled terms are equal if they have equal term structure and equal annotations. In contrast, - * the method {@link EqualsModProperty#equalsModProperty(Object, Property, Object[])} can be used to - * compare terms - * while ignoring certain - * given properties. E.g. by using {@link RenamingTermProperty#RENAMING_TERM_PROPERTY}, just the - * term structures modulo - * renaming are compared whilst ignoring annotations. * - * - * @see JTerm - * @see TermImpl - */ -public class LabeledTermImpl extends TermImpl { - - /** - * @see #getLabels() - */ - private final ImmutableArray labels; - - /** - * creates an instance of a labeled term. - * - * @param op the top level operator - * @param subs the Term that are the subterms of this term - * @param boundVars logic variables bound by the operator - * @param labels the term's labels (must not be null or empty) - * @param origin a String with origin information - */ - public LabeledTermImpl(Operator op, ImmutableArray subs, - ImmutableArray boundVars, - ImmutableArray labels, String origin) { - super(op, subs, boundVars); - assert labels != null : "Term labels must not be null"; - assert !labels.isEmpty() : "There must be at least one term label"; - this.labels = labels; - } - - /** - * creates an instance of a labeled term. - * - * @param op the top level operator - * @param subs the Term that are the subterms of this term - * @param boundVars logic variables bound by the operator - * @param labels the terms labels (must not be null or empty) - */ - public LabeledTermImpl(Operator op, ImmutableArray subs, - ImmutableArray boundVars, - ImmutableArray labels) { - super(op, subs, boundVars); - assert labels != null : "Term labels must not be null"; - assert !labels.isEmpty() : "There must be at least one term label"; - this.labels = labels; - } - - /** - * {@inheritDoc} - */ - @Override - public boolean hasLabels() { - return true; - } - - /** - * returns the labels attached to this term - */ - @Override - public ImmutableArray getLabels() { - return labels; - } - - @Override - public TermLabel getLabel(final Name termLabelName) { - return CollectionUtil.search(labels, - element -> Objects.equals(element.name(), termLabelName)); - } - - /** - * returns true if the given label is attached - * - * @param label the TermLabel for which to look (must not be null) - * @return true iff. the label is attached to this term - */ - @Override - public boolean containsLabel(TermLabel label) { - assert label != null : "Label must not be null"; - for (int i = 0, sz = labels.size(); i < sz; i++) { - if (label.equals(labels.get(i))) { - return true; - } - } - return false; - } - - @Override - public boolean equals(Object o) { - if (o == this) { - return true; - } - - if (o instanceof final LabeledTermImpl cmp) { - if (labels.size() != cmp.labels.size()) { - return false; - } - - if (!super.equals(o)) { - return false; - } - - if (labels.size() == cmp.labels.size()) { - for (int i = 0, sz = labels.size(); i < sz; i++) { - // this is not optimal, but as long as number of labels limited ok - if (!cmp.labels.contains(labels.get(i))) { - return false; - } - } - return true; - } - } - return false; - } - - @Override - public int computeHashCode() { - int hash = super.computeHashCode(); - for (int i = 0, sz = labels.size(); i < sz; i++) { - hash += 7 * labels.get(i).hashCode(); - } - return hash; - } - - @Override - public String toString() { - StringBuilder result = new StringBuilder(super.toString()); - - String labelsStr = labels.stream() - // .filter(TermLabel::isProofRelevant) - .map(TermLabel::toString).collect(Collectors.joining(", ")); - - if (!labelsStr.isEmpty()) { - result.append("<<"); - result.append(labelsStr); - result.append(">>"); - } - - return result.toString(); - } -} diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/StrictTermKey.java b/key.core/src/main/java/de/uka/ilkd/key/logic/StrictTermKey.java new file mode 100644 index 00000000000..ebbf7d4cc00 --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/logic/StrictTermKey.java @@ -0,0 +1,30 @@ +/* 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.logic; + +/** + * A map key wrapping a {@link JTerm} with label-sensitive equality. Since + * {@link JTerm#equals(Object)} ignores term labels, caches whose values depend on the labels of + * the keyed term must not conflate label variants; wrapping the key in this record restores the + * distinction via {@link JTerm#equalsIncludingLabels(Object)}. + * + *

+ * The hash code is the term's {@link JTerm#labeledHashCode() label-sensitive} hash code, so label + * variants land in different buckets just as they did when term equality itself was + * label-sensitive. + *

+ * + * @param term the term to use as a label-sensitive key (must not be null) + */ +public record StrictTermKey(JTerm term) { + @Override + public boolean equals(Object o) { + return o instanceof StrictTermKey other && term.equalsIncludingLabels(other.term); + } + + @Override + public int hashCode() { + return term.labeledHashCode(); + } +} diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/TermFactory.java b/key.core/src/main/java/de/uka/ilkd/key/logic/TermFactory.java index bdd83aacbe3..5a6d05c04a3 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/logic/TermFactory.java +++ b/key.core/src/main/java/de/uka/ilkd/key/logic/TermFactory.java @@ -29,7 +29,7 @@ public final class TermFactory { private static final ImmutableArray NO_SUBTERMS = new ImmutableArray<>(); - private final Map cache; + private final Map cache; // ------------------------------------------------------------------------- @@ -41,7 +41,7 @@ public TermFactory() { this.cache = null; } - public TermFactory(Map cache) { + public TermFactory(Map cache) { this.cache = cache; } @@ -119,22 +119,26 @@ private JTerm doCreateTerm(Operator op, ImmutableArray subs, ImmutableArray boundVars, ImmutableArray labels, String origin) { - final TermImpl newTerm = - (labels == null || labels.isEmpty() - ? new TermImpl(op, subs, boundVars) - : new LabeledTermImpl(op, subs, boundVars, labels, origin)); + final TermImpl newTerm = new TermImpl(op, subs, boundVars, labels); // Check if caching is possible. It is not possible if a non-empty JavaBlock is available // in the term or in one of its children because the meta information like PositionInfos // may be different. + // + // Labeled terms are cached too: the cache is keyed on StrictTermKey, i.e. label-sensitive + // equality, so a term is only shared with a structurally AND label identical one. This + // reproduces the interning behaviour from when term equality itself was label-sensitive + // (and keeps the == fast paths and memory sharing) while term.equals() stays + // label-agnostic for the logic layer. if (cache != null && !newTerm.containsJavaBlockRecursive()) { + final StrictTermKey key = new StrictTermKey(newTerm); JTerm term; synchronized (cache) { - term = cache.get(newTerm); + term = cache.get(key); } if (term == null) { term = newTerm.checked(); synchronized (cache) { - cache.put(term, term); + cache.put(key, term); } } return term; diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/TermImpl.java b/key.core/src/main/java/de/uka/ilkd/key/logic/TermImpl.java index 916f466ac31..73283f40677 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/logic/TermImpl.java +++ b/key.core/src/main/java/de/uka/ilkd/key/logic/TermImpl.java @@ -3,9 +3,11 @@ * SPDX-License-Identifier: GPL-2.0-only */ package de.uka.ilkd.key.logic; +import java.util.Objects; import java.util.concurrent.atomic.AtomicInteger; +import java.util.concurrent.atomic.AtomicIntegerFieldUpdater; +import java.util.stream.Collectors; -import de.uka.ilkd.key.java.ast.PositionInfo; import de.uka.ilkd.key.logic.label.TermLabel; import de.uka.ilkd.key.logic.op.*; @@ -19,12 +21,14 @@ import org.key_project.util.collection.DefaultImmutableSet; import org.key_project.util.collection.ImmutableArray; import org.key_project.util.collection.ImmutableSet; +import org.key_project.util.java.CollectionUtil; import org.jspecify.annotations.NonNull; /** - * The currently only class implementing the Term interface. TermFactory should be the only class + * The only class implementing the {@link JTerm} interface. A term may carry {@link TermLabel}s; + * unlabeled terms share a single empty label array. {@link TermFactory} should be the only class * dealing directly with the TermImpl class. */ class TermImpl implements JTerm { @@ -54,34 +58,68 @@ class TermImpl implements JTerm { private final ImmutableArray subs; private final ImmutableArray boundVars; + /** + * The labels attached to this term, or the shared {@link #EMPTY_LABEL_LIST} if there are + * none. Never {@code null}. Term labels do not participate in {@link #equals(Object)} / + * {@link #hashCode()}; use {@link #equalsIncludingLabels(Object)} for a label-sensitive + * comparison. + */ + private final ImmutableArray labels; + // caches - private enum ThreeValuedTruth { - TRUE, FALSE, UNKNOWN - } private int depth = -1; - /** - * A cached value for computing the term's rigidness. - */ - private ThreeValuedTruth rigid = ThreeValuedTruth.UNKNOWN; private ImmutableSet freeVars = null; /** * Cached {@link #hashCode()} value. */ private int hashcode = -1; + /** + * Cached {@link #labeledHashCode()} value (label-sensitive); only used for terms that + * actually carry a label somewhere in their subtree. + */ + private int labeledHashcode = -1; + private Sort sort; /** - * This flag indicates that the {@link JTerm} itself or one of its children contains a non-empty - * {@link JavaBlock}. {@link JTerm}s which provides a {@link JavaBlock} directly or indirectly - * can't be cached because it is possible that the contained meta information inside the - * {@link JavaBlock}, e.g. {@link PositionInfo}s, are different. + * Packed lazily-computed tri-state predicates, two bits each (see {@link #FLAG_UNKNOWN} / + * {@link #FLAG_FALSE} / {@link #FLAG_TRUE}): rigidness, and whether this term or one of its + * children contains a {@link JavaBlock}, a {@link Transformer}, or a {@link TermLabel}. + * Written at most once per flag via {@link #FLAGS} CAS so that concurrent computation of + * different flags on the same (shared, immutable) term cannot lose updates. */ - private ThreeValuedTruth containsJavaBlockRecursive = ThreeValuedTruth.UNKNOWN; + private volatile int flags = 0; + + private static final AtomicIntegerFieldUpdater FLAGS = + AtomicIntegerFieldUpdater.newUpdater(TermImpl.class, "flags"); + + private static final int FLAG_UNKNOWN = 0; + private static final int FLAG_FALSE = 1; + private static final int FLAG_TRUE = 2; + private static final int FLAG_MASK = 3; - /** caches whether this term or a (direct/indirect) child has a {@link Transformer} operator. */ - private ThreeValuedTruth containsTransformerRecursive = ThreeValuedTruth.UNKNOWN; + private static final int SHIFT_RIGID = 0; + private static final int SHIFT_JAVA_BLOCK = 2; + private static final int SHIFT_TRANSFORMER = 4; + private static final int SHIFT_LABELS = 6; + + /** @return the two-bit state of the flag at {@code shift} */ + private int getFlag(int shift) { + return (flags >>> shift) & FLAG_MASK; + } + + /** Stores {@code value} into the flag at {@code shift}, unless it has meanwhile been set. */ + private void setFlag(int shift, int value) { + int prev; + do { + prev = flags; + if (((prev >>> shift) & FLAG_MASK) != FLAG_UNKNOWN) { + return; + } + } while (!FLAGS.compareAndSet(this, prev, prev | (value << shift))); + } // ------------------------------------------------------------------------- // constructors @@ -98,11 +136,25 @@ private enum ThreeValuedTruth { */ public TermImpl(Operator op, ImmutableArray subs, ImmutableArray boundVars) { + this(op, subs, boundVars, null); + } + + /** + * Constructs a term that may carry term labels. + * + * @param op the operator of the term + * @param subs the sub terms of the constructed term + * @param boundVars the bound variables (if applicable) + * @param labels the term's labels, or {@code null}/empty for an unlabeled term + */ + public TermImpl(Operator op, ImmutableArray subs, + ImmutableArray boundVars, ImmutableArray labels) { assert op != null; assert subs != null; this.op = op; this.subs = subs.isEmpty() ? EMPTY_TERM_LIST : subs; this.boundVars = boundVars == null ? EMPTY_VAR_LIST : boundVars; + this.labels = (labels == null || labels.isEmpty()) ? EMPTY_LABEL_LIST : labels; } private ImmutableSet determineFreeVars() { @@ -228,22 +280,21 @@ public int depth() { @Override public boolean isRigid() { - if (rigid == ThreeValuedTruth.UNKNOWN) { - if (!op.isRigid()) { - rigid = ThreeValuedTruth.FALSE; - } else { - ThreeValuedTruth localIsRigid = ThreeValuedTruth.TRUE; + int flag = getFlag(SHIFT_RIGID); + if (flag == FLAG_UNKNOWN) { + boolean result = op.isRigid(); + if (result) { for (int i = 0, n = arity(); i < n; i++) { if (!sub(i).isRigid()) { - localIsRigid = ThreeValuedTruth.FALSE; + result = false; break; } } - rigid = localIsRigid; } + flag = result ? FLAG_TRUE : FLAG_FALSE; + setFlag(SHIFT_RIGID, flag); } - - return rigid == ThreeValuedTruth.TRUE; + return flag == FLAG_TRUE; } @@ -281,7 +332,8 @@ public void execPreOrder(Visitor visitor) { } /** - * true iff o is syntactically equal to this term + * true iff o is syntactically equal to this term; {@link TermLabel}s are + * ignored. Use {@link #equalsIncludingLabels(Object)} for a label-sensitive comparison. */ @Override public boolean equals(Object o) { @@ -289,18 +341,72 @@ public boolean equals(Object o) { return true; } - if (o == null || o.getClass() != getClass() || hashCode() != o.hashCode()) { + if (!(o instanceof final TermImpl t) || hashCode() != o.hashCode()) { return false; } - final TermImpl t = (TermImpl) o; - - return op.equals(t.op) && t.hasLabels() == hasLabels() && subs.equals(t.subs) + return op.equals(t.op) && subs.equals(t.subs) && boundVars.equals(t.boundVars) // TODO (DD): below is no longer necessary && javaBlock().equals(t.javaBlock()); } + /** + * true iff o is syntactically equal to this term including all + * {@link TermLabel}s attached to this term or any subterm. Labels are compared as sets + * (order-insensitive). This is the label-sensitive counterpart of {@link #equals(Object)} + * needed by the few consumers which must distinguish label variants (e.g. the term + * factory cache and taclet index caches). + */ + @Override + public boolean equalsIncludingLabels(Object o) { + if (o == this) { + return true; + } + if (!equals(o)) { + return false; + } + final TermImpl t = (TermImpl) o; + if (!containsLabelsRecursive() && !t.containsLabelsRecursive()) { + return true; + } + return labelsEqualRecursive(this, t); + } + + /** + * Compares the {@link TermLabel}s of two structurally equal terms recursively. + * + * @param t1 a term + * @param t2 a term already known to be equal to {@code t1} modulo term labels + * @return true iff all (sub)terms carry equal label sets + */ + private static boolean labelsEqualRecursive(JTerm t1, JTerm t2) { + // interned (shared) subterms are reference-identical: prune the whole subtree. This is + // the common case, as the term factory interns terms label-sensitively. + if (t1 == t2) { + return true; + } + final ImmutableArray labels1 = t1.getLabels(); + final ImmutableArray labels2 = t2.getLabels(); + if (labels1.size() != labels2.size()) { + return false; + } + for (int i = 0, sz = labels1.size(); i < sz; i++) { + if (!labels2.contains(labels1.get(i))) { + return false; + } + } + if (!t1.containsLabelsRecursive() && !t2.containsLabelsRecursive()) { + return true; + } + for (int i = 0, ar = t1.arity(); i < ar; i++) { + if (!labelsEqualRecursive(t1.sub(i), t2.sub(i))) { + return false; + } + } + return true; + } + @Override public final int hashCode() { if (hashcode == -1) { @@ -327,6 +433,33 @@ protected int computeHashCode() { return hashcode; } + @Override + public int labeledHashCode() { + // no labels anywhere: the label-sensitive hash coincides with the plain one + if (!containsLabelsRecursive()) { + return hashCode(); + } + if (labeledHashcode == -1) { + this.labeledHashcode = computeLabeledHashCode(); + } + return labeledHashcode; + } + + /** {@link #hashCode()} refined by the labels of this term and all its subterms. */ + private int computeLabeledHashCode() { + int result = hashCode(); + for (int i = 0, sz = labels.size(); i < sz; i++) { + result = result * 17 + labels.get(i).hashCode(); + } + for (int i = 0, ar = arity(); i < ar; i++) { + result = result * 17 + sub(i).labeledHashCode(); + } + if (result == -1) { + result = 0; + } + return result; + } + @Override public boolean equalsModProperty(Object o, Property property, V... v) { if (!(o instanceof JTerm other)) { @@ -357,16 +490,22 @@ public String toString() { sb.append(op()).append("|{").append(javaBlock()).append("}| "); } sb.append("(").append(sub(0)).append(")"); - return sb.toString(); } else { sb.append(op().name()); if (!boundVars.isEmpty()) { sb.append(Strings.formatAsList(boundVars(), "{", ",", "}")); } - if (arity() == 0) { - return sb.toString(); + if (arity() != 0) { + sb.append(Strings.formatAsList(subs(), "(", ",", ")")); + } + } + + if (hasLabels()) { + final String labelsStr = + labels.stream().map(TermLabel::toString).collect(Collectors.joining(", ")); + if (!labelsStr.isEmpty()) { + sb.append("<<").append(labelsStr).append(">>"); } - sb.append(Strings.formatAsList(subs(), "(", ",", ")")); } return sb.toString(); @@ -380,22 +519,29 @@ public int serialNumber() { @Override public boolean hasLabels() { - return false; + return !labels.isEmpty(); } @Override public boolean containsLabel(TermLabel label) { + assert label != null : "Label must not be null"; + for (int i = 0, sz = labels.size(); i < sz; i++) { + if (label.equals(labels.get(i))) { + return true; + } + } return false; } @Override public TermLabel getLabel(Name termLabelName) { - return null; + return CollectionUtil.search(labels, + element -> Objects.equals(element.name(), termLabelName)); } @Override public ImmutableArray getLabels() { - return EMPTY_LABEL_LIST; + return labels; } /** @@ -403,40 +549,62 @@ public ImmutableArray getLabels() { */ @Override public boolean containsJavaBlockRecursive() { - if (containsJavaBlockRecursive == ThreeValuedTruth.UNKNOWN) { - ThreeValuedTruth result = ThreeValuedTruth.FALSE; - if (!javaBlock().isEmpty()) { - result = ThreeValuedTruth.TRUE; - } else { + int flag = getFlag(SHIFT_JAVA_BLOCK); + if (flag == FLAG_UNKNOWN) { + boolean result = !javaBlock().isEmpty(); + if (!result) { for (int i = 0, arity = subs.size(); i < arity; i++) { if (subs.get(i).containsJavaBlockRecursive()) { - result = ThreeValuedTruth.TRUE; + result = true; break; } } } - this.containsJavaBlockRecursive = result; + flag = result ? FLAG_TRUE : FLAG_FALSE; + setFlag(SHIFT_JAVA_BLOCK, flag); } - return containsJavaBlockRecursive == ThreeValuedTruth.TRUE; + return flag == FLAG_TRUE; + } + + /** + * {@inheritDoc} + */ + @Override + public boolean containsLabelsRecursive() { + int flag = getFlag(SHIFT_LABELS); + if (flag == FLAG_UNKNOWN) { + boolean result = hasLabels(); + if (!result) { + for (int i = 0, arity = subs.size(); i < arity; i++) { + if (subs.get(i).containsLabelsRecursive()) { + result = true; + break; + } + } + } + flag = result ? FLAG_TRUE : FLAG_FALSE; + setFlag(SHIFT_LABELS, flag); + } + return flag == FLAG_TRUE; } @Override public boolean containsTransformerRecursive() { - if (containsTransformerRecursive == ThreeValuedTruth.UNKNOWN) { - ThreeValuedTruth result = ThreeValuedTruth.FALSE; - if (op instanceof Transformer) { - result = ThreeValuedTruth.TRUE; - } else { + int flag = getFlag(SHIFT_TRANSFORMER); + if (flag == FLAG_UNKNOWN) { + boolean result = op instanceof Transformer; + if (!result) { for (int i = 0, arity = subs.size(); i < arity; i++) { if (subs.get(i).containsTransformerRecursive()) { - result = ThreeValuedTruth.TRUE; + result = true; break; } } } - this.containsTransformerRecursive = result; + flag = result ? FLAG_TRUE : FLAG_FALSE; + setFlag(SHIFT_TRANSFORMER, flag); } - return containsTransformerRecursive == ThreeValuedTruth.TRUE; + return flag == FLAG_TRUE; } diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/equality/IrrelevantTermLabelsProperty.java b/key.core/src/main/java/de/uka/ilkd/key/logic/equality/IrrelevantTermLabelsProperty.java index 30b0b4a067c..71eda7f01f0 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/logic/equality/IrrelevantTermLabelsProperty.java +++ b/key.core/src/main/java/de/uka/ilkd/key/logic/equality/IrrelevantTermLabelsProperty.java @@ -13,7 +13,17 @@ /** * A property that can be used in * {@link EqualsModProperty#equalsModProperty(Object, Property, Object[])} for terms. - * All irrelevant term labels are ignored in this equality check. + * All irrelevant term labels are ignored in this equality check, while labels that are + * {@link TermLabel#isProofRelevant() proof relevant} still count. + *

+ * This is the middle one of the three label comparison modes: plain + * {@link de.uka.ilkd.key.logic.JTerm#equals(Object)} ignores all term labels, this + * property ignores only the non-proof-relevant (cosmetic) ones, and + * {@link de.uka.ilkd.key.logic.JTerm#equalsIncludingLabels(Object)} respects all labels. Use this + * property when a comparison must distinguish, e.g., an {@code anonHeapFunction}-labeled term + * from an unlabeled one, but must not be affected by origin labels. It deliberately lives in a + * {@link Property} (and not on the term) because it needs label-kind knowledge + * ({@code isProofRelevant()}). *

* The single instance of this property can be accessed through * {@link IrrelevantTermLabelsProperty#IRRELEVANT_TERM_LABELS_PROPERTY}. diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/equality/TermLabelsProperty.java b/key.core/src/main/java/de/uka/ilkd/key/logic/equality/TermLabelsProperty.java index 0e29bf80cb6..909ab1c9e0f 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/logic/equality/TermLabelsProperty.java +++ b/key.core/src/main/java/de/uka/ilkd/key/logic/equality/TermLabelsProperty.java @@ -14,6 +14,13 @@ * {@link EqualsModProperty#equalsModProperty(Object, Property, Object[])} for terms. * All term labels are ignored in this equality check. *

+ * Note: since the standard term equality {@link Object#equals(Object)} ignores all term + * labels as well, this property is equivalent to plain {@code equals} for + * {@link de.uka.ilkd.key.logic.JTerm}s — prefer plain {@code equals} in new code. The property is + * kept for the generic {@link org.key_project.logic.Term} level and for symmetry with + * {@link IrrelevantTermLabelsProperty} (which is not equivalent to {@code equals}: it + * keeps proof-relevant labels significant). + *

* The single instance of this property can be accessed through * {@link TermLabelsProperty#TERM_LABELS_PROPERTY}. * diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/label/TermLabel.java b/key.core/src/main/java/de/uka/ilkd/key/logic/label/TermLabel.java index 7f57d8d7903..e27fd6c8fc3 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/logic/label/TermLabel.java +++ b/key.core/src/main/java/de/uka/ilkd/key/logic/label/TermLabel.java @@ -9,7 +9,6 @@ import de.uka.ilkd.key.logic.op.JModality; import de.uka.ilkd.key.proof.init.Profile; import de.uka.ilkd.key.rule.BuiltInRule; -import de.uka.ilkd.key.rule.label.ChildTermLabelPolicy; import de.uka.ilkd.key.rule.label.TermLabelMerger; import de.uka.ilkd.key.rule.label.TermLabelPolicy; import de.uka.ilkd.key.rule.label.TermLabelRefactoring; @@ -49,21 +48,31 @@ * {@link TermLabelManager} provides also the functionality to parse and maintain them during prove. *

*

- * The {@link TermLabelManager} is responsible during prove to maintain term labels. - * This means that labels of new {@link JTerm}s created during rule application are computed - * via {@link TermLabelManager#instantiateLabels} - * and of existing {@link JTerm}s are refactored (added or removed) via - * {@link TermLabelManager#instantiateLabels}. + * The {@link TermLabelManager} is responsible for maintaining term labels during proof + * construction. This means that labels of new {@link JTerm}s created during rule application are + * computed via {@link TermLabelManager#instantiateLabels} and labels of existing {@link JTerm}s + * are refactored (added or removed) via the refactoring methods of {@link TermLabelManager}. *

*

- * Antecedent and succedent of a {@link Sequent} are sets. The equality check if a - * {@link SequentFormula} is already contained ignores {@link TermLabel}s. To ensure that - * {@link TermLabel}s are not lost, + * Equality: since term labels are not soundness relevant, the standard term equality + * {@link JTerm#equals(Object)} (and {@link JTerm#hashCode()}) ignores all term labels: + * two terms differing only in labels are the same formula. Code that must distinguish label + * variants has two options: {@link JTerm#equalsIncludingLabels(Object)} together with + * {@link JTerm#labeledHashCode()} respects all labels (used for term interning and index caches, + * see {@link de.uka.ilkd.key.logic.StrictTermKey}), while + * {@code equalsModProperty(t, IRRELEVANT_TERM_LABELS_PROPERTY)} ignores only labels that are not + * {@link #isProofRelevant() proof relevant}. + *

+ *

+ * Antecedent and succedent of a {@link Sequent} are sets. The redundancy check whether a + * {@link SequentFormula} is already contained ignores {@link TermLabel}s (consistent with the + * standard term equality). To ensure that {@link TermLabel}s are not lost when a formula is + * rejected as redundant, * {@link TermLabelManager#mergeLabels(de.uka.ilkd.key.java.Services, * de.uka.ilkd.key.logic.SequentChangeInfo)} * merges the labels of the existing {@link SequentFormula} with those of the rejected * {@link SequentFormula}. How this is done in detail is implemented by a {@link TermLabelMerger}. - * If no {@link TermLabelMerger} is available, the {@link TermLabel} of the rejected + * If no {@link TermLabelMerger} is available, the {@link TermLabel}s of the rejected * {@link SequentFormula} are lost. *

*

@@ -108,15 +117,6 @@ *

  • {@code 2 + 3 ~~> 5<>a>>}: A new label has to be added which is not provided by the * rule. Implement a {@link TermLabelUpdate} which adds, sorts or removes * {@link TermLabel} before a new {@link JTerm} is created.
    • - *
  • {@code 2<> + 3<> ~~> 5<>}: A direct child of the application {@link JTerm} - * {@code a} contains the label before. Use a direct {@link ChildTermLabelPolicy} to - * ensure that it is added also to the new term.
    • - *
  • {@code 2 + (3<> - 1<>) ~~> 4<>}: A child or grandchild of the application - * {@link JTerm} {@code a} contains the label before. Use a direct - * {@link ChildTermLabelPolicy} to ensure that it is added also to the new term.
    • - *
  • {@code 2<> + 3<> ~~> 2<> - 3}: Implement a {@link TermLabelRefactoring} - * which works on {@link RefactoringScope#APPLICATION_DIRECT_CHILDREN} to freely add or - * remove {@link TermLabel}s on direct children of the application {@link JTerm}.
    • *
  • {@code 2 + (3<> - 1<>) ~~> 2 * (3<> - 1)}: Implement a * {@link TermLabelRefactoring} which works on * {@link RefactoringScope#APPLICATION_CHILDREN_AND_GRANDCHILDREN_SUBTREE} to freely diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/label/TermLabelContext.java b/key.core/src/main/java/de/uka/ilkd/key/logic/label/TermLabelContext.java new file mode 100644 index 00000000000..2c02059ea31 --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/logic/label/TermLabelContext.java @@ -0,0 +1,54 @@ +/* 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.logic.label; + +import de.uka.ilkd.key.java.Services; +import de.uka.ilkd.key.logic.JTerm; +import de.uka.ilkd.key.proof.Goal; + +import org.key_project.prover.rules.Rule; +import org.key_project.prover.rules.RuleApp; +import org.key_project.prover.sequent.PosInOccurrence; +import org.key_project.prover.sequent.Sequent; + +/** + * The rule application for which term labels are computed or refactored. One instance is created + * per {@link TermLabelManager} entry point invocation and passed unchanged to all term label + * hooks ({@link de.uka.ilkd.key.rule.label.TermLabelPolicy}, + * {@link de.uka.ilkd.key.rule.label.TermLabelUpdate}, + * {@link de.uka.ilkd.key.rule.label.TermLabelRefactoring}); the hooks receive their varying + * payload (the term being created or refactored, the label set) as separate parameters. + * + * @param state the {@link TermLabelState} of the current rule application (mutable scratchpad + * shared by all hook invocations of one rule application) + * @param services the {@link Services} of the proof the rule is applied in + * @param applicationPosInOccurrence the {@link PosInOccurrence} in the previous {@link Sequent} + * which defines the term that is rewritten, or {@code null} if not available (e.g. proof + * obligation creation) + * @param applicationTerm the term defined by {@code applicationPosInOccurrence}, or {@code null} + * @param modalityTerm the modality term below the updates of {@code applicationTerm} + * (see {@code TermBuilder.goBelowUpdates}), or {@code null} where it was not computed + * (refactoring entry points; no modality hooks registered) + * @param rule the {@link Rule} which is applied, or {@code null} + * @param ruleApp the {@link RuleApp} which is currently performed, or {@code null} where the + * entry point does not receive it (refactoring entry points) + * @param goal the optional {@link Goal} on which the new or refactored term will be used, or + * {@code null} + * @param hint an optional hint passed from the active rule to describe the term which should be + * created, or {@code null} + * @param tacletTerm the taclet term which is responsible for the new term, or {@code null} in + * case of built-in rules + */ +public record TermLabelContext( + TermLabelState state, + Services services, + PosInOccurrence applicationPosInOccurrence, + JTerm applicationTerm, + JTerm modalityTerm, + Rule rule, + RuleApp ruleApp, + Goal goal, + Object hint, + JTerm tacletTerm) { +} diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/label/TermLabelManager.java b/key.core/src/main/java/de/uka/ilkd/key/logic/label/TermLabelManager.java index ffa332c3164..c72ca97c164 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/logic/label/TermLabelManager.java +++ b/key.core/src/main/java/de/uka/ilkd/key/logic/label/TermLabelManager.java @@ -4,7 +4,6 @@ package de.uka.ilkd.key.logic.label; import java.util.*; -import java.util.Map.Entry; import de.uka.ilkd.key.java.Services; import de.uka.ilkd.key.logic.*; @@ -57,9 +56,16 @@ *
    • * *

    + * The labels of a new {@link JTerm} are computed by {@link #instantiateLabels} in a fixed order + * which is part of the contract: taclet-provided labels, then the application-term + * {@link TermLabelPolicy} instances, then the modality-term {@link TermLabelPolicy} instances, + * then the rule-specific {@link TermLabelUpdate}s and finally the rule-independent + * {@link TermLabelUpdate}s. {@link TermLabelRefactoring}s run afterwards on the surrounding + * terms, with the scope they request per rule application. + *

    *

    - * For more information about {@link TermLabel}s and how they are maintained during prove read the - * documentation of interface {@link TermLabel}. + * For more information about {@link TermLabel}s and how they are maintained during proof + * construction read the documentation of interface {@link TermLabel}. *

    * * @author Mattias Ulbrich @@ -85,30 +91,6 @@ public class TermLabelManager { private final Map modalityTermPolicyMap = new LinkedHashMap<>(); - /** - * All rule specific direct {@link ChildTermLabelPolicy}s. - */ - private final Map> ruleSpecificDirectChildTermLabelPolicies = - new LinkedHashMap<>(); - - /** - * All rule independent direct {@link ChildTermLabelPolicy}s. - */ - private final Map allRulesDirectChildTermLabelPolicies = - new LinkedHashMap<>(); - - /** - * All rule specific child and grandchild {@link ChildTermLabelPolicy}s. - */ - private final Map> ruleSpecificChildAndGrandchildTermLabelPolicies = - new LinkedHashMap<>(); - - /** - * All rule independent child and grandchild {@link ChildTermLabelPolicy}s. - */ - private final Map allRulesChildAndGrandchildTermLabelPolicies = - new LinkedHashMap<>(); - /** * All rule independent {@link TermLabelUpdate}s. */ @@ -157,13 +139,6 @@ public TermLabelManager(ImmutableList configurations) { applicationTermPolicyMap); analyzeTermPolicies(conf.getTermLabelName(), conf.getModalityTermPolicies(), modalityTermPolicyMap); - analyzeChildTermPolicies(conf.getTermLabelName(), - conf.getDirectChildTermLabelPolicies(), allRulesDirectChildTermLabelPolicies, - ruleSpecificDirectChildTermLabelPolicies); - analyzeChildTermPolicies(conf.getTermLabelName(), - conf.getChildAndGrandchildTermLabelPolicies(), - allRulesChildAndGrandchildTermLabelPolicies, - ruleSpecificChildAndGrandchildTermLabelPolicies); analyzeUpdates(conf.getTermLabelUpdates()); analyzeRefactorings(conf.getTermLabelRefactorings()); analyzeMerger(conf.getTermLabelName(), conf.getTermLabelMerger()); @@ -204,42 +179,6 @@ private void analyzeTermPolicies(Name termLabelName, ImmutableList - * Analyzes the given {@link ChildTermLabelPolicy} and adds it to the given policy {@link Map}s. - *

    - *

    - * This is a helper {@link Map} of {@link #TermLabelManager(ImmutableList)}. - *

    - * - * @param termLabelName The name of the supported {@link TermLabel}. - * @param policies The {@link ChildTermLabelPolicy} instances to analyze. - * @param allRulesPolicyMap The policy {@link Map} with all rules to update. - * @param ruleSpecificPolicyMap The rule specific policy {@link Map} to update. - */ - private void analyzeChildTermPolicies(Name termLabelName, - ImmutableList policies, - Map allRulesPolicyMap, - Map> ruleSpecificPolicyMap) { - if (policies != null) { - for (ChildTermLabelPolicy policy : policies) { - ImmutableList supportedRules = policy.getSupportedRuleNames(); - if (supportedRules == null || supportedRules.isEmpty()) { - allRulesPolicyMap.put(termLabelName, policy); - } else { - for (Name rule : supportedRules) { - Map ruleMap = ruleSpecificPolicyMap.get(rule); - if (ruleMap == null) { - ruleMap = new LinkedHashMap<>(); - ruleSpecificPolicyMap.put(rule, ruleMap); - } - ruleMap.put(termLabelName, policy); - } - } - } - } - } - /** *

    * Analyzes the given {@link TermLabelUpdate} and updates {@link #allRulesUpdates} and @@ -573,54 +512,19 @@ public static ImmutableArray instantiateLabels(TermLabelState state, /** * Do application term specific stuff. * - * @param state The {@link TermLabelState} of the current rule application. - * @param services The {@link Services} used by the {@link Proof} on which a {@link Rule} is - * applied right now. - * @param applicationPosInOccurrence The {@link PosInOccurrence} in the previous {@link Sequent} - * which defines the {@link JTerm} that is rewritten. - * @param applicationTerm The {@link JTerm} defined by the {@link PosInOccurrence} in the - * previous {@link Sequent}. - * @param rule The {@link Rule} which is applied. - * @param goal The optional {@link Goal} on which the {@link JTerm} to create will be used. - * @param hint An optional hint passed from the active rule to describe the term which should be - * created. - * @param tacletTerm The optional {@link JTerm} in the taclet which is responsible to - * instantiate - * the new {@link JTerm} for the new proof node or {@code null} in case of built in - * rules. + * @param context the {@link TermLabelContext} of the current rule application * @param newTerm the template for the new {@link JTerm} to create * @param newLabels The set accumulating the {@link TermLabel}s to add to the new {@link JTerm} * which should be created. */ - private void addLabelsBasedOnApplicationTerm(TermLabelState state, Services services, - PosInOccurrence applicationPosInOccurrence, - JTerm applicationTerm, Rule rule, Goal goal, - Object hint, JTerm tacletTerm, JTerm newTerm, Set newLabels) { - if (applicationTerm == null) { + private void addLabelsBasedOnApplicationTerm(TermLabelContext context, JTerm newTerm, + Set newLabels) { + if (context.applicationTerm() == null) { return; } // Re-add exiting application term labels based on application term policies. - performTermLabelPolicies(state, services, applicationPosInOccurrence, applicationTerm, rule, - goal, hint, tacletTerm, newTerm, applicationTermPolicyMap, newLabels); - // Add labels from direct child term policies. - Map activeDirectChildPolicies = - computeActiveChildPolicies(services, applicationPosInOccurrence, applicationTerm, rule, - goal, hint, tacletTerm, newTerm, ruleSpecificDirectChildTermLabelPolicies, - allRulesDirectChildTermLabelPolicies); - if (!activeDirectChildPolicies.isEmpty()) { - performDirectChildPolicies(services, applicationPosInOccurrence, applicationTerm, rule, - goal, hint, tacletTerm, newTerm, activeDirectChildPolicies, newLabels); - } - - // Add labels from child and grandchild term policies. - Map activeChildAndGrandchildPolicies = - computeActiveChildPolicies(services, applicationPosInOccurrence, applicationTerm, rule, - goal, hint, tacletTerm, newTerm, ruleSpecificChildAndGrandchildTermLabelPolicies, - allRulesChildAndGrandchildTermLabelPolicies); - if (!activeChildAndGrandchildPolicies.isEmpty()) { - performChildAndGrandchildPolicies(services, applicationPosInOccurrence, applicationTerm, - rule, goal, hint, tacletTerm, newTerm, activeChildAndGrandchildPolicies, newLabels); - } + performTermLabelPolicies(context, context.applicationTerm(), newTerm, + applicationTermPolicyMap, newLabels); } /** @@ -672,29 +576,28 @@ public ImmutableArray instantiateLabels(TermLabelState state, Service || !allRulesUpdates.isEmpty() || currentRuleSpecificUpdates != null) ? TermBuilder.goBelowUpdates(applicationTerm) : null; + final TermLabelContext context = new TermLabelContext(state, services, + applicationPosInOccurrence, applicationTerm, modalityTerm, rule, ruleApp, goal, hint, + tacletTerm); // Instantiate empty result Set newLabels = new LinkedHashSet<>(); // Add labels from taclet if (tacletTerm != null && tacletTerm.hasLabels()) { performTacletTerm(tacletTerm, newLabels); } - addLabelsBasedOnApplicationTerm(state, services, applicationPosInOccurrence, - applicationTerm, rule, goal, hint, tacletTerm, newTerm, newLabels); + addLabelsBasedOnApplicationTerm(context, newTerm, newLabels); // Re-add exiting modality term labels based on symbolic execution term policies. if (modalityTerm != null) { - performTermLabelPolicies(state, services, applicationPosInOccurrence, modalityTerm, - rule, goal, hint, tacletTerm, newTerm, modalityTermPolicyMap, newLabels); + performTermLabelPolicies(context, modalityTerm, newTerm, modalityTermPolicyMap, + newLabels); } // Allow rule specific updater to remove and add labels if (currentRuleSpecificUpdates != null) { - performUpdater(state, services, applicationPosInOccurrence, applicationTerm, - modalityTerm, rule, ruleApp, hint, tacletTerm, newTerm, currentRuleSpecificUpdates, - newLabels); + performUpdater(context, newTerm, currentRuleSpecificUpdates, newLabels); } // Allow all rule updater to remove and add labels if (!allRulesUpdates.isEmpty()) { - performUpdater(state, services, applicationPosInOccurrence, applicationTerm, - modalityTerm, rule, ruleApp, hint, tacletTerm, newTerm, allRulesUpdates, newLabels); + performUpdater(context, newTerm, allRulesUpdates, newLabels); } // Return result return new ImmutableArray<>(newLabels.toArray(new TermLabel[0])); @@ -730,273 +633,46 @@ protected void performTacletTerm(JTerm tacletTerm, Set newLabels) { * {@link #instantiateLabels(TermLabelState, Services, PosInOccurrence, Rule, RuleApp, Goal, Object, JTerm, JTerm)} *

    * - * @param state The {@link TermLabelState} of the current rule application. - * @param services The {@link Services} used by the {@link Proof} on which a {@link Rule} is - * applied right now. - * @param applicationPosInOccurrence The {@link PosInOccurrence} in the previous {@link Sequent} - * which defines the {@link JTerm} that is rewritten. - * @param applicationTerm The {@link JTerm} defined by the {@link PosInOccurrence} in the - * previous {@link Sequent}. - * @param rule The {@link Rule} which is applied. - * @param goal The optional {@link Goal} on which the {@link JTerm} to create will be used. - * @param hint An optional hint passed from the active rule to describe the term which should be - * created. - * @param tacletTerm The optional {@link JTerm} in the taclet which is responsible to - * instantiate - * the new {@link JTerm} for the new proof node or {@code null} in case of built in - * rules. - * @param newTerm the template for the new {@link JTerm} to create - * @param policies The {@link TermLabelPolicy} instances to perform. - * @param newLabels The result {@link Set} with the {@link TermLabel}s of the new {@link JTerm}. - */ - protected void performTermLabelPolicies(TermLabelState state, Services services, - PosInOccurrence applicationPosInOccurrence, - JTerm applicationTerm, Rule rule, Goal goal, - Object hint, JTerm tacletTerm, JTerm newTerm, Map policies, - Set newLabels) { - if (applicationTerm.hasLabels() && !policies.isEmpty()) { - for (TermLabel label : applicationTerm.getLabels()) { - performTermLabelPolicies(state, services, applicationPosInOccurrence, - applicationTerm, rule, goal, hint, tacletTerm, newTerm, policies, newLabels, - label); - } - } - } - - /** - *

    - * Performs the given {@link TermLabelPolicy} instances. - *

    - *

    - * This is a helper method of - * {@link #performTermLabelPolicies(TermLabelState, Services, PosInOccurrence, JTerm, Rule, Goal, Object, JTerm, JTerm, Map, Set)} - *

    - * - * @param state The {@link TermLabelState} of the current rule application. - * @param services The {@link Services} used by the {@link Proof} on which a {@link Rule} is - * applied right now. - * @param applicationPosInOccurrence The {@link PosInOccurrence} in the previous {@link Sequent} - * which defines the {@link JTerm} that is rewritten. - * @param applicationTerm The {@link JTerm} defined by the {@link PosInOccurrence} in the - * previous {@link Sequent}. - * @param rule The {@link Rule} which is applied. - * @param goal The optional {@link Goal} on which the {@link JTerm} to create will be used. - * @param hint An optional hint passed from the active rule to describe the term which should be - * created. - * @param tacletTerm The optional {@link JTerm} in the taclet which is responsible to - * instantiate - * the new {@link JTerm} for the new proof node or {@code null} in case of built in - * rules. + * @param context the {@link TermLabelContext} of the current rule application + * @param sourceTerm the {@link JTerm} whose labels are under consideration (application or + * modality term) * @param newTerm the template for the new {@link JTerm} to create * @param policies The {@link TermLabelPolicy} instances to perform. * @param newLabels The result {@link Set} with the {@link TermLabel}s of the new {@link JTerm}. - * @param label The current {@link TermLabel} to ask its {@link TermLabelPolicy}. */ - protected void performTermLabelPolicies(TermLabelState state, Services services, - PosInOccurrence applicationPosInOccurrence, - JTerm applicationTerm, Rule rule, Goal goal, - Object hint, JTerm tacletTerm, JTerm newTerm, Map policies, - Set newLabels, TermLabel label) { - TermLabelPolicy policy = policies.get(label.name()); - if (policy != null) { - label = policy.keepLabel(state, services, applicationPosInOccurrence, applicationTerm, - rule, goal, hint, tacletTerm, newTerm, label); - if (label != null) { - newLabels.add(label); - } - } - } - - /** - *

    - * Computes active {@link ChildTermLabelPolicy} instances which have to be executed during the - * given rule application. - *

    - *

    - * This is a helper {@link Map} of - * {@link #instantiateLabels(TermLabelState, Services, PosInOccurrence, Rule, RuleApp, Goal, Object, JTerm, JTerm)} - *

    - * - * @param services The {@link Services} used by the {@link Proof} on which a {@link Rule} is - * applied right now. - * @param applicationPosInOccurrence The {@link PosInOccurrence} in the previous {@link Sequent} - * which defines the {@link JTerm} that is rewritten. - * @param applicationTerm The {@link JTerm} defined by the {@link PosInOccurrence} in the - * previous {@link Sequent}. - * @param rule The {@link Rule} which is applied. - * @param goal The optional {@link Goal} on which the {@link JTerm} to create will be used. - * @param hint An optional hint passed from the active rule to describe the term which should be - * created. - * @param tacletTerm The optional {@link JTerm} in the taclet which is responsible to - * instantiate - * the new {@link JTerm} for the new proof node or {@code null} in case of built in - * rules. - * @param newTerm the template for the new {@link JTerm} to create - * @param ruleSpecificPolicies Rule specific {@link ChildTermLabelPolicy} instances. - * @param ruleIndependentPolicies All rules {@link ChildTermLabelPolicy} instances. - * @return The active {@link ChildTermLabelPolicy} which have to be performed. - */ - protected Map computeActiveChildPolicies(TermServices services, - PosInOccurrence applicationPosInOccurrence, - JTerm applicationTerm, Rule rule, Goal goal, - Object hint, JTerm tacletTerm, JTerm newTerm, - Map> ruleSpecificPolicies, - Map ruleIndependentPolicies) { - Map activeDirectChildPolicies = - new LinkedHashMap<>(); - if (rule != null) { - Map rulePolicies = ruleSpecificPolicies.get(rule.name()); - if (rulePolicies != null) { - for (Entry entry : rulePolicies.entrySet()) { - if (entry.getValue().isRuleApplicationSupported(services, - applicationPosInOccurrence, applicationTerm, rule, goal, hint, tacletTerm, - newTerm)) { - activeDirectChildPolicies.put(entry.getKey(), entry.getValue()); + protected void performTermLabelPolicies(TermLabelContext context, JTerm sourceTerm, + JTerm newTerm, Map policies, Set newLabels) { + if (sourceTerm.hasLabels() && !policies.isEmpty()) { + for (TermLabel label : sourceTerm.getLabels()) { + TermLabelPolicy policy = policies.get(label.name()); + if (policy != null) { + label = policy.keepLabel(context, sourceTerm, newTerm, label); + if (label != null) { + newLabels.add(label); } } } } - if (!ruleIndependentPolicies.isEmpty()) { - for (Entry entry : ruleIndependentPolicies.entrySet()) { - if (entry.getValue().isRuleApplicationSupported(services, - applicationPosInOccurrence, applicationTerm, rule, goal, hint, tacletTerm, - newTerm)) { - activeDirectChildPolicies.put(entry.getKey(), entry.getValue()); - } - } - } - return activeDirectChildPolicies; - } - - /** - *

    - * Performs the given direct {@link ChildTermLabelPolicy} instances. - *

    - *

    - * This is a helper {@link Map} of - * {@link #instantiateLabels(TermLabelState, Services, PosInOccurrence, Rule, RuleApp, Goal, Object, JTerm, JTerm)} - *

    - * - * @param services The {@link Services} used by the {@link Proof} on which a {@link Rule} is - * applied right now. - * @param applicationPosInOccurrence The {@link PosInOccurrence} in the previous {@link Sequent} - * which defines the {@link JTerm} that is rewritten. - * @param applicationTerm The {@link JTerm} defined by the {@link PosInOccurrence} in the - * previous {@link Sequent}. - * @param rule The {@link Rule} which is applied. - * @param goal The optional {@link Goal} on which the {@link JTerm} to create will be used. - * @param hint An optional hint passed from the active rule to describe the term which should be - * created. - * @param tacletTerm The optional {@link JTerm} in the taclet which is responsible to - * instantiate - * the new {@link JTerm} for the new proof node or {@code null} in case of built in - * rules. - * @param newTerm the template for the new {@link JTerm} to create - * @param policies The {@link ChildTermLabelPolicy} instances to perform. - * @param newLabels The result {@link Set} with the {@link TermLabel}s of the new {@link JTerm}. - */ - protected void performDirectChildPolicies(TermServices services, - PosInOccurrence applicationPosInOccurrence, - JTerm applicationTerm, Rule rule, Goal goal, - Object hint, JTerm tacletTerm, JTerm newTerm, - Map policies, Set newLabels) { - for (JTerm child : applicationTerm.subs()) { - for (TermLabel label : child.getLabels()) { - ChildTermLabelPolicy policy = policies.get(label.name()); - if (policy != null && policy.addLabel(services, applicationPosInOccurrence, - applicationTerm, rule, goal, hint, tacletTerm, newTerm, child, label)) { - newLabels.add(label); - } - } - } } /** *

    - * Performs the given child and grandchild {@link ChildTermLabelPolicy} instances. + * Performs the given {@link TermLabelUpdate} instances. *

    *

    - * This is a helper {@link Map} of + * This is a helper method of * {@link #instantiateLabels(TermLabelState, Services, PosInOccurrence, Rule, RuleApp, Goal, Object, JTerm, JTerm)} *

    * - * @param services The {@link Services} used by the {@link Proof} on which a {@link Rule} is - * applied right now. - * @param applicationPosInOccurrence The {@link PosInOccurrence} in the previous {@link Sequent} - * which defines the {@link JTerm} that is rewritten. - * @param applicationTerm The {@link JTerm} defined by the {@link PosInOccurrence} in the - * previous {@link Sequent}. - * @param rule The {@link Rule} which is applied. - * @param goal The optional {@link Goal} on which the {@link JTerm} to create will be used. - * @param hint An optional hint passed from the active rule to describe the term which should be - * created. - * @param tacletTerm The optional {@link JTerm} in the taclet which is responsible to - * instantiate - * the new {@link JTerm} for the new proof node or {@code null} in case of built in - * rules. + * @param context the {@link TermLabelContext} of the current rule application * @param newTerm the template for the new {@link JTerm} to create - * @param policies The {@link ChildTermLabelPolicy} instances to perform. + * @param updater The {@link TermLabelUpdate} instances to perform. * @param newLabels The result {@link Set} with the {@link TermLabel}s of the new {@link JTerm}. */ - protected void performChildAndGrandchildPolicies(final TermServices services, - final PosInOccurrence applicationPosInOccurrence, - final JTerm applicationTerm, - final Rule rule, final Goal goal, final Object hint, final JTerm tacletTerm, - final JTerm newTerm, final Map policies, - final Set newLabels) { - applicationTerm.execPreOrder((DefaultVisitor) p_visited -> { - final JTerm visited = (JTerm) p_visited; - if (visited != applicationTerm) { - for (TermLabel label : visited.getLabels()) { - ChildTermLabelPolicy policy = policies.get(label.name()); - if (policy != null && policy.addLabel(services, applicationPosInOccurrence, - applicationTerm, rule, goal, hint, tacletTerm, newTerm, visited, - label)) { - newLabels.add(label); - } - } - } - }); - } - - /** - *

    - * Performs the given child and grandchild {@link TermLabelUpdate} instances. - *

    - *

    - * This is a helper {@link Map} of - * {@link #instantiateLabels(TermLabelState, Services, PosInOccurrence, Rule, RuleApp, Goal, Object, JTerm, JTerm)} - *

    - * - * @param state The {@link TermLabelState} of the current rule application. - * @param services The {@link Services} used by the {@link Proof} on which a {@link Rule} is - * applied right now. - * @param applicationPosInOccurrence The {@link PosInOccurrence} in the previous {@link Sequent} - * which defines the {@link JTerm} that is rewritten. - * @param applicationTerm The {@link JTerm} defined by the {@link PosInOccurrence} in the - * previous {@link Sequent}. - * @param modalityTerm The optional modality {@link JTerm}. - * @param rule The {@link Rule} which is applied. - * @param ruleApp The {@link RuleApp} which is currently performed. - * @param hint An optional hint passed from the active rule to describe the term which should be - * created. - * @param tacletTerm The optional {@link JTerm} in the taclet which is responsible to - * instantiate - * the new {@link JTerm} for the new proof node or {@code null} in case of built in - * rules. - * @param newTerm the template for the new {@link JTerm} to create - * @param newLabels The result {@link Set} with the {@link TermLabel}s of the new {@link JTerm}. - */ - protected void performUpdater(TermLabelState state, Services services, - PosInOccurrence applicationPosInOccurrence, - JTerm applicationTerm, JTerm modalityTerm, - Rule rule, RuleApp ruleApp, Object hint, JTerm tacletTerm, - JTerm newTerm, - ImmutableList updater, - Set newLabels) { + protected void performUpdater(TermLabelContext context, JTerm newTerm, + ImmutableList updater, Set newLabels) { for (TermLabelUpdate update : updater) { - update.updateLabels(state, services, applicationPosInOccurrence, applicationTerm, - modalityTerm, rule, ruleApp, hint, tacletTerm, newTerm, newLabels); + update.updateLabels(context, newTerm, newLabels); } } @@ -1053,23 +729,21 @@ public JTerm refactorSequentFormula(TermLabelState state, Services services, JTerm tacletTerm) { final PosInTerm pos = applicationPosInOccurrence.posInTerm(); final JTerm oldTerm = (JTerm) pos.getSubTerm(sequentFormula); + final TermLabelContext context = new TermLabelContext(state, services, + applicationPosInOccurrence, oldTerm, null, rule, null, goal, hint, tacletTerm); // Compute active refactorings - RefactoringsContainer refactorings = computeRefactorings(state, services, - applicationPosInOccurrence, oldTerm, rule, goal, hint, tacletTerm); + RefactoringsContainer refactorings = computeRefactorings(context); // Perform refactoring JTerm newTerm = - refactorApplicationTerm(state, services, applicationPosInOccurrence, oldTerm, - rule, goal, hint, tacletTerm, refactorings, services.getTermFactory()); - if (newTerm != null && !newTerm.equals(oldTerm)) { - return replaceTerm(state, applicationPosInOccurrence, newTerm, + refactorApplicationTerm(context, refactorings, services.getTermFactory()); + if (newTerm != null && !newTerm.equalsIncludingLabels(oldTerm)) { + return replaceTerm(context, applicationPosInOccurrence, newTerm, services.getTermFactory(), - refactorings.childAndGrandchildRefactoringsAndParents(), services, - applicationPosInOccurrence, oldTerm, rule, goal, hint, tacletTerm); + refactorings.childAndGrandchildRefactoringsAndParents()); } else if (!refactorings.childAndGrandchildRefactoringsAndParents().isEmpty()) { - return replaceTerm(state, applicationPosInOccurrence, oldTerm, + return replaceTerm(context, applicationPosInOccurrence, oldTerm, services.getTermFactory(), - refactorings.childAndGrandchildRefactoringsAndParents(), services, - applicationPosInOccurrence, oldTerm, rule, goal, hint, tacletTerm); + refactorings.childAndGrandchildRefactoringsAndParents()); } else { return sequentFormula; } @@ -1131,13 +805,13 @@ public JTerm refactorTerm(TermLabelState state, Services services, PosInOccurrence applicationPosInOccurrence, JTerm applicationTerm, Goal goal, Object hint, Rule rule, JTerm tacletTerm) { + final TermLabelContext context = new TermLabelContext(state, services, + applicationPosInOccurrence, applicationTerm, null, rule, null, goal, hint, tacletTerm); // Compute active refactorings - RefactoringsContainer refactorings = computeRefactorings(state, services, - applicationPosInOccurrence, applicationTerm, rule, goal, hint, tacletTerm); + RefactoringsContainer refactorings = computeRefactorings(context); // Refactor application term JTerm newApplicationTerm = - refactorApplicationTerm(state, services, applicationPosInOccurrence, applicationTerm, - rule, goal, hint, tacletTerm, refactorings, services.getTermFactory()); + refactorApplicationTerm(context, refactorings, services.getTermFactory()); return newApplicationTerm != null ? newApplicationTerm : applicationTerm; } @@ -1203,33 +877,29 @@ public void refactorGoal(TermLabelState state, Services services, PosInOccurrence applicationPosInOccurrence, JTerm applicationTerm, Rule rule, Goal goal, Object hint, JTerm tacletTerm) { + final TermLabelContext context = new TermLabelContext(state, services, + applicationPosInOccurrence, applicationTerm, null, rule, null, goal, hint, tacletTerm); // Compute active refactorings - RefactoringsContainer refactorings = computeRefactorings(state, services, - applicationPosInOccurrence, applicationTerm, rule, goal, hint, tacletTerm); + RefactoringsContainer refactorings = computeRefactorings(context); // Refactor application term final TermFactory tf = services.getTermFactory(); - JTerm newApplicationTerm = - refactorApplicationTerm(state, services, applicationPosInOccurrence, applicationTerm, - rule, goal, hint, tacletTerm, refactorings, tf); - if (newApplicationTerm != null && !newApplicationTerm.equals(applicationTerm)) { - JTerm root = replaceTerm(state, applicationPosInOccurrence, newApplicationTerm, tf, - refactorings.childAndGrandchildRefactoringsAndParents(), services, - applicationPosInOccurrence, newApplicationTerm, rule, goal, hint, tacletTerm); + JTerm newApplicationTerm = refactorApplicationTerm(context, refactorings, tf); + if (newApplicationTerm != null + && !newApplicationTerm.equalsIncludingLabels(applicationTerm)) { + JTerm root = replaceTerm(context, applicationPosInOccurrence, newApplicationTerm, tf, + refactorings.childAndGrandchildRefactoringsAndParents()); goal.changeFormula(new SequentFormula(root), applicationPosInOccurrence.topLevel()); } else if (!refactorings.childAndGrandchildRefactoringsAndParents().isEmpty()) { - JTerm root = replaceTerm(state, applicationPosInOccurrence, applicationTerm, tf, - refactorings.childAndGrandchildRefactoringsAndParents(), services, - applicationPosInOccurrence, newApplicationTerm, rule, goal, hint, tacletTerm); + JTerm root = replaceTerm(context, applicationPosInOccurrence, applicationTerm, tf, + refactorings.childAndGrandchildRefactoringsAndParents()); goal.changeFormula(new SequentFormula(root), applicationPosInOccurrence.topLevel()); } // Do sequent refactoring if required if (!refactorings.sequentRefactorings().isEmpty() && goal != null) { Sequent sequent = goal.sequent(); - refactorSemisequent(state, services, applicationPosInOccurrence, applicationTerm, rule, - goal, hint, tacletTerm, sequent.antecedent(), true, + refactorSemisequent(context, sequent.antecedent(), true, refactorings.sequentRefactorings()); - refactorSemisequent(state, services, applicationPosInOccurrence, applicationTerm, rule, - goal, hint, tacletTerm, sequent.succedent(), false, + refactorSemisequent(context, sequent.succedent(), false, refactorings.sequentRefactorings()); } } @@ -1296,17 +966,16 @@ public void refactorSequent(TermLabelState state, Services services, PosInOccurrence applicationPosInOccurrence, JTerm applicationTerm, Rule rule, Goal goal, Object hint, JTerm tacletTerm) { + final TermLabelContext context = new TermLabelContext(state, services, + applicationPosInOccurrence, applicationTerm, null, rule, null, goal, hint, tacletTerm); // Compute active refactorings - RefactoringsContainer refactorings = computeRefactorings(state, services, - applicationPosInOccurrence, applicationTerm, rule, goal, hint, tacletTerm); + RefactoringsContainer refactorings = computeRefactorings(context); // Do sequent refactoring if required if (!refactorings.sequentRefactorings().isEmpty()) { Sequent sequent = goal.sequent(); - refactorSemisequent(state, services, applicationPosInOccurrence, applicationTerm, rule, - goal, hint, tacletTerm, sequent.antecedent(), true, + refactorSemisequent(context, sequent.antecedent(), true, refactorings.sequentRefactorings()); - refactorSemisequent(state, services, applicationPosInOccurrence, applicationTerm, rule, - goal, hint, tacletTerm, sequent.succedent(), false, + refactorSemisequent(context, sequent.succedent(), false, refactorings.sequentRefactorings()); } } @@ -1314,32 +983,17 @@ public void refactorSequent(TermLabelState state, Services services, /** * Replaces the {@link JTerm} at the specified {@link PosInOccurrence}. * - * @param state The {@link TermLabelState} of the current rule application. + * @param context the {@link TermLabelContext} of the current rule application * @param pio The {@link PosInOccurrence} to replace {@link JTerm} at. * @param newTerm The new {@link JTerm} to set. * @param tf The {@link TermFactory} to use. - * @param parentRefactorings The {@link RefactoringsContainer} to consider. - * @param services The {@link Services} used by the {@link Proof} on which a {@link Rule} is - * applied right now. - * @param applicationPosInOccurrence The {@link PosInOccurrence} in the previous {@link Sequent} - * which defines the {@link JTerm} that is rewritten. - * @param applicationTerm The {@link JTerm} defined by the {@link PosInOccurrence} in the - * previous {@link Sequent}. - * @param rule The {@link Rule} which is applied. - * @param goal The optional {@link Goal} on which the {@link JTerm} to create will be used. - * @param hint An optional hint passed from the active rule to describe the term which should be - * created. - * @param tacletTerm The optional taclet {@link JTerm}. + * @param parentRefactorings The parent {@link TermLabelRefactoring}s to consider. * @return The root of the {@link PosInOccurrence} containing the new {@link JTerm} at the * specified {@link PosInOccurrence}. */ - protected JTerm replaceTerm(TermLabelState state, + protected JTerm replaceTerm(TermLabelContext context, PosInOccurrence pio, JTerm newTerm, - TermFactory tf, Set parentRefactorings, - Services services, - PosInOccurrence applicationPosInOccurrence, - JTerm applicationTerm, - Rule rule, Goal goal, Object hint, JTerm tacletTerm) { + TermFactory tf, Set parentRefactorings) { do { if (pio.isTopLevel()) { pio = null; @@ -1350,8 +1004,7 @@ protected JTerm replaceTerm(TermLabelState state, newTerm = (JTerm) pio.subTerm(); ImmutableArray newLabels; if (!parentRefactorings.isEmpty()) { - newLabels = performRefactoring(state, services, applicationPosInOccurrence, - applicationTerm, rule, goal, hint, tacletTerm, newTerm, parentRefactorings); + newLabels = performRefactoring(context, newTerm, parentRefactorings); } else { newLabels = newTerm.getLabels(); } @@ -1359,7 +1012,7 @@ protected JTerm replaceTerm(TermLabelState state, newSubs[childIndex] = newChild; ImmutableArray newSubsImmutable = new ImmutableArray<>(newSubs); - if (!newSubsImmutable.equals(newTerm.subs()) + if (!newSubs[childIndex].equalsIncludingLabels(newTerm.sub(childIndex)) || !newLabels.equals(newTerm.getLabels())) { newTerm = tf.createTerm(newTerm.op(), newSubsImmutable, newTerm.boundVars(), newLabels); @@ -1370,123 +1023,74 @@ protected JTerm replaceTerm(TermLabelState state, } /** - * Computes the rule-independent {@link TermLabelRefactoring} to consider. + * Computes the rule-specific {@link TermLabelRefactoring} to consider. * - * @param state The {@link TermLabelState} of the current rule application. - * @param services The {@link Services} used by the {@link Proof} on which a {@link Rule} is - * applied right now. - * @param applicationPosInOccurrence The {@link PosInOccurrence} in the previous {@link Sequent} - * which defines the {@link JTerm} that is rewritten. - * @param applicationTerm The {@link JTerm} defined by the {@link PosInOccurrence} in the - * previous {@link Sequent}. - * @param rule The {@link Rule} which is applied. - * @param goal The optional {@link Goal} on which the {@link JTerm} to create will be used. - * @param hint An optional hint passed from the active rule to describe the term which should be - * created. - * @param tacletTerm The optional taclet {@link JTerm}. + * @param context the {@link TermLabelContext} of the current rule application * @param refactorings The already accumulated refactorings to be expanded with rule specific * refactorings */ - private void determineAndCollectRuleSpecificRefactorings(TermLabelState state, - Services services, - PosInOccurrence applicationPosInOccurrence, - JTerm applicationTerm, - Rule rule, Goal goal, Object hint, JTerm tacletTerm, + private void determineAndCollectRuleSpecificRefactorings(TermLabelContext context, RefactoringsContainer refactorings) { + final Rule rule = context.rule(); if (rule != null) { ImmutableList ruleRefactorings = ruleSpecificRefactorings.get(rule.name()); if (ruleRefactorings != null) { for (TermLabelRefactoring refactoring : ruleRefactorings) { - RefactoringScope scope = refactoring.defineRefactoringScope(state, services, - applicationPosInOccurrence, applicationTerm, rule, goal, hint, tacletTerm); - if (RefactoringScope.SEQUENT.equals(scope)) { - refactorings.sequentRefactorings.add(refactoring); - } else if (RefactoringScope.APPLICATION_BELOW_UPDATES.equals(scope)) { - refactorings.belowUpdatesRefactorings.add(refactoring); - } else if (RefactoringScope.APPLICATION_CHILDREN_AND_GRANDCHILDREN_SUBTREE - .equals(scope)) { - refactorings.childAndGrandchildRefactorings.add(refactoring); - } else if (RefactoringScope.APPLICATION_DIRECT_CHILDREN.equals(scope)) { - refactorings.directChildRefactorings.add(refactoring); - } else if (RefactoringScope.APPLICATION_CHILDREN_AND_GRANDCHILDREN_SUBTREE_AND_PARENTS - .equals(scope)) { - refactorings.childAndGrandchildRefactoringsAndParents.add(refactoring); - } + collectRefactoring(context, refactoring, refactorings); } } } } + /** + * Sorts the given {@link TermLabelRefactoring} into the bucket of the + * {@link RefactoringScope} it requests for the current rule application. + * + * @param context the {@link TermLabelContext} of the current rule application + * @param refactoring the {@link TermLabelRefactoring} to sort in + * @param refactorings the accumulated refactorings + */ + private void collectRefactoring(TermLabelContext context, TermLabelRefactoring refactoring, + RefactoringsContainer refactorings) { + RefactoringScope scope = refactoring.defineRefactoringScope(context); + if (RefactoringScope.SEQUENT.equals(scope)) { + refactorings.sequentRefactorings.add(refactoring); + } else if (RefactoringScope.APPLICATION_BELOW_UPDATES.equals(scope)) { + refactorings.belowUpdatesRefactorings.add(refactoring); + } else if (RefactoringScope.APPLICATION_CHILDREN_AND_GRANDCHILDREN_SUBTREE + .equals(scope)) { + refactorings.childAndGrandchildRefactorings.add(refactoring); + } else if (RefactoringScope.APPLICATION_CHILDREN_AND_GRANDCHILDREN_SUBTREE_AND_PARENTS + .equals(scope)) { + refactorings.childAndGrandchildRefactoringsAndParents.add(refactoring); + } + } + /** * Computes the rule-independent {@link TermLabelRefactoring} to consider. * - * @param state The {@link TermLabelState} of the current rule application. - * @param services The {@link Services} used by the {@link Proof} on which a {@link Rule} is - * applied right now. - * @param applicationPosInOccurrence The {@link PosInOccurrence} in the previous {@link Sequent} - * which defines the {@link JTerm} that is rewritten. - * @param applicationTerm The {@link JTerm} defined by the {@link PosInOccurrence} in the - * previous {@link Sequent}. - * @param rule The {@link Rule} which is applied. - * @param goal The optional {@link Goal} on which the {@link JTerm} to create will be used. - * @param hint An optional hint passed from the active rule to describe the term which should be - * created. - * @param tacletTerm The optional taclet {@link JTerm}. + * @param context the {@link TermLabelContext} of the current rule application * @param refactorings The already accumulated refactorings to be expanded with rule independent * refactorings */ - private void determineAndRuleIndependentRefactorings(TermLabelState state, - Services services, - PosInOccurrence applicationPosInOccurrence, - JTerm applicationTerm, - Rule rule, Goal goal, Object hint, JTerm tacletTerm, + private void determineAndRuleIndependentRefactorings(TermLabelContext context, RefactoringsContainer refactorings) { for (TermLabelRefactoring refactoring : allRulesRefactorings) { - RefactoringScope scope = refactoring.defineRefactoringScope(state, services, - applicationPosInOccurrence, applicationTerm, rule, goal, hint, tacletTerm); - if (RefactoringScope.SEQUENT.equals(scope)) { - refactorings.sequentRefactorings.add(refactoring); - } else if (RefactoringScope.APPLICATION_BELOW_UPDATES.equals(scope)) { - refactorings.belowUpdatesRefactorings.add(refactoring); - } else if (RefactoringScope.APPLICATION_CHILDREN_AND_GRANDCHILDREN_SUBTREE - .equals(scope)) { - refactorings.childAndGrandchildRefactorings.add(refactoring); - } else if (RefactoringScope.APPLICATION_DIRECT_CHILDREN.equals(scope)) { - refactorings.directChildRefactorings.add(refactoring); - } else if (RefactoringScope.APPLICATION_CHILDREN_AND_GRANDCHILDREN_SUBTREE_AND_PARENTS - .equals(scope)) { - refactorings.childAndGrandchildRefactoringsAndParents.add(refactoring); - } + collectRefactoring(context, refactoring, refactorings); } } /** * Computes the {@link TermLabelRefactoring} to consider. * - * @param state The {@link TermLabelState} of the current rule application. - * @param services The {@link Services} used by the {@link Proof} on which a {@link Rule} is - * applied right now. - * @param applicationPosInOccurrence The {@link PosInOccurrence} in the previous {@link Sequent} - * which defines the {@link JTerm} that is rewritten. - * @param applicationTerm The {@link JTerm} defined by the {@link PosInOccurrence} in the - * previous {@link Sequent}. - * @param rule The {@link Rule} which is applied. - * @param goal The optional {@link Goal} on which the {@link JTerm} to create will be used. - * @param hint An optional hint passed from the active rule to describe the term which should be - * created. - * @param tacletTerm The optional taclet {@link JTerm}. + * @param context the {@link TermLabelContext} of the current rule application * @return The {@link RefactoringsContainer} with the {@link TermLabelRefactoring}s to consider. */ - protected RefactoringsContainer computeRefactorings(TermLabelState state, Services services, - PosInOccurrence applicationPosInOccurrence, - JTerm applicationTerm, Rule rule, Goal goal, - Object hint, JTerm tacletTerm) { + protected RefactoringsContainer computeRefactorings(TermLabelContext context) { final RefactoringsContainer refactorings = new RefactoringsContainer(); - determineAndCollectRuleSpecificRefactorings(state, services, applicationPosInOccurrence, - applicationTerm, rule, goal, hint, tacletTerm, refactorings); - determineAndRuleIndependentRefactorings(state, services, applicationPosInOccurrence, - applicationTerm, rule, goal, hint, tacletTerm, refactorings); + determineAndCollectRuleSpecificRefactorings(context, refactorings); + determineAndRuleIndependentRefactorings(context, refactorings); return refactorings; } @@ -1495,8 +1099,7 @@ public Map> getFactories() { } /** - * Utility class used by - * {@link TermLabelManager#computeRefactorings(TermLabelState, Services, PosInOccurrence, JTerm, Rule, Goal, Object, JTerm)} + * Utility class used by {@link TermLabelManager#computeRefactorings(TermLabelContext)} * * @param sequentRefactorings The {@link TermLabelRefactoring} for * {@link RefactoringScope#SEQUENT}. @@ -1506,18 +1109,15 @@ public Map> getFactories() { * {@link RefactoringScope#APPLICATION_CHILDREN_AND_GRANDCHILDREN_SUBTREE}. * @param childAndGrandchildRefactoringsAndParents The {@link TermLabelRefactoring} for * {@link RefactoringScope#APPLICATION_CHILDREN_AND_GRANDCHILDREN_SUBTREE_AND_PARENTS}. - * @param directChildRefactorings The {@link TermLabelRefactoring} for - * {@link RefactoringScope#APPLICATION_DIRECT_CHILDREN}. * @author Martin Hentschel */ protected record RefactoringsContainer(Set sequentRefactorings, Set belowUpdatesRefactorings, Set childAndGrandchildRefactorings, - Set childAndGrandchildRefactoringsAndParents, - Set directChildRefactorings) { + Set childAndGrandchildRefactoringsAndParents) { public RefactoringsContainer() { this(new LinkedHashSet<>(), new LinkedHashSet<>(), new LinkedHashSet<>(), - new LinkedHashSet<>(), new LinkedHashSet<>()); + new LinkedHashSet<>()); } /** @@ -1535,94 +1135,28 @@ public Set getAllApplicationChildAndGrandchildRefactorings } } - /** - * Do direct child refactoring if required. - * - * @param state The {@link TermLabelState} of the current rule application. - * @param services The {@link Services} used by the {@link Proof} on which a {@link Rule} is - * applied right now. - * @param applicationPosInOccurrence The {@link PosInOccurrence} in the previous {@link Sequent} - * which defines the {@link JTerm} that is rewritten. - * @param applicationTerm The {@link JTerm} defined by the {@link PosInOccurrence} in the - * previous {@link Sequent}. - * @param rule The {@link Rule} which is applied. - * @param goal The optional {@link Goal} on which the {@link JTerm} to create will be used. - * @param hint An optional hint passed from the active rule to describe the term which should be - * created. - * @param tacletTerm The optional taclet {@link JTerm}. - * @param refactorings The {@link RefactoringsContainer} with the {@link TermLabelRefactoring}s - * to consider. - * @param tf The {@link TermFactory} to create the term. - * @return The new application {@link JTerm} or {@code null} if no refactoring was performed. - */ - private JTerm refactorChildTerms(TermLabelState state, Services services, - PosInOccurrence applicationPosInOccurrence, - JTerm applicationTerm, Rule rule, Goal goal, - Object hint, JTerm tacletTerm, RefactoringsContainer refactorings, TermFactory tf) { - JTerm newApplicationTerm = applicationTerm; - if (!refactorings.directChildRefactorings().isEmpty()) { - boolean changed = false; - JTerm[] newSubs = new JTerm[newApplicationTerm.arity()]; - for (int i = 0; i < newSubs.length; i++) { - final JTerm sub = newApplicationTerm.sub(i); - ImmutableArray newLabels = performRefactoring(state, services, - applicationPosInOccurrence, applicationTerm, rule, goal, hint, tacletTerm, sub, - refactorings.directChildRefactorings()); - - if (newLabels != sub.getLabels()) { - newSubs[i] = - tf.createTerm(sub.op(), sub.subs(), sub.boundVars(), - newLabels); - changed = true; - } else { - newSubs[i] = sub; - } - } - newApplicationTerm = changed ? tf.createTerm(newApplicationTerm.op(), newSubs, - newApplicationTerm.boundVars(), - newApplicationTerm.getLabels()) : applicationTerm; - } - return newApplicationTerm; - } - - /** * Perform below-updates refactoring if required. * - * @param state The {@link TermLabelState} of the current rule application. - * @param services The {@link Services} used by the {@link Proof} on which a {@link Rule} is - * applied right now. - * @param applicationPosInOccurrence The {@link PosInOccurrence} in the previous {@link Sequent} - * which defines the {@link JTerm} that is rewritten. - * @param applicationTerm The {@link JTerm} defined by the {@link PosInOccurrence} in the - * previous {@link Sequent}. - * @param rule The {@link Rule} which is applied. - * @param goal The optional {@link Goal} on which the {@link JTerm} to create will be used. - * @param hint An optional hint passed from the active rule to describe the term which should be - * created. - * @param tacletTerm The optional taclet {@link JTerm}. + * @param context the {@link TermLabelContext} of the current rule application * @param refactorings The {@link RefactoringsContainer} with the {@link TermLabelRefactoring}s * to consider. * @param tf The {@link TermFactory} to create the term. * @param newApplicationTerm The refactored application term until now. * @return The new application {@link JTerm} or {@code null} if no refactoring was performed. */ - private JTerm refactorBelowUpdates(TermLabelState state, Services services, - PosInOccurrence applicationPosInOccurrence, - JTerm applicationTerm, Rule rule, Goal goal, - Object hint, JTerm tacletTerm, RefactoringsContainer refactorings, TermFactory tf, - JTerm newApplicationTerm) { + private JTerm refactorBelowUpdates(TermLabelContext context, + RefactoringsContainer refactorings, TermFactory tf, JTerm newApplicationTerm) { if (!refactorings.belowUpdatesRefactorings().isEmpty()) { Pair, JTerm> pair = TermBuilder.goBelowUpdates2(newApplicationTerm); - ImmutableArray newLabels = performRefactoring(state, services, - applicationPosInOccurrence, applicationTerm, rule, goal, hint, tacletTerm, - pair.second, refactorings.belowUpdatesRefactorings()); + ImmutableArray newLabels = performRefactoring(context, pair.second, + refactorings.belowUpdatesRefactorings()); if (newLabels != pair.second.getLabels()) { JTerm newModality = tf.createTerm(pair.second.op(), pair.second.subs(), pair.second.boundVars(), newLabels); newApplicationTerm = - services.getTermBuilder().applyParallel(pair.first, newModality, + context.services().getTermBuilder().applyParallel(pair.first, newModality, newApplicationTerm.getLabels()); } } @@ -1632,29 +1166,15 @@ private JTerm refactorBelowUpdates(TermLabelState state, Services services, /** * Do child and grandchild refactoring if required. * - * @param state The {@link TermLabelState} of the current rule application. - * @param services The {@link Services} used by the {@link Proof} on which a {@link Rule} is - * applied right now. - * @param applicationPosInOccurrence The {@link PosInOccurrence} in the previous {@link Sequent} - * which defines the {@link JTerm} that is rewritten. - * @param applicationTerm The {@link JTerm} defined by the {@link PosInOccurrence} in the - * previous {@link Sequent}. - * @param rule The {@link Rule} which is applied. - * @param goal The optional {@link Goal} on which the {@link JTerm} to create will be used. - * @param hint An optional hint passed from the active rule to describe the term which should be - * created. - * @param tacletTerm The optional taclet {@link JTerm}. + * @param context the {@link TermLabelContext} of the current rule application * @param refactorings The {@link RefactoringsContainer} with the {@link TermLabelRefactoring}s * to consider. * @param tf The {@link TermFactory} to create the term. * @param newApplicationTerm The refactored application term until now. * @return The new application {@link JTerm} or {@code null} if no refactoring was performed. */ - private JTerm refactorChildrenRecursively(TermLabelState state, Services services, - PosInOccurrence applicationPosInOccurrence, - JTerm applicationTerm, Rule rule, Goal goal, - Object hint, JTerm tacletTerm, RefactoringsContainer refactorings, TermFactory tf, - JTerm newApplicationTerm) { + private JTerm refactorChildrenRecursively(TermLabelContext context, + RefactoringsContainer refactorings, TermFactory tf, JTerm newApplicationTerm) { final Set allChildAndGrandchildRefactorings = refactorings.getAllApplicationChildAndGrandchildRefactorings(); if (!allChildAndGrandchildRefactorings.isEmpty()) { @@ -1662,10 +1182,9 @@ private JTerm refactorChildrenRecursively(TermLabelState state, Services service JTerm[] newSubs = new JTerm[newApplicationTerm.arity()]; for (int i = 0; i < newSubs.length; i++) { JTerm sub = newApplicationTerm.sub(i); - newSubs[i] = refactorLabelsRecursive(state, services, applicationPosInOccurrence, - applicationTerm, rule, goal, hint, tacletTerm, sub, - allChildAndGrandchildRefactorings); - if (!newSubs[i].equals(sub)) { + newSubs[i] = + refactorLabelsRecursive(context, sub, allChildAndGrandchildRefactorings); + if (!newSubs[i].equalsIncludingLabels(sub)) { changed = true; } } @@ -1680,42 +1199,24 @@ private JTerm refactorChildrenRecursively(TermLabelState state, Services service /** * Refactors the labels of the application term. * - * @param state The {@link TermLabelState} of the current rule application. - * @param services The {@link Services} used by the {@link Proof} on which a {@link Rule} is - * applied right now. - * @param applicationPosInOccurrence The {@link PosInOccurrence} in the previous {@link Sequent} - * which defines the {@link JTerm} that is rewritten. - * @param applicationTerm The {@link JTerm} defined by the {@link PosInOccurrence} in the - * previous {@link Sequent}. - * @param rule The {@link Rule} which is applied. - * @param goal The optional {@link Goal} on which the {@link JTerm} to create will be used. - * @param hint An optional hint passed from the active rule to describe the term which should be - * created. - * @param tacletTerm The optional taclet {@link JTerm}. + * @param context the {@link TermLabelContext} of the current rule application * @param refactorings The {@link RefactoringsContainer} with the {@link TermLabelRefactoring}s * to consider. * @param tf The {@link TermFactory} to create the term. * @return The new application {@link JTerm} or {@code null} if no refactoring was performed. */ - protected JTerm refactorApplicationTerm(TermLabelState state, Services services, - PosInOccurrence applicationPosInOccurrence, - JTerm applicationTerm, Rule rule, Goal goal, - Object hint, JTerm tacletTerm, RefactoringsContainer refactorings, TermFactory tf) { - if (applicationTerm != null && (!refactorings.directChildRefactorings().isEmpty() - || !refactorings.childAndGrandchildRefactorings().isEmpty() + protected JTerm refactorApplicationTerm(TermLabelContext context, + RefactoringsContainer refactorings, TermFactory tf) { + final JTerm applicationTerm = context.applicationTerm(); + if (applicationTerm != null && (!refactorings.childAndGrandchildRefactorings().isEmpty() || !refactorings.belowUpdatesRefactorings().isEmpty())) { - JTerm newApplicationTerm; - // Do direct child refactoring if required - newApplicationTerm = refactorChildTerms(state, services, applicationPosInOccurrence, - applicationTerm, rule, goal, hint, tacletTerm, refactorings, tf); + JTerm newApplicationTerm = applicationTerm; // Perform below-updates refactoring newApplicationTerm = - refactorBelowUpdates(state, services, applicationPosInOccurrence, applicationTerm, - rule, goal, hint, tacletTerm, refactorings, tf, newApplicationTerm); + refactorBelowUpdates(context, refactorings, tf, newApplicationTerm); // Do child and grandchild refactoring if required - newApplicationTerm = refactorChildrenRecursively(state, services, - applicationPosInOccurrence, applicationTerm, rule, goal, hint, tacletTerm, - refactorings, tf, newApplicationTerm); + newApplicationTerm = + refactorChildrenRecursively(context, refactorings, tf, newApplicationTerm); return newApplicationTerm; } else { return null; @@ -1725,35 +1226,19 @@ protected JTerm refactorApplicationTerm(TermLabelState state, Services services, /** * Performs a {@link TermLabel} refactoring on the given {@link Semisequent}. * - * @param state The {@link TermLabelState} of the current rule application. - * @param services The {@link Services} used by the {@link Proof} on which a {@link Rule} is - * applied right now. - * @param applicationPosInOccurrence The {@link PosInOccurrence} in the previous {@link Sequent} - * which defines the {@link JTerm} that is rewritten. - * @param applicationTerm The {@link JTerm} defined by the {@link PosInOccurrence} in the - * previous {@link Sequent}. - * @param rule The {@link Rule} which is applied. - * @param goal The optional {@link Goal} on which the {@link JTerm} to create will be used. - * @param hint An optional hint passed from the active rule to describe the term which should be - * created. - * @param tacletTerm The optional taclet {@link JTerm}. + * @param context the {@link TermLabelContext} of the current rule application * @param semisequent The {@link Semisequent} to refactor. * @param inAntec {@code true} antecedent, {@code false} succedent. * @param activeRefactorings The active {@link TermLabelRefactoring}s to execute. */ - protected void refactorSemisequent(TermLabelState state, Services services, - PosInOccurrence applicationPosInOccurrence, - JTerm applicationTerm, Rule rule, Goal goal, - Object hint, JTerm tacletTerm, Semisequent semisequent, boolean inAntec, - Set activeRefactorings) { + protected void refactorSemisequent(TermLabelContext context, Semisequent semisequent, + boolean inAntec, Set activeRefactorings) { if (!activeRefactorings.isEmpty()) { for (SequentFormula sfa : semisequent) { JTerm updatedTerm = - refactorLabelsRecursive(state, services, applicationPosInOccurrence, - applicationTerm, rule, goal, hint, tacletTerm, (JTerm) sfa.formula(), - activeRefactorings); - if (!sfa.formula().equals(updatedTerm)) { - goal.changeFormula(new SequentFormula(updatedTerm), + refactorLabelsRecursive(context, (JTerm) sfa.formula(), activeRefactorings); + if (!((JTerm) sfa.formula()).equalsIncludingLabels(updatedTerm)) { + context.goal().changeFormula(new SequentFormula(updatedTerm), new PosInOccurrence(sfa, PosInTerm.getTopLevel(), inAntec)); } } @@ -1763,41 +1248,25 @@ protected void refactorSemisequent(TermLabelState state, Services services, /** * Performs a {@link TermLabel} refactoring recursively on the given {@link JTerm}. * - * @param state The {@link TermLabelState} of the current rule application. - * @param services The {@link Services} used by the {@link Proof} on which a {@link Rule} is - * applied right now. - * @param applicationPosInOccurrence The {@link PosInOccurrence} in the previous {@link Sequent} - * which defines the {@link JTerm} that is rewritten. - * @param applicationTerm The {@link JTerm} defined by the {@link PosInOccurrence} in the - * previous {@link Sequent}. - * @param rule The {@link Rule} which is applied. - * @param goal The optional {@link Goal} on which the {@link JTerm} to create will be used. - * @param hint An optional hint passed from the active rule to describe the term which should be - * created. - * @param tacletTerm The optional taclet {@link JTerm}. + * @param context the {@link TermLabelContext} of the current rule application * @param term The {@link JTerm} to refactor. * @param activeRefactorings The active {@link TermLabelRefactoring}s to execute. * @return The refactored {@link JTerm} in which the {@link TermLabel}s may have changed. */ - protected JTerm refactorLabelsRecursive(TermLabelState state, Services services, - PosInOccurrence applicationPosInOccurrence, - JTerm applicationTerm, Rule rule, Goal goal, - Object hint, JTerm tacletTerm, JTerm term, + protected JTerm refactorLabelsRecursive(TermLabelContext context, JTerm term, Set activeRefactorings) { boolean subsChanged = false; JTerm[] newSubs = new JTerm[term.arity()]; for (int i = 0; i < newSubs.length; i++) { JTerm oldSub = term.sub(i); - newSubs[i] = refactorLabelsRecursive(state, services, applicationPosInOccurrence, - applicationTerm, rule, goal, hint, tacletTerm, oldSub, activeRefactorings); - if (!newSubs[i].equals(oldSub)) { + newSubs[i] = refactorLabelsRecursive(context, oldSub, activeRefactorings); + if (!newSubs[i].equalsIncludingLabels(oldSub)) { subsChanged = true; } } ImmutableArray newLabels = - performRefactoring(state, services, applicationPosInOccurrence, applicationTerm, rule, - goal, hint, tacletTerm, term, activeRefactorings); - return subsChanged || newLabels != term.getLabels() ? services.getTermFactory() + performRefactoring(context, term, activeRefactorings); + return subsChanged || newLabels != term.getLabels() ? context.services().getTermFactory() .createTerm(term.op(), newSubs, term.boundVars(), newLabels) : term; } @@ -1805,34 +1274,19 @@ protected JTerm refactorLabelsRecursive(TermLabelState state, Services services, /** * Computes the new labels as part of the refactoring for the given {@link JTerm}. * - * @param state The {@link TermLabelState} of the current rule application. - * @param services The {@link Services} used by the {@link Proof} on which a {@link Rule} is - * applied right now. - * @param applicationPosInOccurrence The {@link PosInOccurrence} in the previous {@link Sequent} - * which defines the {@link JTerm} that is rewritten. - * @param applicationTerm The {@link JTerm} defined by the {@link PosInOccurrence} in the - * previous {@link Sequent}. - * @param rule The {@link Rule} which is applied. - * @param goal The optional {@link Goal} on which the {@link JTerm} to create will be used. - * @param hint An optional hint passed from the active rule to describe the term which should be - * created. - * @param tacletTerm The optional taclet {@link JTerm}. + * @param context the {@link TermLabelContext} of the current rule application * @param term The {@link JTerm} to refactor. * @param activeRefactorings The active {@link TermLabelRefactoring}s to execute. * @return The new {@link TermLabel} which should be used for the given {@link JTerm}. */ - protected ImmutableArray performRefactoring(TermLabelState state, Services services, - PosInOccurrence applicationPosInOccurrence, - JTerm applicationTerm, Rule rule, Goal goal, - Object hint, JTerm tacletTerm, JTerm term, + protected ImmutableArray performRefactoring(TermLabelContext context, JTerm term, Set activeRefactorings) { // Create list with all old labels LabelCollection newLabels = new LabelCollection(term.getLabels()); // Give all TermLabelInstantiator instances the chance to remove or to // add labels from/to the list for (TermLabelRefactoring refactoring : activeRefactorings) { - refactoring.refactorLabels(state, services, applicationPosInOccurrence, applicationTerm, - rule, goal, hint, tacletTerm, term, newLabels); + refactoring.refactorLabels(context, term, newLabels); } if (newLabels.isModified()) { return new ImmutableArray<>(newLabels.getLabels()); @@ -1868,16 +1322,6 @@ public static final class TermLabelConfiguration { */ private final ImmutableList modalityTermPolicies; - /** - * The direct {@link ChildTermLabelPolicy} instances to use. - */ - private final ImmutableList directChildTermLabelPolicies; - - /** - * The child and grandchild {@link ChildTermLabelPolicy} instances to use. - */ - private final ImmutableList childAndGrandchildTermLabelPolicies; - /** * The {@link TermLabelUpdate} instances. */ @@ -1900,7 +1344,7 @@ public static final class TermLabelConfiguration { * @param factory The {@link TermLabelFactory} to use. */ public TermLabelConfiguration(Name termLabelName, TermLabelFactory factory) { - this(termLabelName, factory, null, null, null, null, null, null, null); + this(termLabelName, factory, null, null, null, null, null); } /** @@ -1912,10 +1356,6 @@ public TermLabelConfiguration(Name termLabelName, TermLabelFactory factory) { * application term. * @param modalityTermPolicies The {@link TermLabelPolicy} instances applied on the modality * term. - * @param directChildTermLabelPolicies The direct {@link ChildTermLabelPolicy} instances to - * use. - * @param childAndGrandchildTermLabelPolicies The child and grandchild - * {@link ChildTermLabelPolicy} instances to use. * @param termLabelUpdates The {@link TermLabelUpdate} instances. * @param termLabelRefactorings The {@link TermLabelRefactoring} instances. * @param termLabelMerger The {@link TermLabelMerger} instance. @@ -1923,8 +1363,6 @@ public TermLabelConfiguration(Name termLabelName, TermLabelFactory factory) { public TermLabelConfiguration(Name termLabelName, TermLabelFactory factory, ImmutableList applicationTermPolicies, ImmutableList modalityTermPolicies, - ImmutableList directChildTermLabelPolicies, - ImmutableList childAndGrandchildTermLabelPolicies, ImmutableList termLabelUpdates, ImmutableList termLabelRefactorings, TermLabelMerger termLabelMerger) { @@ -1934,8 +1372,6 @@ public TermLabelConfiguration(Name termLabelName, TermLabelFactory factory, this.factory = factory; this.applicationTermPolicies = applicationTermPolicies; this.modalityTermPolicies = modalityTermPolicies; - this.directChildTermLabelPolicies = directChildTermLabelPolicies; - this.childAndGrandchildTermLabelPolicies = childAndGrandchildTermLabelPolicies; this.termLabelUpdates = termLabelUpdates; this.termLabelRefactorings = termLabelRefactorings; this.termLabelMerger = termLabelMerger; @@ -1977,24 +1413,6 @@ public ImmutableList getModalityTermPolicies() { return modalityTermPolicies; } - /** - * Returns the direct {@link ChildTermLabelPolicy} instances to use. - * - * @return The direct {@link ChildTermLabelPolicy} instances to use. - */ - public ImmutableList getDirectChildTermLabelPolicies() { - return directChildTermLabelPolicies; - } - - /** - * Returns the child and grandchild {@link ChildTermLabelPolicy} instances to use. - * - * @return The child and grandchild {@link ChildTermLabelPolicy} instances to use. - */ - public ImmutableList getChildAndGrandchildTermLabelPolicies() { - return childAndGrandchildTermLabelPolicies; - } - /** * Returns the {@link TermLabelUpdate} instances. * diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/OpReplacer.java b/key.core/src/main/java/de/uka/ilkd/key/proof/OpReplacer.java index 4b6338c6e8d..3fceea0cf6e 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/OpReplacer.java +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/OpReplacer.java @@ -18,7 +18,6 @@ import org.key_project.util.collection.ImmutableList; import org.key_project.util.collection.ImmutableSet; -import static de.uka.ilkd.key.logic.equality.TermLabelsProperty.TERM_LABELS_PROPERTY; /** @@ -235,7 +234,7 @@ public JTerm replace(JTerm term) { } for (SyntaxElement svs : map.keySet()) { - if (svs instanceof JTerm t && TERM_LABELS_PROPERTY.equalsModThisProperty(term, t)) { + if (svs instanceof JTerm t && term.equals(t)) { return (JTerm) map.get(svs); } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/PrefixTermTacletAppIndexCacheImpl.java b/key.core/src/main/java/de/uka/ilkd/key/proof/PrefixTermTacletAppIndexCacheImpl.java index c563566ddec..de5e5280200 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/PrefixTermTacletAppIndexCacheImpl.java +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/PrefixTermTacletAppIndexCacheImpl.java @@ -5,6 +5,8 @@ import java.util.Map; +import de.uka.ilkd.key.logic.JTerm; + import org.key_project.logic.Term; import org.key_project.logic.op.QuantifiableVariable; import org.key_project.util.collection.ImmutableList; @@ -98,7 +100,10 @@ public boolean equals(Object obj) { return false; } - return parent == objKey.parent && analysedTerm.equals(objKey.analysedTerm); + // label-sensitive comparison: taclet applicability can depend on term labels + // (e.g. TermLabelCondition), so label variants must not share index entries + return parent == objKey.parent + && ((JTerm) analysedTerm).equalsIncludingLabels(objKey.analysedTerm); } public int hashCode() { diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/init/JavaProfile.java b/key.core/src/main/java/de/uka/ilkd/key/proof/init/JavaProfile.java index 27fc080a30b..ff03d18fac4 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/init/JavaProfile.java +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/init/JavaProfile.java @@ -147,7 +147,6 @@ protected ImmutableList computeTermLabelConfiguration() result = result.prepend(new TermLabelConfiguration(OriginTermLabel.NAME, new OriginTermLabelFactory(), originTermLabelPolicyList, null, null, - null, null, originTermLabelRefactorings, null)); result = diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/SyntacticalReplaceVisitor.java b/key.core/src/main/java/de/uka/ilkd/key/rule/SyntacticalReplaceVisitor.java index 71b977428d6..773691f5673 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/SyntacticalReplaceVisitor.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/SyntacticalReplaceVisitor.java @@ -367,8 +367,10 @@ public void visit(final Term p_visited) { pushNew(resolveSubst(newTerm)); } else { JTerm t; - final ImmutableArray labels = instantiateLabels(visited, visitedOp, - visited.subs(), visited.boundVars(), visited.getLabels()); + // The new term is structurally identical to visited (same op, subs, bound + // variables and labels), so pass visited itself to the label manager instead + // of rebuilding an equal throwaway term for every unchanged node. + final ImmutableArray labels = instantiateLabels(visited, visited); if (!visited.hasLabels() && labels != null && labels.isEmpty()) { t = visited; } else { @@ -389,11 +391,15 @@ private ImmutableArray instantiateLabels(JTerm tacletTerm, Operator n ImmutableArray newTermSubs, ImmutableArray newTermBoundVars, ImmutableArray newTermOriginalLabels) { - return TermLabelManager.instantiateLabels(termLabelState, services, - applicationPosInOccurrence, rule, ruleApp, goal, labelHint, tacletTerm, + return instantiateLabels(tacletTerm, tb.tf().createTerm(newTermOp, newTermSubs, newTermBoundVars, newTermOriginalLabels)); } + private ImmutableArray instantiateLabels(JTerm tacletTerm, JTerm newTerm) { + return TermLabelManager.instantiateLabels(termLabelState, services, + applicationPosInOccurrence, rule, ruleApp, goal, labelHint, tacletTerm, newTerm); + } + private Operator handleParametricFunction(ParametricFunctionInstance pfi) { ImmutableList args = ImmutableList.nil(); diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/UseDependencyContractRule.java b/key.core/src/main/java/de/uka/ilkd/key/rule/UseDependencyContractRule.java index 0f1b89bc6a0..53b8e1b7b1d 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/UseDependencyContractRule.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/UseDependencyContractRule.java @@ -40,7 +40,6 @@ import org.jspecify.annotations.NonNull; import org.jspecify.annotations.Nullable; -import static de.uka.ilkd.key.logic.equality.TermLabelsProperty.TERM_LABELS_PROPERTY; public final class UseDependencyContractRule implements BuiltInRule, ComplexJustificationable { @@ -225,7 +224,7 @@ public static boolean isBaseOcc(JTerm focus, JTerm candidate) { return false; } for (int i = 1, n = candidate.arity(); i < n; i++) { - if (!(candidate.sub(i).equalsModProperty(focus.sub(i), TERM_LABELS_PROPERTY) + if (!(candidate.sub(i).equals(focus.sub(i)) || candidate.sub(i).op() instanceof LogicVariable)) { return false; } diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/label/ChildTermLabelPolicy.java b/key.core/src/main/java/de/uka/ilkd/key/rule/label/ChildTermLabelPolicy.java deleted file mode 100644 index 4c4a58e6e84..00000000000 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/label/ChildTermLabelPolicy.java +++ /dev/null @@ -1,105 +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.rule.label; - -import de.uka.ilkd.key.java.Services; -import de.uka.ilkd.key.logic.JTerm; -import de.uka.ilkd.key.logic.TermServices; -import de.uka.ilkd.key.logic.label.TermLabel; -import de.uka.ilkd.key.logic.label.TermLabelManager; -import de.uka.ilkd.key.logic.label.TermLabelState; -import de.uka.ilkd.key.proof.Goal; -import de.uka.ilkd.key.proof.Proof; - -import org.key_project.prover.rules.Rule; -import org.key_project.prover.rules.RuleApp; -import org.key_project.prover.sequent.PosInOccurrence; -import org.key_project.prover.sequent.Sequent; - -/** - *

    - * A {@link ChildTermLabelPolicy} is used by - * {@link TermLabelManager#instantiateLabels(TermLabelState, Services, PosInOccurrence, Rule, RuleApp, Goal, Object, JTerm, JTerm)} - * to decide for each {@link TermLabel} on a child or grandchild of the application {@link JTerm} if - * it should be re-added to the new {@link JTerm} or not. - *

    - *

    - * For more information about {@link TermLabel}s and how they are maintained during prove read the - * documentation of interface {@link TermLabel}. - *

    - * - * @author Martin Hentschel - * @see TermLabel - * @see TermLabelManager - */ -public interface ChildTermLabelPolicy extends RuleSpecificTask { - /** - * Decides if the currently active {@link Rule} application is supported or not. If it is not - * supported no iteration over children will be executed. Only if it returns {@code true} - * {@link #addLabel( TermServices, PosInOccurrence, JTerm, Rule, Goal, Object, JTerm, JTerm, JTerm, TermLabel)} - * will - * be called if a child {@link JTerm} contains a managed label. - * - * @param services The {@link Services} used by the {@link Proof} on which a {@link Rule} is - * applied right now. - * @param applicationPosInOccurrence The {@link PosInOccurrence} in the previous {@link Sequent} - * which defines the {@link JTerm} that is rewritten. - * @param applicationTerm The {@link JTerm} defined by the {@link PosInOccurrence} in the - * previous {@link Sequent}. - * @param rule The {@link Rule} which is applied. - * @param goal The optional {@link Goal} on which the {@link JTerm} to create will be used. - * @param hint An optional hint passed from the active rule to describe the term which should be - * created. - * @param tacletTerm The optional {@link JTerm} in the taclet which is responsible to - * instantiate - * the new {@link JTerm} for the new proof node or {@code null} in case of built in - * rules. - * @param newTerm the template for the new {@link JTerm} to create - * @return {@code true} keep {@link TermLabel} and add it to the new {@link JTerm}. - * {@code false} - * drop {@link TermLabel} and do not need it to the new {@link JTerm}. - */ - boolean isRuleApplicationSupported(TermServices services, - PosInOccurrence applicationPosInOccurrence, - JTerm applicationTerm, Rule rule, Goal goal, - Object hint, JTerm tacletTerm, JTerm newTerm); - - /** - *

    - * Decides to add or not to add the given {@link TermLabel} on a child or grandchild of the - * application {@link JTerm} to the new {@link JTerm} which will be created. - *

    - *

    - * If the child {@link JTerm} is still a child of the new {@link JTerm} the label will still - * exist - * independent from the result of this method on the child. To remove it from the child a - * refacotring has to be used instead. - *

    - * - * @param services The {@link Services} used by the {@link Proof} on which a {@link Rule} is - * applied right now. - * @param applicationPosInOccurrence The {@link PosInOccurrence} in the previous {@link Sequent} - * which defines the {@link JTerm} that is rewritten. - * @param applicationTerm The {@link JTerm} defined by the {@link PosInOccurrence} in the - * previous {@link Sequent}. - * @param rule The {@link Rule} which is applied. - * @param goal The optional {@link Goal} on which the {@link JTerm} to create will be used. - * @param hint An optional hint passed from the active rule to describe the term which should be - * created. - * @param tacletTerm The optional {@link JTerm} in the taclet which is responsible to - * instantiate - * the new {@link JTerm} for the new proof node or {@code null} in case of built in - * rules. - * @param newTerm the template for the new {@link JTerm} to create - * @param childTerm The {@link JTerm} which is a child or grandchild of the application - * {@link JTerm} that provides the {@link TermLabel}. - * @param label The {@link TermLabel} to decide if it should be kept or dropped. - * @return {@code true} add {@link TermLabel} to new {@link JTerm}. {@code false} do not add - * {@link TermLabel} to new {@link JTerm}. - */ - boolean addLabel(TermServices services, - PosInOccurrence applicationPosInOccurrence, - JTerm applicationTerm, Rule rule, Goal goal, Object hint, JTerm tacletTerm, - JTerm newTerm, JTerm childTerm, TermLabel label); -} diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/label/OriginTermLabelPolicy.java b/key.core/src/main/java/de/uka/ilkd/key/rule/label/OriginTermLabelPolicy.java index 75e0afa259a..46697488d3b 100755 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/label/OriginTermLabelPolicy.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/label/OriginTermLabelPolicy.java @@ -3,16 +3,12 @@ * SPDX-License-Identifier: GPL-2.0-only */ package de.uka.ilkd.key.rule.label; -import de.uka.ilkd.key.java.Services; import de.uka.ilkd.key.logic.JTerm; import de.uka.ilkd.key.logic.label.OriginTermLabel; import de.uka.ilkd.key.logic.label.OriginTermLabel.SpecType; import de.uka.ilkd.key.logic.label.TermLabel; -import de.uka.ilkd.key.logic.label.TermLabelState; -import de.uka.ilkd.key.proof.Goal; +import de.uka.ilkd.key.logic.label.TermLabelContext; -import org.key_project.prover.rules.Rule; -import org.key_project.prover.sequent.PosInOccurrence; /** * Policy for {@link OriginTermLabel}s. @@ -24,19 +20,17 @@ public class OriginTermLabelPolicy implements TermLabelPolicy { @Override - public TermLabel keepLabel(TermLabelState state, Services services, - PosInOccurrence applicationPosInOccurrence, JTerm applicationTerm, Rule rule, Goal goal, - Object hint, JTerm tacletTerm, - JTerm newTerm, TermLabel label) { - if (services.getProof() == null) { + public TermLabel keepLabel(TermLabelContext context, JTerm sourceTerm, JTerm newTerm, + TermLabel label) { + if (context.services().getProof() == null) { return label; } - if (services.getTermBuilder().getOriginFactory() == null) { + if (context.services().getTermBuilder().getOriginFactory() == null) { return null; } - if (!OriginTermLabel.canAddLabel(newTerm.op(), services)) { + if (!OriginTermLabel.canAddLabel(newTerm.op(), context.services())) { return null; } diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/label/OriginTermLabelRefactoring.java b/key.core/src/main/java/de/uka/ilkd/key/rule/label/OriginTermLabelRefactoring.java index b7a14eae08d..5d718a333ba 100755 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/label/OriginTermLabelRefactoring.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/label/OriginTermLabelRefactoring.java @@ -8,15 +8,15 @@ import java.util.Map; import java.util.Set; -import de.uka.ilkd.key.java.Services; import de.uka.ilkd.key.logic.JTerm; +import de.uka.ilkd.key.logic.StrictTermKey; import de.uka.ilkd.key.logic.label.LabelCollection; import de.uka.ilkd.key.logic.label.OriginTermLabel; import de.uka.ilkd.key.logic.label.OriginTermLabel.Origin; import de.uka.ilkd.key.logic.label.OriginTermLabel.SpecType; import de.uka.ilkd.key.logic.label.OriginTermLabelFactory; import de.uka.ilkd.key.logic.label.TermLabel; -import de.uka.ilkd.key.logic.label.TermLabelState; +import de.uka.ilkd.key.logic.label.TermLabelContext; import de.uka.ilkd.key.proof.Goal; import de.uka.ilkd.key.rule.BuiltInRule; import de.uka.ilkd.key.rule.Taclet; @@ -24,7 +24,6 @@ import org.key_project.logic.Name; import org.key_project.prover.indexing.FormulaTag; import org.key_project.prover.rules.Rule; -import org.key_project.prover.sequent.PosInOccurrence; import org.key_project.util.collection.ImmutableArray; import org.key_project.util.collection.ImmutableList; @@ -43,14 +42,13 @@ public ImmutableList getSupportedRuleNames() { } @Override - public RefactoringScope defineRefactoringScope(TermLabelState state, Services services, - PosInOccurrence applicationPosInOccurrence, - JTerm applicationTerm, Rule rule, Goal goal, - Object hint, JTerm tacletTerm) { - if (rule instanceof BuiltInRule - && !TermLabelRefactoring.shouldRefactorOnBuiltInRule(rule, goal, hint)) { + public RefactoringScope defineRefactoringScope(TermLabelContext context) { + if (context.rule() instanceof BuiltInRule + && !TermLabelRefactoring.shouldRefactorOnBuiltInRule(context.rule(), context.goal(), + context.hint())) { return RefactoringScope.NONE; - } else if (rule instanceof Taclet && !shouldRefactorOnTaclet((Taclet) rule)) { + } else if (context.rule() instanceof Taclet + && !shouldRefactorOnTaclet((Taclet) context.rule())) { return RefactoringScope.NONE; } else { return RefactoringScope.APPLICATION_CHILDREN_AND_GRANDCHILDREN_SUBTREE; @@ -58,25 +56,24 @@ public RefactoringScope defineRefactoringScope(TermLabelState state, Services se } @Override - public void refactorLabels(TermLabelState state, Services services, - PosInOccurrence applicationPosInOccurrence, JTerm applicationTerm, Rule rule, Goal goal, - Object hint, JTerm tacletTerm, JTerm term, LabelCollection labels) { - if (services.getProof() == null) { + public void refactorLabels(TermLabelContext context, JTerm term, LabelCollection labels) { + if (context.services().getProof() == null) { return; } - if (rule instanceof BuiltInRule - && !TermLabelRefactoring.shouldRefactorOnBuiltInRule(rule, goal, hint)) { + if (context.rule() instanceof BuiltInRule + && !TermLabelRefactoring.shouldRefactorOnBuiltInRule(context.rule(), context.goal(), + context.hint())) { return; } - if (rule instanceof Taclet && !shouldRefactorOnTaclet((Taclet) rule)) { + if (context.rule() instanceof Taclet && !shouldRefactorOnTaclet((Taclet) context.rule())) { return; } final OriginTermLabel oldLabel = labels.getFirst(OriginTermLabel.class); - if (services.getTermBuilder().getOriginFactory() == null) { + if (context.services().getTermBuilder().getOriginFactory() == null) { if (oldLabel != null) { labels.remove(oldLabel); } @@ -85,13 +82,13 @@ public void refactorLabels(TermLabelState state, Services services, // cache origins per term to avoid a quadratic recursive collection per rule // application - final Map> originsCache = - services.getCaches().getSubtermOriginsCache(); + final Map> originsCache = + context.services().getCaches().getSubtermOriginsCache(); Set subtermOrigins = new LinkedHashSet<>(); for (JTerm sub : term.subs()) { subtermOrigins.addAll(collectSubtermOrigins(sub, originsCache)); } - OriginTermLabelFactory factory = services.getTermBuilder().getOriginFactory(); + OriginTermLabelFactory factory = context.services().getTermBuilder().getOriginFactory(); OriginTermLabel newLabel = null; if (oldLabel != null) { labels.remove(oldLabel); @@ -105,7 +102,7 @@ public void refactorLabels(TermLabelState state, Services services, if (newLabel != null) { final Origin origin = newLabel.getOrigin(); - if (OriginTermLabel.canAddLabel(term, services) + if (OriginTermLabel.canAddLabel(term, context.services()) && (!subtermOrigins.isEmpty() || origin.specType != SpecType.NONE)) { labels.add(newLabel); } @@ -135,8 +132,16 @@ private boolean shouldRefactorOnTaclet(Taclet taclet) { * subterms; the returned set is unmodifiable and shared, do not mutate */ @SuppressWarnings("unchecked") - private Set collectSubtermOrigins(JTerm term, Map> originsCache) { - Set cached = originsCache.get(term); + private Set collectSubtermOrigins(JTerm term, + Map> originsCache) { + // origins live in term labels: a label-free subtree cannot contribute any + if (!term.containsLabelsRecursive()) { + return Collections.emptySet(); + } + + // the cache key must be label-sensitive as the value is derived from the labels + final StrictTermKey key = new StrictTermKey(term); + Set cached = originsCache.get(key); if (cached != null) { return cached; } @@ -156,7 +161,7 @@ private Set collectSubtermOrigins(JTerm term, Map> or Set stored = result.isEmpty() ? Collections.emptySet() : Collections.unmodifiableSet(result); - originsCache.put(term, stored); + originsCache.put(key, stored); return stored; } diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/label/PerpetualTermLabelPolicy.java b/key.core/src/main/java/de/uka/ilkd/key/rule/label/PerpetualTermLabelPolicy.java index 6b552737bad..07ba2dd9552 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/label/PerpetualTermLabelPolicy.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/label/PerpetualTermLabelPolicy.java @@ -3,14 +3,10 @@ * SPDX-License-Identifier: GPL-2.0-only */ package de.uka.ilkd.key.rule.label; -import de.uka.ilkd.key.java.Services; import de.uka.ilkd.key.logic.JTerm; import de.uka.ilkd.key.logic.label.TermLabel; -import de.uka.ilkd.key.logic.label.TermLabelState; -import de.uka.ilkd.key.proof.Goal; +import de.uka.ilkd.key.logic.label.TermLabelContext; -import org.key_project.prover.rules.Rule; -import org.key_project.prover.sequent.PosInOccurrence; /** * This policy always maintains a label. @@ -20,10 +16,8 @@ public class PerpetualTermLabelPolicy implements TermLabelPolicy { @Override - public TermLabel keepLabel(TermLabelState state, Services services, - PosInOccurrence applicationPosInOccurrence, JTerm applicationTerm, Rule rule, Goal goal, - Object hint, JTerm tacletTerm, - JTerm newTerm, TermLabel label) { + public TermLabel keepLabel(TermLabelContext context, JTerm sourceTerm, JTerm newTerm, + TermLabel label) { return label; } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/label/RuleSpecificTask.java b/key.core/src/main/java/de/uka/ilkd/key/rule/label/RuleSpecificTask.java index cc61fb2e985..4193a27460e 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/label/RuleSpecificTask.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/label/RuleSpecificTask.java @@ -10,7 +10,6 @@ * Instances of this class provides functionality only if a supported rule is active. * * @author Martin Hentschel - * @see ChildTermLabelPolicy * @see TermLabelUpdate * @see TermLabelRefactoring */ diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/label/StayOnOperatorTermLabelPolicy.java b/key.core/src/main/java/de/uka/ilkd/key/rule/label/StayOnOperatorTermLabelPolicy.java index d6d0d26fe82..96230850fdd 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/label/StayOnOperatorTermLabelPolicy.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/label/StayOnOperatorTermLabelPolicy.java @@ -3,16 +3,12 @@ * SPDX-License-Identifier: GPL-2.0-only */ package de.uka.ilkd.key.rule.label; -import de.uka.ilkd.key.java.Services; import de.uka.ilkd.key.logic.JTerm; import de.uka.ilkd.key.logic.label.TermLabel; -import de.uka.ilkd.key.logic.label.TermLabelState; +import de.uka.ilkd.key.logic.label.TermLabelContext; import de.uka.ilkd.key.logic.op.JavaDLOperatorUtil; -import de.uka.ilkd.key.proof.Goal; import org.key_project.logic.op.Operator; -import org.key_project.prover.rules.Rule; -import org.key_project.prover.sequent.PosInOccurrence; /** * This {@link TermLabelPolicy} maintains a {@link TermLabel} as long the new {@link JTerm} has the @@ -25,12 +21,10 @@ public class StayOnOperatorTermLabelPolicy implements TermLabelPolicy { * {@inheritDoc} */ @Override - public TermLabel keepLabel(TermLabelState state, Services services, - PosInOccurrence applicationPosInOccurrence, JTerm applicationTerm, Rule rule, Goal goal, - Object hint, JTerm tacletTerm, - JTerm newTerm, TermLabel label) { - return applicationTerm != null - && JavaDLOperatorUtil.opEquals(newTerm.op(), applicationTerm.op()) + public TermLabel keepLabel(TermLabelContext context, JTerm sourceTerm, JTerm newTerm, + TermLabel label) { + return sourceTerm != null + && JavaDLOperatorUtil.opEquals(newTerm.op(), sourceTerm.op()) ? label : null; } diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/label/TermLabelPolicy.java b/key.core/src/main/java/de/uka/ilkd/key/rule/label/TermLabelPolicy.java index 8117fd24dbc..4e93495124e 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/label/TermLabelPolicy.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/label/TermLabelPolicy.java @@ -3,17 +3,10 @@ * SPDX-License-Identifier: GPL-2.0-only */ package de.uka.ilkd.key.rule.label; -import de.uka.ilkd.key.java.Services; import de.uka.ilkd.key.logic.JTerm; import de.uka.ilkd.key.logic.label.TermLabel; +import de.uka.ilkd.key.logic.label.TermLabelContext; import de.uka.ilkd.key.logic.label.TermLabelManager; -import de.uka.ilkd.key.logic.label.TermLabelState; -import de.uka.ilkd.key.proof.Goal; -import de.uka.ilkd.key.proof.Proof; - -import org.key_project.prover.rules.Rule; -import org.key_project.prover.sequent.PosInOccurrence; -import org.key_project.prover.sequent.Sequent; /** @@ -21,11 +14,18 @@ * A {@link TermLabelPolicy} is used by * {@link TermLabelManager#instantiateLabels} * to decide for each {@link TermLabel} of an old {@link JTerm} if it should be re-added to the new - * {@link JTerm} or not. + * {@link JTerm} or not. Policies are registered per label {@link org.key_project.logic.Name} and + * are only asked for labels of that name. + *

    + *

    + * Execution order (part of the contract): within one term creation, policies run + * before all {@link TermLabelUpdate}s — first the application-term policies, then the + * modality-term policies. The label set produced by the policies is what the updates subsequently + * see and may transform. Do not design a label whose update must run before a policy. *

    *

    - * For more information about {@link TermLabel}s and how they are maintained during prove read the - * documentation of interface {@link TermLabel}. + * For more information about {@link TermLabel}s and how they are maintained during proof + * construction read the documentation of interface {@link TermLabel}. *

    * * @author Martin Hentschel @@ -35,31 +35,16 @@ public interface TermLabelPolicy { /** * Decides to keep (add to term which will be created) or to drop (do not add label to new term) - * the given {@link TermLabel} provided by the application {@link JTerm}. + * the given {@link TermLabel} provided by the source {@link JTerm}. * - * @param state The {@link TermLabelState} of the current rule application. - * @param services The {@link Services} used by the {@link Proof} on which a {@link Rule} is - * applied right now. - * @param applicationPosInOccurrence The {@link PosInOccurrence} in the previous {@link Sequent} - * which defines the {@link JTerm} that is rewritten. - * @param applicationTerm The {@link JTerm} defined by the {@link PosInOccurrence} in the - * previous {@link Sequent}. - * @param rule The {@link Rule} which is applied. - * @param goal The optional {@link Goal} on which the {@link JTerm} to create will be used. - * @param hint An optional hint passed from the active rule to describe the term which should be - * created. - * @param tacletTerm The optional {@link JTerm} in the taclet which is responsible to - * instantiate - * the new {@link JTerm} for the new proof node or {@code null} in case of built in - * rules. + * @param context the {@link TermLabelContext} of the current rule application + * @param sourceTerm the {@link JTerm} whose labels are under consideration: the application + * term for application-term policies, the modality term for modality-term policies * @param newTerm the template for the new {@link JTerm} to create * @param label The {@link TermLabel} to decide if it should be kept or dropped. * @return The {@link TermLabel} to keep which might be a different one (e.g. with changed * parameters) or {@code null} if the {@link TermLabel} should be dropped. */ - TermLabel keepLabel(TermLabelState state, Services services, - PosInOccurrence applicationPosInOccurrence, - JTerm applicationTerm, Rule rule, Goal goal, - Object hint, JTerm tacletTerm, - JTerm newTerm, TermLabel label); + TermLabel keepLabel(TermLabelContext context, JTerm sourceTerm, JTerm newTerm, + TermLabel label); } diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/label/TermLabelRefactoring.java b/key.core/src/main/java/de/uka/ilkd/key/rule/label/TermLabelRefactoring.java index e530532abee..08a73aedf91 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/label/TermLabelRefactoring.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/label/TermLabelRefactoring.java @@ -3,13 +3,12 @@ * SPDX-License-Identifier: GPL-2.0-only */ package de.uka.ilkd.key.rule.label; -import de.uka.ilkd.key.java.Services; import de.uka.ilkd.key.logic.JTerm; import de.uka.ilkd.key.logic.TermBuilder; import de.uka.ilkd.key.logic.label.LabelCollection; import de.uka.ilkd.key.logic.label.TermLabel; +import de.uka.ilkd.key.logic.label.TermLabelContext; import de.uka.ilkd.key.logic.label.TermLabelManager; -import de.uka.ilkd.key.logic.label.TermLabelState; import de.uka.ilkd.key.proof.Goal; import de.uka.ilkd.key.proof.Proof; import de.uka.ilkd.key.proof.init.AbstractOperationPO; @@ -21,19 +20,16 @@ import de.uka.ilkd.key.rule.merge.CloseAfterMerge; import org.key_project.prover.rules.Rule; -import org.key_project.prover.sequent.PosInOccurrence; -import org.key_project.prover.sequent.Sequent; import org.key_project.prover.sequent.SequentFormula; /** *

    - * A {@link TermLabelRefactoring} is used by - * {@link TermLabelManager#refactorGoal(TermLabelState, Services, PosInOccurrence, Rule, Goal, Object, JTerm)} - * to refactor the labels of each visited {@link JTerm}. + * A {@link TermLabelRefactoring} is used by {@link TermLabelManager#refactorGoal} to refactor the + * labels of each visited {@link JTerm}. *

    *

    - * For more information about {@link TermLabel}s and how they are maintained during prove read the - * documentation of interface {@link TermLabel}. + * For more information about {@link TermLabel}s and how they are maintained during proof + * construction read the documentation of interface {@link TermLabel}. *

    * * @author Martin Hentschel @@ -94,47 +90,19 @@ static boolean shouldRefactorOnBuiltInRule(Rule rule, Goal goal, Object hint) { /** * Defines if a refactoring is required and if so in which {@link RefactoringScope}. * - * @param state The {@link TermLabelState} of the current rule application. - * @param services The {@link Services} used by the {@link Proof} on which a {@link Rule} is - * applied right now. - * @param applicationPosInOccurrence The {@link PosInOccurrence} in the previous {@link Sequent} - * which defines the {@link JTerm} that is rewritten. - * @param applicationTerm The {@link JTerm} defined by the {@link PosInOccurrence} in the - * previous {@link Sequent}. - * @param rule The {@link Rule} which is applied. - * @param goal The optional {@link Goal} on which the {@link JTerm} to create will be used. - * @param hint An optional hint passed from the active rule to describe the term which should be - * created. - * @param tacletTerm The optional taclet {@link JTerm}. + * @param context the {@link TermLabelContext} of the current rule application * @return The required {@link RefactoringScope}. */ - RefactoringScope defineRefactoringScope(TermLabelState state, Services services, - PosInOccurrence applicationPosInOccurrence, - JTerm applicationTerm, Rule rule, Goal goal, - Object hint, JTerm tacletTerm); + RefactoringScope defineRefactoringScope(TermLabelContext context); /** * This method is used to refactor the labels of the given {@link JTerm}. * - * @param state The {@link TermLabelState} of the current rule application. - * @param services The {@link Services} used by the {@link Proof} on which a {@link Rule} is - * applied right now. - * @param applicationPosInOccurrence The {@link PosInOccurrence} in the previous {@link Sequent} - * which defines the {@link JTerm} that is rewritten. - * @param applicationTerm The {@link JTerm} defined by the {@link PosInOccurrence} in the - * previous {@link Sequent}. - * @param rule The {@link Rule} which is applied. - * @param goal The optional {@link Goal} on which the {@link JTerm} to create will be used. - * @param hint An optional hint passed from the active rule to describe the term which should be - * created. - * @param tacletTerm The optional taclet {@link JTerm}. + * @param context the {@link TermLabelContext} of the current rule application * @param term The {@link JTerm} which is now refactored. * @param labels The new labels the {@link JTerm} will have after the refactoring. */ - void refactorLabels(TermLabelState state, Services services, - PosInOccurrence applicationPosInOccurrence, - JTerm applicationTerm, Rule rule, Goal goal, - Object hint, JTerm tacletTerm, JTerm term, LabelCollection labels); + void refactorLabels(TermLabelContext context, JTerm term, LabelCollection labels); /** * Possible refactoring scopes. @@ -153,11 +121,6 @@ enum RefactoringScope { */ APPLICATION_BELOW_UPDATES, - /** - * Refactor direct children of the application term. - */ - APPLICATION_DIRECT_CHILDREN, - /** * Refactor children and grandchildren of the application term. */ diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/label/TermLabelUpdate.java b/key.core/src/main/java/de/uka/ilkd/key/rule/label/TermLabelUpdate.java index 1dda30f1522..39812f1ea8e 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/label/TermLabelUpdate.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/label/TermLabelUpdate.java @@ -5,29 +5,26 @@ import java.util.Set; -import de.uka.ilkd.key.java.Services; import de.uka.ilkd.key.logic.JTerm; import de.uka.ilkd.key.logic.label.TermLabel; +import de.uka.ilkd.key.logic.label.TermLabelContext; import de.uka.ilkd.key.logic.label.TermLabelManager; -import de.uka.ilkd.key.logic.label.TermLabelState; -import de.uka.ilkd.key.proof.Goal; -import de.uka.ilkd.key.proof.Proof; - -import org.key_project.prover.rules.Rule; -import org.key_project.prover.rules.RuleApp; -import org.key_project.prover.sequent.PosInOccurrence; -import org.key_project.prover.sequent.Sequent; /** *

    - * A {@link TermLabelUpdate} is used by - * {@link TermLabelManager#instantiateLabels(TermLabelState, Services, PosInOccurrence, JTerm, Rule, RuleApp, Goal, Object, JTerm, JTerm)} - * to add or remove maintained {@link TermLabel}s which will be added to the new {@link JTerm}. + * A {@link TermLabelUpdate} is used by {@link TermLabelManager#instantiateLabels} to add or + * remove maintained {@link TermLabel}s which will be added to the new {@link JTerm}. + *

    + *

    + * Execution order (part of the contract): updates run after all + * {@link TermLabelPolicy} instances; the label set passed to {@code updateLabels} already + * contains the taclet-provided labels and the labels kept by the policies. Rule-specific updates + * (see {@link #getSupportedRuleNames()}) run before rule-independent ones. *

    *

    - * For more information about {@link TermLabel}s and how they are maintained during prove read the - * documentation of interface {@link TermLabel}. + * For more information about {@link TermLabel}s and how they are maintained during proof + * construction read the documentation of interface {@link TermLabel}. *

    * * @author Martin Hentschel @@ -36,34 +33,12 @@ */ public interface TermLabelUpdate extends RuleSpecificTask { /** - * This method can freely add, remove or sort the given {@link TermLabel} which will be added to - * the new {@link JTerm}. + * This method can freely add, remove or sort the given {@link TermLabel}s which will be added + * to the new {@link JTerm}. * - * @param state The {@link TermLabelState} of the current rule application. return {@code true} - * keep {@link TermLabel} and add it to the new {@link JTerm}. {@code false} drop - * {@link TermLabel} and do not need it to the new {@link JTerm}. - * @param services The {@link Services} used by the {@link Proof} on which a {@link Rule} is - * applied right now. - * @param applicationPosInOccurrence The {@link PosInOccurrence} in the previous {@link Sequent} - * which defines the {@link JTerm} that is rewritten. - * @param applicationTerm The {@link JTerm} defined by the {@link PosInOccurrence} in the - * previous {@link Sequent}. - * @param modalityTerm The optional modality {@link JTerm}. - * @param rule The {@link Rule} which is applied. - * @param ruleApp The {@link RuleApp} which is currently performed. - * @param hint An optional hint passed from the active rule to describe the term which should be - * created. - * @param tacletTerm The optional {@link JTerm} in the taclet which is responsible to - * instantiate - * the new {@link JTerm} for the new proof node or {@code null} in case of built in - * rules. + * @param context the {@link TermLabelContext} of the current rule application * @param newTerm the template for the new {@link JTerm} to create * @param labels The {@link Set} of {@link TermLabel}s to modify. */ - void updateLabels(TermLabelState state, Services services, - PosInOccurrence applicationPosInOccurrence, - JTerm applicationTerm, JTerm modalityTerm, - Rule rule, RuleApp ruleApp, Object hint, JTerm tacletTerm, - JTerm newTerm, - Set labels); + void updateLabels(TermLabelContext context, JTerm newTerm, Set labels); } diff --git a/key.core/src/main/java/de/uka/ilkd/key/scripts/HideCommand.java b/key.core/src/main/java/de/uka/ilkd/key/scripts/HideCommand.java index a4aa880fb0f..b1e88c367dd 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/scripts/HideCommand.java +++ b/key.core/src/main/java/de/uka/ilkd/key/scripts/HideCommand.java @@ -23,7 +23,6 @@ import org.checkerframework.checker.nullness.qual.MonotonicNonNull; -import static de.uka.ilkd.key.logic.equality.TermLabelsProperty.TERM_LABELS_PROPERTY; /** * Proof script command to hide formulas from the sequent. @@ -88,7 +87,7 @@ private SequentFormula find( for (SequentFormula s : semiseq) { Term term = s.formula(); Term formula = sf.formula(); - if ((TERM_LABELS_PROPERTY).equalsModThisProperty(term, formula)) { + if (term.equals(formula)) { return s; } } 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 1b96b9a1b12..a3989ca2545 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 @@ -34,7 +34,6 @@ import org.slf4j.Logger; import org.slf4j.LoggerFactory; -import static de.uka.ilkd.key.logic.equality.TermLabelsProperty.TERM_LABELS_PROPERTY; import static de.uka.ilkd.key.logic.label.OriginTermLabel.Origin; /** @@ -511,9 +510,9 @@ private static void combineModifiable(FunctionalOperationContractImpl t, // check if the other modifiable is the same as the one in the uniform store. // To obtain meaningful results, check for equality ignoring all term labels! + // (plain term equality now ignores term labels) if (uniformModifiable.containsKey(h)) { - if (!TERM_LABELS_PROPERTY.equalsModThisProperty(uniformModifiable.get(h), - modifiable2)) { + if (!uniformModifiable.get(h).equals(modifiable2)) { uniformModifiable.remove(h); } else { // merge term labels (in particular origin labels) of both modifiable diff --git a/key.core/src/test/java/de/uka/ilkd/key/logic/LabeledTermImplTest.java b/key.core/src/test/java/de/uka/ilkd/key/logic/LabeledTermImplTest.java index b63dd7f6108..d6932e28cba 100644 --- a/key.core/src/test/java/de/uka/ilkd/key/logic/LabeledTermImplTest.java +++ b/key.core/src/test/java/de/uka/ilkd/key/logic/LabeledTermImplTest.java @@ -15,7 +15,6 @@ import org.junit.jupiter.api.BeforeEach; import org.junit.jupiter.api.Test; -import static org.junit.jupiter.api.Assertions.assertNotEquals; public class LabeledTermImplTest { @@ -40,10 +39,69 @@ public void testEqualsLabelOnTop() { JTerm labeledTerm = tf.createTerm(Junctor.AND, tf.createTerm(Junctor.TRUE), tf.createTerm(Junctor.FALSE), labels); - assertNotEquals(labeledTerm, unlabeledTerm, - "Labeled and unlabeled terms must not be equal"); - assertNotEquals(unlabeledTerm, labeledTerm, - "Labeled and unlabeled terms must not be equal"); + // equals ignores term labels ... + Assertions.assertEquals(labeledTerm, unlabeledTerm, + "equals must ignore term labels"); + Assertions.assertEquals(unlabeledTerm, labeledTerm, + "equals must ignore term labels"); + Assertions.assertEquals(labeledTerm.hashCode(), unlabeledTerm.hashCode(), + "hashCode must ignore term labels"); + // ... while equalsIncludingLabels does not + Assertions.assertFalse(labeledTerm.equalsIncludingLabels(unlabeledTerm), + "equalsIncludingLabels must distinguish labeled and unlabeled terms"); + Assertions.assertFalse(unlabeledTerm.equalsIncludingLabels(labeledTerm), + "equalsIncludingLabels must distinguish labeled and unlabeled terms"); + Assertions.assertTrue(labeledTerm.equalsIncludingLabels(labeledTerm)); + } + + /** + * Labels on subterms must be distinguished by + * {@link JTerm#equalsIncludingLabels(Object)}, too. + */ + @Test + public void testEqualsLabelOnSubterm() { + JTerm labeledSub = tf.createTerm(Junctor.TRUE, + new ImmutableArray<>(), null, + new ImmutableArray<>(ParameterlessTermLabel.ANON_HEAP_LABEL)); + JTerm labeledBelow = + tf.createTerm(Junctor.AND, labeledSub, tf.createTerm(Junctor.FALSE)); + JTerm unlabeled = + tf.createTerm(Junctor.AND, tf.createTerm(Junctor.TRUE), tf.createTerm(Junctor.FALSE)); + + Assertions.assertTrue(labeledBelow.containsLabelsRecursive()); + Assertions.assertFalse(unlabeled.containsLabelsRecursive()); + Assertions.assertEquals(labeledBelow, unlabeled); + Assertions.assertFalse(labeledBelow.equalsIncludingLabels(unlabeled)); + Assertions.assertFalse(unlabeled.equalsIncludingLabels(labeledBelow)); + } + + /** + * A caching {@link TermFactory} must intern labeled terms label-sensitively: two + * independently built, label-identical terms are the same object ({@code ==}), while a label + * variant and the unlabeled term are kept distinct. This guards the {@code ==} fast paths and + * memory sharing for the (very common) labeled terms. + */ + @Test + public void testCachedFactoryInternsLabeledTerms() { + TermFactory ctf = + new TermFactory(new java.util.HashMap<>()); + ImmutableArray lbl = + new ImmutableArray<>(ParameterlessTermLabel.ANON_HEAP_LABEL); + + JTerm labeled1 = ctf.createTerm(Junctor.AND, + new ImmutableArray<>(ctf.createTerm(Junctor.TRUE), ctf.createTerm(Junctor.FALSE)), + null, lbl); + JTerm labeled2 = ctf.createTerm(Junctor.AND, + new ImmutableArray<>(ctf.createTerm(Junctor.TRUE), ctf.createTerm(Junctor.FALSE)), + null, lbl); + JTerm unlabeled = ctf.createTerm(Junctor.AND, + new ImmutableArray<>(ctf.createTerm(Junctor.TRUE), ctf.createTerm(Junctor.FALSE)), + null, null); + + Assertions.assertSame(labeled1, labeled2, "identical labeled terms must be interned"); + Assertions.assertNotSame(labeled1, unlabeled, + "labeled and unlabeled variants must not be interned together"); + Assertions.assertEquals(labeled1.labeledHashCode(), labeled2.labeledHashCode()); } /** diff --git a/key.core/src/test/java/de/uka/ilkd/key/logic/TestTermLabelManager.java b/key.core/src/test/java/de/uka/ilkd/key/logic/TestTermLabelManager.java index 37648085ca4..cbb2fe39d6f 100644 --- a/key.core/src/test/java/de/uka/ilkd/key/logic/TestTermLabelManager.java +++ b/key.core/src/test/java/de/uka/ilkd/key/logic/TestTermLabelManager.java @@ -10,6 +10,7 @@ import de.uka.ilkd.key.java.ast.expression.literal.IntLiteral; import de.uka.ilkd.key.ldt.IntegerLDT; import de.uka.ilkd.key.logic.label.*; +import de.uka.ilkd.key.logic.label.TermLabelContext; import de.uka.ilkd.key.logic.label.TermLabelManager.TermLabelConfiguration; import de.uka.ilkd.key.logic.op.LocationVariable; import de.uka.ilkd.key.proof.*; @@ -18,7 +19,6 @@ import de.uka.ilkd.key.proof.init.JavaProfile; import de.uka.ilkd.key.proof.init.Profile; import de.uka.ilkd.key.proof.io.ProblemLoaderException; -import de.uka.ilkd.key.rule.label.ChildTermLabelPolicy; import de.uka.ilkd.key.rule.label.TermLabelPolicy; import de.uka.ilkd.key.rule.label.TermLabelRefactoring; import de.uka.ilkd.key.rule.label.TermLabelRefactoring.RefactoringScope; @@ -29,7 +29,6 @@ import org.key_project.logic.PosInTerm; import org.key_project.prover.rules.Rule; import org.key_project.prover.rules.RuleAbortException; -import org.key_project.prover.rules.RuleApp; import org.key_project.prover.rules.RuleExecutor; import org.key_project.prover.sequent.PosInOccurrence; import org.key_project.prover.sequent.Sequent; @@ -65,19 +64,6 @@ public void testrefactorGoal_childrenAndGrandchildren_ruleSpecific() } - @Test - public void testrefactorGoal_directChildren_allRules() throws ProblemLoaderException { - doRefactoringTestLogging(true, true, RefactoringScope.APPLICATION_DIRECT_CHILDREN); - } - - /** - * - */ - @Test - public void testrefactorGoal_directChildren_ruleSpecific() throws ProblemLoaderException { - doRefactoringTestLogging(true, false, RefactoringScope.APPLICATION_DIRECT_CHILDREN, "rule"); - } - /** * */ @@ -114,7 +100,7 @@ protected void doRefactoringTestLogging(boolean ruleChanged, boolean notSupporte RefactoringScope scope, String... supportedRules) throws ProblemLoaderException { LoggingTermLabelRefactoring refactoring = new LoggingTermLabelRefactoring(scope, supportedRules); - InitConfig initConfig = createTestServices(null, null, null, null, null, refactoring); + InitConfig initConfig = createTestServices(null, null, null, refactoring); Services services = initConfig.getServices(); TermBuilder TB = services.getTermBuilder(); // Create sequent @@ -192,14 +178,6 @@ protected void compareTerms(JTerm expected, JTerm current, boolean changed, } else { assertEquals(expectedName, current.getLabels().get(i).name().toString()); } - } else if (RefactoringScope.APPLICATION_DIRECT_CHILDREN.equals(scope)) { - String expectedName = expected.getLabels().get(i).name().toString(); - if ("ONE".equals(expectedName) || "ADD".equals(expectedName)) { - assertEquals(expectedName + "-CHANGED", - current.getLabels().get(i).name().toString()); - } else { - assertEquals(expectedName, current.getLabels().get(i).name().toString()); - } } else { fail("Unsupported scope \"" + scope + "\"."); } @@ -217,7 +195,7 @@ public void testInstantiateLabels_updates_allRules() { LoggingTermLabelUpdate update = new LoggingTermLabelUpdate(new ParameterlessTermLabel(new Name("UPDATED"))); Services services = Assertions.assertDoesNotThrow( - () -> createTestServices(null, null, null, null, update, null).getServices()); + () -> createTestServices(null, null, update, null).getServices()); PosInOccurrence pos = createTestPosInOccurrence(services); Rule rule = new DummyRule("rule"); JTerm taclet = services.getTermBuilder().tt(); @@ -244,7 +222,7 @@ public void testInstantiateLabels_updates_ruleSpecific() { LoggingTermLabelUpdate update = new LoggingTermLabelUpdate(new ParameterlessTermLabel(new Name("UPDATED")), "rule"); Services services = Assertions.assertDoesNotThrow( - () -> createTestServices(null, null, null, null, update, null).getServices()); + () -> createTestServices(null, null, update, null).getServices()); PosInOccurrence pos = createTestPosInOccurrence(services); Rule rule = new DummyRule("rule"); JTerm taclet = services.getTermBuilder().tt(); @@ -262,161 +240,6 @@ public void testInstantiateLabels_updates_ruleSpecific() { assertEquals(0, labels.size()); } - /** - * - */ - @Test - public void testInstantiateLabels_childAndGrandchildPolicies_allRules() { - LoggingChildTermLabelPolicy policy = new LoggingChildTermLabelPolicy(); - Services services = Assertions.assertDoesNotThrow( - () -> createTestServices(null, null, null, policy, null, null).getServices()); - PosInOccurrence pos = createTestPosInOccurrence(services); - Rule rule = new DummyRule("rule"); - JTerm taclet = services.getTermBuilder().tt(); - // Create labels - ImmutableArray labels = TermLabelManager.instantiateLabels(new TermLabelState(), - services, pos, rule, null, null, null, taclet, null); - assertNotNull(labels); - assertEquals(4, labels.size()); - assertEquals("ONE", labels.get(0).name().toString()); - assertEquals("ADD", labels.get(1).name().toString()); - assertEquals("TWO", labels.get(2).name().toString()); - assertEquals("THREE", labels.get(3).name().toString()); - // Test log - assertEquals(4, policy.getLog().size()); - assertEquals("ONE", policy.getLog().get(0).name().toString()); - assertEquals("ADD", policy.getLog().get(1).name().toString()); - assertEquals("TWO", policy.getLog().get(2).name().toString()); - assertEquals("THREE", policy.getLog().get(3).name().toString()); - // Test other not supported rule - Rule otherRule = new DummyRule("notSupportedRule"); - labels = TermLabelManager.instantiateLabels(new TermLabelState(), services, pos, otherRule, - null, null, null, taclet, null); - assertNotNull(labels); - assertEquals(4, labels.size()); - assertEquals("ONE", labels.get(0).name().toString()); - assertEquals("ADD", labels.get(1).name().toString()); - assertEquals("TWO", labels.get(2).name().toString()); - assertEquals("THREE", labels.get(3).name().toString()); - // Test log - assertEquals(8, policy.getLog().size()); - assertEquals("ONE", policy.getLog().get(0).name().toString()); - assertEquals("ADD", policy.getLog().get(1).name().toString()); - assertEquals("TWO", policy.getLog().get(2).name().toString()); - assertEquals("THREE", policy.getLog().get(3).name().toString()); - assertEquals("ONE", policy.getLog().get(4).name().toString()); - assertEquals("ADD", policy.getLog().get(5).name().toString()); - assertEquals("TWO", policy.getLog().get(6).name().toString()); - assertEquals("THREE", policy.getLog().get(7).name().toString()); - } - - /** - * - */ - @Test - public void testInstantiateLabels_childAndGrandchildPolicies_ruleSpecific() { - LoggingChildTermLabelPolicy policy = new LoggingChildTermLabelPolicy("rule"); - Services services = Assertions.assertDoesNotThrow( - () -> createTestServices(null, null, null, policy, null, null).getServices()); - PosInOccurrence pos = createTestPosInOccurrence(services); - Rule rule = new DummyRule("rule"); - JTerm taclet = services.getTermBuilder().tt(); - // Create labels - ImmutableArray labels = TermLabelManager.instantiateLabels(new TermLabelState(), - services, pos, rule, null, null, null, taclet, null); - assertNotNull(labels); - assertEquals(4, labels.size()); - assertEquals("ONE", labels.get(0).name().toString()); - assertEquals("ADD", labels.get(1).name().toString()); - assertEquals("TWO", labels.get(2).name().toString()); - assertEquals("THREE", labels.get(3).name().toString()); - // Test log - assertEquals(4, policy.getLog().size()); - assertEquals("ONE", policy.getLog().get(0).name().toString()); - assertEquals("ADD", policy.getLog().get(1).name().toString()); - assertEquals("TWO", policy.getLog().get(2).name().toString()); - assertEquals("THREE", policy.getLog().get(3).name().toString()); - // Test other not supported rule - Rule otherRule = new DummyRule("notSupportedRule"); - labels = TermLabelManager.instantiateLabels(new TermLabelState(), services, pos, otherRule, - null, null, null, taclet, null); - assertNotNull(labels); - assertEquals(0, labels.size()); - // Test log - assertEquals(4, policy.getLog().size()); - } - - /** - * - * @throws ProblemLoaderException - * Occurred Exception - */ - @Test - public void testInstantiateLabels_directChildPolicies_allRules() throws ProblemLoaderException { - LoggingChildTermLabelPolicy policy = new LoggingChildTermLabelPolicy(); - Services services = createTestServices(null, null, policy, null, null, null).getServices(); - PosInOccurrence pos = createTestPosInOccurrence(services); - Rule rule = new DummyRule("rule"); - JTerm taclet = services.getTermBuilder().tt(); - // Create labels - ImmutableArray labels = TermLabelManager.instantiateLabels(new TermLabelState(), - services, pos, rule, null, null, null, taclet, null); - assertNotNull(labels); - assertEquals(2, labels.size()); - assertEquals("ONE", labels.get(0).name().toString()); - assertEquals("ADD", labels.get(1).name().toString()); - // Test log - assertEquals(2, policy.getLog().size()); - assertEquals("ONE", policy.getLog().get(0).name().toString()); - assertEquals("ADD", policy.getLog().get(1).name().toString()); - // Test other not supported rule - Rule otherRule = new DummyRule("notSupportedRule"); - labels = TermLabelManager.instantiateLabels(new TermLabelState(), services, pos, otherRule, - null, null, null, taclet, null); - assertNotNull(labels); - assertEquals(2, labels.size()); - assertEquals("ONE", labels.get(0).name().toString()); - assertEquals("ADD", labels.get(1).name().toString()); - // Test log - assertEquals(4, policy.getLog().size()); - assertEquals("ONE", policy.getLog().get(0).name().toString()); - assertEquals("ADD", policy.getLog().get(1).name().toString()); - assertEquals("ONE", policy.getLog().get(2).name().toString()); - assertEquals("ADD", policy.getLog().get(3).name().toString()); - } - - /** - * - */ - @Test - public void testInstantiateLabels_directChildPolicies_ruleSpecific() { - LoggingChildTermLabelPolicy policy = new LoggingChildTermLabelPolicy("rule"); - Services services = Assertions.assertDoesNotThrow( - () -> createTestServices(null, null, policy, null, null, null).getServices()); - PosInOccurrence pos = createTestPosInOccurrence(services); - Rule rule = new DummyRule("rule"); - JTerm taclet = services.getTermBuilder().tt(); - // Create labels - ImmutableArray labels = TermLabelManager.instantiateLabels(new TermLabelState(), - services, pos, rule, null, null, null, taclet, null); - assertNotNull(labels); - assertEquals(2, labels.size()); - assertEquals("ONE", labels.get(0).name().toString()); - assertEquals("ADD", labels.get(1).name().toString()); - // Test log - assertEquals(2, policy.getLog().size()); - assertEquals("ONE", policy.getLog().get(0).name().toString()); - assertEquals("ADD", policy.getLog().get(1).name().toString()); - // Test other not supported rule - Rule otherRule = new DummyRule("notSupportedRule"); - labels = TermLabelManager.instantiateLabels(new TermLabelState(), services, pos, otherRule, - null, null, null, taclet, null); - assertNotNull(labels); - assertEquals(0, labels.size()); - // Test log - assertEquals(2, policy.getLog().size()); - } - /** * */ @@ -424,7 +247,7 @@ public void testInstantiateLabels_directChildPolicies_ruleSpecific() { public void testInstantiateLabels_modalityTermPolicies() { LoggingTermLabelPolicy policy = new LoggingTermLabelPolicy(); Services services = Assertions.assertDoesNotThrow( - () -> createTestServices(null, policy, null, null, null, null).getServices()); + () -> createTestServices(null, policy, null, null).getServices()); TermBuilder TB = services.getTermBuilder(); JTerm modality = TB.label( TB.box(JavaBlock.EMPTY_JAVABLOCK, @@ -457,7 +280,7 @@ public void testInstantiateLabels_modalityTermPolicies() { public void testInstantiateLabels_applicationTermPolicies() { LoggingTermLabelPolicy policy = new LoggingTermLabelPolicy(); Services services = Assertions.assertDoesNotThrow( - () -> createTestServices(policy, null, null, null, null, null).getServices()); + () -> createTestServices(policy, null, null, null).getServices()); PosInOccurrence pos = createTestPosInOccurrence(services); JTerm taclet = services.getTermBuilder().tt(); Rule rule = new DummyRule("rule"); @@ -478,7 +301,7 @@ public void testInstantiateLabels_applicationTermPolicies() { @Test public void testInstantiateLabels_taclet() { Services services = Assertions.assertDoesNotThrow( - () -> createTestServices(null, null, null, null, null, null).getServices()); + () -> createTestServices(null, null, null, null).getServices()); PosInOccurrence pos = createTestPosInOccurrence(services); Rule rule = new DummyRule("rule"); JTerm taclet = services.getTermBuilder().label(services.getTermBuilder().tt(), @@ -526,7 +349,7 @@ protected JTerm createTestTerm(Services services) { @Test public void testParseLabel() throws TermLabelException { Services services = Assertions.assertDoesNotThrow( - () -> createTestServices(null, null, null, null, null, null).getServices()); + () -> createTestServices(null, null, null, null).getServices()); TermLabelManager manager = TermLabelManager.getTermLabelManager(services); // Test null parameter TermLabel label = manager.parseLabel("ONE", null, services); @@ -564,7 +387,7 @@ public void testGetSupportedTermLabelNames() { assertTrue(names.isEmpty()); // Test services Services services = Assertions.assertDoesNotThrow( - () -> createTestServices(null, null, null, null, null, null).getServices()); + () -> createTestServices(null, null, null, null).getServices()); names = TermLabelManager.getSupportedTermLabelNames(services); assertNotNull(names); assertEquals(5, names.size()); @@ -590,8 +413,7 @@ public void testGetTermLabelManager() { } protected InitConfig createTestServices(final TermLabelPolicy applicationTermPolicy, - final TermLabelPolicy modalityTermPolicy, final ChildTermLabelPolicy directChildPolicy, - final ChildTermLabelPolicy childAndGrandchildPolicy, final TermLabelUpdate update, + final TermLabelPolicy modalityTermPolicy, final TermLabelUpdate update, final TermLabelRefactoring refactoring) throws ProblemLoaderException { if (CONFIG == null) { KeYEnvironment env = null; @@ -620,18 +442,6 @@ protected ImmutableList computeTermLabelConfiguration() if (modalityTermPolicy != null) { modalityTermPolicies = modalityTermPolicies.prepend(modalityTermPolicy); } - ImmutableList directChildTermLabelPolicies = - ImmutableList.nil(); - if (directChildPolicy != null) { - directChildTermLabelPolicies = - directChildTermLabelPolicies.prepend(directChildPolicy); - } - ImmutableList childAndGrandchildTermLabelPolicies = - ImmutableList.nil(); - if (childAndGrandchildPolicy != null) { - childAndGrandchildTermLabelPolicies = - childAndGrandchildTermLabelPolicies.prepend(childAndGrandchildPolicy); - } ImmutableList termLabelUpdates = ImmutableList.nil(); if (update != null) { termLabelUpdates = termLabelUpdates.prepend(update); @@ -645,28 +455,23 @@ protected ImmutableList computeTermLabelConfiguration() ImmutableList result = ImmutableList.nil(); result = result.prepend(new TermLabelConfiguration(new Name("ONE"), new LoggingFactory(new Name("ONE")), applicationTermPolicies, - modalityTermPolicies, directChildTermLabelPolicies, - childAndGrandchildTermLabelPolicies, termLabelUpdates, + modalityTermPolicies, termLabelUpdates, termLabelRefactorings, null)); result = result.prepend(new TermLabelConfiguration(new Name("TWO"), new LoggingFactory(new Name("TWO")), applicationTermPolicies, - modalityTermPolicies, directChildTermLabelPolicies, - childAndGrandchildTermLabelPolicies, termLabelUpdates, + modalityTermPolicies, termLabelUpdates, termLabelRefactorings, null)); result = result.prepend(new TermLabelConfiguration(new Name("THREE"), new LoggingFactory(new Name("THREE")), applicationTermPolicies, - modalityTermPolicies, directChildTermLabelPolicies, - childAndGrandchildTermLabelPolicies, termLabelUpdates, + modalityTermPolicies, termLabelUpdates, termLabelRefactorings, null)); result = result.prepend(new TermLabelConfiguration(new Name("ADD"), new LoggingFactory(new Name("ADD")), applicationTermPolicies, - modalityTermPolicies, directChildTermLabelPolicies, - childAndGrandchildTermLabelPolicies, termLabelUpdates, + modalityTermPolicies, termLabelUpdates, termLabelRefactorings, null)); result = result.prepend(new TermLabelConfiguration(new Name("APPLICATION"), new LoggingFactory(new Name("APPLICATION")), applicationTermPolicies, - modalityTermPolicies, directChildTermLabelPolicies, - childAndGrandchildTermLabelPolicies, termLabelUpdates, + modalityTermPolicies, termLabelUpdates, termLabelRefactorings, null)); return result; } @@ -692,18 +497,12 @@ public ImmutableList getSupportedRuleNames() { } @Override - public RefactoringScope defineRefactoringScope(TermLabelState state, Services services, - PosInOccurrence applicationPosInOccurrence, - JTerm applicationTerm, Rule rule, - Goal goal, Object hint, JTerm tacletTerm) { + public RefactoringScope defineRefactoringScope(TermLabelContext context) { return scope; } @Override - public void refactorLabels(TermLabelState state, Services services, - PosInOccurrence applicationPosInOccurrence, - JTerm applicationTerm, Rule rule, - Goal goal, Object hint, JTerm tacletTerm, JTerm term, LabelCollection labels) { + public void refactorLabels(TermLabelContext context, JTerm term, LabelCollection labels) { List changedLabels = new LinkedList<>(); boolean changed = labels.isModified(); for (TermLabel label : labels.getLabels()) { @@ -737,63 +536,18 @@ public ImmutableList getSupportedRuleNames() { } @Override - public void updateLabels(TermLabelState state, Services services, - PosInOccurrence applicationPosInOccurrence, - JTerm applicationTerm, JTerm modalityTerm, - org.key_project.prover.rules.Rule rule, - RuleApp ruleApp, Object hint, JTerm tacletTerm, JTerm newTerm, + public void updateLabels(TermLabelContext context, JTerm newTerm, Set labels) { labels.add(toAdd); } } - private static class LoggingChildTermLabelPolicy implements ChildTermLabelPolicy { - private ImmutableList supportedRuleNames = ImmutableList.nil(); - - private final List log = new LinkedList<>(); - - public LoggingChildTermLabelPolicy(String... supportedRules) { - for (String rule : supportedRules) { - supportedRuleNames = supportedRuleNames.prepend(new Name(rule)); - } - } - - @Override - public ImmutableList getSupportedRuleNames() { - return supportedRuleNames; - } - - @Override - public boolean isRuleApplicationSupported(TermServices services, - PosInOccurrence applicationPosInOccurrence, - JTerm applicationTerm, Rule rule, - Goal goal, Object hint, JTerm tacletTerm, JTerm newTerm) { - return true; - } - - @Override - public boolean addLabel(TermServices services, - PosInOccurrence applicationPosInOccurrence, - JTerm applicationTerm, Rule rule, Goal goal, Object hint, JTerm tacletTerm, - JTerm newTerm, JTerm childTerm, TermLabel label) { - log.add(label); - return true; - } - - public List getLog() { - return log; - } - } - private static class LoggingTermLabelPolicy implements TermLabelPolicy { private final List log = new LinkedList<>(); @Override - public TermLabel keepLabel(TermLabelState state, Services services, - PosInOccurrence applicationPosInOccurrence, - JTerm applicationTerm, Rule rule, - Goal goal, Object hint, JTerm tacletTerm, - JTerm newTerm, TermLabel label) { + public TermLabel keepLabel(TermLabelContext context, JTerm sourceTerm, JTerm newTerm, + TermLabel label) { log.add(label); return label; } diff --git a/key.core/src/test/java/de/uka/ilkd/key/logic/label/TermLabelEquivalenceDumpTest.java b/key.core/src/test/java/de/uka/ilkd/key/logic/label/TermLabelEquivalenceDumpTest.java new file mode 100644 index 00000000000..8ea228ef487 --- /dev/null +++ b/key.core/src/test/java/de/uka/ilkd/key/logic/label/TermLabelEquivalenceDumpTest.java @@ -0,0 +1,196 @@ +/* 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.logic.label; + +import java.nio.file.Files; +import java.nio.file.Path; +import java.nio.file.Paths; +import java.util.Iterator; +import java.util.Set; +import java.util.TreeSet; + +import de.uka.ilkd.key.control.KeYEnvironment; +import de.uka.ilkd.key.logic.JTerm; +import de.uka.ilkd.key.proof.Node; +import de.uka.ilkd.key.proof.Proof; +import de.uka.ilkd.key.settings.ProofSettings; + +import org.key_project.prover.sequent.Sequent; +import org.key_project.prover.sequent.SequentFormula; +import org.key_project.util.collection.ImmutableArray; + +import org.junit.jupiter.api.Test; + +/** + * Regression harness for the term-label reworking (equality flip + LabeledTermImpl/TermImpl + * merge). It replays a curated set of console-style KeY proofs and writes, for every proof node, + * a canonical serialization of the sequent including all term labels at every subterm. + * + *

    + * The dump is written to the directory given by the {@code labeldump.dir} system property (default + * a temp dir). Running this test on two revisions and diffing the two output directories proves + * that the change did not alter any sequent or any term label anywhere in these proofs. The test + * also records which term labels were actually observed ({@code _labels_seen.txt}) so label + * coverage is established from real data rather than assumed. + *

    + * + *

    + * This is intentionally driven by an explicit, hand-written term serializer rather than + * {@link Object#toString()} so that label capture does not depend on any pretty-printer. + *

    + */ +public class TermLabelEquivalenceDumpTest { + + /** + * Proof files relative to the repository root. Chosen to be replayable headlessly and to + * collectively exercise the term labels registered by the plain {@code JavaProfile} (origin, + * anonHeap, selectSK, ...). Labels used only by the symbolic_execution / proof_references + * modules are deliberately out of scope. + */ + private static final String[] PROOFS = { + // heap / JML operation & dependency contracts (anonHeap, selectSK, impl, origin, ...) + "key.ui/examples/heap/observer/ExampleObserver_ExampleObserver.key.proof", + "key.ui/examples/heap/observer/ExampleSubject_ExampleSubject.key.proof", + "key.ui/examples/heap/observer/ExampleSubject_notifyObservers.key.proof", + "key.ui/examples/heap/observer/ExampleSubject_inv.key.proof", + "key.ui/examples/heap/observer/ExampleSubject_change.key.proof", + "key.ui/examples/heap/observer/ExampleObserver_value.key.proof", + "key.ui/examples/heap/observer/ExampleSubject_addObserver.key.proof", + "key.ui/examples/heap/observer/ExampleSubject_value_dep.key.proof", + "key.ui/examples/heap/observer/ExampleObserver_update.key.proof", + "key.ui/examples/heap/verifyThis11_1_Maximum/project.key.proof", + "key.ui/examples/heap/coincidence_count/project.key.proof", + "key.ui/examples/heap/fm12_01_LRS/lcp.key.proof", + "key.ui/examples/heap/permutedSum/perm.proof", + "key.ui/examples/heap/BoyerMoore/BM(BM__monoLemma((I,int,int)).JML normal_behavior operation contract.0.proof", + // java_dl / arithmetic / bit operations (loopScopeIndex, SC, ...) + "key.ui/examples/standard_key/java_dl/recursion/triangular.proof", + "key.ui/examples/standard_key/arith/jdivevenodd.key.proof", + "key.ui/examples/standard_key/bitoperations/exBitwiseOr1.key.proof", + }; + + /** + * Term labels that are actually attached during standard (console) proof search and therefore + * must be observed while replaying {@link #PROOFS}. Note: {@code postCondition}, {@code undef} + * and {@code selfComposedExecution} are attached only by the information-flow module + * (key.core.infflow) and {@code Trigger} only by the SMT translation, so none of them is + * reachable by replaying standard Java profile proofs; the infflow labels are covered by the + * separate testRunAllInfProofs regression instead. + */ + private static final Set EXPECTED_LABELS = Set.of( + "origin", "anonHeapFunction", "selectSK", "impl", "SC", "loopScopeIndex"); + + @Test + public void dumpAllProofSequents() throws Exception { + final Path dumpDir = Paths.get(System.getProperty("key.labeldump.dir", + System.getProperty("java.io.tmpdir") + "/labeldump")); + Files.createDirectories(dumpDir); + final Path root = repoRoot(); + + // origin labels are user-facing and only attached when this setting is on + ProofSettings.DEFAULT_SETTINGS.getTermLabelSettings().setUseOriginLabels(true); + + final Set labelsSeen = new TreeSet<>(); + final StringBuilder index = new StringBuilder(); + int loaded = 0; + for (String rel : PROOFS) { + final Path pf = root.resolve(rel); + if (!Files.exists(pf)) { + index.append("MISSING ").append(rel).append('\n'); + continue; + } + KeYEnvironment env = null; + try { + env = KeYEnvironment.load(pf); + final Proof proof = env.getLoadedProof(); + final StringBuilder sb = new StringBuilder(); + int nodes = 0; + final Iterator it = proof.root().subtreeIterator(); + while (it.hasNext()) { + final Node n = it.next(); + sb.append("=== node ").append(n.serialNr()).append(" ===\n"); + dumpSequent(n.sequent(), sb, labelsSeen); + nodes++; + } + Files.writeString(dumpDir.resolve(dumpName(rel)), sb.toString()); + index.append("OK ").append(nodes).append(" nodes ").append(rel).append('\n'); + loaded++; + } catch (Exception e) { + index.append("FAILED ").append(rel).append(" : ").append(e).append('\n'); + } finally { + if (env != null) { + env.dispose(); + } + } + } + Files.writeString(dumpDir.resolve("_index.txt"), index.toString()); + Files.writeString(dumpDir.resolve("_labels_seen.txt"), String.join("\n", labelsSeen)); + System.out.println("[labeldump] wrote " + loaded + "/" + PROOFS.length + + " proof dumps to " + dumpDir); + System.out.println("[labeldump] labels observed: " + labelsSeen); + + org.junit.jupiter.api.Assertions.assertTrue(loaded >= 15, + "expected at least 15 of the curated proofs to replay, got " + loaded); + org.junit.jupiter.api.Assertions.assertTrue(labelsSeen.containsAll(EXPECTED_LABELS), + "term-label coverage regressed; expected " + EXPECTED_LABELS + " but saw " + + labelsSeen); + } + + private static void dumpSequent(Sequent seq, StringBuilder sb, Set labelsSeen) { + for (SequentFormula sf : seq.antecedent()) { + dumpTerm((JTerm) sf.formula(), sb, labelsSeen); + sb.append('\n'); + } + sb.append("==>\n"); + for (SequentFormula sf : seq.succedent()) { + dumpTerm((JTerm) sf.formula(), sb, labelsSeen); + sb.append('\n'); + } + } + + /** Recursively serialize a term, emitting the (sorted) label set at every node. */ + private static void dumpTerm(JTerm t, StringBuilder sb, Set labelsSeen) { + sb.append(t.op().name()); + if (t.hasLabels()) { + final ImmutableArray labels = t.getLabels(); + final TreeSet here = new TreeSet<>(); + for (int i = 0, sz = labels.size(); i < sz; i++) { + final String s = labels.get(i).toString(); + here.add(s); + labelsSeen.add(labels.get(i).name().toString()); + } + sb.append("<<").append(String.join(",", here)).append(">>"); + } + if (!t.boundVars().isEmpty()) { + sb.append('{').append(t.boundVars()).append('}'); + } + if (t.arity() > 0) { + sb.append('('); + for (int i = 0; i < t.arity(); i++) { + if (i > 0) { + sb.append(','); + } + dumpTerm(t.sub(i), sb, labelsSeen); + } + sb.append(')'); + } + } + + private static String dumpName(String rel) { + return rel.replaceAll("[^A-Za-z0-9._-]", "_") + ".dump"; + } + + /** Walk up from the working directory until the KeY example tree is found. */ + private static Path repoRoot() { + Path p = Paths.get("").toAbsolutePath(); + while (p != null) { + if (Files.exists(p.resolve("key.ui/examples/heap"))) { + return p; + } + p = p.getParent(); + } + throw new IllegalStateException("could not locate repository root from " + + Paths.get("").toAbsolutePath()); + } +} diff --git a/key.core/src/test/java/de/uka/ilkd/key/util/TestLinkedHashMapWrapper.java b/key.core/src/test/java/de/uka/ilkd/key/util/TestLinkedHashMapWrapper.java index a52478d9a61..411adda347e 100644 --- a/key.core/src/test/java/de/uka/ilkd/key/util/TestLinkedHashMapWrapper.java +++ b/key.core/src/test/java/de/uka/ilkd/key/util/TestLinkedHashMapWrapper.java @@ -128,9 +128,10 @@ public void testTermLabelProperties() { assertEquals(1, irrelevantTermLabelsMap.size()); // add mappings with irrelevant labels to all maps - assertNull(basicMap.put(irrelevantLabelTT, 2), - "Nothing should be returned as basicMap should not contain the key"); - assertEquals(2, basicMap.size()); + assertEquals(1, basicMap.put(irrelevantLabelTT, 2), + "Old value should be returned as term equality (basicMap) now ignores term labels"); + assertEquals(1, basicMap.size(), + "Size should not increase as term equality ignores labels"); assertEquals(1, termLabelsMap.put(irrelevantLabelTT, 2), "Old value should be returned as termLabelsMap should already contain the key"); @@ -148,9 +149,10 @@ public void testTermLabelProperties() { // add mappings with relevant labels to all maps - assertNull(basicMap.put(relevantLabelTT, 3), - "Nothing should be returned as basicMap should not contain the key"); - assertEquals(3, basicMap.size()); + assertEquals(2, basicMap.put(relevantLabelTT, 3), + "Old value should be returned as term equality (basicMap) now ignores term labels"); + assertEquals(1, basicMap.size(), + "Size should not increase as term equality ignores labels"); assertEquals(2, termLabelsMap.put(relevantLabelTT, 3), "Value 3 should be returned as termLabelsMap was previously updated with irrelevantLabelTT");