replace --aarch64-dir with --export-aarch64 and re-generate coverage

this is more useful once the MRA files are bundled.

* update coverage run.sh to remove --aarch64-dir usage

* update coverage with new embedded file paths

no changes to recorded coverage outcomes, only the filename in error
messages is different.

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,10 +338,10 @@ let _ =
 
 let main () =
     if !opt_print_version then Printf.printf "%s\n" version
-    else if !opt_print_aarch64_dir then 
-        match Arm_env.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";

libASL/arm_env.ml

@@ -28,7 +28,6 @@ let asl_blobs : LoadASL.source list = [
 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/loadASL.ml

@@ -51,6 +51,15 @@ let read_source = function
         x
     | DataSource (_, data) -> data
 
+let write_source prefix = function
+    | FileSource _ -> failwith "write_source for FileSource is unsupported"
+    | DataSource (name, data) ->
+        let name = Filename.concat prefix name in
+        Utils.mkdir_p (Filename.dirname name);
+        let chan = open_out_bin name in
+        output_string chan data;
+        close_out chan
+
 let report_parse_error (on_error: unit -> 'a) (f: unit -> 'a): 'a =
     (try
         f ()

libASL/loadASL.mli

@@ -12,6 +12,7 @@ type source = FileSource of string | DataSource of string * string
 val pp_source : source -> string
 val name_of_source : source -> string
 val read_source : source -> string
+ val write_source : string -> source -> unit
 
 val mkLoc : string -> string -> AST.l
 

libASL/utils.ml

@@ -7,6 +7,15 @@
 
 (** Generic utility functions *)
 
+let rec mkdir_p p =
+    let open Filename in
+    if Sys.file_exists p then
+        ()
+    else
+        (* make parents, then make final directory. *)
+        (mkdir_p (dirname p); Sys.mkdir p 0o755)
+
+
 (****************************************************************
  * Pretty-printer related
  ****************************************************************)

tests/coverage/aarch64_branch

@@ -153,10 +153,10 @@ ENCODING: aarch64_branch_conditional_test
 0xb7ffffff: [b5=1 ; op=1 ; b40=31 ; imm14=16383 ; Rt=31] --> OK
 
 ENCODING: aarch64_branch_unconditional_dret
-0xd6bf03e0: [] --> UNDEFINED (file "./mra_tools/arch/arch_instrs.asl" line 46870 char 59 - line 46871 char 0)
+0xd6bf03e0: [] --> UNDEFINED (file "<data:mra_tools/arch/arch_instrs.asl>" line 46870 char 59 - line 46871 char 0)
 
 ENCODING: aarch64_branch_unconditional_eret
-0xd69f03e0: [A=0 ; M=0 ; Rn=31 ; op4=0] --> UNDEFINED (file "./mra_tools/arch/arch_instrs.asl" line 30382 char 46 - line 30383 char 0)
+0xd69f03e0: [A=0 ; M=0 ; Rn=31 ; op4=0] --> UNDEFINED (file "<data:mra_tools/arch/arch_instrs.asl>" line 30382 char 46 - line 30383 char 0)
 0xd69f03e1: [A=0 ; M=0 ; Rn=31 ; op4=1] --> (invalid)
 0xd69f03e2: [A=0 ; M=0 ; Rn=31 ; op4=2] --> (invalid)
 0xd69f03e3: [A=0 ; M=0 ; Rn=31 ; op4=3] --> (invalid)
@@ -251,7 +251,7 @@ ENCODING: aarch64_branch_unconditional_eret
 0xd69f0bfc: [A=1 ; M=0 ; Rn=31 ; op4=28] --> (invalid)
 0xd69f0bfd: [A=1 ; M=0 ; Rn=31 ; op4=29] --> (invalid)
 0xd69f0bfe: [A=1 ; M=0 ; Rn=31 ; op4=30] --> (invalid)
-0xd69f0bff: [A=1 ; M=0 ; Rn=31 ; op4=31] --> UNDEFINED (file "./mra_tools/arch/arch_instrs.asl" line 30382 char 46 - line 30383 char 0)
+0xd69f0bff: [A=1 ; M=0 ; Rn=31 ; op4=31] --> UNDEFINED (file "<data:mra_tools/arch/arch_instrs.asl>" line 30382 char 46 - line 30383 char 0)
 0xd69f0fe0: [A=1 ; M=1 ; Rn=31 ; op4=0] --> (invalid)
 0xd69f0fe1: [A=1 ; M=1 ; Rn=31 ; op4=1] --> (invalid)
 0xd69f0fe2: [A=1 ; M=1 ; Rn=31 ; op4=2] --> (invalid)
@@ -283,7 +283,7 @@ ENCODING: aarch64_branch_unconditional_eret
 0xd69f0ffc: [A=1 ; M=1 ; Rn=31 ; op4=28] --> (invalid)
 0xd69f0ffd: [A=1 ; M=1 ; Rn=31 ; op4=29] --> (invalid)
 0xd69f0ffe: [A=1 ; M=1 ; Rn=31 ; op4=30] --> (invalid)
-0xd69f0fff: [A=1 ; M=1 ; Rn=31 ; op4=31] --> UNDEFINED (file "./mra_tools/arch/arch_instrs.asl" line 30382 char 46 - line 30383 char 0)
+0xd69f0fff: [A=1 ; M=1 ; Rn=31 ; op4=31] --> UNDEFINED (file "<data:mra_tools/arch/arch_instrs.asl>" line 30382 char 46 - line 30383 char 0)
 
 ENCODING: aarch64_branch_unconditional_immediate
 0x14000000: [op=0 ; imm26=0] --> OK