Support compilation to Javascript

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))