diff --git a/asli.opam b/asli.opam
index 690da900..4a09e8ae 100644
--- a/asli.opam
+++ b/asli.opam
@@ -24,9 +24,8 @@ depends: [
   "pprint"
   "zarith"
   "z3" {>= "4.8.7"}
-  "pcre"
   "alcotest" {with-test}
-  "dune-site"
+  "ppx_blob"
   "lwt"
   "cohttp-lwt-unix"
   "yojson"
diff --git a/bin/asli.ml b/bin/asli.ml
index c00ae2bc..50d2b6be 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 
@@ -369,7 +370,7 @@ let main () =
         LNoise.history_set ~max_length:100 |> ignore;
         
         let denv = Dis.build_env env in
-        let tcenv = TC.Env.mkEnv TC.env0 and cpu = Cpu.mkCPU env denv in
+        let tcenv = TC.Env.mkEnv !TC.env0 and cpu = Cpu.mkCPU env denv in
 
         repl tcenv cpu
     end
diff --git a/bin/dune b/bin/dune
index 5927fafd..7b572c03 100644
--- a/bin/dune
+++ b/bin/dune
@@ -5,7 +5,7 @@
  (modes exe byte)
  (modules asli)
  (flags (-cclib -lstdc++))
- (libraries libASL linenoise pprint pcre)
+ (libraries asli.libASL linenoise pprint)
  )
 
 (executable
@@ -14,7 +14,7 @@
  (modes exe)
  (modules server)
  (flags (-cclib -lstdc++))
- (libraries libASL pprint pcre lwt.unix yojson cohttp-lwt cohttp-lwt-unix))
+ (libraries asli.libASL pprint lwt.unix yojson cohttp-lwt cohttp-lwt-unix))
 
 
 (executable
@@ -23,7 +23,7 @@
  ; (public_name test_asl_lexer)
  (modules testlexer)
  (flags (-cclib -lstdc++))
- (libraries libASL))
+ (libraries asli.libASL))
 
 (executable
  (name processops)
@@ -31,7 +31,7 @@
  ; (public_name test_asl_lexer)
  (modules processops)
  (flags (-cclib -lstdc++))
- (libraries libASL unix))
+ (libraries asli.libASL unix))
 
 (executable
  (name offline_coverage)
@@ -39,7 +39,7 @@
  (modes exe)
  (modules offline_coverage)
  (flags (-cclib -lstdc++))
- (libraries libASL offlineASL))
+ (libraries asli.libASL offlineASL))
 
 (executable
  (name offline_sem)
@@ -47,4 +47,4 @@
  (modes exe)
  (modules offline_sem)
  (flags (-cclib -lstdc++))
- (libraries libASL offlineASL))
+ (libraries asli.libASL offlineASL))
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 6b9b8780..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
@@ -23,14 +22,12 @@
     "pprint"
     "zarith"
     ("z3"        (>= "4.8.7"))
-    "pcre"
     ("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/decoder_program.ml b/libASL/decoder_program.ml
index 5558e71c..123352ba 100644
--- a/libASL/decoder_program.ml
+++ b/libASL/decoder_program.ml
@@ -116,10 +116,10 @@ let run iset pat env problematic =
 
   (* Find all matching instructions, pulled from testing.ml *)
   let decoder = Eval.Env.getDecoder env (Ident iset) in
-  let re = Pcre.regexp pat in
+  let re = Str.regexp pat in
   let filterfn = function
     | ((Encoding_Block (Ident nm, Ident is, _, _, _, _, _, _)),_,_,_) ->
-        is = iset && Pcre.pmatch ~rex:re nm && not (List.mem nm problematic)
+        is = iset && Str.string_match re nm 0 && not (List.mem nm problematic)
     | _ -> assert false
   in
   let encs = List.filter filterfn (Eval.Env.listInstructions env) in
diff --git a/libASL/dis.ml b/libASL/dis.ml
index b61ba338..0d2b3c22 100644
--- a/libASL/dis.ml
+++ b/libASL/dis.ml
@@ -180,7 +180,7 @@ module LocalEnv = struct
 
     let init (env: Eval.Env.t) =
         let eval e = val_expr (Eval.eval_expr Unknown env e) in
-        let tenv = Tcheck.env0 in
+        let tenv = !Tcheck.env0 in
         let get_global_type id =
             (match Tcheck.GlobalEnv.getGlobalVar tenv id with
             | Some (Type_Bits e) ->
@@ -642,7 +642,7 @@ and width_of_type (loc: l) (t: ty): int =
   | _ -> unsupported loc @@ "Can't get bit width of type: " ^ pp_type t
 
 and width_of_field (loc: l) (t: ty) (f: ident): int =
-  let env = Tcheck.env0 in
+  let env = !Tcheck.env0 in
   let ft =
     (match Tcheck.typeFields env loc t with
     | FT_Record rfs -> Tcheck.get_recordfield loc rfs f
@@ -654,7 +654,7 @@ and width_of_field (loc: l) (t: ty) (f: ident): int =
 
 (** Determine the type of memory access expression (Var, Array, Field) *)
 and type_of_load (loc: l) (x: expr): ty rws =
-  let env = Tcheck.env0 in
+  let env = !Tcheck.env0 in
   (match x with
   | Expr_Var(id) ->
       let+ (_,(t,_)) = DisEnv.gets (LocalEnv.resolveGetVar loc id) in
diff --git a/libASL/dune b/libASL/dune
index 6fae933e..0bb060c8 100644
--- a/libASL/dune
+++ b/libASL/dune
@@ -14,19 +14,46 @@
      (with-stdout-to asl_parser_tail.mly (bash "OTT=${ASLI_OTT:-$(opam config var ott:share)};  grep -v '^%%' $OTT/menhir_library_extra.mly"))
      (with-stdout-to asl_parser.mly (run cat asl_parser_head.mly asl_parser_tail.mly)))))
 
+; libASL is constructed in two stages: stage0, and stage1.
+; stage0 is the minimum needed to define an "expression", and stage1 is the rest.
+; this is so stage0 can be used as a dependency for the libASL_support virtual library
+; which provides flexibility on whether to link z3 (for native compilation) or not (for js compilation).
+; thus, everything after the type-checking phase is in stage1.
+; these stages are merged together in libASL_virtual and re-exported as "LibASL",
+; and asli.libASL provides a publicly available dummy library which additionally
+; links the native implementation of the support code.
+
 (library
- (name libASL)
- (public_name asli.libASL)
+ (name libASL_stage0)
+ (public_name asli.libASL-stage0)
+ (flags (:standard -w -27))
+ (modules asl_ast asl_parser asl_parser_pp asl_utils asl_visitor visitor utils)
+ (libraries pprint (re_export zarith)))
+
+(library
+ (name libASL_stage1)
+ (public_name asli.libASL-stage1)
  (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 res
+  (:standard -w -27 -cclib -lstdc++ -open LibASL_stage0))
+ (modules cpu dis elf eval
+   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 pprint zarith z3 str pcre  dune-site))
+ (preprocessor_deps (alias ../asl_files))
+ (preprocess (pps ppx_blob))
+ (libraries libASL_stage0 libASL_support str))
 
-(generate_sites_module
- (module res)
- (sites asli))
+(library
+ (name libASL_virtual)
+ (public_name asli.libASL-virtual)
+ (modules libASL)
+ (wrapped false) ; exports LibASL module
+ (libraries libASL_stage0 libASL_stage1))
+
+(library
+ (name libASL_dummy)
+ (public_name asli.libASL)
+ (modules)
+ (libraries (re_export libASL_virtual) libASL_support_native))
diff --git a/libASL/eval.ml b/libASL/eval.ml
index 64a25013..39859f6f 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 = (
@@ -1356,29 +1359,11 @@ let evaluation_environment (prelude: string) (files: string list) (verbose: bool
             None
     ) in
 
-    let tcenv = TC.Env.mkEnv Tcheck.env0 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
-
-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/libASL.ml b/libASL/libASL.ml
new file mode 100644
index 00000000..8427825d
--- /dev/null
+++ b/libASL/libASL.ml
@@ -0,0 +1,2 @@
+include LibASL_stage0
+include LibASL_stage1
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, _) -> "<data:" ^ 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/ocaml_backend.ml b/libASL/ocaml_backend.ml
index d6e421e2..7c1f725c 100644
--- a/libASL/ocaml_backend.ml
+++ b/libASL/ocaml_backend.ml
@@ -333,7 +333,7 @@ let write_fn name (ret_tyo,_,targs,args,_,body) st =
  ****************************************************************)
 
 let init_st oc = { depth = 0; skip_seq = false; oc ; ref_vars = IdentSet.empty } 
-let global_deps = ["Utils"]
+let global_deps = ["Offline_utils"]
 
 (* Write an instruction file, containing just the behaviour of one instructions *)
 let write_instr_file fn fnsig dir =
@@ -372,7 +372,8 @@ let write_decoder_file fn fnsig deps dir =
 (* Write the dune build file *)
 let write_dune_file files dir =
   let oc = open_out (dir ^ "/dune") in
-  Printf.fprintf oc "(library
+  Printf.fprintf oc "; AUTO-GENERATED BY OCAML BACKEND
+(library
   (name offlineASL)
   (flags
     (:standard -w -27 -w -33 -cclib -lstdc++))
@@ -381,10 +382,10 @@ let write_dune_file files dir =
     Printf.fprintf oc "    %s\n" (String.lowercase_ascii k)
   ) files;
   Printf.fprintf oc "  )
-  (libraries zarith libASL))";
+  (libraries asli.libASL))";
   close_out oc
 
-(* Write all of the above, expecting Utils.ml to already be present in dir *)
+(* Write all of the above, expecting offline_utils.ml to already be present in dir *)
 let run dfn dfnsig tests fns dir =
   let files = Bindings.fold (fun fn fnsig acc -> (write_instr_file fn fnsig dir)::acc) fns [] in
   let files = (write_test_file tests dir)::files in
diff --git a/libASL/support/dune b/libASL/support/dune
new file mode 100644
index 00000000..fc6ca707
--- /dev/null
+++ b/libASL/support/dune
@@ -0,0 +1,7 @@
+; provides platform-specific dependencies
+
+(library
+ (name libASL_support)
+ (public_name asli.libASL-support)
+ (libraries libASL_stage0)
+ (virtual_modules solver))
diff --git a/libASL/support/native/dune b/libASL/support/native/dune
new file mode 100644
index 00000000..3281f961
--- /dev/null
+++ b/libASL/support/native/dune
@@ -0,0 +1,5 @@
+(library
+ (name libASL_support_native)
+ (public_name asli.libASL-support-native)
+ (implements libASL_support)
+ (libraries z3 libASL_stage0))
diff --git a/libASL/support/native/solver.ml b/libASL/support/native/solver.ml
new file mode 100644
index 00000000..5611d7a3
--- /dev/null
+++ b/libASL/support/native/solver.ml
@@ -0,0 +1,79 @@
+(****************************************************************)
+(** {3 Z3 support code}                                         *)
+(****************************************************************)
+
+(** Convert ASL expression to Z3 expression.
+    This only copes with a limited set of operations: ==, +, -, * and DIV.
+    (It is possible that we will need to extend this list in the future but
+    it is sufficient for the current ASL specifications.)
+
+    The support for DIV is not sound - it is a hack needed to cope with
+    the way ASL code is written and generally needs a side condition
+    that the division is exact (no remainder).
+
+    ufs is a mutable list of conversions used to handle subexpressions
+    that cannot be translated.  We treat such subexpressions as
+    uninterpreted functions and add them to the 'ufs' list so that
+    we can reason that "F(x) == F(x)" without knowing "F".
+ *)
+
+module AST = LibASL_stage0.Asl_ast
+module Asl_utils = LibASL_stage0.Asl_utils
+
+let verbose = false
+
+let rec z3_of_expr (ctx: Z3.context) (ufs: (AST.expr * Z3.Expr.expr) list ref) (x: AST.expr): Z3.Expr.expr =
+    (match x with
+    | Expr_Var(v) ->
+        let intsort = Z3.Arithmetic.Integer.mk_sort ctx in
+        Z3.Expr.mk_const_s ctx (AST.pprint_ident v) intsort
+    | Expr_Parens y -> z3_of_expr ctx ufs y
+    | Expr_LitInt i -> Z3.Arithmetic.Integer.mk_numeral_s ctx i
+
+    (* todo: the following lines involving DIV are not sound *)
+    | Expr_TApply (FIdent ("mul_int",_), [], [Expr_TApply (FIdent ("fdiv_int",_), [], [a; b]); c]) when b = c -> z3_of_expr ctx ufs a
+    | Expr_TApply (FIdent ("mul_int",_), [], [a; Expr_TApply (FIdent ("fdiv_int",_), [], [b; c])]) when a = c -> z3_of_expr ctx ufs b
+    | Expr_TApply (FIdent ("add_int",_), [], [Expr_TApply (FIdent ("fdiv_int",_), [], [a1; b1]);
+                                         Expr_TApply (FIdent ("fdiv_int",_), [], [a2; b2])])
+         when a1 = a2 && b1 = b2 && b1 = Expr_LitInt "2"
+         -> z3_of_expr ctx ufs a1
+    | Expr_TApply (FIdent ("eq_int",_), [], [a; Expr_TApply (FIdent ("fdiv_int",_), [], [b; c])]) ->
+            Z3.Boolean.mk_eq ctx
+                (Z3.Arithmetic.mk_mul ctx [z3_of_expr ctx ufs c; z3_of_expr ctx ufs a])
+                (z3_of_expr ctx ufs b)
+
+    | Expr_TApply (FIdent ("add_int",_),  [], xs)    -> Z3.Arithmetic.mk_add ctx (List.map (z3_of_expr ctx ufs) xs)
+    | Expr_TApply (FIdent ("sub_int",_),  [], xs)    -> Z3.Arithmetic.mk_sub ctx (List.map (z3_of_expr ctx ufs) xs)
+    | Expr_TApply (FIdent ("mul_int",_),  [], xs)    -> Z3.Arithmetic.mk_mul ctx (List.map (z3_of_expr ctx ufs) xs)
+    | Expr_TApply (FIdent ("fdiv_int",_), [], [a;b]) -> Z3.Arithmetic.mk_div ctx (z3_of_expr ctx ufs a) (z3_of_expr ctx ufs b)
+    | Expr_TApply (FIdent ("eq_int",_),   [], [a;b]) -> Z3.Boolean.mk_eq ctx (z3_of_expr ctx ufs a) (z3_of_expr ctx ufs b)
+    | _ ->
+            if verbose then Printf.printf "    Unable to translate %s - using as uninterpreted function\n" (Asl_utils.pp_expr x);
+            let intsort = Z3.Arithmetic.Integer.mk_sort ctx in
+            (match List.assoc_opt x !ufs with
+            | None ->
+                    let uf = Z3.Expr.mk_fresh_const ctx "UNINTERPRETED" intsort in
+                    ufs := (x, uf) :: !ufs;
+                    uf
+            | Some uf ->
+                    uf
+            )
+    )
+
+(** check that bs => cs *)
+let check_constraints (bs: AST.expr list) (cs: AST.expr list): bool =
+    (* note that we rebuild the Z3 context each time.
+     * It is possible to share them across all invocations to save
+     * about 10% of execution time.
+     *)
+    let z3_ctx = Z3.mk_context [] in
+    let solver = Z3.Solver.mk_simple_solver z3_ctx in
+    let ufs = ref [] in (* uninterpreted function list *)
+    let bs' = List.map (z3_of_expr z3_ctx ufs) bs in
+    let cs' = List.map (z3_of_expr z3_ctx ufs) cs in
+    let p = Z3.Boolean.mk_implies z3_ctx (Z3.Boolean.mk_and z3_ctx bs') (Z3.Boolean.mk_and z3_ctx cs') in
+    if verbose then Printf.printf "      - Checking %s\n" (Z3.Expr.to_string p);
+    Z3.Solver.add solver [Z3.Boolean.mk_not z3_ctx p];
+    let q = Z3.Solver.check solver [] in
+    if q = SATISFIABLE then Printf.printf "Failed property %s\n" (Z3.Expr.to_string p);
+    q = UNSATISFIABLE
diff --git a/libASL/support/solver.mli b/libASL/support/solver.mli
new file mode 100644
index 00000000..88c3ed21
--- /dev/null
+++ b/libASL/support/solver.mli
@@ -0,0 +1,8 @@
+(****************************************************************)
+(** {3 Z3 support code}                                         *)
+(****************************************************************)
+
+open LibASL_stage0
+
+(** check that bs => cs *)
+val check_constraints : (Asl_ast.expr list) -> (Asl_ast.expr list) -> bool
diff --git a/libASL/tcheck.ml b/libASL/tcheck.ml
index 7a53c82a..b4086797 100644
--- a/libASL/tcheck.ml
+++ b/libASL/tcheck.ml
@@ -709,83 +709,14 @@ let rec simplify_expr (x: AST.expr): AST.expr =
 (** Perform simple constant folding of expressions within a type *)
 let simplify_type (x: AST.ty): AST.ty =
     let repl = new replaceExprClass (fun e -> Some (simplify_expr e)) in
-    Asl_visitor.visit_type repl x
-
+    Visitor.visit_type repl x
 
 (****************************************************************)
-(** {3 Z3 support code}                                         *)
+(** {3 Constraint solver entry point}                           *)
 (****************************************************************)
 
-(** Convert ASL expression to Z3 expression.
-    This only copes with a limited set of operations: ==, +, -, * and DIV.
-    (It is possible that we will need to extend this list in the future but
-    it is sufficient for the current ASL specifications.)
-
-    The support for DIV is not sound - it is a hack needed to cope with
-    the way ASL code is written and generally needs a side condition
-    that the division is exact (no remainder).
-
-    ufs is a mutable list of conversions used to handle subexpressions
-    that cannot be translated.  We treat such subexpressions as
-    uninterpreted functions and add them to the 'ufs' list so that
-    we can reason that "F(x) == F(x)" without knowing "F".
- *)
-
-let rec z3_of_expr (ctx: Z3.context) (ufs: (AST.expr * Z3.Expr.expr) list ref) (x: AST.expr): Z3.Expr.expr =
-    (match x with
-    | Expr_Var(v) ->
-        let intsort = Z3.Arithmetic.Integer.mk_sort ctx in
-        Z3.Expr.mk_const_s ctx (pprint_ident v) intsort
-    | Expr_Parens y -> z3_of_expr ctx ufs y
-    | Expr_LitInt i -> Z3.Arithmetic.Integer.mk_numeral_s ctx i
-
-    (* todo: the following lines involving DIV are not sound *)
-    | Expr_TApply (FIdent ("mul_int",_), [], [Expr_TApply (FIdent ("fdiv_int",_), [], [a; b]); c]) when b = c -> z3_of_expr ctx ufs a
-    | Expr_TApply (FIdent ("mul_int",_), [], [a; Expr_TApply (FIdent ("fdiv_int",_), [], [b; c])]) when a = c -> z3_of_expr ctx ufs b
-    | Expr_TApply (FIdent ("add_int",_), [], [Expr_TApply (FIdent ("fdiv_int",_), [], [a1; b1]);
-                                         Expr_TApply (FIdent ("fdiv_int",_), [], [a2; b2])])
-         when a1 = a2 && b1 = b2 && b1 = Expr_LitInt "2"
-         -> z3_of_expr ctx ufs a1
-    | Expr_TApply (FIdent ("eq_int",_), [], [a; Expr_TApply (FIdent ("fdiv_int",_), [], [b; c])]) ->
-            Z3.Boolean.mk_eq ctx
-                (Z3.Arithmetic.mk_mul ctx [z3_of_expr ctx ufs c; z3_of_expr ctx ufs a])
-                (z3_of_expr ctx ufs b)
-
-    | Expr_TApply (FIdent ("add_int",_),  [], xs)    -> Z3.Arithmetic.mk_add ctx (List.map (z3_of_expr ctx ufs) xs)
-    | Expr_TApply (FIdent ("sub_int",_),  [], xs)    -> Z3.Arithmetic.mk_sub ctx (List.map (z3_of_expr ctx ufs) xs)
-    | Expr_TApply (FIdent ("mul_int",_),  [], xs)    -> Z3.Arithmetic.mk_mul ctx (List.map (z3_of_expr ctx ufs) xs)
-    | Expr_TApply (FIdent ("fdiv_int",_), [], [a;b]) -> Z3.Arithmetic.mk_div ctx (z3_of_expr ctx ufs a) (z3_of_expr ctx ufs b)
-    | Expr_TApply (FIdent ("eq_int",_),   [], [a;b]) -> Z3.Boolean.mk_eq ctx (z3_of_expr ctx ufs a) (z3_of_expr ctx ufs b)
-    | _ ->
-            if verbose then Printf.printf "    Unable to translate %s - using as uninterpreted function\n" (pp_expr x);
-            let intsort = Z3.Arithmetic.Integer.mk_sort ctx in
-            (match List.assoc_opt x !ufs with
-            | None ->
-                    let uf = Z3.Expr.mk_fresh_const ctx "UNINTERPRETED" intsort in
-                    ufs := (x, uf) :: !ufs;
-                    uf
-            | Some uf ->
-                    uf
-            )
-    )
-
-(** check that bs => cs *)
 let check_constraints (bs: expr list) (cs: expr list): bool =
-    (* note that we rebuild the Z3 context each time.
-     * It is possible to share them across all invocations to save
-     * about 10% of execution time.
-     *)
-    let z3_ctx = Z3.mk_context [] in
-    let solver = Z3.Solver.mk_simple_solver z3_ctx in
-    let ufs = ref [] in (* uninterpreted function list *)
-    let bs' = List.map (z3_of_expr z3_ctx ufs) bs in
-    let cs' = List.map (z3_of_expr z3_ctx ufs) cs in
-    let p = Z3.Boolean.mk_implies z3_ctx (Z3.Boolean.mk_and z3_ctx bs') (Z3.Boolean.mk_and z3_ctx cs') in
-    if verbose then Printf.printf "      - Checking %s\n" (Z3.Expr.to_string p);
-    Z3.Solver.add solver [Z3.Boolean.mk_not z3_ctx p];
-    let q = Z3.Solver.check solver [] in
-    if q = SATISFIABLE then Printf.printf "Failed property %s\n" (Z3.Expr.to_string p);
-    q = UNSATISFIABLE
+    LibASL_support.Solver.check_constraints bs cs
 
 
 (****************************************************************)
@@ -897,7 +828,7 @@ class unifier (loc: AST.l) (assumptions: expr list) = object (self)
             (* attempt to close an expression by replacing all fresh vars with a closed expression *)
         and close_expr (x: expr): expr option =
             let subst = new substFunClass (fun x -> if self#isFresh x then Some (close_ident x) else None) in
-            let x'    = Asl_visitor.visit_expr subst x in
+            let x'    = Visitor.visit_expr subst x in
             if isClosed x' then
                 Some x'
             else
@@ -1027,8 +958,8 @@ let unify_ixtype (u: unifier) (ty1: AST.ixtype) (ty2: AST.ixtype): unit =
 let rec unify_type (env: GlobalEnv.t) (u: unifier) (ty1: AST.ty) (ty2: AST.ty): unit =
     (* Substitute global constants in types *)
     let subst_consts = new substFunClass (GlobalEnv.getConstant env) in
-    let ty1' = Asl_visitor.visit_type subst_consts ty1 in
-    let ty2' = Asl_visitor.visit_type subst_consts ty2 in
+    let ty1' = Visitor.visit_type subst_consts ty1 in
+    let ty2' = Visitor.visit_type subst_consts ty2 in
     (match (derefType env ty1', derefType env ty2') with
     | (Type_Constructor c1,       Type_Constructor c2)       -> ()
     | (Type_Bits(e1),             Type_Bits(e2))             -> u#addEquality e1 e2
@@ -2517,11 +2448,11 @@ let genPrototypes (ds: AST.declaration list): (AST.declaration list * AST.declar
     (List.rev !pre, List.rev !post)
 
 (** Overall typechecking environment shared by all invocations of typechecker *)
-let env0 = GlobalEnv.mkempty ()
+let env0 = ref (GlobalEnv.mkempty ())
 
 (** Typecheck a list of declarations - main entrypoint into typechecker *)
 let tc_declarations (isPrelude: bool) (ds: AST.declaration list): AST.declaration list =
-    if verbose then Printf.printf "  - Using Z3 %s\n" Z3.Version.to_string;
+    (* if verbose then Printf.printf "  - Using Z3 %s\n" Z3.Version.to_string; *)
     (* Process declarations, starting by moving all function definitions to the
      * end of the list and replacing them with function prototypes.
      * As long as the type/var decls are all sorted correctly, this
@@ -2532,8 +2463,8 @@ let tc_declarations (isPrelude: bool) (ds: AST.declaration list): AST.declaratio
      *)
     let (pre, post) = if isPrelude then (ds, []) else genPrototypes ds in
     if verbose then Printf.printf "  - Typechecking %d phase 1 declarations\n" (List.length pre);
-    let pre'  = List.map (tc_declaration env0) pre  in
-    let post' = List.map (tc_declaration env0) post in
+    let pre'  = List.map (tc_declaration !env0) pre  in
+    let post' = List.map (tc_declaration !env0) post in
     if verbose then List.iter (fun ds -> List.iter (fun d -> Printf.printf "\nTypechecked %s\n" (Utils.to_string (PP.pp_declaration d))) ds) post';
     if verbose then Printf.printf "  - Typechecking %d phase 2 declarations\n" (List.length post);
     List.append (List.concat pre') (List.concat post')
diff --git a/libASL/testing.ml b/libASL/testing.ml
index c1f58f06..be51e87e 100644
--- a/libASL/testing.ml
+++ b/libASL/testing.ml
@@ -423,10 +423,10 @@ let op_test_opcode (env: Env.t) (iset: string) (op: int): Env.t opresult =
 let get_opcodes (opt_verbose: bool ref) (iset: string) (instr: string) (env: Env.t): (string * instr_field list * ((int * bool) list) option) list =
   if !opt_verbose then Printf.printf "Coverage for encoding %s\n" instr;
 
-  let re = Pcre.regexp instr in
+  let re = Str.regexp instr in
   let encoding_matches = function
       | (Encoding_Block (Ident nm, Ident is, _, _, _, _, _, _)) ->
-          is = iset && Pcre.pmatch ~rex:re nm
+          is = iset && Str.string_match re nm 0
       | _ -> assert false
   in
   let encs = List.map (fun (x,_,_,_) -> x) (Env.listInstructions env) in
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/offlineASL/decode_tests.ml b/offlineASL/decode_tests.ml
new file mode 100644
index 00000000..3f44e593
--- /dev/null
+++ b/offlineASL/decode_tests.ml
@@ -0,0 +1,4 @@
+(* AUTO-GENERATED LIFTER FILE *)
+
+open Offline_utils
+
diff --git a/offlineASL/dune b/offlineASL/dune
index b2231230..aa2cf6f6 100644
--- a/offlineASL/dune
+++ b/offlineASL/dune
@@ -1,6 +1,11 @@
+; AUTO-GENERATED BY OCAML BACKEND
 (library
   (name offlineASL)
   (flags
-    (:standard -w -27 -cclib -lstdc++))
-  (modules offline utils)
-  (libraries zarith libASL))
+    (:standard -w -27 -w -33 -cclib -lstdc++))
+  (modules 
+    offline
+    decode_tests
+    offline_utils
+  )
+  (libraries asli.libASL))
diff --git a/offlineASL/offline.ml b/offlineASL/offline.ml
index 719ef1f7..1d913f9b 100644
--- a/offlineASL/offline.ml
+++ b/offlineASL/offline.ml
@@ -1,4 +1,7 @@
-open Utils
+(* AUTO-GENERATED LIFTER FILE *)
+
+open Offline_utils
+open Decode_tests
 
 let f_A64_decoder v_enc : unit = 
   failwith "unsupported"
diff --git a/offlineASL/utils.ml b/offlineASL/offline_utils.ml
similarity index 100%
rename from offlineASL/utils.ml
rename to offlineASL/offline_utils.ml
diff --git a/tests/coverage/dune b/tests/coverage/dune
index 718b8ba1..9de2105d 100644
--- a/tests/coverage/dune
+++ b/tests/coverage/dune
@@ -20,8 +20,10 @@
 (rule (with-stdout-to cov_branch  (run ./run "aarch64_branch.+")))
 (rule (with-stdout-to cov_float   (run ./run "aarch64_float_.+")))
 (rule (with-stdout-to cov_vector1 (run ./run "aarch64_vector_arithmetic_binary.+")))
-(rule (with-stdout-to cov_vector2 (run ./run "aarch64_vector_(?!arithmetic_binary).+")))
+(rule (with-stdout-to cov_vector2 (run ./run "aarch64_vector_\\(arithmetic_unary\\|[^a]\\).+")))
 (rule (with-stdout-to cov_memory  (run ./run "aarch64_memory_.+")))
+; note: cov_vector2 is intended to be every vector instruction that's not arithmetic_binary.
+; note ocaml Str regex syntax: https://ocaml.org/manual/5.2/api/Str.html
 
 (rule (alias coverage) (action (diff ./aarch64_integer cov_integer)))
 (rule (alias coverage) (action (diff ./aarch64_branch cov_branch)))
@@ -34,7 +36,7 @@
 (rule (with-stdout-to off_cov_branch  (run ./off_run "aarch64_branch.+")))
 (rule (with-stdout-to off_cov_float   (run ./off_run "aarch64_float_.+")))
 (rule (with-stdout-to off_cov_vector1 (run ./off_run "aarch64_vector_arithmetic_binary.+")))
-(rule (with-stdout-to off_cov_vector2 (run ./off_run "aarch64_vector_(?!arithmetic_binary).+")))
+(rule (with-stdout-to off_cov_vector2 (run ./off_run "aarch64_vector_\\(arithmetic_unary\\|[^a]\\).+")))
 (rule (with-stdout-to off_cov_memory  (run ./off_run "aarch64_memory_.+")))
 
 (rule (alias offline-coverage) (action (diff ./aarch64_integer off_cov_integer)))
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 <data:[...]> with ./[...]
+echo "$output" | sed 's#<data:\([^>]*\)>#./\1#g'
diff --git a/tests/dune b/tests/dune
index 1c01889f..0c1c3027 100644
--- a/tests/dune
+++ b/tests/dune
@@ -1,4 +1,4 @@
 (test (name test_asl)
  (modes exe)
  (flags (-cclib -lstdc++))
- (libraries alcotest libASL))
+ (libraries alcotest asli.libASL))
diff --git a/tests/test_asl.ml b/tests/test_asl.ml
index cb35f83b..80c875f0 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,9 +99,9 @@ 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 tcenv   = TC.Env.mkEnv !TC.env0 in
     let env     = Eval.build_evaluation_environment (prelude @ List.concat mra) in
     [
         ("arith", `Quick, test_arith tcenv env);