Skip to content

Commit

Permalink
move default asl loading to libASL
Browse files Browse the repository at this point in the history
  • Loading branch information
@ailrst
ailrst committed Feb 8, 2024
1 parent 4b8faf8 commit eb58d39
Show file tree
Hide file tree
Showing 4 changed files with 59 additions and 48 deletions.
51 changes: 10 additions & 41 deletions bin/asli.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -19,25 +19,15 @@ module TC = Tcheck
module PP = Asl_parser_pp
module AST = Asl_ast

let opt_prelude : string ref = ref ""
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_verbose = ref false

let opt_debug_level = ref 0


let 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"]


let default_asl_files : string option = match (Res.Sites.aslfiles) with
| hd :: _ -> Some hd
| _ -> None


let () = Printexc.register_printer
(function
| Value.EvalError (loc, msg) ->
Expand Down Expand Up @@ -300,6 +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");
( "--version", Arg.Set opt_print_version, " Print version");
( "--prelude", Arg.Set_string opt_prelude," ASL prelude file (default: ./prelude.asl)");
] )
Expand All @@ -324,40 +315,18 @@ let _ =
(fun s -> opt_filenames := (!opt_filenames) @ [s])
usage_msg


let main () =
if !opt_print_version then Printf.printf "%s\n" version
else begin
if (List.length !opt_filenames) == 0 then
(opt_filenames := match default_asl_files with
| Some s -> List.map (fun file -> (s) ^ "/" ^ (file)) file_load_order
| None -> []);
if (!opt_prelude == "") then opt_prelude := (match default_asl_files with
| Some s -> s ^ "/"
| None -> "") ^ "prelude.asl";
if !opt_verbose then List.iter print_endline banner;
if !opt_verbose then print_endline "\nType :? for help";
let t = LoadASL.read_file !opt_prelude true !opt_verbose in
let ts = List.map (fun filename ->
if Utils.endswith filename ".spec" then begin
LoadASL.read_spec filename !opt_verbose
end else if Utils.endswith filename ".asl" then begin
LoadASL.read_file filename false !opt_verbose
end else if Utils.endswith filename ".prj" then begin
[] (* ignore project files here and process later *)
end else begin
failwith ("Unrecognized file suffix on "^filename)
end
) !opt_filenames
in

if !opt_verbose then Printf.printf "Building evaluation environment\n";
let env = (try
Eval.build_evaluation_environment (List.concat (t::ts))
with
| Value.EvalError (loc, msg) ->
Printf.printf " %s: Evaluation error: %s\n" (pp_loc loc) msg;
exit 1
) in
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
if !opt_verbose then Printf.printf "Built evaluation environment\n";
Dis.debug_level := !opt_debug_level;

Expand Down
7 changes: 2 additions & 5 deletions bin/dune
View file
Original file line number Diff line number Diff line change
Expand Up @@ -3,9 +3,9 @@
(name asli)
(public_name asli)
(modes exe byte)
(modules asli res)
(modules asli)
(flags (-cclib -lstdc++))
(libraries libASL linenoise pprint pcre dune-site)
(libraries libASL linenoise pprint pcre)
)

(executable
Expand All @@ -24,6 +24,3 @@
(flags (-cclib -lstdc++))
(libraries libASL unix))

(generate_sites_module
(module res)
(sites asli))
8 changes: 6 additions & 2 deletions libASL/dune
View file
Original file line number Diff line number Diff line change
Expand Up @@ -19,5 +19,9 @@
(flags
(:standard -w -27 -cclib -lstdc++))
(modules asl_ast asl_parser asl_parser_pp asl_utils asl_visitor cpu dis elf eval
lexer lexersupport loadASL monad primops rws symbolic tcheck testing transforms utils value visitor)
(libraries pprint zarith z3 str pcre))
lexer lexersupport loadASL monad primops rws symbolic tcheck testing transforms utils value visitor res)
(libraries pprint zarith z3 str pcre dune-site))

(generate_sites_module
(module res)
(sites asli))
41 changes: 41 additions & 0 deletions libASL/eval.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1183,6 +1183,8 @@ and eval_encoding (env: Env.t) (x: encoding) (op: value): bool =
false
end



(****************************************************************)
(** {2 Creating environment from global declarations} *)
(****************************************************************)
Expand Down Expand Up @@ -1308,6 +1310,45 @@ let build_evaluation_environment (ds: AST.declaration list): Env.t = begin
end




let evaluation_environment (prelude: string) (files: string list) (verbose: bool) =
let t = LoadASL.read_file prelude true verbose in
let ts = List.map (fun filename ->
if Utils.endswith filename ".spec" then begin
LoadASL.read_spec filename verbose
end else if Utils.endswith filename ".asl" then begin
LoadASL.read_file filename false verbose
end else if Utils.endswith filename ".prj" then begin
[] (* ignore project files here and process later *)
end else begin
failwith ("Unrecognized file suffix on "^filename)
end
) files
in
if verbose then Printf.printf "Building evaluation environment\n";
(try
Some (build_evaluation_environment (List.concat (t::ts)))
with
| Value.EvalError (loc, msg) ->
Printf.printf " %s: Evaluation error: %s\n" (pp_loc loc) msg;
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))))

(****************************************************************
* End
****************************************************************)

0 comments on commit eb58d39

Please sign in to comment.