From 9b14c90fce051cc7bd46a49394d998104e911d6d Mon Sep 17 00:00:00 2001 From: Kait Lam Date: Mon, 24 Jun 2024 11:39:30 +1000 Subject: [PATCH] Embed ARM ASL specs within OCaml (#92) * extract arm environment into separate file. * allow loading files from either disk or memory * use ppx_blob to embed ASL files instead of dune-site This is instead of installing the ASL files to disk. This should make the installation less liable to random breakages when installed or linked in an unexpected way. The binary size increases by 6MB. Updates tests/coverage/run.sh to substitute away the new file paths of the embedded files, so no coverage re-generation needed. * replace --aarch64-dir with --export-aarch64 this is more useful once the MRA files are bundled. --- asli.opam | 2 +- bin/asli.ml | 19 +++++----- bin/offline_coverage.ml | 6 +--- bin/server.ml | 2 +- dune | 44 +++++++++++------------ dune-project | 4 +-- libASL/arm_env.ml | 34 ++++++++++++++++++ libASL/dune | 13 ++++--- libASL/eval.ml | 53 ++++++++++------------------ libASL/loadASL.ml | 77 ++++++++++++++++++++++++++++------------- libASL/loadASL.mli | 12 +++++-- libASL/utils.ml | 9 +++++ tests/coverage/run.sh | 4 +-- tests/test_asl.ml | 4 +-- 14 files changed, 168 insertions(+), 115 deletions(-) create mode 100644 libASL/arm_env.ml diff --git a/asli.opam b/asli.opam index b412139c..4a09e8ae 100644 --- a/asli.opam +++ b/asli.opam @@ -25,7 +25,7 @@ depends: [ "zarith" "z3" {>= "4.8.7"} "alcotest" {with-test} - "dune-site" + "ppx_blob" "lwt" "cohttp-lwt-unix" "yojson" diff --git a/bin/asli.ml b/bin/asli.ml index c00ae2bc..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,25 +338,26 @@ let _ = let main () = if !opt_print_version then Printf.printf "%s\n" version - else if !opt_print_aarch64_dir then - match 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"; + let sources = List.map (fun x -> LoadASL.FileSource x) !opt_filenames in (* 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 + then evaluation_environment (FileSource !opt_prelude) sources !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 (); + Arm_env.aarch64_evaluation_environment ~verbose:!opt_verbose (); end in let env = (match env_opt with diff --git a/bin/offline_coverage.ml b/bin/offline_coverage.ml index 147d6dc8..6263b6f0 100644 --- a/bin/offline_coverage.ml +++ b/bin/offline_coverage.ml @@ -84,13 +84,9 @@ let rec process_command tcenv env cmd = let main () = let opt_verbose = ref false in - let env = match Eval.aarch64_evaluation_environment ~verbose:!opt_verbose () with + let env = match Arm_env.aarch64_evaluation_environment ~verbose:!opt_verbose () with | Some e -> e | _ -> failwith "Unable to build evaluation environment." in - let filenames = Option.get Eval.aarch64_asl_files in - let prj_files = List.filter (fun f -> Utils.endswith f ".prj") (snd filenames) in - let tcenv = Tcheck.Env.mkEnv Tcheck.env0 in - List.iter (fun f -> process_command tcenv env (":project " ^ f)) prj_files; List.map (fun instr -> run opt_verbose instr env) !opt_instr let _ = ignore (main()) diff --git a/bin/server.ml b/bin/server.ml index fa28737d..77a14ba3 100644 --- a/bin/server.ml +++ b/bin/server.ml @@ -15,7 +15,7 @@ open Asl_utils open Lwt -let persistent_env = lazy (Option.get (aarch64_evaluation_environment ())) +let persistent_env = lazy (Option.get (Arm_env.aarch64_evaluation_environment ())) let eval_instr (opcode: string) : string = let pp_raw stmt : string = Utils.to_string (Asl_parser_pp.pp_raw_stmt stmt) |> String.trim in diff --git a/dune b/dune index 10c8b130..6347f813 100644 --- a/dune +++ b/dune @@ -1,26 +1,24 @@ -(install - (files - (prelude.asl as prelude.asl ) - (mra_tools/arch/arch.asl as mra_tools/arch/arch.asl ) - (mra_tools/arch/arch_decode.asl as mra_tools/arch/arch_decode.asl ) - (mra_tools/arch/arch_instrs.asl as mra_tools/arch/arch_instrs.asl ) - (mra_tools/arch/regs.asl as mra_tools/arch/regs.asl ) - (mra_tools/arch/regs_access.asl as mra_tools/arch/regs_access.asl ) - (mra_tools/support/aes.asl as mra_tools/support/aes.asl ) - (mra_tools/support/barriers.asl as mra_tools/support/barriers.asl ) - (mra_tools/support/debug.asl as mra_tools/support/debug.asl ) - (mra_tools/support/feature.asl as mra_tools/support/feature.asl ) - (mra_tools/support/fetchdecode.asl as mra_tools/support/fetchdecode.asl) - (mra_tools/support/hints.asl as mra_tools/support/hints.asl ) - (mra_tools/support/interrupts.asl as mra_tools/support/interrupts.asl ) - (mra_tools/support/memory.asl as mra_tools/support/memory.asl ) - (mra_tools/support/stubs.asl as mra_tools/support/stubs.asl ) - (mra_tools/types.asl as mra_tools/types.asl ) - (tests/override.asl as tests/override.asl ) - (tests/override.prj as tests/override.prj ) - ) - (section (site (asli aslfiles))) - ) +(alias + (name asl_files) + (deps + prelude.asl + mra_tools/arch/arch.asl + mra_tools/arch/arch_decode.asl + mra_tools/arch/arch_instrs.asl + mra_tools/arch/regs.asl + mra_tools/arch/regs_access.asl + mra_tools/support/aes.asl + mra_tools/support/barriers.asl + mra_tools/support/debug.asl + mra_tools/support/feature.asl + mra_tools/support/fetchdecode.asl + mra_tools/support/hints.asl + mra_tools/support/interrupts.asl + mra_tools/support/memory.asl + mra_tools/support/stubs.asl + mra_tools/types.asl + tests/override.asl + tests/override.prj)) (alias (name default) diff --git a/dune-project b/dune-project index f8c331a1..f57814cc 100644 --- a/dune-project +++ b/dune-project @@ -2,7 +2,6 @@ (name asli) (version 0.2.0) -(using dune_site 0.1) (using menhir 2.0) (package @@ -24,12 +23,11 @@ "zarith" ("z3" (>= "4.8.7")) ("alcotest" :with-test) - "dune-site" + "ppx_blob" "lwt" "cohttp-lwt-unix" "yojson" ) - (sites (share aslfiles)) ) (license BSD-3-Clause) diff --git a/libASL/arm_env.ml b/libASL/arm_env.ml new file mode 100644 index 00000000..78557f67 --- /dev/null +++ b/libASL/arm_env.ml @@ -0,0 +1,34 @@ +(* defines the evaluation environment for the bundled Arm spsecifications. *) + +let aarch64_asl_dir: string option = + None + +let prelude_blob : LoadASL.source = DataSource ("prelude.asl", [%blob "../prelude.asl"]) + +let asl_blobs : LoadASL.source list = [ + DataSource ("mra_tools/arch/regs.asl", [%blob "../mra_tools/arch/regs.asl"]); + DataSource ("mra_tools/types.asl", [%blob "../mra_tools/types.asl"]); + DataSource ("mra_tools/arch/arch.asl", [%blob "../mra_tools/arch/arch.asl"]); + DataSource ("mra_tools/arch/arch_instrs.asl", [%blob "../mra_tools/arch/arch_instrs.asl"]); + DataSource ("mra_tools/arch/regs_access.asl", [%blob "../mra_tools/arch/regs_access.asl"]); + DataSource ("mra_tools/arch/arch_decode.asl", [%blob "../mra_tools/arch/arch_decode.asl"]); + DataSource ("mra_tools/support/aes.asl", [%blob "../mra_tools/support/aes.asl"]); + DataSource ("mra_tools/support/barriers.asl", [%blob "../mra_tools/support/barriers.asl"]); + DataSource ("mra_tools/support/debug.asl", [%blob "../mra_tools/support/debug.asl";]); + DataSource ("mra_tools/support/feature.asl", [%blob "../mra_tools/support/feature.asl"]); + DataSource ("mra_tools/support/hints.asl", [%blob "../mra_tools/support/hints.asl"]); + DataSource ("mra_tools/support/interrupts.asl", [%blob "../mra_tools/support/interrupts.asl"]); + DataSource ("mra_tools/support/memory.asl", [%blob "../mra_tools/support/memory.asl";]); + DataSource ("mra_tools/support/stubs.asl", [%blob "../mra_tools/support/stubs.asl"]); + DataSource ("mra_tools/support/fetchdecode.asl", [%blob "../mra_tools/support/fetchdecode.asl"]); + DataSource ("tests/override.asl", [%blob "../tests/override.asl"]); + DataSource ("tests/override.prj", [%blob "../tests/override.prj"]); +] + +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/dune b/libASL/dune index b812b0b9..1ca4d24a 100644 --- a/libASL/dune +++ b/libASL/dune @@ -28,13 +28,12 @@ (flags (:standard -w -27 -cclib -lstdc++)) (modules cpu dis elf eval - lexer lexersupport loadASL monad primops rws symbolic tcheck testing transforms value res + lexer lexersupport loadASL monad primops rws symbolic tcheck testing transforms value symbolic_lifter decoder_program call_graph req_analysis - offline_transform ocaml_backend dis_tc - offline_opt + offline_transform ocaml_backend dis_tc offline_opt + arm_env ) - (libraries libASL_support (re_export libASL_ast) str dune-site)) + (preprocessor_deps (alias ../asl_files)) + (preprocess (pps ppx_blob)) + (libraries libASL_support (re_export libASL_ast) str)) -(generate_sites_module - (module res) - (sites asli)) diff --git a/libASL/eval.ml b/libASL/eval.ml index 64a25013..882c6208 100644 --- a/libASL/eval.ml +++ b/libASL/eval.ml @@ -1319,34 +1319,37 @@ let set_impdef (tcenv: Tcheck.Env.t) (env: Env.t) (fname: string) (rest: string 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 +let evaluate_prj_minimal (tcenv: Tcheck.Env.t) (env: Env.t) (source: LoadASL.source) = + let data = LoadASL.read_source source in + let fname = LoadASL.pp_source source in + let lines = List.map String.trim @@ String.split_on_char '\n' data in + List.iter + (fun line -> 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 + | _ -> failwith @@ "Unrecognised minimal .prj line in " ^ fname ^ ": " ^ line) + lines (** 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 -> +let evaluation_environment (prelude: LoadASL.source) (files: LoadASL.source list) (verbose: bool) = + let t = LoadASL.read_file (prelude) true verbose in + let ts = List.map (fun file -> + let filename = LoadASL.name_of_source file in if Utils.endswith filename ".spec" then begin - LoadASL.read_spec filename verbose + LoadASL.read_spec file verbose end else if Utils.endswith filename ".asl" then begin - LoadASL.read_file filename false verbose + LoadASL.read_file file 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) + failwith ("Unrecognized file suffix on "^(LoadASL.pp_source file)) end ) files in - let prjs = List.filter (fun fname -> Utils.endswith fname ".prj") files in + + let prjs = List.filter + (fun fname -> Utils.endswith (LoadASL.name_of_source fname) ".prj") + files in if verbose then Printf.printf "Building evaluation environment\n"; let env = ( @@ -1361,24 +1364,6 @@ let evaluation_environment (prelude: string) (files: string list) (verbose: bool env -let aarch64_asl_dir: string option = - List.nth_opt Res.Sites.aslfiles 0 - -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/regs_access.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 Option.bind aarch64_asl_dir (fun dir -> - let filenames = List.map (Filename.concat dir) aarch64_file_load_order in - let prelude = Filename.concat dir "prelude.asl" in - Some (prelude, filenames)) - -let aarch64_evaluation_environment ?(verbose = false) (): Env.t option = - Option.bind aarch64_asl_files - (fun (prelude, filenames) -> evaluation_environment prelude filenames verbose) - (**************************************************************** * End ****************************************************************) diff --git a/libASL/loadASL.ml b/libASL/loadASL.ml index 3b06ed79..3c30be1a 100644 --- a/libASL/loadASL.ml +++ b/libASL/loadASL.ml @@ -23,6 +23,42 @@ let mkLoc (fname: string) (input: string): AST.l = let finish: Lexing.position = { pos_fname = fname; pos_lnum = 1; pos_bol = 0; pos_cnum = len } in AST.Range (start, finish) +(** a source of data which may be a file on disk or a byte string in memory. *) +type source = FileSource of string | DataSource of string * string + +let pp_source = function | FileSource s -> s | DataSource (name, _) -> "" + +let name_of_source = function | FileSource s | DataSource (s, _) -> s + +(** opens a variant source. + returns (lexbuf, closer) where closer should be called to close the source. *) +let open_source source = match source with + | FileSource filename -> + let inchan = open_in filename in + let lexbuf = Lexing.from_channel inchan in + lexbuf.lex_curr_p <- { lexbuf.lex_curr_p with pos_fname = pp_source source }; + (lexbuf, fun () -> close_in inchan) + | DataSource (filename, data) -> + let lexbuf = Lexing.from_string data in + lexbuf.lex_curr_p <- { lexbuf.lex_curr_p with pos_fname = pp_source source }; + (lexbuf, Fun.id) + +let read_source = function + | FileSource filename -> + let inchan = open_in_bin filename in + let x = really_input_string inchan (in_channel_length inchan) in + close_in inchan; + 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 @@ -92,10 +128,8 @@ let declare_var_getters (decls: declaration list) = in List.map declare decls -let parse_file (filename : string) (isPrelude: bool) (verbose: bool): AST.declaration list = - let inchan = open_in filename in - let lexbuf = Lexing.from_channel inchan in - lexbuf.lex_curr_p <- { lexbuf.lex_curr_p with pos_fname = filename }; +let parse_file (filename : source) (isPrelude: bool) (verbose: bool): AST.declaration list = + let (lexbuf, close) = open_source filename in let t = report_parse_error (fun _ -> print_endline (pp_loc (Range (lexbuf.lex_start_p, lexbuf.lex_curr_p))); exit 1) @@ -104,46 +138,39 @@ let parse_file (filename : string) (isPrelude: bool) (verbose: bool): AST.declar let lexer = offside_token Lexer.token in (* Run the parser on this line of input. *) - if verbose then Printf.printf "- Parsing %s\n" filename; + if verbose then Printf.printf "- Parsing %s\n" (pp_source filename); Parser.declarations_start lexer lexbuf) in - close_in inchan; + close (); declare_var_getters t -let read_file (filename : string) (isPrelude: bool) (verbose: bool): AST.declaration list = - if verbose then Printf.printf "Processing %s\n" filename; +let read_file (filename : source) (isPrelude: bool) (verbose: bool): AST.declaration list = + if verbose then Printf.printf "Processing %s\n" (pp_source filename); let t = parse_file filename isPrelude verbose in if false then PPrint.ToChannel.pretty 1.0 60 stdout (PP.pp_declarations t); - if verbose then Printf.printf " - Got %d declarations from %s\n" (List.length t) filename; + if verbose then Printf.printf " - Got %d declarations from %s\n" (List.length t) (pp_source filename); let t' = report_type_error (fun _ -> exit 1) (fun _ -> - if verbose then Printf.printf "- Typechecking %s\n" filename; + if verbose then Printf.printf "- Typechecking %s\n" (pp_source filename); TC.tc_declarations isPrelude t ) in if false then PPrint.ToChannel.pretty 1.0 60 stdout (PP.pp_declarations t'); - if verbose then Printf.printf " - Got %d typechecked declarations from %s\n" (List.length t') filename; + if verbose then Printf.printf " - Got %d typechecked declarations from %s\n" (List.length t') (pp_source filename); - if verbose then Printf.printf "Finished %s\n" filename; + if verbose then Printf.printf "Finished %s\n" (pp_source filename); flush stdout; t' -let read_spec (filename : string) (verbose: bool): AST.declaration list = - let r: AST.declaration list list ref = ref [] in - let inchan = open_in filename in - (try - while true do - let t = read_file (input_line inchan) false verbose in - r := t :: !r - done - with - | End_of_file -> - close_in inchan - ); - List.concat (List.rev !r) +let read_spec (filename : source) (verbose: bool): AST.declaration list = + let specfile = read_source filename in + let lines = String.split_on_char '\n' specfile + |> List.map String.trim + |> List.filter (fun x -> x <> "") in + List.concat_map (fun f -> read_file (FileSource f) false verbose) lines let read_impdef (tcenv: TC.Env.t) (loc: AST.l) (s: string): (string * AST.expr) = let lexbuf = Lexing.from_string s in diff --git a/libASL/loadASL.mli b/libASL/loadASL.mli index 7e1810f8..c9ef75fc 100644 --- a/libASL/loadASL.mli +++ b/libASL/loadASL.mli @@ -8,6 +8,12 @@ module AST = Asl_ast module TC = Tcheck +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 val report_parse_error : (unit -> 'a) -> (unit -> 'a) -> 'a @@ -15,12 +21,12 @@ val report_type_error : (unit -> 'a) -> (unit -> 'a) -> 'a val report_eval_error : (unit -> 'a) -> (unit -> 'a) -> 'a (** Parse and typecheck ASL file *) -val read_file : string -> bool -> bool -> Asl_ast.declaration list +val read_file : source -> bool -> bool -> Asl_ast.declaration list -val read_spec : string -> bool -> Asl_ast.declaration list +val read_spec : source -> bool -> Asl_ast.declaration list (** Parse ASL file, but do not typecheck *) -val parse_file : string -> bool -> bool -> Asl_ast.declaration list +val parse_file : source -> bool -> bool -> Asl_ast.declaration list val read_impdef : TC.Env.t -> AST.l -> string -> (string * AST.expr) val read_expr : TC.Env.t -> AST.l -> string -> AST.expr 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 ****************************************************************) diff --git a/tests/coverage/run.sh b/tests/coverage/run.sh index 0b9eebac..375dfdd4 100755 --- a/tests/coverage/run.sh +++ b/tests/coverage/run.sh @@ -2,7 +2,7 @@ pattern="${1:?requires regex pattern as first argument}" -asl_dir="$(asli --aarch64-dir)" output="$(echo ":coverage A64 $pattern" | asli)" -echo "$output" | sed "s#$asl_dir#.#g" +# substitute paths of the form with ./[...] +echo "$output" | sed 's#]*\)>#./\1#g' diff --git a/tests/test_asl.ml b/tests/test_asl.ml index cb35f83b..7b437558 100644 --- a/tests/test_asl.ml +++ b/tests/test_asl.ml @@ -12,7 +12,7 @@ open AST module TC = Tcheck module AST = Asl_ast -let mra_tools () = [ +let mra_tools () = List.map (fun x -> LoadASL.FileSource x) [ "../../../mra_tools/arch/regs.asl"; "../../../mra_tools/types.asl"; "../../../mra_tools/arch/arch.asl"; @@ -99,7 +99,7 @@ let test_compare env () : unit = ) let tests : unit Alcotest.test_case list = - let prelude = LoadASL.read_file "../../../prelude.asl" true false in + let prelude = LoadASL.read_file (FileSource "../../../prelude.asl") true false in let mra = List.map (fun tool -> LoadASL.read_file tool false false) (mra_tools ()) in let tcenv = TC.Env.mkEnv TC.env0 in let env = Eval.build_evaluation_environment (prelude @ List.concat mra) in