CStarToC11.ml

(* Copyright (c) INRIA and Microsoft Corporation. All rights reserved. *)
(* Licensed under the Apache 2.0 and MIT Licenses. *)

(** Converting from C* to C abstract syntax. *)

module C = C11

open C
open CStar
open KPrint
open Common

let is_primitive = Helpers.is_primitive

let zero = C.Constant (K.UInt8, "0")

let cmul x y =
  match x, y with
  | C.Constant (_, "1"), _ -> y
  | _, C.Constant (_, "1") -> x
  | _ -> C.Op2 (K.Mult, x, y)

let is_array = function Array _ -> true | _ -> false

let is_commutative : K.op -> bool = function
  | Add | Mult
  | BOr | BAnd | BXor -> true
  | _ -> false

let is_compoundable : K.op -> bool = function
  | Add | Sub | Mult | Div | Mod
  | BOr | BAnd | BXor | BShiftL | BShiftR -> true
  | _ -> false

(* returns true when expr is definitely pure *)
let rec is_pure : C11.expr -> bool = function
  | Assign _ | CompoundAssign _ | Call _ | Stmt _
  | Member _ | MemberP _ -> false (* Unsure what these are *)

  | Name _ | Literal _ | Constant _ | Bool _
  | Sizeof _ | CompoundLiteral _ | Type _
  | CxxInitializerList _ -> true

  | Op1 (_, e) -> is_pure e
  | Op2 (_, e1, e2) -> is_pure e1 && is_pure e2
  | Index (e1, e2) -> is_pure e1 && is_pure e2
  | Deref e -> is_pure e
  | Address e -> is_pure e
  | Cast (_, e) -> is_pure e
  | MemberAccess (e, _) -> is_pure e
  | MemberAccessPointer (e, _) -> is_pure e
  | InlineComment (_, e, _) -> is_pure e
  | Ternary (e1, e2, e3) -> is_pure e1 && is_pure e2 && is_pure e3

(* Tries to make compound assignments when possible.
   Assumptions:
   - The result is always used in statement context (discarded value), so
     PostIncr vs PreIncr does not matter.

   C standard §6.5.16.2:
     A compound assignment of the form E1 op = E2 is equivalent to the simple
     assignment expression E1 = E1 op (E2), except that the lvalue E1 is
     evaluated only once, and with respect to an indeterminately-sequenced
     function call, the operation of a compound assignment is a single
     evaluation *)
let mk_assign (lhs : C11.expr) (rhs : C11.expr) : C11.expr =
  match rhs with
  (* We don't really generate impure LHS of assignments,
     but it doesn't hurt to be defensive. *)
  | _ when not (is_pure lhs) -> Assign (lhs, rhs)

  | Op2 (Add, e2, Cast (_, Constant (_, "1")))
  | Op2 (Add, e2, Constant (_, "1")) when e2 = lhs ->
    Op1 (PostIncr, lhs)
  | Op2 (Add, Cast (_, Constant (_, "1")), e2)
  | Op2 (Add, Constant (_, "1"), e2) when e2 = lhs ->
    Op1 (PostIncr, lhs)
  | Op2 (Sub, e2, Cast (_, Constant (_, "1")))
  | Op2 (Sub, e2, Constant (_, "1")) when e2 = lhs ->
    Op1 (PostDecr, lhs)
  | Op2 (op, e2, e3) when is_compoundable op && e2 = lhs ->
    CompoundAssign (lhs, op, e3)
  | Op2 (op, e2, e3) when e3 = lhs && is_compoundable op && is_commutative op ->
    CompoundAssign (lhs, op, e2)
  | _ ->
    Assign (lhs, rhs)

let is_var = function Var _ -> true | _ -> false
let is_call = function
  | Call (Qualified (_, s), _) ->
      not (KString.starts_with s "op_Bang_Star__")
  | _ -> false

let fresh =
  let r = ref (-1) in
  fun () ->
    incr r;
    "_" ^ string_of_int !r

let escape_string s =
  let b = Buffer.create 256 in
  String.iter (fun c ->
    match c with
    | '\x27' -> Buffer.add_string b "\\'"
    | '\x22' -> Buffer.add_string b "\\\""
    | '\x3f' -> Buffer.add_string b "\\?"
    | '\x5c' -> Buffer.add_string b "\\\\"
    | '\x07' -> Buffer.add_string b "\\a"
    | '\x08' -> Buffer.add_string b "\\b"
    | '\x0c' -> Buffer.add_string b "\\f"
    | '\x0a' -> Buffer.add_string b "\\n"
    | '\x0d' -> Buffer.add_string b "\\r"
    | '\x09' -> Buffer.add_string b "\\t"
    | '\x0b' -> Buffer.add_string b "\\v"
    | '\x20'..'\x7e' -> Buffer.add_char b c
    | _ -> Printf.bprintf b "\\x%02x" (Char.code c)
  ) s;
  Buffer.contents b

let to_c_name = GlobalNames.to_c_name

let assert_var m =
  function
  | Var v ->
      v
  | Qualified v ->
      to_c_name m (v, Other)
  | e -> Warn.fatal_error
      "TODO: for (int i = 0, t tmp = e1; i < ...; ++i) tmp[i] = \n%s is not a var"
      (show_expr e)

module S = Set.Make(String)

let rec vars_of m = function
  | CStar.Var v ->
      S.singleton v
  | Qualified v
  | Macro v ->
      S.singleton (to_c_name m (v, Other))
  | Constant _
  | Bool _
  | StringLiteral _
  | Any
  | EAbort _
  | Type _
  | BufNull
  | Op _ ->
      S.empty
  | Cast (e, _)
  | Field (e, _)
  | AddrOf e
  | InlineComment (_, e, _) ->
      vars_of m e
  | BufRead (e1, e2)
  | BufSub (e1, e2)
  | Comma (e1, e2)
  | BufCreate (_, e1, e2) ->
      S.union (vars_of m e1) (vars_of m e2)
  | Call (e, es) ->
      List.fold_left S.union (vars_of m e) (List.map (vars_of m) es)
  | BufCreateL (_, es) ->
      KList.reduce S.union (List.map (vars_of m) es)
  | Struct (_, fieldexprs) ->
      KList.reduce S.union (List.map (fun (_, e) -> vars_of m e) fieldexprs)
  | Stmt stmts ->
      vars_of_block m stmts
  | Ternary (e1, e2, e3) ->
      S.union (vars_of m e1) (S.union (vars_of m e2) (vars_of m e3))
  | Sizeof _t ->
      S.empty

and vars_of_block m stmts =
  KList.reduce S.union (List.map (vars_of_stmt m) stmts)

and vars_of_stmt m = function
  | CStar.Abort _
  | Return _
  | Break
  | Continue
  | Comment _ ->
      S.empty
  | Ignore e
  | BufFree (_, e) ->
      vars_of m e
  | Block stmts ->
      vars_of_block m stmts
  | Decl ({ name; _ }, e) ->
      S.remove name (vars_of m e)
  | IfThenElse (_, e, b1, b2) ->
      S.union (vars_of m e) (S.union (vars_of_block m b1) (vars_of_block m b2))
  | While (e, b) ->
      S.union (vars_of m e) (vars_of_block m b)
  | For (i, e, s, b) ->
      begin match i with
      | `Decl ({ name; _ }, e') ->
          S.remove name (
            KList.reduce S.union [
              vars_of m e;
              vars_of m e';
              vars_of_stmt m s;
              vars_of_block m b
            ]
          )
      | `Skip ->
          KList.reduce S.union [
            vars_of m e;
            vars_of_stmt m s;
            vars_of_block m b
          ]
      | `Stmt s' ->
          KList.reduce S.union [
            vars_of m e;
            vars_of_stmt m s;
            vars_of_stmt m s';
            vars_of_block m b
          ]
      end
  | Assign (e, _, e') ->
      S.union (vars_of m e) (vars_of m e')
  | Switch (e, cs, b) ->
      KList.reduce S.union ([
        vars_of m e;
        match b with Some b -> vars_of_block m b | None -> S.empty
      ] @ List.map (fun (_, b) -> vars_of_block m b) cs)
  | BufWrite (e1, e2, e3) ->
      KList.reduce S.union [
        vars_of m e1;
        vars_of m e2;
        vars_of m e3;
      ]
  | BufFill (_, e2, e3, e4) ->
      KList.reduce S.union [
        vars_of m e2;
        vars_of m e3;
        vars_of m e4;
      ]
  | BufBlit (_, e2, e3, e4, e5, e6) ->
      KList.reduce S.union [
        vars_of m e2;
        vars_of m e3;
        vars_of m e4;
        vars_of m e5;
        vars_of m e6;
      ]

let c99_format w =
  let open K in
  "PRIx" ^ string_of_int (bytes_of_width w * 8)

let mk_debug name parameters =
  if Options.debug "c-calls" then
    let formats, args = List.split (List.map (fun (name, typ) ->
      match typ with
      | Int w ->
          Printf.sprintf "%s=0x%%08\"%s\"" name (c99_format w), C.Name name
      | Bool ->
          Printf.sprintf "%s=%%d" name, C.Name name
      (* | Pointer (Int w) -> *)
      (*     Some (Printf.sprintf "%s[0]=%%\"%s\"" name (c99_format w), C.Deref (C.Name name)) *)
      | _ ->
          Printf.sprintf "%s=%%s" name, C.Literal "unknown"
    ) parameters) in
    [ C.Expr (C.Call (C.Name "KRML_HOST_PRINTF", [
        C.Literal (String.concat " " (name :: formats @ [ "\\n" ]))
      ] @ args)) ]
  else
    []

let mk_pretty_type = function
  | "FStar_UInt128_uint128" when !Options.builtin_uint128 ->
      "uint128_t"
  | x ->
      x

let bytes_in = function
  (* SizeT does not have a statically known size *)
  | Int SizeT -> None
  | Int w -> Some (K.bytes_of_width w)
  | Qualified ([ "FStar"; "UInt128" ], "uint128") -> Some (128 / 8)
  | Qualified ([ "Lib"; "IntVector"; "Intrinsics" ], "vec128") -> Some (128 / 8)
  | Qualified ([ "Lib"; "IntVector"; "Intrinsics" ], "vec256") -> Some (256 / 8)
  | Qualified ([ "Lib"; "IntVector"; "Intrinsics" ], "vec32") -> Some (32 / 8)
  | _ -> None

(* https://www.open-std.org/jtc1/sc22/wg14/www/docs/n3088.pdf 6.7.10

  The goal of this function is to generate an initializer list that is i) compact and ii) sensible.

  For compactness, it appears that owing to §20 and §22 above, one can just omit remaining fields /
  indices when their initial value is zero (since they are initialized as if they had static storage
  duration).

  For sensibility, we don't want to be *too* smart and e.g. omit the last field of a struct if it
  statically known to be zero; we also want to emit { 0 } for subarrays, not {} which is C++/C23
  syntax for default (i.e. zero) initialization.
*)
let is_zero_expr = function
  | C11.Constant (_, "0") -> true
  | C11.Cast (_, Constant (_, "0")) -> true
  | _ -> false

let rec is_zero = function
  | InitExpr e -> is_zero_expr e
  | Designated (_, _i) -> false (* too smart: is_zero i *)
  | Initializer is -> List.for_all is_zero is

let rec trim_trailing_zeros l =
  match l with
  | Initializer [] -> Initializer []
  | InitExpr (CompoundLiteral (_, l)) -> Initializer (List.map trim_trailing_zeros (chop_zeros l))
  | InitExpr e -> InitExpr e
  | Designated (d, init) -> Designated (d, trim_trailing_zeros init)
  | Initializer l -> Initializer (List.map trim_trailing_zeros (chop_zeros l))

and chop_zeros is =
  let rec chop_zeros = function
    | hd :: tl when is_zero hd -> chop_zeros tl
    | [] -> [ InitExpr (C11.Constant (K.UInt32, "0")) ]
    | l -> List.rev l
  in
  chop_zeros (List.rev is)

let workaround_gcc_bug53119_fml t init =
  let rec array_nesting = function
    | Array (t, _) -> 1 + array_nesting t
    | Const t -> array_nesting t
    | _ -> 0
  in
  match init with
  | Initializer [ init ] when is_zero init && array_nesting t > 1 ->
      let rec nest l =
        if l = 0 then
          Initializer [ init ]
        else
          Initializer [ nest (l - 1) ]
      in
      nest (array_nesting t - 1)
  | _ ->
      init

(* Turns the ML declaration inside-out to match the C reading of a type.
 *   See: en.cppreference.com/w/c/language/declarations.
 * The continuation is key in the Function case. *)
let rec mk_spec_and_decl m name qs (t: typ) (k: C.declarator -> C.declarator):
  C.qualifier list * C.type_spec * C.declarator
=
  match t with
  | Const t ->
      (* Originally, this was added via a mechanism of attributes and made sense only in the pointer
         case. Now... mostly used by Eurydice to mark constants as global. *)
      mk_spec_and_decl m name [ C.Const ] t k
  | Pointer t ->
      mk_spec_and_decl m name [] t (fun d -> Pointer (qs, k d))
  | Array (t, size) ->
      (* F* guarantees that the initial size of arrays is always something
       * reasonable (i.e. <4GB). *)
      let size = match size with
        | Some (Constant k) -> Some (C.Constant k)
        | Some size -> Some (mk_expr m size)
        | None -> None
      in
      mk_spec_and_decl m name qs t (fun d -> Array ([], k d, size))
  | Function (cc, t, ts) ->
      (* Function types are pointers to function types, except in the top-level
       * declarator for a function, which gets special treatment via
       * mk_spec_and_declarator_f. *)
      mk_spec_and_decl m name [] t (fun d ->
        Function (cc, Pointer (qs, k d), List.mapi (fun i t ->
          mk_spec_and_decl m (KPrint.bsprintf "x%d" i) [] t (fun d -> d)) ts))
  | Int w ->
      qs, Int w, k (Ident name)
  | Void ->
      qs, Void, k (Ident name)
  | Qualified l ->
      qs, Named (mk_pretty_type (to_c_name m (l, Type))), k (Ident name)
  | Enum tags ->
      (* Important: the tags of an enum live in the value namespace, not the type namespace. *)
      let tags = List.map (fun (lid, v) -> to_c_name m (lid, Other), v) tags in
      qs, Enum (None, tags), k (Ident name)
  | Bool ->
      let bool = if !Options.microsoft then "BOOLEAN" else "bool" in
      qs, Named bool, k (Ident name)
  | Struct fields ->
      qs, Struct (None, mk_fields m fields), k (Ident name)
  | Union fields ->
      qs, Union (None, mk_union_fields m fields), k (Ident name)

and mk_fields m fields =
  Some (List.map (fun (name, typ) ->
    let name = match name with Some name -> name | None -> "" in
    let qs, spec, decl = mk_spec_and_declarator m name typ in
    qs, spec, None, None, { maybe_unused = false; target = None }, [ decl, None, None ]
  ) fields)

and mk_union_fields m fields =
  Some (List.map (fun (name, typ) ->
    let qs, spec, decl = mk_spec_and_decl m name [] typ (fun d -> d) in
    qs, spec, None, None, { maybe_unused = false; target = None }, [ decl, None, None ]
  ) fields)

(* Standard spec/declarator pair (e.g. int x). *)
and mk_spec_and_declarator m name t =
  mk_spec_and_decl m name [] t (fun d -> d)

(* A variant dedicated to typedef's, where we need to name structs. *)
and mk_spec_and_declarator_t m name t =
  match t with
  | Struct fields ->
      (* In C, there's a separate namespace for struct names; our type names are
       * unique, therefore, post-fixing them with "_s" also generates a set of
       * unique struct names. *)
      [], C.Struct (Some (name ^ "_s"), mk_fields m fields), Ident name
  | Union fields ->
      [], C.Union (Some (name ^ "_s"), mk_union_fields m fields), Ident name
  | _ ->
      mk_spec_and_declarator m name t

(* A variant dedicated to functions that avoids the conversion of function type
 * to pointer-to-function. *)
and mk_spec_and_declarator_f m cc name ret_t params =
  mk_spec_and_decl m name [] ret_t (fun d ->
    Function (cc, d, List.map (fun (n, t) -> mk_spec_and_declarator m n t) params))

(* Enforce the invariant that declarations are wrapped in compound statements
 * and cannot appear "alone". *)
and mk_compound_if (stmts: C.stmt list) (under_else: bool): C.stmt =
  match stmts with
  | [ Decl _ ] ->
      Compound stmts
  | [ If _ | IfElse _ as stmt ] when under_else ->
      (* Never wrap an if under else with braces, because it would defeat `else
        * if` on the same line. *)
      stmt
  | [ stmt ] when not !Options.curly_braces ->
      stmt
  | _ ->
      Compound stmts

and ensure_compound (stmts: C.stmt list): C.stmt =
  match stmts with
  | [ Compound _ as stmt ] ->
      stmt
  | _ ->
      Compound stmts

(* Ideally, most of the for-loops should've been desugared C89-style if needed
 * beforehand. *)
and mk_for_loop name qs t init test incr body =
  if !Options.c89_scope then
    Compound [
      Decl (qs, t, None, None, { maybe_unused = false; target = None }, [ Ident name, None, None ]);
      For (
        `Expr (Op2 (K.Assign, Name name, init)),
        test, incr, body)
    ]
  else
    For (
      `Decl (qs, t, None, None, { maybe_unused = false; target = None }, [ Ident name, None, Some (InitExpr init)]),
      test, incr, body)

(* Takes e_array of type (Buf t). e_size = size of the array, in number of
   elements *)
and mk_initializer ~null_check t e_array e_size e_value: C.stmt =
  (* KPrint.bprintf "element_size is: %s\n" (C11.show_expr e_size); *) 
  (* KPrint.bprintf "t is: %s\n" (C11.show_type_name t); *) 
  let if_not_null e: C.stmt =
    if null_check then
      if !Options.curly_braces then
        If (Op2 (K.Neq, e_array, Name "NULL"), Compound [ e ])
      else
        If (Op2 (K.Neq, e_array, Name "NULL"), e)
    else
      e
  in
  match e_size with
  | C.Constant (_, "1")
  | C.Cast (_, C.Constant (_, "1")) ->
      if_not_null @@
      Expr (Op2 (K.Assign, Index (e_array, Constant (K.UInt32, "0")), e_value))

  | _ ->
      match e_value with
      | C.Constant (_, s)
      | C.Cast (_, C.Constant (_, s)) when int_of_string s = 0 ->
          (* KPrint.bprintf "need memset 0\n"; *)
          if_not_null @@
          mk_memset t e_array e_size (C.Constant (K.UInt8, "0"))

      | C.Name "Lib_IntVector_Intrinsics_vec128_zero"
      | C.Name "Lib_IntVector_Intrinsics_vec256_zero"
      | C.Name "Lib_IntVector_Intrinsics_vec512_zero" ->
          (* Same as above. This is important to avoid generating avx2 instructions when merely
             allocating simd state. Under the hood, the C memset will use suitable instructions to
             go fast. *)
          (* KPrint.bprintf "need memset 1\n"; *)
          if_not_null @@
          mk_memset t e_array e_size (C.Constant (K.UInt8, "0"))

      | C.Constant (K.UInt8, _)
      | C.Cast (_, C.Constant (K.UInt8, _)) ->
          (* KPrint.bprintf "need memset 2\n"; *)
          if_not_null @@
          mk_memset t e_array e_size e_value

      | _ ->
          if_not_null @@
          mk_for_loop "_i" [] (Int K.UInt32) zero
            (Op2 (K.Lt, Name "_i", e_size))
            (Op1 (K.PreIncr, Name "_i"))
            (Expr (Op2 (K.Assign, Index (e_array, Name "_i"), e_value)))

and mk_memset t e_array e_size e_init =
  let e_size =
    (* Commenting out this optimization below, because:
     *   error: ‘memset’ used with length equal to number of elements without
     *   multiplication by element size [-Werror=memset-elt-size]
     * is it not known that sizeof uint8_t = 1 ? *)
    (* match e_init with
    | C.Constant (K.UInt8, _) ->
        e_size
    | _ -> *)
        Op2 (K.Mult, e_size, Sizeof (Type t))
  in
  Expr (Call (Name "memset", [ e_array; e_init; e_size]))

and mk_check_size m t n_elements: C.stmt list =
  (* [init] is the default value for the elements of the array, and [n_elements] is
   * hopefully a constant *)
  let default = [ C.Expr (C.Call (C.Name "KRML_CHECK_SIZE", [ mk_sizeof m t; n_elements ])) ] in
  match bytes_in t, n_elements with
  | _, C.Cast (_, C.Constant (_, "1"))
  | _, C.Constant (_, "1") ->
      (* C compilers also don't seem to let the user define a type that would be
         greater than size_t, so if the element size is 1, then we can get rid
         of the check as well. *)
      []
  | Some w, C.Cast (_, C.Constant (_, n_elements))
  | Some w, C.Constant (_, n_elements) ->
      (* Compute, if we can, the size statically *)
      let size_bytes = Z.(of_int w * of_string n_elements) in
      let ptr_size = Z.(one lsl 16) in
      (* The C data model guarantees 16 bits wide for size_t, at least. *)
      if Z.( lt size_bytes ptr_size )then
        []
      else
        default
  | _ ->
      (* Nothing much we can deduce statically, bail *)
      default

and mk_sizeof m t =
  C.Sizeof (C.Type (mk_type m t))

and mk_sizeof_mul m t s =
  match s with
    | C.Constant (_, "1")
    | C.Cast (_, C.Constant (_, "1")) ->
        mk_sizeof m t
    | _ ->
        C.Op2 (K.Mult, mk_sizeof m t, s)

and mk_alloc_cast m t e =
  if !Options.cast_allocations then
    C.Cast (mk_type m (Pointer t), e)
  else
    e

and mk_malloc m t s =
  match t with
  | Qualified lid when Helpers.is_aligned_type lid ->
      let sz = Option.get (mk_alignment m t) in
      mk_alloc_cast m t (C.Call (C.Name "KRML_ALIGNED_MALLOC", [ sz; mk_sizeof_mul m t s ]))
  | _ ->
      mk_alloc_cast m t (C.Call (C.Name "KRML_HOST_MALLOC", [ mk_sizeof_mul m t s ]))

and mk_calloc m t s =
  mk_alloc_cast m t (C.Call (C.Name "KRML_HOST_CALLOC", [ s; mk_sizeof m t ]))

and mk_free t e =
  match t with
  | Qualified lid when Helpers.is_aligned_type lid ->
      C.Call (C.Name "KRML_ALIGNED_FREE", [ e ])
  | _ ->
      C.Call (C.Name "KRML_HOST_FREE", [ e ])

and mk_ignore is_var e =
  if is_var then
    C.Call (C.Name "KRML_MAYBE_UNUSED_VAR", [ e ])
  else
    C.Call (C.Name "KRML_HOST_IGNORE", [ e ])

(* NOTE: this is only legal because we rule out the creation of zero-length
 * heap-allocated buffers; if we were to allow that, then this begs the question
 * of whether memset(malloc(0), 0, 0) is UB or not! The result of malloc(0) is
 * implementation-defined, not undefined behavior. *)
and mk_eternal_bufcreate m buf (t: CStar.typ) init size =
  let size = mk_expr m size in
  let e, extra_stmt = match init with
    | Constant (_, "0") ->
        (* NOTE: we MUST NOT catch vector types here because there is no aligned_calloc! *)
        mk_calloc m t size, []
    | Any | Cast (Any, _) ->
        mk_malloc m t size, []
    | _ ->
        mk_malloc m t size,
        [ mk_initializer ~null_check:true (mk_type m t) (mk_expr m buf) size (mk_expr m init) ]
  in
  mk_check_size m t size, e, extra_stmt

and assert_pointer t =
  match t with
  | Array (t, _)
  | Pointer t ->
      t
  | _ ->
      Warn.fatal_error "let-bound bufcreate has type %s instead of Pointer" (show_typ t)

and ensure_array_l t inits =
  assert (List.for_all (function BufCreate _ -> false | _ -> true) inits);
  match t with
  | Pointer t ->
      Array (t, Some (Constant (K.uint32_of_int (List.length inits))))
  | _ ->
      t

(* Returns
   - C* array type
   - C* initializer
   - C* num elems
   - C11 (translated) size of elem
 *)
and ensure_array m (t : CStar.typ) (expr : CStar.expr) : CStar.typ * CStar.expr * CStar.expr * C.expr =
  match t, expr with
  | Pointer t, BufCreate ((Stack | Eternal), init, len)  ->
      let _, init, len', size' = ensure_array m t init in
      Array (t, Some len), init, len, cmul (mk_expr m len') size'
  | Array (t, l), BufCreate ((Stack | Eternal), init, len) ->
      assert (l = Some len);
      let _, init, len', size' = ensure_array m t init in
      Array (t, Some len), init, len, cmul (mk_expr m len') size'
  | _ ->
      t, expr, CStar.Constant (K.UInt8, "1"), C.Sizeof (C.Type (mk_type m t))

and decay_array t =
  match t with
  | Array (t, _) ->
      Pointer t
  | t ->
      Warn.fatal_error "impossible: %s" (show_typ t)

and assert_array t =
  match t with
  | Array (t, _) ->
      t
  | t ->
      Warn.fatal_error "impossible: not an array %s" (show_typ t)

and is_aligned_type = function
  | Qualified lid ->
      Helpers.is_aligned_type lid
  | _ ->
      false

and mk_alignment m t: C11.expr option =
  if is_aligned_type t then
    match t with
    | Qualified (["Lib"; "IntVector"; "Intrinsics"], "vec128") ->
        Some (Constant (CInt, "16"))
    | Qualified (["Lib"; "IntVector"; "Intrinsics"], "vec256") ->
        Some (Constant (CInt, "32"))
    | Qualified (["Lib"; "IntVector"; "Intrinsics"], "vec512") ->
        Some (Constant (CInt, "64"))
    | _ ->
        Some (Sizeof (Type (mk_type m t)))
  else
    None

and to_initializer m = function
  | BufCreateL ((Stack | Eternal), inits) ->
      Initializer (List.map (to_initializer m) inits)
  | BufCreate ((Stack | Eternal), init, size) ->
      begin match size with
      | Constant (_, c) ->
          Initializer (List.init (int_of_string c) (fun _ -> to_initializer m init))
      | _ -> failwith (CStar.show_expr size ^ " is not a constant")
      end
  | e ->
      InitExpr (mk_expr m e)

and mk_stmt m (stmt: stmt): C.stmt list =
  match stmt with
  | Comment s ->
      [ Comment s ]

  | Return e ->
      let e = Option.map (fun e ->
        let e = mk_expr m e in
        if Options.debug "c-calls" then
          C.Call (Name "KRML_DEBUG_RETURN", [ e ])
        else
          e
      ) e in
      [ Return e ]

  | Block stmts ->
      [ Compound (mk_stmts m stmts) ]

  | Break ->
      [ Break ]

  | Continue ->
      [ Continue ]

  (* Ignore injects `expr`s into `stmt`s by ignoring their return value. No need
     to double-ignore, since C does it for us automatically, and C compilers
     treat this as 100% normal UNLESS the programmer uses extensions like
     `__attribute__((nodiscard))`. *)
  | Ignore (Call (Qualified ([ "LowStar"; "Ignore" ], "ignore"), [ arg; _; _ ])) when is_call arg ->
      [ Expr (mk_expr m arg) ]

  | Ignore e ->
      [ Expr (mk_expr m e) ]

  | Decl (binder, BufCreate ((Eternal | Heap), init, size)) ->
      let t = assert_pointer binder.typ in
      let stmt_check, expr_alloc, stmt_extra =
        mk_eternal_bufcreate m (Var binder.name) t init size
      in
      let qs, spec, decl = mk_spec_and_declarator m binder.name binder.typ in
      let decl: C.stmt list = [ Decl (qs, spec, None, None, { maybe_unused = false; target = None }, [ decl, None, Some (InitExpr expr_alloc)]) ] in
      stmt_check @ decl @ stmt_extra

  | Decl (binder, (BufCreate (Stack, _, _) as rhs)) ->
      (* In the case where this is a buffer creation in the C* meaning, then we
       * declare a fixed-length array; this is an "upcast" from pointer type to
       * array type, in the C sense. *)
      let t, init, n_elements, e_size = ensure_array m binder.typ rhs in

      let rebind_n_elements, cstar_n_elements, n_elements =
        (* If the length expression is complex, then assign it to a local
           variable and use that. Otherwise we would duplicate it, potentially
           affecting the meaning. *)
        let rec is_pure e =
          match e with
          | Constant _ | Var _ | Macro _ | Qualified _
          | BufRead _ | BufSub _ | BufNull
          | Op _ | Bool _  | Type _ | StringLiteral _
          | Any | Sizeof _ ->
            true

          | Ternary (c, t, e) ->
            is_pure c && is_pure t && is_pure e

          (* Calls in general we take as impure, but operators
             are pure. *)
          | Call (Op _, args) -> List.for_all is_pure args

          | Call _ | BufCreate _ | BufCreateL _ | Stmt _ | EAbort _ ->
            false

          (* just descend *)
          | Cast (e, _)
          | InlineComment (_, e, _)
          | Field (e, _)
          | AddrOf e ->
            is_pure e
          | Struct (_, fs) ->
            List.for_all (fun (_, e) -> is_pure e) fs
          | Comma (e1, e2) ->
            is_pure e1 && is_pure e2
        in
        if is_pure n_elements then
          [], n_elements, mk_expr m n_elements
        else
          let name_init = "_arraylen" ^ fresh () in
          let no_extra = { maybe_unused = false; target = None } in
          let stmt_init : C.stmt = C.Decl ([], Int SizeT, None, None, no_extra, [(Ident name_init, None, Some (InitExpr (mk_expr m n_elements)))]) in
          [stmt_init], CStar.Var name_init, C.Name name_init
      in
      (* Having rebound n_elements, make sure that `t` uses this expression
         for its size, instead of the original one. Otherwise the declaration
         for the array will contain it. *)
      let t =
        match t with
        | Array (et, Some _len) -> Array (et, Some cstar_n_elements)
        | t -> t
      in

      (* KPrint.bprintf "n_elements is: %s\n" (C11.show_expr n_elements); *)
      (* KPrint.bprintf "e_size is: %s\n" (C11.show_expr e_size); *)
      let alignment = mk_alignment m (assert_array t) in
      let is_constant = match n_elements with Constant _ -> true | _ -> false in
      let use_alloca = not is_constant && !Options.alloca_if_vla in
      let (maybe_init, needs_init): C.init option * _ = match init, n_elements with
        | _, Constant (_, "0") (* zero-sized array... legal for malloc *)
        | Cast (Any, _), _
        | Any, _ ->
            (* No initial value needed in the declarator; no further
             * initialization needed either. *)
            None, false

        | (Constant (_, "0") |
          Qualified (["Lib"; "IntVector"; "Intrinsics"],
            ("vec128_zero" | "vec256_zero" | "vec512_zero"))),
          Constant _ when not use_alloca ->
            (* The only case the we can initialize statically is a known, static
             * size _and_ a zero initializer. If we're about to alloca, don't
             * use a zero-initializer. *)
            Some (Initializer [ InitExpr (C.Constant (K.UInt32, "0")) ]), false

        | _ ->
            None, true
      in
      let t, maybe_init =
        (* If we're doing an alloca, override the initial value (it's now the
         * call to alloca) and decay the array to a pointer type. *)
        if use_alloca then
          if alignment <> None then
            Warn.fatal_error "In the following statement, the variable-length \
              array on the stack (VLA) must be aligned, but -falloca mandates the \
              use of alloca, which krml cannot yet align\n%s\n"
              (show_stmt stmt)
          else
            let bytes = mk_alloc_cast m (assert_pointer t) (C.Call (C.Name "alloca", [ cmul n_elements e_size ])) in
            assert (maybe_init = None);
            decay_array t, Some (InitExpr bytes)
        else
          t, maybe_init
      in
      let init = mk_expr m init in
      let qs, spec, decl = mk_spec_and_declarator m binder.name t in
      let extra_stmt: C.stmt list =
        if needs_init then
          [ mk_initializer ~null_check:false (mk_type m (assert_pointer t)) (Name binder.name) n_elements init ]
        else
          []
      in
      let decl: C.stmt list = [ Decl (qs, spec, None, None, { maybe_unused = false; target = None }, [ decl, alignment, maybe_init ]) ] in
      rebind_n_elements @
      mk_check_size m (assert_pointer binder.typ) n_elements @
      decl @
      extra_stmt

  | Decl (_, BufCreateL ((Eternal | Heap), _)) as s ->
      failwith ("TODO: the array below is either in the eternal or heap region, \
        uses createL, but we don't have (yet) codegen for this:\n" ^
        CStar.show_stmt s)

  | Decl (binder, (BufCreateL (Stack, inits) as init_expr)) ->
      (* Per the C standard, static initializers guarantee for missing fields
       * that they're initialized as if they had static storage duration, i.e.
       * with zero. *)
      let t = ensure_array_l binder.typ inits in
      let alignment = mk_alignment m (assert_array t) in
      let qs, spec, decl = mk_spec_and_declarator m binder.name t in
      let init_expr = trim_trailing_zeros (to_initializer m init_expr) in
      let init_expr = workaround_gcc_bug53119_fml t init_expr in
      [ Decl (qs, spec, None, None, { maybe_unused = false; target = None }, [ decl, alignment, Some init_expr])]

  | Decl (binder, e) ->
      let qs, spec, decl = mk_spec_and_declarator m binder.name binder.typ in
      let init: init option = match e with Any -> None | _ -> Some (trim_trailing_zeros (struct_as_initializer m e)) in
      [ Decl (qs, spec, None, None, { maybe_unused = false; target = None }, [ decl, None, init ]) ]

  | IfThenElse (false, e, b1, b2) ->
      if List.length b2 > 0 then
        [ IfElse (mk_expr m e, mk_compound_if (mk_stmts m b1) false, mk_compound_if (mk_stmts m b2) true) ]
      else
        [ If (mk_expr m e, mk_compound_if (mk_stmts m b1) false) ]

  | IfThenElse (true, e, b1, b2) ->
      let rec find_elif acc = function
        | [ IfThenElse (true, e, b1, b2) ] ->
            let acc = (mk_expr m e, mk_stmts m b1) :: acc in
            find_elif acc b2
        | b ->
            List.rev acc, mk_stmts m b
      in
      let elif_blocks, else_block = find_elif [] b2 in
      [ IfDef (mk_expr m e, mk_stmts m b1, elif_blocks, else_block) ]

  | Assign (BufRead _, _, (Any | Cast (Any, _))) ->
      []

  | Assign (e1, t, BufCreate (Eternal, init, size)) ->
      let v = assert_var m e1 in
      (* Evil bug:
       *   x <- bufcreate 1 e[x]
       * might become:
       *   x <- bufcreate 1 any
       *   x[0] <- e[x]    <--- does NOT evaluate to the previous value of x
       * Note: from Simplify.ml we know that BufCreate appears only under a
       * [Decl] node or an [Assign] node. Name collisions are not possible with
       * the Decl case since [AstToCStar] would've avoided the name conflict,
       * and F* does not have recursive value definitions.
       *)
      let vs = vars_of m init in
      if S.mem v vs then
        let t_elt = assert_pointer t in
        let name_init = "_init" ^ fresh () in
        let size = mk_expr m size in
        let stmt_init = mk_stmt m (Decl ({ name = name_init; typ = t_elt }, init)) in
        let stmt_assign = [ Expr (Assign (mk_expr m e1, mk_malloc m t_elt size)) ] in
        (* GC'd allocation, not null-checking this -- this is LEGACY *)
        let stmt_fill = mk_initializer ~null_check:false (mk_type m t_elt) (mk_expr m e1) size (mk_expr m (Var name_init)) in
        stmt_init @
        stmt_assign @
        [ stmt_fill ]
      else
        let stmt_check, expr_alloc, stmt_extra = mk_eternal_bufcreate m e1 (assert_pointer t) init size in
        stmt_check @
        [ Expr (Assign (mk_expr m e1, expr_alloc)) ] @
        stmt_extra

  | Assign (_, _, BufCreateL (Eternal, _)) ->
      failwith "TODO"

  | Assign (e1, _, e2) ->
      [ Expr (mk_assign (mk_expr m e1) (mk_expr m e2)) ]

  | BufWrite (_, _, (Any | Cast (Any, _))) ->
      []

  | BufWrite (e1, e2, e3) ->
      [ Expr (mk_assign (mk_index m e1 e2) (mk_expr m e3)) ]

  | BufBlit (t, e1, e2, e3, e4, e5) ->
      let dest = match e4 with
        | Constant (_, "0") -> mk_expr m e3
        | _ -> Op2 (K.Add, mk_expr m e3, mk_expr m e4)
      in
      let source = match e2 with
        | Constant (_, "0") -> mk_expr m e1
        | _ -> Op2 (K.Add, mk_expr m e1, mk_expr m e2)
      in
      [ Expr (Call (Name "memcpy", [
        dest;
        source;
        Op2 (K.Mult, mk_expr m e5, mk_sizeof m t)])) ]

  | BufFill (t, buf, v, size) ->
      (* Again, assuming that these are non-effectful. *)
      [ mk_initializer ~null_check:false (mk_type m t) (mk_expr m buf) (mk_expr m size) (mk_expr m v) ]

  | BufFree (t, e) ->
      [ Expr (mk_free t (mk_expr m e)) ]

  | While (e1, e2) ->
      [ While (mk_expr m e1, mk_compound_if (mk_stmts m e2) false) ]

  | Switch (e, branches, default) ->
      [ Switch (
          mk_expr m e,
          List.map (fun (ident, block) ->
            (match ident with
            | `Ident ident -> Name (to_c_name m (ident, Other))
            | `Int k -> Constant k),
            let block = mk_stmts m block in
            if List.length block > 0 then
              match KList.last block with
              | Return _ -> Compound block
              | _ -> Compound (block @ [ Break ])
            else
              Compound [ Break ]
          ) branches,
          match default with
          | Some block ->
              Compound (mk_stmts m block)
          | _ ->
              let p = if !Options.c89_std then "KRML_HOST_PRINTF" else "KRML_HOST_EPRINTF" in
              Compound [
                Expr (Call (Name p, [
                  Literal "KaRaMeL incomplete match at %s:%d\\n"; Name "__FILE__"; Name "__LINE__"  ]));
                Expr (Call (Name "KRML_HOST_EXIT", [ Constant (K.UInt8, "253") ]))
              ]
      )]

  | Abort s ->
      let p = if !Options.c89_std then "KRML_HOST_PRINTF" else "KRML_HOST_EPRINTF" in
      [ Expr (Call (Name p, [
          Literal "KaRaMeL abort at %s:%d\\n%s\\n"; Name "__FILE__"; Name "__LINE__"; Literal (escape_string s) ]));
        Expr (Call (Name "KRML_HOST_EXIT", [ Constant (K.UInt8, "255") ])); ]

  | For (`Decl (binder, e1), e2, e3, b) ->
      let qs, spec, decl = mk_spec_and_declarator m binder.name binder.typ in
      let name = match decl with Ident name -> name | _ -> failwith "not an ident" in
      let init = match struct_as_initializer m e1 with InitExpr init -> init | _ -> failwith "not an initexpr" in
      let e2 = mk_expr m e2 in
      let e3 = match mk_stmt m e3 with [ Expr e3 ] -> e3 | _ -> assert false in
      let b = mk_compound_if (mk_stmts m b) false in
      [ mk_for_loop name qs spec init e2 e3 b ]

  | For (e1, e2, e3, b) ->
      let e1 = match e1 with
        | `Skip -> `Skip
        | `Stmt e1 -> `Expr (match mk_stmt m e1 with [ Expr e1 ] -> e1 | _ -> assert false)
        | _ -> assert false
      in
      let e2 = mk_expr m e2 in
      let e3 = match mk_stmt m e3 with [ Expr e3 ] -> e3 | _ -> assert false in
      let b = mk_compound_if (mk_stmts m b) false in
      [ For (e1, e2, e3, b) ]


and mk_stmts m stmts: C.stmt list =
  let stmts = List.concat_map (mk_stmt m) stmts in
  let rec fixup_c89 in_decls (stmts: C.stmt list) =
    match stmts with
    | C.Decl _ as stmt :: stmts ->
        if in_decls then
          stmt :: fixup_c89 true stmts
        else
          [ C.Compound (stmt :: fixup_c89 true stmts) ]
    | stmt :: stmts ->
        stmt :: fixup_c89 false stmts
    | [] ->
        []
  in
  if !Options.c89_scope then
    fixup_c89 true stmts
  else
    stmts



and mk_index m (e1: expr) (e2: expr): C.expr =
  match e2 with
  | Qualified (["Pulse"; "Lib"; "Pervasives"], "_zero_for_deref")
  | Qualified (["C"], "_zero_for_deref") ->
      mk_deref m e1
  | _ ->
    begin match mk_expr m e2 with
    | Cast (_, (Constant _ as c)) ->
        Index (mk_expr m e1, c)
    | e2' ->
        Index (mk_expr m e1, e2')
    end

and mk_deref m (e: expr) : C.expr =
  match mk_expr m e with
  | Address e' ->
      (* *&expr is equivalent to expr *)
      e'
  | e' ->
      Deref e'

(* Some functions get a special treatment and are pretty-printed in a specific
 * way at the very last minute. KaRaMeL is never supposed to generate unused
 * declarations, so these primitives must not be output in the resulting C
 * files. *)

and mk_expr m (e: expr): C.expr =
  match e with
  | InlineComment (s, e, s') ->
      InlineComment (s, mk_expr m e, s')

  | Call (Op o, [ e ]) ->
      Op1 (o, mk_expr m e)

  | Call (Op o, [ e1; e2 ]) ->
      Op2 (o, mk_expr m e1, mk_expr m e2)

  | Comma (e1, e2) ->
      Op2 (K.Comma, mk_expr m e1, mk_expr m e2)

  | Call (Qualified ([ "LowStar"; "Ignore" ], "ignore"), [ arg; _; _ ]) ->
      mk_ignore (is_var arg) (mk_expr m arg)

  | Call (Qualified ([ "LowStar"; "Ignore" ], "ignore"), _) ->
      (* Only one argument because of unit-to-void elimination -- should not happen. *)
      failwith "`ignore ()` should have been removed earlier on"

  | Call (Qualified ([ "C"; "Nullity" ], s), [ e1 ]) when KString.starts_with s "op_Bang_Star__" ->
      mk_deref m e1

  | Call (Qualified ([ "LowStar"; "BufferOps" ], s), e1 :: _) when KString.starts_with s "op_Bang_Star__" ->
      mk_deref m e1

  | Call (Qualified ([ "LowStar"; "BufferOps" ], s), e1 :: e2 :: _ ) when KString.starts_with s "op_Star_Equals__" ->
      Op2 (K.Assign, mk_deref m e1, mk_expr m e2)

  | Call (Qualified ([ "C"; "String"], "of_literal"), [ StringLiteral _ as s ]) ->
      mk_expr m s

  | Call (Qualified ([ "C"; "Compat"; "String" ], "of_literal"), [ StringLiteral _ as s ]) ->
      mk_expr m s

  | Call (Qualified ([ "C"; "String" ], "get"), [ e1; e2 ])
  | Call (Qualified ([ "C"; "Compat"; "String" ], "get"), [ e1; e2 ])
  | BufRead (e1, e2) ->
      mk_index m e1 e2

  | BufNull ->
      Name "NULL"

  | Call (Qualified ( [ "Steel"; "ST"; "HigherArray" ], "intro_fits_u32"), _ ) ->
      Call (Name "static_assert", [Op2 (K.Lte, Name "UINT32_MAX", Name "SIZE_MAX")])
  | Call (Qualified ( [ "Steel"; "ST"; "HigherArray" ], "intro_fits_u64"), _ ) ->
      Call (Name "static_assert", [Op2 (K.Lte, Name "UINT64_MAX", Name "SIZE_MAX")])
  | Call (Qualified ( [ "Steel"; "ST"; "HigherArray" ], "intro_fits_ptrdiff32"), _ ) ->
      Call (Name "static_assert", [Op2 (K.Lte, Name "INT32_MAX", Name "PTRDIFF_MAX")])
  | Call (Qualified ( [ "Steel"; "ST"; "HigherArray" ], "intro_fits_ptrdiff64"), _ ) ->
      Call (Name "static_assert", [Op2 (K.Lte, Name "INT64_MAX", Name "PTRDIFF_MAX")])

  | Call (Qualified ( [ "FStar"; "UInt128" ], "add"), [ e1; e2 ]) when !Options.builtin_uint128 ->
      Op2 (K.Add, mk_expr m e1, mk_expr m e2)

  | Call (Qualified ( [ "FStar"; "UInt128" ], "mul"), [ e1; e2 ]) when !Options.builtin_uint128 ->
      Op2 (K.Mult, mk_expr m e1, mk_expr m e2)

  | Call (Qualified ( [ "FStar"; "UInt128" ], "add_mod"), [ e1; e2 ]) when !Options.builtin_uint128 ->
      Op2 (K.Add, mk_expr m e1, mk_expr m e2)

  | Call (Qualified ( [ "FStar"; "UInt128" ], "sub"), [ e1; e2 ]) when !Options.builtin_uint128 ->
      Op2 (K.Sub, mk_expr m e1, mk_expr m e2)

  | Call (Qualified ( [ "FStar"; "UInt128" ], "sub_mod"), [ e1; e2 ]) when !Options.builtin_uint128 ->
      Op2 (K.Sub, mk_expr m e1, mk_expr m e2)

  | Call (Qualified ( [ "FStar"; "UInt128" ], "logand"), [ e1; e2 ]) when !Options.builtin_uint128 ->
      Op2 (K.BAnd, mk_expr m e1, mk_expr m e2)

  | Call (Qualified ( [ "FStar"; "UInt128" ], "logor"), [ e1; e2 ]) when !Options.builtin_uint128 ->
      Op2 (K.BOr, mk_expr m e1, mk_expr m e2)

  | Call (Qualified ( [ "FStar"; "UInt128" ], "logxor"), [ e1; e2 ]) when !Options.builtin_uint128 ->
      Op2 (K.BXor, mk_expr m e1, mk_expr m e2)

  | Call (Qualified ( [ "FStar"; "UInt128" ], "lognot"), [ e1 ]) when !Options.builtin_uint128 ->
      Op1 (K.BNot, mk_expr m e1)

  | Call (Qualified ( [ "FStar"; "UInt128" ], "shift_left"), [ e1; e2 ]) when !Options.builtin_uint128 ->
      Op2 (K.BShiftL, mk_expr m e1, mk_expr m e2)

  | Call (Qualified ( [ "FStar"; "UInt128" ], "shift_right"), [ e1; e2 ]) when !Options.builtin_uint128 ->
      Op2 (K.BShiftR, mk_expr m e1, mk_expr m e2)

  | Call (Qualified ( [ "FStar"; "UInt128" ], "uint64_to_uint128"), [ e1 ]) when !Options.builtin_uint128 ->
      Cast (mk_type m (Qualified ([], "uint128_t")), mk_expr m e1)

  | Call (Qualified ( [ "FStar"; "UInt128" ], "uint128_to_uint64"), [ e1 ]) when !Options.builtin_uint128 ->
      Cast (mk_type m (Qualified ([], "uint64_t")), mk_expr m e1)

  | Call (Qualified ( [ "FStar"; "UInt128" ], "mul_wide"), [ e1; e2 ]) when !Options.builtin_uint128 ->
      Op2 (K.Mult, Cast (mk_type m (Qualified ([], "uint128_t")), mk_expr m e1), mk_expr m e2)

  | Call (e, es) ->
      Call (mk_expr m e, List.map (mk_expr m) es)

  | Var ident ->
      Name ident

  | Qualified ident ->
      Name (to_c_name m (ident, Other))
  | Macro ident ->
      Name (to_c_name m (ident, Macro))

  | Constant (w, c) ->
      (* See discussion in AstToCStar.ml, around mk_arith. *)
      if not (Constant.is_float w) && K.is_unsigned w && w <> SizeT then
        Constant (w, c)
      else if not (Constant.is_float w) && K.is_signed w && w <> PtrdiffT then
        (* No point in casting a constant to a signed integer type. Either it
           appears directly under an assignment, in argument position, etc. and
           will be cast directly to the correct type, or *)
        Constant (w, c)
      else
        (* Floats: no known suffix. Cast.
           size_t, ptrdiff_t: still no suffix. Cast. *)
        Cast (([], Int w, Ident ""), Constant (w, c))

  | BufCreate _ | BufCreateL _ ->
      failwith "[mk_expr m]: Buffer.create and Buffer.createl may only appear as let ... = Buffer.create"

  | BufSub (e1, Constant (_, "0")) ->
      mk_expr m e1

  | BufSub (e1, e2) ->
      Op2 (K.Add, mk_expr m e1, mk_expr m e2)

  | Cast (e, t') ->
      (* JP: what is this? TODO review. *)
      begin match e with
      | Cast (_, t) as e when t = t' || t = Int Constant.UInt8 && t' = Pointer Void ->
          mk_expr m e
      | e ->
          Cast (mk_type m t', mk_expr m e)
      end

  | Any ->
      Cast (([], Void, Pointer ([], Ident "")), zero)

  | Op _ ->
      failwith "[mk_expr m]: op should've been caught"

  | Bool b ->
      Bool b

  | Struct (typ, fields) ->
      if typ = None then
        failwith ("Expected a type annotation for: \n" ^ show_expr e);
      let typ = Option.get typ in
      mk_compound_literal m typ fields

  | Field (BufRead (e, Constant (_, "0")), field) ->
      MemberAccessPointer (mk_expr m e, field)

  | Field (e, field) ->
      MemberAccess (mk_expr m e, field)

  | StringLiteral s ->
      Literal (escape_string s)

  | AddrOf e ->
      Address (mk_expr m e)

  | EAbort (t, s) ->
      Call (Name "KRML_EABORT", [ Type (mk_type m t); Literal (escape_string s) ])

  | Stmt s ->
      Stmt (List.concat_map (mk_stmt m) s)

  | Type t ->
      Type (mk_type m t)

  | Ternary (c, t, e) ->
      Ternary (mk_expr m c, mk_expr m t, mk_expr m e)

  | Sizeof t ->
      Sizeof (Type (mk_type m t))

and mk_compound_literal m name fields =
  let name = to_c_name m (name, Type) in
  match fields with
  | [ Some "tag", e1; Some "val", Struct (_, [ Some case, e2 ]) ] when !Options.cxx17_compat ->
      (* Hack that generates foo_s(tag, &foo_s::U::case_bar, value ...) *)
      let name = name ^ "_s" in
      Call (Name name, [
        mk_expr m e1;
        Address (Name (name ^ "::U::" ^ case));
        CxxInitializerList (struct_as_initializer m e2)
      ])
  | _ ->
      (* TODO really properly specify C's type_name! *)
      CompoundLiteral (([], Named name, Ident ""), List.map trim_trailing_zeros (fields_as_initializer_list m fields))

and struct_as_initializer m = function
  | Struct (_, fields) ->
      Initializer (fields_as_initializer_list m fields)
  | e ->
      to_initializer m e

and fields_as_initializer_list m fields =
  List.map (function
    | Some field, e -> Designated (Dot field, struct_as_initializer m e)
    | None, e -> struct_as_initializer m e
  ) fields

and mk_type m t =
  (* hack alert *)
  mk_spec_and_declarator m "" t

let mk_comments =
  List.filter_map (function
    | Comment c when c <> "" ->
        Some c
    | _ ->
        None
  )

let wrap_verbatim lid flags d =
  (if !Options.rst_snippets then
    [ Text (KPrint.bsprintf "/* SNIPPET_START: %s */" lid) ]
  else
    []) @
  List.filter_map (function
    | Prologue s -> Some (Text s)
    | _ -> None
  ) flags @
  List.filter_map (function
    | Deprecated s -> Some (Text (KPrint.bsprintf "KRML_DEPRECATED(\"%s\")" s))
    | _ -> None
  ) flags @
  [ d ] @ List.filter_map (function
    | Epilogue s -> Some (Text s)
    | _ -> None
  ) flags @
  if !Options.rst_snippets then
    [ Text (KPrint.bsprintf "/* SNIPPET_END: %s */" lid) ]
  else
    [] @
  []

let enum_as_macros cases =
  (* Since enums do not support arithmetic operations, we have no issues with
    integer promotion and need not concern ourselves with suffixes or e.g. a
    constant being promoted to a large signed type unintentionally. *)
  let lines: string list = List.mapi (fun i (c, v) ->
    match v with
    | None -> KPrint.bsprintf "#define %s %d" c i
    | Some v ->
        KPrint.bsprintf "#define %s %s" c (Z.to_string v)
  ) cases in
  String.concat "\n" lines

let strengthen_array m t expr =
  match expr with
  | BufCreateL (_, es) ->
      ensure_array_l t es
  | BufCreate _ ->
      let t, _, _, _ = ensure_array m t expr in
      t
  | _ ->
      t

(** Function definition or global definition. *)
let mk_function_or_global_body m (d: decl): C.declaration_or_function list =
  match d with
  | External _
  | TypeForward _
  | Type _ ->
      []

  | Function (cc, flags, return_type, name, parameters, body) ->
      if is_primitive name then
        []
      else
        let name = to_c_name m (name, Other) in
        begin try
          let static = if List.exists ((=) Private) flags then Some Static else None in
          let inline =
            if List.mem NoInline flags then
              Some C11.NoInline
            else if List.mem Inline flags then
              Some C11.Inline
            else if List.mem MustInline flags then
              Some C11.MustInline
            else
              None
          in
          let parameters = List.map (fun { name; typ } -> name, typ) parameters in
          let qs, spec, decl = mk_spec_and_declarator_f m cc name return_type parameters in
          let body = ensure_compound (mk_debug name parameters @ mk_stmts m body) in
          let extra = { maybe_unused = List.mem MaybeUnused flags; target = List.find_map (function | Target s -> Some s | _ -> None) flags } in
          wrap_verbatim name flags (Function (mk_comments flags, (qs, spec, inline, static, extra, [ decl, None, None ]), body))
        with e ->
          beprintf "Fatal exception raised in %s\n" name;
          raise e
        end

  | Global (name, macro, flags, t, expr) ->
      if is_primitive name || macro then
        []
      else
        let name = to_c_name m (name, Other) in
        let t = strengthen_array m t expr in
        let alignment = if is_array t then mk_alignment m (assert_array t) else None in
        let t = if List.mem (Common.Const "") flags then CStar.Const t else t in
        let qs, spec, decl = mk_spec_and_declarator m name t in
        let static = if List.exists ((=) Private) flags then Some Static else None in
        let extra = { maybe_unused = List.mem MaybeUnused flags; target = List.find_map (function | Target s -> Some s | _ -> None) flags } in
        match expr with
        | Any ->
            wrap_verbatim name flags (Decl (mk_comments flags, (qs, spec, None, static, extra, [ decl, alignment, None ])))
        | (BufCreateL _) as init_expr ->
            let init_expr = trim_trailing_zeros (to_initializer m init_expr) in
            let init_expr = workaround_gcc_bug53119_fml t init_expr in
            wrap_verbatim name flags (Decl (mk_comments flags, (qs, spec, None, static, extra, [
              decl, alignment, Some init_expr ])))
        (* Global static arrays of arithmetic type are initialized implicitly to 0 *)
        | BufCreate (_, Constant (_, "0"), _)
        | BufCreate (_, CStar.Bool false, _)
        | BufCreate (_, CStar.Any, _) ->
            wrap_verbatim name flags (Decl (mk_comments flags, (qs, spec, None, static, extra, [
              decl, alignment, None ])))
        | _ ->
            let expr = struct_as_initializer m expr in
            wrap_verbatim name flags (Decl (mk_comments flags, (qs, spec, None, static, extra, [ decl, alignment, Some expr ])))

(** Function prototype, or extern global declaration (no definition). *)
let mk_function_or_global_stub m (d: decl): C.declaration_or_function list =
  match d with
  | External _
  | TypeForward _
  | Type _ ->
      []

  | Function (cc, flags, return_type, name, parameters, _) ->
      if is_primitive name then
        []
      else
        let name = to_c_name m (name, Other) in
        begin try
          let parameters = List.map (fun { name; typ } -> name, typ) parameters in
          let qs, spec, decl = mk_spec_and_declarator_f m cc name return_type parameters in
          (* JP: shouldn't we check for the presence of `inline` here? What does
           * the C standard say? inline on prototype and declaration? *)
          (* Regarding __attribute__((unused)), either one is enough. *)
          wrap_verbatim name flags (Decl (mk_comments flags, (qs, spec, None, None, { maybe_unused = false; target = None }, [ decl, None, None ])))
        with e ->
          beprintf "Fatal exception raised in %s\n" name;
          raise e
        end

  | Global (name, macro, flags, t, expr) ->
      if is_primitive name || macro then
        []
      else
        let name = to_c_name m (name, Other) in
        let t = strengthen_array m t expr in
        let t = if List.mem (Common.Const "") flags then CStar.Const t else t in
        let qs, spec, decl = mk_spec_and_declarator m name t in
        wrap_verbatim name flags (Decl (mk_comments flags, (qs, spec, None, Some Extern, { maybe_unused = false; target = None }, [ decl, None, None ])))

type where = H | C

let declared_in_library lid =
  List.exists (fun b -> Bundle.pattern_matches_lid b lid) !Options.library

let hand_written lid =
  List.exists (fun b -> Bundle.pattern_matches_lid b lid) !Options.hand_written

(* Type declarations, external function declarations. These are the things that
 * are either declared in the header (public), or in the c file (private), but
 * not twice. *)
let mk_type_or_external m (w: where) ?(is_inline_static=false) (d: decl): C.declaration_or_function list =
  let mk_forward_decl name flags k =
    let d = match k with
      | FStruct -> C.Struct (Some (name ^ "_s"), None)
      | FUnion -> C.Union (Some (name ^ "_s"), None)
    in
    wrap_verbatim name flags (Decl ([], ([], d, None, Some Typedef, { maybe_unused = false; target = None }, [ Ident name, None, None ])))
  in
  match d with
  | TypeForward (name, flags, k) ->
      let name = to_c_name m (name, Type) in
      mk_forward_decl name flags k
  | Type (name, Struct _, flags) when w = H && List.mem AbstractStruct flags ->
      let name = to_c_name m (name, Type) in
      mk_forward_decl name flags FStruct
  | Type (name, t, flags) ->
      if is_primitive name || (is_inline_static && declared_in_library name) then
        []
      else begin
        let name = to_c_name m (name, Type) in
        match t with
        | Enum cases when !Options.short_enums ->
            (* Note: EEnum translates as just a name -- so we don't have to
             * change use-sites, they directly resolve as the macro. *)
            let max_value, min_value =
              let custom_values = List.filter_map snd cases in
              let custom_values = List.sort compare custom_values in
              (* print_endline (String.concat ", " (List.map Z.to_string custom_values)); *)
              max
                (* conservative if we allow signed values *)
                (if custom_values <> [] then KList.last custom_values else Z.zero)
                (Z.of_int (List.length cases)),
              if custom_values <> [] then List.hd custom_values else Z.zero
            in
            let t =
              if Z.(geq min_value zero && leq max_value (of_string "0xff")) then
                K.UInt8
              else if Z.(geq min_value zero && leq max_value (of_string "0xffff")) then
                K.UInt16
              else if Z.(geq min_value zero && leq max_value (of_string "0xffffffff")) then
                K.UInt32
              else if Z.(geq min_value zero && leq max_value (of_string "0xffffffffffffffff")) then
                K.UInt64
              else if Z.(geq min_value (of_string "-0x7e") && leq max_value (of_string "0x7f")) then
                K.Int8
              else if Z.(geq min_value (of_string "-0x7ffe") && leq max_value (of_string "0x7fff")) then
                K.Int16
              else if Z.(geq min_value (of_string "-0x7ffffffe") && leq max_value (of_string "0x7fffffff")) then
                K.Int32
              else if Z.(geq min_value (of_string "-0x7ffffffffffffffe") && leq max_value (of_string "0x7fffffffffffffff")) then
                K.Int64
              else
                failwith "TODO: support for negative enum values"
            in
            let cases = List.map (fun (lid, v) -> to_c_name m (lid, Other), v) cases in
            wrap_verbatim name flags (Text (enum_as_macros cases)) @
            let qs, spec, decl = mk_spec_and_declarator_t m name (Int t) in
            [ Decl ([], (qs, spec, None, Some Typedef, { maybe_unused = false; target = None }, [ decl, None, None ]))]
        | _ ->
            let qs, spec, decl = mk_spec_and_declarator_t m name t in
            wrap_verbatim name flags (Decl (mk_comments flags, (qs, spec, None, Some Typedef, { maybe_unused = false; target = None }, [ decl, None, None ])))
      end

  | External (name, Function (cc, t, ts), flags, pp) ->
      if is_primitive name ||
        (is_inline_static && declared_in_library name && not (hand_written name))
      then
        []
      else
        let name = to_c_name m (name, Other) in
        let missing_names = List.length ts - List.length pp in
        let arg_names =
          if missing_names >= 0 then
            pp @ List.init missing_names (fun i -> KPrint.bsprintf "x%d" i)
          else
            (* For functions that take a single unit argument, the name of the
             * unit is gone. *)
            fst (KList.split (List.length ts) pp)
        in
        let qs, spec, decl = mk_spec_and_declarator_f m cc name t (List.combine arg_names ts) in
        let inline =
          if List.mem NoInline flags then
            Some C11.NoInline
          else
            None
        in
        wrap_verbatim name flags (Decl (mk_comments flags, (qs, spec, inline, Some Extern, { maybe_unused = false; target = None }, [ decl, None, None ])))

  | External (name, t, flags, _) ->
      if is_primitive name ||
        (is_inline_static && declared_in_library name && not (hand_written name))
      then
        []
      else
        let name = to_c_name m (name, Other) in
        let qs, spec, decl = mk_spec_and_declarator m name t in
        wrap_verbatim name flags (Decl (mk_comments flags, (qs, spec, None, Some Extern, { maybe_unused = false; target = None }, [ decl, None, None ])))

  | Global (name, macro, flags, _, body) when macro && not (is_inline_static && declared_in_library name) ->
      (* Macros behave like types, they ought to be declared once. *)
      let name = to_c_name m (name, Other) in
      wrap_verbatim name flags (Macro (mk_comments flags, name, mk_expr m body))

  | Function _ | Global _ ->
      []


let flags_of_decl (d: CStar.decl) =
  match d with
  | Global (_, _, flags, _, _)
  | Function (_, flags, _, _, _, _)
  | Type (_, _, flags)
  | TypeForward (_, flags, _)
  | External (_, _, flags, _) ->
      flags

(* A mini-DSL to expression control-flow for generation of C declarations in the
 * presence of visibility, C abstract structs, and potentially static headers.
 * *)
let either f1 f2 x =
  match f1 x with
  | [] -> f2 x
  | l -> l

let if_private f d =
  let flags = flags_of_decl d in
  if List.mem Private flags then
    f d
  else
    []

let if_public f d =
  if not (List.mem Private (flags_of_decl d)) && not (List.mem Internal (flags_of_decl d)) then
    f d
  else
    []

let if_internal_or_abstract_struct f d =
  let flags = flags_of_decl d in
  if List.mem Internal flags || List.mem AbstractStruct flags then
    (* let _ = KPrint.bprintf "%a is internal\n" PrintAst.Ops.plid (lid_of_decl d) in *)
    f d
  else
    []

let none _ = []

let if_header_inline_static m f1 f2 d =
  let lid = lid_of_decl d in
  let is_inline_static =
    List.exists (fun p ->
      (* Only things that end up in headers are in the reverse-map. *)
      (Hashtbl.mem m (lid, GlobalNames.Other) || Hashtbl.mem m (lid, GlobalNames.Type) || Hashtbl.mem m (lid, GlobalNames.Macro)) &&
      Bundle.pattern_matches_lid p lid)
    !Options.static_header ||
    List.mem lid [
      [ "FStar"; "UInt8" ], "eq_mask";
      [ "FStar"; "UInt8" ], "gte_mask";
      [ "FStar"; "UInt16" ], "eq_mask";
      [ "FStar"; "UInt16" ], "gte_mask";
      [ "FStar"; "UInt32" ], "eq_mask";
      [ "FStar"; "UInt32" ], "gte_mask";
      [ "FStar"; "UInt64" ], "eq_mask";
      [ "FStar"; "UInt64" ], "gte_mask";
    ]
  in
  (* KPrint.bprintf "%a is inline static? %b\n" PrintAst.Ops.plid lid is_inline_static; *)
  if is_inline_static then
    f1 d
  else
    f2 d

(* Building a .c file *)
let mk_file (m: GlobalNames.mapping) decls =
  (* In the C file, we put function bodies, global bodies, and type
   * definitions and external definitions that were private to the file only.
   * *)
  List.concat_map
    (if_header_inline_static m
      none
      (either
        (mk_function_or_global_body m)
        (if_private (mk_type_or_external m C))))
    decls

let mk_files (map: GlobalNames.mapping) files =
  List.map (fun (name, program) -> name, mk_file map program) files

(* Building three flavors of headers. *)

let mk_static f d =
  let promote_inline inline =
    match inline with
    | None | Some C11.Inline -> Some C11.Inline
    | Some NoInline -> Some NoInline
    | Some MustInline -> Some MustInline
  in

  List.concat_map (function
    | C.Decl (comments, (qs, ts, inline, (None | Some (Static | Extern)), extra, decl_inits)) ->
        let is_func = match decl_inits with
          | [ Function _, _, _ ] -> promote_inline inline
          | [ _ ] -> inline
          | _ -> assert false
        in
        [ C.Decl (comments, (qs, ts, is_func, Some Static, extra, decl_inits)) ]
    | C.Function (comments, (qs, ts, inline, (None | Some (Static | Extern)), extra, decl_inits), body) ->
        (* We make the function static *and* inline UNLESS the user requested
           NoInline *)
        [ C.Function (comments, (qs, ts, promote_inline inline, Some Static, extra, decl_inits), body) ]
    | d ->
        [ d ]
  ) (f d)

(* Generates either a static header (the union of public + internal), OR just
   the public part. *)
let mk_public_header (m: GlobalNames.mapping) decls =
  (* In the header file, we put functions and global stubs, along with type
   * definitions that are visible from the outside. *)
  (* What should be the behavior for a type declaration marked as CAbstract but
   * whose module has -static-header? This ignores CAbstract. *)
  (* Note that static_header + library means that corresponding declarations are
   * effectively dropped on the basis that the user is doing separate extraction
   * & compilation + providing the required header. *)
  List.concat_map
    (if_public (
      (if_header_inline_static m
        (mk_static (either (mk_function_or_global_body m) (mk_type_or_external m ~is_inline_static:true C)))
        (either (mk_function_or_global_stub m) (mk_type_or_external m H)))))
    decls

(* Private part if not already a static header, empty otherwise. *)
let mk_internal_header (m: GlobalNames.mapping) decls =
  List.concat_map
    (if_internal_or_abstract_struct (
      (if_header_inline_static m
        (mk_static (either (mk_function_or_global_body m) (mk_type_or_external m ~is_inline_static:true C)))
        (either (mk_function_or_global_stub m) (mk_type_or_external m C)))))
    decls

let mk_headers (map: GlobalNames.mapping)
  (files: (string * CStar.decl list) list)
=
  (* Generate headers with a sensible order for the message "WRITING H FILES: ...". *)
  let headers = List.fold_left (fun acc (name, program) ->
    (* KPrint.bprintf "making header for %s\n" name; *)
    (* List.iter (fun d -> *)
    (*   KPrint.bprintf "  %a\n" PrintAst.Ops.plid (lid_of_decl d)) program; *)
    let h = mk_public_header map program in
    let acc = if List.length h > 0 then (name, Public h) :: acc else acc in
    let h = mk_internal_header map program in
    let acc = if List.length h > 0 then (name, C.Internal h) :: acc else acc in
    acc
  ) [] files in
  List.rev headers

let drop_empty_headers deps headers: Bundles.all_deps Bundles.StringMap.t =
  let open Bundles in
  (* Refine dependencies to ignore now-gone empty headers. *)
  let kept_internal = List.filter_map (function (name, C.Internal _) -> Some name | _ -> None) headers in
  let kept_public = List.filter_map (function (name, C.Public _) -> Some name | _ -> None) headers in
  let not_dropped_internal f = List.mem f kept_internal in
  let not_dropped_public f = List.mem f kept_public in
  let filter_dep { internal; public } = {
    internal = StringSet.filter not_dropped_internal internal;
    public = StringSet.filter not_dropped_public public
  } in
  StringMap.map (fun { h; internal_h; c } ->
    { h = filter_dep h; internal_h = filter_dep internal_h; c = filter_dep c }
  ) deps