Skip to content

Commit

Permalink
use ppx_blob to embed ASL files instead of dune-site
Browse files Browse the repository at this point in the history 
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.
  • Loading branch information
@katrinafyi
katrinafyi committed Jun 24, 2024
1 parent 7d37249 commit 5dad8d5
Show file tree
Hide file tree
Showing 7 changed files with 58 additions and 50 deletions.
2 changes: 1 addition & 1 deletion asli.opam
View file
Original file line number Diff line number Diff line change
Expand Up @@ -25,7 +25,7 @@ depends: [
"zarith"
"z3" {>= "4.8.7"}
"alcotest" {with-test}
"dune-site"
"ppx_blob"
"lwt"
"cohttp-lwt-unix"
"yojson"
Expand Down
44 changes: 21 additions & 23 deletions dune
View file
Original file line number Diff line number Diff line change
@@ -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)
Expand Down
4 changes: 1 addition & 3 deletions dune-project
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,6 @@
(name asli)
(version 0.2.0)

(using dune_site 0.1)
(using menhir 2.0)

(package
Expand All @@ -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)
Expand Down
39 changes: 26 additions & 13 deletions libASL/arm_env.ml
View file
Original file line number Diff line number Diff line change
@@ -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
Expand Down
9 changes: 4 additions & 5 deletions libASL/dune
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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))
6 changes: 3 additions & 3 deletions libASL/loadASL.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
4 changes: 2 additions & 2 deletions tests/coverage/run.sh
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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 <data:[...]> with ./[...]
echo "$output" | sed 's#<data:\([^>]*\)>#./\1#g'

0 comments on commit 5dad8d5

Please sign in to comment.