path: root/src/jib/jib_smt.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 Anf
open Ast
open Ast_defs
open Ast_util
open Jib
open Jib_util
open Smtlib
open Property

module IntSet = Set.Make(struct type t = int let compare = compare end)
module IntMap = Map.Make(struct type t = int let compare = compare end)

let zencode_upper_id id = Util.zencode_upper_string (string_of_id id)
let zencode_id id = Util.zencode_string (string_of_id id)
let zencode_name id = string_of_name ~deref_current_exception:false ~zencode:true id
let zencode_uid (id, ctyps) =
  Util.zencode_string (string_of_id id ^ "#" ^ Util.string_of_list "_" string_of_ctyp ctyps)

let opt_ignore_overflow = ref false

let opt_auto = ref false

let opt_debug_graphs = ref false

let opt_propagate_vars = ref false

let opt_unroll_limit = ref 10

module EventMap = Map.Make(Event)

(* Note that we have to use x : ty ref rather than mutable x : ty, to
   make sure { ctx with x = ... } doesn't break the mutable state. *)

(* See mli file for a description of each field *)
type ctx = {
    lbits_index : int;
    lint_size : int;
    vector_index : int;
    register_map : id list CTMap.t;
    tuple_sizes : IntSet.t ref;
    tc_env : Type_check.Env.t;
    pragma_l : Ast.l;
    arg_stack : (int * string) Stack.t;
    ast : Type_check.tannot ast;
    shared : ctyp Bindings.t;
    preserved : IdSet.t;
    events : smt_exp Stack.t EventMap.t ref;
    node : int;
    pathcond : smt_exp Lazy.t;
    use_string : bool ref;
    use_real : bool ref
  }

(* These give the default bounds for various SMT types, stored in the
   initial_ctx. They shouldn't be read or written by anything else! If
   they are changed the output of sail -help needs to be updated to
   reflect this. *)
let opt_default_lint_size = ref 128
let opt_default_lbits_index = ref 8
let opt_default_vector_index = ref 5

let initial_ctx () = {
    lbits_index = !opt_default_lbits_index;
    lint_size = !opt_default_lint_size;
    vector_index = !opt_default_vector_index;
    register_map = CTMap.empty;
    tuple_sizes = ref IntSet.empty;
    tc_env = Type_check.initial_env;
    pragma_l = Parse_ast.Unknown;
    arg_stack = Stack.create ();
    ast = empty_ast;
    shared = Bindings.empty;
    preserved = IdSet.empty;
    events = ref EventMap.empty;
    node = -1;
    pathcond = lazy (Bool_lit true);
    use_string = ref false;
    use_real = ref false;
  }

let event_stack ctx ev =
  match EventMap.find_opt ev !(ctx.events) with
  | Some stack -> stack
  | None ->
     let stack = Stack.create () in
     ctx.events := EventMap.add ev stack !(ctx.events);
     stack

let add_event ctx ev smt =
  let stack = event_stack ctx ev in
  Stack.push (Fn ("and", [Lazy.force ctx.pathcond; smt])) stack

let add_pathcond_event ctx ev =
  Stack.push (Lazy.force ctx.pathcond) (event_stack ctx ev)

let overflow_check ctx smt =
  if not !opt_ignore_overflow then (
    Reporting.warn "Overflow check in generated SMT for" ctx.pragma_l "";
    add_event ctx Overflow smt
  )

let lbits_size ctx = Util.power 2 ctx.lbits_index

let vector_index = ref 5

let smt_unit = mk_enum "Unit" ["Unit"]
let smt_lbits ctx = mk_record "Bits" [("size", Bitvec ctx.lbits_index); ("bits", Bitvec (lbits_size ctx))]

(* [required_width n] is the required number of bits to losslessly
   represent an integer n *)
let required_width n =
  let rec required_width' n =
    if Big_int.equal n Big_int.zero then
      1
    else
      1 + required_width' (Big_int.shift_right n 1)
  in
  required_width' (Big_int.abs n)

let rec smt_ctyp ctx = function
  | CT_constant n -> Bitvec (required_width n)
  | CT_fint n -> Bitvec n
  | CT_lint -> Bitvec ctx.lint_size
  | CT_unit -> smt_unit
  | CT_bit -> Bitvec 1
  | CT_fbits (n, _) -> Bitvec n
  | CT_sbits (n, _) -> smt_lbits ctx
  | CT_lbits _ -> smt_lbits ctx
  | CT_bool -> Bool
  | CT_enum (id, elems) ->
     mk_enum (zencode_upper_id id) (List.map zencode_id elems)
  | CT_struct (id, fields) ->
     mk_record (zencode_upper_id id) (List.map (fun (uid, ctyp) -> (zencode_uid uid, smt_ctyp ctx ctyp)) fields)
  | CT_variant (id, ctors) ->
     mk_variant (zencode_upper_id id) (List.map (fun (uid, ctyp) -> (zencode_uid uid, smt_ctyp ctx ctyp)) ctors)
  | CT_tup ctyps ->
     ctx.tuple_sizes := IntSet.add (List.length ctyps) !(ctx.tuple_sizes);
     Tuple (List.map (smt_ctyp ctx) ctyps)
  | CT_vector (_, ctyp) -> Array (Bitvec !vector_index, smt_ctyp ctx ctyp)
  | CT_string ->
     ctx.use_string := true;
     String
  | CT_real ->
     ctx.use_real := true;
     Real
  | CT_ref ctyp ->
     begin match CTMap.find_opt ctyp ctx.register_map with
     | Some regs -> Bitvec (required_width (Big_int.of_int (List.length regs)))
     | _ -> failwith ("No registers with ctyp: " ^ string_of_ctyp ctyp)
     end
  | CT_list _ -> raise (Reporting.err_todo ctx.pragma_l "Lists not yet supported in SMT generation")
  | CT_fvector _ ->
     Reporting.unreachable ctx.pragma_l __POS__ "Found CT_fvector in SMT property"
  | CT_poly ->
     Reporting.unreachable ctx.pragma_l __POS__ "Found polymorphic type in SMT property"

(* We often need to create a SMT bitvector of a length sz with integer
   value x. [bvpint sz x] does this for positive integers, and [bvint sz x]
   does this for all integers. It's quite awkward because we
   don't have a very good way to get the binary representation of
   either an ocaml integer or a big integer. *)
let bvpint sz x =
  let open Sail2_values in
  if Big_int.less_equal Big_int.zero x && Big_int.less_equal x (Big_int.of_int max_int) then (
    let x = Big_int.to_int x in
    match Printf.sprintf "%X" x |> Util.string_to_list |> List.map nibble_of_char |> Util.option_all with
    | Some nibbles ->
       let bin = List.map (fun (a, b, c, d) -> [a; b; c; d]) nibbles |> List.concat in
       let _, bin = Util.take_drop (function B0 -> true | _ -> false) bin in
       let padding = List.init (sz - List.length bin) (fun _ -> B0) in
       Bitvec_lit (padding @ bin)
    | None -> assert false
  ) else if Big_int.greater x (Big_int.of_int max_int) then (
    let y = ref x in
    let bin = ref [] in
    while (not (Big_int.equal !y Big_int.zero)) do
      let (q, m) = Big_int.quomod !y (Big_int.of_int 2) in
      bin := (if Big_int.equal m Big_int.zero then B0 else B1) :: !bin;
      y := q
    done;
    let padding_size = sz - List.length !bin in
    if padding_size < 0 then
      raise (Reporting.err_general Parse_ast.Unknown
               (Printf.sprintf "Could not create a %d-bit integer with value %s.\nTry increasing the maximum integer size"
                  sz (Big_int.to_string x)));
    let padding = List.init padding_size (fun _ -> B0) in
    Bitvec_lit (padding @ !bin)
  ) else failwith "Invalid bvpint"

let bvint sz x =
  if Big_int.less x Big_int.zero then
    Fn ("bvadd", [Fn ("bvnot", [bvpint sz (Big_int.abs x)]); bvpint sz (Big_int.of_int 1)])
  else
    bvpint sz x

(** [force_size ctx n m exp] takes a smt expression assumed to be a
   integer (signed bitvector) of length m and forces it to be length n
   by either sign extending it or truncating it as required *)
let force_size ?checked:(checked=true) ctx n m smt =
  if n = m then
    smt
  else if n > m then
    SignExtend (n - m, smt)
  else
    let check =
      (* If the top bit of the truncated number is one *)
      Ite (Fn ("=", [Extract (n - 1, n - 1, smt); Bitvec_lit [Sail2_values.B1]]),
           (* Then we have an overflow, unless all bits we truncated were also one *)
           Fn ("not", [Fn ("=", [Extract (m - 1, n, smt); bvones (m - n)])]),
           (* Otherwise, all the top bits must be zero *)
           Fn ("not", [Fn ("=", [Extract (m - 1, n, smt); bvzero (m - n)])]))
    in
    if checked then overflow_check ctx check else ();
    Extract (n - 1, 0, smt)

(** [unsigned_size ctx n m exp] is much like force_size, but it
   assumes that the bitvector is unsigned *)
let unsigned_size ?checked:(checked=true) ctx n m smt =
  if n = m then
    smt
  else if n > m then
    Fn ("concat", [bvzero (n - m); smt])
  else
    Extract (n - 1, 0, smt)

let smt_conversion ctx from_ctyp to_ctyp x =
  match from_ctyp, to_ctyp with
  | _, _ when ctyp_equal from_ctyp to_ctyp -> x
  | CT_constant c, CT_fint sz ->
     bvint sz c
  | CT_constant c, CT_lint ->
     bvint ctx.lint_size c
  | CT_fint sz, CT_lint ->
     force_size ctx ctx.lint_size sz x
  | CT_lint, CT_fint sz ->
     force_size ctx sz ctx.lint_size x
  | CT_lint, CT_fbits (n, _) ->
     force_size ctx n ctx.lint_size x
  | CT_lint, CT_lbits _ ->
     Fn ("Bits", [bvint ctx.lbits_index (Big_int.of_int ctx.lint_size); force_size ctx (lbits_size ctx) ctx.lint_size x])
  | CT_fint n, CT_lbits _ ->
     Fn ("Bits", [bvint ctx.lbits_index (Big_int.of_int n); force_size ctx (lbits_size ctx) n x])
  | CT_lbits _, CT_fbits (n, _) ->
     unsigned_size ctx n (lbits_size ctx) (Fn ("contents", [x]))
  | CT_fbits (n, _), CT_fbits (m, _) ->
     unsigned_size ctx m n x
  | CT_fbits (n, _), CT_lbits _ ->
     Fn ("Bits", [bvint ctx.lbits_index (Big_int.of_int n); unsigned_size ctx (lbits_size ctx) n x])

  | _, _ -> failwith (Printf.sprintf "Cannot perform conversion from %s to %s" (string_of_ctyp from_ctyp) (string_of_ctyp to_ctyp))

(* Translate Jib literals into SMT *)
let rec smt_value ctx vl ctyp =
  let open Value2 in
  match vl, ctyp with
  | VL_bits (bv, true), CT_fbits (n, _) ->
     unsigned_size ctx n (List.length bv) (Bitvec_lit bv)
  | VL_bits (bv, true), CT_lbits _ ->
     let sz = List.length bv in
     Fn ("Bits", [bvint ctx.lbits_index (Big_int.of_int sz); unsigned_size ctx (lbits_size ctx) sz (Bitvec_lit bv)])
  | VL_bool b, _ -> Bool_lit b
  | VL_int n, CT_constant m -> bvint (required_width n) n
  | VL_int n, CT_fint sz -> bvint sz n
  | VL_int n, CT_lint -> bvint ctx.lint_size n
  | VL_bit b, CT_bit -> Bitvec_lit [b]
  | VL_unit, _ -> Enum "unit"
  | VL_string str, _ ->
     ctx.use_string := true;
     String_lit (String.escaped str)
  | VL_real str, _ ->
     ctx.use_real := true;
     if str.[0] = '-' then
       Fn ("-", [Real_lit (String.sub str 1 (String.length str - 1))])
     else
       Real_lit str
  | VL_enum str, _ -> Enum (Util.zencode_string str)
  | VL_ref reg_name, _ ->
     let id = mk_id reg_name in
     let rmap = CTMap.filter (fun ctyp regs -> List.exists (fun reg -> Id.compare reg id = 0) regs) ctx.register_map in
     assert (CTMap.cardinal rmap = 1);
     begin match CTMap.min_binding_opt rmap with
     | Some (ctyp, regs) ->
        begin match Util.list_index (fun reg -> Id.compare reg id = 0) regs with
        | Some i ->
           bvint (required_width (Big_int.of_int (List.length regs))) (Big_int.of_int i)
        | None -> assert false
        end
     | _ -> assert false
     end
  | _ -> failwith ("Cannot translate literal to SMT: " ^ string_of_value vl ^ " : " ^ string_of_ctyp ctyp)

let rec smt_cval ctx cval =
  match cval_ctyp cval with
  | CT_constant n ->
     bvint (required_width n) n
  | _ ->
     match cval with
     | V_lit (vl, ctyp) -> smt_value ctx vl ctyp
     | V_id ((Name (id, _) | Global (id, _)) as ssa_id, _) ->
        begin match Type_check.Env.lookup_id id ctx.tc_env with
        | Enum _ -> Enum (zencode_id id)
        | _ when Bindings.mem id ctx.shared -> Shared (zencode_id id)
        | _ -> Var (zencode_name ssa_id)
        end
     | V_id (ssa_id, _) -> Var (zencode_name ssa_id)
     | V_call (Neq, [cval1; cval2]) ->
        Fn ("not", [Fn ("=", [smt_cval ctx cval1; smt_cval ctx cval2])])
     | V_call (Bvor, [cval1; cval2]) ->
        Fn ("bvor", [smt_cval ctx cval1; smt_cval ctx cval2])
     | V_call (Eq, [cval1; cval2]) ->
        Fn ("=", [smt_cval ctx cval1; smt_cval ctx cval2])
     | V_call (Bnot, [cval]) ->
        Fn ("not", [smt_cval ctx cval])
     | V_call (Band, cvals) ->
        smt_conj (List.map (smt_cval ctx) cvals)
     | V_call (Bor, cvals) ->
        smt_disj (List.map (smt_cval ctx) cvals)
     | V_call (Igt, [cval1; cval2]) ->
        Fn ("bvsgt", [smt_cval ctx cval1; smt_cval ctx cval2])
     | V_call (Iadd, [cval1; cval2]) ->
        Fn ("bvadd", [smt_cval ctx cval1; smt_cval ctx cval2])
     | V_ctor_kind (union, ctor_id, unifiers, _) ->
        Fn ("not", [Tester (zencode_uid (ctor_id, unifiers), smt_cval ctx union)])
     | V_ctor_unwrap (ctor_id, union, unifiers, _) ->
        Fn ("un" ^ zencode_uid (ctor_id, unifiers), [smt_cval ctx union])
     | V_field (record, field) ->
        begin match cval_ctyp record with
        | CT_struct (struct_id, _) ->
           Field (zencode_upper_id struct_id ^ "_" ^ zencode_uid field, smt_cval ctx record)
        | _ -> failwith "Field for non-struct type"
        end
     | V_struct (fields, ctyp) ->
        begin match ctyp with
        | CT_struct (struct_id, field_ctyps) ->
           let set_field (field, cval) =
             match Util.assoc_compare_opt UId.compare field field_ctyps with
             | None -> failwith "Field type not found"
             | Some ctyp ->
                zencode_upper_id struct_id ^ "_" ^ zencode_uid field,
                smt_conversion ctx (cval_ctyp cval) ctyp (smt_cval ctx cval)
           in
           Struct (zencode_upper_id struct_id, List.map set_field fields)
        | _ -> failwith "Struct does not have struct type"
        end
     | V_tuple_member (frag, len, n) ->
        ctx.tuple_sizes := IntSet.add len !(ctx.tuple_sizes);
        Fn (Printf.sprintf "tup_%d_%d" len n, [smt_cval ctx frag])
     | cval -> failwith ("Unrecognised cval " ^ string_of_cval cval)

(**************************************************************************)
(* 1. Generating SMT for Sail builtins                                    *)
(**************************************************************************)

let builtin_type_error ctx fn cvals =
  let args = Util.string_of_list ", " (fun cval -> string_of_ctyp (cval_ctyp cval)) cvals in
  function
  | Some ret_ctyp ->
     let message = Printf.sprintf "%s : (%s) -> %s" fn args (string_of_ctyp ret_ctyp) in
     raise (Reporting.err_todo ctx.pragma_l message)
  | None ->
     raise (Reporting.err_todo ctx.pragma_l (Printf.sprintf "%s : (%s)" fn args))

(* ***** Basic comparisons: lib/flow.sail ***** *)

let builtin_int_comparison fn big_int_fn ctx v1 v2 =
  match cval_ctyp v1, cval_ctyp v2 with
  | CT_lint, CT_lint ->
     Fn (fn, [smt_cval ctx v1; smt_cval ctx v2])
  | CT_fint sz1, CT_fint sz2 ->
     if sz1 == sz2 then
       Fn (fn, [smt_cval ctx v1; smt_cval ctx v2])
     else if sz1 > sz2 then
       Fn (fn, [smt_cval ctx v1; SignExtend (sz1 - sz2, smt_cval ctx v2)])
     else
       Fn (fn, [SignExtend (sz2 - sz1, smt_cval ctx v1); smt_cval ctx v2])
  | CT_constant c, CT_fint sz ->
     Fn (fn, [bvint sz c; smt_cval ctx v2])
  | CT_constant c, CT_lint ->
     Fn (fn, [bvint ctx.lint_size c; smt_cval ctx v2])
  | CT_fint sz, CT_constant c ->
     Fn (fn, [smt_cval ctx v1; bvint sz c])
  | CT_fint sz, CT_lint when sz < ctx.lint_size ->
     Fn (fn, [SignExtend (ctx.lint_size - sz, smt_cval ctx v1); smt_cval ctx v2])
  | CT_lint, CT_fint sz when sz < ctx.lint_size ->
     Fn (fn, [smt_cval ctx v1; SignExtend (ctx.lint_size - sz, smt_cval ctx v2)])
  | CT_lint, CT_constant c ->
     Fn (fn, [smt_cval ctx v1; bvint ctx.lint_size c])
  | CT_constant c1, CT_constant c2 ->
     Bool_lit (big_int_fn c1 c2)
  | _, _ -> builtin_type_error ctx fn [v1; v2] None

let builtin_eq_int = builtin_int_comparison "=" Big_int.equal

let builtin_lt = builtin_int_comparison "bvslt" Big_int.less
let builtin_lteq = builtin_int_comparison "bvsle" Big_int.less_equal
let builtin_gt = builtin_int_comparison "bvsgt" Big_int.greater
let builtin_gteq = builtin_int_comparison "bvsge" Big_int.greater_equal

(* ***** Arithmetic operations: lib/arith.sail ***** *)

let int_size ctx = function
  | CT_constant n -> required_width n
  | CT_fint sz -> sz
  | CT_lint -> ctx.lint_size
  | _ -> Reporting.unreachable ctx.pragma_l __POS__ "Argument to int_size must be an integer type"

let builtin_arith fn big_int_fn padding ctx v1 v2 ret_ctyp =
  (* To detect arithmetic overflow we can expand the input bitvectors
     to some size determined by a padding function, then check we
     don't lose precision when going back after performing the
     operation. *)
  let padding = if !opt_ignore_overflow then (fun x -> x) else padding in
  match cval_ctyp v1, cval_ctyp v2, ret_ctyp with
  | _, _, CT_constant c ->
     bvint (required_width c) c
  | CT_constant c1, CT_constant c2, _ ->
     bvint (int_size ctx ret_ctyp) (big_int_fn c1 c2)

  | ctyp1, ctyp2, _ ->
     let ret_sz = int_size ctx ret_ctyp in
     let smt1 = smt_cval ctx v1 in
     let smt2 = smt_cval ctx v2 in
     force_size ctx ret_sz (padding ret_sz) (Fn (fn, [force_size ctx (padding ret_sz) (int_size ctx ctyp1) smt1;
                                                      force_size ctx (padding ret_sz) (int_size ctx ctyp2) smt2]))

let builtin_add_int = builtin_arith "bvadd" Big_int.add (fun x -> x + 1)
let builtin_sub_int = builtin_arith "bvsub" Big_int.sub (fun x -> x + 1)
let builtin_mult_int = builtin_arith "bvmul" Big_int.mul (fun x -> x * 2)

let builtin_sub_nat ctx v1 v2 ret_ctyp =
  let result = builtin_arith "bvsub" Big_int.sub (fun x -> x + 1) ctx v1 v2 ret_ctyp in
  Ite (Fn ("bvslt", [result; bvint (int_size ctx ret_ctyp) Big_int.zero]),
       bvint (int_size ctx ret_ctyp) Big_int.zero,
       result)

let builtin_negate_int ctx v ret_ctyp =
  match cval_ctyp v, ret_ctyp with
  | _, CT_constant c ->
     bvint (required_width c) c
  | CT_constant c, _ ->
     bvint (int_size ctx ret_ctyp) (Big_int.negate c)
  | ctyp, _ ->
     let open Sail2_values in
     let smt = force_size ctx (int_size ctx ret_ctyp) (int_size ctx ctyp) (smt_cval ctx v) in
     overflow_check ctx (Fn ("=", [smt; Bitvec_lit (B1 :: List.init (int_size ctx ret_ctyp - 1) (fun _ -> B0))]));
     Fn ("bvneg", [smt])

let builtin_shift_int fn big_int_fn ctx v1 v2 ret_ctyp =
  match cval_ctyp v1, cval_ctyp v2, ret_ctyp with
  | _, _, CT_constant c ->
     bvint (required_width c) c
  | CT_constant c1, CT_constant c2, _ ->
     bvint (int_size ctx ret_ctyp) (big_int_fn c1 (Big_int.to_int c2))

  | ctyp, CT_constant c, _ ->
     let n = int_size ctx ctyp in
     force_size ctx (int_size ctx ret_ctyp) n (Fn (fn, [smt_cval ctx v1; bvint n c]))
  | CT_constant c, ctyp, _ ->
     let n = int_size ctx ctyp in
     force_size ctx (int_size ctx ret_ctyp) n (Fn (fn, [bvint n c; smt_cval ctx v2]))

  | ctyp1, ctyp2, _ ->
     let ret_sz = int_size ctx ret_ctyp in
     let smt1 = smt_cval ctx v1 in
     let smt2 = smt_cval ctx v2 in
     (Fn (fn, [force_size ctx ret_sz (int_size ctx ctyp1) smt1;
               force_size ctx ret_sz (int_size ctx ctyp2) smt2]))

let builtin_shl_int = builtin_shift_int "bvshl" Big_int.shift_left
let builtin_shr_int = builtin_shift_int "bvashr" Big_int.shift_right

let builtin_abs_int ctx v ret_ctyp =
  match cval_ctyp v, ret_ctyp with
  | _, CT_constant c ->
     bvint (required_width c) c
  | CT_constant c, _ ->
     bvint (int_size ctx ret_ctyp) (Big_int.abs c)
  | ctyp, _ ->
     let sz = int_size ctx ctyp in
     let smt = smt_cval ctx v in
     Ite (Fn ("=", [Extract (sz - 1, sz -1, smt); Bitvec_lit [Sail2_values.B1]]),
          force_size ctx (int_size ctx ret_ctyp) sz (Fn ("bvneg", [smt])),
          force_size ctx (int_size ctx ret_ctyp) sz smt)

let builtin_pow2 ctx v ret_ctyp =
  match cval_ctyp v, ret_ctyp with
  | CT_constant n, _ when Big_int.greater_equal n Big_int.zero ->
     bvint (int_size ctx ret_ctyp) (Big_int.pow_int_positive 2 (Big_int.to_int n))

  | _ -> builtin_type_error ctx "pow2" [v] (Some ret_ctyp)

let builtin_max_int ctx v1 v2 ret_ctyp =
  match cval_ctyp v1, cval_ctyp v2 with
  | CT_constant n, CT_constant m ->
     bvint (int_size ctx ret_ctyp) (max n m)

  | ctyp1, ctyp2 ->
     let ret_sz = int_size ctx ret_ctyp in
     let smt1 = force_size ctx ret_sz (int_size ctx ctyp1) (smt_cval ctx v1) in
     let smt2 = force_size ctx ret_sz (int_size ctx ctyp2) (smt_cval ctx v2) in
     Ite (Fn ("bvslt", [smt1; smt2]),
          smt2,
          smt1)

let builtin_min_int ctx v1 v2 ret_ctyp =
  match cval_ctyp v1, cval_ctyp v2 with
  | CT_constant n, CT_constant m ->
     bvint (int_size ctx ret_ctyp) (min n m)

  | ctyp1, ctyp2 ->
     let ret_sz = int_size ctx ret_ctyp in
     let smt1 = force_size ctx ret_sz (int_size ctx ctyp1) (smt_cval ctx v1) in
     let smt2 = force_size ctx ret_sz (int_size ctx ctyp2) (smt_cval ctx v2) in
     Ite (Fn ("bvslt", [smt1; smt2]),
          smt1,
          smt2)

let builtin_min_int ctx v1 v2 ret_ctyp =
  match cval_ctyp v1, cval_ctyp v2 with
  | CT_constant n, CT_constant m ->
     bvint (int_size ctx ret_ctyp) (min n m)

  | ctyp1, ctyp2 ->
     let ret_sz = int_size ctx ret_ctyp in
     let smt1 = force_size ctx ret_sz (int_size ctx ctyp1) (smt_cval ctx v1) in
     let smt2 = force_size ctx ret_sz (int_size ctx ctyp2) (smt_cval ctx v2) in
     Ite (Fn ("bvslt", [smt1; smt2]),
          smt1,
          smt2)

let builtin_tdiv_int =
  builtin_arith "bvudiv" (Sail2_values.tdiv_int) (fun x -> x)

let builtin_tmod_int =
  builtin_arith "bvurem" (Sail2_values.tmod_int) (fun x -> x)
  
let bvmask ctx len =
  let all_ones = bvones (lbits_size ctx) in
  let shift = Fn ("concat", [bvzero (lbits_size ctx - ctx.lbits_index); len]) in
  bvnot (bvshl all_ones shift)

let fbits_mask ctx n len = bvnot (bvshl (bvones n) len)

let builtin_eq_bits ctx v1 v2 =
  match cval_ctyp v1, cval_ctyp v2 with
  | CT_fbits (n, _), CT_fbits (m, _) ->
     let o = max n m in
     let smt1 = unsigned_size ctx o n (smt_cval ctx v1) in
     let smt2 = unsigned_size ctx o n (smt_cval ctx v2) in
     Fn ("=", [smt1; smt2])

  | CT_lbits _, CT_lbits _ ->
     let len1 = Fn ("len", [smt_cval ctx v1]) in
     let contents1 = Fn ("contents", [smt_cval ctx v1]) in
     let len2 = Fn ("len", [smt_cval ctx v1]) in
     let contents2 = Fn ("contents", [smt_cval ctx v1]) in
     Fn ("and", [Fn ("=", [len1; len2]);
                 Fn ("=", [Fn ("bvand", [bvmask ctx len1; contents1]); Fn ("bvand", [bvmask ctx len2; contents2])])])

  | CT_lbits _, CT_fbits (n, _) ->
     let smt1 = unsigned_size ctx n (lbits_size ctx) (Fn ("contents", [smt_cval ctx v1])) in
     Fn ("=", [smt1; smt_cval ctx v2])

  | CT_fbits (n, _), CT_lbits _ ->
     let smt2 = unsigned_size ctx n (lbits_size ctx) (Fn ("contents", [smt_cval ctx v2])) in
     Fn ("=", [smt_cval ctx v1; smt2])

  | _ -> builtin_type_error ctx "eq_bits" [v1; v2] None

let builtin_zeros ctx v ret_ctyp =
  match cval_ctyp v, ret_ctyp with
  | _, CT_fbits (n, _) -> bvzero n
  | CT_constant c, CT_lbits _ ->
     Fn ("Bits", [bvint ctx.lbits_index c; bvzero (lbits_size ctx)])
  | ctyp, CT_lbits _ when int_size ctx ctyp >= ctx.lbits_index ->
     Fn ("Bits", [extract (ctx.lbits_index - 1) 0 (smt_cval ctx v); bvzero (lbits_size ctx)])
  | _ -> builtin_type_error ctx "zeros" [v] (Some ret_ctyp)

let builtin_ones ctx cval = function
  | CT_fbits (n, _) -> bvones n
  | CT_lbits _ ->
     let len = extract (ctx.lbits_index - 1) 0 (smt_cval ctx cval) in
     Fn ("Bits", [len; Fn ("bvand", [bvmask ctx len; bvones (lbits_size ctx)])]);
  | ret_ctyp -> builtin_type_error ctx "ones" [cval] (Some ret_ctyp)

(* [bvzeint ctx esz cval] (BitVector Zero Extend INTeger), takes a cval
   which must be an integer type (either CT_fint, or CT_lint), and
   produces a bitvector which is either zero extended or truncated to
   exactly esz bits. *)
let bvzeint ctx esz cval =
  let sz = int_size ctx (cval_ctyp cval) in
  match cval with
  | V_lit (VL_int n, _) ->
     bvint esz n
  | _ ->
     let smt = smt_cval ctx cval in
     if esz = sz then
       smt
     else if esz > sz then
       Fn ("concat", [bvzero (esz - sz); smt])
     else
       Extract (esz - 1, 0, smt)

let builtin_zero_extend ctx vbits vlen ret_ctyp =
  match cval_ctyp vbits, ret_ctyp with
  | CT_fbits (n, _), CT_fbits (m, _) when n = m ->
     smt_cval ctx vbits
  | CT_fbits (n, _), CT_fbits (m, _) ->
     let bv = smt_cval ctx vbits in
     Fn ("concat", [bvzero (m - n); bv])
  | CT_lbits _, CT_fbits (m, _) ->
     assert (lbits_size ctx >= m);
     Extract (m - 1, 0, Fn ("contents", [smt_cval ctx vbits]))
  | CT_fbits (n, _), CT_lbits _ ->
     assert (lbits_size ctx >= n);
     let vbits =
       if lbits_size ctx = n then smt_cval ctx vbits else
       if lbits_size ctx > n then Fn ("concat", [bvzero (lbits_size ctx - n); smt_cval ctx vbits]) else
       assert false
     in
     Fn ("Bits", [bvzeint ctx ctx.lbits_index vlen; vbits])

  | _ -> builtin_type_error ctx "zero_extend" [vbits; vlen] (Some ret_ctyp)

let builtin_sign_extend ctx vbits vlen ret_ctyp =
  match cval_ctyp vbits, ret_ctyp with
  | CT_fbits (n, _), CT_fbits (m, _) when n = m ->
     smt_cval ctx vbits
  | CT_fbits (n, _), CT_fbits (m, _) ->
     let bv = smt_cval ctx vbits in
     let top_bit_one = Fn ("=", [Extract (n - 1, n - 1, bv); Bitvec_lit [Sail2_values.B1]]) in
     Ite (top_bit_one, Fn ("concat", [bvones (m - n); bv]), Fn ("concat", [bvzero (m - n); bv]))

  | _ -> builtin_type_error ctx "sign_extend" [vbits; vlen] (Some ret_ctyp)

let builtin_shift shiftop ctx vbits vshift ret_ctyp =
  match cval_ctyp vbits with
  | CT_fbits (n, _) ->
     let bv = smt_cval ctx vbits in
     let len = bvzeint ctx n vshift in
     Fn (shiftop, [bv; len])

  | CT_lbits _ ->
     let bv = smt_cval ctx vbits in
     let shift = bvzeint ctx (lbits_size ctx) vshift in
     Fn ("Bits", [Fn ("len", [bv]); Fn (shiftop, [Fn ("contents", [bv]); shift])])

  | _ -> builtin_type_error ctx shiftop [vbits; vshift] (Some ret_ctyp)

let builtin_not_bits ctx v ret_ctyp =
  match cval_ctyp v, ret_ctyp with
  | CT_lbits _, CT_fbits (n, _) ->
     bvnot (Extract (n - 1, 0, Fn ("contents", [smt_cval ctx v])))

  | CT_lbits _, CT_lbits _ ->
     let bv = smt_cval ctx v in
     let len = Fn ("len", [bv]) in
     Fn ("Bits", [len; Fn ("bvand", [bvmask ctx len; bvnot (Fn ("contents", [bv]))])])

  | CT_fbits (n, _), CT_fbits (m, _) when n = m ->
     bvnot (smt_cval ctx v)

  | _, _ -> builtin_type_error ctx "not_bits" [v] (Some ret_ctyp)

let builtin_bitwise fn ctx v1 v2 ret_ctyp =
  match cval_ctyp v1, cval_ctyp v2, ret_ctyp with
  | CT_fbits (n, _), CT_fbits (m, _), CT_fbits (o, _) ->
     assert (n = m && m = o);
     let smt1 = smt_cval ctx v1 in
     let smt2 = smt_cval ctx v2 in
     Fn (fn, [smt1; smt2])

  | CT_lbits _, CT_lbits _, CT_lbits _ ->
     let smt1 = smt_cval ctx v1 in
     let smt2 = smt_cval ctx v2 in
     Fn ("Bits", [Fn ("len", [smt1]); Fn (fn, [Fn ("contents", [smt1]); Fn ("contents", [smt2])])])

  | _ -> builtin_type_error ctx fn [v1; v2] (Some ret_ctyp)

let builtin_and_bits = builtin_bitwise "bvand"
let builtin_or_bits = builtin_bitwise "bvor"
let builtin_xor_bits = builtin_bitwise "bvxor"

let builtin_append ctx v1 v2 ret_ctyp =
  match cval_ctyp v1, cval_ctyp v2, ret_ctyp with
  | CT_fbits (n, _), CT_fbits (m, _), CT_fbits (o, _) ->
     assert (n + m = o);
     let smt1 = smt_cval ctx v1 in
     let smt2 = smt_cval ctx v2 in
     Fn ("concat", [smt1; smt2])

  | CT_fbits (n, _), CT_lbits _, CT_lbits _ ->
     let smt1 = smt_cval ctx v1 in
     let smt2 = smt_cval ctx v2 in
     let x = Fn ("concat", [bvzero (lbits_size ctx - n); smt1]) in
     let shift = Fn ("concat", [bvzero (lbits_size ctx - ctx.lbits_index); Fn ("len", [smt2])]) in
     Fn ("Bits", [bvadd (bvint ctx.lbits_index (Big_int.of_int n)) (Fn ("len", [smt2]));
                  bvor (bvshl x shift) (Fn ("contents", [smt2]))])

  | CT_lbits _, CT_fbits (n, _), CT_fbits (m, _) ->
     let smt1 = smt_cval ctx v1 in
     let smt2 = smt_cval ctx v2 in
     Extract (m - 1, 0, Fn ("concat", [Fn ("contents", [smt1]); smt2]))

  | CT_lbits _, CT_fbits (n, _), CT_lbits _ ->
     let smt1 = smt_cval ctx v1 in
     let smt2 = smt_cval ctx v2 in
     Fn ("Bits", [bvadd (bvint ctx.lbits_index (Big_int.of_int n)) (Fn ("len", [smt1]));
                  Extract (lbits_size ctx - 1, 0, Fn ("concat", [Fn ("contents", [smt1]); smt2]))])

  | CT_fbits (n, _), CT_fbits (m, _), CT_lbits _ ->
     let smt1 = smt_cval ctx v1 in
     let smt2 = smt_cval ctx v2 in
     Fn ("Bits", [bvint ctx.lbits_index (Big_int.of_int (n + m));
                  unsigned_size ctx (lbits_size ctx) (n + m) (Fn ("concat", [smt1; smt2]))])

  | CT_lbits _, CT_lbits _, CT_lbits _ ->
     let smt1 = smt_cval ctx v1 in
     let smt2 = smt_cval ctx v2 in
     let x = Fn ("contents", [smt1]) in
     let shift = Fn ("concat", [bvzero (lbits_size ctx - ctx.lbits_index); Fn ("len", [smt2])]) in
     Fn ("Bits", [bvadd (Fn ("len", [smt1])) (Fn ("len", [smt2])); bvor (bvshl x shift) (Fn ("contents", [smt2]))])

  | CT_lbits _, CT_lbits _, CT_fbits (n, _) ->
     let smt1 = smt_cval ctx v1 in
     let smt2 = smt_cval ctx v2 in
     let x = Fn ("contents", [smt1]) in
     let shift = Fn ("concat", [bvzero (lbits_size ctx - ctx.lbits_index); Fn ("len", [smt2])]) in
     unsigned_size ctx n (lbits_size ctx) (bvor (bvshl x shift) (Fn ("contents", [smt2])))

  | _ -> builtin_type_error ctx "append" [v1; v2] (Some ret_ctyp)

let builtin_length ctx v ret_ctyp =
  match cval_ctyp v, ret_ctyp with
  | CT_fbits (n, _), (CT_constant _ | CT_fint _ | CT_lint) ->
     bvint (int_size ctx ret_ctyp) (Big_int.of_int n)

  | CT_lbits _, (CT_constant _ | CT_fint _ | CT_lint) ->
     let sz = ctx.lbits_index in
     let m = int_size ctx ret_ctyp in
     let len = Fn ("len", [smt_cval ctx v]) in
     if m = sz then
       len
     else if m > sz then
       Fn ("concat", [bvzero (m - sz); len])
     else
       Extract (m - 1, 0, len)

  | _, _ -> builtin_type_error ctx "length" [v] (Some ret_ctyp)

let builtin_vector_subrange ctx vec i j ret_ctyp =
  match cval_ctyp vec, cval_ctyp i, cval_ctyp j, ret_ctyp with
  | CT_fbits (n, _), CT_constant i, CT_constant j, CT_fbits _ ->
     Extract (Big_int.to_int i, Big_int.to_int j, smt_cval ctx vec)

  | CT_lbits _, CT_constant i, CT_constant j, CT_fbits _ ->
     Extract (Big_int.to_int i, Big_int.to_int j, Fn ("contents", [smt_cval ctx vec]))

  | CT_fbits (n, _), i_ctyp, CT_constant j, CT_lbits _ when Big_int.equal j Big_int.zero ->
     let i' = force_size ~checked:false ctx ctx.lbits_index (int_size ctx i_ctyp) (smt_cval ctx i) in
     let len = bvadd i' (bvint ctx.lbits_index (Big_int.of_int 1)) in
     Fn ("Bits", [len; Fn ("bvand", [bvmask ctx len; unsigned_size ctx (lbits_size ctx) n (smt_cval ctx vec)])])

  | CT_fbits (n, b), i_ctyp, j_ctyp, ret_ctyp ->
     let i' = force_size ctx n (int_size ctx i_ctyp) (smt_cval ctx i) in
     let j' = force_size ctx n (int_size ctx j_ctyp) (smt_cval ctx j) in
     let len = bvadd (bvadd i' (bvneg j')) (bvint n (Big_int.of_int 1)) in
     let vec' = bvand (bvlshr (smt_cval ctx vec) j') (fbits_mask ctx n len) in
     smt_conversion ctx (CT_fbits (n, b)) ret_ctyp vec'

  | _ -> builtin_type_error ctx "vector_subrange" [vec; i; j] (Some ret_ctyp)

let builtin_vector_access ctx vec i ret_ctyp =
  match cval_ctyp vec, cval_ctyp i, ret_ctyp with
  | CT_fbits (n, _), CT_constant i, CT_bit ->
     Extract (Big_int.to_int i, Big_int.to_int i, smt_cval ctx vec)
  | CT_lbits _, CT_constant i, CT_bit ->
     Extract (Big_int.to_int i, Big_int.to_int i, Fn ("contents", [smt_cval ctx vec]))

  | CT_lbits _, i_ctyp, CT_bit ->
     let shift = force_size ~checked:false ctx (lbits_size ctx) (int_size ctx i_ctyp) (smt_cval ctx i) in
     Extract (0, 0, Fn ("bvlshr", [Fn ("contents", [smt_cval ctx vec]); shift]))

  | CT_vector _, CT_constant i, _ ->
     Fn ("select", [smt_cval ctx vec; bvint !vector_index i])
  | CT_vector _, index_ctyp, _ ->
     Fn ("select", [smt_cval ctx vec; force_size ctx !vector_index (int_size ctx index_ctyp) (smt_cval ctx i)])

  | _ -> builtin_type_error ctx "vector_access" [vec; i] (Some ret_ctyp)

let builtin_vector_update ctx vec i x ret_ctyp =
  match cval_ctyp vec, cval_ctyp i, cval_ctyp x, ret_ctyp with
  | CT_fbits (n, _), CT_constant i, CT_bit, CT_fbits (m, _) when n - 1 > Big_int.to_int i && Big_int.to_int i > 0 ->
     assert (n = m);
     let top = Extract (n - 1, Big_int.to_int i + 1, smt_cval ctx vec) in
     let bot = Extract (Big_int.to_int i - 1, 0, smt_cval ctx vec) in
     Fn ("concat", [top; Fn ("concat", [smt_cval ctx x; bot])])

  | CT_fbits (n, _), CT_constant i, CT_bit, CT_fbits (m, _) when n - 1 = Big_int.to_int i && Big_int.to_int i > 0 ->
     let bot = Extract (Big_int.to_int i - 1, 0, smt_cval ctx vec) in
     Fn ("concat", [smt_cval ctx x; bot])

  | CT_fbits (n, _), CT_constant i, CT_bit, CT_fbits (m, _) when n - 1 > Big_int.to_int i && Big_int.to_int i = 0 ->
     let top = Extract (n - 1, 1, smt_cval ctx vec) in
     Fn ("concat", [top; smt_cval ctx x])

  | CT_fbits (n, _), CT_constant i, CT_bit, CT_fbits (m, _) when n - 1 = 0 && Big_int.to_int i = 0 ->
     smt_cval ctx x

  | CT_vector _, CT_constant i, ctyp, CT_vector _ ->
     Fn ("store", [smt_cval ctx vec; bvint !vector_index i; smt_cval ctx x])
  | CT_vector _, index_ctyp, _, CT_vector _ ->
     Fn ("store", [smt_cval ctx vec; force_size ctx !vector_index (int_size ctx index_ctyp) (smt_cval ctx i); smt_cval ctx x])

  | _ -> builtin_type_error ctx "vector_update" [vec; i; x] (Some ret_ctyp)

let builtin_vector_update_subrange ctx vec i j x ret_ctyp =
  match cval_ctyp vec, cval_ctyp i, cval_ctyp j, cval_ctyp x, ret_ctyp with
  | CT_fbits (n, _), CT_constant i, CT_constant j, CT_fbits (sz, _), CT_fbits (m, _) when n - 1 > Big_int.to_int i && Big_int.to_int j > 0 ->
     assert (n = m);
     let top = Extract (n - 1, Big_int.to_int i + 1, smt_cval ctx vec) in
     let bot = Extract (Big_int.to_int j - 1, 0, smt_cval ctx vec) in
     Fn ("concat", [top; Fn ("concat", [smt_cval ctx x; bot])])

  | CT_fbits (n, _), CT_constant i, CT_constant j, CT_fbits (sz, _), CT_fbits (m, _) when n - 1 = Big_int.to_int i && Big_int.to_int j > 0 ->
     assert (n = m);
     let bot = Extract (Big_int.to_int j - 1, 0, smt_cval ctx vec) in
     Fn ("concat", [smt_cval ctx x; bot])

  | CT_fbits (n, _), CT_constant i, CT_constant j, CT_fbits (sz, _), CT_fbits (m, _) when n - 1 > Big_int.to_int i && Big_int.to_int j = 0 ->
     assert (n = m);
     let top = Extract (n - 1, Big_int.to_int i + 1, smt_cval ctx vec) in
     Fn ("concat", [top; smt_cval ctx x])

  | CT_fbits (n, _), CT_constant i, CT_constant j, CT_fbits (sz, _), CT_fbits (m, _) when n - 1 = Big_int.to_int i && Big_int.to_int j = 0 ->
     smt_cval ctx x

  | CT_fbits (n, b), ctyp_i, ctyp_j, ctyp_x, CT_fbits (m, _) ->
     assert (n = m);
     let i' = force_size ctx n (int_size ctx ctyp_i) (smt_cval ctx i) in
     let j' = force_size ctx n (int_size ctx ctyp_j) (smt_cval ctx j) in
     let x' = smt_conversion ctx ctyp_x (CT_fbits (n, b)) (smt_cval ctx x) in
     let len = bvadd (bvadd i' (bvneg j')) (bvint n (Big_int.of_int 1)) in
     let mask = bvshl (fbits_mask ctx n len) j' in
     bvor (bvand (smt_cval ctx vec) (bvnot mask)) (bvand (bvshl x' j') mask)

  | _ -> builtin_type_error ctx "vector_update_subrange" [vec; i; j; x] (Some ret_ctyp)

let builtin_unsigned ctx v ret_ctyp =
  match cval_ctyp v, ret_ctyp with
  | CT_fbits (n, _), CT_fint m when m > n ->
     let smt = smt_cval ctx v in
     Fn ("concat", [bvzero (m - n); smt])

  | CT_fbits (n, _), CT_lint ->
     if n >= ctx.lint_size then
       failwith "Overflow detected"
     else
       let smt = smt_cval ctx v in
       Fn ("concat", [bvzero (ctx.lint_size - n); smt])

  | CT_lbits _, CT_lint ->
     Extract (ctx.lint_size - 1, 0, Fn ("contents", [smt_cval ctx v]))

  | CT_lbits _, CT_fint m ->
     let smt = Fn ("contents", [smt_cval ctx v]) in
     force_size ctx m (lbits_size ctx) smt

  | ctyp, _ -> builtin_type_error ctx "unsigned" [v] (Some ret_ctyp)

let builtin_signed ctx v ret_ctyp =
  match cval_ctyp v, ret_ctyp with
  | CT_fbits (n, _), CT_fint m when m >= n ->
     SignExtend(m - n, smt_cval ctx v)

  | CT_fbits (n, _), CT_lint ->
     SignExtend(ctx.lint_size - n, smt_cval ctx v)

  | CT_lbits _, CT_lint ->
     Extract (ctx.lint_size - 1, 0, Fn ("contents", [smt_cval ctx v]))
    
  | ctyp, _ -> builtin_type_error ctx "signed" [v] (Some ret_ctyp)

let builtin_add_bits ctx v1 v2 ret_ctyp =
  match cval_ctyp v1, cval_ctyp v2, ret_ctyp with
  | CT_fbits (n, _), CT_fbits (m, _), CT_fbits (o, _) ->
     assert (n = m && m = o);
     Fn ("bvadd", [smt_cval ctx v1; smt_cval ctx v2])

  | CT_lbits _, CT_lbits _, CT_lbits _ ->
     let smt1 = smt_cval ctx v1 in
     let smt2 = smt_cval ctx v2 in
     Fn ("Bits", [Fn ("len", [smt1]); Fn ("bvadd", [Fn ("contents", [smt1]); Fn ("contents", [smt2])])])
     
  | _ -> builtin_type_error ctx "add_bits" [v1; v2] (Some ret_ctyp)

let builtin_sub_bits ctx v1 v2 ret_ctyp =
  match cval_ctyp v1, cval_ctyp v2, ret_ctyp with
  | CT_fbits (n, _), CT_fbits (m, _), CT_fbits (o, _) ->
     assert (n = m && m = o);
     Fn ("bvadd", [smt_cval ctx v1; Fn ("bvneg", [smt_cval ctx v2])])

  | _ -> failwith "Cannot compile sub_bits"

let builtin_add_bits_int ctx v1 v2 ret_ctyp =
  match cval_ctyp v1, cval_ctyp v2, ret_ctyp with
  | CT_fbits (n, _), CT_constant c, CT_fbits (o, _) when n = o ->
     Fn ("bvadd", [smt_cval ctx v1; bvint o c])

  | CT_fbits (n, _), CT_fint m, CT_fbits (o, _) when n = o ->
     Fn ("bvadd", [smt_cval ctx v1; force_size ctx o m (smt_cval ctx v2)])

  | CT_fbits (n, _), CT_lint, CT_fbits (o, _) when n = o ->
     Fn ("bvadd", [smt_cval ctx v1; force_size ctx o ctx.lint_size (smt_cval ctx v2)])

  | CT_lbits _, CT_fint n, CT_lbits _ when n < lbits_size ctx ->
     let smt1 = smt_cval ctx v1 in
     let smt2 = force_size ctx (lbits_size ctx) n (smt_cval ctx v2) in
     Fn ("Bits", [Fn ("len", [smt1]); Fn ("bvadd", [Fn ("contents", [smt1]); smt2])])

  | _ -> builtin_type_error ctx "add_bits_int" [v1; v2] (Some ret_ctyp)

let builtin_sub_bits_int ctx v1 v2 ret_ctyp =
  match cval_ctyp v1, cval_ctyp v2, ret_ctyp with
  | CT_fbits (n, _), CT_constant c, CT_fbits (o, _) when n = o ->
     Fn ("bvadd", [smt_cval ctx v1; bvint o (Big_int.negate c)])

  | CT_fbits (n, _), CT_fint m, CT_fbits (o, _) when n = o ->
     Fn ("bvsub", [smt_cval ctx v1; force_size ctx o m (smt_cval ctx v2)])

  | CT_fbits (n, _), CT_lint, CT_fbits (o, _) when n = o ->
     Fn ("bvsub", [smt_cval ctx v1; force_size ctx o ctx.lint_size (smt_cval ctx v2)])

  | _ -> builtin_type_error ctx "sub_bits_int" [v1; v2] (Some ret_ctyp)

let builtin_replicate_bits ctx v1 v2 ret_ctyp =
  match cval_ctyp v1, cval_ctyp v2, ret_ctyp with
  | CT_fbits (n, _), CT_constant c, CT_fbits (m, _) ->
     assert (n * Big_int.to_int c = m);
     let smt = smt_cval ctx v1 in
     Fn ("concat", List.init (Big_int.to_int c) (fun _ -> smt))

  | CT_fbits (n, _), _, CT_fbits (m, _) ->
     let smt = smt_cval ctx v1 in
     let c = m / n in
     Fn ("concat", List.init c (fun _ -> smt))

  | CT_fbits (n, _), v2_ctyp, CT_lbits _ ->
     let times = (lbits_size ctx / n) + 1 in
     let len = force_size ~checked:false ctx ctx.lbits_index (int_size ctx v2_ctyp) (smt_cval ctx v2) in
     let smt1 = smt_cval ctx v1 in
     let contents = Extract (lbits_size ctx - 1, 0, Fn ("concat", List.init times (fun _ -> smt1))) in
     Fn ("Bits", [len; Fn ("bvand", [bvmask ctx len; contents])])

  | _ -> builtin_type_error ctx "replicate_bits" [v1; v2] (Some ret_ctyp)

let builtin_sail_truncate ctx v1 v2 ret_ctyp =
  match cval_ctyp v1, cval_ctyp v2, ret_ctyp with
  | CT_fbits (n, _), CT_constant c, CT_fbits (m, _) ->
     assert (Big_int.to_int c = m);
     Extract (Big_int.to_int c - 1, 0, smt_cval ctx v1)

  | CT_lbits _, CT_constant c, CT_fbits (m, _) ->
     assert (Big_int.to_int c = m && m < lbits_size ctx);
     Extract (Big_int.to_int c - 1, 0, Fn ("contents", [smt_cval ctx v1]))

  | CT_fbits (n, _), _, CT_lbits _ ->
     let smt1 = unsigned_size ctx (lbits_size ctx) n (smt_cval ctx v1) in
     let smt2 = bvzeint ctx ctx.lbits_index v2 in
     Fn ("Bits", [smt2; Fn ("bvand", [bvmask ctx smt2; smt1])])

  | _ -> builtin_type_error ctx "sail_truncate" [v1; v2] (Some ret_ctyp)

let builtin_sail_truncateLSB ctx v1 v2 ret_ctyp =
  match cval_ctyp v1, cval_ctyp v2, ret_ctyp with
  | CT_fbits (n, _), CT_constant c, CT_fbits (m, _) ->
     assert (Big_int.to_int c = m);
     Extract (n - 1, n - Big_int.to_int c, smt_cval ctx v1)

  | _ -> builtin_type_error ctx "sail_truncateLSB" [v1; v2] (Some ret_ctyp)

let builtin_slice ctx v1 v2 v3 ret_ctyp =
  match cval_ctyp v1, cval_ctyp v2, cval_ctyp v3, ret_ctyp with
  | CT_lbits _, CT_constant start, CT_constant len, CT_fbits (_, _) ->
     let top = Big_int.pred (Big_int.add start len) in
     Extract(Big_int.to_int top, Big_int.to_int start, Fn ("contents", [smt_cval ctx v1]))

  | CT_fbits (_, _), CT_constant start, CT_constant len, CT_fbits (_, _) ->
     let top = Big_int.pred (Big_int.add start len) in
     Extract(Big_int.to_int top, Big_int.to_int start, smt_cval ctx v1)

  | CT_fbits (_, ord), CT_fint _, CT_constant len, CT_fbits (_, _) ->
     Extract(Big_int.to_int (Big_int.pred len), 0, builtin_shift "bvlshr" ctx v1 v2 (cval_ctyp v1))

  | CT_fbits(n, ord), ctyp2, _, CT_lbits _ ->
     let smt1 = force_size ctx (lbits_size ctx) n (smt_cval ctx v1) in
     let smt2 = force_size ctx (lbits_size ctx) (int_size ctx ctyp2) (smt_cval ctx v2) in
     let smt3 = bvzeint ctx ctx.lbits_index v3 in
     Fn ("Bits", [smt3; Fn ("bvand", [Fn ("bvlshr", [smt1; smt2]); bvmask ctx smt3])])

  | _ -> builtin_type_error ctx "slice" [v1; v2; v3] (Some ret_ctyp)

let builtin_get_slice_int ctx v1 v2 v3 ret_ctyp =
  match cval_ctyp v1, cval_ctyp v2, cval_ctyp v3, ret_ctyp with
  | CT_constant len, ctyp, CT_constant start, CT_fbits (ret_sz, _) ->
     let len = Big_int.to_int len in
     let start = Big_int.to_int start in
     let in_sz = int_size ctx ctyp in
     let smt =
       if in_sz < len + start then
         force_size ctx (len + start) in_sz (smt_cval ctx v2)
       else
         smt_cval ctx v2
     in
     Extract ((start + len) - 1, start, smt)

  | CT_lint, CT_lint, CT_constant start, CT_lbits _ when Big_int.equal start Big_int.zero ->
     let len = Extract (ctx.lbits_index - 1, 0, smt_cval ctx v1) in
     let contents = unsigned_size ~checked:false ctx (lbits_size ctx) ctx.lint_size (smt_cval ctx v2) in
     Fn ("Bits", [len; Fn ("bvand", [bvmask ctx len; contents])])

  | CT_lint, ctyp2, ctyp3, ret_ctyp ->
     let len = Extract (ctx.lbits_index - 1, 0, smt_cval ctx v1) in
     let smt2 = force_size ctx (lbits_size ctx) (int_size ctx ctyp2) (smt_cval ctx v2) in
     let smt3 = force_size ctx (lbits_size ctx) (int_size ctx ctyp3) (smt_cval ctx v3) in
     let result = bvand (bvmask ctx len) (bvlshr smt2 smt3) in
     smt_conversion ctx CT_lint ret_ctyp result

  | _ -> builtin_type_error ctx "get_slice_int" [v1; v2; v3] (Some ret_ctyp)

let builtin_count_leading_zeros ctx v ret_ctyp =
  let ret_sz = int_size ctx ret_ctyp in
  let rec lzcnt sz smt =
    if sz == 1 then
      Ite (Fn ("=", [Extract (0, 0, smt); Bitvec_lit [Sail2_values.B0]]),
           bvint ret_sz (Big_int.of_int 1),
           bvint ret_sz (Big_int.zero))
    else (
      assert (sz land (sz - 1) = 0);
      let hsz = sz / 2 in
      Ite (Fn ("=", [Extract (sz - 1, hsz, smt); bvzero hsz]),
           Fn ("bvadd", [bvint ret_sz (Big_int.of_int hsz); lzcnt hsz (Extract (hsz - 1, 0, smt))]),
           lzcnt hsz (Extract (sz - 1, hsz, smt)))
    )
  in
  let smallest_greater_power_of_two n =
    let m = ref 1 in
    while !m < n do
      m := !m lsl 1
    done;
    assert (!m land (!m - 1) = 0);
    !m
  in
  match cval_ctyp v with
  | CT_fbits (sz, _) when sz land (sz - 1) = 0 ->
     lzcnt sz (smt_cval ctx v)

  | CT_fbits (sz, _) ->
     let padded_sz = smallest_greater_power_of_two sz in
     let padding = bvzero (padded_sz - sz) in
     Fn ("bvsub", [lzcnt padded_sz (Fn ("concat", [padding; smt_cval ctx v]));
                   bvint ret_sz (Big_int.of_int (padded_sz - sz))])

  | CT_lbits _ ->
     let smt = smt_cval ctx v in
     Fn ("bvsub", [lzcnt (lbits_size ctx) (Fn ("contents", [smt]));
                   Fn ("bvsub", [bvint ret_sz (Big_int.of_int (lbits_size ctx));
                                 Fn ("concat", [bvzero (ret_sz - ctx.lbits_index); Fn ("len", [smt])])])])

  | _ -> builtin_type_error ctx "count_leading_zeros" [v] (Some ret_ctyp)

let builtin_set_slice_bits ctx v1 v2 v3 v4 v5 ret_ctyp =
  match cval_ctyp v1, cval_ctyp v2, cval_ctyp v3, cval_ctyp v4, cval_ctyp v5, ret_ctyp with
  | CT_constant n', CT_constant m', CT_fbits (n, _), CT_constant pos, CT_fbits (m, _), CT_fbits(n'', _)
    when Big_int.to_int m' = m && Big_int.to_int n' = n && n'' = n && Big_int.less_equal (Big_int.add pos m') n' ->
     let pos = Big_int.to_int pos in
     if pos = 0 then
       let mask = Fn ("concat", [bvones (n - m); bvzero m]) in
       let smt5 = Fn ("concat", [bvzero (n - m); smt_cval ctx v5]) in
       Fn ("bvor", [Fn ("bvand", [smt_cval ctx v3; mask]); smt5])
     else if n - m - pos = 0 then
       let mask = Fn ("concat", [bvzero m; bvones pos]) in
       let smt5 = Fn ("concat", [smt_cval ctx v5; bvzero pos]) in
       Fn ("bvor", [Fn ("bvand", [smt_cval ctx v3; mask]); smt5])
     else
       let mask = Fn ("concat", [bvones (n - m - pos); Fn ("concat", [bvzero m; bvones pos])]) in
       let smt5 = Fn ("concat", [bvzero (n - m - pos); Fn ("concat", [smt_cval ctx v5; bvzero pos])]) in
       Fn ("bvor", [Fn ("bvand", [smt_cval ctx v3; mask]); smt5])

  (* set_slice_bits(len, slen, x, pos, y) =
       let mask = slice_mask(len, pos, slen) in
       (x AND NOT(mask)) OR ((unsigned_size(len, y) << pos) AND mask) *)
  | CT_constant n', _, CT_fbits (n, _), _, CT_lbits _, CT_fbits (n'', _)
    when Big_int.to_int n' = n && n'' = n ->
      let pos = bvzeint ctx (lbits_size ctx) v4 in
      let slen = bvzeint ctx ctx.lbits_index v2 in
      let mask = Fn ("bvshl", [bvmask ctx slen; pos]) in
      let smt3 = unsigned_size ctx (lbits_size ctx) n (smt_cval ctx v3) in
      let smt3' = Fn ("bvand", [smt3; Fn ("bvnot", [mask])]) in
      let smt5 = Fn ("contents", [smt_cval ctx v5]) in
      let smt5' = Fn ("bvand", [Fn ("bvshl", [smt5; pos]); mask]) in
      Extract (n - 1, 0, Fn ("bvor", [smt3'; smt5']))

  | _ -> builtin_type_error ctx "set_slice" [v1; v2; v3; v4; v5] (Some ret_ctyp)

let builtin_compare_bits fn ctx v1 v2 ret_ctyp =
  match cval_ctyp v1, cval_ctyp v2 with
  | CT_fbits (n, _), CT_fbits (m, _) when n = m ->
     Fn (fn, [smt_cval ctx v1; smt_cval ctx v2])

  | _ -> builtin_type_error ctx fn [v1; v2] (Some ret_ctyp)

(* ***** String operations: lib/real.sail ***** *)

let builtin_decimal_string_of_bits ctx v =
  begin match cval_ctyp v with
  | CT_fbits (n, _) ->
     Fn ("int.to.str", [Fn ("bv2nat", [smt_cval ctx v])])

  | _ -> builtin_type_error ctx "decimal_string_of_bits" [v] None
  end

(* ***** Real number operations: lib/real.sail ***** *)

let builtin_sqrt_real ctx root v =
  ctx.use_real := true;
  let smt = smt_cval ctx v in
  [Declare_const (root, Real);
   Assert (Fn ("and", [Fn ("=", [smt; Fn ("*", [Var root; Var root])]);
                       Fn (">=", [Var root; Real_lit "0.0"])]))]

let smt_builtin ctx name args ret_ctyp =
  match name, args, ret_ctyp with
  | "eq_anything", [v1; v2], CT_bool -> Fn ("=", [smt_cval ctx v1; smt_cval ctx v2])

  (* lib/flow.sail *)
  | "eq_bit",  [v1; v2], CT_bool -> Fn ("=", [smt_cval ctx v1; smt_cval ctx v2])
  | "eq_bool", [v1; v2], CT_bool -> Fn ("=", [smt_cval ctx v1; smt_cval ctx v2])
  | "eq_unit", [v1; v2], CT_bool -> Fn ("=", [smt_cval ctx v1; smt_cval ctx v2])

  | "eq_int",  [v1; v2], CT_bool -> builtin_eq_int ctx v1 v2

  | "not", [v], _ -> Fn ("not", [smt_cval ctx v])
  | "lt",   [v1; v2], _ -> builtin_lt ctx v1 v2
  | "lteq", [v1; v2], _ -> builtin_lteq ctx v1 v2
  | "gt",   [v1; v2], _ -> builtin_gt ctx v1 v2
  | "gteq", [v1; v2], _ -> builtin_gteq ctx v1 v2

  (* lib/arith.sail *)
  | "add_int", [v1; v2], _ -> builtin_add_int ctx v1 v2 ret_ctyp
  | "sub_int", [v1; v2], _ -> builtin_sub_int ctx v1 v2 ret_ctyp
  | "sub_nat", [v1; v2], _ -> builtin_sub_nat ctx v1 v2 ret_ctyp
  | "mult_int", [v1; v2], _ -> builtin_mult_int ctx v1 v2 ret_ctyp
  | "neg_int", [v], _ -> builtin_negate_int ctx v ret_ctyp
  | "shl_int", [v1; v2], _ -> builtin_shl_int ctx v1 v2 ret_ctyp
  | "shr_int", [v1; v2], _ -> builtin_shr_int ctx v1 v2 ret_ctyp
  | "shl_mach_int", [v1; v2], _ -> builtin_shl_int ctx v1 v2 ret_ctyp
  | "shr_mach_int", [v1; v2], _ -> builtin_shr_int ctx v1 v2 ret_ctyp
  | "abs_int", [v], _ -> builtin_abs_int ctx v ret_ctyp
  | "pow2", [v], _ -> builtin_pow2 ctx v ret_ctyp

  | "max_int", [v1; v2], _ -> builtin_max_int ctx v1 v2 ret_ctyp
  | "min_int", [v1; v2], _ -> builtin_min_int ctx v1 v2 ret_ctyp

  | "ediv_int", [v1; v2], _ -> builtin_tdiv_int ctx v1 v2 ret_ctyp

  (* All signed and unsigned bitvector comparisons *)
  | "slt_bits", [v1; v2], CT_bool -> builtin_compare_bits "bvslt" ctx v1 v2 ret_ctyp
  | "ult_bits", [v1; v2], CT_bool -> builtin_compare_bits "bvult" ctx v1 v2 ret_ctyp
  | "sgt_bits", [v1; v2], CT_bool -> builtin_compare_bits "bvsgt" ctx v1 v2 ret_ctyp
  | "ugt_bits", [v1; v2], CT_bool -> builtin_compare_bits "bvugt" ctx v1 v2 ret_ctyp
  | "slteq_bits", [v1; v2], CT_bool -> builtin_compare_bits "bvsle" ctx v1 v2 ret_ctyp
  | "ulteq_bits", [v1; v2], CT_bool -> builtin_compare_bits "bvule" ctx v1 v2 ret_ctyp
  | "sgteq_bits", [v1; v2], CT_bool -> builtin_compare_bits "bvsge" ctx v1 v2 ret_ctyp
  | "ugteq_bits", [v1; v2], CT_bool -> builtin_compare_bits "bvuge" ctx v1 v2 ret_ctyp

  (* lib/vector_dec.sail *)
  | "eq_bits", [v1; v2], CT_bool -> builtin_eq_bits ctx v1 v2
  | "zeros", [v], _ -> builtin_zeros ctx v ret_ctyp
  | "sail_zeros", [v], _ -> builtin_zeros ctx v ret_ctyp
  | "ones", [v], _ -> builtin_ones ctx v ret_ctyp
  | "sail_ones", [v], _ -> builtin_ones ctx v ret_ctyp
  | "zero_extend", [v1; v2], _ -> builtin_zero_extend ctx v1 v2 ret_ctyp
  | "sign_extend", [v1; v2], _ -> builtin_sign_extend ctx v1 v2 ret_ctyp
  | "sail_truncate", [v1; v2], _ -> builtin_sail_truncate ctx v1 v2 ret_ctyp
  | "sail_truncateLSB", [v1; v2], _ -> builtin_sail_truncateLSB ctx v1 v2 ret_ctyp
  | "shiftl", [v1; v2], _ -> builtin_shift "bvshl" ctx v1 v2 ret_ctyp
  | "shiftr", [v1; v2], _ -> builtin_shift "bvlshr" ctx v1 v2 ret_ctyp
  | "arith_shiftr", [v1; v2], _ -> builtin_shift "bvashr" ctx v1 v2 ret_ctyp
  | "and_bits", [v1; v2], _ -> builtin_and_bits ctx v1 v2 ret_ctyp
  | "or_bits", [v1; v2], _ -> builtin_or_bits ctx v1 v2 ret_ctyp
  | "xor_bits", [v1; v2], _ -> builtin_xor_bits ctx v1 v2 ret_ctyp
  | "not_bits", [v], _ -> builtin_not_bits ctx v ret_ctyp
  | "add_bits", [v1; v2], _ -> builtin_add_bits ctx v1 v2 ret_ctyp
  | "add_bits_int", [v1; v2], _ -> builtin_add_bits_int ctx v1 v2 ret_ctyp
  | "sub_bits", [v1; v2], _ -> builtin_sub_bits ctx v1 v2 ret_ctyp
  | "sub_bits_int", [v1; v2], _ -> builtin_sub_bits_int ctx v1 v2 ret_ctyp
  | "append", [v1; v2], _ -> builtin_append ctx v1 v2 ret_ctyp
  | "length", [v], ret_ctyp -> builtin_length ctx v ret_ctyp
  | "vector_access", [v1; v2], ret_ctyp -> builtin_vector_access ctx v1 v2 ret_ctyp
  | "vector_subrange", [v1; v2; v3], ret_ctyp -> builtin_vector_subrange ctx v1 v2 v3 ret_ctyp
  | "vector_update", [v1; v2; v3], ret_ctyp -> builtin_vector_update ctx v1 v2 v3 ret_ctyp
  | "vector_update_subrange", [v1; v2; v3; v4], ret_ctyp -> builtin_vector_update_subrange ctx v1 v2 v3 v4 ret_ctyp
  | "sail_unsigned", [v], ret_ctyp -> builtin_unsigned ctx v ret_ctyp
  | "sail_signed", [v], ret_ctyp -> builtin_signed ctx v ret_ctyp
  | "replicate_bits", [v1; v2], ret_ctyp -> builtin_replicate_bits ctx v1 v2 ret_ctyp
  | "count_leading_zeros", [v], ret_ctyp -> builtin_count_leading_zeros ctx v ret_ctyp
  | "slice", [v1; v2; v3], ret_ctyp -> builtin_slice ctx v1 v2 v3 ret_ctyp
  | "get_slice_int", [v1; v2; v3], ret_ctyp -> builtin_get_slice_int ctx v1 v2 v3 ret_ctyp
  | "set_slice", [v1; v2; v3; v4; v5], ret_ctyp -> builtin_set_slice_bits ctx v1 v2 v3 v4 v5 ret_ctyp

  (* string builtins *)
  | "concat_str", [v1; v2], CT_string -> ctx.use_string := true; Fn ("str.++", [smt_cval ctx v1; smt_cval ctx v2])
  | "eq_string", [v1; v2], CT_bool -> ctx.use_string := true; Fn ("=", [smt_cval ctx v1; smt_cval ctx v2])
  | "decimal_string_of_bits", [v], CT_string -> ctx.use_string := true; builtin_decimal_string_of_bits ctx v

  (* lib/real.sail *)
  (* Note that sqrt_real is special and is handled by smt_instr. *)
  | "eq_real", [v1; v2], CT_bool -> ctx.use_real := true; Fn ("=", [smt_cval ctx v1; smt_cval ctx v2])
  | "neg_real", [v], CT_real -> ctx.use_real := true; Fn ("-", [smt_cval ctx v])
  | "add_real",  [v1; v2], CT_real -> ctx.use_real := true; Fn ("+", [smt_cval ctx v1; smt_cval ctx v2])
  | "sub_real",  [v1; v2], CT_real -> ctx.use_real := true; Fn ("-", [smt_cval ctx v1; smt_cval ctx v2])
  | "mult_real", [v1; v2], CT_real -> ctx.use_real := true; Fn ("*", [smt_cval ctx v1; smt_cval ctx v2])
  | "div_real",  [v1; v2], CT_real -> ctx.use_real := true; Fn ("/", [smt_cval ctx v1; smt_cval ctx v2])
  | "lt_real",   [v1; v2], CT_bool -> ctx.use_real := true; Fn ("<", [smt_cval ctx v1; smt_cval ctx v2])
  | "gt_real",   [v1; v2], CT_bool -> ctx.use_real := true; Fn (">", [smt_cval ctx v1; smt_cval ctx v2])
  | "lteq_real", [v1; v2], CT_bool -> ctx.use_real := true; Fn ("<=", [smt_cval ctx v1; smt_cval ctx v2])
  | "gteq_real", [v1; v2], CT_bool -> ctx.use_real := true; Fn (">=", [smt_cval ctx v1; smt_cval ctx v2])

  | _ ->
     Reporting.unreachable ctx.pragma_l __POS__ ("Unknown builtin " ^ name ^ " " ^ Util.string_of_list ", " string_of_ctyp (List.map cval_ctyp args) ^ " -> " ^ string_of_ctyp ret_ctyp)

let loc_doc = function
  | Parse_ast.Documented (str, l) -> str
  | _ -> "UNKNOWN"

(* Memory reads and writes as defined in lib/regfp.sail *)
let writes = ref (-1)

let builtin_write_mem l ctx wk addr_size addr data_size data =
  incr writes;
  let name = "W" ^ string_of_int !writes in
  [Write_mem {
       name = name;
       node = ctx.node;
       active = Lazy.force ctx.pathcond;
       kind = smt_cval ctx wk;
       addr = smt_cval ctx addr;
       addr_type = smt_ctyp ctx (cval_ctyp addr);
       data = smt_cval ctx data;
       data_type = smt_ctyp ctx (cval_ctyp data);
       doc = loc_doc l
  }],
  Var (name ^ "_ret")

let ea_writes = ref (-1)

let builtin_write_mem_ea ctx wk addr_size addr data_size =
  incr ea_writes;
  let name = "A" ^ string_of_int !ea_writes in
  [Write_mem_ea (name, ctx.node, Lazy.force ctx.pathcond, smt_cval ctx wk,
                 smt_cval ctx addr, smt_ctyp ctx (cval_ctyp addr), smt_cval ctx data_size, smt_ctyp ctx (cval_ctyp data_size))],
  Enum "unit"

let reads = ref (-1)

let builtin_read_mem l ctx rk addr_size addr data_size ret_ctyp =
  incr reads;
  let name = "R" ^ string_of_int !reads in
  [Read_mem {
       name = name;
       node = ctx.node;
       active = Lazy.force ctx.pathcond;
       ret_type = smt_ctyp ctx ret_ctyp;
       kind = smt_cval ctx rk;
       addr = smt_cval ctx addr;
       addr_type = smt_ctyp ctx (cval_ctyp addr);
       doc = loc_doc l
  }],
  Read_res name

let excl_results = ref (-1)

let builtin_excl_res ctx =
  incr excl_results;
  let name = "E" ^ string_of_int !excl_results in
  [Excl_res (name, ctx.node, Lazy.force ctx.pathcond)],
  Var (name ^ "_ret")

let barriers = ref (-1)

let builtin_barrier l ctx bk =
  incr barriers;
  let name = "B" ^ string_of_int !barriers in
  [Barrier {
       name = name;
       node = ctx.node;
       active = Lazy.force ctx.pathcond;
       kind = smt_cval ctx bk;
       doc = loc_doc l
  }],
  Enum "unit"

let cache_maintenances = ref (-1)

let builtin_cache_maintenance l ctx cmk addr_size addr =
  incr cache_maintenances;
  let name = "M" ^ string_of_int !cache_maintenances in
  [Cache_maintenance {
       name = name;
       node = ctx.node;
       active = Lazy.force ctx.pathcond;
       kind = smt_cval ctx cmk;
       addr = smt_cval ctx addr;
       addr_type = smt_ctyp ctx (cval_ctyp addr);
       doc = loc_doc l
  }],
  Enum "unit"

let branch_announces = ref (-1)

let builtin_branch_announce l ctx addr_size addr =
  incr branch_announces;
  let name = "C" ^ string_of_int !branch_announces in
  [Branch_announce {
       name = name;
       node = ctx.node;
       active = Lazy.force ctx.pathcond;
       addr = smt_cval ctx addr;
       addr_type = smt_ctyp ctx (cval_ctyp addr);
       doc = loc_doc l
  }],
  Enum "unit"

let define_const ctx id ctyp exp = Define_const (zencode_name id, smt_ctyp ctx ctyp, exp)
let preserve_const ctx id ctyp exp = Preserve_const (string_of_id id, smt_ctyp ctx ctyp, exp)
let declare_const ctx id ctyp = Declare_const (zencode_name id, smt_ctyp ctx ctyp)

let smt_ctype_def ctx = function
  | CTD_enum (id, elems) ->
     [declare_datatypes (mk_enum (zencode_upper_id id) (List.map zencode_id elems))]

  | CTD_struct (id, fields) ->
     [declare_datatypes
       (mk_record (zencode_upper_id id)
          (List.map (fun (field, ctyp) -> zencode_upper_id id ^ "_" ^ zencode_uid field, smt_ctyp ctx ctyp) fields))]

  | CTD_variant (id, ctors) ->
     [declare_datatypes
       (mk_variant (zencode_upper_id id)
         (List.map (fun (ctor, ctyp) -> zencode_uid ctor, smt_ctyp ctx ctyp) ctors))]

let rec generate_ctype_defs ctx = function
  | CDEF_type ctd :: cdefs -> smt_ctype_def ctx ctd :: generate_ctype_defs ctx cdefs
  | _ :: cdefs -> generate_ctype_defs ctx cdefs
  | [] -> []

let rec generate_reg_decs ctx inits = function
  | CDEF_reg_dec (id, ctyp, _) :: cdefs when not (NameMap.mem (Global (id, 0)) inits)->
     Declare_const (zencode_name (Global (id, 0)), smt_ctyp ctx ctyp)
     :: generate_reg_decs ctx inits cdefs
  | _ :: cdefs -> generate_reg_decs ctx inits cdefs
  | [] -> []

(**************************************************************************)
(* 2. Converting sail types to Jib types for SMT                          *)
(**************************************************************************)

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))

module SMT_config(Opts : sig val unroll_limit : int end) : Jib_compile.Config = struct
  open Jib_compile

  (** Convert a sail type into a C-type. This function can be quite
     slow, because it uses ctx.local_env and SMT to analyse the Sail
     types and attempts to fit them into the smallest possible C
     types, provided ctx.optimize_smt is true (default) **)
  let rec convert_typ ctx typ =
    let open Ast in
    let open Type_check in
    let Typ_aux (typ_aux, l) as typ = Env.expand_synonyms ctx.tc_env typ in
    match typ_aux with
    | Typ_id id when string_of_id id = "bit"    -> CT_bit
    | Typ_id id when string_of_id id = "bool"   -> CT_bool
    | Typ_id id when string_of_id id = "int"    -> CT_lint
    | Typ_id id when string_of_id id = "nat"    -> CT_lint
    | Typ_id id when string_of_id id = "unit"   -> CT_unit
    | Typ_id id when string_of_id id = "string" -> CT_string
    | Typ_id id when string_of_id id = "real"   -> CT_real

    | Typ_app (id, _) when string_of_id id = "atom_bool" -> CT_bool

    | Typ_app (id, args) when string_of_id id = "itself" ->
       convert_typ ctx (Typ_aux (Typ_app (mk_id "atom", args), l))
    | Typ_app (id, _) when string_of_id id = "range" || string_of_id id = "atom" || string_of_id id = "implicit" ->
       begin match destruct_range Env.empty typ with
       | None -> assert false (* Checked if range type in guard *)
       | Some (kids, constr, n, m) ->
          let ctx = { ctx with local_env = add_existential Parse_ast.Unknown (List.map (mk_kopt K_int) kids) constr ctx.local_env } in
          match nexp_simp n, nexp_simp m with
          | Nexp_aux (Nexp_constant n, _), Nexp_aux (Nexp_constant m, _)
               when n = m ->
             CT_constant n
          | Nexp_aux (Nexp_constant n, _), Nexp_aux (Nexp_constant m, _)
               when Big_int.less_equal (min_int 64) n && Big_int.less_equal m (max_int 64) ->
             CT_fint 64
          | n, m ->
             if prove __POS__ ctx.local_env (nc_lteq (nconstant (min_int 64)) n) && prove __POS__ ctx.local_env (nc_lteq m (nconstant (max_int 64))) then
               CT_fint 64
             else
               CT_lint
       end

    | Typ_app (id, [A_aux (A_typ typ, _)]) when string_of_id id = "list" ->
       CT_list (convert_typ ctx typ)

    (* Note that we have to use lbits for zero-length bitvectors because they are not allowed by SMTLIB *)
    | Typ_app (id, [A_aux (A_nexp n, _); A_aux (A_order ord, _)])
         when string_of_id id = "bitvector"  ->
       let direction = match ord with Ord_aux (Ord_dec, _) -> true | Ord_aux (Ord_inc, _) -> false | _ -> assert false in
       begin match nexp_simp n with
       | Nexp_aux (Nexp_constant n, _) when Big_int.equal n Big_int.zero -> CT_lbits direction
       | Nexp_aux (Nexp_constant n, _) -> CT_fbits (Big_int.to_int n, direction)
       | _ -> CT_lbits direction
       end

    | Typ_app (id, [A_aux (A_nexp n, _);
                    A_aux (A_order ord, _);
                    A_aux (A_typ typ, _)])
         when string_of_id id = "vector" ->
       let direction = match ord with Ord_aux (Ord_dec, _) -> true | Ord_aux (Ord_inc, _) -> false | _ -> assert false in
       CT_vector (direction, convert_typ ctx typ)

    | Typ_app (id, [A_aux (A_typ typ, _)]) when string_of_id id = "register" ->
       CT_ref (convert_typ ctx typ)

    | Typ_id id | Typ_app (id, _) when Bindings.mem id ctx.records  -> CT_struct (id, Bindings.find id ctx.records |> UBindings.bindings)
    | Typ_id id | Typ_app (id, _) when Bindings.mem id ctx.variants -> CT_variant (id, Bindings.find id ctx.variants |> UBindings.bindings)
    | Typ_id id when Bindings.mem id ctx.enums -> CT_enum (id, Bindings.find id ctx.enums |> IdSet.elements)

    | Typ_tup typs -> CT_tup (List.map (convert_typ ctx) typs)

    | Typ_exist _ ->
       (* Use Type_check.destruct_exist when optimising with SMT, to
          ensure that we don't cause any type variable clashes in
          local_env, and that we can optimize the existential based
          upon it's constraints. *)
       begin match destruct_exist (Env.expand_synonyms ctx.local_env typ) with
       | Some (kids, nc, typ) ->
          let env = add_existential l kids nc ctx.local_env in
          convert_typ { ctx with local_env = env } typ
       | None -> raise (Reporting.err_unreachable l __POS__ "Existential cannot be destructured!")
       end

    | Typ_var kid -> CT_poly

    | _ -> raise (Reporting.err_unreachable l __POS__ ("No SMT type for type " ^ string_of_typ typ))

  let hex_char =
    let open Sail2_values in
    function
    | '0' -> [B0; B0; B0; B0]
    | '1' -> [B0; B0; B0; B1]
    | '2' -> [B0; B0; B1; B0]
    | '3' -> [B0; B0; B1; B1]
    | '4' -> [B0; B1; B0; B0]
    | '5' -> [B0; B1; B0; B1]
    | '6' -> [B0; B1; B1; B0]
    | '7' -> [B0; B1; B1; B1]
    | '8' -> [B1; B0; B0; B0]
    | '9' -> [B1; B0; B0; B1]
    | 'A' | 'a' -> [B1; B0; B1; B0]
    | 'B' | 'b' -> [B1; B0; B1; B1]
    | 'C' | 'c' -> [B1; B1; B0; B0]
    | 'D' | 'd' -> [B1; B1; B0; B1]
    | 'E' | 'e' -> [B1; B1; B1; B0]
    | 'F' | 'f' -> [B1; B1; B1; B1]
    | _ -> failwith "Invalid hex character"

  let literal_to_cval (L_aux (l_aux, _) as lit) =
    match l_aux with
    | L_num n -> Some (V_lit (VL_int n, CT_constant n))
    | L_hex str when String.length str <= 16 ->
       let content = Util.string_to_list str |> List.map hex_char |> List.concat in
       Some (V_lit (VL_bits (content, true), CT_fbits (String.length str * 4, true)))
    | L_unit -> Some (V_lit (VL_unit, CT_unit))
    | L_true -> Some (V_lit (VL_bool true, CT_bool))
    | L_false -> Some (V_lit (VL_bool false, CT_bool))
    | _ -> None

  let c_literals ctx =
    let rec c_literal env l = function
      | AV_lit (lit, typ) as v ->
         begin match literal_to_cval lit with
         | Some cval -> AV_cval (cval, typ)
         | None -> v
         end
      | AV_tuple avals -> AV_tuple (List.map (c_literal env l) avals)
      | v -> v
    in
    map_aval c_literal

(* If we know the loop variables exactly (especially after
   specialization), we can unroll the exact number of times required,
   and omit any comparisons. *)
let unroll_static_foreach ctx = function
  | AE_aux (AE_for (id, from_aexp, to_aexp, by_aexp, order, body), env, l) as aexp ->
     begin match convert_typ ctx (aexp_typ from_aexp), convert_typ ctx (aexp_typ to_aexp), convert_typ ctx (aexp_typ by_aexp), order with
     | CT_constant f, CT_constant t, CT_constant b, Ord_aux (Ord_inc, _) ->
        let i = ref f in
        let unrolled = ref [] in
        while Big_int.less_equal !i t do
          let current_index = AE_aux (AE_val (AV_lit (L_aux (L_num !i, gen_loc l), atom_typ (nconstant !i))), env, gen_loc l) in
          let iteration = AE_aux (AE_let (Immutable, id, atom_typ (nconstant !i), current_index, body, unit_typ), env, gen_loc l) in
          unrolled := iteration :: !unrolled;
          i := Big_int.add !i b
        done;
        begin match !unrolled with
        | last :: iterations ->
           AE_aux (AE_block (List.rev iterations, last, unit_typ), env, gen_loc l)
        | [] -> AE_aux (AE_val (AV_lit (L_aux (L_unit, gen_loc l), unit_typ)), env, gen_loc l)
        end
     | _ -> aexp
     end
  | aexp -> aexp

  let optimize_anf ctx aexp =
    aexp
    |> c_literals ctx
    |> fold_aexp (unroll_static_foreach ctx)

  let specialize_calls = true
  let ignore_64 = true
  let unroll_loops = Some Opts.unroll_limit
  let struct_value = true
  let use_real = true
  let branch_coverage = None
  let track_throw = false
end


(**************************************************************************)
(* 3. Generating SMT                                                      *)
(**************************************************************************)

let push_smt_defs stack smt_defs =
  List.iter (fun def -> Stack.push def stack) smt_defs

(* When generating SMT when we encounter joins between two or more
   blocks such as in the example below, we have to generate a muxer
   that chooses the correct value of v_n or v_m to assign to v_o. We
   use the pi nodes that contain the path condition for each
   block to generate an if-then-else for each phi function. The order
   of the arguments to each phi function is based on the graph node
   index for the predecessor nodes.

   +---------------+      +---------------+
   | pi(cond_1)    |      | pi(cond_2)    |
   | ...           |      | ...           |
   | Basic block 1 |      | Basic block 2 |
   +---------------+      +---------------+
              \               /
               \             /
            +---------------------+
            | v/o = phi(v/n, v/m) |
            | ...                 |
            +---------------------+

   would generate:

   (define-const v/o (ite cond_1 v/n v/m_))
*)
let smt_ssanode ctx cfg preds =
  let open Jib_ssa in
  function
  | Pi _ -> []
  | Phi (id, ctyp, ids) ->
     let get_pi n =
       match get_vertex cfg n with
       | Some ((ssa_elems, _), _, _) ->
          List.concat (List.map (function Pi guards -> guards | _ -> []) ssa_elems)
       | None -> failwith "Predecessor node does not exist"
     in
     let pis = List.map get_pi (IntSet.elements preds) in
     let mux =
       List.fold_right2 (fun pi id chain ->
           let pathcond = smt_conj (List.map (smt_cval ctx) pi) in
           match chain with
           | Some smt ->
              Some (Ite (pathcond, Var (zencode_name id), smt))
           | None ->
              Some (Var (zencode_name id)))
         pis ids None
     in
     match mux with
     | None -> assert false
     | Some mux ->
        [Define_const (zencode_name id, smt_ctyp ctx ctyp, mux)]

(* The pi condition are computed by traversing the dominator tree,
   with each node having a pi condition defined as the conjunction of
   all guards between it and the start node in the dominator
   tree. This is imprecise because we have situations like:

      1
     / \
    2   3
    |   |
    |   4
    |   |\
    5   6 9
     \ /  |
      7   10
      |
      8

   where 8 = match_failure, 1 = start and 10 = return.
   2, 3, 6 and 9 are guards as they come directly after a control flow
   split, which always follows a conditional jump.

   Here the path through the dominator tree for the match_failure is
   1->7->8 which contains no guards so the pi condition would be empty.
   What we do now is walk backwards (CFG must be acyclic at this point)
   until we hit the join point prior to where we require a path
   condition. We then take the disjunction of the pi conditions for the
   join point's predecessors, so 5 and 6 in this case. Which gives us a
   path condition of 2 | (3 & 6) as the dominator chains are 1->2->5 and
   1->3->4->6.

   This should work as any split in the control flow must have been
   caused by a conditional jump followed by distinct guards, so each of
   the nodes immediately prior to a join point must be dominated by at
   least one unique guard. It also explains why the pi conditions are
   sufficient to choose outcomes of phi functions above.

   If we hit a guard before a join (such as 9 for return's path
   conditional) we just return the pi condition for that guard, i.e.
   (3 & 9) for 10. If we reach start then the path condition is simply
   true.
*)
let rec get_pathcond n cfg ctx =
  let open Jib_ssa in
  let get_pi m =
    match get_vertex cfg m with
    | Some ((ssa_elems, _), _, _) ->
       V_call (Band, List.concat (List.map (function Pi guards -> guards | _ -> []) ssa_elems))
    | None -> failwith "Node does not exist"
  in
  match get_vertex cfg n with
  | Some ((_, CF_guard cond), _, _) ->
     smt_cval ctx (get_pi n)
  | Some (_, preds, succs) ->
     if IntSet.cardinal preds = 0 then
       Bool_lit true
     else if IntSet.cardinal preds = 1 then
       get_pathcond (IntSet.min_elt preds) cfg ctx
     else
       let pis = List.map get_pi (IntSet.elements preds) in
       smt_cval ctx (V_call (Bor, pis))

  | None -> assert false (* Should never be called for a non-existent node *)

(* For any complex l-expression we need to turn it into a
   read-modify-write in the SMT solver. The SSA transform turns CL_id
   nodes into CL_rmw (read, write, ctyp) nodes when CL_id is wrapped
   in any other l-expression. The read and write must have the same
   name but different SSA numbers.
*)
let rec rmw_write = function
  | CL_rmw (_, write, ctyp) -> write, ctyp
  | CL_id _ -> assert false
  | CL_tuple (clexp, _) -> rmw_write clexp
  | CL_field (clexp, _) -> rmw_write clexp
  | clexp -> failwith "Could not understand l-expression"

let rmw_read = function
  | CL_rmw (read, _, _) -> zencode_name read
  | _ -> assert false

let rmw_modify smt = function
  | CL_tuple (clexp, n) ->
     let ctyp = clexp_ctyp clexp in
     begin match ctyp with
     | CT_tup ctyps ->
        let len = List.length ctyps in
        let set_tup i =
          if i == n then
            smt
          else
            Fn (Printf.sprintf "tup_%d_%d" len i, [Var (rmw_read clexp)])
        in
        Fn ("tup" ^ string_of_int len, List.init len set_tup)
     | _ ->
        failwith "Tuple modify does not have tuple type"
     end
  | CL_field (clexp, field) ->
     let ctyp = clexp_ctyp clexp in
     begin match ctyp with
     | CT_struct (struct_id, fields) ->
        let set_field (field', _) =
          if UId.compare field field' = 0 then
            smt
          else
            Field (zencode_upper_id struct_id ^ "_" ^ zencode_uid field', Var (rmw_read clexp))
        in
        Fn (zencode_upper_id struct_id, List.map set_field fields)
     | _ ->
        failwith "Struct modify does not have struct type"
     end
  | _ -> assert false

let smt_terminator ctx =
  let open Jib_ssa in
  function
  | T_end id ->
     add_event ctx Return (Var (zencode_name id));
     []

  | T_match_failure ->
     add_pathcond_event ctx Match;
     []

  | T_undefined _ | T_goto _ | T_jump _ | T_label _ | T_none -> []

(* For a basic block (contained in a control-flow node / cfnode), we
   turn the instructions into a sequence of define-const and
   declare-const expressions. Because we are working with a SSA graph,
   each variable is guaranteed to only be declared once.
*)
let smt_instr ctx =
  let open Type_check in
  function
  | I_aux (I_funcall (CL_id (id, ret_ctyp), extern, function_id, args), (_, l)) ->
     if Env.is_extern (fst function_id) ctx.tc_env "c" && not extern then
       let name = Env.get_extern (fst function_id) ctx.tc_env "c" in
       if name = "sqrt_real" then
         begin match args with
         | [v] -> builtin_sqrt_real ctx (zencode_name id) v
         | _ ->
            Reporting.unreachable l __POS__ "Bad arguments for sqrt_real"
         end
       (* See lib/regfp.sail *)
       else if name = "platform_write_mem" then
         begin match args with
         | [wk; addr_size; addr; data_size; data] ->
            let mem_event, var = builtin_write_mem l ctx wk addr_size addr data_size data in
            mem_event @ [define_const ctx id ret_ctyp var]
         | _ ->
            Reporting.unreachable l __POS__ "Bad arguments for __write_mem"
         end
       else if name = "platform_write_mem_ea" then
         begin match args with
         | [wk; addr_size; addr; data_size] ->
            let mem_event, var = builtin_write_mem_ea ctx wk addr_size addr data_size in
            mem_event @ [define_const ctx id ret_ctyp var]
         | _ ->
            Reporting.unreachable l __POS__ "Bad arguments for __write_mem_ea"
         end
       else if name = "platform_read_mem" then
         begin match args with
         | [rk; addr_size; addr; data_size] ->
            let mem_event, var = builtin_read_mem l ctx rk addr_size addr data_size ret_ctyp in
            mem_event @ [define_const ctx id ret_ctyp var]
         | _ ->
            Reporting.unreachable l __POS__ "Bad arguments for __read_mem"
         end
       else if name = "platform_barrier" then
         begin match args with
         | [bk] ->
            let mem_event, var = builtin_barrier l ctx bk in
            mem_event @ [define_const ctx id ret_ctyp var]
         | _ ->
            Reporting.unreachable l __POS__ "Bad arguments for __barrier"
         end
       else if name = "platform_cache_maintenance" then
         begin match args with
         | [cmk; addr_size; addr] ->
            let mem_event, var = builtin_cache_maintenance l ctx cmk addr_size addr in
            mem_event @ [define_const ctx id ret_ctyp var]
         | _ ->
            Reporting.unreachable l __POS__ "Bad arguments for __barrier"
         end
       else if name = "platform_branch_announce" then
         begin match args with
         | [addr_size; addr] ->
            let mem_event, var = builtin_branch_announce l ctx addr_size addr in
            mem_event @ [define_const ctx id ret_ctyp var]
         | _ ->
            Reporting.unreachable l __POS__ "Bad arguments for __barrier"
         end
       else if name = "platform_excl_res" then
         begin match args with
         | [_] ->
            let mem_event, var = builtin_excl_res ctx in
            mem_event @ [define_const ctx id ret_ctyp var]
         | _ ->
            Reporting.unreachable l __POS__ "Bad arguments for __excl_res"
         end
       else if name = "sail_exit" then
         (add_event ctx Assertion (Bool_lit false); [])
       else if name = "sail_assert" then
         begin match args with
         | [assertion; _] ->
            let smt = smt_cval ctx assertion in
            add_event ctx Assertion (Fn ("not", [smt]));
            []
         | _ ->
            Reporting.unreachable l __POS__ "Bad arguments for assertion"
         end
       else
         let value = smt_builtin ctx name args ret_ctyp in
         [define_const ctx id ret_ctyp (Syntactic (value, List.map (smt_cval ctx) args))]
     else if extern && string_of_id (fst function_id) = "internal_vector_init" then
       [declare_const ctx id ret_ctyp]
     else if extern && string_of_id (fst function_id) = "internal_vector_update" then
       begin match args with
       | [vec; i; x] ->
          let sz = int_size ctx (cval_ctyp i) in
          [define_const ctx id ret_ctyp
             (Fn ("store", [smt_cval ctx vec; force_size ~checked:false ctx ctx.vector_index sz (smt_cval ctx i); smt_cval ctx x]))]
       | _ ->
          Reporting.unreachable l __POS__ "Bad arguments for internal_vector_update"
       end
     else if (string_of_id (fst function_id) = "update_fbits"
              || string_of_id (fst function_id) = "update_lbits") && extern then
       begin match args with
       | [vec; i; x] ->
          [define_const ctx id ret_ctyp (builtin_vector_update ctx vec i x ret_ctyp)]
       | _ ->
          Reporting.unreachable l __POS__ "Bad arguments for update_{f,l}bits"
       end
     else if string_of_id (fst function_id) = "sail_assume" then
       begin match args with
       | [assumption] ->
          let smt = smt_cval ctx assumption in
          add_event ctx Assumption smt;
          []
       | _ ->
          Reporting.unreachable l __POS__ "Bad arguments for assumption"
       end
     else if not extern then
       let smt_args = List.map (smt_cval ctx) args in
       [define_const ctx id ret_ctyp (Ctor (zencode_uid function_id, smt_args))]
     else
       failwith ("Unrecognised function " ^ string_of_uid function_id)

  | I_aux (I_copy (CL_addr (CL_id (_, _)), _), (_, l)) ->
     Reporting.unreachable l __POS__ "Register reference write should be re-written by now"

  | I_aux (I_init (ctyp, id, cval), _) | I_aux (I_copy (CL_id (id, ctyp), cval), _) ->
     begin match id, cval with
     | (Name (id, _) | Global (id, _)), _ when IdSet.mem id ctx.preserved ->
        [preserve_const ctx id ctyp
           (smt_conversion ctx (cval_ctyp cval) ctyp (smt_cval ctx cval))]
     | _, V_lit (VL_undefined, _) ->
        (* Declare undefined variables as arbitrary but fixed *)
        [declare_const ctx id ctyp]
     | _, _ ->
        [define_const ctx id ctyp
           (smt_conversion ctx (cval_ctyp cval) ctyp (smt_cval ctx cval))]
     end

  | I_aux (I_copy (clexp, cval), _) ->
     let smt = smt_cval ctx cval in
     let write, ctyp = rmw_write clexp in
     [define_const ctx write ctyp (rmw_modify smt clexp)]

  | I_aux (I_decl (ctyp, id), (_, l)) ->
     (* Function arguments have unique locations defined from the
        $property pragma. We record how they will appear in the
        generated SMT so we can check models. *)
     begin match l with
     | Unique (n, l') when l' = ctx.pragma_l ->
        Stack.push (n, zencode_name id) ctx.arg_stack
     | _ -> ()
     end;
     [declare_const ctx id ctyp]

  | I_aux (I_clear _, _) -> []

  (* Should only appear as terminators for basic blocks. *)
  | I_aux ((I_jump _ | I_goto _ | I_end _ | I_match_failure | I_undefined _), (_, l)) ->
     Reporting.unreachable l __POS__ "SMT: Instruction should only appear as block terminator"

  | I_aux (_, (_, l)) ->
     Reporting.unreachable l __POS__ "Cannot translate instruction"

let smt_cfnode all_cdefs ctx ssa_elems =
  let open Jib_ssa in
  function
  | CF_start inits ->
     let smt_reg_decs = generate_reg_decs ctx inits all_cdefs in
     let smt_start (id, ctyp) =
       match id with
       | Have_exception _ -> define_const ctx id ctyp (Bool_lit false)
       | _ -> declare_const ctx id ctyp
     in
     smt_reg_decs @ List.map smt_start (NameMap.bindings inits)
  | CF_block (instrs, terminator) ->
     let smt_instrs = List.map (smt_instr ctx) instrs in
     let smt_term = smt_terminator ctx terminator in
     List.concat (smt_instrs @ [smt_term])
  (* We can ignore any non basic-block/start control-flow nodes *)
  | _ -> []

(** When we generate a property for a CDEF_spec, we find it's
   associated function body in a CDEF_fundef node. However, we must
   keep track of any global letbindings between the spec and the
   fundef, so they can appear in the generated SMT. *)
let rec find_function lets id = function
  | CDEF_fundef (id', heap_return, args, body) :: _ when Id.compare id id' = 0 ->
     lets, Some (heap_return, args, body)
  | CDEF_let (_, vars, setup) :: cdefs ->
     let vars = List.map (fun (id, ctyp) -> idecl (id_loc id) ctyp (global id)) vars in
     find_function (lets @ vars @ setup) id cdefs;
  | _ :: cdefs ->
     find_function lets id cdefs
  | [] -> lets, None

module type Sequence = sig
  type 'a t
  val create : unit -> 'a t
  val add : 'a -> 'a t -> unit
end

module Make_optimizer(S : Sequence) = struct

  let optimize stack =
    let stack' = Stack.create () in
    let uses = Hashtbl.create (Stack.length stack) in

    let rec uses_in_exp = function
      | Var var ->
         begin match Hashtbl.find_opt uses var with
         | Some n -> Hashtbl.replace uses var (n + 1)
         | None -> Hashtbl.add uses var 1
         end
      | Syntactic (exp, _) -> uses_in_exp exp
      | Shared _ | Enum _ | Read_res _ | Bitvec_lit _ | Bool_lit _ | String_lit _ | Real_lit _ -> ()
      | Fn (_, exps) | Ctor (_, exps) ->
         List.iter uses_in_exp exps
      | Field (_, exp) ->
         uses_in_exp exp
      | Struct (_, fields) ->
         List.iter (fun (_, exp) -> uses_in_exp exp) fields
      | Ite (cond, t, e) ->
         uses_in_exp cond; uses_in_exp t; uses_in_exp e
      | Extract (_, _, exp) | Tester (_, exp) | SignExtend (_, exp) ->
         uses_in_exp exp
      | Forall _ -> assert false
    in

    let remove_unused () = function
      | Declare_const (var, _) as def ->
         begin match Hashtbl.find_opt uses var with
         | None -> ()
         | Some _ ->
            Stack.push def stack'
         end
      | Declare_fun _ as def ->
         Stack.push def stack'
      | Preserve_const (_, _, exp) as def ->
         uses_in_exp exp;
         Stack.push def stack'
      | Define_const (var, _, exp) as def ->
         begin match Hashtbl.find_opt uses var with
         | None -> ()
         | Some _ ->
            uses_in_exp exp;
            Stack.push def stack'
         end
      | (Declare_datatypes _ | Declare_tuple _) as def ->
         Stack.push def stack'
      | Write_mem w as def ->
         uses_in_exp w.active; uses_in_exp w.kind; uses_in_exp w.addr; uses_in_exp w.data;
         Stack.push def stack'
      | Write_mem_ea (_, _, active, wk, addr, _, data_size, _) as def ->
         uses_in_exp active; uses_in_exp wk; uses_in_exp addr; uses_in_exp data_size;
         Stack.push def stack'
      | Read_mem r as def ->
         uses_in_exp r.active; uses_in_exp r.kind; uses_in_exp r.addr;
         Stack.push def stack'
      | Barrier b as def ->
         uses_in_exp b.active; uses_in_exp b.kind;
         Stack.push def stack'
      | Cache_maintenance m as def ->
         uses_in_exp m.active; uses_in_exp m.kind; uses_in_exp m.addr;
         Stack.push def stack'
      | Branch_announce c as def ->
         uses_in_exp c.active; uses_in_exp c.addr;
         Stack.push def stack'
      | Excl_res (_, _, active) as def ->
         uses_in_exp active;
         Stack.push def stack'
      | Assert exp as def ->
         uses_in_exp exp;
         Stack.push def stack'
      | Define_fun _ -> assert false
    in
    Stack.fold remove_unused () stack;

    let vars = Hashtbl.create (Stack.length stack') in
    let kinds = Hashtbl.create (Stack.length stack') in
    let seq = S.create () in

    let constant_propagate = function
      | Declare_const _ as def ->
         S.add def seq
      | Declare_fun _ as def ->
         S.add def seq
      | Preserve_const (var, typ, exp) ->
         S.add (Preserve_const (var, typ, simp_smt_exp vars kinds exp)) seq
      | Define_const (var, typ, exp) ->
         let exp = simp_smt_exp vars kinds exp in
         begin match Hashtbl.find_opt uses var, simp_smt_exp vars kinds exp with
         | _, (Bitvec_lit _ | Bool_lit _) ->
            Hashtbl.add vars var exp
         | _, Var _ when !opt_propagate_vars ->
            Hashtbl.add vars var exp
         | _, (Ctor (str, _)) ->
            Hashtbl.add kinds var str;
            S.add (Define_const (var, typ, exp)) seq
         | Some 1, _ ->
            Hashtbl.add vars var exp
         | Some _, exp ->
            S.add (Define_const (var, typ, exp)) seq
         | None, _ -> assert false
         end
      | Write_mem w ->
         S.add (Write_mem { w with active = simp_smt_exp vars kinds w.active;
                                   kind = simp_smt_exp vars kinds w.kind;
                                   addr = simp_smt_exp vars kinds w.addr;
                                   data = simp_smt_exp vars kinds w.data })
               seq
      | Write_mem_ea (name, node, active, wk, addr, addr_ty, data_size, data_size_ty) ->
         S.add (Write_mem_ea (name, node, simp_smt_exp vars kinds active, simp_smt_exp vars kinds wk,
                              simp_smt_exp vars kinds addr, addr_ty, simp_smt_exp vars kinds data_size, data_size_ty))
               seq
      | Read_mem r ->
         S.add (Read_mem { r with active = simp_smt_exp vars kinds r.active;
                                  kind = simp_smt_exp vars kinds r.kind;
                                  addr = simp_smt_exp vars kinds r.addr })
               seq
      | Barrier b ->
         S.add (Barrier { b with active = simp_smt_exp vars kinds b.active; kind = simp_smt_exp vars kinds b.kind }) seq
      | Cache_maintenance m ->
         S.add (Cache_maintenance { m with active = simp_smt_exp vars kinds m.active;
                                           kind = simp_smt_exp vars kinds m.kind;
                                           addr = simp_smt_exp vars kinds m.addr })
               seq
      | Branch_announce c ->
         S.add (Branch_announce { c with active = simp_smt_exp vars kinds c.active; addr = simp_smt_exp vars kinds c.addr }) seq
      | Excl_res (name, node, active) ->
         S.add (Excl_res (name, node, simp_smt_exp vars kinds active)) seq
      | Assert exp ->
         S.add (Assert (simp_smt_exp vars kinds exp)) seq
      | (Declare_datatypes _ | Declare_tuple _) as def ->
         S.add def seq
      | Define_fun _ -> assert false
    in
    Stack.iter constant_propagate stack';
    seq

end

module Queue_optimizer =
  Make_optimizer(struct
    type 'a t = 'a Queue.t
    let create = Queue.create
    let add = Queue.add
    let iter = Queue.iter
  end)

(** [smt_header ctx cdefs] produces a list of smt definitions for all the datatypes in a specification *)
let smt_header ctx cdefs =
  let smt_ctype_defs = List.concat (generate_ctype_defs ctx cdefs) in
  [declare_datatypes (mk_enum "Unit" ["unit"])]
  @ (IntSet.elements !(ctx.tuple_sizes) |> List.map (fun n -> Declare_tuple n))
  @ [declare_datatypes (mk_record "Bits" [("len", Bitvec ctx.lbits_index);
                                          ("contents", Bitvec (lbits_size ctx))])

    ]
  @ smt_ctype_defs

(* For generating SMT when we have a reg_deref(r : register(t))
   function, we have to expand it into a if-then-else cascade that
   checks if r is any one of the registers with type t, and reads that
   register if it is. We also do a similar thing for *r = x
*)
let expand_reg_deref env register_map = function
  | I_aux (I_funcall (CL_addr (CL_id (id, ctyp)), false, function_id, args), (_, l)) ->
     begin match ctyp with
     | CT_ref reg_ctyp ->
        begin match CTMap.find_opt reg_ctyp register_map with
        | Some regs ->
           let end_label = label "end_reg_write_" in
           let try_reg r =
             let next_label = label "next_reg_write_" in
             [ijump l (V_call (Neq, [V_lit (VL_ref (string_of_id r), reg_ctyp); V_id (id, ctyp)])) next_label;
              ifuncall l (CL_id (global r, reg_ctyp)) function_id args;
              igoto end_label;
              ilabel next_label]
           in
           iblock (List.concat (List.map try_reg regs) @ [ilabel end_label])
        | None ->
           raise (Reporting.err_general l ("Could not find any registers with type " ^ string_of_ctyp reg_ctyp))
        end
     | _ ->
        raise (Reporting.err_general l "Register reference assignment must take a register reference as an argument")
     end
  | I_aux (I_funcall (clexp, false, function_id, [reg_ref]), (_, l)) as instr ->
     let open Type_check in
     begin match (if Env.is_extern (fst function_id) env "smt" then Some (Env.get_extern (fst function_id) env "smt") else None) with
     | Some "reg_deref" ->
        begin match cval_ctyp reg_ref with
        | CT_ref reg_ctyp ->
           (* Not find all the registers with this ctyp *)
           begin match CTMap.find_opt reg_ctyp register_map with
           | Some regs ->
              let end_label = label "end_reg_deref_" in
              let try_reg r =
                let next_label = label "next_reg_deref_" in
                [ijump l (V_call (Neq, [V_lit (VL_ref (string_of_id r), reg_ctyp); reg_ref])) next_label;
                 icopy l clexp (V_id (global r, reg_ctyp));
                 igoto end_label;
                 ilabel next_label]
              in
              iblock (List.concat (List.map try_reg regs) @ [ilabel end_label])
           | None ->
              raise (Reporting.err_general l ("Could not find any registers with type " ^ string_of_ctyp reg_ctyp))
           end
        | _ ->
           raise (Reporting.err_general l "Register dereference must have a register reference as an argument")
        end
     | _ -> instr
     end
  | I_aux (I_copy (CL_addr (CL_id (id, ctyp)), cval), (_, l)) ->
     begin match ctyp with
     | CT_ref reg_ctyp ->
        begin match CTMap.find_opt reg_ctyp register_map with
        | Some regs ->
           let end_label = label "end_reg_write_" in
           let try_reg r =
             let next_label = label "next_reg_write_" in
             [ijump l (V_call (Neq, [V_lit (VL_ref (string_of_id r), reg_ctyp); V_id (id, ctyp)])) next_label;
              icopy l (CL_id (global r, reg_ctyp)) cval;
              igoto end_label;
              ilabel next_label]
           in
           iblock (List.concat (List.map try_reg regs) @ [ilabel end_label])
        | None ->
           raise (Reporting.err_general l ("Could not find any registers with type " ^ string_of_ctyp reg_ctyp))
        end
     | _ ->
        raise (Reporting.err_general l "Register reference assignment must take a register reference as an argument")
     end
  | instr -> instr

let rec smt_query ctx = function
  | Q_all ev ->
     let stack = event_stack ctx ev in
     smt_conj (Stack.fold (fun xs x -> x :: xs) [] stack)
  | Q_exist ev ->
     let stack = event_stack ctx ev in
     smt_disj (Stack.fold (fun xs x -> x :: xs) [] stack)
  | Q_not q ->
     Fn ("not", [smt_query ctx q])
  | Q_and qs ->
     Fn ("and", List.map (smt_query ctx) qs)
  | Q_or qs ->
     Fn ("or", List.map (smt_query ctx) qs)

let dump_graph name cfg =
  let gv_file = name ^ ".gv" in
  let out_chan = open_out gv_file in
  Jib_ssa.make_dot out_chan cfg;
  close_out out_chan

let smt_instr_list name ctx all_cdefs instrs =
  let stack = Stack.create () in

  let open Jib_ssa in
  let start, cfg = ssa instrs in
  let visit_order =
    try topsort cfg with
    | Not_a_DAG n ->
       dump_graph name cfg;
       raise (Reporting.err_general ctx.pragma_l
               (Printf.sprintf "%s: control flow graph is not acyclic (node %d is in cycle)\nWrote graph to %s.gv" name n name))
  in
  if !opt_debug_graphs then
    dump_graph name cfg;

  List.iter (fun n ->
      match get_vertex cfg n with
      | None -> ()
      | Some ((ssa_elems, cfnode), preds, succs) ->
         let muxers =
           ssa_elems |> List.map (smt_ssanode ctx cfg preds) |> List.concat
         in
         let ctx = { ctx with node = n; pathcond = lazy (get_pathcond n cfg ctx) } in
         let basic_block = smt_cfnode all_cdefs ctx ssa_elems cfnode in
         push_smt_defs stack muxers;
         push_smt_defs stack basic_block
    ) visit_order;

  stack, start, cfg

let smt_cdef props lets name_file ctx all_cdefs = function
  | CDEF_spec (function_id, _, arg_ctyps, ret_ctyp) when Bindings.mem function_id props ->
     begin match find_function [] function_id all_cdefs with
     | intervening_lets, Some (None, args, instrs) ->
        let prop_type, prop_args, pragma_l, vs = Bindings.find function_id props in

        let pragma = parse_pragma pragma_l prop_args in

        let ctx = { ctx with events = ref EventMap.empty; pragma_l = pragma_l; arg_stack = Stack.create () } in

        (* When we create each argument declaration, give it a unique
           location from the $property pragma, so we can identify it later. *)
        let arg_decls =
          List.map2 (fun id ctyp -> let l = unique pragma_l in idecl l ctyp (name id)) args arg_ctyps
        in
        let instrs =
          let open Jib_optimize in
          (lets @ intervening_lets @ arg_decls @ instrs)
          |> inline all_cdefs (fun _ -> true)
          |> List.map (map_instr (expand_reg_deref ctx.tc_env ctx.register_map))
          |> flatten_instrs
          |> remove_unused_labels
          |> remove_pointless_goto
        in

        let stack, _, _ = smt_instr_list (string_of_id function_id) ctx all_cdefs instrs in

        let query = smt_query ctx pragma.query in
        push_smt_defs stack [Assert (Fn ("not", [query]))];

        let fname = name_file (string_of_id function_id) in
        let out_chan = open_out fname in
        if prop_type = "counterexample" then
          output_string out_chan "(set-option :produce-models true)\n";

        let header = smt_header ctx all_cdefs in

        if !(ctx.use_string) || !(ctx.use_real) then
          output_string out_chan "(set-logic ALL)\n"
        else
          output_string out_chan "(set-logic QF_AUFBVDT)\n";

        List.iter (fun def -> output_string out_chan (string_of_smt_def def); output_string out_chan "\n") header;

        let queue = Queue_optimizer.optimize stack in
        Queue.iter (fun def -> output_string out_chan (string_of_smt_def def); output_string out_chan "\n") queue;

        output_string out_chan "(check-sat)\n";
        if prop_type = "counterexample" then
          output_string out_chan "(get-model)\n";

        close_out out_chan;
        if prop_type = "counterexample" && !opt_auto then (
          let arg_names = Stack.fold (fun m (k, v) -> (k, v) :: m) [] ctx.arg_stack in
          let arg_smt_names =
            List.map (function
                | (I_aux (I_decl (_, Name (id, _)), (_, Unique (n, _)))) ->
                   (id, List.assoc_opt n arg_names)
                | _ -> assert false
              ) arg_decls
          in
          check_counterexample ctx.ast ctx.tc_env fname function_id args arg_ctyps arg_smt_names
        );

     | _ -> failwith "Bad function body"
     end
  | _ -> ()

let rec smt_cdefs props lets name_file ctx ast =
  function
  | CDEF_let (_, vars, setup) :: cdefs ->
     let vars = List.map (fun (id, ctyp) -> idecl (id_loc id) ctyp (global id)) vars in
     smt_cdefs props (lets @ vars @ setup) name_file ctx ast cdefs;
  | cdef :: cdefs ->
     smt_cdef props lets name_file ctx ast cdef;
     smt_cdefs props lets name_file ctx ast cdefs
  | [] -> ()

(* In order to support register references, we need to build a map
   from each ctyp to a list of registers with that ctyp, then when we
   see a type like register(bits(32)) we can use the map to figure out
   all the registers that such a reference could be pointing to.
*)
let rec build_register_map rmap = function
  | CDEF_reg_dec (reg, ctyp, _) :: cdefs ->
     let rmap = match CTMap.find_opt ctyp rmap with
       | Some regs ->
          CTMap.add ctyp (reg :: regs) rmap
       | None ->
          CTMap.add ctyp [reg] rmap
     in
     build_register_map rmap cdefs
  | _ :: cdefs -> build_register_map rmap cdefs
  | [] -> rmap

let compile env ast =
  let cdefs, jib_ctx =
    let module Jibc = Jib_compile.Make(SMT_config(struct let unroll_limit = !opt_unroll_limit end)) in
    let ctx = Jib_compile.(initial_ctx (add_special_functions env)) in
    let t = Profile.start () in
    let cdefs, ctx = Jibc.compile_ast ctx ast in
    Profile.finish "Compiling to Jib IR" t;
    cdefs, ctx
  in
  let cdefs = Jib_optimize.unique_per_function_ids cdefs in
  let rmap = build_register_map CTMap.empty cdefs in
  cdefs, jib_ctx, { (initial_ctx ()) with tc_env = jib_ctx.tc_env; register_map = rmap; ast = ast }

let serialize_smt_model file env ast =
  let cdefs, _, ctx = compile env ast in
  let out_chan = open_out file in
  Marshal.to_channel out_chan cdefs [];
  Marshal.to_channel out_chan (Type_check.Env.set_prover None ctx.tc_env) [];
  Marshal.to_channel out_chan ctx.register_map [];
  close_out out_chan

let deserialize_smt_model file =
  let in_chan = open_in file in
  let cdefs = (Marshal.from_channel in_chan : cdef list) in
  let env = (Marshal.from_channel in_chan : Type_check.env) in
  let rmap = (Marshal.from_channel in_chan : id list CTMap.t) in
  close_in in_chan;
  (cdefs, { (initial_ctx ()) with tc_env = env; register_map = rmap })

let generate_smt props name_file env ast =
  try
    let cdefs, _, ctx = compile env ast in
    smt_cdefs props [] name_file ctx cdefs cdefs
  with
  | Type_check.Type_error (_, l, err) ->
     raise (Reporting.err_typ l (Type_error.string_of_type_error err));