tests: Add a demo

cpitclaudel · Mar 26, 2018 · b848d78 · b848d78
1 parent 10da8d8
commit b848d78
Show file tree

Hide file tree

Showing 6 changed files with 318 additions and 0 deletions.
diff --git a/.gitignore b/.gitignore
@@ -1,3 +1,5 @@
 /z3-js/
 /.vagrant/
 /provision.log
+/html/z3w.wasm
+/html/z3w.js
diff --git a/html/demo.js b/html/demo.js
@@ -0,0 +1,95 @@
+/* exported makeZ3Demo */
+function makeZ3Demo(window, queries, responses, ace) {
+    var editor;
+    var worker;
+    var verification_start;
+
+    var console = window.console;
+    var document = window.document;
+    var command_line_args = document.getElementById("command-line-args");
+    var run_button = document.getElementById("run");
+    var stdout_textbox = document.getElementById("stdout");
+
+    function postZ3Message(query, payload) {
+        console.info("[Window] → Z3 (" + query + "):", payload);
+        worker.postMessage({ kind: query, payload: payload });
+    }
+
+    function clear(node) {
+        while (node.hasChildNodes()) {
+            node.removeChild(node.lastChild);
+        }
+    }
+
+    function disableButton(message) {
+        run_button.disabled = true;
+        run_button.value = message;
+    }
+
+    function enableButton() {
+        run_button.disabled = false;
+        run_button.value = "Run Z3!";
+    }
+
+    function verifyCurrentInput(_event) {
+        var input = editor.getValue();
+        var args = command_line_args.value.split(/ +/);
+        clear(stdout_textbox);
+        disableButton("Running…");
+        verification_start = window.performance.now();
+        postZ3Message(queries.VERIFY, { args: args, input: input });
+    }
+
+    function logOutput(message, cssClass) {
+        var span_node = window.document.createElement("span");
+        span_node.className = cssClass;
+        span_node.appendChild(window.document.createTextNode(message + "\n"));
+        stdout_textbox.appendChild(span_node);
+    }
+
+    function onZ3Message(event) {
+        console.info("Z3 → [Window]:", event);
+        var kind = event.data.kind;
+        var payload = event.data.payload;
+        switch (kind) {
+        case responses.PROGRESS:
+            disableButton(payload);
+            break;
+        case responses.READY:
+            enableButton();
+            break;
+        case responses.STDOUT:
+            logOutput(payload, "stdout-msg");
+            break;
+        case responses.STDERR:
+            logOutput(payload, "stderr-msg")
+            break;
+        case responses.VERIFICATION_COMPLETE:
+            enableButton();
+            var elapsed = Math.round(window.performance.now() - verification_start);
+            logOutput ("-- Verification complete (" + elapsed + "ms)", "info-msg");
+            break;
+        }
+    }
+
+    function setupZ3Worker() {
+        worker = new window.Worker("worker.js");
+        worker.onmessage = onZ3Message;
+    }
+
+    function setupAceEditor() {
+        editor = ace.edit("editor");
+        editor.setTheme("ace/theme/monokai");
+        editor.getSession().setMode("ace/mode/lisp");
+        editor.setOptions({ fontFamily: "Ubuntu Mono, monospace", fontSize: "1rem" });
+    }
+
+    function init() {
+        setupAceEditor();
+        setupZ3Worker();
+        clear(stdout_textbox);
+        run_button.onclick = verifyCurrentInput;
+    }
+
+    return { init: init };
+}
diff --git a/html/protocol.js b/html/protocol.js
@@ -0,0 +1,4 @@
+var queries = { VERIFY: "VERIFY" };
+var responses = { PROGRESS: "PROGRESS", READY: "READY",
+                  STDOUT: "STDOUT", STDERR: "STDERR",
+                  VERIFICATION_COMPLETE: "VERIFICATION_COMPLETE" };
diff --git a/html/worker.js b/html/worker.js
@@ -0,0 +1,76 @@
+function makeWorker(self, console, queries, responses, performance) {
+    var INPUT_FNAME = "input.smt2";
+
+    var solver;
+    var ready = false;
+
+    function postMessage(kind, payload) {
+        console.info("Z3 → Window (" + kind + "):", payload);
+        self.postMessage({ kind: kind, payload: payload });
+    }
+
+    function runSolver(input, args) {
+        if (!ready) {
+            console.error("Cannot run SMT solver yet.");
+            postMessage(responses.DONE, false);
+            return;
+        }
+
+        args.push(INPUT_FNAME);
+        console.log("Running SMT solver with", args);
+        solver.FS.writeFile(INPUT_FNAME, input, { encoding: "utf8" });
+        solver.callMain(args);
+        postMessage(responses.VERIFICATION_COMPLETE, true);
+    }
+
+    function progress(message) {
+        postMessage(responses.PROGRESS, message);
+        console.info("Worker:", message, performance.now());
+    }
+
+    function onRuntimeInitialized() {
+        ready = true;
+        progress("Done initializing SMT solver.");
+        postMessage(responses.READY);
+    }
+
+    var STUB_MSG = "Calling stub instead of signal()"
+
+    function postOutput(channel, output) {
+        output = output.replace(STUB_MSG, "");
+        if (output != "") {
+            postMessage(channel, output);
+        }
+    }
+
+    function loadSolver() {
+        progress("Downloading SMT solver…");
+        self.importScripts("z3w.js");
+        progress("Initializing SMT solver…");
+        solver = Z3({ ENVIRONMENT: "WORKER",
+                      onRuntimeInitialized: onRuntimeInitialized,
+                      print: function(message) { postOutput(responses.STDOUT, message); },
+                      printErr: function(message) { postOutput(responses.STDERR, message); } });
+    }
+
+    function onMessage(event) {
+        console.info("Window → Z3:", event);
+        var kind = event.data.kind;
+        var payload = event.data.payload;
+        switch (kind) {
+        case queries.VERIFY:
+            runSolver(payload.input, payload.args);
+            break;
+        }
+    }
+
+    function init() {
+        loadSolver();
+        self.onmessage = onMessage;
+    }
+
+    return { init: init };
+}
+
+importScripts("protocol.js");
+makeWorker(self, console, queries, responses, performance).init();
diff --git a/html/z3.css b/html/z3.css
@@ -0,0 +1,87 @@
+html {
+    padding: 1rem;
+    font-family: "Ubuntu", sans-serif;
+}
+
+body {
+    border: 1px solid #BBB;
+    margin: auto;
+    max-width: 60em;
+}
+
+h1 {
+    margin-top: 0;
+    margin-bottom: 0.5rem;
+    font-weight: normal;
+}
+
+#main {
+    background: #F0F0F0;
+    padding: 1rem;
+}
+
+#editor {
+    height: 20rem;
+    width: 100%;
+}
+
+#control-panel {
+    width: 100%;
+    display: table;
+    margin-top: 0.5rem;
+}
+
+.column { display: table-column; }
+.row { display: table-row; }
+
+#command-line-args, #run, #stdout {
+    font-family: "Ubuntu Mono", monospace;
+}
+
+#command-line-args, #run {
+    font-size: 1.2rem;
+}
+
+.stderr-msg {
+    color: #f57900;
+}
+
+.info-msg {
+    color: #729fcf;
+}
+
+#run-cell {
+    display: table-cell;
+    padding-left: 0.5rem;
+    width: 1px;
+}
+
+#run {
+    min-width: 7.5rem;
+}
+
+#command-line-args {
+    box-sizing: border-box;
+    display: table-cell;
+    width: 100%;
+}
+
+#stdout {
+    background: black;
+    box-sizing: border-box;
+    color: white;
+    font-size: 1rem;
+    margin-bottom: 0;
+    margin-top: 0.5rem;
+    min-height: 3rem;
+    padding: 0.5rem;
+    white-space: pre-wrap;
+    width: 100%;
+}
+
+#footer {
+    text-align: right;
+    font-size: 0.7rem;
+    font-style: italic;
+    margin-top: 1rem;
+}
diff --git a/html/z3.html b/html/z3.html
@@ -0,0 +1,54 @@
+<!DOCTYPE html>
+<html lang="en">
+  <head>
+    <meta charset="utf-8">
+    <title>Z3.wasm demo</title>
+    <link rel="stylesheet" href="z3.css">
+    <script src="./demo.js"></script>
+  </head>
+  <body>
+    <div id="main">
+      <h1>Z3.wasm</h1>
+
+      <div id="editor">(declare-fun x () Int)
+(declare-fun y () Int)
+(declare-fun z () Int)
+(assert (>= (* 2 x) (+ y z)))
+(declare-fun f (Int) Int)
+(declare-fun g (Int Int) Int)
+(assert (< (f x) (g x x)))
+(assert (> (f y) (g x x)))
+(check-sat)
+(get-model)
+(push)
+(assert (= x y))
+(check-sat)
+(get-model)
+(check-sat)
+(pop)
+(exit)</div>
+
+      <hr />
+
+      <div id="control-panel">
+        <div class="row">
+          <input class="cell" id="command-line-args" type="text" value="-smt2" />
+          <span id="run-cell"><input id="run" type="button" value="" disabled="disabled" /></span>
+        </div>
+      </div>
+      <pre id="stdout"></pre>
+
+      <div id="footer">
+        Assembled by <a href="http://pit-claudel.fr/clement/">Clément Pit-Claudel</a> by compiling Z3 with <a href="http://kripken.github.io/emscripten-site/">Emscripten</a>.
+      </div>
+    </div>
+
+    <script src="https://cdnjs.cloudflare.com/ajax/libs/ace/1.2.6/ace.js" integrity="sha256-xrr4HH5eSY+cFz4SH7ja/LaAi9qcEdjMpeMP49/iOLs=" crossorigin="anonymous"></script>
+    <script src="https://cdnjs.cloudflare.com/ajax/libs/ace/1.2.6/mode-lisp.js" integrity="sha256-wfwED8MuFsljraPmCVHtcP7jjyi6ffnB1kk1kY2ha5g=" crossorigin="anonymous"></script>
+    <script src="./protocol.js"></script>
+
+    <script>
+      makeZ3Demo(window, queries, responses, ace).init();
+    </script>
+  </body>
+</html>