From 7d1d7eaaede4dee972aa0fd23f3b7d4b1a9f2bc7 Mon Sep 17 00:00:00 2001 From: rina Date: Fri, 21 Jun 2024 18:19:44 +1000 Subject: [PATCH] replace --aarch64-dir with --export-aarch64 this is more useful once the MRA files are bundled. --- bin/asli.ml | 14 +++++++------- libASL/arm_env.ml | 1 - libASL/loadASL.ml | 9 +++++++++ libASL/loadASL.mli | 1 + libASL/utils.ml | 9 +++++++++ 5 files changed, 26 insertions(+), 8 deletions(-) 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 ****************************************************************)