Functorise and refactor C code generator

Currently uses the -c2 option

Now generates a sail_state struct which is passed as a pointer to all
generated functions. This contains all registers, letbindings, and the
exception state. (Letbindings must be included as they can contain
pointers to registers). This should make it possible to use sail models
in a multi-threaded program by creating multiple sail_states, provided a
suitable set of thread-safe memory builtins are provided. Currently the
sail_state cannot be passed to the memory builtins.

For foo.sail, now generate a foo.c, foo.h, and (optionally) a foo_emu.c.
foo_emu.c wraps the generated library into an emulator that behaves the
same as the one we previously generated.

The sail_assert and sail_match_failure builtins are now in a separate
file, as they must exist even when the RTS is not used.

Name mangling can be controlled via the exports and exports_mangled
fields of the configuration struct (currently not exposed outside of
OCaml). exports allows specifying a name in C for any Sail identifier
(before name mangling) and exports_mangled allows specifiying a name for
a mangled Sail identifier - this is primarily useful for generic
functions and data structures which have been specialised.

1 files changed, 1617 insertions, 0 deletions

diff --git a/src/jib/c_codegen.ml b/src/jib/c_codegen.ml
new file mode 100644
index 00000000..6aa0060c
--- /dev/null
+++ b/src/jib/c_codegen.ml
@@ -0,0 +1,1617 @@
+(**************************************************************************)
+(*     Sail                                                               *)
+(*                                                                        *)
+(*  Copyright (c) 2013-2017                                               *)
+(*    Kathyrn Gray                                                        *)
+(*    Shaked Flur                                                         *)
+(*    Stephen Kell                                                        *)
+(*    Gabriel Kerneis                                                     *)
+(*    Robert Norton-Wright                                                *)
+(*    Christopher Pulte                                                   *)
+(*    Peter Sewell                                                        *)
+(*    Alasdair Armstrong                                                  *)
+(*    Brian Campbell                                                      *)
+(*    Thomas Bauereiss                                                    *)
+(*    Anthony Fox                                                         *)
+(*    Jon French                                                          *)
+(*    Dominic Mulligan                                                    *)
+(*    Stephen Kell                                                        *)
+(*    Mark Wassell                                                        *)
+(*                                                                        *)
+(*  All rights reserved.                                                  *)
+(*                                                                        *)
+(*  This software was developed by the University of Cambridge Computer   *)
+(*  Laboratory as part of the Rigorous Engineering of Mainstream Systems  *)
+(*  (REMS) project, funded by EPSRC grant EP/K008528/1.                   *)
+(*                                                                        *)
+(*  Redistribution and use in source and binary forms, with or without    *)
+(*  modification, are permitted provided that the following conditions    *)
+(*  are met:                                                              *)
+(*  1. Redistributions of source code must retain the above copyright     *)
+(*     notice, this list of conditions and the following disclaimer.      *)
+(*  2. Redistributions in binary form must reproduce the above copyright  *)
+(*     notice, this list of conditions and the following disclaimer in    *)
+(*     the documentation and/or other materials provided with the         *)
+(*     distribution.                                                      *)
+(*                                                                        *)
+(*  THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS''    *)
+(*  AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED     *)
+(*  TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A       *)
+(*  PARTICULAR PURPOSE ARE DISCLAIMED.  IN NO EVENT SHALL THE AUTHOR OR   *)
+(*  CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,          *)
+(*  SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT      *)
+(*  LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF      *)
+(*  USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND   *)
+(*  ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,    *)
+(*  OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT    *)
+(*  OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF    *)
+(*  SUCH DAMAGE.                                                          *)
+(**************************************************************************)
+
+open Ast
+open Ast_util
+open Jib
+open Jib_compile
+open Jib_util
+open Type_check
+open PPrint
+open Printf
+open Value2
+   
+module StringMap = Map.Make(String)
+module Big_int = Nat_big_num
+
+let opt_no_main = ref false
+let opt_no_lib = ref false
+let opt_no_rts = ref false
+               
+let (gensym, _) = symbol_generator "c2"
+let ngensym () = name (gensym ())
+ 
+let zencode_id id = Util.zencode_string (string_of_id id)
+
+let zencode_uid (id, ctyps) =
+  match ctyps with
+  | [] -> Util.zencode_string (string_of_id id)
+  | _ -> Util.zencode_string (string_of_id id ^ "#" ^ Util.string_of_list "_" string_of_ctyp ctyps)
+
+let ctor_bindings = List.fold_left (fun map (id, ctyp) -> UBindings.add id ctyp map) UBindings.empty
+       
+let max_int n = Big_int.pred (Big_int.pow_int_positive 2 (n - 1))
+let min_int n = Big_int.negate (Big_int.pow_int_positive 2 (n - 1))
+
+(** This function is used to split types into those we allocate on the
+   stack, versus those which need to live on the heap, or otherwise
+   require some additional memory management *)
+let rec is_stack_ctyp ctyp = match ctyp with
+  | CT_fbits _ | CT_sbits _ | CT_bit | CT_unit | CT_bool | CT_enum _ -> true
+  | CT_fint n -> n <= 64
+  (* | CT_lint when !optimize_fixed_int -> true *)
+  | CT_lint -> false
+  (* | CT_lbits _ when !optimize_fixed_bits -> true *)
+  | CT_lbits _ -> false
+  | CT_real | CT_string | CT_list _ | CT_vector _ | CT_fvector _ -> false
+  | CT_struct (_, fields) -> List.for_all (fun (_, ctyp) -> is_stack_ctyp ctyp) fields
+  | CT_variant (_, ctors) -> false (* List.for_all (fun (_, ctyp) -> is_stack_ctyp ctyp) ctors *) (* FIXME *)
+  | CT_tup ctyps -> List.for_all is_stack_ctyp ctyps
+  | CT_ref ctyp -> true
+  | CT_poly -> true
+  | CT_constant n -> Big_int.less_equal (min_int 64) n && Big_int.greater_equal n (max_int 64)
+
+let v_mask_lower i = V_lit (VL_bits (Util.list_init i (fun _ -> Sail2_values.B1), true), CT_fbits (i, true))
+       
+type codegen_options = {
+    exports : string Bindings.t;
+    exports_mangled : string StringMap.t;
+  }
+
+let add_export opts id = { opts with exports = Bindings.add id (string_of_id id) opts.exports }
+
+let add_custom_export opts id into = { opts with exports = Bindings.add id into opts.exports }
+                       
+let add_mangled_rename opts (from, into) = { opts with exports_mangled = StringMap.add from into opts.exports_mangled }
+                       
+let add_export_uid opts (id, ctyps) =
+  match ctyps with
+  | [] -> { opts with exports = Bindings.add id (string_of_id id) opts.exports }
+  | _ -> opts
+                          
+let ctype_def_initial_options opts = function
+  | CTD_enum (id, ids) ->
+     List.fold_left add_export (add_export opts id) ids
+  | CTD_struct (id, ctors) ->
+     List.fold_left add_export_uid (add_export opts id) (List.map fst ctors)
+  | _ -> opts
+                     
+let cdef_initial_options opts = function
+  | CDEF_type ctype_def -> ctype_def_initial_options opts ctype_def
+  | CDEF_reg_dec (id, _, _) -> add_export opts id
+  | CDEF_let (_, bindings, _) -> List.fold_left (fun opts (id, _) -> add_export opts id) opts bindings
+  | _ -> opts
+
+let initial_options = {
+    exports = Bindings.empty;
+    exports_mangled = StringMap.empty;
+  }
+       
+let default_options cdefs =
+  let opts = List.fold_left cdef_initial_options initial_options cdefs in
+  let opts = add_export opts (mk_id "initialize_registers") in
+  let opts = add_custom_export opts (mk_id "main") "sail_main" in
+  List.fold_left add_mangled_rename opts (List.init 9 (fun n -> "ztup" ^ string_of_int n, "tuple_" ^ string_of_int n))
+ 
+module type Config = sig
+  val opts : codegen_options
+end
+
+module Make(C: Config) = struct
+
+let mangle str =
+  let mangled = Util.zencode_string str in
+  match StringMap.find_opt mangled C.opts.exports_mangled with
+  | Some export -> export
+  | None -> mangled
+  
+let sgen_id id =
+  match Bindings.find_opt id C.opts.exports with
+  | Some export -> export
+  | None -> mangle (string_of_id id)
+
+let sgen_name =
+  function
+  | Name (id, _) ->
+     sgen_id id
+  | Global (id, _) ->
+     sprintf "(state->%s)" (sgen_id id)
+  | Have_exception _ ->
+     "(state->have_exception)"
+  | Return _ ->
+     assert false
+  | Current_exception _ ->
+     "(*(state->current_exception))"
+  | Throw_location _ ->
+     "(state->throw_location)"
+             
+let sgen_uid (id, ctyps) =
+  match ctyps with
+  | [] -> sgen_id id
+  | _ ->
+     mangle (string_of_id id ^ "#" ^ Util.string_of_list "_" string_of_ctyp ctyps)
+
+let codegen_id id = string (sgen_id id)
+let codegen_uid id = string (sgen_uid id)
+
+let sgen_function_id id = sgen_id id
+let sgen_function_uid uid = sgen_uid uid
+let codegen_function_id id = string (sgen_function_id id)
+
+let rec sgen_ctyp = function
+  | CT_unit -> "unit"
+  | CT_bit -> "fbits"
+  | CT_bool -> "bool"
+  | CT_fbits _ -> "uint64_t"
+  | CT_sbits _ -> "sbits"
+  | CT_fint _ -> "int64_t"
+  | CT_constant _ -> "int64_t"
+  | CT_lint -> "sail_int"
+  | CT_lbits _ -> "lbits"
+  | CT_tup _ as tup -> "struct " ^ Util.zencode_string ("tuple_" ^ string_of_ctyp tup)
+  | CT_struct (id, _) -> "struct " ^ sgen_id id
+  | CT_enum (id, _) -> "enum " ^ sgen_id id
+  | CT_variant (id, _) -> "struct " ^ sgen_id id
+  | CT_list _ as l -> Util.zencode_string (string_of_ctyp l)
+  | CT_vector _ as v -> Util.zencode_string (string_of_ctyp v)
+  | CT_fvector (_, ord, typ) -> sgen_ctyp (CT_vector (ord, typ))
+  | CT_string -> "sail_string"
+  | CT_real -> "real"
+  | CT_ref ctyp -> sgen_ctyp ctyp ^ "*"
+  | CT_poly -> "POLY" (* c_error "Tried to generate code for non-monomorphic type" *)
+
+let rec sgen_ctyp_name = function
+  | CT_unit -> "unit"
+  | CT_bit -> "fbits"
+  | CT_bool -> "bool"
+  | CT_fbits _ -> "fbits"
+  | CT_sbits _ -> "sbits"
+  | CT_fint _ -> "mach_int"
+  | CT_constant _ -> "mach_int"
+  | CT_lint -> "sail_int"
+  | CT_lbits _ -> "lbits"
+  | CT_tup _ as tup -> Util.zencode_string ("tuple_" ^ string_of_ctyp tup)
+  | CT_struct (id, _) -> sgen_id id
+  | CT_enum (id, _) -> sgen_id id
+  | CT_variant (id, _) -> sgen_id id
+  | CT_list _ as l -> Util.zencode_string (string_of_ctyp l)
+  | CT_vector _ as v -> Util.zencode_string (string_of_ctyp v)
+  | CT_fvector (_, ord, typ) -> sgen_ctyp_name (CT_vector (ord, typ))
+  | CT_string -> "sail_string"
+  | CT_real -> "real"
+  | CT_ref ctyp -> "ref_" ^ sgen_ctyp_name ctyp
+  | CT_poly -> "POLY" (* c_error "Tried to generate code for non-monomorphic type" *)
+
+let sgen_mask n =
+  if n = 0 then
+    "UINT64_C(0)"
+  else if n <= 64 then
+    let chars_F = String.make (n / 4) 'F' in
+    let first = match (n mod 4) with
+      | 0 -> ""
+      | 1 -> "1"
+      | 2 -> "3"
+      | 3 -> "7"
+      | _ -> assert false
+    in
+    "UINT64_C(0x" ^ first ^ chars_F ^ ")"
+  else
+    failwith "Tried to create a mask literal for a vector greater than 64 bits."
+
+let rec sgen_value = function
+  | VL_bits ([], _) -> "UINT64_C(0)"
+  | VL_bits (bs, true) -> "UINT64_C(" ^ Sail2_values.show_bitlist bs ^ ")"
+  | VL_bits (bs, false) -> "UINT64_C(" ^ Sail2_values.show_bitlist (List.rev bs) ^ ")"
+  | VL_int i -> Big_int.to_string i ^ "l"
+  | VL_bool true -> "true"
+  | VL_bool false -> "false"
+  | VL_unit -> "UNIT"
+  | VL_bit Sail2_values.B0 -> "UINT64_C(0)"
+  | VL_bit Sail2_values.B1 -> "UINT64_C(1)"
+  | VL_bit Sail2_values.BU -> failwith "Undefined bit found in value"
+  | VL_real str -> str
+  | VL_string str -> "\"" ^ str ^ "\""
+  | VL_empty_list -> "NULL"
+  | VL_enum element -> mangle element
+  | VL_ref r -> "&(state->" ^ sgen_id (mk_id r) ^ ")"
+  | VL_undefined ->
+     Reporting.unreachable Parse_ast.Unknown __POS__ "Cannot generate C value for an undefined literal"
+
+let rec sgen_cval ctx = function
+  | V_id (id, ctyp) ->
+     sgen_name id
+  | V_lit (vl, ctyp) -> sgen_value vl
+  | V_call (op, cvals) -> sgen_call ctx op cvals
+  | V_field (f, field) ->
+     sprintf "%s.%s" (sgen_cval ctx f) (sgen_uid field)
+  | V_tuple_member (f, _, n) ->
+     sprintf "%s.%s" (sgen_cval ctx f) (mangle ("tup" ^ string_of_int n))
+  | V_ctor_kind (f, ctor, unifiers, _) ->
+     sgen_cval ctx f ^ ".kind"
+     ^ " != Kind_" ^ zencode_uid (ctor, unifiers)
+  | V_struct (fields, _) ->
+     sprintf "{%s}"
+       (Util.string_of_list ", " (fun (field, cval) -> zencode_uid field ^ " = " ^ sgen_cval ctx cval) fields)
+  | V_ctor_unwrap (ctor, f, unifiers, _) ->
+     sprintf "%s.%s"
+       (sgen_cval ctx f)
+       (sgen_uid (ctor, unifiers))
+  | V_poly (f, _) -> sgen_cval ctx f
+
+and sgen_call ctx op cvals =
+  match op, cvals with
+  | Bnot, [v] -> "!(" ^ sgen_cval ctx v ^ ")"
+  | List_hd, [v] ->
+     sprintf "(%s).hd" ("*" ^ sgen_cval ctx v)
+  | List_tl, [v] ->
+     sprintf "(%s).tl" ("*" ^ sgen_cval ctx v)
+  | Eq, [v1; v2] ->
+     begin match cval_ctyp v1 with
+     | CT_sbits _ ->
+        sprintf "eq_sbits(%s, %s)" (sgen_cval ctx v1) (sgen_cval ctx v2)
+     | _ ->
+        sprintf "(%s == %s)" (sgen_cval ctx v1) (sgen_cval ctx v2)
+     end
+  | Neq, [v1; v2] ->
+     begin match cval_ctyp v1 with
+     | CT_sbits _ ->
+        sprintf "neq_sbits(%s, %s)" (sgen_cval ctx v1) (sgen_cval ctx v2)
+     | _ ->
+        sprintf "(%s != %s)" (sgen_cval ctx v1) (sgen_cval ctx v2)
+     end
+  | Ilt, [v1; v2] ->
+     sprintf "(%s < %s)" (sgen_cval ctx v1) (sgen_cval ctx v2)
+  | Igt, [v1; v2] ->
+     sprintf "(%s > %s)" (sgen_cval ctx v1) (sgen_cval ctx v2)
+  | Ilteq, [v1; v2] ->
+     sprintf "(%s <= %s)" (sgen_cval ctx v1) (sgen_cval ctx v2)
+  | Igteq, [v1; v2] ->
+     sprintf "(%s >= %s)" (sgen_cval ctx v1) (sgen_cval ctx v2)
+  | Iadd, [v1; v2] ->
+     sprintf "(%s + %s)" (sgen_cval ctx v1) (sgen_cval ctx v2)
+  | Isub, [v1; v2] ->
+     sprintf "(%s - %s)" (sgen_cval ctx v1) (sgen_cval ctx v2)
+  | Unsigned 64, [vec] ->
+     sprintf "((mach_int) %s)" (sgen_cval ctx vec)
+  | Signed 64, [vec] ->
+     begin match cval_ctyp vec with
+     | CT_fbits (n, _) ->
+        sprintf "fast_signed(%s, %d)" (sgen_cval ctx vec) n
+     | _ -> assert false
+     end
+  | Bvand, [v1; v2] ->
+     begin match cval_ctyp v1 with
+     | CT_fbits _ ->
+        sprintf "(%s & %s)" (sgen_cval ctx v1) (sgen_cval ctx v2)
+     | CT_sbits _ ->
+        sprintf "and_sbits(%s, %s)" (sgen_cval ctx v1) (sgen_cval ctx v2)
+     | _ -> assert false
+     end
+  | Bvnot, [v] ->
+     begin match cval_ctyp v with
+     | CT_fbits (n, _) ->
+        sprintf "(~(%s) & %s)" (sgen_cval ctx v) (sgen_cval ctx (v_mask_lower n))
+     | CT_sbits _ ->
+        sprintf "not_sbits(%s)" (sgen_cval ctx v)
+     | _ -> assert false
+     end
+  | Bvor, [v1; v2] ->
+     begin match cval_ctyp v1 with
+     | CT_fbits _ ->
+        sprintf "(%s | %s)" (sgen_cval ctx v1) (sgen_cval ctx v2)
+     | CT_sbits _ ->
+        sprintf "or_sbits(%s, %s)" (sgen_cval ctx v1) (sgen_cval ctx v2)
+     | _ -> assert false
+     end
+  | Bvxor, [v1; v2] ->
+     begin match cval_ctyp v1 with
+     | CT_fbits _ ->
+        sprintf "(%s ^ %s)" (sgen_cval ctx v1) (sgen_cval ctx v2)
+     | CT_sbits _ ->
+        sprintf "xor_sbits(%s, %s)" (sgen_cval ctx v1) (sgen_cval ctx v2)
+     | _ -> assert false
+     end
+  | Bvadd, [v1; v2] ->
+     begin match cval_ctyp v1 with
+     | CT_fbits (n, _) ->
+        sprintf "((%s + %s) & %s)" (sgen_cval ctx v1) (sgen_cval ctx v2) (sgen_cval ctx (v_mask_lower n))
+     | CT_sbits _ ->
+        sprintf "add_sbits(%s, %s)" (sgen_cval ctx v1) (sgen_cval ctx v2)
+     | _ -> assert false
+     end
+  | Bvsub, [v1; v2] ->
+     begin match cval_ctyp v1 with
+     | CT_fbits (n, _) ->
+        sprintf "((%s - %s) & %s)" (sgen_cval ctx v1) (sgen_cval ctx v2) (sgen_cval ctx (v_mask_lower n))
+     | CT_sbits _ ->
+        sprintf "sub_sbits(%s, %s)" (sgen_cval ctx v1) (sgen_cval ctx v2)
+     | _ -> assert false
+     end
+  | Bvaccess, [vec; n] ->
+     begin match cval_ctyp vec with
+     | CT_fbits _ ->
+        sprintf "(UINT64_C(1) & (%s >> %s))" (sgen_cval ctx vec) (sgen_cval ctx n)
+     | CT_sbits _ ->
+        sprintf "(UINT64_C(1) & (%s.bits >> %s))" (sgen_cval ctx vec) (sgen_cval ctx n)
+     | _ -> assert false
+     end
+  | Slice len, [vec; start] ->
+     begin match cval_ctyp vec with
+     | CT_fbits _ ->
+        sprintf "(safe_rshift(UINT64_MAX, 64 - %d) & (%s >> %s))" len (sgen_cval ctx vec) (sgen_cval ctx start)
+     | CT_sbits _ ->
+        sprintf "(safe_rshift(UINT64_MAX, 64 - %d) & (%s.bits >> %s))" len (sgen_cval ctx vec) (sgen_cval ctx start)
+     | _ -> assert false
+     end
+  | Sslice 64, [vec; start; len] ->
+     begin match cval_ctyp vec with
+     | CT_fbits _ ->
+        sprintf "sslice(%s, %s, %s)" (sgen_cval ctx vec) (sgen_cval ctx start) (sgen_cval ctx len)
+     | CT_sbits _ ->
+        sprintf "sslice(%s.bits, %s, %s)" (sgen_cval ctx vec) (sgen_cval ctx start) (sgen_cval ctx len)
+     | _ -> assert false
+     end
+  | Set_slice, [vec; start; slice] ->
+     begin match cval_ctyp vec, cval_ctyp slice with
+     | CT_fbits (n, _), CT_fbits (m, _) ->
+        sprintf "((%s & ~(%s << %s)) | (%s << %s))" (sgen_cval ctx vec) (sgen_mask m) (sgen_cval ctx start) (sgen_cval ctx slice) (sgen_cval ctx start)
+     | _ -> assert false
+     end
+  | Zero_extend n, [v] ->
+     begin match cval_ctyp v with
+     | CT_fbits _ -> sgen_cval ctx v
+     | CT_sbits _ ->
+        sprintf "fast_zero_extend(%s, %d)" (sgen_cval ctx v) n
+     | _ -> assert false
+     end
+  | Sign_extend n, [v] ->
+     begin match cval_ctyp v with
+     | CT_fbits (m, _) ->
+        sprintf "fast_sign_extend(%s, %d, %d)" (sgen_cval ctx v) m n
+     | CT_sbits _ ->
+        sprintf "fast_sign_extend2(%s, %d)" (sgen_cval ctx v) n
+     | _ -> assert false
+     end
+  | Replicate n, [v] ->
+     begin match cval_ctyp v with
+     | CT_fbits (m, _) ->
+        sprintf "fast_replicate_bits(UINT64_C(%d), %s, %d)" m (sgen_cval ctx v) n
+     | _ -> assert false
+     end
+  | Concat, [v1; v2] ->
+     (* Optimized routines for all combinations of fixed and small bits
+        appends, where the result is guaranteed to be smaller than 64. *)
+     begin match cval_ctyp v1, cval_ctyp v2 with
+     | CT_fbits (0, _), CT_fbits (n2, _) ->
+        sgen_cval ctx v2
+     | CT_fbits (n1, _), CT_fbits (n2, _) ->
+        sprintf "(%s << %d) | %s" (sgen_cval ctx v1) n2 (sgen_cval ctx v2)
+     | CT_sbits (64, ord1), CT_fbits (n2, _) ->
+        sprintf "append_sf(%s, %s, %d)" (sgen_cval ctx v1) (sgen_cval ctx v2) n2
+     | CT_fbits (n1, ord1), CT_sbits (64, ord2) ->
+        sprintf "append_fs(%s, %d, %s)" (sgen_cval ctx v1) n1 (sgen_cval ctx v2)
+     | CT_sbits (64, ord1), CT_sbits (64, ord2) ->
+        sprintf "append_ss(%s, %s)" (sgen_cval ctx v1) (sgen_cval ctx v2)
+     | _ -> assert false
+     end
+  | _, _ ->
+     failwith "Could not generate cval primop"
+
+let sgen_cval_param ctx cval =
+  match cval_ctyp cval with
+  | CT_lbits direction ->
+     sgen_cval ctx cval ^ ", " ^ string_of_bool direction
+  | CT_sbits (_, direction) ->
+     sgen_cval ctx cval ^ ", " ^ string_of_bool direction
+  | CT_fbits (len, direction) ->
+     sgen_cval ctx cval ^ ", UINT64_C(" ^ string_of_int len ^ ") , " ^ string_of_bool direction
+  | _ ->
+     sgen_cval ctx cval
+
+let rec sgen_clexp ctx = function
+  | CL_id (Have_exception _, _) -> "(state->have_exception)"
+  | CL_id (Current_exception _, _) -> "(state->current_exception)"
+  | CL_id (Throw_location _, _) -> "(state->throw_location)"
+  | CL_id (Return _, _) -> assert false
+  | CL_id (Global (id, _), _) -> "&(state->" ^ sgen_id id ^ ")"
+  | CL_id (Name (id, _), _) -> "&" ^ sgen_id id
+  | CL_field (clexp, field) -> "&((" ^ sgen_clexp ctx clexp ^ ")->" ^ sgen_uid field ^ ")"
+  | CL_tuple (clexp, n) -> "&((" ^ sgen_clexp ctx clexp ^ ")->" ^ mangle ("tup" ^ string_of_int n) ^ ")"
+  | CL_addr clexp -> "(*(" ^ sgen_clexp ctx clexp ^ "))"
+  | CL_void -> assert false
+  | CL_rmw _ -> assert false
+
+let rec sgen_clexp_pure ctx = function
+  | CL_id (Have_exception _, _) -> "(state->have_exception)"
+  | CL_id (Current_exception _, _) -> "(state->current_exception)"
+  | CL_id (Throw_location _, _) -> "(state->throw_location)"
+  | CL_id (Return _, _) -> assert false
+  | CL_id (Global (id, _), _) -> "state->" ^ sgen_id id
+  | CL_id (Name (id, _), _) -> sgen_id id
+  | CL_field (clexp, field) -> sgen_clexp_pure ctx clexp ^ "." ^ sgen_uid field
+  | CL_tuple (clexp, n) -> sgen_clexp_pure ctx clexp ^ "." ^ mangle ("tup" ^ string_of_int n)
+  | CL_addr clexp -> "(*(" ^ sgen_clexp_pure ctx clexp ^ "))"
+  | CL_void -> assert false
+  | CL_rmw _ -> assert false
+
+(** Generate instructions to copy from a cval to a clexp. This will
+   insert any needed type conversions from big integers to small
+   integers (or vice versa), or from arbitrary-length bitvectors to
+   and from uint64 bitvectors as needed. *)
+let rec codegen_conversion l ctx clexp cval =
+  let ctyp_to = clexp_ctyp clexp in
+  let ctyp_from = cval_ctyp cval in
+  match ctyp_to, ctyp_from with
+  (* When both types are equal, we don't need any conversion. *)
+  | _, _ when ctyp_equal ctyp_to ctyp_from ->
+     if is_stack_ctyp ctyp_to then
+       ksprintf string "  %s = %s;" (sgen_clexp_pure ctx clexp) (sgen_cval ctx cval)
+     else
+       ksprintf string "  COPY(%s)(%s, %s);" (sgen_ctyp_name ctyp_to) (sgen_clexp ctx clexp) (sgen_cval ctx cval)
+
+  | CT_ref ctyp_to, ctyp_from ->
+     codegen_conversion l ctx (CL_addr clexp) cval
+
+  (* If we have to convert between tuple types, convert the fields individually. *)
+  | CT_tup ctyps_to, CT_tup ctyps_from when List.length ctyps_to = List.length ctyps_from ->
+     let len = List.length ctyps_to in
+     let conversions =
+       List.mapi (fun i ctyp -> codegen_conversion l ctx (CL_tuple (clexp, i)) (V_tuple_member (cval, len, i))) ctyps_from
+     in
+     string "  /* conversions */"
+     ^^ hardline
+     ^^ separate hardline conversions
+     ^^ hardline
+     ^^ string "  /* end conversions */"
+
+  (* For anything not special cased, just try to call a appropriate CONVERT_OF function. *)
+  | _, _ when is_stack_ctyp (clexp_ctyp clexp) ->
+     ksprintf string "  %s = CONVERT_OF(%s, %s)(%s);"
+       (sgen_clexp_pure ctx clexp) (sgen_ctyp_name ctyp_to) (sgen_ctyp_name ctyp_from) (sgen_cval_param ctx cval)
+  | _, _ ->
+     ksprintf string "  CONVERT_OF(%s, %s)(%s, %s);"
+       (sgen_ctyp_name ctyp_to) (sgen_ctyp_name ctyp_from) (sgen_clexp ctx clexp) (sgen_cval_param ctx cval)
+
+let extra_params () = "sail_state *state, "
+
+let extra_arguments is_extern =
+  if is_extern then
+    ""
+  else
+    "state, "
+ 
+let rec codegen_instr fid ctx (I_aux (instr, (_, l))) =
+  match instr with
+  | I_decl (ctyp, id) when is_stack_ctyp ctyp ->
+     ksprintf string "  %s %s;" (sgen_ctyp ctyp) (sgen_name id)
+  | I_decl (ctyp, id) ->
+     ksprintf string "  %s %s;" (sgen_ctyp ctyp) (sgen_name id) ^^ hardline
+     ^^ ksprintf string "  CREATE(%s)(&%s);" (sgen_ctyp_name ctyp) (sgen_name id)
+
+  | I_copy (clexp, cval) -> codegen_conversion l ctx clexp cval
+
+  | I_jump (cval, label) ->
+     ksprintf string "  if (%s) goto %s;" (sgen_cval ctx cval) label
+
+  | I_if (cval, [then_instr], [], ctyp) ->
+     ksprintf string "  if (%s)" (sgen_cval ctx cval) ^^ hardline
+     ^^ twice space ^^ codegen_instr fid ctx then_instr
+  | I_if (cval, then_instrs, [], ctyp) ->
+     string "  if" ^^ space ^^ parens (string (sgen_cval ctx cval)) ^^ space
+     ^^ surround 0 0 lbrace (separate_map hardline (codegen_instr fid ctx) then_instrs) (twice space ^^ rbrace)
+  | I_if (cval, then_instrs, else_instrs, ctyp) ->
+     string "  if" ^^ space ^^ parens (string (sgen_cval ctx cval)) ^^ space
+     ^^ surround 0 0 lbrace (separate_map hardline (codegen_instr fid ctx) then_instrs) (twice space ^^ rbrace)
+     ^^ space ^^ string "else" ^^ space
+     ^^ surround 0 0 lbrace (separate_map hardline (codegen_instr fid ctx) else_instrs) (twice space ^^ rbrace)
+
+  | I_block instrs ->
+     string "  {"
+     ^^ jump 2 2 (separate_map hardline (codegen_instr fid ctx) instrs) ^^ hardline
+     ^^ string "  }"
+
+  | I_try_block instrs ->
+     string "  { /* try */"
+     ^^ jump 2 2 (separate_map hardline (codegen_instr fid ctx) instrs) ^^ hardline
+     ^^ string "  }"
+
+  | I_funcall (x, special_extern, f, args) ->
+     let c_args = Util.string_of_list ", " (sgen_cval ctx) args in
+     let ctyp = clexp_ctyp x in
+     let is_extern = Env.is_extern (fst f) ctx.tc_env "c" || special_extern in
+     let fname =
+       if special_extern then
+         string_of_id (fst f)
+       else if Env.is_extern (fst f) ctx.tc_env "c" then
+         Env.get_extern (fst f) ctx.tc_env "c"
+       else
+         sgen_function_uid f
+     in
+     let fname =
+       match fname, ctyp with
+       | "internal_pick", _ -> sprintf "pick_%s" (sgen_ctyp_name ctyp)
+       | "cons", _ ->
+          begin match snd f with
+          | [ctyp] -> Util.zencode_string ("cons#" ^ string_of_ctyp ctyp)
+          | _ -> Reporting.unreachable l __POS__ "cons without specified type"
+          end
+       | "eq_anything", _ ->
+          begin match args with
+          | cval :: _ -> sprintf "eq_%s" (sgen_ctyp_name (cval_ctyp cval))
+          | _ -> Reporting.unreachable l __POS__ "eq_anything function with bad arity."
+          end
+       | "length", _ ->
+          begin match args with
+          | cval :: _ -> sprintf "length_%s" (sgen_ctyp_name (cval_ctyp cval))
+          | _ -> Reporting.unreachable l __POS__ "length function with bad arity."
+          end
+       | "vector_access", CT_bit -> "bitvector_access"
+       | "vector_access", _ ->
+          begin match args with
+          | cval :: _ -> sprintf "vector_access_%s" (sgen_ctyp_name (cval_ctyp cval))
+          | _ -> Reporting.unreachable l __POS__ "vector access function with bad arity."
+          end
+       | "vector_update_subrange", _ -> sprintf "vector_update_subrange_%s" (sgen_ctyp_name ctyp)
+       | "vector_subrange", _ -> sprintf "vector_subrange_%s" (sgen_ctyp_name ctyp)
+       | "vector_update", CT_fbits _ -> "update_fbits"
+       | "vector_update", CT_lbits _ -> "update_lbits"
+       | "vector_update", _ -> sprintf "vector_update_%s" (sgen_ctyp_name ctyp)
+       | "string_of_bits", _ ->
+          begin match cval_ctyp (List.nth args 0) with
+          | CT_fbits _ -> "string_of_fbits"
+          | CT_lbits _ -> "string_of_lbits"
+          | _ -> assert false
+          end
+       | "decimal_string_of_bits", _ ->
+          begin match cval_ctyp (List.nth args 0) with
+          | CT_fbits _ -> "decimal_string_of_fbits"
+          | CT_lbits _ -> "decimal_string_of_lbits"
+          | _ -> assert false
+          end
+       | "internal_vector_update", _ -> sprintf "internal_vector_update_%s" (sgen_ctyp_name ctyp)
+       | "internal_vector_init", _ -> sprintf "internal_vector_init_%s" (sgen_ctyp_name ctyp)
+       | "undefined_bitvector", CT_fbits _ -> "UNDEFINED(fbits)"
+       | "undefined_bitvector", CT_lbits _ -> "UNDEFINED(lbits)"
+       | "undefined_bit", _ -> "UNDEFINED(fbits)"
+       | "undefined_vector", _ -> sprintf "UNDEFINED(vector_%s)" (sgen_ctyp_name ctyp)
+       | "undefined_list", _ -> sprintf "UNDEFINED(%s)" (sgen_ctyp_name ctyp)
+       | fname, _ -> fname
+     in
+     if fname = "reg_deref" then
+       if is_stack_ctyp ctyp then
+         ksprintf string "  %s = *(%s);" (sgen_clexp_pure ctx x) c_args
+       else
+         ksprintf string "  COPY(%s)(&%s, *(%s));" (sgen_ctyp_name ctyp) (sgen_clexp_pure ctx x) c_args
+     else
+       if is_stack_ctyp ctyp then
+         ksprintf string "  %s = %s(%s%s);" (sgen_clexp_pure ctx x) fname (extra_arguments is_extern) c_args
+       else
+         ksprintf string "  %s(%s%s, %s);" fname (extra_arguments is_extern) (sgen_clexp ctx x) c_args
+
+  | I_clear (ctyp, id) when is_stack_ctyp ctyp ->
+     empty
+  | I_clear (ctyp, id) ->
+     ksprintf string "  KILL(%s)(&%s);" (sgen_ctyp_name ctyp) (sgen_name id)
+
+  | I_init (ctyp, id, cval) ->
+     codegen_instr fid ctx (idecl ctyp id) ^^ hardline
+     ^^ codegen_conversion Parse_ast.Unknown ctx (CL_id (id, ctyp)) cval
+
+  | I_reinit (ctyp, id, cval) ->
+     codegen_instr fid ctx (ireset ctyp id) ^^ hardline
+     ^^ codegen_conversion Parse_ast.Unknown ctx (CL_id (id, ctyp)) cval
+
+  | I_reset (ctyp, id) when is_stack_ctyp ctyp ->
+     ksprintf string "  %s %s;" (sgen_ctyp ctyp) (sgen_name id)
+  | I_reset (ctyp, id) ->
+     ksprintf string "  RECREATE(%s)(&%s);" (sgen_ctyp_name ctyp) (sgen_name id)
+
+  | I_return cval ->
+     ksprintf string "  return %s;" (sgen_cval ctx cval)
+
+  | I_throw cval ->
+     Reporting.unreachable l __POS__ "I_throw reached code generator"
+
+  | I_undefined ctyp ->
+     let rec codegen_exn_return ctyp =
+       match ctyp with
+       | CT_unit -> "UNIT", []
+       | CT_bit -> "UINT64_C(0)", []
+       | CT_fint _ -> "INT64_C(0xdeadc0de)", []
+       (* | CT_lint when !optimize_fixed_int -> "((sail_int) 0xdeadc0de)", [] *)
+       | CT_fbits _ -> "UINT64_C(0xdeadc0de)", []
+       | CT_sbits _ -> "undefined_sbits()", []
+       (* | CT_lbits _ when !optimize_fixed_bits -> "undefined_lbits(false)", [] *)
+       | CT_bool -> "false", []
+       | CT_enum (_, ctor :: _) -> sgen_id ctor, []
+       | CT_tup ctyps when is_stack_ctyp ctyp ->
+          let gs = ngensym () in
+          let fold (inits, prev) (n, ctyp) =
+            let init, prev' = codegen_exn_return ctyp in
+            sprintf ".%s = %s" (mangle ("tup" ^ string_of_int n)) init :: inits, prev @ prev'
+          in
+          let inits, prev = List.fold_left fold ([], []) (List.mapi (fun i x -> (i, x)) ctyps) in
+          sgen_name gs,
+          [sprintf "struct %s %s = { " (sgen_ctyp_name ctyp) (sgen_name gs)
+           ^ Util.string_of_list ", " (fun x -> x) inits ^ " };"] @ prev
+       | CT_struct (id, ctors) when is_stack_ctyp ctyp ->
+          let gs = ngensym () in
+          let fold (inits, prev) (uid, ctyp) =
+            let init, prev' = codegen_exn_return ctyp in
+            sprintf ".%s = %s" (sgen_uid uid) init :: inits, prev @ prev'
+          in
+          let inits, prev = List.fold_left fold ([], []) ctors in
+          sgen_name gs,
+          [sprintf "struct %s %s = { " (sgen_ctyp_name ctyp) (sgen_name gs)
+           ^ Util.string_of_list ", " (fun x -> x) inits ^ " };"] @ prev
+       | ctyp -> Reporting.unreachable l __POS__ ("Cannot create undefined value for type: " ^ string_of_ctyp ctyp)
+     in
+     let ret, prev = codegen_exn_return ctyp in
+     separate_map hardline (fun str -> string ("  " ^ str)) (List.rev prev)
+     ^^ hardline
+     ^^ ksprintf string "  return %s;" ret
+ 
+  | I_comment str ->
+     string ("  /* " ^ str ^ " */")
+
+  | I_label str ->
+     string (str ^ ": ;")
+
+  | I_goto str ->
+     ksprintf string "  goto %s;" str
+
+  | I_raw _ when ctx.no_raw -> empty
+  | I_raw str ->
+     string ("  " ^ str)
+
+  | I_end _ -> assert false
+
+  | I_match_failure ->
+     string ("  sail_match_failure(\"" ^ String.escaped (string_of_id fid) ^ "\");")
+
+(**************************************************************************)
+(* Code generation for type definitions (enums, structs, and variants)    *)
+(**************************************************************************)
+    
+let codegen_type_def_header = function
+  | CTD_enum (id, ids) ->
+     ksprintf string "// enum %s" (string_of_id id) ^^ hardline
+     ^^ separate space [string "enum"; codegen_id id; lbrace; separate_map (comma ^^ space) codegen_id ids; rbrace ^^ semi]
+     ^^ twice hardline
+
+  | CTD_struct (id, ctors) ->
+     let codegen_ctor (id, ctyp) =
+       string (sgen_ctyp ctyp) ^^ space ^^ codegen_uid id
+     in
+     ksprintf string "// struct %s" (string_of_id id) ^^ hardline
+     ^^ string "struct" ^^ space ^^ codegen_id id ^^ space
+     ^^ surround 2 0 lbrace
+          (separate_map (semi ^^ hardline) codegen_ctor ctors ^^ semi)
+          rbrace
+     ^^ semi ^^ twice hardline
+
+  | CTD_variant (id, tus) ->
+     let codegen_tu (ctor_id, ctyp) =
+       separate space [string "struct"; lbrace; string (sgen_ctyp ctyp); codegen_uid ctor_id ^^ semi; rbrace]
+     in
+     ksprintf string "// union %s" (string_of_id id) ^^ hardline
+     ^^ string "enum" ^^ space
+     ^^ string ("kind_" ^ sgen_id id) ^^ space
+     ^^ separate space [ lbrace;
+                         separate_map (comma ^^ space) (fun id -> string ("Kind_" ^ sgen_uid id)) (List.map fst tus);
+                         rbrace ^^ semi ]
+     ^^ twice hardline
+     ^^ string "struct" ^^ space ^^ codegen_id id ^^ space
+     ^^ surround 2 0 lbrace
+                 (separate space [string "enum"; string ("kind_" ^ sgen_id id); string "kind" ^^ semi]
+                  ^^ hardline
+                  ^^ string "union" ^^ space
+                  ^^ surround 2 0 lbrace
+                              (separate_map (semi ^^ hardline) codegen_tu tus ^^ semi)
+                              rbrace
+                  ^^ semi)
+                 rbrace
+     ^^ semi
+     ^^ twice hardline
+
+let codegen_type_def_body ctx = function
+  | CTD_enum (id, ((first_id :: _) as ids)) ->
+     let codegen_eq =
+       let name = sgen_id id in
+       string (Printf.sprintf "bool eq_%s(enum %s op1, enum %s op2) { return op1 == op2; }" name name name)
+     in
+     let codegen_undefined =
+       let name = sgen_id id in
+       string (Printf.sprintf "enum %s UNDEFINED(%s)(unit u) { return %s; }" name name (sgen_id first_id))
+     in
+     codegen_eq
+     ^^ twice hardline
+     ^^ codegen_undefined
+
+  | CTD_enum (id, []) -> Reporting.unreachable Parse_ast.Unknown __POS__ ("Cannot compile empty enum " ^ string_of_id id)
+
+  | CTD_struct (id, ctors) ->
+     let struct_ctyp = CT_struct (id, ctors) in
+     (* Generate a set_T function for every struct T *)
+     let codegen_set (id, ctyp) =
+       if is_stack_ctyp ctyp then
+         string (Printf.sprintf "rop->%s = op.%s;" (sgen_uid id) (sgen_uid id))
+       else
+         string (Printf.sprintf "COPY(%s)(&rop->%s, op.%s);" (sgen_ctyp_name ctyp) (sgen_uid id) (sgen_uid id))
+     in
+     let codegen_setter id ctors =
+       string (let n = sgen_id id in Printf.sprintf "static void COPY(%s)(struct %s *rop, const struct %s op)" n n n) ^^ space
+       ^^ surround 2 0 lbrace
+                   (separate_map hardline codegen_set (UBindings.bindings ctors))
+                   rbrace
+     in
+     (* Generate an init/clear_T function for every struct T *)
+     let codegen_field_init f (id, ctyp) =
+       if not (is_stack_ctyp ctyp) then
+         [string (Printf.sprintf "%s(%s)(&op->%s);" f (sgen_ctyp_name ctyp) (sgen_uid id))]
+       else []
+     in
+     let codegen_init f id ctors =
+       string (let n = sgen_id id in Printf.sprintf "static void %s(%s)(struct %s *op)" f n n) ^^ space
+       ^^ surround 2 0 lbrace
+                   (separate hardline (UBindings.bindings ctors |> List.map (codegen_field_init f) |> List.concat))
+                   rbrace
+     in
+     let codegen_eq =
+       let codegen_eq_test (id, ctyp) =
+         string (Printf.sprintf "EQUAL(%s)(op1.%s, op2.%s)" (sgen_ctyp_name ctyp) (sgen_uid id) (sgen_uid id))
+       in
+       string (Printf.sprintf "static bool EQUAL(%s)(struct %s op1, struct %s op2)" (sgen_id id) (sgen_id id) (sgen_id id))
+       ^^ space
+       ^^ surround 2 0 lbrace
+            (string "return" ^^ space
+             ^^ separate_map (string " && ") codegen_eq_test ctors
+             ^^ string ";")
+            rbrace
+     in
+     (* Generate the struct and add the generated functions *)
+     let codegen_ctor (id, ctyp) =
+       string (sgen_ctyp ctyp) ^^ space ^^ codegen_uid id
+     in
+     codegen_setter id (ctor_bindings ctors)
+     ^^ (if not (is_stack_ctyp struct_ctyp) then
+           twice hardline
+           ^^ codegen_init "CREATE" id (ctor_bindings ctors)
+           ^^ twice hardline
+           ^^ codegen_init "RECREATE" id (ctor_bindings ctors)
+           ^^ twice hardline
+           ^^ codegen_init "KILL" id (ctor_bindings ctors)
+         else empty)
+     ^^ twice hardline
+     ^^ codegen_eq
+
+  | CTD_variant (id, tus) ->
+     let codegen_tu (ctor_id, ctyp) =
+       separate space [string "struct"; lbrace; string (sgen_ctyp ctyp); codegen_uid ctor_id ^^ semi; rbrace]
+     in
+     (* Create an if, else if, ... block that does something for each constructor *)
+     let rec each_ctor v f = function
+       | [] -> string "{}"
+       | [(ctor_id, ctyp)] ->
+          string (Printf.sprintf "if (%skind == Kind_%s)" v (sgen_uid ctor_id)) ^^ lbrace ^^ hardline
+          ^^ jump 0 2 (f ctor_id ctyp)
+          ^^ hardline ^^ rbrace
+       | (ctor_id, ctyp) :: ctors ->
+          string (Printf.sprintf "if (%skind == Kind_%s) " v (sgen_uid ctor_id)) ^^ lbrace ^^ hardline
+          ^^ jump 0 2 (f ctor_id ctyp)
+          ^^ hardline ^^ rbrace ^^ string " else " ^^ each_ctor v f ctors
+     in
+     let codegen_init =
+       let n = sgen_id id in
+       let ctor_id, ctyp = List.hd tus in
+       string (Printf.sprintf "static void CREATE(%s)(struct %s *op)" n n)
+       ^^ hardline
+       ^^ surround 2 0 lbrace
+                   (string (Printf.sprintf "op->kind = Kind_%s;" (sgen_uid ctor_id)) ^^ hardline
+                    ^^ if not (is_stack_ctyp ctyp) then
+                         string (Printf.sprintf "CREATE(%s)(&op->%s);" (sgen_ctyp_name ctyp) (sgen_uid ctor_id))
+                       else empty)
+                   rbrace
+     in
+     let codegen_reinit =
+       let n = sgen_id id in
+       string (Printf.sprintf "static void RECREATE(%s)(struct %s *op) {}" n n)
+     in
+     let clear_field v ctor_id ctyp =
+       if is_stack_ctyp ctyp then
+         string (Printf.sprintf "/* do nothing */")
+       else
+         string (Printf.sprintf "KILL(%s)(&%s->%s);" (sgen_ctyp_name ctyp) v (sgen_uid ctor_id))
+     in
+     let codegen_clear =
+       let n = sgen_id id in
+       string (Printf.sprintf "static void KILL(%s)(struct %s *op)" n n) ^^ hardline
+       ^^ surround 2 0 lbrace
+                   (each_ctor "op->" (clear_field "op") tus ^^ semi)
+                   rbrace
+     in
+     let codegen_ctor (ctor_id, ctyp) =
+       let ctor_args = Printf.sprintf "%s op" (sgen_ctyp ctyp) in
+       string (Printf.sprintf "static void %s(%sstruct %s *rop, %s)" (sgen_function_uid ctor_id) (extra_params ()) (sgen_id id) ctor_args) ^^ hardline
+       ^^ surround 2 0 lbrace
+                   (each_ctor "rop->" (clear_field "rop") tus ^^ hardline
+                    ^^ string ("rop->kind = Kind_" ^ sgen_uid ctor_id) ^^ semi ^^ hardline
+                    ^^ if is_stack_ctyp ctyp then
+                         string (Printf.sprintf "rop->%s = op;" (sgen_uid ctor_id))
+                       else
+                         string (Printf.sprintf "CREATE(%s)(&rop->%s);" (sgen_ctyp_name ctyp) (sgen_uid ctor_id)) ^^ hardline
+                         ^^ string (Printf.sprintf "COPY(%s)(&rop->%s, op);" (sgen_ctyp_name ctyp) (sgen_uid ctor_id)))
+                   rbrace
+     in
+     let codegen_setter =
+       let n = sgen_id id in
+       let set_field ctor_id ctyp =
+         if is_stack_ctyp ctyp then
+           string (Printf.sprintf "rop->%s = op.%s;" (sgen_uid ctor_id) (sgen_uid ctor_id))
+         else
+           string (Printf.sprintf "CREATE(%s)(&rop->%s);" (sgen_ctyp_name ctyp) (sgen_uid ctor_id))
+           ^^ string (Printf.sprintf " COPY(%s)(&rop->%s, op.%s);" (sgen_ctyp_name ctyp) (sgen_uid ctor_id) (sgen_uid ctor_id))
+       in
+       string (Printf.sprintf "static void COPY(%s)(struct %s *rop, struct %s op)" n n n) ^^ hardline
+       ^^ surround 2 0 lbrace
+                   (each_ctor "rop->" (clear_field "rop") tus
+                    ^^ semi ^^ hardline
+                    ^^ string "rop->kind = op.kind"
+                    ^^ semi ^^ hardline
+                    ^^ each_ctor "op." set_field tus)
+                   rbrace
+     in
+     let codegen_eq =
+       let codegen_eq_test ctor_id ctyp =
+         string (Printf.sprintf "return EQUAL(%s)(op1.%s, op2.%s);" (sgen_ctyp_name ctyp) (sgen_uid ctor_id) (sgen_uid ctor_id))
+       in
+       let rec codegen_eq_tests = function
+         | [] -> string "return false;"
+         | (ctor_id, ctyp) :: ctors ->
+            string (Printf.sprintf "if (op1.kind == Kind_%s && op2.kind == Kind_%s) " (sgen_uid ctor_id) (sgen_uid ctor_id)) ^^ lbrace ^^ hardline
+            ^^ jump 0 2 (codegen_eq_test ctor_id ctyp)
+            ^^ hardline ^^ rbrace ^^ string " else " ^^ codegen_eq_tests ctors
+       in
+       let n = sgen_id id in
+       string (Printf.sprintf "static bool EQUAL(%s)(struct %s op1, struct %s op2) " n n n)
+       ^^ surround 2 0 lbrace (codegen_eq_tests tus) rbrace
+     in
+     codegen_init
+     ^^ twice hardline
+     ^^ codegen_reinit
+     ^^ twice hardline
+     ^^ codegen_clear
+     ^^ twice hardline
+     ^^ codegen_setter
+     ^^ twice hardline
+     ^^ codegen_eq
+     ^^ twice hardline
+     ^^ separate_map (twice hardline) codegen_ctor tus
+
+let codegen_type_def ctx ctype_def =
+  codegen_type_def_header ctype_def, codegen_type_def_body ctx ctype_def
+     
+(**************************************************************************)
+(* Code generation for generated types (lists, tuples, etc)               *)
+(**************************************************************************)
+     
+(** GLOBAL: because C doesn't have real anonymous tuple types
+   (anonymous structs don't quite work the way we need) every tuple
+   type in the spec becomes some generated named struct in C. This is
+   done in such a way that every possible tuple type has a unique name
+   associated with it. This global variable keeps track of these
+   generated struct names, so we never generate two copies of the
+   struct that is used to represent them in C.
+
+   The way this works is that codegen_def scans each definition's type
+   annotations for tuple types and generates the required structs
+   using codegen_type_def before the actual definition is generated by
+   codegen_def'.
+
+   This variable should be reset to empty only when the entire AST has
+   been translated to C. **)
+let generated = ref IdSet.empty
+
+let codegen_tup ctx ctyps =
+  let id = mk_id ("tuple_" ^ string_of_ctyp (CT_tup ctyps)) in
+  if IdSet.mem id !generated then
+    empty, empty
+  else
+    begin
+      let _, fields = List.fold_left (fun (n, fields) ctyp -> n + 1, UBindings.add (mk_id ("tup" ^ string_of_int n), []) ctyp fields)
+                                     (0, UBindings.empty)
+                                     ctyps
+      in
+      generated := IdSet.add id !generated;
+      codegen_type_def ctx (CTD_struct (id, UBindings.bindings fields))
+    end
+ 
+let codegen_list_header id =
+  ksprintf string "// generated list type %s" (string_of_id id) ^^ hardline
+  ^^ ksprintf string "struct node_%s;" (sgen_id id) ^^ hardline
+  ^^ ksprintf string "typedef struct node_%s *%s;" (sgen_id id) (sgen_id id)
+  ^^ twice hardline
+ 
+let codegen_node id ctyp =
+  ksprintf string "struct node_%s {\n  %s hd;\n  struct node_%s *tl;\n};\n" (sgen_id id) (sgen_ctyp ctyp) (sgen_id id)
+  ^^ ksprintf string "typedef struct node_%s *%s;" (sgen_id id) (sgen_id id)
+
+let codegen_list_init id =
+  ksprintf string "static void CREATE(%s)(%s *rop) { *rop = NULL; }" (sgen_id id) (sgen_id id)
+
+let codegen_list_clear id ctyp =
+  ksprintf string "static void KILL(%s)(%s *rop) {\n" (sgen_id id) (sgen_id id)
+  ^^ ksprintf string "  if (*rop == NULL) return;"
+  ^^ (if is_stack_ctyp ctyp then empty
+      else ksprintf string "  KILL(%s)(&(*rop)->hd);\n" (sgen_ctyp_name ctyp))
+  ^^ ksprintf string "  KILL(%s)(&(*rop)->tl);\n" (sgen_id id)
+  ^^ string "  sail_free(*rop);"
+  ^^ string "}"
+
+let codegen_list_recreate id =
+  ksprintf string "static void RECREATE(%s)(%s *rop) { KILL(%s)(rop); *rop = NULL; }" (sgen_id id) (sgen_id id) (sgen_id id)
+
+let codegen_list_set id ctyp =
+  ksprintf string "static void internal_set_%s(%s *rop, const %s op) {\n" (sgen_id id) (sgen_id id) (sgen_id id)
+  ^^ string "  if (op == NULL) { *rop = NULL; return; };\n"
+  ^^ ksprintf string "  *rop = sail_malloc(sizeof(struct node_%s));\n" (sgen_id id)
+  ^^ (if is_stack_ctyp ctyp then
+        string "  (*rop)->hd = op->hd;\n"
+      else
+        ksprintf string "  CREATE(%s)(&(*rop)->hd);\n" (sgen_ctyp_name ctyp)
+        ^^ ksprintf string "  COPY(%s)(&(*rop)->hd, op->hd);\n" (sgen_ctyp_name ctyp))
+  ^^ ksprintf string "  internal_set_%s(&(*rop)->tl, op->tl);\n" (sgen_id id)
+  ^^ string "}"
+  ^^ twice hardline
+  ^^ ksprintf string "static void COPY(%s)(%s *rop, const %s op) {\n" (sgen_id id) (sgen_id id) (sgen_id id)
+  ^^ ksprintf string "  KILL(%s)(rop);\n" (sgen_id id)
+  ^^ ksprintf string "  internal_set_%s(rop, op);\n" (sgen_id id)
+  ^^ string "}"
+
+let codegen_cons id ctyp =
+  let cons_id = mk_id ("cons#" ^ string_of_ctyp ctyp) in
+  ksprintf string "static void %s(%s *rop, const %s x, const %s xs) {\n" (sgen_function_id cons_id) (sgen_id id) (sgen_ctyp ctyp) (sgen_id id)
+  ^^ ksprintf string "  *rop = sail_malloc(sizeof(struct node_%s));\n" (sgen_id id)
+  ^^ (if is_stack_ctyp ctyp then
+        string "  (*rop)->hd = x;\n"
+      else
+        ksprintf string "  CREATE(%s)(&(*rop)->hd);\n" (sgen_ctyp_name ctyp)
+        ^^ ksprintf string "  COPY(%s)(&(*rop)->hd, x);\n" (sgen_ctyp_name ctyp))
+  ^^ string "  (*rop)->tl = xs;\n"
+  ^^ string "}"
+
+let codegen_pick id ctyp =
+  if is_stack_ctyp ctyp then
+    ksprintf string "static %s pick_%s(const %s xs) { return xs->hd; }" (sgen_ctyp ctyp) (sgen_ctyp_name ctyp) (sgen_id id)
+  else
+    ksprintf string "static void pick_%s(%s *x, const %s xs) { COPY(%s)(x, xs->hd); }" (sgen_ctyp_name ctyp) (sgen_ctyp ctyp) (sgen_id id) (sgen_ctyp_name ctyp)
+
+let codegen_list_equal id ctyp =
+  ksprintf string "static bool EQUAL(%s)(const %s op1, const %s op2) {\n" (sgen_id id) (sgen_id id) (sgen_id id)
+  ^^ ksprintf string "  if (op1 == NULL && op2 == NULL) { return true; };\n"
+  ^^ ksprintf string "  if (op1 == NULL || op2 == NULL) { return false; };\n"
+  ^^ ksprintf string "  return EQUAL(%s)(op1->hd, op2->hd) && EQUAL(%s)(op1->tl, op2->tl);\n" (sgen_ctyp_name ctyp) (sgen_id id)
+  ^^ string "}"
+
+let codegen_list_undefined id ctyp =
+  ksprintf string "static void UNDEFINED(%s)(%s *rop, %s u) {\n" (sgen_id id) (sgen_id id) (sgen_ctyp ctyp)
+  ^^ ksprintf string "  *rop = NULL;\n"
+  ^^ string "}"
+  
+let codegen_list ctx ctyp =
+  let id = mk_id (string_of_ctyp (CT_list ctyp)) in
+  if IdSet.mem id !generated then (
+    (empty, empty)
+  ) else (
+    generated := IdSet.add id !generated;
+    let header = codegen_list_header id in
+    let body =
+      codegen_node id ctyp ^^ twice hardline
+      ^^ codegen_list_init id ^^ twice hardline
+      ^^ codegen_list_clear id ctyp ^^ twice hardline
+      ^^ codegen_list_recreate id ^^ twice hardline
+      ^^ codegen_list_set id ctyp ^^ twice hardline
+      ^^ codegen_cons id ctyp ^^ twice hardline
+      ^^ codegen_pick id ctyp ^^ twice hardline
+      ^^ codegen_list_equal id ctyp ^^ twice hardline
+      ^^ codegen_list_undefined id ctyp
+    in
+    (header, body)
+  )
+
+(* Generate functions for working with non-bit vectors of some specific type. *)
+let codegen_vector_header ctx id (direction, ctyp) =
+  let vector_typedef =
+    string (Printf.sprintf "struct %s {\n  size_t len;\n  %s *data;\n};\n" (sgen_id id) (sgen_ctyp ctyp))
+    ^^ string (Printf.sprintf "typedef struct %s %s;" (sgen_id id) (sgen_id id))
+  in
+  vector_typedef ^^ twice hardline
+  
+let codegen_vector_body ctx id (direction, ctyp) =
+  let vector_init =
+    string (Printf.sprintf "static void CREATE(%s)(%s *rop) {\n  rop->len = 0;\n  rop->data = NULL;\n}" (sgen_id id) (sgen_id id))
+  in
+  let vector_set =
+    string (Printf.sprintf "static void COPY(%s)(%s *rop, %s op) {\n" (sgen_id id) (sgen_id id) (sgen_id id))
+    ^^ string (Printf.sprintf "  KILL(%s)(rop);\n" (sgen_id id))
+    ^^ string "  rop->len = op.len;\n"
+    ^^ string (Printf.sprintf "  rop->data = sail_malloc((rop->len) * sizeof(%s));\n" (sgen_ctyp ctyp))
+    ^^ string "  for (int i = 0; i < op.len; i++) {\n"
+    ^^ string (if is_stack_ctyp ctyp then
+                 "    (rop->data)[i] = op.data[i];\n"
+               else
+                 Printf.sprintf "    CREATE(%s)((rop->data) + i);\n    COPY(%s)((rop->data) + i, op.data[i]);\n" (sgen_ctyp_name ctyp) (sgen_ctyp_name ctyp))
+    ^^ string "  }\n"
+    ^^ string "}"
+  in
+  let vector_clear =
+    string (Printf.sprintf "static void KILL(%s)(%s *rop) {\n" (sgen_id id) (sgen_id id))
+    ^^ (if is_stack_ctyp ctyp then empty
+        else
+          string "  for (int i = 0; i < (rop->len); i++) {\n"
+          ^^ string (Printf.sprintf "    KILL(%s)((rop->data) + i);\n" (sgen_ctyp_name ctyp))
+          ^^ string "  }\n")
+    ^^ string "  if (rop->data != NULL) sail_free(rop->data);\n"
+    ^^ string "}"
+  in
+  let vector_update =
+    string (Printf.sprintf "static void vector_update_%s(%s *rop, %s op, sail_int n, %s elem) {\n" (sgen_id id) (sgen_id id) (sgen_id id) (sgen_ctyp ctyp))
+    ^^ string "  int m = sail_int_get_ui(n);\n"
+    ^^ string "  if (rop->data == op.data) {\n"
+    ^^ string (if is_stack_ctyp ctyp then
+                 "    rop->data[m] = elem;\n"
+               else
+                 Printf.sprintf "  COPY(%s)((rop->data) + m, elem);\n" (sgen_ctyp_name ctyp))
+    ^^ string "  } else {\n"
+    ^^ string (Printf.sprintf "    COPY(%s)(rop, op);\n" (sgen_id id))
+    ^^ string (if is_stack_ctyp ctyp then
+                 "    rop->data[m] = elem;\n"
+               else
+                 Printf.sprintf "  COPY(%s)((rop->data) + m, elem);\n" (sgen_ctyp_name ctyp))
+    ^^ string "  }\n"
+    ^^ string "}"
+  in
+  let internal_vector_update =
+    string (Printf.sprintf "static void internal_vector_update_%s(%s *rop, %s op, const int64_t n, %s elem) {\n" (sgen_id id) (sgen_id id) (sgen_id id) (sgen_ctyp ctyp))
+    ^^ string (if is_stack_ctyp ctyp then
+                 "  rop->data[n] = elem;\n"
+               else
+                 Printf.sprintf "  COPY(%s)((rop->data) + n, elem);\n" (sgen_ctyp_name ctyp))
+    ^^ string "}"
+  in
+  let vector_access =
+    if is_stack_ctyp ctyp then
+      string (Printf.sprintf "static %s vector_access_%s(%s op, sail_int n) {\n" (sgen_ctyp ctyp) (sgen_id id) (sgen_id id))
+      ^^ string "  int m = sail_int_get_ui(n);\n"
+      ^^ string "  return op.data[m];\n"
+      ^^ string "}"
+    else
+      string (Printf.sprintf "static void vector_access_%s(%s *rop, %s op, sail_int n) {\n" (sgen_id id) (sgen_ctyp ctyp) (sgen_id id))
+      ^^ string "  int m = sail_int_get_ui(n);\n"
+      ^^ string (Printf.sprintf "  COPY(%s)(rop, op.data[m]);\n" (sgen_ctyp_name ctyp))
+      ^^ string "}"
+  in
+  let internal_vector_init =
+    string (Printf.sprintf "static void internal_vector_init_%s(%s *rop, const int64_t len) {\n" (sgen_id id) (sgen_id id))
+    ^^ string "  rop->len = len;\n"
+    ^^ string (Printf.sprintf "  rop->data = sail_malloc(len * sizeof(%s));\n" (sgen_ctyp ctyp))
+    ^^ (if not (is_stack_ctyp ctyp) then
+          string "  for (int i = 0; i < len; i++) {\n"
+          ^^ string (Printf.sprintf "    CREATE(%s)((rop->data) + i);\n" (sgen_ctyp_name ctyp))
+          ^^ string "  }\n"
+        else empty)
+    ^^ string "}"
+  in
+  let vector_undefined =
+    string (Printf.sprintf "static void undefined_vector_%s(%s *rop, sail_int len, %s elem) {\n" (sgen_id id) (sgen_id id) (sgen_ctyp ctyp))
+    ^^ string (Printf.sprintf "  rop->len = sail_int_get_ui(len);\n")
+    ^^ string (Printf.sprintf "  rop->data = sail_malloc((rop->len) * sizeof(%s));\n" (sgen_ctyp ctyp))
+    ^^ string "  for (int i = 0; i < (rop->len); i++) {\n"
+    ^^ string (if is_stack_ctyp ctyp then
+                 "    (rop->data)[i] = elem;\n"
+               else
+                 Printf.sprintf "    CREATE(%s)((rop->data) + i);\n    COPY(%s)((rop->data) + i, elem);\n" (sgen_ctyp_name ctyp) (sgen_ctyp_name ctyp))
+    ^^ string "  }\n"
+    ^^ string "}"
+  in
+  vector_init ^^ twice hardline
+  ^^ vector_clear ^^ twice hardline
+  ^^ vector_undefined ^^ twice hardline
+  ^^ vector_access ^^ twice hardline
+  ^^ vector_set ^^ twice hardline
+  ^^ vector_update ^^ twice hardline
+  ^^ internal_vector_update ^^ twice hardline
+  ^^ internal_vector_init ^^ twice hardline
+  
+let codegen_vector ctx (direction, ctyp) =
+  let id = mk_id (string_of_ctyp (CT_vector (direction, ctyp))) in
+  if IdSet.mem id !generated then (
+    empty, empty
+  ) else (
+    generated := IdSet.add id !generated;
+    codegen_vector_header ctx id (direction, ctyp),
+    codegen_vector_body ctx id (direction, ctyp)
+  )
+  
+(**************************************************************************)
+(* Code generation for definitions                                        *)
+(**************************************************************************)
+
+(** To keep things neat we use GCC's local labels extension to limit
+   the scope of labels. We do this by iterating over all the blocks
+   and adding a __label__ declaration with all the labels local to
+   that block.
+
+   See https://gcc.gnu.org/onlinedocs/gcc/Local-Labels.html **)
+let add_local_labels' instrs =
+  let is_label (I_aux (instr, _)) =
+    match instr with
+    | I_label str -> [str]
+    | _ -> []
+  in
+  let labels = List.concat (List.map is_label instrs) in
+  let local_label_decl = iraw ("__label__ " ^ String.concat ", " labels ^ ";\n") in
+  if labels = [] then
+    instrs
+  else
+    local_label_decl :: instrs
+
+let is_decl = function
+  | I_aux (I_decl _, _) -> true
+  | _ -> false
+  
+let codegen_decl = function
+  | I_aux (I_decl (ctyp, id), _) ->
+     string (Printf.sprintf "%s %s;" (sgen_ctyp ctyp) (sgen_name id))
+  | _ -> assert false
+
+let codegen_alloc = function
+  | I_aux (I_decl (ctyp, id), _) when is_stack_ctyp ctyp -> empty
+  | I_aux (I_decl (ctyp, id), _) ->
+     string (Printf.sprintf "  CREATE(%s)(&%s);" (sgen_ctyp_name ctyp) (sgen_name id))
+  | _ -> assert false
+       
+let add_local_labels instrs =
+  match map_instrs add_local_labels' (iblock instrs) with
+  | I_aux (I_block instrs, _) -> instrs
+  | _ -> assert false
+  
+let codegen_def_header ctx = function
+  | CDEF_spec (id, _, arg_ctyps, ret_ctyp) ->
+     if Env.is_extern id ctx.tc_env "c" then
+       empty
+     else if is_stack_ctyp ret_ctyp then
+       ksprintf string "%s %s(%s%s);"
+         (sgen_ctyp ret_ctyp) (sgen_function_id id) (extra_params ()) (Util.string_of_list ", " sgen_ctyp arg_ctyps)
+       ^^ twice hardline
+     else
+       ksprintf string "void %s(%s%s *rop, %s);"
+         (sgen_function_id id) (extra_params ()) (sgen_ctyp ret_ctyp) (Util.string_of_list ", " sgen_ctyp arg_ctyps)
+       ^^ twice hardline
+
+  | CDEF_type ctype_def ->
+     codegen_type_def_header ctype_def
+ 
+  | _ -> empty
+
+let codegen_def_body ctx = function
+  | CDEF_reg_dec _ -> empty
+
+  | CDEF_spec _ -> empty
+     
+  | CDEF_fundef (id, ret_arg, args, instrs) as def ->
+     let arg_ctyps, ret_ctyp = match Bindings.find_opt id ctx.valspecs with
+       | Some vs -> vs
+       | None ->
+          Reporting.unreachable (id_loc id) __POS__ ("No valspec found for " ^ string_of_id id)
+     in
+
+     (* Check that the function has the correct arity at this point. *)
+     if List.length arg_ctyps <> List.length args then
+       Reporting.unreachable (id_loc id) __POS__
+         ("function arguments "
+          ^ Util.string_of_list ", " string_of_id args
+          ^ " matched against type "
+          ^ Util.string_of_list ", " string_of_ctyp arg_ctyps)
+     else ();
+
+     let instrs = add_local_labels instrs in
+     let args = Util.string_of_list ", " (fun x -> x) (List.map2 (fun ctyp arg -> sgen_ctyp ctyp ^ " " ^ sgen_id arg) arg_ctyps args) in
+     let function_header =
+       match ret_arg with
+       | None ->
+          assert (is_stack_ctyp ret_ctyp);
+          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));
+          string "void" ^^ space ^^ codegen_function_id id
+          ^^ parens (string (extra_params ()) ^^ string (sgen_ctyp ret_ctyp ^ " *" ^ sgen_id gs ^ ", ") ^^ string args)
+          ^^ hardline
+     in
+     function_header
+     ^^ string "{"
+     ^^ jump 0 2 (separate_map hardline (codegen_instr id ctx) instrs) ^^ hardline
+     ^^ string "}"
+     ^^ twice hardline
+
+  | CDEF_type ctype_def ->
+     codegen_type_def_body ctx ctype_def
+
+  | CDEF_startup (id, instrs) ->
+     let startup_header = string (Printf.sprintf "void startup_%s(void)" (sgen_function_id id)) in
+     separate_map hardline codegen_decl instrs
+     ^^ twice hardline
+     ^^ startup_header ^^ hardline
+     ^^ string "{"
+     ^^ jump 0 2 (separate_map hardline codegen_alloc instrs) ^^ hardline
+     ^^ string "}"
+
+  | CDEF_finish (id, instrs) ->
+     let finish_header = string (Printf.sprintf "void finish_%s(void)" (sgen_function_id id)) in
+     separate_map hardline codegen_decl (List.filter is_decl instrs)
+     ^^ twice hardline
+     ^^ finish_header ^^ hardline
+     ^^ string "{"
+     ^^ jump 0 2 (separate_map hardline (codegen_instr id ctx) instrs) ^^ hardline
+     ^^ string "}"
+
+  | CDEF_let (number, bindings, instrs) ->
+     let instrs = add_local_labels instrs in
+     let setup =
+       List.concat (List.map (fun (id, ctyp) -> [idecl ctyp (global id)]) bindings)
+     in
+     let cleanup =
+       List.concat (List.map (fun (id, ctyp) -> [iclear ctyp (global id)]) bindings)
+     in
+     hardline ^^ string (Printf.sprintf "void sail_create_letbind_%d(sail_state *state) " number)
+     ^^ string "{"
+     ^^ jump 0 2 (separate_map hardline codegen_alloc setup) ^^ hardline
+     ^^ jump 0 2 (separate_map hardline (codegen_instr (mk_id "let") { ctx with no_raw = true }) instrs) ^^ hardline
+     ^^ string "}"
+     ^^ hardline ^^ string (Printf.sprintf "void sail_kill_letbind_%d(sail_state *state) " number)
+     ^^ string "{"
+     ^^ jump 0 2 (separate_map hardline (codegen_instr (mk_id "let") ctx) cleanup) ^^ hardline
+     ^^ string "}"
+     ^^ twice hardline
+ 
+(** As we generate C we need to generate specialized version of tuple,
+   list, and vector type. These must be generated in the correct
+   order. The ctyp_dependencies function generates a list of
+   c_gen_typs in the order they must be generated. Types may be
+   repeated in ctyp_dependencies so it's up to the code-generator not
+   to repeat definitions pointlessly (using the !generated variable)
+   *)
+type c_gen_typ =
+  | CTG_tup of ctyp list
+  | CTG_list of ctyp
+  | CTG_vector of bool * ctyp
+
+let rec ctyp_dependencies = function
+  | CT_tup ctyps -> List.concat (List.map ctyp_dependencies ctyps) @ [CTG_tup ctyps]
+  | CT_list ctyp -> ctyp_dependencies ctyp @ [CTG_list ctyp]
+  | CT_vector (direction, ctyp) | CT_fvector (_, direction, ctyp) -> ctyp_dependencies ctyp @ [CTG_vector (direction, ctyp)]
+  | CT_ref ctyp -> ctyp_dependencies ctyp
+  | CT_struct (_, ctors) -> List.concat (List.map (fun (_, ctyp) -> ctyp_dependencies ctyp) ctors)
+  | CT_variant (_, ctors) -> List.concat (List.map (fun (_, ctyp) -> ctyp_dependencies ctyp) ctors)
+  | CT_lint | CT_fint _ | CT_lbits _ | CT_fbits _ | CT_sbits _ | CT_unit | CT_bool | CT_real | CT_bit | CT_string | CT_enum _ | CT_poly | CT_constant _ -> []
+
+let codegen_ctg ctx = function
+  | CTG_vector (direction, ctyp) -> codegen_vector ctx (direction, ctyp)
+  | CTG_tup ctyps -> codegen_tup ctx ctyps
+  | CTG_list ctyp -> codegen_list ctx ctyp
+
+(** When we generate code for a definition, we need to first generate
+   any auxillary type definitions that are required. *)
+let codegen_def ctx def =
+  let ctyps = cdef_ctyps def |> CTSet.elements in
+  (* We should have erased any polymorphism introduced by variants at this point! *)
+  if List.exists is_polymorphic ctyps then
+    let polymorphic_ctyps = List.filter is_polymorphic ctyps in
+    Reporting.unreachable Parse_ast.Unknown __POS__
+      (sprintf "Found polymorphic types:\n%s\nwhile generating definition."
+         (Util.string_of_list "\n" string_of_ctyp polymorphic_ctyps))
+  else
+    let deps = List.concat (List.map ctyp_dependencies ctyps) in
+    let deps_header, deps_body = List.map (codegen_ctg ctx) deps |> List.split in
+    concat deps_header ^^ codegen_def_header ctx def,
+    concat deps_body ^^ codegen_def_body ctx def
+
+let codegen_state_struct_def ctx = function
+  | CDEF_reg_dec (id, ctyp, _) ->
+     ksprintf string "    %s %s;" (sgen_ctyp ctyp) (sgen_id id) ^^ hardline
+
+  | CDEF_let (_, [], _) -> empty
+  | CDEF_let (_, bindings, _) ->
+     separate_map hardline (fun (id, ctyp) -> string (Printf.sprintf "  %s %s;" (sgen_ctyp ctyp) (sgen_id id))) bindings
+     ^^ hardline
+
+  | _ -> empty
+
+let codegen_state_struct ctx cdefs =
+  string "struct sail_state {" ^^ hardline
+  ^^ concat_map (codegen_state_struct_def ctx) cdefs
+  ^^ (if not (Bindings.mem (mk_id "exception") ctx.variants) then (
+        empty
+      ) else (
+        string "    // exception handling support" ^^ hardline
+        ^^ ksprintf string "    struct %s *current_exception;" (sgen_id (mk_id "exception")) ^^ hardline
+        ^^ string "    bool have_exception;" ^^ hardline
+        ^^ string "    sail_string *throw_location;" ^^ hardline
+     ))
+  ^^ string "};"
+
+let is_cdef_startup = function
+  | CDEF_startup _ -> true
+  | _ -> false
+
+let sgen_startup = function
+  | CDEF_startup (id, _) ->
+     Printf.sprintf "  startup_%s();" (sgen_id id)
+  | _ -> assert false
+
+let sgen_instr id ctx instr =
+  Pretty_print_sail.to_string (codegen_instr id ctx instr)
+
+let is_cdef_finish = function
+  | CDEF_startup _ -> true
+  | _ -> false
+
+let sgen_finish = function
+  | CDEF_startup (id, _) ->
+     Printf.sprintf "  finish_%s();" (sgen_id id)
+  | _ -> assert false
+
+let rec get_recursive_functions (Defs defs) =
+  match defs with
+  | DEF_internal_mutrec fundefs :: defs ->
+     IdSet.union (List.map id_of_fundef fundefs |> IdSet.of_list) (get_recursive_functions (Defs defs))
+
+  | (DEF_fundef fdef as def) :: defs ->
+     let open Rewriter in
+     let ids = ref IdSet.empty in
+     let collect_funcalls e_aux annot =
+       match e_aux with
+       | E_app (id, args) -> (ids := IdSet.add id !ids; E_aux (e_aux, annot))
+       | _ -> E_aux (e_aux, annot)
+     in
+     let map_exp = {
+         id_exp_alg with
+         e_aux = (fun (e_aux, annot) -> collect_funcalls e_aux annot)
+       } in
+     let map_defs = { rewriters_base with rewrite_exp = (fun _ -> fold_exp map_exp) } in
+     let _ = rewrite_def map_defs def in
+     if IdSet.mem (id_of_fundef fdef) !ids then
+       IdSet.add (id_of_fundef fdef) (get_recursive_functions (Defs defs))
+     else
+       get_recursive_functions (Defs defs)
+
+  | _ :: defs -> get_recursive_functions (Defs defs)
+  | [] -> IdSet.empty
+  
+let codegen_output file_name docs =
+  let chan = open_out file_name in
+  output_string chan (Pretty_print_sail.to_string docs);
+  flush chan;
+  close_out chan
+
+let codegen ctx output_name cdefs =
+  let docs_header, docs_body = List.map (codegen_def ctx) cdefs |> List.split in
+
+  let state = codegen_state_struct ctx cdefs in
+
+  let stdlib_headers =
+    string "#include <stdint.h>" ^^ hardline
+    ^^ string "#include <stdbool.h>"
+  in
+  let sail_headers =
+    string "#include \"sail.h\"" ^^ hardline
+    ^^ string "#include \"sail_failure.h\""
+  in
+
+  let register_init_clear (id, ctyp, instrs) =
+    if is_stack_ctyp ctyp then
+      List.map (sgen_instr (mk_id "reg") ctx) instrs, []
+    else
+      [ Printf.sprintf "  CREATE(%s)(&(state->%s));" (sgen_ctyp_name ctyp) (sgen_id id) ]
+      @ List.map (sgen_instr (mk_id "reg") ctx) instrs,
+      [ Printf.sprintf "  KILL(%s)(&(state->%s));" (sgen_ctyp_name ctyp) (sgen_id id) ]
+  in
+
+  let header =
+    stdlib_headers
+    ^^ hardline
+    ^^ sail_headers ^^ twice hardline
+    ^^ string "struct sail_state;" ^^ hardline
+    ^^ string "typedef struct sail_state sail_state;"
+    ^^ twice hardline
+    ^^ concat docs_header
+    ^^ state
+    ^^ twice hardline
+    ^^ string "void sail_initialize_state(sail_state *state);"
+    ^^ hardline
+    ^^ string "void sail_finalize_state(sail_state *state);"
+    ^^ hardline
+  in
+
+  let regs = c_ast_registers cdefs in
+
+  let letbind_initializers =
+    List.map (fun n -> Printf.sprintf "  sail_create_letbind_%d(state);" n) (List.rev ctx.letbinds)
+  in
+  let letbind_finalizers =
+    List.map (fun n -> Printf.sprintf "  sail_kill_letbind_%d(state);" n) ctx.letbinds
+  in
+  
+  let body =
+    ksprintf string "#include \"%s.h\"" output_name
+    ^^ twice hardline
+    ^^ concat docs_body
+    ^^ string "void sail_initialize_letbindings(sail_state *state) {" ^^ hardline
+    ^^ separate_map hardline string letbind_initializers ^^ hardline
+    ^^ string "}"
+    ^^ twice hardline
+    ^^ string "void sail_finalize_letbindings(sail_state *state) {" ^^ hardline
+    ^^ separate_map hardline string letbind_finalizers ^^ hardline
+    ^^ string "}"
+    ^^ twice hardline
+    ^^ string "void sail_initialize_state(sail_state *state) {" ^^ hardline
+    ^^ separate_map hardline string (List.map (fun r -> fst (register_init_clear r)) regs |> List.concat)
+    ^^ (if not (Bindings.mem (mk_id "exception") ctx.variants) then (
+          empty
+        ) else (
+          string "  state->have_exception = false;"
+          ^^ ksprintf string "  state->current_exception = sail_malloc(sizeof(struct %s));"
+            (sgen_id (mk_id "exception")) ^^ hardline
+          ^^ ksprintf string "  CREATE(%s)(state->current_exception);" (sgen_id (mk_id "exception")) ^^ hardline
+          ^^ string "  state->throw_location = sail_malloc(sizeof(sail_string));" ^^ hardline
+          ^^ string "  CREATE(sail_string)(state->throw_location);"
+       ))
+    ^^ hardline
+    ^^ string "  sail_initialize_letbindings(state);"  ^^ hardline
+    ^^ string "}"
+    ^^ twice hardline
+    ^^ string "void sail_finalize_state(sail_state *state) {" ^^ hardline
+    ^^ separate_map hardline string (List.map (fun r -> snd (register_init_clear r)) regs |> List.concat)
+    ^^ (if not (Bindings.mem (mk_id "exception") ctx.variants) then (
+          empty
+        ) else (
+          ksprintf string "  KILL(%s)(state->current_exception);" (sgen_id (mk_id "exception")) ^^ hardline
+          ^^ string "  sail_free(state->current_exception);" ^^ hardline
+          ^^ string "  KILL(sail_string)(state->throw_location);" ^^ hardline
+          ^^ string "  sail_free(state->throw_location);"
+       ))
+    ^^ hardline
+    ^^ string "  sail_finalize_letbindings(state);"  ^^ hardline
+    ^^ string "}"
+    ^^ hardline
+  in
+
+  codegen_output (output_name ^ ".h") header;
+  codegen_output (output_name ^ ".c") body
+
+let emulator ctx output_name cdefs =
+  codegen ctx output_name cdefs;
+
+  let preamble = separate hardline
+                   ((if !opt_no_lib then [] else
+                       [ string "#include \"sail.h\"";
+                         string "#include \"sail_failure.h\"" ])
+                    @ (if !opt_no_rts then [] else
+                         [ string "#include \"rts.h\"";
+                           string "#include \"elf.h\"" ])
+                    @ [ ksprintf string "#include \"%s.h\"" output_name ]
+                    @ (List.map (fun h -> string (Printf.sprintf "#include \"%s\"" h)) [] (*c_includes*)))
+  in
+ 
+  let startup cdefs =
+    List.map sgen_startup (List.filter is_cdef_startup cdefs)
+  in
+  let finish cdefs =
+    List.map sgen_finish (List.filter is_cdef_finish cdefs)
+  in
+
+  let regs = c_ast_registers cdefs in
+ 
+  let model_init = separate hardline (List.map string
+     ( [ "void model_init(sail_state *state)";
+         "{";
+         "  sail_initialize_state(state);";
+         "  setup_rts();" ]
+     @ startup cdefs
+     @ (if regs = [] then [] else [ Printf.sprintf "  %s(state, UNIT);" (sgen_function_id (mk_id "initialize_registers")) ])
+     @ [ "}" ] ))
+  in
+
+  let model_fini = separate hardline (List.map string
+     ( [ "void model_fini(sail_state *state)";
+         "{" ]
+     @ finish cdefs
+     @ [ "  cleanup_rts();";
+         "  sail_finalize_state(state);";
+         "}" ]))
+  in
+
+  let model_default_main = separate hardline (List.map string
+       ([ "int model_main(int argc, char *argv[])";
+          "{";
+          "  sail_state state;";
+          "  model_init(&state);";
+          "  if (process_arguments(argc, argv)) exit(EXIT_FAILURE);";
+          sprintf "  %s(&state, UNIT);" (sgen_function_id (mk_id "main")) ]
+        @ (if not (Bindings.mem (mk_id "exception") ctx.variants) then [] else
+             [ "  if (state.have_exception) {fprintf(stderr, \"Exiting due to uncaught exception: %s\\n\", *state.throw_location);}" ])
+        @ [ "  model_fini(&state);" ]
+        @ (if not (Bindings.mem (mk_id "exception") ctx.variants) then [] else
+             [ "  if (state.have_exception) {return(EXIT_FAILURE);}" ])
+        @ [ "  return EXIT_SUCCESS;";
+            "}" ]))
+  in
+
+  let model_main = separate hardline (if (!opt_no_main) then [] else List.map string
+       [ "int main(int argc, char *argv[])";
+         "{";
+         "  return model_main(argc, argv);";
+         "}" ] )
+  in
+
+  let hlhl = hardline ^^ hardline in
+  let emu =
+    preamble ^^ hlhl
+    ^^ (if not !opt_no_rts then
+          model_init ^^ hlhl
+          ^^ model_fini ^^ hlhl
+          ^^ model_default_main ^^ hlhl
+        else
+          empty)
+    ^^ model_main ^^ hardline
+  in
+  codegen_output (output_name ^ "_emu.c") emu
+
+end