Matcher Follow-Up: Remove monolithic matcher for Java programs (compiler) + move more matching logic to ncore#3922
Merged
Merged
Conversation
unp1
added
Prover Core
🛠 Maintenance
wadoon
approved these changes
Jul 14, 2026
Rename key.ncore.compiler -> key.ncore.matcher and move the interpreter VM framework (org.key_project.prover.rules.matcher.vm) into it from key.ncore.calculus. The two halves of the match-plan framework now live in one module: the single-source compiler (matcher.compiler) and the interpreter back-end it derives (matcher.vm). Package FQNs are unchanged, so this is a pure module-location move: no source edits in the key.core realizations, only the module name in settings.gradle and key.core's dependency. The dependency direction is preserved (key.core -> key.ncore.matcher -> key.ncore.calculus -> key.ncore); nothing in the ncore modules points back at core, so the framework stays reusable by other provers. Created with AI tooling support
…sion
For a schema-variable pattern carrying bound variables, the interpreter
emission added one gotoNextSibling per bound variable AFTER the
schema-variable match had already advanced past the whole term. The
schema-variable instruction matches at the term node and never descends,
so those skips move the cursor at the sibling level -- past elements
that do not belong to the pattern. (In OperatorPlan the same skips are
correct because its cursor first descends into the term's children.)
The class comment always described the correct sequence ("matchSV +
gotoNextSibling, wrapped in bind/unbind"); the code now matches it. The
defect was lifted verbatim from the pre-framework generator (see
13e8d13^), and the path is dead in practice: an instrumented load of
the standard taclet base finds no schema-variable pattern with bound
variables (bound variables attach to binder operators). The compiled
back-end (element-based, no cursor) was already consistent.
Created with AI tooling support
…afe flag Consistency pass over the term-side match-plan framework and its Java-DL front-end, aligning them with the (reified) program side: * toString on the term plan nodes and heads (OperatorPlan, SchemaVarPlan, GenericOperatorHead, ModalityHead, ParametricFunctionHead, ElementaryUpdateHead, MatchSchemaVariableInstruction), so a find pattern's whole plan tree renders for debugging, like the program plans already do. * MatchPlan.emitInstructions renamed to emit -- one name for the interpreter emission across MatchPlan, MatchHead and ProgramMatchPlan. * The key.matcher.programInstructions property moves from the legacy SyntaxElementMatchProgramGenerator to JavaMatchPlanBuilder (its only reader): the framework no longer references a class slated for deletion. * MatchPlan.compile() documents the called-once contract; a comment in OperatorPlan.emit explains why the bound-variable skips are correct there (the cursor descended into the term first). * Javadoc line-wrap artifacts (orphan words) smoothed in the framework and front-end docs. No behavioural change. Created with AI tooling support
Comment-only. Class docs added for the instructions that had none (program SV, variable SV, modal-operator SV, generic sort, parametric-function similarity, bind/unbind, schema-variable base) and sharpened where they were one-liners (term labels, instruction-set factory); javadoc wrap artifacts smoothed in the sub-program and context-block instructions. Created with AI tooling support
A schema-variable pattern never carries bound variables: bound variables attach to binder operators (matched by OperatorPlan), and an instrumented load of the standard taclet base confirms no schema-variable pattern with bound variables exists. Remove the bind/unbind scaffolding from SchemaVarPlan (its constructor now takes only the schema-variable instruction) and let JavaMatchPlanBuilder treat the shape as unsupported -- it falls back with the framework's clear "no head for this find pattern" error instead of silently matching through untested code. Deliberately a single, isolated commit: reverting it restores the corrected implementation from the previous fix commit, should the shape ever become constructible. Created with AI tooling support
The program half of the single-source match framework becomes generic, mirroring the term half that already lives here: a language front-end describes each program construct once as a ProgramMatchPlan, and both matcher back-ends are derived from it. New in org.key_project.prover.rules.matcher.compiler: * ProgramMatchPlan -- the plan interface (emit / compile / listSV / interpretable); * ProgramLeafPlan -- an element matched by a single front-end-supplied instruction, shared by both back-ends; * ProgramStructuralPlan -- the default structural match: same concrete class as the pattern, an optional language-supplied guard, children matched recursively (fixed arity directly, variable arity through a cursor walk); * ProgramListSVPlan -- a list schema variable, driven by its enclosing plan; * ProgramChildSequence -- the mixed fixed/list child walk, owning the greedy list-SV run; * ProgramChildCursor -- the positional child cursor over SyntaxElement (the language-agnostic counterpart of the per-language SourceData classes); * ListSVMatcher -- the language SPI for list schema variables (element admissibility and typed recording of the matched run), alongside the existing BinderMatcher and ProgramMatchHook axes. MatchProgramElementInstruction (exact class + child count) moves to the generic instruction package -- it reads only SyntaxElement. The package description now covers both symmetric halves and lists exactly what a language front-end supplies -- a dispatch, its schema variable instructions, and the three SPIs plus per-operator heads -- versus what the framework shares: the plugging-in guide for prover front-ends. The module still depends on nothing above key.ncore.calculus. The Java front-end switches to this framework in the follow-up commit. Created with AI tooling support
JavaProgramMatchPlanBuilder describes every Java construct of a find
pattern's program once, as a ProgramMatchPlan from the generic
framework, and both matcher back-ends are derived from that single
description. The dispatch covers: fixed-arity structural elements,
value leaves (literals, empty statements), schema type references,
dimension-guarded type references and variable specifications,
schematic field references, concrete program variables and methods,
variable-arity list schema variables, and context statement blocks
(the ubiquitous {@code .. ...} pattern) -- including the
variable-length prefix descent, the inner execution context
({@code .#ex..} / {@code .#pm@#t(#v)..}, matched by ordinary
sub-plans), the active statements, and the recorded prefix/suffix
positions. The compiled back-end reads only the structure of pattern
and source; it calls no AST {@code match(SourceData, MatchConditions)}
method at all (SourceData remains the cursor of the interpreter's AST
matchers only).
The Java-DL judgements plug into the framework's SPIs: the new
JavaListSVMatcher singleton supplies the two list-SV judgements
(admissibility via ProgramSVSort.canStandFor in the recorded execution
context; runs stored as ImmutableArray<ProgramElement>,
agree-or-record). The Java-only field-reference and context-block
nodes remain in the front-end, composing the generic child walk.
The legacy compiled program matcher (JavaProgramCompiler) is deleted.
A program the dispatch does not describe fails at taclet-load time
with the framework's "no head for this find pattern" error -- the same
contract the term side has -- instead of silently matching through the
AST; an instrumented load of the standard taclet base and the full
RunAllProofs corpus hit zero such fallbacks before the net was
removed. The interpreter back-end is untouched and remains the
reference implementation: its converted-instruction mode now asks the
dispatch per element first (one description for both back-ends), and
the monolithic MatchProgramInstruction stays as its safety net, newly
documented in that role, together with a rework of the context-match
documentation on ContextStatementBlock for readers new to it.
The equivalence of plan-based and AST program matching was validated
with a differential oracle running both matchers side by side over the
full RunAllProofs corpus: 53,419,581 match datapoints, 0 mismatches.
TestMatchTaclet gains cases for list schema variables and
variable-arity context blocks.
Created with AI tooling support
A schema variable that is already bound matches a program element again only if the element IS its binding -- the bound program element itself, or, for a term binding, the term's operator. MatchProgramSVInstruction accepted more: it converted the candidate to a term and compared the terms, so a schema variable bound to a literal term could re-match the corresponding literal program element where ProgramSV.match (the AST matcher, used by the interpreter back-end) rejects it. Rule applications driven by proof scripts pre-bind schema variables and can reach this difference; ordinary find-matching over the whole RAP corpus cannot (validated unchanged either way). Both matcher back-ends and the AST matcher now agree on the rule. Created with AI tooling support
The term half of the match framework gains the same division of labour
the program half already has: the language-independent walk lives in
key.ncore.matcher, the language supplies only its own decisions.
* MatchPlanBuilder -- the abstract skeleton of a term-side dispatch: it
recurses over a find pattern (operator, subterms, bound variables),
composes SchemaVarPlan / OperatorPlan nodes, and owns the
fail-at-load contract ("no head for this find pattern"). A front-end
subclass supplies the schema-variable instructions, the per-operator
head dispatch, its BinderMatcher, and an optional plan wrap for
language-specific in-place checks (term labels in Java-DL).
* ModalityHead moves here and becomes language-agnostic: the modal
kind and the program are the modality operator's two syntax children
(Modality.kind() / Modality.programBlock() -- an abstraction all
provers' modalities share), so the head needs only a
front-end-supplied kind instruction and the ProgramMatchHook. The
Java dispatch constructs it directly; the compiled program entry
reads the operator's programBlock(), the same object
JTerm.javaBlock() returns for a modality term.
* MatchByEqualsInstruction (value-carrying leaves by equals) moves to
the generic instruction package beside MatchIdentityInstruction --
it reads only SyntaxElement.
The Java front-end still carries its own copy of the term recursion;
it switches to the skeleton in the follow-up commit.
Created with AI tooling support
JavaMatchPlanBuilder now extends the framework's MatchPlanBuilder and supplies only the Java-DL decisions: the schema-variable instruction factory, the per-operator head dispatch (elementary update, parametric function instance, modality, generic default), the JavaBinderMatcher, and the term-label wrap (labels stay a Java-DL concern; the framework only offers the wrap hook). The recursion over the pattern, the derivation of interpreter program and compiled matcher, and the fail-at-load error are inherited. Two shared dispatch instances carry the one piece of front-end state, the key.matcher.programInstructions flag; the static facades keep their signatures, so callers are unchanged. Created with AI tooling support
Comment-only. The framework and front-end docs describe the current state of each class in its own terms: what a node matches, what each back-end does, and what a front-end supplies. References that compared a class to the matcher fragments it was derived from, lifecycle remarks, and mentions of individual prover front-ends are gone -- the framework is not specific to any set of provers. Domain notions (schema variable, elementary update, parametric function instance) are glossed where a class doc first uses them. Created with AI tooling support
…r operation BinderMatcher exposes each binding operation once: binder(boundVars) (element-based, applied by both back-ends as it is) and unbind(mc, boundVars) (a pure state transformation). The interpreter form of unbind is derived by the framework -- OperatorPlan wraps the call into a cursor-neutral instruction -- instead of being a second SPI method, so the back-end split lives in the framework, not in the front-end contract. unbind receives the bound variables because closing a scope is not scope-structured in every binding representation: a front-end that keeps a counted stack of the variables bound along the current path (for example for de-Bruijn-indexed terms) pops exactly boundVars.size() entries and needs the count, while Java-DL's nested renaming table pops one scope and ignores the argument. The Java-DL UnbindVariablesInstruction and its factory method (whose parameter was unused) are deleted; the framework's wrapper performs the same MatchConditions.shrinkRenameTable() at the same point in the instruction stream. Created with AI tooling support
Comment-only. Each class doc that speaks of an SPI expands the
abbreviation at its first use ("SPI (service provider interface)");
passing mentions name the interface instead. The Java program-match
hook's doc names the SPI it implements, like the other two Java-DL
SPI implementations.
Created with AI tooling support
A pre-compiled child of a ProgramChildSequence is either a list schema variable or a fixed child's matcher. This alternative is now a sealed interface with one record per kind, instead of a record with two nullable fields whose either-or invariant lived only in a comment -- the nullness checker verifies the dereferences now, and a violation of the fixed-arity contract of matchOneToOneFrom fails as a cast error instead of a null dereference. Created with AI tooling support
VMProgramInterpreter.match and matchChildrenFrom returned the borrowed PoolSyntaxElementCursor to the pool after the match loop, but not on the exception path -- an instruction throwing mid-match abandoned the cursor (the pool then allocates a fresh one, so this is resource hygiene, not a correctness bug). The release now runs in a finally. Created with AI tooling support
TestMatchTaclet gains a case for a find pattern whose modality program
is a plain statement block without the .. ... context markers and with
a fixed (non-list) statement: \find(\<{ #slhs1 = #e; }\>post) matched
against \<{ i = 1; }\>true. Such a program is matched structurally as
a whole (exact class and child count per element); the existing
non-context cases all used list schema variables or empty blocks, so
this shape had no direct test.
Created with AI tooling support
…ies on A concrete generic argument of a parametric function instance is matched by reference identity on its GenericArgument. That is complete because ParametricFunctionInstance.get interns instances by value: a source operator with the same base and concrete arguments is the same object as the pattern's and therefore shares its argument objects. A comment states this at the match site, and ParametricFunctionInterningTest pins the interning contract (equal requests return one shared instance, arguments included) plus its matcher-level consequence (an independently built equal instance matches) -- so weakening the interner fails these tests instead of making the matcher silently reject taclet applications. (A pattern mixing a generic sort with a concrete argument in one instance would not share its concrete argument objects with a source; no multi-parameter parametric function exists in the shipped base, so identity is kept for its cheapness on the hot matching path.) Created with AI tooling support
Remove the separate key.matcher.interpreterAssumes property, which forced the interpreter for a taclet's \assumes formulas independently of its find pattern. The remaining key.matcher.interpreter property (and its GUI feature flag) is now the single switch: it selects the back-end for all of a taclet's matching, find and \assumes together. The \assumes formulas follow the find's back-end unconditionally. Behaviour is unchanged with the property off (the default): assumes already followed the find back-end then. Only the ability to diverge the two, a headless A/B knob, is dropped. Created with AI tooling support
Which taclet matcher runs (compiled or interpreter) is a core setting, not an optional extension, so it should not be a FeatureSettings feature: features are meant for extensions and are all switched on at once by --experimental, which would silently force the interpreter. Drop INTERPRETER_MATCHER_FEATURE and its GUI registration anchor in SettingsManager; the key.matcher.interpreter system property is the sole switch. Default behaviour is unchanged (the property is off by default, as the feature was); the only change is that --experimental no longer swaps the matcher back-end. Created with AI tooling support
…matcher The lint against shared mutable static state on the proving path walked the classes of key.core only. Every taclet match runs through the match framework, which this branch moves to key.ncore.matcher, so that code left the guard's scope: a shared HashMap added there would not have been reported. Scan the matcher module's packages too. A module reaches the test classpath either as its classes directory (the module the test lives in) or as its jar (a module dependency), so class names are now read from both layouts. A scanned package that yields no classes fails the test instead of being skipped silently -- that is what let the scope go stale unnoticed in the first place, and it mirrors the existing check for stale allowlist entries. Verified by injecting a static HashMap into a key.ncore.matcher class: the lint fails, and passes again once removed. Created with AI tooling support
unp1
force-pushed
the
bubel/program-matcher-single-source
branch
from
July 15, 2026 07:56
54b82d3 to
145e353
Compare
Comment-only. Em-dashes are replaced by plain punctuation throughout the matcher's javadoc. The entry points introduce the domain notions they use: the package description and the plan/builder docs say what a taclet, a find pattern and a schema variable are before relying on them. The class documentation of VMTacletMatcher describes what the class is (the matcher of one taclet: find and assumes matchers built through the match-plan framework, back-end chosen by the property, results threaded through immutable match conditions) instead of the approach it was inspired by, and VMProgramInterpreter's description is reduced to its contract. Created with AI tooling support
MatchGenericSortInstruction.matchSorts declared a result variable it never used, next to a commented-out assertion referring to a variable name that no longer exists. The information the assertion carried (the source sort may itself be generic, because proving a taclet correct matches schematic patterns against schematic terms) is now a comment. Created with AI tooling support
…h, dead fallback Findings of a correctness and thread-safety audit of the matching code (both back-ends; no thread-safety findings): * A modal-operator schema variable that was already instantiated silently took a new modality kind on a second match, because SVInstantiations.add overwrites without warning and the instruction had no instantiate-or-agree step (every other schema-variable instruction has one). It now matches an instantiated variable only against the same kind again. No taclet in the shipped base matches one modal-operator variable twice, so the rule base is unaffected. * VMTacletMatcher.matchSV routed every candidate through the term-typed overload, so a program-element candidate handed to a term-kind schema variable failed with a ClassCastException instead of a failed match. Program elements now dispatch to the program-element overload, whose base implementation rejects the match for schema-variable kinds that stand for terms. * matchAssumes rejects a template that is not one of the taclet's assumes formulas with a clear IllegalArgumentException instead of a NullPointerException. * The compiled-or-interpreter fallback in matchProgramFor and the compiledProgramOrNull facades are removed: both back-ends derive from the same match plan, so the fallback could only ever rebuild the same failure and the branch was dead. Unsupported patterns fail at taclet-load time on either back-end, as documented. Created with AI tooling support
A schema-variable match candidate is either a term or a program element (an update's left-hand side, for example, is a program variable). Previously the generic match(SyntaxElement) overload of each schema-variable instruction meant "match a term" and cast accordingly, program elements had a separate overload, and the program schema variable hand-rolled the type split; VMTacletMatcher.matchSV had to repeat that split at the call site. The base class now routes each candidate once: its final match(SyntaxElement) dispatches to an abstract match(JTerm) and to match(ProgramElement), whose default rejects (only the program schema variable overrides it). Subclasses implement typed methods without casts, and matchSV is back to a single uniform call. Created with AI tooling support
unp1
enabled auto-merge
July 16, 2026 07:06
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.
Intended Change
The previous introduction of the matcher based on "compilation" (partial evaluation) used a monolithic program matcher with fall-backs to the matching code in the AST classes. This PR breaks the monolithic matcher in single instructions and removes any dependency on AST internal matching methods.
Advantages:
These changes make the compiler adaption easier for other provers like RustyKeY and SolidiKeY
In addition JavaDoc comments were partially reworded to make them easier to read. In particular wording referring to the development process of the PR have been removed. They are now more focused on describing the "is" state than on how the "is" state was achieved.
Changes in
key.ncore.matcherThe generic machinery lives in
key.ncore.matcher, renamed fromkey.ncore.compilerby a pure move that leaves the package names unchanged (the ncore modules still do not depend onkey.core). This PR adds the program half of the framework, mirroring the term-side plans already present:ProgramMatchPlannodes (ProgramLeafPlan,ProgramStructuralPlan,ProgramListSVPlan) for the program inside a modality, andProgramChildSequencefor the fixed- and variable-arity walk over a node's children via a generic positional cursor. The calculus-specific parts stay behind two small SPIs:ProgramMatchHookfor entering a modality's program andListSVMatcherfor list schema variables.Changes in
key.coreJavaProgramMatchPlanBuilderdescribes each Java program construct once, from plain statements and value literals to schematic field references and the.. ...context statement blocks of symbolic-execution taclets. The compiled back-end then matches purely from the structure of pattern and source, calling no ASTmatch(SourceData, MatchConditions)method, so the monolithicJavaProgramCompileris removed. A construct the dispatch does not describe fails at taclet-load time with a clear error (the same behaviour the term side already has) instead of silently matching through the AST; no construct in the current taclet base reaches this. The interpreter back-end is left as is and serves as the reference against which the compiled matcher is validated.Type of pull request
Ensuring quality
key.coretest suite greenModality.programBlock(), the same objectJTerm.javaBlock()returns for a modality term; the binder rework routes unbinding through the framework wrapper at the same point in the instruction stream. Both re-validated by the oracle run above.Additional information and contact(s)
Created with AI tooling support
The contributions within this pull request are licensed under GPLv2 (only) for inclusion in KeY.