Improve thread-safety of KeY (#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.

Author: Drodt

key.core.symbolic_execution/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);

key.core.symbolic_execution/src/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<>();

key.core.symbolic_execution/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();

key.core.symbolic_execution/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());
             }

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

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

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

key.core/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();

key.core/src/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));
                 }

key.core/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)) {