path: root/src/jib/c_codegen.ml

(**************************************************************************)
(*     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_defs
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)

(** For now, the types that can be used in the state API are the types that fits on the stack.
    In the future, this can be expanded to support more complex types if needed. *)
let is_api_ctyp = is_stack_ctyp

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;
    (** Control which sail_state variables accessors will be implemented
       by the consumer of the library. This is a list of regular expressions,
       if one of those regular expression matches the name of a sail_state variable,
       only the declaration of the accessors will be generated. *)
    external_state_api : string list;
  }

let initial_options = {
    exports = Bindings.empty;
    exports_mangled = StringMap.empty;
    extra_headers = [];
    extra_state = [];
    state_primops = StringSet.empty;
    external_state_api = [];
  }

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_external_state_api_regex opts regex =
  { opts with external_state_api = regex :: opts.external_state_api }

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
  let process_state_primops opts = function
    | `String member -> { opts with state_primops = StringSet.add member opts.state_primops }
    | json -> bad_key "state_primops" json
  in
  let opts = match member "state_primops" json with
    | `List members -> List.fold_left process_state_primops opts members
    | `Null ->
       Reporting.simple_warn "No state_primops key in codegen json configuration";
       opts
    | json -> bad_key "state_primops" json
  in
  let process_external_state_api opts = function
    | `String member -> add_external_state_api_regex opts member
    | json -> bad_key "external_state_api" json
  in
  let opts = match member "external_state_api" json with
    | `List members -> List.fold_left process_external_state_api opts members
    | `Null ->
       Reporting.simple_warn "No external_state_api key in codegen json configuration";
       opts
    | json -> bad_key "external_state_api" 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 ctyp id =
  match id with
  | Name (id, _) ->
     sgen_id id
  | Global (id, _) ->
     if is_api_ctyp ctyp then
        sprintf "(state_get_%s(state))" (sgen_id id)
     else
        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 ctyp id
  | V_lit (vl, ctyp) -> sgen_value vl
  | V_call (op, cvals) -> sgen_call ctx op cvals
  | V_field (f, field) -> 
    begin match f with
    | V_id (Global (id, _), ctyp) when is_api_ctyp ctyp ->
       sprintf "state_get_%s_in_%s(state)" (sgen_uid field) (sgen_id id)
    | _ -> sprintf "%s.%s" (sgen_cval ctx f) (sgen_uid field)
    end
  | 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_state_api = function
  | CL_id (Global (id, _), _) -> sgen_id id
  | CL_field (clexp, field) -> sgen_uid field ^ "_in_" ^ sgen_clexp_state_api clexp 
  | _ -> assert false

let sgen_cval_state_api = function
  | V_id (Global (id, _), ctyp) -> sgen_id id
  | _ -> assert false

let rec is_state_api_cval = function
  | V_id (Global (id, _), ctyp) ->
    begin match ctyp with 
    | CT_vector (_, vctyp) -> is_api_ctyp vctyp
    | CT_fvector (_, _, vctyp) -> is_api_ctyp vctyp
    | _ when is_api_ctyp ctyp -> true
    | _ -> false
    end
  | V_field (clexp, field) -> is_state_api_cval clexp
  | _ -> false

let rec is_state_api_clexp = function
  | CL_id (Global (id, _), ctyp) ->
    begin match ctyp with 
    | CT_vector (_, vctyp) -> is_api_ctyp vctyp
    | CT_fvector (_, _, vctyp) -> is_api_ctyp vctyp
    | _ when is_api_ctyp ctyp -> true
    | _ -> false
    end
  | CL_field (clexp, field) -> is_state_api_clexp clexp
  | _ -> false

let rec sgen_clexp ctx clexp =
  match clexp with
  | 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, _), _) -> 
    let ctyp = clexp_ctyp clexp in
    if is_api_ctyp ctyp then
      "(state_get_" ^ sgen_id id ^ "(state))"
    else
      "&(state->" ^ sgen_id id ^ ")"
  | CL_id (Name (id, _), _) -> "&" ^ sgen_id id
  | CL_field (clexp, field) ->
     begin match clexp with
     | CL_id (Global (id, _), ctyp) when is_api_ctyp ctyp -> "(state_get_ " ^ sgen_uid field ^ "_in_" ^ sgen_clexp_state_api clexp ^ "(state))"
     | _ -> "&((" ^ sgen_clexp ctx clexp ^ ")->" ^ sgen_uid field ^ ")"
     end
  | 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 clexp =
  match clexp with
  | 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, _), _) ->
    let ctyp = clexp_ctyp clexp in
    assert (not (is_api_ctyp ctyp));
      "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
       if is_state_api_clexp clexp then
         ksprintf string "  state_set_%s(state, %s);" (sgen_clexp_state_api clexp) (sgen_cval ctx cval)
       else
         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) ->
    if is_state_api_clexp clexp then
     ksprintf string "  state_set_%s(state, CONVERT_OF(%s, %s)(%s));"
       (sgen_clexp_state_api clexp) (sgen_ctyp_name ctyp_to) (sgen_ctyp_name ctyp_from) (sgen_cval_param ctx cval)
    else
     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 ctyp id)
  | I_decl (ctyp, id) ->
     ksprintf string "  %s %s;" (sgen_ctyp ctyp) (sgen_name ctyp id) ^^ hardline
     ^^ ksprintf string "  CREATE(%s)(&%s);" (sgen_ctyp_name ctyp) (sgen_name ctyp 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 : string ref = ref 
       (if is_extern && StringSet.mem fname O.opts.state_primops then
         "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 :: _  when is_state_api_cval cval -> sail_state_arg := "state, "; sprintf "state_vector_access_%s" (sgen_cval_state_api cval) 
          | 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", _ -> if is_state_api_clexp x then (
                                 sail_state_arg := "state, ";
                                 sprintf "state_vector_update_%s" (sgen_clexp_state_api x))
                               else
                                 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
          if is_state_api_clexp x then
            ksprintf string "  state_set_%s(state, %s(%s%s%s));" (sgen_clexp_state_api x) fname !sail_state_arg (extra_arguments is_extern) c_args
          else
            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 ctyp 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 ctyp id)
  | I_reset (ctyp, id) ->
     ksprintf string "  RECREATE(%s)(&%s);" (sgen_ctyp_name ctyp) (sgen_name ctyp 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 ctyp gs,
          [sprintf "struct %s %s = { " (sgen_ctyp_name ctyp) (sgen_name ctyp 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 ctyp gs,
          [sprintf "struct %s %s = { " (sgen_ctyp_name ctyp) (sgen_name ctyp 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 ^^ hardline ^^
  string (Printf.sprintf "void vector_update_%s(%s *rop, %s op, sail_int n, %s elem);" (sgen_id id) (sgen_id id) (sgen_id id) (sgen_ctyp ctyp)) ^^ hardline ^^
  if is_stack_ctyp ctyp then
    string (Printf.sprintf "%s vector_access_%s(%s op, sail_int n);" (sgen_ctyp ctyp) (sgen_id id) (sgen_id id))
  else
    string "" (* Not needed in the header file at the moment *)
  ^^ 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 "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 "%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 ctyp 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 ctyp 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_function_body_on_match id body =
  let is_external = List.exists (fun regex -> Str.string_match (Str.regexp regex) id 0) O.opts.external_state_api in
  if is_external then
    ("" ,";")
  else
    ("static inline ", Printf.sprintf " { %s }" body) 

let codegen_state_api_struct id ctyp =
  match ctyp with
  | CT_struct (_, fields) ->
     let codegen_state_api_field ((fid, _), ctyp) =
       if is_api_ctyp ctyp then
         let set_attrs, set_body = codegen_state_function_body_on_match (sgen_id fid) (Printf.sprintf "st->%s.%s = u;" (sgen_id id) (sgen_id fid)) in 
         let get_attrs, get_body = codegen_state_function_body_on_match (sgen_id fid) (Printf.sprintf "return st->%s.%s;" (sgen_id id) (sgen_id fid)) in
         ksprintf string "%svoid state_set_%s_in_%s(sail_state* st, %s u)%s"
           set_attrs (sgen_id fid) (sgen_id id) (sgen_ctyp ctyp) set_body
         ^^ hardline
         ^^ ksprintf string "%s%s state_get_%s_in_%s(sail_state* st)%s"
              get_attrs (sgen_ctyp ctyp) (sgen_id fid) (sgen_id id) get_body
       else
         empty
     in
     separate_map hardline codegen_state_api_field fields ^^ hardline
  | _ -> empty

let codegen_state_api_vector id ctyp vctyp =
  let attrs, body = codegen_state_function_body_on_match (sgen_id id) (Printf.sprintf "vector_update_%s(rop, op, n, elem);" (sgen_ctyp ctyp)) in
  string (Printf.sprintf "%svoid state_vector_update_%s(sail_state* st, %s *rop, %s op, sail_int n, %s elem)%s"
          attrs (sgen_id id) (sgen_ctyp ctyp) (sgen_ctyp ctyp) (sgen_ctyp vctyp) body)
    ^^ hardline ^^
  let attrs, body = codegen_state_function_body_on_match (sgen_id id) (Printf.sprintf "return vector_access_%s(op, n);" (sgen_ctyp ctyp)) in
  string (Printf.sprintf "%s%s state_vector_access_%s(sail_state* st, %s op, sail_int n)%s"
    attrs (sgen_ctyp vctyp) (sgen_id id) (sgen_ctyp ctyp) body)
    ^^ hardline

let codegen_state_api_reg_dec id ctyp =
  begin match ctyp with
  | _ when is_api_ctyp ctyp ->
    let attrs, body = codegen_state_function_body_on_match (sgen_id id) (Printf.sprintf "return st->%s;" (sgen_id id)) in
    ksprintf string "%s%s state_get_%s(sail_state* st)%s" attrs (sgen_ctyp ctyp) (sgen_id id) body ^^ hardline ^^ 
    let attrs, body = codegen_state_function_body_on_match (sgen_id id) (Printf.sprintf "st->%s = n;" (sgen_id id)) in
    ksprintf string "%svoid state_set_%s(sail_state* st, %s n)%s" attrs (sgen_id id) (sgen_ctyp ctyp) body ^^ hardline ^^
    codegen_state_api_struct id ctyp
  | CT_vector (_, vctyp) when is_api_ctyp vctyp -> codegen_state_api_vector id ctyp vctyp 
  | CT_fvector (_, _, vctyp) when is_api_ctyp vctyp -> codegen_state_api_vector id ctyp vctyp 
  | _ -> empty
  end

let codegen_state_api ctx = function
| CDEF_reg_dec (id, ctyp, _) -> codegen_state_api_reg_dec id ctyp
| CDEF_let (_, [], _) -> empty
| CDEF_let (_, bindings, _) ->
    separate_map hardline (fun (id, ctyp) -> codegen_state_api_reg_dec id ctyp) 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 "};" ^^ hardline ^^ hardline
  ^^ concat_map (codegen_state_api ctx) cdefs

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 =
  match defs with
  | DEF_internal_mutrec fundefs :: defs ->
     IdSet.union (List.map id_of_fundef fundefs |> IdSet.of_list) (get_recursive_functions 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)
     else
       get_recursive_functions defs

  | _ :: defs -> get_recursive_functions 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_state.h\"" ^^ hardline
    ^^ 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_symbol = String.uppercase_ascii (Filename.basename output_name) in
  let header =
    ksprintf string "#ifndef SAILC_%s_H" header_symbol ^^ hardline 
    ^^ ksprintf string "#define SAILC_%s_H" header_symbol ^^ hardline
    ^^ stdlib_headers ^^ hardline
    ^^ sail_headers ^^ hardline
    ^^ concat_map add_extra_header O.opts.extra_headers ^^ hardline
    ^^ concat docs_header
    ^^ state
    ^^ twice hardline
    ^^ string "void sail_initialize_state(sail_state *state);"
    ^^ hardline
    ^^ string "void sail_finalize_state(sail_state *state);"
    ^^ twice hardline
    ^^ string "#endif"
    ^^ hardline
  in

  let regs = c_ast_registers cdefs in

  let letbind_initializers =
    List.map (fun n -> sprintf "  sail_create_letbind_%d(state);" n) (List.rev ctx.letbinds)
  in
  let letbind_finalizers =
    List.map (fun n -> 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