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.
UQ-PAC · Jun 18, 2024 · 1ef6942 · 1ef6942
1 parent bcf0918
commit 1ef6942
Show file tree

Hide file tree

Showing 4 changed files with 54 additions and 28 deletions.
diff --git 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 "<args>" (":project " ^ f)) prj_files;
+
         repl tcenv cpu
     end
 

diff --git 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
@@ -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
@@ -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