From 5dad8d5a10b258763322a5785846fdc2fd842778 Mon Sep 17 00:00:00 2001 From: rina Date: Fri, 21 Jun 2024 17:54:44 +1000 Subject: [PATCH] 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. --- asli.opam | 2 +- dune | 44 +++++++++++++++++++++---------------------- dune-project | 4 +--- libASL/arm_env.ml | 39 +++++++++++++++++++++++++------------- libASL/dune | 9 ++++----- libASL/loadASL.ml | 6 +++--- tests/coverage/run.sh | 4 ++-- 7 files changed, 58 insertions(+), 50 deletions(-) diff --git a/asli.opam b/asli.opam index b412139c..4a09e8ae 100644 --- a/asli.opam +++ b/asli.opam @@ -25,7 +25,7 @@ depends: [ "zarith" "z3" {>= "4.8.7"} "alcotest" {with-test} - "dune-site" + "ppx_blob" "lwt" "cohttp-lwt-unix" "yojson" diff --git a/dune b/dune index 10c8b130..6347f813 100644 --- a/dune +++ b/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) diff --git a/dune-project b/dune-project index f8c331a1..f57814cc 100644 --- a/dune-project +++ b/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) diff --git a/libASL/arm_env.ml b/libASL/arm_env.ml index f3b9d8bb..3282137d 100644 --- a/libASL/arm_env.ml +++ b/libASL/arm_env.ml @@ -1,20 +1,33 @@ (* defines the evaluation environment for the bundled Arm spsecifications. *) let aarch64_asl_dir: string option = - List.nth_opt Res.Sites.aslfiles 0 + 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_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 aarch64_evaluation_environment ?(verbose = false) (): Eval.Env.t option = Option.bind aarch64_asl_files diff --git a/libASL/dune b/libASL/dune index dc13689d..1ca4d24a 100644 --- a/libASL/dune +++ b/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 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)) 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 diff --git a/tests/coverage/run.sh b/tests/coverage/run.sh index 0b9eebac..375dfdd4 100755 --- a/tests/coverage/run.sh +++ b/tests/coverage/run.sh @@ -2,7 +2,7 @@ pattern="${1:?requires regex pattern as first argument}" -asl_dir="$(asli --aarch64-dir)" output="$(echo ":coverage A64 $pattern" | asli)" -echo "$output" | sed "s#$asl_dir#.#g" +# substitute paths of the form with ./[...] +echo "$output" | sed 's#]*\)>#./\1#g'