WebCtrl for interactive tutorials

key.ui/build.gradle

@@ -39,6 +39,8 @@ dependencies {
     runtimeOnly project(":keyext.slicing")
     runtimeOnly project(":keyext.proofmanagement")
     runtimeOnly project(":keyext.isabelletranslation")
+
+    runtimeOnly project(":keyext.webctrl")
 }
 
 tasks.register('createExamplesZip', Zip) {

keyext.webctrl/build.gradle

@@ -0,0 +1,4 @@
+dependencies {
+    implementation project(":key.core")
+    implementation project(":key.ui")
+}

keyext.webctrl/src/main/java/org/key_project/webctrl/ExampleOpenerHandler.java

@@ -0,0 +1,106 @@
+package org.key_project.webctrl;
+
+import com.sun.net.httpserver.HttpExchange;
+import com.sun.net.httpserver.HttpHandler;
+import de.uka.ilkd.key.core.KeYMediator;
+import de.uka.ilkd.key.gui.ExampleChooser;
+import de.uka.ilkd.key.gui.MainWindow;
+import org.jspecify.annotations.NullMarked;
+import org.slf4j.Logger;
+import org.slf4j.LoggerFactory;
+
+import javax.swing.*;
+import java.io.IOException;
+import java.io.PrintWriter;
+import java.io.StringWriter;
+import java.net.InetAddress;
+import java.nio.charset.Charset;
+import java.nio.charset.StandardCharsets;
+import java.util.List;
+import java.util.function.Consumer;
+
+@NullMarked
+class ExampleOpenerHandler implements HttpHandler {
+    private static final Logger LOGGER = LoggerFactory.getLogger(ExampleOpenerHandler.class);
+    private final MainWindow mainWindow;
+
+    public ExampleOpenerHandler(MainWindow mainWindow,
+                                KeYMediator mediator) {
+        this.mainWindow = mainWindow;
+    }
+
+    @Override
+    public void handle(HttpExchange exchange) throws IOException {
+        var params = WebCtrlExtension.queryToMap(exchange);
+        var name = params.get("name");
+        WebCtrlExtension.LOGGER.info("Incoming request to open example {}", name);
+
+        var ipv6 = InetAddress.getByName("::1");
+        final var incomingAddress = exchange.getRemoteAddress().getAddress();
+        if (!(incomingAddress.equals(InetAddress.getLocalHost())
+                || incomingAddress.equals(ipv6))
+        ) {
+            WebCtrlExtension.LOGGER.warn("Incoming request does not comes frm loopback address ({}, {}) but from {}. Abort processing.",
+                    ipv6, InetAddress.getLoopbackAddress(), incomingAddress);
+            exchange.sendResponseHeaders(403, 0);
+            exchange.close();
+            return;
+        }
+
+        var examples =
+                ExampleChooser.listExamples(ExampleChooser.lookForExamples());
+
+        for (ExampleChooser.Example example : examples) {
+            if (example.getName().equals(name)) {
+                LOGGER.info("Found example: {}. KeY will open it.", example);
+                SwingUtilities.invokeLater(() ->
+                        mainWindow.loadProblem(example.getObligationFile().toPath()));
+                exchange.sendResponseHeaders(200, 0);
+                exchange.close();
+                return;
+            }
+        }
+
+        writeOverview(exchange, examples);
+        exchange.getResponseBody().flush(); // so important
+        exchange.getResponseBody().close();
+    }
+
+    private static void writeOverview(HttpExchange exchange, List<ExampleChooser.Example> examples) throws IOException {
+        exchange.getResponseHeaders().add("Content-Type", "text/html");
+        sendHtml(exchange, 200, (out) -> {
+            out.println("""
+                        <h1>Available Examples:</h1>
+                        <ul>
+                    """);
+            for (ExampleChooser.Example example : examples) {
+                out.format("<li><a href=\"/openExample?name=%s\">%s</a><pre>%s</pre></li>",
+                        example.getName(), example.getName(), example.getDescription());
+            }
+            out.format("</ul>");
+        });
+    }
+
+    private static void sendHtml(HttpExchange exchange, int status, Consumer<PrintWriter> c) throws IOException {
+        StringWriter sw = new StringWriter(4 * 1024 * 1024);
+        PrintWriter out = new PrintWriter(sw, false);
+        out.format("<!DOCTYPE html><html><head></head><body>%n");
+        c.accept(out);
+        out.format("</body></html>");
+        out.flush();
+        out.close();
+        var str = sw.toString();
+
+        try {
+            final var bytes = str.getBytes(StandardCharsets.UTF_8);
+            exchange.sendResponseHeaders(status, bytes.length);
+            System.out.println("ExampleOpenerHandler.sendHtml1");
+            exchange.getResponseBody().write(bytes);
+            System.out.println("ExampleOpenerHandler.sendHtml2");
+            exchange.getResponseBody().flush(); // so important
+            System.out.println("ExampleOpenerHandler.sendHtml3");
+        } catch (Exception e) {
+            e.printStackTrace();
+        }
+    }
+}

keyext.webctrl/src/main/java/org/key_project/webctrl/SelectHandler.java

@@ -0,0 +1,19 @@
+package org.key_project.webctrl;
+
+import com.sun.net.httpserver.HttpExchange;
+import com.sun.net.httpserver.HttpHandler;
+import de.uka.ilkd.key.core.KeYMediator;
+import de.uka.ilkd.key.gui.MainWindow;
+import org.checkerframework.checker.nullness.qual.MonotonicNonNull;
+
+import java.io.IOException;
+
+class SelectHandler implements HttpHandler {
+    public SelectHandler(@MonotonicNonNull MainWindow mainWindow, @MonotonicNonNull KeYMediator mediator) {
+    }
+
+    @Override
+    public void handle(HttpExchange exchange) throws IOException {
+
+    }
+}

keyext.webctrl/src/main/java/org/key_project/webctrl/WebCtrlExtension.java

@@ -0,0 +1,111 @@
+/* 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.webctrl;
+
+import com.sun.net.httpserver.HttpExchange;
+import com.sun.net.httpserver.HttpServer;
+import de.uka.ilkd.key.core.KeYMediator;
+import de.uka.ilkd.key.gui.MainWindow;
+import de.uka.ilkd.key.gui.extension.api.KeYGuiExtension;
+import org.checkerframework.checker.nullness.qual.MonotonicNonNull;
+import org.jspecify.annotations.Nullable;
+import org.slf4j.Logger;
+import org.slf4j.LoggerFactory;
+
+import javax.swing.*;
+import java.io.IOException;
+import java.net.InetSocketAddress;
+import java.net.URLDecoder;
+import java.nio.charset.Charset;
+import java.util.HashMap;
+import java.util.List;
+import java.util.Map;
+import java.util.concurrent.Executor;
+import java.util.concurrent.ExecutorService;
+import java.util.concurrent.Executors;
+
+
+///
+@KeYGuiExtension.Info(name = "webctrl", experimental = false,
+        description = "Allows to control KeY via a local webserver.")
+public class WebCtrlExtension implements KeYGuiExtension, KeYGuiExtension.StatusLine, KeYGuiExtension.Startup {
+    public static final Logger LOGGER = LoggerFactory.getLogger(WebCtrlExtension.class);
+    public static final int PORT = 8000;
+
+    private @MonotonicNonNull MainWindow mainWindow;
+    private @MonotonicNonNull KeYMediator mediator;
+    private @MonotonicNonNull JCheckBox chkBoxOnOff = new JCheckBox("webctrl");
+    private @Nullable HttpServer server;
+
+
+    public WebCtrlExtension() {
+    }
+
+    public void init(MainWindow window, KeYMediator mediator) {
+        LOGGER.info("Initializing WebCtrl Extension");
+
+        this.mainWindow = window;
+        this.mediator = mediator;
+
+        chkBoxOnOff.addActionListener(evt -> {
+            if (server == null && chkBoxOnOff.isSelected()) {
+                try {
+                    start();
+                } catch (IOException e) {
+                    LOGGER.error("Error starting webctrl server", e);
+                }
+            }
+
+            if (server != null && !chkBoxOnOff.isSelected()) {
+                stop();
+            }
+        });
+    }
+
+    private void stop() {
+        if (server != null) {
+            LOGGER.info("Tear down WebCtrl Extension");
+            server.stop(0);
+        }
+    }
+
+    private void start() throws IOException {
+        assert server != null;
+
+        LOGGER.info("Starting WebCtrl Extension at port {}", PORT);
+        HttpServer server = HttpServer.create(new InetSocketAddress(PORT), 0);
+        server.createContext("/openExample", new ExampleOpenerHandler(mainWindow, mediator));
+        server.createContext("/select", new SelectHandler(mainWindow, mediator));
+
+        server.setExecutor(Executors.newVirtualThreadPerTaskExecutor()); // creates a default executor
+        server.start();
+    }
+
+    @Override
+    public List<JComponent> getStatusLineComponents() {
+        return List.of(chkBoxOnOff);
+    }
+
+
+    /// Helper method to parse query string into a map
+    public static Map<String, String> queryToMap(HttpExchange exchange) {
+        String query = exchange.getRequestURI().getRawQuery();
+        if (query == null) {
+            return Map.of();
+        }
+        Map<String, String> result = new HashMap<>();
+        for (String param : query.split("&")) {
+            String[] entry = param.split("=");
+            if (entry.length > 1) {
+                result.put(
+                        URLDecoder.decode(entry[0], Charset.defaultCharset()),
+                        URLDecoder.decode(entry[1], Charset.defaultCharset())
+                );
+            } else {
+                result.put(URLDecoder.decode(entry[0], Charset.defaultCharset()), "");
+            }
+        }
+        return result;
+    }
+}

keyext.webctrl/src/main/resources/META-INF/services/de.uka.ilkd.key.gui.extension.api.KeYGuiExtension

@@ -0,0 +1 @@
+org.key_project.webctrl.WebCtrlExtension

settings.gradle

@@ -22,6 +22,8 @@ include 'keyext.slicing'
 include 'keyext.caching'
 include 'keyext.isabelletranslation'
 
+include("keyext.webctrl")
+
 // ENABLE NULLNESS here or on the CLI
 // This flag is activated to enable the checker framework.
 // System.setProperty("ENABLE_NULLNESS", "true")