extract arm environment into separate file.

bin/asli.ml

@@ -339,7 +339,7 @@ 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 
+        match Arm_env.aarch64_asl_dir with 
         | Some d -> Printf.printf "%s\n" d
         | None -> (Printf.eprintf "Unable to retrieve installed asl directory\n"; exit 1)
     else begin
@@ -356,7 +356,7 @@ let main () =
                         "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 

bin/offline_coverage.ml

@@ -84,10 +84,10 @@ 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 filenames = Option.get Arm_env.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;

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

libASL/arm_env.ml

@@ -0,0 +1,20 @@
+(* defines the evaluation environment for the bundled Arm spsecifications. *)
+
+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) (): Eval.Env.t option = 
+    Option.bind aarch64_asl_files 
+        (fun (prelude, filenames) -> Eval.evaluation_environment prelude filenames verbose)
+

libASL/dune

@@ -22,8 +22,8 @@
  (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 res
    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 pprint zarith z3 str pcre  dune-site))
 

libASL/eval.ml

@@ -1361,24 +1361,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
  ****************************************************************)