From 1ef6942253a297b593fd73d9ca252fcbe1a995da Mon Sep 17 00:00:00 2001 From: Kait Lam Date: Tue, 18 Jun 2024 12:36:09 +1000 Subject: [PATCH] support a subset of .prj syntax in the pre-built aarch64 env (#86) This allows downstream API users (e.g. gtirb-semantics) to have correct implementation-defined values, as set in override.prj. The supported subset is currently only `:set impdef "IMPDEF NAME" = TRUE` or similar. --- bin/asli.ml | 23 +++++++--------------- libASL/eval.ml | 49 ++++++++++++++++++++++++++++++++++------------ libASL/loadASL.ml | 8 ++++++++ libASL/loadASL.mli | 2 ++ 4 files changed, 54 insertions(+), 28 deletions(-) diff --git a/bin/asli.ml b/bin/asli.ml index aae3f506..c00ae2bc 100644 --- a/bin/asli.ml +++ b/bin/asli.ml @@ -68,12 +68,6 @@ let flags = [ ("eval:concrete_unknown", Value.concrete_unknown) ] -let mkLoc (fname: string) (input: string): AST.l = - let len = String.length input in - let start : Lexing.position = { pos_fname = fname; pos_lnum = 1; pos_bol = 0; pos_cnum = 0 } in - let finish: Lexing.position = { pos_fname = fname; pos_lnum = 1; pos_bol = 0; pos_cnum = len } in - AST.Range (start, finish) - let () = Random.self_init () let rec process_command (tcenv: TC.Env.t) (cpu: Cpu.cpu) (fname: string) (input0: string): unit = @@ -242,11 +236,7 @@ let rec process_command (tcenv: TC.Env.t) (cpu: Cpu.cpu) (fname: string) (input0 Marshal.to_channel chan (stmts : stmt list) []; close_out chan | (":set" :: "impdef" :: rest) -> - let cmd = String.concat " " rest in - let loc = mkLoc fname cmd in - let (x, e) = LoadASL.read_impdef tcenv loc cmd in - let v = Eval.eval_expr loc cpu.env e in - Eval.Env.setImpdef cpu.env x v + Eval.set_impdef tcenv cpu.env fname rest | [":set"; flag] when Utils.startswith flag "+" -> (match List.assoc_opt (Utils.stringDrop 1 flag) flags with | None -> Printf.printf "Unknown flag %s\n" flag; @@ -283,7 +273,7 @@ let rec process_command (tcenv: TC.Env.t) (cpu: Cpu.cpu) (fname: string) (input0 let s = LoadASL.read_stmt tcenv input in Eval.eval_stmt cpu.env s end else begin - let loc = mkLoc fname input in + let loc = LoadASL.mkLoc fname input in let e = LoadASL.read_expr tcenv loc input in let v = Eval.eval_expr loc cpu.env e in print_endline (Value.pp_value v) @@ -355,6 +345,8 @@ let main () = else begin if !opt_verbose then List.iter print_endline banner; if !opt_verbose then print_endline "\nType :? for help"; + + (* Note: .prj files are handled by `evaluation_environment`. *) let env_opt = if (!opt_no_default_aarch64) then evaluation_environment !opt_prelude !opt_filenames !opt_verbose @@ -366,20 +358,19 @@ let main () = 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 not !opt_no_default_aarch64 then - opt_filenames := snd (Option.get aarch64_asl_files); (* (!) should be safe if environment built successfully. *) + if !opt_verbose then Printf.printf "Built evaluation environment\n"; LNoise.history_load ~filename:"asl_history" |> ignore; LNoise.history_set ~max_length:100 |> ignore; let denv = Dis.build_env env in - let prj_files = List.filter (fun f -> Utils.endswith f ".prj") !opt_filenames in let tcenv = TC.Env.mkEnv TC.env0 and cpu = Cpu.mkCPU env denv in - List.iter (fun f -> process_command tcenv cpu "" (":project " ^ f)) prj_files; + repl tcenv cpu end diff --git a/libASL/eval.ml b/libASL/eval.ml index c72491f7..64a25013 100644 --- a/libASL/eval.ml +++ b/libASL/eval.ml @@ -1310,8 +1310,29 @@ let build_evaluation_environment (ds: AST.declaration list): Env.t = begin end - - +let set_impdef (tcenv: Tcheck.Env.t) (env: Env.t) (fname: string) (rest: string list) = + (* `rest` is of the form: "Has MTE extension" = FALSE *) + let cmd = String.concat " " rest in + let loc = LoadASL.mkLoc fname cmd in + let (x, e) = LoadASL.read_impdef tcenv loc cmd in + let v = eval_expr loc env e in + Env.setImpdef env x v + +(** Evaluates a minimal subset of the .prj syntax, sufficient for override.prj. *) +let evaluate_prj_minimal (tcenv: Tcheck.Env.t) (env: Env.t) (fname: string) = + let inchan = open_in fname in + try + while true do + let line = input_line inchan in + match (String.split_on_char ' ' line) with + | ":set" :: "impdef" :: rest -> set_impdef tcenv env fname rest + | empty when List.for_all (String.equal "") empty -> () (* ignore empty lines *) + | _ -> failwith @@ "Unrecognised minimal .prj line in " ^ fname ^ ": " ^ line + done + with | End_of_file -> close_in inchan + +(** Constructs an evaluation environment with the given prelude file and .asl/.prj files. + .prj files given here are required to be minimal. *) 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 -> @@ -1324,16 +1345,21 @@ let evaluation_environment (prelude: string) (files: string list) (verbose: bool end else begin failwith ("Unrecognized file suffix on "^filename) end - ) files - in + ) files in + let prjs = List.filter (fun fname -> Utils.endswith fname ".prj") 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 env = ( + 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 + ) in + + let tcenv = TC.Env.mkEnv Tcheck.env0 in + Option.iter (fun env -> List.iter (evaluate_prj_minimal tcenv env) prjs) env; + env + let aarch64_asl_dir: string option = List.nth_opt Res.Sites.aslfiles 0 @@ -1349,7 +1375,6 @@ let aarch64_asl_files: (string * string list) option = let prelude = Filename.concat dir "prelude.asl" in Some (prelude, filenames)) -(** XXX: .prj files NOT evaluated in this environment! *) let aarch64_evaluation_environment ?(verbose = false) (): Env.t option = Option.bind aarch64_asl_files (fun (prelude, filenames) -> evaluation_environment prelude filenames verbose) diff --git a/libASL/loadASL.ml b/libASL/loadASL.ml index ec9c22a2..3b06ed79 100644 --- a/libASL/loadASL.ml +++ b/libASL/loadASL.ml @@ -16,6 +16,14 @@ module AST = Asl_ast open Lexersupport open Lexing +(** Returns a new location corresponding to the given line occuring in the given file. *) +let mkLoc (fname: string) (input: string): AST.l = + let len = String.length input in + let start : Lexing.position = { pos_fname = fname; pos_lnum = 1; pos_bol = 0; pos_cnum = 0 } in + let finish: Lexing.position = { pos_fname = fname; pos_lnum = 1; pos_bol = 0; pos_cnum = len } in + AST.Range (start, finish) + + 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 d1b9e6d2..7e1810f8 100644 --- a/libASL/loadASL.mli +++ b/libASL/loadASL.mli @@ -8,6 +8,8 @@ module AST = Asl_ast module TC = Tcheck +val mkLoc : string -> string -> AST.l + val report_parse_error : (unit -> 'a) -> (unit -> 'a) -> 'a val report_type_error : (unit -> 'a) -> (unit -> 'a) -> 'a val report_eval_error : (unit -> 'a) -> (unit -> 'a) -> 'a