From 57e2c8a106b03caa03f2fb4ff3163ab31f77ca4b Mon Sep 17 00:00:00 2001 From: Alexander Weigl Date: Sun, 5 Oct 2025 00:44:50 +0200 Subject: [PATCH] WebCtrl for interactive tutorials --- key.ui/build.gradle | 2 + keyext.webctrl/build.gradle | 4 + .../webctrl/ExampleOpenerHandler.java | 106 +++++++++++++++++ .../key_project/webctrl/SelectHandler.java | 19 +++ .../key_project/webctrl/WebCtrlExtension.java | 111 ++++++++++++++++++ ...ilkd.key.gui.extension.api.KeYGuiExtension | 1 + settings.gradle | 2 + 7 files changed, 245 insertions(+) create mode 100644 keyext.webctrl/build.gradle create mode 100644 keyext.webctrl/src/main/java/org/key_project/webctrl/ExampleOpenerHandler.java create mode 100644 keyext.webctrl/src/main/java/org/key_project/webctrl/SelectHandler.java create mode 100644 keyext.webctrl/src/main/java/org/key_project/webctrl/WebCtrlExtension.java create mode 100644 keyext.webctrl/src/main/resources/META-INF/services/de.uka.ilkd.key.gui.extension.api.KeYGuiExtension diff --git a/key.ui/build.gradle b/key.ui/build.gradle index 83df19c5297..c5eff39048f 100644 --- a/key.ui/build.gradle +++ b/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) { diff --git a/keyext.webctrl/build.gradle b/keyext.webctrl/build.gradle new file mode 100644 index 00000000000..c448ade9d8c --- /dev/null +++ b/keyext.webctrl/build.gradle @@ -0,0 +1,4 @@ +dependencies { + implementation project(":key.core") + implementation project(":key.ui") +} \ No newline at end of file diff --git a/keyext.webctrl/src/main/java/org/key_project/webctrl/ExampleOpenerHandler.java b/keyext.webctrl/src/main/java/org/key_project/webctrl/ExampleOpenerHandler.java new file mode 100644 index 00000000000..d727e0eb46c --- /dev/null +++ b/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 examples) throws IOException { + exchange.getResponseHeaders().add("Content-Type", "text/html"); + sendHtml(exchange, 200, (out) -> { + out.println(""" +

Available Examples:

+ "); + }); + } + + private static void sendHtml(HttpExchange exchange, int status, Consumer c) throws IOException { + StringWriter sw = new StringWriter(4 * 1024 * 1024); + PrintWriter out = new PrintWriter(sw, false); + out.format("%n"); + c.accept(out); + out.format(""); + 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(); + } + } +} diff --git a/keyext.webctrl/src/main/java/org/key_project/webctrl/SelectHandler.java b/keyext.webctrl/src/main/java/org/key_project/webctrl/SelectHandler.java new file mode 100644 index 00000000000..70ed57f9f49 --- /dev/null +++ b/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 { + + } +} diff --git a/keyext.webctrl/src/main/java/org/key_project/webctrl/WebCtrlExtension.java b/keyext.webctrl/src/main/java/org/key_project/webctrl/WebCtrlExtension.java new file mode 100644 index 00000000000..c1a2c7075c1 --- /dev/null +++ b/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 getStatusLineComponents() { + return List.of(chkBoxOnOff); + } + + + /// Helper method to parse query string into a map + public static Map queryToMap(HttpExchange exchange) { + String query = exchange.getRequestURI().getRawQuery(); + if (query == null) { + return Map.of(); + } + Map 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; + } +} diff --git a/keyext.webctrl/src/main/resources/META-INF/services/de.uka.ilkd.key.gui.extension.api.KeYGuiExtension b/keyext.webctrl/src/main/resources/META-INF/services/de.uka.ilkd.key.gui.extension.api.KeYGuiExtension new file mode 100644 index 00000000000..88881635d4b --- /dev/null +++ b/keyext.webctrl/src/main/resources/META-INF/services/de.uka.ilkd.key.gui.extension.api.KeYGuiExtension @@ -0,0 +1 @@ +org.key_project.webctrl.WebCtrlExtension \ No newline at end of file diff --git a/settings.gradle b/settings.gradle index 063d12034fa..b5c37db388e 100644 --- a/settings.gradle +++ b/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")