Support compilation to Javascript (#90)

* Split libASL and isolate Z3 into virtual library (#91)

Z3 links to a native shared library, and so is unsuitable for use via js-of-ocaml. This separates the one use of Z3 in the code (the type-checker's constraint solver) into a separate library which may be stubbed for non-native platforms.

This separates libASL into two parts: libASL_ast which is the minimum needed to define the ASL syntax tree, and libASL which contains the rest of the library. libASL should still be used as the public interface of the library. Since libASL re-exports all of libASL_ast, this should not affect the API visible by downstream users.

This is required since we need to insert a platform-specific library, libASL_support, which introduces z3 only on native builds. The dependency tree now looks like: libASL_ast <- libASL_support (virtual) <- libASL.

* remove pcre library, use ocaml str instead (#93)

PCRE relies on a shared library, precluding its use in Javascript.
instead, we use the standard ocaml "str" library. note, however,
that this supports a smaller subscript of regex (notably no negative
lookahead), and has a different syntax.

see: https://ocaml.org/manual/5.2/api/Str.html

* Embed ARM ASL specs within OCaml (#92)

* extract arm environment into separate file.

* allow loading files from either disk or memory

* use ppx_blob to embed ASL files instead of dune-site

This is instead of installing the ASL files to disk.
This should make the installation less liable to random
breakages when installed or linked in an unexpected way.

The binary size increases by 6MB.

Updates tests/coverage/run.sh to substitute away the
new file paths of the embedded files, so no coverage
re-generation needed.

* replace --aarch64-dir with --export-aarch64

this is more useful once the MRA files are bundled.

* initialising jsoo

* tcheck: make global env0 mutable

necessary for correct unmarshalling, as this
must contain global variables

* dummy libASL to reduce conflicts

* rename libASL parts to stage0/stage1

asli.opam

@@ -24,9 +24,8 @@ depends: [
   "pprint"
   "zarith"
   "z3" {>= "4.8.7"}
-  "pcre"
   "alcotest" {with-test}
-  "dune-site"
+  "ppx_blob"
   "lwt"
   "cohttp-lwt-unix"
   "yojson"

bin/asli.ml

@@ -23,7 +23,7 @@ let opt_prelude : string ref = ref "prelude.asl"
 let opt_filenames : string list ref = ref []
 let opt_print_version = ref false
 let opt_no_default_aarch64 = ref false
-let opt_print_aarch64_dir = ref false
+let opt_export_aarch64_dir = ref ""
 let opt_verbose = ref false
 
 
@@ -309,8 +309,8 @@ let rec repl (tcenv: TC.Env.t) (cpu: Cpu.cpu): unit =
 let options = Arg.align ([
     ( "-x", Arg.Set_int Dis.debug_level,      "       Partial evaluation debugging (requires debug level argument >= 0)");
     ( "-v", Arg.Set opt_verbose,              "       Verbose output");
-    ( "--no-aarch64", Arg.Set opt_no_default_aarch64 , "       Disable bundled AArch64 semantics");
-    ( "--aarch64-dir", Arg.Set opt_print_aarch64_dir, "       Print directory of bundled AArch64 semantics");
+    ( "--no-aarch64", Arg.Set opt_no_default_aarch64 ,    "       Disable bundled AArch64 semantics");
+    ( "--export-aarch64", Arg.Set_string opt_export_aarch64_dir,  "       Export bundled AArch64 MRA to the given directory");
     ( "--version", Arg.Set opt_print_version, "       Print version");
     ( "--prelude", Arg.Set_string opt_prelude,"       ASL prelude file (default: ./prelude.asl)");
 ] )
@@ -338,25 +338,26 @@ let _ =
 
 let main () =
     if !opt_print_version then Printf.printf "%s\n" version
-    else if !opt_print_aarch64_dir then 
-        match aarch64_asl_dir with 
-        | Some d -> Printf.printf "%s\n" d
-        | None -> (Printf.eprintf "Unable to retrieve installed asl directory\n"; exit 1)
+    else if "" <> !opt_export_aarch64_dir then
+        let dir = !opt_export_aarch64_dir in
+        ignore @@ Sys.readdir dir;
+        List.iter LoadASL.(write_source dir) Arm_env.(prelude_blob :: asl_blobs);
     else begin
         if !opt_verbose then List.iter print_endline banner;
         if !opt_verbose then print_endline "\nType :? for help";
 
+        let sources = List.map (fun x -> LoadASL.FileSource x) !opt_filenames in
         (* Note: .prj files are handled by `evaluation_environment`. *)
         let env_opt =
             if (!opt_no_default_aarch64)  
-            then evaluation_environment !opt_prelude !opt_filenames !opt_verbose
+            then evaluation_environment (FileSource !opt_prelude) sources !opt_verbose
             else begin
                 if List.length (!opt_filenames) != 0 then
                     Printf.printf
                         "Warning: asl file arguments ignored without --no-aarch64 (%s)\n"
                         (String.concat " " !opt_filenames)
                 else ();
-                aarch64_evaluation_environment ~verbose:!opt_verbose ();
+                Arm_env.aarch64_evaluation_environment ~verbose:!opt_verbose ();
             end in
 
         let env = (match env_opt with 
@@ -369,7 +370,7 @@ let main () =
         LNoise.history_set ~max_length:100 |> ignore;
 
         let denv = Dis.build_env env in
-        let tcenv = TC.Env.mkEnv TC.env0 and cpu = Cpu.mkCPU env denv in
+        let tcenv = TC.Env.mkEnv !TC.env0 and cpu = Cpu.mkCPU env denv in
 
         repl tcenv cpu
     end

bin/dune

@@ -5,7 +5,7 @@
  (modes exe byte)
  (modules asli)
  (flags (-cclib -lstdc++))
- (libraries libASL linenoise pprint pcre)
+ (libraries asli.libASL linenoise pprint)
  )
 
 (executable
@@ -14,7 +14,7 @@
  (modes exe)
  (modules server)
  (flags (-cclib -lstdc++))
- (libraries libASL pprint pcre lwt.unix yojson cohttp-lwt cohttp-lwt-unix))
+ (libraries asli.libASL pprint lwt.unix yojson cohttp-lwt cohttp-lwt-unix))
 
 
 (executable
@@ -23,28 +23,28 @@
  ; (public_name test_asl_lexer)
  (modules testlexer)
  (flags (-cclib -lstdc++))
- (libraries libASL))
+ (libraries asli.libASL))
 
 (executable
  (name processops)
  (modes exe)
  ; (public_name test_asl_lexer)
  (modules processops)
  (flags (-cclib -lstdc++))
- (libraries libASL unix))
+ (libraries asli.libASL unix))
 
 (executable
  (name offline_coverage)
  (public_name asloff-coverage)
  (modes exe)
  (modules offline_coverage)
  (flags (-cclib -lstdc++))
- (libraries libASL offlineASL))
+ (libraries asli.libASL offlineASL))
 
 (executable
  (name offline_sem)
  (public_name asloff-sem)
  (modes exe)
  (modules offline_sem)
  (flags (-cclib -lstdc++))
- (libraries libASL offlineASL))
+ (libraries asli.libASL offlineASL))

bin/offline_coverage.ml

@@ -84,13 +84,9 @@ let rec process_command tcenv env cmd =
 
 let main () = 
   let opt_verbose = ref false in
-  let env = match Eval.aarch64_evaluation_environment ~verbose:!opt_verbose () with
+  let env = match Arm_env.aarch64_evaluation_environment ~verbose:!opt_verbose () with
   | Some e -> e
   | _ -> failwith "Unable to build evaluation environment." in
-  let filenames = Option.get Eval.aarch64_asl_files in
-  let prj_files = List.filter (fun f -> Utils.endswith f ".prj") (snd filenames) in
-  let tcenv = Tcheck.Env.mkEnv Tcheck.env0 in
-  List.iter (fun f -> process_command tcenv env (":project " ^ f)) prj_files;
   List.map (fun instr -> run opt_verbose instr env) !opt_instr
 
 let _ = ignore (main())

bin/server.ml

@@ -15,7 +15,7 @@ open Asl_utils
 open Lwt
 
 
-let persistent_env = lazy (Option.get (aarch64_evaluation_environment ()))
+let persistent_env = lazy (Option.get (Arm_env.aarch64_evaluation_environment ()))
 
 let eval_instr (opcode: string) : string =
     let pp_raw stmt : string = Utils.to_string (Asl_parser_pp.pp_raw_stmt stmt) |> String.trim  in

dune

@@ -1,26 +1,24 @@
-(install 
-  (files
-   (prelude.asl                       as   prelude.asl                      )
-   (mra_tools/arch/arch.asl           as   mra_tools/arch/arch.asl          )
-   (mra_tools/arch/arch_decode.asl    as   mra_tools/arch/arch_decode.asl   )
-   (mra_tools/arch/arch_instrs.asl    as   mra_tools/arch/arch_instrs.asl   )
-   (mra_tools/arch/regs.asl           as   mra_tools/arch/regs.asl          )
-   (mra_tools/arch/regs_access.asl    as   mra_tools/arch/regs_access.asl   )
-   (mra_tools/support/aes.asl         as   mra_tools/support/aes.asl        )
-   (mra_tools/support/barriers.asl    as   mra_tools/support/barriers.asl   )
-   (mra_tools/support/debug.asl       as   mra_tools/support/debug.asl      )
-   (mra_tools/support/feature.asl     as   mra_tools/support/feature.asl    )
-   (mra_tools/support/fetchdecode.asl as   mra_tools/support/fetchdecode.asl)
-   (mra_tools/support/hints.asl       as   mra_tools/support/hints.asl      )
-   (mra_tools/support/interrupts.asl  as   mra_tools/support/interrupts.asl )
-   (mra_tools/support/memory.asl      as   mra_tools/support/memory.asl     )
-   (mra_tools/support/stubs.asl       as   mra_tools/support/stubs.asl      )
-   (mra_tools/types.asl               as   mra_tools/types.asl              )
-   (tests/override.asl                as   tests/override.asl               )
-   (tests/override.prj                as   tests/override.prj               )
-  )
-  (section (site (asli aslfiles)))
- )
+(alias 
+  (name asl_files)
+  (deps
+    prelude.asl
+    mra_tools/arch/arch.asl
+    mra_tools/arch/arch_decode.asl
+    mra_tools/arch/arch_instrs.asl
+    mra_tools/arch/regs.asl
+    mra_tools/arch/regs_access.asl
+    mra_tools/support/aes.asl
+    mra_tools/support/barriers.asl
+    mra_tools/support/debug.asl
+    mra_tools/support/feature.asl
+    mra_tools/support/fetchdecode.asl
+    mra_tools/support/hints.asl
+    mra_tools/support/interrupts.asl
+    mra_tools/support/memory.asl
+    mra_tools/support/stubs.asl
+    mra_tools/types.asl
+    tests/override.asl
+    tests/override.prj))
 
 (alias
  (name default)

dune-project

@@ -2,7 +2,6 @@
 (name asli)
 (version 0.2.0)
 
-(using dune_site 0.1)
 (using menhir 2.0)
 
 (package
@@ -23,14 +22,12 @@
     "pprint"
     "zarith"
     ("z3"        (>= "4.8.7"))
-    "pcre"
     ("alcotest"  :with-test)
-    "dune-site"
+    "ppx_blob"
     "lwt"
     "cohttp-lwt-unix"
     "yojson"
   )
-  (sites (share aslfiles))
 )
 
 (license BSD-3-Clause)

libASL/arm_env.ml

@@ -0,0 +1,34 @@
+(* defines the evaluation environment for the bundled Arm spsecifications. *)
+
+let aarch64_asl_dir: string option = 
+    None
+
+let prelude_blob : LoadASL.source = DataSource ("prelude.asl", [%blob "../prelude.asl"])
+
+let asl_blobs : LoadASL.source list = [
+    DataSource ("mra_tools/arch/regs.asl", [%blob "../mra_tools/arch/regs.asl"]);
+    DataSource ("mra_tools/types.asl", [%blob "../mra_tools/types.asl"]);
+    DataSource ("mra_tools/arch/arch.asl", [%blob "../mra_tools/arch/arch.asl"]);
+    DataSource ("mra_tools/arch/arch_instrs.asl", [%blob "../mra_tools/arch/arch_instrs.asl"]);
+    DataSource ("mra_tools/arch/regs_access.asl", [%blob "../mra_tools/arch/regs_access.asl"]);
+    DataSource ("mra_tools/arch/arch_decode.asl", [%blob "../mra_tools/arch/arch_decode.asl"]);
+    DataSource ("mra_tools/support/aes.asl", [%blob "../mra_tools/support/aes.asl"]);
+    DataSource ("mra_tools/support/barriers.asl", [%blob "../mra_tools/support/barriers.asl"]);
+    DataSource ("mra_tools/support/debug.asl", [%blob "../mra_tools/support/debug.asl";]);
+    DataSource ("mra_tools/support/feature.asl", [%blob "../mra_tools/support/feature.asl"]);
+    DataSource ("mra_tools/support/hints.asl", [%blob "../mra_tools/support/hints.asl"]);
+    DataSource ("mra_tools/support/interrupts.asl", [%blob "../mra_tools/support/interrupts.asl"]);
+    DataSource ("mra_tools/support/memory.asl", [%blob "../mra_tools/support/memory.asl";]);
+    DataSource ("mra_tools/support/stubs.asl", [%blob "../mra_tools/support/stubs.asl"]);
+    DataSource ("mra_tools/support/fetchdecode.asl", [%blob "../mra_tools/support/fetchdecode.asl"]);
+    DataSource ("tests/override.asl", [%blob "../tests/override.asl"]);
+    DataSource ("tests/override.prj", [%blob "../tests/override.prj"]);
+]
+
+let aarch64_asl_files: (LoadASL.source * LoadASL.source list) option =
+    Some (prelude_blob, asl_blobs)
+
+let aarch64_evaluation_environment ?(verbose = false) (): Eval.Env.t option = 
+    Option.bind aarch64_asl_files 
+        (fun (prelude, filenames) -> Eval.evaluation_environment prelude filenames verbose)
+

libASL/decoder_program.ml

@@ -116,10 +116,10 @@ let run iset pat env problematic =
 
   (* Find all matching instructions, pulled from testing.ml *)
   let decoder = Eval.Env.getDecoder env (Ident iset) in
-  let re = Pcre.regexp pat in
+  let re = Str.regexp pat in
   let filterfn = function
     | ((Encoding_Block (Ident nm, Ident is, _, _, _, _, _, _)),_,_,_) ->
-        is = iset && Pcre.pmatch ~rex:re nm && not (List.mem nm problematic)
+        is = iset && Str.string_match re nm 0 && not (List.mem nm problematic)
     | _ -> assert false
   in
   let encs = List.filter filterfn (Eval.Env.listInstructions env) in

libASL/dis.ml

@@ -180,7 +180,7 @@ module LocalEnv = struct
 
     let init (env: Eval.Env.t) =
         let eval e = val_expr (Eval.eval_expr Unknown env e) in
-        let tenv = Tcheck.env0 in
+        let tenv = !Tcheck.env0 in
         let get_global_type id =
             (match Tcheck.GlobalEnv.getGlobalVar tenv id with
             | Some (Type_Bits e) ->
@@ -642,7 +642,7 @@ and width_of_type (loc: l) (t: ty): int =
   | _ -> unsupported loc @@ "Can't get bit width of type: " ^ pp_type t
 
 and width_of_field (loc: l) (t: ty) (f: ident): int =
-  let env = Tcheck.env0 in
+  let env = !Tcheck.env0 in
   let ft =
     (match Tcheck.typeFields env loc t with
     | FT_Record rfs -> Tcheck.get_recordfield loc rfs f
@@ -654,7 +654,7 @@ and width_of_field (loc: l) (t: ty) (f: ident): int =
 
 (** Determine the type of memory access expression (Var, Array, Field) *)
 and type_of_load (loc: l) (x: expr): ty rws =
-  let env = Tcheck.env0 in
+  let env = !Tcheck.env0 in
   (match x with
   | Expr_Var(id) ->
       let+ (_,(t,_)) = DisEnv.gets (LocalEnv.resolveGetVar loc id) in

libASL/dune

@@ -14,19 +14,46 @@
      (with-stdout-to asl_parser_tail.mly (bash "OTT=${ASLI_OTT:-$(opam config var ott:share)};  grep -v '^%%' $OTT/menhir_library_extra.mly"))
      (with-stdout-to asl_parser.mly (run cat asl_parser_head.mly asl_parser_tail.mly)))))
 
+; libASL is constructed in two stages: stage0, and stage1.
+; stage0 is the minimum needed to define an "expression", and stage1 is the rest.
+; this is so stage0 can be used as a dependency for the libASL_support virtual library
+; which provides flexibility on whether to link z3 (for native compilation) or not (for js compilation).
+; thus, everything after the type-checking phase is in stage1.
+; these stages are merged together in libASL_virtual and re-exported as "LibASL",
+; and asli.libASL provides a publicly available dummy library which additionally
+; links the native implementation of the support code.
+
 (library
- (name libASL)
- (public_name asli.libASL)
+ (name libASL_stage0)
+ (public_name asli.libASL-stage0)
+ (flags (:standard -w -27))
+ (modules asl_ast asl_parser asl_parser_pp asl_utils asl_visitor visitor utils)
+ (libraries pprint (re_export zarith)))
+
+(library
+ (name libASL_stage1)
+ (public_name asli.libASL-stage1)
  (flags
-  (:standard -w -27 -cclib -lstdc++))
- (modules asl_ast asl_parser asl_parser_pp asl_utils asl_visitor cpu dis elf eval
-   lexer lexersupport loadASL monad primops rws symbolic tcheck testing transforms utils value visitor res
+  (:standard -w -27 -cclib -lstdc++ -open LibASL_stage0))
+ (modules cpu dis elf eval
+   lexer lexersupport loadASL monad primops rws symbolic tcheck testing transforms value
    symbolic_lifter decoder_program call_graph req_analysis
-   offline_transform ocaml_backend dis_tc
-   offline_opt
+   offline_transform ocaml_backend dis_tc offline_opt
+   arm_env
    )
- (libraries pprint zarith z3 str pcre  dune-site))
+ (preprocessor_deps (alias ../asl_files))
+ (preprocess (pps ppx_blob))
+ (libraries libASL_stage0 libASL_support str))
 
-(generate_sites_module
- (module res)
- (sites asli))
+(library
+ (name libASL_virtual)
+ (public_name asli.libASL-virtual)
+ (modules libASL)
+ (wrapped false) ; exports LibASL module
+ (libraries libASL_stage0 libASL_stage1))
+
+(library
+ (name libASL_dummy)
+ (public_name asli.libASL)
+ (modules)
+ (libraries (re_export libASL_virtual) libASL_support_native))