From e7f67fa8998e5a192c43b8b53a9c453657cecc00 Mon Sep 17 00:00:00 2001 From: Richard Bubel Date: Fri, 3 Jul 2026 07:47:18 +0200 Subject: [PATCH 01/14] Remove unused ChildTermLabelPolicy hook family from term label framework No profile ever registers a ChildTermLabelPolicy (neither direct child nor child-and-grandchild variant). Delete the interface, the four policy maps and their dispatch in TermLabelManager, the corresponding TermLabelConfiguration parameters, and the tests exercising the dead hooks. Generated with AI tooling support --- .../profile/SimplifyTermProfile.java | 2 +- .../profile/SymbolicExecutionJavaProfile.java | 10 +- .../uka/ilkd/key/logic/label/TermLabel.java | 7 - .../key/logic/label/TermLabelManager.java | 277 +----------------- .../uka/ilkd/key/proof/init/JavaProfile.java | 1 - .../key/rule/label/ChildTermLabelPolicy.java | 105 ------- .../ilkd/key/rule/label/RuleSpecificTask.java | 1 - .../ilkd/key/logic/TestTermLabelManager.java | 240 +-------------- 8 files changed, 21 insertions(+), 622 deletions(-) delete mode 100644 key.core/src/main/java/de/uka/ilkd/key/rule/label/ChildTermLabelPolicy.java 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..62a2cdf42b8 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 @@ -66,7 +66,7 @@ protected ImmutableList computeTermLabelConfiguration() 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/logic/label/TermLabel.java b/key.core/src/main/java/de/uka/ilkd/key/logic/label/TermLabel.java index 7f57d8d7903..7460f2179fa 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; @@ -108,12 +107,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}.
    • 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..511d515607e 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.*; @@ -85,30 +84,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 +132,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 +172,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 @@ -602,25 +534,6 @@ private void addLabelsBasedOnApplicationTerm(TermLabelState state, Services serv // 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); - } } /** @@ -807,158 +720,6 @@ protected void performTermLabelPolicies(TermLabelState state, Services services, } } - /** - *

    - * 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()); - } - } - } - } - 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. - *

    - *

    - * 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 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. @@ -1868,16 +1629,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 +1651,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 +1663,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 +1670,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 +1679,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 +1720,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/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/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/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/test/java/de/uka/ilkd/key/logic/TestTermLabelManager.java b/key.core/src/test/java/de/uka/ilkd/key/logic/TestTermLabelManager.java index 37648085ca4..f48aba6762b 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 @@ -18,7 +18,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; @@ -114,7 +113,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 @@ -217,7 +216,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 +243,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 +261,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 +268,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 +301,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 +322,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 +370,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 +408,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 +434,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 +463,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 +476,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; } @@ -747,44 +573,6 @@ public void updateLabels(TermLabelState state, Services services, } } - 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<>(); From d633afd9b7cfef262488af2d2b534f8b7c125f43 Mon Sep 17 00:00:00 2001 From: Richard Bubel Date: Fri, 3 Jul 2026 08:08:04 +0200 Subject: [PATCH 02/14] Make term equality label-agnostic; add equalsIncludingLabels for strict cases Term labels are not soundness-relevant and sequent membership already ignores them (isRedundant uses RENAMING_TERM_PROPERTY). Yet TermImpl.equals/hashCode were label-sensitive, forcing ~74 call sites to opt out via equalsModProperty(IRRELEVANT_TERM_LABELS/TERM_LABELS). Flip the default: - TermImpl.equals/hashCode now ignore all term labels; LabeledTermImpl drops its equals/computeHashCode overrides. - Add JTerm.equalsIncludingLabels (label-sensitive, sets per subterm) plus a cached containsLabelsRecursive() guard on TermImpl. - Protect the few caches whose correctness needs label distinction: the TermFactory intern cache now skips label-carrying terms; the taclet-app index CacheKey and the origin-subterm cache (via new StrictTermKey) use equalsIncludingLabels. TermLabelManager refactoring change-detection uses equalsIncludingLabels. Collapsing the redundant equalsModProperty call sites follows separately. Generated with AI tooling support --- .../de/uka/ilkd/key/java/ServiceCaches.java | 8 +- .../java/de/uka/ilkd/key/logic/JTerm.java | 20 +++++ .../uka/ilkd/key/logic/LabeledTermImpl.java | 50 ++--------- .../de/uka/ilkd/key/logic/StrictTermKey.java | 29 ++++++ .../de/uka/ilkd/key/logic/TermFactory.java | 7 +- .../java/de/uka/ilkd/key/logic/TermImpl.java | 89 +++++++++++++++++-- .../key/logic/label/TermLabelManager.java | 13 +-- .../PrefixTermTacletAppIndexCacheImpl.java | 7 +- .../label/OriginTermLabelRefactoring.java | 17 +++- .../ilkd/key/logic/LabeledTermImplTest.java | 39 ++++++-- 10 files changed, 209 insertions(+), 70 deletions(-) create mode 100644 key.core/src/main/java/de/uka/ilkd/key/logic/StrictTermKey.java 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..44634c988f4 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; @@ -162,9 +163,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 +184,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; } 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..111c22c1b70 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,26 @@ 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); + /** * 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 index 4f1dba590ea..169745776e6 100644 --- 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 @@ -22,13 +22,12 @@ * 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. * + * As for all terms, {@link #equals(Object)} compares the term structure and ignores term labels. + * Use {@link #equalsIncludingLabels(Object)} to compare labels as well. 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. * * @see JTerm * @see TermImpl @@ -114,43 +113,6 @@ public boolean containsLabel(TermLabel label) { 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()); 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..5e19e68350b --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/logic/StrictTermKey.java @@ -0,0 +1,29 @@ +/* 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 (label-agnostic) hash code: label variants collide, which is + * harmless as {@link #equals(Object)} disambiguates them. + *

    + * + * @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.hashCode(); + } +} 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..86bf07e51e5 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 @@ -125,8 +125,11 @@ private JTerm doCreateTerm(Operator op, ImmutableArray subs, : new LabeledTermImpl(op, subs, boundVars, labels, origin)); // 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. - if (cache != null && !newTerm.containsJavaBlockRecursive()) { + // may be different. Terms carrying term labels (directly or in a subterm) are not cached + // either: equals() ignores labels, so the cache would conflate label variants and + // silently drop labels from newly created terms. + if (cache != null && !newTerm.containsJavaBlockRecursive() + && !newTerm.containsLabelsRecursive()) { JTerm term; synchronized (cache) { term = cache.get(newTerm); 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..9b3df4c056f 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 @@ -83,6 +83,13 @@ private enum ThreeValuedTruth { /** caches whether this term or a (direct/indirect) child has a {@link Transformer} operator. */ private ThreeValuedTruth containsTransformerRecursive = ThreeValuedTruth.UNKNOWN; + /** + * This flag indicates that the {@link JTerm} itself or one of its children carries a + * {@link TermLabel}. As {@link #equals(Object)} ignores term labels, label-sensitive + * consumers (e.g. the term factory cache) use this flag as a cheap guard. + */ + private ThreeValuedTruth containsLabelsRecursive = ThreeValuedTruth.UNKNOWN; + // ------------------------------------------------------------------------- // constructors // ------------------------------------------------------------------------- @@ -281,7 +288,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 +297,67 @@ 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) { + 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) { @@ -420,6 +477,28 @@ public boolean containsJavaBlockRecursive() { return containsJavaBlockRecursive == ThreeValuedTruth.TRUE; } + /** + * {@inheritDoc} + */ + @Override + public boolean containsLabelsRecursive() { + if (containsLabelsRecursive == ThreeValuedTruth.UNKNOWN) { + ThreeValuedTruth result = ThreeValuedTruth.FALSE; + if (hasLabels()) { + result = ThreeValuedTruth.TRUE; + } else { + for (int i = 0, arity = subs.size(); i < arity; i++) { + if (subs.get(i).containsLabelsRecursive()) { + result = ThreeValuedTruth.TRUE; + break; + } + } + } + this.containsLabelsRecursive = result; + } + return containsLabelsRecursive == ThreeValuedTruth.TRUE; + } + @Override public boolean containsTransformerRecursive() { if (containsTransformerRecursive == ThreeValuedTruth.UNKNOWN) { 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 511d515607e..2fb13b5053d 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 @@ -821,7 +821,7 @@ public JTerm refactorSequentFormula(TermLabelState state, Services services, JTerm newTerm = refactorApplicationTerm(state, services, applicationPosInOccurrence, oldTerm, rule, goal, hint, tacletTerm, refactorings, services.getTermFactory()); - if (newTerm != null && !newTerm.equals(oldTerm)) { + if (newTerm != null && !newTerm.equalsIncludingLabels(oldTerm)) { return replaceTerm(state, applicationPosInOccurrence, newTerm, services.getTermFactory(), refactorings.childAndGrandchildRefactoringsAndParents(), services, @@ -972,7 +972,8 @@ public void refactorGoal(TermLabelState state, Services services, JTerm newApplicationTerm = refactorApplicationTerm(state, services, applicationPosInOccurrence, applicationTerm, rule, goal, hint, tacletTerm, refactorings, tf); - if (newApplicationTerm != null && !newApplicationTerm.equals(applicationTerm)) { + if (newApplicationTerm != null + && !newApplicationTerm.equalsIncludingLabels(applicationTerm)) { JTerm root = replaceTerm(state, applicationPosInOccurrence, newApplicationTerm, tf, refactorings.childAndGrandchildRefactoringsAndParents(), services, applicationPosInOccurrence, newApplicationTerm, rule, goal, hint, tacletTerm); @@ -1120,7 +1121,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); @@ -1426,7 +1427,7 @@ private JTerm refactorChildrenRecursively(TermLabelState state, Services service newSubs[i] = refactorLabelsRecursive(state, services, applicationPosInOccurrence, applicationTerm, rule, goal, hint, tacletTerm, sub, allChildAndGrandchildRefactorings); - if (!newSubs[i].equals(sub)) { + if (!newSubs[i].equalsIncludingLabels(sub)) { changed = true; } } @@ -1513,7 +1514,7 @@ protected void refactorSemisequent(TermLabelState state, Services services, refactorLabelsRecursive(state, services, applicationPosInOccurrence, applicationTerm, rule, goal, hint, tacletTerm, (JTerm) sfa.formula(), activeRefactorings); - if (!sfa.formula().equals(updatedTerm)) { + if (!((JTerm) sfa.formula()).equalsIncludingLabels(updatedTerm)) { goal.changeFormula(new SequentFormula(updatedTerm), new PosInOccurrence(sfa, PosInTerm.getTopLevel(), inAntec)); } @@ -1551,7 +1552,7 @@ protected JTerm refactorLabelsRecursive(TermLabelState state, Services services, JTerm oldSub = term.sub(i); newSubs[i] = refactorLabelsRecursive(state, services, applicationPosInOccurrence, applicationTerm, rule, goal, hint, tacletTerm, oldSub, activeRefactorings); - if (!newSubs[i].equals(oldSub)) { + if (!newSubs[i].equalsIncludingLabels(oldSub)) { subsChanged = true; } } 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/rule/label/OriginTermLabelRefactoring.java b/key.core/src/main/java/de/uka/ilkd/key/rule/label/OriginTermLabelRefactoring.java index b7a14eae08d..419bdcedb10 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 @@ -10,6 +10,7 @@ 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; @@ -85,7 +86,7 @@ public void refactorLabels(TermLabelState state, Services services, // cache origins per term to avoid a quadratic recursive collection per rule // application - final Map> originsCache = + final Map> originsCache = services.getCaches().getSubtermOriginsCache(); Set subtermOrigins = new LinkedHashSet<>(); for (JTerm sub : term.subs()) { @@ -135,8 +136,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 +165,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/test/java/de/uka/ilkd/key/logic/LabeledTermImplTest.java b/key.core/src/test/java/de/uka/ilkd/key/logic/LabeledTermImplTest.java index b63dd7f6108..aa88ea19289 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,40 @@ 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)); } /** From 20647463a706e2fd248c4595c65d4c15460ccdcc Mon Sep 17 00:00:00 2001 From: Richard Bubel Date: Fri, 3 Jul 2026 08:26:40 +0200 Subject: [PATCH 03/14] Add term-label equivalence regression harness Replays 17 console-style KeY proofs (~23k nodes) and serializes every proof node's sequent including all term labels at every subterm, to the directory given by -Dkey.labeldump.dir. Diffing the output across two revisions proves a change did not alter any sequent or label. Asserts coverage of the six term labels actually attached during standard proof search (origin, anonHeapFunction, selectSK, impl, SC, loopScopeIndex). Generated with AI tooling support --- .../label/TermLabelEquivalenceDumpTest.java | 195 ++++++++++++++++++ 1 file changed, 195 insertions(+) create mode 100644 key.core/src/test/java/de/uka/ilkd/key/logic/label/TermLabelEquivalenceDumpTest.java 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..eed78f30c38 --- /dev/null +++ b/key.core/src/test/java/de/uka/ilkd/key/logic/label/TermLabelEquivalenceDumpTest.java @@ -0,0 +1,195 @@ +/* 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} and + * {@code undef} are registered by {@code JavaProfile} but never attached by any rule, so they + * are not expected; {@code selfComposedExecution} is information-flow only and {@code Trigger} + * is SMT-translation only, so neither is reachable by proof replay. + */ + 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()); + } +} From 79f4df11f7df402c4e5dfd2e6d7cbf28ddb9400e Mon Sep 17 00:00:00 2001 From: Richard Bubel Date: Fri, 3 Jul 2026 08:31:56 +0200 Subject: [PATCH 04/14] Merge LabeledTermImpl into TermImpl With term labels no longer part of term identity, the LabeledTermImpl subclass only served to keep a labels field off unlabeled terms. Fold it into TermImpl: a single nullable labels field (empty normalized to the shared EMPTY_LABEL_LIST), label accessors and label-aware toString moved up, and TermFactory now always constructs TermImpl. This removes the two-class hierarchy and the 'same value, different class, still equal' hazard the equality flip introduced. Verified behavior-preserving: replaying 17 console proofs (23373 nodes) yields byte-identical sequents including every term label at every subterm. Generated with AI tooling support --- .../uka/ilkd/key/logic/LabeledTermImpl.java | 132 ------------------ .../de/uka/ilkd/key/logic/TermFactory.java | 5 +- .../java/de/uka/ilkd/key/logic/TermImpl.java | 55 ++++++-- 3 files changed, 48 insertions(+), 144 deletions(-) delete mode 100644 key.core/src/main/java/de/uka/ilkd/key/logic/LabeledTermImpl.java 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 169745776e6..00000000000 --- a/key.core/src/main/java/de/uka/ilkd/key/logic/LabeledTermImpl.java +++ /dev/null @@ -1,132 +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. - *

    - * - * As for all terms, {@link #equals(Object)} compares the term structure and ignores term labels. - * Use {@link #equalsIncludingLabels(Object)} to compare labels as well. 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. - * - * @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 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/TermFactory.java b/key.core/src/main/java/de/uka/ilkd/key/logic/TermFactory.java index 86bf07e51e5..a5658297d54 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 @@ -119,10 +119,7 @@ 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. Terms carrying term labels (directly or in a subterm) are not cached 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 9b3df4c056f..4f4f1b54415 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,7 +3,9 @@ * 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.stream.Collectors; import de.uka.ilkd.key.java.ast.PositionInfo; import de.uka.ilkd.key.logic.label.TermLabel; @@ -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,6 +58,14 @@ 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 @@ -105,11 +117,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() { @@ -414,16 +440,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(); @@ -437,22 +469,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; } /** From d3760d0b4a744ec40522d173a3471f6212b3470e Mon Sep 17 00:00:00 2001 From: Richard Bubel Date: Fri, 3 Jul 2026 08:41:06 +0200 Subject: [PATCH 05/14] Intern labeled terms via a label-sensitive cache key The equality flip left the TermFactory cache keyed on the now label-agnostic term equality, which would have conflated label variants; the interim fix excluded label-carrying terms from the cache entirely. That is a regression: origin labels alone are attached to a large fraction of terms, so the cache would go largely unused, term interning (and the == fast paths that rely on it) would stop firing, and memory would grow through duplicate labeled terms. Instead key the cache on StrictTermKey (label-sensitive equality) and cache all terms again. This reproduces exactly the interning behaviour from when term equality was itself label-sensitive, while keeping term.equals() label-agnostic for the logic layer. Add JTerm.labeledHashCode() (cached, label-sensitive) so label variants keep distinct hash buckets. Generated with AI tooling support --- .../de/uka/ilkd/key/java/ServiceCaches.java | 8 +++-- .../java/de/uka/ilkd/key/logic/JTerm.java | 10 ++++++ .../de/uka/ilkd/key/logic/StrictTermKey.java | 7 ++-- .../de/uka/ilkd/key/logic/TermFactory.java | 22 ++++++++----- .../java/de/uka/ilkd/key/logic/TermImpl.java | 33 +++++++++++++++++++ .../ilkd/key/logic/LabeledTermImplTest.java | 29 ++++++++++++++++ 6 files changed, 94 insertions(+), 15 deletions(-) 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 44634c988f4..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 @@ -118,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 @@ -216,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 111c22c1b70..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 @@ -138,6 +138,16 @@ public interface JTerm */ 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/StrictTermKey.java b/key.core/src/main/java/de/uka/ilkd/key/logic/StrictTermKey.java index 5e19e68350b..ebbf7d4cc00 100644 --- 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 @@ -10,8 +10,9 @@ * distinction via {@link JTerm#equalsIncludingLabels(Object)}. * *

    - * The hash code is the term's (label-agnostic) hash code: label variants collide, which is - * harmless as {@link #equals(Object)} disambiguates them. + * 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) @@ -24,6 +25,6 @@ public boolean equals(Object o) { @Override public int hashCode() { - return term.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 a5658297d54..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; } @@ -122,19 +122,23 @@ private JTerm doCreateTerm(Operator op, ImmutableArray subs, 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. Terms carrying term labels (directly or in a subterm) are not cached - // either: equals() ignores labels, so the cache would conflate label variants and - // silently drop labels from newly created terms. - if (cache != null && !newTerm.containsJavaBlockRecursive() - && !newTerm.containsLabelsRecursive()) { + // 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 4f4f1b54415..db9154bd235 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 @@ -82,6 +82,12 @@ private enum ThreeValuedTruth { */ 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; /** @@ -410,6 +416,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)) { 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 aa88ea19289..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 @@ -75,6 +75,35 @@ public void testEqualsLabelOnSubterm() { 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()); + } + /** * Tests {@link JTerm#hasLabels()}, {@link JTerm#hasLabels()} and * {@link JTerm#containsLabel(TermLabel)}. From 5342cca70d71a2c26c66f132259a7ea33bd847da Mon Sep 17 00:00:00 2001 From: Richard Bubel Date: Fri, 3 Jul 2026 08:45:43 +0200 Subject: [PATCH 06/14] Update TestLinkedHashMapWrapper for label-agnostic term equality The plain LinkedHashMap baseline in testTermLabelProperties encoded the old label-sensitive term equality; under the flip a plain map treats label variants as the same key. Adjust the basicMap assertions accordingly (wrapper-map assertions are unaffected as they compare via a Property). Generated with AI tooling support --- .../ilkd/key/util/TestLinkedHashMapWrapper.java | 14 ++++++++------ 1 file changed, 8 insertions(+), 6 deletions(-) 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"); From 486fbb92e9896ed2136f522d283ca2d2e3280333 Mon Sep 17 00:00:00 2001 From: Richard Bubel Date: Fri, 3 Jul 2026 08:52:17 +0200 Subject: [PATCH 07/14] Short-circuit labelsEqualRecursive on reference-identical subterms equalsIncludingLabels walks the tree once for structural equality and once for labels. Because the term factory interns terms label-sensitively, structurally shared subterms are reference-identical, so add a t1 == t2 fast path to the label walk. This restores cached labeled-term construction to parity with the pre-flip factory (a synthetic all-labeled depth-15 tree went 6.3ms -> 2.4ms, matching stock main's 2.3ms); equals on labeled terms is now marginally faster than stock. Generated with AI tooling support --- key.core/src/main/java/de/uka/ilkd/key/logic/TermImpl.java | 5 +++++ 1 file changed, 5 insertions(+) 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 db9154bd235..9a732252b1c 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 @@ -369,6 +369,11 @@ public boolean equalsIncludingLabels(Object o) { * @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()) { From 6ef226938b4c11f279cda9e8edc2e9761a5ff79f Mon Sep 17 00:00:00 2001 From: Richard Bubel Date: Fri, 3 Jul 2026 09:03:10 +0200 Subject: [PATCH 08/14] Pack TermImpl lazy tri-state caches into a single int Replace the four ThreeValuedTruth reference fields (rigid, containsJavaBlock/ Transformer/LabelsRecursive) with one packed int (two bits each), saving ~12 bytes per term object. Writes go through an AtomicIntegerFieldUpdater CAS that only sets a still-UNKNOWN flag, so concurrent computation of different flags on the same shared, immutable term cannot lose updates (the previous separate reference fields were independently written; a shared word needs CAS). The field is volatile; reads are plain volatile int loads. Generated with AI tooling support --- .../java/de/uka/ilkd/key/logic/TermImpl.java | 120 ++++++++++-------- 1 file changed, 66 insertions(+), 54 deletions(-) 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 9a732252b1c..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 @@ -5,9 +5,9 @@ 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.*; @@ -67,15 +67,8 @@ class TermImpl implements JTerm { 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. @@ -91,22 +84,42 @@ private enum ThreeValuedTruth { 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; - /** caches whether this term or a (direct/indirect) child has a {@link Transformer} operator. */ - private ThreeValuedTruth containsTransformerRecursive = ThreeValuedTruth.UNKNOWN; + private static final AtomicIntegerFieldUpdater FLAGS = + AtomicIntegerFieldUpdater.newUpdater(TermImpl.class, "flags"); - /** - * This flag indicates that the {@link JTerm} itself or one of its children carries a - * {@link TermLabel}. As {@link #equals(Object)} ignores term labels, label-sensitive - * consumers (e.g. the term factory cache) use this flag as a cheap guard. - */ - private ThreeValuedTruth containsLabelsRecursive = ThreeValuedTruth.UNKNOWN; + 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; + + 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 @@ -267,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; } @@ -537,21 +549,21 @@ 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; } /** @@ -559,40 +571,40 @@ public boolean containsJavaBlockRecursive() { */ @Override public boolean containsLabelsRecursive() { - if (containsLabelsRecursive == ThreeValuedTruth.UNKNOWN) { - ThreeValuedTruth result = ThreeValuedTruth.FALSE; - if (hasLabels()) { - result = ThreeValuedTruth.TRUE; - } else { + 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 = ThreeValuedTruth.TRUE; + result = true; break; } } } - this.containsLabelsRecursive = result; + flag = result ? FLAG_TRUE : FLAG_FALSE; + setFlag(SHIFT_LABELS, flag); } - return containsLabelsRecursive == ThreeValuedTruth.TRUE; + 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; } From e33df5153b0028845e53f2ca8fa8c935e9efcd26 Mon Sep 17 00:00:00 2001 From: Richard Bubel Date: Fri, 3 Jul 2026 09:56:39 +0200 Subject: [PATCH 09/14] Collapse TERM_LABELS_PROPERTY comparisons to plain term equality TermLabelsProperty ignores all term labels, which is exactly what the (now label-agnostic) default term equality does. Replace the four equalsModProperty(TERM_LABELS_PROPERTY) / equalsModThisProperty call sites with plain equals() and drop the dead imports. (The TermLabelsProperty class is kept for now; its removal is bundled with the IRRELEVANT_TERM_LABELS_PROPERTY review.) Generated with AI tooling support --- key.core/src/main/java/de/uka/ilkd/key/proof/OpReplacer.java | 3 +-- .../java/de/uka/ilkd/key/rule/UseDependencyContractRule.java | 3 +-- .../src/main/java/de/uka/ilkd/key/scripts/HideCommand.java | 3 +-- .../main/java/de/uka/ilkd/key/speclang/ContractFactory.java | 5 ++--- 4 files changed, 5 insertions(+), 9 deletions(-) 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/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/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 From 1e7c9511b36a5ec8a984079c0bf500d7c8d66edb Mon Sep 17 00:00:00 2001 From: Richard Bubel Date: Fri, 3 Jul 2026 10:38:05 +0200 Subject: [PATCH 10/14] Remove unused APPLICATION_DIRECT_CHILDREN refactoring scope No term label refactoring ever returns this scope (verified across all modules). Delete the enum value, the directChildRefactorings bucket in RefactoringsContainer, the refactorChildTerms pass, and the framework tests exercising the dead scope. Co-Authored-By: Claude Opus 4.8 --- .../uka/ilkd/key/logic/label/TermLabel.java | 3 - .../key/logic/label/TermLabelManager.java | 70 ++----------------- .../key/rule/label/TermLabelRefactoring.java | 5 -- .../ilkd/key/logic/TestTermLabelManager.java | 21 ------ 4 files changed, 4 insertions(+), 95 deletions(-) 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 7460f2179fa..18877b4cdfe 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 @@ -107,9 +107,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<> ~~> 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/TermLabelManager.java b/key.core/src/main/java/de/uka/ilkd/key/logic/label/TermLabelManager.java index 2fb13b5053d..0dbdce30a62 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 @@ -1169,8 +1169,6 @@ private void determineAndCollectRuleSpecificRefactorings(TermLabelState state, } 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); @@ -1214,8 +1212,6 @@ private void determineAndRuleIndependentRefactorings(TermLabelState state, } 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); @@ -1268,18 +1264,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<>()); } /** @@ -1297,57 +1290,6 @@ 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. * @@ -1463,13 +1405,9 @@ 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() + 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, 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..49f3abf8167 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 @@ -153,11 +153,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/test/java/de/uka/ilkd/key/logic/TestTermLabelManager.java b/key.core/src/test/java/de/uka/ilkd/key/logic/TestTermLabelManager.java index f48aba6762b..c6a352440d4 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 @@ -64,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"); - } - /** * */ @@ -191,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 + "\"."); } From 6681f861ad06ed9cf98028847340922bb8afa23e Mon Sep 17 00:00:00 2001 From: Richard Bubel Date: Fri, 3 Jul 2026 10:42:44 +0200 Subject: [PATCH 11/14] Correct label-coverage note: postCondition/undef/selfComposedExecution are infflow-attached These labels are attached by key.core.infflow (InfFlowBlockContract/ WhileInvariantRule, PrepareInfFlowContractPreBranchesMacro, InfFlowInputOutputRelationSnippet), not dead as the harness comment claimed; they are simply unreachable from standard Java profile replays and covered by testRunAllInfProofs instead. Co-Authored-By: Claude Opus 4.8 --- .../key/logic/label/TermLabelEquivalenceDumpTest.java | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) 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 index eed78f30c38..8ea228ef487 100644 --- 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 @@ -72,10 +72,11 @@ public class TermLabelEquivalenceDumpTest { /** * Term labels that are actually attached during standard (console) proof search and therefore - * must be observed while replaying {@link #PROOFS}. Note: {@code postCondition} and - * {@code undef} are registered by {@code JavaProfile} but never attached by any rule, so they - * are not expected; {@code selfComposedExecution} is information-flow only and {@code Trigger} - * is SMT-translation only, so neither is reachable by proof replay. + * 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"); From a7370888fa2f013e252c82b89b9e277ebb11ba39 Mon Sep 17 00:00:00 2001 From: Richard Bubel Date: Fri, 3 Jul 2026 11:05:21 +0200 Subject: [PATCH 12/14] Rewrite term-label API documentation for the reworked framework Document the new equality contract on TermLabel (equals ignores all labels; equalsIncludingLabels/labeledHashCode strict; IRRELEVANT property in between), make the Policy-before-Update execution order an explicit documented contract on both hook interfaces and on TermLabelManager, state on TermLabelsProperty that it is now equivalent to plain equals for JTerms, and describe on IrrelevantTermLabelsProperty the three comparison modes and why label-kind knowledge lives in a Property rather than on the term. Co-Authored-By: Claude Opus 4.8 --- .../IrrelevantTermLabelsProperty.java | 12 +++++++- .../logic/equality/TermLabelsProperty.java | 7 +++++ .../uka/ilkd/key/logic/label/TermLabel.java | 28 +++++++++++++------ .../key/logic/label/TermLabelManager.java | 11 ++++++-- .../ilkd/key/rule/label/TermLabelPolicy.java | 13 +++++++-- .../ilkd/key/rule/label/TermLabelUpdate.java | 10 +++++-- 6 files changed, 64 insertions(+), 17 deletions(-) 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 18877b4cdfe..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 @@ -48,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. *

    *

    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 0dbdce30a62..94b70ceecbc 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 @@ -56,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 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..8b390f2f471 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 @@ -21,11 +21,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. *

    *

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

    * * @author Martin Hentschel 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..ab9da0ecfce 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 @@ -26,8 +26,14 @@ * to add or remove maintained {@link TermLabel}s which will be added to the new {@link JTerm}. *

    *

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

    * * @author Martin Hentschel From e05adcbd65c6448b83b0dede84c99f2afaf8ed50 Mon Sep 17 00:00:00 2001 From: Richard Bubel Date: Fri, 3 Jul 2026 11:22:44 +0200 Subject: [PATCH 13/14] Introduce TermLabelContext parameter object for term label hooks The term label hooks dragged the identical 8-tuple (state, services, applicationPosInOccurrence, applicationTerm, rule, goal/ruleApp, hint, tacletTerm) through every signature: keepLabel took 10 parameters, updateLabels 11, and 26 TermLabelManager methods re-threaded the tuple hop by hop. Bundle the rule application into an immutable TermLabelContext record, constructed once per manager entry point; hooks now receive (context, payload...) only: TermLabel keepLabel(TermLabelContext, JTerm sourceTerm, JTerm newTerm, TermLabel) void updateLabels(TermLabelContext, JTerm newTerm, Set) RefactoringScope defineRefactoringScope(TermLabelContext) void refactorLabels(TermLabelContext, JTerm term, LabelCollection) The policy signature keeps the source term explicit because modality-term policies are invoked with the modality term, not the application term (this also documents that so-far implicit contract). The context carries both goal and ruleApp (nullable), removing the arbitrary asymmetry where policies got only the former and updates only the latter. TermLabelMerger is unchanged (its parameters are all payload). The static entry points keep their raw signatures, so rule implementations are untouched. Net -418 lines; TermLabelManager shrinks from ~1990 to 1629 lines. Verified: full sequent+label equivalence over the 17-proof corpus (byte-identical), logic tests green. Co-Authored-By: Claude Opus 4.8 --- .../BlockContractValidityTermLabelUpdate.java | 21 +- .../label/FormulaTermLabelRefactoring.java | 44 +- .../rule/label/FormulaTermLabelUpdate.java | 29 +- .../rule/label/LoopBodyTermLabelUpdate.java | 16 +- ...nvariantNormalBehaviorTermLabelUpdate.java | 16 +- ...veInCheckBranchesTermLabelRefactoring.java | 21 +- .../label/StayOnFormulaTermLabelPolicy.java | 26 +- .../SymbolicExecutionTermLabelUpdate.java | 24 +- .../profile/SimplifyTermProfile.java | 4 +- .../key/logic/label/TermLabelContext.java | 54 ++ .../key/logic/label/TermLabelManager.java | 521 +++++------------- .../key/rule/label/OriginTermLabelPolicy.java | 18 +- .../label/OriginTermLabelRefactoring.java | 38 +- .../rule/label/PerpetualTermLabelPolicy.java | 12 +- .../label/StayOnOperatorTermLabelPolicy.java | 16 +- .../ilkd/key/rule/label/TermLabelPolicy.java | 36 +- .../key/rule/label/TermLabelRefactoring.java | 50 +- .../ilkd/key/rule/label/TermLabelUpdate.java | 45 +- .../ilkd/key/logic/TestTermLabelManager.java | 25 +- 19 files changed, 326 insertions(+), 690 deletions(-) create mode 100644 key.core/src/main/java/de/uka/ilkd/key/logic/label/TermLabelContext.java 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 62a2cdf42b8..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,9 +61,7 @@ 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)); 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 94b70ceecbc..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 @@ -512,35 +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); + performTermLabelPolicies(context, context.applicationTerm(), newTerm, + applicationTermPolicyMap, newLabels); } /** @@ -592,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])); @@ -650,121 +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 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}. */ - 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); + 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); + } + } } } } /** *

    - * Performs the given {@link TermLabelPolicy} instances. + * Performs the given {@link TermLabelUpdate} 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 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); - } - } - } - - /** - *

    - * 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 context the {@link TermLabelContext} of the current rule application * @param newTerm the template for the new {@link JTerm} to create + * @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 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); } } @@ -821,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()); + refactorApplicationTerm(context, refactorings, services.getTermFactory()); if (newTerm != null && !newTerm.equalsIncludingLabels(oldTerm)) { - return replaceTerm(state, applicationPosInOccurrence, newTerm, + 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; } @@ -899,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; } @@ -971,34 +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); + JTerm newApplicationTerm = refactorApplicationTerm(context, refactorings, tf); if (newApplicationTerm != null && !newApplicationTerm.equalsIncludingLabels(applicationTerm)) { - JTerm root = replaceTerm(state, applicationPosInOccurrence, newApplicationTerm, tf, - refactorings.childAndGrandchildRefactoringsAndParents(), services, - applicationPosInOccurrence, newApplicationTerm, rule, goal, hint, tacletTerm); + 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()); } } @@ -1065,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()); } } @@ -1083,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; @@ -1119,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(); } @@ -1139,119 +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_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_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; } @@ -1260,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}. @@ -1300,40 +1138,25 @@ public Set getAllApplicationChildAndGrandchildRefactorings /** * 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()); } } @@ -1343,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()) { @@ -1373,9 +1182,8 @@ 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); + newSubs[i] = + refactorLabelsRecursive(context, sub, allChildAndGrandchildRefactorings); if (!newSubs[i].equalsIncludingLabels(sub)) { changed = true; } @@ -1391,38 +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) { + 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 = 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; @@ -1432,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); + refactorLabelsRecursive(context, (JTerm) sfa.formula(), activeRefactorings); if (!((JTerm) sfa.formula()).equalsIncludingLabels(updatedTerm)) { - goal.changeFormula(new SequentFormula(updatedTerm), + context.goal().changeFormula(new SequentFormula(updatedTerm), new PosInOccurrence(sfa, PosInTerm.getTopLevel(), inAntec)); } } @@ -1470,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); + 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; } @@ -1512,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()); 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 419bdcedb10..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,7 +8,6 @@ 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; @@ -17,7 +16,7 @@ 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; @@ -25,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; @@ -44,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; @@ -59,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); } @@ -87,12 +83,12 @@ 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(); + 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); @@ -106,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); } 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/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 8b390f2f471..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; /** @@ -42,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 49f3abf8167..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. 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 ab9da0ecfce..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,25 +5,16 @@ 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 @@ -42,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/test/java/de/uka/ilkd/key/logic/TestTermLabelManager.java b/key.core/src/test/java/de/uka/ilkd/key/logic/TestTermLabelManager.java index c6a352440d4..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.*; @@ -28,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; @@ -497,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()) { @@ -542,11 +536,7 @@ 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); } @@ -556,11 +546,8 @@ 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; } From ae60f0a070079173df1e95f92bd8ecd7451133e2 Mon Sep 17 00:00:00 2001 From: Richard Bubel Date: Fri, 3 Jul 2026 14:45:27 +0200 Subject: [PATCH 14/14] Avoid rebuilding an identical term per node in SyntacticalReplaceVisitor In the unchanged branch of the visitor the term handed to the label manager is structurally identical to the visited term (same operator, subterms, bound variables and labels). It was nevertheless rebuilt via TermFactory.createTerm for every visited node, only to be discarded when the node turned out to keep its labels. Pass the visited term directly instead, via a new instantiateLabels(tacletTerm, newTerm) overload; the reconstructing overload stays for the changed branch. Removes one term construction (and, since labeled terms are interned, one StrictTermKey allocation and cache lookup) per unchanged node. Behaviour-preserving: the 17-proof label-equivalence dump stays byte-identical. Co-Authored-By: Claude Opus 4.8 --- .../ilkd/key/rule/SyntacticalReplaceVisitor.java | 14 ++++++++++---- 1 file changed, 10 insertions(+), 4 deletions(-) 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();