From bd0ec31931a8258ecef48e98bb61bcd7296f93de Mon Sep 17 00:00:00 2001 From: rina Date: Mon, 24 Jun 2024 16:53:35 +1000 Subject: [PATCH] prototype ui --- libASL/support/web/dune | 4 ++ libASL/support/web/solver.ml | 4 ++ web/aslp.js | 87 ++++++++++++++++++++++++++++++++++++ web/dune | 7 +-- web/index.html | 86 ++++++++++++++++++++++++++++++++++- web/js.ml | 40 +++++++++++++++-- web/reset.css | 27 +++++++++++ web/worker.js | 12 +++++ 8 files changed, 260 insertions(+), 7 deletions(-) create mode 100644 libASL/support/web/dune create mode 100644 libASL/support/web/solver.ml create mode 100644 web/aslp.js create mode 100644 web/reset.css create mode 100644 web/worker.js diff --git a/libASL/support/web/dune b/libASL/support/web/dune new file mode 100644 index 00000000..f9cb6a66 --- /dev/null +++ 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 new file mode 100644 index 00000000..fa6b9717 --- /dev/null +++ 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 new file mode 100644 index 00000000..e312b86f --- /dev/null +++ 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 index 0c1ced8f..5daaee9b 100644 --- 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 index 1288b982..aa33d859 100644 --- a/web/index.html +++ b/web/index.html @@ -1,9 +1,93 @@ - Cubes + ASLp Web + + + + + +

ASLp Web

+
+
+

+ +
+ + +

+
+

+ +

+ +

+ + +

+ +

+ +

+ Debug options + +
+ +

+ +
+ +

Output

+

+ + + +

+

+ 


+      
+      

+    

+
+
+    
   
 
diff --git a/web/js.ml b/web/js.ml
index 8e5deaa9..f6cab93e 100644
--- 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
new file mode 100644
index 00000000..bafd2ab0
--- /dev/null
+++ 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
new file mode 100644
index 00000000..42063258
--- /dev/null
+++ 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]);
+};