Term label cleanup: simpler framework, label-agnostic term equality#3884
Draft
unp1 wants to merge 14 commits into
Draft
Term label cleanup: simpler framework, label-agnostic term equality#3884unp1 wants to merge 14 commits into
unp1 wants to merge 14 commits into
Conversation
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
…ct 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
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
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
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
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
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
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
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
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 <noreply@anthropic.com>
…n 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 <noreply@anthropic.com>
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 <noreply@anthropic.com>
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<TermLabel>) 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 <noreply@anthropic.com>
unp1
added
🛠 Maintenance
unp1
added a commit
to KeYProject/key-docs
that referenced
this pull request
Jul 3, 2026
Flag both term-label pages as documenting an as-yet-unmerged pull request whose details may change during review.
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 <noreply@anthropic.com>
flo2702
reviewed
Jul 6, 2026
| * This is the middle one of the three label comparison modes: plain | ||
| * {@link de.uka.ilkd.key.logic.JTerm#equals(Object)} ignores <em>all</em> 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 |
Member
There was a problem hiding this comment.
There's also a TermLabelsProperty which is only used in test code and seems to be redundant with JTerm.equalsIncludingLabels. Should that be removed?
| * @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); |
Member
There was a problem hiding this comment.
Probably, the documentation here should reference IrrelevantTermLabelProperty, so people don't get confused and use one when they really want the other.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
In one paragraph: the term-label subsystem carried a lot of generality that was designed up-front but never actually used, and its central design choice, term
equals/hashCodebeing label-sensitive, forced a comparison-modulo-labels idiom to spread across the code base. This PR removes the unused machinery, flips term equality to ignore labels by default (the common and now-uniform case), restores the few places that genuinely need label-sensitive comparison via a small explicit apparatus, and simplifiesTermLabelManagerand the hook API. Proofs are unaffected: replaying a 17-proof corpus yields byte-identical sequents including every term label, and the information-flow and well-definedness proof suites match stockmaster.Main changes and intentions
Remove speculative-but-unused features. Several extension points were anticipated but never materialized in any profile:
ChildTermLabelPolicyhook family (direct + child/grandchild) — registered by nobody;APPLICATION_DIRECT_CHILDRENrefactoring scope — returned by no refactoring;LabeledTermImplsubclass — folded intoTermImpl.Change the semantics of term equality:
equals/hashCodenow ignore all term labels. Term labels are, by contract, not soundness relevant, and sequent redundancy elimination already ignored them — so the default now agrees with the calculus' own notion of "same formula". The two label-sensitive needs that remain are served explicitly:IRRELEVANT_TERM_LABELS_PROPERTY(ignore only cosmetic labels, keep proof-relevant ones) andequalsIncludingLabels/labeledHashCode(respect all labels, used only by term interning / index caches). Rationale and the full pro/contra discussion are in the table below.Simplify
TermLabelManagerand the hook API.TermLabelManagershrinks from 2211 to 1629 lines. The hooks (TermLabelPolicy/Update/Refactoring) no longer thread an 8-parameter rule-application tuple through every signature and every internal delegation; a single immutableTermLabelContextrecord carries it.Net: 40 files, +1015 / −1691 (−676 lines), Java only, no taclet changes.
Related Issue
Addresses the two long-standing complaints about the term-label implementation: the
framework being too general/partly inefficient, and the proliferation of
equalsModIrrelevantTermLabelscomparisons.Intended Change
(A) Prune unused generality
ChildTermLabelPolicy(and its direct / child-and-grandchild variants) is deleted together with its dispatch inTermLabelManager. NoTermLabelConfigurationin any profile ever registered one.RefactoringScope.APPLICATION_DIRECT_CHILDRENand itsRefactoringsContainerbucket / dispatch are deleted; no live refactoring returns that scope.LabeledTermImplis merged intoTermImpl. With labels no longer part of term identity, the subclass existed only to keep alabelsfield off unlabeled terms; a single nullable field (empty normalized to a shared array) replaces it, removing the two-class hierarchy and the "same value, different class, still equal" hazard.(B) Term equality ignores labels
TermImpl.equals/hashCodenow ignore all term labels. Three comparison modes now coexist, cleanly separated by who owns the knowledge:t1.equals(t2)/hashCodeequalsModProperty(t, IRRELEVANT_TERM_LABELS_PROPERTY)isProofRelevant()anonHeapFunction-labeled term distinct while ignoring origin labelsequalsIncludingLabels+labeledHashCodeStrictTermKey)Supporting apparatus (all label-opaque, hence on
TermImpl, not leaking label kinds): -equalsIncludingLabels(Object)and cachedlabeledHashCode()— the label-sensitive counterparts ofequals/hashCode.labeledHashCodeis cached on the term becausehashCodeModPropertyis not and the term factory cache queries it per construction. -StrictTermKey— a label-sensitive map key. TheTermFactoryintern cache and the taclet-app indexCacheKeyuse it, so labeled terms are still interned exactly as before (memory sharing and==fast paths preserved), even thoughequalsignores labels. Taclet matching can depend on labels, so the index must stay label-sensitive. - A cachedcontainsLabelsRecursive()guard so label-free subtrees are skipped in O(1).The four
TERM_LABELS_PROPERTYcomparison sites (which meant "ignore all labels") are now plainequals; that property is no longer used in application code.(C) API simplification
TermLabelContext: an immutable record bundling the rule application (state, services, applicationPosInOccurrence, applicationTerm, modalityTerm, rule, ruleApp, goal, hint, tacletTerm), built once perTermLabelManagerentry point. Hooks now take(context, payload…):keepLabelwent 10→3 params,updateLabels11→3,defineRefactoringScope8→1,refactorLabels10→3. 26 manager methods that re-threaded the tuple collapse to one-argument delegation.TermLabelMergeris unchanged (its parameters are genuine payload). The static entry points keep their signatures, so rule implementations are untouched.Why "ignore all" and not "keep the old label-sensitive equals": pro / contra
The decision (which default
equalsshould have) was deliberate. Both candidates are label-opaque (neither leaks specific label knowledge intoTerm).equalsincludes all labels (old)equalsignores all labels (this PR)equalsdoes not (the "rejected as duplicate yet not equal to any member" trap)equals/map breaks once origin labels are enabled (the historical bug pattern)equalsIncludingLabels+ cachedlabeledHashCode+StrictTermKey(small, and interning is preserved)equalsmarginally faster on labeled termsThe deciding factor is that the proliferation of comparison-modulo-labels only has an exit under "ignore all": under the old default, plain equality is unusable the moment origin labels are on, so the weakening idiom is structurally forced everywhere. Under this PR the weakening residue is the ~51
IRRELEVANT_TERM_LABELS_PROPERTYsites that genuinely need the middle mode (a per-site review confirmed each: emptiness/constant classification in the loop/contract rules and WD, instantiation identity inSVInstantiations/RuleCommand, and a few non-soundness strategy heuristics).Plan
Finished at submission time.
ChildTermLabelPolicyhook familyequalsIncludingLabelsLabeledTermImplintoTermImplStrictTermKey)TestLinkedHashMapWrapperfor label-agnostic equalitylabelsEqualRecursiveon reference-identical subterms (perf)TermImpllazy tri-state caches into a single int (−12 bytes/term)TERM_LABELS_PROPERTYcomparisons to plainequalsAPPLICATION_DIRECT_CHILDRENrefactoring scopeTermLabelContextparameter objectType of pull request
equals/hashCodesemantics of terms, and theTermLabelPolicy/Update/Refactoringhook signatures — relevant only to code implementing those hooks or relying on label-sensitive term equality)Ensuring quality
TermLabel, the hook interfaces, andTermLabelManager.TermLabelEquivalenceDumpTest) that replays console proofs and dumps every node's sequent including all labels; plus label-interning and equality-contract unit tests.:key.core:test,:key.core.infflow:testRunAllInfProofs, and:key.core.wd:testRunAllWdProofsare green and match stockmaster.mastershows parity on the cached-construction hot path (the production path); labeled-termequalsis marginally faster. The flag packing saves ~12 bytes per term object.Additional information
@flo2702 thanks a lot for offering to look into this PR
Map/SetonJTermexpecting label sensitivity; such code should wrap keys inStrictTermKey. The (deprecated)key.core.symbolic_executionandkey.core.proof_referencesmodules were left untouched and pass their proof suites.TermLabelsProperty(mode "ignore all") is now equivalent to plainequalsand unused in application code; it is retained only for tests and can be removed in a follow-up.The contributions within this pull request are licensed under GPLv2 (only) for inclusion in KeY.