diff --git a/key.core/build.gradle b/key.core/build.gradle index 128931a290c..94de2268192 100644 --- a/key.core/build.gradle +++ b/key.core/build.gradle @@ -10,6 +10,7 @@ dependencies { api project(':key.util') api project(':key.ncore') api project(':key.ncore.calculus') + api project(':key.ncore.compiler') antlr4 "org.antlr:antlr4:4.13.2" api "org.antlr:antlr4-runtime:4.13.2" @@ -235,14 +236,21 @@ tasks.register("testRAP", Test) { dependsOn('generateRAPUnitTests', 'testClasses') forkEvery = 1 - maxParallelForks = 2 + // run the regression proofs on up to 10 parallel JVMs (overridable with -PrapForks=N); + // for clean perfTest timing reproduction use -PrapForks=1 + maxParallelForks = (project.findProperty('rapForks') ?: '10') as int useJUnitPlatform() it.filter { it.includeTestsMatching "de.uka.ilkd.key.proof.runallproofs.gen.*" } - // set heap size for the test JVM(s) + // forward the compiled-matcher switch to the (in-process) proof runs in each fork; default + // off, enable with -Pmatcher.compiled=true (or -Dkey.matcher.compiled=true) + systemProperty 'key.matcher.compiled', + (project.findProperty('matcher.compiled') + ?: System.getProperty('key.matcher.compiled', 'false')) + // set heap size for the test JVM(s) (overridable with -PrapHeap=8g for the large examples) minHeapSize = "1g" - maxHeapSize = "3g" + maxHeapSize = (project.findProperty('rapHeap') ?: '3g') // set JVM arguments for the test JVM(s) //jvmArgs('-XX:MaxPermSize=1g') diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/ast/ContextStatementBlock.java b/key.core/src/main/java/de/uka/ilkd/key/java/ast/ContextStatementBlock.java index 304e085d9f5..2b3b5c8030d 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/ast/ContextStatementBlock.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/ast/ContextStatementBlock.java @@ -16,10 +16,12 @@ import de.uka.ilkd.key.rule.MatchConditions; import de.uka.ilkd.key.rule.inst.SVInstantiations; -import org.key_project.logic.IntIterator; +import org.key_project.prover.rules.matcher.vm.ProgramChildrenMatcher; import org.key_project.util.collection.ImmutableArray; import org.key_project.util.collection.ImmutableSLList; +import org.jspecify.annotations.Nullable; + /** * In the DL-formulae description of Taclets the program part can have the following form * {@code < pi @@ -130,6 +132,28 @@ public boolean compatibleBlockSize(int pos, int max) { } public MatchConditions match(SourceData source, MatchConditions matchCond) { + return match(source, matchCond, null); + } + + /** + * Matches this context block against the given source. Phases (1) prefix descent to the active + * statement, (2) inner execution context matching and (4) completion of the context + * instantiation (prefix/suffix positions) are always performed here. Phase (3), the matching of + * the active statements (this block's children from the active offset), is delegated to the + * supplied {@code activeStatements} matcher when one is given (and the located source position + * is a regular child offset); otherwise the built-in {@link #matchChildren} is used. All three + * yield identical results; the {@code activeStatements} matcher (a VM sub-program or a compiled + * matcher) simply matches the active-statement subtree by direct navigation instead of the + * monolithic AST matcher. + * + * @param source the source to match against + * @param matchCond the match conditions found so far + * @param activeStatements a matcher for the active statements, or {@code null} to use the + * built-in {@link #matchChildren} for phase (3) + * @return the resulting match conditions, or {@code null} if matching fails + */ + public MatchConditions match(SourceData source, MatchConditions matchCond, + @Nullable ProgramChildrenMatcher activeStatements) { assert getPrefixLength() > 0; SourceData newSource = source; @@ -192,8 +216,13 @@ public MatchConditions match(SourceData source, MatchConditions matchCond) { return null; } - // matching children - matchCond = matchChildren(newSource, matchCond, executionContext == null ? 0 : 1); + // matching children (the active statements) -- phase (3) + final int offset = executionContext == null ? 0 : 1; + if (activeStatements != null && newSource.getChildPos() >= 0) { + matchCond = matchActiveStatements(newSource, matchCond, activeStatements, offset); + } else { + matchCond = matchChildren(newSource, matchCond, offset); + } if (matchCond == null) { return null; @@ -205,6 +234,37 @@ public MatchConditions match(SourceData source, MatchConditions matchCond) { return matchCond; } + /** + * Phase (3) via a supplied matcher (VM sub-program or compiled): matches the active statements + * of this context block (its children from index {@code offset}) against the children of + * {@code newSource.getElement()} starting at {@code newSource.getChildPos()}. This mirrors + * {@link #matchChildren(SourceData, MatchConditions, int)} for the case where every active + * statement consumes exactly one source child (the only case the generator converts -- list + * schema variables and other variable-arity constructs keep the interpreter). On success the + * source position is advanced exactly as {@code matchChildren} would, so the subsequent + * {@link #makeContextInfoComplete} computes the same suffix start. + */ + private @Nullable MatchConditions matchActiveStatements(SourceData newSource, + MatchConditions matchCond, ProgramChildrenMatcher activeStatements, int offset) { + final int startPos = newSource.getChildPos(); + // number of active statements to match (each consumes exactly one source child) + final int n = getChildCount() - offset; + final ProgramElement parent = newSource.getElement(); + if (!(parent instanceof NonTerminalProgramElement ntParent) + || ntParent.getChildCount() < startPos + n) { + // not enough source children -> matchChildren would also fail (null source child) + return null; + } + final MatchConditions result = (MatchConditions) activeStatements.matchChildrenFrom( + parent, startPos, matchCond, newSource.getServices()); + if (result == null) { + return null; + } + // advance the source position past the matched children, as matchChildren would + newSource.setChildPos(startPos + n); + return result; + } + /** * completes match of context block by adding the prefix end position and the suffix start * position @@ -295,10 +355,10 @@ private PosInProgram matchPrefixEnd(final ProgramPrefix prefix, int pos, PosInPr ProgramPrefix currentPrefix = prefix; int i = 0; while (i <= pos) { - final IntIterator it = currentPrefix.getFirstActiveChildPos().iterator(); - while (it.hasNext()) { - prefixEnd = prefixEnd.down(it.next()); - } + // concatenate this prefix element's active-child position in one step instead of + // iterating + a fresh PosInProgram per position (matchPrefixEnd is the dominant + // cost of a context match; this avoids an IntIterator and intermediate copies) + prefixEnd = prefixEnd.append(currentPrefix.getFirstActiveChildPos()); i++; if (i <= pos) { // as fail-fast measure I do not test here using 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 dc84ea2b302..834f47ef7bb 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 @@ -119,6 +119,16 @@ public interface JTerm */ boolean containsJavaBlockRecursive(); + /** + * 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 + * {@link de.uka.ilkd.key.rule.RewriteTaclet#checkPrefix} to skip the prefix walk in the common + * transformer-free case. + * + * @return {@code true} iff a transformer occurs anywhere in the term tree + */ + boolean containsTransformerRecursive(); + /** * Returns a human-readable source of this term. For example the filename with line and offset. */ 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 42063167176..505b7a872a5 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 @@ -81,6 +81,9 @@ private enum ThreeValuedTruth { */ private ThreeValuedTruth containsJavaBlockRecursive = ThreeValuedTruth.UNKNOWN; + /** caches whether this term or a (direct/indirect) child has a {@link Transformer} operator. */ + private ThreeValuedTruth containsTransformerRecursive = ThreeValuedTruth.UNKNOWN; + // ------------------------------------------------------------------------- // constructors // ------------------------------------------------------------------------- @@ -441,5 +444,24 @@ public boolean containsJavaBlockRecursive() { return containsJavaBlockRecursive == ThreeValuedTruth.TRUE; } + @Override + public boolean containsTransformerRecursive() { + if (containsTransformerRecursive == ThreeValuedTruth.UNKNOWN) { + ThreeValuedTruth result = ThreeValuedTruth.FALSE; + if (op instanceof Transformer) { + result = ThreeValuedTruth.TRUE; + } else { + for (int i = 0, arity = subs.size(); i < arity; i++) { + if (subs.get(i).containsTransformerRecursive()) { + result = ThreeValuedTruth.TRUE; + break; + } + } + } + this.containsTransformerRecursive = result; + } + return containsTransformerRecursive == ThreeValuedTruth.TRUE; + } + } 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 f08bb194f98..b04df10fb86 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 @@ -5,7 +5,6 @@ import java.util.*; import java.util.Map.Entry; -import java.util.stream.Collectors; import de.uka.ilkd.key.java.Services; import de.uka.ilkd.key.logic.*; @@ -2156,10 +2155,55 @@ public static JTerm removeIrrelevantLabels(JTerm term, Services services) { * @see TermLabel#isProofRelevant() */ public static JTerm removeIrrelevantLabels(JTerm term, TermFactory tf) { + // Identity-preserving rebuild: only allocate along paths that actually carry an irrelevant + // label, and return the original term unchanged otherwise. The previous implementation + // rebuilt the whole term tree on every call (stream().map()/filter().collect() per node), + // which was the single biggest allocator during proof search (~20%) even though the vast + // majority of subterms have no irrelevant labels and need not change. + final ImmutableArray subs = term.subs(); + final int n = subs.size(); + JTerm[] newSubs = null; // allocated lazily, only once a sub actually changes + for (int i = 0; i < n; i++) { + final JTerm oldSub = subs.get(i); + final JTerm newSub = removeIrrelevantLabels(oldSub, tf); + if (newSub != oldSub && newSubs == null) { + newSubs = new JTerm[n]; + for (int j = 0; j < i; j++) { + newSubs[j] = subs.get(j); + } + } + if (newSubs != null) { + newSubs[i] = newSub; + } + } + + final ImmutableArray labels = term.getLabels(); + ImmutableArray newLabels = labels; + if (!labels.isEmpty()) { + int relevant = 0; + for (int i = 0, sz = labels.size(); i < sz; i++) { + if (labels.get(i).isProofRelevant()) { + relevant++; + } + } + if (relevant != labels.size()) { + final TermLabel[] kept = new TermLabel[relevant]; + int k = 0; + for (int i = 0, sz = labels.size(); i < sz; i++) { + final TermLabel l = labels.get(i); + if (l.isProofRelevant()) { + kept[k++] = l; + } + } + newLabels = new ImmutableArray<>(kept); + } + } + + if (newSubs == null && newLabels == labels) { + return term; // no irrelevant label anywhere in this subtree -> no allocation + } return tf.createTerm(term.op(), - new ImmutableArray<>(term.subs().stream().map(t -> removeIrrelevantLabels(t, tf)) - .collect(Collectors.toList())), - term.boundVars(), new ImmutableArray<>(term.getLabels().stream() - .filter(TermLabel::isProofRelevant).collect(Collectors.toList()))); + newSubs == null ? subs : new ImmutableArray<>(newSubs), + term.boundVars(), newLabels); } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/nparser/ParsingFacade.java b/key.core/src/main/java/de/uka/ilkd/key/nparser/ParsingFacade.java index b86472b9215..f5249b0f4a3 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/nparser/ParsingFacade.java +++ b/key.core/src/main/java/de/uka/ilkd/key/nparser/ParsingFacade.java @@ -112,6 +112,24 @@ private static JavaKeYParser createParser(CharStream stream) { return createParser(createLexer(stream)); } + /** + * Releases the ANTLR prediction (DFA) cache of the KeY parser. + *

+ * This cache is built lazily while parsing and held on the generated parser's {@code static} + * fields, so it stays resident for the whole JVM -- including during proof search, where it is + * not needed (on a large proof it retains ~15-20 MB). It is a pure cache: ANTLR rebuilds it + * transparently on the next parse, so dropping it is correctness-safe (one-time re-warm on a + * subsequent parse). Intended to be called once a problem/proof has finished loading. + */ + public static void clearParserCaches() { + try { + new JavaKeYParser(new CommonTokenStream(createLexer(CharStreams.fromString("")))) + .getInterpreter().clearDFA(); + } catch (RuntimeException e) { + LOGGER.warn("Could not clear parser DFA caches", e); + } + } + public static JavaKeYLexer createLexer(Path file) throws IOException { return createLexer(CharStreams.fromPath(file)); } diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/Goal.java b/key.core/src/main/java/de/uka/ilkd/key/proof/Goal.java index 2e12543c5f1..e5fee125729 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/Goal.java +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/Goal.java @@ -39,6 +39,7 @@ import org.key_project.prover.sequent.Sequent; import org.key_project.prover.sequent.SequentChangeInfo; import org.key_project.prover.sequent.SequentFormula; +import org.key_project.prover.strategy.DelegationBasedRuleApplicationManager; import org.key_project.prover.strategy.RuleApplicationManager; import org.key_project.util.collection.ImmutableList; import org.key_project.util.collection.ImmutableSLList; @@ -243,6 +244,15 @@ private void fireSequentChanged(SequentChangeInfo sci) { var time1 = System.nanoTime(); PERF_UPDATE_TAG_MANAGER.getAndAdd(time1 - time); ruleAppIndex.sequentChanged(sci); + // Feed the change to the (possibly delegation-wrapped) queue manager so it can wake parked + // assumes-bases on their matching round (see QueueRuleApplicationManager#parkedByOp). + RuleApplicationManager m = ruleAppManager; + while (m instanceof DelegationBasedRuleApplicationManager d) { + m = d.getDelegate(); + } + if (m instanceof QueueRuleApplicationManager qm) { + qm.sequentChanged(sci); + } var time2 = System.nanoTime(); PERF_UPDATE_RULE_APP_INDEX.getAndAdd(time2 - time1); for (GoalListener listener : listeners) { diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/io/AbstractProblemLoader.java b/key.core/src/main/java/de/uka/ilkd/key/proof/io/AbstractProblemLoader.java index e4462551b58..9d311ee8108 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/io/AbstractProblemLoader.java +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/io/AbstractProblemLoader.java @@ -14,6 +14,7 @@ import de.uka.ilkd.key.java.Services; import de.uka.ilkd.key.nparser.JavaKeYLexer; import de.uka.ilkd.key.nparser.KeyAst.ProofScript; +import de.uka.ilkd.key.nparser.ParsingFacade; import de.uka.ilkd.key.nparser.ProofScriptEntry; import de.uka.ilkd.key.proof.Node; import de.uka.ilkd.key.proof.Proof; @@ -30,6 +31,7 @@ import de.uka.ilkd.key.settings.ProofIndependentSettings; import de.uka.ilkd.key.speclang.Contract; import de.uka.ilkd.key.speclang.SLEnvInput; +import de.uka.ilkd.key.speclang.njml.JmlFacade; import de.uka.ilkd.key.strategy.Strategy; import de.uka.ilkd.key.strategy.StrategyProperties; @@ -339,6 +341,11 @@ public final void load(Consumer callbackProofLoaded) throws Exception { } } finally { control.loadingFinished(this, poContainer, proofList, result); + // parsing is done; release the ANTLR DFA caches so they are not retained during the + // (long) proof search. They are a pure cache and rebuild transparently on the next + // parse. + ParsingFacade.clearParserCaches(); + JmlFacade.clearCaches(); } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/RewriteTaclet.java b/key.core/src/main/java/de/uka/ilkd/key/rule/RewriteTaclet.java index 95de43b22f2..7d1cd26f955 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/RewriteTaclet.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/RewriteTaclet.java @@ -37,6 +37,7 @@ * structure described by the term of the find-part. */ public class RewriteTaclet extends FindTaclet { + /** * creates a Schematic Theory Specific Rule (Taclet) with the given parameters that represents a * rewrite rule. @@ -108,6 +109,13 @@ private boolean veto(JTerm t) { public MatchConditions checkPrefix( PosInOccurrence p_pos, MatchConditions p_mc) { + // Fast path: for an unrestricted taclet the loop below only vetoes on a Transformer on the + // path; if the formula has none at all (cached), neither can the prefix, so the O(depth) + // walk is skipped. + if (applicationRestriction().equals(ApplicationRestriction.NONE) + && !((JTerm) p_pos.sequentFormula().formula()).containsTransformerRecursive()) { + return p_mc; + } int polarity = p_pos.isInAntec() ? -1 : 1; // init polarity SVInstantiations svi = p_mc.getInstantiations(); // this is assumed to hold diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/executor/javadl/RewriteTacletExecutor.java b/key.core/src/main/java/de/uka/ilkd/key/rule/executor/javadl/RewriteTacletExecutor.java index 9f5ffd143d1..76a204ec8aa 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/executor/javadl/RewriteTacletExecutor.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/executor/javadl/RewriteTacletExecutor.java @@ -15,7 +15,7 @@ import de.uka.ilkd.key.rule.TacletApp; import de.uka.ilkd.key.rule.tacletbuilder.RewriteTacletGoalTemplate; -import org.key_project.logic.IntIterator; +import org.key_project.logic.PosInTerm; import org.key_project.logic.sort.Sort; import org.key_project.prover.rules.ApplicationRestriction; import org.key_project.prover.rules.instantiation.MatchResultInfo; @@ -36,18 +36,20 @@ public RewriteTacletExecutor(RewriteTaclet taclet) { */ private JTerm replace(JTerm term, JTerm with, TermLabelState termLabelState, TacletLabelHint labelHint, PosInOccurrence posOfFind, - IntIterator it, + PosInTerm pit, int depthIdx, MatchResultInfo mc, Sort maxSort, Goal goal, Services services, TacletApp ruleApp) { - if (it.hasNext()) { - final int indexOfNextSubTerm = it.next(); + // walk the find-position by index instead of via PosInTerm.iterator(), to avoid allocating + // a PiTIterator per rule application (same indices/order as the forward iterator). + if (depthIdx < pit.depth()) { + final int indexOfNextSubTerm = pit.getIndexAt(depthIdx); final JTerm[] subs = new JTerm[term.arity()]; term.subs().arraycopy(0, subs, 0, term.arity()); final Sort newMaxSort = TermHelper.getMaxSort(term, indexOfNextSubTerm); subs[indexOfNextSubTerm] = replace(term.sub(indexOfNextSubTerm), with, termLabelState, - labelHint, posOfFind, it, mc, newMaxSort, goal, services, ruleApp); + labelHint, posOfFind, pit, depthIdx + 1, mc, newMaxSort, goal, services, ruleApp); return services.getTermFactory().createTerm(term.op(), subs, term.boundVars(), term.getLabels()); @@ -71,11 +73,10 @@ private SequentFormula applyReplacewithHelper(Goal goal, MatchResultInfo matchCond, TacletApp ruleApp) { final JTerm term = (JTerm) posOfFind.sequentFormula().formula(); - final IntIterator it = posOfFind.posInTerm().iterator(); final JTerm rwTemplate = gt.replaceWith(); JTerm formula = replace(term, rwTemplate, termLabelState, new TacletLabelHint(rwTemplate), - posOfFind, it, matchCond, term.sort(), goal, services, ruleApp); + posOfFind, posOfFind.posInTerm(), 0, matchCond, term.sort(), goal, services, ruleApp); formula = TermLabelManager.refactorSequentFormula(termLabelState, services, formula, posOfFind, taclet, goal, null, rwTemplate); if (term == formula) { diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/match/vm/ElementaryUpdateHead.java b/key.core/src/main/java/de/uka/ilkd/key/rule/match/vm/ElementaryUpdateHead.java new file mode 100644 index 00000000000..cbf6531f410 --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/match/vm/ElementaryUpdateHead.java @@ -0,0 +1,73 @@ +/* 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.match.vm; + +import java.util.List; + +import de.uka.ilkd.key.logic.op.ElementaryUpdate; +import de.uka.ilkd.key.logic.op.LocationVariable; + +import org.key_project.logic.Term; +import org.key_project.logic.op.sv.SchemaVariable; +import org.key_project.prover.rules.matcher.compiler.MatchHead; +import org.key_project.prover.rules.matcher.vm.MatchProgram; +import org.key_project.prover.rules.matcher.vm.instruction.MatchInstruction; +import org.key_project.prover.rules.matcher.vm.instruction.VMInstruction; + +import org.jspecify.annotations.Nullable; + +import static de.uka.ilkd.key.rule.match.vm.instructions.JavaDLMatchVMInstructionSet.getCheckNodeKindInstruction; +import static de.uka.ilkd.key.rule.match.vm.instructions.JavaDLMatchVMInstructionSet.getMatchIdentityInstruction; +import static de.uka.ilkd.key.rule.match.vm.instructions.JavaDLMatchVMInstructionSet.getMatchInstructionForSV; +import static de.uka.ilkd.key.rule.match.vm.instructions.JavaDLMatchVMInstructionSet.gotoNextInstruction; +import static de.uka.ilkd.key.rule.match.vm.instructions.JavaDLMatchVMInstructionSet.gotoNextSiblingInstruction; + +/** + * Match head for an {@link ElementaryUpdate} {@code lhs := value}: it matches the operator and the + * left-hand side; the value subterm is matched by the enclosing + * {@link org.key_project.prover.rules.matcher.compiler.OperatorPlan}. Mirrors the elementary-update + * fragments of the hand-written interpreter generator and compiled matcher. + */ +public final class ElementaryUpdateHead implements MatchHead { + + private final MatchInstruction lhsMatcher; + /** whether the left-hand side is a schema variable (it advances by sibling, not by descent). */ + private final boolean lhsIsSchemaVariable; + + private ElementaryUpdateHead(MatchInstruction lhsMatcher, boolean lhsIsSchemaVariable) { + this.lhsMatcher = lhsMatcher; + this.lhsIsSchemaVariable = lhsIsSchemaVariable; + } + + /** + * @param elUp the elementary update pattern + * @return a head for {@code elUp}, or {@code null} if its left-hand side is neither a schema + * variable nor a concrete location variable (then the caller falls back) + */ + public static @Nullable ElementaryUpdateHead of(ElementaryUpdate elUp) { + if (elUp.lhs() instanceof SchemaVariable sv) { + return new ElementaryUpdateHead(getMatchInstructionForSV(sv), true); + } else if (elUp.lhs() instanceof LocationVariable locVar) { + return new ElementaryUpdateHead(getMatchIdentityInstruction(locVar), false); + } + return null; + } + + @Override + public void emit(List out) { + out.add(getCheckNodeKindInstruction(ElementaryUpdate.class)); + out.add(gotoNextInstruction()); + out.add(lhsMatcher); + out.add(lhsIsSchemaVariable ? gotoNextSiblingInstruction() : gotoNextInstruction()); + } + + @Override + public MatchProgram compileHeadCheck() { + final MatchInstruction lhs = lhsMatcher; + return (element, mc, + services) -> ((Term) element).op() instanceof ElementaryUpdate actualElUp + ? lhs.match(actualElUp.lhs(), mc, services) + : null; + } +} diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/match/vm/JavaBinderMatcher.java b/key.core/src/main/java/de/uka/ilkd/key/rule/match/vm/JavaBinderMatcher.java new file mode 100644 index 00000000000..15d74b455c4 --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/match/vm/JavaBinderMatcher.java @@ -0,0 +1,46 @@ +/* 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.match.vm; + +import de.uka.ilkd.key.rule.MatchConditions; +import de.uka.ilkd.key.rule.match.vm.instructions.UnbindVariablesInstruction; + +import org.key_project.logic.op.QuantifiableVariable; +import org.key_project.prover.rules.instantiation.MatchResultInfo; +import org.key_project.prover.rules.matcher.compiler.BinderMatcher; +import org.key_project.prover.rules.matcher.vm.instruction.MatchInstruction; +import org.key_project.prover.rules.matcher.vm.instruction.VMInstruction; +import org.key_project.util.collection.ImmutableArray; + +import static de.uka.ilkd.key.rule.match.vm.instructions.JavaDLMatchVMInstructionSet.matchAndBindVariables; + +/** + * Java-DL implementation of the {@link BinderMatcher} SPI: bound variables are bound via the + * {@code matchAndBindVariables} instruction and the renaming scope is popped via + * {@link UnbindVariablesInstruction} (interpreter) / {@link MatchConditions#shrinkRenameTable()} + * (compiled). + */ +public final class JavaBinderMatcher implements BinderMatcher { + + /** stateless; a single shared instance suffices. */ + public static final JavaBinderMatcher INSTANCE = new JavaBinderMatcher(); + + private JavaBinderMatcher() {} + + @SuppressWarnings("unchecked") + @Override + public MatchInstruction binder(ImmutableArray boundVars) { + return matchAndBindVariables((ImmutableArray) boundVars); + } + + @Override + public VMInstruction unbinderInstruction() { + return new UnbindVariablesInstruction(); + } + + @Override + public MatchResultInfo unbind(MatchResultInfo mc) { + return ((MatchConditions) mc).shrinkRenameTable(); + } +} diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/match/vm/JavaMatchPlanBuilder.java b/key.core/src/main/java/de/uka/ilkd/key/rule/match/vm/JavaMatchPlanBuilder.java new file mode 100644 index 00000000000..06471eb8003 --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/match/vm/JavaMatchPlanBuilder.java @@ -0,0 +1,196 @@ +/* This file is part of KeY - https://key-project.org + * KeY is licensed under the GNU General Public License Version 2 + * SPDX-License-Identifier: GPL-2.0-only */ +package de.uka.ilkd.key.rule.match.vm; + +import java.util.ArrayList; +import java.util.List; + +import de.uka.ilkd.key.logic.JTerm; +import de.uka.ilkd.key.logic.op.ElementaryUpdate; +import de.uka.ilkd.key.logic.op.ParametricFunctionInstance; + +import org.key_project.logic.op.Modality; +import org.key_project.logic.op.Operator; +import org.key_project.logic.op.sv.SchemaVariable; +import org.key_project.prover.rules.instantiation.MatchResultInfo; +import org.key_project.prover.rules.matcher.compiler.GenericOperatorHead; +import org.key_project.prover.rules.matcher.compiler.MatchHead; +import org.key_project.prover.rules.matcher.compiler.MatchPlan; +import org.key_project.prover.rules.matcher.compiler.OperatorPlan; +import org.key_project.prover.rules.matcher.compiler.SchemaVarPlan; +import org.key_project.prover.rules.matcher.vm.MatchProgram; +import org.key_project.prover.rules.matcher.vm.instruction.MatchInstruction; +import org.key_project.prover.rules.matcher.vm.instruction.VMInstruction; + +import org.jspecify.annotations.Nullable; + +import static de.uka.ilkd.key.rule.match.vm.instructions.JavaDLMatchVMInstructionSet.getMatchInstructionForSV; +import static de.uka.ilkd.key.rule.match.vm.instructions.JavaDLMatchVMInstructionSet.matchTermLabelSV; + +/** + * The single Java-DL dispatch that builds a {@link MatchPlan} for a find pattern, from which both + * the interpreter and the compiled find-matcher are derived. Describing a construct here gives both + * back-ends at once -- this is the sole source of truth for find-matching; there is no separate + * hand-written interpreter generator or compiled matcher to keep in sync. + * + *

+ * It covers the whole Java-DL find-taclet base: the FOL term skeleton (schema variables, ordinary + * operators with their subterms, bound variables), term labels, elementary updates, parametric + * function instances and modalities (the Java program is matched through a + * {@link org.key_project.prover.rules.matcher.compiler.ProgramMatchHook}). A pattern the dispatch + * genuinely cannot model yields {@code null} and the {@linkplain #interpreterProgram facades} raise + * a clear error pointing at the missing head (no current taclet hits this; adding a construct means + * adding one head, see the developer docs). + */ +public final class JavaMatchPlanBuilder { + + private JavaMatchPlanBuilder() {} + + /** + * Builds the interpreter program for {@code pattern} through the match-plan framework, reading + * the {@code key.matcher.programInstructions} flag. + * + * @param pattern the find / assumes pattern + * @return the VM instruction program + */ + public static VMInstruction[] interpreterProgram(JTerm pattern) { + return interpreterProgram(pattern, + Boolean.getBoolean(SyntaxElementMatchProgramGenerator.PROGRAM_INSTRUCTIONS_PROPERTY)); + } + + /** + * Builds the interpreter program for {@code pattern} through the match-plan framework. + * + * @param pattern the find / assumes pattern + * @param programInstructions whether modality programs are converted to VM instructions + * @return the VM instruction program + */ + public static VMInstruction[] interpreterProgram(JTerm pattern, boolean programInstructions) { + final List out = new ArrayList<>(); + planOrThrow(pattern, programInstructions).emitInstructions(out); + return out.toArray(new VMInstruction[0]); + } + + /** + * Builds the cursor-free compiled matcher for {@code pattern} through the match-plan framework. + * + * @param pattern the find pattern + * @return the compiled matcher + */ + public static MatchProgram compiledProgram(JTerm pattern) { + return planOrThrow(pattern, false).compile(); + } + + /** + * Like {@link #compiledProgram(JTerm)}, but returns {@code null} instead of throwing when the + * dispatch has no head for {@code pattern} (so the caller can fall back to the interpreter). + * Used for {@code \assumes} formulas, which are not guaranteed to be among the patterns the + * find-matcher coverage is validated against. + * + * @param pattern the find / assumes pattern + * @return the compiled matcher, or {@code null} if the pattern is not compilable + */ + public static @Nullable MatchProgram compiledProgramOrNull(JTerm pattern) { + final MatchPlan plan = buildPlan(pattern, false); + return plan == null ? null : plan.compile(); + } + + private static MatchPlan planOrThrow(JTerm pattern, boolean programInstructions) { + final MatchPlan plan = buildPlan(pattern, programInstructions); + if (plan == null) { + throw new UnsupportedOperationException( + "the match-plan framework has no head for this find pattern (op " + + pattern.op() + "); add one (see the taclet-matching developer docs): " + + pattern); + } + return plan; + } + + /** + * Builds a match plan for {@code pattern}, or returns {@code null} if it uses a construct the + * dispatch cannot model (no current taclet does). + * + * @param pattern the find (sub)pattern + * @param programInstructions whether modality programs are converted to VM instructions on the + * interpreter side (irrelevant for the FOL skeleton and the compiled back-end) + * @return a match plan, or {@code null} + */ + public static @Nullable MatchPlan buildPlan(JTerm pattern, boolean programInstructions) { + final MatchPlan core = buildCore(pattern, programInstructions); + if (core == null || !pattern.hasLabels()) { + return core; + } + // term labels are matched in place (no cursor move), before the operator/subterms + return new LabelPlan(matchTermLabelSV(pattern.getLabels()), core); + } + + private static @Nullable MatchPlan buildCore(JTerm pattern, boolean programInstructions) { + final Operator op = pattern.op(); + + if (op instanceof SchemaVariable sv) { + if (pattern.arity() != 0) { + return null; // unusual schema-variable shape + } + return new SchemaVarPlan(getMatchInstructionForSV(sv), pattern.boundVars(), + JavaBinderMatcher.INSTANCE); + } + + final MatchHead head = buildHead(pattern, programInstructions); + if (head == null) { + return null; // unsupported construct or uncompilable program + } + + // the operator head plus a plan per subterm + final int arity = pattern.arity(); + final List children = new ArrayList<>(arity); + for (int i = 0; i < arity; i++) { + final MatchPlan child = buildPlan(pattern.sub(i), programInstructions); + if (child == null) { + return null; // a subterm is not handled -> the whole pattern is unsupported + } + children.add(child); + } + return new OperatorPlan(head, children, pattern.boundVars(), JavaBinderMatcher.INSTANCE); + } + + /** + * The operator-specific head for {@code pattern}'s operator, or {@code null} if the operator is + * not supported (or, for a modality, its program cannot be matched by the framework). + */ + private static @Nullable MatchHead buildHead(JTerm pattern, boolean programInstructions) { + final Operator op = pattern.op(); + if (op instanceof ElementaryUpdate elUp) { + return ElementaryUpdateHead.of(elUp); + } + if (op instanceof ParametricFunctionInstance pfi) { + return ParametricFunctionHead.of(pfi); + } + if (op instanceof Modality mod) { + return ModalityHead.of(mod, pattern.javaBlock().program(), programInstructions); + } + return new GenericOperatorHead(op); + } + + /** + * Wraps a plan with a term-label match: the labels are matched in place (the same + * {@code matchTermLabelSV} instruction the interpreter uses, no cursor move) before the wrapped + * operator/subterm matching. Reused by both back-ends. + */ + private record LabelPlan(MatchInstruction labelInstr, MatchPlan inner) implements MatchPlan { + @Override + public void emitInstructions(List out) { + out.add(labelInstr); + inner.emitInstructions(out); + } + + @Override + public MatchProgram compile() { + final MatchProgram innerCompiled = inner.compile(); + return (element, mc, services) -> { + final MatchResultInfo r = labelInstr.match(element, mc, services); + return r == null ? null : innerCompiled.match(element, r, services); + }; + } + } +} diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/match/vm/JavaProgramCompiler.java b/key.core/src/main/java/de/uka/ilkd/key/rule/match/vm/JavaProgramCompiler.java new file mode 100644 index 00000000000..83f009f0bac --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/match/vm/JavaProgramCompiler.java @@ -0,0 +1,201 @@ +/* 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.match.vm; + +import de.uka.ilkd.key.java.Services; +import de.uka.ilkd.key.java.ast.ContextStatementBlock; +import de.uka.ilkd.key.java.ast.JavaProgramElement; +import de.uka.ilkd.key.java.ast.ProgramElement; +import de.uka.ilkd.key.java.ast.SourceData; +import de.uka.ilkd.key.logic.JavaBlock; +import de.uka.ilkd.key.logic.op.ProgramSV; +import de.uka.ilkd.key.rule.MatchConditions; + +import org.key_project.logic.LogicServices; +import org.key_project.logic.SyntaxElement; +import org.key_project.logic.op.sv.SchemaVariable; +import org.key_project.prover.rules.instantiation.MatchResultInfo; +import org.key_project.prover.rules.matcher.vm.MatchProgram; +import org.key_project.prover.rules.matcher.vm.ProgramChildrenMatcher; +import org.key_project.prover.rules.matcher.vm.instruction.MatchInstruction; + +import org.jspecify.annotations.Nullable; + +import static de.uka.ilkd.key.rule.match.vm.instructions.JavaDLMatchVMInstructionSet.getMatchInstructionForSV; + +/** + * Compiles the cursor-free matcher for the Java program of a modality, used by the Java + * {@link org.key_project.prover.rules.matcher.compiler.ProgramMatchHook} (the compiled side of the + * match-plan framework). It navigates the Java AST directly via {@code getChild(i)} instead of a + * cursor, mirroring the converted program VM instructions of + * {@link SyntaxElementMatchProgramGenerator}. + * + *

+ * A top-level {@link ContextStatementBlock} keeps phases (1)(2)(4) of the context match in + * {@code ContextStatementBlock.match} and compiles only phase (3); generic structural elements are + * matched by class equality + exact-size child recursion; elements with their own {@code match} + * (value literals, type references, loops, ...) and generic elements with variable-arity children + * (a + * list schema variable {@code #slist}) are reused cursor-free by {@linkplain #delegateToMatch + * delegating to their own match}. + * + * @see org.key_project.prover.rules.matcher.vm.VMProgramInterpreter + */ +final class JavaProgramCompiler { + + private JavaProgramCompiler() {} + + /** + * A single compiled matching step over a program (sub)element. Navigates the Java AST directly + * via {@code getChild(i)} instead of a cursor, mirroring the converted program VM instructions. + */ + @FunctionalInterface + private interface ProgStep { + @Nullable + MatchResultInfo match(SyntaxElement actual, MatchResultInfo mc, LogicServices services); + } + + /** + * Compiles the cursor-free matcher for the Java program {@code prog} of a modality, applied + * directly to the source {@link JavaBlock} (it extracts the block's program element). A + * top-level + * {@link ContextStatementBlock} keeps phases (1)(2)(4) of the context match in + * {@code ContextStatementBlock.match} and compiles only phase (3) (each active statement + * consumes + * one source child), unless an active statement is variable-arity (a list SV) or otherwise + * uncompilable -- then the whole context match is delegated to + * {@code ContextStatementBlock.match} + * (its {@code matchChildren} handles list SVs) while the surrounding term skeleton stays + * compiled. + * Any other program is compiled by {@link #compileProgram}. Returns {@code null} only if that + * generic compilation cannot handle the program. + */ + static @Nullable MatchProgram compiledProgramMatcher(JavaProgramElement prog) { + if (prog instanceof ContextStatementBlock csb) { + final ProgStep[] active = compileActiveStatements(csb); + if (active != null) { + // phase (3) of the context match, cursor-free: each active statement consumes one + // child + final ProgramChildrenMatcher phase3 = (parent, startChild, mc, services) -> { + MatchResultInfo r = mc; + for (int k = 0; k < active.length; k++) { + r = active[k].match(parent.getChild(startChild + k), r, services); + if (r == null) { + return null; + } + } + return r; + }; + // phases (1)(2)(4) stay in ContextStatementBlock.match; only phase (3) is compiled + return (block, mc, services) -> csb.match( + new SourceData(((JavaBlock) block).program(), -1, (Services) services), + (MatchConditions) mc, phase3); + } + // an active statement is variable-arity (a list SV) or otherwise uncompilable: + // delegate the whole context match to the interpreter (its matchChildren handles + // list SVs); the surrounding term skeleton stays compiled + return (block, mc, services) -> csb.match( + new SourceData(((JavaBlock) block).program(), -1, (Services) services), + (MatchConditions) mc); + } + final ProgStep ps = compileProgram(prog); + if (ps == null) { + return null; + } + return (block, mc, services) -> ps.match(((JavaBlock) block).program(), mc, services); + } + + /** + * Compiles a Java program (sub)element: a generic-match element with a fixed, one-source-child + * structure is matched by direct {@code getChild} navigation (class equality + exact-size child + * recursion); a non-list program schema variable reuses its program-SV instruction. Anything + * else that is still a {@link ProgramElement} -- an element with its own {@code match} (value + * literals, type references, loops, ...) or a generic element whose children are not a + * fixed one-to-one structure (e.g. they contain a list schema variable {@code #slist}) -- is + * matched cursor-free by {@linkplain #delegateToMatch delegating to its own match}. Returns + * {@code null} only for a list schema variable on its own (variable arity: its enclosing + * element + * delegates) and for non-program schema variables. + */ + private static @Nullable ProgStep compileProgram(SyntaxElement pe) { + if (pe instanceof ProgramSV psv) { + if (psv.isListSV()) { + // a list SV by itself is variable-arity; the enclosing element delegates instead + return null; + } + final MatchInstruction svInstr = getMatchInstructionForSV(psv); + return svInstr::match; + } + if (pe instanceof SchemaVariable) { + return null; // other schema variables in programs: be safe, fall back + } + if (!(pe instanceof ProgramElement progEl)) { + return null; + } + if (SyntaxElementMatchProgramGenerator.isGenericMatch(progEl)) { + final int childCount = pe.getChildCount(); + final ProgStep[] subs = new ProgStep[childCount]; + boolean fixedStructure = true; + for (int i = 0; i < childCount; i++) { + final ProgStep s = compileProgram(pe.getChild(i)); + if (s == null) { + fixedStructure = false; // e.g. a list SV child -> not one-to-one + break; + } + subs[i] = s; + } + if (fixedStructure) { + final Class kind = pe.getClass(); + return (actual, mc, services) -> { + if (actual.getClass() != kind || actual.getChildCount() != childCount) { + return null; + } + MatchResultInfo r = mc; + for (int i = 0; i < childCount; i++) { + r = subs[i].match(actual.getChild(i), r, services); + if (r == null) { + return null; + } + } + return r; + }; + } + } + // an element with its own match (value literals, TypeRef, SchematicFieldReference, + // VariableSpecification, loops, ...) or a generic element with variable-arity children + // (a list SV): reuse its own match cursor-free (see delegateToMatch) + return delegateToMatch(progEl); + } + + /** + * Matches {@code progEl} by reusing its own {@code match(SourceData, MatchConditions)} + * cursor-free, exactly as {@code MatchProgramInstruction} does at the program root. This keeps + * the surrounding program compiled (only this sub-element delegates) and is + * behaviour-preserving + * by construction: it is the very match the interpreter would call, including the + * {@code matchChildren} handling of list schema variables. + */ + private static ProgStep delegateToMatch(ProgramElement progEl) { + return (actual, mc, services) -> progEl.match( + new SourceData((ProgramElement) actual, -1, (Services) services), (MatchConditions) mc); + } + + /** + * Compiles the active statements of a context block (its children from the active offset, i.e. + * skipping the execution context if present), or returns {@code null} if any active statement + * uses a construct the compiler does not handle. + */ + private static ProgStep @Nullable [] compileActiveStatements(ContextStatementBlock csb) { + final int offset = csb.getExecutionContext() == null ? 0 : 1; + final ProgStep[] active = new ProgStep[csb.getChildCount() - offset]; + for (int i = offset, n = csb.getChildCount(); i < n; i++) { + final ProgStep s = compileProgram(csb.getChildAt(i)); + if (s == null) { + return null; + } + active[i - offset] = s; + } + return active; + } +} diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/match/vm/JavaProgramMatchHook.java b/key.core/src/main/java/de/uka/ilkd/key/rule/match/vm/JavaProgramMatchHook.java new file mode 100644 index 00000000000..167623ddb8f --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/match/vm/JavaProgramMatchHook.java @@ -0,0 +1,67 @@ +/* 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.match.vm; + +import de.uka.ilkd.key.java.ast.JavaProgramElement; + +import org.key_project.prover.rules.matcher.compiler.ProgramMatchHook; +import org.key_project.prover.rules.matcher.vm.MatchProgram; +import org.key_project.prover.rules.matcher.vm.instruction.VMInstruction; + +import org.jspecify.annotations.Nullable; + +import static de.uka.ilkd.key.rule.match.vm.SyntaxElementMatchProgramGenerator.buildProgramInstruction; +import static de.uka.ilkd.key.rule.match.vm.instructions.JavaDLMatchVMInstructionSet.matchProgram; + +/** + * Java-DL implementation of the {@link ProgramMatchHook} program-AST axis: it matches the + * {@code JavaBlock} program of a modality. The interpreter side reuses the generator's converted + * program instruction ({@link SyntaxElementMatchProgramGenerator#buildProgramInstruction}, falling + * back to the monolithic {@code MatchProgramInstruction} when conversion is off or unavailable); + * the + * compiled side reuses {@link JavaProgramCompiler#compiledProgramMatcher} (context-block phases + + * generic {@code getChild} navigation + value-leaf / list-SV delegation). Both are lifted verbatim + * from the hand-written matchers, so the framework reproduces them exactly. + */ +public final class JavaProgramMatchHook implements ProgramMatchHook { + + private final JavaProgramElement prog; + private final boolean programInstructions; + private final MatchProgram compiled; + + private JavaProgramMatchHook(JavaProgramElement prog, boolean programInstructions, + MatchProgram compiled) { + this.prog = prog; + this.programInstructions = programInstructions; + this.compiled = compiled; + } + + /** + * @param prog the modality's program pattern + * @param programInstructions whether the interpreter side converts the program to VM + * instructions (otherwise the monolithic {@code MatchProgramInstruction} is used) + * @return a hook for {@code prog}, or {@code null} if the compiled side cannot handle the + * program + * (then the enclosing modality falls back to the legacy matcher) + */ + public static @Nullable JavaProgramMatchHook of(JavaProgramElement prog, + boolean programInstructions) { + final MatchProgram compiled = JavaProgramCompiler.compiledProgramMatcher(prog); + if (compiled == null) { + return null; + } + return new JavaProgramMatchHook(prog, programInstructions, compiled); + } + + @Override + public VMInstruction programInstruction() { + final VMInstruction converted = programInstructions ? buildProgramInstruction(prog) : null; + return converted != null ? converted : matchProgram(prog); + } + + @Override + public MatchProgram compileProgram() { + return compiled; + } +} diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/match/vm/ModalityHead.java b/key.core/src/main/java/de/uka/ilkd/key/rule/match/vm/ModalityHead.java new file mode 100644 index 00000000000..d1accbea58b --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/match/vm/ModalityHead.java @@ -0,0 +1,92 @@ +/* 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.match.vm; + +import java.util.List; + +import de.uka.ilkd.key.java.ast.JavaProgramElement; +import de.uka.ilkd.key.logic.JTerm; +import de.uka.ilkd.key.logic.op.ModalOperatorSV; + +import org.key_project.logic.Term; +import org.key_project.logic.op.Modality; +import org.key_project.prover.rules.instantiation.MatchResultInfo; +import org.key_project.prover.rules.matcher.compiler.MatchHead; +import org.key_project.prover.rules.matcher.compiler.ProgramMatchHook; +import org.key_project.prover.rules.matcher.vm.MatchProgram; +import org.key_project.prover.rules.matcher.vm.instruction.MatchInstruction; +import org.key_project.prover.rules.matcher.vm.instruction.VMInstruction; + +import org.jspecify.annotations.Nullable; + +import static de.uka.ilkd.key.rule.match.vm.instructions.JavaDLMatchVMInstructionSet.getCheckNodeKindInstruction; +import static de.uka.ilkd.key.rule.match.vm.instructions.JavaDLMatchVMInstructionSet.getMatchIdentityInstruction; +import static de.uka.ilkd.key.rule.match.vm.instructions.JavaDLMatchVMInstructionSet.gotoNextInstruction; +import static de.uka.ilkd.key.rule.match.vm.instructions.JavaDLMatchVMInstructionSet.gotoNextSiblingInstruction; +import static de.uka.ilkd.key.rule.match.vm.instructions.JavaDLMatchVMInstructionSet.matchModalOperatorSV; + +/** + * Match head for a {@link Modality} {@code \<{ prog }\> post}: it matches the operator, the modal + * kind (a {@link ModalOperatorSV} or a concrete kind by identity) and the Java program (through a + * {@link ProgramMatchHook}); the post-condition subterm is matched by the enclosing + * {@link org.key_project.prover.rules.matcher.compiler.OperatorPlan}. The program AST is the second + * cross-language axis (see {@link ProgramMatchHook}); the kind and skeleton are lifted from the + * hand-written interpreter generator and compiled matcher. + */ +public final class ModalityHead implements MatchHead { + + private final MatchInstruction kindInstr; + private final ProgramMatchHook programHook; + + private ModalityHead(MatchInstruction kindInstr, ProgramMatchHook programHook) { + this.kindInstr = kindInstr; + this.programHook = programHook; + } + + /** + * @param mod the modality pattern + * @param prog the modality's Java program ({@code pattern.javaBlock().program()}) + * @param programInstructions whether the interpreter side converts the program to VM + * instructions + * @return a head for {@code mod}, or {@code null} if the program cannot be matched by the + * framework (then the caller falls back) + */ + public static @Nullable ModalityHead of(Modality mod, JavaProgramElement prog, + boolean programInstructions) { + final JavaProgramMatchHook hook = JavaProgramMatchHook.of(prog, programInstructions); + if (hook == null) { + return null; + } + final MatchInstruction kindInstr = mod.kind() instanceof ModalOperatorSV sv + ? matchModalOperatorSV(sv) + : getMatchIdentityInstruction(mod.kind()); + return new ModalityHead(kindInstr, hook); + } + + @Override + public void emit(List out) { + out.add(getCheckNodeKindInstruction(Modality.class)); + out.add(gotoNextInstruction()); + out.add(kindInstr); + out.add(gotoNextInstruction()); + out.add(programHook.programInstruction()); + out.add(gotoNextSiblingInstruction()); + } + + @Override + public MatchProgram compileHeadCheck() { + final MatchInstruction kind = kindInstr; + final MatchProgram programMatch = programHook.compileProgram(); + return (element, mc, services) -> { + if (!(((Term) element).op() instanceof Modality m)) { + return null; + } + final MatchResultInfo r = kind.match(m.kind(), mc, services); + if (r == null) { + return null; + } + return programMatch.match(((JTerm) element).javaBlock(), r, services); + }; + } +} diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/match/vm/ParametricFunctionHead.java b/key.core/src/main/java/de/uka/ilkd/key/rule/match/vm/ParametricFunctionHead.java new file mode 100644 index 00000000000..c67cf949670 --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/match/vm/ParametricFunctionHead.java @@ -0,0 +1,94 @@ +/* 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.match.vm; + +import java.util.List; + +import de.uka.ilkd.key.logic.GenericArgument; +import de.uka.ilkd.key.logic.op.ParametricFunctionInstance; +import de.uka.ilkd.key.logic.sort.GenericSort; +import de.uka.ilkd.key.logic.sort.ParametricSortInstance; + +import org.key_project.logic.Term; +import org.key_project.prover.rules.instantiation.MatchResultInfo; +import org.key_project.prover.rules.matcher.compiler.MatchHead; +import org.key_project.prover.rules.matcher.vm.MatchProgram; +import org.key_project.prover.rules.matcher.vm.instruction.MatchInstruction; +import org.key_project.prover.rules.matcher.vm.instruction.VMInstruction; + +import org.jspecify.annotations.Nullable; + +import static de.uka.ilkd.key.rule.match.vm.instructions.JavaDLMatchVMInstructionSet.getCheckNodeKindInstruction; +import static de.uka.ilkd.key.rule.match.vm.instructions.JavaDLMatchVMInstructionSet.getMatchGenericSortInstruction; +import static de.uka.ilkd.key.rule.match.vm.instructions.JavaDLMatchVMInstructionSet.getMatchIdentityInstruction; +import static de.uka.ilkd.key.rule.match.vm.instructions.JavaDLMatchVMInstructionSet.getSimilarParametricFunctionInstruction; +import static de.uka.ilkd.key.rule.match.vm.instructions.JavaDLMatchVMInstructionSet.gotoNextInstruction; + +/** + * Match head for a {@link ParametricFunctionInstance}: it checks that the operator has the same + * base + * and matches the generic arguments (a generic sort, or a concrete argument by identity); the + * function's subterms are matched by the enclosing + * {@link org.key_project.prover.rules.matcher.compiler.OperatorPlan}. Mirrors the + * parametric-function fragments of the hand-written matchers. + */ +public final class ParametricFunctionHead implements MatchHead { + + private final MatchInstruction similar; + private final MatchInstruction[] argMatchers; + + private ParametricFunctionHead(MatchInstruction similar, MatchInstruction[] argMatchers) { + this.similar = similar; + this.argMatchers = argMatchers; + } + + /** + * @param pfi the parametric function instance pattern + * @return a head for {@code pfi}, or {@code null} if a generic argument uses a parametric sort + * instance (which the matchers do not handle; then the caller falls back) + */ + public static @Nullable ParametricFunctionHead of(ParametricFunctionInstance pfi) { + final int argCount = pfi.getChildCount(); + final MatchInstruction[] argMatchers = new MatchInstruction[argCount]; + for (int i = 0; i < argCount; i++) { + final GenericArgument arg = (GenericArgument) pfi.getChild(i); + if (arg.sort() instanceof GenericSort gs) { + argMatchers[i] = getMatchGenericSortInstruction(gs); + } else if (arg.sort() instanceof ParametricSortInstance) { + return null; + } else { + argMatchers[i] = getMatchIdentityInstruction(arg); + } + } + return new ParametricFunctionHead(getSimilarParametricFunctionInstruction(pfi), + argMatchers); + } + + @Override + public void emit(List out) { + out.add(getCheckNodeKindInstruction(ParametricFunctionInstance.class)); + out.add(similar); + out.add(gotoNextInstruction()); + for (MatchInstruction argMatcher : argMatchers) { + out.add(argMatcher); + out.add(gotoNextInstruction()); + } + } + + @Override + public MatchProgram compileHeadCheck() { + final MatchInstruction sim = similar; + final MatchInstruction[] args = argMatchers; + return (element, mc, services) -> { + if (!(((Term) element).op() instanceof ParametricFunctionInstance actualPfi)) { + return null; + } + MatchResultInfo r = sim.match(actualPfi, mc, services); + for (int i = 0; r != null && i < args.length; i++) { + r = args[i].match(actualPfi.getChild(i), r, services); + } + return r; + }; + } +} diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/match/vm/SyntaxElementMatchProgramGenerator.java b/key.core/src/main/java/de/uka/ilkd/key/rule/match/vm/SyntaxElementMatchProgramGenerator.java index b62cff84d0b..0afdb914e3c 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/match/vm/SyntaxElementMatchProgramGenerator.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/match/vm/SyntaxElementMatchProgramGenerator.java @@ -4,130 +4,162 @@ package de.uka.ilkd.key.rule.match.vm; import java.util.ArrayList; +import java.util.List; +import java.util.Map; +import java.util.concurrent.ConcurrentHashMap; -import de.uka.ilkd.key.logic.GenericArgument; -import de.uka.ilkd.key.logic.JTerm; +import de.uka.ilkd.key.java.ast.ContextStatementBlock; +import de.uka.ilkd.key.java.ast.JavaNonTerminalProgramElement; +import de.uka.ilkd.key.java.ast.JavaProgramElement; +import de.uka.ilkd.key.java.ast.ProgramElement; +import de.uka.ilkd.key.java.ast.SourceData; import de.uka.ilkd.key.logic.op.*; -import de.uka.ilkd.key.logic.sort.GenericSort; -import de.uka.ilkd.key.logic.sort.ParametricSortInstance; +import de.uka.ilkd.key.rule.MatchConditions; +import de.uka.ilkd.key.rule.match.vm.instructions.MatchContextStatementBlockInstruction; +import de.uka.ilkd.key.rule.match.vm.instructions.MatchProgramElementInstruction; +import de.uka.ilkd.key.rule.match.vm.instructions.MatchSubProgramInstruction; -import org.key_project.logic.op.Modality; -import org.key_project.logic.op.Operator; -import org.key_project.logic.op.QuantifiableVariable; +import org.key_project.logic.SyntaxElement; import org.key_project.logic.op.sv.SchemaVariable; -import org.key_project.prover.rules.matcher.vm.instruction.MatchInstruction; +import org.key_project.prover.rules.matcher.vm.VMProgramInterpreter; import org.key_project.prover.rules.matcher.vm.instruction.VMInstruction; -import org.key_project.util.collection.ImmutableArray; + +import org.jspecify.annotations.Nullable; import static de.uka.ilkd.key.rule.match.vm.instructions.JavaDLMatchVMInstructionSet.*; /** - * This class generates a matching program for a given syntax element that can be - * interpreted by the virtual machine's interpreter + * Converts the Java program of a modality into VM match-instructions ({@link VMInstruction}s) by + * direct tree navigation, for the interpreter side of the match-plan framework (used by the Java + * {@link org.key_project.prover.rules.matcher.compiler.ProgramMatchHook}). The term skeleton itself + * is built by {@link JavaMatchPlanBuilder}; this class only handles the program-element conversion + * (generic structural elements and non-list program schema variables; anything else is matched by + * the monolithic {@code MatchProgramInstruction}). * * @see org.key_project.prover.rules.matcher.vm.VMProgramInterpreter */ public class SyntaxElementMatchProgramGenerator { /** - * creates a matcher for the given pattern - * - * @param pattern the {@link JTerm} specifying the pattern - * @return the specialized matcher for the given pattern + * System property ({@code -Dkey.matcher.programInstructions=true}) selecting whether the Java + * program of a modality is matched by a sub-program of {@link VMInstruction}s (a {@link + * MatchSubProgramInstruction}) instead of the monolithic {@code MatchProgramInstruction}. Only + * patterns built from generic-match element kinds + (non-list) program schema variables are + * converted; anything else (context blocks, loops, value literals, list SVs) falls back to the + * interpreter. Default {@code false} keeps the existing behaviour. + *

+ * Read at matcher-construction time (i.e. when the taclet base is loaded) rather than once at + * class load, so toggling it and reloading the proof switches the behaviour. */ - public static VMInstruction[] createProgram(JTerm pattern) { - ArrayList program = new ArrayList<>(); - createProgram(pattern, program); - return program.toArray(new VMInstruction[0]); - } + public static final String PROGRAM_INSTRUCTIONS_PROPERTY = "key.matcher.programInstructions"; /** - * creates a matching program for the given pattern. It appends the necessary match instruction - * to the given list of instructions - * - * @param pattern the {@link JTerm} used as pattern for which to create a matcher - * @param program the list of {@link MatchInstruction} to which the instructions for matching - * {@code pattern} are added. + * caches, per program-element class, whether it uses the generic {@code match} (no override). */ - private static void createProgram(JTerm pattern, ArrayList program) { - final Operator op = pattern.op(); + private static final Map, Boolean> GENERIC_MATCH = new ConcurrentHashMap<>(); - final ImmutableArray boundVars = pattern.boundVars(); - - if (!boundVars.isEmpty()) { - program.add(matchAndBindVariables(boundVars)); - } - - if (pattern.hasLabels()) { - program.add(matchTermLabelSV(pattern.getLabels())); + /** + * Builds the instruction matching the Java program {@code prog} of a modality by direct tree + * navigation, or returns {@code null} if {@code prog} uses a construct the converter does not + * handle (the caller then falls back to the monolithic {@code MatchProgramInstruction}). A + * top-level {@link ContextStatementBlock} (the {@code .. ...} pattern of symbolic-execution + * taclets) is matched by a {@link MatchContextStatementBlockInstruction} that converts only the + * active-statement matching; any other program is matched generically by a + * {@link MatchSubProgramInstruction}. + */ + static @Nullable VMInstruction buildProgramInstruction(JavaProgramElement prog) { + if (prog instanceof ContextStatementBlock csb) { + final VMInstruction[] active = buildContextActiveStatementsProgram(csb); + return active == null ? null + : new MatchContextStatementBlockInstruction(csb, + new VMProgramInterpreter(active)); } + final VMInstruction[] sub = buildProgramSubProgram(prog); + return sub == null ? null : new MatchSubProgramInstruction(new VMProgramInterpreter(sub)); + } - if (op instanceof SchemaVariable sv) { - program.add(getMatchInstructionForSV(sv)); - program.add(gotoNextSiblingInstruction()); - } else { - program.add(getCheckNodeKindInstruction(JTerm.class)); - program.add(gotoNextInstruction()); - switch (op) { - case ParametricFunctionInstance pfi -> { - program.add(getCheckNodeKindInstruction(ParametricFunctionInstance.class)); - program.add(getSimilarParametricFunctionInstruction(pfi)); - program.add(gotoNextInstruction()); - for (int i = 0; i < pfi.getChildCount(); i++) { - var arg = (GenericArgument) pfi.getChild(i); - if (arg.sort() instanceof GenericSort gs) { - program.add(getMatchGenericSortInstruction(gs)); - } else if (arg.sort() instanceof ParametricSortInstance) { - throw new UnsupportedOperationException( - "TODO @ DD: Parametric sort in generic args!"); - } else { - program.add(getMatchIdentityInstruction(arg)); - } - program.add(gotoNextInstruction()); - } - } - case ElementaryUpdate elUp -> { - program.add(getCheckNodeKindInstruction(ElementaryUpdate.class)); - program.add(gotoNextInstruction()); - if (elUp.lhs() instanceof SchemaVariable sv) { - program.add(getMatchInstructionForSV(sv)); - program.add(gotoNextSiblingInstruction()); - } else if (elUp.lhs() instanceof LocationVariable locVar) { - program.add(getMatchIdentityInstruction(locVar)); - program.add(gotoNextInstruction()); - } - } - case Modality mod -> { - program.add(getCheckNodeKindInstruction(Modality.class)); - program.add(gotoNextInstruction()); - if (mod.kind() instanceof ModalOperatorSV modKindSV) { - program.add(matchModalOperatorSV(modKindSV)); - } else { - program.add(getMatchIdentityInstruction(mod.kind())); - } - program.add(gotoNextInstruction()); - program.add(matchProgram(pattern.javaBlock().program())); - program.add(gotoNextSiblingInstruction()); - } - default -> { - program.add(getMatchIdentityInstruction(op)); - program.add(gotoNextInstruction()); - } + /** + * Builds a sub-program matching the active statements of the context block {@code csb} (its + * children from the active offset, i.e. skipping the execution context if present), or returns + * {@code null} if any active statement uses a construct the converter does not handle. The + * resulting program is meant to be run via + * {@link VMProgramInterpreter#matchChildrenFrom(org.key_project.logic.SyntaxElement, int, org.key_project.prover.rules.instantiation.MatchResultInfo, org.key_project.logic.LogicServices)} + * starting at the located source child, so that each per-statement matcher consumes exactly one + * source child -- mirroring {@code matchChildren} on the interpreter side. + */ + private static VMInstruction @Nullable [] buildContextActiveStatementsProgram( + ContextStatementBlock csb) { + final int offset = csb.getExecutionContext() == null ? 0 : 1; + final List out = new ArrayList<>(); + for (int i = offset, n = csb.getChildCount(); i < n; i++) { + if (!appendProgram(csb.getChildAt(i), out)) { + return null; } } + return out.toArray(new VMInstruction[0]); + } + + /** + * Builds a sub-program of {@link VMInstruction}s matching the given Java program by direct tree + * navigation, or returns {@code null} if the program uses a construct the converter does not + * handle (the caller then falls back to the monolithic {@code MatchProgramInstruction}). + */ + private static VMInstruction @Nullable [] buildProgramSubProgram(JavaProgramElement prog) { + final List out = new ArrayList<>(); + return appendProgram(prog, out) ? out.toArray(new VMInstruction[0]) : null; + } - if (!boundVars.isEmpty()) { - for (int i = 0; i < boundVars.size(); i++) { - program.add(gotoNextSiblingInstruction()); + /** + * Appends instructions matching {@code pe} (and its subtree) to {@code out}, mirroring the + * generic program match (class equality + exact-size child recursion) and reusing the existing + * program-SV instruction. Returns {@code false} (leaving {@code out} unusable) for any + * construct + * that is not safe to convert: list schema variables, other schema variables, and element types + * that override {@code match} (context blocks, loops, value-checking literals, ...). + */ + private static boolean appendProgram(SyntaxElement pe, List out) { + if (pe instanceof ProgramSV psv) { + if (psv.isListSV()) { + return false; // list SV -> variable block size, leave it to the interpreter } + out.add(getMatchInstructionForSV(psv)); + out.add(gotoNextSiblingInstruction()); + return true; } - - for (int i = 0; i < pattern.arity(); i++) { - createProgram(pattern.sub(i), program); + if (pe instanceof SchemaVariable) { + return false; // other schema variables in programs: be safe, fall back } - - if (!boundVars.isEmpty()) { - program.add(unbindVariables(boundVars)); + if (!(pe instanceof ProgramElement progEl) || !isGenericMatch(progEl)) { + return false; // overrides match (context block, loop, value literal, ...) -> fall back } + final int childCount = pe.getChildCount(); + out.add(new MatchProgramElementInstruction(pe.getClass(), childCount)); + out.add(gotoNextInstruction()); + for (int i = 0; i < childCount; i++) { + if (!appendProgram(pe.getChild(i), out)) { + return false; + } + } + return true; + } + + /** + * @return whether the element's class uses the generic + * {@code match(SourceData, MatchConditions)} (declared in {@code JavaProgramElement} or + * {@code JavaNonTerminalProgramElement}: class equality + exact-size child recursion) + * rather than its own override. + */ + static boolean isGenericMatch(ProgramElement pe) { + return GENERIC_MATCH.computeIfAbsent(pe.getClass(), c -> { + try { + final Class declaring = + c.getMethod("match", SourceData.class, MatchConditions.class) + .getDeclaringClass(); + return declaring == JavaProgramElement.class + || declaring == JavaNonTerminalProgramElement.class; + } catch (NoSuchMethodException e) { + return false; + } + }); } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/match/vm/VMTacletMatcher.java b/key.core/src/main/java/de/uka/ilkd/key/rule/match/vm/VMTacletMatcher.java index 2a877e4fabc..b0506e3f103 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/rule/match/vm/VMTacletMatcher.java +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/match/vm/VMTacletMatcher.java @@ -17,6 +17,7 @@ import de.uka.ilkd.key.rule.match.TacletMatcherKit; import de.uka.ilkd.key.rule.match.vm.instructions.JavaDLMatchVMInstructionSet; import de.uka.ilkd.key.rule.match.vm.instructions.MatchSchemaVariableInstruction; +import de.uka.ilkd.key.settings.FeatureSettings; import org.key_project.logic.LogicServices; import org.key_project.logic.SyntaxElement; @@ -29,6 +30,7 @@ import org.key_project.prover.rules.instantiation.AssumesFormulaInstantiation; import org.key_project.prover.rules.instantiation.AssumesMatchResult; import org.key_project.prover.rules.instantiation.MatchResultInfo; +import org.key_project.prover.rules.matcher.vm.MatchProgram; import org.key_project.prover.rules.matcher.vm.VMProgramInterpreter; import org.key_project.prover.sequent.Sequent; import org.key_project.prover.sequent.SequentFormula; @@ -56,10 +58,42 @@ */ public class VMTacletMatcher implements TacletMatcher { + /** + * System property ({@code -Dkey.matcher.interpreter=true}) forcing the legacy cursor-based + * interpreter find-matcher. The cursor-free compiled matcher is the default; this is mainly for + * headless / CI A/B comparison. In the GUI use the {@link #INTERPRETER_MATCHER_FEATURE} feature + * flag instead. + *

+ * Read in the constructor (i.e. per taclet, when the taclet base is loaded) rather than once at + * class load, so toggling it and reloading the proof switches matchers. + */ + public static final String INTERPRETER_MATCHER_PROPERTY = "key.matcher.interpreter"; + + /** + * Feature flag (Settings → Feature Flags, persistent) forcing the legacy interpreter + * find-matcher, the GUI-friendly equivalent of {@link #INTERPRETER_MATCHER_PROPERTY}. The + * compiled matcher is the default; activate this to fall back to the interpreter. Like the + * property it is read per taclet at construction time, so it takes effect for newly loaded + * proofs (or after reloading the current one) -- hence {@code restartRequired = true}. + */ + public static final FeatureSettings.Feature INTERPRETER_MATCHER_FEATURE = + FeatureSettings.createFeature("MATCHER_INTERPRETER", + "Use the legacy interpreter taclet find-matcher instead of the compiled one " + + "(reload the proof to apply).", + true); + + /** + * System property ({@code -Dkey.matcher.interpreterAssumes=true}) forcing the interpreter for + * {@code \assumes} formula matching even when the compiled find-matcher is selected. The + * compiled matcher (incl. the Java program of a modality) is used for assumes by default; this + * is mainly for headless A/B comparison of the compiled-assumes extension. + */ + public static final String INTERPRETER_ASSUMES_PROPERTY = "key.matcher.interpreterAssumes"; + /** the matcher for the find expression of the taclet */ - private final VMProgramInterpreter findMatchProgram; + private final MatchProgram findMatchProgram; /** the matcher for the taclet's assumes formulas */ - private final HashMap assumesMatchPrograms = + private final HashMap assumesMatchPrograms = new HashMap<>(); /** @@ -95,24 +129,48 @@ public VMTacletMatcher(Taclet taclet) { boundVars = taclet.getBoundVariables(); varsNotFreeIn = taclet.varsNotFreeIn(); + // both back-ends are derived from the unified match-plan framework (one dispatch per + // construct, see JavaMatchPlanBuilder); the compiled matcher is the default, the + // interpreter is used only when explicitly selected (property/feature flag) or as the + // automatic fallback for a pattern the compiler does not handle + final boolean useInterpreter = Boolean.getBoolean(INTERPRETER_MATCHER_PROPERTY) + || FeatureSettings.isFeatureActivated(INTERPRETER_MATCHER_FEATURE); + if (taclet instanceof final FindTaclet findTaclet) { findExp = findTaclet.find(); ignoreTopLevelUpdates = taclet.ignoreTopLevelUpdates() && !(findExp.op() instanceof UpdateApplication); - findMatchProgram = - new VMProgramInterpreter(SyntaxElementMatchProgramGenerator.createProgram(findExp)); - + findMatchProgram = matchProgramFor(findExp, useInterpreter); } else { ignoreTopLevelUpdates = false; findExp = null; findMatchProgram = null; } + // The taclet's \assumes formulas use the same back-end as the find: when the compiled + // matcher is selected they are compiled too (cursor-free, including the Java program of a + // modality), unless -Dkey.matcher.interpreterAssumes forces the interpreter for them. + final boolean assumesInterpreter = + useInterpreter || Boolean.getBoolean(INTERPRETER_ASSUMES_PROPERTY); for (final SequentFormula sf : assumesSequent) { assumesMatchPrograms.put(sf.formula(), - new VMProgramInterpreter( - SyntaxElementMatchProgramGenerator.createProgram((JTerm) sf.formula()))); + matchProgramFor((JTerm) sf.formula(), assumesInterpreter)); + } + } + + /** + * Builds the matcher for a find / assumes {@code pattern}: the cursor-free compiled matcher + * unless the interpreter is requested or the compiler has no head for the pattern (then the + * interpreter is used as a fallback). + */ + private static MatchProgram matchProgramFor(JTerm pattern, boolean interpreter) { + if (!interpreter) { + final MatchProgram compiled = JavaMatchPlanBuilder.compiledProgramOrNull(pattern); + if (compiled != null) { + return compiled; + } } + return new VMProgramInterpreter(JavaMatchPlanBuilder.interpreterProgram(pattern)); } /** @@ -127,7 +185,7 @@ public VMTacletMatcher(Taclet taclet) { @NonNull Term p_template, @NonNull MatchResultInfo p_matchCond, @NonNull LogicServices p_services) { - VMProgramInterpreter interpreter = assumesMatchPrograms.get(p_template); + MatchProgram program = assumesMatchPrograms.get(p_template); final var mc = (MatchConditions) p_matchCond; ImmutableList resFormulas = ImmutableSLList.nil(); @@ -149,7 +207,7 @@ public VMTacletMatcher(Taclet taclet) { } if (formula != null) {// update context not present or update context match succeeded final MatchResultInfo newMC = - checkConditions(interpreter.match(formula, mc, p_services), p_services); + checkConditions(program.match(formula, mc, p_services), p_services); if (newMC != null) { resFormulas = resFormulas.prepend(cf); diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/match/vm/instructions/MatchContextStatementBlockInstruction.java b/key.core/src/main/java/de/uka/ilkd/key/rule/match/vm/instructions/MatchContextStatementBlockInstruction.java new file mode 100644 index 00000000000..1c5955bc2ea --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/match/vm/instructions/MatchContextStatementBlockInstruction.java @@ -0,0 +1,51 @@ +/* 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.match.vm.instructions; + +import de.uka.ilkd.key.java.Services; +import de.uka.ilkd.key.java.ast.ContextStatementBlock; +import de.uka.ilkd.key.java.ast.SourceData; +import de.uka.ilkd.key.logic.JavaBlock; +import de.uka.ilkd.key.rule.MatchConditions; + +import org.key_project.logic.LogicServices; +import org.key_project.logic.SyntaxElement; +import org.key_project.prover.rules.instantiation.MatchResultInfo; +import org.key_project.prover.rules.matcher.vm.VMProgramInterpreter; +import org.key_project.prover.rules.matcher.vm.instruction.MatchInstruction; + +import org.jspecify.annotations.Nullable; + +/** + * Matches the Java program of a modality whose program is a {@link ContextStatementBlock} (the + * {@code .. ... } pattern that is ubiquitous in symbolic-execution taclets). The intricate context + * bookkeeping (variable-length prefix descent, inner execution context, prefix/suffix positions) is + * still performed by {@link ContextStatementBlock#match}; only the matching of the active + * statements + * is delegated to the supplied VM sub-program, replacing the monolithic + * {@code MatchProgramInstruction} + * for that subtree. The current element is the modality's {@link JavaBlock} (as for + * {@code MatchProgramInstruction}). + * + * @see ContextStatementBlock#match(SourceData, MatchConditions, VMProgramInterpreter) + */ +public final class MatchContextStatementBlockInstruction implements MatchInstruction { + + private final ContextStatementBlock contextBlock; + private final VMProgramInterpreter activeStatements; + + public MatchContextStatementBlockInstruction(ContextStatementBlock contextBlock, + VMProgramInterpreter activeStatements) { + this.contextBlock = contextBlock; + this.activeStatements = activeStatements; + } + + @Override + public @Nullable MatchResultInfo match(SyntaxElement actualElement, + MatchResultInfo matchConditions, LogicServices services) { + return contextBlock.match( + new SourceData(((JavaBlock) actualElement).program(), -1, (Services) services), + (MatchConditions) matchConditions, activeStatements); + } +} diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/match/vm/instructions/MatchProgramElementInstruction.java b/key.core/src/main/java/de/uka/ilkd/key/rule/match/vm/instructions/MatchProgramElementInstruction.java new file mode 100644 index 00000000000..fe02c7538c9 --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/match/vm/instructions/MatchProgramElementInstruction.java @@ -0,0 +1,39 @@ +/* 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.match.vm.instructions; + +import org.key_project.logic.LogicServices; +import org.key_project.logic.SyntaxElement; +import org.key_project.prover.rules.instantiation.MatchResultInfo; +import org.key_project.prover.rules.matcher.vm.instruction.MatchInstruction; + +import org.jspecify.annotations.Nullable; + +/** + * Matches a single program element structurally: the current element must have exactly the expected + * concrete class and number of children. This mirrors the generic program matching + * ({@code JavaProgramElement.match} / {@code JavaNonTerminalProgramElement.match}: class equality + * plus an exact block size), and is only emitted for element types that use that generic match (the + * compiler falls back to the interpreter's {@code MatchProgramInstruction} for any type that + * overrides {@code match}, e.g. context blocks, loops or value-checking literals). + */ +public final class MatchProgramElementInstruction implements MatchInstruction { + + private final Class kind; + private final int childCount; + + public MatchProgramElementInstruction(Class kind, int childCount) { + this.kind = kind; + this.childCount = childCount; + } + + @Override + public @Nullable MatchResultInfo match(SyntaxElement actualElement, + MatchResultInfo matchConditions, LogicServices services) { + if (actualElement.getClass() == kind && actualElement.getChildCount() == childCount) { + return matchConditions; + } + return null; + } +} diff --git a/key.core/src/main/java/de/uka/ilkd/key/rule/match/vm/instructions/MatchSubProgramInstruction.java b/key.core/src/main/java/de/uka/ilkd/key/rule/match/vm/instructions/MatchSubProgramInstruction.java new file mode 100644 index 00000000000..7578fd0dc59 --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/rule/match/vm/instructions/MatchSubProgramInstruction.java @@ -0,0 +1,39 @@ +/* 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.match.vm.instructions; + +import de.uka.ilkd.key.logic.JavaBlock; + +import org.key_project.logic.LogicServices; +import org.key_project.logic.SyntaxElement; +import org.key_project.prover.rules.instantiation.MatchResultInfo; +import org.key_project.prover.rules.matcher.vm.VMProgramInterpreter; +import org.key_project.prover.rules.matcher.vm.instruction.MatchInstruction; + +import org.jspecify.annotations.Nullable; + +/** + * Matches the Java program of a modality by running a sub-program of {@code VMInstruction}s over + * the + * program tree (with its own cursor), instead of the monolithic {@code MatchProgramInstruction} + * which delegates to the separate {@code ProgramElement.match} AST matcher. The current element is + * the modality's {@link JavaBlock} (as for {@code MatchProgramInstruction}); the sub-program runs + * on + * its {@code program()}, leaving the outer cursor at the {@code JavaBlock} so the surrounding + * navigation is unchanged. + */ +public final class MatchSubProgramInstruction implements MatchInstruction { + + private final VMProgramInterpreter program; + + public MatchSubProgramInstruction(VMProgramInterpreter program) { + this.program = program; + } + + @Override + public @Nullable MatchResultInfo match(SyntaxElement actualElement, + MatchResultInfo matchConditions, LogicServices services) { + return program.match(((JavaBlock) actualElement).program(), matchConditions, services); + } +} diff --git a/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/JmlFacade.java b/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/JmlFacade.java index 80b93be0ce9..c06f0143751 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/JmlFacade.java +++ b/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/JmlFacade.java @@ -39,6 +39,21 @@ private JmlFacade() { return new JmlLexer(stream); } + /** + * Releases the ANTLR prediction (DFA) cache of the JML parser. It is a pure, lazily-built cache + * held on the generated parser's static fields, only needed while parsing, not during proof + * search; ANTLR rebuilds it transparently on the next parse. See + * {@code ParsingFacade.clearParserCaches}. + */ + public static void clearCaches() { + try { + new JmlParser(new CommonTokenStream(createLexer(CharStreams.fromString("")))) + .getInterpreter().clearDFA(); + } catch (RuntimeException ignored) { + // best-effort cache release; a failure here only forgoes the memory saving + } + } + /** * Creates a JML lexer for the given string with position. The position information of the lexer * is changed accordingly. diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/BuiltInRuleAppContainer.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/BuiltInRuleAppContainer.java index cbcb861dd3f..b52f6df4541 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/strategy/BuiltInRuleAppContainer.java +++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/BuiltInRuleAppContainer.java @@ -101,7 +101,8 @@ private PosInOccurrence getPosInOccurrence(Goal p_goal) { static RuleAppContainer createAppContainer(IBuiltInRuleApp bir, PosInOccurrence pio, Goal goal) { - final RuleAppCost cost = goal.getGoalStrategy().computeCost(bir, pio, goal); + final RuleAppCost cost = + withAge(goal.getGoalStrategy().computeCost(bir, pio, goal), goal); return new BuiltInRuleAppContainer(bir, pio, cost, goal); } diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/CostReuse.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/CostReuse.java new file mode 100644 index 00000000000..87e1731d3ac --- /dev/null +++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/CostReuse.java @@ -0,0 +1,238 @@ +/* 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.strategy; + +import java.lang.reflect.Array; +import java.lang.reflect.Field; +import java.lang.reflect.Modifier; +import java.util.*; +import java.util.concurrent.ConcurrentHashMap; + +import de.uka.ilkd.key.strategy.feature.AbstractNonDuplicateAppFeature; +import de.uka.ilkd.key.strategy.feature.NonDuplicateAppFeature; +import de.uka.ilkd.key.strategy.feature.RuleSetDispatchFeature; + +import org.key_project.prover.rules.Taclet; +import org.key_project.prover.strategy.costbased.feature.CostLocal; +import org.key_project.prover.strategy.costbased.feature.CostNonLocal; +import org.key_project.prover.strategy.costbased.feature.Feature; +import org.key_project.prover.strategy.costbased.termgenerator.TermGenerator; + +import org.jspecify.annotations.Nullable; + +/** + * Phase-2 cost reuse (perf round 3): decide whether a taclet's strategy cost is a pure function of + * the rule app and its find-position subterm (plus the always-recomputed age term and + * {@code NonDuplicateApp}-family vetoes). For such "cost-local" taclets the base re-cost performed + * by {@link TacletAppContainer#createFurtherApps} on every peek round can be replaced by arithmetic + * (carry the stored cost forward, refresh only the age term), avoiding the dominant + * {@code Strategy.computeCost} work. + * + *

Classification (sound-by-construction, default-impure)

+ * A taclet is eligible iff every {@link Feature} reachable in its per-taclet cost bindings resolves + * to local. Per feature, in order: + *
    + *
  1. veto ({@link AbstractNonDuplicateAppFeature}): a 0/Top guard. Collected and re-checked + * at reuse time (an app that became a duplicate must still be dropped); not descended into.
    2. + *
  2. explicit override: {@link CostNonLocal} forces non-local (the author wins).
    3. + *
  3. {@link CostLocal}: local. For a leaf that is the whole story; for a composite it means + * "transparent" -- the walk still recurses into its child features, so it stays local only if they + * all are. There is NO automatic "any feature with children is transparent" guess: a composite is + * trusted only because its author annotated it after checking that its own computation (including + * any non-Feature inputs such as projections/term-generators) is find-local. The transparent + * combinators are annotated once (Sum/Shannon/Scale/Let/ComprehendedSum/...).
    4. + *
  4. otherwise (unannotated): non-local (the SAFE default). A new feature -- leaf or + * composite -- is non-local until someone reviews it and adds {@link CostLocal}; forgetting costs + * only performance, never soundness.
    5. + *
+ * A {@link CostLocal} composite is local only if, in addition to its child features, every child + * {@link TermGenerator} it holds is also {@link CostLocal} -- a generator is a non-Feature input + * that decides locality (e.g. {@code SuperTermGenerator} is find-local, {@code + * SequentFormulasGenerator} reads the whole sequent and is not). The walk descends only through + * {@link Feature}- and {@link TermGenerator}-typed references (never arbitrary objects): the live + * feature tree holds mutable scratch state (e.g. TermBuffers) that must not be traversed. + * + *

+ * Optional verification (-Dkey.strategy.costReuse.verify): when reuse is applied also + * recompute the cost and log a warning on any mismatch -- a development aid to catch a feature that + * is mis-classified local (it should then get {@link CostNonLocal}). + */ +public final class CostReuse { + + public static final boolean VERIFY = Boolean.getBoolean("key.strategy.costReuse.verify"); + + private static final org.slf4j.Logger LOGGER = + org.slf4j.LoggerFactory.getLogger(CostReuse.class); + + private CostReuse() {} + + private static volatile @Nullable List dispatchers; + /** + * taclet -> collected veto features. An ELIGIBLE taclet always has at least the top-level + * NonDuplicateApp veto, so an empty array is used as the INELIGIBLE sentinel (ConcurrentHashMap + * forbids null values). + */ + private static final Map classification = new ConcurrentHashMap<>(); + /** Per-class locality decision, cached (class annotations are stable for the JVM run). */ + private static final Map, Kind> kindCache = new ConcurrentHashMap<>(); + /** Cached "not eligible for reuse" marker (the map forbids null values). */ + private static final Feature[] INELIGIBLE = new Feature[0]; + + private enum Kind { + VETO, NON_LOCAL, LOCAL + } + + /** + * @return the {@link AbstractNonDuplicateAppFeature} vetoes to re-check for a cost-local + * taclet, + * or {@code null} if the taclet is not eligible for cost reuse. + */ + public static Feature @Nullable [] vetoesIfEligible(Object strategy, Taclet taclet) { + final Feature[] r = classification.computeIfAbsent(taclet, t -> { + final Feature[] res = classify(strategy, t); + return res == null ? INELIGIBLE : res; + }); + return r == INELIGIBLE ? null : r; + } + + private static Feature @Nullable [] classify(Object strategy, Taclet taclet) { + final Set vetoes = Collections.newSetFromMap(new IdentityHashMap<>()); + vetoes.add(NonDuplicateAppFeature.INSTANCE); // top-level veto, applies to every taclet + final boolean[] local = { true }; + final Set seen = Collections.newSetFromMap(new IdentityHashMap<>()); + for (RuleSetDispatchFeature d : dispatchers(strategy)) { + var rs = taclet.getRuleSets(); + while (!rs.isEmpty()) { + final Feature f = d.get(rs.head()); + if (f != null) { + walk(f, vetoes, local, seen); + } + rs = rs.tail(); + } + } + return local[0] ? vetoes.toArray(new Feature[0]) : null; + } + + /** + * Classify a feature; for a transparent composite, recurse into its child features and require + * its child term-generators to be local too (see the class comment). + */ + private static void walk(Feature f, Set vetoes, boolean[] local, Set seen) { + if (!local[0] || !seen.add(f)) { + return; + } + switch (kind(f)) { + case VETO -> vetoes.add(f); + case NON_LOCAL -> local[0] = false; + // LOCAL: a leaf is done; a composite stays local iff all its child FEATURES are local + // AND all its child TERM-GENERATORS are local. The generator matters because e.g. + // ComprehendedSumFeature sums its body over a generator: SuperTermGenerator (find + // ancestors) is local, but SequentFormulasGenerator (whole sequent) is not -- and a + // generator is a non-Feature input the feature recursion would otherwise miss. + case LOCAL -> forEachChild(f, child -> { + if (child instanceof Feature cf) { + walk(cf, vetoes, local, seen); + } else if (!isLocal(child.getClass())) { // a TermGenerator (or similar input) + local[0] = false; + } + }); + } + } + + /** + * A non-Feature classifying input (e.g. a TermGenerator) is local only if {@link CostLocal}. + */ + private static boolean isLocal(Class c) { + return !c.isAnnotationPresent(CostNonLocal.class) && c.isAnnotationPresent(CostLocal.class); + } + + /** + * Classify a feature's class (cached). SOUND-by-construction: a feature is treated as local + * ONLY if it is explicitly {@link CostLocal}-annotated (its author asserts it depends only on + * the app + find subterm, modulo its child features) -- there is no structural "any composite + * is transparent" guess. {@link CostNonLocal} forces non-local; everything unannotated is + * non-local (the safe default). + */ + private static Kind kind(Feature f) { + return kindCache.computeIfAbsent(f.getClass(), c -> { + if (c.isAnnotationPresent(CostNonLocal.class)) { + return Kind.NON_LOCAL; // explicit author override wins + } + if (f instanceof AbstractNonDuplicateAppFeature) { + return Kind.VETO; + } + return c.isAnnotationPresent(CostLocal.class) ? Kind.LOCAL : Kind.NON_LOCAL; + }); + } + + /** + * Apply {@code action} to each {@link Feature} and {@link TermGenerator} held one structural + * step inside {@code f}. + */ + private static void forEachChild(Feature f, java.util.function.Consumer action) { + for (Field fld : allFields(f.getClass())) { + if (Modifier.isStatic(fld.getModifiers()) || fld.getType().isPrimitive()) { + continue; + } + try { + fld.setAccessible(true); + follow(fld.get(f), action); + } catch (Throwable ignored) { + } + } + } + + private static void follow(@Nullable Object o, java.util.function.Consumer action) { + if (o == null) { + return; + } + if (o instanceof Feature || o instanceof TermGenerator) { + action.accept(o); + return; + } + Class c = o.getClass(); + if (c.isArray()) { + if (!c.getComponentType().isPrimitive()) { + int n = Array.getLength(o); + for (int i = 0; i < n; i++) { + follow(Array.get(o, i), action); + } + } + return; + } + if (o instanceof Iterable it) { + for (Object e : it) { + follow(e, action); + } + } + // other object types (TermBuffer, ProjectionToTerm, Name, ...) are NOT traversed + } + + /** + * Verification aid (only when {@link #VERIFY}): warn if a reused cost differs from the freshly + * recomputed one, i.e. some feature is mis-classified local and should be {@link CostNonLocal}. + */ + static void warnMismatch(Taclet taclet, Object reused, Object fresh) { + LOGGER.warn("cost-reuse mismatch for taclet {}: a feature is mis-classified local; " + + "annotate it @CostNonLocal (reused={}, fresh={})", taclet.name(), reused, fresh); + } + + private static List dispatchers(Object strategy) { + List d = dispatchers; + if (d == null) { + d = strategy instanceof ModularJavaDLStrategy m ? m.costRuleSetDispatchers() + : List.of(); + dispatchers = d; + } + return d; + } + + private static List allFields(Class c) { + List fs = new ArrayList<>(); + for (Class k = c; k != null && k != Object.class; k = k.getSuperclass()) { + fs.addAll(Arrays.asList(k.getDeclaredFields())); + } + return fs; + } +} diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/FIFOStrategy.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/FIFOStrategy.java index 9aaac0ef5a5..90319d42885 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/strategy/FIFOStrategy.java +++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/FIFOStrategy.java @@ -40,7 +40,9 @@ private FIFOStrategy() { PosInOccurrence pio, Goal goal, MutableState mState) { - return NumberRuleAppCost.create(((de.uka.ilkd.key.proof.Goal) goal).getTime()); + // FIFO ordering is purely the goal age, which RuleAppContainer.withAge adds once per + // container, so the age-free strategy cost is zero. + return NumberRuleAppCost.getZeroCost(); } /** diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/FindTacletAppContainer.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/FindTacletAppContainer.java index 886be2b0b58..1892a519177 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/strategy/FindTacletAppContainer.java +++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/FindTacletAppContainer.java @@ -49,14 +49,15 @@ public class FindTacletAppContainer extends TacletAppContainer { * * @param app the taclet application * @param pio the position in occurrence - * @param cost the rule application cost + * @param ageFreeCost the rule application cost without the goal-age term + * @param cost the rule application cost (age-free cost plus the goal-age term) * @param goal the goal to apply the taclet on * @param age the age */ FindTacletAppContainer(NoPosTacletApp app, PosInOccurrence pio, - RuleAppCost cost, Goal goal, + RuleAppCost ageFreeCost, RuleAppCost cost, Goal goal, long age) { - super(app, cost, age); + super(app, ageFreeCost, cost, age); applicationPosition = pio; final FormulaTag posTag = goal.getFormulaTagManager().getTagForPos(pio.topLevel()); diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/ModularJavaDLStrategy.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/ModularJavaDLStrategy.java index e7f9bce2798..9e9923a3024 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/strategy/ModularJavaDLStrategy.java +++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/ModularJavaDLStrategy.java @@ -10,7 +10,6 @@ import de.uka.ilkd.key.proof.Goal; import de.uka.ilkd.key.proof.Proof; import de.uka.ilkd.key.strategy.ComponentStrategy.StrategyAspect; -import de.uka.ilkd.key.strategy.feature.AgeFeature; import de.uka.ilkd.key.strategy.feature.MatchedAssumesFeature; import de.uka.ilkd.key.strategy.feature.NonDuplicateAppFeature; import de.uka.ilkd.key.strategy.feature.RuleSetDispatchFeature; @@ -57,6 +56,9 @@ public class ModularJavaDLStrategy extends AbstractFeatureStrategy { private final ResponsibleStrategyCache responsibleStrategyCache; + /// the conflict-resolution cost dispatcher; kept for {@link #costRuleSetDispatchers} + private final RuleSetDispatchFeature conflictCostDispatcher; + public ModularJavaDLStrategy(Proof proof, List componentStrategies, StrategyProperties properties) { super(proof); @@ -69,7 +71,7 @@ public ModularJavaDLStrategy(Proof proof, List componentStrat // if more than one strategy is responsible for a _ruleset_ we need to determine how to // resolve the // competing computations - RuleSetDispatchFeature conflictCostDispatcher = resolveConflicts(); + conflictCostDispatcher = resolveConflicts(); final Feature ifMatchedF = ifZero(MatchedAssumesFeature.INSTANCE, longConst(+1)); Feature reduceCostTillMaxF = new ReduceTillMaxFeature(Feature::computeCost, @@ -80,10 +82,12 @@ public ModularJavaDLStrategy(Proof proof, List componentStrat (rule) -> responsibleStrategyCache.getResponsibleStrategies(rule, strategies, StrategyAspect.Instantiation)); - // the feature for the cost computation + // the feature for the cost computation. Age (goal time) is NOT part of the strategy cost: + // it is a first-class container-level term added once by RuleAppContainer.withAge, so the + // cost here is age-free (this lets cost reuse carry the age-free base forward verbatim). totalCost = add(AutomatedRuleFeature.getInstance(), ifMatchedF, NonDuplicateAppFeature.INSTANCE, - reduceCostTillMaxF, conflictCostDispatcher, AgeFeature.INSTANCE); + reduceCostTillMaxF, conflictCostDispatcher); // The feature for instantiateApp, built once instead of on every call. // Note that no conflict dispatcher takes part in this sum: resolveConflicts() @@ -93,10 +97,28 @@ public ModularJavaDLStrategy(Proof proof, List componentStrat enableInstantiate(); totalInstCost = add(AutomatedRuleFeature.getInstance(), ifMatchedF, NonDuplicateAppFeature.INSTANCE, - reduceInstTillMaxF, AgeFeature.INSTANCE); + reduceInstTillMaxF); disableInstantiate(); } + /** + * The {@link RuleSetDispatchFeature}s that contribute to a rule's COST (the conflict-resolution + * dispatcher plus each component strategy's cost dispatcher). Exposed for {@link CostReuse}'s + * feature-locality classification, which must NOT reach this via reflection from the strategy + * object (that would traverse the live proof graph the strategy references). + */ + public List costRuleSetDispatchers() { + final List result = new ArrayList<>(); + result.add(conflictCostDispatcher); + for (ComponentStrategy s : strategies) { + final RuleSetDispatchFeature d = s.getDispatcher(StrategyAspect.Cost); + if (d != null) { + result.add(d); + } + } + return result; + } + private record StratAndDispatcher(ComponentStrategy strategy, RuleSetDispatchFeature dispatcher) { } diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/NoFindTacletAppContainer.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/NoFindTacletAppContainer.java index c1ca6c8fb87..9a521d58451 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/strategy/NoFindTacletAppContainer.java +++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/NoFindTacletAppContainer.java @@ -13,8 +13,9 @@ */ public class NoFindTacletAppContainer extends TacletAppContainer { - NoFindTacletAppContainer(NoPosTacletApp p_app, RuleAppCost p_cost, long p_age) { - super(p_app, p_cost, p_age); + NoFindTacletAppContainer(NoPosTacletApp p_app, RuleAppCost p_ageFreeCost, RuleAppCost p_cost, + long p_age) { + super(p_app, p_ageFreeCost, p_cost, p_age); } /** diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/QueueRuleApplicationManager.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/QueueRuleApplicationManager.java index ff7fbb523af..5c56c0cf2a7 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/strategy/QueueRuleApplicationManager.java +++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/QueueRuleApplicationManager.java @@ -5,13 +5,27 @@ import java.util.ArrayList; import java.util.Iterator; +import java.util.LinkedHashMap; +import java.util.LinkedHashSet; +import java.util.List; +import java.util.Map; import java.util.concurrent.atomic.AtomicLong; +import de.uka.ilkd.key.logic.JTerm; +import de.uka.ilkd.key.logic.op.UpdateApplication; import de.uka.ilkd.key.proof.Goal; +import de.uka.ilkd.key.rule.NoPosTacletApp; +import de.uka.ilkd.key.rule.inst.SVInstantiations; +import org.key_project.logic.op.Operator; +import org.key_project.logic.op.sv.SchemaVariable; import org.key_project.prover.proof.ProofGoal; import org.key_project.prover.rules.RuleApp; +import org.key_project.prover.sequent.FormulaChangeInfo; import org.key_project.prover.sequent.PosInOccurrence; +import org.key_project.prover.sequent.Sequent; +import org.key_project.prover.sequent.SequentChangeInfo; +import org.key_project.prover.sequent.SequentFormula; import org.key_project.prover.strategy.RuleApplicationManager; import org.key_project.prover.strategy.costbased.MutableState; import org.key_project.prover.strategy.costbased.RuleAppCost; @@ -67,6 +81,47 @@ public class QueueRuleApplicationManager implements RuleApplicationManager private long nextRuleTime; + /** + * Parked assumes-incomplete taclet bases, indexed by the concrete top operator(s) of their + * {@code \assumes} formulas. Such bases re-expand to nothing (no new assumes match) on almost + * every round (profiling: 96.8% of queue pops fail at the unmatched {@code \assumes}, and + * 97-99.6% of the resulting re-expansions yield no new instance -- the dominant remaining queue + * churn), so instead of re-popping and re-expanding them each round they are parked here and + * woken only when a formula they could match appears. A base is stored under each of its wake + * operators and woken when any of them is added/modified. Insertion-ordered for determinism; + * {@code null} until the first base is parked. + *

+ * Sound (byte-identical) by construction, unlike the earlier sequent-growth heuristic: + *

    + *
  • Only effectively-indexable bases are parked -- every {@code \assumes} formula's + * top operator is concrete or a schema variable already bound by the find-match (see + * {@link #assumesWakeOps}). Bases with an unbound-generic top (which would match any formula) + * are never parked; they stay in the active queue and re-expand every round exactly as without + * parking.
    • + *
  • A parked base is woken (re-inserted into the active queue) on exactly the round a formula + * with a matching top operator is added or modified ({@link #sequentChanged}/{@code + * pendingWakeOps}) -- the same round its non-parked counterpart would first see that formula as + * "new" and re-expand to the instance. So the instance enters the queue at the identical round, + * with the identical (current) age and cost, and the proof is byte-identical.
    • + *
  • The wake set is a sound superset: it walks the changed formula's update-prefix + * spine of operators (the assumes matcher strips the update context before matching, see + * {@code VMTacletMatcher.matchUpdateContext}). Over-waking is harmless -- a spuriously woken + * base + * is popped, re-expands to nothing, and is re-parked, exactly as a non-parked base would behave + * that round. Only missing a wake would diverge, and that cannot happen for an + * effectively-indexable base.
    • + *
  • All structures are insertion-ordered ({@link LinkedHashMap}/{@link LinkedHashSet}) so + * parking introduces no non-determinism.
    • + *
+ */ + private @Nullable LinkedHashMap> parkedByOp = null; + /** + * Top operators (along the update-prefix spine) of formulas added/modified since the previous + * round; the wake candidates consumed at the start of the next round. Insertion-ordered for + * determinism; {@code null} until the first change is recorded. + */ + private @Nullable LinkedHashSet pendingWakeOps = null; + @Override public void setGoal(Goal p_goal) { goal = p_goal; @@ -79,6 +134,8 @@ public void setGoal(Goal p_goal) { public void clearCache() { queue = null; previousMinimum = null; + parkedByOp = null; + pendingWakeOps = null; if (goal != null) { goal.proof().getServices().getCaches().getIfInstantiationCache().releaseAll(); } @@ -279,11 +336,20 @@ private void computeNextRuleApp(ImmutableHeap<@NonNull RuleAppContainer> further */ ImmutableList workingList = ImmutableSLList.nil(); + // Wake parked assumes-bases whose \assumes top operator matches a formula added/modified + // since the last round, re-inserting them into the active queue so they re-expand during + // THIS + // round -- the identical round their non-parked counterparts would first see that formula + // as + // new. No completeness net is needed (or wanted): an effectively-indexable base is always + // woken on its matching round, and a late re-injection would surface its instance at the + // wrong round, the very divergence parking must avoid. + wakeParkedBases(); + /* * Try to find a rule app that can be completed until both queues are exhausted. */ while (nextRuleApp == null && !(queue.isEmpty() && furtherAppsQueue.isEmpty())) { - /* * Determine the minimum rule app container, ranging over both queues. Putting this into * a separate method would be convenient. But since we are using immutable data @@ -353,11 +419,24 @@ private void computeNextRuleApp(ImmutableHeap<@NonNull RuleAppContainer> further * Create further apps if found in main queue. Rule apps obtained this way will * be considered during the current round. */ + final ImmutableList further = + minRuleAppContainer.createFurtherApps(goal); + // Empty assumes yield (the re-expansion is just the re-costed base itself, with + // the now-current age): if the base is effectively indexable, park it instead + // of + // re-adding so it stops being re-popped every round. Park further.head() (the + // freshly re-costed container) so the parked age advances exactly as the + // non-parked base's would, keeping later assumes matches from re-deriving stale + // instances. A non-indexable base falls through and is re-added unchanged. + if (further.size() == 1 + && further.head() instanceof TacletAppContainer base + && !base.getTacletApp().assumesInstantionsComplete() + && park(base)) { + continue; + } var time = System.nanoTime(); try { - furtherAppsQueue = - push(minRuleAppContainer.createFurtherApps(goal).iterator(), - furtherAppsQueue); + furtherAppsQueue = push(further.iterator(), furtherAppsQueue); } finally { PERF_QUEUE_OPS.addAndGet(System.nanoTime() - time); } @@ -382,6 +461,170 @@ private void computeNextRuleApp(ImmutableHeap<@NonNull RuleAppContainer> further } } + // --------------------------------------------------------------------------------------------- + // Assumes-base parking (see parkedByOp) + // --------------------------------------------------------------------------------------------- + + /** + * Park an assumes-incomplete base, indexing it under the top operator(s) of its + * {@code \assumes} + * formulas so it can be woken when a matching formula appears. + * + * @param base the re-costed base container to park (carries the current age) + * @return {@code true} if the base was parked; {@code false} if it is not effectively indexable + * (an unbound-generic {@code \assumes} top), in which case the caller must keep it in + * the + * active queue + */ + private boolean park(TacletAppContainer base) { + final List ops = assumesWakeOps(base); + if (ops == null) { + return false; + } + if (parkedByOp == null) { + parkedByOp = new LinkedHashMap<>(); + } + for (Operator op : ops) { + parkedByOp.computeIfAbsent(op, k -> new LinkedHashSet<>()).add(base); + } + return true; + } + + /** + * Re-insert into the active queue every parked base waiting on an operator that was added or + * modified since the previous round (see {@link #pendingWakeOps}). Woken bases are collected in + * insertion order (deterministic) and removed from all their index buckets. + */ + private void wakeParkedBases() { + if (pendingWakeOps == null) { + return; + } + if (parkedByOp != null && !parkedByOp.isEmpty()) { + LinkedHashSet woken = null; + for (Operator op : pendingWakeOps) { + final LinkedHashSet bucket = parkedByOp.get(op); + if (bucket != null) { + if (woken == null) { + woken = new LinkedHashSet<>(); + } + woken.addAll(bucket); + } + } + if (woken != null) { + for (RuleAppContainer c : woken) { + unindexParked(c); + } + var time = System.nanoTime(); + try { + queue = queue.insert(woken.iterator()); + } finally { + PERF_QUEUE_OPS.addAndGet(System.nanoTime() - time); + } + } + } + pendingWakeOps.clear(); + } + + /** Remove a woken container from every operator bucket it was parked under. */ + private void unindexParked(RuleAppContainer c) { + if (parkedByOp == null || !(c instanceof TacletAppContainer tac)) { + return; + } + final List ops = assumesWakeOps(tac); + if (ops == null) { + return; + } + for (Operator op : ops) { + final LinkedHashSet bucket = parkedByOp.get(op); + if (bucket != null) { + bucket.remove(c); + if (bucket.isEmpty()) { + parkedByOp.remove(op); + } + } + } + } + + /** + * The concrete top operator(s) of the {@code \assumes} formulas of the given base, resolved + * through the find-match's schema-variable instantiations. + * + * @return the wake operators, or {@code null} if the base is not effectively indexable + * -- i.e. some {@code \assumes} formula has a top that is an unbound schema variable + * (it + * would match any formula, so no precise wake operator exists) or has no + * {@code \assumes} + * formulas at all + */ + private static @Nullable List assumesWakeOps(TacletAppContainer base) { + final NoPosTacletApp app = base.getTacletApp(); + final Sequent assumesSeq = app.taclet().assumesSequent(); + if (assumesSeq.isEmpty()) { + return null; + } + final SVInstantiations insts = app.instantiations(); + final List ops = new ArrayList<>(assumesSeq.size()); + for (SequentFormula sf : assumesSeq) { + Operator op = sf.formula().op(); + if (op instanceof SchemaVariable sv) { + final Object inst = insts.getInstantiation(sv); + if (!(inst instanceof JTerm instTerm)) { + return null; // unbound (or non-term) generic top -> not indexable + } + op = instTerm.op(); + if (op instanceof SchemaVariable) { + return null; // still schematic -> not indexable + } + } + ops.add(op); + } + return ops; + } + + /** + * Record, for the next round's wake-up, the top operators of every formula added or modified by + * this sequent change. The assumes matcher strips the update context before matching, so the + * whole update-prefix spine of each changed formula is recorded -- a sound superset of the + * operators a parked base could match (see {@link #parkedByOp}). Called by {@code Goal} on + * every + * sequent change. + */ + public void sequentChanged(SequentChangeInfo sci) { + recordWakeOps(sci.addedFormulas(true)); + recordWakeOps(sci.addedFormulas(false)); + recordModifiedWakeOps(sci.modifiedFormulas(true)); + recordModifiedWakeOps(sci.modifiedFormulas(false)); + } + + private void recordWakeOps(ImmutableList added) { + for (SequentFormula sf : added) { + recordSpineOps(sf.formula()); + } + } + + private void recordModifiedWakeOps(ImmutableList modified) { + for (FormulaChangeInfo fci : modified) { + recordSpineOps(fci.newFormula().formula()); + } + } + + /** Add the operators along a formula's update-application spine to {@link #pendingWakeOps}. */ + private void recordSpineOps(org.key_project.logic.Term formula) { + if (pendingWakeOps == null) { + pendingWakeOps = new LinkedHashSet<>(); + } + org.key_project.logic.Term t = formula; + while (true) { + final Operator op = t.op(); + pendingWakeOps.add(op); + if (op instanceof UpdateApplication && t instanceof JTerm jt) { + t = UpdateApplication.getTarget(jt); + } else { + break; + } + } + } + @Override public RuleApplicationManager copy() { // noinspection unchecked @@ -393,6 +636,19 @@ public Object clone() { QueueRuleApplicationManager res = new QueueRuleApplicationManager(); res.queue = queue; res.previousMinimum = previousMinimum; + // the parking structures are mutable and goal-local: deep-copy so split goals park/wake + // independently (the contained containers and operators are immutable and shared) + if (parkedByOp != null) { + final LinkedHashMap> copy = + new LinkedHashMap<>(parkedByOp.size()); + for (Map.Entry> e : parkedByOp.entrySet()) { + copy.put(e.getKey(), new LinkedHashSet<>(e.getValue())); + } + res.parkedByOp = copy; + } + if (pendingWakeOps != null) { + res.pendingWakeOps = new LinkedHashSet<>(pendingWakeOps); + } return res; } diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/RuleAppContainer.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/RuleAppContainer.java index 5e622bbb551..cba962e6a06 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/strategy/RuleAppContainer.java +++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/RuleAppContainer.java @@ -10,6 +10,7 @@ import org.key_project.prover.rules.RuleApp; import org.key_project.prover.sequent.PosInOccurrence; +import org.key_project.prover.strategy.costbased.NumberRuleAppCost; import org.key_project.prover.strategy.costbased.RuleAppCost; import org.key_project.util.collection.ImmutableList; import org.key_project.util.collection.ImmutableSLList; @@ -61,6 +62,18 @@ public final RuleAppCost getCost() { return cost; } + /** + * Add the goal-age term to a strategy-computed cost. Age (the goal time, i.e. number of rules + * applied so far) is a single first-class component of every container's cost, contributed here + * rather than inside any {@link de.uka.ilkd.key.strategy.Strategy#computeCost} -- so a strategy + * (and each of its components) computes only its age-free cost, and age is added exactly once + * per queued container regardless of how strategies are composed. {@code Top} stays + * {@code Top}. + */ + protected static RuleAppCost withAge(RuleAppCost ageFreeCost, Goal goal) { + return ageFreeCost.add(NumberRuleAppCost.create(goal.getTime())); + } + /** * Create container for a RuleApp. * diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/SimpleFilteredStrategy.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/SimpleFilteredStrategy.java index 7c20b783df1..b532efeb4b2 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/strategy/SimpleFilteredStrategy.java +++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/SimpleFilteredStrategy.java @@ -66,7 +66,9 @@ public Name name() { return res; } - long cost = ((de.uka.ilkd.key.proof.Goal) goal).getTime(); + // The goal-age ordering is added once by RuleAppContainer.withAge; only the age-free + // malus remains in the strategy cost. + long cost = 0; if (app instanceof TacletApp tacletApp && !tacletApp.assumesInstantionsComplete()) { cost += IF_NOT_MATCHED_MALUS; } diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/TacletAppContainer.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/TacletAppContainer.java index 22282daa683..75ec1d7eab1 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/strategy/TacletAppContainer.java +++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/TacletAppContainer.java @@ -18,12 +18,17 @@ import org.key_project.prover.rules.instantiation.AssumesFormulaInstantiation; import org.key_project.prover.sequent.PosInOccurrence; import org.key_project.prover.sequent.Sequent; +import org.key_project.prover.strategy.costbased.MutableState; +import org.key_project.prover.strategy.costbased.NumberRuleAppCost; import org.key_project.prover.strategy.costbased.RuleAppCost; import org.key_project.prover.strategy.costbased.TopRuleAppCost; +import org.key_project.prover.strategy.costbased.feature.Feature; import org.key_project.util.collection.ImmutableList; import org.key_project.util.collection.ImmutableSLList; import org.key_project.util.collection.ImmutableSet; +import org.jspecify.annotations.Nullable; + /** * Instances of this class are immutable */ @@ -36,13 +41,32 @@ public abstract class TacletAppContainer extends RuleAppContainer { // save any memory (at the moment). // This is because Java's memory alingment. + /** + * Creation time of this container ({@code -1} for an initial/just-loaded container). Since age + * became a first-class container-level cost term ({@link RuleAppContainer#withAge}) this field + * no longer feeds the cost; it is purely the {@link AssumesInstantiator} freshness key (was + * this + * container built before or after a given if-formula). + */ private final long age; + /** + * The age-free strategy cost: {@code getCost()} without the goal-age term that + * {@link RuleAppContainer#withAge} adds. Stored so cost reuse can carry it forward unchanged + * across re-expansion and only re-add the current age, with no reconstruction arithmetic. + */ + private final RuleAppCost ageFreeCost; - protected TacletAppContainer(RuleApp p_app, RuleAppCost p_cost, long p_age) { + protected TacletAppContainer(RuleApp p_app, RuleAppCost p_ageFreeCost, RuleAppCost p_cost, + long p_age) { super(p_app, p_cost); + ageFreeCost = p_ageFreeCost; age = p_age; } + RuleAppCost getAgeFreeCost() { + return ageFreeCost; + } + protected NoPosTacletApp getTacletApp() { return (NoPosTacletApp) getRuleApp(); } @@ -66,14 +90,15 @@ protected static TacletAppContainer createContainer(NoPosTacletApp p_app, private static TacletAppContainer createContainer(NoPosTacletApp p_app, PosInOccurrence p_pio, - Goal p_goal, RuleAppCost p_cost, boolean p_initial) { + Goal p_goal, RuleAppCost p_ageFreeCost, boolean p_initial) { // This relies on the fact that the method Goal.getTime() // never returns a value less than zero final long localage = p_initial ? -1 : p_goal.getTime(); + final RuleAppCost cost = withAge(p_ageFreeCost, p_goal); if (p_pio == null) { - return new NoFindTacletAppContainer(p_app, p_cost, localage); + return new NoFindTacletAppContainer(p_app, p_ageFreeCost, cost, localage); } else { - return new FindTacletAppContainer(p_app, p_pio, p_cost, p_goal, localage); + return new FindTacletAppContainer(p_app, p_pio, p_ageFreeCost, cost, p_goal, localage); } } @@ -88,7 +113,11 @@ public final ImmutableList createFurtherApps(Goal p_goal) { return ImmutableSLList.nil(); } - final TacletAppContainer newCont = createContainer(p_goal); + final TacletAppContainer newCont = costLocalReusedContainerOr(p_goal); + if (newCont == null) { + // a veto fired on the cost-local fast path: the re-costed base would be infinite + return ImmutableSLList.nil(); + } if (newCont.getCost() instanceof TopRuleAppCost) { return ImmutableSLList.nil(); } @@ -183,6 +212,45 @@ private TacletAppContainer createContainer(Goal p_goal) { return createContainer(getTacletApp(), getPosInOccurrence(p_goal), p_goal, false); } + /** + * Re-cost the base app for {@link #createFurtherApps}. On the cost-reuse fast path (taclet + * classified cost-local by {@link CostReuse}, numeric age-free cost) the full + * {@link de.uka.ilkd.key.strategy.Strategy#computeCost} is skipped: the stored age-free cost is + * carried forward verbatim and {@link RuleAppContainer#withAge} re-adds the current goal age + * when the new container is built -- no reconstruction arithmetic, and initial containers + * (age {@code -1}) reuse soundly too, since age is no longer part of the stored cost. The + * {@code NonDuplicateApp}-family vetoes that contribute are re-evaluated first; if one fires + * the + * full cost would be {@link TopRuleAppCost}, so {@code null} is returned (drop the app). + * Otherwise, and whenever reuse is disabled/inapplicable, falls back to the normal recompute. + */ + private @Nullable TacletAppContainer costLocalReusedContainerOr(Goal p_goal) { + if (getAgeFreeCost() instanceof NumberRuleAppCost base) { + final Feature[] vetoes = + CostReuse.vetoesIfEligible(p_goal.getGoalStrategy(), getTacletApp().taclet()); + if (vetoes != null) { + final PosInOccurrence pos = getPosInOccurrence(p_goal); + final MutableState mState = new MutableState(); + for (Feature veto : vetoes) { + if (veto.computeCost(getTacletApp(), pos, p_goal, + mState) instanceof TopRuleAppCost) { + return null; + } + } + if (CostReuse.VERIFY) { + final RuleAppCost freshBase = + p_goal.getGoalStrategy().computeCost(getTacletApp(), pos, p_goal); + if (!base.equals(freshBase)) { + CostReuse.warnMismatch(getTacletApp().taclet(), base, freshBase); + } + } + // carry the age-free base forward; createContainer re-adds the current age + return createContainer(getTacletApp(), pos, p_goal, base, false); + } + } + return createContainer(p_goal); + } + /** * Create containers for NoFindTaclets. */ diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/AbstractMonomialSmallerThanFeature.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/AbstractMonomialSmallerThanFeature.java index 3c69ff78ab3..a99ae9ef628 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/AbstractMonomialSmallerThanFeature.java +++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/AbstractMonomialSmallerThanFeature.java @@ -44,8 +44,19 @@ protected int introductionTime(Operator op, Goal goal) { if (res == null) { res = introductionTimeHelp(op, goal); - synchronized (introductionTimeCache) { - introductionTimeCache.put(op, res); + // Do NOT cache the "not introduced (yet)" answer (-1): op may be introduced by a later + // rule application, after which introductionTimeHelp would find a real time. Caching + // the + // -1 would freeze it, making the value depend on whether op happened to be first + // queried + // before or after its introduction -- i.e. on the access pattern (which features run, + // when). That makes term ordering, and hence OneStepSimplifier rewriting, subtly + // non-deterministic. A real introduction time, once found, is stable (the introducing + // rule stays in the applied-rule prefix), so it is safe to cache. + if (res != -1) { + synchronized (introductionTimeCache) { + introductionTimeCache.put(op, res); + } } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/AgeFeature.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/AgeFeature.java deleted file mode 100644 index 3428ec49609..00000000000 --- a/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/AgeFeature.java +++ /dev/null @@ -1,34 +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.strategy.feature; - -import org.key_project.prover.proof.ProofGoal; -import org.key_project.prover.rules.RuleApp; -import org.key_project.prover.sequent.PosInOccurrence; -import org.key_project.prover.strategy.costbased.MutableState; -import org.key_project.prover.strategy.costbased.NumberRuleAppCost; -import org.key_project.prover.strategy.costbased.RuleAppCost; -import org.key_project.prover.strategy.costbased.feature.Feature; - -import org.jspecify.annotations.NonNull; - -/** - * Feature that computes the age of the goal (i.e. total number of rules applications that have been - * performed at the goal) to which a rule is supposed to be applied - */ -public class AgeFeature implements Feature { - - public static final Feature INSTANCE = new AgeFeature(); - - private AgeFeature() {} - - @Override - public > RuleAppCost computeCost(RuleApp app, - PosInOccurrence pos, Goal goal, MutableState mState) { - return NumberRuleAppCost.create(((de.uka.ilkd.key.proof.Goal) goal).getTime()); - // return LongRuleAppCost.create ( goal.getTime() / goal.sequent ().size () ); - // return LongRuleAppCost.create ( (long)Math.sqrt ( goal.getTime () ) ); - } - -} diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/CheckApplyEqFeature.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/CheckApplyEqFeature.java index 6cf5302230b..c9bbf5c347d 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/CheckApplyEqFeature.java +++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/CheckApplyEqFeature.java @@ -13,6 +13,7 @@ import org.key_project.prover.sequent.PIOPathIterator; import org.key_project.prover.sequent.PosInOccurrence; import org.key_project.prover.strategy.costbased.MutableState; +import org.key_project.prover.strategy.costbased.feature.CostLocal; import org.key_project.prover.strategy.costbased.feature.Feature; /** @@ -20,6 +21,7 @@ * rule application must not be one side of an equation that is the instantiation of the first * if-formula. If the rule application is admissible, zero is returned. */ +@CostLocal public class CheckApplyEqFeature extends BinaryTacletAppFeature { public static final Feature INSTANCE = new CheckApplyEqFeature(); diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/ComprehendedSumFeature.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/ComprehendedSumFeature.java index 2eabf7ed9ce..ec13ad5cd01 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/ComprehendedSumFeature.java +++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/ComprehendedSumFeature.java @@ -11,6 +11,7 @@ import org.key_project.prover.strategy.costbased.NumberRuleAppCost; import org.key_project.prover.strategy.costbased.RuleAppCost; import org.key_project.prover.strategy.costbased.TopRuleAppCost; +import org.key_project.prover.strategy.costbased.feature.CostLocal; import org.key_project.prover.strategy.costbased.feature.Feature; import org.key_project.prover.strategy.costbased.termProjection.TermBuffer; import org.key_project.prover.strategy.costbased.termgenerator.TermGenerator; @@ -21,6 +22,10 @@ * A feature that computes the sum of the values of a feature term when a given variable ranges over * a sequence of terms */ +// @CostLocal: transparent -- it sums its (recursed) body over a TermGenerator. CostReuse also +// classifies that generator: it stays local only with a find-local generator (e.g. +// SuperTermGenerator), and is non-local with a sequent-scanning one (SequentFormulasGenerator). +@CostLocal public class ComprehendedSumFeature> implements Feature { private final TermBuffer var; diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/FindRightishFeature.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/FindRightishFeature.java index a3ddddddbb5..cfbf42e18f3 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/FindRightishFeature.java +++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/FindRightishFeature.java @@ -14,6 +14,7 @@ import org.key_project.prover.strategy.costbased.MutableState; import org.key_project.prover.strategy.costbased.NumberRuleAppCost; import org.key_project.prover.strategy.costbased.RuleAppCost; +import org.key_project.prover.strategy.costbased.feature.CostLocal; import org.key_project.prover.strategy.costbased.feature.Feature; import org.jspecify.annotations.NonNull; @@ -23,6 +24,7 @@ * choose the left branch (subterm) and how the right branches. This is used to identify the * upper/righter/bigger summands in a polynomial that is arranged in a left-associated way. */ +@CostLocal public class FindRightishFeature implements Feature { private final Operator add; private final static RuleAppCost one = NumberRuleAppCost.create(1); diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/InstantiatedSVFeature.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/InstantiatedSVFeature.java index 650c6f6abac..30cda232d76 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/InstantiatedSVFeature.java +++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/InstantiatedSVFeature.java @@ -10,6 +10,7 @@ import org.key_project.logic.Name; import org.key_project.prover.sequent.PosInOccurrence; import org.key_project.prover.strategy.costbased.MutableState; +import org.key_project.prover.strategy.costbased.feature.CostLocal; import org.key_project.prover.strategy.costbased.feature.Feature; import org.key_project.prover.strategy.costbased.termProjection.ProjectionToTerm; @@ -17,6 +18,7 @@ * Feature that returns zero iff a certain schema variable is instantiated. If the schemavariable is * not instantiated schema variable or does not occur in the taclet infinity costs are returned. */ +@CostLocal public class InstantiatedSVFeature extends BinaryTacletAppFeature { private final ProjectionToTerm instProj; diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/MatchedAssumesFeature.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/MatchedAssumesFeature.java index d712c639ec5..ed53957cd49 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/MatchedAssumesFeature.java +++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/MatchedAssumesFeature.java @@ -8,12 +8,14 @@ import org.key_project.prover.sequent.PosInOccurrence; import org.key_project.prover.strategy.costbased.MutableState; +import org.key_project.prover.strategy.costbased.feature.CostLocal; import org.key_project.prover.strategy.costbased.feature.Feature; /** * Binary features that returns zero iff the if-formulas of a Taclet are instantiated or the Taclet * does not have any if-formulas. */ +@CostLocal public final class MatchedAssumesFeature extends BinaryTacletAppFeature { public static final Feature INSTANCE = new MatchedAssumesFeature(); diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/MonomialsSmallerThanFeature.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/MonomialsSmallerThanFeature.java index b9209f7d756..75aacbb0b6a 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/MonomialsSmallerThanFeature.java +++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/MonomialsSmallerThanFeature.java @@ -14,6 +14,7 @@ import org.key_project.prover.strategy.costbased.MutableState; import org.key_project.prover.strategy.costbased.NumberRuleAppCost; import org.key_project.prover.strategy.costbased.TopRuleAppCost; +import org.key_project.prover.strategy.costbased.feature.CostLocal; import org.key_project.prover.strategy.costbased.feature.Feature; import org.key_project.prover.strategy.costbased.termProjection.ProjectionToTerm; import org.key_project.prover.strategy.costbased.termfeature.BinarySumTermFeature; @@ -28,6 +29,7 @@ * Feature that returns zero iff each monomial of one polynomial is smaller than all monomials of a * second polynomial */ +@CostLocal public class MonomialsSmallerThanFeature extends AbstractMonomialSmallerThanFeature { private final TermFeature hasCoeff; diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/NoSelfApplicationFeature.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/NoSelfApplicationFeature.java index 4b9d1c21a48..6bd69a25079 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/NoSelfApplicationFeature.java +++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/NoSelfApplicationFeature.java @@ -9,6 +9,7 @@ import org.key_project.prover.rules.instantiation.AssumesFormulaInstantiation; import org.key_project.prover.sequent.PosInOccurrence; import org.key_project.prover.strategy.costbased.MutableState; +import org.key_project.prover.strategy.costbased.feature.CostLocal; import org.key_project.prover.strategy.costbased.feature.Feature; import org.key_project.util.collection.ImmutableList; @@ -16,6 +17,7 @@ * This feature checks that the position of application is not contained in the if-formulas. If the * rule application is admissible, zero is returned. */ +@CostLocal public class NoSelfApplicationFeature extends BinaryTacletAppFeature { public static final Feature INSTANCE = new NoSelfApplicationFeature(); diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/TermSmallerThanFeature.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/TermSmallerThanFeature.java index ba1d7620655..93ce0456a42 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/TermSmallerThanFeature.java +++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/TermSmallerThanFeature.java @@ -8,12 +8,14 @@ import org.key_project.prover.sequent.PosInOccurrence; import org.key_project.prover.strategy.costbased.MutableState; +import org.key_project.prover.strategy.costbased.feature.CostLocal; import org.key_project.prover.strategy.costbased.feature.Feature; import org.key_project.prover.strategy.costbased.termProjection.ProjectionToTerm; /** * Feature that returns zero iff one term is smaller than another term in the current term ordering */ +@CostLocal public class TermSmallerThanFeature extends SmallerThanFeature { private final ProjectionToTerm left, right; diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/TrivialMonomialLCRFeature.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/TrivialMonomialLCRFeature.java index e211b83ffbc..4382a0578a3 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/TrivialMonomialLCRFeature.java +++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/feature/TrivialMonomialLCRFeature.java @@ -10,6 +10,7 @@ import org.key_project.prover.sequent.PosInOccurrence; import org.key_project.prover.strategy.costbased.MutableState; +import org.key_project.prover.strategy.costbased.feature.CostLocal; import org.key_project.prover.strategy.costbased.feature.Feature; import org.key_project.prover.strategy.costbased.termProjection.ProjectionToTerm; @@ -20,6 +21,7 @@ *

* "A critical-pair/completion algorithm for finitely generated ideals in rings" */ +@CostLocal public class TrivialMonomialLCRFeature extends BinaryTacletAppFeature { private final ProjectionToTerm a, b; diff --git a/key.core/src/main/java/de/uka/ilkd/key/strategy/termgenerator/SuperTermGenerator.java b/key.core/src/main/java/de/uka/ilkd/key/strategy/termgenerator/SuperTermGenerator.java index 20fe63a4c66..3a953109864 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/strategy/termgenerator/SuperTermGenerator.java +++ b/key.core/src/main/java/de/uka/ilkd/key/strategy/termgenerator/SuperTermGenerator.java @@ -23,10 +23,12 @@ import org.key_project.prover.sequent.PosInOccurrence; import org.key_project.prover.strategy.costbased.MutableState; import org.key_project.prover.strategy.costbased.TopRuleAppCost; +import org.key_project.prover.strategy.costbased.feature.CostLocal; import org.key_project.prover.strategy.costbased.termfeature.TermFeature; import org.key_project.prover.strategy.costbased.termgenerator.TermGenerator; import org.key_project.util.collection.ImmutableArray; +@CostLocal public abstract class SuperTermGenerator implements TermGenerator { private final TermFeature cond; diff --git a/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/sequence/seqRules.key b/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/sequence/seqRules.key index 859e9bf83db..c5249415413 100644 --- a/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/sequence/seqRules.key +++ b/key.core/src/main/resources/de/uka/ilkd/key/proof/rules/sequence/seqRules.key @@ -494,7 +494,7 @@ \replacewith(\if(from < to) \then(to - from) \else(0)) - \heuristics(simplify, find_term_not_in_assumes) + // \heuristics(simplify, find_term_not_in_assumes) \displayname "lenOfSeqSub" }; diff --git a/key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/ProofCollections.java b/key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/ProofCollections.java index cdf13ad9404..a34f470e8d0 100644 --- a/key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/ProofCollections.java +++ b/key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/ProofCollections.java @@ -103,6 +103,14 @@ public static ProofCollection automaticJavaDL() throws IOException { */ // runOnlyOn = group1, group2 (the space after each comma is mandatory) // settings.setRunOnlyOn("performance, performancePOConstruction"); + // perf round 3: the perfTest group (defined below) is the curated measurement set. By + // default ALL groups run (full regression, exactly like main); pass + // -Dkey.runallproofs.runOnlyOn=perfTest to restrict to it, e.g. to reproduce the combined + // benchmark without running the whole suite. + String runOnly = System.getProperty("key.runallproofs.runOnlyOn", ""); + if (!runOnly.isBlank()) { + settings.setRunOnlyOn(runOnly); + } settings.setKeySettings(GenerateUnitTestsUtil.loadFromFile("automaticJAVADL.properties")); @@ -188,6 +196,33 @@ public static ProofCollection automaticJavaDL() throws IOException { // .provable("performance-test/updateSimplification/loop_5000.key"); + // ---------------------------------------------------------------------------------- + // Perf round 3 (cost-memoization / queue-redesign experiment) goal set. + // + // The 12 goals supplied for evaluating strategy-cost memoization, split into a + // development ("test") subset used while iterating on the change and a held-out + // ("validation") subset only consulted to confirm we did not overfit. The split is + // stratified across categories (heap lists, search/sort, arithmetic, information flow, + // static init) so each subset is representative. + // + // Selected to run via setRunOnlyOn("perfTest, perfValidation") above. REVERT before + // merging to main. + var perfTest = c.group("perfTest"); + perfTest.provable("heap/list_seq/SimplifiedLinkedList.remove.key"); + perfTest.provable("standard_key/arith/gemplusDecimal/add.key"); + perfTest.provable("heap/saddleback_search/Saddleback_search.key"); + perfTest.provable("standard_key/java_dl/symmArray.key"); + perfTest.provable("heap/coincidence_count/project.key"); + perfTest.provable("heap/list_seq/ArrayList.remove.1.key"); + + var perfValidation = c.group("perfValidation"); + perfValidation.provable("standard_key/java_dl/jml-information-flow.key"); + perfValidation.provable("heap/quicksort/sort.key"); + perfValidation.provable("heap/list/ArrayList_concatenate.key"); + perfValidation.provable("standard_key/arith/median.key"); + perfValidation.provable("standard_key/staticInitialisation/objectOfErroneousClass.key"); + perfValidation.provable("heap/removeDups/removeDup.key"); + // Tests for rule application restrictions var g = c.group("applicationRestrictions"); g.provable("heap/polarity_tests/wellformed1.key"); diff --git a/key.core/src/test/java/de/uka/ilkd/key/rule/match/vm/CompiledMatchProgramBenchmark.java b/key.core/src/test/java/de/uka/ilkd/key/rule/match/vm/CompiledMatchProgramBenchmark.java new file mode 100644 index 00000000000..4f01ffafe5e --- /dev/null +++ b/key.core/src/test/java/de/uka/ilkd/key/rule/match/vm/CompiledMatchProgramBenchmark.java @@ -0,0 +1,165 @@ +/* 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.match.vm; + +import java.nio.file.Files; +import java.nio.file.Path; +import java.util.ArrayList; +import java.util.List; + +import de.uka.ilkd.key.java.Services; +import de.uka.ilkd.key.logic.JTerm; +import de.uka.ilkd.key.proof.ProofAggregate; +import de.uka.ilkd.key.rule.FindTaclet; +import de.uka.ilkd.key.rule.MatchConditions; +import de.uka.ilkd.key.rule.Taclet; +import de.uka.ilkd.key.util.HelperClassForTests; + +import org.key_project.prover.rules.instantiation.MatchResultInfo; +import org.key_project.prover.rules.matcher.vm.MatchProgram; +import org.key_project.prover.rules.matcher.vm.VMProgramInterpreter; +import org.key_project.prover.sequent.SequentFormula; + +import org.junit.jupiter.api.Test; + +import static org.junit.jupiter.api.Assertions.assertEquals; + +/** + * Isolated micro-benchmark for the find matcher (no taclet index, strategy or proof pipeline): it + * compares the interpreter ({@link VMProgramInterpreter} over the framework's instruction program) + * against the cursor-free compiled matcher, both built by the match-plan framework + * ({@link JavaMatchPlanBuilder}), over the real taclet base. + * + *

+ * By default it runs on the self-contained {@code tacletMatch1.key}. Point it at a wider set (e.g. + * the bundled TPTP PUZ/SYN problems, which load the full FOL taclet base) with + * {@code -Dbench.problems=/abs/a.key,/abs/b.key}. Run with + * {@code ./gradlew :key.core:test --tests *CompiledMatchProgramBenchmark}. + */ +public class CompiledMatchProgramBenchmark { + + private static final MatchResultInfo EMPTY = MatchConditions.EMPTY_MATCHCONDITIONS; + + /** supplementary closed formulas (used when a problem's own sequent yields few terms). */ + private static final String[] CORPUS_FORMULAS = { + "A & B", "(!A | (A <-> B)) & B", "A -> (B -> A)", "\\forall int x; x >= 0", + "\\forall int x; x + 1 > x", "\\forall int x; \\exists int y; x + y = 0", + "1 + 2 * 3 = 7", "\\forall int x; \\forall int y; (x + y = y + x)" + }; + + private record Task(List interps, List comps, + List corpus, Services services) { + } + + @Test + public void benchmarkInterpreterVsCompiled() { + final List tasks = new ArrayList<>(); + for (String p : problemPaths()) { + final Task t = buildTask(p); + if (t != null) { + tasks.add(t); + } + } + if (tasks.isEmpty()) { + return; + } + + // warmup + for (int pass = 0; pass < 5; pass++) { + for (Task t : tasks) { + run(t.interps, t); + run(t.comps, t); + } + } + + // timed: alternate phases per pass to average out JIT / cache effects + final int passes = 30; + long interpMatches = 0, compMatches = 0, interpNanos = 0, compNanos = 0; + for (int pass = 0; pass < passes; pass++) { + for (Task t : tasks) { + long t0 = System.nanoTime(); + interpMatches += run(t.interps, t); + interpNanos += System.nanoTime() - t0; + + t0 = System.nanoTime(); + compMatches += run(t.comps, t); + compNanos += System.nanoTime() - t0; + } + } + + System.out.printf("[isolated matcher, %d problem(s)] interpreter=%.1f ms compiled=%.1f ms" + + " speedup=%.2fx (matches interp=%d comp=%d)%n", + tasks.size(), interpNanos / 1e6, compNanos / 1e6, + (double) interpNanos / compNanos, interpMatches / passes, compMatches / passes); + assertEquals(interpMatches, compMatches, + "compiled and interpreter must agree on the number of matches"); + } + + private static List problemPaths() { + final String prop = System.getProperty("bench.problems"); + if (prop != null && !prop.isBlank()) { + return List.of(prop.split(",")); + } + return List.of(HelperClassForTests.TESTCASE_DIRECTORY.resolve("tacletmatch") + .resolve("tacletMatch1.key").toString()); + } + + private static Task buildTask(String pathStr) { + final Path path = Path.of(pathStr.trim()); + if (!Files.exists(path)) { + System.out.println(" (skip, not found) " + path); + return null; + } + final ProofAggregate pa = HelperClassForTests.parse(path); + final Services services = pa.getFirstProof().getServices(); + + final List corpus = new ArrayList<>(); + for (SequentFormula sf : pa.getFirstProof().root().sequent()) { + collectSubterms((JTerm) sf.formula(), corpus); + } + for (String f : CORPUS_FORMULAS) { + try { + collectSubterms(services.getTermBuilder().parseTerm(f), corpus); + } catch (Exception ignored) { + // formula not parseable in this problem's signature + } + } + + final List interps = new ArrayList<>(); + final List comps = new ArrayList<>(); + int findTaclets = 0; + for (Taclet t : pa.getFirstProof().getInitConfig().activatedTaclets()) { + if (!(t instanceof FindTaclet ft)) { + continue; + } + findTaclets++; + final JTerm find = (JTerm) ft.find(); + comps.add(JavaMatchPlanBuilder.compiledProgram(find)); + interps.add(new VMProgramInterpreter(JavaMatchPlanBuilder.interpreterProgram(find))); + } + System.out.printf(" %-22s findTaclets=%4d corpus=%d%n", + path.getFileName(), findTaclets, corpus.size()); + return new Task(interps, comps, corpus, services); + } + + private static long run(List programs, Task t) { + long matches = 0; + for (int p = 0, np = programs.size(); p < np; p++) { + final MatchProgram prog = programs.get(p); + for (int i = 0, n = t.corpus.size(); i < n; i++) { + if (prog.match(t.corpus.get(i), EMPTY, t.services) != null) { + matches++; + } + } + } + return matches; + } + + private static void collectSubterms(JTerm t, List out) { + out.add(t); + for (int i = 0, n = t.arity(); i < n; i++) { + collectSubterms(t.sub(i), out); + } + } +} diff --git a/key.core/src/test/java/de/uka/ilkd/key/rule/match/vm/CompiledMatchProgramTest.java b/key.core/src/test/java/de/uka/ilkd/key/rule/match/vm/CompiledMatchProgramTest.java new file mode 100644 index 00000000000..49d29c6843c --- /dev/null +++ b/key.core/src/test/java/de/uka/ilkd/key/rule/match/vm/CompiledMatchProgramTest.java @@ -0,0 +1,123 @@ +/* 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.match.vm; + +import de.uka.ilkd.key.java.Services; +import de.uka.ilkd.key.logic.JTerm; +import de.uka.ilkd.key.parser.ParserException; +import de.uka.ilkd.key.proof.ProofAggregate; +import de.uka.ilkd.key.rule.FindTaclet; +import de.uka.ilkd.key.rule.MatchConditions; +import de.uka.ilkd.key.rule.Taclet; +import de.uka.ilkd.key.util.HelperClassForTests; + +import org.key_project.logic.Name; +import org.key_project.prover.rules.instantiation.MatchResultInfo; +import org.key_project.prover.rules.matcher.vm.MatchProgram; + +import org.junit.jupiter.api.BeforeAll; +import org.junit.jupiter.api.Test; + +import static org.junit.jupiter.api.Assertions.assertNotNull; +import static org.junit.jupiter.api.Assertions.assertNull; +import static org.junit.jupiter.api.Assertions.assertSame; +import static org.junit.jupiter.api.Assertions.assertTrue; + +/** + * Unit tests for the cursor-free compiled find-matcher built by the match-plan framework + * ({@link JavaMatchPlanBuilder#compiledProgram}), the compiled counterpart of + * {@link VMTacletMatcherTest} (which covers the interpreter). For the same taclets and the same + * matching / non-matching terms it asserts that the compiled matcher produces the expected result + * -- success with the expected schema-variable instantiations, and {@code null} on the failure + * cases -- so the compiled path is checked against explicit expectations. + * + *

+ * Coverage focuses on term-level matching (propositional / function patterns) and, importantly, + * {@link #compiledBoundVariableMatching() bound variables} (quantifiers / renaming), which the + * compiler handles cursor-free. + */ +public class CompiledMatchProgramTest { + + private static final MatchResultInfo EMPTY = MatchConditions.EMPTY_MATCHCONDITIONS; + + private static Services services; + private static FindTaclet propositional; // taclet_match_rule_1: phi & psi + private static FindTaclet function; // taclet_match_rule_2: f(...) + private static FindTaclet binder; // taclet_match_rule_3: \forall x; ... + + @BeforeAll + public static void init() { + final ProofAggregate pa = HelperClassForTests.parse( + HelperClassForTests.TESTCASE_DIRECTORY.resolve("tacletmatch") + .resolve("tacletMatch1.key")); + services = pa.getFirstProof().getServices(); + propositional = findTaclet(pa, "taclet_match_rule_1"); + function = findTaclet(pa, "taclet_match_rule_2"); + binder = findTaclet(pa, "taclet_match_rule_3"); + } + + private static FindTaclet findTaclet(ProofAggregate pa, String name) { + final Taclet t = + pa.getFirstProof().getInitConfig().lookupActiveTaclet(new Name(name)); + assertTrue(t instanceof FindTaclet, name + " must be a find taclet"); + return (FindTaclet) t; + } + + /** compiles the find expression; the taclets here are all within the framework's coverage. */ + private static MatchProgram compile(FindTaclet t) { + final MatchProgram p = JavaMatchPlanBuilder.compiledProgram((JTerm) t.find()); + assertNotNull(p, "find pattern of " + t.name() + " was expected to compile"); + return p; + } + + private MatchResultInfo match(MatchProgram p, String term) throws ParserException { + return p.match(services.getTermBuilder().parseTerm(term), EMPTY, services); + } + + @Test + public void compiledPropositionalMatching() throws ParserException { + final MatchProgram p = compile(propositional); + + final JTerm toMatch = services.getTermBuilder().parseTerm("A & B"); + final MatchResultInfo mc = p.match(toMatch, EMPTY, services); + assertNotNull(mc, "compiled matcher should match A & B"); + assertSame(toMatch.sub(0), mc.getInstantiations().lookupValue(new Name("phi"))); + assertSame(toMatch.sub(1), mc.getInstantiations().lookupValue(new Name("psi"))); + + for (String matching : new String[] { "(!A | (A<->B)) & B", "A & (B & A)", + "(\\forall int x; x>=0) & A" }) { + assertNotNull(match(p, matching), "compiled matcher should match " + matching); + } + // failure cases + for (String nonMatching : new String[] { "A | (B & A)", "A", + "\\forall int x;(x>=0 & A)" }) { + assertNull(match(p, nonMatching), "compiled matcher should not match " + nonMatching); + } + } + + @Test + public void compiledFunctionMatching() throws ParserException { + final MatchProgram p = compile(function); + + for (String matching : new String[] { "f(1, 1, 2)", "f(c, c, d)" }) { + assertNotNull(match(p, matching), "compiled matcher should match " + matching); + } + // failure cases: wrong shape / different head symbol / repeated-SV mismatch + for (String nonMatching : new String[] { "f(1,2,1)", "g(1,1,2)", "h(1,1)", "c", + "z(1,1,1,1)", "f(c,d,c)" }) { + assertNull(match(p, nonMatching), "compiled matcher should not match " + nonMatching); + } + } + + @Test + public void compiledBoundVariableMatching() throws ParserException { + final MatchProgram p = compile(binder); + + assertNotNull(match(p, "\\forall int x; x + 1 > 0"), + "compiled matcher should match the bound-variable pattern"); + // failure case: the body shape differs (1 + x rather than x + 1) + assertNull(match(p, "\\forall int x; 1 + x > 0"), + "compiled matcher should not match a differing bound-variable body"); + } +} diff --git a/key.core/src/test/resources/de/uka/ilkd/key/nparser/taclets.old.txt b/key.core/src/test/resources/de/uka/ilkd/key/nparser/taclets.old.txt index 69b18dc9c6b..7c195cd9116 100644 --- a/key.core/src/test/resources/de/uka/ilkd/key/nparser/taclets.old.txt +++ b/key.core/src/test/resources/de/uka/ilkd/key/nparser/taclets.old.txt @@ -12185,7 +12185,6 @@ lenOfSeqSubEQ { \assumes ([equals(seqSub(seq,from,to),EQ)]==>[]) \find(seqLen(EQ)) \sameUpdateLevel\replacewith(if-then-else(lt(from,to),sub(to,from),Z(0(#)))) -\heuristics(find_term_not_in_assumes, simplify) Choices: sequences:on} ----------------------------------------------------- == lenOfSeqUpd (lenOfSeqUpd) ========================================= diff --git a/key.ncore.calculus/src/main/java/org/key_project/prover/rules/matcher/vm/MatchProgram.java b/key.ncore.calculus/src/main/java/org/key_project/prover/rules/matcher/vm/MatchProgram.java new file mode 100644 index 00000000000..adce1a3ea8d --- /dev/null +++ b/key.ncore.calculus/src/main/java/org/key_project/prover/rules/matcher/vm/MatchProgram.java @@ -0,0 +1,35 @@ +/* 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 org.key_project.prover.rules.matcher.vm; + +import org.key_project.logic.LogicServices; +import org.key_project.logic.SyntaxElement; +import org.key_project.prover.rules.instantiation.MatchResultInfo; + +import org.jspecify.annotations.Nullable; + +/** + * A program that matches a syntax element against a fixed pattern (the find expression of a + * taclet). + *

+ * There are two implementations: the {@link VMProgramInterpreter}, which interprets a sequence of + * {@code VMInstruction}s over a generic cursor, and a compiled variant that navigates the term + * structure directly (no cursor) for the patterns it supports. Both are interchangeable; which one + * a + * {@code VMTacletMatcher} uses is selected at construction time, so the system can always fall back + * to the pure interpreter. + */ +public interface MatchProgram { + + /** + * Attempts to match the given syntax element against this program's pattern. + * + * @param toMatch the {@link SyntaxElement} to be matched + * @param mc the initial match conditions; may be extended on success + * @param services the {@link LogicServices} + * @return the resulting {@link MatchResultInfo} on success, or {@code null} if no match + */ + @Nullable + MatchResultInfo match(SyntaxElement toMatch, MatchResultInfo mc, LogicServices services); +} diff --git a/key.ncore.calculus/src/main/java/org/key_project/prover/rules/matcher/vm/ProgramChildrenMatcher.java b/key.ncore.calculus/src/main/java/org/key_project/prover/rules/matcher/vm/ProgramChildrenMatcher.java new file mode 100644 index 00000000000..0ac8082ff90 --- /dev/null +++ b/key.ncore.calculus/src/main/java/org/key_project/prover/rules/matcher/vm/ProgramChildrenMatcher.java @@ -0,0 +1,37 @@ +/* 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 org.key_project.prover.rules.matcher.vm; + +import org.key_project.logic.LogicServices; +import org.key_project.logic.SyntaxElement; +import org.key_project.prover.rules.instantiation.MatchResultInfo; + +import org.jspecify.annotations.Nullable; + +/** + * Matches a contiguous run of children of a parent syntax element, starting at a given child index. + * This is the abstraction used for the active statements of a context block (phase (3) of the + * context match): the located source element and the offset of the first active statement are + * provided, and the run of active-statement matchers consumes one child each. + *

+ * It is implemented both by the interpreter ({@link VMProgramInterpreter#matchChildrenFrom}, which + * navigates the children with a cursor) and by the compiled matcher (which navigates them directly + * via {@code getChild}), so the same context-block bookkeeping can drive either matcher. + */ +@FunctionalInterface +public interface ProgramChildrenMatcher { + + /** + * Matches the children of {@code parent} starting at index {@code startChild}. + * + * @param parent the element whose children are to be matched + * @param startChild the index of the first child to match against + * @param mc the initial match conditions + * @param services the logic services + * @return the resulting match conditions, or {@code null} if the match fails + */ + @Nullable + MatchResultInfo matchChildrenFrom(SyntaxElement parent, int startChild, MatchResultInfo mc, + LogicServices services); +} diff --git a/key.ncore.calculus/src/main/java/org/key_project/prover/rules/matcher/vm/VMProgramInterpreter.java b/key.ncore.calculus/src/main/java/org/key_project/prover/rules/matcher/vm/VMProgramInterpreter.java index 711c6138a05..6bb4ed14385 100644 --- a/key.ncore.calculus/src/main/java/org/key_project/prover/rules/matcher/vm/VMProgramInterpreter.java +++ b/key.ncore.calculus/src/main/java/org/key_project/prover/rules/matcher/vm/VMProgramInterpreter.java @@ -26,7 +26,7 @@ * constraints such as variable instantiations if successful, or {@code null} * if the match fails. */ -public class VMProgramInterpreter { +public class VMProgramInterpreter implements MatchProgram, ProgramChildrenMatcher { /** * The sequence of instructions to be executed. @@ -55,6 +55,7 @@ public VMProgramInterpreter(VMInstruction[] instruction) { * @return a {@link MatchResultInfo} containing the result of the match, * or {@code null} if no match was possible */ + @Override public @Nullable MatchResultInfo match(SyntaxElement toMatch, MatchResultInfo mc, LogicServices services) { MatchResultInfo result = mc; @@ -67,4 +68,45 @@ public VMProgramInterpreter(VMInstruction[] instruction) { navi.release(); return result; } + + /** + * Executes the program against the children of {@code parent} starting at child index + * {@code startChild}, i.e. the program is interpreted as a sequence of per-child matchers each + * consuming exactly one child of {@code parent} (advancing via {@code gotoNextSibling}). This + * is + * used to match the active statements of a context block, where matching does not start at the + * root but at a child offset of the located source element (the equivalent of + * {@code matchChildren(source, mc, offset)} on the interpreter side). + *

+ * The caller must guarantee that {@code parent} has at least {@code startChild + k} children, + * where {@code k} is the number of children this program consumes; otherwise the cursor would + * run past the available children. (The context-block matcher ensures this before calling.) + * + * @param parent the element whose children are to be matched + * @param startChild the index of the first child to match against + * @param mc the initial match conditions + * @param services the logic services + * @return the resulting match conditions, or {@code null} if the match fails + */ + @Override + public @Nullable MatchResultInfo matchChildrenFrom(SyntaxElement parent, int startChild, + MatchResultInfo mc, LogicServices services) { + if (instruction.length == 0) { + // nothing to match (empty active-statement block) -> succeed unchanged + return mc; + } + MatchResultInfo result = mc; + final PoolSyntaxElementCursor navi = PoolSyntaxElementCursor.get(parent); + navi.gotoNext(); // descend to the first child of parent + for (int i = 0; i < startChild; i++) { + navi.gotoNextSibling(); // advance to child number startChild + } + int instrPtr = 0; + while (result != null && instrPtr < instruction.length) { + result = instruction[instrPtr].match(navi, result, services); + instrPtr++; + } + navi.release(); + return result; + } } diff --git a/key.ncore.calculus/src/main/java/org/key_project/prover/strategy/costbased/feature/ConstFeature.java b/key.ncore.calculus/src/main/java/org/key_project/prover/strategy/costbased/feature/ConstFeature.java index 8d1ba7bf3ed..e7ef17721a4 100644 --- a/key.ncore.calculus/src/main/java/org/key_project/prover/strategy/costbased/feature/ConstFeature.java +++ b/key.ncore.calculus/src/main/java/org/key_project/prover/strategy/costbased/feature/ConstFeature.java @@ -12,6 +12,7 @@ import org.jspecify.annotations.NonNull; /// A feature that returns a constant value +@CostLocal public class ConstFeature implements Feature { @Override diff --git a/key.ncore.calculus/src/main/java/org/key_project/prover/strategy/costbased/feature/CostLocal.java b/key.ncore.calculus/src/main/java/org/key_project/prover/strategy/costbased/feature/CostLocal.java new file mode 100644 index 00000000000..7ff7fa360e4 --- /dev/null +++ b/key.ncore.calculus/src/main/java/org/key_project/prover/strategy/costbased/feature/CostLocal.java @@ -0,0 +1,36 @@ +/* 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 org.key_project.prover.strategy.costbased.feature; + +import java.lang.annotation.ElementType; +import java.lang.annotation.Retention; +import java.lang.annotation.RetentionPolicy; +import java.lang.annotation.Target; + +/** + * Marks a {@link Feature} whose cost is a pure function of the rule application and the subterm at + * its find position -- i.e. it does NOT depend on other formulas of the sequent, the set of applied + * rules on the branch, or any other goal-global state. + * + *

+ * This lets the strategy-cost reuse (see {@code de.uka.ilkd.key.strategy.CostReuse}) carry a + * container's cost forward across the per-round re-expansion instead of recomputing it, as long as + * the find position is unmodified. The default (no annotation) is the SAFE one: an unannotated leaf + * feature is treated as non-local, so cost reuse simply does not apply to taclets that use it (they + * are re-costed in full). Forgetting to annotate a new feature therefore costs performance, never + * soundness. + * + *

+ * For a composite feature (one that combines child features) this annotation means "transparent": + * the classifier recurses into the child features, so the composite counts as local only when all + * of them are. There is no automatic structural transparency -- a composite is trusted only because + * its author annotated it after checking that its own computation (including any non-Feature inputs + * such as projections or term-generators) is find-local. Use {@link CostNonLocal} to force a + * feature + * to be treated as non-local. + */ +@Retention(RetentionPolicy.RUNTIME) +@Target(ElementType.TYPE) +public @interface CostLocal { +} diff --git a/key.ncore.calculus/src/main/java/org/key_project/prover/strategy/costbased/feature/CostNonLocal.java b/key.ncore.calculus/src/main/java/org/key_project/prover/strategy/costbased/feature/CostNonLocal.java new file mode 100644 index 00000000000..d36694796fb --- /dev/null +++ b/key.ncore.calculus/src/main/java/org/key_project/prover/strategy/costbased/feature/CostNonLocal.java @@ -0,0 +1,28 @@ +/* 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 org.key_project.prover.strategy.costbased.feature; + +import java.lang.annotation.ElementType; +import java.lang.annotation.Retention; +import java.lang.annotation.RetentionPolicy; +import java.lang.annotation.Target; + +/** + * Explicitly marks a {@link Feature} as NON-local for strategy-cost reuse (see + * {@code de.uka.ilkd.key.strategy.CostReuse}): its cost may depend on goal-global state (other + * sequent formulas, applied rules, instantiation context, ...), so it must be recomputed on every + * re-expansion. + * + *

+ * This is an override: it wins over the automatic classification. Use it on a composite feature + * that would otherwise be auto-classified local (because all its children are local) but that + * itself reads goal-global state, or to defensively pin a feature whose locality is in doubt. The + * default for an unannotated leaf feature is already non-local, so this annotation is only needed + * to + * override the automatic decision. + */ +@Retention(RetentionPolicy.RUNTIME) +@Target(ElementType.TYPE) +public @interface CostNonLocal { +} diff --git a/key.ncore.calculus/src/main/java/org/key_project/prover/strategy/costbased/feature/FindDepthFeature.java b/key.ncore.calculus/src/main/java/org/key_project/prover/strategy/costbased/feature/FindDepthFeature.java index a87d7b0c86d..3a2a37f0965 100644 --- a/key.ncore.calculus/src/main/java/org/key_project/prover/strategy/costbased/feature/FindDepthFeature.java +++ b/key.ncore.calculus/src/main/java/org/key_project/prover/strategy/costbased/feature/FindDepthFeature.java @@ -17,6 +17,7 @@ /// depth zero or if not a find taclet) /// /// TODO: eliminate this class and use term features instead +@CostLocal public class FindDepthFeature implements Feature { private static final Feature INSTANCE = new FindDepthFeature(); diff --git a/key.ncore.calculus/src/main/java/org/key_project/prover/strategy/costbased/feature/LetFeature.java b/key.ncore.calculus/src/main/java/org/key_project/prover/strategy/costbased/feature/LetFeature.java index bf31a9a4275..f84a957f0ea 100644 --- a/key.ncore.calculus/src/main/java/org/key_project/prover/strategy/costbased/feature/LetFeature.java +++ b/key.ncore.calculus/src/main/java/org/key_project/prover/strategy/costbased/feature/LetFeature.java @@ -18,6 +18,10 @@ /// is generated by a ProjectionToTerm. This is mostly useful to make feature terms /// more /// readable, and to avoid repeated evaluation of projections. +// @CostLocal: a let-binding is transparent -- its bound value is a ProjectionToTerm over the +// app/find term and its body is recursed; local iff the body is. (Reuse only applies while the +// find position is unmodified, so the projected focus term is stable.) +@CostLocal public class LetFeature> implements Feature { private final TermBuffer var; diff --git a/key.ncore.calculus/src/main/java/org/key_project/prover/strategy/costbased/feature/ScaleFeature.java b/key.ncore.calculus/src/main/java/org/key_project/prover/strategy/costbased/feature/ScaleFeature.java index bfdde9c2908..a155cd30e0e 100644 --- a/key.ncore.calculus/src/main/java/org/key_project/prover/strategy/costbased/feature/ScaleFeature.java +++ b/key.ncore.calculus/src/main/java/org/key_project/prover/strategy/costbased/feature/ScaleFeature.java @@ -147,6 +147,7 @@ protected static boolean isZero(double p) { return Math.abs(p) < 0.0000001; } + @CostLocal private static class MultFeature extends ScaleFeature { /// the coefficient diff --git a/key.ncore.calculus/src/main/java/org/key_project/prover/strategy/costbased/feature/ShannonFeature.java b/key.ncore.calculus/src/main/java/org/key_project/prover/strategy/costbased/feature/ShannonFeature.java index 1e723e2e4cd..3e2253718f5 100644 --- a/key.ncore.calculus/src/main/java/org/key_project/prover/strategy/costbased/feature/ShannonFeature.java +++ b/key.ncore.calculus/src/main/java/org/key_project/prover/strategy/costbased/feature/ShannonFeature.java @@ -19,6 +19,7 @@ /// value of the whole expression is f1 (if c returns zero, or more /// general /// if c returns a distinguished value trueCost) or f2 +@CostLocal public class ShannonFeature implements Feature { /// The filter that decides which sub-feature is to be evaluated diff --git a/key.ncore.calculus/src/main/java/org/key_project/prover/strategy/costbased/feature/SumFeature.java b/key.ncore.calculus/src/main/java/org/key_project/prover/strategy/costbased/feature/SumFeature.java index 05f4f131360..32b05c15efc 100644 --- a/key.ncore.calculus/src/main/java/org/key_project/prover/strategy/costbased/feature/SumFeature.java +++ b/key.ncore.calculus/src/main/java/org/key_project/prover/strategy/costbased/feature/SumFeature.java @@ -16,6 +16,7 @@ import org.jspecify.annotations.NonNull; /// A feature that computes the sum of a given list (vector) of features +@CostLocal public class SumFeature implements Feature { @Override diff --git a/key.ncore.calculus/src/main/java/org/key_project/prover/strategy/costbased/termfeature/ApplyTFFeature.java b/key.ncore.calculus/src/main/java/org/key_project/prover/strategy/costbased/termfeature/ApplyTFFeature.java index 1bb33ac65a3..5066fe51aea 100644 --- a/key.ncore.calculus/src/main/java/org/key_project/prover/strategy/costbased/termfeature/ApplyTFFeature.java +++ b/key.ncore.calculus/src/main/java/org/key_project/prover/strategy/costbased/termfeature/ApplyTFFeature.java @@ -10,12 +10,14 @@ import org.key_project.prover.strategy.costbased.MutableState; import org.key_project.prover.strategy.costbased.RuleAppCost; import org.key_project.prover.strategy.costbased.TopRuleAppCost; +import org.key_project.prover.strategy.costbased.feature.CostLocal; import org.key_project.prover.strategy.costbased.feature.Feature; import org.key_project.prover.strategy.costbased.termProjection.ProjectionToTerm; import org.jspecify.annotations.NonNull; /// Feature for invoking a term feature on the instantiation of a schema variable +@CostLocal public class ApplyTFFeature> implements Feature { private final ProjectionToTerm proj; diff --git a/key.ncore.compiler/build.gradle b/key.ncore.compiler/build.gradle new file mode 100644 index 00000000000..a1bf3d11a48 --- /dev/null +++ b/key.ncore.compiler/build.gradle @@ -0,0 +1,25 @@ +repositories { + mavenCentral() +} + +dependencies { + api project(':key.util') + api project(':key.ncore') + api project(':key.ncore.calculus') + implementation('org.jspecify:jspecify:1.0.0') +} + +checkerFramework { + if (System.getProperty("ENABLE_NULLNESS")) { + checkers = [ + "org.checkerframework.checker.nullness.NullnessChecker", + ] + extraJavacArgs = [ + "-Xmaxerrs", "10000", + "-Astubs=$rootDir/key.util/src/main/checkerframework:permit-nullness-assertion-exception.astub", + "-AstubNoWarnIfNotFound", + "-Werror", + "-Aversion", + ] + } +} diff --git a/key.ncore.compiler/src/main/java/org/key_project/prover/rules/matcher/compiler/BinderMatcher.java b/key.ncore.compiler/src/main/java/org/key_project/prover/rules/matcher/compiler/BinderMatcher.java new file mode 100644 index 00000000000..08341f22c53 --- /dev/null +++ b/key.ncore.compiler/src/main/java/org/key_project/prover/rules/matcher/compiler/BinderMatcher.java @@ -0,0 +1,51 @@ +/* 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 org.key_project.prover.rules.matcher.compiler; + +import org.key_project.logic.op.QuantifiableVariable; +import org.key_project.prover.rules.instantiation.MatchResultInfo; +import org.key_project.prover.rules.matcher.vm.instruction.MatchInstruction; +import org.key_project.prover.rules.matcher.vm.instruction.VMInstruction; +import org.key_project.util.collection.ImmutableArray; + +/** + * Language SPI for matching bound variables (the variables introduced by a binder such as + * a quantifier, a substitution or a {@code let}). This is one of the two axes on which the + * Java/Rust/Solidity front-ends differ: each binds its own kind of logic / schema variables (e.g. + * {@code LogicVariable} vs. {@code BoundVariable}) and keeps its own renaming/instantiation state. + * + *

+ * The match-plan framework owns the scaffolding (bind the pattern's bound variables before + * matching the operator and subterms, then unbind afterwards, in both back-ends); a language plugs + * in the actual binding behaviour here. The {@linkplain #binder(ImmutableArray) binder} matches the + * pattern's bound variables against the source element's own bound variables and is shared by both + * back-ends (it is element-based); only the un-binding is back-end specific (an instruction for the + * interpreter, a direct call for the compiler). + */ +public interface BinderMatcher { + + /** + * The element-based instruction that binds the given pattern bound variables (it reads the + * source element's own bound variables). Used by both back-ends. + * + * @param boundVars the pattern's bound variables + * @return the binding instruction + */ + MatchInstruction binder(ImmutableArray boundVars); + + /** + * The interpreter instruction that pops the binding scope opened by {@link #binder}. + * + * @return the un-binding instruction + */ + VMInstruction unbinderInstruction(); + + /** + * Pops the binding scope opened by {@link #binder} for the compiled back-end. + * + * @param mc the match result after matching the binder body + * @return the match result with the binding scope removed + */ + MatchResultInfo unbind(MatchResultInfo mc); +} diff --git a/key.ncore.compiler/src/main/java/org/key_project/prover/rules/matcher/compiler/GenericOperatorHead.java b/key.ncore.compiler/src/main/java/org/key_project/prover/rules/matcher/compiler/GenericOperatorHead.java new file mode 100644 index 00000000000..a074927fb89 --- /dev/null +++ b/key.ncore.compiler/src/main/java/org/key_project/prover/rules/matcher/compiler/GenericOperatorHead.java @@ -0,0 +1,40 @@ +/* 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 org.key_project.prover.rules.matcher.compiler; + +import java.util.List; + +import org.key_project.logic.Term; +import org.key_project.logic.op.Operator; +import org.key_project.prover.rules.matcher.vm.MatchProgram; +import org.key_project.prover.rules.matcher.vm.instruction.GotoNextInstruction; +import org.key_project.prover.rules.matcher.vm.instruction.MatchIdentityInstruction; +import org.key_project.prover.rules.matcher.vm.instruction.VMInstruction; + +/** + * The head for an ordinary operator: the operator must be (reference-)identical to the pattern's. + * This is the language-agnostic default for any operator that has no special matching (i.e. is + * matched by {@code MatchIdentityInstruction} in the interpreter and by an {@code op() == op} check + * in the compiler). + */ +public final class GenericOperatorHead implements MatchHead { + + private final Operator op; + + public GenericOperatorHead(Operator op) { + this.op = op; + } + + @Override + public void emit(List out) { + out.add(new MatchIdentityInstruction(op)); + out.add(GotoNextInstruction.INSTANCE); + } + + @Override + public MatchProgram compileHeadCheck() { + final Operator expected = op; + return (element, mc, services) -> ((Term) element).op() == expected ? mc : null; + } +} diff --git a/key.ncore.compiler/src/main/java/org/key_project/prover/rules/matcher/compiler/MatchHead.java b/key.ncore.compiler/src/main/java/org/key_project/prover/rules/matcher/compiler/MatchHead.java new file mode 100644 index 00000000000..8423dfc4cea --- /dev/null +++ b/key.ncore.compiler/src/main/java/org/key_project/prover/rules/matcher/compiler/MatchHead.java @@ -0,0 +1,43 @@ +/* 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 org.key_project.prover.rules.matcher.compiler; + +import java.util.List; + +import org.key_project.prover.rules.matcher.vm.MatchProgram; +import org.key_project.prover.rules.matcher.vm.instruction.VMInstruction; + +/** + * The operator-specific "head" of an {@link OperatorPlan}: it checks the operator of a term and any + * operator-specific data (e.g. a modal-operator kind, a parametric function's generic arguments, + * an elementary update's left-hand side), but not the subterms -- those are recursed by + * the + * enclosing {@link OperatorPlan}. + * + *

+ * Generic heads (ordinary operators) live in this module; language-specific heads (modalities, + * parametric functions, ...) are supplied by the front-end. A head carries both back-ends, lifted + * from the corresponding hand-written matcher fragments. + */ +public interface MatchHead { + + /** + * Appends the interpreter instructions matching this head. On entry the cursor points at the + * operator; on completion it must point at the first subterm so the enclosing + * {@link OperatorPlan} can match the subterms. + * + * @param out the instruction list being built + */ + void emit(List out); + + /** + * Builds the compiled head check: applied to the term element, it verifies the operator (and + * head-specific data) and returns the extended match result, or {@code null} on failure. It + * does + * not recurse into subterms. + * + * @return the compiled head matcher + */ + MatchProgram compileHeadCheck(); +} diff --git a/key.ncore.compiler/src/main/java/org/key_project/prover/rules/matcher/compiler/MatchPlan.java b/key.ncore.compiler/src/main/java/org/key_project/prover/rules/matcher/compiler/MatchPlan.java new file mode 100644 index 00000000000..6daac292c75 --- /dev/null +++ b/key.ncore.compiler/src/main/java/org/key_project/prover/rules/matcher/compiler/MatchPlan.java @@ -0,0 +1,56 @@ +/* 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 org.key_project.prover.rules.matcher.compiler; + +import java.util.List; + +import org.key_project.prover.rules.matcher.vm.MatchProgram; +import org.key_project.prover.rules.matcher.vm.instruction.VMInstruction; + +/** + * A node of a match plan: a single, language-agnostic description of how to match one + * (sub)pattern, from which both back-ends are derived. + * + *

+ * A match plan is built once per find pattern (when the taclet base is loaded) by a per-language + * dispatch that composes plan nodes for each syntax construct. The point is that each construct is + * described in exactly one place: a node carries both + *

    + *
  • {@link #emitInstructions(List)} — the interpreted back-end: it appends the cursor-based + * {@link VMInstruction}s executed by {@code VMProgramInterpreter}; and
    • + *
  • {@link #compile()} — the compiled back-end: it builds a cursor-free {@link MatchProgram} that + * navigates the syntax element directly.
    • + *
+ * Adding a construct (or fixing its matching) is therefore done once, in the node, and both the + * interpreter and the compiler stay in sync by construction. + * + *

+ * Both emissions are produced at plan-construction time, so neither adds runtime overhead over the + * hand-written matchers they replace: the interpreter still runs a {@code VMInstruction[]} and the + * compiler still runs the resulting {@link MatchProgram}. + */ +public interface MatchPlan { + + /** + * Appends, to {@code out}, the {@link VMInstruction}s matching this (sub)pattern for the + * cursor-based interpreter. The cursor is expected to point at the element to be matched and, + * on + * completion of the appended instructions, to have advanced past it (to its next sibling), so + * that sibling plans can be appended directly after. + * + * @param out the instruction list being built + */ + void emitInstructions(List out); + + /** + * Builds the cursor-free compiled matcher for this (sub)pattern. The returned + * {@link MatchProgram} is applied to the syntax element to be matched (the same element the + * interpreter's cursor would point at) and returns the extended match result, or {@code null} + * on + * failure. + * + * @return the compiled matcher for this plan node + */ + MatchProgram compile(); +} diff --git a/key.ncore.compiler/src/main/java/org/key_project/prover/rules/matcher/compiler/OperatorPlan.java b/key.ncore.compiler/src/main/java/org/key_project/prover/rules/matcher/compiler/OperatorPlan.java new file mode 100644 index 00000000000..b2236a78420 --- /dev/null +++ b/key.ncore.compiler/src/main/java/org/key_project/prover/rules/matcher/compiler/OperatorPlan.java @@ -0,0 +1,110 @@ +/* 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 org.key_project.prover.rules.matcher.compiler; + +import java.util.List; + +import org.key_project.logic.Term; +import org.key_project.logic.op.QuantifiableVariable; +import org.key_project.prover.rules.instantiation.MatchResultInfo; +import org.key_project.prover.rules.matcher.vm.MatchProgram; +import org.key_project.prover.rules.matcher.vm.instruction.CheckNodeKindInstruction; +import org.key_project.prover.rules.matcher.vm.instruction.GotoNextInstruction; +import org.key_project.prover.rules.matcher.vm.instruction.GotoNextSiblingInstruction; +import org.key_project.prover.rules.matcher.vm.instruction.MatchInstruction; +import org.key_project.prover.rules.matcher.vm.instruction.VMInstruction; +import org.key_project.util.collection.ImmutableArray; + +import org.jspecify.annotations.Nullable; + +/** + * Plan for a term whose top operator is matched by a {@link MatchHead} (the operator + any + * operator-specific data) and whose subterms are matched by child plans. Bound variables, if any, + * are bound around the whole node via the {@link BinderMatcher}. + * + *

+ * This is the language-agnostic counterpart of the non-schema-variable branch of the hand-written + * matchers: the interpreter emission reproduces {@code checkNodeKind(Term) + gotoNext + head + + * (skip bound variables) + subterms} (wrapped in bind/unbind), and the compiled emission checks the + * head then recurses the subterms (wrapped in bind/unbind). + */ +public final class OperatorPlan implements MatchPlan { + + private final MatchHead head; + private final List children; + private final ImmutableArray boundVars; + private final BinderMatcher binder; + + /** + * @param head the operator head (operator + operator-specific checks) + * @param children one plan per subterm, in order + * @param boundVars the term's bound variables (possibly empty) + * @param binder the binder SPI (used only if {@code boundVars} is non-empty) + */ + public OperatorPlan(MatchHead head, List children, + ImmutableArray boundVars, BinderMatcher binder) { + this.head = head; + this.children = children; + this.boundVars = boundVars; + this.binder = binder; + } + + @Override + public void emitInstructions(List out) { + final boolean bound = !boundVars.isEmpty(); + if (bound) { + out.add(binder.binder(boundVars)); + } + out.add(new CheckNodeKindInstruction(Term.class)); + out.add(GotoNextInstruction.INSTANCE); + head.emit(out); + if (bound) { + for (int i = 0, n = boundVars.size(); i < n; i++) { + out.add(GotoNextSiblingInstruction.INSTANCE); + } + } + for (MatchPlan child : children) { + child.emitInstructions(out); + } + if (bound) { + out.add(binder.unbinderInstruction()); + } + } + + @Override + public MatchProgram compile() { + final MatchProgram headCheck = head.compileHeadCheck(); + final int n = children.size(); + final MatchProgram[] childMatchers = new MatchProgram[n]; + for (int i = 0; i < n; i++) { + childMatchers[i] = children.get(i).compile(); + } + final MatchProgram core = (element, mc, services) -> { + MatchResultInfo r = headCheck.match(element, mc, services); + if (r == null) { + return null; + } + final Term term = (Term) element; + for (int i = 0; i < n; i++) { + r = childMatchers[i].match(term.sub(i), r, services); + if (r == null) { + return null; + } + } + return r; + }; + if (boundVars.isEmpty()) { + return core; + } + final MatchInstruction bind = binder.binder(boundVars); + return (element, mc, services) -> { + final @Nullable MatchResultInfo bound = bind.match(element, mc, services); + if (bound == null) { + return null; + } + final @Nullable MatchResultInfo body = core.match(element, bound, services); + return body == null ? null : binder.unbind(body); + }; + } +} diff --git a/key.ncore.compiler/src/main/java/org/key_project/prover/rules/matcher/compiler/ProgramMatchHook.java b/key.ncore.compiler/src/main/java/org/key_project/prover/rules/matcher/compiler/ProgramMatchHook.java new file mode 100644 index 00000000000..cc47ce845f4 --- /dev/null +++ b/key.ncore.compiler/src/main/java/org/key_project/prover/rules/matcher/compiler/ProgramMatchHook.java @@ -0,0 +1,52 @@ +/* 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 org.key_project.prover.rules.matcher.compiler; + +import org.key_project.prover.rules.matcher.vm.MatchProgram; +import org.key_project.prover.rules.matcher.vm.instruction.VMInstruction; + +/** + * Language SPI for matching the program carried by a modality (the {@code \<{ ... }\>} of + * a + * symbolic-execution taclet). This is the second of the two axes on which the Java/Rust/Solidity + * front-ends differ (the first is {@link BinderMatcher}): each has its own program AST -- Java's + * {@code JavaBlock}/{@code ContextStatementBlock}, Rust's {@code RustyBlock}, Solidity's block -- + * but all are {@link org.key_project.logic.SyntaxElement}s navigated through {@code getChild}. + * + *

+ * A hook is built per modality pattern (it captures that pattern's program) and exposes the program + * matcher for both back-ends. On the interpreter side it is a single {@link VMInstruction} run with + * the cursor positioned at the program block; on the compiled side it is a {@link MatchProgram} + * applied directly to the source program block. Both consume exactly one element (the block), so + * the + * enclosing modality head can advance to the post-condition subterm afterwards. + * + *

+ * The framework owns the surrounding modality skeleton (check the modality, match its kind, then + * the + * program, then recurse the subterms); a language plugs in only the divergent program matching + * here. + * Java additionally has the rich {@code ContextStatementBlock} prefix/suffix machinery, which is + * entirely encapsulated behind this hook; Rust and Solidity supply their own simpler block + * matchers. + */ +public interface ProgramMatchHook { + + /** + * The interpreter instruction matching the modality's program. On entry the cursor points at + * the + * source program block; it consumes that block. + * + * @return the program-matching instruction + */ + VMInstruction programInstruction(); + + /** + * The compiled matcher for the modality's program, applied directly to the source program + * block. + * + * @return the compiled program matcher + */ + MatchProgram compileProgram(); +} diff --git a/key.ncore.compiler/src/main/java/org/key_project/prover/rules/matcher/compiler/SchemaVarPlan.java b/key.ncore.compiler/src/main/java/org/key_project/prover/rules/matcher/compiler/SchemaVarPlan.java new file mode 100644 index 00000000000..ce61c1c12dc --- /dev/null +++ b/key.ncore.compiler/src/main/java/org/key_project/prover/rules/matcher/compiler/SchemaVarPlan.java @@ -0,0 +1,75 @@ +/* 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 org.key_project.prover.rules.matcher.compiler; + +import java.util.List; + +import org.key_project.logic.op.QuantifiableVariable; +import org.key_project.prover.rules.instantiation.MatchResultInfo; +import org.key_project.prover.rules.matcher.vm.MatchProgram; +import org.key_project.prover.rules.matcher.vm.instruction.GotoNextSiblingInstruction; +import org.key_project.prover.rules.matcher.vm.instruction.MatchInstruction; +import org.key_project.prover.rules.matcher.vm.instruction.VMInstruction; +import org.key_project.util.collection.ImmutableArray; + +import org.jspecify.annotations.Nullable; + +/** + * Plan for a (sub)pattern that is a schema variable: it matches the whole element via the provided + * schema-variable {@link MatchInstruction} (which the front-end supplies, since schema-variable + * kinds are language-specific). Bound variables, if any, are bound around it via the + * {@link BinderMatcher}. + * + *

+ * Language-agnostic counterpart of the schema-variable branch of the hand-written matchers: the + * interpreter emission is {@code matchSV + gotoNextSibling} (wrapped in bind/unbind), the compiled + * emission applies the schema-variable instruction directly (wrapped in bind/unbind). + */ +public final class SchemaVarPlan implements MatchPlan { + + private final MatchInstruction schemaVarInstruction; + private final ImmutableArray boundVars; + private final BinderMatcher binder; + + public SchemaVarPlan(MatchInstruction schemaVarInstruction, + ImmutableArray boundVars, BinderMatcher binder) { + this.schemaVarInstruction = schemaVarInstruction; + this.boundVars = boundVars; + this.binder = binder; + } + + @Override + public void emitInstructions(List out) { + final boolean bound = !boundVars.isEmpty(); + if (bound) { + out.add(binder.binder(boundVars)); + } + out.add(schemaVarInstruction); + out.add(GotoNextSiblingInstruction.INSTANCE); + if (bound) { + for (int i = 0, n = boundVars.size(); i < n; i++) { + out.add(GotoNextSiblingInstruction.INSTANCE); + } + out.add(binder.unbinderInstruction()); + } + } + + @Override + public MatchProgram compile() { + final MatchInstruction sv = schemaVarInstruction; + final MatchProgram core = sv::match; + if (boundVars.isEmpty()) { + return core; + } + final MatchInstruction bind = binder.binder(boundVars); + return (element, mc, services) -> { + final @Nullable MatchResultInfo bound = bind.match(element, mc, services); + if (bound == null) { + return null; + } + final @Nullable MatchResultInfo body = core.match(element, bound, services); + return body == null ? null : binder.unbind(body); + }; + } +} diff --git a/key.ncore.compiler/src/main/java/org/key_project/prover/rules/matcher/compiler/package-info.java b/key.ncore.compiler/src/main/java/org/key_project/prover/rules/matcher/compiler/package-info.java new file mode 100644 index 00000000000..7c0238be3aa --- /dev/null +++ b/key.ncore.compiler/src/main/java/org/key_project/prover/rules/matcher/compiler/package-info.java @@ -0,0 +1,25 @@ +/* + * 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 + */ + +/** + * A language-agnostic framework for taclet find-matching that produces, from a single description + * of + * a pattern, both an interpreted matcher (a sequence of + * {@link org.key_project.prover.rules.matcher.vm.instruction.VMInstruction}s run by + * {@link org.key_project.prover.rules.matcher.vm.VMProgramInterpreter}) and a cursor-free compiled + * matcher. + * + *

+ * It works purely over {@link org.key_project.logic.SyntaxElement} / + * {@link org.key_project.logic.Term} + * and the calculus matcher abstractions ({@code MatchResultInfo}, {@code VMInstruction}, + * {@code MatchProgram}); it depends only on {@code key.ncore}, {@code key.ncore.calculus} and + * {@code key.util}, never on the Java-DL specific {@code key.core}. Language-specific behaviour + * (the concrete syntax constructs, the program/AST sub-matching and the binding of bound variables) + * is supplied through small SPIs so that the Java, Rust and Solidity front-ends can share this core + * and only add their own constructs. + */ +package org.key_project.prover.rules.matcher.compiler; diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/settings/SettingsManager.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/settings/SettingsManager.java index de5f4c9cc88..494931f62ea 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/settings/SettingsManager.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/settings/SettingsManager.java @@ -20,6 +20,7 @@ import de.uka.ilkd.key.gui.keyshortcuts.ShortcutSettings; import de.uka.ilkd.key.gui.smt.settings.SMTSettingsProvider; import de.uka.ilkd.key.proof.Proof; +import de.uka.ilkd.key.rule.match.vm.VMTacletMatcher; import de.uka.ilkd.key.settings.*; import org.slf4j.Logger; @@ -40,6 +41,15 @@ public class SettingsManager { public static final ColorSettingsProvider COLOR_SETTINGS = new ColorSettingsProvider(); public static final FeatureSettingsPanel FEATURE_SETTINGS_PANEL = new FeatureSettingsPanel(); + /** + * Registration anchor: referencing a feature flag declared in a lazily-loaded core class (here + * the interpreter-matcher fallback flag in {@link VMTacletMatcher}) forces its registration so + * it shows in the {@link FeatureSettingsPanel} on a fresh start, before any proof is loaded. + */ + @SuppressWarnings("unused") + public static final FeatureSettings.Feature INTERPRETER_MATCHER_FEATURE = + VMTacletMatcher.INTERPRETER_MATCHER_FEATURE; + private static SettingsManager INSTANCE; private final List settingsProviders = new LinkedList<>(); diff --git a/key.util/src/main/java/org/key_project/util/collection/Pair.java b/key.util/src/main/java/org/key_project/util/collection/Pair.java index 29a7d3f9393..bef98dfa5fd 100644 --- a/key.util/src/main/java/org/key_project/util/collection/Pair.java +++ b/key.util/src/main/java/org/key_project/util/collection/Pair.java @@ -55,7 +55,10 @@ public boolean equals(@Nullable Object o) { @Override public int hashCode() { - return Objects.hash(first, second); + // Same value as Objects.hash(first, second) but without allocating the varargs Object[] + // on every call (Pair is heavily used as a hash-map key during proof search). + int result = 31 + (first == null ? 0 : first.hashCode()); + return 31 * result + (second == null ? 0 : second.hashCode()); } /////////////////////////////////////////////////////////// diff --git a/settings.gradle b/settings.gradle index 00226f6fa82..e217520e491 100644 --- a/settings.gradle +++ b/settings.gradle @@ -7,6 +7,7 @@ plugins { include "key.util" include "key.ncore" include 'key.ncore.calculus' +include 'key.ncore.compiler' include "key.core" //include "key.core.rifl"