Merge branch 'sail2' into mono-tweaks

1 files changed, 1714 insertions, 0 deletions

diff --git a/src/jib/c_codegen.ml b/src/jib/c_codegen.ml
new file mode 100644
index 00000000..d5015318
--- /dev/null
+++ b/src/jib/c_codegen.ml
@@ -0,0 +1,1714 @@
+(**************************************************************************)
+(*     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 StringSet = Set.Make(String)
+module Big_int = Nat_big_num
+module Json = Yojson.Basic
+
+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 = {
+    (** Rewrites a Sail identifier into a user-specified name in the generated C *)
+    exports : string Bindings.t;
+    (** Rewrites a generated symbol after name-mangling has ocurred *)
+    exports_mangled : string StringMap.t;
+    (** Extra headers to include in the generated .h file *)
+    extra_headers : string list;
+    (** Extra lines that are included in the sail_state struct. Used
+       to add user-specified state to the structs, which can then be
+       passed to primops in state_primops *)
+    extra_state : string list;
+    (** Primitives in this set will be passed a pointer to the
+       sail_state struct *)
+    state_primops : StringSet.t;
+  }
+
+let initial_options = {
+    exports = Bindings.empty;
+    exports_mangled = StringMap.empty;
+    extra_headers = [];
+    extra_state = [];
+    state_primops = StringSet.empty;
+  }
+
+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, members) | CTD_variant (id, members) ->
+     List.fold_left add_export_uid (add_export opts id) (List.map fst members)
+
+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 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))
+
+let options_from_json json cdefs =
+  let open Json.Util in
+  let bad_key k json =
+    raise (Reporting.err_general Parse_ast.Unknown
+             (sprintf "Invalid %s key in codegen json configuration: %s" k (Json.to_string json)))
+  in
+  let opts = match member "default_exports" json with
+    | `Bool true -> default_options cdefs
+    | `Bool false -> initial_options
+    | `Null ->
+       Reporting.simple_warn "No default_exports key in codegen json configuration";
+       initial_options
+    | json -> bad_key "default_exports" json
+  in
+  let process_exports opts = function
+    | `List [`String from; `String into] -> add_custom_export opts (mk_id from) into
+    | `String str -> add_export opts (mk_id str)
+    | json -> bad_key "exports" json
+  in
+  let opts = match member "exports" json with
+    | `List exports -> List.fold_left process_exports opts exports
+    | `Null ->
+       Reporting.simple_warn "No exports key in codegen json configuration";
+       opts
+    | json -> bad_key "exports" json
+  in
+  let process_exports_mangled opts = function
+    | `List [`String from; `String into] -> add_mangled_rename opts (from, into)
+    | json -> bad_key "exports_mangled" json
+  in
+  let opts = match member "exports_mangled" json with
+    | `List exports -> List.fold_left process_exports_mangled opts exports
+    | `Null ->
+       Reporting.simple_warn "No exports_mangled key in codegen json configuration";
+       opts
+    | json -> bad_key "exports_mangled" json
+  in
+  let process_extra_header opts = function
+    | `String header -> { opts with extra_headers = header :: opts.extra_headers }
+    | json -> bad_key "extra_headers" json
+  in
+  let opts = match member "extra_headers" json with
+    | `List headers -> List.fold_left process_extra_header opts headers
+    | `Null ->
+       Reporting.simple_warn "No extra_headers key in codegen json configuration";
+       opts
+    | json -> bad_key "extra_headers" json
+  in
+  let process_extra_state opts = function
+    | `String member -> { opts with extra_state = member :: opts.extra_state }
+    | json -> bad_key "extra_state" json
+  in
+  let opts = match member "extra_state" json with
+    | `List members -> List.fold_left process_extra_state opts members
+    | `Null ->
+       Reporting.simple_warn "No extra_state key in codegen json configuration";
+       opts
+    | json -> bad_key "extra_state" json
+  in
+  opts
+
+module type Options = sig
+  val opts : codegen_options
+end
+
+module Make(O: Options) = struct
+
+let mangle str =
+  let mangled = Util.zencode_string str in
+  match StringMap.find_opt mangled O.opts.exports_mangled with
+  | Some export -> export
+  | None -> mangled
+
+let sgen_id id =
+  match Bindings.find_opt id O.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 " ^ mangle ("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 -> mangle (string_of_ctyp l)
+  | CT_vector _ as v -> mangle (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 -> mangle ("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 -> mangle (string_of_ctyp l)
+  | CT_vector _ as v -> mangle (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 ->
+     if Big_int.equal i (min_int 64) then
+       "INT64_MIN"
+     else
+       "INT64_C(" ^ Big_int.to_string i ^ ")"
+  | 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_" ^ sgen_uid (ctor, unifiers)
+  | V_struct (fields, _) ->
+     sprintf "{%s}"
+       (Util.string_of_list ", " (fun (field, cval) -> sgen_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 fname, is_extern =
+       if special_extern then
+         (string_of_id (fst f), true)
+       else if Env.is_extern (fst f) ctx.tc_env "c" then
+         (Env.get_extern (fst f) ctx.tc_env "c", true)
+       else
+         (sgen_function_uid f, false)
+     in
+     let sail_state_arg =
+       if is_extern && StringSet.mem fname O.opts.state_primops then
+         "sail_state *state, "
+       else
+         ""
+     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%s);" (sgen_clexp_pure ctx x) fname sail_state_arg (extra_arguments is_extern) c_args
+       else
+         ksprintf string "  %s(%s%s%s, %s);" fname sail_state_arg (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
+
+let codegen_progress n total = function
+  | CDEF_reg_dec (id, _, _) ->
+     Util.progress "Codegen " ("R " ^ string_of_id id) n total
+  | CDEF_fundef (id, _, _, _) ->
+     Util.progress "Codegen " (string_of_id id) n total
+  | _ ->
+     Util.progress "Codegen " "" n total
+
+(** When we generate code for a definition, we need to first generate
+   any auxillary type definitions that are required. *)
+let codegen_def n total ctx def =
+  codegen_progress n total 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
+     ))
+  ^^ concat_map (fun str -> string ("  " ^ str) ^^ hardline) O.opts.extra_state
+  ^^ 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 add_extra_header str =
+  if String.length str > 0 then (
+    if str.[0] == '<' && str.[String.length str - 1] == '>' then
+      string ("#include " ^ str) ^^ hardline
+    else
+      string ("#include \"" ^ str ^ "\"") ^^ hardline
+  ) else (
+    empty
+  )
+
+let codegen ctx output_name cdefs =
+  let total = List.length cdefs in
+  let docs_header, docs_body = List.mapi (fun n def -> codegen_def (n + 1) total ctx def) 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 ^^ hardline
+    ^^ concat_map add_extra_header O.opts.extra_headers ^^ 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\"" (Filename.basename 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 headers = separate hardline
+    ([ string "#include \"sail.h\"";
+       string "#include \"sail_failure.h\"";
+       string "#include \"rts.h\"";
+       string "#include \"elf.h\"";
+       ksprintf string "#include \"%s.h\"" (Filename.basename 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_initialize(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_finalize(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_initialize(&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_finalize(&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 (List.map string
+       [ "int main(int argc, char *argv[])";
+         "{";
+         "  return model_main(argc, argv);";
+         "}" ])
+  in
+
+  let emu =
+    headers ^^ twice hardline
+    ^^ model_init ^^ twice hardline
+    ^^ model_fini ^^ twice hardline
+    ^^ model_default_main ^^ twice hardline
+    ^^ model_main ^^ hardline
+  in
+  codegen_output (output_name ^ "_emu.c") emu
+
+end