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