Skip to content

Term label cleanup: simpler framework, label-agnostic term equality #3884

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Draft
unp1 wants to merge 14 commits into
base: main
Choose a base branch
from
Draft

Term label cleanup: simpler framework, label-agnostic term equality #3884

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
14 commits
Select commit Hold shift + click to select a range
e7f67fa
Remove unused ChildTermLabelPolicy hook family from term label framework
unp1 Jul 3, 2026
d633afd
Make term equality label-agnostic; add equalsIncludingLabels for stri…
unp1 Jul 3, 2026
2064746
Add term-label equivalence regression harness
unp1 Jul 3, 2026
79f4df1
Merge LabeledTermImpl into TermImpl
unp1 Jul 3, 2026
d3760d0
Intern labeled terms via a label-sensitive cache key
unp1 Jul 3, 2026
5342cca
Update TestLinkedHashMapWrapper for label-agnostic term equality
unp1 Jul 3, 2026
486fbb9
Short-circuit labelsEqualRecursive on reference-identical subterms
unp1 Jul 3, 2026
6ef2269
Pack TermImpl lazy tri-state caches into a single int
unp1 Jul 3, 2026
e33df51
Collapse TERM_LABELS_PROPERTY comparisons to plain term equality
unp1 Jul 3, 2026
1e7c951
Remove unused APPLICATION_DIRECT_CHILDREN refactoring scope
unp1 Jul 3, 2026
6681f86
Correct label-coverage note: postCondition/undef/selfComposedExecutio…
unp1 Jul 3, 2026
a737088
Rewrite term-label API documentation for the reworked framework
unp1 Jul 3, 2026
e05adcb
Introduce TermLabelContext parameter object for term label hooks
unp1 Jul 3, 2026
ae60f0a
Avoid rebuilding an identical term per node in SyntacticalReplaceVisitor
unp1 Jul 3, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
21 changes: 8 additions & 13 deletions ...cution/src/main/java/de/uka/ilkd/key/rule/label/BlockContractValidityTermLabelUpdate.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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;

Expand All @@ -40,18 +36,17 @@ public ImmutableList<Name> 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<TermLabel> labels) {
if ((rule instanceof BlockContractInternalRule || rule instanceof LoopContractInternalRule)
&& ((BlockContractInternalRule.BlockContractHint) hint)
public void updateLabels(TermLabelContext context, JTerm newTerm, Set<TermLabel> 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()));
}
}
}
Expand Down
44 changes: 21 additions & 23 deletions ...bolic_execution/src/main/java/de/uka/ilkd/key/rule/label/FormulaTermLabelRefactoring.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down Expand Up @@ -112,19 +113,17 @@ public ImmutableList<Name> 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;
Expand All @@ -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);
}
}

Expand Down
29 changes: 12 additions & 17 deletions ...e.symbolic_execution/src/main/java/de/uka/ilkd/key/rule/label/FormulaTermLabelUpdate.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand All @@ -48,33 +44,31 @@ public ImmutableList<Name> 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<TermLabel> labels) {
if (hint instanceof TacletLabelHint tacletHint) {
public void updateLabels(TermLabelContext context, JTerm newTerm, Set<TermLabel> labels) {
if (context.hint() instanceof TacletLabelHint tacletHint) {
if ((TacletOperation.ADD_ANTECEDENT.equals(tacletHint.getTacletOperation())
|| TacletOperation.ADD_SUCCEDENT.equals(tacletHint.getTacletOperation()))
&& (TruthValueTracingUtil.isPredicate(newTerm)
|| TruthValueTracingUtil.isLogicOperator(newTerm.op(),
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<SequentFormula, FormulaTermLabel> ifLabels =
new LinkedHashMap<>();
Expand All @@ -92,11 +86,12 @@ public void updateLabels(TermLabelState state, Services services,
for (Entry<SequentFormula, FormulaTermLabel> 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());
}
}
Expand Down
16 changes: 5 additions & 11 deletions ....symbolic_execution/src/main/java/de/uka/ilkd/key/rule/label/LoopBodyTermLabelUpdate.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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;

/**
Expand All @@ -37,12 +33,10 @@ public ImmutableList<Name> 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<TermLabel> labels) {
if (rule instanceof WhileInvariantRule && "LoopBodyModality".equals(hint)
&& SymbolicExecutionUtil.hasSymbolicExecutionLabel(modalityTerm)) {
public void updateLabels(TermLabelContext context, JTerm newTerm, Set<TermLabel> labels) {
if (context.rule() instanceof WhileInvariantRule
&& "LoopBodyModality".equals(context.hint())
&& SymbolicExecutionUtil.hasSymbolicExecutionLabel(context.modalityTerm())) {
labels.add(SymbolicExecutionUtil.LOOP_BODY_LABEL);
}
}
Expand Down
16 changes: 5 additions & 11 deletions .../src/main/java/de/uka/ilkd/key/rule/label/LoopInvariantNormalBehaviorTermLabelUpdate.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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;

/**
Expand All @@ -37,12 +33,10 @@ public ImmutableList<Name> 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<TermLabel> labels) {
if (rule instanceof WhileInvariantRule && "LoopBodyImplication".equals(hint)
&& SymbolicExecutionUtil.hasSymbolicExecutionLabel(modalityTerm)) {
public void updateLabels(TermLabelContext context, JTerm newTerm, Set<TermLabel> labels) {
if (context.rule() instanceof WhileInvariantRule
&& "LoopBodyImplication".equals(context.hint())
&& SymbolicExecutionUtil.hasSymbolicExecutionLabel(context.modalityTerm())) {
labels.add(SymbolicExecutionUtil.LOOP_INVARIANT_NORMAL_BEHAVIOR_LABEL);
}
}
Expand Down
21 changes: 6 additions & 15 deletions ...n/src/main/java/de/uka/ilkd/key/rule/label/RemoveInCheckBranchesTermLabelRefactoring.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand All @@ -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;

/**
Expand Down Expand Up @@ -67,13 +63,10 @@ public ImmutableList<Name> 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;
Expand All @@ -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()));
}
}
Loading
Loading