Merge branch 'sail2' of https://github.com/rems-project/sail into sail2

11 files changed, 1234 insertions, 906 deletions

diff --git a/src/jib/c_backend.ml b/src/jib/c_backend.ml
index 98ee5bc1..2b144d35 100644
--- a/src/jib/c_backend.ml
+++ b/src/jib/c_backend.ml
@@ -100,7 +100,9 @@ let zencode_uid (id, ctyps) =
   match ctyps with
   | [] -> Util.zencode_string (string_of_id id)
   | _ -> Util.zencode_string (string_of_id id ^ "#" ^ Util.string_of_list "_" string_of_ctyp ctyps)
-                              
+
+let ctor_bindings = List.fold_left (fun map (id, ctyp) -> UBindings.add id ctyp map) UBindings.empty
+
 (**************************************************************************)
 (* 2. Converting sail types to C types                                    *)
 (**************************************************************************)
@@ -108,90 +110,9 @@ let zencode_uid (id, ctyps) =
 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))
 
-(** 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 ctyp_of_typ ctx typ =
-  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" ->
-     ctyp_of_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 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 (ctyp_of_typ ctx typ)
-
-  (* When converting a sail bitvector type into C, we have three options in order of efficiency:
-     - If the length is obviously static and smaller than 64, use the fixed bits type (aka uint64_t), fbits.
-     - If the length is less than 64, then use a small bits type, sbits.
-     - If the length may be larger than 64, use a large bits type lbits. *)
-  | 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.less_equal n (Big_int.of_int 64) -> CT_fbits (Big_int.to_int n, direction)
-     | n when prove __POS__ ctx.local_env (nc_lteq n (nint 64)) -> CT_sbits (64, 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, ctyp_of_typ ctx typ)
-
-  | Typ_app (id, [A_aux (A_typ typ, _)]) when string_of_id id = "register" ->
-     CT_ref (ctyp_of_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 (ctyp_of_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
-        ctyp_of_typ { ctx with local_env = env } typ
-     | None -> raise (Reporting.err_unreachable l __POS__ "Existential cannot be destructured!")
-     end
-
-  | Typ_var kid -> CT_poly
-
-  | _ -> c_error ~loc:l ("No C type for type " ^ string_of_typ typ)
-
+(** This function is used to split types into those we allocate on the
+   stack, versus those which need to live on the heap, or otherwise
+   require some additional memory management *)
 let rec is_stack_ctyp ctyp = match ctyp with
   | CT_fbits _ | CT_sbits _ | CT_bit | CT_unit | CT_bool | CT_enum _ -> true
   | CT_fint n -> n <= 64
@@ -199,7 +120,7 @@ let rec is_stack_ctyp ctyp = match ctyp with
   | CT_lint -> false
   | CT_lbits _ when !optimize_fixed_bits -> true
   | CT_lbits _ -> false
-  | CT_real | CT_string | CT_list _ | CT_vector _ -> false
+  | CT_real | CT_string | CT_list _ | CT_vector _ | CT_fvector _ -> false
   | CT_struct (_, fields) -> List.for_all (fun (_, ctyp) -> is_stack_ctyp ctyp) fields
   | CT_variant (_, ctors) -> false (* List.for_all (fun (_, ctyp) -> is_stack_ctyp ctyp) ctors *) (* FIXME *)
   | CT_tup ctyps -> List.for_all is_stack_ctyp ctyps
@@ -207,346 +128,442 @@ let rec is_stack_ctyp ctyp = match ctyp with
   | CT_poly -> true
   | CT_constant n -> Big_int.less_equal (min_int 64) n && Big_int.greater_equal n (max_int 64)
 
-let is_stack_typ ctx typ = is_stack_ctyp (ctyp_of_typ ctx typ)
-
-let is_fbits_typ ctx typ =
-  match ctyp_of_typ ctx typ with
-  | CT_fbits _ -> true
-  | _ -> false
-
-let is_sbits_typ ctx typ =
-  match ctyp_of_typ ctx typ with
-  | CT_sbits _ -> true
-  | _ -> false
-
-let ctor_bindings = List.fold_left (fun map (id, ctyp) -> UBindings.add id ctyp map) UBindings.empty
-
-(**************************************************************************)
-(* 3. Optimization of primitives and literals                             *)
-(**************************************************************************)
-
-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_fragment (L_aux (l_aux, _) as lit) =
-  match l_aux with
-  | L_num n when Big_int.less_equal (min_int 64) n && Big_int.less_equal n (max_int 64) ->
-     Some (V_lit (VL_int n, CT_fint 64))
-  | L_hex str when String.length str <= 16 ->
-     let padding = 16 - String.length str in
-     let padding = Util.list_init padding (fun _ -> Sail2_values.B0) in
-     let content = Util.string_to_list str |> List.map hex_char |> List.concat in
-     Some (V_lit (VL_bits (padding @ 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 when is_stack_ctyp (ctyp_of_typ { ctx with local_env = env } typ) ->
-       begin
-         match literal_to_fragment 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
-
-let rec is_bitvector = function
-  | [] -> true
-  | AV_lit (L_aux (L_zero, _), _) :: avals -> is_bitvector avals
-  | AV_lit (L_aux (L_one, _), _) :: avals -> is_bitvector avals
-  | _ :: _ -> false
-
-let rec value_of_aval_bit = function
-  | AV_lit (L_aux (L_zero, _), _) -> Sail2_values.B0
-  | AV_lit (L_aux (L_one, _), _) -> Sail2_values.B1
-  | _ -> assert false
-
-(** Used to make sure the -Ofixed_int and -Ofixed_bits don't interfere
-   with assumptions made about optimizations in the common case. *)
-let rec never_optimize = function
-  | CT_lbits _ | CT_lint -> true
-  | _ -> false
-
-let rec c_aval ctx = function
-  | AV_lit (lit, typ) as v ->
-     begin
-       match literal_to_fragment lit with
-       | Some cval -> AV_cval (cval, typ)
-       | None -> v
-     end
-  | AV_cval (cval, typ) -> AV_cval (cval, typ)
-  (* An id can be converted to a C fragment if it's type can be
-     stack-allocated. *)
-  | AV_id (id, lvar) as v ->
-     begin
-       match lvar with
-       | Local (_, typ) ->
-          let ctyp = ctyp_of_typ ctx typ in
-          if is_stack_ctyp ctyp && not (never_optimize ctyp) then
-            begin
-              try
-                (* We need to check that id's type hasn't changed due to flow typing *)
-                let _, ctyp' = Bindings.find id ctx.locals in
-                if ctyp_equal ctyp ctyp' then
-                  AV_cval (V_id (name id, ctyp), typ)
-                else
-                  (* id's type changed due to flow
-                     typing, so it's really still heap allocated!  *)
-                  v
-              with
-                (* Hack: Assuming global letbindings don't change from flow typing... *)
-                Not_found -> AV_cval (V_id (name id, ctyp), typ)
-            end
-          else
-            v
-       | Register (_, _, typ) ->
-          let ctyp = ctyp_of_typ ctx typ in
-          if is_stack_ctyp ctyp && not (never_optimize ctyp) then
-            AV_cval (V_id (name id, ctyp), typ)
-          else
-            v
-       | _ -> v
-     end
-  | AV_vector (v, typ) when is_bitvector v && List.length v <= 64 ->
-     let bitstring = VL_bits (List.map value_of_aval_bit v, true) in
-     AV_cval (V_lit (bitstring, CT_fbits (List.length v, true)), typ)
-  | AV_tuple avals -> AV_tuple (List.map (c_aval ctx) avals)
-  | aval -> aval
-
-let c_fragment = function
-  | AV_cval (cval, _) -> cval
-  | _ -> assert false
-
 let v_mask_lower i = V_lit (VL_bits (Util.list_init i (fun _ -> Sail2_values.B1), true), CT_fbits (i, true))
 
-(* Map over all the functions in an aexp. *)
-let rec analyze_functions ctx f (AE_aux (aexp, env, l)) =
-  let ctx = { ctx with local_env = env } in
-  let aexp = match aexp with
-    | AE_app (id, vs, typ) -> f ctx id vs typ
+module C_config : Config = struct
 
-    | AE_cast (aexp, typ) -> AE_cast (analyze_functions ctx f aexp, typ)
+(** 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 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 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
 
-    | AE_assign (id, typ, aexp) -> AE_assign (id, typ, analyze_functions ctx f aexp)
+    | Typ_app (id, [A_aux (A_typ typ, _)]) when string_of_id id = "list" ->
+       CT_list (convert_typ ctx typ)
+
+    (* When converting a sail bitvector type into C, we have three options in order of efficiency:
+       - If the length is obviously static and smaller than 64, use the fixed bits type (aka uint64_t), fbits.
+       - If the length is less than 64, then use a small bits type, sbits.
+       - If the length may be larger than 64, use a large bits type lbits. *)
+    | 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.less_equal n (Big_int.of_int 64) -> CT_fbits (Big_int.to_int n, direction)
+       | n when prove __POS__ ctx.local_env (nc_lteq n (nint 64)) -> CT_sbits (64, direction)
+       | _ -> CT_lbits direction
+       end
 
-    | AE_write_ref (id, typ, aexp) -> AE_write_ref (id, typ, analyze_functions ctx f aexp)
+    | 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
 
-    | AE_short_circuit (op, aval, aexp) -> AE_short_circuit (op, aval, analyze_functions ctx f aexp)
+    | Typ_var kid -> CT_poly
 
-    | AE_let (mut, id, typ1, aexp1, (AE_aux (_, env2, _) as aexp2), typ2) ->
-       let aexp1 = analyze_functions ctx f aexp1 in
-       (* Use aexp2's environment because it will contain constraints for id *)
-       let ctyp1 = ctyp_of_typ { ctx with local_env = env2 } typ1 in
-       let ctx = { ctx with locals = Bindings.add id (mut, ctyp1) ctx.locals } in
-       AE_let (mut, id, typ1, aexp1, analyze_functions ctx f aexp2, typ2)
+    | _ -> c_error ~loc:l ("No C type for type " ^ string_of_typ typ)
 
-    | AE_block (aexps, aexp, typ) -> AE_block (List.map (analyze_functions ctx f) aexps, analyze_functions ctx f aexp, typ)
+  let is_stack_typ ctx typ = is_stack_ctyp (convert_typ ctx typ)
 
-    | AE_if (aval, aexp1, aexp2, typ) ->
-       AE_if (aval, analyze_functions ctx f aexp1, analyze_functions ctx f aexp2, typ)
+  let is_fbits_typ ctx typ =
+    match convert_typ ctx typ with
+    | CT_fbits _ -> true
+    | _ -> false
 
-    | AE_loop (loop_typ, aexp1, aexp2) -> AE_loop (loop_typ, analyze_functions ctx f aexp1, analyze_functions ctx f aexp2)
+  let is_sbits_typ ctx typ =
+    match convert_typ ctx typ with
+    | CT_sbits _ -> true
+    | _ -> false
 
-    | AE_for (id, aexp1, aexp2, aexp3, order, aexp4) ->
-       let aexp1 = analyze_functions ctx f aexp1 in
-       let aexp2 = analyze_functions ctx f aexp2 in
-       let aexp3 = analyze_functions ctx f aexp3 in
-       let aexp4 = analyze_functions ctx f aexp4 in
-       (* Currently we assume that loop indexes are always safe to put into an int64 *)
-       let ctx = { ctx with locals = Bindings.add id (Immutable, CT_fint 64) ctx.locals } in
-       AE_for (id, aexp1, aexp2, aexp3, order, aexp4)
+  (**************************************************************************)
+  (* 3. Optimization of primitives and literals                             *)
+  (**************************************************************************)
+
+  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_fragment (L_aux (l_aux, _) as lit) =
+    match l_aux with
+    | L_num n when Big_int.less_equal (min_int 64) n && Big_int.less_equal n (max_int 64) ->
+       Some (V_lit (VL_int n, CT_fint 64))
+    | L_hex str when String.length str <= 16 ->
+       let padding = 16 - String.length str in
+       let padding = Util.list_init padding (fun _ -> Sail2_values.B0) in
+       let content = Util.string_to_list str |> List.map hex_char |> List.concat in
+       Some (V_lit (VL_bits (padding @ 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 when is_stack_ctyp (convert_typ { ctx with local_env = env } typ) ->
+         begin
+           match literal_to_fragment 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
+
+  let rec is_bitvector = function
+    | [] -> true
+    | AV_lit (L_aux (L_zero, _), _) :: avals -> is_bitvector avals
+    | AV_lit (L_aux (L_one, _), _) :: avals -> is_bitvector avals
+    | _ :: _ -> false
+
+  let rec value_of_aval_bit = function
+    | AV_lit (L_aux (L_zero, _), _) -> Sail2_values.B0
+    | AV_lit (L_aux (L_one, _), _) -> Sail2_values.B1
+    | _ -> assert false
+
+  (** Used to make sure the -Ofixed_int and -Ofixed_bits don't
+     interfere with assumptions made about optimizations in the common
+     case. *)
+  let rec never_optimize = function
+    | CT_lbits _ | CT_lint -> true
+    | _ -> false
 
-    | AE_case (aval, cases, typ) ->
-       let analyze_case (AP_aux (_, env, _) as pat, aexp1, aexp2) =
-         let pat_bindings = Bindings.bindings (apat_types pat) in
-         let ctx = { ctx with local_env = env } in
-         let ctx =
-           List.fold_left (fun ctx (id, typ) -> { ctx with locals = Bindings.add id (Immutable, ctyp_of_typ ctx typ) ctx.locals }) ctx pat_bindings
+  let rec c_aval ctx = function
+    | AV_lit (lit, typ) as v ->
+       begin
+         match literal_to_fragment lit with
+         | Some cval -> AV_cval (cval, typ)
+         | None -> v
+       end
+    | AV_cval (cval, typ) -> AV_cval (cval, typ)
+    (* An id can be converted to a C fragment if it's type can be
+     stack-allocated. *)
+    | AV_id (id, lvar) as v ->
+       begin
+         match lvar with
+         | Local (_, typ) ->
+            let ctyp = convert_typ ctx typ in
+            if is_stack_ctyp ctyp && not (never_optimize ctyp) then
+              begin
+                try
+                  (* We need to check that id's type hasn't changed due to flow typing *)
+                  let _, ctyp' = Bindings.find id ctx.locals in
+                  if ctyp_equal ctyp ctyp' then
+                    AV_cval (V_id (name id, ctyp), typ)
+                  else
+                    (* id's type changed due to flow typing, so it's
+                       really still heap allocated!  *)
+                    v
+                with
+                  (* Hack: Assuming global letbindings don't change from flow typing... *)
+                  Not_found -> AV_cval (V_id (name id, ctyp), typ)
+              end
+            else
+              v
+         | Register (_, _, typ) ->
+            let ctyp = convert_typ ctx typ in
+            if is_stack_ctyp ctyp && not (never_optimize ctyp) then
+              AV_cval (V_id (name id, ctyp), typ)
+            else
+              v
+         | _ -> v
+       end
+    | AV_vector (v, typ) when is_bitvector v && List.length v <= 64 ->
+       let bitstring = VL_bits (List.map value_of_aval_bit v, true) in
+       AV_cval (V_lit (bitstring, CT_fbits (List.length v, true)), typ)
+    | AV_tuple avals -> AV_tuple (List.map (c_aval ctx) avals)
+    | aval -> aval
+
+  let c_fragment = function
+    | AV_cval (cval, _) -> cval
+    | _ -> assert false
+
+  (* Map over all the functions in an aexp. *)
+  let rec analyze_functions ctx f (AE_aux (aexp, env, l)) =
+    let ctx = { ctx with local_env = env } in
+    let aexp = match aexp with
+      | AE_app (id, vs, typ) -> f ctx id vs typ
+
+      | AE_cast (aexp, typ) -> AE_cast (analyze_functions ctx f aexp, typ)
+
+      | AE_assign (id, typ, aexp) -> AE_assign (id, typ, analyze_functions ctx f aexp)
+
+      | AE_write_ref (id, typ, aexp) -> AE_write_ref (id, typ, analyze_functions ctx f aexp)
+
+      | AE_short_circuit (op, aval, aexp) -> AE_short_circuit (op, aval, analyze_functions ctx f aexp)
+
+      | AE_let (mut, id, typ1, aexp1, (AE_aux (_, env2, _) as aexp2), typ2) ->
+         let aexp1 = analyze_functions ctx f aexp1 in
+         (* Use aexp2's environment because it will contain constraints for id *)
+         let ctyp1 = convert_typ { ctx with local_env = env2 } typ1 in
+         let ctx = { ctx with locals = Bindings.add id (mut, ctyp1) ctx.locals } in
+         AE_let (mut, id, typ1, aexp1, analyze_functions ctx f aexp2, typ2)
+
+      | AE_block (aexps, aexp, typ) -> AE_block (List.map (analyze_functions ctx f) aexps, analyze_functions ctx f aexp, typ)
+
+      | AE_if (aval, aexp1, aexp2, typ) ->
+         AE_if (aval, analyze_functions ctx f aexp1, analyze_functions ctx f aexp2, typ)
+
+      | AE_loop (loop_typ, aexp1, aexp2) -> AE_loop (loop_typ, analyze_functions ctx f aexp1, analyze_functions ctx f aexp2)
+
+      | AE_for (id, aexp1, aexp2, aexp3, order, aexp4) ->
+         let aexp1 = analyze_functions ctx f aexp1 in
+         let aexp2 = analyze_functions ctx f aexp2 in
+         let aexp3 = analyze_functions ctx f aexp3 in
+         let aexp4 = analyze_functions ctx f aexp4 in
+         (* Currently we assume that loop indexes are always safe to put into an int64 *)
+         let ctx = { ctx with locals = Bindings.add id (Immutable, CT_fint 64) ctx.locals } in
+         AE_for (id, aexp1, aexp2, aexp3, order, aexp4)
+
+      | AE_case (aval, cases, typ) ->
+         let analyze_case (AP_aux (_, env, _) as pat, aexp1, aexp2) =
+           let pat_bindings = Bindings.bindings (apat_types pat) in
+           let ctx = { ctx with local_env = env } in
+           let ctx =
+             List.fold_left (fun ctx (id, typ) -> { ctx with locals = Bindings.add id (Immutable, convert_typ ctx typ) ctx.locals }) ctx pat_bindings
+           in
+           pat, analyze_functions ctx f aexp1, analyze_functions ctx f aexp2
          in
-         pat, analyze_functions ctx f aexp1, analyze_functions ctx f aexp2
-       in
-       AE_case (aval, List.map analyze_case cases, typ)
+         AE_case (aval, List.map analyze_case cases, typ)
 
-    | AE_try (aexp, cases, typ) ->
-       AE_try (analyze_functions ctx f aexp, List.map (fun (pat, aexp1, aexp2) -> pat, analyze_functions ctx f aexp1, analyze_functions ctx f aexp2) cases, typ)
+      | AE_try (aexp, cases, typ) ->
+         AE_try (analyze_functions ctx f aexp, List.map (fun (pat, aexp1, aexp2) -> pat, analyze_functions ctx f aexp1, analyze_functions ctx f aexp2) cases, typ)
 
-    | AE_field _ | AE_record_update _ | AE_val _ | AE_return _ | AE_throw _ as v -> v
-  in
-  AE_aux (aexp, env, l)
+      | AE_field _ | AE_record_update _ | AE_val _ | AE_return _ | AE_throw _ as v -> v
+    in
+    AE_aux (aexp, env, l)
 
-let analyze_primop' ctx id args typ =
-  let no_change = AE_app (id, args, typ) in
-  let args = List.map (c_aval ctx) args in
-  let extern = if Env.is_extern id ctx.tc_env "c" then Env.get_extern id ctx.tc_env "c" else failwith "Not extern" in
+  let analyze_primop' ctx id args typ =
+    let no_change = AE_app (id, args, typ) in
+    let args = List.map (c_aval ctx) args in
+    let extern = if Env.is_extern id ctx.tc_env "c" then Env.get_extern id ctx.tc_env "c" else failwith "Not extern" in
 
-  let v_one = V_lit (VL_int (Big_int.of_int 1), CT_fint 64) in
-  let v_int n = V_lit (VL_int (Big_int.of_int n), CT_fint 64) in
+    let v_one = V_lit (VL_int (Big_int.of_int 1), CT_fint 64) in
+    let v_int n = V_lit (VL_int (Big_int.of_int n), CT_fint 64) in
 
-  match extern, args with
-  | "eq_bits", [AV_cval (v1, _); AV_cval (v2, _)] when ctyp_equal (cval_ctyp v1) (cval_ctyp v2) ->
-     begin match cval_ctyp v1 with
-     | CT_fbits _ | CT_sbits _ ->
+    match extern, args with
+    | "eq_bits", [AV_cval (v1, _); AV_cval (v2, _)] when ctyp_equal (cval_ctyp v1) (cval_ctyp v2) ->
+       begin match cval_ctyp v1 with
+       | CT_fbits _ | CT_sbits _ ->
         AE_val (AV_cval (V_call (Eq, [v1; v2]), typ))
-     | _ -> no_change
-     end
+       | _ -> no_change
+       end
 
-  | "neq_bits", [AV_cval (v1, _); AV_cval (v2, _)] when ctyp_equal (cval_ctyp v1) (cval_ctyp v2) ->
-     begin match cval_ctyp v1 with
-     | CT_fbits _ | CT_sbits _ ->
-        AE_val (AV_cval (V_call (Neq, [v1; v2]), typ))
-     | _ -> no_change
-     end
+    | "neq_bits", [AV_cval (v1, _); AV_cval (v2, _)] when ctyp_equal (cval_ctyp v1) (cval_ctyp v2) ->
+       begin match cval_ctyp v1 with
+       | CT_fbits _ | CT_sbits _ ->
+          AE_val (AV_cval (V_call (Neq, [v1; v2]), typ))
+       | _ -> no_change
+       end
 
-  | "eq_int", [AV_cval (v1, _); AV_cval (v2, _)] ->
-     AE_val (AV_cval (V_call (Eq, [v1; v2]), typ))
+    | "eq_int", [AV_cval (v1, _); AV_cval (v2, _)] ->
+       AE_val (AV_cval (V_call (Eq, [v1; v2]), typ))
 
-  | "eq_bit", [AV_cval (v1, _); AV_cval (v2, _)] ->
-     AE_val (AV_cval (V_call (Eq, [v1; v2]), typ))
+    | "eq_bit", [AV_cval (v1, _); AV_cval (v2, _)] ->
+       AE_val (AV_cval (V_call (Eq, [v1; v2]), typ))
 
-  | "zeros", [_] ->
-     begin match destruct_vector ctx.tc_env typ with
-     | Some (Nexp_aux (Nexp_constant n, _), _, Typ_aux (Typ_id id, _))
-          when string_of_id id = "bit" && Big_int.less_equal n (Big_int.of_int 64) ->
-        let n = Big_int.to_int n in
-        AE_val (AV_cval (V_lit (VL_bits (Util.list_init n (fun _ -> Sail2_values.B0), true), CT_fbits (n, true)), typ))
-     | _ -> no_change
-     end
+    | "zeros", [_] ->
+       begin match destruct_vector ctx.tc_env typ with
+       | Some (Nexp_aux (Nexp_constant n, _), _, Typ_aux (Typ_id id, _))
+            when string_of_id id = "bit" && Big_int.less_equal n (Big_int.of_int 64) ->
+          let n = Big_int.to_int n in
+          AE_val (AV_cval (V_lit (VL_bits (Util.list_init n (fun _ -> Sail2_values.B0), true), CT_fbits (n, true)), typ))
+       | _ -> no_change
+       end
 
-  | "zero_extend", [AV_cval (v, _); _] ->
-     begin match destruct_vector ctx.tc_env typ with
-     | Some (Nexp_aux (Nexp_constant n, _), _, Typ_aux (Typ_id id, _))
-          when string_of_id id = "bit" && Big_int.less_equal n (Big_int.of_int 64) ->
-        AE_val (AV_cval (V_call (Zero_extend (Big_int.to_int n), [v]), typ))
-     | _ -> no_change
-     end
+    | "zero_extend", [AV_cval (v, _); _] ->
+       begin match destruct_vector ctx.tc_env typ with
+       | Some (Nexp_aux (Nexp_constant n, _), _, Typ_aux (Typ_id id, _))
+            when string_of_id id = "bit" && Big_int.less_equal n (Big_int.of_int 64) ->
+          AE_val (AV_cval (V_call (Zero_extend (Big_int.to_int n), [v]), typ))
+       | _ -> no_change
+       end
 
-  | "sign_extend", [AV_cval (v, _); _] ->
-     begin match destruct_vector ctx.tc_env typ with
-     | Some (Nexp_aux (Nexp_constant n, _), _, Typ_aux (Typ_id id, _))
-          when string_of_id id = "bit" && Big_int.less_equal n (Big_int.of_int 64) ->
-        AE_val (AV_cval (V_call (Sign_extend (Big_int.to_int n), [v]), typ))
-     | _ -> no_change
-     end
+    | "sign_extend", [AV_cval (v, _); _] ->
+       begin match destruct_vector ctx.tc_env typ with
+       | Some (Nexp_aux (Nexp_constant n, _), _, Typ_aux (Typ_id id, _))
+            when string_of_id id = "bit" && Big_int.less_equal n (Big_int.of_int 64) ->
+          AE_val (AV_cval (V_call (Sign_extend (Big_int.to_int n), [v]), typ))
+       | _ -> no_change
+       end
 
-  | "lteq", [AV_cval (v1, _); AV_cval (v2, _)] ->
-     AE_val (AV_cval (V_call (Ilteq, [v1; v2]), typ))
-  | "gteq", [AV_cval (v1, _); AV_cval (v2, _)] ->
-     AE_val (AV_cval (V_call (Igteq, [v1; v2]), typ))
-  | "lt", [AV_cval (v1, _); AV_cval (v2, _)] ->
-     AE_val (AV_cval (V_call (Ilt, [v1; v2]), typ))
-  | "gt", [AV_cval (v1, _); AV_cval (v2, _)] ->
-     AE_val (AV_cval (V_call (Igt, [v1; v2]), typ))
-
-  | "append", [AV_cval (v1, _); AV_cval (v2, _)] ->
-     begin match ctyp_of_typ ctx typ with
-     | CT_fbits _ | CT_sbits _ ->
-        AE_val (AV_cval (V_call (Concat, [v1; v2]), typ))
-     | _ -> no_change
-     end
+    | "lteq", [AV_cval (v1, _); AV_cval (v2, _)] ->
+       AE_val (AV_cval (V_call (Ilteq, [v1; v2]), typ))
+    | "gteq", [AV_cval (v1, _); AV_cval (v2, _)] ->
+       AE_val (AV_cval (V_call (Igteq, [v1; v2]), typ))
+    | "lt", [AV_cval (v1, _); AV_cval (v2, _)] ->
+       AE_val (AV_cval (V_call (Ilt, [v1; v2]), typ))
+    | "gt", [AV_cval (v1, _); AV_cval (v2, _)] ->
+       AE_val (AV_cval (V_call (Igt, [v1; v2]), typ))
+
+    | "append", [AV_cval (v1, _); AV_cval (v2, _)] ->
+       begin match convert_typ ctx typ with
+       | CT_fbits _ | CT_sbits _ ->
+          AE_val (AV_cval (V_call (Concat, [v1; v2]), typ))
+       | _ -> no_change
+       end
 
-  | "not_bits", [AV_cval (v, _)] ->
-     AE_val (AV_cval (V_call (Bvnot, [v]), typ))
+    | "not_bits", [AV_cval (v, _)] ->
+       AE_val (AV_cval (V_call (Bvnot, [v]), typ))
 
-  | "add_bits", [AV_cval (v1, _); AV_cval (v2, _)] when ctyp_equal (cval_ctyp v1) (cval_ctyp v2) ->
-     AE_val (AV_cval (V_call (Bvadd, [v1; v2]), typ))
+    | "add_bits", [AV_cval (v1, _); AV_cval (v2, _)] when ctyp_equal (cval_ctyp v1) (cval_ctyp v2) ->
+       AE_val (AV_cval (V_call (Bvadd, [v1; v2]), typ))
 
-  | "sub_bits", [AV_cval (v1, _); AV_cval (v2, _)] when ctyp_equal (cval_ctyp v1) (cval_ctyp v2) ->
-     AE_val (AV_cval (V_call (Bvsub, [v1; v2]), typ))
+    | "sub_bits", [AV_cval (v1, _); AV_cval (v2, _)] when ctyp_equal (cval_ctyp v1) (cval_ctyp v2) ->
+       AE_val (AV_cval (V_call (Bvsub, [v1; v2]), typ))
 
-  | "and_bits", [AV_cval (v1, _); AV_cval (v2, _)] when ctyp_equal (cval_ctyp v1) (cval_ctyp v2) ->
-     AE_val (AV_cval (V_call (Bvand, [v1; v2]), typ))
+    | "and_bits", [AV_cval (v1, _); AV_cval (v2, _)] when ctyp_equal (cval_ctyp v1) (cval_ctyp v2) ->
+       AE_val (AV_cval (V_call (Bvand, [v1; v2]), typ))
 
-  | "or_bits", [AV_cval (v1, _); AV_cval (v2, _)] when ctyp_equal (cval_ctyp v1) (cval_ctyp v2) ->
-     AE_val (AV_cval (V_call (Bvor, [v1; v2]), typ))
+    | "or_bits", [AV_cval (v1, _); AV_cval (v2, _)] when ctyp_equal (cval_ctyp v1) (cval_ctyp v2) ->
+       AE_val (AV_cval (V_call (Bvor, [v1; v2]), typ))
 
-  | "xor_bits", [AV_cval (v1, _); AV_cval (v2, _)] when ctyp_equal (cval_ctyp v1) (cval_ctyp v2) ->
-     AE_val (AV_cval (V_call (Bvxor, [v1; v2]), typ))
+    | "xor_bits", [AV_cval (v1, _); AV_cval (v2, _)] when ctyp_equal (cval_ctyp v1) (cval_ctyp v2) ->
+       AE_val (AV_cval (V_call (Bvxor, [v1; v2]), typ))
 
-  | "vector_subrange", [AV_cval (vec, _); AV_cval (f, _); AV_cval (t, _)] ->
-     begin match ctyp_of_typ ctx typ with
-     | CT_fbits (n, true) ->
-        AE_val (AV_cval (V_call (Slice n, [vec; t]), typ))
-     | _ -> no_change
-     end
+    | "vector_subrange", [AV_cval (vec, _); AV_cval (f, _); AV_cval (t, _)] ->
+       begin match convert_typ ctx typ with
+       | CT_fbits (n, true) ->
+          AE_val (AV_cval (V_call (Slice n, [vec; t]), typ))
+       | _ -> no_change
+       end
 
-  | "slice", [AV_cval (vec, _); AV_cval (start, _); AV_cval (len, _)] ->
-     begin match ctyp_of_typ ctx typ with
-     | CT_fbits (n, _) ->
-        AE_val (AV_cval (V_call (Slice n, [vec; start]), typ))
-     | CT_sbits (64, _) ->
-        AE_val (AV_cval (V_call (Sslice 64, [vec; start; len]), typ))
-     | _ -> no_change
-     end
+    | "slice", [AV_cval (vec, _); AV_cval (start, _); AV_cval (len, _)] ->
+       begin match convert_typ ctx typ with
+       | CT_fbits (n, _) ->
+          AE_val (AV_cval (V_call (Slice n, [vec; start]), typ))
+       | CT_sbits (64, _) ->
+          AE_val (AV_cval (V_call (Sslice 64, [vec; start; len]), typ))
+       | _ -> no_change
+       end
 
-  | "vector_access", [AV_cval (vec, _); AV_cval (n, _)] ->
-     AE_val (AV_cval (V_call (Bvaccess, [vec; n]), typ))
+    | "vector_access", [AV_cval (vec, _); AV_cval (n, _)] ->
+       AE_val (AV_cval (V_call (Bvaccess, [vec; n]), typ))
 
-  | "add_int", [AV_cval (op1, _); AV_cval (op2, _)] ->
-     begin match destruct_range Env.empty typ with
-     | None -> no_change
-     | Some (kids, constr, n, m) ->
-        match nexp_simp n, nexp_simp m with
-        | Nexp_aux (Nexp_constant n, _), Nexp_aux (Nexp_constant m, _)
+    | "add_int", [AV_cval (op1, _); AV_cval (op2, _)] ->
+       begin match destruct_range Env.empty typ with
+       | None -> no_change
+       | Some (kids, constr, n, m) ->
+          match nexp_simp n, nexp_simp m with
+          | 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) ->
-           AE_val (AV_cval (V_call (Iadd, [op1; op2]), typ))
-        | n, m when prove __POS__ ctx.local_env (nc_lteq (nconstant (min_int 64)) n) && prove __POS__ ctx.local_env (nc_lteq m (nconstant (max_int 64))) ->
-           AE_val (AV_cval (V_call (Iadd, [op1; op2]), typ))
-        | _ -> no_change
-     end
+             AE_val (AV_cval (V_call (Iadd, [op1; op2]), typ))
+          | n, m when prove __POS__ ctx.local_env (nc_lteq (nconstant (min_int 64)) n) && prove __POS__ ctx.local_env (nc_lteq m (nconstant (max_int 64))) ->
+             AE_val (AV_cval (V_call (Iadd, [op1; op2]), typ))
+          | _ -> no_change
+       end
 
-  | "replicate_bits", [AV_cval (vec, vtyp); _] ->
-     begin match destruct_vector ctx.tc_env typ, destruct_vector ctx.tc_env vtyp with
-     | Some (Nexp_aux (Nexp_constant n, _), _, _), Some (Nexp_aux (Nexp_constant m, _), _, _)
-          when Big_int.less_equal n (Big_int.of_int 64) ->
-        let times = Big_int.div n m in
-        if Big_int.equal (Big_int.mul m times) n then
-          AE_val (AV_cval (V_call (Replicate (Big_int.to_int times), [vec]), typ))
-        else
+    | "replicate_bits", [AV_cval (vec, vtyp); _] ->
+       begin match destruct_vector ctx.tc_env typ, destruct_vector ctx.tc_env vtyp with
+       | Some (Nexp_aux (Nexp_constant n, _), _, _), Some (Nexp_aux (Nexp_constant m, _), _, _)
+            when Big_int.less_equal n (Big_int.of_int 64) ->
+          let times = Big_int.div n m in
+          if Big_int.equal (Big_int.mul m times) n then
+            AE_val (AV_cval (V_call (Replicate (Big_int.to_int times), [vec]), typ))
+          else
+            no_change
+       | _, _ ->
           no_change
-     | _, _ ->
-        no_change
-     end
-
-  | "undefined_bit", _ ->
-     AE_val (AV_cval (V_lit (VL_bit Sail2_values.B0, CT_bit), typ))
+       end
 
-  | "undefined_bool", _ ->
-     AE_val (AV_cval (V_lit (VL_bool false, CT_bool), typ))
+    | "undefined_bit", _ ->
+       AE_val (AV_cval (V_lit (VL_bit Sail2_values.B0, CT_bit), typ))
 
-  | _, _ ->
-     no_change
+    | "undefined_bool", _ ->
+       AE_val (AV_cval (V_lit (VL_bool false, CT_bool), typ))
 
-let analyze_primop ctx id args typ =
-  let no_change = AE_app (id, args, typ) in
-  if !optimize_primops then
-    try analyze_primop' ctx id args typ with
-    | Failure str ->
+    | _, _ ->
        no_change
-  else
-    no_change
+
+  let analyze_primop ctx id args typ =
+    let no_change = AE_app (id, args, typ) in
+    if !optimize_primops then
+      try analyze_primop' ctx id args typ with
+      | Failure str ->
+         no_change
+    else
+      no_change
+
+  let optimize_anf ctx aexp =
+    analyze_functions ctx analyze_primop (c_literals ctx aexp)
+
+
+  let unroll_loops () = None
+  let specialize_calls = false
+  let ignore_64 = false
+  let struct_value = false
+  let use_real = false
+end
 
 (** Functions that have heap-allocated return types are implemented by
    passing a pointer a location where the return value should be
@@ -571,9 +588,9 @@ let fix_early_heap_return ret ret_ctyp instrs =
        before
        @ [iblock (rewrite_return instrs)]
        @ rewrite_return after
-    | before, I_aux (I_if (cval, then_instrs, else_instrs, ctyp), _) :: after ->
+    | before, I_aux (I_if (cval, then_instrs, else_instrs, ctyp), (_, l)) :: after ->
        before
-       @ [iif cval (rewrite_return then_instrs) (rewrite_return else_instrs) ctyp]
+       @ [iif l cval (rewrite_return then_instrs) (rewrite_return else_instrs) ctyp]
        @ rewrite_return after
     | before, I_aux (I_funcall (CL_id (Return _, ctyp), extern, fid, args), aux) :: after ->
        before
@@ -608,9 +625,9 @@ let fix_early_stack_return ret ret_ctyp instrs =
        before
        @ [iblock (rewrite_return instrs)]
        @ rewrite_return after
-    | before, I_aux (I_if (cval, then_instrs, else_instrs, ctyp), _) :: after ->
+    | before, I_aux (I_if (cval, then_instrs, else_instrs, ctyp), (_, l)) :: after ->
        before
-       @ [iif cval (rewrite_return then_instrs) (rewrite_return else_instrs) ctyp]
+       @ [iif l cval (rewrite_return then_instrs) (rewrite_return else_instrs) ctyp]
        @ rewrite_return after
     | before, I_aux (I_funcall (CL_id (Return _, ctyp), extern, fid, args), aux) :: after ->
        before
@@ -631,7 +648,7 @@ let fix_early_stack_return ret ret_ctyp instrs =
   rewrite_return instrs
 
 let rec insert_heap_returns ret_ctyps = function
-  | (CDEF_spec (id, _, ret_ctyp) as cdef) :: cdefs ->
+  | (CDEF_spec (id, _, _, ret_ctyp) as cdef) :: cdefs ->
      cdef :: insert_heap_returns (Bindings.add id ret_ctyp ret_ctyps) cdefs
 
   | CDEF_fundef (id, None, args, body) :: cdefs ->
@@ -1022,7 +1039,7 @@ let optimize recursive_functions cdefs =
 
 let sgen_id id = Util.zencode_string (string_of_id id)
 let sgen_uid uid = zencode_uid uid
-let sgen_name id = string_of_name id
+let sgen_name id = string_of_name ~deref_current_exception:true ~zencode:true id
 let codegen_id id = string (sgen_id id)
 let codegen_uid id = string (sgen_uid id)
 
@@ -1033,7 +1050,7 @@ let sgen_function_id id =
 let sgen_function_uid uid =
   let str = zencode_uid uid in
   !opt_prefix ^ String.sub str 1 (String.length str - 1)
-  
+
 let codegen_function_id id = string (sgen_function_id id)
 
 let rec sgen_ctyp = function
@@ -1052,6 +1069,7 @@ let rec sgen_ctyp = function
   | CT_variant (id, _) -> "struct " ^ sgen_id id
   | CT_list _ as l -> Util.zencode_string (string_of_ctyp l)
   | CT_vector _ as v -> Util.zencode_string (string_of_ctyp v)
+  | CT_fvector (_, ord, typ) -> sgen_ctyp (CT_vector (ord, typ))
   | CT_string -> "sail_string"
   | CT_real -> "real"
   | CT_ref ctyp -> sgen_ctyp ctyp ^ "*"
@@ -1073,6 +1091,7 @@ let rec sgen_ctyp_name = function
   | CT_variant (id, _) -> sgen_id id
   | CT_list _ as l -> Util.zencode_string (string_of_ctyp l)
   | CT_vector _ as v -> Util.zencode_string (string_of_ctyp v)
+  | CT_fvector (_, ord, typ) -> sgen_ctyp_name (CT_vector (ord, typ))
   | CT_string -> "sail_string"
   | CT_real -> "real"
   | CT_ref ctyp -> "ref_" ^ sgen_ctyp_name ctyp
@@ -1094,24 +1113,27 @@ let sgen_mask n =
   else
     failwith "Tried to create a mask literal for a vector greater than 64 bits."
 
-let sgen_value = function
+let rec sgen_value = function
   | VL_bits ([], _) -> "UINT64_C(0)"
   | VL_bits (bs, true) -> "UINT64_C(" ^ Sail2_values.show_bitlist bs ^ ")"
   | VL_bits (bs, false) -> "UINT64_C(" ^ Sail2_values.show_bitlist (List.rev bs) ^ ")"
   | VL_int i -> Big_int.to_string i ^ "l"
   | VL_bool true -> "true"
   | VL_bool false -> "false"
-  | VL_null -> "NULL"
   | VL_unit -> "UNIT"
   | VL_bit Sail2_values.B0 -> "UINT64_C(0)"
   | VL_bit Sail2_values.B1 -> "UINT64_C(1)"
   | VL_bit Sail2_values.BU -> failwith "Undefined bit found in value"
   | VL_real str -> str
   | VL_string str -> "\"" ^ str ^ "\""
-  
+  | VL_empty_list -> "NULL"
+  | VL_enum element -> Util.zencode_string element
+  | VL_ref r -> "&" ^ Util.zencode_string r
+  | VL_undefined ->
+     Reporting.unreachable Parse_ast.Unknown __POS__ "Cannot generate C value for an undefined literal"
+
 let rec sgen_cval = function
-  | V_id (id, ctyp) -> string_of_name id
-  | V_ref (id, _) -> "&" ^ string_of_name id
+  | V_id (id, ctyp) -> sgen_name id
   | V_lit (vl, ctyp) -> sgen_value vl
   | V_call (op, cvals) -> sgen_call op cvals
   | V_field (f, field) ->
@@ -1133,8 +1155,6 @@ let rec sgen_cval = function
 and sgen_call op cvals =
   let open Printf in
   match op, cvals with
-  | Bit_to_bool, [v] ->
-     sprintf "((bool) %s)" (sgen_cval v)
   | Bnot, [v] -> "!(" ^ sgen_cval v ^ ")"
   | List_hd, [v] ->
      sprintf "(%s).hd" ("*" ^ sgen_cval v)
@@ -1306,6 +1326,7 @@ let sgen_cval_param cval =
 let rec sgen_clexp = function
   | CL_id (Have_exception _, _) -> "have_exception"
   | CL_id (Current_exception _, _) -> "current_exception"
+  | CL_id (Throw_location _, _) -> "throw_location"
   | CL_id (Return _, _) -> assert false
   | CL_id (Name (id, _), _) -> "&" ^ sgen_id id
   | CL_field (clexp, field) -> "&((" ^ sgen_clexp clexp ^ ")->" ^ zencode_uid field ^ ")"
@@ -1317,6 +1338,7 @@ let rec sgen_clexp = function
 let rec sgen_clexp_pure = function
   | CL_id (Have_exception _, _) -> "have_exception"
   | CL_id (Current_exception _, _) -> "current_exception"
+  | CL_id (Throw_location _, _) -> "throw_location"
   | CL_id (Return _, _) -> assert false
   | CL_id (Name (id, _), _) -> sgen_id id
   | CL_field (clexp, field) -> sgen_clexp_pure clexp ^ "." ^ zencode_uid field
@@ -1400,21 +1422,26 @@ let rec codegen_instr fid ctx (I_aux (instr, (_, l))) =
      ^^ jump 2 2 (separate_map hardline (codegen_instr fid ctx) instrs) ^^ hardline
      ^^ string "  }"
 
-  | I_funcall (x, extern, f, args) ->
+  | I_funcall (x, special_extern, f, args) ->
      let c_args = Util.string_of_list ", " sgen_cval args in
      let ctyp = clexp_ctyp x in
-     let is_extern = Env.is_extern (fst f) ctx.tc_env "c" || extern in
+     let is_extern = Env.is_extern (fst f) ctx.tc_env "c" || special_extern in
      let fname =
-       if Env.is_extern (fst f) ctx.tc_env "c" then
-         Env.get_extern (fst f) ctx.tc_env "c"
-       else if extern then
+       if special_extern then
          string_of_id (fst f)
+       else if Env.is_extern (fst f) ctx.tc_env "c" then
+         Env.get_extern (fst f) ctx.tc_env "c"
        else
          sgen_function_uid f
      in
      let fname =
        match fname, ctyp with
        | "internal_pick", _ -> Printf.sprintf "pick_%s" (sgen_ctyp_name ctyp)
+       | "cons", _ ->
+          begin match snd f with
+          | [ctyp] -> Util.zencode_string ("cons#" ^ string_of_ctyp ctyp)
+          | _ -> c_error "cons without specified type"
+          end
        | "eq_anything", _ ->
           begin match args with
           | cval :: _ -> Printf.sprintf "eq_%s" (sgen_ctyp_name (cval_ctyp cval))
@@ -1765,6 +1792,8 @@ let codegen_type_def ctx = function
           ^^ string "struct zexception *current_exception = NULL;"
           ^^ hardline
           ^^ string "bool have_exception = false;"
+          ^^ hardline
+          ^^ string "sail_string *throw_location = NULL;"
         else
           empty
 
@@ -1994,7 +2023,7 @@ let codegen_def' ctx = function
      string (Printf.sprintf "// register %s" (string_of_id id)) ^^ hardline
      ^^ string (Printf.sprintf "%s %s;" (sgen_ctyp ctyp) (sgen_id id))
 
-  | CDEF_spec (id, arg_ctyps, ret_ctyp) ->
+  | CDEF_spec (id, _, arg_ctyps, ret_ctyp) ->
      let static = if !opt_static then "static " else "" in
      if Env.is_extern id ctx.tc_env "c" then
        empty
@@ -2009,7 +2038,7 @@ let codegen_def' ctx = function
        | None ->
           c_error ~loc:(id_loc id) ("No valspec found for " ^ string_of_id id)
      in
- 
+
      (* Check that the function has the correct arity at this point. *)
      if List.length arg_ctyps <> List.length args then
        c_error ~loc:(id_loc id) ("function arguments "
@@ -2095,7 +2124,7 @@ type c_gen_typ =
 let rec ctyp_dependencies = function
   | CT_tup ctyps -> List.concat (List.map ctyp_dependencies ctyps) @ [CTG_tup ctyps]
   | CT_list ctyp -> ctyp_dependencies ctyp @ [CTG_list ctyp]
-  | CT_vector (direction, ctyp) -> ctyp_dependencies ctyp @ [CTG_vector (direction, ctyp)]
+  | CT_vector (direction, ctyp) | CT_fvector (_, direction, ctyp) -> ctyp_dependencies ctyp @ [CTG_vector (direction, ctyp)]
   | CT_ref ctyp -> ctyp_dependencies ctyp
   | CT_struct (_, ctors) -> List.concat (List.map (fun (_, ctyp) -> ctyp_dependencies ctyp) ctors)
   | CT_variant (_, ctors) -> List.concat (List.map (fun (_, ctyp) -> ctyp_dependencies ctyp) ctors)
@@ -2169,20 +2198,17 @@ let rec get_recursive_functions (Defs defs) =
   | [] -> IdSet.empty
 
 let jib_of_ast env ast =
-  let ctx =
-    initial_ctx
-      ~convert_typ:ctyp_of_typ
-      ~optimize_anf:(fun ctx aexp -> analyze_functions ctx analyze_primop (c_literals ctx aexp))
-      env
-  in
-  Jib_compile.compile_ast ctx ast
+  let module Jibc = Make(C_config) in
+  let ctx = initial_ctx (add_special_functions env) in
+  Jibc.compile_ast ctx ast
 
 let compile_ast env output_chan c_includes ast =
   try
     let recursive_functions = Spec_analysis.top_sort_defs ast |> get_recursive_functions in
 
     let cdefs, ctx = jib_of_ast env ast in
-    Jib_interactive.ir := cdefs;
+    let cdefs', _ = Jib_optimize.remove_tuples cdefs ctx in
+    Jib_interactive.ir := cdefs';
     let cdefs = insert_heap_returns Bindings.empty cdefs in
     let cdefs = optimize recursive_functions cdefs in
 
@@ -2199,10 +2225,15 @@ let compile_ast env output_chan c_includes ast =
     let exn_boilerplate =
       if not (Bindings.mem (mk_id "exception") ctx.variants) then ([], []) else
         ([ "  current_exception = sail_malloc(sizeof(struct zexception));";
-           "  CREATE(zexception)(current_exception);" ],
-         [ "  KILL(zexception)(current_exception);";
+           "  CREATE(zexception)(current_exception);";
+           "  throw_location = sail_malloc(sizeof(sail_string));";
+           "  CREATE(sail_string)(throw_location);" ],
+         [ "  if (have_exception) {fprintf(stderr, \"Exiting due to uncaught exception: %s\\n\", *throw_location);}";
+           "  KILL(zexception)(current_exception);";
            "  sail_free(current_exception);";
-           "  if (have_exception) {fprintf(stderr, \"Exiting due to uncaught exception\\n\"); exit(EXIT_FAILURE);}" ])
+           "  KILL(sail_string)(throw_location);";
+           "  sail_free(throw_location);";
+           "  if (have_exception) {exit(EXIT_FAILURE);}" ])
     in
 
     let letbind_initializers =
diff --git a/src/jib/c_backend.mli b/src/jib/c_backend.mli
index 2f748fd7..e627ebd8 100644
--- a/src/jib/c_backend.mli
+++ b/src/jib/c_backend.mli
@@ -106,8 +106,5 @@ val optimize_alias : bool ref
 val optimize_fixed_int : bool ref
 val optimize_fixed_bits : bool ref
 
-(** Convert a typ to a IR ctyp *)
-val ctyp_of_typ : Jib_compile.ctx -> Ast.typ -> ctyp
-
 val jib_of_ast : Env.t -> tannot Ast.defs -> cdef list * Jib_compile.ctx
 val compile_ast : Env.t -> out_channel -> string list -> tannot Ast.defs -> unit
diff --git a/src/jib/jib_compile.ml b/src/jib/jib_compile.ml
index 0efac940..4282ae30 100644
--- a/src/jib/jib_compile.ml
+++ b/src/jib/jib_compile.ml
@@ -58,6 +58,7 @@ open Value2
 open Anf
 
 let opt_memo_cache = ref false
+let opt_track_throw = ref true
 
 let optimize_aarch64_fast_struct = ref false
 
@@ -151,38 +152,38 @@ type ctx =
     enums : IdSet.t Bindings.t;
     variants : (ctyp UBindings.t) Bindings.t;
     valspecs : (ctyp list * ctyp) Bindings.t;
-    tc_env : Env.t;
     local_env : Env.t;
+    tc_env : Env.t;
     locals : (mut * ctyp) Bindings.t;
     letbinds : int list;
     no_raw : bool;
-    convert_typ : ctx -> typ -> ctyp;
-    optimize_anf : ctx -> typ aexp -> typ aexp;
-    specialize_calls : bool;
-    ignore_64 : bool;
-    struct_value : bool;
-    use_real : bool;
   }
 
-let initial_ctx ~convert_typ:convert_typ ~optimize_anf:optimize_anf env =
+let initial_ctx env =
   { records = Bindings.empty;
     enums = Bindings.empty;
     variants = Bindings.empty;
     valspecs = Bindings.empty;
-    tc_env = env;
     local_env = env;
+    tc_env = env;
     locals = Bindings.empty;
     letbinds = [];
     no_raw = false;
-    convert_typ = convert_typ;
-    optimize_anf = optimize_anf;
-    specialize_calls = false;
-    ignore_64 = false;
-    struct_value = false;
-    use_real = false;
   }
 
-let ctyp_of_typ ctx typ = ctx.convert_typ ctx typ
+module type Config = sig
+  val convert_typ : ctx -> typ -> ctyp
+  val optimize_anf : ctx -> typ aexp -> typ aexp
+  val unroll_loops : unit -> int option
+  val specialize_calls : bool
+  val ignore_64 : bool
+  val struct_value : bool
+  val use_real : bool
+end
+
+module Make(C: Config) = struct
+
+let ctyp_of_typ ctx typ = C.convert_typ ctx typ
 
 let rec chunkify n xs =
   match Util.take n xs, Util.drop n xs with
@@ -210,12 +211,12 @@ let rec compile_aval l ctx = function
      end
 
   | AV_ref (id, typ) ->
-     [], V_ref (name id, ctyp_of_typ ctx (lvar_typ typ)), []
+     [], V_lit (VL_ref (string_of_id id), CT_ref (ctyp_of_typ ctx (lvar_typ typ))), []
 
   | AV_lit (L_aux (L_string str, _), typ) ->
      [], V_lit ((VL_string (String.escaped str)), ctyp_of_typ ctx typ), []
 
-  | AV_lit (L_aux (L_num n, _), typ) when ctx.ignore_64 ->
+  | AV_lit (L_aux (L_num n, _), typ) when C.ignore_64 ->
      [], V_lit ((VL_int n), ctyp_of_typ ctx typ), []
 
   | AV_lit (L_aux (L_num n, _), typ) when Big_int.less_equal (min_int 64) n && Big_int.less_equal n (max_int 64) ->
@@ -237,7 +238,7 @@ let rec compile_aval l ctx = function
   | AV_lit (L_aux (L_false, _), _) -> [], V_lit (VL_bool false, CT_bool), []
 
   | AV_lit (L_aux (L_real str, _), _) ->
-     if ctx.use_real then
+     if C.use_real then
        [], V_lit (VL_real str, CT_real), []
      else
        let gs = ngensym () in
@@ -247,6 +248,10 @@ let rec compile_aval l ctx = function
 
   | AV_lit (L_aux (L_unit, _), _) -> [], V_lit (VL_unit, CT_unit), []
 
+  | AV_lit (L_aux (L_undef, _), typ) ->
+     let ctyp = ctyp_of_typ ctx typ in
+     [], V_lit (VL_undefined, ctyp), []
+
   | AV_lit (L_aux (_, l) as lit, _) ->
      raise (Reporting.err_general l ("Encountered unexpected literal " ^ string_of_lit lit ^ " when converting ANF represention into IR"))
 
@@ -264,7 +269,7 @@ let rec compile_aval l ctx = function
      [iclear tup_ctyp gs]
      @ cleanup
 
-  | AV_record (fields, typ) when ctx.struct_value ->
+  | AV_record (fields, typ) when C.struct_value ->
      let ctyp = ctyp_of_typ ctx typ in
      let gs = ngensym () in
      let compile_fields (id, aval) =
@@ -309,7 +314,7 @@ let rec compile_aval l ctx = function
      end
 
   (* Convert a small bitvector to a uint64_t literal. *)
-  | AV_vector (avals, typ) when is_bitvector avals && (List.length avals <= 64 || ctx.ignore_64) ->
+  | AV_vector (avals, typ) when is_bitvector avals && (List.length avals <= 64 || C.ignore_64) ->
      begin
        let bitstring = List.map value_of_aval_bit avals in
        let len = List.length avals in
@@ -358,11 +363,14 @@ let rec compile_aval l ctx = function
        | V_lit (VL_bit Sail2_values.B1, _) ->
           [icopy l (CL_id (gs, ctyp)) (V_call (Bvor, [V_id (gs, ctyp); V_lit (mask i, ctyp)]))]
        | _ ->
-          (* FIXME: Make this work in C *)
-          setup @ [iif (V_call (Bit_to_bool, [cval])) [icopy l (CL_id (gs, ctyp)) (V_call (Bvor, [V_id (gs, ctyp); V_lit (mask i, ctyp)]))] [] CT_unit] @ cleanup
+          setup
+          @ [iextern (CL_id (gs, ctyp))
+                     (mk_id "update_fbits", [])
+                     [V_id (gs, ctyp); V_lit (VL_int (Big_int.of_int i), CT_fint 64); cval]]
+          @ cleanup
      in
      [idecl ctyp gs;
-      icopy l (CL_id (gs, ctyp)) (V_lit (VL_bits (Util.list_init 64 (fun _ -> Sail2_values.B0), direction), ctyp))]
+      icopy l (CL_id (gs, ctyp)) (V_lit (VL_bits (Util.list_init len (fun _ -> Sail2_values.B0), direction), ctyp))]
      @ List.concat (List.mapi aval_mask (List.rev avals)),
      V_id (gs, ctyp),
      []
@@ -403,7 +411,7 @@ let rec compile_aval l ctx = function
      let gs = ngensym () in
      let mk_cons aval =
        let setup, cval, cleanup = compile_aval l ctx aval in
-       setup @ [ifuncall (CL_id (gs, CT_list ctyp)) (mk_id ("cons#" ^ string_of_ctyp ctyp), []) [cval; V_id (gs, CT_list ctyp)]] @ cleanup
+       setup @ [iextern (CL_id (gs, CT_list ctyp)) (mk_id "cons", [ctyp]) [cval; V_id (gs, CT_list ctyp)]] @ cleanup
      in
      [idecl (CT_list ctyp) gs]
      @ List.concat (List.map mk_cons (List.rev avals)),
@@ -420,7 +428,7 @@ let optimize_call l ctx clexp id args arg_ctyps ret_ctyp =
           let have_ctyp = cval_ctyp cval in
           if is_polymorphic ctyp then
             V_poly (cval, have_ctyp)
-          else if ctx.specialize_calls || ctyp_equal ctyp have_ctyp then
+          else if C.specialize_calls || ctyp_equal ctyp have_ctyp then
             cval
           else
             let gs = ngensym () in
@@ -429,7 +437,7 @@ let optimize_call l ctx clexp id args arg_ctyps ret_ctyp =
             V_id (gs, ctyp))
         arg_ctyps args
     in
-    if ctx.specialize_calls || ctyp_equal (clexp_ctyp clexp) ret_ctyp then
+    if C.specialize_calls || ctyp_equal (clexp_ctyp clexp) ret_ctyp then
       !setup @ [ifuncall clexp id cast_args] @ !cleanup
     else
       let gs = ngensym () in
@@ -440,7 +448,7 @@ let optimize_call l ctx clexp id args arg_ctyps ret_ctyp =
          iclear ret_ctyp gs]
       @ !cleanup
   in
-  if not ctx.specialize_calls && Env.is_extern (fst id) ctx.tc_env "c" then
+  if not C.specialize_calls && Env.is_extern (fst id) ctx.tc_env "c" then
     let extern = Env.get_extern (fst id) ctx.tc_env "c" in
     begin match extern, List.map cval_ctyp args, clexp_ctyp clexp with
     | "slice", [CT_fbits _; CT_lint; _], CT_fbits (n, _) ->
@@ -506,7 +514,7 @@ let rec compile_match ctx (AP_aux (apat_aux, env, l)) cval case_label =
   let ctyp = cval_ctyp cval in
   match apat_aux with
   | AP_id (pid, _) when Env.is_union_constructor pid ctx.tc_env ->
-     [ijump (V_ctor_kind (cval, pid, [], cval_ctyp cval)) case_label],
+     [ijump l (V_ctor_kind (cval, pid, [], cval_ctyp cval)) case_label],
      [],
      ctx
 
@@ -517,7 +525,7 @@ let rec compile_match ctx (AP_aux (apat_aux, env, l)) cval case_label =
   | AP_id (pid, _) when is_ct_enum ctyp ->
      begin match Env.lookup_id pid ctx.tc_env with
      | Unbound -> [idecl ctyp (name pid); icopy l (CL_id (name pid, ctyp)) cval], [], ctx
-     | _ -> [ijump (V_call (Neq, [V_id (name pid, ctyp); cval])) case_label], [], ctx
+     | _ -> [ijump l (V_call (Neq, [V_id (name pid, ctyp); cval])) case_label], [], ctx
      end
 
   | AP_id (pid, typ) ->
@@ -562,7 +570,7 @@ let rec compile_match ctx (AP_aux (apat_aux, env, l)) cval case_label =
             [], ctor_ctyp
         in
         let instrs, cleanup, ctx = compile_match ctx apat (V_ctor_unwrap (ctor, cval, unifiers, ctor_ctyp)) case_label in
-        [ijump (V_ctor_kind (cval, ctor, unifiers, pat_ctyp)) case_label]
+        [ijump l (V_ctor_kind (cval, ctor, unifiers, pat_ctyp)) case_label]
         @ instrs,
         cleanup,
         ctx
@@ -581,12 +589,12 @@ let rec compile_match ctx (AP_aux (apat_aux, env, l)) cval case_label =
      | CT_list ctyp ->
         let hd_setup, hd_cleanup, ctx = compile_match ctx hd_apat (V_call (List_hd, [cval])) case_label in
         let tl_setup, tl_cleanup, ctx = compile_match ctx tl_apat (V_call (List_tl, [cval])) case_label in
-        [ijump (V_call (Eq, [cval; V_lit (VL_null, CT_list ctyp)])) case_label] @ hd_setup @ tl_setup, tl_cleanup @ hd_cleanup, ctx
+        [ijump l (V_call (Eq, [cval; V_lit (VL_empty_list, CT_list ctyp)])) case_label] @ hd_setup @ tl_setup, tl_cleanup @ hd_cleanup, ctx
      | _ ->
         raise (Reporting.err_general l "Tried to pattern match cons on non list type")
      end
 
-  | AP_nil _ -> [ijump (V_call (Neq, [cval; V_lit (VL_null, ctyp)])) case_label], [], ctx
+  | AP_nil _ -> [ijump l (V_call (Neq, [cval; V_lit (VL_empty_list, ctyp)])) case_label], [], ctx
 
 let unit_cval = V_lit (VL_unit, CT_unit)
 
@@ -633,7 +641,7 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) =
          destructure
          @ (if not trivial_guard then
               guard_setup @ [idecl CT_bool gs; guard_call (CL_id (gs, CT_bool))] @ guard_cleanup
-              @ [iif (V_call (Bnot, [V_id (gs, CT_bool)])) (destructure_cleanup @ [igoto case_label]) [] CT_unit]
+              @ [iif l (V_call (Bnot, [V_id (gs, CT_bool)])) (destructure_cleanup @ [igoto case_label]) [] CT_unit]
             else [])
          @ body_setup @ [body_call (CL_id (case_return_id, ctyp))] @ body_cleanup @ destructure_cleanup
          @ [igoto finish_match_label]
@@ -674,7 +682,7 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) =
          destructure @ [icomment "end destructuring"]
          @ (if not trivial_guard then
               guard_setup @ [idecl CT_bool gs; guard_call (CL_id (gs, CT_bool))] @ guard_cleanup
-              @ [ijump (V_call (Bnot, [V_id (gs, CT_bool)])) try_label]
+              @ [ijump l (V_call (Bnot, [V_id (gs, CT_bool)])) try_label]
               @ [icomment "end guard"]
             else [])
          @ body_setup @ [body_call (CL_id (try_return_id, ctyp))] @ body_cleanup @ destructure_cleanup
@@ -685,7 +693,7 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) =
      assert (ctyp_equal ctyp (ctyp_of_typ ctx typ));
      [idecl ctyp try_return_id;
       itry_block (aexp_setup @ [aexp_call (CL_id (try_return_id, ctyp))] @ aexp_cleanup);
-      ijump (V_call (Bnot, [V_id (have_exception, CT_bool)])) handled_exception_label]
+      ijump l (V_call (Bnot, [V_id (have_exception, CT_bool)])) handled_exception_label]
      @ List.concat (List.map compile_case cases)
      @ [igoto fallthrough_label;
         ilabel handled_exception_label;
@@ -707,7 +715,7 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) =
        in
        let setup, cval, cleanup = compile_aval l ctx aval in
        setup,
-       (fun clexp -> iif cval
+       (fun clexp -> iif l cval
                          (compile_branch then_aexp clexp)
                          (compile_branch else_aexp clexp)
                          if_ctyp),
@@ -742,7 +750,7 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) =
      let gs = ngensym () in
      left_setup
      @ [ idecl CT_bool gs;
-         iif cval
+         iif l cval
              (right_setup @ [call (CL_id (gs, CT_bool))] @ right_cleanup)
              [icopy l (CL_id (gs, CT_bool)) (V_lit (VL_bool false, CT_bool))]
              CT_bool ]
@@ -755,7 +763,7 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) =
      let gs = ngensym () in
      left_setup
      @ [ idecl CT_bool gs;
-         iif cval
+         iif l cval
              [icopy l (CL_id (gs, CT_bool)) (V_lit (VL_bool true, CT_bool))]
              (right_setup @ [call (CL_id (gs, CT_bool))] @ right_cleanup)
              CT_bool ]
@@ -813,7 +821,7 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) =
      @ [iblock (cond_setup
                 @ [cond_call (CL_id (gs, CT_bool))]
                 @ cond_cleanup
-                @ [ijump loop_test loop_end_label]
+                @ [ijump l loop_test loop_end_label]
                 @ body_setup
                 @ [body_call (CL_id (unit_gs, CT_unit))]
                 @ body_cleanup
@@ -838,7 +846,7 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) =
                 @ cond_setup
                 @ [cond_call (CL_id (gs, CT_bool))]
                 @ cond_cleanup
-                @ [ijump loop_test loop_end_label]
+                @ [ijump l loop_test loop_end_label]
                 @ [igoto loop_start_label])]
      @ [ilabel loop_end_label],
      (fun clexp -> icopy l clexp unit_cval),
@@ -869,7 +877,7 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) =
   | AE_throw (aval, typ) ->
      (* Cleanup info will be handled by fix_exceptions *)
      let throw_setup, cval, _ = compile_aval l ctx aval in
-     throw_setup @ [ithrow cval],
+     throw_setup @ [ithrow l cval],
      (fun clexp -> icomment "unreachable after throw"),
      []
 
@@ -927,21 +935,29 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) =
 
      let loop_var = name loop_var in
 
+     let loop_body prefix continue =
+       prefix
+       @ [iblock ([ijump l (V_call ((if is_inc then Igt else Ilt), [V_id (loop_var, CT_fint 64); V_id (to_gs, CT_fint 64)])) loop_end_label]
+                  @ body_setup
+                  @ [body_call (CL_id (body_gs, CT_unit))]
+                  @ body_cleanup
+                  @ [icopy l (CL_id (loop_var, (CT_fint 64)))
+                       (V_call ((if is_inc then Iadd else Isub), [V_id (loop_var, CT_fint 64); V_id (step_gs, CT_fint 64)]))]
+                  @ continue ())]
+     in
+     (* We can either generate an actual loop body for C, or unroll the body for SMT *)
+     let actual = loop_body [ilabel loop_start_label] (fun () -> [igoto loop_start_label]) in
+     let rec unroll max n = loop_body [] (fun () -> if n < max then unroll max (n + 1) else [imatch_failure ()]) in
+     let body = match C.unroll_loops () with Some times -> unroll times 0 | None -> actual in
+
      variable_init from_gs from_setup from_call from_cleanup
      @ variable_init to_gs to_setup to_call to_cleanup
      @ variable_init step_gs step_setup step_call step_cleanup
      @ [iblock ([idecl (CT_fint 64) loop_var;
                  icopy l (CL_id (loop_var, (CT_fint 64))) (V_id (from_gs, CT_fint 64));
-                 idecl CT_unit body_gs;
-                 iblock ([ilabel loop_start_label]
-                         @ [ijump (V_call ((if is_inc then Igt else Ilt), [V_id (loop_var, CT_fint 64); V_id (to_gs, CT_fint 64)])) loop_end_label]
-                         @ body_setup
-                         @ [body_call (CL_id (body_gs, CT_unit))]
-                         @ body_cleanup
-                         @ [icopy l (CL_id (loop_var, (CT_fint 64)))
-                                  (V_call ((if is_inc then Iadd else Isub), [V_id (loop_var, CT_fint 64); V_id (step_gs, CT_fint 64)]))]
-                         @ [igoto loop_start_label]);
-                 ilabel loop_end_label])],
+                 idecl CT_unit body_gs]
+                @ body
+                @ [ilabel loop_end_label])],
      (fun clexp -> icopy l clexp unit_cval),
      []
 
@@ -1032,19 +1048,23 @@ let fix_exception_block ?return:(return=None) ctx instrs =
        before
        @ [iblock (rewrite_exception (historic @ before) instrs)]
        @ rewrite_exception (historic @ before) after
-    | before, I_aux (I_if (cval, then_instrs, else_instrs, ctyp), _) :: after ->
+    | before, I_aux (I_if (cval, then_instrs, else_instrs, ctyp), (_, l)) :: after ->
        let historic = historic @ before in
        before
-       @ [iif cval (rewrite_exception historic then_instrs) (rewrite_exception historic else_instrs) ctyp]
+       @ [iif l cval (rewrite_exception historic then_instrs) (rewrite_exception historic else_instrs) ctyp]
        @ rewrite_exception historic after
     | before, I_aux (I_throw cval, (_, l)) :: after ->
        before
        @ [icopy l (CL_id (current_exception, cval_ctyp cval)) cval;
           icopy l (CL_id (have_exception, CT_bool)) (V_lit (VL_bool true, CT_bool))]
+       @ (if !opt_track_throw then
+            let loc_string = Reporting.short_loc_to_string l in
+            [icopy l (CL_id (throw_location, CT_string)) (V_lit (VL_string loc_string, CT_string))]
+          else [])
        @ generate_cleanup (historic @ before)
        @ [igoto end_block_label]
        @ rewrite_exception (historic @ before) after
-    | before, (I_aux (I_funcall (x, _, f, args), _) as funcall) :: after ->
+    | before, (I_aux (I_funcall (x, _, f, args), (_, l)) as funcall) :: after ->
        let effects = match Env.get_val_spec (fst f) ctx.tc_env with
          | _, Typ_aux (Typ_fn (_, _, effects), _) -> effects
          | exception (Type_error _) -> no_effect (* nullary union constructor, so no val spec *)
@@ -1053,7 +1073,7 @@ let fix_exception_block ?return:(return=None) ctx instrs =
        if has_effect effects BE_escape then
          before
          @ [funcall;
-            iif (V_id (have_exception, CT_bool)) (generate_cleanup (historic @ before) @ [igoto end_block_label]) [] CT_unit]
+            iif l (V_id (have_exception, CT_bool)) (generate_cleanup (historic @ before) @ [igoto end_block_label]) [] CT_unit]
          @ rewrite_exception (historic @ before) after
        else
          before @ funcall :: rewrite_exception (historic @ before) after
@@ -1147,10 +1167,10 @@ let fix_early_return ret instrs =
        before
        @ [iblock (rewrite_return (historic @ before) instrs)]
        @ rewrite_return (historic @ before) after
-    | before, I_aux (I_if (cval, then_instrs, else_instrs, ctyp), _) :: after ->
+    | before, I_aux (I_if (cval, then_instrs, else_instrs, ctyp), (_, l)) :: after ->
        let historic = historic @ before in
        before
-       @ [iif cval (rewrite_return historic then_instrs) (rewrite_return historic else_instrs) ctyp]
+       @ [iif l cval (rewrite_return historic then_instrs) (rewrite_return historic else_instrs) ctyp]
        @ rewrite_return historic after
     | before, I_aux (I_return cval, (_, l)) :: after ->
        let cleanup_label = label "cleanup_" in
@@ -1211,7 +1231,7 @@ let compile_funcl ctx id pat guard exp =
 
   let guard_instrs = match guard with
     | Some guard ->
-       let guard_aexp = ctx.optimize_anf ctx (no_shadow (pat_ids pat) (anf guard)) in
+       let guard_aexp = C.optimize_anf ctx (no_shadow (pat_ids pat) (anf guard)) in
        let guard_setup, guard_call, guard_cleanup = compile_aexp ctx guard_aexp in
        let guard_label = label "guard_" in
        let gs = ngensym () in
@@ -1220,7 +1240,7 @@ let compile_funcl ctx id pat guard exp =
             @ guard_setup
             @ [guard_call (CL_id (gs, CT_bool))]
             @ guard_cleanup
-            @ [ijump (V_id (gs, CT_bool)) guard_label;
+            @ [ijump (id_loc id) (V_id (gs, CT_bool)) guard_label;
                imatch_failure ();
                ilabel guard_label]
        )]
@@ -1228,7 +1248,7 @@ let compile_funcl ctx id pat guard exp =
   in
 
   (* Optimize and compile the expression to ANF. *)
-  let aexp = ctx.optimize_anf ctx (no_shadow (pat_ids pat) (anf exp)) in
+  let aexp = C.optimize_anf ctx (no_shadow (pat_ids pat) (anf exp)) in
 
   let setup, call, cleanup = compile_aexp ctx aexp in
   let destructure, destructure_cleanup =
@@ -1280,7 +1300,7 @@ and compile_def' n total ctx = function
   | DEF_reg_dec (DEC_aux (DEC_reg (_, _, typ, id), _)) ->
      [CDEF_reg_dec (id, ctyp_of_typ ctx typ, [])], ctx
   | DEF_reg_dec (DEC_aux (DEC_config (id, typ, exp), _)) ->
-     let aexp = ctx.optimize_anf ctx (no_shadow IdSet.empty (anf exp)) in
+     let aexp = C.optimize_anf ctx (no_shadow IdSet.empty (anf exp)) in
      let setup, call, cleanup = compile_aexp ctx aexp in
      let instrs = setup @ [call (CL_id (name id, ctyp_of_typ ctx typ))] @ cleanup in
      [CDEF_reg_dec (id, ctyp_of_typ ctx typ, instrs)], ctx
@@ -1290,13 +1310,19 @@ and compile_def' n total ctx = function
 
   | DEF_spec (VS_aux (VS_val_spec (_, id, _, _), _)) ->
      let quant, Typ_aux (fn_typ, _) = Env.get_val_spec id ctx.tc_env in
+     let extern =
+       if Env.is_extern id ctx.tc_env "c" then
+         Some (Env.get_extern id ctx.tc_env "c")
+       else
+         None
+     in
      let arg_typs, ret_typ = match fn_typ with
        | Typ_fn (arg_typs, ret_typ, _) -> arg_typs, ret_typ
        | _ -> assert false
      in
      let ctx' = { ctx with local_env = add_typquant (id_loc id) quant ctx.local_env } in
      let arg_ctyps, ret_ctyp = List.map (ctyp_of_typ ctx') arg_typs, ctyp_of_typ ctx' ret_typ in
-     [CDEF_spec (id, arg_ctyps, ret_ctyp)],
+     [CDEF_spec (id, extern, arg_ctyps, ret_ctyp)],
      { ctx with valspecs = Bindings.add id (arg_ctyps, ret_ctyp) ctx.valspecs }
 
   | DEF_fundef (FD_aux (FD_function (_, _, _, [FCL_aux (FCL_Funcl (id, Pat_aux (Pat_exp (pat, exp), _)), _)]), _)) ->
@@ -1323,7 +1349,7 @@ and compile_def' n total ctx = function
 
   | DEF_val (LB_aux (LB_val (pat, exp), _)) ->
      let ctyp = ctyp_of_typ ctx (typ_of_pat pat) in
-     let aexp = ctx.optimize_anf ctx (no_shadow IdSet.empty (anf exp)) in
+     let aexp = C.optimize_anf ctx (no_shadow IdSet.empty (anf exp)) in
      let setup, call, cleanup = compile_aexp ctx aexp in
      let apat = anf_pat ~global:true pat in
      let gs = ngensym () in
@@ -1544,12 +1570,6 @@ let sort_ctype_defs cdefs =
   ctype_defs @ cdefs
 
 let compile_ast ctx (Defs defs) =
-  let assert_vs = Initial_check.extern_of_string (mk_id "sail_assert") "(bool, string) -> unit" in
-  let exit_vs = Initial_check.extern_of_string (mk_id "sail_exit") "unit -> unit" in
-  let cons_vs = Initial_check.extern_of_string (mk_id "sail_cons") "forall ('a : Type). ('a, list('a)) -> list('a)" in
-
-  let ctx = { ctx with tc_env = snd (Type_error.check ctx.tc_env (Defs [assert_vs; exit_vs; cons_vs])) } in
-
   if !opt_memo_cache then
     (try
        if Sys.is_directory "_sbuild" then
@@ -1568,3 +1588,12 @@ let compile_ast ctx (Defs defs) =
   let cdefs, ctx = specialize_variants ctx [] cdefs in
   let cdefs = sort_ctype_defs cdefs in
   cdefs, ctx
+
+end
+
+let add_special_functions env =
+  let assert_vs = Initial_check.extern_of_string (mk_id "sail_assert") "(bool, string) -> unit" in
+  let exit_vs = Initial_check.extern_of_string (mk_id "sail_exit") "unit -> unit" in
+  let cons_vs = Initial_check.extern_of_string (mk_id "sail_cons") "forall ('a : Type). ('a, list('a)) -> list('a)" in
+
+  snd (Type_error.check env (Defs [assert_vs; exit_vs; cons_vs]))
diff --git a/src/jib/jib_compile.mli b/src/jib/jib_compile.mli
index 273e9e03..9014d8f7 100644
--- a/src/jib/jib_compile.mli
+++ b/src/jib/jib_compile.mli
@@ -58,53 +58,69 @@ open Type_check
 
 (** This forces all integer struct fields to be represented as
    int64_t. Specifically intended for the various TLB structs in the
-   ARM v8.5 spec. *)
+   ARM v8.5 spec. It is unsound in general. *)
 val optimize_aarch64_fast_struct : bool ref
 
+(** If true (default) track the location of the last exception thrown,
+   useful for debugging C but we want to turn it off for SMT generation
+   where we can't use strings *)
+val opt_track_throw : bool ref
+ 
 (** {2 Jib context} *)
 
-(** Context for compiling Sail to Jib. We need to pass a (global)
-   typechecking environment given by checking the full AST. We have to
-   provide a conversion function from Sail types into Jib types, as
-   well as a function that optimizes ANF expressions (which can just
-   be the identity function) *)
+(** Dynamic context for compiling Sail to Jib. We need to pass a
+   (global) typechecking environment given by checking the full
+   AST. *)
 type ctx =
   { records : (ctyp Jib_util.UBindings.t) Bindings.t;
     enums : IdSet.t Bindings.t;
     variants : (ctyp Jib_util.UBindings.t) Bindings.t;
     valspecs : (ctyp list * ctyp) Bindings.t;
-    tc_env : Env.t;
     local_env : Env.t;
+    tc_env : Env.t;
     locals : (mut * ctyp) Bindings.t;
     letbinds : int list;
     no_raw : bool;
-    convert_typ : ctx -> typ -> ctyp;
-    optimize_anf : ctx -> typ aexp -> typ aexp;
-    (** If false (default), function arguments must match the function
-       type exactly. If true, they can be more specific. *)
-    specialize_calls : bool;
-    (** If false (default), will ensure that fixed size bitvectors are
-       specifically less that 64-bits. If true this restriction will
-       be ignored. *)
-    ignore_64 : bool;
-    (** If false (default) we won't generate any V_struct values *)
-    struct_value : bool;
-    (** Allow real literals *)
-    use_real : bool;
   }
 
-val initial_ctx :
-  convert_typ:(ctx -> typ -> ctyp) ->
-  optimize_anf:(ctx -> typ aexp -> typ aexp) ->
-  Env.t ->
-  ctx
+val initial_ctx : Env.t -> ctx
 
 (** {2 Compilation functions} *)
 
-(** Compile a Sail definition into a Jib definition. The first two
-   arguments are is the current definition number and the total number
-   of definitions, and can be used to drive a progress bar (see
-   Util.progress). *)
-val compile_def : int -> int -> ctx -> tannot def -> cdef list * ctx
+(** The Config module specifies static configuration for compiling
+   Sail into Jib.  We have to provide a conversion function from Sail
+   types into Jib types, as well as a function that optimizes ANF
+   expressions (which can just be the identity function) *)
+module type Config = sig
+  val convert_typ : ctx -> typ -> ctyp
+  val optimize_anf : ctx -> typ aexp -> typ aexp
+  (** Unroll all for loops a bounded number of times. Used for SMT
+       generation. *)
+  val unroll_loops : unit -> int option
+  (** If false, function arguments must match the function
+       type exactly. If true, they can be more specific. *)
+  val specialize_calls : bool
+  (** If false, will ensure that fixed size bitvectors are
+       specifically less that 64-bits. If true this restriction will
+       be ignored. *)
+  val ignore_64 : bool
+  (** If false we won't generate any V_struct values *)
+  val struct_value : bool
+  (** Allow real literals *)
+  val use_real : bool
+end
+
+module Make(C: Config) : sig
+  (** Compile a Sail definition into a Jib definition. The first two
+       arguments are is the current definition number and the total
+       number of definitions, and can be used to drive a progress bar
+       (see Util.progress). *)
+  val compile_def : int -> int -> ctx -> tannot def -> cdef list * ctx
+
+  val compile_ast : ctx -> tannot defs -> cdef list * ctx
+end
 
-val compile_ast : ctx -> tannot defs -> cdef list * ctx
+(** Adds some special functions to the environment that are used to
+   convert several Sail language features, these are sail_assert,
+   sail_exit, and sail_cons. *)
+val add_special_functions : Env.t -> Env.t
diff --git a/src/jib/jib_ir.ml b/src/jib/jib_ir.ml
index c5f2b20a..4bf726aa 100644
--- a/src/jib/jib_ir.ml
+++ b/src/jib/jib_ir.ml
@@ -69,7 +69,9 @@ let string_of_name =
      "return" ^ ssa_num n
   | Current_exception n ->
      "current_exception" ^ ssa_num n
-
+  | Throw_location n ->
+     "throw_location" ^ ssa_num n
+    
 let rec string_of_clexp = function
   | CL_id (id, ctyp) -> string_of_name id
   | CL_field (clexp, field) -> string_of_clexp clexp ^ "." ^ string_of_uid field
@@ -107,7 +109,9 @@ module Ir_formatter = struct
       | I_label label ->
          C.output_label_instr buf label_map label
       | I_jump (cval, label) ->
-         add_instr n buf indent (C.keyword "jump" ^ " " ^ C.value cval ^ " " ^ C.string_of_label (StringMap.find label label_map))
+         add_instr n buf indent (C.keyword "jump" ^ " " ^ C.value cval ^ " "
+                                 ^ C.keyword "goto" ^ " " ^ C.string_of_label (StringMap.find label label_map)
+                                 ^ " ` \"" ^ Reporting.short_loc_to_string l ^ "\"")
       | I_goto label ->
          add_instr n buf indent (C.keyword "goto" ^ " " ^ C.string_of_label (StringMap.find label label_map))
       | I_match_failure ->
@@ -151,8 +155,10 @@ module Ir_formatter = struct
     let output_def buf = function
       | CDEF_reg_dec (id, ctyp, _) ->
          Buffer.add_string buf (sprintf "%s %s : %s" (C.keyword "register") (zencode_id id) (C.typ ctyp))
-      | CDEF_spec (id, ctyps, ctyp) ->
+      | CDEF_spec (id, None, ctyps, ctyp) ->
          Buffer.add_string buf (sprintf "%s %s : (%s) ->  %s" (C.keyword "val") (zencode_id id) (Util.string_of_list ", " C.typ ctyps) (C.typ ctyp));
+      | CDEF_spec (id, Some extern, ctyps, ctyp) ->
+         Buffer.add_string buf (sprintf "%s %s = \"%s\" : (%s) ->  %s" (C.keyword "val") (zencode_id id) extern (Util.string_of_list ", " C.typ ctyps) (C.typ ctyp));
       | CDEF_fundef (id, ret, args, instrs) ->
          let instrs = C.modify_instrs instrs in
          let label_map = C.make_label_map instrs in
@@ -244,10 +250,10 @@ let () =
   let open Interactive in
   let open Jib_interactive in
 
-  (fun arg ->
+  ArgString ("(val|register)? identifier", fun arg -> Action (fun () ->
     let is_def id = function
       | CDEF_fundef (id', _, _, _) -> Id.compare id id' = 0
-      | CDEF_spec (id', _, _) -> Id.compare id (prepend_id "val " id') = 0
+      | CDEF_spec (id', _, _, _) -> Id.compare id (prepend_id "val " id') = 0
       | CDEF_reg_dec (id', _, _) -> Id.compare id (prepend_id "register " id') = 0
       | _ -> false
     in
@@ -258,12 +264,12 @@ let () =
        let buf = Buffer.create 256 in
        with_colors (fun () -> Flat_ir_formatter.output_def buf cdef);
        print_endline (Buffer.contents buf)
-  ) |> Interactive.(register_command ~name:"ir" ~help:(sprintf ":ir %s - Print the ir representation of a toplevel definition" (arg "(val|register)? identifier")));
+  )) |> Interactive.register_command ~name:"ir" ~help:"Print the ir representation of a toplevel definition";
 
-  (fun file ->
+  ArgString ("file", fun file -> Action (fun () ->
     let buf = Buffer.create 256 in
     let out_chan = open_out file in
     Flat_ir_formatter.output_defs buf !ir;
     output_string out_chan (Buffer.contents buf);
     close_out out_chan
-  ) |> Interactive.(register_command ~name:"dump_ir" ~help:(sprintf ":dump_ir %s - Dump the ir to a file" (arg "file")))
+  )) |> Interactive.register_command ~name:"dump_ir" ~help:"Dump the ir to a file"
diff --git a/src/jib/jib_optimize.ml b/src/jib/jib_optimize.ml
index 323f3cd0..e0f3bf0d 100644
--- a/src/jib/jib_optimize.ml
+++ b/src/jib/jib_optimize.ml
@@ -102,10 +102,10 @@ let rec flatten_instrs = function
   | I_aux ((I_block block | I_try_block block), _) :: instrs ->
      flatten_instrs block @ flatten_instrs instrs
 
-  | I_aux (I_if (cval, then_instrs, else_instrs, _), _) :: instrs ->
+  | I_aux (I_if (cval, then_instrs, else_instrs, _), (_, l)) :: instrs ->
      let then_label = label "then_" in
      let endif_label = label "endif_" in
-     [ijump cval then_label]
+     [ijump l cval then_label]
      @ flatten_instrs else_instrs
      @ [igoto endif_label]
      @ [ilabel then_label]
@@ -153,7 +153,7 @@ let unique_per_function_ids cdefs =
     | CDEF_reg_dec (id, ctyp, instrs) -> CDEF_reg_dec (id, ctyp, unique_instrs i instrs)
     | CDEF_type ctd -> CDEF_type ctd
     | CDEF_let (n, bindings, instrs) -> CDEF_let (n, bindings, unique_instrs i instrs)
-    | CDEF_spec (id, ctyps, ctyp) -> CDEF_spec (id, ctyps, ctyp)
+    | CDEF_spec (id, extern, ctyps, ctyp) -> CDEF_spec (id, extern, ctyps, ctyp)
     | CDEF_fundef (id, heap_return, args, instrs) -> CDEF_fundef (id, heap_return, args, unique_instrs i instrs)
     | CDEF_startup (id, instrs) -> CDEF_startup (id, unique_instrs i instrs)
     | CDEF_finish (id, instrs) -> CDEF_finish (id, unique_instrs i instrs)
@@ -162,7 +162,6 @@ let unique_per_function_ids cdefs =
 
 let rec cval_subst id subst = function
   | V_id (id', ctyp) -> if Name.compare id id' = 0 then subst else V_id (id', ctyp)
-  | V_ref (reg_id, ctyp) -> V_ref (reg_id, ctyp)
   | V_lit (vl, ctyp) -> V_lit (vl, ctyp)
   | V_call (op, cvals) -> V_call (op, List.map (cval_subst id subst) cvals)
   | V_field (cval, field) -> V_field (cval_subst id subst cval, field)
@@ -174,7 +173,6 @@ let rec cval_subst id subst = function
 
 let rec cval_map_id f = function
   | V_id (id, ctyp) -> V_id (f id, ctyp)
-  | V_ref (id, ctyp) -> V_ref (f id, ctyp)
   | V_lit (vl, ctyp) -> V_lit (vl, ctyp)
   | V_call (call, cvals) -> V_call (call, List.map (cval_map_id f) cvals)
   | V_field (cval, field) -> V_field (cval_map_id f cval, field)
@@ -249,6 +247,7 @@ let ssa_name i = function
   | Name (id, _) -> Name (id, i)
   | Have_exception _ -> Have_exception i
   | Current_exception _ -> Current_exception i
+  | Throw_location _ -> Throw_location i
   | Return _ -> Return i
 
 let inline cdefs should_inline instrs =
@@ -347,6 +346,15 @@ let rec remove_pointless_goto = function
      instr :: remove_pointless_goto instrs
   | [] -> []
 
+let rec remove_pointless_exit = function
+  | I_aux (I_end id, aux) :: I_aux (I_end _, _) :: instrs  ->
+     I_aux (I_end id, aux) :: remove_pointless_exit instrs
+  | I_aux (I_end id, aux) :: I_aux (I_undefined _, _) :: instrs  ->
+     I_aux (I_end id, aux) :: remove_pointless_exit instrs
+  | instr :: instrs ->
+     instr :: remove_pointless_exit instrs
+  | [] -> []
+
 module StringSet = Set.Make(String)
 
 let rec get_used_labels set = function
@@ -364,7 +372,6 @@ let remove_unused_labels instrs =
   in
   go [] instrs
 
-
 let remove_dead_after_goto instrs =
   let rec go acc = function
     | (I_aux (I_goto _, _) as instr) :: instrs -> go_dead (instr :: acc) instrs
@@ -379,7 +386,7 @@ let remove_dead_after_goto instrs =
 
 let rec remove_dead_code instrs =
   let instrs' =
-    instrs |> remove_unused_labels |> remove_pointless_goto |> remove_dead_after_goto
+    instrs |> remove_unused_labels |> remove_pointless_goto |> remove_dead_after_goto |> remove_pointless_exit
   in
   if List.length instrs' < List.length instrs then
     remove_dead_code instrs'
@@ -398,7 +405,7 @@ let remove_tuples cdefs ctx =
        CTSet.add ctyp (List.fold_left CTSet.union CTSet.empty (List.map all_tuples ctyps))
     | CT_struct (_, id_ctyps) | CT_variant (_, id_ctyps) ->
        List.fold_left (fun cts (_, ctyp) -> CTSet.union (all_tuples ctyp) cts) CTSet.empty id_ctyps
-    | CT_list ctyp | CT_vector (_, ctyp) | CT_ref ctyp ->
+    | CT_list ctyp | CT_vector (_, ctyp) | CT_fvector (_, _, ctyp) | CT_ref ctyp ->
        all_tuples ctyp
     | CT_lint | CT_fint _ | CT_lbits _ | CT_sbits _ | CT_fbits _ | CT_constant _
       | CT_unit | CT_bool | CT_real | CT_bit | CT_poly | CT_string | CT_enum _ ->
@@ -409,7 +416,7 @@ let remove_tuples cdefs ctx =
        1 + List.fold_left (fun d ctyp -> max d (tuple_depth ctyp)) 0 ctyps
     | CT_struct (_, id_ctyps) | CT_variant (_, id_ctyps) ->
        List.fold_left (fun d (_, ctyp) -> max (tuple_depth ctyp) d) 0 id_ctyps
-    | CT_list ctyp | CT_vector (_, ctyp) | CT_ref ctyp ->
+    | CT_list ctyp | CT_vector (_, ctyp) | CT_fvector (_, _, ctyp) | CT_ref ctyp ->
        tuple_depth ctyp
     | CT_lint | CT_fint _ | CT_lbits _ | CT_sbits _ | CT_fbits _ | CT_constant _
       | CT_unit | CT_bool | CT_real | CT_bit | CT_poly | CT_string | CT_enum _ ->
@@ -426,6 +433,7 @@ let remove_tuples cdefs ctx =
        CT_variant (id, List.map (fun (id, ctyp) -> id, fix_tuples ctyp) id_ctyps)
     | CT_list ctyp -> CT_list (fix_tuples ctyp)
     | CT_vector (d, ctyp) -> CT_vector (d, fix_tuples ctyp)
+    | CT_fvector (n, d, ctyp) -> CT_fvector (n, d, fix_tuples ctyp)
     | CT_ref ctyp -> CT_ref (fix_tuples ctyp)
     | (CT_lint | CT_fint _ | CT_lbits _ | CT_sbits _ | CT_fbits _ | CT_constant _
        | CT_unit | CT_bool | CT_real | CT_bit | CT_poly | CT_string | CT_enum _) as ctyp ->
@@ -433,7 +441,6 @@ let remove_tuples cdefs ctx =
   in
   let rec fix_cval = function
     | V_id (id, ctyp) -> V_id (id, ctyp)
-    | V_ref (id, ctyp) -> V_ref (id, ctyp)
     | V_lit (vl, ctyp) -> V_lit (vl, ctyp)
     | V_ctor_kind (cval, id, unifiers, ctyp) ->
        V_ctor_kind (fix_cval cval, id, unifiers, ctyp)
diff --git a/src/jib/jib_smt.ml b/src/jib/jib_smt.ml
index fbaf8d3f..81b876a4 100644
--- a/src/jib/jib_smt.ml
+++ b/src/jib/jib_smt.ml
@@ -73,6 +73,8 @@ 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
@@ -89,6 +91,8 @@ type ctx = {
     pragma_l : Ast.l;
     arg_stack : (int * string) Stack.t;
     ast : Type_check.tannot defs;
+    shared : ctyp Bindings.t;
+    preserved : IdSet.t;
     events : smt_exp Stack.t EventMap.t ref;
     node : int;
     pathcond : smt_exp Lazy.t;
@@ -114,6 +118,8 @@ let initial_ctx () = {
     pragma_l = Parse_ast.Unknown;
     arg_stack = Stack.create ();
     ast = Defs [];
+    shared = Bindings.empty;
+    preserved = IdSet.empty;
     events = ref EventMap.empty;
     node = -1;
     pathcond = lazy (Bool_lit true);
@@ -129,6 +135,19 @@ let event_stack ctx ev =
      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
@@ -179,6 +198,8 @@ let rec smt_ctyp ctx = function
      | _ -> 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"
 
@@ -188,21 +209,17 @@ let rec smt_ctyp ctx = function
    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 open Sail_lib in
     let x = Big_int.to_int x in
-    if sz mod 4 = 0 then
-      let hex = Printf.sprintf "%X" x in
-      let padding = String.make (sz / 4 - String.length hex) '0' in
-      Hex (padding ^ hex)
-    else
-      let bin = Printf.sprintf "%X" x |> list_of_string |> List.map hex_char |> List.concat in
-      let _, bin = Util.take_drop (function B0 -> true | B1 -> false) bin in
-      let bin = String.concat "" (List.map string_of_bit bin) in
-      let padding = String.make (sz - String.length bin) '0' in
-      Bin (padding ^ bin)
+    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 open Sail_lib in
     let y = ref x in
     let bin = ref [] in
     while (not (Big_int.equal !y Big_int.zero)) do
@@ -210,14 +227,13 @@ let bvpint sz x =
       bin := (if Big_int.equal m Big_int.zero then B0 else B1) :: !bin;
       y := q
     done;
-    let bin = String.concat "" (List.map string_of_bit !bin) in
-    let padding_size = sz - String.length bin in
+    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 = String.make (sz - String.length bin) '0' in
-    Bin (padding ^ bin)
+    let padding = List.init padding_size (fun _ -> B0) in
+    Bitvec_lit (padding @ !bin)
   ) else failwith "Invalid bvpint"
 
 let bvint sz x =
@@ -226,22 +242,68 @@ let bvint sz x =
   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_lbits _, CT_fbits (n, _) ->
+     unsigned_size ctx n (lbits_size ctx) (Fn ("contents", [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 smt_value ctx vl ctyp =
+let rec smt_value ctx vl ctyp =
   let open Value2 in
   match vl, ctyp with
-  | VL_bits (bs, true), CT_fbits (n, _) ->
-     (* FIXME: Output the correct number of bits in Jib_compile *)
-     begin match Sail2_values.hexstring_of_bits (List.rev (Util.take n (List.rev bs))) with
-     | Some s -> Hex (Xstring.implode s)
-     | None -> Bin (Xstring.implode (List.map Sail2_values.bitU_char (List.rev (Util.take n (List.rev bs)))))
-     end
+  | 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 Sail2_values.B0, CT_bit -> Bin "0"
-  | VL_bit Sail2_values.B1, CT_bit -> Bin "1"
+  | VL_bit b, CT_bit -> Bitvec_lit [b]
   | VL_unit, _ -> Enum "unit"
   | VL_string str, _ ->
      ctx.use_string := true;
@@ -252,7 +314,21 @@ let smt_value ctx vl ctyp =
        Fn ("-", [Real_lit (String.sub str 1 (String.length str - 1))])
      else
        Real_lit str
-  | vl, _ -> failwith ("Cannot translate literal to SMT: " ^ string_of_value vl)
+  | 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
@@ -264,6 +340,7 @@ let rec smt_cval ctx cval =
      | V_id (Name (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)
@@ -271,8 +348,6 @@ let rec smt_cval ctx cval =
         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 (Bit_to_bool, [cval]) ->
-        Fn ("=", [smt_cval ctx cval; Bin "1"])
      | V_call (Eq, [cval1; cval2]) ->
         Fn ("=", [smt_cval ctx cval1; smt_cval ctx cval2])
      | V_call (Bnot, [cval]) ->
@@ -281,14 +356,18 @@ let rec smt_cval ctx cval =
         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 (union, field) ->
-        begin match cval_ctyp union with
+     | V_field (record, field) ->
+        begin match cval_ctyp record with
         | CT_struct (struct_id, _) ->
-           Fn (zencode_upper_id struct_id ^ "_" ^ zencode_uid field, [smt_cval ctx union])
+           Field (zencode_upper_id struct_id ^ "_" ^ zencode_uid field, smt_cval ctx record)
         | _ -> failwith "Field for non-struct type"
         end
      | V_struct (fields, ctyp) ->
@@ -297,43 +376,18 @@ let rec smt_cval ctx cval =
            let set_field (field, cval) =
              match Util.assoc_compare_opt UId.compare field field_ctyps with
              | None -> failwith "Field type not found"
-             | Some ctyp when ctyp_equal (cval_ctyp cval) ctyp ->
-                smt_cval ctx cval
-             | _ -> failwith "Type mismatch when generating struct for SMT"
+             | Some ctyp ->
+                zencode_upper_id struct_id ^ "_" ^ zencode_uid field,
+                smt_conversion ctx (cval_ctyp cval) ctyp (smt_cval ctx cval)
            in
-           Fn (zencode_upper_id struct_id, List.map set_field fields)
+           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])
-     | V_ref (Name (id, _), _) ->
-        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
      | cval -> failwith ("Unrecognised cval " ^ string_of_cval cval)
 
-let add_event ctx ev smt =
-  let stack = event_stack ctx ev in
-  Stack.push (Fn ("=>", [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
-  )
-
 (**************************************************************************)
 (* 1. Generating SMT for Sail builtins                                    *)
 (**************************************************************************)
@@ -342,8 +396,8 @@ 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 ->
-     raise (Reporting.err_todo ctx.pragma_l
-       (Printf.sprintf "%s : (%s) -> %s" fn args (string_of_ctyp 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))
 
@@ -385,36 +439,6 @@ let builtin_gteq = builtin_int_comparison "bvsge" Big_int.greater_equal
 
 (* ***** Arithmetic operations: lib/arith.sail ***** *)
 
-(** [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); Bin "1"]),
-           (* 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 int_size ctx = function
   | CT_constant n -> required_width n
   | CT_fint sz -> sz
@@ -457,8 +481,9 @@ let builtin_negate_int ctx v ret_ctyp =
   | 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; Bin ("1" ^ String.make (int_size ctx ret_ctyp - 1) '0')]));
+     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 =
@@ -494,7 +519,7 @@ let builtin_abs_int ctx v ret_ctyp =
   | ctyp, _ ->
      let sz = int_size ctx ctyp in
      let smt = smt_cval ctx v in
-     Ite (Fn ("=", [Extract (sz - 1, sz -1, smt); Bin "1"]),
+     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)
 
@@ -531,6 +556,25 @@ let builtin_min_int ctx v1 v2 ret_ctyp =
           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
@@ -623,7 +667,7 @@ let builtin_sign_extend ctx vbits vlen ret_ctyp =
      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); Bin "1"]) 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)
@@ -658,14 +702,14 @@ let builtin_not_bits ctx v ret_ctyp =
   | _, _ -> 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 with
-  | CT_fbits (n, _), CT_fbits (m, _) ->
-     assert (n = m);
+  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 _, 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])])])
@@ -674,6 +718,7 @@ let builtin_bitwise fn ctx v1 v2 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
@@ -743,19 +788,29 @@ let builtin_length ctx v ret_ctyp =
   | _, _ -> 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 with
-  | CT_fbits (n, _), CT_constant i, CT_constant j ->
+  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_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 len = force_size ~checked:false ctx ctx.lbits_index (int_size ctx i_ctyp) (smt_cval ctx i) in
+     Fn ("Bits", [len; Fn ("bvand", [bvmask ctx len; unsigned_size ctx (lbits_size ctx) n (smt_cval ctx 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])
@@ -787,6 +842,21 @@ let builtin_vector_update ctx vec i x ret_ctyp =
 
   | _ -> 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])
+
+  | _ -> 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 ->
@@ -800,6 +870,9 @@ let builtin_unsigned ctx v ret_ctyp =
        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]))
+
   | ctyp, _ -> builtin_type_error ctx "unsigned" [v] (Some ret_ctyp)
 
 let builtin_signed ctx v ret_ctyp =
@@ -810,6 +883,9 @@ let builtin_signed ctx v ret_ctyp =
   | 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 =
@@ -818,6 +894,11 @@ let builtin_add_bits ctx v1 v2 ret_ctyp =
      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 =
@@ -866,6 +947,13 @@ let builtin_replicate_bits ctx v1 v2 ret_ctyp =
      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 =
@@ -928,13 +1016,18 @@ let builtin_get_slice_int ctx v1 v2 v3 ret_ctyp =
      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])])
+
   | _ -> 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); Bin "0"]),
+      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 (
@@ -1050,6 +1143,8 @@ let smt_builtin ctx name args 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
@@ -1072,8 +1167,9 @@ let smt_builtin ctx name args 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
-  | "or_bits", [v1; v2], _ -> builtin_or_bits 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
@@ -1084,6 +1180,7 @@ let smt_builtin ctx name args 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
@@ -1110,16 +1207,30 @@ let smt_builtin ctx name args ret_ctyp =
   | "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])
 
-  | _ -> failwith ("Unknown builtin " ^ name ^ " " ^ Util.string_of_list ", " string_of_ctyp (List.map cval_ctyp args) ^ " -> " ^ string_of_ctyp ret_ctyp)
+  | _ ->
+     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 ctx wk addr_size addr data_size data =
+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, ctx.node, Lazy.force ctx.pathcond, smt_cval ctx wk,
-              smt_cval ctx addr, smt_ctyp ctx (cval_ctyp addr), smt_cval ctx data, smt_ctyp ctx (cval_ctyp data))],
+  [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)
@@ -1133,11 +1244,19 @@ let builtin_write_mem_ea ctx wk addr_size addr data_size =
 
 let reads = ref (-1)
 
-let builtin_read_mem ctx rk addr_size addr data_size ret_ctyp =
+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, ctx.node, Lazy.force ctx.pathcond, smt_ctyp ctx ret_ctyp, smt_cval ctx rk,
-             smt_cval ctx addr, smt_ctyp ctx (cval_ctyp addr))],
+  [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)
@@ -1150,26 +1269,51 @@ let builtin_excl_res ctx =
 
 let barriers = ref (-1)
 
-let builtin_barrier ctx bk =
+let builtin_barrier l ctx bk =
   incr barriers;
   let name = "B" ^ string_of_int !barriers in
-  [Barrier (name, ctx.node, Lazy.force ctx.pathcond, smt_cval ctx bk)],
+  [Barrier {
+       name = name;
+       node = ctx.node;
+       active = Lazy.force ctx.pathcond;
+       kind = smt_cval ctx bk;
+       doc = loc_doc l
+  }],
   Enum "unit"
 
-let rec 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_lbits _, CT_fbits (n, _) ->
-     unsigned_size ctx n (lbits_size ctx) (Fn ("contents", [x]))
-  | _, _ -> failwith (Printf.sprintf "Cannot perform conversion from %s to %s" (string_of_ctyp from_ctyp) (string_of_ctyp to_ctyp))
+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
@@ -1205,143 +1349,144 @@ let rec generate_reg_decs ctx inits = function
 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))
 
-(** 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 ctyp_of_typ ctx typ =
-  let open Ast in
-  let open Type_check in
-  let open Jib_compile 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" ->
-     ctyp_of_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
+module SMT_config : 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
-           else
-             CT_lint
-     end
-
-  | Typ_app (id, [A_aux (A_typ typ, _)]) when string_of_id id = "list" ->
-     CT_list (ctyp_of_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, ctyp_of_typ ctx typ)
-
-  | Typ_app (id, [A_aux (A_typ typ, _)]) when string_of_id id = "register" ->
-     CT_ref (ctyp_of_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 (ctyp_of_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
-        ctyp_of_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))
+          | 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
 
-(**************************************************************************)
-(* 3. Optimization of primitives and literals                             *)
-(**************************************************************************)
+    | 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
 
-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
+    | 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
-    | AV_tuple avals -> AV_tuple (List.map (c_literal env l) avals)
-    | v -> v
-  in
-  map_aval c_literal
 
-let unroll_foreach ctx = function
+    | 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 ctyp_of_typ ctx (aexp_typ from_aexp), ctyp_of_typ ctx (aexp_typ to_aexp), ctyp_of_typ ctx (aexp_typ by_aexp), order with
+     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
@@ -1360,6 +1505,19 @@ let unroll_foreach ctx = function
      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 !opt_unroll_limit
+  let struct_value = true
+  let use_real = true
+end
+
+
 (**************************************************************************)
 (* 3. Generating SMT                                                      *)
 (**************************************************************************)
@@ -1414,7 +1572,7 @@ let smt_ssanode ctx cfg preds =
          pis ids None
      in
      match mux with
-     | None -> []
+     | None -> assert false
      | Some mux ->
         [Define_const (zencode_name id, smt_ctyp ctx ctyp, mux)]
 
@@ -1492,7 +1650,7 @@ let rec rmw_write = function
   | CL_id _ -> assert false
   | CL_tuple (clexp, _) -> rmw_write clexp
   | CL_field (clexp, _) -> rmw_write clexp
-  | clexp -> assert false
+  | clexp -> failwith "Could not understand l-expression"
 
 let rmw_read = function
   | CL_rmw (read, _, _) -> zencode_name read
@@ -1522,7 +1680,7 @@ let rmw_modify smt = function
           if UId.compare field field' = 0 then
             smt
           else
-            Fn (zencode_upper_id struct_id ^ "_" ^ zencode_uid field', [Var (rmw_read clexp)])
+            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)
      | _ ->
@@ -1564,7 +1722,7 @@ let smt_instr ctx =
        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 ctx wk addr_size addr data_size data in
+            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"
@@ -1580,7 +1738,7 @@ let smt_instr ctx =
        else if name = "platform_read_mem" then
          begin match args with
          | [rk; addr_size; addr; data_size] ->
-            let mem_event, var = builtin_read_mem ctx rk addr_size addr data_size ret_ctyp in
+            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"
@@ -1588,7 +1746,23 @@ let smt_instr ctx =
        else if name = "platform_barrier" then
          begin match args with
          | [bk] ->
-            let mem_event, var = builtin_barrier ctx bk in
+            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"
@@ -1601,9 +1775,20 @@ let smt_instr ctx =
          | _ ->
             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 value]
+         [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
@@ -1615,15 +1800,6 @@ let smt_instr ctx =
        | _ ->
           Reporting.unreachable l __POS__ "Bad arguments for internal_vector_update"
        end
-     else if string_of_id (fst function_id) = "sail_assert" then
-       begin match args with
-       | [assertion; _] ->
-          let smt = smt_cval ctx assertion in
-          add_event ctx Assertion smt;
-          []
-       | _ ->
-          Reporting.unreachable l __POS__ "Bad arguments for assertion"
-       end
      else if string_of_id (fst function_id) = "sail_assume" then
        begin match args with
        | [assumption] ->
@@ -1643,8 +1819,14 @@ let smt_instr ctx =
      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), _) ->
-     [define_const ctx id ctyp
-        (smt_conversion ctx (cval_ctyp cval) ctyp (smt_cval ctx cval))]
+     begin match id with
+     | Name (id, _) when IdSet.mem id ctx.preserved ->
+        [preserve_const ctx id ctyp
+           (smt_conversion ctx (cval_ctyp cval) ctyp (smt_cval ctx cval))]
+     | _ ->
+        [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
@@ -1721,13 +1903,19 @@ module Make_optimizer(S : Sequence) = struct
          | Some n -> Hashtbl.replace uses var (n + 1)
          | None -> Hashtbl.add uses var 1
          end
-      | Enum _ | Read_res _ | Hex _ | Bin _ | Bool_lit _ | String_lit _ | Real_lit _ -> ()
+      | 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
@@ -1737,6 +1925,11 @@ module Make_optimizer(S : Sequence) = struct
          | 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 -> ()
@@ -1746,17 +1939,23 @@ module Make_optimizer(S : Sequence) = struct
          end
       | (Declare_datatypes _ | Declare_tuple _) as def ->
          Stack.push def stack'
-      | Write_mem (_, _, active, wk, addr, _, data, _) as def ->
-         uses_in_exp active; uses_in_exp wk; uses_in_exp addr; uses_in_exp data;
+      | 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 (_, _, active, _, rk, addr, _) as def ->
-         uses_in_exp active; uses_in_exp rk; uses_in_exp addr;
+      | 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'
-      | Barrier (_, _, active, bk) as def ->
-         uses_in_exp active; uses_in_exp bk;
+      | 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;
@@ -1775,10 +1974,14 @@ module Make_optimizer(S : Sequence) = struct
     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
-         | _, (Bin _ | Bool_lit _) ->
+         | _, (Bitvec_lit _ | Bool_lit _) ->
             Hashtbl.add vars var exp
          | _, Var _ when !opt_propagate_vars ->
             Hashtbl.add vars var exp
@@ -1791,20 +1994,30 @@ module Make_optimizer(S : Sequence) = struct
             S.add (Define_const (var, typ, exp)) seq
          | None, _ -> assert false
          end
-      | Write_mem (name, node, active, wk, addr, addr_ty, data, data_ty) ->
-         S.add (Write_mem (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, data_ty))
+      | 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 (name, node, active, typ, rk, addr, addr_typ) ->
-         S.add (Read_mem (name, node, simp_smt_exp vars kinds active, typ, simp_smt_exp vars kinds rk,
-                          simp_smt_exp vars kinds addr, addr_typ))
+      | 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 (name, node, active, bk) ->
-         S.add (Barrier (name, node, simp_smt_exp vars kinds active, simp_smt_exp vars kinds bk)) 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 ->
@@ -1843,6 +2056,26 @@ let smt_header ctx cdefs =
    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 (CL_id (name 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
@@ -1855,7 +2088,7 @@ let expand_reg_deref env register_map = function
               let end_label = label "end_reg_deref_" in
               let try_reg r =
                 let next_label = label "next_reg_deref_" in
-                [ijump (V_call (Neq, [V_ref (name r, reg_ctyp); reg_ref])) next_label;
+                [ijump l (V_call (Neq, [V_lit (VL_ref (string_of_id r), reg_ctyp); reg_ref])) next_label;
                  icopy l clexp (V_id (name r, reg_ctyp));
                  igoto end_label;
                  ilabel next_label]
@@ -1877,7 +2110,7 @@ let expand_reg_deref env register_map = function
            let end_label = label "end_reg_write_" in
            let try_reg r =
              let next_label = label "next_reg_write_" in
-             [ijump (V_call (Neq, [V_ref (name r, reg_ctyp); V_id (id, ctyp)])) next_label;
+             [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 (name r, reg_ctyp)) cval;
               igoto end_label;
               ilabel next_label]
@@ -1927,7 +2160,7 @@ let smt_instr_list name ctx all_cdefs instrs =
     dump_graph name cfg;
 
   List.iter (fun n ->
-      begin match get_vertex cfg n with
+      match get_vertex cfg n with
       | None -> ()
       | Some ((ssa_elems, cfnode), preds, succs) ->
          let muxers =
@@ -1937,13 +2170,12 @@ let smt_instr_list name ctx all_cdefs instrs =
          let basic_block = smt_cfnode all_cdefs ctx ssa_elems cfnode in
          push_smt_defs stack muxers;
          push_smt_defs stack basic_block
-      end
     ) visit_order;
 
-  stack, cfg
+  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 ->
+  | 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
@@ -1967,7 +2199,7 @@ let smt_cdef props lets name_file ctx all_cdefs = function
           |> remove_pointless_goto
         in
 
-        let stack, _ = smt_instr_list (string_of_id function_id) ctx all_cdefs instrs 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]))];
@@ -2038,25 +2270,20 @@ let rec build_register_map rmap = function
   | [] -> rmap
 
 let compile env ast =
-  let cdefs =
-    let open Jib_compile in
-    let ctx =
-      initial_ctx
-        ~convert_typ:ctyp_of_typ
-        ~optimize_anf:(fun ctx aexp -> fold_aexp (unroll_foreach ctx) (c_literals ctx aexp))
-        env
-    in
+  let cdefs, jib_ctx =
+    let module Jibc = Jib_compile.Make(SMT_config) in
+    let ctx = Jib_compile.(initial_ctx (add_special_functions env)) in
     let t = Profile.start () in
-    let cdefs, ctx = compile_ast { ctx with specialize_calls = true; ignore_64 = true; struct_value = true; use_real = true } ast in
+    let cdefs, ctx = Jibc.compile_ast ctx ast in
     Profile.finish "Compiling to Jib IR" t;
-    cdefs
+    cdefs, ctx
   in
   let cdefs = Jib_optimize.unique_per_function_ids cdefs in
   let rmap = build_register_map CTMap.empty cdefs in
-  cdefs, { (initial_ctx ()) with tc_env = env; register_map = rmap; ast = ast }
+  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 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) [];
@@ -2073,7 +2300,7 @@ let deserialize_smt_model file =
 
 let generate_smt props name_file env ast =
   try
-    let cdefs, ctx = compile env ast in
+    let cdefs, _, ctx = compile env ast in
     smt_cdefs props [] name_file ctx cdefs cdefs
   with
   | Type_check.Type_error (_, l, err) ->
diff --git a/src/jib/jib_smt.mli b/src/jib/jib_smt.mli
index cdaf7e39..616877e4 100644
--- a/src/jib/jib_smt.mli
+++ b/src/jib/jib_smt.mli
@@ -73,44 +73,57 @@ val opt_default_lbits_index : int ref
 val opt_default_vector_index : int ref
 
 type ctx = {
-    (** Arbitrary-precision bitvectors are represented as a (BitVec lbits_index, BitVec (2 ^ lbits_index)) pair. *)
     lbits_index : int;
-    (** The size we use for integers where we don't know how large they are statically. *)
+    (** Arbitrary-precision bitvectors are represented as a (BitVec lbits_index, BitVec (2 ^ lbits_index)) pair. *)
     lint_size : int;
+    (** The size we use for integers where we don't know how large they are statically. *)
+    vector_index : int;
     (** A generic vector, vector('a) becomes Array (BitVec vector_index) 'a.
        We need to take care that vector_index is large enough for all generic vectors. *)
-    vector_index : int;
-    (** A map from each ctyp to a list of registers of that ctyp *)
     register_map : id list CTMap.t;
-    (** A set to keep track of all the tuple sizes we need to generate types for *)
+    (** A map from each ctyp to a list of registers of that ctyp *)
     tuple_sizes : IntSet.t ref;
-    (** tc_env is the global type-checking environment *)
+    (** A set to keep track of all the tuple sizes we need to generate types for *)
     tc_env : Type_check.Env.t;
+    (** tc_env is the global type-checking environment *)
+    pragma_l : Ast.l;
     (** A location, usually the $counterexample or $property we are
        generating the SMT for. Used for error messages. *)
-    pragma_l : Ast.l;
-    (** Used internally to keep track of function argument names *)
     arg_stack : (int * string) Stack.t;
-    (** The fully type-checked ast *)
+    (** Used internally to keep track of function argument names *)
     ast : Type_check.tannot defs;
+    (** The fully type-checked ast *)
+    shared : ctyp Bindings.t;
+    (** Shared variables. These variables do not get renamed by
+       Smtlib.suffix_variables_def, and their SSA number is
+       omitted. They should therefore only ever be read and never
+       written. Used by sail-axiomatic for symbolic values in the
+       initial litmus state. *)
+    preserved : IdSet.t;
+    (** icopy instructions to an id in preserved will generated a
+       define-const (by using Smtlib.Preserved_const) that will not be
+       simplified away or renamed. It will also not get a SSA
+       number. Such variables can therefore only ever be written to
+       once, and never read. They are used by sail-axiomatic to
+       extract information from the generated SMT. *)
+    events : smt_exp Stack.t EventMap.t ref;
     (** For every event type we have a stack of boolean SMT
        expressions for each occurance of that event. See
        src/property.ml for the event types *)
-    events : smt_exp Stack.t EventMap.t ref;
+    node : int;
+    pathcond : smt_exp Lazy.t;
     (** When generating SMT for an instruction pathcond will contain
        the global path conditional of the containing block/node in the
        control flow graph *)
-    node : int;
-    pathcond : smt_exp Lazy.t;
+    use_string : bool ref;
+    use_real : bool ref
     (** Set if we need to use strings or real numbers in the generated
        SMT, which then requires set-logic ALL or similar depending on
        the solver *)
-    use_string : bool ref;
-    use_real : bool ref
   }
 
 (** Compile an AST into Jib suitable for SMT generation, and initialise a context. *)
-val compile : Type_check.Env.t -> Type_check.tannot defs -> cdef list * ctx
+val compile : Type_check.Env.t -> Type_check.tannot defs -> cdef list * Jib_compile.ctx * ctx
 
 (* TODO: Currently we internally use mutable stacks and queues to
    avoid any issues with stack overflows caused by some non
@@ -122,7 +135,7 @@ val smt_header : ctx -> cdef list -> smt_def list
 
 val smt_query : ctx -> Property.query -> smt_exp
 
-val smt_instr_list : string -> ctx -> cdef list -> instr list -> smt_def Stack.t * (ssa_elem list * cf_node) Jib_ssa.array_graph
+val smt_instr_list : string -> ctx -> cdef list -> instr list -> smt_def Stack.t * int * (ssa_elem list * cf_node) Jib_ssa.array_graph
 
 module type Sequence = sig
   type 'a t
diff --git a/src/jib/jib_smt_fuzz.ml b/src/jib/jib_smt_fuzz.ml
index 846d0178..58665bde 100644
--- a/src/jib/jib_smt_fuzz.ml
+++ b/src/jib/jib_smt_fuzz.ml
@@ -152,13 +152,13 @@ let rec run frame =
 exception Skip_iteration of string;;
 
 let fuzz_cdef ctx all_cdefs = function
-  | CDEF_spec (id, arg_ctyps, ret_ctyp) when not (string_of_id id = "and_bool" || string_of_id id = "or_bool") ->
+  | CDEF_spec (id, _, arg_ctyps, ret_ctyp) when not (string_of_id id = "and_bool" || string_of_id id = "or_bool") ->
      let open Type_check in
      let open Interpreter in
      if Env.is_extern id ctx.tc_env "smt" then (
        let extern = Env.get_extern id ctx.tc_env "smt" in
        let typq, (Typ_aux (aux, _) as typ) = Env.get_val_spec id ctx.tc_env in
-       let istate = initial_state ctx.ast ctx.tc_env Value.primops in
+       let istate = initial_state ctx.ast ctx.tc_env !Value.primops in
        let header = smt_header ctx all_cdefs in
        prerr_endline (Util.("Fuzz: " |> cyan |> clear) ^ string_of_id id ^ " = \"" ^ extern ^ "\" : " ^ string_of_typ typ);
 
@@ -192,7 +192,7 @@ let fuzz_cdef ctx all_cdefs = function
                    @ [iend ()]
                  in
                  let smt_defs =
-                   try fst (smt_instr_list extern ctx all_cdefs jib) with
+                   try (fun (x, _, _) -> x) (smt_instr_list extern ctx all_cdefs jib) with
                    | _ ->
                       raise (Skip_iteration ("SMT error for: " ^ Util.string_of_list ", " string_of_exp (List.map fst values)))
                  in
@@ -253,6 +253,6 @@ let fuzz_cdef ctx all_cdefs = function
 let fuzz seed env ast =
   Random.init seed;
 
-  let cdefs, ctx = compile env ast in
+  let cdefs, _, ctx = compile env ast in
 
   List.iter (fuzz_cdef ctx cdefs) cdefs
diff --git a/src/jib/jib_ssa.ml b/src/jib/jib_ssa.ml
index 9c405a48..fe3238a4 100644
--- a/src/jib/jib_ssa.ml
+++ b/src/jib/jib_ssa.ml
@@ -504,6 +504,7 @@ let rename_variables graph root children =
     | Name (id, _) -> Name (id, i)
     | Have_exception _ -> Have_exception i
     | Current_exception _ -> Current_exception i
+    | Throw_location _ -> Throw_location i
     | Return _ -> Return i
   in
 
@@ -524,9 +525,6 @@ let rename_variables graph root children =
     | V_id (id, ctyp) ->
        let i = top_stack id in
        V_id (ssa_name i id, ctyp)
-    | V_ref (id, ctyp) ->
-       let i = top_stack id in
-       V_ref (ssa_name i id, ctyp)
     | V_lit (vl, ctyp) -> V_lit (vl, ctyp)
     | V_call (id, fs) -> V_call (id, List.map fold_cval fs)
     | V_field (f, field) -> V_field (fold_cval f, field)
diff --git a/src/jib/jib_util.ml b/src/jib/jib_util.ml
index 13438208..9b06c7be 100644
--- a/src/jib/jib_util.ml
+++ b/src/jib/jib_util.ml
@@ -83,7 +83,7 @@ let ireset ?loc:(l=Parse_ast.Unknown) ctyp id =
 let iinit ?loc:(l=Parse_ast.Unknown) ctyp id cval =
   I_aux (I_init (ctyp, id, cval), (instr_number (), l))
 
-let iif ?loc:(l=Parse_ast.Unknown) cval then_instrs else_instrs ctyp =
+let iif l cval then_instrs else_instrs ctyp =
   I_aux (I_if (cval, then_instrs, else_instrs, ctyp), (instr_number (), l))
 
 let ifuncall ?loc:(l=Parse_ast.Unknown) clexp id cvals =
@@ -113,7 +113,7 @@ let iblock ?loc:(l=Parse_ast.Unknown) instrs =
 let itry_block ?loc:(l=Parse_ast.Unknown) instrs =
   I_aux (I_try_block instrs, (instr_number (), l))
 
-let ithrow ?loc:(l=Parse_ast.Unknown) cval =
+let ithrow l cval =
   I_aux (I_throw cval, (instr_number (), l))
 
 let icomment ?loc:(l=Parse_ast.Unknown) str =
@@ -134,7 +134,7 @@ let imatch_failure ?loc:(l=Parse_ast.Unknown) () =
 let iraw ?loc:(l=Parse_ast.Unknown) str =
   I_aux (I_raw str, (instr_number (), l))
 
-let ijump ?loc:(l=Parse_ast.Unknown) cval label =
+let ijump l cval label =
   I_aux (I_jump (cval, label), (instr_number (), l))
 
 module Name = struct
@@ -153,6 +153,8 @@ module Name = struct
     | _, Have_exception _ -> -1
     | Current_exception _, _ -> 1
     | _, Current_exception _ -> -1
+    | Throw_location _, _ -> 1
+    | _, Throw_location _ -> -1
 end
 
 module NameSet = Set.Make(Name)
@@ -160,6 +162,7 @@ module NameMap = Map.Make(Name)
 
 let current_exception = Current_exception (-1)
 let have_exception = Have_exception (-1)
+let throw_location = Throw_location (-1)
 let return = Return (-1)
 
 let name id = Name (id, -1)
@@ -167,8 +170,6 @@ let name id = Name (id, -1)
 let rec cval_rename from_id to_id = function
   | V_id (id, ctyp) when Name.compare id from_id = 0 -> V_id (to_id, ctyp)
   | V_id (id, ctyp) -> V_id (id, ctyp)
-  | V_ref (id, ctyp) when Name.compare id from_id = 0 -> V_ref (to_id, ctyp)
-  | V_ref (id, ctyp) -> V_ref (id, ctyp)
   | V_lit (vl, ctyp) -> V_lit (vl, ctyp)
   | V_call (call, cvals) -> V_call (call, List.map (cval_rename from_id to_id) cvals)
   | V_field (f, field) -> V_field (cval_rename from_id to_id f, field)
@@ -257,8 +258,7 @@ let rec instr_rename from_id to_id (I_aux (instr, aux)) =
 (* 1. Instruction pretty printer                                          *)
 (**************************************************************************)
 
-
-let string_of_name ?deref_current_exception:(dce=true) ?zencode:(zencode=true) =
+let string_of_name ?deref_current_exception:(dce=false) ?zencode:(zencode=true) =
   let ssa_num n = if n = -1 then "" else ("/" ^ string_of_int n) in
   function
   | Name (id, n) ->
@@ -271,6 +271,8 @@ let string_of_name ?deref_current_exception:(dce=true) ?zencode:(zencode=true) =
      "(*current_exception)" ^ ssa_num n
   | Current_exception n ->
      "current_exception" ^ ssa_num n
+  | Throw_location n ->
+     "throw_location" ^ ssa_num n
 
 let string_of_op = function
   | Bnot -> "@not"
@@ -278,7 +280,6 @@ let string_of_op = function
   | Bor -> "@or"
   | List_hd -> "@hd"
   | List_tl -> "@tl"
-  | Bit_to_bool -> "@bit_to_bool"
   | Eq -> "@eq"
   | Neq -> "@neq"
   | Bvnot -> "@bvnot"
@@ -309,9 +310,9 @@ let string_of_op = function
 let rec string_of_ctyp = function
   | CT_lint -> "%i"
   | CT_fint n -> "%i" ^ string_of_int n
-  | CT_lbits _ -> "%lb"
-  | CT_sbits (n, _) -> "%sb" ^ string_of_int n
-  | CT_fbits (n, _) -> "%fb" ^ string_of_int n
+  | CT_lbits _ -> "%bv"
+  | CT_sbits (n, _) -> "%sbv" ^ string_of_int n
+  | CT_fbits (n, _) -> "%bv" ^ string_of_int n
   | CT_constant n -> Big_int.to_string n
   | CT_bit -> "%bit"
   | CT_unit -> "%unit"
@@ -323,6 +324,7 @@ let rec string_of_ctyp = function
   | CT_enum (id, _) -> "%enum " ^ Util.zencode_string (string_of_id id)
   | CT_variant (id, _) -> "%union " ^ Util.zencode_string (string_of_id id)
   | CT_vector (_, ctyp) -> "%vec(" ^ string_of_ctyp ctyp ^ ")"
+  | CT_fvector (n, _, ctyp) -> "%fvec(" ^ string_of_int n ^ ", " ^ string_of_ctyp ctyp ^ ")"
   | CT_list ctyp -> "%list(" ^ string_of_ctyp ctyp ^ ")"
   | CT_ref ctyp -> "&(" ^ string_of_ctyp ctyp ^ ")"
   | CT_poly -> "*"
@@ -352,24 +354,27 @@ and full_string_of_ctyp = function
   | CT_ref ctyp -> "ref(" ^ full_string_of_ctyp ctyp ^ ")"
   | ctyp -> string_of_ctyp ctyp
 
-let string_of_value = function
-  | VL_bits ([], _) -> "empty"
+let rec string_of_value = function
+  | VL_bits ([], _) -> "UINT64_C(0)"
   | VL_bits (bs, true) -> Sail2_values.show_bitlist bs
   | VL_bits (bs, false) -> Sail2_values.show_bitlist (List.rev bs)
   | VL_int i -> Big_int.to_string i
   | VL_bool true -> "true"
   | VL_bool false -> "false"
-  | VL_null -> "NULL"
   | VL_unit -> "()"
   | VL_bit Sail2_values.B0 -> "bitzero"
   | VL_bit Sail2_values.B1 -> "bitone"
-  | VL_bit Sail2_values.BU -> "bitundef"
+  | VL_bit Sail2_values.BU -> failwith "Undefined bit found in value"
   | VL_real str -> str
   | VL_string str -> "\"" ^ str ^ "\""
+  | VL_empty_list -> "NULL"
+  | VL_enum element -> Util.zencode_string element
+  | VL_ref r -> "&" ^ Util.zencode_string r
+  | VL_undefined -> "undefined"
 
 let rec string_of_cval = function
   | V_id (id, ctyp) -> string_of_name id
-  | V_ref (id, _) -> "&" ^ string_of_name id
+  | V_lit (VL_undefined, ctyp) -> string_of_value VL_undefined ^ " : " ^ string_of_ctyp ctyp
   | V_lit (vl, ctyp) -> string_of_value vl
   | V_call (op, cvals) ->
      Printf.sprintf "%s(%s)" (string_of_op op) (Util.string_of_list ", " string_of_cval cvals)
@@ -377,16 +382,10 @@ let rec string_of_cval = function
      Printf.sprintf "%s.%s" (string_of_cval f) (string_of_uid field)
   | V_tuple_member (f, _, n) ->
      Printf.sprintf "%s.ztup%d" (string_of_cval f) n
-  | V_ctor_kind (f, ctor, [], _) ->
-     string_of_cval f ^ " is " ^ Util.zencode_string (string_of_id ctor)
   | V_ctor_kind (f, ctor, unifiers, _) ->
-     string_of_cval f ^ " is " ^ Util.zencode_string (string_of_id ctor ^ "_" ^ Util.string_of_list "_" string_of_ctyp unifiers)
-  | V_ctor_unwrap (ctor, f, [], _) ->
-     Printf.sprintf "%s as %s" (string_of_cval f) (string_of_id ctor)
+     string_of_cval f ^ " is " ^ string_of_uid (ctor, unifiers)
   | V_ctor_unwrap (ctor, f, unifiers, _) ->
-     Printf.sprintf "%s as %s"
-       (string_of_cval f)
-       (Util.zencode_string (string_of_id ctor ^ "_" ^ Util.string_of_list "_" string_of_ctyp unifiers))
+     string_of_cval f ^ " as " ^ string_of_uid (ctor, unifiers)
   | V_struct (fields, _) ->
      Printf.sprintf "{%s}"
        (Util.string_of_list ", " (fun (field, cval) -> string_of_uid field ^ " = " ^ string_of_cval cval) fields)
@@ -398,6 +397,7 @@ let rec map_ctyp f = function
   | CT_tup ctyps -> f (CT_tup (List.map (map_ctyp f) ctyps))
   | CT_ref ctyp -> f (CT_ref (map_ctyp f ctyp))
   | CT_vector (direction, ctyp) -> f (CT_vector (direction, map_ctyp f ctyp))
+  | CT_fvector (n, direction, ctyp) -> f (CT_fvector (n, direction, map_ctyp f ctyp))
   | CT_list ctyp -> f (CT_list (map_ctyp f ctyp))
   | CT_struct (id, ctors) ->
      f (CT_struct (id, List.map (fun ((id, ctyps), ctyp) -> (id, List.map (map_ctyp f) ctyps), map_ctyp f ctyp) ctors))
@@ -423,6 +423,7 @@ let rec ctyp_equal ctyp1 ctyp2 =
   | CT_string, CT_string -> true
   | CT_real, CT_real -> true
   | CT_vector (d1, ctyp1), CT_vector (d2, ctyp2) -> d1 = d2 && ctyp_equal ctyp1 ctyp2
+  | CT_fvector (n1, d1, ctyp1), CT_fvector (n2, d2, ctyp2) -> n1 = n2 && d1 = d2 && ctyp_equal ctyp1 ctyp2
   | CT_list ctyp1, CT_list ctyp2 -> ctyp_equal ctyp1 ctyp2
   | CT_ref ctyp1, CT_ref ctyp2 -> ctyp_equal ctyp1 ctyp2
   | CT_poly, CT_poly -> true
@@ -492,6 +493,11 @@ let rec ctyp_compare ctyp1 ctyp2 =
   | CT_vector _, _ -> 1
   | _, CT_vector _ -> -1
 
+  | CT_fvector (n1, d1, ctyp1), CT_fvector (n2, d2, ctyp2) ->
+     lex_ord (compare n1 n2) (lex_ord (ctyp_compare ctyp1 ctyp2) (compare d1 d2))
+  | CT_fvector _, _ -> 1
+  | _, CT_fvector _ -> -1
+
   | ctyp1, ctyp2 -> String.compare (full_string_of_ctyp ctyp1) (full_string_of_ctyp ctyp2)
 
 module CT = struct
@@ -564,6 +570,7 @@ let rec ctyp_suprema = function
   | CT_struct (id, ctors) -> CT_struct (id, ctors)
   | CT_variant (id, ctors) -> CT_variant (id, ctors)
   | CT_vector (d, ctyp) -> CT_vector (d, ctyp_suprema ctyp)
+  | CT_fvector (n, d, ctyp) -> CT_fvector (n, d, ctyp_suprema ctyp)
   | CT_list ctyp -> CT_list (ctyp_suprema ctyp)
   | CT_ref ctyp -> CT_ref (ctyp_suprema ctyp)
   | CT_poly -> CT_poly
@@ -573,7 +580,7 @@ let rec ctyp_ids = function
   | CT_struct (id, ctors) | CT_variant (id, ctors) ->
      IdSet.add id (List.fold_left (fun ids (_, ctyp) -> IdSet.union (ctyp_ids ctyp) ids) IdSet.empty ctors)
   | CT_tup ctyps -> List.fold_left (fun ids ctyp -> IdSet.union (ctyp_ids ctyp) ids) IdSet.empty ctyps
-  | CT_vector (_, ctyp) | CT_list ctyp | CT_ref ctyp -> ctyp_ids ctyp
+  | CT_vector (_, ctyp) | CT_fvector (_, _, ctyp) | CT_list ctyp | CT_ref ctyp -> ctyp_ids ctyp
   | CT_lint | CT_fint _ | CT_constant _ | CT_lbits _ | CT_fbits _ | CT_sbits _ | CT_unit
     | CT_bool | CT_real | CT_bit | CT_string | CT_poly -> IdSet.empty
 
@@ -588,11 +595,11 @@ let rec is_polymorphic = function
   | CT_tup ctyps -> List.exists is_polymorphic ctyps
   | CT_enum _ -> false
   | CT_struct (_, ctors) | CT_variant (_, ctors) -> List.exists (fun (_, ctyp) -> is_polymorphic ctyp) ctors
-  | CT_vector (_, ctyp) | CT_list ctyp | CT_ref ctyp -> is_polymorphic ctyp
+  | CT_fvector (_, _, ctyp) | CT_vector (_, ctyp) | CT_list ctyp | CT_ref ctyp -> is_polymorphic ctyp
   | CT_poly -> true
 
 let rec cval_deps = function
-  | V_id (id, _) | V_ref (id, _) -> NameSet.singleton id
+  | V_id (id, _) -> NameSet.singleton id
   | V_lit _ -> NameSet.empty
   | V_field (cval, _) | V_poly (cval, _) | V_tuple_member (cval, _, _) -> cval_deps cval
   | V_call (_, cvals) -> List.fold_left NameSet.union NameSet.empty (List.map cval_deps cvals)
@@ -666,7 +673,6 @@ let rec map_clexp_ctyp f = function
 
 let rec map_cval_ctyp f = function
   | V_id (id, ctyp) -> V_id (id, f ctyp)
-  | V_ref (id, ctyp) -> V_ref (id, f ctyp)
   | V_lit (vl, ctyp) -> V_lit (vl, f ctyp)
   | V_ctor_kind (cval, id, unifiers, ctyp) ->
      V_ctor_kind (map_cval_ctyp f cval, id, List.map f unifiers, f ctyp)
@@ -734,7 +740,7 @@ let rec concatmap_instr f (I_aux (instr, aux)) =
        I_try_block (List.concat (List.map (concatmap_instr f) instrs))
   in
   f (I_aux (instr, aux))
-  
+
 (** Iterate over each instruction within an instruction, bottom-up *)
 let rec iter_instr f (I_aux (instr, aux)) =
   match instr with
@@ -754,7 +760,7 @@ let cdef_map_instr f = function
   | CDEF_fundef (id, heap_return, args, instrs) -> CDEF_fundef (id, heap_return, args, List.map (map_instr f) instrs)
   | CDEF_startup (id, instrs) -> CDEF_startup (id, List.map (map_instr f) instrs)
   | CDEF_finish (id, instrs) -> CDEF_finish (id, List.map (map_instr f) instrs)
-  | CDEF_spec (id, ctyps, ctyp) -> CDEF_spec (id, ctyps, ctyp)
+  | CDEF_spec (id, extern, ctyps, ctyp) -> CDEF_spec (id, extern, ctyps, ctyp)
   | CDEF_type tdef -> CDEF_type tdef
 
 (** Map over each instruction in a cdef using concatmap_instr *)
@@ -769,7 +775,7 @@ let cdef_concatmap_instr f = function
      CDEF_startup (id, List.concat (List.map (concatmap_instr f) instrs))
   | CDEF_finish (id, instrs) ->
      CDEF_finish (id, List.concat (List.map (concatmap_instr f) instrs))
-  | CDEF_spec (id, ctyps, ctyp) -> CDEF_spec (id, ctyps, ctyp)
+  | CDEF_spec (id, extern, ctyps, ctyp) -> CDEF_spec (id, extern, ctyps, ctyp)
   | CDEF_type tdef -> CDEF_type tdef
 
 let ctype_def_map_ctyp f = function
@@ -784,7 +790,7 @@ let cdef_map_ctyp f = function
   | CDEF_fundef (id, heap_return, args, instrs) -> CDEF_fundef (id, heap_return, args, List.map (map_instr_ctyp f) instrs)
   | CDEF_startup (id, instrs) -> CDEF_startup (id, List.map (map_instr_ctyp f) instrs)
   | CDEF_finish (id, instrs) -> CDEF_finish (id, List.map (map_instr_ctyp f) instrs)
-  | CDEF_spec (id, ctyps, ctyp) -> CDEF_spec (id, List.map f ctyps, f ctyp)
+  | CDEF_spec (id, extern, ctyps, ctyp) -> CDEF_spec (id, extern, List.map f ctyps, f ctyp)
   | CDEF_type tdef -> CDEF_type (ctype_def_map_ctyp f tdef)
 
 (* Map over all sequences of instructions contained within an instruction *)
@@ -838,7 +844,6 @@ let label str =
 
 let rec infer_call op vs =
   match op, vs with
-  | Bit_to_bool, _ -> CT_bool
   | Bnot, _ -> CT_bool
   | Band, _ -> CT_bool
   | Bor, _ -> CT_bool
@@ -900,7 +905,6 @@ let rec infer_call op vs =
 
 and cval_ctyp = function
   | V_id (_, ctyp) -> ctyp
-  | V_ref (_, ctyp) -> CT_ref ctyp
   | V_lit (vl, ctyp) -> ctyp
   | V_ctor_kind _ -> CT_bool
   | V_ctor_unwrap (ctor, cval, unifiers, ctyp) -> ctyp
@@ -984,7 +988,7 @@ let ctype_def_ctyps = function
 let cdef_ctyps = function
   | CDEF_reg_dec (_, ctyp, instrs) ->
      CTSet.add ctyp (instrs_ctyps instrs)
-  | CDEF_spec (_, ctyps, ctyp) ->
+  | CDEF_spec (_, _, ctyps, ctyp) ->
      CTSet.add ctyp (List.fold_left (fun m ctyp -> CTSet.add ctyp m) CTSet.empty ctyps)
   | CDEF_fundef (_, _, _, instrs) | CDEF_startup (_, instrs) | CDEF_finish (_, instrs) ->
      instrs_ctyps instrs