support multiple :gen backends (#63)

also documents the :gen command in :help and adds support for user-specified output directories.
UQ-PAC · Mar 22, 2024 · f0287df · f0287df
1 parent 77efd8e
commit f0287df
Show file tree

Hide file tree

Showing 4 changed files with 45 additions and 12 deletions.
diff --git a/bin/asli.ml b/bin/asli.ml
@@ -41,6 +41,8 @@ let help_msg = [
     {|:opcode <instr-set> <int>      Decode and execute opcode|};
     {|:sem <instr-set> <int>         Decode and print opcode semantics|};
     {|:ast <instr-set> <int> [file]  Decode and write opcode semantics to stdout or a file, in a structured ast format|};
+    {|:gen <instr-set> <regex>       Generate an offline lifter using the given backend|};
+    {|      [backend] [dir]|};
     {|:project <file>                Execute ASLi commands in <file>|};
     {|:q :quit                       Exit the interpreter|};
     {|:run                           Execute instructions|};
@@ -54,6 +56,12 @@ let help_msg = [
     {|<stmt> ;                       Execute ASL statement|}
 ]
 
+(** supported backends for :gen and their default output directories *)
+let gen_backends = [
+    ("ocaml", (Cpu.Ocaml, "offlineASL"));
+    ("cpp",   (Cpu.Cpp, "offlineASL-cpp"));
+]
+
 let flags = [
     ("trace:write", Eval.trace_write);
     ("trace:fun",   Eval.trace_funcall);
@@ -205,10 +213,18 @@ let rec process_command (tcenv: TC.Env.t) (cpu: Cpu.cpu) (fname: string) (input0
             (fun s -> Printf.fprintf chan "%s\n" (Utils.to_string (PP.pp_raw_stmt s)))
             (Dis.dis_decode_entry cpu.env cpu.denv decoder op);
         Option.iter close_out chan_opt
-    | [":gen"; iset; id] ->
+    | ":gen" :: iset :: id :: rest when List.length rest <= 2 ->
+        let backend = Option.value List.(nth_opt rest 0) ~default:"ocaml" in
+        Printf.printf "Generating lifter for %s %s using %s backend\n" iset id backend;
+
+        let (backend, default_dir) = match List.assoc_opt backend gen_backends with
+            | Some x -> x
+            | None -> invalid_arg @@ Printf.sprintf "unknown backend %s (supported: %s)"
+                                     backend (String.concat ", " List.(map fst gen_backends)) in
+
+        let dir = Option.value List.(nth_opt rest 1) ~default:default_dir in
         let cpu' = Cpu.mkCPU cpu.env cpu.denv in
-        Printf.printf "Generating lifter for %s %s\n" iset id;
-        cpu'.gen iset id
+        cpu'.gen iset id backend dir
     | ":dump" :: iset :: opcode :: rest ->
         let fname = 
             (match rest with 

diff --git a/libASL/cpu.ml b/libASL/cpu.ml
@@ -9,6 +9,12 @@ module AST = Asl_ast
 
 open Asl_utils
 
+type gen_backend =
+    | Ocaml
+    | Cpp
+
+type gen_function = AST.ident -> Eval.fun_sig -> Eval.fun_sig Bindings.t -> Eval.fun_sig Bindings.t -> string -> unit
+
 type cpu = {
     env      : Eval.Env.t;
     denv     : Dis.env;
@@ -19,7 +25,7 @@ type cpu = {
     elfwrite : Int64.t -> char -> unit;
     opcode   : string -> Primops.bigint -> unit;
     sem      : string -> Primops.bigint -> unit;
-    gen      : string -> string -> unit
+    gen      : string -> string -> gen_backend -> string -> unit;
 }
 
 let mkCPU (env : Eval.Env.t) (denv: Dis.env): cpu =
@@ -56,14 +62,19 @@ let mkCPU (env : Eval.Env.t) (denv: Dis.env): cpu =
             (fun s -> Printf.printf "%s\n" (pp_stmt s))
             (Dis.dis_decode_entry env denv decoder op)
 
-    and gen (iset: string) (pat: string): unit =
+    and gen (iset: string) (pat: string) (backend: gen_backend) (dir: string): unit =
+        if not (Sys.file_exists dir) then failwith ("Can't find target dir " ^ dir);
+
         (* Build the symbolic lifter *)
         let (decoder_id,decoder_fnsig,tests,instrs) = Symbolic_lifter.run iset pat env in
 
+        let run_gen_backend : gen_function =
+            match backend with
+            | Ocaml -> Ocaml_backend.run
+            | Cpp -> failwith "cpp backend not yet implemented" in
+
         (* Build backend program *)
-        (* TODO: other backends *)
-        if not (Sys.file_exists "offlineASL") then failwith "Can't find target dir offlineASL\n";
-        Ocaml_backend.run decoder_id decoder_fnsig tests instrs "offlineASL"
+        run_gen_backend decoder_id decoder_fnsig tests instrs dir
 
     in
     {

diff --git a/libASL/cpu.mli b/libASL/cpu.mli
@@ -5,6 +5,12 @@
  * SPDX-Licence-Identifier: BSD-3-Clause
  ****************************************************************)
 
+type gen_backend =
+    | Ocaml
+    | Cpp
+
+type gen_function = Asl_ast.ident -> Eval.fun_sig -> Eval.fun_sig Asl_utils.Bindings.t -> Eval.fun_sig Asl_utils.Bindings.t -> string -> unit
+
 type cpu = {
     env      : Eval.Env.t;
     denv     : Dis.env;
@@ -15,7 +21,7 @@ type cpu = {
     elfwrite : Int64.t -> char -> unit;
     opcode   : string -> Primops.bigint -> unit;
     sem      : string -> Primops.bigint -> unit;
-    gen      : string -> string -> unit
+    gen      : string -> string -> gen_backend -> string -> unit;
 }
 
 val mkCPU : Eval.Env.t -> Dis.env -> cpu

diff --git a/libASL/eval.ml b/libASL/eval.ml
@@ -128,9 +128,9 @@ module Env : sig
     val getVar              : AST.l -> t -> ident -> value
     val setVar              : AST.l -> t -> ident -> value -> unit
 
-    val getFun              : AST.l -> t -> ident -> (ty option * ((ty * ident) list) * ident list * ident list * AST.l * stmt list)
-    val getFunOpt           : AST.l -> t -> ident -> (ty option * ((ty * ident) list) * ident list * ident list * AST.l * stmt list) option
-    val addFun              : AST.l -> t -> ident -> (ty option * ((ty * ident) list) * ident list * ident list * AST.l * stmt list) -> unit
+    val getFun              : AST.l -> t -> ident -> fun_sig
+    val getFunOpt           : AST.l -> t -> ident -> fun_sig option
+    val addFun              : AST.l -> t -> ident -> fun_sig -> unit
 
     val getInstruction      : AST.l -> t -> ident -> (encoding * (stmt list) option * bool * stmt list)
     val addInstruction      : AST.l -> t -> ident -> (encoding * (stmt list) option * bool * stmt list) -> unit