Skip to content

Commit

Permalink
use ppx_blob to embed mra files
Browse files Browse the repository at this point in the history
  • Loading branch information
katrinafyi committed Jun 21, 2024
1 parent 21aaebf commit 9a960ce
Show file tree
Hide file tree
Showing 5 changed files with 31 additions and 15 deletions.
1 change: 1 addition & 0 deletions asli.opam
Original file line number Diff line number Diff line change
Expand Up @@ -30,6 +30,7 @@ depends: [
"lwt"
"cohttp-lwt-unix"
"yojson"
"ppx_blob"
"odoc" {with-doc}
]
build: [
Expand Down
1 change: 1 addition & 0 deletions dune-project
Original file line number Diff line number Diff line change
Expand Up @@ -29,6 +29,7 @@
"lwt"
"cohttp-lwt-unix"
"yojson"
"ppx_blob"
)
(sites (share aslfiles))
)
Expand Down
37 changes: 25 additions & 12 deletions libASL/arm_env.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
1 change: 1 addition & 0 deletions libASL/dune
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
6 changes: 3 additions & 3 deletions libASL/loadASL.ml
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

0 comments on commit 9a960ce

Please sign in to comment.