Improve thread-safety of KeY (KeYProject#3335)

This PR prepares KeY for more parallelisation in an upcoming PR The changes are relatively low risk and improve code quality in general - Make strategies stateless - Move static cache to instance cache managed by ServiceCaches No introduction of synchronization primitives in this PR.
Drodt · Nov 14, 2023 · ac66700 · ac66700
2 parents e978aed + 6d635c8
commit ac66700
Show file tree

Hide file tree

Showing 167 changed files with 901 additions and 599 deletions.
diff --git a/...tion/src/main/java/de/uka/ilkd/key/symbolic_execution/strategy/CutHeapObjectsFeature.java b/...tion/src/main/java/de/uka/ilkd/key/symbolic_execution/strategy/CutHeapObjectsFeature.java
@@ -15,6 +15,7 @@
 import de.uka.ilkd.key.proof.Goal;
 import de.uka.ilkd.key.rule.RuleApp;
 import de.uka.ilkd.key.strategy.feature.BinaryFeature;
+import de.uka.ilkd.key.strategy.feature.MutableState;
 import de.uka.ilkd.key.strategy.termProjection.SVInstantiationProjection;
 
 /**
@@ -35,9 +36,10 @@ public class CutHeapObjectsFeature extends BinaryFeature {
      * {@inheritDoc}
      */
     @Override
-    protected boolean filter(RuleApp app, PosInOccurrence pos, Goal goal) {
+    protected boolean filter(RuleApp app, PosInOccurrence pos, Goal goal, MutableState mState) {
         Term cutFormula =
-            SVInstantiationProjection.create(new Name("cutFormula"), false).toTerm(app, pos, goal);
+            SVInstantiationProjection.create(new Name("cutFormula"), false).toTerm(app, pos, goal,
+                mState);
         if (cutFormula != null) {
             if (cutFormula.op() == Junctor.NOT) {
                 cutFormula = cutFormula.sub(0);

diff --git a/...rc/main/java/de/uka/ilkd/key/symbolic_execution/strategy/CutHeapObjectsTermGenerator.java b/...rc/main/java/de/uka/ilkd/key/symbolic_execution/strategy/CutHeapObjectsTermGenerator.java
@@ -17,6 +17,7 @@
 import de.uka.ilkd.key.logic.op.Function;
 import de.uka.ilkd.key.proof.Goal;
 import de.uka.ilkd.key.rule.RuleApp;
+import de.uka.ilkd.key.strategy.feature.MutableState;
 import de.uka.ilkd.key.strategy.termgenerator.TermGenerator;
 
 /**
@@ -31,7 +32,8 @@ public class CutHeapObjectsTermGenerator implements TermGenerator {
      * {@inheritDoc}
      */
     @Override
-    public Iterator<Term> generate(RuleApp app, PosInOccurrence pos, Goal goal) {
+    public Iterator<Term> generate(RuleApp app, PosInOccurrence pos, Goal goal,
+            MutableState mState) {
         // Compute collect terms of sequent formulas
         Sequent sequent = goal.sequent();
         Set<Term> topTerms = new LinkedHashSet<>();

diff --git a/...ution/src/main/java/de/uka/ilkd/key/symbolic_execution/strategy/SimplifyTermStrategy.java b/...ution/src/main/java/de/uka/ilkd/key/symbolic_execution/strategy/SimplifyTermStrategy.java
@@ -49,7 +49,7 @@ public Name name() {
     @Override
     protected Feature setupApprovalF() {
         Feature superFeature = super.setupApprovalF();
-        Feature labelFeature = (app, pos, goal) -> {
+        Feature labelFeature = (app, pos, goal, mState) -> {
             boolean hasLabel = false;
             if (pos != null && app instanceof TacletApp) {
                 Term findTerm = pos.subTerm();

diff --git a/.../src/main/java/de/uka/ilkd/key/symbolic_execution/strategy/SymbolicExecutionStrategy.java b/.../src/main/java/de/uka/ilkd/key/symbolic_execution/strategy/SymbolicExecutionStrategy.java
@@ -117,7 +117,8 @@ protected Feature setupGlobalF(Feature dispatcher) {
         // body branches)
         globalF = add(globalF, ifZero(not(new BinaryFeature() {
             @Override
-            protected boolean filter(RuleApp app, PosInOccurrence pos, Goal goal) {
+            protected boolean filter(RuleApp app, PosInOccurrence pos, Goal goal,
+                    MutableState mState) {
                 return pos != null
                         && SymbolicExecutionUtil.hasSymbolicExecutionLabel(pos.subTerm());
             }

diff --git a/key.core.testgen/src/main/java/de/uka/ilkd/key/macros/TestGenMacro.java b/key.core.testgen/src/main/java/de/uka/ilkd/key/macros/TestGenMacro.java
@@ -17,6 +17,7 @@
 import de.uka.ilkd.key.strategy.NumberRuleAppCost;
 import de.uka.ilkd.key.strategy.RuleAppCost;
 import de.uka.ilkd.key.strategy.Strategy;
+import de.uka.ilkd.key.strategy.feature.MutableState;
 
 public class TestGenMacro extends StrategyProofMacro {
     @Override
@@ -78,11 +79,12 @@ public TestGenStrategy(Strategy delegate) {
     }
 
     @Override
-    public RuleAppCost computeCost(RuleApp app, PosInOccurrence pio, Goal goal) {
+    public RuleAppCost computeCost(RuleApp app, PosInOccurrence pio, Goal goal,
+            MutableState mState) {
         if (TestGenStrategy.isUnwindRule(app.rule())) {
             return NumberRuleAppCost.create(TestGenStrategy.UNWIND_COST);
         }
-        return super.computeCost(app, pio, goal);
+        return super.computeCost(app, pio, goal, mState);
     }
 
     private int computeUnwindRules(Goal goal) {

diff --git a/key.core/src/main/java/de/uka/ilkd/key/api/Matcher.java b/key.core/src/main/java/de/uka/ilkd/key/api/Matcher.java
@@ -15,8 +15,9 @@
 import de.uka.ilkd.key.nparser.ParsingFacade;
 import de.uka.ilkd.key.rule.*;
 import de.uka.ilkd.key.rule.inst.SVInstantiations;
-import de.uka.ilkd.key.rule.match.legacy.LegacyTacletMatcher;
+import de.uka.ilkd.key.rule.match.vm.VMTacletMatcher;
 
+import org.key_project.util.collection.ImmutableArray;
 import org.key_project.util.collection.ImmutableList;
 
 import org.antlr.v4.runtime.CharStreams;
@@ -67,7 +68,7 @@ public List<VariableAssignments> matchPattern(String pattern, Sequent currentSeq
         Taclet t = parseTaclet(patternString, copyServices);
 
         // Build Matcher for Matchpattern
-        LegacyTacletMatcher ltm = new LegacyTacletMatcher(t);
+        VMTacletMatcher tacletMatcher = new VMTacletMatcher(t);
 
         // patternSequent should not be null, as we have created it
         assert t.ifSequent() != null;
@@ -79,9 +80,9 @@ public List<VariableAssignments> matchPattern(String pattern, Sequent currentSeq
         List<SearchNode> finalCandidates = new ArrayList<>(100);
         if (size > 0) {
             // Iteratoren durch die Sequent
-            ImmutableList<IfFormulaInstantiation> antecCand =
+            ImmutableArray<IfFormulaInstantiation> antecCand =
                 IfFormulaInstSeq.createList(currentSeq, true, copyServices);
-            ImmutableList<IfFormulaInstantiation> succCand =
+            ImmutableArray<IfFormulaInstantiation> succCand =
                 IfFormulaInstSeq.createList(currentSeq, false, copyServices);
 
             SequentFormula[] patternArray = new SequentFormula[patternSeq.size()];
@@ -93,16 +94,16 @@ public List<VariableAssignments> matchPattern(String pattern, Sequent currentSeq
 
             Queue<SearchNode> queue = new LinkedList<>();
             // init
-            queue.add(new SearchNode(patternArray, asize, antecCand, succCand));
+            queue.add(new SearchNode(patternArray, asize));
 
 
             while (!queue.isEmpty()) {
                 SearchNode node = queue.remove();
                 boolean inAntecedent = node.isAntecedent();
                 LOGGER.debug(inAntecedent ? "In Antec: " : "In Succ");
 
-                IfMatchResult ma = ltm.matchIf((inAntecedent ? antecCand : succCand),
-                    node.getPatternTerm(), node.mc, copyServices);
+                IfMatchResult ma = tacletMatcher.matchIf((inAntecedent ? antecCand : succCand),
+                    node.getPatternTerm(), node.getMatchConditions(), copyServices);
 
                 if (!ma.getMatchConditions().isEmpty()) {
                     ImmutableList<MatchConditions> testma = ma.getMatchConditions();
@@ -138,7 +139,7 @@ public List<VariableAssignments> matchPattern(String pattern, Sequent currentSeq
      */
     private VariableAssignments extractAssignments(SearchNode sn, VariableAssignments assignments) {
         VariableAssignments va = new VariableAssignments();
-        SVInstantiations insts = sn.mc.getInstantiations();
+        SVInstantiations insts = sn.getInstantiations();
         Set<String> varNames = assignments.getTypeMap().keySet();
         for (String varName : varNames) {
             SchemaVariable sv = insts.lookupVar(new Name(varName));

diff --git a/key.core/src/main/java/de/uka/ilkd/key/api/SearchNode.java b/key.core/src/main/java/de/uka/ilkd/key/api/SearchNode.java
@@ -5,31 +5,23 @@
 
 import de.uka.ilkd.key.logic.SequentFormula;
 import de.uka.ilkd.key.logic.Term;
-import de.uka.ilkd.key.rule.IfFormulaInstantiation;
 import de.uka.ilkd.key.rule.MatchConditions;
-
-import org.key_project.util.collection.ImmutableList;
+import de.uka.ilkd.key.rule.inst.SVInstantiations;
 
 /**
  * Created by sarah on 5/2/17.
  */
-public class SearchNode {
-    final SequentFormula[] pattern;
-    int pos = 0;
-    int succAntPos = 0;
-    public final MatchConditions mc;
-    final ImmutableList<IfFormulaInstantiation> antec;
-    final ImmutableList<IfFormulaInstantiation> succ;
-
+public final class SearchNode {
+    private final SequentFormula[] pattern;
+    private final int pos;
+    private final int succAntPos;
+    private final MatchConditions mc;
 
 
-    public SearchNode(SequentFormula[] pattern, int succAntPos,
-            ImmutableList<IfFormulaInstantiation> antec,
-            ImmutableList<IfFormulaInstantiation> succ) {
+    public SearchNode(SequentFormula[] pattern, int succAntPos) {
         this.pattern = pattern;
+        this.pos = 0;
         this.succAntPos = succAntPos;
-        this.antec = antec;
-        this.succ = succ;
         this.mc = MatchConditions.EMPTY_MATCHCONDITIONS;
     }
 
@@ -38,8 +30,6 @@ public SearchNode(SearchNode parent, MatchConditions cond) {
         this.succAntPos = parent.succAntPos;
         int parentPos = parent.pos;
         this.pos = parentPos + 1;
-        antec = parent.antec;
-        succ = parent.succ;
         mc = cond;
     }
 
@@ -55,4 +45,11 @@ public boolean isFinished() {
         return pos >= pattern.length;
     }
 
+    public SVInstantiations getInstantiations() {
+        return mc == null ? null : mc.getInstantiations();
+    }
+
+    public MatchConditions getMatchConditions() {
+        return mc;
+    }
 }
diff --git a/...e/src/main/java/de/uka/ilkd/key/control/instantiation_model/TacletInstantiationModel.java b/...e/src/main/java/de/uka/ilkd/key/control/instantiation_model/TacletInstantiationModel.java
@@ -15,6 +15,7 @@
 import de.uka.ilkd.key.rule.*;
 import de.uka.ilkd.key.rule.inst.SortException;
 
+import org.key_project.util.collection.ImmutableArray;
 import org.key_project.util.collection.ImmutableList;
 import org.key_project.util.collection.ImmutableSLList;
 
@@ -119,9 +120,9 @@ private void initIfChoiceModels() {
         int size = asize + ifseq.succedent().size();
 
         if (size > 0) {
-            ImmutableList<IfFormulaInstantiation> antecCand =
+            ImmutableArray<IfFormulaInstantiation> antecCand =
                 IfFormulaInstSeq.createList(seq, true, services);
-            ImmutableList<IfFormulaInstantiation> succCand =
+            ImmutableArray<IfFormulaInstantiation> succCand =
                 IfFormulaInstSeq.createList(seq, false, services);
 
             Iterator<SequentFormula> it = ifseq.iterator();

diff --git a/.../main/java/de/uka/ilkd/key/informationflow/macros/SelfcompositionStateExpansionMacro.java b/.../main/java/de/uka/ilkd/key/informationflow/macros/SelfcompositionStateExpansionMacro.java
@@ -22,6 +22,7 @@
 import de.uka.ilkd.key.strategy.Strategy;
 import de.uka.ilkd.key.strategy.StrategyProperties;
 import de.uka.ilkd.key.strategy.TopRuleAppCost;
+import de.uka.ilkd.key.strategy.feature.MutableState;
 
 import org.key_project.util.collection.ImmutableList;
 
@@ -123,14 +124,15 @@ public Name name() {
         }
 
         @Override
-        public RuleAppCost computeCost(RuleApp ruleApp, PosInOccurrence pio, Goal goal) {
+        public RuleAppCost computeCost(RuleApp ruleApp, PosInOccurrence pio, Goal goal,
+                MutableState mState) {
             String name = ruleApp.rule().name().toString();
             if ((admittedRuleNames.contains(name) || name.startsWith(INF_FLOW_UNFOLD_PREFIX))
                     && ruleApplicationInContextAllowed(ruleApp, pio, goal)) {
                 JavaCardDLStrategyFactory strategyFactory = new JavaCardDLStrategyFactory();
                 Strategy javaDlStrategy =
                     strategyFactory.create(goal.proof(), new StrategyProperties());
-                RuleAppCost costs = javaDlStrategy.computeCost(ruleApp, pio, goal);
+                RuleAppCost costs = javaDlStrategy.computeCost(ruleApp, pio, goal, mState);
                 if ("orLeft".equals(name)) {
                     costs = costs.add(NumberRuleAppCost.create(100));
                 }

diff --git a/...src/main/java/de/uka/ilkd/key/informationflow/macros/UseInformationFlowContractMacro.java b/...src/main/java/de/uka/ilkd/key/informationflow/macros/UseInformationFlowContractMacro.java
@@ -22,6 +22,7 @@
 import de.uka.ilkd.key.strategy.TopRuleAppCost;
 import de.uka.ilkd.key.strategy.feature.FocusIsSubFormulaOfInfFlowContractAppFeature;
 import de.uka.ilkd.key.strategy.feature.InfFlowContractAppFeature;
+import de.uka.ilkd.key.strategy.feature.MutableState;
 
 import org.key_project.util.collection.DefaultImmutableSet;
 import org.key_project.util.collection.ImmutableList;
@@ -181,7 +182,8 @@ public Name name() {
 
 
         @Override
-        public RuleAppCost computeCost(RuleApp ruleApp, PosInOccurrence pio, Goal goal) {
+        public RuleAppCost computeCost(RuleApp ruleApp, PosInOccurrence pio, Goal goal,
+                MutableState mState) {
             // first try to apply
             // - impLeft on previous information flow contract application
             // formula, else
@@ -190,14 +192,14 @@ public RuleAppCost computeCost(RuleApp ruleApp, PosInOccurrence pio, Goal goal)
             String name = ruleApp.rule().name().toString();
             if (name.startsWith(INF_FLOW_RULENAME_PREFIX)
                     && ruleApplicationInContextAllowed(ruleApp, pio, goal)) {
-                return InfFlowContractAppFeature.INSTANCE.computeCost(ruleApp, pio, goal);
+                return InfFlowContractAppFeature.INSTANCE.computeCost(ruleApp, pio, goal, mState);
             } else if (name.equals(DOUBLE_IMP_LEFT_RULENAME)) {
                 RuleAppCost impLeftCost = FocusIsSubFormulaOfInfFlowContractAppFeature.INSTANCE
-                        .computeCost(ruleApp, pio, goal);
+                        .computeCost(ruleApp, pio, goal, mState);
                 return impLeftCost.add(NumberRuleAppCost.create(-10010));
             } else if (name.equals(IMP_LEFT_RULENAME)) {
                 RuleAppCost impLeftCost = FocusIsSubFormulaOfInfFlowContractAppFeature.INSTANCE
-                        .computeCost(ruleApp, pio, goal);
+                        .computeCost(ruleApp, pio, goal, mState);
                 return impLeftCost.add(NumberRuleAppCost.create(-10000));
             } else if (admittedRuleNames.contains(name)
                     && ruleApplicationInContextAllowed(ruleApp, pio, goal)) {

diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/ServiceCaches.java b/key.core/src/main/java/de/uka/ilkd/key/java/ServiceCaches.java
@@ -23,10 +23,12 @@
 import de.uka.ilkd.key.strategy.feature.AbstractBetaFeature.TermInfo;
 import de.uka.ilkd.key.strategy.feature.AppliedRuleAppsNameCache;
 import de.uka.ilkd.key.strategy.quantifierHeuristics.ClausesGraph;
+import de.uka.ilkd.key.strategy.quantifierHeuristics.Metavariable;
 import de.uka.ilkd.key.strategy.quantifierHeuristics.TriggersSet;
 import de.uka.ilkd.key.util.Pair;
 
 import org.key_project.util.LRUCache;
+import org.key_project.util.collection.ImmutableSet;
 
 /**
  * <p>
@@ -147,6 +149,10 @@ public class ServiceCaches {
     private final AppliedRuleAppsNameCache appliedRuleAppsNameCache =
         new AppliedRuleAppsNameCache();
 
+    /** Cache used by EqualityConstraint to speed up meta variable search */
+    private final LRUCache<Term, ImmutableSet<Metavariable>> mvCache = new LRUCache<>(2000);
+
+
     /**
      * Returns the cache used by {@link TermTacletAppIndexCacheSet} instances.
      *
@@ -219,4 +225,9 @@ public final IfFormulaInstantiationCache getIfFormulaInstantiationCache() {
     public AppliedRuleAppsNameCache getAppliedRuleAppsNameCache() {
         return appliedRuleAppsNameCache;
     }
+
+    public LRUCache<Term, ImmutableSet<Metavariable>> getMVCache() {
+        return mvCache;
+    }
+
 }
diff --git a/key.core/src/main/java/de/uka/ilkd/key/logic/TermFactory.java b/key.core/src/main/java/de/uka/ilkd/key/logic/TermFactory.java
@@ -128,12 +128,11 @@ private ImmutableArray<Term> createSubtermArray(Term[] subs) {
     private Term doCreateTerm(Operator op, ImmutableArray<Term> subs,
             ImmutableArray<QuantifiableVariable> boundVars, JavaBlock javaBlock,
             ImmutableArray<TermLabel> labels, String origin) {
-        final Term newTerm =
+        final TermImpl newTerm =
             (labels == null || labels.isEmpty()
                     ? new TermImpl(op, subs, boundVars, javaBlock, origin)
-                    : new LabeledTermImpl(op, subs, boundVars, javaBlock, labels, origin))
-                            .checked();
-        // Check if caching is possible. It is not possible if a non empty JavaBlock is available
+                    : new LabeledTermImpl(op, subs, boundVars, javaBlock, labels, origin));
+        // Check if caching is possible. It is not possible if a non-empty JavaBlock is available
         // in the term or in one of its children because the meta information like PositionInfos
         // may be different.
         if (cache != null && !newTerm.containsJavaBlockRecursive()) {
@@ -142,14 +141,14 @@ private Term doCreateTerm(Operator op, ImmutableArray<Term> subs,
                 term = cache.get(newTerm);
             }
             if (term == null) {
-                term = newTerm;
+                term = newTerm.checked();
                 synchronized (cache) {
                     cache.put(term, term);
                 }
             }
             return term;
         } else {
-            return newTerm;
+            return newTerm.checked();
         }
     }
 

diff --git a/key.core/src/main/java/de/uka/ilkd/key/macros/AbstractBlastingMacro.java b/key.core/src/main/java/de/uka/ilkd/key/macros/AbstractBlastingMacro.java
@@ -41,6 +41,7 @@
 import de.uka.ilkd.key.strategy.RuleAppCostCollector;
 import de.uka.ilkd.key.strategy.Strategy;
 import de.uka.ilkd.key.strategy.TopRuleAppCost;
+import de.uka.ilkd.key.strategy.feature.MutableState;
 
 import org.key_project.util.collection.ImmutableList;
 
@@ -204,7 +205,8 @@ public Name name() {
         }
 
         @Override
-        public RuleAppCost computeCost(RuleApp app, PosInOccurrence pio, Goal goal) {
+        public RuleAppCost computeCost(RuleApp app, PosInOccurrence pio, Goal goal,
+                MutableState mState) {
 
             if (app.rule() instanceof OneStepSimplifier) {
                 return NumberRuleAppCost.getZeroCost();

diff --git a/key.core/src/main/java/de/uka/ilkd/key/macros/AbstractPropositionalExpansionMacro.java b/key.core/src/main/java/de/uka/ilkd/key/macros/AbstractPropositionalExpansionMacro.java
@@ -15,6 +15,7 @@
 import de.uka.ilkd.key.rule.OneStepSimplifierRuleApp;
 import de.uka.ilkd.key.rule.RuleApp;
 import de.uka.ilkd.key.strategy.*;
+import de.uka.ilkd.key.strategy.feature.MutableState;
 
 /**
  * The Class AbstractPropositionalExpansionMacro applies purely propositional rules.
@@ -96,12 +97,13 @@ public Name name() {
         }
 
         @Override
-        public RuleAppCost computeCost(RuleApp ruleApp, PosInOccurrence pio, Goal goal) {
+        public RuleAppCost computeCost(RuleApp ruleApp, PosInOccurrence pio, Goal goal,
+                MutableState mState) {
             String name = ruleApp.rule().name().toString();
             if (ruleApp instanceof OneStepSimplifierRuleApp && allowOSS) {
-                return delegate.computeCost(ruleApp, pio, goal);
+                return delegate.computeCost(ruleApp, pio, goal, mState);
             } else if (admittedRuleNames.contains(name)) {
-                final RuleAppCost origCost = delegate.computeCost(ruleApp, pio, goal);
+                final RuleAppCost origCost = delegate.computeCost(ruleApp, pio, goal, mState);
                 // pass through negative costs
                 if (origCost instanceof NumberRuleAppCost
                         && ((NumberRuleAppCost) origCost).getValue() < 0) {