Allow user-specified state to be passed through generated C

For example:

sail -c_extra_params "CPUMIPSState *env" -c_extra_args env

would pass a QEMU MIPS cpu state to every non-builtin function call.

Also add documentation for each C compilation option in C_backend.mli

3 files changed, 69 insertions, 13 deletions

diff --git a/src/c_backend.ml b/src/c_backend.ml
index a656a097..ab388223 100644
--- a/src/c_backend.ml
+++ b/src/c_backend.ml
@@ -71,6 +71,18 @@ let opt_no_main = ref false
 let opt_memo_cache = ref false
 let opt_no_rts = ref false
 let opt_prefix = ref "z"
+let opt_extra_params = ref None
+let opt_extra_arguments = ref None
+
+let extra_params () =
+  match !opt_extra_params with
+  | Some str -> str ^ ", "
+  | _ -> ""
+
+let extra_arguments is_extern =
+  match !opt_extra_arguments with
+  | Some str when not is_extern -> str ^ ", "
+  | _ -> ""
 
 (* Optimization flags *)
 let optimize_primops = ref false
@@ -2588,6 +2600,7 @@ let rec codegen_instr fid ctx (I_aux (instr, (_, l))) =
   | I_funcall (x, extern, f, args) ->
      let c_args = Util.string_of_list ", " sgen_cval args in
      let ctyp = clexp_ctyp x in
+     let is_extern = Env.is_extern f ctx.tc_env "c" || extern in
      let fname =
        if Env.is_extern f ctx.tc_env "c" then
          Env.get_extern f ctx.tc_env "c"
@@ -2649,9 +2662,9 @@ let rec codegen_instr fid ctx (I_aux (instr, (_, l))) =
          string (Printf.sprintf  "  COPY(%s)(&%s, *(%s));" (sgen_ctyp_name ctyp) (sgen_clexp_pure x) c_args)
      else
        if is_stack_ctyp ctyp then
-         string (Printf.sprintf "  %s = %s(%s);" (sgen_clexp_pure x) fname c_args)
+         string (Printf.sprintf "  %s = %s(%s%s);" (sgen_clexp_pure x) fname (extra_arguments is_extern) c_args)
        else
-         string (Printf.sprintf "  %s(%s, %s);" fname (sgen_clexp x) c_args)
+         string (Printf.sprintf "  %s(%s%s, %s);" fname (extra_arguments is_extern) (sgen_clexp x) c_args)
 
   | I_clear (ctyp, id) when is_stack_ctyp ctyp ->
      empty
@@ -2867,7 +2880,7 @@ let codegen_type_def ctx = function
          in
          Printf.sprintf "%s op" (sgen_ctyp ctyp), empty, empty
        in
-       string (Printf.sprintf "static void %s(struct %s *rop, %s)" (sgen_function_id ctor_id) (sgen_id id) ctor_args) ^^ hardline
+       string (Printf.sprintf "static void %s(%sstruct %s *rop, %s)" (sgen_function_id ctor_id) (extra_params ()) (sgen_id id) ctor_args) ^^ hardline
        ^^ surround 2 0 lbrace
                    (tuple
                     ^^ each_ctor "rop->" (clear_field "rop") tus ^^ hardline
@@ -3183,9 +3196,9 @@ let codegen_def' ctx = function
      if Env.is_extern id ctx.tc_env "c" then
        empty
      else if is_stack_ctyp ret_ctyp then
-       string (Printf.sprintf "%s%s %s(%s);" static (sgen_ctyp ret_ctyp) (sgen_function_id id) (Util.string_of_list ", " sgen_ctyp arg_ctyps))
+       string (Printf.sprintf "%s%s %s(%s%s);" static (sgen_ctyp ret_ctyp) (sgen_function_id id) (extra_params ()) (Util.string_of_list ", " sgen_ctyp arg_ctyps))
      else
-       string (Printf.sprintf "%svoid %s(%s *rop, %s);" static (sgen_function_id id) (sgen_ctyp ret_ctyp) (Util.string_of_list ", " sgen_ctyp arg_ctyps))
+       string (Printf.sprintf "%svoid %s(%s%s *rop, %s);" static (sgen_function_id id) (extra_params ()) (sgen_ctyp ret_ctyp) (Util.string_of_list ", " sgen_ctyp arg_ctyps))
 
   | CDEF_fundef (id, ret_arg, args, instrs) as def ->
      if !opt_debug_flow_graphs then make_dot id (instrs_graph instrs) else ();
@@ -3226,12 +3239,12 @@ let codegen_def' ctx = function
        | None ->
           assert (is_stack_ctyp ret_ctyp);
           (if !opt_static then string "static " else empty)
-          ^^ string (sgen_ctyp ret_ctyp) ^^ space ^^ codegen_function_id id ^^ parens (string args) ^^ hardline
+          ^^ string (sgen_ctyp ret_ctyp) ^^ space ^^ codegen_function_id id ^^ parens (string (extra_params ()) ^^ string args) ^^ hardline
        | Some gs ->
           assert (not (is_stack_ctyp ret_ctyp));
           (if !opt_static then string "static " else empty)
           ^^ string "void" ^^ space ^^ codegen_function_id id
-          ^^ parens (string (sgen_ctyp ret_ctyp ^ " *" ^ sgen_id gs ^ ", ") ^^ string args)
+          ^^ parens (string (extra_params ()) ^^ string (sgen_ctyp ret_ctyp ^ " *" ^ sgen_id gs ^ ", ") ^^ string args)
           ^^ hardline
      in
      function_header
diff --git a/src/c_backend.mli b/src/c_backend.mli
index e6cc783c..3b26acdf 100644
--- a/src/c_backend.mli
+++ b/src/c_backend.mli
@@ -53,18 +53,54 @@ open Type_check
 
 (** Global compilation options *)
 
+(** Output a dataflow graph for each generated function in Graphviz
+   (dot) format. *)
 val opt_debug_flow_graphs : bool ref
+
+(** Print the ANF and IR representations of a specific function. *)
 val opt_debug_function : string ref
+
+(** Instrument generated code to output a trace. opt_smt_trace is WIP
+   but intended to enable generating traces suitable for concolic
+   execution with SMT. *)
 val opt_trace : bool ref
 val opt_smt_trace : bool ref
+
+(** Define generated functions as static *)
 val opt_static : bool ref
+
+(** Do not generate a main function *)
 val opt_no_main : bool ref
+
+(** (WIP) Do not include rts.h (the runtime), and do not generate code
+   that requires any setup or teardown routines to be run by a runtime
+   before executing any instruction semantics. *)
 val opt_no_rts : bool ref
+
+(** Ordinarily we use plain z-encoding to name-mangle generated Sail
+   identifiers into a form suitable for C. If opt_prefix is set, then
+   the "z" which is added on the front of each generated C function
+   will be replaced by opt_prefix. E.g. opt_prefix := "sail_" would
+   give sail_my_function rather than zmy_function. *)
 val opt_prefix : string ref
 
-(** [opt_memo_cache] will store the compiled function definitions in
-   file _sbuild/ccacheDIGEST where DIGEST is the md5sum of the
-   original function to be compiled. Enabled using the -memo
+(** opt_extra_params and opt_extra_arguments allow additional state to
+   be threaded through the generated C code by adding an additional
+   parameter to each function type, and then giving an extra argument
+   to each function call. For example we could have
+
+   opt_extra_params := Some "CPUMIPSState *env"
+   opt_extra_arguments := Some "env"
+
+   and every generated function will take a pointer to a QEMU MIPS
+   processor state, and each function will be passed the env argument
+   when it is called. *)
+val opt_extra_params : string option ref
+val opt_extra_arguments : string option ref
+
+(** (WIP) [opt_memo_cache] will store the compiled function
+   definitions in file _sbuild/ccacheDIGEST where DIGEST is the md5sum
+   of the original function to be compiled. Enabled using the -memo
    flag. Uses Marshal so it's quite picky about the exact version of
    the Sail version. This cache can obviously become stale if the C
    backend changes - it'll load an old version compiled without said
@@ -82,13 +118,14 @@ val optimize_experimental : bool ref
 (** The compilation context. *)
 type ctx
 
-(** Convert a typ to a IR ctyp *)
-val ctyp_of_typ : ctx -> Ast.typ -> ctyp
-
 (** Create a context from a typechecking environment. This environment
    should be the environment returned by typechecking the full AST. *)
 val initial_ctx : Env.t -> ctx
 
+(** Convert a typ to a IR ctyp *)
+val ctyp_of_typ : ctx -> Ast.typ -> ctyp
+
+
 val compile_aexp : ctx -> Ast.typ Anf.aexp -> instr list * (clexp -> instr) * instr list
 
 val compile_ast : ctx -> out_channel -> string list -> tannot Ast.defs -> unit
diff --git a/src/sail.ml b/src/sail.ml
index 0450c0ca..949663d4 100644
--- a/src/sail.ml
+++ b/src/sail.ml
@@ -145,6 +145,12 @@ let options = Arg.align ([
   ( "-c_prefix",
     Arg.String (fun prefix -> C_backend.opt_prefix := prefix),
     "<prefix> prefix generated C functions" );
+  ( "-c_extra_params",
+    Arg.String (fun params -> C_backend.opt_extra_params := Some params),
+    "<parameters> generate C functions with additional parameters" );
+  ( "-c_extra_args",
+    Arg.String (fun args -> C_backend.opt_extra_arguments := Some args),
+    "<arguments> supply extra argument to every generated C function call" );
   ( "-elf",
     Arg.String (fun elf -> opt_process_elf := Some elf),
     " process an ELF file so that it can be executed by compiled C code");