Performance (overview): round-3 combined — 1.82× faster automode (all five PRs)

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')

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

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.
      */

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;
+    }
+
 
 }

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<JTerm> 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<TermLabel> labels = term.getLabels();
+        ImmutableArray<TermLabel> 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);
     }
 }

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

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<Goal> m = ruleAppManager;
+        while (m instanceof DelegationBasedRuleApplicationManager<Goal> 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) {

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

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