Fix RPCLayer handler thread shutdown and unknown-id NPE

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 {

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

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;
 
@@ -59,10 +62,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<Void, Boolean> exitHandler;
@@ -86,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<ProofMacro> availableMacros = loadAll(ProofMacro.class);
+    private final List<ProofScriptCommand> availableScriptCommands =
+        loadAll(ProofScriptCommand.class);
+    private final Map<String, ProofMacro> macrosByName = availableMacros.stream()
+            .collect(Collectors.toUnmodifiableMap(ProofMacro::getName, m -> m, (a, b) -> a));
+
     public KeyApiImpl() {
     }
 
+    private static <T> List<T> loadAll(Class<T> service) {
+        return StreamSupport.stream(
+            ClassLoaderUtil.loadServices(service).spliterator(), false).toList();
+    }
+
     @Override
     @JsonRequest
     public CompletableFuture<List<ExampleDesc>> examples() {
@@ -124,18 +145,13 @@ public CompletableFuture<String> getVersion() {
     @Override
     public CompletableFuture<List<ProofMacroDesc>> 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<List<ProofScriptCommandDesc>> getAvailableScriptCommands() {
         return CompletableFuture.completedFuture(
-            StreamSupport
-                    .stream(ClassLoaderUtil.loadServices(ProofScriptCommand.class).spliterator(),
-                        false)
-                    .map(ProofScriptCommandDesc::from).toList());
+            availableScriptCommands.stream().map(ProofScriptCommandDesc::from).toList());
     }
 
     @Override
@@ -162,9 +178,10 @@ public CompletableFuture<MacroStatistic> 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 =
@@ -184,8 +201,8 @@ public CompletableFuture<ProofStatus> 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 +373,48 @@ public CompletableFuture<List<TreeNodeDesc>> treeChildren(ProofId proof, TreeNod
 
     @Override
     public CompletableFuture<List<TreeNodeDesc>> 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<Node>();
+            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<TreeNodeDesc>();
+            var stack = new Stack<Node>();
+            stack.push(start);
+            while (!stack.empty()) {
+                var node = stack.pop();
+                result.add(TreeNodeDesc.from(proof, node));
+                var children = new ArrayList<Node>();
+                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
@@ -578,8 +636,9 @@ public CompletableFuture<ProofId> 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 +654,17 @@ public CompletableFuture<ProofId> 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
+                    }
+                }
             }
         });
     }

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<ClientApi>()
                         .setOutput(out)
                         .setInput(in)

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

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