key/keyext.webctrl/src/main/java/org/key_project/webctrl/ExampleOpenerHandler.java at 57e2c8a106b03caa03f2fb4ff3163ab31f77ca4b · KeYProject/key · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
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();
        }
    }
}