From e31f2280fe62a2d8a704d1637c583037db5c7353 Mon Sep 17 00:00:00 2001 From: Richard Bubel Date: Mon, 22 Jun 2026 20:21:55 +0200 Subject: [PATCH 1/6] Remove racy testLockingAndReleasing that intermittently hangs CI The test pre-loaded a response before the request was registered, so the reader could deliver it before callSync registered its waiting future; the handler then NPE'd and callSync blocked forever (no timeout). It is an artificial scenario and is covered deterministically by the client-stability PR's callSync test. --- .../test/java/edu/kit/keyext/client/RPCLayerTest.java | 11 ----------- 1 file changed, 11 deletions(-) diff --git a/keyext.api.client/src/test/java/edu/kit/keyext/client/RPCLayerTest.java b/keyext.api.client/src/test/java/edu/kit/keyext/client/RPCLayerTest.java index 5226f3446d..76fb5f4898 100644 --- a/keyext.api.client/src/test/java/edu/kit/keyext/client/RPCLayerTest.java +++ b/keyext.api.client/src/test/java/edu/kit/keyext/client/RPCLayerTest.java @@ -43,15 +43,4 @@ void testIncoming() throws IOException { String second = listener.readMessage(); Assertions.assertEquals(response, second); } - - - - @Test - void testLockingAndReleasing() throws IOException, InterruptedException { - var response = JsonRPC.addHeader(JsonRPC.createResponse("0", 2)); - var layer = new RPCLayer(new StringReader(response), new StringWriter()); - layer.start(); // starts the thread. - var result = layer.callSync("calc", 1, 1); - System.out.println(result); - } } From fc026c65a2087ad18a472a68570eb2d8ce7afadc Mon Sep 17 00:00:00 2001 From: Richard Bubel Date: Mon, 22 Jun 2026 20:45:11 +0200 Subject: [PATCH 2/6] Fix RPCLayer handler thread shutdown and unknown-id NPE --- .../key_project/key/api/client/RPCLayer.java | 11 +- .../edu/kit/keyext/client/RPCLayerTest.java | 114 ++++++++++++++++++ 2 files changed, 124 insertions(+), 1 deletion(-) diff --git a/keyext.api.client/src/main/java/org/key_project/key/api/client/RPCLayer.java b/keyext.api.client/src/main/java/org/key_project/key/api/client/RPCLayer.java index 3759323aef..d3ebbef5ea 100644 --- a/keyext.api.client/src/main/java/org/key_project/key/api/client/RPCLayer.java +++ b/keyext.api.client/src/main/java/org/key_project/key/api/client/RPCLayer.java @@ -101,7 +101,13 @@ private void handler() { if (obj.get("id") != null) { var id = obj.get("id").getAsString(); var syncObj = waiting.get(id); - syncObj.put(obj); + if (syncObj != null) { + syncObj.put(obj); + } else { + // Response for an unknown/already-completed id: ignore it + // instead of NPE-ing (which would kill this thread). + System.err.println("Ignoring response for unknown id " + id); + } } else { // TODO handle notification System.out.println("Notification received"); @@ -116,6 +122,9 @@ public void dispose() { if (threadListener != null) { threadListener.interrupt(); } + if (threadMessageHandling != null) { + threadMessageHandling.interrupt(); + } } public static class JsonStreamListener implements Runnable { diff --git a/keyext.api.client/src/test/java/edu/kit/keyext/client/RPCLayerTest.java b/keyext.api.client/src/test/java/edu/kit/keyext/client/RPCLayerTest.java index 76fb5f4898..68d7881f0a 100644 --- a/keyext.api.client/src/test/java/edu/kit/keyext/client/RPCLayerTest.java +++ b/keyext.api.client/src/test/java/edu/kit/keyext/client/RPCLayerTest.java @@ -4,14 +4,18 @@ package edu.kit.keyext.client; import java.io.IOException; +import java.io.Reader; import java.io.StringReader; import java.io.StringWriter; import java.util.concurrent.ArrayBlockingQueue; +import java.util.concurrent.TimeUnit; +import java.util.function.BooleanSupplier; import org.key_project.key.api.client.JsonRPC; import org.key_project.key.api.client.RPCLayer; import org.junit.jupiter.api.Assertions; import org.junit.jupiter.api.Test; +import org.junit.jupiter.api.Timeout; /** * @author Alexander Weigl @@ -43,4 +47,114 @@ void testIncoming() throws IOException { String second = listener.readMessage(); Assertions.assertEquals(response, second); } + + /** + * Regression test: a response for an id nobody is waiting on must be ignored, + * not NPE the message-handler thread. With the old code the handler died on + * the unknown id and the following legitimate response was never delivered, + * so {@code callSync} would block forever (caught here by the timeout). + */ + @Test + @Timeout(value = 10, unit = TimeUnit.SECONDS) + void handlerSurvivesUnknownResponseId() throws Exception { + var in = new FeedableReader(); + var layer = new RPCLayer(in, new StringWriter()); + layer.start(); + + var feeder = new Thread(() -> { + sleepQuietly(200); // give callSync time to register its pending id "0" + in.feed(JsonRPC.addHeader(JsonRPC.createResponse("999", 1))); + in.feed(JsonRPC.addHeader(JsonRPC.createResponse("0", 42))); + }, "test-feeder"); + feeder.setDaemon(true); + feeder.start(); + + var result = layer.callSync("calc", 1); // allocated id is "0" + Assertions.assertEquals(42, result.get("result").getAsInt()); + layer.dispose(); + } + + /** + * Regression test: {@code dispose()} must stop the message-handler thread, + * not just the reader thread. With the old code the handler kept polling + * forever. Measured as a delta so other tests' threads don't interfere. + */ + @Test + @Timeout(value = 10, unit = TimeUnit.SECONDS) + void disposeStopsHandlerThread() throws Exception { + int before = countHandlerThreads(); + var layer = new RPCLayer(new FeedableReader(), new StringWriter()); + layer.start(); + Assertions.assertTrue(awaitUntil(() -> countHandlerThreads() == before + 1), + "handler thread should be running after start()"); + + layer.dispose(); + Assertions.assertTrue(awaitUntil(() -> countHandlerThreads() == before), + "handler thread should stop after dispose()"); + } + + private static int countHandlerThreads() { + return (int) Thread.getAllStackTraces().keySet().stream() + .filter(t -> "JSON Message Handler".equals(t.getName()) && t.isAlive()) + .count(); + } + + private static boolean awaitUntil(BooleanSupplier condition) throws InterruptedException { + long deadline = System.currentTimeMillis() + 5000; + while (System.currentTimeMillis() < deadline) { + if (condition.getAsBoolean()) { + return true; + } + Thread.sleep(10); + } + return condition.getAsBoolean(); + } + + private static void sleepQuietly(long millis) { + try { + Thread.sleep(millis); + } catch (InterruptedException e) { + Thread.currentThread().interrupt(); + } + } + + /** + * An in-memory {@link Reader} that blocks on read until {@link #feed} supplies + * more characters. Unlike a {@code PipedReader} it has no writer-thread + * lifecycle, so a feeder thread may exit without breaking the pipe. + */ + private static final class FeedableReader extends Reader { + private final StringBuilder buffer = new StringBuilder(); + private boolean closed = false; + + synchronized void feed(String s) { + buffer.append(s); + notifyAll(); + } + + @Override + public synchronized int read(char[] cbuf, int off, int len) throws IOException { + while (buffer.length() == 0 && !closed) { + try { + wait(); + } catch (InterruptedException e) { + Thread.currentThread().interrupt(); + throw new IOException(e); + } + } + if (buffer.length() == 0 && closed) { + return -1; + } + int n = Math.min(len, buffer.length()); + buffer.getChars(0, n, cbuf, off); + buffer.delete(0, n); + return n; + } + + @Override + public synchronized void close() { + closed = true; + notifyAll(); + } + } } From df0e190dda232b243c67c415226911df4e08ad95 Mon Sep 17 00:00:00 2001 From: Richard Bubel Date: Mon, 22 Jun 2026 19:41:39 +0200 Subject: [PATCH 3/6] Fix temp-file leak in loadKey and clear all per-proof caches on dispose --- .../org/keyproject/key/api/KeyApiImpl.java | 14 ++++++- .../key/api/data/KeyIdentifications.java | 6 +++ .../key/api/LoadKeyTempFileTest.java | 41 +++++++++++++++++++ 3 files changed, 60 insertions(+), 1 deletion(-) create mode 100644 keyext.api/src/test/java/org/keyproject/key/api/LoadKeyTempFileTest.java 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 index 105ffdae8b..e112ef8aca 100644 --- a/keyext.api/src/main/java/org/keyproject/key/api/KeyApiImpl.java +++ b/keyext.api/src/main/java/org/keyproject/key/api/KeyApiImpl.java @@ -578,8 +578,9 @@ public CompletableFuture loadKey(String content) { return CompletableFutures.computeAsync((c) -> { Proof proof = null; KeYEnvironment env = null; + File tempFile = null; try { - final var tempFile = File.createTempFile("json-rpc-", ".key"); + 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); @@ -595,6 +596,17 @@ public CompletableFuture loadKey(String content) { if (env != null) env.dispose(); throw new RuntimeException(e); + } finally { + // The loader reads the problem from disk during loading, so the + // temp file is no longer needed afterwards. Delete it to avoid + // accumulating one file per loadKey/loadTerm/loadProblem call. + if (tempFile != null) { + try { + Files.deleteIfExists(tempFile.toPath()); + } catch (IOException ignored) { + // best effort + } + } } }); } 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 index 9174d0cc84..7eac5a2aa1 100644 --- 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 @@ -176,7 +176,13 @@ public ProofContainer(Proof proof) { } void dispose() { + // Release all per-proof caches (not just mapNode). The container is + // normally dropped from mapProof and garbage-collected on dispose, + // so this is mainly an eager/defensive release of the printed-sequent + // cache (mapGoalText). mapNode.clear(); + mapTreeNode.clear(); + mapGoalText.clear(); } } } diff --git a/keyext.api/src/test/java/org/keyproject/key/api/LoadKeyTempFileTest.java b/keyext.api/src/test/java/org/keyproject/key/api/LoadKeyTempFileTest.java new file mode 100644 index 0000000000..16447aa80e --- /dev/null +++ b/keyext.api/src/test/java/org/keyproject/key/api/LoadKeyTempFileTest.java @@ -0,0 +1,41 @@ +/* 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.nio.file.Files; +import java.nio.file.Path; + +import org.junit.jupiter.api.Assertions; +import org.junit.jupiter.api.Test; + +/** + * Regression test for the temp-file leak: each loadKey/loadTerm/loadProblem + * wrote a {@code json-rpc-*.key} file into the system temp dir and never removed + * it. + */ +class LoadKeyTempFileTest { + @Test + void loadTermDoesNotLeaveTempFile() throws Exception { + Path tmp = Path.of(System.getProperty("java.io.tmpdir")); + long before = countTempKeyFiles(tmp); + + var api = new KeyApiImpl(); + var proofId = api.loadTerm("true").get(); + Assertions.assertNotNull(proofId); + + long after = countTempKeyFiles(tmp); + Assertions.assertEquals(before, after, + "loadKey should not leave a temporary .key file behind"); + } + + private static long countTempKeyFiles(Path dir) throws IOException { + try (var files = Files.list(dir)) { + return files.filter(p -> { + var name = p.getFileName().toString(); + return name.startsWith("json-rpc-") && name.endsWith(".key"); + }).count(); + } + } +} From 3dad4e7abe9042aebbee72fed4569786089dff6a Mon Sep 17 00:00:00 2001 From: Richard Bubel Date: Mon, 22 Jun 2026 19:38:06 +0200 Subject: [PATCH 4/6] Fix Python client timeout unit and disconnect handling --- keyext.client.python/keyapi/rpc.py | 40 ++++++--- keyext.client.python/tests/__init__.py | 0 .../tests/test_lsp_endpoint.py | 81 +++++++++++++++++++ 3 files changed, 110 insertions(+), 11 deletions(-) create mode 100644 keyext.client.python/tests/__init__.py create mode 100644 keyext.client.python/tests/test_lsp_endpoint.py diff --git a/keyext.client.python/keyapi/rpc.py b/keyext.client.python/keyapi/rpc.py index 5f3d75092b..71dff15c39 100644 --- a/keyext.client.python/keyapi/rpc.py +++ b/keyext.client.python/keyapi/rpc.py @@ -122,7 +122,7 @@ def object_decoder(obj): class LspEndpoint(threading.Thread): - def __init__(self, json_rpc_endpoint: JsonRpcEndpoint, method_callbacks=None, notify_callbacks=None, timeout=2000): + def __init__(self, json_rpc_endpoint: JsonRpcEndpoint, method_callbacks=None, notify_callbacks=None, timeout=None): super().__init__() self.json_rpc_endpoint: JsonRpcEndpoint = json_rpc_endpoint self.notify_callbacks: Dict = notify_callbacks or {} @@ -144,6 +144,20 @@ def stop(self): self.shutdown_flag = True def run(self): + try: + self._run_loop() + finally: + # Stop and wake any callers still waiting so they fail fast instead + # of blocking forever once the connection is gone. + self.shutdown_flag = True + self._wake_pending() + + def _wake_pending(self): + for cond in list(self.event_dict.values()): + with cond: + cond.notify_all() + + def _run_loop(self): rpc_id = None while not self.shutdown_flag: try: @@ -201,16 +215,20 @@ def call_method(self, method_name, args): cond = threading.Condition() self.event_dict[current_id] = cond - cond.acquire() - self.send_message(method_name, args, current_id) - if self.shutdown_flag: - return None - - if not cond.wait(timeout=self._timeout): - raise TimeoutError() - cond.release() - - self.event_dict.pop(current_id) + with cond: + self.send_message(method_name, args, current_id) + # `timeout` is in seconds; None waits indefinitely. KeY operations + # can run for a long time, so a premature timeout is worse than none. + if not self.shutdown_flag: + cond.wait(timeout=self._timeout) + + self.event_dict.pop(current_id, None) + if current_id not in self.response_dict: + # Woken without a result: the wait timed out, or the reader thread + # stopped because the server closed the connection. + if self.shutdown_flag: + raise ConnectionError("server closed the connection before responding") + raise TimeoutError("no response within %s seconds" % self._timeout) result, error = self.response_dict.pop(current_id) if error: raise ResponseError(error.get("code"), error.get("message"), error.get("data")) diff --git a/keyext.client.python/tests/__init__.py b/keyext.client.python/tests/__init__.py new file mode 100644 index 0000000000..e69de29bb2 diff --git a/keyext.client.python/tests/test_lsp_endpoint.py b/keyext.client.python/tests/test_lsp_endpoint.py new file mode 100644 index 0000000000..fff84619b6 --- /dev/null +++ b/keyext.client.python/tests/test_lsp_endpoint.py @@ -0,0 +1,81 @@ +# 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 +"""Stability tests for keyapi.rpc.LspEndpoint (timeout semantics, disconnect). + +Run with:: + + python3 -m unittest discover -s tests -t . + +from the ``keyext.client.python`` directory. +""" +import threading +import time +import unittest + +from keyapi.rpc import LspEndpoint + + +class _SilentEndpoint: + """Never responds and never closes — used to exercise the timeout path.""" + + def send_request(self, message): + pass + + def recv_response(self): + time.sleep(3600) + return None + + +class _DisconnectingEndpoint: + """Simulates the server closing the connection shortly after a request.""" + + def send_request(self, message): + pass + + def recv_response(self): + time.sleep(0.1) + return None # connection closed + + +class LspEndpointTimeoutTest(unittest.TestCase): + def test_default_timeout_is_none(self): + # #13: the default must be an unambiguous "wait indefinitely", not the + # old 2000 that looked like milliseconds but meant ~33 minutes (seconds). + self.assertIsNone(LspEndpoint(_SilentEndpoint())._timeout) + + def test_finite_timeout_is_seconds_and_raises(self): + endpoint = LspEndpoint(_SilentEndpoint(), timeout=0.2) + endpoint.daemon = True + endpoint.start() + start = time.monotonic() + with self.assertRaises(TimeoutError): + endpoint.call_method("ping", []) + # 0.2 is interpreted as seconds, so the call returns promptly. + self.assertLess(time.monotonic() - start, 5) + + def test_server_disconnect_wakes_pending_call(self): + # With no timeout a disconnect must still wake the caller (ConnectionError) + # instead of hanging forever. + endpoint = LspEndpoint(_DisconnectingEndpoint()) + endpoint.daemon = True + endpoint.start() + + outcome = {} + + def call(): + try: + endpoint.call_method("ping", []) + except Exception as exc: # noqa: BLE001 - recorded for assertion + outcome["exc"] = exc + + t = threading.Thread(target=call) + t.daemon = True # so an unfixed (hanging) endpoint can't block the suite + t.start() + t.join(timeout=5) + self.assertFalse(t.is_alive(), "call_method hung after server disconnect") + self.assertIsInstance(outcome.get("exc"), ConnectionError) + + +if __name__ == "__main__": + unittest.main() From a8c0f6b0443a11c5d261a008290fcd54e62ca80f Mon Sep 17 00:00:00 2001 From: Richard Bubel Date: Mon, 22 Jun 2026 19:46:25 +0200 Subject: [PATCH 5/6] Implement treeSubtree; fix websocket stream setup and auto() stdout logging --- .../org/keyproject/key/api/KeyApiImpl.java | 51 +++++++++++++++++-- .../org/keyproject/key/api/StartServer.java | 2 + .../keyproject/key/api/TreeSubtreeTest.java | 36 +++++++++++++ 3 files changed, 86 insertions(+), 3 deletions(-) create mode 100644 keyext.api/src/test/java/org/keyproject/key/api/TreeSubtreeTest.java 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 index e112ef8aca..f79407a102 100644 --- a/keyext.api/src/main/java/org/keyproject/key/api/KeyApiImpl.java +++ b/keyext.api/src/main/java/org/keyproject/key/api/KeyApiImpl.java @@ -59,10 +59,14 @@ import org.keyproject.key.api.data.KeyIdentifications.*; import org.keyproject.key.api.remoteapi.KeyApi; import org.keyproject.key.api.remoteclient.ClientApi; +import org.slf4j.Logger; +import org.slf4j.LoggerFactory; import static org.keyproject.key.api.data.ProofNodeDescription.collectPathInformation; public final class KeyApiImpl implements KeyApi { + private static final Logger LOGGER = LoggerFactory.getLogger(KeyApiImpl.class); + private final KeyIdentifications data = new KeyIdentifications(); private Function exitHandler; @@ -184,8 +188,8 @@ public CompletableFuture auto(ProofId proofId, StrategyOptions opti var env = data.find(proofId.env()); options.configure(proof); try { - System.out.println("Starting proof with setting " - + proof.getSettings().getStrategySettings().getActiveStrategyProperties() + LOGGER.debug("Starting proof with stop mode {}", + proof.getSettings().getStrategySettings().getActiveStrategyProperties() .getProperty(StrategyProperties.STOPMODE_OPTIONS_KEY)); env.getProofControl().startAndWaitForAutoMode(proof); // clientListener); @@ -356,7 +360,48 @@ public CompletableFuture> treeChildren(ProofId proof, TreeNod @Override public CompletableFuture> treeSubtree(ProofId proof, TreeNodeId nodeId) { - return CompletableFuture.completedFuture(List.of()); + return CompletableFuture.supplyAsync(() -> { + var serial = Integer.parseInt(nodeId.id()); + Node root = data.find(proof).root(); + + // locate the requested node by its serial number + Node start = null; + var search = new Stack(); + search.push(root); + while (!search.empty()) { + var node = search.pop(); + if (node.serialNr() == serial) { + start = node; + break; + } + var it = node.childrenIterator(); + while (it.hasNext()) { + search.push(it.next()); + } + } + if (start == null) { + return List.of(); + } + + // collect the whole subtree rooted at `start`, in pre-order + // (the node itself followed by its descendants) + var result = new ArrayList(); + var stack = new Stack(); + stack.push(start); + while (!stack.empty()) { + var node = stack.pop(); + result.add(TreeNodeDesc.from(proof, node)); + var children = new ArrayList(); + var it = node.childrenIterator(); + while (it.hasNext()) { + children.add(it.next()); + } + for (int i = children.size() - 1; i >= 0; i--) { + stack.push(children.get(i)); + } + } + return result; + }); } @Override 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 index 4d30491f60..0c35b452ad 100644 --- a/keyext.api/src/main/java/org/keyproject/key/api/StartServer.java +++ b/keyext.api/src/main/java/org/keyproject/key/api/StartServer.java @@ -151,6 +151,8 @@ public void run() { } if (websocket) { + // Without this, in/out stay null and the launcher gets no streams. + establishStreams(); var launcherBuilder = new WebSocketLauncherBuilder() .setOutput(out) .setInput(in) diff --git a/keyext.api/src/test/java/org/keyproject/key/api/TreeSubtreeTest.java b/keyext.api/src/test/java/org/keyproject/key/api/TreeSubtreeTest.java new file mode 100644 index 0000000000..d0a536a7d8 --- /dev/null +++ b/keyext.api/src/test/java/org/keyproject/key/api/TreeSubtreeTest.java @@ -0,0 +1,36 @@ +/* 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.List; + +import org.junit.jupiter.api.Assertions; +import org.junit.jupiter.api.Test; +import org.keyproject.key.api.data.KeyIdentifications.TreeNodeId; +import org.keyproject.key.api.data.TreeNodeDesc; + +/** + * Regression test for {@code treeSubtree}, which previously always returned an + * empty list (a silent stub). + */ +class TreeSubtreeTest { + @Test + void treeSubtreeReturnsTheSubtreeRootedAtTheNode() throws Exception { + var api = new KeyApiImpl(); + var proofId = api.loadTerm("true").get(); + var treeRoot = api.treeRoot(proofId).get(); + var rootSerial = treeRoot.id().nodeId(); + + List subtree = + api.treeSubtree(proofId, new TreeNodeId(rootSerial)).get(); + Assertions.assertFalse(subtree.isEmpty(), "subtree of the root must not be empty"); + Assertions.assertTrue( + subtree.stream().anyMatch(d -> d.id().nodeId().equals(rootSerial)), + "subtree should contain the root node itself"); + + // an unknown node yields an empty list + Assertions.assertTrue( + api.treeSubtree(proofId, new TreeNodeId("999999")).get().isEmpty()); + } +} From 6e4d26361169a9e5ebc12f42e61483f114119165 Mon Sep 17 00:00:00 2001 From: Richard Bubel Date: Mon, 22 Jun 2026 20:11:01 +0200 Subject: [PATCH 6/6] Cache service-loader lookups for macros and script commands --- .../org/keyproject/key/api/KeyApiImpl.java | 33 +++++++++++------ .../key/api/KeyApiServiceCacheTest.java | 36 +++++++++++++++++++ 2 files changed, 59 insertions(+), 10 deletions(-) create mode 100644 keyext.api/src/test/java/org/keyproject/key/api/KeyApiServiceCacheTest.java 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 index f79407a102..f057958e30 100644 --- a/keyext.api/src/main/java/org/keyproject/key/api/KeyApiImpl.java +++ b/keyext.api/src/main/java/org/keyproject/key/api/KeyApiImpl.java @@ -10,11 +10,14 @@ import java.util.ArrayList; import java.util.Collection; import java.util.List; +import java.util.Map; +import java.util.NoSuchElementException; import java.util.Objects; import java.util.Stack; import java.util.concurrent.CompletableFuture; import java.util.concurrent.atomic.AtomicInteger; import java.util.function.Function; +import java.util.stream.Collectors; import java.util.stream.Stream; import java.util.stream.StreamSupport; @@ -90,9 +93,23 @@ public void taskFinished(TaskFinishedInfo info) { }; private final AtomicInteger uniqueCounter = new AtomicInteger(); + // Available macros and script commands are discovered via the service loader + // (a classpath scan). They don't change at runtime, so scan once here instead + // of on every getAvailableMacros/getAvailableScriptCommands/macro request. + private final List availableMacros = loadAll(ProofMacro.class); + private final List availableScriptCommands = + loadAll(ProofScriptCommand.class); + private final Map macrosByName = availableMacros.stream() + .collect(Collectors.toUnmodifiableMap(ProofMacro::getName, m -> m, (a, b) -> a)); + public KeyApiImpl() { } + private static List loadAll(Class service) { + return StreamSupport.stream( + ClassLoaderUtil.loadServices(service).spliterator(), false).toList(); + } + @Override @JsonRequest public CompletableFuture> examples() { @@ -128,18 +145,13 @@ public CompletableFuture getVersion() { @Override public CompletableFuture> getAvailableMacros() { return CompletableFuture.completedFuture( - StreamSupport - .stream(ClassLoaderUtil.loadServices(ProofMacro.class).spliterator(), false) - .map(ProofMacroDesc::from).toList()); + availableMacros.stream().map(ProofMacroDesc::from).toList()); } @Override public CompletableFuture> getAvailableScriptCommands() { return CompletableFuture.completedFuture( - StreamSupport - .stream(ClassLoaderUtil.loadServices(ProofScriptCommand.class).spliterator(), - false) - .map(ProofScriptCommandDesc::from).toList()); + availableScriptCommands.stream().map(ProofScriptCommandDesc::from).toList()); } @Override @@ -166,9 +178,10 @@ public CompletableFuture macro(ProofId proofId, String macroName 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(); + var macro = macrosByName.get(macroName); + if (macro == null) { + throw new NoSuchElementException("No macro named '" + macroName + "'"); + } try { var info = diff --git a/keyext.api/src/test/java/org/keyproject/key/api/KeyApiServiceCacheTest.java b/keyext.api/src/test/java/org/keyproject/key/api/KeyApiServiceCacheTest.java new file mode 100644 index 0000000000..8c432bb7e5 --- /dev/null +++ b/keyext.api/src/test/java/org/keyproject/key/api/KeyApiServiceCacheTest.java @@ -0,0 +1,36 @@ +/* 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.NoSuchElementException; +import java.util.concurrent.ExecutionException; + +import org.junit.jupiter.api.Assertions; +import org.junit.jupiter.api.Test; + +/** + * Tests for the cached service-loader lookups (macros / script commands). The + * caching is by construction; these guard against regressions in the behaviour. + */ +class KeyApiServiceCacheTest { + @Test + void availableMacrosAndCommandsAreNonEmptyAndStable() throws Exception { + var api = new KeyApiImpl(); + var macros1 = api.getAvailableMacros().get(); + var macros2 = api.getAvailableMacros().get(); + Assertions.assertFalse(macros1.isEmpty(), "expected built-in macros"); + Assertions.assertEquals(macros1, macros2, "repeated calls must be consistent"); + Assertions.assertFalse(api.getAvailableScriptCommands().get().isEmpty(), + "expected built-in script commands"); + } + + @Test + void macroRejectsUnknownName() throws Exception { + var api = new KeyApiImpl(); + var proofId = api.loadTerm("true").get(); + var ex = Assertions.assertThrows(ExecutionException.class, + () -> api.macro(proofId, "definitely-not-a-real-macro", null).get()); + Assertions.assertInstanceOf(NoSuchElementException.class, ex.getCause()); + } +}