Create a JSON-RPC for KeY

key.core.example/src/main/java/org/key_project/Main.java

@@ -96,6 +96,7 @@ private static void proveEnvironmemt(KeYEnvironment<?> env) {
                 LOGGER.info("Found contract '" + contract.getDisplayName());
                 proveContract(env, contract);
             }
+        } catch (InterruptedException ignored) {
         } finally {
             env.dispose(); // Ensure always that all instances of KeYEnvironment are disposed
         }
@@ -134,7 +135,8 @@ private static List<Contract> getContracts(KeYEnvironment<?> env) {
      * @param env the {@link KeYEnvironment} in which to prove the contract
      * @param contract the {@link Contract} to be proven
      */
-    private static void proveContract(KeYEnvironment<?> env, Contract contract) {
+    private static void proveContract(KeYEnvironment<?> env, Contract contract)
+            throws InterruptedException {
         Proof proof = null;
         try {
             // Create proof

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

@@ -36,7 +36,7 @@ public void taskStarted(TaskStartedInfo info) {
         numOfInvokedMacros++;
         if (superordinateListener != null) {
             superordinateListener.taskStarted(new DefaultTaskStartedInfo(TaskKind.Macro,
-                macroName + (macroName.length() == 0 ? "" : " -- ") + info.message(),
+                macroName + (macroName.isEmpty() ? "" : " -- ") + info.message(),
                 info.size()));
         }
     }

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

@@ -3,10 +3,7 @@
  * SPDX-License-Identifier: GPL-2.0-only */
 package de.uka.ilkd.key.proof;
 
-import java.util.ArrayList;
-import java.util.Collection;
-import java.util.LinkedList;
-import java.util.List;
+import java.util.*;
 import java.util.concurrent.atomic.AtomicLong;
 
 import de.uka.ilkd.key.java.Services;
@@ -15,16 +12,15 @@
 import de.uka.ilkd.key.logic.op.ProgramVariable;
 import de.uka.ilkd.key.pp.LogicPrinter;
 import de.uka.ilkd.key.pp.NotationInfo;
+import de.uka.ilkd.key.proof.mgt.RuleJustification;
 import de.uka.ilkd.key.proof.proofevent.NodeChangeJournal;
 import de.uka.ilkd.key.proof.proofevent.RuleAppInfo;
-import de.uka.ilkd.key.rule.AbstractExternalSolverRuleApp;
-import de.uka.ilkd.key.rule.IBuiltInRuleApp;
-import de.uka.ilkd.key.rule.NoPosTacletApp;
-import de.uka.ilkd.key.rule.TacletApp;
+import de.uka.ilkd.key.rule.*;
 import de.uka.ilkd.key.rule.inst.SVInstantiations;
 import de.uka.ilkd.key.rule.merge.MergeRule;
 import de.uka.ilkd.key.strategy.QueueRuleApplicationManager;
 import de.uka.ilkd.key.strategy.Strategy;
+import de.uka.ilkd.key.util.MiscTools;
 import de.uka.ilkd.key.util.properties.MapProperties;
 import de.uka.ilkd.key.util.properties.Properties;
 import de.uka.ilkd.key.util.properties.Properties.Property;
@@ -740,6 +736,13 @@ public List<RuleApp> getAllBuiltInRuleApps() {
         return ruleApps;
     }
 
+    /**
+     * Return a list with available taclet application on this goal.
+     */
+    public List<TacletApp> getAllTacletApps() {
+        return getAllTacletApps(proof().getServices());
+    }
+
     public List<TacletApp> getAllTacletApps(Services services) {
         RuleAppIndex index = ruleAppIndex();
         index.autoModeStopped();
@@ -764,4 +767,37 @@ protected boolean filter(Taclet taclet) {
         return allApps;
     }
 
+    /**
+     * Returns a list with all known rule applications within this proof goal.
+     */
+    public List<RuleApp> getAllAvailableRules() {
+        var taclets = getAllTacletApps();
+        var builtin = getAllBuiltInRuleApps();
+        builtin.addAll(taclets);
+        return builtin;
+    }
+
+    public List<Rule> getAvailableRules() {
+        var s = new ArrayList<Rule>(2048);
+        for (final BuiltInRule br : ruleAppIndex().builtInRuleAppIndex()
+                .builtInRuleIndex().rules()) {
+            s.add(br);
+        }
+
+        Set<NoPosTacletApp> set = ruleAppIndex().tacletIndex().allNoPosTacletApps();
+        OneStepSimplifier simplifier = MiscTools.findOneStepSimplifier(proof());
+        if (simplifier != null && !simplifier.isShutdown()) {
+            set.addAll(simplifier.getCapturedTaclets());
+        }
+
+        for (final NoPosTacletApp app : set) {
+            RuleJustification just = proof().mgt().getJustification(app);
+            if (just == null) {
+                continue; // do not break system because of this
+            }
+            s.add(app.taclet()); // TODO not good
+        }
+        return s;
+    }
+
 }

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

@@ -3,6 +3,7 @@
  * SPDX-License-Identifier: GPL-2.0-only */
 package de.uka.ilkd.key.proof;
 
+import java.util.*;
 import java.util.ArrayList;
 import java.util.Collection;
 import java.util.Collections;
@@ -12,6 +13,7 @@
 import java.util.LinkedList;
 import java.util.List;
 import java.util.ListIterator;
+import java.util.stream.Stream;
 
 import de.uka.ilkd.key.logic.RenamingTable;
 import de.uka.ilkd.key.logic.op.IProgramVariable;
@@ -50,11 +52,14 @@ public class Node implements Iterable<Node> {
 
     private static final String NODES = "nodes";
 
-    /** the proof the node belongs to */
+    /**
+     * the proof the node belongs to
+     */
     private final Proof proof;
 
     /** The parent node. **/
     private @Nullable Node parent = null;
+
     /**
      * The branch location of this proof node.
      */
@@ -82,7 +87,9 @@ public class Node implements Iterable<Node> {
 
     private boolean closed = false;
 
-    /** contains non-logical content, used for user feedback */
+    /**
+     * contains non-logical content, used for user feedback
+     */
     private NodeInfo nodeInfo;
 
     /**
@@ -161,7 +168,9 @@ public void setSequent(Sequent seq) {
         this.seq = seq;
     }
 
-    /** returns the sequent of this node */
+    /**
+     * returns the sequent of this node
+     */
     public Sequent sequent() {
         return seq;
     }
@@ -175,7 +184,9 @@ public NodeInfo getNodeInfo() {
         return nodeInfo;
     }
 
-    /** returns the proof the Node belongs to */
+    /**
+     * returns the proof the Node belongs to
+     */
     public Proof proof() {
         return proof;
     }
@@ -225,7 +236,9 @@ public RuleApp getAppliedRuleApp() {
         return appliedRuleApp;
     }
 
-    /** Returns the set of NoPosTacletApps at this node */
+    /**
+     * Returns the set of NoPosTacletApps at this node
+     */
     public Iterable<NoPosTacletApp> getLocalIntroducedRules() {
         return localIntroducedRules;
     }
@@ -249,7 +262,7 @@ public void addLocalProgVars(Iterable<? extends IProgramVariable> elements) {
 
     /**
      * Returns the set of freshly created function symbols known to this node.
-     *
+     * <p>
      * In the resulting list, the newest additions come first.
      *
      * @return a non-null immutable list of function symbols.
@@ -471,13 +484,14 @@ public Iterator<Node> subtreeIterator() {
         return new SubtreeIterator(this);
     }
 
-    /** @return number of children */
+    /**
+     * @return number of children
+     */
     public int childrenCount() {
         return children.size();
     }
 
     /**
-     *
      * @param i an index (starting at 0).
      * @return the i-th child of this node.
      */
@@ -667,7 +681,9 @@ public boolean sanityCheckDoubleLinks() {
         return true;
     }
 
-    /** marks a node as closed */
+    /**
+     * marks a node as closed
+     */
     Node close() {
         closed = true;
         Node tmp = parent;
@@ -684,7 +700,7 @@ Node close() {
     /**
      * Opens a previously closed node and all its closed parents.
      * <p>
-     *
+     * <p>
      * This is, for instance, needed for the {@link MergeRule}: In a situation where a merge node
      * and its associated partners have been closed and the merge node is then pruned away, the
      * partners have to be reopened again. Otherwise, we have a soundness issue.
@@ -699,7 +715,9 @@ void reopen() {
         clearNameCache();
     }
 
-    /** @return true iff this inner node is closeable */
+    /**
+     * @return true iff this inner node is closeable
+     */
     private boolean isCloseable() {
         assert childrenCount() > 0;
         for (Node child : children) {
@@ -838,4 +856,8 @@ public int getStepIndex() {
     void setStepIndex(int stepIndex) {
         this.stepIndex = stepIndex;
     }
+
+    public Stream<Node> childrenStream() {
+        return children.stream();
+    }
 }

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

@@ -0,0 +1,45 @@
+/* This file is part of KeY - https://key-project.org
+ * KeY is licensed under the GNU General Public License Version 2
+ * SPDX-License-Identifier: GPL-2.0-only */
+package de.uka.ilkd.key.proof;
+
+import java.io.Serializable;
+
+public class ProofNodeDescription implements Serializable {
+    /**
+     * Collects the information from the tree to which branch the current node belongs:
+     * <ul>
+     * <li>Invariant Initially Valid</li>
+     * <li>Body Preserves Invariant</li>
+     * <li>Use Case</li>
+     * <li>...</li>
+     * </ul>
+     *
+     * @param node the current node
+     * @return a String containing the path information to display
+     */
+    public static String collectPathInformation(Node node) {
+        while (node != null) {
+            if (node.getNodeInfo() != null && node.getNodeInfo().getBranchLabel() != null) {
+                String label = node.getNodeInfo().getBranchLabel();
+                /*
+                 * Are there other interesting labels? Please feel free to add them here.
+                 */
+                if (label.equals("Invariant Initially Valid")
+                        || label.equals("Invariant Preserved and Used") // for loop scope invariant
+                        || label.equals("Body Preserves Invariant") || label.equals("Use Case")
+                        || label.equals("Show Axiom Satisfiability") || label.startsWith("Pre (")
+                        || label.startsWith("Exceptional Post (") // exceptional postcondition
+                        || label.startsWith("Post (") // postcondition of a method
+                        || label.contains("Normal Execution") || label.contains("Null Reference")
+                        || label.contains("Index Out of Bounds") || label.contains("Validity")
+                        || label.contains("Precondition") || label.contains("Usage")) {
+                    return label;
+                }
+            }
+            node = node.parent();
+        }
+        // if no label was found we have to prove the postcondition
+        return "Show Postcondition/Modifiable";
+    }
+}

key.ui/src/main/java/de/uka/ilkd/key/core/Main.java

@@ -464,25 +464,27 @@ private AbstractMediatorUserInterfaceControl createUserInterface(List<Path> file
     }
 
     public static void ensureExamplesAvailable() {
-        File examplesDir = getExamplesDir() == null ? ExampleChooser.lookForExamples()
-                : new File(getExamplesDir());
-        if (!examplesDir.exists()) {
+        Path examplesDir = getExamplesDir() == null
+                ? ExampleChooser.lookForExamples()
+                : getExamplesDir();
+
+        if (!Files.exists(examplesDir)) {
             examplesDir = setupExamples();
         }
-        setExamplesDir(examplesDir.getAbsolutePath());
+        setExamplesDir(examplesDir.toAbsolutePath());
     }
 
-    private static File setupExamples() {
+    private static Path setupExamples() {
         try {
             URL examplesURL = Main.class.getResource("/examples.zip");
             if (examplesURL == null) {
                 throw new IOException("Missing examples.zip in resources");
             }
 
-            File tempDir = createTempDirectory();
+            Path tempDir = createTempDirectory();
 
             if (tempDir != null) {
-                IOUtil.extractZip(examplesURL.openStream(), tempDir.toPath());
+                IOUtil.extractZip(examplesURL.openStream(), tempDir);
             }
             return tempDir;
         } catch (IOException e) {
@@ -491,13 +493,9 @@ private static File setupExamples() {
         }
     }
 
-    private static File createTempDirectory() throws IOException {
-        final File tempDir = File.createTempFile("keyheap-examples-", null);
-        tempDir.delete();
-        if (!tempDir.mkdir()) {
-            return null;
-        }
-        Runtime.getRuntime().addShutdownHook(new Thread(() -> IOUtil.delete(tempDir)));
+    private static Path createTempDirectory() throws IOException {
+        Path tempDir = Files.createTempDirectory("keyheap-examples-");
+        Runtime.getRuntime().addShutdownHook(new Thread(() -> IOUtil.delete(tempDir.toFile())));
         return tempDir;
     }
 
@@ -541,7 +539,7 @@ private void preProcessInput()
         }
 
         if (inputFiles != null && !inputFiles.isEmpty()) {
-            Path f = inputFiles.get(0);
+            Path f = inputFiles.getFirst();
             if (Files.isDirectory(f)) {
                 workingDir = f;
             } else {
@@ -552,20 +550,20 @@ private void preProcessInput()
         }
     }
 
-    private static String EXAMPLE_DIR = null;
+    private static Path EXAMPLE_DIR = null;
 
-    public static @Nullable String getExamplesDir() {
+    public static @Nullable Path getExamplesDir() {
         return EXAMPLE_DIR;
     }
 
     /**
-     * Defines the examples directory. This method is used by the Eclipse
+     * Defines the examples' directory. This method is used by the Eclipse
      * integration (KeY4Eclipse)
      * to use the examples extract from the plug-in into the workspace.
      *
      * @param newExamplesDir The new examples directory to use.
      */
-    public static void setExamplesDir(String newExamplesDir) {
+    public static void setExamplesDir(Path newExamplesDir) {
         EXAMPLE_DIR = newExamplesDir;
     }
 }