diff --git a/bin/asli.ml b/bin/asli.ml index ce7ab103..82d0da74 100644 --- a/bin/asli.ml +++ b/bin/asli.ml @@ -23,7 +23,7 @@ let opt_prelude : string ref = ref "prelude.asl" let opt_filenames : string list ref = ref [] let opt_print_version = ref false let opt_no_default_aarch64 = ref false -let opt_print_aarch64_dir = ref false +let opt_export_aarch64_dir = ref "" let opt_verbose = ref false @@ -309,8 +309,8 @@ let rec repl (tcenv: TC.Env.t) (cpu: Cpu.cpu): unit = let options = Arg.align ([ ( "-x", Arg.Set_int Dis.debug_level, " Partial evaluation debugging (requires debug level argument >= 0)"); ( "-v", Arg.Set opt_verbose, " Verbose output"); - ( "--no-aarch64", Arg.Set opt_no_default_aarch64 , " Disable bundled AArch64 semantics"); - ( "--aarch64-dir", Arg.Set opt_print_aarch64_dir, " Print directory of bundled AArch64 semantics"); + ( "--no-aarch64", Arg.Set opt_no_default_aarch64 , " Disable bundled AArch64 semantics"); + ( "--export-aarch64", Arg.Set_string opt_export_aarch64_dir, " Export bundled AArch64 MRA to the given directory"); ( "--version", Arg.Set opt_print_version, " Print version"); ( "--prelude", Arg.Set_string opt_prelude," ASL prelude file (default: ./prelude.asl)"); ] ) @@ -338,10 +338,10 @@ let _ = let main () = if !opt_print_version then Printf.printf "%s\n" version - else if !opt_print_aarch64_dir then - match Arm_env.aarch64_asl_dir with - | Some d -> Printf.printf "%s\n" d - | None -> (Printf.eprintf "Unable to retrieve installed asl directory\n"; exit 1) + else if "" <> !opt_export_aarch64_dir then + let dir = !opt_export_aarch64_dir in + ignore @@ Sys.readdir dir; + List.iter LoadASL.(write_source dir) Arm_env.(prelude_blob :: asl_blobs); else begin if !opt_verbose then List.iter print_endline banner; if !opt_verbose then print_endline "\nType :? for help"; diff --git a/libASL/arm_env.ml b/libASL/arm_env.ml index 3282137d..78557f67 100644 --- a/libASL/arm_env.ml +++ b/libASL/arm_env.ml @@ -28,7 +28,6 @@ let asl_blobs : LoadASL.source list = [ 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 (fun (prelude, filenames) -> Eval.evaluation_environment prelude filenames verbose) diff --git a/libASL/loadASL.ml b/libASL/loadASL.ml index 5c0d5b6a..3c30be1a 100644 --- a/libASL/loadASL.ml +++ b/libASL/loadASL.ml @@ -51,6 +51,15 @@ let read_source = function x | DataSource (_, data) -> data +let write_source prefix = function + | FileSource _ -> failwith "write_source for FileSource is unsupported" + | DataSource (name, data) -> + let name = Filename.concat prefix name in + Utils.mkdir_p (Filename.dirname name); + let chan = open_out_bin name in + output_string chan data; + close_out chan + let report_parse_error (on_error: unit -> 'a) (f: unit -> 'a): 'a = (try f () diff --git a/libASL/loadASL.mli b/libASL/loadASL.mli index 92504656..c9ef75fc 100644 --- a/libASL/loadASL.mli +++ b/libASL/loadASL.mli @@ -12,6 +12,7 @@ type source = FileSource of string | DataSource of string * string val pp_source : source -> string val name_of_source : source -> string val read_source : source -> string + val write_source : string -> source -> unit val mkLoc : string -> string -> AST.l diff --git a/libASL/utils.ml b/libASL/utils.ml index e71887df..cc0917c1 100644 --- a/libASL/utils.ml +++ b/libASL/utils.ml @@ -7,6 +7,15 @@ (** Generic utility functions *) +let rec mkdir_p p = + let open Filename in + if Sys.file_exists p then + () + else + (* make parents, then make final directory. *) + (mkdir_p (dirname p); Sys.mkdir p 0o755) + + (**************************************************************** * Pretty-printer related ****************************************************************) 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'