Modularity for Proof Strategies (#3650)

Author: wadoon

.gitignore

@@ -67,6 +67,7 @@ key/key.ui/examples/**/**.proof
 
 # generated by the antlr plugin of IntelliJ
 key.core/src/main/antlr4/gen/
+*.tokens
 
 scripts/tools/checkstyle/key_checks_incremental.xml
 checkstyle-diff.txt

key.core.infflow/src/main/java/de/uka/ilkd/key/informationflow/macros/PrepareInfFlowContractPreBranchesMacro.java

@@ -138,17 +138,9 @@ private String getAppRuleName(Node parent) {
             return parentRuleName;
         }
 
-
-        @Override
-        protected RuleAppCost instantiateApp(RuleApp app, PosInOccurrence pio, Goal goal,
-                MutableState mState) {
-            return computeCost(app, pio, goal, mState);
-        }
-
         @Override
         public boolean isStopAtFirstNonCloseableGoal() {
             return false;
         }
     }
-
 }

key.core.infflow/src/main/java/de/uka/ilkd/key/informationflow/macros/SelfcompositionStateExpansionMacro.java

@@ -12,10 +12,7 @@
 import de.uka.ilkd.key.proof.Goal;
 import de.uka.ilkd.key.proof.Proof;
 import de.uka.ilkd.key.proof.init.ProofOblInput;
-import de.uka.ilkd.key.strategy.JavaCardDLStrategyFactory;
-import de.uka.ilkd.key.strategy.RuleAppCostCollector;
-import de.uka.ilkd.key.strategy.Strategy;
-import de.uka.ilkd.key.strategy.StrategyProperties;
+import de.uka.ilkd.key.strategy.*;
 
 import org.key_project.logic.Name;
 import org.key_project.prover.proof.ProofGoal;
@@ -136,10 +133,10 @@ public Name name() {
             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<@NonNull Goal> javaDlStrategy =
+                ModularJavaDLStrategyFactory strategyFactory = new ModularJavaDLStrategyFactory();
+                Strategy<@NonNull Goal> dlStrategy =
                     strategyFactory.create(goal.proof(), new StrategyProperties());
-                RuleAppCost costs = javaDlStrategy.computeCost(ruleApp, pio, goal, mState);
+                RuleAppCost costs = dlStrategy.computeCost(ruleApp, pio, goal, mState);
                 if ("orLeft".equals(name)) {
                     costs = costs.add(NumberRuleAppCost.create(100));
                 }

key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/strategy/SymbolicExecutionStrategy.java

@@ -5,7 +5,6 @@
 
 import java.util.ArrayList;
 
-import de.uka.ilkd.key.logic.JTerm;
 import de.uka.ilkd.key.proof.Goal;
 import de.uka.ilkd.key.proof.Proof;
 import de.uka.ilkd.key.strategy.JavaCardDLStrategy;
@@ -85,7 +84,7 @@ private SymbolicExecutionStrategy(Proof proof, StrategyProperties sp) {
                 .equals(sp.get(StrategyProperties.SYMBOLIC_EXECUTION_ALIAS_CHECK_OPTIONS_KEY))) {
             // Make sure that an immediately alias check is performed by doing cuts of objects to
             // find out if they can be the same or not
-            RuleSetDispatchFeature instRsd = getInstantiationDispatcher();
+            RuleSetDispatchFeature instRsd = getDispatcher(StrategyAspect.Instantiation);
             enableInstantiate();
             final TermBuffer<Goal> buffer = new TermBuffer<>();
             Feature originalCut = instRsd.get(getHeuristic("cut"));
@@ -106,7 +105,7 @@ private SymbolicExecutionStrategy(Proof proof, StrategyProperties sp) {
      * {@inheritDoc}
      */
     @Override
-    protected Feature setupApprovalF() {
+    protected @NonNull Feature setupApprovalF() {
         Feature result = super.setupApprovalF();
         // Make sure that cuts are only applied if the cut term is not already part of the sequent.
         // This check is performed exactly before the rule is applied because the sequent might has
@@ -122,17 +121,17 @@ protected Feature setupApprovalF() {
      * {@inheritDoc}
      */
     @Override
-    protected Feature setupGlobalF(Feature dispatcher) {
+    protected @NonNull Feature setupGlobalF(@NonNull Feature dispatcher) {
         Feature globalF = super.setupGlobalF(dispatcher);
         // Make sure that modalities without symbolic execution label are executed first because
         // they might forbid rule application on modalities with symbolic execution label (see loop
         // body branches)
         globalF = add(globalF, ifZero(not(new BinaryFeature() {
             @Override
-            protected <Goal extends ProofGoal<@NonNull Goal>> boolean filter(RuleApp app,
-                    PosInOccurrence pos, Goal goal, MutableState mState) {
+            protected <GOAL extends ProofGoal<@NonNull GOAL>> boolean filter(RuleApp app,
+                    PosInOccurrence pos, GOAL goal, MutableState mState) {
                 return pos != null
-                        && SymbolicExecutionUtil.hasSymbolicExecutionLabel((JTerm) pos.subTerm());
+                        && SymbolicExecutionUtil.hasSymbolicExecutionLabel(pos.subTerm());
             }
         }), longConst(-3000)));
         // Make sure that the modality which executes a loop body is preferred against the
@@ -141,9 +140,9 @@ protected Feature setupGlobalF(Feature dispatcher) {
             add(globalF,
                 ifZero(add(new Feature() {
                     @Override
-                    public <Goal extends ProofGoal<@NonNull Goal>> RuleAppCost computeCost(
+                    public <GOAL extends ProofGoal<@NonNull GOAL>> RuleAppCost computeCost(
                             RuleApp app, PosInOccurrence pos,
-                            Goal goal, MutableState mState) {
+                            GOAL goal, MutableState mState) {
                         return pos != null ? cost(0) : TopRuleAppCost.INSTANCE;
                     }
                 },
@@ -302,7 +301,7 @@ public static class Factory implements StrategyFactory {
          * {@inheritDoc}
          */
         @Override
-        public StrategySettingsDefinition getSettingsDefinition() {
+        public @NonNull StrategySettingsDefinition getSettingsDefinition() {
             // Properties
             OneOfStrategyPropertyDefinition methodTreatment = new OneOfStrategyPropertyDefinition(
                 StrategyProperties.METHOD_OPTIONS_KEY, "Method Treatment",

key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/util/SymbolicExecutionUtil.java

@@ -46,7 +46,7 @@
 import de.uka.ilkd.key.settings.StrategySettings;
 import de.uka.ilkd.key.speclang.Contract;
 import de.uka.ilkd.key.speclang.OperationContract;
-import de.uka.ilkd.key.strategy.JavaCardDLStrategyFactory;
+import de.uka.ilkd.key.strategy.ModularJavaDLStrategyFactory;
 import de.uka.ilkd.key.strategy.Strategy;
 import de.uka.ilkd.key.strategy.StrategyProperties;
 import de.uka.ilkd.key.symbolic_execution.ExecutionVariableExtractor;
@@ -4325,7 +4325,7 @@ public static void initializeStrategy(SymbolicExecutionTreeBuilder builder) {
                 new SymbolicExecutionStrategy.Factory().create(proof, strategyProperties));
         } else {
             proof.setActiveStrategy(
-                new JavaCardDLStrategyFactory().create(proof, strategyProperties));
+                new ModularJavaDLStrategyFactory().create(proof, strategyProperties));
         }
     }
 

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

@@ -86,7 +86,6 @@ protected boolean ruleApplicationInContextAllowed(RuleApp ruleApp,
      * rejects everything else.
      */
     private static class PropExpansionStrategy implements Strategy<Goal> {
-
         private final Name NAME = new Name(PropExpansionStrategy.class.getSimpleName());
 
         private final Set<String> admittedRuleNames;
@@ -142,6 +141,5 @@ public void instantiateApp(RuleApp app, PosInOccurrence pio, Goal goal,
         public boolean isStopAtFirstNonCloseableGoal() {
             return false;
         }
-
     }
 }

key.core/src/main/java/de/uka/ilkd/key/nparser/KeyAst.java

@@ -5,7 +5,7 @@
 
 import java.net.URI;
 import java.net.URISyntaxException;
-import java.net.URL;
+import java.nio.file.Path;
 import java.util.ArrayList;
 import java.util.HashMap;
 import java.util.List;
@@ -129,7 +129,7 @@ public static class File extends KeyAst<KeYParser.FileContext> {
 
         /// Returns the includes (possible empty but not null) computed from the underlying parse
         /// tree.
-        public Includes getIncludes(URL base) {
+        public Includes getIncludes(Path base) {
             IncludeFinder finder = new IncludeFinder(base);
             accept(finder);
             return finder.getIncludes();

key.core/src/main/java/de/uka/ilkd/key/nparser/ParsingFacade.java

@@ -6,6 +6,7 @@
 import java.io.BufferedInputStream;
 import java.io.File;
 import java.io.IOException;
+import java.net.URISyntaxException;
 import java.net.URL;
 import java.nio.channels.Channels;
 import java.nio.channels.ReadableByteChannel;
@@ -70,7 +71,14 @@ public static List<KeyAst.File> parseFiles(URL url) throws IOException {
             reached.add(url);
             KeyAst.File ctx = parseFile(url);
             ctxs.add(ctx);
-            Collection<RuleSource> includes = ctx.getIncludes(url).getRuleSets();
+            Path path = null;
+            try {
+                path = Path.of(url.toURI());
+            } catch (URISyntaxException e) {
+                throw new IOException(e);
+            }
+            path = path.getParent();
+            Collection<RuleSource> includes = ctx.getIncludes(path).getRuleSets();
             for (RuleSource u : includes) {
                 if (!reached.contains(u.url())) {
                     queue.push(u.url());

key.core/src/main/java/de/uka/ilkd/key/nparser/builder/IncludeFinder.java

@@ -5,7 +5,8 @@
 
 import java.io.File;
 import java.net.MalformedURLException;
-import java.net.URL;
+import java.net.URI;
+import java.nio.file.Path;
 
 import de.uka.ilkd.key.nparser.KeYParser;
 import de.uka.ilkd.key.proof.init.Includes;
@@ -22,15 +23,12 @@
  * @see #getIncludes()
  */
 public class IncludeFinder extends AbstractBuilder<Void> {
-    private final URL base;
+    private final Path base;
     private final Includes includes = new Includes();
-    private final String basePath;
     private boolean ldt = false;
 
-    public IncludeFinder(URL base) {
+    public IncludeFinder(Path base) {
         this.base = base;
-        String a = base.getPath();
-        basePath = a.substring(0, a.lastIndexOf('/'));
     }
 
     @Override
@@ -44,29 +42,30 @@ public Void visitOne_include_statement(KeYParser.One_include_statementContext ct
     public Void visitOne_include(KeYParser.One_includeContext ctx) {
         String value = StringUtil.trim(ctx.getText(), "\"'");
         try {
-            addInclude(value, ctx.relfile != null);
+            addInclude(value);
         } catch (MalformedURLException e) {
             throw new BuildingException(ctx, e);
         }
         return null;
     }
 
-    private void addInclude(String filename, boolean relativePath) throws MalformedURLException {
+    private void addInclude(String filename) throws MalformedURLException {
         RuleSource source;
         if (!filename.endsWith(".key")) {
             filename += ".key";
         }
 
-        if (relativePath) {
-            filename = filename.replace('/', File.separatorChar); // Not required for Windows, but
-                                                                  // whatsoever
-            filename = filename.replace('\\', File.separatorChar); // Special handling for Linux
-            URL path = new URL(base.getProtocol(), base.getHost(), base.getPort(),
-                basePath + "/" + filename);
-            source = RuleSourceFactory.initRuleFile(path);
-        } else {
-            source = RuleSourceFactory.fromDefaultLocation(filename);
+        filename = filename.replace('/', File.separatorChar); // Not required for Windows, but
+        // whatsoever
+        filename = filename.replace('\\', File.separatorChar); // Special handling for Linux
+        var path = base.resolve(filename).normalize();
+        String pathString = path.toString().replace(File.separatorChar, '/'); // URIs on Windows
+
+        if (!(pathString.startsWith("file:") || pathString.startsWith("jar:"))) {
+            pathString = "file:///" + pathString;
         }
+        var url = URI.create(pathString).toURL();
+        source = RuleSourceFactory.initRuleFile(url);
         if (ldt) {
             includes.putLDT(filename, source);
         } else {

key.core/src/main/java/de/uka/ilkd/key/proof/Goal.java

@@ -650,6 +650,10 @@ public ImmutableList<Goal> apply(final RuleApp ruleApp) {
             removeLastAppliedRuleApp();
             node().setAppliedRuleApp(null);
             return null;
+        } catch (IndexOutOfBoundsException e) {
+            removeLastAppliedRuleApp();
+            node().setAppliedRuleApp(null);
+            return null;
         } finally {
             PERF_APP_EXECUTE.getAndAdd(System.nanoTime() - time);
         }