Merge branch 'sail2' into rmem_interpreter

11 files changed, 716 insertions, 428 deletions

diff --git a/src/jib/anf.ml b/src/jib/anf.ml
index 025138d0..0a410249 100644
--- a/src/jib/anf.ml
+++ b/src/jib/anf.ml
@@ -91,6 +91,7 @@ and 'a apat_aux =
   | AP_global of id * 'a
   | AP_app of id * 'a apat * 'a
   | AP_cons of 'a apat * 'a apat
+  | AP_as of 'a apat * id * 'a
   | AP_nil of 'a
   | AP_wild of 'a
 
@@ -113,6 +114,7 @@ let rec apat_bindings (AP_aux (apat_aux, _, _)) =
   | AP_global (id, _) -> IdSet.empty
   | AP_app (id, apat, _) -> apat_bindings apat
   | AP_cons (apat1, apat2) -> IdSet.union (apat_bindings apat1) (apat_bindings apat2)
+  | AP_as (apat, id, _) -> IdSet.add id (apat_bindings apat)
   | AP_nil _ -> IdSet.empty
   | AP_wild _ -> IdSet.empty
 
@@ -132,6 +134,7 @@ let rec apat_types (AP_aux (apat_aux, _, _)) =
   | AP_global (id, _) -> Bindings.empty
   | AP_app (id, apat, _) -> apat_types apat
   | AP_cons (apat1, apat2) -> (Bindings.merge merge) (apat_types apat1) (apat_types apat2)
+  | AP_as (apat, id, typ) -> Bindings.add id typ (apat_types apat)
   | AP_nil _ -> Bindings.empty
   | AP_wild _ -> Bindings.empty
 
@@ -143,6 +146,8 @@ let rec apat_rename from_id to_id (AP_aux (apat_aux, env, l)) =
     | AP_global (id, typ) -> AP_global (id, typ)
     | AP_app (ctor, apat, typ) -> AP_app (ctor, apat_rename from_id to_id apat, typ)
     | AP_cons (apat1, apat2) -> AP_cons (apat_rename from_id to_id apat1, apat_rename from_id to_id apat2)
+    | AP_as (apat, id, typ) when Id.compare id from_id = 0 -> AP_as (apat, to_id, typ)
+    | AP_as (apat, id, typ) -> AP_as (apat, id, typ)
     | AP_nil typ -> AP_nil typ
     | AP_wild typ -> AP_wild typ
   in
@@ -158,7 +163,7 @@ let rec aval_rename from_id to_id = function
   | AV_list (avals, typ) -> AV_list (List.map (aval_rename from_id to_id) avals, typ)
   | AV_vector (avals, typ) -> AV_vector (List.map (aval_rename from_id to_id) avals, typ)
   | AV_record (avals, typ) -> AV_record (Bindings.map (aval_rename from_id to_id) avals, typ)
-  | AV_C_fragment (fragment, typ, ctyp) -> AV_C_fragment (frag_rename from_id to_id fragment, typ, ctyp)
+  | AV_C_fragment (fragment, typ, ctyp) -> AV_C_fragment (frag_rename (name from_id) (name to_id) fragment, typ, ctyp)
 
 let rec aexp_rename from_id to_id (AE_aux (aexp, env, l)) =
   let recur = aexp_rename from_id to_id in
@@ -382,6 +387,7 @@ and pp_apat (AP_aux (apat_aux, _, _)) =
   | AP_app (id, apat, typ) -> pp_annot typ (pp_id id ^^ parens (pp_apat apat))
   | AP_nil _ -> string "[||]"
   | AP_cons (hd_apat, tl_apat) -> pp_apat hd_apat ^^ string " :: " ^^ pp_apat tl_apat
+  | AP_as (apat, id, ctyp) -> pp_apat apat ^^ string " as " ^^ pp_id id
 
 and pp_cases cases = surround 2 0 lbrace (separate_map (comma ^^ hardline) pp_case cases) rbrace
 
@@ -445,6 +451,7 @@ let rec anf_pat ?global:(global=false) (P_aux (p_aux, annot) as pat) =
   | P_cons (hd_pat, tl_pat) -> mk_apat (AP_cons (anf_pat ~global:global hd_pat, anf_pat ~global:global tl_pat))
   | P_list pats -> List.fold_right (fun pat apat -> mk_apat (AP_cons (anf_pat ~global:global pat, apat))) pats (mk_apat (AP_nil (typ_of_pat pat)))
   | P_lit (L_aux (L_unit, _)) -> mk_apat (AP_wild (typ_of_pat pat))
+  | P_as (pat, id) -> mk_apat (AP_as (anf_pat ~global:global pat, id, typ_of_pat pat))
   | _ ->
      raise (Reporting.err_unreachable (fst annot) __POS__
        ("Could not convert pattern to ANF: " ^ string_of_pat pat))
@@ -456,6 +463,7 @@ let rec apat_globals (AP_aux (aux, _, _)) =
   | AP_tup apats -> List.concat (List.map apat_globals apats)
   | AP_app (_, apat, _) -> apat_globals apat
   | AP_cons (hd_apat, tl_apat) -> apat_globals hd_apat @ apat_globals tl_apat
+  | AP_as (apat, _, _) -> apat_globals apat
 
 let rec anf (E_aux (e_aux, ((l, _) as exp_annot)) as exp) =
   let mk_aexp aexp = AE_aux (aexp, env_of_annot exp_annot, l) in
@@ -526,8 +534,8 @@ let rec anf (E_aux (e_aux, ((l, _) as exp_annot)) as exp) =
      wrap (mk_aexp (AE_if (cond_val, then_aexp, else_aexp, typ_of exp)))
 
   | E_app_infix (x, Id_aux (Id op, l), y) ->
-     anf (E_aux (E_app (Id_aux (DeIid op, l), [x; y]), exp_annot))
-  | E_app_infix (x, Id_aux (DeIid op, l), y) ->
+     anf (E_aux (E_app (Id_aux (Operator op, l), [x; y]), exp_annot))
+  | E_app_infix (x, Id_aux (Operator op, l), y) ->
      anf (E_aux (E_app (Id_aux (Id op, l), [x; y]), exp_annot))
 
   | E_vector exps ->
diff --git a/src/jib/anf.mli b/src/jib/anf.mli
index 79fb35ca..26b847e2 100644
--- a/src/jib/anf.mli
+++ b/src/jib/anf.mli
@@ -111,6 +111,7 @@ and 'a apat_aux =
   | AP_global of id * 'a
   | AP_app of id * 'a apat * 'a
   | AP_cons of 'a apat * 'a apat
+  | AP_as of 'a apat * id * 'a
   | AP_nil of 'a
   | AP_wild of 'a
 
diff --git a/src/jib/c_backend.ml b/src/jib/c_backend.ml
index 846b619f..ee16e2e6 100644
--- a/src/jib/c_backend.ml
+++ b/src/jib/c_backend.ml
@@ -86,7 +86,6 @@ let optimize_primops = ref false
 let optimize_hoist_allocations = ref false
 let optimize_struct_updates = ref false
 let optimize_alias = ref false
-let optimize_experimental = ref false
 
 let c_debug str =
   if !c_verbosity > 0 then prerr_endline (Lazy.force str) else ()
@@ -96,7 +95,7 @@ let c_error ?loc:(l=Parse_ast.Unknown) message =
 
 let zencode_id = function
   | Id_aux (Id str, l) -> Id_aux (Id (Util.zencode_string str), l)
-  | Id_aux (DeIid str, l) -> Id_aux (Id (Util.zencode_string ("op " ^ str)), l)
+  | Id_aux (Operator str, l) -> Id_aux (Id (Util.zencode_string ("op " ^ str)), l)
 
 (**************************************************************************)
 (* 2. Converting sail types to C types                                    *)
@@ -310,21 +309,21 @@ let rec c_aval ctx = function
                 (* 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_C_fragment (F_id id, typ, ctyp)
+                  AV_C_fragment (F_id (name id), typ, ctyp)
                 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_C_fragment (F_id id, typ, ctyp)
+                Not_found -> AV_C_fragment (F_id (name id), typ, ctyp)
             end
           else
             v
        | Register (_, _, typ) when is_stack_typ ctx typ ->
           let ctyp = ctyp_of_typ ctx typ in
           if is_stack_ctyp ctyp then
-            AV_C_fragment (F_id id, typ, ctyp)
+            AV_C_fragment (F_id (name id), typ, ctyp)
           else
             v
        | _ -> v
@@ -612,24 +611,6 @@ let analyze_primop ctx id args typ =
   else
     no_change
 
-let generate_cleanup instrs =
-  let generate_cleanup' (I_aux (instr, _)) =
-    match instr with
-    | I_init (ctyp, id, cval) -> [(id, iclear ctyp id)]
-    | I_decl (ctyp, id) -> [(id, iclear ctyp id)]
-    | instr -> []
-  in
-  let is_clear ids = function
-    | I_aux (I_clear (_, id), _) -> IdSet.add id ids
-    | _ -> ids
-  in
-  let cleaned = List.fold_left is_clear IdSet.empty instrs in
-  instrs
-  |> List.map generate_cleanup'
-  |> List.concat
-  |> List.filter (fun (id, _) -> not (IdSet.mem id cleaned))
-  |> List.map snd
-
 (** Functions that have heap-allocated return types are implemented by
    passing a pointer a location where the return value should be
    stored. The ANF -> Sail IR pass for expressions simply outputs an
@@ -643,7 +624,7 @@ let fix_early_heap_return ret ret_ctyp instrs =
   let end_function_label = label "end_function_" in
   let is_return_recur (I_aux (instr, _)) =
     match instr with
-    | I_if _ | I_block _ | I_end | I_funcall _ | I_copy _ | I_undefined _ -> true
+    | I_if _ | I_block _ | I_end _ | I_funcall _ | I_copy _ | I_undefined _ -> true
     | _ -> false
   in
   let rec rewrite_return instrs =
@@ -657,15 +638,15 @@ let fix_early_heap_return ret ret_ctyp instrs =
        before
        @ [iif cval (rewrite_return then_instrs) (rewrite_return else_instrs) ctyp]
        @ rewrite_return after
-    | before, I_aux (I_funcall (CL_return ctyp, extern, fid, args), aux) :: after ->
+    | before, I_aux (I_funcall (CL_id (Return _, ctyp), extern, fid, args), aux) :: after ->
        before
        @ [I_aux (I_funcall (CL_addr (CL_id (ret, CT_ref ctyp)), extern, fid, args), aux)]
        @ rewrite_return after
-    | before, I_aux (I_copy (CL_return ctyp, cval), aux) :: after ->
+    | before, I_aux (I_copy (CL_id (Return _, ctyp), cval), aux) :: after ->
        before
        @ [I_aux (I_copy (CL_addr (CL_id (ret, CT_ref ctyp)), cval), aux)]
        @ rewrite_return after
-    | before, I_aux ((I_end | I_undefined _), _) :: after ->
+    | before, I_aux ((I_end _ | I_undefined _), _) :: after ->
        before
        @ [igoto end_function_label]
        @ rewrite_return after
@@ -680,7 +661,7 @@ let fix_early_heap_return ret ret_ctyp instrs =
 let fix_early_stack_return ret ret_ctyp instrs =
   let is_return_recur (I_aux (instr, _)) =
     match instr with
-    | I_if _ | I_block _ | I_end | I_funcall _ | I_copy _ -> true
+    | I_if _ | I_block _ | I_end _ | I_funcall _ | I_copy _ -> true
     | _ -> false
   in
   let rec rewrite_return instrs =
@@ -694,15 +675,15 @@ let fix_early_stack_return ret ret_ctyp instrs =
        before
        @ [iif cval (rewrite_return then_instrs) (rewrite_return else_instrs) ctyp]
        @ rewrite_return after
-    | before, I_aux (I_funcall (CL_return ctyp, extern, fid, args), aux) :: after ->
+    | before, I_aux (I_funcall (CL_id (Return _, ctyp), extern, fid, args), aux) :: after ->
        before
        @ [I_aux (I_funcall (CL_id (ret, ctyp), extern, fid, args), aux)]
        @ rewrite_return after
-    | before, I_aux (I_copy (CL_return ctyp, cval), aux) :: after ->
+    | before, I_aux (I_copy (CL_id (Return _, ctyp), cval), aux) :: after ->
        before
        @ [I_aux (I_copy (CL_id (ret, ctyp), cval), aux)]
        @ rewrite_return after
-    | before, I_aux (I_end, _) :: after ->
+    | before, I_aux (I_end _, _) :: after ->
        before
        @ [ireturn (F_id ret, ret_ctyp)]
        @ rewrite_return after
@@ -722,10 +703,10 @@ let rec insert_heap_returns ret_ctyps = function
      | None ->
         raise (Reporting.err_general (id_loc id) ("Cannot find return type for function " ^ string_of_id id))
      | Some ret_ctyp when not (is_stack_ctyp ret_ctyp) ->
-        CDEF_fundef (id, Some gs, args, fix_early_heap_return gs ret_ctyp body)
+        CDEF_fundef (id, Some gs, args, fix_early_heap_return (name gs) ret_ctyp body)
         :: insert_heap_returns ret_ctyps cdefs
      | Some ret_ctyp ->
-        CDEF_fundef (id, None, args, fix_early_stack_return gs ret_ctyp (idecl ret_ctyp gs :: body))
+        CDEF_fundef (id, None, args, fix_early_stack_return (name gs) ret_ctyp (idecl ret_ctyp (name gs) :: body))
         :: insert_heap_returns ret_ctyps cdefs
      end
 
@@ -766,32 +747,6 @@ let add_local_labels instrs =
 (* 5. Optimizations                                                       *)
 (**************************************************************************)
 
-let rec instrs_rename from_id to_id =
-  let rename id = if Id.compare id from_id = 0 then to_id else id in
-  let crename = cval_rename from_id to_id in
-  let irename instrs = instrs_rename from_id to_id instrs in
-  let lrename = clexp_rename from_id to_id in
-  function
-  | (I_aux (I_decl (ctyp, new_id), _) :: _) as instrs when Id.compare from_id new_id = 0 -> instrs
-  | I_aux (I_decl (ctyp, new_id), aux) :: instrs -> I_aux (I_decl (ctyp, new_id), aux) :: irename instrs
-  | I_aux (I_reset (ctyp, id), aux) :: instrs -> I_aux (I_reset (ctyp, rename id), aux) :: irename instrs
-  | I_aux (I_init (ctyp, id, cval), aux) :: instrs -> I_aux (I_init (ctyp, rename id, crename cval), aux) :: irename instrs
-  | I_aux (I_reinit (ctyp, id, cval), aux) :: instrs -> I_aux (I_reinit (ctyp, rename id, crename cval), aux) :: irename instrs
-  | I_aux (I_if (cval, then_instrs, else_instrs, ctyp), aux) :: instrs ->
-     I_aux (I_if (crename cval, irename then_instrs, irename else_instrs, ctyp), aux) :: irename instrs
-  | I_aux (I_jump (cval, label), aux) :: instrs -> I_aux (I_jump (crename cval, label), aux) :: irename instrs
-  | I_aux (I_funcall (clexp, extern, id, cvals), aux) :: instrs ->
-     I_aux (I_funcall (lrename clexp, extern, rename id, List.map crename cvals), aux) :: irename instrs
-  | I_aux (I_copy (clexp, cval), aux) :: instrs -> I_aux (I_copy (lrename clexp, crename cval), aux) :: irename instrs
-  | I_aux (I_alias (clexp, cval), aux) :: instrs -> I_aux (I_alias (lrename clexp, crename cval), aux) :: irename instrs
-  | I_aux (I_clear (ctyp, id), aux) :: instrs -> I_aux (I_clear (ctyp, rename id), aux) :: irename instrs
-  | I_aux (I_return cval, aux) :: instrs -> I_aux (I_return (crename cval), aux) :: irename instrs
-  | I_aux (I_block block, aux) :: instrs -> I_aux (I_block (irename block), aux) :: irename instrs
-  | I_aux (I_try_block block, aux) :: instrs -> I_aux (I_try_block (irename block), aux) :: irename instrs
-  | I_aux (I_throw cval, aux) :: instrs -> I_aux (I_throw (crename cval), aux) :: irename instrs
-  | (I_aux ((I_comment _ | I_raw _ | I_end | I_label _ | I_goto _ | I_match_failure | I_undefined _), _) as instr) :: instrs -> instr :: irename instrs
-  | [] -> []
-
 let hoist_ctyp = function
   | CT_lint | CT_lbits _ | CT_struct _ -> true
   | _ -> false
@@ -800,7 +755,7 @@ let hoist_counter = ref 0
 let hoist_id () =
   let id = mk_id ("gh#" ^ string_of_int !hoist_counter) in
   incr hoist_counter;
-  id
+  name id
 
 let hoist_allocations recursive_functions = function
   | CDEF_fundef (function_id, _, _, _) as cdef when IdSet.mem function_id recursive_functions ->
@@ -871,7 +826,7 @@ let rec specialize_variants ctx prior =
            if ctyp_equal ctyp suprema then
              [], (unpoly frag, ctyp), []
            else
-             let gs = gensym () in
+             let gs = ngensym () in
              [idecl suprema gs;
               icopy l (CL_id (gs, suprema)) (unpoly frag, ctyp)],
              (F_id gs, suprema),
@@ -997,26 +952,26 @@ let remove_alias =
     let rec scan ctyp id n instrs =
       match n, !alias, instrs with
       | 0, None, I_aux (I_copy (CL_id (id', ctyp'), (F_id a, ctyp'')), _) :: instrs
-           when Id.compare id id' = 0 && ctyp_equal ctyp ctyp' && ctyp_equal ctyp' ctyp'' ->
+           when Name.compare id id' = 0 && ctyp_equal ctyp ctyp' && ctyp_equal ctyp' ctyp'' ->
          alias := Some a;
          scan ctyp id 1 instrs
 
       | 1, Some a, I_aux (I_copy (CL_id (a', ctyp'), (F_id id', ctyp'')), _) :: instrs
-           when Id.compare a a' = 0 && Id.compare id id' = 0 && ctyp_equal ctyp ctyp' && ctyp_equal ctyp' ctyp'' ->
+           when Name.compare a a' = 0 && Name.compare id id' = 0 && ctyp_equal ctyp ctyp' && ctyp_equal ctyp' ctyp'' ->
          scan ctyp id 2 instrs
 
       | 1, Some a, instr :: instrs ->
-         if IdSet.mem a (instr_ids instr) then
+         if NameSet.mem a (instr_ids instr) then
            None
          else
            scan ctyp id 1 instrs
 
       | 2, Some a, I_aux (I_clear (ctyp', id'), _) :: instrs
-           when Id.compare id id' = 0 && ctyp_equal ctyp ctyp' ->
+           when Name.compare id id' = 0 && ctyp_equal ctyp ctyp' ->
          scan ctyp id 2 instrs
 
       | 2, Some a, instr :: instrs ->
-         if IdSet.mem id (instr_ids instr) then
+         if NameSet.mem id (instr_ids instr) then
            None
          else
            scan ctyp id 2 instrs
@@ -1031,9 +986,9 @@ let remove_alias =
   in
   let remove_alias id alias = function
     | I_aux (I_copy (CL_id (id', _), (F_id alias', _)), _)
-         when Id.compare id id' = 0 && Id.compare alias alias' = 0 -> removed
+         when Name.compare id id' = 0 && Name.compare alias alias' = 0 -> removed
     | I_aux (I_copy (CL_id (alias', _), (F_id id', _)), _)
-         when Id.compare id id' = 0 && Id.compare alias alias' = 0 -> removed
+         when Name.compare id id' = 0 && Name.compare alias alias' = 0 -> removed
     | I_aux (I_clear (_, id'), _) -> removed
     | instr -> instr
   in
@@ -1066,17 +1021,17 @@ let unique_names =
   let unique_id () =
     let id = mk_id ("u#" ^ string_of_int !unique_counter) in
     incr unique_counter;
-    id
+    name id
   in
 
   let rec opt seen = function
-    | I_aux (I_decl (ctyp, id), aux) :: instrs when IdSet.mem id seen ->
+    | I_aux (I_decl (ctyp, id), aux) :: instrs when NameSet.mem id seen ->
        let id' = unique_id () in
        let instrs', seen = opt seen instrs in
        I_aux (I_decl (ctyp, id'), aux) :: instrs_rename id id' instrs', seen
 
     | I_aux (I_decl (ctyp, id), aux) :: instrs ->
-       let instrs', seen = opt (IdSet.add id seen) instrs in
+       let instrs', seen = opt (NameSet.add id seen) instrs in
        I_aux (I_decl (ctyp, id), aux) :: instrs', seen
 
     | I_aux (I_block block, aux) :: instrs ->
@@ -1103,11 +1058,11 @@ let unique_names =
   in
   function
   | CDEF_fundef (function_id, heap_return, args, body) ->
-     [CDEF_fundef (function_id, heap_return, args, fst (opt IdSet.empty body))]
+     [CDEF_fundef (function_id, heap_return, args, fst (opt NameSet.empty body))]
   | CDEF_reg_dec (id, ctyp, instrs) ->
-     [CDEF_reg_dec (id, ctyp, fst (opt IdSet.empty instrs))]
+     [CDEF_reg_dec (id, ctyp, fst (opt NameSet.empty instrs))]
   | CDEF_let (n, bindings, instrs) ->
-     [CDEF_let (n, bindings, fst (opt IdSet.empty instrs))]
+     [CDEF_let (n, bindings, fst (opt NameSet.empty instrs))]
   | cdef -> [cdef]
 
 (** This optimization looks for patterns of the form
@@ -1135,26 +1090,26 @@ let combine_variables =
          scan id 1 instrs
 
       | 1, Some c, I_aux (I_copy (CL_id (id', ctyp'), (F_id c', ctyp'')), _) :: instrs
-           when Id.compare c c' = 0 && Id.compare id id' = 0 && ctyp_equal ctyp ctyp' && ctyp_equal ctyp' ctyp'' ->
+           when Name.compare c c' = 0 && Name.compare id id' = 0 && ctyp_equal ctyp ctyp' && ctyp_equal ctyp' ctyp'' ->
          scan id 2 instrs
 
       (* Ignore seemingly early clears of x, as this can happen along exception paths *)
       | 1, Some c, I_aux (I_clear (_, id'), _) :: instrs
-           when Id.compare id id' = 0 ->
+           when Name.compare id id' = 0 ->
          scan id 1 instrs
 
       | 1, Some c, instr :: instrs ->
-         if IdSet.mem id (instr_ids instr) then
+         if NameSet.mem id (instr_ids instr) then
            None
          else
            scan id 1 instrs
 
       | 2, Some c, I_aux (I_clear (ctyp', c'), _) :: instrs
-           when Id.compare c c' = 0 && ctyp_equal ctyp ctyp' ->
+           when Name.compare c c' = 0 && ctyp_equal ctyp ctyp' ->
          !combine
 
       | 2, Some c, instr :: instrs ->
-         if IdSet.mem c (instr_ids instr) then
+         if NameSet.mem c (instr_ids instr) then
            None
          else
            scan id 2 instrs
@@ -1167,12 +1122,12 @@ let combine_variables =
     scan id 0
   in
   let remove_variable id = function
-    | I_aux (I_decl (_, id'), _) when Id.compare id id' = 0 -> removed
-    | I_aux (I_clear (_, id'), _) when Id.compare id id' = 0 -> removed
+    | I_aux (I_decl (_, id'), _) when Name.compare id id' = 0 -> removed
+    | I_aux (I_clear (_, id'), _) when Name.compare id id' = 0 -> removed
     | instr -> instr
   in
   let is_not_self_assignment = function
-    | I_aux (I_copy (CL_id (id, _), (F_id id', _)), _) when Id.compare id id' = 0 -> false
+    | I_aux (I_copy (CL_id (id, _), (F_id id', _)), _) when Name.compare id id' = 0 -> false
     | _ -> true
   in
   let rec opt = function
@@ -1200,63 +1155,6 @@ let combine_variables =
      [CDEF_fundef (function_id, heap_return, args, opt body)]
   | cdef -> [cdef]
 
-(** hoist_alias looks for patterns like
-
-    recreate x; y = x; // no furthner mentions of x
-
-    Provided x has a certain type, then we can make y an alias to x
-    (denoted in the IR as 'alias y = x'). This only works if y also has
-    a lifespan that also spans the entire function body. It's possible
-    we may need to do a more thorough lifetime evaluation to get this
-    to be 100% correct - so it's behind the -Oexperimental flag
-    for now. Some benchmarking shows that this kind of optimization
-    is very valuable however! *)
-let hoist_alias =
-  (* Must return true for a subset of the types hoist_ctyp would return true for. *)
-  let is_struct = function
-    | CT_struct _ -> true
-    | _ -> false
-  in
-  let pattern heap_return id ctyp instrs =
-    let rec scan instrs =
-      match instrs with
-      (* The only thing that has a longer lifetime than id is the
-         function return, so we want to make sure we avoid that
-         case. *)
-      | (I_aux (I_copy (clexp, (F_id id', ctyp')), aux) as instr) :: instrs
-           when not (IdSet.mem heap_return (instr_writes instr)) && Id.compare id id' = 0
-                && ctyp_equal (clexp_ctyp clexp) ctyp && ctyp_equal ctyp ctyp' ->
-         if List.exists (IdSet.mem id) (List.map instr_ids instrs) then
-           instr :: scan instrs
-         else
-           I_aux (I_alias (clexp, (F_id id', ctyp')), aux) :: instrs
-
-      | instr :: instrs -> instr :: scan instrs
-      | [] -> []
-    in
-    scan instrs
-  in
-  let optimize heap_return =
-    let rec opt = function
-      | (I_aux (I_reset (ctyp, id), _) as instr) :: instrs when not (is_stack_ctyp ctyp) && is_struct ctyp ->
-         instr :: opt (pattern heap_return id ctyp instrs)
-
-      | I_aux (I_block block, aux) :: instrs -> I_aux (I_block (opt block), aux) :: opt instrs
-      | I_aux (I_try_block block, aux) :: instrs -> I_aux (I_try_block (opt block), aux) :: opt instrs
-      | I_aux (I_if (cval, then_instrs, else_instrs, ctyp), aux) :: instrs ->
-         I_aux (I_if (cval, opt then_instrs, opt else_instrs, ctyp), aux) :: opt instrs
-
-      | instr :: instrs ->
-         instr :: opt instrs
-      | [] -> []
-    in
-    opt
-  in
-  function
-  | CDEF_fundef (function_id, Some heap_return, args, body) ->
-     [CDEF_fundef (function_id, Some heap_return, args, optimize heap_return body)]
-  | cdef -> [cdef]
-
 let concatMap f xs = List.concat (List.map f xs)
 
 let optimize recursive_functions cdefs =
@@ -1267,13 +1165,13 @@ let optimize recursive_functions cdefs =
   |> (if !optimize_alias then concatMap combine_variables else nothing)
   (* We need the runtime to initialize hoisted allocations *)
   |> (if !optimize_hoist_allocations && not !opt_no_rts then concatMap (hoist_allocations recursive_functions) else nothing)
-  |> (if !optimize_hoist_allocations && !optimize_experimental then concatMap hoist_alias else nothing)
 
 (**************************************************************************)
 (* 6. Code generation                                                     *)
 (**************************************************************************)
 
 let sgen_id id = Util.zencode_string (string_of_id id)
+let sgen_name id = string_of_name id
 let codegen_id id = string (sgen_id id)
 
 let sgen_function_id id =
@@ -1286,9 +1184,9 @@ let rec sgen_ctyp = function
   | CT_unit -> "unit"
   | CT_bit -> "fbits"
   | CT_bool -> "bool"
-  | CT_fbits _ -> "fbits"
+  | CT_fbits _ -> "uint64_t"
   | CT_sbits _ -> "sbits"
-  | CT_fint _ -> "mach_int"
+  | CT_fint _ -> "int64_t"
   | CT_lint -> "sail_int"
   | CT_lbits _ -> "lbits"
   | CT_tup _ as tup -> "struct " ^ Util.zencode_string ("tuple_" ^ string_of_ctyp tup)
@@ -1336,23 +1234,23 @@ let sgen_cval_param (frag, ctyp) =
 let sgen_cval = function (frag, _) -> string_of_fragment frag
 
 let rec sgen_clexp = function
-  | CL_id (id, _) -> "&" ^ sgen_id id
+  | CL_id (Have_exception _, _) -> "have_exception"
+  | CL_id (Current_exception _, _) -> "current_exception"
+  | CL_id (Return _, _) -> assert false
+  | CL_id (Name (id, _), _) -> "&" ^ sgen_id id
   | CL_field (clexp, field) -> "&((" ^ sgen_clexp clexp ^ ")->" ^ Util.zencode_string field ^ ")"
   | CL_tuple (clexp, n) -> "&((" ^ sgen_clexp clexp ^ ")->ztup" ^ string_of_int n ^ ")"
   | CL_addr clexp -> "(*(" ^ sgen_clexp clexp ^ "))"
-  | CL_have_exception -> "have_exception"
-  | CL_current_exception _ -> "current_exception"
-  | CL_return _ -> assert false
   | CL_void -> assert false
 
 let rec sgen_clexp_pure = function
-  | CL_id (id, _) -> sgen_id id
+  | CL_id (Have_exception _, _) -> "have_exception"
+  | CL_id (Current_exception _, _) -> "current_exception"
+  | CL_id (Return _, _) -> assert false
+  | CL_id (Name (id, _), _) -> sgen_id id
   | CL_field (clexp, field) -> sgen_clexp_pure clexp ^ "." ^ Util.zencode_string field
   | CL_tuple (clexp, n) -> sgen_clexp_pure clexp ^ ".ztup" ^ string_of_int n
   | CL_addr clexp -> "(*(" ^ sgen_clexp_pure clexp ^ "))"
-  | CL_have_exception -> "have_exception"
-  | CL_current_exception _ -> "current_exception"
-  | CL_return _ -> assert false
   | CL_void -> assert false
 
 (** Generate instructions to copy from a cval to a clexp. This will
@@ -1397,16 +1295,13 @@ let rec codegen_instr fid ctx (I_aux (instr, (_, l))) =
   let open Printf in
   match instr with
   | I_decl (ctyp, id) when is_stack_ctyp ctyp ->
-     ksprintf string "  %s %s;" (sgen_ctyp ctyp) (sgen_id id)
+     ksprintf string "  %s %s;" (sgen_ctyp ctyp) (sgen_name id)
   | I_decl (ctyp, id) ->
-     ksprintf string "  %s %s;" (sgen_ctyp ctyp) (sgen_id id) ^^ hardline
-     ^^ ksprintf string "  CREATE(%s)(&%s);" (sgen_ctyp_name ctyp) (sgen_id id)
+     ksprintf string "  %s %s;" (sgen_ctyp ctyp) (sgen_name id) ^^ hardline
+     ^^ ksprintf string "  CREATE(%s)(&%s);" (sgen_ctyp_name ctyp) (sgen_name id)
 
   | I_copy (clexp, cval) -> codegen_conversion l clexp cval
 
-  | I_alias (clexp, cval) ->
-     ksprintf string "  %s = %s;" (sgen_clexp_pure clexp) (sgen_cval cval)
-
   | I_jump (cval, label) ->
      ksprintf string "  if (%s) goto %s;" (sgen_cval cval) label
 
@@ -1488,9 +1383,7 @@ let rec codegen_instr fid ctx (I_aux (instr, (_, l))) =
        | "undefined_vector", _ -> Printf.sprintf "UNDEFINED(vector_%s)" (sgen_ctyp_name ctyp)
        | fname, _ -> fname
      in
-     if fname = "sail_assert" && !optimize_experimental then
-       empty
-     else if fname = "reg_deref" then
+     if fname = "reg_deref" then
        if is_stack_ctyp ctyp then
          string (Printf.sprintf  "  %s = *(%s);" (sgen_clexp_pure x) c_args)
        else
@@ -1504,7 +1397,7 @@ let rec codegen_instr fid ctx (I_aux (instr, (_, l))) =
   | I_clear (ctyp, id) when is_stack_ctyp ctyp ->
      empty
   | I_clear (ctyp, id) ->
-     string (Printf.sprintf "  KILL(%s)(&%s);" (sgen_ctyp_name ctyp) (sgen_id id))
+     string (Printf.sprintf "  KILL(%s)(&%s);" (sgen_ctyp_name ctyp) (sgen_name id))
 
   | I_init (ctyp, id, cval) ->
      codegen_instr fid ctx (idecl ctyp id) ^^ hardline
@@ -1515,9 +1408,9 @@ let rec codegen_instr fid ctx (I_aux (instr, (_, l))) =
      ^^ codegen_conversion Parse_ast.Unknown (CL_id (id, ctyp)) cval
 
   | I_reset (ctyp, id) when is_stack_ctyp ctyp ->
-     string (Printf.sprintf "  %s %s;" (sgen_ctyp ctyp) (sgen_id id))
+     string (Printf.sprintf "  %s %s;" (sgen_ctyp ctyp) (sgen_name id))
   | I_reset (ctyp, id) ->
-     string (Printf.sprintf "  RECREATE(%s)(&%s);" (sgen_ctyp_name ctyp) (sgen_id id))
+     string (Printf.sprintf "  RECREATE(%s)(&%s);" (sgen_ctyp_name ctyp) (sgen_name id))
 
   | I_return cval ->
      string (Printf.sprintf "  return %s;" (sgen_cval cval))
@@ -1536,24 +1429,24 @@ let rec codegen_instr fid ctx (I_aux (instr, (_, l))) =
        | CT_bool -> "false", []
        | CT_enum (_, ctor :: _) -> sgen_id ctor, [] 
        | CT_tup ctyps when is_stack_ctyp ctyp ->
-          let gs = gensym () in
+          let gs = ngensym () in
           let fold (inits, prev) (n, ctyp) =
             let init, prev' = codegen_exn_return ctyp in
             Printf.sprintf ".ztup%d = %s" n init :: inits, prev @ prev'
           in
           let inits, prev = List.fold_left fold ([], []) (List.mapi (fun i x -> (i, x)) ctyps) in
-          sgen_id gs,
-          [Printf.sprintf "struct %s %s = { " (sgen_ctyp_name ctyp) (sgen_id gs)
+          sgen_name gs,
+          [Printf.sprintf "struct %s %s = { " (sgen_ctyp_name ctyp) (sgen_name gs)
            ^ Util.string_of_list ", " (fun x -> x) inits ^ " };"] @ prev
        | CT_struct (id, ctors) when is_stack_ctyp ctyp ->
-          let gs = gensym () in
+          let gs = ngensym () in
           let fold (inits, prev) (id, ctyp) =
             let init, prev' = codegen_exn_return ctyp in
             Printf.sprintf ".%s = %s" (sgen_id id) init :: inits, prev @ prev'
           in
           let inits, prev = List.fold_left fold ([], []) ctors in
-          sgen_id gs,
-          [Printf.sprintf "struct %s %s = { " (sgen_ctyp_name ctyp) (sgen_id gs)
+          sgen_name gs,
+          [Printf.sprintf "struct %s %s = { " (sgen_ctyp_name ctyp) (sgen_name gs)
            ^ Util.string_of_list ", " (fun x -> x) inits ^ " };"] @ prev
        | ctyp -> c_error ("Cannot create undefined value for type: " ^ string_of_ctyp ctyp)
      in
@@ -1575,7 +1468,7 @@ let rec codegen_instr fid ctx (I_aux (instr, (_, l))) =
   | I_raw str ->
      string ("  " ^ str)
 
-  | I_end -> assert false
+  | I_end _ -> assert false
 
   | I_match_failure ->
      string ("  sail_match_failure(\"" ^ String.escaped (string_of_id fid) ^ "\");")
@@ -2014,13 +1907,13 @@ let is_decl = function
 
 let codegen_decl = function
   | I_aux (I_decl (ctyp, id), _) ->
-     string (Printf.sprintf "%s %s;" (sgen_ctyp ctyp) (sgen_id id))
+     string (Printf.sprintf "%s %s;" (sgen_ctyp ctyp) (sgen_name id))
   | _ -> assert false
 
 let codegen_alloc = function
   | I_aux (I_decl (ctyp, id), _) when is_stack_ctyp ctyp -> empty
   | I_aux (I_decl (ctyp, id), _) ->
-     string (Printf.sprintf "  CREATE(%s)(&%s);" (sgen_ctyp_name ctyp) (sgen_id id))
+     string (Printf.sprintf "  CREATE(%s)(&%s);" (sgen_ctyp_name ctyp) (sgen_name id))
   | _ -> assert false
 
 let codegen_def' ctx = function
@@ -2101,10 +1994,10 @@ let codegen_def' ctx = function
   | CDEF_let (number, bindings, instrs) ->
      let instrs = add_local_labels instrs in
      let setup =
-       List.concat (List.map (fun (id, ctyp) -> [idecl ctyp id]) bindings)
+       List.concat (List.map (fun (id, ctyp) -> [idecl ctyp (name id)]) bindings)
      in
      let cleanup =
-       List.concat (List.map (fun (id, ctyp) -> [iclear ctyp id]) bindings)
+       List.concat (List.map (fun (id, ctyp) -> [iclear ctyp (name id)]) bindings)
      in
      separate_map hardline (fun (id, ctyp) -> string (Printf.sprintf "%s %s;" (sgen_ctyp ctyp) (sgen_id id))) bindings
      ^^ hardline ^^ string (Printf.sprintf "static void create_letbind_%d(void) " number)
diff --git a/src/jib/c_backend.mli b/src/jib/c_backend.mli
index 7314eb5a..3e8c426b 100644
--- a/src/jib/c_backend.mli
+++ b/src/jib/c_backend.mli
@@ -100,7 +100,6 @@ val optimize_primops : bool ref
 val optimize_hoist_allocations : bool ref
 val optimize_struct_updates : bool ref
 val optimize_alias : bool ref
-val optimize_experimental : bool ref
 
 (** Convert a typ to a IR ctyp *)
 val ctyp_of_typ : Jib_compile.ctx -> Ast.typ -> ctyp
diff --git a/src/jib/jib_compile.ml b/src/jib/jib_compile.ml
index 27f833d8..4a72ffff 100644
--- a/src/jib/jib_compile.ml
+++ b/src/jib/jib_compile.ml
@@ -61,6 +61,8 @@ let opt_debug_function = ref ""
 let opt_debug_flow_graphs = ref false
 let opt_memo_cache = ref false
 
+let ngensym () = name (gensym ())
+
 (**************************************************************************)
 (* 4. Conversion to low-level AST                                         *)
 (**************************************************************************)
@@ -183,26 +185,26 @@ let rec compile_aval l ctx = function
      begin
        try
          let _, ctyp = Bindings.find id ctx.locals in
-         [], (F_id id, ctyp), []
+         [], (F_id (name id), ctyp), []
        with
        | Not_found ->
-          [], (F_id id, ctyp_of_typ ctx (lvar_typ typ)), []
+          [], (F_id (name id), ctyp_of_typ ctx (lvar_typ typ)), []
      end
 
   | AV_ref (id, typ) ->
-     [], (F_ref id, CT_ref (ctyp_of_typ ctx (lvar_typ typ))), []
+     [], (F_ref (name id), CT_ref (ctyp_of_typ ctx (lvar_typ typ))), []
 
   | AV_lit (L_aux (L_string str, _), typ) ->
      [], (F_lit (V_string (String.escaped str)), 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) ->
-     let gs = gensym () in
+     let gs = ngensym () in
      [iinit CT_lint gs (F_lit (V_int n), CT_fint 64)],
      (F_id gs, CT_lint),
      [iclear CT_lint gs]
 
   | AV_lit (L_aux (L_num n, _), typ) ->
-     let gs = gensym () in
+     let gs = ngensym () in
      [iinit CT_lint gs (F_lit (V_string (Big_int.to_string n)), CT_string)],
      (F_id gs, CT_lint),
      [iclear CT_lint gs]
@@ -214,7 +216,7 @@ let rec compile_aval l ctx = function
   | AV_lit (L_aux (L_false, _), _) -> [], (F_lit (V_bool false), CT_bool), []
 
   | AV_lit (L_aux (L_real str, _), _) ->
-     let gs = gensym () in
+     let gs = ngensym () in
      [iinit CT_real gs (F_lit (V_string str), CT_string)],
      (F_id gs, CT_real),
      [iclear CT_real gs]
@@ -230,7 +232,7 @@ let rec compile_aval l ctx = function
      let setup = List.concat (List.map (fun (setup, _, _) -> setup) elements) in
      let cleanup = List.concat (List.rev (List.map (fun (_, _, cleanup) -> cleanup) elements)) in
      let tup_ctyp = CT_tup (List.map cval_ctyp cvals) in
-     let gs = gensym () in
+     let gs = ngensym () in
      setup
      @ [idecl tup_ctyp gs]
      @ List.mapi (fun n cval -> icopy l (CL_tuple (CL_id (gs, tup_ctyp), n)) cval) cvals,
@@ -240,7 +242,7 @@ let rec compile_aval l ctx = function
 
   | AV_record (fields, typ) ->
      let ctyp = ctyp_of_typ ctx typ in
-     let gs = gensym () in
+     let gs = ngensym () in
      let compile_fields (id, aval) =
        let field_setup, cval, field_cleanup = compile_aval l ctx aval in
        field_setup
@@ -278,7 +280,7 @@ let rec compile_aval l ctx = function
      let bitstring avals = F_lit (V_bits (List.map value_of_aval_bit avals)) in
      let first_chunk = bitstring (Util.take (len mod 64) avals) in
      let chunks = Util.drop (len mod 64) avals |> chunkify 64 |> List.map bitstring in
-     let gs = gensym () in
+     let gs = ngensym () in
      [iinit (CT_lbits true) gs (first_chunk, CT_fbits (len mod 64, true))]
      @ List.map (fun chunk -> ifuncall (CL_id (gs, CT_lbits true))
                                        (mk_id "append_64")
@@ -295,7 +297,7 @@ let rec compile_aval l ctx = function
        | Ord_aux (Ord_dec, _) -> true
        | Ord_aux (Ord_var _, _) -> raise (Reporting.err_general l "Polymorphic vector direction found")
      in
-     let gs = gensym () in
+     let gs = ngensym () in
      let ctyp = CT_fbits (len, direction) in
      let mask i = V_bits (Util.list_init (63 - i) (fun _ -> Sail2_values.B0) @ [Sail2_values.B1] @ Util.list_init i (fun _ -> Sail2_values.B0)) in
      let aval_mask i aval =
@@ -323,7 +325,7 @@ let rec compile_aval l ctx = function
        | Ord_aux (Ord_var _, _) -> raise (Reporting.err_general l "Polymorphic vector direction found")
      in
      let vector_ctyp = CT_vector (direction, ctyp_of_typ ctx typ) in
-     let gs = gensym () in
+     let gs = ngensym () in
      let aval_set i aval =
        let setup, cval, cleanup = compile_aval l ctx aval in
        setup
@@ -346,7 +348,7 @@ let rec compile_aval l ctx = function
        | Typ_app (id, [A_aux (A_typ typ, _)]) when string_of_id id = "list" -> ctyp_of_typ ctx typ
        | _ -> raise (Reporting.err_general l "Invalid list type")
      in
-     let gs = gensym () in
+     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; (F_id gs, CT_list ctyp)]] @ cleanup
@@ -384,7 +386,7 @@ let compile_funcall l ctx id args typ =
     else if ctyp_equal ctyp have_ctyp then
       cval
     else
-      let gs = gensym () in
+      let gs = ngensym () in
       setup := iinit ctyp gs cval :: !setup;
       cleanup := iclear ctyp gs :: !cleanup;
       (F_id gs, ctyp)
@@ -399,7 +401,7 @@ let compile_funcall l ctx id args typ =
   if ctyp_equal (clexp_ctyp clexp) ret_ctyp then
     ifuncall clexp id setup_args
   else
-    let gs = gensym () in
+    let gs = ngensym () in
     iblock [idecl ret_ctyp gs;
             ifuncall (CL_id (gs, ret_ctyp)) id setup_args;
             icopy l clexp (F_id gs, ret_ctyp);
@@ -414,30 +416,37 @@ let rec apat_ctyp ctx (AP_aux (apat, _, _)) =
   | AP_cons (apat, _) -> CT_list (apat_ctyp ctx apat)
   | AP_wild typ | AP_nil typ | AP_id (_, typ) -> ctyp_of_typ ctx typ
   | AP_app (_, _, typ) -> ctyp_of_typ ctx typ
+  | AP_as (_, _, typ) -> ctyp_of_typ ctx typ
 
 let rec compile_match ctx (AP_aux (apat_aux, env, l)) cval case_label =
   let ctx = { ctx with local_env = env } in
   match apat_aux, cval with
   | AP_id (pid, _), (frag, ctyp) when Env.is_union_constructor pid ctx.tc_env ->
-     [ijump (F_op (F_field (frag, "kind"), "!=", F_lit (V_ctor_kind (string_of_id pid))), CT_bool) case_label],
+     [ijump (F_ctor_kind (frag, pid, [], ctyp), CT_bool) case_label],
      [],
      ctx
 
   | AP_global (pid, typ), (frag, ctyp) ->
      let global_ctyp = ctyp_of_typ ctx typ in
-     [icopy l (CL_id (pid, global_ctyp)) cval], [], ctx
+     [icopy l (CL_id (name pid, global_ctyp)) cval], [], ctx
 
   | AP_id (pid, _), (frag, ctyp) when is_ct_enum ctyp ->
      begin match Env.lookup_id pid ctx.tc_env with
-     | Unbound -> [idecl ctyp pid; icopy l (CL_id (pid, ctyp)) (frag, ctyp)], [], ctx
-     | _ -> [ijump (F_op (F_id pid, "!=", frag), CT_bool) case_label], [], ctx
+     | Unbound -> [idecl ctyp (name pid); icopy l (CL_id (name pid, ctyp)) (frag, ctyp)], [], ctx
+     | _ -> [ijump (F_op (F_id (name pid), "!=", frag), CT_bool) case_label], [], ctx
      end
 
   | AP_id (pid, typ), _ ->
      let ctyp = cval_ctyp cval in
      let id_ctyp = ctyp_of_typ ctx typ in
      let ctx = { ctx with locals = Bindings.add pid (Immutable, id_ctyp) ctx.locals } in
-     [idecl id_ctyp pid; icopy l (CL_id (pid, id_ctyp)) cval], [iclear id_ctyp pid], ctx
+     [idecl id_ctyp (name pid); icopy l (CL_id (name pid, id_ctyp)) cval], [iclear id_ctyp (name pid)], ctx
+
+  | AP_as (apat, id, typ), _ ->
+     let id_ctyp = ctyp_of_typ ctx typ in
+     let instrs, cleanup, ctx = compile_match ctx apat cval case_label in
+     let ctx = { ctx with locals = Bindings.add id (Immutable, id_ctyp) ctx.locals } in
+     instrs @ [idecl id_ctyp (name id); icopy l (CL_id (name id, id_ctyp)) cval], iclear id_ctyp (name id) :: cleanup, ctx
 
   | AP_tup apats, (frag, ctyp) ->
      begin
@@ -456,25 +465,21 @@ let rec compile_match ctx (AP_aux (apat_aux, env, l)) cval case_label =
   | AP_app (ctor, apat, variant_typ), (frag, ctyp) ->
      begin match ctyp with
      | CT_variant (_, ctors) ->
-        let ctor_c_id = string_of_id ctor in
         let ctor_ctyp = Bindings.find ctor (ctor_bindings ctors) in
+        let pat_ctyp = apat_ctyp ctx apat in
         (* These should really be the same, something has gone wrong if they are not. *)
         if ctyp_equal ctor_ctyp (ctyp_of_typ ctx variant_typ) then
           raise (Reporting.err_general l (Printf.sprintf "%s is not the same type as %s" (string_of_ctyp ctor_ctyp) (string_of_ctyp (ctyp_of_typ ctx variant_typ))))
         else ();
-        let ctor_c_id, ctor_ctyp =
+        let unifiers, ctor_ctyp =
           if is_polymorphic ctor_ctyp then
-            let unification = List.map ctyp_suprema (ctyp_unify ctor_ctyp (apat_ctyp ctx apat)) in
-            (if List.length unification > 0 then
-               ctor_c_id ^ "_" ^ Util.string_of_list "_" (fun ctyp -> Util.zencode_string (string_of_ctyp ctyp)) unification
-             else
-               ctor_c_id),
-            ctyp_suprema (apat_ctyp ctx apat)
+            let unifiers = List.map ctyp_suprema (ctyp_unify ctor_ctyp pat_ctyp) in
+            unifiers, ctyp_suprema (apat_ctyp ctx apat)
           else
-            ctor_c_id, ctor_ctyp
+            [], ctor_ctyp
         in
-        let instrs, cleanup, ctx = compile_match ctx apat ((F_field (frag, Util.zencode_string ctor_c_id), ctor_ctyp)) case_label in
-        [ijump (F_op (F_field (frag, "kind"), "!=", F_lit (V_ctor_kind ctor_c_id)), CT_bool) case_label]
+        let instrs, cleanup, ctx = compile_match ctx apat (F_ctor_unwrap (ctor, unifiers, frag), ctor_ctyp) case_label in
+        [ijump (F_ctor_kind (frag, ctor, unifiers, pat_ctyp), CT_bool) case_label]
         @ instrs,
         cleanup,
         ctx
@@ -507,7 +512,9 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) =
      let binding_ctyp = ctyp_of_typ { ctx with local_env = body_env } binding_typ in
      let setup, call, cleanup = compile_aexp ctx binding in
      let letb_setup, letb_cleanup =
-       [idecl binding_ctyp id; iblock (setup @ [call (CL_id (id, binding_ctyp))] @ cleanup)], [iclear binding_ctyp id]
+       [idecl binding_ctyp (name id);
+        iblock (setup @ [call (CL_id (name id, binding_ctyp))] @ cleanup)],
+       [iclear binding_ctyp (name id)]
      in
      let ctx = { ctx with locals = Bindings.add id (mut, binding_ctyp) ctx.locals } in
      let setup, call, cleanup = compile_aexp ctx body in
@@ -524,7 +531,7 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) =
   | AE_case (aval, cases, typ) ->
      let ctyp = ctyp_of_typ ctx typ in
      let aval_setup, cval, aval_cleanup = compile_aval l ctx aval in
-     let case_return_id = gensym () in
+     let case_return_id = ngensym () in
      let finish_match_label = label "finish_match_" in
      let compile_case (apat, guard, body) =
        let trivial_guard = match guard with
@@ -536,13 +543,12 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) =
        let destructure, destructure_cleanup, ctx = compile_match ctx apat cval case_label in
        let guard_setup, guard_call, guard_cleanup = compile_aexp ctx guard in
        let body_setup, body_call, body_cleanup = compile_aexp ctx body in
-       let gs = gensym () in
+       let gs = ngensym () in
        let case_instrs =
-         destructure @ [icomment "end destructuring"]
+         destructure
          @ (if not trivial_guard then
               guard_setup @ [idecl CT_bool gs; guard_call (CL_id (gs, CT_bool))] @ guard_cleanup
               @ [iif (F_unary ("!", F_id gs), CT_bool) (destructure_cleanup @ [igoto case_label]) [] CT_unit]
-              @ [icomment "end guard"]
             else [])
          @ body_setup @ [body_call (CL_id (case_return_id, ctyp))] @ body_cleanup @ destructure_cleanup
          @ [igoto finish_match_label]
@@ -552,21 +558,19 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) =
        else
          [iblock case_instrs; ilabel case_label]
      in
-     [icomment "begin match"]
-     @ aval_setup @ [idecl ctyp case_return_id]
+     aval_setup @ [idecl ctyp case_return_id]
      @ List.concat (List.map compile_case cases)
      @ [imatch_failure ()]
      @ [ilabel finish_match_label],
      (fun clexp -> icopy l clexp (F_id case_return_id, ctyp)),
      [iclear ctyp case_return_id]
      @ aval_cleanup
-     @ [icomment "end match"]
 
   (* Compile try statement *)
   | AE_try (aexp, cases, typ) ->
      let ctyp = ctyp_of_typ ctx typ in
      let aexp_setup, aexp_call, aexp_cleanup = compile_aexp ctx aexp in
-     let try_return_id = gensym () in
+     let try_return_id = ngensym () in
      let handled_exception_label = label "handled_exception_" in
      let fallthrough_label = label "fallthrough_exception_" in
      let compile_case (apat, guard, body) =
@@ -576,11 +580,11 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) =
          | _ -> false
        in
        let try_label = label "try_" in
-       let exn_cval = (F_current_exception, ctyp_of_typ ctx (mk_typ (Typ_id (mk_id "exception")))) in
+       let exn_cval = (F_id current_exception, ctyp_of_typ ctx (mk_typ (Typ_id (mk_id "exception")))) in
        let destructure, destructure_cleanup, ctx = compile_match ctx apat exn_cval try_label in
        let guard_setup, guard_call, guard_cleanup = compile_aexp ctx guard in
        let body_setup, body_call, body_cleanup = compile_aexp ctx body in
-       let gs = gensym () in
+       let gs = ngensym () in
        let case_instrs =
          destructure @ [icomment "end destructuring"]
          @ (if not trivial_guard then
@@ -596,11 +600,11 @@ 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 (F_unary ("!", F_have_exception), CT_bool) handled_exception_label]
+      ijump (F_unary ("!", F_id have_exception), CT_bool) handled_exception_label]
      @ List.concat (List.map compile_case cases)
      @ [igoto fallthrough_label;
         ilabel handled_exception_label;
-        icopy l CL_have_exception (F_lit (V_bool false), CT_bool);
+        icopy l (CL_id (have_exception, CT_bool)) (F_lit (V_bool false), CT_bool);
         ilabel fallthrough_label],
      (fun clexp -> icopy l clexp (F_id try_return_id, ctyp)),
      []
@@ -631,7 +635,7 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) =
        | CT_struct (_, ctors) -> List.fold_left (fun m (k, v) -> Bindings.add k v m) Bindings.empty ctors
        | _ -> raise (Reporting.err_general l "Cannot perform record update for non-record type")
      in
-     let gs = gensym () in
+     let gs = ngensym () in
      let compile_fields (id, aval) =
        let field_setup, cval, field_cleanup = compile_aval l ctx aval in
        field_setup
@@ -650,7 +654,7 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) =
   | AE_short_circuit (SC_and, aval, aexp) ->
      let left_setup, cval, left_cleanup = compile_aval l ctx aval in
      let right_setup, call, right_cleanup = compile_aexp ctx aexp in
-     let gs = gensym () in
+     let gs = ngensym () in
      left_setup
      @ [ idecl CT_bool gs;
          iif cval
@@ -663,7 +667,7 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) =
   | AE_short_circuit (SC_or, aval, aexp) ->
      let left_setup, cval, left_cleanup = compile_aval l ctx aval in
      let right_setup, call, right_cleanup = compile_aexp ctx aexp in
-     let gs = gensym () in
+     let gs = ngensym () in
      left_setup
      @ [ idecl CT_bool gs;
          iif cval
@@ -681,7 +685,7 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) =
      let compile_fields (field_id, aval) =
        let field_setup, cval, field_cleanup = compile_aval l ctx aval in
        field_setup
-       @ [icopy l (CL_field (CL_id (id, ctyp_of_typ ctx typ), string_of_id field_id)) cval]
+       @ [icopy l (CL_field (CL_id (name id, ctyp_of_typ ctx typ), string_of_id field_id)) cval]
        @ field_cleanup
      in
      List.concat (List.map compile_fields (Bindings.bindings fields)),
@@ -695,7 +699,7 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) =
        | None -> ctyp_of_typ ctx assign_typ
      in
      let setup, call, cleanup = compile_aexp ctx aexp in
-     setup @ [call (CL_id (id, assign_ctyp))], (fun clexp -> icopy l clexp unit_fragment), cleanup
+     setup @ [call (CL_id (name id, assign_ctyp))], (fun clexp -> icopy l clexp unit_fragment), cleanup
 
   | AE_block (aexps, aexp, _) ->
      let block = compile_block ctx aexps in
@@ -707,8 +711,8 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) =
      let loop_end_label = label "wend_" in
      let cond_setup, cond_call, cond_cleanup = compile_aexp ctx cond in
      let body_setup, body_call, body_cleanup = compile_aexp ctx body in
-     let gs = gensym () in
-     let unit_gs = gensym () in
+     let gs = ngensym () in
+     let unit_gs = ngensym () in
      let loop_test = (F_unary ("!", F_id gs), CT_bool) in
      [idecl CT_bool gs; idecl CT_unit unit_gs]
      @ [ilabel loop_start_label]
@@ -729,8 +733,8 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) =
      let loop_end_label = label "until_" in
      let cond_setup, cond_call, cond_cleanup = compile_aexp ctx cond in
      let body_setup, body_call, body_cleanup = compile_aexp ctx body in
-     let gs = gensym () in
-     let unit_gs = gensym () in
+     let gs = ngensym () in
+     let unit_gs = ngensym () in
      let loop_test = (F_id gs, CT_bool) in
      [idecl CT_bool gs; idecl CT_unit unit_gs]
      @ [ilabel loop_start_label]
@@ -759,7 +763,7 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) =
        if ctyp_equal fn_return_ctyp (cval_ctyp cval) then
          [ireturn cval]
        else
-         let gs = gensym () in
+         let gs = ngensym () in
          [idecl fn_return_ctyp gs;
           icopy l (CL_id (gs, fn_return_ctyp)) cval;
           ireturn (F_id gs, fn_return_ctyp)]
@@ -775,7 +779,8 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) =
      (fun clexp -> icomment "unreachable after throw"),
      []
 
-  | AE_field (aval, id, _) ->
+  | AE_field (aval, id, typ) ->
+     let aval_ctyp = ctyp_of_typ ctx typ in
      let setup, cval, cleanup = compile_aval l ctx aval in
      let ctyp = match cval_ctyp cval with
        | CT_struct (struct_id, fields) ->
@@ -788,8 +793,19 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) =
        | _ ->
           raise (Reporting.err_unreachable l __POS__ "Field access on non-struct type in ANF representation!")
      in
+     let unifiers, ctyp =
+       if is_polymorphic ctyp then
+         let unifiers = List.map ctyp_suprema (ctyp_unify ctyp aval_ctyp) in
+         unifiers, ctyp_suprema aval_ctyp
+       else
+         [], ctyp
+     in
+     let field_str = match unifiers with
+       | [] -> Util.zencode_string (string_of_id id)
+       | _ -> Util.zencode_string (string_of_id id ^ "_" ^ Util.string_of_list "_" string_of_ctyp unifiers)
+     in
      setup,
-     (fun clexp -> icopy l clexp (F_field (fst cval, Util.zencode_string (string_of_id id)), ctyp)),
+     (fun clexp -> icopy l clexp (F_field (fst cval, field_str), ctyp)),
      cleanup
 
   | AE_for (loop_var, loop_from, loop_to, loop_step, Ord_aux (ord, _), body) ->
@@ -804,11 +820,11 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) =
 
      (* Loop variables *)
      let from_setup, from_call, from_cleanup = compile_aexp ctx loop_from in
-     let from_gs = gensym () in
+     let from_gs = ngensym () in
      let to_setup, to_call, to_cleanup = compile_aexp ctx loop_to in
-     let to_gs = gensym () in
+     let to_gs = ngensym () in
      let step_setup, step_call, step_cleanup = compile_aexp ctx loop_step in
-     let step_gs = gensym () in
+     let step_gs = ngensym () in
      let variable_init gs setup call cleanup =
        [idecl (CT_fint 64) gs;
         iblock (setup @ [call (CL_id (gs, CT_fint 64))] @ cleanup)]
@@ -817,7 +833,9 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) =
      let loop_start_label = label "for_start_" in
      let loop_end_label = label "for_end_" in
      let body_setup, body_call, body_cleanup = compile_aexp ctx body in
-     let body_gs = gensym () in
+     let body_gs = ngensym () in
+
+     let loop_var = name loop_var in
 
      variable_init from_gs from_setup from_call from_cleanup
      @ variable_init to_gs to_setup to_call to_cleanup
@@ -842,7 +860,7 @@ and compile_block ctx = function
   | exp :: exps ->
      let setup, call, cleanup = compile_aexp ctx exp in
      let rest = compile_block ctx exps in
-     let gs = gensym () in
+     let gs = ngensym () in
      iblock (setup @ [idecl CT_unit gs; call (CL_id (gs, CT_unit))] @ cleanup) :: rest
 
 (** Compile a sail type definition into a IR one. Most of the
@@ -892,14 +910,14 @@ let generate_cleanup instrs =
     | instr -> []
   in
   let is_clear ids = function
-    | I_aux (I_clear (_, id), _) -> IdSet.add id ids
+    | I_aux (I_clear (_, id), _) -> NameSet.add id ids
     | _ -> ids
   in
-  let cleaned = List.fold_left is_clear IdSet.empty instrs in
+  let cleaned = List.fold_left is_clear NameSet.empty instrs in
   instrs
   |> List.map generate_cleanup'
   |> List.concat
-  |> List.filter (fun (id, _) -> not (IdSet.mem id cleaned))
+  |> List.filter (fun (id, _) -> not (NameSet.mem id cleaned))
   |> List.map snd
 
 let fix_exception_block ?return:(return=None) ctx instrs =
@@ -927,8 +945,8 @@ let fix_exception_block ?return:(return=None) ctx instrs =
        @ rewrite_exception historic after
     | before, I_aux (I_throw cval, (_, l)) :: after ->
        before
-       @ [icopy l (CL_current_exception (cval_ctyp cval)) cval;
-          icopy l CL_have_exception (F_lit (V_bool true), CT_bool)]
+       @ [icopy l (CL_id (current_exception, cval_ctyp cval)) cval;
+          icopy l (CL_id (have_exception, CT_bool)) (F_lit (V_bool true), CT_bool)]
        @ generate_cleanup (historic @ before)
        @ [igoto end_block_label]
        @ rewrite_exception (historic @ before) after
@@ -941,7 +959,7 @@ let fix_exception_block ?return:(return=None) ctx instrs =
        if has_effect effects BE_escape then
          before
          @ [funcall;
-            iif (F_have_exception, CT_bool) (generate_cleanup (historic @ before) @ [igoto end_block_label]) [] CT_unit]
+            iif (F_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
@@ -958,10 +976,10 @@ let rec map_try_block f (I_aux (instr, aux)) =
     | I_decl _ | I_reset _ | I_init _ | I_reinit _ -> instr
     | I_if (cval, instrs1, instrs2, ctyp) ->
        I_if (cval, List.map (map_try_block f) instrs1, List.map (map_try_block f) instrs2, ctyp)
-    | I_funcall _ | I_copy _ | I_alias _ | I_clear _ | I_throw _ | I_return _ -> instr
+    | I_funcall _ | I_copy _ | I_clear _ | I_throw _ | I_return _ -> instr
     | I_block instrs -> I_block (List.map (map_try_block f) instrs)
     | I_try_block instrs -> I_try_block (f (List.map (map_try_block f) instrs))
-    | I_comment _ | I_label _ | I_goto _ | I_raw _ | I_jump _ | I_match_failure | I_undefined _ | I_end -> instr
+    | I_comment _ | I_label _ | I_goto _ | I_raw _ | I_jump _ | I_match_failure | I_undefined _ | I_end _ -> instr
   in
   I_aux (instr, aux)
 
@@ -979,7 +997,7 @@ let rec compile_arg_pat ctx label (P_aux (p_aux, (l, _)) as pat) ctyp =
   | _ ->
      let apat = anf_pat pat in
      let gs = gensym () in
-     let destructure, cleanup, _ = compile_match ctx apat (F_id gs, ctyp) label in
+     let destructure, cleanup, _ = compile_match ctx apat (F_id (name gs), ctyp) label in
      (gs, (destructure, cleanup))
 
 let rec compile_arg_pats ctx label (P_aux (p_aux, (l, _)) as pat) ctyps =
@@ -994,10 +1012,10 @@ let rec compile_arg_pats ctx label (P_aux (p_aux, (l, _)) as pat) ctyps =
      let arg_id, (destructure, cleanup) = compile_arg_pat ctx label pat (CT_tup ctyps) in
      let new_ids = List.map (fun ctyp -> gensym (), ctyp) ctyps in
      destructure
-     @ [idecl (CT_tup ctyps) arg_id]
-     @ List.mapi (fun i (id, ctyp) -> icopy l (CL_tuple (CL_id (arg_id, CT_tup ctyps), i)) (F_id id, ctyp)) new_ids,
+     @ [idecl (CT_tup ctyps) (name arg_id)]
+     @ List.mapi (fun i (id, ctyp) -> icopy l (CL_tuple (CL_id (name arg_id, CT_tup ctyps), i)) (F_id (name id), ctyp)) new_ids,
      List.map (fun (id, _) -> id, ([], [])) new_ids,
-     [iclear (CT_tup ctyps) arg_id]
+     [iclear (CT_tup ctyps) (name arg_id)]
      @ cleanup
 
 let combine_destructure_cleanup xs = List.concat (List.map fst xs), List.concat (List.rev (List.map snd xs))
@@ -1108,7 +1126,7 @@ and compile_def' n total ctx = function
   | DEF_reg_dec (DEC_aux (DEC_config (id, typ, exp), _)) ->
      let aexp = ctx.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 (id, ctyp_of_typ ctx typ))] @ cleanup 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
 
   | DEF_reg_dec (DEC_aux (_, (l, _))) ->
@@ -1161,8 +1179,8 @@ and compile_def' n total ctx = function
        compiled_args |> List.map snd |> combine_destructure_cleanup |> fix_destructure fundef_label
      in
 
-     let instrs = arg_setup @ destructure @ setup @ [call (CL_return ret_ctyp)] @ cleanup @ destructure_cleanup @ arg_cleanup in
-     let instrs = fix_early_return (CL_return ret_ctyp) instrs in
+     let instrs = arg_setup @ destructure @ setup @ [call (CL_id (return, ret_ctyp))] @ cleanup @ destructure_cleanup @ arg_cleanup in
+     let instrs = fix_early_return (CL_id (return, ret_ctyp)) instrs in
      let instrs = fix_exception ~return:(Some ret_ctyp) ctx instrs in
 
      if Id.compare (mk_id !opt_debug_function) id = 0 then
@@ -1179,10 +1197,15 @@ and compile_def' n total ctx = function
      if !opt_debug_flow_graphs then
        begin
          let instrs = Jib_optimize.(instrs |> optimize_unit |> flatten_instrs) in
-         let cfg = Jib_ssa.ssa instrs in
+         let root, _, cfg = Jib_ssa.control_flow_graph instrs in
+         let idom = Jib_ssa.immediate_dominators cfg root in
+         let _, cfg = Jib_ssa.ssa instrs in
          let out_chan = open_out (Util.zencode_string (string_of_id id) ^ ".gv") in
          Jib_ssa.make_dot out_chan cfg;
          close_out out_chan;
+         let out_chan = open_out (Util.zencode_string (string_of_id id) ^ ".dom.gv") in
+         Jib_ssa.make_dominators_dot out_chan idom cfg;
+         close_out out_chan;
        end;
 
      [CDEF_fundef (id, None, List.map fst compiled_args, instrs)], orig_ctx
@@ -1206,7 +1229,7 @@ and compile_def' n total ctx = function
      let aexp = ctx.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 = gensym () in
+     let gs = ngensym () in
      let end_label = label "let_end_" in
      let destructure, destructure_cleanup, _ = compile_match ctx apat (F_id gs, ctyp) end_label in
      let gs_setup, gs_cleanup =
@@ -1257,13 +1280,19 @@ let rec specialize_variants ctx prior =
     | CT_variant (id, ctors) when Id.compare id var_id = 0 -> CT_variant (id, new_ctors)
     | ctyp -> ctyp
   in
+  let fix_struct_ctyp struct_id new_fields = function
+    | CT_struct (id, ctors) when Id.compare id struct_id = 0 -> CT_struct (id, new_fields)
+    | ctyp -> ctyp
+  in
 
-  let specialize_constructor ctx ctor_id ctyp =
-    function
+  (* specialize_constructor is called on all instructions when we find
+     a constructor in a union type that is polymorphic. It's job is to
+     record all uses of that constructor so we can monomorphise it. *)
+  let specialize_constructor ctx ctor_id ctyp = function
     | I_aux (I_funcall (clexp, extern, id, [cval]), ((_, l) as aux)) as instr when Id.compare id ctor_id = 0 ->
        (* Work out how each call to a constructor in instantiated and add that to unifications *)
-       let unification = List.map ctyp_suprema (ctyp_unify ctyp (cval_ctyp cval)) in
-       let mono_id = append_id ctor_id ("_" ^ Util.string_of_list "_" (fun ctyp -> Util.zencode_string (string_of_ctyp ctyp)) unification) in
+       let unifiers = List.map ctyp_suprema (ctyp_unify ctyp (cval_ctyp cval)) in
+       let mono_id = append_id ctor_id ("_" ^ Util.string_of_list "_" (fun ctyp -> string_of_ctyp ctyp) unifiers) in
        unifications := Bindings.add mono_id (ctyp_suprema (cval_ctyp cval)) !unifications;
 
        (* We need to cast each cval to it's ctyp_suprema in order to put it in the most general constructor *)
@@ -1273,7 +1302,7 @@ let rec specialize_variants ctx prior =
            if ctyp_equal ctyp suprema then
              [], (unpoly frag, ctyp), []
            else
-             let gs = gensym () in
+             let gs = ngensym () in
              [idecl suprema gs;
               icopy l (CL_id (gs, suprema)) (unpoly frag, ctyp)],
              (F_id gs, suprema),
@@ -1297,17 +1326,36 @@ let rec specialize_variants ctx prior =
     | I_aux (I_funcall (clexp, extern, id, cvals), ((_, l) as aux)) as instr when Id.compare id ctor_id = 0 ->
        Reporting.unreachable l __POS__ "Multiple argument constructor found"
 
+    (* We have to be careful this is the only place where an F_ctor_kind can appear before calling specialize variants *)
+    | I_aux (I_jump ((F_ctor_kind (_, id, unifiers, pat_ctyp), CT_bool), _), _) as instr when Id.compare id ctor_id = 0 ->
+       let mono_id = append_id ctor_id ("_" ^ Util.string_of_list "_" (fun ctyp -> string_of_ctyp ctyp) unifiers) in
+       unifications := Bindings.add mono_id (ctyp_suprema pat_ctyp) !unifications;
+       instr
+
     | instr -> instr
   in
 
+  (* specialize_field performs the same job as specialize_constructor,
+     but for struct fields rather than union constructors. *)
+  let specialize_field ctx field_id ctyp = function
+    | I_aux (I_copy (CL_field (clexp, field_str), cval), aux) when string_of_id field_id = field_str ->
+       let unifiers = List.map ctyp_suprema (ctyp_unify ctyp (cval_ctyp cval)) in
+       let mono_id = append_id field_id ("_" ^ Util.string_of_list "_" (fun ctyp -> string_of_ctyp ctyp) unifiers) in
+       unifications := Bindings.add mono_id (ctyp_suprema (cval_ctyp cval)) !unifications;
+       I_aux (I_copy (CL_field (clexp, string_of_id mono_id), cval), aux)
+      
+    | instr -> instr
+  in
+  
   function
   | (CDEF_type (CTD_variant (var_id, ctors)) as cdef) :: cdefs ->
      let polymorphic_ctors = List.filter (fun (_, ctyp) -> is_polymorphic ctyp) ctors in
 
      let cdefs =
-       List.fold_left (fun cdefs (ctor_id, ctyp) -> List.map (cdef_map_instr (specialize_constructor ctx ctor_id ctyp)) cdefs)
-                      cdefs
-                      polymorphic_ctors
+       List.fold_left
+         (fun cdefs (ctor_id, ctyp) -> List.map (cdef_map_instr (specialize_constructor ctx ctor_id ctyp)) cdefs)
+         cdefs
+         polymorphic_ctors
      in
 
      let monomorphic_ctors = List.filter (fun (_, ctyp) -> not (is_polymorphic ctyp)) ctors in
@@ -1324,6 +1372,30 @@ let rec specialize_variants ctx prior =
      let prior = List.map (cdef_map_ctyp (map_ctyp (fix_variant_ctyp var_id new_ctors))) prior in
      specialize_variants ctx (CDEF_type (CTD_variant (var_id, new_ctors)) :: prior) cdefs
 
+  | (CDEF_type (CTD_struct (struct_id, fields)) as cdef) :: cdefs ->
+     let polymorphic_fields = List.filter (fun (_, ctyp) -> is_polymorphic ctyp) fields in
+
+     let cdefs =
+       List.fold_left
+         (fun cdefs (field_id, ctyp) -> List.map (cdef_map_instr (specialize_field ctx field_id ctyp)) cdefs)
+         cdefs
+         polymorphic_fields
+     in
+
+     let monomorphic_fields = List.filter (fun (_, ctyp) -> not (is_polymorphic ctyp)) fields in
+     let specialized_fields = Bindings.bindings !unifications in
+     let new_fields = monomorphic_fields @ specialized_fields in
+
+     let ctx = {
+         ctx with records = Bindings.add struct_id
+                              (List.fold_left (fun m (id, ctyp) -> Bindings.add id ctyp m) !unifications monomorphic_fields)
+                              ctx.records
+       } in
+
+     let cdefs = List.map (cdef_map_ctyp (map_ctyp (fix_struct_ctyp struct_id new_fields))) cdefs in
+     let prior = List.map (cdef_map_ctyp (map_ctyp (fix_struct_ctyp struct_id new_fields))) prior in     
+     specialize_variants ctx (CDEF_type (CTD_struct (struct_id, new_fields)) :: prior) cdefs
+     
   | cdef :: cdefs ->
      let remove_poly (I_aux (instr, aux)) =
        match instr with
diff --git a/src/jib/jib_compile.mli b/src/jib/jib_compile.mli
index f3bd8c76..a0cacc3c 100644
--- a/src/jib/jib_compile.mli
+++ b/src/jib/jib_compile.mli
@@ -63,6 +63,8 @@ val opt_debug_flow_graphs : bool ref
 (** Print the IR representation of a specific function. *)
 val opt_debug_function : string ref
 
+val ngensym : unit -> name
+  
 (** {2 Jib context} *)
 
 (** Context for compiling Sail to Jib. We need to pass a (global)
diff --git a/src/jib/jib_optimize.ml b/src/jib/jib_optimize.ml
index 889e650e..73b175a1 100644
--- a/src/jib/jib_optimize.ml
+++ b/src/jib/jib_optimize.ml
@@ -71,12 +71,6 @@ let optimize_unit instrs =
           I_aux (I_copy (CL_void, unit_cval cval), annot)
        | _ -> instr
        end
-    | I_aux (I_alias (clexp, cval), annot) as instr ->
-       begin match clexp_ctyp clexp with
-       | CT_unit ->
-          I_aux (I_alias (CL_void, unit_cval cval), annot)
-       | _ -> instr
-       end
     | instr -> instr
   in
   let non_pointless_copy (I_aux (aux, annot)) =
@@ -90,7 +84,7 @@ let flat_counter = ref 0
 let flat_id () =
   let id = mk_id ("local#" ^ string_of_int !flat_counter) in
   incr flat_counter;
-  id
+  name id
 
 let rec flatten_instrs = function
   | I_aux (I_decl (ctyp, decl_id), aux) :: instrs ->
@@ -127,3 +121,157 @@ let flatten_cdef =
     CDEF_let (n, bindings, flatten_instrs instrs)
 
   | cdef -> cdef
+
+let unique_per_function_ids cdefs =
+  let unique_id i = function
+    | Name (id, ssa_num) -> Name (append_id id ("#u" ^ string_of_int i), ssa_num)
+    | name -> name
+  in
+  let rec unique_instrs i = function
+    | I_aux (I_decl (ctyp, id), aux) :: rest ->
+       I_aux (I_decl (ctyp, unique_id i id), aux) :: unique_instrs i (instrs_rename id (unique_id i id) rest)
+    | I_aux (I_init (ctyp, id, cval), aux) :: rest ->
+       I_aux (I_init (ctyp, unique_id i id, cval), aux) :: unique_instrs i (instrs_rename id (unique_id i id) rest)
+    | I_aux (I_block instrs, aux) :: rest ->
+       I_aux (I_block (unique_instrs i instrs), aux) :: unique_instrs i rest
+    | I_aux (I_try_block instrs, aux) :: rest ->
+       I_aux (I_try_block (unique_instrs i instrs), aux) :: unique_instrs i rest
+    | I_aux (I_if (cval, then_instrs, else_instrs, ctyp), aux) :: rest ->
+       I_aux (I_if (cval, unique_instrs i then_instrs, unique_instrs i else_instrs, ctyp), aux) :: unique_instrs i rest
+    | instr :: instrs -> instr :: unique_instrs i instrs
+    | [] -> []
+  in
+  let unique_cdef i = function
+    | 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_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)
+  in
+  List.mapi unique_cdef cdefs
+
+let rec frag_subst id subst = function
+  | F_id id' -> if Name.compare id id' = 0 then subst else F_id id'
+  | F_ref reg_id -> F_ref reg_id
+  | F_lit vl -> F_lit vl
+  | F_op (frag1, op, frag2) -> F_op (frag_subst id subst frag1, op, frag_subst id subst frag2)
+  | F_unary (op, frag) -> F_unary (op, frag_subst id subst frag)
+  | F_call (op, frags) -> F_call (op, List.map (frag_subst id subst) frags)
+  | F_field (frag, field) -> F_field (frag_subst id subst frag, field)
+  | F_raw str -> F_raw str
+  | F_ctor_kind (frag, ctor, unifiers, ctyp) -> F_ctor_kind (frag_subst id subst frag, ctor, unifiers, ctyp)
+  | F_ctor_unwrap (ctor, unifiers, frag) -> F_ctor_unwrap (ctor, unifiers, frag_subst id subst frag)
+  | F_poly frag -> F_poly (frag_subst id subst frag)
+
+let cval_subst id subst (frag, ctyp) = frag_subst id subst frag, ctyp
+
+let rec instrs_subst id subst =
+  function
+  | (I_aux (I_decl (_, id'), _) :: _) as instrs when Name.compare id id' = 0 ->
+     instrs
+
+  | I_aux (I_init (ctyp, id', cval), aux) :: rest when Name.compare id id' = 0 ->
+     I_aux (I_init (ctyp, id', cval_subst id subst cval), aux) :: rest
+
+  | (I_aux (I_reset (_, id'), _) :: _) as instrs when Name.compare id id' = 0 ->
+     instrs
+
+  | I_aux (I_reinit (ctyp, id', cval), aux) :: rest when Name.compare id id' = 0 ->
+     I_aux (I_reinit (ctyp, id', cval_subst id subst cval), aux) :: rest
+
+  | I_aux (instr, aux) :: instrs ->
+     let instrs = instrs_subst id subst instrs in
+     let instr = match instr with
+       | I_decl (ctyp, id') -> I_decl (ctyp, id')
+       | I_init (ctyp, id', cval) -> I_init (ctyp, id', cval_subst id subst cval)
+       | I_jump (cval, label) -> I_jump (cval_subst id subst cval, label)
+       | I_goto label -> I_goto label
+       | I_label label -> I_label label
+       | I_funcall (clexp, extern, fid, args) -> I_funcall (clexp, extern, fid, List.map (cval_subst id subst) args)
+       | I_copy (clexp, cval) -> I_copy (clexp, cval_subst id subst cval)
+       | I_clear (clexp, id') -> I_clear (clexp, id')
+       | I_undefined ctyp -> I_undefined ctyp
+       | I_match_failure -> I_match_failure
+       | I_end id' -> I_end id'
+       | I_if (cval, then_instrs, else_instrs, ctyp) ->
+          I_if (cval_subst id subst cval, instrs_subst id subst then_instrs, instrs_subst id subst else_instrs, ctyp)
+       | I_block instrs -> I_block (instrs_subst id subst instrs)
+       | I_try_block instrs -> I_try_block (instrs_subst id subst instrs)
+       | I_throw cval -> I_throw (cval_subst id subst cval)
+       | I_comment str -> I_comment str
+       | I_raw str -> I_raw str
+       | I_return cval -> I_return cval
+       | I_reset (ctyp, id') -> I_reset (ctyp, id')
+       | I_reinit (ctyp, id', cval) -> I_reinit (ctyp, id', cval_subst id subst cval)
+     in
+     I_aux (instr, aux) :: instrs
+
+  | [] -> []
+
+let rec clexp_subst id subst = function
+  | CL_id (id', ctyp) when Name.compare id id' = 0 ->
+     assert (ctyp_equal ctyp (clexp_ctyp subst));
+     subst
+  | CL_id (id', ctyp) -> CL_id (id', ctyp)
+  | CL_field (clexp, field) -> CL_field (clexp_subst id subst clexp, field)
+  | CL_addr clexp -> CL_addr (clexp_subst id subst clexp)
+  | CL_tuple (clexp, n) -> CL_tuple (clexp_subst id subst clexp, n)
+  | CL_void -> CL_void
+
+let rec find_function fid = function
+  | CDEF_fundef (fid', heap_return, args, body) :: _ when Id.compare fid fid' = 0 ->
+     Some (heap_return, args, body)
+
+  | cdef :: cdefs -> find_function fid cdefs
+
+  | [] -> None
+
+let inline cdefs should_inline instrs =
+  let inlines = ref (-1) in
+
+  let replace_return subst = function
+    | I_aux (I_funcall (clexp, extern, fid, args), aux) ->
+       I_aux (I_funcall (clexp_subst return subst clexp, extern, fid, args), aux)
+    | I_aux (I_copy (clexp, cval), aux) ->
+       I_aux (I_copy (clexp_subst return subst clexp, cval), aux)
+    | instr -> instr
+  in
+
+  let replace_end label = function
+    | I_aux (I_end _, aux) -> I_aux (I_goto label, aux)
+    | I_aux (I_undefined _, aux) -> I_aux (I_goto label, aux)
+    | instr -> instr
+  in
+
+  let rec inline_instr = function
+    | I_aux (I_funcall (clexp, false, function_id, args), aux) as instr when should_inline function_id ->
+       begin match find_function function_id cdefs with
+       | Some (None, ids, body) ->
+          incr inlines;
+          let inline_label = label "end_inline_" in
+          let body = List.fold_right2 instrs_subst (List.map name ids) (List.map fst args) body in
+          let body = List.map (map_instr (replace_end inline_label)) body in
+          let body = List.map (map_instr (replace_return clexp)) body in
+          I_aux (I_block (body @ [ilabel inline_label]), aux)
+       | Some (Some _, ids, body) ->
+          (* Some _ is only introduced by C backend, so we don't
+             expect it at this point. *)
+          raise (Reporting.err_general (snd aux) "Unexpected return method in IR")
+       | None -> instr
+       end
+    | instr -> instr
+  in
+
+  let rec go instrs =
+    if !inlines <> 0 then
+      begin
+        inlines := 0;
+        let instrs = List.map (map_instr inline_instr) instrs in
+        go instrs
+      end
+    else
+      instrs
+  in
+  go instrs
diff --git a/src/jib/jib_optimize.mli b/src/jib/jib_optimize.mli
index beffa81e..78759d08 100644
--- a/src/jib/jib_optimize.mli
+++ b/src/jib/jib_optimize.mli
@@ -61,3 +61,6 @@ val optimize_unit : instr list -> instr list
 val flatten_instrs : instr list -> instr list
 val flatten_cdef : cdef -> cdef
 
+val unique_per_function_ids : cdef list -> cdef list
+
+val inline : cdef list -> (Ast.id -> bool) -> instr list -> instr list
diff --git a/src/jib/jib_ssa.ml b/src/jib/jib_ssa.ml
index 1f477696..a086f0b9 100644
--- a/src/jib/jib_ssa.ml
+++ b/src/jib/jib_ssa.ml
@@ -68,6 +68,15 @@ let make ~initial_size () = {
     nodes = Array.make initial_size None
   }
 
+let get_vertex graph n = graph.nodes.(n)
+
+let iter_graph f graph =
+  for n = 0 to graph.next - 1 do
+    match graph.nodes.(n) with
+    | Some (x, y, z) -> f x y z
+    | None -> ()
+  done
+                       
 (** Add a vertex to a graph, returning the node index *)
 let add_vertex data graph =
   let n = graph.next in
@@ -133,8 +142,11 @@ let prune visited graph =
 type cf_node =
   | CF_label of string
   | CF_block of instr list
+  | CF_guard of cval
   | CF_start
 
+let cval_not (f, ctyp) = (F_unary ("!", f), ctyp)
+
 let control_flow_graph instrs =
   let module StringMap = Map.Make(String) in
   let labels = ref StringMap.empty in
@@ -150,14 +162,14 @@ let control_flow_graph instrs =
 
   let cf_split (I_aux (aux, _)) =
     match aux with
-    | I_block _ | I_label _ | I_goto _ | I_jump _ | I_if _ | I_end | I_match_failure | I_undefined _ -> true
+    | I_block _ | I_label _ | I_goto _ | I_jump _ | I_if _ | I_end _ | I_match_failure | I_undefined _ -> true
     | _ -> false
   in
 
   let rec cfg preds instrs =
     let before, after = instr_split_at cf_split instrs in
     let last = match after with
-      | I_aux (I_label _, _) :: _ -> []
+      | I_aux ((I_label _ | I_goto _ | I_jump _), _) :: _ -> []
       | instr :: _ -> [instr]
       | _ -> []
     in
@@ -174,7 +186,7 @@ let control_flow_graph instrs =
        let e = cfg preds else_instrs in
        cfg (t @ e) after
 
-    | I_aux ((I_end | I_match_failure | I_undefined _), _) :: after ->
+    | I_aux ((I_end _ | I_match_failure | I_undefined _), _) :: after ->
        cfg [] after
 
     | I_aux (I_goto label, _) :: after ->
@@ -182,8 +194,11 @@ let control_flow_graph instrs =
        cfg [] after
 
     | I_aux (I_jump (cval, label), _) :: after ->
-       List.iter (fun p -> add_edge p (StringMap.find label !labels) graph) preds;
-       cfg preds after
+       let t = add_vertex ([], CF_guard cval) graph in
+       let f = add_vertex ([], CF_guard (cval_not cval)) graph in
+       List.iter (fun p -> add_edge p t graph; add_edge p f graph) preds;
+       add_edge t (StringMap.find label !labels) graph;
+       cfg [f] after
 
     | I_aux (I_label label, _) :: after ->
        cfg (StringMap.find label !labels :: preds) after
@@ -351,55 +366,56 @@ let dominance_frontiers graph root idom children =
 (**************************************************************************)
 
 type ssa_elem =
-  | Phi of Ast.id * Ast.id list
+  | Phi of Jib.name * Jib.ctyp * Jib.name list
+  | Pi of Jib.cval list
 
 let place_phi_functions graph df =
-  let defsites = ref Bindings.empty in
+  let defsites = ref NameCTMap.empty in
 
-  let all_vars = ref IdSet.empty in
+  let all_vars = ref NameCTSet.empty in
 
   let rec all_decls = function
-    | I_aux (I_decl (_, id), _) :: instrs ->
-       IdSet.add id (all_decls instrs)
+    | I_aux ((I_init (ctyp, id, _) | I_decl (ctyp, id)), _) :: instrs ->
+       NameCTSet.add (id, ctyp) (all_decls instrs)
     | _ :: instrs -> all_decls instrs
-    | [] -> IdSet.empty
+    | [] -> NameCTSet.empty
   in
 
   let orig_A n =
     match graph.nodes.(n) with
     | Some ((_, CF_block instrs), _, _) ->
-       let vars = List.fold_left IdSet.union IdSet.empty (List.map instr_writes instrs) in
-       let vars = IdSet.diff vars (all_decls instrs) in
-       all_vars := IdSet.union vars !all_vars;
+       let vars = List.fold_left NameCTSet.union NameCTSet.empty (List.map instr_typed_writes instrs) in
+       let vars = NameCTSet.diff vars (all_decls instrs) in
+       all_vars := NameCTSet.union vars !all_vars;
        vars
-    | Some _ -> IdSet.empty
-    | None -> IdSet.empty
+    | Some _ -> NameCTSet.empty
+    | None -> NameCTSet.empty
   in
-  let phi_A = ref Bindings.empty in
+  let phi_A = ref NameCTMap.empty in
 
   for n = 0 to graph.next - 1 do
-    IdSet.iter (fun a ->
-        let ds = match Bindings.find_opt a !defsites with Some ds -> ds | None -> IntSet.empty in
-        defsites := Bindings.add a (IntSet.add n ds) !defsites
+    NameCTSet.iter (fun a ->
+        let ds = match NameCTMap.find_opt a !defsites with Some ds -> ds | None -> IntSet.empty in
+        defsites := NameCTMap.add a (IntSet.add n ds) !defsites
       ) (orig_A n)
   done;
 
-  IdSet.iter (fun a ->
-      let workset = ref (Bindings.find a !defsites) in
+  NameCTSet.iter (fun a ->
+      let workset = ref (NameCTMap.find a !defsites) in
       while not (IntSet.is_empty !workset) do
         let n = IntSet.choose !workset in
         workset := IntSet.remove n !workset;
         IntSet.iter (fun y ->
-            let phi_A_a = match Bindings.find_opt a !phi_A with Some set -> set | None -> IntSet.empty in
+            let phi_A_a = match NameCTMap.find_opt a !phi_A with Some set -> set | None -> IntSet.empty in
             if not (IntSet.mem y phi_A_a) then
               begin
                 begin match graph.nodes.(y) with
                 | Some ((phis, cfnode), preds, succs) ->
-                   graph.nodes.(y) <- Some ((Phi (a, Util.list_init (IntSet.cardinal preds) (fun _ -> a)) :: phis, cfnode), preds, succs)
+                   graph.nodes.(y) <- Some ((Phi (fst a, snd a, Util.list_init (IntSet.cardinal preds) (fun _ -> fst a)) :: phis, cfnode), preds, succs)
                 | None -> assert false
                 end;
-                phi_A := Bindings.add a (IntSet.add y phi_A_a) !phi_A;
-                if not (IdSet.mem a (orig_A y)) then
+                phi_A := NameCTMap.add a (IntSet.add y phi_A_a) !phi_A;
+                if not (NameCTSet.mem a (orig_A y)) then
                   workset := IntSet.add y !workset
               end
           ) df.(n)
@@ -407,49 +423,53 @@ let place_phi_functions graph df =
     ) !all_vars
 
 let rename_variables graph root children =
-  let counts = ref Bindings.empty in
-  let stacks = ref Bindings.empty in
+  let counts = ref NameMap.empty in
+  let stacks = ref NameMap.empty in
 
   let get_count id =
-    match Bindings.find_opt id !counts with Some n -> n | None -> 0
+    match NameMap.find_opt id !counts with Some n -> n | None -> 0
   in
   let top_stack id =
-    match Bindings.find_opt id !stacks with Some (x :: _) -> x | (Some [] | None) -> 0
+    match NameMap.find_opt id !stacks with Some (x :: _) -> x | (Some [] | None) -> 0
   in
   let push_stack id n =
-    stacks := Bindings.add id (n :: match Bindings.find_opt id !stacks with Some s -> s | None -> []) !stacks
+    stacks := NameMap.add id (n :: match NameMap.find_opt id !stacks with Some s -> s | None -> []) !stacks
+  in
+
+  let ssa_name i = function
+    | Name (id, _) -> Name (id, i)
+    | Have_exception _ -> Have_exception i
+    | Current_exception _ -> Current_exception i
+    | Return _ -> Return i
   in
 
   let rec fold_frag = function
     | F_id id ->
        let i = top_stack id in
-       F_id (append_id id ("_" ^ string_of_int i))
+       F_id (ssa_name i id)
     | F_ref id ->
        let i = top_stack id in
-       F_ref (append_id id ("_" ^ string_of_int i))
+       F_ref (ssa_name i id)
     | F_lit vl -> F_lit vl
-    | F_have_exception -> F_have_exception
-    | F_current_exception -> F_current_exception
     | F_op (f1, op, f2) -> F_op (fold_frag f1, op, fold_frag f2)
     | F_unary (op, f) -> F_unary (op, fold_frag f)
     | F_call (id, fs) -> F_call (id, List.map fold_frag fs)
     | F_field (f, field) -> F_field (fold_frag f, field)
     | F_raw str -> F_raw str
+    | F_ctor_kind (f, ctor, unifiers, ctyp) -> F_ctor_kind (fold_frag f, ctor, unifiers, ctyp)
+    | F_ctor_unwrap (ctor, unifiers, f) -> F_ctor_unwrap (ctor, unifiers, fold_frag f)
     | F_poly f -> F_poly (fold_frag f)
   in
 
   let rec fold_clexp = function
     | CL_id (id, ctyp) ->
        let i = get_count id + 1 in
-       counts := Bindings.add id i !counts;
+       counts := NameMap.add id i !counts;
        push_stack id i;
-       CL_id (append_id id ("_" ^ string_of_int i), ctyp)
+       CL_id (ssa_name i id, ctyp)
     | CL_field (clexp, field) -> CL_field (fold_clexp clexp, field)
     | CL_addr clexp -> CL_addr (fold_clexp clexp)
     | CL_tuple (clexp, n) -> CL_tuple (fold_clexp clexp, n)
-    | CL_current_exception ctyp -> CL_current_exception ctyp
-    | CL_have_exception -> CL_have_exception
-    | CL_return ctyp -> CL_return ctyp
     | CL_void -> CL_void
   in
 
@@ -465,15 +485,20 @@ let rename_variables graph root children =
          I_copy (fold_clexp clexp, cval)
       | I_decl (ctyp, id) ->
          let i = get_count id + 1 in
-         counts := Bindings.add id i !counts;
+         counts := NameMap.add id i !counts;
          push_stack id i;
-         I_decl (ctyp, append_id id ("_" ^ string_of_int i))
+         I_decl (ctyp, ssa_name i id)
       | I_init (ctyp, id, cval) ->
          let cval = fold_cval cval in
          let i = get_count id + 1 in
-         counts := Bindings.add id i !counts;
+         counts := NameMap.add id i !counts;
          push_stack id i;
-         I_init (ctyp, append_id id ("_" ^ string_of_int i), cval)
+         I_init (ctyp, ssa_name i id, cval)
+      | I_jump (cval, label) ->
+         I_jump (fold_cval cval, label)
+      | I_end id ->
+         let i = top_stack id in
+         I_end (ssa_name i id)
       | instr -> instr
     in
     I_aux (aux, annot)
@@ -483,24 +508,28 @@ let rename_variables graph root children =
     | CF_start -> CF_start
     | CF_block instrs -> CF_block (List.map ssa_instr instrs)
     | CF_label label -> CF_label label
+    | CF_guard cval -> CF_guard (fold_cval cval)
   in
 
   let ssa_ssanode = function
-    | Phi (id, args) ->
+    | Phi (id, ctyp, args) ->
        let i = get_count id + 1 in
-       counts := Bindings.add id i !counts;
+       counts := NameMap.add id i !counts;
        push_stack id i;
-       Phi (append_id id ("_" ^ string_of_int i), args)
+       Phi (ssa_name i id, ctyp, args)
+    | Pi _ -> assert false (* Should not be introduced at this point *)
   in
 
   let fix_phi j = function
-    | Phi (id, ids) ->
-       Phi (id, List.mapi (fun k a ->
-                    if k = j then
-                      let i = top_stack a in
-                      append_id a ("_" ^ string_of_int i)
-                    else a)
-                  ids)
+    | Phi (id, ctyp, ids) ->
+       let fix_arg k a =
+         if k = j then
+           let i = top_stack a in
+           ssa_name i a
+         else a
+       in
+       Phi (id, ctyp, List.mapi fix_arg ids)
+    | Pi _ -> assert false (* Should not be introduced at this point *)
   in
 
   let rec rename n =
@@ -529,6 +558,53 @@ let rename_variables graph root children =
   in
   rename root
 
+let place_pi_functions graph start idom children =
+  let get_guard = function
+    | CF_guard guard -> [guard]
+    | _ -> []
+  in
+  let get_pi_contents ssanodes =
+    List.concat (List.map (function Pi guards -> guards | _ -> []) ssanodes)
+  in
+
+  let rec go n =
+    begin match graph.nodes.(n) with
+    | Some ((ssa, cfnode), preds, succs) ->
+       let p = idom.(n) in
+       if p <> -1 then
+         begin match graph.nodes.(p) with
+         | Some ((dom_ssa, _), _, _) ->
+            let args = get_guard cfnode @ get_pi_contents dom_ssa in
+            graph.nodes.(n) <- Some ((Pi args :: ssa, cfnode), preds, succs)
+         | None -> assert false
+         end
+    | None -> assert false
+    end;
+    IntSet.iter go children.(n)
+  in
+  go start
+
+(** Remove p nodes. Assumes the graph is acyclic. *)
+let remove_nodes remove_cf graph =
+  for n = 0 to graph.next - 1 do
+    match graph.nodes.(n) with
+    | Some ((_, cfnode), preds, succs) when remove_cf cfnode ->
+       IntSet.iter (fun pred ->
+           match graph.nodes.(pred) with
+           | Some (content, preds', succs') ->
+              graph.nodes.(pred) <- Some (content, preds', IntSet.remove n (IntSet.union succs succs'))
+           | None -> assert false
+         ) preds;
+       IntSet.iter (fun succ ->
+           match graph.nodes.(succ) with
+           | Some (content, preds', succs') ->
+              graph.nodes.(succ) <- Some (content, IntSet.remove n (IntSet.union preds preds'), succs')
+           | None -> assert false
+         ) succs;
+       graph.nodes.(n) <- None
+    | _ -> ()
+  done
+
 let ssa instrs =
   let start, finish, cfg = control_flow_graph instrs in
   let idom = immediate_dominators cfg start in
@@ -536,36 +612,39 @@ let ssa instrs =
   let df = dominance_frontiers cfg start idom children in
   place_phi_functions cfg df;
   rename_variables cfg start children;
-  cfg
+  place_pi_functions cfg start idom children;
+  (* remove_guard_nodes (function CF_guard _ -> true | CF_label _ -> true | _ -> false) cfg; *)
+  start, cfg
 
 (* Debugging utilities for outputing Graphviz files. *)
 
+let string_of_ssainstr = function
+  | Phi (id, ctyp, args) ->
+     string_of_name id ^ " : " ^ string_of_ctyp ctyp ^ " = &phi;(" ^ Util.string_of_list ", " string_of_name args ^ ")"
+  | Pi cvals ->
+     "&pi;(" ^ Util.string_of_list ", " (fun (f, _) -> String.escaped (string_of_fragment ~zencode:false f)) cvals ^ ")"
+
 let string_of_phis = function
   | [] -> ""
-  | phis -> Util.string_of_list "\\l" (fun (Phi (id, args)) -> string_of_id id ^ " = phi(" ^ Util.string_of_list ", " string_of_id args ^ ")") phis ^ "\\l"
+  | phis -> Util.string_of_list "\\l" string_of_ssainstr phis ^ "\\l"
 
 let string_of_node = function
   | (phis, CF_label label) -> string_of_phis phis ^ label
   | (phis, CF_block instrs) -> string_of_phis phis ^ Util.string_of_list "\\l" (fun instr -> String.escaped (Pretty_print_sail.to_string (pp_instr ~short:true instr))) instrs
   | (phis, CF_start) -> string_of_phis phis ^ "START"
+  | (phis, CF_guard cval) -> string_of_phis phis ^ (String.escaped (Pretty_print_sail.to_string (pp_cval cval)))
 
 let vertex_color = function
   | (_, CF_start)   -> "peachpuff"
   | (_, CF_block _) -> "white"
   | (_, CF_label _) -> "springgreen"
-
-let edge_color node_from node_to =
-  match node_from, node_to with
-  | CF_block _, CF_block _ -> "black"
-  | CF_label _, CF_block _ -> "red"
-  | CF_block _, CF_label _ -> "blue"
-  | _, _ -> "deeppink"
+  | (_, CF_guard _) -> "yellow"
 
 let make_dot out_chan graph =
   Util.opt_colors := false;
   output_string out_chan "digraph DEPS {\n";
   let make_node i n =
-    output_string out_chan (Printf.sprintf "  n%i [label=\"%s\";shape=box;style=filled;fillcolor=%s];\n" i (string_of_node n) (vertex_color n))
+    output_string out_chan (Printf.sprintf "  n%i [label=\"%i\\n%s\\l\";shape=box;style=filled;fillcolor=%s];\n" i i (string_of_node n) (vertex_color n))
   in
   let make_line i s =
     output_string out_chan (Printf.sprintf "  n%i -> n%i [color=black];\n" i s)
@@ -584,7 +663,7 @@ let make_dominators_dot out_chan idom graph =
   Util.opt_colors := false;
   output_string out_chan "digraph DOMS {\n";
   let make_node i n =
-    output_string out_chan (Printf.sprintf "  n%i [label=\"%s\";shape=box;style=filled;fillcolor=%s];\n" i (string_of_node n) (vertex_color n))
+    output_string out_chan (Printf.sprintf "  n%i [label=\"%i\\n%s\\l\";shape=box;style=filled;fillcolor=%s];\n" i i (string_of_node n) (vertex_color n))
   in
   let make_line i s =
     output_string out_chan (Printf.sprintf "  n%i -> n%i [color=black];\n" i s)
diff --git a/src/jib/jib_ssa.mli b/src/jib/jib_ssa.mli
index 3796a114..b146861c 100644
--- a/src/jib/jib_ssa.mli
+++ b/src/jib/jib_ssa.mli
@@ -57,6 +57,12 @@ type 'a array_graph
    underlying array. *)
 val make : initial_size:int -> unit -> 'a array_graph
 
+module IntSet : Set.S with type elt = int
+  
+val get_vertex : 'a array_graph -> int -> ('a * IntSet.t * IntSet.t) option
+
+val iter_graph : ('a -> IntSet.t -> IntSet.t -> unit) -> 'a array_graph -> unit
+  
 (** Add a vertex to a graph, returning the index of the inserted
    vertex. If the number of vertices exceeds the size of the
    underlying array, then it is dynamically resized. *)
@@ -69,17 +75,25 @@ val add_edge : int -> int -> 'a array_graph -> unit
 type cf_node =
   | CF_label of string
   | CF_block of Jib.instr list
+  | CF_guard of Jib.cval
   | CF_start
 
 val control_flow_graph : Jib.instr list -> int * int list * ('a list * cf_node) array_graph
 
+(** [immediate_dominators graph root] will calculate the immediate
+   dominators for a control flow graph with a specified root node. *)
+val immediate_dominators : 'a array_graph -> int -> int array
+
 type ssa_elem =
-  | Phi of Ast.id * Ast.id list
+  | Phi of Jib.name * Jib.ctyp * Jib.name list
+  | Pi of Jib.cval list
 
 (** Convert a list of instructions into SSA form *)
-val ssa : Jib.instr list -> (ssa_elem list * cf_node) array_graph
+val ssa : Jib.instr list -> int * (ssa_elem list * cf_node) array_graph
 
 (** Output the control-flow graph in graphviz format for
    debugging. Can use 'dot -Tpng X.gv -o X.png' to generate a png
    image of the graph. *)
 val make_dot : out_channel -> (ssa_elem list * cf_node) array_graph -> unit
+
+val make_dominators_dot : out_channel -> int array -> (ssa_elem list * cf_node) array_graph -> unit
diff --git a/src/jib/jib_util.ml b/src/jib/jib_util.ml
index 81cd07ef..904e0209 100644
--- a/src/jib/jib_util.ml
+++ b/src/jib/jib_util.ml
@@ -82,12 +82,12 @@ let ifuncall ?loc:(l=Parse_ast.Unknown) clexp id cvals =
 let iextern ?loc:(l=Parse_ast.Unknown) clexp id cvals =
   I_aux (I_funcall (clexp, true, id, cvals), (instr_number (), l))
 
+let icall ?loc:(l=Parse_ast.Unknown) clexp extern id cvals =
+  I_aux (I_funcall (clexp, extern, id, cvals), (instr_number (), l))
+
 let icopy l clexp cval =
   I_aux (I_copy (clexp, cval), (instr_number (), l))
 
-let ialias l clexp cval =
-  I_aux (I_alias (clexp, cval), (instr_number (), l))
-
 let iclear ?loc:(l=Parse_ast.Unknown) ctyp id =
   I_aux (I_clear (ctyp, id), (instr_number (), l))
 
@@ -95,7 +95,7 @@ let ireturn ?loc:(l=Parse_ast.Unknown) cval =
   I_aux (I_return cval, (instr_number (), l))
 
 let iend ?loc:(l=Parse_ast.Unknown) () =
-  I_aux (I_end, (instr_number (), l))
+  I_aux (I_end (Return (-1)), (instr_number (), l))
 
 let iblock ?loc:(l=Parse_ast.Unknown) instrs =
   I_aux (I_block instrs, (instr_number (), l))
@@ -105,11 +105,13 @@ let itry_block ?loc:(l=Parse_ast.Unknown) instrs =
 
 let ithrow ?loc:(l=Parse_ast.Unknown) cval =
   I_aux (I_throw cval, (instr_number (), l))
+
 let icomment ?loc:(l=Parse_ast.Unknown) str =
   I_aux (I_comment str, (instr_number (), l))
 
 let ilabel ?loc:(l=Parse_ast.Unknown) label =
   I_aux (I_label label, (instr_number (), l))
+
 let igoto ?loc:(l=Parse_ast.Unknown) label =
   I_aux (I_goto label, (instr_number (), l))
 
@@ -125,25 +127,52 @@ let iraw ?loc:(l=Parse_ast.Unknown) str =
 let ijump ?loc:(l=Parse_ast.Unknown) cval label =
   I_aux (I_jump (cval, label), (instr_number (), l))
 
+module Name = struct
+  type t = name
+  let compare id1 id2 =
+    match id1, id2 with
+    | Name (x, n), Name (y, m) ->
+       let c1 = Id.compare x y in
+       if c1 = 0 then compare n m else c1
+    | Have_exception n, Have_exception m -> compare n m
+    | Current_exception n, Current_exception m -> compare n m
+    | Return n, Return m -> compare n m
+    | Name _, _ -> 1
+    | _, Name _ -> -1
+    | Have_exception _, _ -> 1
+    | _, Have_exception _ -> -1
+    | Current_exception _, _ -> 1
+    | _, Current_exception _ -> -1
+end
+
+module NameSet = Set.Make(Name)
+module NameMap = Map.Make(Name)
+
+let current_exception = Current_exception (-1)
+let have_exception = Have_exception (-1)
+let return = Return (-1)
+
+let name id = Name (id, -1)
+
 let rec frag_rename from_id to_id = function
-  | F_id id when Id.compare id from_id = 0 -> F_id to_id
+  | F_id id when Name.compare id from_id = 0 -> F_id to_id
   | F_id id -> F_id id
-  | F_ref id when Id.compare id from_id = 0 -> F_ref to_id
+  | F_ref id when Name.compare id from_id = 0 -> F_ref to_id
   | F_ref id -> F_ref id
   | F_lit v -> F_lit v
-  | F_have_exception -> F_have_exception
-  | F_current_exception -> F_current_exception
   | F_call (call, frags) -> F_call (call, List.map (frag_rename from_id to_id) frags)
   | F_op (f1, op, f2) -> F_op (frag_rename from_id to_id f1, op, frag_rename from_id to_id f2)
   | F_unary (op, f) -> F_unary (op, frag_rename from_id to_id f)
   | F_field (f, field) -> F_field (frag_rename from_id to_id f, field)
   | F_raw raw -> F_raw raw
+  | F_ctor_kind (f, ctor, unifiers, ctyp) -> F_ctor_kind (frag_rename from_id to_id f, ctor, unifiers, ctyp)
+  | F_ctor_unwrap (ctor, unifiers, f) -> F_ctor_unwrap (ctor, unifiers, frag_rename from_id to_id f)
   | F_poly f -> F_poly (frag_rename from_id to_id f)
 
 let cval_rename from_id to_id (frag, ctyp) = (frag_rename from_id to_id frag, ctyp)
 
 let rec clexp_rename from_id to_id = function
-  | CL_id (id, ctyp) when Id.compare id from_id = 0 -> CL_id (to_id, ctyp)
+  | CL_id (id, ctyp) when Name.compare id from_id = 0 -> CL_id (to_id, ctyp)
   | CL_id (id, ctyp) -> CL_id (id, ctyp)
   | CL_field (clexp, field) ->
      CL_field (clexp_rename from_id to_id clexp, field)
@@ -151,17 +180,14 @@ let rec clexp_rename from_id to_id = function
      CL_addr (clexp_rename from_id to_id clexp)
   | CL_tuple (clexp, n) ->
      CL_tuple (clexp_rename from_id to_id clexp, n)
-  | CL_current_exception ctyp -> CL_current_exception ctyp
-  | CL_have_exception -> CL_have_exception
-  | CL_return ctyp -> CL_return ctyp
   | CL_void -> CL_void
 
 let rec instr_rename from_id to_id (I_aux (instr, aux)) =
   let instr = match instr with
-    | I_decl (ctyp, id) when Id.compare id from_id = 0 -> I_decl (ctyp, to_id)
+    | I_decl (ctyp, id) when Name.compare id from_id = 0 -> I_decl (ctyp, to_id)
     | I_decl (ctyp, id) -> I_decl (ctyp, id)
 
-    | I_init (ctyp, id, cval) when Id.compare id from_id = 0 ->
+    | I_init (ctyp, id, cval) when Name.compare id from_id = 0 ->
        I_init (ctyp, to_id, cval_rename from_id to_id cval)
     | I_init (ctyp, id, cval) ->
        I_init (ctyp, id, cval_rename from_id to_id cval)
@@ -178,9 +204,8 @@ let rec instr_rename from_id to_id (I_aux (instr, aux)) =
        I_funcall (clexp_rename from_id to_id clexp, extern, id, List.map (cval_rename from_id to_id) args)
 
     | I_copy (clexp, cval) -> I_copy (clexp_rename from_id to_id clexp, cval_rename from_id to_id cval)
-    | I_alias (clexp, cval) -> I_alias (clexp_rename from_id to_id clexp, cval_rename from_id to_id cval)
 
-    | I_clear (ctyp, id) when Id.compare id from_id = 0 -> I_clear (ctyp, to_id)
+    | I_clear (ctyp, id) when Name.compare id from_id = 0 -> I_clear (ctyp, to_id)
     | I_clear (ctyp, id) -> I_clear (ctyp, id)
 
     | I_return cval -> I_return (cval_rename from_id to_id cval)
@@ -203,12 +228,13 @@ let rec instr_rename from_id to_id (I_aux (instr, aux)) =
 
     | I_match_failure -> I_match_failure
 
-    | I_end -> I_end
+    | I_end id when Name.compare id from_id = 0 -> I_end to_id
+    | I_end id -> I_end id
 
-    | I_reset (ctyp, id) when Id.compare id from_id = 0 -> I_reset (ctyp, to_id)
+    | I_reset (ctyp, id) when Name.compare id from_id = 0 -> I_reset (ctyp, to_id)
     | I_reset (ctyp, id) -> I_reset (ctyp, id)
 
-    | I_reinit (ctyp, id, cval) when Id.compare id from_id = 0 ->
+    | I_reinit (ctyp, id, cval) when Name.compare id from_id = 0 ->
        I_reinit (ctyp, to_id, cval_rename from_id to_id cval)
     | I_reinit (ctyp, id, cval) ->
        I_reinit (ctyp, id, cval_rename from_id to_id cval)
@@ -229,15 +255,24 @@ let string_of_value = function
   | V_unit -> "UNIT"
   | V_bit Sail2_values.B0 -> "UINT64_C(0)"
   | V_bit Sail2_values.B1 -> "UINT64_C(1)"
+  | V_bit Sail2_values.BU -> failwith "Undefined bit found in value"
   | V_string str -> "\"" ^ str ^ "\""
-  | V_ctor_kind str -> "Kind_" ^ Util.zencode_string str
-  | _ -> failwith "Cannot convert value to string"
+
+let string_of_name ?zencode:(zencode=true) =
+  let ssa_num n = if n < 0 then "" else ("/" ^ string_of_int n) in
+  function
+  | Name (id, n) ->
+     (if zencode then Util.zencode_string (string_of_id id) else string_of_id id) ^ ssa_num n
+  | Have_exception n ->
+     "have_exception" ^ ssa_num n
+  | Return n ->
+     "return" ^ ssa_num n
+  | Current_exception n ->
+     "(*current_exception)" ^ ssa_num n
 
 let rec string_of_fragment ?zencode:(zencode=true) = function
-  | F_id id when zencode -> Util.zencode_string (string_of_id id)
-  | F_id id -> string_of_id id
-  | F_ref id when zencode -> "&" ^ Util.zencode_string (string_of_id id)
-  | F_ref id -> "&" ^ string_of_id id
+  | F_id id -> string_of_name ~zencode:zencode id
+  | F_ref id -> "&" ^ string_of_name ~zencode:zencode id
   | F_lit v -> string_of_value v
   | F_call (str, frags) ->
      Printf.sprintf "%s(%s)" str (Util.string_of_list ", " (string_of_fragment ~zencode:zencode) frags)
@@ -247,9 +282,21 @@ let rec string_of_fragment ?zencode:(zencode=true) = function
      Printf.sprintf "%s %s %s" (string_of_fragment' ~zencode:zencode f1) op (string_of_fragment' ~zencode:zencode f2)
   | F_unary (op, f) ->
      op ^ string_of_fragment' ~zencode:zencode f
-  | F_have_exception -> "have_exception"
-  | F_current_exception -> "(*current_exception)"
   | F_raw raw -> raw
+  | F_ctor_kind (f, ctor, [], _) ->
+     string_of_fragment' ~zencode:zencode f ^ ".kind"
+     ^ " != Kind_" ^ Util.zencode_string (string_of_id ctor)
+  | F_ctor_kind (f, ctor, unifiers, _) ->
+     string_of_fragment' ~zencode:zencode f ^ ".kind"
+     ^ " != Kind_" ^ Util.zencode_string (string_of_id ctor ^ "_" ^ Util.string_of_list "_" string_of_ctyp unifiers)
+  | F_ctor_unwrap (ctor, [], f) ->
+     Printf.sprintf "%s.%s"
+       (string_of_fragment' ~zencode:zencode f)
+       (Util.zencode_string (string_of_id ctor))
+  | F_ctor_unwrap (ctor, unifiers, f) ->
+     Printf.sprintf "%s.%s"
+       (string_of_fragment' ~zencode:zencode f)
+       (Util.zencode_string (string_of_id ctor ^ "_" ^ Util.string_of_list "_" string_of_ctyp unifiers))
   | F_poly f -> string_of_fragment ~zencode:zencode f
 and string_of_fragment' ?zencode:(zencode=true) f =
   match f with
@@ -284,9 +331,14 @@ and string_of_ctyp = function
    constructors in variants and structs. Used for debug output. *)
 and full_string_of_ctyp = function
   | CT_tup ctyps -> "(" ^ Util.string_of_list ", " full_string_of_ctyp ctyps ^ ")"
-  | CT_struct (id, ctors) | CT_variant (id, ctors) ->
+  | CT_struct (id, ctors) ->
      "struct " ^ string_of_id id
-     ^ "{ "
+     ^ "{"
+     ^ Util.string_of_list ", " (fun (id, ctyp) -> string_of_id id ^ " : " ^ full_string_of_ctyp ctyp) ctors
+     ^ "}"
+  | CT_variant (id, ctors) ->
+     "union " ^ string_of_id id
+     ^ "{"
      ^ Util.string_of_list ", " (fun (id, ctyp) -> string_of_id id ^ " : " ^ full_string_of_ctyp ctyp) ctors
      ^ "}"
   | CT_vector (true, ctyp) -> "vector(dec, " ^ full_string_of_ctyp ctyp ^ ")"
@@ -407,6 +459,13 @@ let rec ctyp_unify ctyp1 ctyp2 =
 
   | CT_list ctyp1, CT_list ctyp2 -> ctyp_unify ctyp1 ctyp2
 
+  | CT_struct (id1, fields1), CT_struct (id2, fields2)
+       when Id.compare id1 id2 = 0 && List.length fields1 == List.length fields2 ->
+     if List.for_all2 (fun x y -> x = y) (List.map fst fields1) (List.map fst fields2) then
+       List.concat (List.map2 ctyp_unify (List.map snd fields1) (List.map snd fields2))
+     else
+       raise (Invalid_argument "ctyp_unify")
+                                  
   | CT_ref ctyp1, CT_ref ctyp2 -> ctyp_unify ctyp1 ctyp2
 
   | CT_poly, _ -> [ctyp2]
@@ -466,6 +525,9 @@ let rec is_polymorphic = function
 let pp_id id =
   string (string_of_id id)
 
+let pp_name id =
+  string (string_of_name ~zencode:false id)
+
 let pp_ctyp ctyp =
   string (full_string_of_ctyp ctyp |> Util.yellow |> Util.clear)
 
@@ -476,19 +538,16 @@ let pp_cval (frag, ctyp) =
   string (string_of_fragment ~zencode:false frag) ^^ string " : " ^^ pp_ctyp ctyp
 
 let rec pp_clexp = function
-  | CL_id (id, ctyp) -> pp_id id ^^ string " : " ^^ pp_ctyp ctyp
+  | CL_id (id, ctyp) -> pp_name id ^^ string " : " ^^ pp_ctyp ctyp
   | CL_field (clexp, field) -> parens (pp_clexp clexp) ^^ string "." ^^ string field
   | CL_tuple (clexp, n) -> parens (pp_clexp clexp) ^^ string "." ^^ string (string_of_int n)
   | CL_addr clexp -> string "*" ^^ pp_clexp clexp
-  | CL_current_exception ctyp -> string "current_exception : " ^^ pp_ctyp ctyp
-  | CL_have_exception -> string "have_exception"
-  | CL_return ctyp -> string "return : " ^^ pp_ctyp ctyp
   | CL_void -> string "void"
 
 let rec pp_instr ?short:(short=false) (I_aux (instr, aux)) =
   match instr with
   | I_decl (ctyp, id) ->
-     pp_keyword "var" ^^ pp_id id ^^ string " : " ^^ pp_ctyp ctyp
+     pp_keyword "var" ^^ pp_name id ^^ string " : " ^^ pp_ctyp ctyp
   | I_if (cval, then_instrs, else_instrs, ctyp) ->
      let pp_if_block = function
        | [] -> string "{}"
@@ -508,20 +567,18 @@ let rec pp_instr ?short:(short=false) (I_aux (instr, aux)) =
   | I_try_block instrs ->
      pp_keyword "try" ^^ surround 2 0 lbrace (separate_map (semi ^^ hardline) pp_instr instrs) rbrace
   | I_reset (ctyp, id) ->
-     pp_keyword "recreate" ^^ pp_id id ^^ string " : " ^^ pp_ctyp ctyp
+     pp_keyword "recreate" ^^ pp_name id ^^ string " : " ^^ pp_ctyp ctyp
   | I_init (ctyp, id, cval) ->
-     pp_keyword "create" ^^ pp_id id ^^ string " : " ^^ pp_ctyp ctyp ^^ string " = " ^^ pp_cval cval
+     pp_keyword "create" ^^ pp_name id ^^ string " : " ^^ pp_ctyp ctyp ^^ string " = " ^^ pp_cval cval
   | I_reinit (ctyp, id, cval) ->
-     pp_keyword "recreate" ^^ pp_id id ^^ string " : " ^^ pp_ctyp ctyp ^^ string " = " ^^ pp_cval cval
+     pp_keyword "recreate" ^^ pp_name id ^^ string " : " ^^ pp_ctyp ctyp ^^ string " = " ^^ pp_cval cval
   | I_funcall (x, _, f, args) ->
      separate space [ pp_clexp x; string "=";
                       string (string_of_id f |> Util.green |> Util.clear) ^^ parens (separate_map (string ", ") pp_cval args) ]
   | I_copy (clexp, cval) ->
      separate space [pp_clexp clexp; string "="; pp_cval cval]
-  | I_alias (clexp, cval) ->
-     pp_keyword "alias" ^^ separate space [pp_clexp clexp; string "="; pp_cval cval]
   | I_clear (ctyp, id) ->
-     pp_keyword "kill" ^^ pp_id id ^^ string " : " ^^ pp_ctyp ctyp
+     pp_keyword "kill" ^^ pp_name id ^^ string " : " ^^ pp_ctyp ctyp
   | I_return cval ->
      pp_keyword "return" ^^ pp_cval cval
   | I_throw cval ->
@@ -534,7 +591,7 @@ let rec pp_instr ?short:(short=false) (I_aux (instr, aux)) =
      pp_keyword "goto" ^^ string (str |> Util.blue |> Util.clear)
   | I_match_failure ->
      pp_keyword "match_failure"
-  | I_end ->
+  | I_end _ ->
      pp_keyword "end"
   | I_undefined ctyp ->
      pp_keyword "undefined" ^^ pp_ctyp ctyp
@@ -584,55 +641,72 @@ let pp_cdef = function
      ^^ hardline
 
 let rec fragment_deps = function
-  | F_id id | F_ref id -> IdSet.singleton id
-  | F_lit _ -> IdSet.empty
+  | F_id id | F_ref id -> NameSet.singleton id
+  | F_lit _ -> NameSet.empty
   | F_field (frag, _) | F_unary (_, frag) | F_poly frag -> fragment_deps frag
-  | F_call (_, frags) -> List.fold_left IdSet.union IdSet.empty (List.map fragment_deps frags)
-  | F_op (frag1, _, frag2) -> IdSet.union (fragment_deps frag1) (fragment_deps frag2)
-  | F_current_exception -> IdSet.empty
-  | F_have_exception -> IdSet.empty
-  | F_raw _ -> IdSet.empty
+  | F_call (_, frags) -> List.fold_left NameSet.union NameSet.empty (List.map fragment_deps frags)
+  | F_op (frag1, _, frag2) -> NameSet.union (fragment_deps frag1) (fragment_deps frag2)
+  | F_ctor_kind (frag, _, _, _) -> fragment_deps frag
+  | F_ctor_unwrap (_, _, frag) -> fragment_deps frag
+  | F_raw _ -> NameSet.empty
 
 let cval_deps = function (frag, _) -> fragment_deps frag
 
 let rec clexp_deps = function
-  | CL_id (id, _) -> IdSet.singleton id
+  | CL_id (id, _) -> NameSet.singleton id
   | CL_field (clexp, _) -> clexp_deps clexp
   | CL_tuple (clexp, _) -> clexp_deps clexp
   | CL_addr clexp -> clexp_deps clexp
-  | CL_have_exception -> IdSet.empty
-  | CL_current_exception _ -> IdSet.empty
-  | CL_return _ -> IdSet.empty
-  | CL_void -> IdSet.empty
+  | CL_void -> NameSet.empty
 
 (* Return the direct, read/write dependencies of a single instruction *)
 let instr_deps = function
-  | I_decl (ctyp, id) -> IdSet.empty, IdSet.singleton id
-  | I_reset (ctyp, id) -> IdSet.empty, IdSet.singleton id
-  | I_init (ctyp, id, cval) | I_reinit (ctyp, id, cval) -> cval_deps cval, IdSet.singleton id
-  | I_if (cval, _, _, _) -> cval_deps cval, IdSet.empty
-  | I_jump (cval, label) -> cval_deps cval, IdSet.empty
-  | I_funcall (clexp, _, _, cvals) -> List.fold_left IdSet.union IdSet.empty (List.map cval_deps cvals), clexp_deps clexp
+  | I_decl (ctyp, id) -> NameSet.empty, NameSet.singleton id
+  | I_reset (ctyp, id) -> NameSet.empty, NameSet.singleton id
+  | I_init (ctyp, id, cval) | I_reinit (ctyp, id, cval) -> cval_deps cval, NameSet.singleton id
+  | I_if (cval, _, _, _) -> cval_deps cval, NameSet.empty
+  | I_jump (cval, label) -> cval_deps cval, NameSet.empty
+  | I_funcall (clexp, _, _, cvals) -> List.fold_left NameSet.union NameSet.empty (List.map cval_deps cvals), clexp_deps clexp
   | I_copy (clexp, cval) -> cval_deps cval, clexp_deps clexp
-  | I_alias (clexp, cval) -> cval_deps cval, clexp_deps clexp
-  | I_clear (_, id) -> IdSet.singleton id, IdSet.empty
-  | I_throw cval | I_return cval -> cval_deps cval, IdSet.empty
-  | I_block _ | I_try_block _ -> IdSet.empty, IdSet.empty
-  | I_comment _ | I_raw _ -> IdSet.empty, IdSet.empty
-  | I_label label -> IdSet.empty, IdSet.empty
-  | I_goto label -> IdSet.empty, IdSet.empty
-  | I_undefined _ -> IdSet.empty, IdSet.empty
-  | I_match_failure -> IdSet.empty, IdSet.empty
-  | I_end -> IdSet.empty, IdSet.empty
+  | I_clear (_, id) -> NameSet.singleton id, NameSet.empty
+  | I_throw cval | I_return cval -> cval_deps cval, NameSet.empty
+  | I_block _ | I_try_block _ -> NameSet.empty, NameSet.empty
+  | I_comment _ | I_raw _ -> NameSet.empty, NameSet.empty
+  | I_label label -> NameSet.empty, NameSet.empty
+  | I_goto label -> NameSet.empty, NameSet.empty
+  | I_undefined _ -> NameSet.empty, NameSet.empty
+  | I_match_failure -> NameSet.empty, NameSet.empty
+  | I_end id -> NameSet.singleton id, NameSet.empty
+
+module NameCT = struct
+  type t = name * ctyp
+  let compare (n1, ctyp1) (n2, ctyp2) =
+    let c = Name.compare n1 n2 in
+    if c = 0 then CT.compare ctyp1 ctyp2 else c
+end
+
+module NameCTSet = Set.Make(NameCT)
+module NameCTMap = Map.Make(NameCT)
+
+let rec clexp_typed_writes = function
+  | CL_id (id, ctyp) -> NameCTSet.singleton (id, ctyp)
+  | CL_field (clexp, _) -> clexp_typed_writes clexp
+  | CL_tuple (clexp, _) -> clexp_typed_writes clexp
+  | CL_addr clexp -> clexp_typed_writes clexp
+  | CL_void -> NameCTSet.empty
+
+let instr_typed_writes (I_aux (aux, _)) =
+  match aux with
+  | I_decl (ctyp, id) | I_reset (ctyp, id) -> NameCTSet.singleton (id, ctyp)
+  | I_init (ctyp, id, _) | I_reinit (ctyp, id, _) -> NameCTSet.singleton (id, ctyp)
+  | I_funcall (clexp, _, _, _) | I_copy (clexp, _) -> clexp_typed_writes clexp
+  | _ -> NameCTSet.empty
 
 let rec map_clexp_ctyp f = function
   | CL_id (id, ctyp) -> CL_id (id, f ctyp)
   | CL_field (clexp, field) -> CL_field (map_clexp_ctyp f clexp, field)
   | CL_tuple (clexp, n) -> CL_tuple (map_clexp_ctyp f clexp, n)
   | CL_addr clexp -> CL_addr (map_clexp_ctyp f clexp)
-  | CL_current_exception ctyp -> CL_current_exception (f ctyp)
-  | CL_have_exception -> CL_have_exception
-  | CL_return ctyp -> CL_return (f ctyp)
   | CL_void -> CL_void
 
 let rec map_instr_ctyp f (I_aux (instr, aux)) =
@@ -645,7 +719,6 @@ let rec map_instr_ctyp f (I_aux (instr, aux)) =
     | I_funcall (clexp, extern, id, cvals) ->
        I_funcall (map_clexp_ctyp f clexp, extern, id, List.map (fun (frag, ctyp) -> frag, f ctyp) cvals)
     | I_copy (clexp, (frag, ctyp)) -> I_copy (map_clexp_ctyp f clexp, (frag, f ctyp))
-    | I_alias (clexp, (frag, ctyp)) -> I_alias (map_clexp_ctyp f clexp, (frag, f ctyp))
     | I_clear (ctyp, id) -> I_clear (f ctyp, id)
     | I_return (frag, ctyp) -> I_return (frag, f ctyp)
     | I_block instrs -> I_block (List.map (map_instr_ctyp f) instrs)
@@ -654,7 +727,7 @@ let rec map_instr_ctyp f (I_aux (instr, aux)) =
     | I_undefined ctyp -> I_undefined (f ctyp)
     | I_reset (ctyp, id) -> I_reset (f ctyp, id)
     | I_reinit (ctyp1, id, (frag, ctyp2)) -> I_reinit (f ctyp1, id, (frag, f ctyp2))
-    | I_end -> I_end
+    | I_end id -> I_end id
     | (I_comment _ | I_raw _ | I_label _ | I_goto _ | I_match_failure) as instr -> instr
   in
   I_aux (instr, aux)
@@ -663,8 +736,8 @@ let rec map_instr_ctyp f (I_aux (instr, aux)) =
 let rec map_instr f (I_aux (instr, aux)) =
   let instr = match instr with
     | I_decl _ | I_init _ | I_reset _ | I_reinit _
-      | I_funcall _ | I_copy _ | I_alias _ | I_clear _ | I_jump _ | I_throw _ | I_return _
-      | I_comment _ | I_label _ | I_goto _ | I_raw _ | I_match_failure | I_undefined _ | I_end -> instr
+      | I_funcall _ | I_copy _ | I_clear _ | I_jump _ | I_throw _ | I_return _
+      | I_comment _ | I_label _ | I_goto _ | I_raw _ | I_match_failure | I_undefined _ | I_end _ -> instr
     | I_if (cval, instrs1, instrs2, ctyp) ->
        I_if (cval, List.map (map_instr f) instrs1, List.map (map_instr f) instrs2, ctyp)
     | I_block instrs ->
@@ -678,8 +751,8 @@ let rec map_instr f (I_aux (instr, aux)) =
 let rec iter_instr f (I_aux (instr, aux)) =
   match instr with
   | I_decl _ | I_init _ | I_reset _ | I_reinit _
-    | I_funcall _ | I_copy _ | I_alias _ | I_clear _ | I_jump _ | I_throw _ | I_return _
-    | I_comment _ | I_label _ | I_goto _ | I_raw _ | I_match_failure | I_undefined _ | I_end -> f (I_aux (instr, aux))
+    | I_funcall _ | I_copy _ | I_clear _ | I_jump _ | I_throw _ | I_return _
+    | I_comment _ | I_label _ | I_goto _ | I_raw _ | I_match_failure | I_undefined _ | I_end _ -> f (I_aux (instr, aux))
   | I_if (cval, instrs1, instrs2, ctyp) ->
      List.iter (iter_instr f) instrs1;
      List.iter (iter_instr f) instrs2
@@ -717,10 +790,10 @@ let rec map_instrs f (I_aux (instr, aux)) =
     | I_decl _ | I_init _ | I_reset _ | I_reinit _ -> instr
     | I_if (cval, instrs1, instrs2, ctyp) ->
        I_if (cval, f (List.map (map_instrs f) instrs1), f (List.map (map_instrs f) instrs2), ctyp)
-    | I_funcall _ | I_copy _ | I_alias _ | I_clear _ | I_jump _ | I_throw _ | I_return _ -> instr
+    | I_funcall _ | I_copy _ | I_clear _ | I_jump _ | I_throw _ | I_return _ -> instr
     | I_block instrs -> I_block (f (List.map (map_instrs f) instrs))
     | I_try_block instrs -> I_try_block (f (List.map (map_instrs f) instrs))
-    | I_comment _ | I_label _ | I_goto _ | I_raw _ | I_match_failure | I_undefined _  | I_end -> instr
+    | I_comment _ | I_label _ | I_goto _ | I_raw _ | I_match_failure | I_undefined _  | I_end _ -> instr
   in
   I_aux (instr, aux)
 
@@ -732,7 +805,7 @@ let map_instrs_list f instrs =
 
 let rec instr_ids (I_aux (instr, _)) =
   let reads, writes = instr_deps instr in
-  IdSet.union reads writes
+  NameSet.union reads writes
 
 let rec instr_reads (I_aux (instr, _)) =
   fst (instr_deps instr)
@@ -764,7 +837,6 @@ let cval_ctyp = function (_, ctyp) -> ctyp
 
 let rec clexp_ctyp = function
   | CL_id (_, ctyp) -> ctyp
-  | CL_return ctyp -> ctyp
   | CL_field (clexp, field) ->
      begin match clexp_ctyp clexp with
      | CT_struct (id, ctors) ->
@@ -788,8 +860,6 @@ let rec clexp_ctyp = function
         end
      | ctyp -> failwith ("Bad ctyp for CL_addr " ^ string_of_ctyp ctyp)
      end
-  | CL_have_exception -> CT_bool
-  | CL_current_exception ctyp -> ctyp
   | CL_void -> CT_unit
 
 let rec instr_ctyps (I_aux (instr, aux)) =
@@ -805,13 +875,13 @@ let rec instr_ctyps (I_aux (instr, aux)) =
   | I_funcall (clexp, _, _, cvals) ->
      List.fold_left (fun m ctyp -> CTSet.add ctyp m) CTSet.empty (List.map cval_ctyp cvals)
      |> CTSet.add (clexp_ctyp clexp)
-  | I_copy (clexp, cval) | I_alias (clexp, cval) ->
+  | I_copy (clexp, cval)  ->
      CTSet.add (clexp_ctyp clexp) (CTSet.singleton (cval_ctyp cval))
   | I_block instrs | I_try_block instrs ->
      instrs_ctyps instrs
   | I_throw cval | I_jump (cval, _) | I_return cval ->
      CTSet.singleton (cval_ctyp cval)
-  | I_comment _ | I_label _ | I_goto _ | I_raw _ | I_match_failure | I_end ->
+  | I_comment _ | I_label _ | I_goto _ | I_raw _ | I_match_failure | I_end _ ->
      CTSet.empty
 
 and instrs_ctyps instrs = List.fold_left CTSet.union CTSet.empty (List.map instr_ctyps instrs)
@@ -848,12 +918,12 @@ let instr_split_at f =
   instr_split_at' f []
 
 let rec instrs_rename from_id to_id =
-  let rename id = if Id.compare id from_id = 0 then to_id else id in
+  let rename id = if Name.compare id from_id = 0 then to_id else id in
   let crename = cval_rename from_id to_id in
   let irename instrs = instrs_rename from_id to_id instrs in
   let lrename = clexp_rename from_id to_id in
   function
-  | (I_aux (I_decl (ctyp, new_id), _) :: _) as instrs when Id.compare from_id new_id = 0 -> instrs
+  | (I_aux (I_decl (ctyp, new_id), _) :: _) as instrs when Name.compare from_id new_id = 0 -> instrs
   | I_aux (I_decl (ctyp, new_id), aux) :: instrs -> I_aux (I_decl (ctyp, new_id), aux) :: irename instrs
   | I_aux (I_reset (ctyp, id), aux) :: instrs -> I_aux (I_reset (ctyp, rename id), aux) :: irename instrs
   | I_aux (I_init (ctyp, id, cval), aux) :: instrs -> I_aux (I_init (ctyp, rename id, crename cval), aux) :: irename instrs
@@ -861,14 +931,13 @@ let rec instrs_rename from_id to_id =
   | I_aux (I_if (cval, then_instrs, else_instrs, ctyp), aux) :: instrs ->
      I_aux (I_if (crename cval, irename then_instrs, irename else_instrs, ctyp), aux) :: irename instrs
   | I_aux (I_jump (cval, label), aux) :: instrs -> I_aux (I_jump (crename cval, label), aux) :: irename instrs
-  | I_aux (I_funcall (clexp, extern, id, cvals), aux) :: instrs ->
-     I_aux (I_funcall (lrename clexp, extern, rename id, List.map crename cvals), aux) :: irename instrs
+  | I_aux (I_funcall (clexp, extern, function_id, cvals), aux) :: instrs ->
+     I_aux (I_funcall (lrename clexp, extern, function_id, List.map crename cvals), aux) :: irename instrs
   | I_aux (I_copy (clexp, cval), aux) :: instrs -> I_aux (I_copy (lrename clexp, crename cval), aux) :: irename instrs
-  | I_aux (I_alias (clexp, cval), aux) :: instrs -> I_aux (I_alias (lrename clexp, crename cval), aux) :: irename instrs
   | I_aux (I_clear (ctyp, id), aux) :: instrs -> I_aux (I_clear (ctyp, rename id), aux) :: irename instrs
   | I_aux (I_return cval, aux) :: instrs -> I_aux (I_return (crename cval), aux) :: irename instrs
   | I_aux (I_block block, aux) :: instrs -> I_aux (I_block (irename block), aux) :: irename instrs
   | I_aux (I_try_block block, aux) :: instrs -> I_aux (I_try_block (irename block), aux) :: irename instrs
   | I_aux (I_throw cval, aux) :: instrs -> I_aux (I_throw (crename cval), aux) :: irename instrs
-  | (I_aux ((I_comment _ | I_raw _ | I_end | I_label _ | I_goto _ | I_match_failure | I_undefined _), _) as instr) :: instrs -> instr :: irename instrs
+  | (I_aux ((I_comment _ | I_raw _ | I_end _ | I_label _ | I_goto _ | I_match_failure | I_undefined _), _) as instr) :: instrs -> instr :: irename instrs
   | [] -> []