prototype ui

UQ-PAC · Jun 24, 2024 · bd0ec31 · bd0ec31
1 parent 72ad324
commit bd0ec31
Show file tree

Hide file tree

Showing 8 changed files with 260 additions and 7 deletions.
diff --git a/libASL/support/web/dune b/libASL/support/web/dune
@@ -0,0 +1,4 @@
+(library
+ (name libASL_web)
+ (implements libASL_support)
+ (libraries libASL_ast zarith_stubs_js))
diff --git a/libASL/support/web/solver.ml b/libASL/support/web/solver.ml
@@ -0,0 +1,4 @@
+
+module AST = Asl_ast
+
+let check_constraints (_bs: AST.expr list) (_cs: AST.expr list): bool = true
diff --git a/web/aslp.js b/web/aslp.js
@@ -0,0 +1,87 @@
+/**
+ * Supporting code to enable ASLp-in-JS. Handles input/output.
+ */
+
+const get = query => {
+  const result = document.querySelector(query);
+  console.assert(result, "query returned null: " + query);
+  return result;
+};
+
+// XXX: cannot use worker due to worker stack size being too small
+// const worker = new Worker('worker.js');
+
+const input = get('#op');
+const output = get('#output');
+const loading = get('#loading');
+
+
+const OPCODE = 'opcode';
+const BYTES = 'bytes';
+let mode = OPCODE;
+
+const flipEndian = s => {
+  const chunked = s.match(/.{1,2}/g); // chunks of 2
+  chunked.reverse();
+  return chunked.join('');
+};
+
+// always returns BIG-endian string
+const getOpcode = () => {
+  const val = input.value.trim().replace(/^0x/, '').replace(/\s/g, '').padStart(8, '0');
+
+  if (val.length > 8) throw Error('opcode too long: ' + val.length);
+  if (mode == OPCODE) return val;
+  return flipEndian(val);
+}
+
+const setOpcodeMode = newMode => {
+  if (mode != newMode) {
+    const op = getOpcode();
+    mode = newMode;
+
+    if (mode == OPCODE) {
+      input.value = '0x' + op.toLowerCase();
+    } else {
+      input.value = flipEndian(op).toUpperCase().match(/.{1,2}/g).join(' ');
+    }
+  }
+};
+
+const onChangeDebug = el => {
+  libASL_web.setDebugLevel(parseInt(el.value, 10));
+};
+
+const clearOutput = () => {
+  output.innerHTML = '';
+};
+
+const submit = () => {
+  clearOutput();
+  loading.classList.remove('invisible');
+  // defer computation so loading indicator shows.
+  setTimeout(() => {
+    try {
+      libASL_web.dis('0x' + getOpcode());
+    } finally {
+      loading.classList.add('invisible');
+    }
+  }, 30);
+};
+
+
+const write = (isError) => s => {
+  const span = document.createElement('span');
+  const data = new Uint8Array(s.length);
+  for (let i = 0; i < s.length; i++) {
+    data[i] = s.charCodeAt(i);
+  }
+  span.textContent = new TextDecoder('utf-8').decode(data);
+  if (isError)
+    span.classList.add('stderr');
+  output.appendChild(span);
+  return 0;
+};
+
+libASL_web.init(write(false), write(true));
+libASL_web.setDebugLevel(0);
diff --git a/web/dune b/web/dune
@@ -2,10 +2,11 @@
   (name js)
   (modes js)
   (modules js)
-  (libraries z3 libASLResources dune-site str zarith pprint zarith_stubs_js)
-  (js_of_ocaml (flags --debug-info --no-inline :standard \ --source-map-inline))
+  (libraries libASL libASL_web js_of_ocaml)
+  (js_of_ocaml (flags --debug-info --no-inline --sourcemap :standard \ --source-map-inline))
+  (preprocess (pps js_of_ocaml-ppx))
   )
 
 (alias
  (name default)
- (deps js.bc.js index.html))
+ (deps js.bc.js index.html reset.css aslp.js worker.js))
diff --git a/web/index.html b/web/index.html
@@ -1,9 +1,93 @@
 <!doctype html>
 <html>
   <head>
-    <title>Cubes</title>
+    <title>ASLp Web</title>
     <script type="text/javascript" src="js.bc.js"></script>
+    <link href="reset.css" rel="stylesheet" />
+    <meta name="viewport" content="width=device-width, initial-scale=1.0">
   </head>
+
+  <style>
+    body {
+      font-family: sans-serif;
+      padding: 2em;
+    }
+
+    .monospace {
+      font-family: monospace;
+    }
+
+    .small {
+      font-size: 12px;
+    }
+
+    p {
+      margin-bottom: 0.5em;
+    }
+
+    input[type="radio"], label, summary {
+      cursor: pointer;
+    }
+
+    .invisible {
+      visibility: hidden;
+    }
+
+    .stderr {
+      color: #ce0000;
+    }
+  </style>
+
   <body>
+    <h1>ASLp Web</h1>
+    <form action="javascript:submit();">
+      <div>
+        <p>
+          <input onclick="setOpcodeMode('opcode');" type="radio" id="opcode" name="mode" value="opcode" checked />
+          <label for="opcode">Opcode (big-endian)</label><br/>
+          <input onclick="setOpcodeMode('bytes');" type="radio" id="bytes" name="mode" value="bytes" />
+          <label for="bytes">Bytes (little-endian)</label>
+        </p>
+      </div>
+      <p>
+        <input id="op" type="text" class="monospace" required autofocus value="0x8b031041"
+               pattern="[a-fA-F0-9x ]+" />
+      </p>
+
+      <p>
+        <button id="go" submit>Semantics</button>
+        <span id="loading" class="invisible">Loading...</span>
+      </p>
+
+      <p>
+
+        <details>
+          <summary>Debug options</summary>
+          <select onchange="onChangeDebug(this);" name="debug" id="debug">
+            <option value="0">minimal</option>
+            <option value="1">stack trace</option>
+            <option value="2">stack trace, variables</option>
+            <option value="3">stack trace, variables, residual programs</option>
+          </select>
+        </details>
+
+      </p>
+
+      <hr/>
+
+      <h4>Output</h4>
+      <p>
+        <button disabled type=button class="small" id="dl">Download</button>
+        <button disabled type=button class="small" id="share">Share</button>
+        <button onclick="clearOutput();" type=button class="small" id="clear">Clear</button>
+      </p>
+      <p>
+        <pre id="output"></pre>
+
+      </p>
+    </form>
+
+
+    <script type="text/javascript" src="aslp.js"></script>
   </body>
 </html>
diff --git a/web/js.ml b/web/js.ml
@@ -1,4 +1,38 @@
+
+let init input out err =
+  Js_of_ocaml.Sys_js.set_channel_flusher stdout out;
+  Js_of_ocaml.Sys_js.set_channel_flusher stderr err;
+  Js_of_ocaml.Sys_js.set_channel_filler stdin input;
+  ()
+
+let env = lazy (Option.get @@ LibASL.Arm_env.aarch64_evaluation_environment ())
+let denv = lazy (LibASL.Dis.build_env @@ Lazy.force env)
+
+let print_pp = ref true
+
+let pp_stmt () =
+  if !print_pp then Asl_utils.pp_stmt else fun x -> Utils.to_string (Asl_parser_pp.pp_raw_stmt x)
+
+let dis (x: string) =
+  let stmts = LibASL.Dis.retrieveDisassembly Lazy.(force env) Lazy.(force denv) x in
+  List.iter
+    (fun s -> print_endline @@ pp_stmt () s)
+    stmts;
+  flush stdout
+
+
 let () =
-  print_endline "hello from js";
-  print_endline @@ Int.to_string @@ List.length LibASLResources.Res.Sites.aslfiles
-  (* print_endline @@ LibASL.Value.(pp_value @@ from_bitsLit "100") *)
+  print_endline "libASL_web ocaml-side...";
+
+  let open Js_of_ocaml in
+  let () = Js.export "libASL_web"
+    (object%js
+      (* TODO: support stdin from javascript for repl, possibly converting asli repl to lwt *)
+      method init (out : string -> unit) (err : string -> unit) = init (fun () -> "") out err
+
+      method force = let _ = Lazy.force env and _ = Lazy.force denv in ()
+      method dis (x: string) = dis x
+      method setDebugLevel i = (LibASL.Dis.debug_level := i)
+      method setPrettyPrint (x : bool) = (print_pp := x)
+     end) in
+  ()
diff --git a/web/reset.css b/web/reset.css
@@ -0,0 +1,27 @@
+/*
+  Josh's Custom CSS Reset
+  https://www.joshwcomeau.com/css/custom-css-reset/
+*/
+*, *::before, *::after {
+  box-sizing: border-box;
+}
+* {
+  margin: 0;
+}
+body {
+  line-height: 1.5;
+  -webkit-font-smoothing: antialiased;
+}
+img, picture, video, canvas, svg {
+  display: block;
+  max-width: 100%;
+}
+input, button, textarea, select {
+  font: inherit;
+}
+p, h1, h2, h3, h4, h5, h6 {
+  overflow-wrap: break-word;
+}
+#root, #__next {
+  isolation: isolate;
+}
diff --git a/web/worker.js b/web/worker.js
@@ -0,0 +1,12 @@
+importScripts('js.bc.js');
+
+console.log('libASL_web js-side:', libASL_web);
+
+libASL_web.go();
+console.log('libASL_web worker ready');
+
+onmessage = function(e) {
+  const fn = libASL_web[e.data[0]];
+  console.assert(fn, "libASL_web function not found: " + e.data);
+  fn(...e.data[1]);
+};
Original file line number	Diff line number	Diff line change
		@@ -0,0 +1,4 @@

		module AST = Asl_ast

		let check_constraints (_bs: AST.expr list) (_cs: AST.expr list): bool = true