Skip to content

Commit

Permalink
Invert flag so aarch64 semantics are used by default.
Browse files Browse the repository at this point in the history
  • Loading branch information
katrinafyi committed Feb 9, 2024
1 parent eb58d39 commit 1f40b75
Show file tree
Hide file tree
Showing 2 changed files with 33 additions and 22 deletions.
26 changes: 17 additions & 9 deletions bin/asli.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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)");
] )
Expand Down Expand Up @@ -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 to build evaluation environment.") in
if !opt_verbose then Printf.printf "Built evaluation environment\n";
Dis.debug_level := !opt_debug_level;

Expand All @@ -340,7 +348,7 @@ let main () =
repl tcenv cpu
end

let _ =ignore(main ())
let _ = ignore (main ())

(****************************************************************
* End
Expand Down
29 changes: 16 additions & 13 deletions libASL/eval.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down

0 comments on commit 1f40b75

Please sign in to comment.