From 9a960ce393d6d202c31e89d26c964f2cba845868 Mon Sep 17 00:00:00 2001
From: rina <k@rina.fyi>
Date: Fri, 21 Jun 2024 17:54:44 +1000
Subject: [PATCH] use ppx_blob to embed mra files

---
 asli.opam         |  1 +
 dune-project      |  1 +
 libASL/arm_env.ml | 37 +++++++++++++++++++++++++------------
 libASL/dune       |  1 +
 libASL/loadASL.ml |  6 +++---
 5 files changed, 31 insertions(+), 15 deletions(-)

diff --git a/asli.opam b/asli.opam
index 690da900..8f1324c9 100644
--- a/asli.opam
+++ b/asli.opam
@@ -30,6 +30,7 @@ depends: [
   "lwt"
   "cohttp-lwt-unix"
   "yojson"
+  "ppx_blob"
   "odoc" {with-doc}
 ]
 build: [
diff --git a/dune-project b/dune-project
index 6b9b8780..015e328a 100644
--- a/dune-project
+++ b/dune-project
@@ -29,6 +29,7 @@
     "lwt"
     "cohttp-lwt-unix"
     "yojson"
+    "ppx_blob"
   )
   (sites (share aslfiles))
 )
diff --git a/libASL/arm_env.ml b/libASL/arm_env.ml
index f3b9d8bb..153d8a49 100644
--- a/libASL/arm_env.ml
+++ b/libASL/arm_env.ml
@@ -3,18 +3,31 @@
 let aarch64_asl_dir: string option = 
     List.nth_opt Res.Sites.aslfiles 0
 
-let aarch64_asl_files: (LoadASL.source * LoadASL.source 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
-        let prelude = LoadASL.FileSource prelude in
-        let filenames = List.map (fun x -> LoadASL.FileSource x) filenames in
-        Some (prelude, filenames))
+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 
diff --git a/libASL/dune b/libASL/dune
index 28bb75f6..0be28013 100644
--- a/libASL/dune
+++ b/libASL/dune
@@ -25,6 +25,7 @@
    offline_transform ocaml_backend dis_tc offline_opt
    arm_env
    )
+ (preprocess (pps ppx_blob))
  (libraries pprint zarith z3 str pcre  dune-site))
 
 (generate_sites_module
diff --git a/libASL/loadASL.ml b/libASL/loadASL.ml
index 808295c6..5c0d5b6a 100644
--- a/libASL/loadASL.ml
+++ b/libASL/loadASL.ml
@@ -32,15 +32,15 @@ let name_of_source = function | FileSource s | DataSource (s, _) -> s
 
 (** opens a variant source.
     returns (lexbuf, closer) where closer should be called to close the source. *)
-let open_source = function
+let open_source source = match source with
     | FileSource filename ->
         let inchan = open_in filename in
         let lexbuf = Lexing.from_channel inchan in
-        lexbuf.lex_curr_p <- { lexbuf.lex_curr_p with pos_fname = filename };
+        lexbuf.lex_curr_p <- { lexbuf.lex_curr_p with pos_fname = pp_source source };
         (lexbuf, fun () -> close_in inchan)
     | DataSource (filename, data) ->
         let lexbuf = Lexing.from_string data in
-        lexbuf.lex_curr_p <- { lexbuf.lex_curr_p with pos_fname = filename };
+        lexbuf.lex_curr_p <- { lexbuf.lex_curr_p with pos_fname = pp_source source };
         (lexbuf, Fun.id)
 
 let read_source = function