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.

asli.opam

@@ -25,7 +25,7 @@ depends: [
   "zarith"
   "z3" {>= "4.8.7"}
   "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 

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
@@ -24,12 +23,11 @@
     "zarith"
     ("z3"        (>= "4.8.7"))
     ("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/dune

@@ -28,13 +28,12 @@
  (flags
   (:standard -w -27 -cclib -lstdc++))
  (modules cpu dis elf eval
-   lexer lexersupport loadASL monad primops rws symbolic tcheck testing transforms value res
+   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 libASL_support (re_export libASL_ast) str dune-site))
+ (preprocessor_deps (alias ../asl_files))
+ (preprocess (pps ppx_blob))
+ (libraries libASL_support (re_export libASL_ast) str))
 
-(generate_sites_module
- (module res)
- (sites asli))

libASL/eval.ml

@@ -1319,34 +1319,37 @@ let set_impdef (tcenv: Tcheck.Env.t) (env: Env.t) (fname: string) (rest: string
     Env.setImpdef env x v
 
 (** Evaluates a minimal subset of the .prj syntax, sufficient for override.prj. *)
-let evaluate_prj_minimal (tcenv: Tcheck.Env.t) (env: Env.t) (fname: string) =
-    let inchan = open_in fname in
-    try
-        while true do
-            let line = input_line inchan in
-            match (String.split_on_char ' ' line) with
+let evaluate_prj_minimal (tcenv: Tcheck.Env.t) (env: Env.t) (source: LoadASL.source) =
+    let data = LoadASL.read_source source in
+    let fname = LoadASL.pp_source source in
+    let lines = List.map String.trim @@ String.split_on_char '\n' data in
+    List.iter
+        (fun line -> match (String.split_on_char ' ' line) with
             | ":set" :: "impdef" :: rest -> set_impdef tcenv env fname rest
             | empty when List.for_all (String.equal "") empty -> ()  (* ignore empty lines *)
-            | _ -> failwith @@ "Unrecognised minimal .prj line in " ^ fname ^ ": " ^ line
-        done
-    with | End_of_file -> close_in inchan
+            | _ -> failwith @@ "Unrecognised minimal .prj line in " ^ fname ^ ": " ^ line)
+        lines
 
 (** Constructs an evaluation environment with the given prelude file and .asl/.prj files.
     .prj files given here are required to be minimal. *)
-let evaluation_environment (prelude: string) (files: string list) (verbose: bool) = 
-    let t  = LoadASL.read_file prelude true verbose in
-    let ts = List.map (fun filename ->
+let evaluation_environment (prelude: LoadASL.source) (files: LoadASL.source list) (verbose: bool) = 
+    let t  = LoadASL.read_file (prelude) true verbose in
+    let ts = List.map (fun file ->
+        let filename = LoadASL.name_of_source file in
         if Utils.endswith filename ".spec" then begin
-            LoadASL.read_spec filename verbose 
+            LoadASL.read_spec file verbose 
         end else if Utils.endswith filename ".asl" then begin
-            LoadASL.read_file filename false verbose 
+            LoadASL.read_file file false verbose 
         end else if Utils.endswith filename ".prj" then begin
             [] (* ignore project files here and process later *)
         end else begin
-            failwith ("Unrecognized file suffix on "^filename)
+            failwith ("Unrecognized file suffix on "^(LoadASL.pp_source file))
         end
     ) files in
-    let prjs = List.filter (fun fname -> Utils.endswith fname ".prj") files in
+
+    let prjs = List.filter
+        (fun fname -> Utils.endswith (LoadASL.name_of_source fname) ".prj")
+        files in
 
     if verbose then Printf.printf "Building evaluation environment\n";
     let env = (
@@ -1361,24 +1364,6 @@ let evaluation_environment (prelude: string) (files: string list) (verbose: bool
     env
 
 
-let aarch64_asl_dir: string option = 
-    List.nth_opt Res.Sites.aslfiles 0
-
-let aarch64_asl_files: (string * string list) option = 
-    let aarch64_file_load_order = 
-       ["mra_tools/arch/regs.asl"; "mra_tools/types.asl"; "mra_tools/arch/arch.asl"; "mra_tools/arch/arch_instrs.asl"; "mra_tools/arch/regs_access.asl";
-        "mra_tools/arch/arch_decode.asl"; "mra_tools/support/aes.asl"; "mra_tools/support/barriers.asl"; "mra_tools/support/debug.asl"; 
-        "mra_tools/support/feature.asl"; "mra_tools/support/hints.asl"; "mra_tools/support/interrupts.asl"; "mra_tools/support/memory.asl"; 
-        "mra_tools/support/stubs.asl"; "mra_tools/support/fetchdecode.asl"; "tests/override.asl"; "tests/override.prj"]
-    in Option.bind aarch64_asl_dir (fun dir ->
-        let filenames = List.map (Filename.concat dir) aarch64_file_load_order in
-        let prelude = Filename.concat dir "prelude.asl" in
-        Some (prelude, filenames))
-
-let aarch64_evaluation_environment ?(verbose = false) (): Env.t option = 
-    Option.bind aarch64_asl_files 
-        (fun (prelude, filenames) -> evaluation_environment prelude filenames verbose)
-
 (****************************************************************
  * End
  ****************************************************************)