allow loading files from either disk or memory

bin/asli.ml

@@ -346,10 +346,11 @@ let main () =
         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

bin/offline_coverage.ml

@@ -87,10 +87,6 @@ let main () =
   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 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;
   List.map (fun instr -> run opt_verbose instr env) !opt_instr
 
 let _ = ignore (main())

libASL/arm_env.ml

@@ -3,7 +3,7 @@
 let aarch64_asl_dir: string option = 
     List.nth_opt Res.Sites.aslfiles 0
 
-let aarch64_asl_files: (string * string list) option = 
+let aarch64_asl_files: (LoadASL.source * LoadASL.source 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"; 
@@ -12,6 +12,8 @@ let aarch64_asl_files: (string * string list) option =
     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
+        let prelude = LoadASL.FileSource prelude in
+        let filenames = List.map (fun x -> LoadASL.FileSource x) filenames in
         Some (prelude, filenames))
 
 let aarch64_evaluation_environment ?(verbose = false) (): Eval.Env.t option = 

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 = (

libASL/loadASL.ml

@@ -23,6 +23,33 @@ 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 = function
+    | 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 = filename };
+        (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 = filename };
+        (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 report_parse_error (on_error: unit -> 'a) (f: unit -> 'a): 'a =
     (try
@@ -92,10 +119,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 +129,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

libASL/loadASL.mli

@@ -8,19 +8,24 @@
 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 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
 
 (** 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

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