From 794e845518d25073c80d48473b0e15036808d64e Mon Sep 17 00:00:00 2001 From: rina Date: Fri, 9 Feb 2024 15:13:10 +1000 Subject: [PATCH] Invert flag so aarch64 semantics are used by default. --- bin/asli.ml | 26 +++++++++++++++++--------- libASL/eval.ml | 29 ++++++++++++++++------------- 2 files changed, 33 insertions(+), 22 deletions(-) diff --git a/bin/asli.ml b/bin/asli.ml index 128ae64b..3949c25c 100644 --- a/bin/asli.ml +++ b/bin/asli.ml @@ -22,7 +22,7 @@ module AST = Asl_ast let opt_prelude : string ref = ref "prelude.asl" let opt_filenames : string list ref = ref [] let opt_print_version = ref false -let opt_use_default_aarch64 = ref false +let opt_no_default_aarch64 = ref false let opt_verbose = ref false let opt_debug_level = ref 0 @@ -290,7 +290,7 @@ let rec repl (tcenv: TC.Env.t) (cpu: Cpu.cpu): unit = let options = Arg.align ([ ( "-x", Arg.Set_int opt_debug_level, " Debugging output"); ( "-v", Arg.Set opt_verbose, " Verbose output"); - ( "--aarch64", Arg.Set opt_use_default_aarch64 , " Use bundled AArch64 Semantics"); + ( "--no-aarch64", Arg.Set opt_no_default_aarch64 , " Disable bundled AArch64 semantics"); ( "--version", Arg.Set opt_print_version, " Print version"); ( "--prelude", Arg.Set_string opt_prelude," ASL prelude file (default: ./prelude.asl)"); ] ) @@ -321,12 +321,20 @@ let main () = else begin if !opt_verbose then List.iter print_endline banner; if !opt_verbose then print_endline "\nType :? for help"; - let env = (match (if (!opt_use_default_aarch64) - then (aarch64_evaluation_environment ()) - else (evaluation_environment !opt_prelude !opt_filenames !opt_verbose)) - with - | Some e -> e - | None -> failwith "Unable to load bundled ASL.") in + let env_opt = + if (!opt_no_default_aarch64) + then evaluation_environment !opt_prelude !opt_filenames !opt_verbose + else begin + if List.length (!opt_filenames) != 0 then + Printf.printf + "Warning: asl file arguments ignored without --no-aarch64 (%s)\n" + (String.concat " " !opt_filenames) + else (); + aarch64_evaluation_environment ~verbose:!opt_verbose () + end in + let env = (match env_opt with + | Some e -> e + | None -> failwith "Unable build evaluation environment.") in if !opt_verbose then Printf.printf "Built evaluation environment\n"; Dis.debug_level := !opt_debug_level; @@ -340,7 +348,7 @@ let main () = repl tcenv cpu end -let _ =ignore(main ()) +let _ = ignore (main ()) (**************************************************************** * End diff --git a/libASL/eval.ml b/libASL/eval.ml index 7a055324..cfd31e59 100644 --- a/libASL/eval.ml +++ b/libASL/eval.ml @@ -1335,19 +1335,22 @@ let evaluation_environment (prelude: string) (files: string list) (verbose: bool None ) - -let aarch64_evaluation_environment (): Env.t 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/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 - let aarch64_default_asl_files : string option = match (Res.Sites.aslfiles) with - | hd :: _ -> Some hd - | _ -> None in - Option.bind aarch64_default_asl_files (fun s -> ( - (let filenames = List.map (fun file -> Filename.concat s file) aarch64_file_load_order in - let prelude = Filename.concat s "prelude.asl" in - (evaluation_environment prelude filenames false)))) +let aarch64_asl_files: (string * string 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/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 match Res.Sites.aslfiles with + | [dir] -> + let filenames = List.map (Filename.concat dir) aarch64_file_load_order in + let prelude = Filename.concat dir "prelude.asl" in + Some (prelude, filenames) + | _ -> None + +let aarch64_evaluation_environment ?(verbose = false) (): Env.t option = + Option.bind aarch64_asl_files + (fun (prelude, filenames) -> evaluation_environment prelude filenames verbose) (**************************************************************** * End