diff --git a/key.core.example/src/main/java/org/key_project/Main.java b/key.core.example/src/main/java/org/key_project/Main.java index ca565fbae3b..415765778d6 100644 --- a/key.core.example/src/main/java/org/key_project/Main.java +++ b/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 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 diff --git a/key.core/src/main/java/de/uka/ilkd/key/macros/ProofMacroListener.java b/key.core/src/main/java/de/uka/ilkd/key/macros/ProofMacroListener.java index 1e1d871c1ec..efeed331615 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/macros/ProofMacroListener.java +++ b/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())); } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/Goal.java b/key.core/src/main/java/de/uka/ilkd/key/proof/Goal.java index 94fa2803998..0e398d1edf4 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/Goal.java +++ b/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 getAllBuiltInRuleApps() { return ruleApps; } + /** + * Return a list with available taclet application on this goal. + */ + public List getAllTacletApps() { + return getAllTacletApps(proof().getServices()); + } + public List 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 getAllAvailableRules() { + var taclets = getAllTacletApps(); + var builtin = getAllBuiltInRuleApps(); + builtin.addAll(taclets); + return builtin; + } + + public List getAvailableRules() { + var s = new ArrayList(2048); + for (final BuiltInRule br : ruleAppIndex().builtInRuleAppIndex() + .builtInRuleIndex().rules()) { + s.add(br); + } + + Set 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; + } + } diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/Node.java b/key.core/src/main/java/de/uka/ilkd/key/proof/Node.java index 93c58da43ce..fe064657e70 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/Node.java +++ b/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 { 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 { 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 getLocalIntroducedRules() { return localIntroducedRules; } @@ -249,7 +262,7 @@ public void addLocalProgVars(Iterable elements) { /** * Returns the set of freshly created function symbols known to this node. - * + *

* In the resulting list, the newest additions come first. * * @return a non-null immutable list of function symbols. @@ -471,13 +484,14 @@ public Iterator 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. *

- * + *

* 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 childrenStream() { + return children.stream(); + } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/ProofNodeDescription.java b/key.core/src/main/java/de/uka/ilkd/key/proof/ProofNodeDescription.java new file mode 100644 index 00000000000..30cd0d78bea --- /dev/null +++ b/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: + *

    + *
  • Invariant Initially Valid
    • + *
  • Body Preserves Invariant
    • + *
  • Use Case
    • + *
  • ...
    • + *
+ * + * @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"; + } +} diff --git a/key.ui/src/main/java/de/uka/ilkd/key/core/Main.java b/key.ui/src/main/java/de/uka/ilkd/key/core/Main.java index dc9ffcc611e..a3c0b134658 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/core/Main.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/core/Main.java @@ -464,25 +464,27 @@ private AbstractMediatorUserInterfaceControl createUserInterface(List 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; } } diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/Example.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/Example.java new file mode 100644 index 00000000000..f93329cbe06 --- /dev/null +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/Example.java @@ -0,0 +1,198 @@ +/* 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.gui; + +import java.io.IOException; +import java.nio.charset.StandardCharsets; +import java.nio.file.Files; +import java.nio.file.Path; +import java.util.ArrayList; +import java.util.Enumeration; +import java.util.List; +import java.util.Properties; +import javax.swing.tree.DefaultMutableTreeNode; +import javax.swing.tree.DefaultTreeModel; + +import org.slf4j.Logger; +import org.slf4j.LoggerFactory; + +/** + * This class wraps a {@link java.io.File} and has a special {@link #toString()} method only using + * the + * short file name w/o path. + *

+ * Used for displaying files in the examples list w/o prefix + */ +public class Example { + private static final Logger LOGGER = LoggerFactory.getLogger(Example.class); + /** + * This constant is accessed by the eclipse based projects. + */ + public static final String KEY_FILE_NAME = "project.key"; + + private static final String PROOF_FILE_NAME = "project.proof"; + + /** + * The default category under which examples range if they do not have {@link #KEY_PATH} + * set. + */ + public static final String DEFAULT_CATEGORY_PATH = "Unsorted"; + + /** + * The {@link Properties} key to specify the path in the tree. + */ + public static final String KEY_PATH = "example.path"; + + /** + * The {@link Properties} key to specify the name of the example. Directory name if left + * open. + */ + public static final String KEY_NAME = "example.name"; + + /** + * The {@link Properties} key to specify the file for the example. KEY_FILE_NAME by default + */ + public static final String KEY_FILE = "example.file"; + + /** + * The {@link Properties} key to specify the proof file in the tree. May be left open + */ + public static final String KEY_PROOF_FILE = "example.proofFile"; + + /** + * The {@link Properties} key to specify the path in the tree. Prefix to specify additional + * files to load. Append 1, 2, 3, ... + */ + public static final String ADDITIONAL_FILE_PREFIX = "example.additionalFile."; + + /** + * The {@link Properties} key to specify the path in the tree. Prefix to specify export + * files which are not shown as tabs in the example wizard but are extracted to Java + * projects in the Eclipse integration. Append 1, 2, 3, ... + */ + public static final String EXPORT_FILE_PREFIX = "example.exportFile."; + + public final Path exampleFile; + public final Path directory; + public final String description; + public final Properties properties; + + public Example(Path file) throws IOException { + this.exampleFile = file; + this.directory = file.getParent(); + this.properties = new Properties(); + StringBuilder sb = new StringBuilder(); + extractDescription(file, sb, properties); + this.description = sb.toString(); + } + + public Path getDirectory() { + return directory; + } + + public Path getProofFile() { + return directory.resolve(properties.getProperty(KEY_PROOF_FILE, PROOF_FILE_NAME)); + } + + public Path getObligationFile() { + return directory.resolve(properties.getProperty(KEY_FILE, KEY_FILE_NAME)); + } + + public String getName() { + return properties.getProperty(KEY_NAME, directory.getFileName().toString()); + } + + public String getDescription() { + return description; + } + + public Path getExampleFile() { + return exampleFile; + } + + public List getAdditionalFiles() { + var result = new ArrayList(); + int i = 1; + while (properties.containsKey(ADDITIONAL_FILE_PREFIX + i)) { + result.add(directory.resolve(properties.getProperty(ADDITIONAL_FILE_PREFIX + i))); + i++; + } + return result; + } + + public List getExportFiles() { + var result = new ArrayList(); + int i = 1; + while (properties.containsKey(EXPORT_FILE_PREFIX + i)) { + result.add(directory.resolve(properties.getProperty(EXPORT_FILE_PREFIX + i))); + i++; + } + return result; + } + + public String[] getPath() { + return properties.getProperty(KEY_PATH, DEFAULT_CATEGORY_PATH).split("/"); + } + + @Override + public String toString() { + return getName(); + } + + public void addToTreeModel(DefaultTreeModel model) { + DefaultMutableTreeNode node = + findChild((DefaultMutableTreeNode) model.getRoot(), getPath(), 0); + node.add(new DefaultMutableTreeNode(this)); + } + + private DefaultMutableTreeNode findChild(DefaultMutableTreeNode root, String[] path, + int from) { + if (from == path.length) { + return root; + } + Enumeration en = root.children(); + while (en.hasMoreElements()) { + DefaultMutableTreeNode node = (DefaultMutableTreeNode) en.nextElement(); + if (node.getUserObject().equals(path[from])) { + return findChild(node, path, from + 1); + } + } + // not found ==> add new + DefaultMutableTreeNode node = new DefaultMutableTreeNode(path[from]); + root.add(node); + return findChild(node, path, from + 1); + } + + public boolean hasProof() { + return properties.containsKey(KEY_PROOF_FILE); + } + + private static StringBuilder extractDescription(Path file, StringBuilder sb, + Properties properties) { + try { + boolean emptyLineSeen = false; + for (var line : Files.readAllLines(file, StandardCharsets.UTF_8)) { + if (emptyLineSeen) { + sb.append(line).append("\n"); + } else { + String trimmed = line.trim(); + if (trimmed.isEmpty()) { + emptyLineSeen = true; + } else { + if (!trimmed.startsWith("#")) { + String[] entry = trimmed.split(" *[:=] *", 2); + if (entry.length > 1) { + properties.put(entry[0], entry[1]); + } + } + } + } + } + } catch (IOException e) { + LOGGER.error("", e); + return sb; + } + return sb; + } +} diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/ExampleChooser.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/ExampleChooser.java index f5e40873058..21bf9149322 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/ExampleChooser.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/ExampleChooser.java @@ -6,12 +6,12 @@ import java.awt.*; import java.awt.event.MouseAdapter; import java.awt.event.MouseEvent; -import java.io.BufferedReader; import java.io.File; -import java.io.FileReader; import java.io.IOException; -import java.nio.charset.StandardCharsets; -import java.util.*; +import java.nio.file.Files; +import java.nio.file.Path; +import java.nio.file.Paths; +import java.util.ArrayList; import java.util.List; import javax.swing.*; import javax.swing.border.TitledBorder; @@ -26,6 +26,7 @@ import org.key_project.util.java.IOUtil; +import org.jspecify.annotations.Nullable; import org.slf4j.Logger; import org.slf4j.LoggerFactory; @@ -39,15 +40,6 @@ public final class ExampleChooser extends JDialog { */ public static final String EXAMPLES_PATH = "examples"; - private static final long serialVersionUID = -4405666868752394532L; - - /** - * This constant is accessed by the eclipse based projects. - */ - public static final String KEY_FILE_NAME = "project.key"; - - private static final String PROOF_FILE_NAME = "project.proof"; - /** * Java property name to specify a custom key example folder. */ @@ -70,165 +62,21 @@ public final class ExampleChooser extends JDialog { /** * The result value of the dialog. null if nothing to be loaded */ - private File fileToLoad = null; + private Path fileToLoad = null; /** * The currently selected example. null if none selected */ private Example selectedExample; - /** - * This class wraps a {@link File} and has a special {@link #toString()} method only using the - * short file name w/o path. - *

- * Used for displaying files in the examples list w/o prefix - */ - public static class Example { - /** - * The default category under which examples range if they do not have {@link #KEY_PATH} - * set. - */ - private static final String DEFAULT_CATEGORY_PATH = "Unsorted"; - - /** - * The {@link Properties} key to specify the path in the tree. - */ - private static final String KEY_PATH = "example.path"; - - /** - * The {@link Properties} key to specify the name of the example. Directory name if left - * open. - */ - private static final String KEY_NAME = "example.name"; - - /** - * The {@link Properties} key to specify the file for the example. KEY_FILE_NAME by default - */ - private static final String KEY_FILE = "example.file"; - - /** - * The {@link Properties} key to specify the proof file in the tree. May be left open - */ - private static final String KEY_PROOF_FILE = "example.proofFile"; - - /** - * The {@link Properties} key to specify the path in the tree. Prefix to specify additional - * files to load. Append 1, 2, 3, ... - */ - private static final String ADDITIONAL_FILE_PREFIX = "example.additionalFile."; - - /** - * The {@link Properties} key to specify the path in the tree. Prefix to specify export - * files which are not shown as tabs in the example wizard but are extracted to Java - * projects in the Eclipse integration. Append 1, 2, 3, ... - */ - private static final String EXPORT_FILE_PREFIX = "example.exportFile."; - - private final File exampleFile; - private final File directory; - private final String description; - private final Properties properties; - - public Example(File file) throws IOException { - this.exampleFile = file; - this.directory = file.getParentFile(); - this.properties = new Properties(); - StringBuilder sb = new StringBuilder(); - extractDescription(file, sb, properties); - this.description = sb.toString(); - } - - public File getDirectory() { - return directory; - } - - public File getProofFile() { - return new File(directory, properties.getProperty(KEY_PROOF_FILE, PROOF_FILE_NAME)); - } - - public File getObligationFile() { - return new File(directory, properties.getProperty(KEY_FILE, KEY_FILE_NAME)); - } - - public String getName() { - return properties.getProperty(KEY_NAME, directory.getName()); - } - - public String getDescription() { - return description; - } - - public File getExampleFile() { - return exampleFile; - } - - public List getAdditionalFiles() { - ArrayList result = new ArrayList<>(); - int i = 1; - while (properties.containsKey(ADDITIONAL_FILE_PREFIX + i)) { - result.add(new File(directory, properties.getProperty(ADDITIONAL_FILE_PREFIX + i))); - i++; - } - return result; - } - - public List getExportFiles() { - ArrayList result = new ArrayList<>(); - int i = 1; - while (properties.containsKey(EXPORT_FILE_PREFIX + i)) { - result.add(new File(directory, properties.getProperty(EXPORT_FILE_PREFIX + i))); - i++; - } - return result; - } - - public String[] getPath() { - return properties.getProperty(KEY_PATH, DEFAULT_CATEGORY_PATH).split("/"); - } - - @Override - public String toString() { - return getName(); - } - - public void addToTreeModel(DefaultTreeModel model) { - DefaultMutableTreeNode node = - findChild((DefaultMutableTreeNode) model.getRoot(), getPath(), 0); - node.add(new DefaultMutableTreeNode(this)); - } - - private DefaultMutableTreeNode findChild(DefaultMutableTreeNode root, String[] path, - int from) { - if (from == path.length) { - return root; - } - Enumeration en = root.children(); - while (en.hasMoreElements()) { - DefaultMutableTreeNode node = (DefaultMutableTreeNode) en.nextElement(); - if (node.getUserObject().equals(path[from])) { - return findChild(node, path, from + 1); - } - } - // not found ==> add new - DefaultMutableTreeNode node = new DefaultMutableTreeNode(path[from]); - root.add(node); - return findChild(node, path, from + 1); - } - - public boolean hasProof() { - return properties.containsKey(KEY_PROOF_FILE); - } - - } // ------------------------------------------------------------------------- // constructors // ------------------------------------------------------------------------- - private ExampleChooser(File examplesDir) { + private ExampleChooser(Path examplesDir) { super(MainWindow.getInstance(), "Load Example", true); assert examplesDir != null; - assert examplesDir.isDirectory(); // create list panel final JPanel listPanel = new JPanel(); @@ -341,10 +189,10 @@ public void mouseClicked(MouseEvent e) { // internal methods // ------------------------------------------------------------------------- - public static File lookForExamples() { + public static Path lookForExamples() { // weigl: using java properties: -Dkey.examples.dir="..." if (System.getProperty(KEY_EXAMPLE_DIR) != null) { - return new File(System.getProperty(KEY_EXAMPLE_DIR)); + return Paths.get(System.getProperty(KEY_EXAMPLE_DIR)); } // greatly simplified version without parent path lookup. @@ -352,47 +200,18 @@ public static File lookForExamples() { if (!folder.exists()) { folder = new File(IOUtil.getClassLocation(ExampleChooser.class), EXAMPLES_PATH); } - return folder; + return folder.toPath(); } - private static String fileAsString(File f) { + private static String fileAsString(Path f) { try { - return IOUtil.readFrom(f); + return Files.readString(f); } catch (IOException e) { LOGGER.error("Could not read file '{}'", f, e); return ""; } } - private static StringBuilder extractDescription(File file, StringBuilder sb, - Properties properties) { - try (BufferedReader r = new BufferedReader(new FileReader(file, StandardCharsets.UTF_8))) { - String line; - boolean emptyLineSeen = false; - while ((line = r.readLine()) != null) { - if (emptyLineSeen) { - sb.append(line).append("\n"); - } else { - String trimmed = line.trim(); - if (trimmed.length() == 0) { - emptyLineSeen = true; - } else if (trimmed.startsWith("#")) { - // ignore - } else { - String[] entry = trimmed.split(" *[:=] *", 2); - if (entry.length > 1) { - properties.put(entry[0], entry[1]); - } - } - } - } - } catch (IOException e) { - LOGGER.error("", e); - return sb; - } - return sb; - } - private void updateDescription() { @@ -414,8 +233,8 @@ private void updateDescription() { if (p >= 0) { addTab(fileAsString.substring(p), "Proof Obligation", false); } - for (File file : example.getAdditionalFiles()) { - addTab(fileAsString(file), file.getName(), false); + for (Path file : example.getAdditionalFiles()) { + addTab(fileAsString(file), file.getFileName().toString(), false); } loadButton.setEnabled(true); loadProofButton.setEnabled(example.hasProof()); @@ -447,16 +266,16 @@ private void addTab(String string, String name, boolean wrap) { * Shows the dialog, using the passed examples directory. If null is passed, tries to find * examples directory on its own. */ - public static File showInstance(String examplesDirString) { + public static @Nullable Path showInstance(Path examplesDirString) { // get examples directory - File examplesDir; + Path examplesDir; if (examplesDirString == null) { examplesDir = lookForExamples(); } else { - examplesDir = new File(examplesDirString); + examplesDir = examplesDirString; } - if (!examplesDir.isDirectory()) { + if (!Files.isDirectory(examplesDir)) { JOptionPane.showMessageDialog(MainWindow.getInstance(), "The examples directory cannot be found.\n" + "Please install them at " + (examplesDirString == null ? IOUtil.getProjectRoot(ExampleChooser.class) + "/" @@ -483,19 +302,17 @@ public static File showInstance(String examplesDirString) { * @param examplesDir The examples directory to list examples in. * @return The found examples. */ - public static List listExamples(File examplesDir) { - List result = new LinkedList<>(); - - String line; - final File index = new File(new File(examplesDir, "index"), "samplesIndex.txt"); - try (BufferedReader br = - new BufferedReader(new FileReader(index, StandardCharsets.UTF_8))) { - while ((line = br.readLine()) != null) { + public static List listExamples(Path examplesDir) { + List result = new ArrayList<>(64); + + final Path index = examplesDir.resolve("index").resolve("samplesIndex.txt"); + try { + for (var line : Files.readAllLines(index)) { line = line.trim(); - if (line.startsWith("#") || line.length() == 0) { + if (line.startsWith("#") || line.isEmpty()) { continue; } - File f = new File(examplesDir, line); + Path f = examplesDir.resolve(line); try { result.add(new Example(f)); } catch (IOException e) { diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/ProofMacroWorker.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/ProofMacroWorker.java index e3ba8f7dee1..cac18137e4c 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/ProofMacroWorker.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/ProofMacroWorker.java @@ -5,6 +5,8 @@ import java.util.ArrayList; import java.util.List; +import java.util.concurrent.locks.Condition; +import java.util.concurrent.locks.ReentrantLock; import javax.swing.*; import de.uka.ilkd.key.control.InteractionListener; @@ -70,6 +72,8 @@ public class ProofMacroWorker extends SwingWorker private Exception exception; private final List interactionListeners = new ArrayList<>(); + private final Condition finish; + /** * Instantiates a new proof macro worker. * @@ -86,6 +90,8 @@ public ProofMacroWorker(Node node, ProofMacro macro, KeYMediator mediator, this.macro = macro; this.mediator = mediator; this.posInOcc = posInOcc; + + finish = new ReentrantLock().newCondition(); } @Override @@ -106,6 +112,8 @@ protected ProofMacroFinishedInfo doInBackground() { } catch (final Exception exception) { // This should actually never happen. this.exception = exception; + } finally { + finish.signalAll(); } return info; @@ -121,8 +129,7 @@ protected void done() { synchronized (macro) { mediator.removeInterruptedListener(this); if (!isCancelled() && exception != null) { // user cancelled task is fine, we do not - // report this - // This should actually never happen. + // report this // This should actually never happen. LOGGER.error("", exception); IssueDialog.showExceptionDialog(MainWindow.getInstance(), exception); } @@ -169,4 +176,11 @@ private void selectOpenGoalBelow() { } } } + + /** + * @return a condition for waiting on this thread to be finished + */ + public Condition getFinish() { + return finish; + } } diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/OpenExampleAction.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/OpenExampleAction.java index a630237bd5f..49265a1dcb5 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/OpenExampleAction.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/OpenExampleAction.java @@ -4,7 +4,7 @@ package de.uka.ilkd.key.gui.actions; import java.awt.event.ActionEvent; -import java.io.File; +import java.nio.file.Path; import de.uka.ilkd.key.core.Main; import de.uka.ilkd.key.gui.ExampleChooser; @@ -16,12 +16,6 @@ * Opens a file dialog allowing to select the example to be loaded */ public final class OpenExampleAction extends MainWindowAction { - - /** - * - */ - private static final long serialVersionUID = -7703620988220254791L; - public OpenExampleAction(MainWindow mainWindow) { super(mainWindow); setName("Load Example..."); @@ -30,10 +24,10 @@ public OpenExampleAction(MainWindow mainWindow) { } public void actionPerformed(ActionEvent e) { - File file = ExampleChooser.showInstance(Main.getExamplesDir()); + Path file = ExampleChooser.showInstance(Main.getExamplesDir()); if (file != null) { - KeYFileChooser.getFileChooser("Select file to load").setSelectedFile(file); - mainWindow.loadProblem(file.toPath()); + KeYFileChooser.getFileChooser("Select file to load").setSelectedFile(file.toFile()); + mainWindow.loadProblem(file); } } } diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/RunAllProofsAction.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/RunAllProofsAction.java index 798ce7bcdbd..62a52707985 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/RunAllProofsAction.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/RunAllProofsAction.java @@ -100,7 +100,7 @@ public RunAllProofsAction(MainWindow mainWindow) { super(mainWindow); Main.ensureExamplesAvailable(); - exampleDir = Paths.get(Main.getExamplesDir()); + exampleDir = Main.getExamplesDir(); try { files = loadFiles(); diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/sourceview/SourceView.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/sourceview/SourceView.java index b5fbbbc88bc..ee0da259ca4 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/sourceview/SourceView.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/sourceview/SourceView.java @@ -47,6 +47,7 @@ import de.uka.ilkd.key.proof.Node; import de.uka.ilkd.key.proof.Proof; import de.uka.ilkd.key.proof.ProofJavaSourceCollection; +import de.uka.ilkd.key.proof.ProofNodeDescription; import de.uka.ilkd.key.proof.io.consistency.FileRepo; import de.uka.ilkd.key.settings.ProofIndependentSettings; @@ -684,7 +685,7 @@ private void updateGUI() { } // set the path information in the status bar - sourceStatusBar.setText(collectPathInformation(currentNode)); + sourceStatusBar.setText(ProofNodeDescription.collectPathInformation(currentNode)); } else { tabPane.setBorder(new TitledBorder(NO_SOURCE)); sourceStatusBar.setText(NO_SOURCE); @@ -822,43 +823,6 @@ private static PositionInfo joinPositionsRec(SourceElement se) { } } - /** - * Collects the information from the tree to which branch the current node belongs: - *

    - *
  • Invariant Initially Valid
    • - *
  • Body Preserves Invariant
    • - *
  • Use Case
    • - *
  • ...
    • - *
- * - * @param node the current node - * @return a String containing the path information to display - */ - private 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"; - } - /** * The type of the tabbed pane contained in this {@code SourceView}. * diff --git a/key.ui/src/main/java/de/uka/ilkd/key/ui/ConsoleUserInterfaceControl.java b/key.ui/src/main/java/de/uka/ilkd/key/ui/ConsoleUserInterfaceControl.java index 4b33d65c79b..fcc53a3d524 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/ui/ConsoleUserInterfaceControl.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/ui/ConsoleUserInterfaceControl.java @@ -181,7 +181,11 @@ public void taskFinished(TaskFinishedInfo info) { } else if (macroChosen()) { applyMacro(); } else { - finish(proof); + try { + finish(proof); + } catch (InterruptedException e) { + throw new RuntimeException(e); + } } } } @@ -238,7 +242,7 @@ public void registerProofAggregate(ProofAggregate pa) { proofStack = proofStack.prepend(pa.getFirstProof()); } - void finish(Proof proof) { + void finish(Proof proof) throws InterruptedException { // setInteractive(false) has to be called because the ruleAppIndex // has to be notified that we work in auto mode (CS) mediator.setInteractive(false); diff --git a/keydata.py b/keydata.py new file mode 100644 index 00000000000..59511c2a7a8 --- /dev/null +++ b/keydata.py @@ -0,0 +1,493 @@ +from __future__ import annotations +import enum +import abc +import typing +from abc import abstractmethod, ABCMeta + +class ExampleDesc: + """""" + + name : str + """""" + + description : str + """""" + + def __init__(self, name, description): + self.name = name + self.description = description + +class ProofScriptCommandDesc: + """""" + + def __init__(self, ): + pass + + +class ProofMacroDesc: + """""" + + name : str + """""" + + category : str + """""" + + description : str + """""" + + scriptCommandName : str + """""" + + def __init__(self, name, category, description, scriptCommandName): + self.name = name + self.category = category + self.description = description + self.scriptCommandName = scriptCommandName + +class TraceValue(enum.Enum): + """""" + + Off = None + Message = None + All = None + +class SetTraceParams: + """""" + + value : TraceValue + """""" + + def __init__(self, value): + self.value = value + +class EnvironmentId: + """""" + + envId : str + """""" + + def __init__(self, envId): + self.envId = envId + +class ProofId: + """""" + + env : EnvironmentId + """""" + + proofId : str + """""" + + def __init__(self, env, proofId): + self.env = env + self.proofId = proofId + +class TreeNodeDesc: + """""" + + def __init__(self, ): + pass + + +class TreeNodeId: + """""" + + id : str + """""" + + def __init__(self, id): + self.id = id + +class NodeId: + """""" + + proofId : ProofId + """""" + + nodeId : int + """""" + + def __init__(self, proofId, nodeId): + self.proofId = proofId + self.nodeId = nodeId + +class PrintOptions: + """""" + + unicode : bool + """""" + + width : int + """""" + + indentation : int + """""" + + pure : bool + """""" + + termLabels : bool + """""" + + def __init__(self, unicode, width, indentation, pure, termLabels): + self.unicode = unicode + self.width = width + self.indentation = indentation + self.pure = pure + self.termLabels = termLabels + +class NodeTextId: + """""" + + nodeId : NodeId + """""" + + nodeTextId : int + """""" + + def __init__(self, nodeId, nodeTextId): + self.nodeId = nodeId + self.nodeTextId = nodeTextId + +class NodeTextDesc: + """""" + + id : NodeTextId + """""" + + result : str + """""" + + def __init__(self, id, result): + self.id = id + self.result = result + +class TermActionId: + """""" + + nodeId : NodeId + """""" + + pio : str + """""" + + id : str + """""" + + def __init__(self, nodeId, pio, id): + self.nodeId = nodeId + self.pio = pio + self.id = id + +class TermActionKind(enum.Enum): + """""" + + BuiltIn = None + Script = None + Macro = None + Taclet = None + +class TermActionDesc: + """""" + + commandId : TermActionId + """""" + + displayName : str + """""" + + description : str + """""" + + category : str + """""" + + kind : TermActionKind + """""" + + def __init__(self, commandId, displayName, description, category, kind): + self.commandId = commandId + self.displayName = displayName + self.description = description + self.category = category + self.kind = kind + +class List: + """""" + + def __init__(self, ): + pass + + +class SortDesc: + """""" + + string : str + """""" + + documentation : str + """""" + + extendsSorts : List + """""" + + anAbstract : bool + """""" + + s : str + """""" + + def __init__(self, string, documentation, extendsSorts, anAbstract, s): + self.string = string + self.documentation = documentation + self.extendsSorts = extendsSorts + self.anAbstract = anAbstract + self.s = s + +class FunctionDesc: + """""" + + name : str + """""" + + sort : str + """""" + + retSort : SortDesc + """""" + + argSorts : List + """""" + + rigid : bool + """""" + + unique : bool + """""" + + skolemConstant : bool + """""" + + def __init__(self, name, sort, retSort, argSorts, rigid, unique, skolemConstant): + self.name = name + self.sort = sort + self.retSort = retSort + self.argSorts = argSorts + self.rigid = rigid + self.unique = unique + self.skolemConstant = skolemConstant + +class ContractId: + """""" + + envId : EnvironmentId + """""" + + contractId : int + """""" + + def __init__(self, envId, contractId): + self.envId = envId + self.contractId = contractId + +class ContractDesc: + """""" + + contractId : ContractId + """""" + + name : str + """""" + + displayName : str + """""" + + typeName : str + """""" + + htmlText : str + """""" + + plainText : str + """""" + + def __init__(self, contractId, name, displayName, typeName, htmlText, plainText): + self.contractId = contractId + self.name = name + self.displayName = displayName + self.typeName = typeName + self.htmlText = htmlText + self.plainText = plainText + +class LoadParams: + """""" + + keyFile : str + """""" + + javaFile : str + """""" + + classPath : List + """""" + + bootClassPath : str + """""" + + includes : List + """""" + + def __init__(self, keyFile, javaFile, classPath, bootClassPath, includes): + self.keyFile = keyFile + self.javaFile = javaFile + self.classPath = classPath + self.bootClassPath = bootClassPath + self.includes = includes + +class ProblemDefinition: + """""" + + sorts : List + """""" + + functions : List + """""" + + predicates : List + """""" + + antecTerms : List + """""" + + succTerms : List + """""" + + def __init__(self, sorts, functions, predicates, antecTerms, succTerms): + self.sorts = sorts + self.functions = functions + self.predicates = predicates + self.antecTerms = antecTerms + self.succTerms = succTerms + +class LogTraceParams: + """""" + + messag : str + """""" + + verbose : str + """""" + + def __init__(self, messag, verbose): + self.messag = messag + self.verbose = verbose + +class MessageType(enum.Enum): + """""" + + Unused = None + Error = None + Warning = None + Info = None + Log = None + Debug = None + +class ShowMessageParams: + """""" + + type : MessageType + """""" + + message : str + """""" + + def __init__(self, type, message): + self.type = type + self.message = message + +class ShowMessageRequestParams: + """""" + + type : MessageType + """""" + + message : str + """""" + + actions : List + """""" + + def __init__(self, type, message, actions): + self.type = type + self.message = message + self.actions = actions + +class MessageActionItem: + """""" + + title : str + """""" + + def __init__(self, title): + self.title = title + +class Range: + """""" + + start : int + """""" + + end : int + """""" + + def __init__(self, start, end): + self.start = start + self.end = end + +class ShowDocumentParams: + """""" + + uri : str + """""" + + external : bool + """""" + + takeFocus : bool + """""" + + selection : Range + """""" + + def __init__(self, uri, external, takeFocus, selection): + self.uri = uri + self.external = external + self.takeFocus = takeFocus + self.selection = selection + +class ShowDocumentResult: + """""" + + success : bool + """""" + + def __init__(self, success): + self.success = success + +class TaskFinishedInfo: + """""" + + def __init__(self, ): + pass + + +class TaskStartedInfo: + """""" + + def __init__(self, ): + pass + + +KEY_DATA_CLASSES = { "ExampleDesc": ExampleDesc,"ProofScriptCommandDesc": ProofScriptCommandDesc,"ProofMacroDesc": ProofMacroDesc,"TraceValue": TraceValue,"SetTraceParams": SetTraceParams,"EnvironmentId": EnvironmentId,"ProofId": ProofId,"TreeNodeDesc": TreeNodeDesc,"TreeNodeId": TreeNodeId,"NodeId": NodeId,"PrintOptions": PrintOptions,"NodeTextId": NodeTextId,"NodeTextDesc": NodeTextDesc,"TermActionId": TermActionId,"TermActionKind": TermActionKind,"TermActionDesc": TermActionDesc,"List": List,"SortDesc": SortDesc,"FunctionDesc": FunctionDesc,"ContractId": ContractId,"ContractDesc": ContractDesc,"LoadParams": LoadParams,"ProblemDefinition": ProblemDefinition,"LogTraceParams": LogTraceParams,"MessageType": MessageType,"ShowMessageParams": ShowMessageParams,"ShowMessageRequestParams": ShowMessageRequestParams,"MessageActionItem": MessageActionItem,"Range": Range,"ShowDocumentParams": ShowDocumentParams,"ShowDocumentResult": ShowDocumentResult,"TaskFinishedInfo": TaskFinishedInfo,"TaskStartedInfo": TaskStartedInfo } + diff --git a/keyext.api.doc/build.gradle b/keyext.api.doc/build.gradle new file mode 100644 index 00000000000..5522b0a95c7 --- /dev/null +++ b/keyext.api.doc/build.gradle @@ -0,0 +1,13 @@ +plugins { + id "application" +} + +dependencies { + implementation(project(":keyext.api")) + implementation("org.freemarker:freemarker:2.3.34") + implementation("info.picocli:picocli:4.7.6") +} + +application { + mainClass.set("org.key_project.key.api.doc.Main") +} diff --git a/keyext.api.doc/src/main/java/org/key_project/key/api/doc/DocGen.java b/keyext.api.doc/src/main/java/org/key_project/key/api/doc/DocGen.java new file mode 100644 index 00000000000..69da9c866de --- /dev/null +++ b/keyext.api.doc/src/main/java/org/key_project/key/api/doc/DocGen.java @@ -0,0 +1,95 @@ +/* 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 org.key_project.key.api.doc; + +import de.uka.ilkd.key.util.KeYConstants; +import de.uka.ilkd.key.util.KeYResourceManager; +import freemarker.core.HTMLOutputFormat; +import freemarker.ext.beans.ZeroArgumentNonVoidMethodPolicy; +import freemarker.template.Configuration; +import freemarker.template.DefaultObjectWrapper; +import freemarker.template.TemplateException; +import freemarker.template.TemplateExceptionHandler; + +import java.io.IOException; +import java.io.StringWriter; +import java.util.*; +import java.util.function.Supplier; +import java.util.stream.Collectors; + +/** + * Generation of Markdown documentation. + * + * @author Alexander Weigl + * @version 1 (29.10.23) + */ +public class DocGen implements Supplier { + private final Metamodel.KeyApi metamodel; + + public DocGen(Metamodel.KeyApi metamodel) { + this.metamodel = metamodel; + } + + @Override + public String get() { + final StringWriter target = new StringWriter(); + try { + // 1) Configure FreeMarker + var cfg = new Configuration(Configuration.VERSION_2_3_32); + cfg.setClassForTemplateLoading(DocGen.class, "/templates"); // classpath + cfg.setDefaultEncoding("UTF-8"); + cfg.setAutoEscapingPolicy(Configuration.DISABLE_AUTO_ESCAPING_POLICY); + cfg.setTemplateExceptionHandler(TemplateExceptionHandler.HTML_DEBUG_HANDLER); + cfg.setLogTemplateExceptions(false); + cfg.setWrapUncheckedExceptions(true); + cfg.setFallbackOnNullLoopVariable(false); + cfg.setOutputFormat(HTMLOutputFormat.INSTANCE); + + // Use DefaultObjectWrapper to expose fields of objects in the data model + DefaultObjectWrapper wrapper = new DefaultObjectWrapper(Configuration.VERSION_2_3_32); + wrapper.setExposeFields(true); + wrapper.setMethodsShadowItems(true); + wrapper.setRecordZeroArgumentNonVoidMethodPolicy( + ZeroArgumentNonVoidMethodPolicy.BOTH_METHOD_AND_PROPERTY_UNLESS_BEAN_PROPERTY_READ_METHOD); + wrapper.setForceLegacyNonListCollections(false); + wrapper.setDefaultDateType(freemarker.template.TemplateDateModel.DATETIME); + cfg.setObjectWrapper(wrapper); + + // 2) Build the data-model + Map model = new TreeMap<>(); + + model.put("segmentDocumentation", metamodel.segmentDocumentation()); + + model.put("endpoints", + metamodel.endpoints() + .stream().sorted(Comparator.comparing(Metamodel.Endpoint::name)) + .toList()); + + final Map> collect = metamodel.endpoints() + .stream().sorted(Comparator.comparing(Metamodel.Endpoint::name)) + .collect(Collectors.groupingBy(Metamodel.Endpoint::segment, TreeMap::new, Collectors.toList())); + + model.put("endpointsBySegment", collect); + + model.put("types", + metamodel.types().values() + .stream().sorted(Comparator.comparing(Metamodel.Type::name)) + .toList()); + + model.put("version", + KeYResourceManager.getManager().getVersion() + + " (" + KeYConstants.INTERNAL_VERSION.substring(0, 8) + ")"); + model.put("date", new Date()); + + // 3) Get template + var tpl = cfg.getTemplate("docs.ftl"); + + // 4) Merge and output + tpl.process(model, target); + return target.toString(); + } catch (IOException | TemplateException e) { + throw new RuntimeException(e); + } + } +} diff --git a/keyext.api.doc/src/main/java/org/key_project/key/api/doc/ExtractMetaData.java b/keyext.api.doc/src/main/java/org/key_project/key/api/doc/ExtractMetaData.java new file mode 100644 index 00000000000..4140b1ecfeb --- /dev/null +++ b/keyext.api.doc/src/main/java/org/key_project/key/api/doc/ExtractMetaData.java @@ -0,0 +1,421 @@ +/* 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 org.key_project.key.api.doc;/* + * 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 + */ + +import java.io.File; +import java.lang.reflect.*; +import java.util.*; +import java.util.concurrent.CompletableFuture; +import java.util.stream.Stream; + +import de.uka.ilkd.key.proof.Proof; + +import org.key_project.key.api.doc.Metamodel.HelpText; +import org.key_project.key.api.doc.Metamodel.HelpTextEntry; + +import com.github.therapi.runtimejavadoc.*; +import org.eclipse.lsp4j.jsonrpc.messages.Either; +import org.eclipse.lsp4j.jsonrpc.services.JsonNotification; +import org.eclipse.lsp4j.jsonrpc.services.JsonRequest; +import org.eclipse.lsp4j.jsonrpc.services.JsonSegment; +import org.jspecify.annotations.Nullable; +import org.keyproject.key.api.remoteapi.KeyApi; +import org.keyproject.key.api.remoteclient.ClientApi; + +/** + * @author Alexander Weigl + * @version 1 (14.10.23) + */ + +public class ExtractMetaData implements Runnable { + private final List endpoints = new LinkedList<>(); + private final Map, Metamodel.Type> types = new HashMap<>(); + private final Map segDocumentation = new TreeMap<>(); + private final Metamodel.KeyApi keyApi = + new Metamodel.KeyApi(endpoints, types, segDocumentation); + + public ExtractMetaData() { + } + + @Override + public void run() { + for (Method method : KeyApi.class.getMethods()) { + addServerEndpoint(method); + } + + for (Method method : ClientApi.class.getMethods()) { + addClientEndpoint(method); + } + + for (var anInterface : KeyApi.class.getInterfaces()) { + var js = anInterface.getAnnotation(JsonSegment.class); + if (js != null) { + var key = js.value(); + var doc = findDocumentation(anInterface); + segDocumentation.put(key, doc); + } + } + } + + private void addServerEndpoint(Method method) { + var jsonSegment = method.getDeclaringClass().getAnnotation(JsonSegment.class); + if (jsonSegment == null) + return; + var segment = jsonSegment.value(); + + var req = method.getAnnotation(JsonRequest.class); + var resp = method.getAnnotation(JsonNotification.class); + + var args = translate(method.getParameters()); + + if (req != null) { + var mn = callMethodName(method.getName(), segment, req.value(), req.useSegment()); + + if (method.getReturnType() == Void.class) { + System.err.println("Found void as return type for a request! " + method); + return; + } + + var retType = getOrFindType(method.getGenericReturnType()); + Objects.requireNonNull(retType, "No retType found " + method.getGenericReturnType()); + var documentation = findDocumentation(method); + var mm = new Metamodel.ServerRequest(mn, documentation, args, retType); + endpoints.add(mm); + return; + } + + if (resp != null) { + var mn = callMethodName(method.getName(), segment, resp.value(), resp.useSegment()); + var documentation = findDocumentation(method); + var mm = new Metamodel.ServerNotification(mn, documentation, args); + endpoints.add(mm); + return; + } + + throw new IllegalStateException( + "Method " + method + " is neither a request nor a notification"); + } + + private @Nullable HelpText findDocumentation(Method method) { + MethodJavadoc javadoc = RuntimeJavadoc.getJavadoc(method); + if (javadoc.isEmpty()) + return null; + + final var visitor = new ToHtmlStringCommentVisitor(); + javadoc.getComment().visit(visitor); + + var t = javadoc.getThrows().stream() + .map(it -> new HelpTextEntry(it.getName(), it.getComment().toString())); + + var p = javadoc.getParams().stream() + .map(it -> new HelpTextEntry(it.getName(), it.getComment().toString())); + + var r = Stream.of(new HelpTextEntry("returns", javadoc.getReturns().toString())); + + return new HelpText(visitor.build(), + Stream.concat(r, Stream.concat(p, t)).toList()); + } + + private List translate(Parameter[] parameters) { + return Arrays.stream(parameters).map(this::translate).toList(); + } + + private Metamodel.Argument translate(Parameter parameter) { + var type = getOrFindType(parameter.getType()).name(); + return new Metamodel.Argument(parameter.getName(), type); + } + + private Metamodel.Type getOrFindType(Class type) { + if (type == String.class) + return Metamodel.BuiltinType.STRING; + if (type == Integer.class) + return Metamodel.BuiltinType.INT; + if (type == Double.class) + return Metamodel.BuiltinType.DOUBLE; + if (type == Long.class) + return Metamodel.BuiltinType.LONG; + if (type == Character.class) + return Metamodel.BuiltinType.LONG; + if (type == File.class) + return Metamodel.BuiltinType.STRING; + if (type == Boolean.class) + return Metamodel.BuiltinType.BOOL; + if (type == Boolean.TYPE) + return Metamodel.BuiltinType.BOOL; + + if (type == Integer.TYPE) + return Metamodel.BuiltinType.INT; + if (type == Double.TYPE) + return Metamodel.BuiltinType.DOUBLE; + if (type == Long.TYPE) + return Metamodel.BuiltinType.LONG; + if (type == Character.TYPE) + return Metamodel.BuiltinType.LONG; + + if (type == CompletableFuture.class) { + return getOrFindType(type.getTypeParameters()[0].getClass()); + } + + + if (type == List.class) { + // TODO try to get the type below. + var subType = getOrFindType(type.getTypeParameters()[0]); + return new Metamodel.ListType(subType); + } + + if (type == Class.class || type == Constructor.class || type == Proof.class) { + throw new IllegalStateException("Forbidden class reached!"); + } + + + var t = types.get(type); + if (t != null) + return t; + var a = createType(type); + types.put(type, a); + return a; + } + + private Metamodel.Type createType(Class type) { + final var documentation = findDocumentation(type); + if (type.isEnum()) { + return new Metamodel.EnumType(type.getSimpleName(), type.getName(), + Arrays.stream(type.getEnumConstants()) + .map( + it -> new Metamodel.EnumConstant(it.toString(), + findDocumentationEnum(type, it))) + .toList(), + documentation); + } + + var obj = new Metamodel.ObjectType(type.getSimpleName(), type.getName(), new ArrayList<>(), + documentation); + final var list = Arrays.stream(type.getDeclaredFields()) + .map(it -> new Metamodel.Field(it.getName(), getOrFindTypeName(it.getGenericType()), + type.isRecord() + ? findDocumentationRecord(type, it.getName()) + : findDocumentation(it))) + .toList(); + obj.fields().addAll(list); + return obj; + } + + private @Nullable HelpText findDocumentation(Field it) { + var javadoc = RuntimeJavadoc.getJavadoc(it); + if (javadoc.isEmpty()) + return null; + return printFieldDocumentation(javadoc); + } + + private @Nullable HelpText findDocumentationEnum(Class type, Object enumConstant) { + ClassJavadoc javadoc = RuntimeJavadoc.getJavadoc(type); + if (javadoc.isEmpty()) + return null; + for (var cdoc : javadoc.getEnumConstants()) { + if (cdoc.getName().equalsIgnoreCase(enumConstant.toString())) { + return printFieldDocumentation(cdoc); + } + } + return null; + } + + private @Nullable HelpText findDocumentationRecord(Class type, String name) { + ClassJavadoc javadoc = RuntimeJavadoc.getJavadoc(type); + if (javadoc.isEmpty()) + return null; + for (var cdoc : javadoc.getRecordComponents()) { + if (cdoc.getName().equalsIgnoreCase(name)) { + return new HelpText(cdoc.getComment().toString(), List.of()); + } + } + return null; + } + + private static HelpText printFieldDocumentation(FieldJavadoc javadoc) { + final var visitor = new ToHtmlStringCommentVisitor(); + javadoc.getComment().visit(visitor); + + var t = javadoc.getOther().stream() + .map(it -> new HelpTextEntry(it.getName(), it.getComment().toString())); + + var p = javadoc.getSeeAlso().stream().map( + it -> new HelpTextEntry(it.getSeeAlsoType().toString(), it.getStringLiteral())); + + return new HelpText(visitor.build(), Stream.concat(p, t).toList()); + } + + private @Nullable HelpText findDocumentation(Class type) { + ClassJavadoc classDoc = RuntimeJavadoc.getJavadoc(type); + if (!classDoc.isEmpty()) { // optionally skip absent documentation + var other = classDoc.getOther() + .stream().map(it -> new HelpTextEntry(it.getName(), + it.getComment().toString())); + var also = classDoc.getSeeAlso() + .stream().map(it -> new HelpTextEntry(it.getSeeAlsoType().toString(), + it.getStringLiteral())); + + return new HelpText( + classDoc.getComment().toString(), + Stream.concat(other, also).toList()); + } + return null; + } + + private void addClientEndpoint(Method method) { + var jsonSegment = method.getDeclaringClass().getAnnotation(JsonSegment.class); + var segment = jsonSegment == null ? "" : jsonSegment.value(); + + var req = method.getAnnotation(JsonRequest.class); + var resp = method.getAnnotation(JsonNotification.class); + + var args = translate(method.getParameters()); + + if (req != null) { + var retType = getOrFindType(method.getGenericReturnType()); + Objects.requireNonNull(retType); + var mn = callMethodName(method.getName(), segment, req.value(), req.useSegment()); + var documentation = findDocumentation(method); + var mm = new Metamodel.ClientRequest(mn, documentation, args, retType); + endpoints.add(mm); + return; + } + + if (resp != null) { + var mn = callMethodName(method.getName(), segment, resp.value(), resp.useSegment()); + var documentation = findDocumentation(method); + var mm = new Metamodel.ClientNotification(mn, documentation, args); + endpoints.add(mm); + } + } + + private static String callMethodName(String method, String segment, + @Nullable String userValue, + boolean useSegment) { + if (!useSegment) { + if (userValue == null || userValue.isBlank()) { + return method; + } else { + return userValue; + } + } else { + if (userValue == null || userValue.isBlank()) { + return segment + "/" + method; + } else { + return segment + "/" + userValue; + } + } + } + + + private String getOrFindTypeName(Type type) { + switch (type) { + case GenericArrayType a -> throw new RuntimeException("Unwanted type found: " + type); + case Class c -> { + return getOrFindTypeName(c); + } + case ParameterizedType pt -> { + if (Objects.equals(pt.getRawType().getTypeName(), + CompletableFuture.class.getTypeName())) { + return getOrFindTypeName(pt.getActualTypeArguments()[0]); + } + if (Objects.equals(pt.getRawType().getTypeName(), List.class.getTypeName())) { + String base = getOrFindTypeName(pt.getActualTypeArguments()[0]); + return base + "[]"; + } + + if (Objects.equals(pt.getRawType().getTypeName(), Either.class.getTypeName())) { + var base1 = getOrFindType(pt.getActualTypeArguments()[0]); + var base2 = getOrFindType(pt.getActualTypeArguments()[1]); + return "either<" + base1 + ", " + base2 + ">"; + } + } + default -> { + } + } + + return "!!!"; + } + + private String getOrFindTypeName(Class type) { + var t = types.get(type); + + if (t != null) + return t.name(); + else if (type == String.class) + return Metamodel.BuiltinType.STRING.name(); + else if (type == Integer.class) + return Metamodel.BuiltinType.INT.name(); + else if (type == Double.class) + return Metamodel.BuiltinType.DOUBLE.name(); + else if (type == Long.class) + return Metamodel.BuiltinType.LONG.name(); + else if (type == Character.class) + return Metamodel.BuiltinType.LONG.name(); + else if (type == File.class) + return Metamodel.BuiltinType.STRING.name(); + else if (type == Boolean.class) + return Metamodel.BuiltinType.BOOL.name(); + else if (type == Boolean.TYPE) + return Metamodel.BuiltinType.BOOL.name(); + else if (type == Integer.TYPE) + return Metamodel.BuiltinType.INT.name(); + else if (type == Double.TYPE) + return Metamodel.BuiltinType.DOUBLE.name(); + else if (type == Long.TYPE) + return Metamodel.BuiltinType.LONG.name(); + else if (type == Character.TYPE) + return Metamodel.BuiltinType.LONG.name(); + else if (type == CompletableFuture.class) { + return getOrFindTypeName(type.getTypeParameters()[0].getClass()); + } else if (type == List.class) { + var subType = getOrFindTypeName(type.getTypeParameters()[0]); + return subType + "[]"; + } else if (type == Class.class || type == Constructor.class || type == Proof.class) { + throw new IllegalStateException("Forbidden class reached!"); + } else if (type instanceof Class) { + return type.getSimpleName(); + } + return "!!!??!?!?"; + } + + + private Metamodel.@Nullable Type getOrFindType(Type genericReturnType) { + switch (genericReturnType) { + case GenericArrayType a -> + throw new RuntimeException("Unwanted type found: " + genericReturnType); + case Class c -> { + return getOrFindType(c); + } + case ParameterizedType pt -> { + if (Objects.equals(pt.getRawType().getTypeName(), + CompletableFuture.class.getTypeName())) { + return getOrFindType(pt.getActualTypeArguments()[0]); + } + if (Objects.equals(pt.getRawType().getTypeName(), List.class.getTypeName())) { + var base = getOrFindType(pt.getActualTypeArguments()[0]); + return new Metamodel.ListType(base); + } + + if (Objects.equals(pt.getRawType().getTypeName(), Either.class.getTypeName())) { + var base1 = getOrFindType(pt.getActualTypeArguments()[0]); + var base2 = getOrFindType(pt.getActualTypeArguments()[1]); + return new Metamodel.EitherType(base1, base2); + } + } + default -> { + } + } + + return null; + } + + public Metamodel.KeyApi getApi() { + return keyApi; + } +} diff --git a/keyext.api.doc/src/main/java/org/key_project/key/api/doc/Main.java b/keyext.api.doc/src/main/java/org/key_project/key/api/doc/Main.java new file mode 100644 index 00000000000..72544b5f375 --- /dev/null +++ b/keyext.api.doc/src/main/java/org/key_project/key/api/doc/Main.java @@ -0,0 +1,86 @@ +/* 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 org.key_project.key.api.doc; + +import java.io.IOException; +import java.nio.file.Files; +import java.nio.file.Path; +import java.nio.file.Paths; +import java.util.concurrent.Callable; +import java.util.function.Function; +import java.util.function.Supplier; + +import org.key_project.key.api.doc.Metamodel.Endpoint; +import org.key_project.key.api.doc.Metamodel.Type; + +import com.google.gson.Gson; +import com.google.gson.GsonBuilder; +import com.google.gson.JsonObject; +import com.google.gson.JsonSerializer; +import org.jspecify.annotations.Nullable; +import picocli.CommandLine; + +/** + * @author Alexander Weigl + * @version 1 (7/8/25) + */ +@CommandLine.Command(name = "gendoc", + mixinStandardHelpOptions = true, + version = "gendoc 1.0", + description = "Generates the documentation for key.api") +public class Main implements Callable { + @CommandLine.Option(names = { "-s", "--source" }, + description = "Source folder for getting JavaDoc") + private @Nullable Path source = Paths.get("keyext.api", "src", "main", "java"); + + @CommandLine.Option(names = { "-o", "--output" }, description = "Output folder") + private Path output = Paths.get("out"); + + public static void main(String[] args) { + int exitCode = new CommandLine(new Main()).execute(args); + System.exit(exitCode); + } + + @Override + public Integer call() throws IOException { + var metadata = new ExtractMetaData(); + metadata.run(); + Files.createDirectories(output); + + runGenerator(metadata.getApi(), "api.meta.json", (a) -> () -> getGson().toJson(a)); + runGenerator(metadata.getApi(), "api.meta.html", DocGen::new); + runGenerator(metadata.getApi(), "keydata.py", PythonGenerator.PyDataGen::new); + runGenerator(metadata.getApi(), "server.py", PythonGenerator.PyApiGen::new); + return 0; + } + + + private void runGenerator(Metamodel.KeyApi keyApi, String target, + Function> api) { + try { + var n = api.apply(keyApi); + Files.writeString(output.resolve(target), n.get()); + } catch (IOException e) { + e.printStackTrace(); + } + } + + private static Gson getGson() { + return new GsonBuilder() + .setPrettyPrinting() + .registerTypeAdapter(Type.class, + (JsonSerializer) (src, typeOfSrc, context) -> { + JsonObject json = (JsonObject) context.serialize(src); + json.addProperty("kind", src.kind()); + return json; + }) + .registerTypeAdapter(Endpoint.class, + (JsonSerializer) (src, typeOfSrc, context) -> { + JsonObject json = (JsonObject) context.serialize(src); + json.addProperty("kind", src.kind()); + return json; + }) + .create(); + } +} diff --git a/keyext.api.doc/src/main/java/org/key_project/key/api/doc/Metamodel.java b/keyext.api.doc/src/main/java/org/key_project/key/api/doc/Metamodel.java new file mode 100644 index 00000000000..464249b47da --- /dev/null +++ b/keyext.api.doc/src/main/java/org/key_project/key/api/doc/Metamodel.java @@ -0,0 +1,238 @@ +/* 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 org.key_project.key.api.doc; + +import java.util.List; +import java.util.Map; + +import org.jspecify.annotations.NullMarked; +import org.jspecify.annotations.Nullable; +import org.keyproject.key.api.data.DataExamples; + +/// Metamodel of the API. This class contains classes which represents the functionality and +/// interfaces of the API. +/// +/// @author Alexander Weigl +/// @version 1 (29.10.23) +@NullMarked +public class Metamodel { + + /// Root class of the metamodel. + /// + /// @param endpoints a list of provided services + /// @param types a list of known types + public record KeyApi( + List endpoints, + java.util.Map, Type> types, + Map segmentDocumentation) { + } + + /// Javadoc texts + public record HelpText(String text, List others) { + } + + /// Javadoc categories + public record HelpTextEntry(String name, String value) { + } + + + /// An {@link Endpoint} is a provided service/method. + public sealed interface Endpoint { + /// complete name of the service + String name(); + + /// a markdown documentation + @Nullable + HelpText documentation(); + + default String kind() { + return getClass().getName(); + } + + /// a list of its arguments + List args(); + + /// + default String segment() { + int idx = name().indexOf("/"); + if (idx == -1) { + return ""; + } + return name().substring(0, idx); + } + + /// sender of this invocation + default String sender() { + return getClass().getSimpleName().startsWith("Server") ? "Client" : "Server"; + } + + /// + default boolean isAsync() { + return getClass().getSimpleName().endsWith("Notification"); + } + } + + /// A [Argument] of an endpoint + /// + /// @param name the argument name + /// @param type the argument type + public record Argument(String name, String type) { + } + + /// A {@link ServerRequest} is the caller to the callee expecting an answer. + /// + /// @param name + /// @param args + /// @param documentation + /// @param returnType + public record ServerRequest(String name, @Nullable HelpText documentation, List args, + Type returnType) + implements Endpoint { + } + + /// + public record ServerNotification(String name, @Nullable HelpText documentation, + List args) + implements Endpoint { + } + + /// + public record ClientRequest(String name, @Nullable HelpText documentation, List args, + Type returnType) + implements Endpoint { + } + + /// + public record ClientNotification(String name, @Nullable HelpText documentation, + List args) + implements Endpoint { + } + + /// + public record Field(String name, /* Type */ String type, @Nullable HelpText documentation) { + Field(String name, String type) { + this(name, type, null); + } + } + + /// A data type + public sealed interface Type { + default String kind() { + return getClass().getName(); + } + + /// Documentation of the data type + @Nullable + HelpText documentation(); + + /// name of the data type + String name(); + + /// + String identifier(); + } + + + /// Typical built-in data types supported by the API + public enum BuiltinType implements Type { + INT, LONG, STRING, BOOL, DOUBLE; + + @Override + public HelpText documentation() { + return new HelpText("built-in data type", List.of()); + } + + public String identifier() { + return name().toLowerCase(); + } + + } + + /// List of `type`. + /// + /// @param type the type of list elements + public record ListType(Type type) implements Type { + @Override + public String name() { + return type().name() + "[]"; + } + + public String identifier() { + return type().identifier() + "[]"; + } + + @Override + public @Nullable HelpText documentation() { + return null; + } + } + + /// Data type of objects or struct or record. + /// + /// @param typeName short type name + /// @param typeFullName fully-qualified type name + /// @param fields list of fields + /// @param documentation documentation of data type + public record ObjectType(String typeName, String typeFullName, List fields, + HelpText documentation) implements Type { + @Override + public String name() { + return typeName; + } + + public String identifier() { + return typeFullName; + } + + /// + public @Nullable String jsonExample() { + return DataExamples.get(typeFullName); + } + } + + /// A data type representing that a method returns or expecting either type `a` or `b`. + /// + /// @param a + /// @param b + public record EitherType(Type a, Type b) implements Type { + + @Override + public String name() { + return "either"; + } + + public String identifier() { + return name(); + } + + @Override + public @Nullable HelpText documentation() { + return null; + } + } + + /// Enumeration data type + /// + /// @param typeName short name of the data type + /// @param typeFullName fully-qualified name + /// @param values possible values of the enum + /// @param documentation documentation of the data type + public record EnumType(String typeName, String typeFullName, List values, + HelpText documentation) implements Type { + + @Override + public String name() { + return typeName; + } + + public String identifier() { + return typeFullName; + } + + } + + public record EnumConstant(String value, @Nullable HelpText documentation) { + } + +} diff --git a/keyext.api.doc/src/main/java/org/key_project/key/api/doc/PythonGenerator.java b/keyext.api.doc/src/main/java/org/key_project/key/api/doc/PythonGenerator.java new file mode 100644 index 00000000000..b9305fec135 --- /dev/null +++ b/keyext.api.doc/src/main/java/org/key_project/key/api/doc/PythonGenerator.java @@ -0,0 +1,228 @@ +/* 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 org.key_project.key.api.doc; + +import java.io.PrintWriter; +import java.io.StringWriter; +import java.util.Comparator; +import java.util.List; +import java.util.function.Supplier; +import java.util.stream.Collectors; +import java.util.stream.Stream; + +/** + * @author Alexander Weigl + * @version 1 (29.10.23) + */ +public abstract class PythonGenerator implements Supplier { + protected final Metamodel.KeyApi metamodel; + protected final StringWriter target = new StringWriter(); + protected final PrintWriter out = new PrintWriter(target); + + public PythonGenerator(Metamodel.KeyApi metamodel) { + this.metamodel = metamodel; + } + + @Override + public String get() { + run(); + return target.toString(); + } + + protected abstract void run(); + + protected String asPython(String typeName) { + return switch (typeName) { + case "INT", "LONG" -> "int"; + case "STRING" -> "str"; + case "BOOL" -> "bool"; + case "DOUBLE" -> "float"; + default -> { + var t = findType(typeName); + yield asPython(t); + } + }; + } + + protected String asPython(Metamodel.Type t) { + return switch (t) { + case Metamodel.ListType lt -> "typing.List[" + asPython(lt.type()) + "]"; + case Metamodel.EitherType lt -> + "typing.Union[" + asPython(lt.a()) + ", " + asPython(lt.b()) + "]"; + case Metamodel.BuiltinType bt -> switch (bt) { + case INT, LONG -> "int"; + case STRING -> "str"; + case BOOL -> "bool"; + case DOUBLE -> "float"; + }; + default -> t.name(); + }; + + } + + protected Metamodel.Type findType(String typeName) { + return this.metamodel.types().values().stream() + .filter(it -> { + if (it instanceof Metamodel.ListType lt) + return lt.type().name().equals(typeName); + return it.name().equals(typeName); + }) + .findFirst() + .orElse(new Metamodel.ObjectType("...", "...", List.of(), null)); + // new RuntimeException("Could not find type: " + typeName)); + } + + + public static class PyApiGen extends PythonGenerator { + public PyApiGen(Metamodel.KeyApi metamodel) { + super(metamodel); + } + + @Override + protected void run() { + out.format(""" + from __future__ import annotations + from .keydata import * + from .rpc import ServerBase, LspEndpoint + + import enum + import abc + import typing + from abc import abstractmethod + """); + server( + metamodel.endpoints() + .stream() + .filter(it -> it instanceof Metamodel.ServerRequest + || it instanceof Metamodel.ServerNotification) + .sorted(Comparator.comparing(Metamodel.Endpoint::name))); + + client( + metamodel.endpoints() + .stream() + .filter(it -> it instanceof Metamodel.ClientRequest + || it instanceof Metamodel.ClientNotification) + .sorted(Comparator.comparing(Metamodel.Endpoint::name))); + } + + + private void client(Stream sorted) { + out.format("class Client(abc.ABCMeta):%n"); + sorted.forEach(this::clientEndpoint); + } + + private void clientEndpoint(Metamodel.Endpoint endpoint) { + var args = endpoint.args().stream() + .map(it -> "%s : %s".formatted(it.name(), asPython(it.type()))) + .collect(Collectors.joining(", ")); + out.format(" @abstractmethod%n"); + if (endpoint instanceof Metamodel.ClientRequest sr) { + out.format(" def %s(self, %s) -> %s:%n", endpoint.name().replace("/", "_"), args, + asPython(sr.returnType())); + } else { + out.format(" def %s(self, %s):%n", endpoint.name().replace("/", "_"), args); + } + out.format(" \"\"\"%s\"\"\"%n%n", endpoint.documentation()); + out.format(" pass"); + out.println(); + out.println(); + } + + private void server(Stream sorted) { + out.format(""" + class KeyServer(ServerBase):%n + def __init__(self, endpoint : LspEndpoint): + super().__init__(endpoint) + + """); + sorted.forEach(this::serverEndpoint); + } + + private void serverEndpoint(Metamodel.Endpoint endpoint) { + var args = endpoint.args().stream() + .map(it -> "%s : %s".formatted(it.name(), asPython(it.type()))) + .collect(Collectors.joining(", ")); + + var params = "[]"; + if (!endpoint.args().isEmpty()) { + params = endpoint.args().stream() + .map(Metamodel.Argument::name) + .collect(Collectors.joining(" , ", "[", "]")); + } + + if (endpoint instanceof Metamodel.ServerRequest sr) { + out.format(" def %s(self, %s) -> %s:%n", endpoint.name().replace("/", "_"), args, + asPython(sr.returnType())); + out.format(" \"\"\"%s\"\"\"%n%n", sr.documentation()); + out.format( + " return self._call_sync(\"%s\", %s)".formatted(endpoint.name(), params)); + } else { + out.format(" def %s(self, %s):%n", endpoint.name().replace("/", "_"), args); + out.format(" \"\"\"%s\"\"\"%n%n", endpoint.documentation()); + out.format(" return self._call_async(\"%s\", %s)".formatted(endpoint.name(), + params)); + } + out.println(); + out.println(); + } + + } + + + public static class PyDataGen extends PythonGenerator { + public PyDataGen(Metamodel.KeyApi metamodel) { + super(metamodel); + } + + protected void run() { + out.format(""" + from __future__ import annotations + import enum + import abc + import typing + from abc import abstractmethod, ABCMeta + + """); + metamodel.types().values().forEach(this::printType); + + var names = + metamodel.types().values().stream() + .map(it -> "\"%s\": %s".formatted(it.identifier(), it.name())) + .collect(Collectors.joining(",")); + out.format("KEY_DATA_CLASSES = { %s }%n%n", names); + var names_reverse = + metamodel.types().values().stream() + .map(it -> "\"%s\": \"%s\"".formatted(it.name(), it.identifier())) + .collect(Collectors.joining(",")); + out.format("KEY_DATA_CLASSES_REV = { %s }%n%n", names_reverse); + } + + private void printType(Metamodel.Type type) { + if (type instanceof Metamodel.ObjectType ot) { + out.format("class %s:%n".formatted(type.name())); + out.format(" \"\"\"%s\"\"\"%n", type.documentation()); + ot.fields().forEach(it -> out.format("%n %s : %s%n \"\"\"%s\"\"\"%n" + .formatted(it.name(), asPython(it.type()), it.documentation()))); + + out.format("\n def __init__(self%s):%n".formatted( + ot.fields().stream() + .map(Metamodel.Field::name) + .collect(Collectors.joining(", ", ", ", "")))); + + if (ot.fields().isEmpty()) + out.format(" pass%n%n"); + + for (Metamodel.Field field : ot.fields()) { + out.format(" self.%s = %s%n", field.name(), field.name()); + } + + } else if (type instanceof Metamodel.EnumType et) { + out.format("class %s(enum.Enum):%n".formatted(type.name())); + out.format(" \"\"\"%s\"\"\"%n%n", type.documentation()); + et.values().forEach(it -> out.format(" %s = None%n".formatted(it))); + } + out.println(); + } + } +} diff --git a/keyext.api.doc/src/main/java/org/key_project/key/api/doc/package-info.java b/keyext.api.doc/src/main/java/org/key_project/key/api/doc/package-info.java new file mode 100644 index 00000000000..1722df1f0cf --- /dev/null +++ b/keyext.api.doc/src/main/java/org/key_project/key/api/doc/package-info.java @@ -0,0 +1,8 @@ +/** + * @author Alexander Weigl + * @version 1 (7/8/25) + */ +@NullMarked +package org.key_project.key.api.doc; + +import org.jspecify.annotations.NullMarked; diff --git a/keyext.api.doc/src/main/resources/templates/docs.ftl b/keyext.api.doc/src/main/resources/templates/docs.ftl new file mode 100644 index 00000000000..a135cdf6c05 --- /dev/null +++ b/keyext.api.doc/src/main/resources/templates/docs.ftl @@ -0,0 +1,304 @@ +<#-- @ftlvariable name="types" type="java.util.Collection" --> +<#-- @ftlvariable name="endpoints" type="java.util.Collection" --> +<#-- @ftlvariable name="segmentDocumentation" type="java.util.Map" --> +<#-- @ftlvariable name="endpointsBySegment" type="java.util.Map>" --> + + + + + KeY API Documentation + + + + + +
+ +
+

Base Definitions

+

+ This API builds upon and uses the same convention as the Language + Server Protocol. + In basic, the protocol builds upon a simple HTTP protocol with a JSON playoad. A request message looks as +

+ 
Content-Length: 80\r\n
+Content-Type: application/vscode-jsonrpc; charset=utf-8\r\n
+\r\n
+{
+	"jsonrpc": "2.0",
+	"id": 1,
+	"method": "env/version",
+	"params": {
+		...
+	}
+}
+

+ Header Content-Type is optional. The \r\n are mandatory. The field id make + the difference between a request or a notification. Later do not result into a response. A response message + contains the fields result or error, depending on a normal or exceptional execution of + the request. +

+

+ The communication is always asynchronous and duplex. Meaning you can send and receive messages at any time. + For synchronous calls, the client and server library need to implement a waiting mechanism. +

+ + +

Types

+
+ <#list types as type> + <#assign isEnum = true> + <#if type.fields??> + <#assign isEnum = false> + + +
+

${type.name()} ${isEnum?string("enum","type")}

+
+ ${isEnum?string("enum","type")} + ${type.name()} {
+ <#if type.fields??> + <#list type.fields as field> +
+ <#if field.documentation()??> +
/* ${field.documentation.text} */
+ +
${type.name()} ${field.name()}; +
+
+ + + <#if type.values??> + <#list type.values()?sort as value> + <#if value.documentation??> + /* ${value.documentation.text} */ + + ${value.value()} + + + } +
+ <#if type.documentation??> +
+

+ ${type.documentation.text} +

+
    + <#list type.documentation.others as o> +
  • ${o.name}: ${o.value}
    • + +
+
+ + <#if (type.jsonExample)??> +
+
+ Example + ${type.jsonExample} +
+
+ + +
+ +
+ +

Endpoints

+ <#assign lastSegment = ""> +
+ <#list endpoints as ep> + <#if lastSegment!=ep.segment()> + <#assign lastSegment = ep.segment()> +

Segment: ${lastSegment}

+ <#if segmentDocumentation[lastSegment]??> + <#assign doc = segmentDocumentation[lastSegment]> +
+

+ ${doc.text} +

+
    + <#list doc.others as o> +
  • ${o.name}: ${o.value}
    • + +
+
+ + + +
+

+ <#if ep.isAsync()> + Notification: + <#else> + Request: + + ${ep.name()} + + <#if ep.sender() == "Server" && ep.isAsync()> + server ~~> client + <#elseif ep.sender() == "Server" && !ep.isAsync()> + server --> client + <#elseif ep.sender() == "Client" && !ep.isAsync()> + client --> server + <#elseif ep.sender() == "Client" && ep.isAsync()> + client ~~> server + + +

+ + + ${ep.name()}( + <#list ep.args() as arg> + ${arg.type} + ${arg.name}<#sep>, + + ) + <#if ep.returnType??> + : + ${ep.returnType.name()} + + + <#if ep.documentation??> +
+

+ ${ep.documentation.text} +

+
    + <#list ep.documentation.others as o> +
  • ${o.name}: ${o.value}
    • + +
+
+ +
+ +
+
+
+ + diff --git a/keyext.api.doc/src/main/resources/templates/test.ftl b/keyext.api.doc/src/main/resources/templates/test.ftl new file mode 100644 index 00000000000..741952e3fb2 --- /dev/null +++ b/keyext.api.doc/src/main/resources/templates/test.ftl @@ -0,0 +1,2 @@ +<#-- @ftlvariable name="type" type="org.key_project.key.api.doc.Metamodel.ObjectType" --> + diff --git a/keyext.api/build.gradle b/keyext.api/build.gradle new file mode 100644 index 00000000000..f6785812c44 --- /dev/null +++ b/keyext.api/build.gradle @@ -0,0 +1,40 @@ +plugins { + id 'application' + + // Used to create a single executable jar file with all dependencies + // see task "shadowJar" below + // https://github.com/GradleUp/shadow + id 'com.gradleup.shadow' version "9.0.1" +} + +description "Verification server interface via JSON-RPC" + +application { + mainClass.set("org.keyproject.key.api.StartServer") +} + +dependencies { + api(project(":key.core")) + api(project(":key.ui")) + + api("org.eclipse.lsp4j:org.eclipse.lsp4j.jsonrpc:0.23.1") + implementation("org.eclipse.lsp4j:org.eclipse.lsp4j.websocket.jakarta:0.23.1") + implementation("org.eclipse.lsp4j:org.eclipse.lsp4j.websocket.jakarta:0.23.1") + implementation("org.eclipse.jetty.websocket:websocket-javax-server:10.0.16") + implementation("info.picocli:picocli:4.7.5") + + implementation("com.google.guava:guava:32.1.3-jre") + + + annotationProcessor "com.github.therapi:therapi-runtime-javadoc-scribe:0.13.0" + api "com.github.therapi:therapi-runtime-javadoc:0.13.0" + + //for GraalVM annotationProcessor 'info.picocli:picocli-codegen:4.7.5' +} + + +compileJava { + // for GraalVM options.compilerArgs += ["-Aproject=${project.group}/${project.name}"] + options.compilerArgs += ["-parameters"] // for having parameter name in reflection +} + diff --git a/keyext.api/src/main/java/org/keyproject/key/api/KeyApiImpl.java b/keyext.api/src/main/java/org/keyproject/key/api/KeyApiImpl.java new file mode 100644 index 00000000000..6b03be709b1 --- /dev/null +++ b/keyext.api/src/main/java/org/keyproject/key/api/KeyApiImpl.java @@ -0,0 +1,610 @@ +/* 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 org.keyproject.key.api; + +import java.io.File; +import java.io.IOException; +import java.nio.file.Files; +import java.util.Collection; +import java.util.List; +import java.util.Objects; +import java.util.concurrent.CompletableFuture; +import java.util.concurrent.atomic.AtomicInteger; +import java.util.function.Function; +import java.util.stream.Stream; +import java.util.stream.StreamSupport; + +import de.uka.ilkd.key.control.AbstractUserInterfaceControl; +import de.uka.ilkd.key.control.DefaultUserInterfaceControl; +import de.uka.ilkd.key.control.KeYEnvironment; +import de.uka.ilkd.key.gui.ExampleChooser; +import de.uka.ilkd.key.macros.ProofMacro; +import de.uka.ilkd.key.macros.ProofMacroFinishedInfo; +import de.uka.ilkd.key.nparser.ParsingFacade; +import de.uka.ilkd.key.pp.IdentitySequentPrintFilter; +import de.uka.ilkd.key.pp.LogicPrinter; +import de.uka.ilkd.key.pp.NotationInfo; +import de.uka.ilkd.key.pp.PosTableLayouter; +import de.uka.ilkd.key.proof.Goal; +import de.uka.ilkd.key.proof.Node; +import de.uka.ilkd.key.proof.Proof; +import de.uka.ilkd.key.proof.ProofAggregate; +import de.uka.ilkd.key.proof.init.*; +import de.uka.ilkd.key.proof.io.AbstractProblemLoader; +import de.uka.ilkd.key.proof.io.ProblemLoaderException; +import de.uka.ilkd.key.scripts.ProofScriptCommand; +import de.uka.ilkd.key.scripts.ProofScriptEngine; +import de.uka.ilkd.key.scripts.ScriptException; +import de.uka.ilkd.key.speclang.PositionedString; +import de.uka.ilkd.key.strategy.StrategyProperties; +import de.uka.ilkd.key.util.KeYConstants; + +import org.key_project.prover.engine.ProverTaskListener; +import org.key_project.prover.engine.TaskFinishedInfo; +import org.key_project.util.collection.ImmutableList; +import org.key_project.util.collection.ImmutableSet; +import org.key_project.util.reflection.ClassLoaderUtil; + +import org.eclipse.lsp4j.jsonrpc.CompletableFutures; +import org.eclipse.lsp4j.jsonrpc.messages.Either; +import org.eclipse.lsp4j.jsonrpc.services.JsonRequest; +import org.keyproject.key.api.data.*; +import org.keyproject.key.api.data.KeyIdentifications.*; +import org.keyproject.key.api.remoteapi.KeyApi; +import org.keyproject.key.api.remoteclient.ClientApi; + +import static de.uka.ilkd.key.proof.ProofNodeDescription.collectPathInformation; + +public final class KeyApiImpl implements KeyApi { + private final KeyIdentifications data = new KeyIdentifications(); + + private Function exitHandler; + + private ClientApi clientApi; + private final ProverTaskListener clientListener = new ProverTaskListener() { + @Override + public void taskStarted(org.key_project.prover.engine.TaskStartedInfo info) { + clientApi.taskStarted(org.keyproject.key.api.data.TaskStartedInfo.from(info)); + } + + @Override + public void taskProgress(int position) { + clientApi.taskProgress(position); + } + + @Override + public void taskFinished(TaskFinishedInfo info) { + clientApi.taskFinished(org.keyproject.key.api.data.TaskFinishedInfo.from(info)); + } + }; + private final AtomicInteger uniqueCounter = new AtomicInteger(); + + public KeyApiImpl() { + } + + @Override + @JsonRequest + public CompletableFuture> examples() { + return CompletableFutures + .computeAsync((c) -> ExampleChooser.listExamples(ExampleChooser.lookForExamples()) + .stream().map(ExampleDesc::from).toList()); + } + + @Override + public CompletableFuture shutdown() { + return CompletableFuture.completedFuture(true); + } + + @Override + public void exit() { + this.exitHandler.apply(null); + } + + public void setExitHandler(Function exitHandler) { + this.exitHandler = exitHandler; + } + + @Override + public void setTrace(SetTraceParams params) { + + } + + @Override + public CompletableFuture getVersion() { + return CompletableFuture.completedFuture(KeYConstants.VERSION); + } + + @Override + public CompletableFuture> getAvailableMacros() { + return CompletableFuture.completedFuture( + StreamSupport + .stream(ClassLoaderUtil.loadServices(ProofMacro.class).spliterator(), false) + .map(ProofMacroDesc::from).toList()); + } + + @Override + public CompletableFuture> getAvailableScriptCommands() { + return CompletableFuture.completedFuture( + StreamSupport + .stream(ClassLoaderUtil.loadServices(ProofScriptCommand.class).spliterator(), + false) + .map(ProofScriptCommandDesc::from).toList()); + } + + @Override + public CompletableFuture script(ProofId proofId, String scriptLine, + StrategyOptions options) { + return CompletableFuture.supplyAsync(() -> { + var proof = data.find(proofId); + var env = data.find(proofId.env()); + var script = ParsingFacade.parseScript(scriptLine); + var pe = new ProofScriptEngine(script); + + try { + pe.execute((AbstractUserInterfaceControl) env.getProofControl(), proof); + return new MacroStatistic(proofId, scriptLine, -1, -1); + } catch (IOException | InterruptedException | ScriptException e) { + throw new RuntimeException(e); + } + }); + } + + @Override + public CompletableFuture macro(ProofId proofId, String macroName, + StrategyOptions options) { + return CompletableFuture.supplyAsync(() -> { + var proof = data.find(proofId); + var env = data.find(proofId.env()); + var macro = StreamSupport + .stream(ClassLoaderUtil.loadServices(ProofMacro.class).spliterator(), false) + .filter(it -> it.getName().equals(macroName)).findFirst().orElseThrow(); + + try { + var info = + macro.applyTo(env.getUi(), proof, proof.openGoals(), null, clientListener); + return MacroStatistic.from(proofId, info); + } catch (Exception e) { + throw new RuntimeException(e); + } + }); + + } + + @Override + public CompletableFuture auto(ProofId proofId, StrategyOptions options) { + return CompletableFuture.supplyAsync(() -> { + var proof = data.find(proofId); + var env = data.find(proofId.env()); + options.configure(proof); + try { + System.out.println("Starting proof with setting " + + proof.getSettings().getStrategySettings().getActiveStrategyProperties() + .getProperty(StrategyProperties.STOPMODE_OPTIONS_KEY)); + env.getProofControl().startAndWaitForAutoMode(proof); + // clientListener); + return ProofStatus.from(proofId, proof); + } catch (Exception e) { + throw new RuntimeException(e); + } + }); + + } + + @Override + public CompletableFuture dispose(ProofId id) { + data.dispose(id); + return CompletableFuture.completedFuture(true); + } + + @Override + public CompletableFuture> goals(ProofId proofId, boolean onlyOpened, + boolean onlyEnabled) { + return CompletableFuture.supplyAsync(() -> { + var proof = data.find(proofId); + if (onlyOpened && !onlyEnabled) { + return asNodeDesc(proofId, proof.openGoals()); + } else if (onlyEnabled && onlyOpened) { + return asNodeDesc(proofId, proof.openEnabledGoals()); + } else { + return asNodeDesc(proofId, proof.allGoals()); + } + }); + } + + private List asNodeDesc(ProofId proofId, ImmutableList goals) { + return asNodeDesc(proofId, goals.stream().map(Goal::node)); + } + + private List asNodeDesc(ProofId proofId, Stream nodes) { + return nodes.map(it -> asNodeDesc(proofId, it)).toList(); + } + + private NodeDesc asNodeDesc(ProofId proofId, Node it) { + return new NodeDesc(proofId, it.serialNr(), it.getNodeInfo().getBranchLabel(), + it.getNodeInfo().getScriptRuleApplication(), collectPathInformation(it)); + } + + @Override + public CompletableFuture tree(ProofId proofId) { + return CompletableFuture.supplyAsync(() -> { + var proof = data.find(proofId); + return asNodeDescRecursive(proofId, proof.root()); + }); + } + + private NodeDesc asNodeDescRecursive(ProofId proofId, Node root) { + final List list = + root.childrenStream().map(it -> asNodeDescRecursive(proofId, it)).toList(); + return new NodeDesc(new NodeId(proofId, "" + root.serialNr()), + root.getNodeInfo().getBranchLabel(), + root.getNodeInfo().getScriptRuleApplication(), + list, collectPathInformation(root)); + } + + + @Override + public CompletableFuture> children(NodeId nodeId) { + return CompletableFuture.supplyAsync(() -> { + var node = data.find(nodeId); + return asNodeDesc(nodeId.proofId(), node.childrenStream()); + }); + } + + @Override + public CompletableFuture> pruneTo(NodeId nodeId) { + return null; + } + + /* + * @Override + * public CompletableFuture statistics(ProofId proofId) { + * return CompletableFuture.supplyAsync(() -> { + * var proof = data.find(proofId); + * return proof.getStatistics(); + * }); + * } + */ + + @Override + public CompletableFuture treeRoot(ProofId proof) { + return CompletableFuture.completedFuture( + TreeNodeDesc.from(proof, data.find(proof).root())); + } + + @Override + public CompletableFuture root(ProofId proofId) { + return CompletableFuture.supplyAsync(() -> { + var proof = data.find(proofId); + return asNodeDesc(proofId, proof.root()); + }); + } + + + @Override + public CompletableFuture> treeChildren(ProofId proof, TreeNodeId nodeId) { + return null; + } + + @Override + public CompletableFuture> treeSubtree(ProofId proof, TreeNodeId nodeId) { + return null; + } + + @Override + public CompletableFuture> sorts(EnvironmentId envId) { + return CompletableFuture.supplyAsync(() -> { + var env = data.find(envId); + var sorts = env.getServices().getNamespaces().sorts().allElements(); + return sorts.stream().map(SortDesc::from).toList(); + }); + } + + @Override + public CompletableFuture> functions(EnvironmentId envId) { + return CompletableFuture.supplyAsync(() -> { + var env = data.find(envId); + var functions = env.getServices().getNamespaces().functions().allElements(); + return functions.stream().map(FunctionDesc::from).toList(); + }); + } + + @Override + public CompletableFuture> contracts(EnvironmentId envId) { + return CompletableFuture.supplyAsync(() -> { + var env = data.find(envId); + var contracts = env.getProofContracts(); + return contracts.stream().map(it -> ContractDesc.from(envId, env.getServices(), it)) + .toList(); + }); + } + + @Override + public CompletableFuture openContract(ContractId contractId) { + return CompletableFuture.supplyAsync(() -> { + var env = data.find(contractId.envId()); + var contracts = env.getProofContracts(); + var contract = + contracts.stream() + .filter(it -> Objects.equals(it.getName(), contractId.contractId())) + .findFirst(); + if (contract.isPresent()) { + try { + var proof = env.createProof(contract.get().createProofObl(env.getInitConfig())); + return data.register(contractId.envId(), proof); + } catch (ProofInputException e) { + throw new RuntimeException(e); + } + } else { + return null; + } + }); + } + + @Override + public CompletableFuture dispose(EnvironmentId environmentId) { + data.dispose(environmentId); + return CompletableFuture.completedFuture( + true); + } + + @Override + public CompletableFuture print(NodeId nodeId, PrintOptions options) { + return CompletableFuture.supplyAsync(() -> { + var node = data.find(nodeId); + var env = data.find(nodeId.proofId().env()); + var notInfo = new NotationInfo(); + final var layouter = + new PosTableLayouter(options.width(), options.indentation(), options.pure()); + var lp = new LogicPrinter(notInfo, env.getServices(), layouter); + lp.printSequent(node.sequent()); + + var id = new NodeTextId(nodeId, uniqueCounter.getAndIncrement()); + var t = new NodeText(lp.result(), layouter.getInitialPositionTable()); + data.register(id, t); + return new NodeTextDesc(id, lp.result()); + }); + } + + private final IdentitySequentPrintFilter filter = new IdentitySequentPrintFilter(); + + @Override + public CompletableFuture> actions(NodeTextId printId, int caretPos) { + return CompletableFuture.supplyAsync(() -> { + var node = data.find(printId.nodeId()); + var proof = data.find(printId.nodeId().proofId()); + var goal = proof.getOpenGoal(node); + var nodeText = data.find(printId); + var pis = nodeText.table().getPosInSequent(caretPos, filter); + return new TermActionUtil(printId, data.find(printId.nodeId().proofId().env()), pis, + goal) + .getActions(); + }); + + } + + @Override + public CompletableFuture applyAction(TermActionId id) { + return CompletableFuture.completedFuture(false); + } + + @Override + public void freePrint(NodeTextId printId) { + CompletableFuture.runAsync(() -> data.dispose(printId)); + } + + public void setClientApi(ClientApi remoteProxy) { + clientApi = remoteProxy; + } + + private final DefaultUserInterfaceControl control = new MyDefaultUserInterfaceControl(); + + @Override + public CompletableFuture loadExample(String name) { + return CompletableFutures.computeAsync((c) -> { + var examples = ExampleChooser.listExamples(ExampleChooser.lookForExamples()) + .stream().filter(it -> it.getName().equals(name)).findFirst(); + if (examples.isPresent()) { + var ex = examples.get(); + Proof proof = null; + KeYEnvironment env = null; + try { + var loader = control.load(JavaProfile.getDefaultProfile(), + ex.getObligationFile(), + null, null, null, null, true, null); + InitConfig initConfig = loader.getInitConfig(); + + env = new KeYEnvironment<>(control, initConfig, loader.getProof(), + loader.getProofScript(), loader.getResult()); + var envId = new EnvironmentId(env.toString()); + data.register(envId, env); + proof = Objects.requireNonNull(env.getLoadedProof()); + var proofId = new ProofId(envId, proof.name().toString()); + return data.register(proofId, proof); + } catch (ProblemLoaderException e) { + if (env != null) + env.dispose(); + throw new RuntimeException(e); + } + } + throw new IllegalArgumentException("Unknown example"); + }); + } + + @Override + public CompletableFuture loadProblem(ProblemDefinition problem) { + return CompletableFutures.computeAsync((c) -> { + Proof proof = null; + KeYEnvironment env = null; + /* + * var loader = control.load(JavaProfile.getDefaultProfile(), + * ex.getObligationFile(), null, null, null, null, true, null); + * InitConfig initConfig = loader.getInitConfig(); + * + * env = new KeYEnvironment<>(control, initConfig, loader.getProof(), + * loader.getProofScript(), loader.getResult()); + * var envId = new EnvironmentId(env.toString()); + * data.register(envId, env); + * proof = Objects.requireNonNull(env.getLoadedProof()); + * var proofId = new ProofId(envId, proof.name().toString()); + * return data.register(proofId, proof); + */ + return null; + }); + + } + + @Override + public CompletableFuture loadKey(String content) { + return CompletableFutures.computeAsync((c) -> { + Proof proof = null; + KeYEnvironment env = null; + try { + final var tempFile = File.createTempFile("json-rpc-", ".key"); + Files.writeString(tempFile.toPath(), content); + var loader = control.load(JavaProfile.getDefaultProfile(), + tempFile.toPath(), null, null, null, null, true, null); + InitConfig initConfig = loader.getInitConfig(); + env = new KeYEnvironment<>(control, initConfig, loader.getProof(), + loader.getProofScript(), loader.getResult()); + var envId = new EnvironmentId(env.toString()); + data.register(envId, env); + proof = Objects.requireNonNull(env.getLoadedProof()); + var proofId = new ProofId(envId, proof.name().toString()); + return data.register(proofId, proof); + } catch (ProblemLoaderException | IOException e) { + if (env != null) + env.dispose(); + throw new RuntimeException(e); + } + }); + } + + @Override + public CompletableFuture loadTerm(String term) { + return loadKey("\\problem{ " + term + " }"); + } + + @Override + public CompletableFuture> load(LoadParams params) { + return CompletableFutures.computeAsync((c) -> { + Proof proof; + KeYEnvironment env; + try { + var loader = control.load(JavaProfile.getDefaultProfile(), + params.problemFile() != null ? params.problemFile().asPath() : null, + params.classPath() != null + ? params.classPath().stream().map(Uri::asPath).toList() + : null, + params.bootClassPath() != null ? params.bootClassPath().asPath() : null, + params.includes() != null ? params.includes().stream().map(Uri::asPath).toList() + : null, + null, + true, + null); + InitConfig initConfig = loader.getInitConfig(); + env = new KeYEnvironment<>(control, initConfig, loader.getProof(), + loader.getProofScript(), loader.getResult()); + var envId = new EnvironmentId(env.toString()); + data.register(envId, env); + if ((proof = env.getLoadedProof()) != null) { + var proofId = new ProofId(envId, proof.name().toString()); + return Either.forRight(data.register(proofId, proof)); + } else { + return Either.forLeft(envId); + } + } catch (ProblemLoaderException e) { + throw new RuntimeException(e); + } + }); + } + + private class MyDefaultUserInterfaceControl extends DefaultUserInterfaceControl { + @Override + public void taskStarted(org.key_project.prover.engine.TaskStartedInfo info) { + clientApi.taskStarted(org.keyproject.key.api.data.TaskStartedInfo.from(info)); + } + + @Override + public void taskProgress(int position) { + clientApi.taskProgress(position); + } + + @Override + public void taskFinished(org.key_project.prover.engine.TaskFinishedInfo info) { + clientApi.taskFinished(org.keyproject.key.api.data.TaskFinishedInfo.from(info)); + } + + @Override + protected void macroStarted(org.key_project.prover.engine.TaskStartedInfo info) { + clientApi.taskStarted(org.keyproject.key.api.data.TaskStartedInfo.from(info)); + } + + @Override + protected synchronized void macroFinished(ProofMacroFinishedInfo info) { + clientApi.taskFinished(org.keyproject.key.api.data.TaskFinishedInfo.from(info)); + } + + @Override + public void loadingStarted(AbstractProblemLoader loader) { + super.loadingStarted(loader); + } + + @Override + public void loadingFinished(AbstractProblemLoader loader, + IPersistablePO.LoadedPOContainer poContainer, ProofAggregate proofList, + AbstractProblemLoader.ReplayResult result) throws ProblemLoaderException { + super.loadingFinished(loader, poContainer, proofList, result); + } + + @Override + public void progressStarted(Object sender) { + super.progressStarted(sender); + } + + @Override + public void progressStopped(Object sender) { + super.progressStopped(sender); + } + + @Override + public void reportStatus(Object sender, String status, int progress) { + super.reportStatus(sender, status, progress); + } + + @Override + public void reportStatus(Object sender, String status) { + super.reportStatus(sender, status); + } + + @Override + public void resetStatus(Object sender) { + super.resetStatus(sender); + } + + @Override + public void reportException(Object sender, ProofOblInput input, Exception e) { + super.reportException(sender, input, e); + } + + @Override + public void setProgress(int progress) { + super.setProgress(progress); + } + + @Override + public void setMaximum(int maximum) { + super.setMaximum(maximum); + } + + @Override + public void reportWarnings(ImmutableSet warnings) { + super.reportWarnings(warnings); + } + + @Override + public void showIssueDialog(Collection issues) { + super.showIssueDialog(issues); + } + } +} diff --git a/keyext.api/src/main/java/org/keyproject/key/api/RuntimeClassNameTypeAdapterFactory.java b/keyext.api/src/main/java/org/keyproject/key/api/RuntimeClassNameTypeAdapterFactory.java new file mode 100644 index 00000000000..855e1e3ca84 --- /dev/null +++ b/keyext.api/src/main/java/org/keyproject/key/api/RuntimeClassNameTypeAdapterFactory.java @@ -0,0 +1,158 @@ +/* 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 org.keyproject.key.api; + +import java.io.IOException; +import java.util.LinkedHashMap; +import java.util.Map; + +import com.google.gson.Gson; +import com.google.gson.JsonElement; +import com.google.gson.JsonObject; +import com.google.gson.JsonParseException; +import com.google.gson.JsonPrimitive; +import com.google.gson.TypeAdapter; +import com.google.gson.TypeAdapterFactory; +import com.google.gson.internal.Streams; +import com.google.gson.reflect.TypeToken; +import com.google.gson.stream.JsonReader; +import com.google.gson.stream.JsonWriter; +import org.keyproject.key.api.data.KeYDataTransferObject; + +/* + * Taken & Modified from + * https://stackoverflow.com/questions/39999278/gson-how-to-include-class-name-property-when- + * serializing-object-of-any-type + */ + +public final class RuntimeClassNameTypeAdapterFactory implements TypeAdapterFactory { + private final Class baseType; + private final String typeFieldName; + private final Map> labelToSubtype = new LinkedHashMap>(); + private final Map, String> subtypeToLabel = new LinkedHashMap, String>(); + + private RuntimeClassNameTypeAdapterFactory(Class baseType, String typeFieldName) { + if (typeFieldName == null || baseType == null) { + throw new NullPointerException(); + } + this.baseType = baseType; + this.typeFieldName = typeFieldName; + } + + /** + * Creates a new runtime type adapter using for {@code baseType} using {@code + * typeFieldName} as the type field name. Type field names are case sensitive. + */ + public static RuntimeClassNameTypeAdapterFactory of(Class baseType, + String typeFieldName) { + return new RuntimeClassNameTypeAdapterFactory(baseType, typeFieldName); + } + + /** + * Creates a new runtime type adapter for {@code baseType} using {@code "type"} as + * the type field name. + */ + public static RuntimeClassNameTypeAdapterFactory of(Class baseType) { + return new RuntimeClassNameTypeAdapterFactory(baseType, "class"); + } + + /** + * Registers {@code type} identified by {@code label}. Labels are case + * sensitive. + * + * @throws IllegalArgumentException if either {@code type} or {@code label} + * have already been registered on this type adapter. + */ + public RuntimeClassNameTypeAdapterFactory registerSubtype(Class type, + String label) { + if (type == null || label == null) { + throw new NullPointerException(); + } + if (subtypeToLabel.containsKey(type) || labelToSubtype.containsKey(label)) { + throw new IllegalArgumentException("types and labels must be unique"); + } + labelToSubtype.put(label, type); + subtypeToLabel.put(type, label); + return this; + } + + /** + * Registers {@code type} identified by its {@link Class#getSimpleName simple + * name}. Labels are case sensitive. + * + * @throws IllegalArgumentException if either {@code type} or its simple name + * have already been registered on this type adapter. + */ + public RuntimeClassNameTypeAdapterFactory registerSubtype(Class type) { + return registerSubtype(type, type.getSimpleName()); + } + + public TypeAdapter create(Gson gson, TypeToken type) { + + if (!KeYDataTransferObject.class.isAssignableFrom(type.getRawType())) { + return null; + } + + final Map> labelToDelegate = + new LinkedHashMap>(); + final Map, TypeAdapter> subtypeToDelegate = + new LinkedHashMap, TypeAdapter>(); + + if (Object.class.isAssignableFrom(type.getRawType())) { + TypeAdapter delegate = gson.getDelegateAdapter(this, type); + // Modified: What is type.getRawType().getName() now was "class" before + labelToDelegate.put(type.getRawType().getName(), delegate); + subtypeToDelegate.put(type.getRawType(), delegate); + } + + return new TypeAdapter() { + @Override + public R read(JsonReader in) throws IOException { + JsonElement jsonElement = Streams.parse(in); + JsonElement labelJsonElement = jsonElement.getAsJsonObject().remove(typeFieldName); + if (labelJsonElement == null) { + throw new JsonParseException("cannot deserialize " + baseType + + " because it does not define a field named " + typeFieldName); + } + String label = labelJsonElement.getAsString(); + @SuppressWarnings("unchecked") // registration requires that subtype extends T + TypeAdapter delegate = (TypeAdapter) labelToDelegate.get(label); + if (delegate == null) { + throw new JsonParseException( + "cannot deserialize " + baseType + " subtype named " + + label + "; did you forget to register a subtype?"); + } + return delegate.fromJsonTree(jsonElement); + } + + @Override + public void write(JsonWriter out, R value) throws IOException { + Class srcType = value.getClass(); + String label = srcType.getName(); + @SuppressWarnings("unchecked") // registration requires that subtype extends T + TypeAdapter delegate = (TypeAdapter) subtypeToDelegate.get(srcType); + if (delegate == null) { + throw new JsonParseException("cannot serialize " + srcType.getName() + + "; did you forget to register a subtype?"); + } + JsonElement jsonTree = delegate.toJsonTree(value); + if (jsonTree.isJsonPrimitive()) { + Streams.write(jsonTree, out); + } else { + JsonObject jsonObject = jsonTree.getAsJsonObject(); + if (jsonObject.has(typeFieldName)) { + throw new JsonParseException("cannot serialize " + srcType.getName() + + " because it already defines a field named " + typeFieldName); + } + JsonObject clone = new JsonObject(); + clone.add(typeFieldName, new JsonPrimitive(label)); + for (Map.Entry e : jsonObject.entrySet()) { + clone.add(e.getKey(), e.getValue()); + } + Streams.write(clone, out); + } + } + }.nullSafe(); + } +} diff --git a/keyext.api/src/main/java/org/keyproject/key/api/StartServer.java b/keyext.api/src/main/java/org/keyproject/key/api/StartServer.java new file mode 100644 index 00000000000..e052a6e9f6d --- /dev/null +++ b/keyext.api/src/main/java/org/keyproject/key/api/StartServer.java @@ -0,0 +1,225 @@ +/* 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 org.keyproject.key.api; + + +import java.io.*; +import java.net.InetAddress; +import java.net.ServerSocket; +import java.net.Socket; +import java.util.concurrent.CancellationException; +import java.util.concurrent.ExecutionException; +import java.util.concurrent.Future; +import java.util.function.Function; +import javax.annotation.Nullable; + +import com.google.gson.GsonBuilder; +import org.eclipse.lsp4j.jsonrpc.Launcher; +import org.eclipse.lsp4j.websocket.jakarta.WebSocketLauncherBuilder; +import org.keyproject.key.api.adapters.KeyAdapter; +import org.keyproject.key.api.remoteclient.ClientApi; +import org.slf4j.Logger; +import org.slf4j.LoggerFactory; +import picocli.CommandLine; +import picocli.CommandLine.Option; + +/** + * @author Alexander Weigl + * @version 1 (07.10.23) + */ +@CommandLine.Command +public class StartServer implements Runnable { + private static final Logger LOGGER = LoggerFactory.getLogger(StartServer.class); + + // region CLI arguments + @Option(names = "--std", description = "use stdout and stdin for communication") + boolean stdStreams; + @Option(names = "--trace", description = "use stdout and stdin for communication") + boolean enableTracing; + + @Option(names = "--server", paramLabel = "PORT", description = "enables the TCP server mode") + @Nullable + Integer serverPort; + + @Option(names = "--connectTo", paramLabel = "PORT", description = "enables the TCP client mode") + @Nullable + Integer clientPort; + + + @Option(names = "--infile", paramLabel = "FILE or PIPE", + description = "read from named pipe or file") + @Nullable + File inFile; + + @Option(names = "--outfile", paramLabel = "FILE or PIPE", + description = "write to named pipe or file") + File outFile; + + @Option(names = { "-h", "--help" }, usageHelp = true, description = "display a help message") + boolean helpRequested = false; + + @Option(names = "--websocket") + boolean websocket = false; + // endregion + + public static void main(String[] args) { + new CommandLine(new StartServer()).execute(args); + } + + @Nullable + private InputStream in; + + @Nullable + private OutputStream out; + + @Nullable + private Socket socket; + + @Nullable + private Future listenerFuture; + + private void establishStreams() throws IOException { + in = System.in; + out = System.out; + + if (stdStreams) { + return; + } + + if (clientPort != null) { + socket = new Socket(InetAddress.getLocalHost(), clientPort); + socket.setKeepAlive(true); + socket.setTcpNoDelay(true); + in = socket.getInputStream(); + out = socket.getOutputStream(); + return; + } + + if (serverPort != null) { + var server = new ServerSocket(serverPort); + LOGGER.info("Waiting on port {}", serverPort); + socket = server.accept(); + LOGGER.info("Connection to client established: {}", socket.getRemoteSocketAddress()); + socket.setKeepAlive(true); + socket.setTcpNoDelay(true); + in = socket.getInputStream(); + out = socket.getOutputStream(); + return; + } + + if (inFile != null) { + in = new FileInputStream(inFile); + } + + if (outFile != null) { + out = new FileOutputStream(outFile); + } + + if (out == null || in == null) { + throw new IllegalStateException("Could not initialize the streams"); + } + } + + private boolean shutdownHandler() { + LOGGER.info("Shutting down..."); + try { + LOGGER.info("Closing Listener"); + if (listenerFuture != null) { + listenerFuture.cancel(true); + } + LOGGER.info("Closing In Stream"); + if (in != null) { + in.close(); + } + LOGGER.info("Closing Out Stream"); + if (out != null) { + out.close(); + } + LOGGER.info("Closing Socket"); + if (socket != null) { + socket.close(); + } + } catch (IOException e) { + LOGGER.error("Error while closing streams", e); + return false; + } + return true; + } + + + @Override + public void run() { + if (helpRequested) { + return; + } + + try { + final var keyApi = new KeyApiImpl(); + + if (websocket) { + var launcherBuilder = new WebSocketLauncherBuilder() + .setOutput(out) + .setInput(in) + .traceMessages(new PrintWriter(System.err)) + .validateMessages(true); + launcherBuilder.configureGson(StartServer::configureJson); + launcherBuilder.setLocalService(keyApi); + launcherBuilder.setRemoteInterface(ClientApi.class); + + final var clientApiLauncher = launcherBuilder.create(); + keyApi.setClientApi(clientApiLauncher.getRemoteProxy()); + clientApiLauncher.startListening().get(); + } else { + establishStreams(); + try (var lin = in; var lout = out) { + var listener = launch(lout, lin, keyApi); + LOGGER.info("JSON-RPC is listening for requests"); + keyApi.setClientApi(listener.getRemoteProxy()); + keyApi.setExitHandler(new Function() { + @Override + public Boolean apply(Void unused) { + return StartServer.this.shutdownHandler(); + } + }); + // listener.startListening().get(); + listenerFuture = listener.startListening(); + try { + listenerFuture.get(); + } catch (CancellationException e) { + LOGGER.info("Listener was cancelled; shutting down..."); + } + } + } + } catch (IOException | InterruptedException | ExecutionException e) { + throw new RuntimeException(e); + } + } + + + public static void configureJson(GsonBuilder gsonBuilder) { + gsonBuilder.registerTypeAdapter(File.class, new KeyAdapter.FileTypeAdapter()); + gsonBuilder.registerTypeAdapter(Throwable.class, new KeyAdapter.ThrowableAdapter()); + gsonBuilder.registerTypeAdapterFactory( + RuntimeClassNameTypeAdapterFactory.of(Object.class, "$class")); + gsonBuilder.serializeNulls(); + } + + public static Launcher launch(OutputStream out, InputStream in, KeyApiImpl keyApi) { + // var localServices = getLocalServices(); + // var remoteInterfaces = getRemoteInterfaces(); + var launcherBuilder = new Launcher.Builder() + .setOutput(out) + .setInput(in) + // .traceMessages(new PrintWriter(System.err)) + .validateMessages(true); + + launcherBuilder.configureGson(StartServer::configureJson); + // if (localServices != null && !localServices.isEmpty()) + launcherBuilder.setLocalService(keyApi); + // if (remoteInterfaces != null && !remoteInterfaces.isEmpty()) + launcherBuilder.setRemoteInterface(ClientApi.class); + + return launcherBuilder.create(); + } +} diff --git a/keyext.api/src/main/java/org/keyproject/key/api/TermActionUtil.java b/keyext.api/src/main/java/org/keyproject/key/api/TermActionUtil.java new file mode 100644 index 00000000000..75f3c029516 --- /dev/null +++ b/keyext.api/src/main/java/org/keyproject/key/api/TermActionUtil.java @@ -0,0 +1,137 @@ +/* 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 org.keyproject.key.api; + +import java.util.ArrayList; +import java.util.List; +import java.util.Set; + +import de.uka.ilkd.key.control.KeYEnvironment; +import de.uka.ilkd.key.control.ProofControl; +import de.uka.ilkd.key.macros.ProofMacro; +import de.uka.ilkd.key.pp.PosInSequent; +import de.uka.ilkd.key.proof.Goal; +import de.uka.ilkd.key.rule.*; + +import org.key_project.logic.Name; +import org.key_project.prover.sequent.PosInOccurrence; +import org.key_project.util.collection.ImmutableList; +import org.key_project.util.collection.ImmutableSLList; +import org.key_project.util.reflection.ClassLoaderUtil; + +import org.jspecify.annotations.NonNull; +import org.keyproject.key.api.data.KeyIdentifications; +import org.keyproject.key.api.data.KeyIdentifications.NodeTextId; +import org.keyproject.key.api.data.TermActionDesc; +import org.keyproject.key.api.data.TermActionKind; + +/** + * @author Alexander Weigl + * @version 1 (29.10.23) + */ +public class TermActionUtil { + private static final Set CLUTTER_RULESETS = + Set.of(new Name("notHumanReadable"), + new Name("obsolete"), + new Name("pullOutQuantifierAll"), + new Name("pullOutQuantifierEx")); + + private static final Set CLUTTER_RULES = Set.of( + new Name("cut_direct_r"), + new Name("cut_direct_l"), + new Name("case_distinction_r"), + new Name("case_distinction_l"), + new Name("local_cut"), + new Name("commute_and_2"), + new Name("commute_or_2"), + new Name("boxToDiamond"), + new Name("pullOut"), + new Name("typeStatic"), + new Name("less_is_total"), + new Name("less_zero_is_total"), + new Name("applyEqReverse"), + + // the following are used for drag'n'drop interactions + new Name("eqTermCut"), + new Name("instAll"), + new Name("instEx")); + private static final Set FILTER_SCRIPT_COMMANDS = Set.of( + "exit", + "leave", + "javascript", + "skip", + "macro", + "rule", + "script"); + + private final PosInSequent pos; + private final Goal goal; + private final PosInOccurrence occ; + + private final List actions = new ArrayList<>(1024); + private final NodeTextId nodeTextId; + + public TermActionUtil(@NonNull NodeTextId nodeTextId, @NonNull KeYEnvironment env, + @NonNull PosInSequent pos, @NonNull Goal goal) { + this.pos = pos; + this.goal = goal; + this.nodeTextId = nodeTextId; + occ = pos.getPosInOccurrence(); + ProofControl c = env.getUi().getProofControl(); + final ImmutableList builtInRules = c.getBuiltInRule(goal, occ); + var macros = ClassLoaderUtil.loadServices(ProofMacro.class); + for (ProofMacro macro : macros) { + var id = new KeyIdentifications.TermActionId(nodeTextId.nodeId(), pos.toString(), + "macro:" + macro.getScriptCommandName()); + TermActionDesc ta = new TermActionDesc(id, macro.getName(), macro.getDescription(), + macro.getCategory(), TermActionKind.Macro); + add(ta); + } + ImmutableList findTaclet = c.getFindTaclet(goal, occ); + var find = removeRewrites(findTaclet) + .prepend(c.getRewriteTaclet(goal, occ)); + var nofind = c.getNoFindTaclet(goal); + + + for (TacletApp tacletApp : find) { + var id = new KeyIdentifications.TermActionId(nodeTextId.nodeId(), pos.toString(), + "find:" + tacletApp.rule()); + TermActionDesc ta = new TermActionDesc(id, tacletApp.rule().displayName(), + tacletApp.rule().toString(), "", TermActionKind.Taclet); + add(ta); + } + + for (TacletApp tacletApp : nofind) { + var id = new KeyIdentifications.TermActionId(nodeTextId.nodeId(), pos.toString(), + "nofind:" + tacletApp.rule()); + TermActionDesc ta = new TermActionDesc(id, tacletApp.rule().displayName(), + tacletApp.rule().toString(), "", TermActionKind.Taclet); + add(ta); + } + } + + private void add(TermActionDesc ta) { + actions.add(ta); + } + + /** + * Removes RewriteTaclet from the list. + * + * @param list the IList from where the RewriteTaclet are removed + * @return list without RewriteTaclets + */ + private static ImmutableList removeRewrites( + ImmutableList list) { + ImmutableList result = ImmutableSLList.nil(); + for (TacletApp tacletApp : list) { + Taclet taclet = tacletApp.taclet(); + result = (taclet instanceof RewriteTaclet ? result : result.prepend(tacletApp)); + } + return result; + } + + public List getActions() { + return actions; + } +} diff --git a/keyext.api/src/main/java/org/keyproject/key/api/adapters/KeyAdapter.java b/keyext.api/src/main/java/org/keyproject/key/api/adapters/KeyAdapter.java new file mode 100644 index 00000000000..414cc332e5d --- /dev/null +++ b/keyext.api/src/main/java/org/keyproject/key/api/adapters/KeyAdapter.java @@ -0,0 +1,120 @@ +/* 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 org.keyproject.key.api.adapters; + +import java.io.File; +import java.io.IOException; +import java.lang.reflect.Type; + +import de.uka.ilkd.key.macros.ProofMacro; + +import org.key_project.logic.op.Function; + +import com.google.gson.*; +import com.google.gson.stream.JsonReader; +import com.google.gson.stream.JsonToken; +import com.google.gson.stream.JsonWriter; +import org.keyproject.key.api.data.MacroDescription; + +/** + * @author Alexander Weigl + * @version 1 (14.10.23) + */ +public class KeyAdapter { + // private final BiMap> map = HashBiMap.create(1024); + // private final TypeAdapter adaptor; + + public KeyAdapter(GsonBuilder gson) { + gson.registerTypeAdapter(File.class, new FileTypeAdapter()); + // gson.registerTypeAdapter(Function.class, new FunctionSerializer()); + // gson.registerTypeAdapter(ProofMacro.class, new MacroSerializer()); + } + + + /* + * //translating entities to identification strings + * public void insert(Identifiable p) { + * var id = p.identification(); + * if (!map.containsKey(id)) { + * map.put(id, new WeakReference<>(p)); + * } + * } + * + * public Object find(String id) { + * return map.get(id).get(); + * } + * //endregion + */ + + static class MacroSerializer implements JsonSerializer { + @Override + public JsonElement serialize(ProofMacro src, Type typeOfSrc, + JsonSerializationContext context) { + return context.serialize(MacroDescription.from(src)); + } + } + + public static class FileTypeAdapter extends TypeAdapter { + @Override + public void write(JsonWriter out, File value) throws IOException { + out.value(String.valueOf(value)); + } + + @Override + public File read(JsonReader in) throws IOException { + var tokenType = in.peek(); + if (tokenType == JsonToken.NULL) { + in.nextNull(); + return null; + } + return new File(in.nextString()); + } + } + + static class FunctionSerializer implements JsonSerializer { + @Override + public JsonElement serialize(Function src, Type typeOfSrc, + JsonSerializationContext context) { + var obj = new JsonObject(); + obj.add("name", context.serialize(src.name().toString())); + obj.add("skolemConstant", context.serialize(src.isSkolemConstant())); + obj.add("isRigid", context.serialize(src.isRigid())); + obj.add("isUnique", context.serialize(src.isUnique())); + obj.add("sort", context.serialize(src.sort())); + obj.add("argSorts", context.serialize(src.argSorts())); + return obj; + } + } + + public static class ThrowableAdapter implements JsonSerializer { + @Override + public JsonElement serialize(Throwable src, Type typeOfSrc, + JsonSerializationContext context) { + var obj = new JsonObject(); + obj.add("$class", context.serialize(src.getClass().getSimpleName())); + obj.add("message", context.serialize(src.getMessage())); + obj.add("cause", context.serialize(src.getCause())); + return obj; + } + } + + /* + * class IdentifiableTypeAdapter implements JsonSerializer, + * JsonDeserializer { + * + * @Override + * public Identifiable deserialize(JsonElement json, Type typeOfT, JsonDeserializationContext + * context) throws JsonParseException { + * return (Identifiable) find(json.getAsString()); + * } + * + * @Override + * public JsonElement serialize(Identifiable src, Type typeOfSrc, JsonSerializationContext + * context) { + * insert(src); + * return context.serialize(src.identification()); + * } + * } + */ +} diff --git a/keyext.api/src/main/java/org/keyproject/key/api/adapters/package-info.java b/keyext.api/src/main/java/org/keyproject/key/api/adapters/package-info.java new file mode 100644 index 00000000000..522f32d9b3b --- /dev/null +++ b/keyext.api/src/main/java/org/keyproject/key/api/adapters/package-info.java @@ -0,0 +1,7 @@ +/** + * Adapter classes for translating things from Java to JSON via GSON api. + * + * @author Alexander Weigl + * @version 1 (14.10.23) + */ +package org.keyproject.key.api.adapters; diff --git a/keyext.api/src/main/java/org/keyproject/key/api/data/ContractDesc.java b/keyext.api/src/main/java/org/keyproject/key/api/data/ContractDesc.java new file mode 100644 index 00000000000..16dac00a307 --- /dev/null +++ b/keyext.api/src/main/java/org/keyproject/key/api/data/ContractDesc.java @@ -0,0 +1,35 @@ +/* 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 org.keyproject.key.api.data; + +import de.uka.ilkd.key.java.Services; +import de.uka.ilkd.key.speclang.Contract; + +/** + * Description of a loadable contract in KeY. + * + * Contracts can be arbitrary objects, representing a functional, dependency, information flow, etc. + * contract. + * Contracts can be loaded into proofs. + * + * @param contractId an identifier of the contract + * @param name Name of the contract + * @param displayName Showable name + * @param typeName the typename which is associated with this contract + * @param htmlText content of the contract as html text + * @param plainText content of the contract as plain text + * + * @author Alexander Weigl + * @version 1 (13.10.23) + */ +public record ContractDesc(KeyIdentifications.ContractId contractId, String name, + String displayName, String typeName, String htmlText, String plainText) + implements KeYDataTransferObject { + public static ContractDesc from(KeyIdentifications.EnvironmentId envId, + Services services, Contract it) { + return new ContractDesc(new KeyIdentifications.ContractId(envId, it.getName()), + it.getName(), it.getDisplayName(), it.getTypeName(), + it.getHTMLText(services), it.getPlainText(services)); + } +} diff --git a/keyext.api/src/main/java/org/keyproject/key/api/data/DataExamples.java b/keyext.api/src/main/java/org/keyproject/key/api/data/DataExamples.java new file mode 100644 index 00000000000..621494e9b03 --- /dev/null +++ b/keyext.api/src/main/java/org/keyproject/key/api/data/DataExamples.java @@ -0,0 +1,150 @@ +/* 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 org.keyproject.key.api.data; + +import java.io.File; +import java.lang.reflect.InvocationTargetException; +import java.util.List; +import java.util.Map; +import java.util.TreeMap; +import java.util.concurrent.ExecutionException; + +import de.uka.ilkd.key.macros.FinishSymbolicExecutionMacro; +import de.uka.ilkd.key.scripts.RuleCommand; + +import com.google.gson.Gson; +import com.google.gson.GsonBuilder; +import org.jspecify.annotations.Nullable; +import org.keyproject.key.api.KeyApiImpl; +import org.keyproject.key.api.data.KeyIdentifications.EnvironmentId; +import org.keyproject.key.api.data.KeyIdentifications.ProofId; +import org.keyproject.key.api.remoteapi.ServerManagement; +import org.keyproject.key.api.remoteclient.ShowDocumentParams; +import org.keyproject.key.api.remoteclient.ShowDocumentResult; + +public class DataExamples { + private final KeyApiImpl impl = new KeyApiImpl(); + // private final KeyIdentifications.ProofId proof; + + public DataExamples() throws ExecutionException, InterruptedException { + // var name = impl.examples().get().getFirst().name(); + // proof = impl.loadExample(name).get(); + } + + private static @Nullable DataExamples instance; + private static final Map cache = new TreeMap<>(); + private static final Gson gson = new GsonBuilder().setPrettyPrinting().create(); + + public static @Nullable String get(String typeFullName) { + try { + if (cache.containsKey(typeFullName)) { + return cache.get(typeFullName); + } + + if (instance == null) { + instance = new DataExamples(); + } + + var clazz = Class.forName(typeFullName); + for (var method : instance.getClass().getMethods()) { + if (method.getReturnType().equals(clazz)) { + var object = method.invoke(instance); + return gson.toJson(object); + } + } + + return null; + } catch (ClassNotFoundException | ExecutionException | InterruptedException + | IllegalAccessException | InvocationTargetException e) { + throw new RuntimeException(e); + } + } + + + /* + * public ExampleDesc getExample() { + * return ExampleChooser.listExamples(ExampleChooser.lookForExamples()) + * .stream().map(ExampleDesc::from).findFirst().orElseThrow(); + * } + */ + + public ServerManagement.SetTraceParams getTraceParams() { + return new ServerManagement.SetTraceParams(TraceValue.Info); + } + + public ProofStatus getProofStatus() { + return new ProofStatus(getProofId(), 10, 23); + } + + public LoadParams getLoadParams() { + return new LoadParams(Uri.from(new File("/home/weigl/test.key")), + List.of(), null, List.of()); + } + + + public ProofId getProofId() { + return new ProofId(getEnvId(), "proof-5"); + } + + public EnvironmentId getEnvId() { + return new EnvironmentId("env-1"); + } + + public ShowDocumentParams getSDP() { + return new ShowDocumentParams("", true, true, getTextRange()); + } + + public @Nullable TextRange getTextRange() { + return new TextRange(25, 100); + } + + public ShowDocumentResult getSDR() { + return new ShowDocumentResult(true); + } + + public TermActionDesc getTermActionDesc() { + return new TermActionDesc(getTermActionId(), "andLeft", "Apply taclet 'andLeft'.", + "rules", TermActionKind.Taclet); + } + + private KeyIdentifications.TermActionId getTermActionId() { + return new KeyIdentifications.TermActionId(getNodeId(), "0.1.0", "taclet-andLeft-010"); + } + + private KeyIdentifications.NodeId getNodeId() { + return new KeyIdentifications.NodeId(getProofId(), "01010102"); + } + + public MacroDescription getMacroDescription() { + return MacroDescription.from(new FinishSymbolicExecutionMacro()); + } + + public PrintOptions getPrintingOptions() { + return new PrintOptions(true, 80, 4, true, false); + } + + public ProofScriptCommandDesc getPSCDesc() throws ExecutionException, InterruptedException { + return ProofScriptCommandDesc.from(new RuleCommand()); + } + + /* + * public NodeTextDesc getNodeText() throws ExecutionException, InterruptedException { + * var root = impl.treeRoot(proof).get(); + * return impl.print(root.id(), getPrintingOptions()).get(); + * } + * + * public FunctionDesc getFunctionDescription() throws ExecutionException, InterruptedException + * { + * return impl.functions(proof.env()).get().getFirst(); + * } + * + * public ProofScriptCommandDesc getPSCDesc() throws ExecutionException, InterruptedException { + * return impl.getAvailableScriptCommands().get().getFirst(); + * } + * + * public SortDesc getSortDesc() throws ExecutionException, InterruptedException { + * return impl.sorts(proof.env()).get().getFirst(); + * } + */ +} diff --git a/keyext.api/src/main/java/org/keyproject/key/api/data/ExampleDesc.java b/keyext.api/src/main/java/org/keyproject/key/api/data/ExampleDesc.java new file mode 100644 index 00000000000..0e3a53057c2 --- /dev/null +++ b/keyext.api/src/main/java/org/keyproject/key/api/data/ExampleDesc.java @@ -0,0 +1,21 @@ +/* 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 org.keyproject.key.api.data; + +import de.uka.ilkd.key.gui.Example; + +/** + * This class represents a built-in example. + * TODO (weigl,rpc) Also deliver the contents of the example (files)? + * + * @param name the name of the example, also used as an identifer + * @param description a description of the example + * @author Alexander Weigl + * @version 1 (29.10.23) + */ +public record ExampleDesc(String name, String description) { + public static ExampleDesc from(Example example) { + return new ExampleDesc(example.getName(), example.getDescription()); + } +} diff --git a/keyext.api/src/main/java/org/keyproject/key/api/data/FunctionDesc.java b/keyext.api/src/main/java/org/keyproject/key/api/data/FunctionDesc.java new file mode 100644 index 00000000000..c86e4a45179 --- /dev/null +++ b/keyext.api/src/main/java/org/keyproject/key/api/data/FunctionDesc.java @@ -0,0 +1,27 @@ +/* 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 org.keyproject.key.api.data; + +import java.util.List; + +import org.key_project.logic.op.Function; + + +/** + * @author Alexander Weigl + * @version 1 (15.10.23) + */ +public record FunctionDesc(String name, String sort, SortDesc retSort, + List argSorts, + boolean rigid, + boolean unique, boolean skolemConstant) implements KeYDataTransferObject { + public static FunctionDesc from(Function fn) { + return new FunctionDesc(fn.name().toString(), fn.sort().declarationString(), + SortDesc.from(fn.sort()), + fn.argSorts().stream().map(SortDesc::from).toList(), + fn.isRigid(), + fn.isUnique(), + fn.isSkolemConstant()); + } +} diff --git a/keyext.api/src/main/java/org/keyproject/key/api/data/KeYDataTransferObject.java b/keyext.api/src/main/java/org/keyproject/key/api/data/KeYDataTransferObject.java new file mode 100644 index 00000000000..6a4e8711ce5 --- /dev/null +++ b/keyext.api/src/main/java/org/keyproject/key/api/data/KeYDataTransferObject.java @@ -0,0 +1,9 @@ +/* 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 org.keyproject.key.api.data; + +/// An object allowed to be transfered via the JSON RPC +/// +public interface KeYDataTransferObject { +} diff --git a/keyext.api/src/main/java/org/keyproject/key/api/data/KeyIdentifications.java b/keyext.api/src/main/java/org/keyproject/key/api/data/KeyIdentifications.java new file mode 100644 index 00000000000..0a8b67c2893 --- /dev/null +++ b/keyext.api/src/main/java/org/keyproject/key/api/data/KeyIdentifications.java @@ -0,0 +1,172 @@ +/* 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 org.keyproject.key.api.data; + +import java.util.Objects; + +import de.uka.ilkd.key.control.KeYEnvironment; +import de.uka.ilkd.key.proof.Node; +import de.uka.ilkd.key.proof.Proof; + +import com.google.common.collect.BiMap; +import com.google.common.collect.HashBiMap; + +/** + * @author Alexander Weigl + * @version 1 (29.10.23) + */ +public class KeyIdentifications { + private final BiMap mapEnv = HashBiMap.create(16); + + public KeyEnvironmentContainer getContainer(EnvironmentId environmentId) { + return Objects.requireNonNull(mapEnv.get(environmentId), + "Could not find environment for id" + environmentId); + } + + public ProofContainer getContainer(ProofId proofId) { + return Objects.requireNonNull(getContainer(proofId.env()).mapProof.get(proofId), + "Could not find proof for id" + proofId); + } + + public KeYEnvironment find(EnvironmentId envid) { + return getContainer(envid).env; + } + + public Proof find(ProofId proofId) { + return getContainer(proofId).wProof; + } + + public NodeText find(NodeTextId nodeTextId) { + return Objects.requireNonNull( + getContainer(nodeTextId.nodeId().proofId()).mapGoalText.get(nodeTextId), + "Could not find a print-out with the id " + nodeTextId); + } + + public void dispose(NodeTextId nodeTextId) { + var c = getContainer(nodeTextId.nodeId().proofId()); + c.mapGoalText.remove(nodeTextId); + } + + public void dispose(ProofId id) { + var c = getContainer(id); + getContainer(id.env).mapProof.remove(id); + c.dispose(); + } + + public void dispose(EnvironmentId id) { + var c = getContainer(id); + c.mapProof.forEach(((proofId, proofContainer) -> this.dispose(proofId))); + mapEnv.remove(id); + c.dispose(); + } + + public Node find(NodeId nodeId) { + Proof p = find(nodeId.proofId); + var id = Integer.parseInt(nodeId.nodeId()); + var opt = p.findAny(it -> it.serialNr() == id); + return Objects.requireNonNull(opt, "Could not find node with serialNr " + nodeId.nodeId); + } + + public ProofId register(EnvironmentId envId, Proof proof) { + var id = new ProofId(envId, proof.name().toString()); + getContainer(envId).mapProof.put(id, new ProofContainer(proof)); + return id; + } + + public void register(NodeTextId nodeId, NodeText nodeText) { + var c = getContainer(nodeId.nodeId().proofId()); + c.mapGoalText().put(nodeId, nodeText); + + } + + public EnvironmentId register(EnvironmentId envId, KeYEnvironment env) { + mapEnv.put(envId, new KeyEnvironmentContainer(env)); + return envId; + } + + public ProofId register(ProofId proofId, Proof proof) { + getContainer(proofId.env()).mapProof.put(proofId, new ProofContainer(proof)); + return proofId; + } + + + /** + * @author Alexander Weigl + * @version 1 (28.10.23) + */ + public record EnvironmentId(String envId) implements KeYDataTransferObject { + } + + /** + * @author Alexander Weigl + * @version 1 (28.10.23) + */ + public record ContractId(EnvironmentId envId, String contractId) + implements KeYDataTransferObject { + } + + /** + * @author Alexander Weigl + * @version 1 (29.10.23) + */ + public record NodeId(ProofId proofId, String nodeId) implements KeYDataTransferObject { + } + + public record ProofId(EnvironmentId env, String proofId) implements KeYDataTransferObject { + } + + /** + * @author Alexander Weigl + * @version 1 (29.10.23) + */ + public record NodeTextId(NodeId nodeId, int nodeTextId) implements KeYDataTransferObject { + } + + + /** + * @author Alexander Weigl + * @version 1 (13.10.23) + */ + public record TermActionId(NodeId nodeId, String pio, String id) + implements KeYDataTransferObject { + } + + /** + * @author Alexander Weigl + * @version 1 (13.10.23) + */ + public record TreeNodeId(String id) implements KeYDataTransferObject { + } + + + /** + * @author Alexander Weigl + * @version 1 (28.10.23) + */ + public record KeyEnvironmentContainer(KeYEnvironment env, + BiMap mapProof) { + + public KeyEnvironmentContainer(KeYEnvironment env) { + this(env, HashBiMap.create(1)); + } + + void dispose() { + mapProof.clear(); + env.dispose(); + } + } + + private record ProofContainer(Proof wProof, + BiMap mapNode, + BiMap mapTreeNode, + BiMap mapGoalText) { + public ProofContainer(Proof proof) { + this(proof, HashBiMap.create(16), HashBiMap.create(16), HashBiMap.create(16)); + } + + void dispose() { + mapNode.clear(); + } + } +} diff --git a/keyext.api/src/main/java/org/keyproject/key/api/data/LoadParams.java b/keyext.api/src/main/java/org/keyproject/key/api/data/LoadParams.java new file mode 100644 index 00000000000..4b0809941ba --- /dev/null +++ b/keyext.api/src/main/java/org/keyproject/key/api/data/LoadParams.java @@ -0,0 +1,22 @@ +/* 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 org.keyproject.key.api.data; + +import java.util.List; + +import org.jspecify.annotations.Nullable; + +/** + * + * @param problemFile URI to the problem file to be loaded + * @param classPath optional + * @param bootClassPath xxx + * @param includes xxx + */ +public record LoadParams(@Nullable Uri problemFile, + @Nullable List classPath, + @Nullable Uri bootClassPath, + @Nullable List includes) + implements KeYDataTransferObject { +} diff --git a/keyext.api/src/main/java/org/keyproject/key/api/data/MacroDescription.java b/keyext.api/src/main/java/org/keyproject/key/api/data/MacroDescription.java new file mode 100644 index 00000000000..09b98b19ccb --- /dev/null +++ b/keyext.api/src/main/java/org/keyproject/key/api/data/MacroDescription.java @@ -0,0 +1,20 @@ +/* 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 org.keyproject.key.api.data; + +import de.uka.ilkd.key.macros.ProofMacro; + +/** + * + * @param name + * @param description + * @param category + */ +public record MacroDescription(String name, String description, String category) + implements KeYDataTransferObject { + + public static MacroDescription from(ProofMacro m) { + return new MacroDescription(m.getName(), m.getDescription(), m.getCategory()); + } +} diff --git a/keyext.api/src/main/java/org/keyproject/key/api/data/MacroStatistic.java b/keyext.api/src/main/java/org/keyproject/key/api/data/MacroStatistic.java new file mode 100644 index 00000000000..ac4b75275a9 --- /dev/null +++ b/keyext.api/src/main/java/org/keyproject/key/api/data/MacroStatistic.java @@ -0,0 +1,19 @@ +/* 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 org.keyproject.key.api.data; + +import de.uka.ilkd.key.macros.ProofMacroFinishedInfo; + +/** + * @author Alexander Weigl + * @version 1 (13.10.23) + */ +public record MacroStatistic(KeyIdentifications.ProofId proofId, String macroId, int appliedRules, + int closedGoals) implements KeYDataTransferObject { + public static MacroStatistic from(KeyIdentifications.ProofId proofId, + ProofMacroFinishedInfo info) { + return new MacroStatistic(proofId, info.getMacro().getName(), info.getAppliedRules(), + info.getClosedGoals()); + } +} diff --git a/keyext.api/src/main/java/org/keyproject/key/api/data/NodeDesc.java b/keyext.api/src/main/java/org/keyproject/key/api/data/NodeDesc.java new file mode 100644 index 00000000000..6002b896c32 --- /dev/null +++ b/keyext.api/src/main/java/org/keyproject/key/api/data/NodeDesc.java @@ -0,0 +1,25 @@ +/* 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 org.keyproject.key.api.data; + +import java.util.List; + +import org.jspecify.annotations.Nullable; + +/** + * @author Alexander Weigl + * @version 1 (13.10.23) + */ +public record NodeDesc(KeyIdentifications.NodeId nodeid, + String branchLabel, + boolean scriptRuleApplication, + @Nullable List children, + String description) implements KeYDataTransferObject { + public NodeDesc(KeyIdentifications.ProofId proofId, int serialNr, String branchLabel, + boolean scriptRuleApplication, String description) { + this(new KeyIdentifications.NodeId(proofId, "" + serialNr), branchLabel, + scriptRuleApplication, + null, description); + } +} diff --git a/keyext.api/src/main/java/org/keyproject/key/api/data/NodeText.java b/keyext.api/src/main/java/org/keyproject/key/api/data/NodeText.java new file mode 100644 index 00000000000..ddc57f452da --- /dev/null +++ b/keyext.api/src/main/java/org/keyproject/key/api/data/NodeText.java @@ -0,0 +1,13 @@ +/* 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 org.keyproject.key.api.data; + +import de.uka.ilkd.key.pp.InitialPositionTable; + +/** + * @author Alexander Weigl + * @version 1 (13.10.23) + */ +public record NodeText(String text, InitialPositionTable table) { +} diff --git a/keyext.api/src/main/java/org/keyproject/key/api/data/NodeTextDesc.java b/keyext.api/src/main/java/org/keyproject/key/api/data/NodeTextDesc.java new file mode 100644 index 00000000000..d47182cdf78 --- /dev/null +++ b/keyext.api/src/main/java/org/keyproject/key/api/data/NodeTextDesc.java @@ -0,0 +1,19 @@ +/* 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 org.keyproject.key.api.data; + + +import org.keyproject.key.api.data.KeyIdentifications.NodeTextId; + +/** + * A printed sequent. + * + * @param id a handle identifying this print-out + * @param result the plain textual notation of the sequent + * @author Alexander Weigl + * @version 1 (29.10.23) + */ +public record NodeTextDesc(NodeTextId id, String result) + implements KeYDataTransferObject { +} diff --git a/keyext.api/src/main/java/org/keyproject/key/api/data/PredicateDesc.java b/keyext.api/src/main/java/org/keyproject/key/api/data/PredicateDesc.java new file mode 100644 index 00000000000..c8be657b4b5 --- /dev/null +++ b/keyext.api/src/main/java/org/keyproject/key/api/data/PredicateDesc.java @@ -0,0 +1,13 @@ +/* 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 org.keyproject.key.api.data; + +import java.util.List; + +/** + * @author Alexander Weigl + * @version 1 (15.10.23) + */ +public record PredicateDesc(String name, List argSorts) implements KeYDataTransferObject { +} diff --git a/keyext.api/src/main/java/org/keyproject/key/api/data/PrintOptions.java b/keyext.api/src/main/java/org/keyproject/key/api/data/PrintOptions.java new file mode 100644 index 00000000000..aad19e86abe --- /dev/null +++ b/keyext.api/src/main/java/org/keyproject/key/api/data/PrintOptions.java @@ -0,0 +1,12 @@ +/* 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 org.keyproject.key.api.data; + +/** + * @author Alexander Weigl + * @version 1 (29.10.23) + */ +public record PrintOptions(boolean unicode, int width, int indentation, boolean pure, + boolean termLabels) { +} diff --git a/keyext.api/src/main/java/org/keyproject/key/api/data/ProblemDefinition.java b/keyext.api/src/main/java/org/keyproject/key/api/data/ProblemDefinition.java new file mode 100644 index 00000000000..6397f247821 --- /dev/null +++ b/keyext.api/src/main/java/org/keyproject/key/api/data/ProblemDefinition.java @@ -0,0 +1,21 @@ +/* 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 org.keyproject.key.api.data; + + +import java.util.List; + +import org.jspecify.annotations.Nullable; + +/** + * @author Alexander Weigl + * @version 1 (15.10.23) + */ +public record ProblemDefinition( + @Nullable List sorts, + @Nullable List functions, + @Nullable List predicates, + @Nullable List antecTerms, + @Nullable List succTerms) implements KeYDataTransferObject { +} diff --git a/keyext.api/src/main/java/org/keyproject/key/api/data/ProofMacroDesc.java b/keyext.api/src/main/java/org/keyproject/key/api/data/ProofMacroDesc.java new file mode 100644 index 00000000000..34f0e21f2a0 --- /dev/null +++ b/keyext.api/src/main/java/org/keyproject/key/api/data/ProofMacroDesc.java @@ -0,0 +1,18 @@ +/* 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 org.keyproject.key.api.data; + +import de.uka.ilkd.key.macros.ProofMacro; + +/** + * @author Alexander Weigl + * @version 1 (29.10.23) + */ +public record ProofMacroDesc(String name, String category, String description, + String scriptCommandName) implements KeYDataTransferObject { + public static ProofMacroDesc from(ProofMacro proofMacro) { + return new ProofMacroDesc(proofMacro.getName(), proofMacro.getCategory(), + proofMacro.getDescription(), proofMacro.getScriptCommandName()); + } +} diff --git a/keyext.api/src/main/java/org/keyproject/key/api/data/ProofScriptCommandDesc.java b/keyext.api/src/main/java/org/keyproject/key/api/data/ProofScriptCommandDesc.java new file mode 100644 index 00000000000..f4d1722e1c9 --- /dev/null +++ b/keyext.api/src/main/java/org/keyproject/key/api/data/ProofScriptCommandDesc.java @@ -0,0 +1,18 @@ +/* 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 org.keyproject.key.api.data; + +import de.uka.ilkd.key.scripts.ProofScriptCommand; + +/** + * @author Alexander Weigl + * @version 1 (29.10.23) + */ +public record ProofScriptCommandDesc(String macroId, String documentation) + implements KeYDataTransferObject { + public static ProofScriptCommandDesc from(ProofScriptCommand proofScriptCommand) { + return new ProofScriptCommandDesc(proofScriptCommand.getName(), + proofScriptCommand.getDocumentation()); + } +} diff --git a/keyext.api/src/main/java/org/keyproject/key/api/data/ProofStatus.java b/keyext.api/src/main/java/org/keyproject/key/api/data/ProofStatus.java new file mode 100644 index 00000000000..432dac80244 --- /dev/null +++ b/keyext.api/src/main/java/org/keyproject/key/api/data/ProofStatus.java @@ -0,0 +1,21 @@ +/* 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 org.keyproject.key.api.data; + +import de.uka.ilkd.key.proof.Proof; + +/** + * + * @param id handle of the proof + * @param openGoals open goals + * @param closedGoals closed goals + * @author teuber + */ +public record ProofStatus(KeyIdentifications.ProofId id, int openGoals, int closedGoals) + implements KeYDataTransferObject { + + public static ProofStatus from(KeyIdentifications.ProofId id, Proof proof) { + return new ProofStatus(id, proof.openGoals().size(), proof.closedGoals().size()); + } +} diff --git a/keyext.api/src/main/java/org/keyproject/key/api/data/SortDesc.java b/keyext.api/src/main/java/org/keyproject/key/api/data/SortDesc.java new file mode 100644 index 00000000000..212d8248567 --- /dev/null +++ b/keyext.api/src/main/java/org/keyproject/key/api/data/SortDesc.java @@ -0,0 +1,22 @@ +/* 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 org.keyproject.key.api.data; + +import java.util.List; + +import org.key_project.logic.sort.Sort; + +/** + * @author Alexander Weigl + * @version 1 (13.10.23) + */ +public record SortDesc(String string, String documentation, + List extendsSorts, + boolean anAbstract, String s) implements KeYDataTransferObject { + public static SortDesc from(Sort sort) { + return new SortDesc(sort.name().toString(), sort.getDocumentation(), + sort.extendsSorts().stream().map(SortDesc::from).toList(), + sort.isAbstract(), sort.declarationString()); + } +} diff --git a/keyext.api/src/main/java/org/keyproject/key/api/data/StrategyOptions.java b/keyext.api/src/main/java/org/keyproject/key/api/data/StrategyOptions.java new file mode 100644 index 00000000000..ab65233fea5 --- /dev/null +++ b/keyext.api/src/main/java/org/keyproject/key/api/data/StrategyOptions.java @@ -0,0 +1,96 @@ +/* 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 org.keyproject.key.api.data; + +import java.lang.reflect.Field; + +import de.uka.ilkd.key.proof.Proof; +import de.uka.ilkd.key.settings.StrategySettings; +import de.uka.ilkd.key.strategy.StrategyProperties; + +/** + * @author Alexander Weigl + * @version 1 (13.10.23) + */ +public record StrategyOptions( + String method, + String dep, + String query, + String nonLinArith, + String stopMode, + int maxSteps) implements KeYDataTransferObject { + public static StrategyOptions defaultOptions() { + return new StrategyOptions( + "METHOD_CONTRACT", + "DEP_ON", + "QUERY_ON", + "NON_LIN_ARITH_DEF_OPS", + "STOPMODE_NONCLOSE", + 1000); + } + + public static StrategyOptions from(StrategySettings settings) { + var sp = settings.getActiveStrategyProperties(); + return new StrategyOptions( + sp.getProperty(StrategyProperties.METHOD_OPTIONS_KEY), + sp.getProperty(StrategyProperties.DEP_OPTIONS_KEY), + sp.getProperty(StrategyProperties.QUERY_OPTIONS_KEY), + sp.getProperty(StrategyProperties.NON_LIN_ARITH_OPTIONS_KEY), + sp.getProperty(StrategyProperties.STOPMODE_OPTIONS_KEY), + settings.getMaxSteps()); + } + + private String getVal(String key) { + Field f = null; + try { + f = StrategyProperties.class.getField(key); + } catch (NoSuchFieldException e) { + throw new RuntimeException("Unknown key: " + key); + } + Class t = f.getType(); + if (t == String.class) { + try { + return (String) f.get(this); + } catch (IllegalAccessException e) { + throw new RuntimeException("Cannot access field: " + key); + } + } else { + throw new RuntimeException("Type mismatch: " + t); + } + } + + public void configure(Proof proof) { + var defaultOptions = defaultOptions(); + StrategyProperties sp = proof.getSettings().getStrategySettings() + .getActiveStrategyProperties(); + if (method != null) { + sp.setProperty(StrategyProperties.METHOD_OPTIONS_KEY, getVal(method)); + } else { + sp.setProperty(StrategyProperties.METHOD_OPTIONS_KEY, defaultOptions.method()); + } + if (dep != null) { + sp.setProperty(StrategyProperties.DEP_OPTIONS_KEY, getVal(dep)); + } else { + sp.setProperty(StrategyProperties.DEP_OPTIONS_KEY, defaultOptions.dep()); + } + if (query != null) { + sp.setProperty(StrategyProperties.QUERY_OPTIONS_KEY, getVal(query)); + } else { + sp.setProperty(StrategyProperties.QUERY_OPTIONS_KEY, defaultOptions.query()); + } + if (nonLinArith != null) { + sp.setProperty(StrategyProperties.NON_LIN_ARITH_OPTIONS_KEY, getVal(nonLinArith)); + } else { + sp.setProperty(StrategyProperties.NON_LIN_ARITH_OPTIONS_KEY, + defaultOptions.nonLinArith()); + } + if (stopMode != null) { + sp.setProperty(StrategyProperties.STOPMODE_OPTIONS_KEY, getVal(stopMode)); + } else { + sp.setProperty(StrategyProperties.STOPMODE_OPTIONS_KEY, defaultOptions.stopMode()); + } + proof.getSettings().getStrategySettings().setActiveStrategyProperties(sp); + proof.getSettings().getStrategySettings().setMaxSteps(maxSteps); + } +} diff --git a/keyext.api/src/main/java/org/keyproject/key/api/data/TaskFinishedInfo.java b/keyext.api/src/main/java/org/keyproject/key/api/data/TaskFinishedInfo.java new file mode 100644 index 00000000000..5a4042dd009 --- /dev/null +++ b/keyext.api/src/main/java/org/keyproject/key/api/data/TaskFinishedInfo.java @@ -0,0 +1,11 @@ +/* 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 org.keyproject.key.api.data; + +public record TaskFinishedInfo(long time, int appliedRules, int closedGoals) + implements KeYDataTransferObject { + public static TaskFinishedInfo from(org.key_project.prover.engine.TaskFinishedInfo info) { + return new TaskFinishedInfo(info.getTime(), info.getAppliedRules(), info.getClosedGoals()); + } +} diff --git a/keyext.api/src/main/java/org/keyproject/key/api/data/TaskStartedInfo.java b/keyext.api/src/main/java/org/keyproject/key/api/data/TaskStartedInfo.java new file mode 100644 index 00000000000..9ecd5757c85 --- /dev/null +++ b/keyext.api/src/main/java/org/keyproject/key/api/data/TaskStartedInfo.java @@ -0,0 +1,13 @@ +/* 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 org.keyproject.key.api.data; + +import org.key_project.prover.engine.TaskStartedInfo.TaskKind; + +public record TaskStartedInfo(String message, int size, TaskKind kind) + implements KeYDataTransferObject { + public static TaskStartedInfo from(org.key_project.prover.engine.TaskStartedInfo info) { + return new TaskStartedInfo(info.message(), info.size(), info.kind()); + } +} diff --git a/keyext.api/src/main/java/org/keyproject/key/api/data/TermActionDesc.java b/keyext.api/src/main/java/org/keyproject/key/api/data/TermActionDesc.java new file mode 100644 index 00000000000..10238c3adb7 --- /dev/null +++ b/keyext.api/src/main/java/org/keyproject/key/api/data/TermActionDesc.java @@ -0,0 +1,25 @@ +/* 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 org.keyproject.key.api.data; + +import org.keyproject.key.api.data.KeyIdentifications.TermActionId; + +/** + * This class represents an action that can be executed on a term. + * + * @param commandId Unique identification + * @param displayName A string to display to the user. + * @param description Long description of the action for the user. + * @param category A string identifying a category + * @param kind Kind of the action + * @author Alexander Weigl + * @version 1 (13.10.23) + */ +public record TermActionDesc( + TermActionId commandId, + String displayName, + String description, + String category, + TermActionKind kind) implements KeYDataTransferObject { +} diff --git a/keyext.api/src/main/java/org/keyproject/key/api/data/TermActionKind.java b/keyext.api/src/main/java/org/keyproject/key/api/data/TermActionKind.java new file mode 100644 index 00000000000..2b904481ff1 --- /dev/null +++ b/keyext.api/src/main/java/org/keyproject/key/api/data/TermActionKind.java @@ -0,0 +1,29 @@ +/* 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 org.keyproject.key.api.data; + +/** + * Possible kinds of an action applicable to position on a sequent. + * + * @author Alexander Weigl + * @version 1 (29.10.23) + */ +public enum TermActionKind implements KeYDataTransferObject { + /** + * Built-In Rule + */ + BuiltIn, + /** + * Proof Script + */ + Script, + /** + * Proof Macro + */ + Macro, + /** + * Taclet + */ + Taclet +} diff --git a/keyext.api/src/main/java/org/keyproject/key/api/data/TextRange.java b/keyext.api/src/main/java/org/keyproject/key/api/data/TextRange.java new file mode 100644 index 00000000000..4e4ad0aecab --- /dev/null +++ b/keyext.api/src/main/java/org/keyproject/key/api/data/TextRange.java @@ -0,0 +1,13 @@ +/* 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 org.keyproject.key.api.data; + +/** + * TextRange specifies a range of integer numbers e.g. character positions. + * + * @param start this range's (included) start position. + * @param end this range's (excluded) end position. + */ +public record TextRange(int start, int end) implements KeYDataTransferObject { +} diff --git a/keyext.api/src/main/java/org/keyproject/key/api/data/TraceValue.java b/keyext.api/src/main/java/org/keyproject/key/api/data/TraceValue.java new file mode 100644 index 00000000000..45ba6db4862 --- /dev/null +++ b/keyext.api/src/main/java/org/keyproject/key/api/data/TraceValue.java @@ -0,0 +1,34 @@ +/* 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 org.keyproject.key.api.data; + +public enum TraceValue implements KeYDataTransferObject { + /** + * + */ + Off, + /** + * An error message. + */ + Error, + /** + * A warning message. + */ + Warning, + /** + * An information message. + */ + Info, + /** + * A log message. + */ + Log, + /** + * A debug message. + * + * @proposed + * @since 3.18.0 + */ + Debug +} diff --git a/keyext.api/src/main/java/org/keyproject/key/api/data/TreeNodeDesc.java b/keyext.api/src/main/java/org/keyproject/key/api/data/TreeNodeDesc.java new file mode 100644 index 00000000000..04f90c009cc --- /dev/null +++ b/keyext.api/src/main/java/org/keyproject/key/api/data/TreeNodeDesc.java @@ -0,0 +1,19 @@ +/* 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 org.keyproject.key.api.data; + +import de.uka.ilkd.key.proof.Node; + + +/** + * @author Alexander Weigl + * @version 1 (13.10.23) + */ +public record TreeNodeDesc(KeyIdentifications.NodeId id, String name) + implements KeYDataTransferObject { + public static TreeNodeDesc from(KeyIdentifications.ProofId proofId, Node root) { + return new TreeNodeDesc(new KeyIdentifications.NodeId(proofId, "" + root.serialNr()), + root.name()); + } +} diff --git a/keyext.api/src/main/java/org/keyproject/key/api/data/Uri.java b/keyext.api/src/main/java/org/keyproject/key/api/data/Uri.java new file mode 100644 index 00000000000..87319c422fa --- /dev/null +++ b/keyext.api/src/main/java/org/keyproject/key/api/data/Uri.java @@ -0,0 +1,50 @@ +/* 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 org.keyproject.key.api.data; + +import java.io.File; +import java.lang.reflect.Type; +import java.nio.file.Path; +import java.nio.file.Paths; + +import com.google.gson.*; +import org.jspecify.annotations.Nullable; + +/** + * Value class of a uniform resource identifier + * + * @author Alexander Weigl + * @version 1 (11/30/25) + */ +public record Uri(String uri) { + public static @Nullable Uri from(File sel) { + return new Uri(sel.toURI().toString()); + } + + public Path asPath() { + if (uri.startsWith("file://")) { + return Paths.get(uri.substring("file://".length())); + } + + try { + return Paths.get(uri); + } catch (Exception ignored) { + throw new RuntimeException("Illegal file URI"); + } + } + + public static class UriSerializer implements JsonSerializer, JsonDeserializer { + @Override + public Uri deserialize(JsonElement jsonElement, Type type, + JsonDeserializationContext jsonDeserializationContext) throws JsonParseException { + return new Uri(jsonElement.getAsString()); + } + + @Override + public JsonElement serialize(Uri uri, Type type, + JsonSerializationContext jsonSerializationContext) { + return jsonSerializationContext.serialize(uri); + } + } +} diff --git a/keyext.api/src/main/java/org/keyproject/key/api/data/package-info.java b/keyext.api/src/main/java/org/keyproject/key/api/data/package-info.java new file mode 100644 index 00000000000..39ecb9745a4 --- /dev/null +++ b/keyext.api/src/main/java/org/keyproject/key/api/data/package-info.java @@ -0,0 +1,8 @@ +/** + * @author Alexander Weigl + * @version 1 (20.10.24) + */ +@NullMarked +package org.keyproject.key.api.data; + +import org.jspecify.annotations.NullMarked; diff --git a/keyext.api/src/main/java/org/keyproject/key/api/package-info.java b/keyext.api/src/main/java/org/keyproject/key/api/package-info.java new file mode 100644 index 00000000000..c979030e065 --- /dev/null +++ b/keyext.api/src/main/java/org/keyproject/key/api/package-info.java @@ -0,0 +1,8 @@ +/** + * @author Alexander Weigl + * @version 1 (20.10.24) + */ +@NullMarked +package org.keyproject.key.api; + +import org.jspecify.annotations.NullMarked; diff --git a/keyext.api/src/main/java/org/keyproject/key/api/remoteapi/EnvApi.java b/keyext.api/src/main/java/org/keyproject/key/api/remoteapi/EnvApi.java new file mode 100644 index 00000000000..6f2beb69fc5 --- /dev/null +++ b/keyext.api/src/main/java/org/keyproject/key/api/remoteapi/EnvApi.java @@ -0,0 +1,75 @@ +/* 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 org.keyproject.key.api.remoteapi; + +import java.util.List; +import java.util.concurrent.CompletableFuture; + +import org.eclipse.lsp4j.jsonrpc.services.JsonRequest; +import org.eclipse.lsp4j.jsonrpc.services.JsonSegment; +import org.keyproject.key.api.data.ContractDesc; +import org.keyproject.key.api.data.FunctionDesc; +import org.keyproject.key.api.data.KeyIdentifications.*; +import org.keyproject.key.api.data.SortDesc; + +/** + * The management (retrieval functions) of proof environments. + * Using the following functions, you can obtain information of defined signature (sorts, functions, + * etc.) + * of an environment. + * + * @author Alexander Weigl + * @version 1 (13.10.23) + */ +@JsonSegment("env") +public interface EnvApi { + + /** + * A possible empty list of defined sorts in the environment. + * + * @param env a handle to the environment + * @return a list of {@link SortDesc} + */ + @JsonRequest + CompletableFuture> sorts(EnvironmentId env); + + /** + * A possible empty list of defined functions in the environment. + * + * @param env a handle to the environment + * @return a list of {@link FunctionDesc} + */ + @JsonRequest + CompletableFuture> functions(EnvironmentId env); + + /** + * A possible empty list of defined contracts in the environment. + * + * @param env a handle to the environment + * @return a list of {@link ContractDesc} + */ + @JsonRequest + CompletableFuture> contracts(EnvironmentId env); + + /** + * Starts a proof given by the contract handle. + * + * @param contractId a handle to the environment + * @return a handle to a proof encoded as an {@link ProofId} + */ + @JsonRequest + CompletableFuture openContract(ContractId contractId); + + /** + * This method frees the memory and datastructure of the given environment {@code env}. + *

+ * After calling this method, you are not allowed t use the environment or any proof inside this + * environment anymore. + * + * @param env a handle to the environment + * @return true if the environment was dispose. + */ + @JsonRequest + CompletableFuture dispose(EnvironmentId env); +} diff --git a/keyext.api/src/main/java/org/keyproject/key/api/remoteapi/ExampleApi.java b/keyext.api/src/main/java/org/keyproject/key/api/remoteapi/ExampleApi.java new file mode 100644 index 00000000000..e1cf96053eb --- /dev/null +++ b/keyext.api/src/main/java/org/keyproject/key/api/remoteapi/ExampleApi.java @@ -0,0 +1,38 @@ +/* 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 org.keyproject.key.api.remoteapi; + +import java.util.List; +import java.util.concurrent.CompletableFuture; + +import org.eclipse.lsp4j.jsonrpc.services.JsonRequest; +import org.eclipse.lsp4j.jsonrpc.services.JsonSegment; +import org.keyproject.key.api.data.ExampleDesc; +import org.keyproject.key.api.data.KeyIdentifications; + +/** + * Management of the built-in examples of KeY. + * + * @author weigl + */ +@JsonSegment("examples") +public interface ExampleApi { + /** + * A list of examples that are built-in into KeY. + * + * @return a list of examples descriptions + */ + @JsonRequest("list") + CompletableFuture> examples(); + + /** + * I am not sure whether this is helpful. Mainly a feature for testing?! + * + * @param name of the example + * @return opens a new proof returns a handle + * @see ExampleDesc#name() + */ + @JsonRequest + CompletableFuture loadExample(String name); +} diff --git a/keyext.api/src/main/java/org/keyproject/key/api/remoteapi/GoalApi.java b/keyext.api/src/main/java/org/keyproject/key/api/remoteapi/GoalApi.java new file mode 100644 index 00000000000..6c93c433b93 --- /dev/null +++ b/keyext.api/src/main/java/org/keyproject/key/api/remoteapi/GoalApi.java @@ -0,0 +1,65 @@ +/* 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 org.keyproject.key.api.remoteapi; + +import java.util.List; +import java.util.concurrent.CompletableFuture; + +import org.eclipse.lsp4j.jsonrpc.services.JsonNotification; +import org.eclipse.lsp4j.jsonrpc.services.JsonRequest; +import org.eclipse.lsp4j.jsonrpc.services.JsonSegment; +import org.keyproject.key.api.data.KeyIdentifications.NodeId; +import org.keyproject.key.api.data.KeyIdentifications.NodeTextId; +import org.keyproject.key.api.data.KeyIdentifications.TermActionId; +import org.keyproject.key.api.data.NodeTextDesc; +import org.keyproject.key.api.data.PrintOptions; +import org.keyproject.key.api.data.TermActionDesc; + +/** + * Working with goals: This includes the applications of rules, macros and user interaction to + * sequents. + * + * @author Alexander Weigl + * @version 1 (13.10.23) + */ +@JsonSegment("goal") +public interface GoalApi { + /** + * Prints the sequent of the given node using the given {@code options}. + * + * @param id a handle of a node + * @param options printing options + * @return the printed sequent + */ + @JsonRequest + CompletableFuture print(NodeId id, PrintOptions options); + + /** + * Finds possible actions for the print-out given handle {@code id} and the + * textual positon {@code pos}. Caret position starts with 0. + * + * @param id handle + * @param caretPos position inside the print-out (0<= pos < text_length) + * @return a list of possible actions that can be invoked at the caret position. + */ + @JsonRequest + CompletableFuture> actions(NodeTextId id, int caretPos); + + /** + * Applies the given action identify by {@code id}. + * + * @param id a handle to a term action + * @return true + */ + @JsonRequest("apply_action") + CompletableFuture applyAction(TermActionId id); + + /** + * Frees the privious occupied print-out of a sequent. + * + * @param id + */ + @JsonNotification("free") + void freePrint(NodeTextId id); +} diff --git a/keyext.api/src/main/java/org/keyproject/key/api/remoteapi/KeyApi.java b/keyext.api/src/main/java/org/keyproject/key/api/remoteapi/KeyApi.java new file mode 100644 index 00000000000..4d4f168f3eb --- /dev/null +++ b/keyext.api/src/main/java/org/keyproject/key/api/remoteapi/KeyApi.java @@ -0,0 +1,18 @@ +/* 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 org.keyproject.key.api.remoteapi; + +/** + * The combined interface that is provided by KeY. + */ +public interface KeyApi extends + ExampleApi, + MetaApi, + ServerManagement, + ProofApi, + ProofTreeApi, + GoalApi, + EnvApi, + ProofLoadApi { +} diff --git a/keyext.api/src/main/java/org/keyproject/key/api/remoteapi/MetaApi.java b/keyext.api/src/main/java/org/keyproject/key/api/remoteapi/MetaApi.java new file mode 100644 index 00000000000..252008f0b81 --- /dev/null +++ b/keyext.api/src/main/java/org/keyproject/key/api/remoteapi/MetaApi.java @@ -0,0 +1,39 @@ +/* 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 org.keyproject.key.api.remoteapi; + +import java.util.List; +import java.util.concurrent.CompletableFuture; + +import org.eclipse.lsp4j.jsonrpc.services.JsonRequest; +import org.eclipse.lsp4j.jsonrpc.services.JsonSegment; +import org.keyproject.key.api.data.KeyIdentifications.*; +import org.keyproject.key.api.data.ProofMacroDesc; +import org.keyproject.key.api.data.ProofScriptCommandDesc; + +/** + * The meta segments provides functionalities around the KeY systems and environment. + */ +@JsonSegment("meta") +public interface MetaApi { + /** + * The current version string. + * + * @return version of KeY + */ + @JsonRequest("version") + CompletableFuture getVersion(); + + /** + * @return a list of available proof macros + */ + @JsonRequest("available_macros") + CompletableFuture> getAvailableMacros(); + + /** + * @return a list of available proof script commands + */ + @JsonRequest("available_script_commands") + CompletableFuture> getAvailableScriptCommands(); +} diff --git a/keyext.api/src/main/java/org/keyproject/key/api/remoteapi/ProofApi.java b/keyext.api/src/main/java/org/keyproject/key/api/remoteapi/ProofApi.java new file mode 100644 index 00000000000..2c4f76978ad --- /dev/null +++ b/keyext.api/src/main/java/org/keyproject/key/api/remoteapi/ProofApi.java @@ -0,0 +1,121 @@ +/* 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 org.keyproject.key.api.remoteapi; + +import java.util.List; +import java.util.concurrent.CompletableFuture; + +import org.eclipse.lsp4j.jsonrpc.services.JsonRequest; +import org.eclipse.lsp4j.jsonrpc.services.JsonSegment; +import org.keyproject.key.api.data.KeyIdentifications.*; +import org.keyproject.key.api.data.MacroStatistic; +import org.keyproject.key.api.data.NodeDesc; +import org.keyproject.key.api.data.ProofStatus; +import org.keyproject.key.api.data.StrategyOptions; + +/** + * + * @author Alexander Weigl + * @version 1 (13.10.23) + */ +@JsonSegment("proof") +public interface ProofApi { + /** + * + * @param proofId + * @return + */ + @JsonRequest + CompletableFuture root(ProofId proofId); + + /** + * Executes the given {@code script} against the proof using the given {@code options}. + * + * @param proof handle of a proof + * @param script proof script + * @param options options towards the proof strategy + * @return the run-time statistics + */ + @JsonRequest + CompletableFuture script(ProofId proof, String script, StrategyOptions options); + + /** + * Executes the macro given by {@code macroName} against the proof + * using the given {@code options}. + * + * @param proof handle of a proof + * @param macroName proof script + * @param options options towards the proof strategy + * @return the run-time statistics + */ + @JsonRequest + CompletableFuture macro(ProofId proof, String macroName, + StrategyOptions options); + + /** + * Auto against the proof + * + * @param proof handle of a proof + * @param options options towards the proof strategy + * @return + */ + @JsonRequest + CompletableFuture auto(ProofId proof, StrategyOptions options); + + /** + * Frees the resources occupied by the proof. + * + * @param proof + * @return + */ + @JsonRequest + CompletableFuture dispose(ProofId proof); + + /** + * + * @param proof + * @param onlyOpened + * @param onlyEnabled + * @return + */ + @JsonRequest + CompletableFuture> goals(ProofId proof, boolean onlyOpened, boolean onlyEnabled); + + /** + * + * @param proof + * @return + */ + @JsonRequest + CompletableFuture tree(ProofId proof); + + /** + * + * @param nodeId + * @return + */ + @JsonRequest + CompletableFuture> children(NodeId nodeId); + + /** + * Prunes the proof branch from the leafs to the given {@code nodeId}. + * + * @param nodeId + * @return + */ + @JsonRequest + CompletableFuture> pruneTo(NodeId nodeId); + + /** + * + * TODO + * + * @param proof + * @return + */ + @JsonRequest + default CompletableFuture statistics(ProofId proof) { + return CompletableFuture.completedFuture(null); + } +} diff --git a/keyext.api/src/main/java/org/keyproject/key/api/remoteapi/ProofLoadApi.java b/keyext.api/src/main/java/org/keyproject/key/api/remoteapi/ProofLoadApi.java new file mode 100644 index 00000000000..00e4c93cfc8 --- /dev/null +++ b/keyext.api/src/main/java/org/keyproject/key/api/remoteapi/ProofLoadApi.java @@ -0,0 +1,59 @@ +/* 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 org.keyproject.key.api.remoteapi; + +import java.util.concurrent.CompletableFuture; + +import de.uka.ilkd.key.proof.io.ProblemLoaderException; + +import org.eclipse.lsp4j.jsonrpc.messages.Either; +import org.eclipse.lsp4j.jsonrpc.services.JsonRequest; +import org.eclipse.lsp4j.jsonrpc.services.JsonSegment; +import org.keyproject.key.api.data.KeyIdentifications.EnvironmentId; +import org.keyproject.key.api.data.KeyIdentifications.ProofId; +import org.keyproject.key.api.data.LoadParams; +import org.keyproject.key.api.data.ProblemDefinition; + +/** + * Functionalities for loading proofs either from a built-in example, or from a set of files. + * + * @author Alexander Weigl + * @since v1 + */ +@JsonSegment("loading") +public interface ProofLoadApi { + + /** + * Do not use. Not implemented + * @param problem + * @return + */ + @JsonRequest + CompletableFuture loadProblem(ProblemDefinition problem); + + /** + * + * @param content + * @return + */ + @JsonRequest + CompletableFuture loadKey(String content); + + /** + * + * @param term + * @return + */ + @JsonRequest + CompletableFuture loadTerm(String term); + + /** + * @param params parameters for loading + * @return either an {@link EnvironmentId or a ProofId depending on the given params.} + * @throws ProblemLoaderException if something went wrong + */ + @JsonRequest + CompletableFuture> load(LoadParams params) + throws ProblemLoaderException; +} diff --git a/keyext.api/src/main/java/org/keyproject/key/api/remoteapi/ProofTreeApi.java b/keyext.api/src/main/java/org/keyproject/key/api/remoteapi/ProofTreeApi.java new file mode 100644 index 00000000000..6f0d14a2aed --- /dev/null +++ b/keyext.api/src/main/java/org/keyproject/key/api/remoteapi/ProofTreeApi.java @@ -0,0 +1,50 @@ +/* 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 org.keyproject.key.api.remoteapi; + +import java.util.List; +import java.util.concurrent.CompletableFuture; + +import org.eclipse.lsp4j.jsonrpc.services.JsonRequest; +import org.eclipse.lsp4j.jsonrpc.services.JsonSegment; +import org.keyproject.key.api.data.KeyIdentifications.ProofId; +import org.keyproject.key.api.data.KeyIdentifications.TreeNodeId; +import org.keyproject.key.api.data.TreeNodeDesc; + +/** + * Operations on the proof tree. + * + * @author Alexander Weigl + * @version 1 (13.10.23) + */ +@JsonSegment("proofTree") +public interface ProofTreeApi { + /** + * Returns the node root of the tree. + * + * @param id + * @return + */ + @JsonRequest("root") + CompletableFuture treeRoot(ProofId id); + + /** + * + * @param proof + * @param nodeId + * @return + */ + @JsonRequest("children") + CompletableFuture> treeChildren(ProofId proof, TreeNodeId nodeId); + + /** + * + * @param proof + * @param nodeId + * TODO param depth + * @return + */ + @JsonRequest("subtree") + CompletableFuture> treeSubtree(ProofId proof, TreeNodeId nodeId); +} diff --git a/keyext.api/src/main/java/org/keyproject/key/api/remoteapi/ServerManagement.java b/keyext.api/src/main/java/org/keyproject/key/api/remoteapi/ServerManagement.java new file mode 100644 index 00000000000..cb74dd5fb24 --- /dev/null +++ b/keyext.api/src/main/java/org/keyproject/key/api/remoteapi/ServerManagement.java @@ -0,0 +1,56 @@ +/* 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 org.keyproject.key.api.remoteapi; + +import java.util.concurrent.CompletableFuture; + +import org.eclipse.lsp4j.jsonrpc.services.JsonNotification; +import org.eclipse.lsp4j.jsonrpc.services.JsonRequest; +import org.eclipse.lsp4j.jsonrpc.services.JsonSegment; +import org.keyproject.key.api.data.TraceValue; + +/** + * This is a text and should appear in the documentation + * + * @author Alexander Weigl + * @version 1 (13.10.23) + */ +@JsonSegment("server") +public interface ServerManagement { + /** + * The shutdown request is sent from the client to the server. It asks the server to shut down, + * but to not exit (otherwise the response might not be delivered correctly to the client). + * There is a separate exit notification that asks the server to exit. Clients must not send any + * notifications other than exit or requests to a server to which they have sent a shutdown + * request. Clients should also wait with sending the exit notification until they have received + * a response from the shutdown request. + *

+ * If a server receives requests after a shutdown request those requests should error with + * InvalidRequest. + */ + @JsonRequest + CompletableFuture shutdown(); + + /** + * A notification to ask the server to exit its process. The server should exit with success + * code 0 if the shutdown request has been received before; otherwise with error code 1. + */ + @JsonNotification + void exit(); + + + /** + * Values + * + * @param value The new value that should be assigned to the trace setting. + */ + public record SetTraceParams(TraceValue value) { + } + + /** + * A notification that should be used by the client to modify the trace setting of the server. + */ + @JsonNotification + void setTrace(SetTraceParams params); +} diff --git a/keyext.api/src/main/java/org/keyproject/key/api/remoteapi/package-info.java b/keyext.api/src/main/java/org/keyproject/key/api/remoteapi/package-info.java new file mode 100644 index 00000000000..ccaca3e03b6 --- /dev/null +++ b/keyext.api/src/main/java/org/keyproject/key/api/remoteapi/package-info.java @@ -0,0 +1,8 @@ +/** + * @author Alexander Weigl + * @version 1 (20.10.24) + */ +@NullMarked +package org.keyproject.key.api.remoteapi; + +import org.jspecify.annotations.NullMarked; diff --git a/keyext.api/src/main/java/org/keyproject/key/api/remoteclient/ClientApi.java b/keyext.api/src/main/java/org/keyproject/key/api/remoteclient/ClientApi.java new file mode 100644 index 00000000000..198e4706b07 --- /dev/null +++ b/keyext.api/src/main/java/org/keyproject/key/api/remoteclient/ClientApi.java @@ -0,0 +1,91 @@ +/* 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 org.keyproject.key.api.remoteclient; + +import java.util.concurrent.CompletableFuture; +import javax.annotation.Nullable; + +import org.eclipse.lsp4j.jsonrpc.services.JsonNotification; +import org.eclipse.lsp4j.jsonrpc.services.JsonRequest; +import org.eclipse.lsp4j.jsonrpc.services.JsonSegment; +import org.jspecify.annotations.NullMarked; +import org.keyproject.key.api.data.TaskFinishedInfo; +import org.keyproject.key.api.data.TaskStartedInfo; + +/** + * This segment contains the functionalities that a client needs to implement. + * Mainly, it is logging and displaying of information. + */ +@JsonSegment("client") +@NullMarked +public interface ClientApi { + /** + * A notification to log the trace of the server’s execution. + * The amount and content of these notifications depends on the current trace configuration. + * If trace is 'off', the server should not send any logTrace notification. + * If trace is 'messages', the server should not add the 'verbose' field in the LogTraceParams. + *

+ * $/logTrace should be used for systematic trace reporting. For single debugging messages, the + * server should send window/logMessage notifications. + */ + @JsonNotification + void logTrace(LogTraceParams params); + + // region Window + + /** + * The show message notification is sent from a server to a client to ask the client to display + * a particular message in the user interface. + */ + @JsonNotification("showMessage") + void showMessage(ShowMessageParams params); + + /** + * The show message request is sent from a server to a client to ask the client to display a + * particular message in the user interface. In addition to the show message notification the + * request allows to pass actions and to wait for an answer from the client. + */ + @JsonRequest + @Nullable + CompletableFuture showMessageWithActions(ShowMessageRequestParams params); + + + /** + * The show document request is sent from a server to a client to ask the client to display a + * particular resource referenced by a URI in the user interface. + */ + @JsonRequest + CompletableFuture showDocument(ShowDocumentParams params); + + + /** + * Notifiation about the finishing of a task. + * + * @param info task information + */ + @JsonNotification + void taskFinished(TaskFinishedInfo info); + + /** + * Progress on the current task running + * + * @param position some integer + * @TODO weigl: This call is stupid w/o information of the task assigned. + * we also should send max value for showing a progress indicator, + * and a message. + */ + @JsonNotification + void taskProgress(int position); + + /** + * This call notifies the client that a task has been started. + * Task are started, mainly triggered by the client, for various reason, e.g., + * letting the macro run. + * + * @param info information about the task + */ + @JsonNotification + void taskStarted(TaskStartedInfo info); + // endregion +} diff --git a/keyext.api/src/main/java/org/keyproject/key/api/remoteclient/LogMessageParams.java b/keyext.api/src/main/java/org/keyproject/key/api/remoteclient/LogMessageParams.java new file mode 100644 index 00000000000..1fdf872b84d --- /dev/null +++ b/keyext.api/src/main/java/org/keyproject/key/api/remoteclient/LogMessageParams.java @@ -0,0 +1,12 @@ +/* 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 org.keyproject.key.api.remoteclient; + +/** + * @param type The message type. See {@link MessageType} + * @param message the actual message + */ +public record LogMessageParams(MessageType type, String message) { + +} diff --git a/keyext.api/src/main/java/org/keyproject/key/api/remoteclient/LogTraceParams.java b/keyext.api/src/main/java/org/keyproject/key/api/remoteclient/LogTraceParams.java new file mode 100644 index 00000000000..6dcb08fb585 --- /dev/null +++ b/keyext.api/src/main/java/org/keyproject/key/api/remoteclient/LogTraceParams.java @@ -0,0 +1,14 @@ +/* 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 org.keyproject.key.api.remoteclient; + +import org.eclipse.lsp4j.jsonrpc.validation.NonNull; + +/** + * @param message The message to be logged. + * @param level Additional information that can be computed if the `trace` configuration is set to + * `'verbose'` + */ +public record LogTraceParams(@NonNull String message, String level) { +} diff --git a/keyext.api/src/main/java/org/keyproject/key/api/remoteclient/MessageActionItem.java b/keyext.api/src/main/java/org/keyproject/key/api/remoteclient/MessageActionItem.java new file mode 100644 index 00000000000..c541125670e --- /dev/null +++ b/keyext.api/src/main/java/org/keyproject/key/api/remoteclient/MessageActionItem.java @@ -0,0 +1,10 @@ +/* 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 org.keyproject.key.api.remoteclient; + +/** + * @param title A short title like 'Retry', 'Open Log' etc. + */ +public record MessageActionItem(String title) { +} diff --git a/keyext.api/src/main/java/org/keyproject/key/api/remoteclient/MessageType.java b/keyext.api/src/main/java/org/keyproject/key/api/remoteclient/MessageType.java new file mode 100644 index 00000000000..8564f136f36 --- /dev/null +++ b/keyext.api/src/main/java/org/keyproject/key/api/remoteclient/MessageType.java @@ -0,0 +1,31 @@ +/* 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 org.keyproject.key.api.remoteclient; + +public enum MessageType { + Unused, + /** + * An error message. + */ + Error, + /** + * A warning message. + */ + Warning, + /** + * An information message. + */ + Info, + /** + * A log message. + */ + Log, + /** + * A debug message. + * + * @proposed + * @since 3.18.0 + */ + Debug +} diff --git a/keyext.api/src/main/java/org/keyproject/key/api/remoteclient/ShowDocumentParams.java b/keyext.api/src/main/java/org/keyproject/key/api/remoteclient/ShowDocumentParams.java new file mode 100644 index 00000000000..69491ca5398 --- /dev/null +++ b/keyext.api/src/main/java/org/keyproject/key/api/remoteclient/ShowDocumentParams.java @@ -0,0 +1,30 @@ +/* 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 org.keyproject.key.api.remoteclient; + +import org.jspecify.annotations.Nullable; +import org.keyproject.key.api.data.TextRange; + +/** + * Information to show a document on the client side. + * + * @param uri The uri to show. + * @param external Indicates to show the resource in an external program. + * To show, for example, `https://code.visualstudio.com/` + * in the default WEB browser set `external` to `true`. + * @param takeFocus An optional property to indicate whether the editor + * showing the document should take focus or not. + * Clients might ignore this property if an external + * program is started. + * @param selection An optional selection range if the document is a text + * document. Clients might ignore the property if an + * external program is started or the file is not a text + * file. + */ +public record ShowDocumentParams( + String uri, + boolean external, + boolean takeFocus, + @Nullable TextRange selection) { +} diff --git a/keyext.api/src/main/java/org/keyproject/key/api/remoteclient/ShowDocumentResult.java b/keyext.api/src/main/java/org/keyproject/key/api/remoteclient/ShowDocumentResult.java new file mode 100644 index 00000000000..85b3c24c21f --- /dev/null +++ b/keyext.api/src/main/java/org/keyproject/key/api/remoteclient/ShowDocumentResult.java @@ -0,0 +1,10 @@ +/* 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 org.keyproject.key.api.remoteclient; + +/** + * @param success A boolean indicating if the show was successful. + */ +public record ShowDocumentResult(boolean success) { +} diff --git a/keyext.api/src/main/java/org/keyproject/key/api/remoteclient/ShowMessageParams.java b/keyext.api/src/main/java/org/keyproject/key/api/remoteclient/ShowMessageParams.java new file mode 100644 index 00000000000..3ed56927c85 --- /dev/null +++ b/keyext.api/src/main/java/org/keyproject/key/api/remoteclient/ShowMessageParams.java @@ -0,0 +1,11 @@ +/* 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 org.keyproject.key.api.remoteclient; + +/** + * @param type The message type. See {@link MessageType}. + * @param message the actual message + */ +public record ShowMessageParams(MessageType type, String message) { +} diff --git a/keyext.api/src/main/java/org/keyproject/key/api/remoteclient/ShowMessageRequestParams.java b/keyext.api/src/main/java/org/keyproject/key/api/remoteclient/ShowMessageRequestParams.java new file mode 100644 index 00000000000..3f1c3e8be59 --- /dev/null +++ b/keyext.api/src/main/java/org/keyproject/key/api/remoteclient/ShowMessageRequestParams.java @@ -0,0 +1,14 @@ +/* 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 org.keyproject.key.api.remoteclient; + +import java.util.List; + +/** + * @param type The message type. See {@link MessageType}. + * @param message the actual message + */ +public record ShowMessageRequestParams( + MessageType type, String message, List actions) { +} diff --git a/keyext.api/src/main/java/org/keyproject/key/api/remoteclient/package-info.java b/keyext.api/src/main/java/org/keyproject/key/api/remoteclient/package-info.java new file mode 100644 index 00000000000..2151dd10601 --- /dev/null +++ b/keyext.api/src/main/java/org/keyproject/key/api/remoteclient/package-info.java @@ -0,0 +1,8 @@ +/** + * @author Alexander Weigl + * @version 1 (20.10.24) + */ +@NullMarked +package org.keyproject.key.api.remoteclient; + +import org.jspecify.annotations.NullMarked; diff --git a/keyext.api/src/main/resources/logback.xml b/keyext.api/src/main/resources/logback.xml new file mode 100644 index 00000000000..4957bda9dc6 --- /dev/null +++ b/keyext.api/src/main/resources/logback.xml @@ -0,0 +1,59 @@ + + + + + + + + + ${user.home}/.key/logs/key_${timestamp}.log + false + + UTF-8 + + %date|%level|%thread|%logger|%file:%line|%replace(%msg){'[\n\r]','\\n'}|%replace(%ex){'[\n\r]','\\n'}%nopex|%n + true + + + + + + [%date{HH:mm:ss.SSS}] %highlight(%-5level) %cyan(%logger{0}) - %msg%ex%n + + + + INFO + + + + + + + + + + + System.err + + [%relative] %highlight(%-5level) %cyan(%logger{0}): %msg %n + + + TRACE + + + + + + + + diff --git a/keyext.api/src/test/java/org/keyproject/key/api/SimpleClient.java b/keyext.api/src/test/java/org/keyproject/key/api/SimpleClient.java new file mode 100644 index 00000000000..3be5c910081 --- /dev/null +++ b/keyext.api/src/test/java/org/keyproject/key/api/SimpleClient.java @@ -0,0 +1,53 @@ +/* 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 org.keyproject.key.api; + +import java.util.concurrent.CompletableFuture; +import javax.annotation.Nullable; + +import org.jspecify.annotations.NullMarked; +import org.keyproject.key.api.data.TaskFinishedInfo; +import org.keyproject.key.api.data.TaskStartedInfo; +import org.keyproject.key.api.remoteclient.*; + +@NullMarked +class SimpleClient implements ClientApi { + + @Override + public void logTrace(LogTraceParams params) { + + } + + @Override + public void showMessage(ShowMessageParams params) { + + } + + @Nullable + @Override + public CompletableFuture showMessageWithActions( + ShowMessageRequestParams params) { + return null; + } + + @Override + public CompletableFuture showDocument(ShowDocumentParams params) { + return null; + } + + @Override + public void taskFinished(TaskFinishedInfo info) { + System.out.println(info); + } + + @Override + public void taskProgress(int position) { + + } + + @Override + public void taskStarted(TaskStartedInfo info) { + System.out.println(info); + } +} diff --git a/keyext.api/src/test/java/org/keyproject/key/api/TestRpc.java b/keyext.api/src/test/java/org/keyproject/key/api/TestRpc.java new file mode 100644 index 00000000000..9e7869bdfaa --- /dev/null +++ b/keyext.api/src/test/java/org/keyproject/key/api/TestRpc.java @@ -0,0 +1,84 @@ +/* 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 org.keyproject.key.api; + +import java.io.IOException; +import java.io.PipedInputStream; +import java.io.PipedOutputStream; +import java.io.PrintWriter; +import java.util.Collections; +import java.util.concurrent.ExecutionException; +import java.util.concurrent.Future; +import java.util.logging.Level; +import java.util.logging.Logger; + +import org.eclipse.lsp4j.jsonrpc.Launcher; +import org.eclipse.lsp4j.jsonrpc.json.StreamMessageProducer; +import org.junit.jupiter.api.AfterEach; +import org.junit.jupiter.api.BeforeEach; +import org.junit.jupiter.api.Test; +import org.keyproject.key.api.remoteapi.KeyApi; +import org.keyproject.key.api.remoteclient.ClientApi; + +public class TestRpc { + private Future clientListening, serverListening; + private KeyApi keyApi; + + @BeforeEach + void setup() throws IOException { + PipedInputStream inClient = new PipedInputStream(); + PipedOutputStream outClient = new PipedOutputStream(); + PipedInputStream inServer = new PipedInputStream(); + PipedOutputStream outServer = new PipedOutputStream(); + + inClient.connect(outServer); + outClient.connect(inServer); + + KeyApiImpl impl = new KeyApiImpl(); + Launcher serverLauncher = StartServer.launch(outServer, inServer, impl); + impl.setClientApi(serverLauncher.getRemoteProxy()); + + var client = new SimpleClient(); + Launcher clientLauncher = new Launcher.Builder() + .setLocalService(client) + .setRemoteInterfaces(Collections.singleton(KeyApi.class)) + .setInput(inClient) + .setOutput(outClient) + .configureGson(StartServer::configureJson) + .traceMessages(new PrintWriter(System.err)) + .create(); + + Logger logger = Logger.getLogger(StreamMessageProducer.class.getName()); + logger.setLevel(Level.SEVERE); + + clientListening = clientLauncher.startListening(); + serverListening = serverLauncher.startListening(); + + keyApi = clientLauncher.getRemoteProxy(); + } + + @AfterEach + void teardown() { + serverListening.cancel(true); + clientListening.cancel(true); + } + + + @Test + public void hello() { + + } + + @Test + public void listMacros() throws ExecutionException, InterruptedException { + var examples = keyApi.getAvailableMacros().get(); + System.out.println(examples); + } + + @Test + public void listExamples() throws ExecutionException, InterruptedException { + var examples = keyApi.examples().get(); + System.out.println(examples); + } +} diff --git a/keyext.caching/build.gradle b/keyext.caching/build.gradle index fc751b22881..62850b24cc2 100644 --- a/keyext.caching/build.gradle +++ b/keyext.caching/build.gradle @@ -3,6 +3,6 @@ description = "Caching of provable nodes to make proving with KeY faster." dependencies { implementation project(":key.core") implementation project(":key.ui") - implementation project(":keyext.slicing") + implementation "com.google.code.gson:gson:2.11.0" } \ No newline at end of file diff --git a/keyext.client.java/build.gradle b/keyext.client.java/build.gradle new file mode 100644 index 00000000000..50d4e4fcbc2 --- /dev/null +++ b/keyext.client.java/build.gradle @@ -0,0 +1,37 @@ +plugins { + id 'java' + id 'application' + id 'org.javamodularity.moduleplugin' version '1.8.12' + id 'org.openjfx.javafxplugin' version '0.1.0' +} + +repositories { + mavenCentral() +} + +tasks.withType(JavaCompile) { + options.encoding = 'UTF-8' +} + +application { + mainClass = 'edu.kit.iti.formal.keyextclientjava.Main' +} + +javafx { + version = "23.0.2" + modules = [ 'javafx.controls' ] +} + +dependencies { + implementation project(":keyext.api") + + implementation('org.controlsfx:controlsfx:11.2.1') + implementation('org.kordamp.ikonli:ikonli-javafx:12.3.1') + implementation('org.kordamp.ikonli:ikonli-fontawesome5-pack:12.3.1') + implementation('org.kordamp.bootstrapfx:bootstrapfx-core:0.4.0') + implementation('com.google.code.gson:gson:2.11.0') +} + +test { + useJUnitPlatform() +} \ No newline at end of file diff --git a/keyext.client.java/src/main/java/edu/kit/iti/formal/keyextclientjava/Main.java b/keyext.client.java/src/main/java/edu/kit/iti/formal/keyextclientjava/Main.java new file mode 100644 index 00000000000..1fb11b468d7 --- /dev/null +++ b/keyext.client.java/src/main/java/edu/kit/iti/formal/keyextclientjava/Main.java @@ -0,0 +1,27 @@ +/* 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 edu.kit.iti.formal.keyextclientjava; + +import java.io.IOException; +import javafx.application.Application; +import javafx.scene.Scene; +import javafx.scene.control.*; +import javafx.stage.Stage; + +public class Main { + public static class HelloApplication extends Application { + @Override + public void start(Stage stage) throws IOException { + Scene scene = new Scene(new MyKeyClient().root, 320, 240); + stage.setTitle("KeY Demo"); + stage.setScene(scene); + stage.show(); + } + + } + + public static void main(String[] args) { + Application.launch(HelloApplication.class, args); + } +} diff --git a/keyext.client.java/src/main/java/edu/kit/iti/formal/keyextclientjava/MyKeyClient.java b/keyext.client.java/src/main/java/edu/kit/iti/formal/keyextclientjava/MyKeyClient.java new file mode 100644 index 00000000000..c90fd8ec61c --- /dev/null +++ b/keyext.client.java/src/main/java/edu/kit/iti/formal/keyextclientjava/MyKeyClient.java @@ -0,0 +1,154 @@ +/* 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 edu.kit.iti.formal.keyextclientjava; + +import java.io.IOException; +import java.io.PipedInputStream; +import java.io.PipedOutputStream; +import java.io.PrintWriter; +import java.util.Collections; +import java.util.concurrent.CompletableFuture; +import java.util.concurrent.ExecutionException; +import java.util.logging.Level; +import java.util.logging.Logger; +import javafx.geometry.Orientation; +import javafx.scene.control.*; +import javafx.scene.layout.BorderPane; +import javafx.stage.FileChooser; + +import de.uka.ilkd.key.proof.io.ProblemLoaderException; + +import edu.kit.iti.formal.keyextclientjava.rpc.KeyRemote; +import edu.kit.iti.formal.keyextclientjava.rpc.RPCLayer; +import org.eclipse.lsp4j.jsonrpc.Launcher; +import org.eclipse.lsp4j.jsonrpc.json.StreamMessageProducer; +import org.jspecify.annotations.NullMarked; +import org.keyproject.key.api.KeyApiImpl; +import org.keyproject.key.api.StartServer; +import org.keyproject.key.api.data.*; +import org.keyproject.key.api.remoteapi.KeyApi; +import org.keyproject.key.api.remoteclient.*; +import org.kordamp.ikonli.fontawesome5.FontAwesomeRegular; +import org.kordamp.ikonli.javafx.FontIcon; + +@NullMarked +public class MyKeyClient { + public static final String JAR_FILE = ""; + private final ToolBar toolbar = new ToolBar(); + private final Label txtStatus = new Label("Yeah!"); + public final BorderPane root = new BorderPane(); + private final TreeView tnid = new TreeView<>(); + private final TextArea txtSequentView = new TextArea(); + + private final FileChooser fc = new FileChooser(); + private final KeyApi keyApi; + private KeyIdentifications.ProofId loadedProof; + + public MyKeyClient() throws IOException { + // region toolbar + var btnOpen = new Button("Open", new FontIcon(FontAwesomeRegular.FOLDER_OPEN)); + btnOpen.setOnAction(actionEvent -> openFile()); + toolbar.getItems().setAll(btnOpen, new Separator(Orientation.VERTICAL)); + // endregion + + var splitCenter = new SplitPane(tnid, txtSequentView); + splitCenter.setDividerPositions(.2); + root.setTop(toolbar); + root.setCenter(splitCenter); + root.setBottom(txtStatus); + + // var startKey = ForkJoinPool.commonPool().submit(this::startKey); + + PipedInputStream inClient = new PipedInputStream(); + PipedOutputStream outClient = new PipedOutputStream(); + PipedInputStream inServer = new PipedInputStream(); + PipedOutputStream outServer = new PipedOutputStream(); + + inClient.connect(outServer); + outClient.connect(inServer); + + KeyApiImpl impl = new KeyApiImpl(); + Launcher serverLauncher = StartServer.launch(outServer, inServer, impl); + impl.setClientApi(serverLauncher.getRemoteProxy()); + + var client = new SimpleClient(); + Launcher clientLauncher = new Launcher.Builder() + .setLocalService(client) + .setRemoteInterfaces(Collections.singleton(KeyApi.class)) + .setInput(inClient) + .setOutput(outClient) + .configureGson(StartServer::configureJson) + .traceMessages(new PrintWriter(System.err)) + .create(); + + Logger logger = Logger.getLogger(StreamMessageProducer.class.getName()); + logger.setLevel(Level.SEVERE); + + clientLauncher.startListening(); + serverLauncher.startListening(); + + this.keyApi = clientLauncher.getRemoteProxy(); + } + + private Object startKey() throws IOException { + return new KeyRemote(RPCLayer.startWithCLI(JAR_FILE)); + } + + private void openFile() { + var sel = fc.showOpenDialog(null); + if (sel != null) { + try { + loadedProof = keyApi.load( + new LoadParams(Uri.from(sel), null, null, null)) + .get().getRight(); + var root = keyApi.root(loadedProof).get(); + var sequent = + keyApi.print(root.nodeid(), new PrintOptions(true, 80, 4, true, false)) + .get(); + txtSequentView.setText(sequent.result()); + } catch (ProblemLoaderException | ExecutionException | InterruptedException e) { + throw new RuntimeException(e); + } + } + } + + @NullMarked + private static class SimpleClient implements ClientApi { + @Override + public void logTrace(LogTraceParams params) { + + } + + @Override + public void showMessage(ShowMessageParams params) { + + } + + @Override + public CompletableFuture showMessageWithActions( + ShowMessageRequestParams params) { + return null; + } + + @Override + public CompletableFuture showDocument(ShowDocumentParams params) { + return null; + } + + @Override + public void taskFinished(TaskFinishedInfo info) { + + } + + @Override + public void taskProgress(int position) { + + } + + @Override + public void taskStarted(TaskStartedInfo info) { + + } + } +} diff --git a/keyext.client.java/src/main/java/edu/kit/iti/formal/keyextclientjava/rpc/JsonRPC.java b/keyext.client.java/src/main/java/edu/kit/iti/formal/keyextclientjava/rpc/JsonRPC.java new file mode 100644 index 00000000000..adb642c758c --- /dev/null +++ b/keyext.client.java/src/main/java/edu/kit/iti/formal/keyextclientjava/rpc/JsonRPC.java @@ -0,0 +1,107 @@ +/* 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 edu.kit.iti.formal.keyextclientjava.rpc; + +import com.google.gson.Gson; +import com.google.gson.JsonArray; +import com.google.gson.JsonElement; +import com.google.gson.JsonObject; +import org.jspecify.annotations.Nullable; + +/** + * @author Alexander Weigl + * @version 1 (24.11.24) + */ +public class JsonRPC { + public static final String CONTENT_LENGTH = "Content-Length:"; + private static final Gson gson = new Gson(); + + public static String createNotification(String method, Object... args) { + return createRequest(null, method, args); + } + + public static String createRequest(@Nullable String id, String method, Object... args) { + JsonArray params = gson.toJsonTree(args).getAsJsonArray(); + return createRequest(id, method, params); + } + + public static String createRequest(@Nullable String id, String method, JsonArray params) { + var jsonObject = new JsonObject(); + jsonObject.addProperty("jsonrpc", "2.0"); + if (id != null) { + jsonObject.addProperty("id", id); + } + + jsonObject.addProperty("method", method); + jsonObject.add("params", params); + + return jsonObject.toString(); + } + + public static String createResponse(String id, Object result) { + return createResponse(id, gson.toJsonTree(result), null); + } + + public static String createErrorReponse(String id, int code, String message, + @Nullable Object data) { + return createResponse(id, null, createError(code, message, data)); + } + + public static String createResponse(String id, @Nullable JsonElement result, + @Nullable JsonObject error) { + if (result != null && error != null) { + throw new IllegalArgumentException("result and error at the same time is invalid"); + } + + if (!(result != null || error != null)) { + throw new IllegalArgumentException("at least one of result and error must be not null"); + } + + var jsonObject = new JsonObject(); + jsonObject.addProperty("jsonrpc", "2.0"); + jsonObject.addProperty("id", id); + + if (result != null) { + jsonObject.add("result", result); + } + if (error != null) { + jsonObject.add("error", error); + } + + return jsonObject.toString(); + } + + /** + * 5.1 Error object + * When a rpc call encounters an error, the Response Object MUST contain the error member with a + * value that is a Object with the following members: + *

+ * code + * A Number that indicates the error type that occurred. + * This MUST be an integer. + * message + * A String providing a short description of the error. + * The message SHOULD be limited to a concise single sentence. + * data + * A Primitive or Structured value that contains additional information about the error. + * This may be omitted. + * The value of this member is defined by the Server (e.g. detailed error information, nested + * errors etc.). + * + * @return + */ + public static JsonObject createError(int code, String message, @Nullable Object data) { + var jsonObject = new JsonObject(); + jsonObject.addProperty("code", code); + jsonObject.addProperty("message", message); + if (data != null) { + jsonObject.add("data", gson.toJsonTree(data)); + } + return jsonObject; + } + + public static String addHeader(String response) { + return "%s %d\r\n\r\n%s\r\n".formatted(CONTENT_LENGTH, response.length(), response); + } +} diff --git a/keyext.client.java/src/main/java/edu/kit/iti/formal/keyextclientjava/rpc/KeyRemote.java b/keyext.client.java/src/main/java/edu/kit/iti/formal/keyextclientjava/rpc/KeyRemote.java new file mode 100644 index 00000000000..71c49088273 --- /dev/null +++ b/keyext.client.java/src/main/java/edu/kit/iti/formal/keyextclientjava/rpc/KeyRemote.java @@ -0,0 +1,22 @@ +/* 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 edu.kit.iti.formal.keyextclientjava.rpc; + + +/** + * @author Alexander Weigl + * @version 1 (22.11.24) + */ +public class KeyRemote { + private final RPCLayer layer; + + public KeyRemote(RPCLayer rpcLayer) { + this.layer = rpcLayer; + } + + public String meta_version() { + final var obj = layer.callSync("meta/version"); + return obj.get("result").getAsString(); + } +} diff --git a/keyext.client.java/src/main/java/edu/kit/iti/formal/keyextclientjava/rpc/RPCLayer.java b/keyext.client.java/src/main/java/edu/kit/iti/formal/keyextclientjava/rpc/RPCLayer.java new file mode 100644 index 00000000000..569b8a091f9 --- /dev/null +++ b/keyext.client.java/src/main/java/edu/kit/iti/formal/keyextclientjava/rpc/RPCLayer.java @@ -0,0 +1,258 @@ +/* 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 edu.kit.iti.formal.keyextclientjava.rpc; + +import java.io.*; +import java.util.concurrent.*; +import java.util.concurrent.atomic.AtomicInteger; + +import com.google.gson.JsonObject; +import com.google.gson.JsonParser; +import org.jspecify.annotations.Nullable; + +/** + * @author Alexander Weigl + * @version 1 (22.11.24) + */ +public final class RPCLayer { + private final BufferedReader incoming; + private final Writer outgoing; + + private @Nullable Thread threadListener; + private @Nullable Thread threadMessageHandling; + + private final ConcurrentHashMap waiting = new ConcurrentHashMap<>(); + public final ArrayBlockingQueue incomingMessages = new ArrayBlockingQueue<>(16); + + private final AtomicInteger idCounter = new AtomicInteger(); + + + public RPCLayer(Reader incoming, Writer outgoing) { + this.incoming = new BufferedReader(incoming); + this.outgoing = outgoing; + } + + public static RPCLayer startWithCLI(String jarFile) throws IOException { + var pbuilder = new ProcessBuilder("java", "-jar", jarFile); + var p = pbuilder.start(); + var incoming = new InputStreamReader(p.getInputStream()); + var outgoing = new OutputStreamWriter(p.getOutputStream()); + return new RPCLayer(incoming, outgoing); + } + + public JsonObject waitForResponse(String id) throws InterruptedException, ExecutionException { + var cond = waiting.get(id); + var r = cond.get(); + waiting.remove(id); + return r; + } + + public JsonObject callSync(String methodName, Object... args) { + var id = nextId(); + waiting.put(id, new SimpleFuture()); + try { + sendAsync(id, methodName, args); + var response = waitForResponse(id); + return handleError(response); + } catch (InterruptedException | IOException | ExecutionException e) { + throw new RuntimeException(e); + } + } + + private JsonObject handleError(JsonObject response) { + if (response.get("error") != null) { + throw new RuntimeException("Request did not succeed " + response.get("error")); + } + return response; + } + + public void callAsync(String methodName, Object... args) throws IOException { + var id = nextId(); + sendAsync(id, methodName, args); + } + + private String nextId() { + return "" + idCounter.getAndIncrement(); + } + + private void sendAsync(String id, String methodName, Object[] args) throws IOException { + var json = JsonRPC.createRequest(id, methodName, args); + final var str = JsonRPC.addHeader(json); + outgoing.write(str); + outgoing.flush(); + } + + public void start() { + threadListener = + new Thread(new JsonStreamListener(incoming, incomingMessages), "JSON Message Reader"); + threadMessageHandling = new Thread(this::handler, "JSON Message Handler"); + threadListener.start(); + threadMessageHandling.start(); + } + + private void handler() { + try { + while (true) { + var obj = incomingMessages.poll(1, TimeUnit.MINUTES); + if (obj == null) { + continue; + } + if (obj.get("id") != null) { + var id = obj.get("id").getAsString(); + var syncObj = waiting.get(id); + syncObj.put(obj); + } else { + // TODO handle notification + System.out.println("Notification received"); + System.out.println(obj); + } + } + } catch (InterruptedException ignored) { + } + } + + public void dispose() { + if (threadListener != null) { + threadListener.interrupt(); + } + } + + public static class JsonStreamListener implements Runnable { + private final char[] CLENGTH = (JsonRPC.CONTENT_LENGTH + " ").toCharArray(); + private final PushbackReader incoming; + private final ArrayBlockingQueue incomingMessageQueue; + /** + * Internal buffer for reading efficient. + */ + private char[] buf = new char[4 * 1024]; + + public JsonStreamListener(Reader incoming, ArrayBlockingQueue queue) { + this.incoming = new PushbackReader(new BufferedReader(incoming)); // ensure bufferness + this.incomingMessageQueue = queue; + } + + @Override + public void run() { + try { + while (true) { + final var message = readMessage(); + if (message == null) + break; + final var jsonObject = JsonParser.parseString(message).getAsJsonObject(); + incomingMessageQueue.add(jsonObject); + } + } catch (IOException e) { + throw new RuntimeException(e); + } + } + + protected void processIncomingMessage(String message) { + + } + + + public @Nullable String readMessage() throws IOException { + expectedContentLength(); + final var len = readLength() + 2; // also read \r\n, + + if (len == 2) {// EOF reached + return null; + } + + if (buf.length <= len) { // reallocate more if necessary + buf = new char[len]; + } + + int count = incoming.read(buf, 0, len); + assert count == len; + consumeCRNL(); + return new String(buf, 0, count).trim(); + } + + private int readLength() throws IOException { + int c; + int len = 0; + do { + c = incoming.read(); + // if (Character.isWhitespace(c)) continue; + if (c == -1) + return 0; + if (c == '\r' || c == '\n') + break; + if (Character.isDigit(c)) { + len = len * 10 + c - '0'; + } else { + throw new IllegalStateException("Expected: a digit, but got '%c'".formatted(c)); + } + } while (c != -1); + c = incoming.read(); // consume the '\n' + assert c == '\n'; + return len; + } + + private void expectedContentLength() throws IOException { + for (var e : CLENGTH) { + int c = incoming.read(); + if (c == -1) + return; + if (e != c) { + throw new IllegalStateException("Expected: '%c', but got '%c'".formatted(e, c)); + } + } + } + + private void consumeCRNL() throws IOException { + int c = incoming.read(); + if (c == '\r') { + c = incoming.read(); + assert c == '\n'; + } else { + incoming.unread(c); + } + } + } +} + + +class SimpleFuture implements Future { + private final CountDownLatch latch = new CountDownLatch(1); + private JsonObject value; + + @Override + public boolean cancel(boolean mayInterruptIfRunning) { + return false; + } + + @Override + public boolean isCancelled() { + return false; + } + + @Override + public boolean isDone() { + return value != null; + } + + @Override + public JsonObject get() throws InterruptedException, ExecutionException { + latch.await(); + return value; + } + + @Override + public JsonObject get(long timeout, TimeUnit unit) + throws InterruptedException, TimeoutException { + if (latch.await(timeout, unit)) { + return value; + } else { + throw new TimeoutException(); + } + } + + void put(JsonObject value) { + this.value = value; + latch.countDown(); + } + +} diff --git a/keyext.client.java/src/main/resources/edu/kit/iti/formal/keyextclientjava/hello-view.fxml b/keyext.client.java/src/main/resources/edu/kit/iti/formal/keyextclientjava/hello-view.fxml new file mode 100644 index 00000000000..982318240d9 --- /dev/null +++ b/keyext.client.java/src/main/resources/edu/kit/iti/formal/keyextclientjava/hello-view.fxml @@ -0,0 +1,16 @@ + + + + + + + + + + + + +