Determinism hardening

key.core/src/main/java/de/uka/ilkd/key/java/ServiceCaches.java

@@ -18,6 +18,7 @@
 import de.uka.ilkd.key.proof.TermTacletAppIndexCacheSet;
 import de.uka.ilkd.key.rule.metaconstruct.arith.Monomial;
 import de.uka.ilkd.key.rule.metaconstruct.arith.Polynomial;
+import de.uka.ilkd.key.strategy.CostReuse;
 import de.uka.ilkd.key.strategy.IfInstantiationCachePool;
 import de.uka.ilkd.key.strategy.feature.AbstractBetaFeature.TermInfo;
 import de.uka.ilkd.key.strategy.feature.AppliedRuleAppsNameCache;
@@ -126,7 +127,8 @@ public class ServiceCaches implements SessionCaches {
      * this class (a {@code CostReuse.Eligibility}, or its ineligible sentinel) to keep this package
      * independent of the strategy package.
      */
-    private final Map<Taclet, Object> costReuseClassificationCache = new ConcurrentHashMap<>();
+    private final Map<Taclet, CostReuse.ConditionalEligibility> costReuseClassificationCache =
+        new ConcurrentHashMap<>();
 
     private final Map<org.key_project.logic.Term, Monomial> monomialCache =
         new ConcurrentLruCache<>(2000);
@@ -243,7 +245,7 @@ public final Map<Operator, Integer> getIntroductionTimeCache() {
         return introductionTimeCache;
     }
 
-    public final Map<Taclet, Object> getCostReuseClassificationCache() {
+    public final Map<Taclet, CostReuse.ConditionalEligibility> getCostReuseClassificationCache() {
         return costReuseClassificationCache;
     }
 

key.core/src/main/java/de/uka/ilkd/key/macros/ApplyScriptsMacro.java

@@ -176,7 +176,7 @@ private static JmlAssert getJmlAssert(Node node) {
         Term appliedOn = ruleApp.posInOccurrence().subTerm();
         if (appliedOn.op() instanceof UpdateApplication) {
             var update = UpdateApplication.getUpdate((JTerm) appliedOn);
-            Map<JTerm, JTerm> updates = new HashMap<>();
+            Map<JTerm, JTerm> updates = new LinkedHashMap<>();
             Services services = goal.proof().getServices();
             collectUpdates(update, updates, services);
             return new OpReplacer(updates, services.getTermFactory());
@@ -311,7 +311,7 @@ private JTerm correctSelfVar(int index, JavaBlock javaBlock,
 
     private Map<LocationVariable, JFunction> makeObtainVarMap(
             ImmutableList<LocationVariable> locationVariables) {
-        HashMap<LocationVariable, JFunction> result = new HashMap<>();
+        HashMap<LocationVariable, JFunction> result = new LinkedHashMap<>();
         for (LocationVariable lv : locationVariables) {
             result.put(lv, null);
         }

key.core/src/main/java/de/uka/ilkd/key/speclang/LoopContractImpl.java

@@ -339,7 +339,7 @@ public static LoopContract combine(ImmutableSet<LoopContract> contracts, Service
      */
     private static OpReplacer createOpReplacer(final ProgramVariable index,
             final ProgramVariable values, Services services) {
-        final Map<SyntaxElement, SyntaxElement> replacementMap = new HashMap<>();
+        final Map<SyntaxElement, SyntaxElement> replacementMap = new LinkedHashMap<>();
         if (index != null) {
             replacementMap.put(services.getTermBuilder().index(),
                 services.getTermBuilder().var(index));
@@ -624,8 +624,8 @@ public BlockContract toBlockContract() {
 
 
         if (head != null) {
-            Map<JTerm, JTerm> preReplacementMap = new HashMap<>();
-            Map<JTerm, JTerm> postReplacementMap = new HashMap<>();
+            Map<JTerm, JTerm> preReplacementMap = new LinkedHashMap<>();
+            Map<JTerm, JTerm> postReplacementMap = new LinkedHashMap<>();
             for (int i = 0; i < head.getStatementCount(); ++i) {
                 Statement stmt = head.getStatementAt(i);
                 if (stmt instanceof LocalVariableDeclaration decl) {

key.core/src/main/java/de/uka/ilkd/key/strategy/CostReuse.java

@@ -21,6 +21,7 @@
 import org.key_project.prover.strategy.costbased.feature.StableCost;
 import org.key_project.prover.strategy.costbased.feature.VolatileCost;
 import org.key_project.prover.strategy.costbased.feature.WeakStableCost;
+import org.key_project.prover.strategy.costbased.termgenerator.TermGenerator;
 
 import org.jspecify.annotations.Nullable;
 
@@ -94,8 +95,16 @@ public record Eligibility(Feature[] vetoes, boolean weakStable) {
     }
 
     /**
-     * @param strategy the goal's strategy; classified against its cost dispatchers (only used to
-     *        obtain those -- never dereferenced beyond {@link #dispatchers})
+     * Secondary cache key for cost reuse eligibility is the strategy as a strategy change
+     * invalidates the previously established eligibility
+     */
+    public record ConditionalEligibility(Strategy<?> strategy, Eligibility verdict) {
+    }
+
+    /**
+     * determines the eligibility of a taclet for cost reuse
+     *
+     * @param strategy the goal's strategy
      * @param proof the proof being worked on; supplies the per-proof classification cache
      * @param taclet the taclet whose cost is a candidate for reuse
      * @return how the taclet may reuse its cost, or {@code null} if it is not eligible at all.
@@ -108,20 +117,16 @@ public record Eligibility(Feature[] vetoes, boolean weakStable) {
         if (disp.isEmpty()) {
             return null;
         }
-        // The verdict is cached in the PROOF's ServiceCaches, NOT a static map: a taclet's locality
-        // depends on the cost dispatchers in force (which differ with the taclet options), while
-        // Taclet#equals is only name + find term. A cache shared across proofs would let one option
-        // set read another's verdict for a same-named but structurally different taclet -- exactly
-        // the static-cache hazard ServiceCaches exists to avoid. Per proof, it is also freed with
-        // the proof. (ELIGIBLE => at least the top-level NonDuplicateApp veto, so the empty-veto
-        // INELIGIBLE acts as the "not eligible" sentinel, the map forbidding null values.)
-        final Map<Taclet, Object> cache = proof.getServices().getCaches()
+        final Map<Taclet, ConditionalEligibility> cache = proof.getServices().getCaches()
                 .getCostReuseClassificationCache();
-        final Object e = cache.computeIfAbsent(taclet, t -> {
-            final Eligibility res = classify(disp, t);
-            return res == null ? INELIGIBLE : res;
-        });
-        return e == INELIGIBLE ? null : (Eligibility) e;
+        final ConditionalEligibility cached = cache.get(taclet);
+        if (cached instanceof ConditionalEligibility c &&
+                c.strategy() == strategy) { // cached result only valid if strategy did not change
+            return c.verdict() == INELIGIBLE ? null : (Eligibility) c.verdict();
+        }
+        final Eligibility res = classify(disp, taclet);
+        cache.put(taclet, new ConditionalEligibility(strategy, res == null ? INELIGIBLE : res));
+        return res;
     }
 
     private static @Nullable Eligibility classify(List<RuleSetDispatchFeature> dispatchers,
@@ -161,8 +166,8 @@ private static void walk(CostClassifiable f, Set<Feature> vetoes, boolean[] loca
         }
         switch (localityOf(f)) {
             case VOLATILE -> local[0] = false;
-            // Transparent: recurse into every child component -- a Feature, TermGenerator or
-            // ProjectionToTerm, all of which receive the goal -- and stay local only if they all
+            // Transparent: recurse into every child component; a Feature, TermGenerator or
+            // ProjectionToTerm, all of which receive the goal, and stay local only if they all
             // are. WEAK_STABLE additionally reads the whole find formula, so reuse is gated on
             // that formula being unchanged (see Eligibility). Children are discovered reflectively
             // (see forEachChild), so authors annotate locality and never enumerate children.
@@ -221,7 +226,7 @@ private static void follow(@Nullable Object o,
                 follow(e, action);
             }
         }
-        // Everything else is not a cost component and is not traversed -- notably TermFeature (its
+        // Everything else is not a cost component and is not traversed, notably TermFeature (its
         // compute() has no goal, so it is stable by construction), plus Name, RuleAppCost, ...
     }
 
@@ -235,12 +240,12 @@ static void warnMismatch(Taclet taclet, Object reused, Object fresh) {
     }
 
     /**
-     * The cost dispatchers to classify against, taken from the strategy of the goal being costed.
-     * Must NOT be cached across strategies: different goals/proofs use different strategy instances
+     * The cost dispatchers to classify against, taken from the strategy of the goal on which
+     * the costs should be computed.
+     * Must not be cached across strategies: different goals/proofs use different strategy instances
      * (and some are not {@link ModularJavaDLStrategy} at all). A stale or empty cached value would
      * make the {@link #walk} traverse nothing and thus classify every taclet as (wrongly) local.
-     * When the strategy exposes no cost dispatchers, the taclet is treated as ineligible (see
-     * {@link #vetoesIfEligible}) -- never as trivially local.
+     * When the strategy exposes no cost dispatchers, the taclet is treated as ineligible.
      */
     private static List<RuleSetDispatchFeature> dispatchers(Strategy<?> strategy) {
         return strategy instanceof ModularJavaDLStrategy m ? m.costRuleSetDispatchers() : List.of();

key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/EqualityConstraint.java

@@ -22,7 +22,6 @@
 import org.key_project.logic.op.QuantifiableVariable;
 import org.key_project.logic.op.sv.SchemaVariable;
 import org.key_project.logic.sort.Sort;
-import org.key_project.util.ConcurrentLruCache;
 import org.key_project.util.collection.DefaultImmutableSet;
 import org.key_project.util.collection.ImmutableList;
 import org.key_project.util.collection.ImmutableSet;
@@ -42,9 +41,6 @@
 @Deprecated
 public class EqualityConstraint implements Constraint {
 
-    /** contains a boolean value */
-    private static final BooleanContainer CONSTRAINTBOOLEANCONTAINER = new BooleanContainer();
-
     /**
      * stores constraint content as a mapping from Metavariable to Term
      */
@@ -209,7 +205,7 @@ private JTerm instantiate(JTerm p, Services services) {
      */
     @Override
     public Constraint unify(JTerm t1, JTerm t2, Services services) {
-        return unify(t1, t2, services, CONSTRAINTBOOLEANCONTAINER);
+        return unify(t1, t2, services, new BooleanContainer());
     }
 
     /**
@@ -651,7 +647,7 @@ public boolean isAsWeakAs(Constraint co) {
      */
     @Override
     public Constraint join(Constraint co, Services services) {
-        return join(co, services, CONSTRAINTBOOLEANCONTAINER);
+        return join(co, services, new BooleanContainer());
     }
 
 
@@ -683,40 +679,9 @@ public synchronized Constraint join(Constraint co, Services services,
             return co.join(this, services);
         }
 
-        final ECPair cacheKey;
-
-        lookup: synchronized (joinCacheMonitor) {
-            ecPair0.set(this, co);
-            Constraint res = joinCache.get(ecPair0);
-
-            if (res == null) {
-                cacheKey = ecPair0.copy();
-                res = joinCacheOld.get(cacheKey);
-                if (res == null) {
-                    break lookup;
-                }
-                joinCache.put(cacheKey, res);
-            }
-
-            unchanged.setVal(this == res);
-            return res;
-        }
-
         final Constraint res = joinHelp((EqualityConstraint) co, services);
-
         unchanged.setVal(res == this);
-
-        synchronized (joinCacheMonitor) {
-            if (joinCache.size() > 1000) {
-                joinCacheOld.clear();
-                final Map<ECPair, Constraint> t = joinCacheOld;
-                joinCacheOld = joinCache;
-                joinCache = t;
-            }
-
-            joinCache.put(cacheKey, res);
-            return res;
-        }
+        return res;
     }
 
 
@@ -825,48 +790,6 @@ public String toString() {
     }
 
 
-    private static final class ECPair {
-        private Constraint first;
-        private Constraint second;
-        private int hash;
-
-        public boolean equals(Object o) {
-            if (!(o instanceof ECPair e)) {
-                return false;
-            }
-            return first == e.first && second == e.second;
-        }
-
-        public void set(Constraint first, Constraint second) {
-            this.first = first;
-            this.second = second;
-            this.hash = first.hashCode() + second.hashCode();
-        }
-
-        public int hashCode() {
-            return hash;
-        }
-
-        public ECPair copy() {
-            return new ECPair(first, second, hash);
-        }
-
-        public ECPair(Constraint first, Constraint second, int hash) {
-            this.first = first;
-            this.second = second;
-            this.hash = hash;
-        }
-    }
-
-    private static final Object joinCacheMonitor = new Object();
-
-    // the methods using these caches seem not to be used anymore otherwise refactor and move it
-    // into ServiceCaches
-    private static Map<ECPair, Constraint> joinCache = new ConcurrentLruCache<>(0);
-    private static Map<ECPair, Constraint> joinCacheOld = new ConcurrentLruCache<>(0);
-
-    private static final ECPair ecPair0 = new ECPair(null, null, 0);
-
     @Override
     public int hashCode() {
         if (hashCode == null) {

key.core/src/main/java/de/uka/ilkd/key/strategy/termgenerator/TriggeredInstantiations.java

@@ -5,6 +5,7 @@
 
 import java.util.HashSet;
 import java.util.Iterator;
+import java.util.LinkedHashSet;
 import java.util.Set;
 
 import de.uka.ilkd.key.java.Services;
@@ -88,8 +89,8 @@ public Iterator<org.key_project.logic.Term> generate(RuleApp app, PosInOccurrenc
             final Sequent seq = goal.sequent();
             final CandidateCache cached = candidateCache.get();
             if (seq != cached.last()) {
-                terms = new HashSet<>();
-                axiomSet = new HashSet<>();
+                terms = new LinkedHashSet<>();
+                axiomSet = new LinkedHashSet<>();
                 computeAxiomAndCandidateSets(seq, terms, axiomSet, services);
                 for (JTerm axiom : axiomSet) {
                     axioms = axioms.add(axiom);
@@ -184,7 +185,7 @@ private HashSet<org.key_project.logic.Term> computeInstances(Services services,
             ImmutableSet<JTerm> axioms,
             TacletApp app) {
 
-        final HashSet<org.key_project.logic.Term> instances = new HashSet<>();
+        final LinkedHashSet<org.key_project.logic.Term> instances = new LinkedHashSet<>();
         final HashSet<JTerm> alreadyChecked = new HashSet<>();
         // The axioms are fixed for the sequent, so the congruence and the normalization are
         // built once here instead of once per avoid condition per candidate.

key.core/src/main/java/de/uka/ilkd/key/util/InfFlowProgVarRenamer.java

@@ -3,7 +3,6 @@
  * SPDX-License-Identifier: GPL-2.0-only */
 package de.uka.ilkd.key.util;
 
-import java.util.HashMap;
 import java.util.Map;
 
 import de.uka.ilkd.key.java.Services;
@@ -54,7 +53,7 @@ public InfFlowProgVarRenamer(JTerm[] terms, Map<JTerm, JTerm> preInitialisedRepl
         this.postfix = postfix;
         this.goalForVariableRegistration = goalForVariableRegistration;
         if (preInitialisedReplaceMap == null) {
-            this.replaceMap = new HashMap<>();
+            this.replaceMap = new LinkedHashMap<>();
         } else {
             this.replaceMap = preInitialisedReplaceMap;
         }
@@ -241,7 +240,7 @@ private JavaBlock renameJavaBlock(Map<LocationVariable, LocationVariable> progVa
     private Map<LocationVariable, LocationVariable> restrictToProgramVariables(
             Map<JTerm, JTerm> replaceMap) {
         Map<LocationVariable, LocationVariable> progVarReplaceMap =
-            new HashMap<>();
+            new LinkedHashMap<>();
         for (final JTerm t : replaceMap.keySet()) {
             if (t.op() instanceof LocationVariable lv) {
                 progVarReplaceMap.put(lv,

key.core/src/test/resources/de/uka/ilkd/key/prover/mt/shared-state-allowlist.txt

@@ -28,8 +28,6 @@ de.uka.ilkd.key.logic.op.QualifierWrapper#INSTANCES                            #
 de.uka.ilkd.key.proof.calculus.JavaDLSequentKit#INSTANCE                       # assigned once at class-init; reads via synchronized getInstance()
 de.uka.ilkd.key.proof.init.JavaProfile#defaultInstance                         # lazy singleton; every access inside synchronized getDefaultInstance()
 de.uka.ilkd.key.proof.init.JavaProfile#defaultInstancePermissions              # lazy singleton; every access inside synchronized getDefaultInstance()
-de.uka.ilkd.key.strategy.quantifierHeuristics.EqualityConstraint#joinCache     # every read/write inside synchronized(joinCacheMonitor)
-de.uka.ilkd.key.strategy.quantifierHeuristics.EqualityConstraint#joinCacheOld  # every read/write inside synchronized(joinCacheMonitor)
 
 # --- written only during single-threaded setup/loading, never by proof-search workers ---
 de.uka.ilkd.key.logic.sort.ArraySort#aSH                                       # mutated only via getArraySort during type modeling at load time; NOT safe for callers during proving