Have exceptions working in C backend

4 files changed, 199 insertions, 91 deletions

diff --git a/src/c_backend.ml b/src/c_backend.ml
index 429040ad..ad9dc2f3 100644
--- a/src/c_backend.ml
+++ b/src/c_backend.ml
@@ -59,6 +59,9 @@ let c_verbosity = ref 1
 let c_debug str =
   if !c_verbosity > 0 then prerr_endline str else ()
 
+let c_error ?loc:(l=Parse_ast.Unknown) message =
+  raise (Reporting_basic.err_general l ("C backend: " ^ 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)
@@ -318,16 +321,16 @@ let rec split_block = function
   | exp :: exps ->
      let exps, last = split_block exps in
      exp :: exps, last
-  | [] -> failwith "empty block"
+  | [] -> c_error "empty block"
 
-let rec anf_pat (P_aux (p_aux, _) as pat) =
+let rec anf_pat (P_aux (p_aux, (l, _)) as pat) =
   match p_aux with
   | P_id id -> AP_id id
   | P_wild -> AP_wild
   | P_tup pats -> AP_tup (List.map anf_pat pats)
   | P_app (id, [pat]) -> AP_app (id, anf_pat pat)
   | P_app (id, pats) -> AP_app (id, AP_tup (List.map anf_pat pats))
-  | _ -> failwith ("anf_pat: " ^ string_of_pat pat)
+  | _ -> c_error ~loc:l ("anf_pat: " ^ string_of_pat pat)
 
 let rec anf (E_aux (e_aux, exp_annot) as exp) =
   let to_aval = function
@@ -362,6 +365,9 @@ let rec anf (E_aux (e_aux, exp_annot) as exp) =
      let aexp = anf exp in
      AE_assign (id, lvar_typ (Env.lookup_id id (env_of exp)), aexp)
 
+  | E_assign (lexp, _) ->
+     failwith ("Encountered complex l-expression " ^ string_of_lexp lexp ^ " when converting to ANF")
+
   | E_loop (loop_typ, cond, exp) ->
      let acond = anf cond in
      let aexp = anf exp in
@@ -415,20 +421,20 @@ let rec anf (E_aux (e_aux, exp_annot) as exp) =
      let wrap = List.fold_left (fun f g x -> f (g x)) (fun x -> x) (List.map snd avals) in
      wrap (AE_app (id, List.map fst avals, typ_of exp))
 
-  | E_throw exp ->
-     let aexp = anf exp in
+  | E_throw exn_exp ->
+     let aexp = anf exn_exp in
      let aval, wrap = to_aval aexp in
-     wrap (AE_throw (aval, unit_typ))
+     wrap (AE_throw (aval, typ_of exp))
 
   | E_exit exp ->
      let aexp = anf exp in
      let aval, wrap = to_aval aexp in
      wrap (AE_app (mk_id "exit", [aval], unit_typ))
 
-  | E_return exp ->
-     let aexp = anf exp in
+  | E_return ret_exp ->
+     let aexp = anf ret_exp in
      let aval, wrap = to_aval aexp in
-     wrap (AE_return (aval, unit_typ))
+     wrap (AE_return (aval, typ_of exp))
 
   | E_assert (exp1, exp2) ->
      let aexp1 = anf exp1 in
@@ -455,10 +461,6 @@ let rec anf (E_aux (e_aux, exp_annot) as exp) =
      let lvar = Env.lookup_id id (env_of exp) in
      AE_val (AV_ref (id, lvar))
 
-  | E_return exp ->
-     let aval, wrap = to_aval (anf exp) in
-     wrap (AE_return (aval, typ_of exp))
-
   | E_case (match_exp, pexps) ->
      let match_aval, match_wrap = to_aval (anf match_exp) in
      let anf_pexp (Pat_aux (pat_aux, _)) =
@@ -488,6 +490,9 @@ let rec anf (E_aux (e_aux, exp_annot) as exp) =
      let lvar = Env.lookup_id id env in
      AE_let (id, lvar_typ lvar, anf binding, anf body, typ_of exp)
 
+  | E_var (lexp, _, _) ->
+     failwith ("Encountered complex l-expression " ^ string_of_lexp lexp ^ " when converting to ANF")
+
   | E_let (LB_aux (LB_val (pat, binding), _), body) ->
      anf (E_aux (E_case (binding, [Pat_aux (Pat_exp (pat, body), (Parse_ast.Unknown, None))]), exp_annot))
 
@@ -515,7 +520,14 @@ let rec anf (E_aux (e_aux, exp_annot) as exp) =
      (* We don't compile E_nondet nodes *)
      failwith "encountered E_nondet node when converting to ANF"
 
-  | _ -> failwith ("Cannot convert to ANF: " ^ string_of_exp exp)
+  | E_comment _ | E_comment_struc _ ->
+     (* comment AST nodes not-supported *)
+     failwith "encountered E_comment or E_comment_struc node when converting to ANF"
+
+  | E_internal_cast _ | E_internal_exp _ | E_sizeof_internal _ | E_internal_plet _ | E_internal_return _ | E_internal_exp_user _ ->
+     failwith "encountered unexpected internal node when converting to ANF"
+
+  | E_record _ -> failwith ("Cannot convert to ANF: " ^ string_of_exp exp)
 
 (**************************************************************************)
 (* 2. Converting sail types to C types                                    *)
@@ -527,6 +539,9 @@ let min_int64 = Big_int.of_int64 Int64.min_int
 type ctyp =
   (* Arbitrary precision GMP integer, mpz_t in C. *)
   | CT_mpz
+  (* The real type in sail. Abstract here, but implemented using
+     either GMP rationals or high-precision floating point. *)
+  | CT_real
   (* Variable length bitvector - flag represents direction, inc or dec *)
   | CT_bv of bool
   (* Fixed length bitvector that fits within a 64-bit word. - int
@@ -578,8 +593,11 @@ let rec ctyp_equal ctyp1 ctyp2 =
   | CT_variant (id1, _), CT_variant (id2, _) -> Id.compare id1 id2 = 0
   | CT_tup ctyps1, CT_tup ctyps2 -> List.for_all2 ctyp_equal ctyps1 ctyps2
   | CT_string, CT_string -> true
+  | CT_real, CT_real -> true
   | _, _ -> false
 
+(* String representation of ctyps here is only for debugging and
+   intermediate language pretty-printer. *)
 let rec string_of_ctyp = function
   | CT_mpz -> "mpz_t"
   | CT_bv true -> "bv_t<dec>"
@@ -590,13 +608,14 @@ let rec string_of_ctyp = function
   | CT_int -> "int"
   | CT_unit -> "unit"
   | CT_bool -> "bool"
+  | CT_real -> "real"
   | CT_tup ctyps -> "(" ^ Util.string_of_list ", " string_of_ctyp ctyps ^ ")"
   | CT_struct (id, _) | CT_enum (id, _) | CT_variant (id, _) -> string_of_id id
   | CT_string -> "string"
 
-(* Convert a sail type into a C-type *)
+(** Convert a sail type into a C-type **)
 let rec ctyp_of_typ ctx typ =
-  let Typ_aux (typ_aux, _) as typ = Env.expand_synonyms ctx.tc_env typ in
+  let Typ_aux (typ_aux, l) as typ = Env.expand_synonyms ctx.tc_env typ in
   match typ_aux with
   | Typ_id id when string_of_id id = "bit" -> CT_int
   | Typ_id id when string_of_id id = "bool" -> CT_bool
@@ -624,6 +643,7 @@ let rec ctyp_of_typ ctx typ =
      end
   | Typ_id id when string_of_id id = "unit" -> CT_unit
   | Typ_id id when string_of_id id = "string" -> CT_string
+  | Typ_id id when string_of_id id = "real" -> CT_real
 
   | Typ_id id | Typ_app (id, _) when Bindings.mem id ctx.records -> CT_struct (id, Bindings.find id ctx.records)
   | Typ_id id | Typ_app (id, _) when Bindings.mem id ctx.variants -> CT_variant (id, Bindings.find id ctx.variants)
@@ -633,11 +653,11 @@ let rec ctyp_of_typ ctx typ =
 
   | Typ_exist (_, _, typ) -> ctyp_of_typ ctx typ
 
-  | _ -> failwith ("No C-type for type " ^ string_of_typ typ)
+  | _ -> c_error ~loc:l ("No C-type for type " ^ string_of_typ typ)
 
 let rec is_stack_ctyp ctyp = match ctyp with
   | CT_uint64 _ | CT_int64 | CT_int | CT_unit | CT_bool | CT_enum _ -> true
-  | CT_bv _ | CT_mpz | CT_string _ -> false
+  | CT_bv _ | CT_mpz | CT_real | CT_string -> false
   | CT_struct (_, fields) -> Bindings.for_all (fun _ ctyp -> is_stack_ctyp ctyp) fields
   | CT_variant (_, ctors) -> Bindings.for_all (fun _ ctyp -> is_stack_ctyp ctyp) ctors
   | CT_tup ctyps -> List.for_all is_stack_ctyp ctyps
@@ -829,6 +849,7 @@ type clexp =
   | CL_id of id
   | CL_field of id * id
   | CL_addr of clexp
+  | CL_raw of string
 
 type instr =
   | I_decl of ctyp * id
@@ -898,6 +919,7 @@ let rec pp_clexp = function
   | CL_id id -> pp_id id
   | CL_field (id, field) -> pp_id id ^^ string "." ^^ pp_id field
   | CL_addr clexp -> string "*" ^^ pp_clexp clexp
+  | CL_raw str -> string str
 
 let rec pp_instr = function
   | I_decl (ctyp, id) ->
@@ -947,6 +969,10 @@ let is_ct_enum = function
   | CT_enum _ -> true
   | _ -> false
 
+let is_ct_variant = function
+  | CT_variant _ -> true
+  | _ -> false
+
 let is_ct_tup = function
   | CT_tup _ -> true
   | _ -> false
@@ -998,7 +1024,15 @@ let compile_funcall ctx id args typ =
   let setup = ref [] in
   let cleanup = ref [] in
 
-  let _, Typ_aux (fn_typ, _) = Env.get_val_spec id ctx.tc_env in
+  let _, Typ_aux (fn_typ, _) =
+    try Env.get_val_spec id ctx.tc_env with
+    | Type_error _ ->
+       (* If we can't find the function type, then it must be a nullary union constructor. *)
+       begin match Env.lookup_id id ctx.tc_env with
+       | Union (typq, typ) -> typq, function_typ unit_typ typ no_effect
+       | _ -> failwith ("Got function identifier " ^ string_of_id id ^ " which is neither a function nor a constructor.")
+       end
+  in
   let arg_typs, ret_typ = match fn_typ with
     | Typ_fn (Typ_aux (Typ_tup arg_typs, _), ret_typ, _) -> arg_typs, ret_typ
     | Typ_fn (arg_typ, ret_typ, _) -> [arg_typ], ret_typ
@@ -1021,7 +1055,8 @@ let compile_funcall ctx id args typ =
       cleanup := I_clear (ctyp, gs) :: !cleanup;
       CV_id (gs, ctyp)
     else
-      assert false
+      c_error ~loc:(id_loc id)
+        (Printf.sprintf "Failure when setting up function arguments: %s and %s." (string_of_ctyp have_ctyp) (string_of_ctyp ctyp))
   in
 
   let sargs = List.map2 setup_arg arg_ctyps args in
@@ -1043,6 +1078,16 @@ let compile_funcall ctx id args typ =
 
 let rec compile_match ctx apat cval case_label =
   match apat, cval with
+  | AP_id pid, _ when is_ct_variant (cval_ctyp cval) ->
+     let frag = match cval with
+       | CV_id (id, _) -> F_id id
+       | CV_C_fragment (frag, _) -> frag
+     in
+     [I_if (CV_C_fragment (F_op (F_field (frag, "kind"), "!=", F_lit ("Kind_" ^ Util.zencode_string (string_of_id pid))), CT_bool),
+            [I_goto case_label],
+            [],
+            CT_unit)],
+     []
   | AP_id pid, CV_C_fragment (code, ctyp) when is_ct_enum ctyp ->
      [I_if (CV_C_fragment (F_op (F_id pid, "!=", code), CT_bool), [I_goto case_label], [], CT_unit)], []
   | AP_id pid, CV_id (id, ctyp) when is_ct_enum ctyp ->
@@ -1064,6 +1109,19 @@ let rec compile_match ctx apat cval case_label =
           instrs, cleanup
        | _ -> assert false
      end
+  | AP_tup apats, CV_C_fragment (frag, ctyp) ->
+     begin
+       let get_tup n ctyp = CV_C_fragment (F_field (frag, "ztup" ^ string_of_int n), ctyp) in
+       let fold (instrs, cleanup, n) apat ctyp =
+         let instrs', cleanup' = compile_match ctx apat (get_tup n ctyp) case_label in
+         instrs @ instrs', cleanup' @ cleanup, n + 1
+       in
+       match ctyp with
+       | CT_tup ctyps ->
+          let instrs, cleanup, _ = List.fold_left2 fold ([], [], 0) apats ctyps in
+          instrs, cleanup
+       | _ -> assert false
+     end
   | AP_app (ctor, apat), CV_id (id, ctyp) ->
      begin match ctyp with
      | CT_variant (_, ctors) ->
@@ -1078,7 +1136,21 @@ let rec compile_match ctx apat cval case_label =
         cleanup
      | _ -> failwith "AP_app constructor with non-variant type"
      end
-  | _, _ -> [], []
+  | AP_app (ctor, apat), CV_C_fragment (frag, ctyp) ->
+     begin match ctyp with
+     | CT_variant (_, ctors) ->
+        let ctor_c_id = Util.zencode_string (string_of_id ctor) in
+        let ctor_ctyp = Bindings.find ctor ctors in
+        let instrs, cleanup = compile_match ctx apat (CV_C_fragment (F_field (frag, ctor_c_id), ctor_ctyp)) case_label in
+        [ I_if (CV_C_fragment (F_op (F_field (frag, "kind"), "!=", F_lit ("Kind_" ^ ctor_c_id)), CT_bool),
+                [I_goto case_label],
+                [],
+                CT_unit) ]
+        @ instrs,
+        cleanup
+     | _ -> failwith "AP_app constructor with non-variant type"
+     end
+  | AP_wild, _ -> [], []
 
 let unit_fragment = CV_C_fragment (F_lit "UNIT", CT_unit)
 
@@ -1154,7 +1226,7 @@ let rec compile_aexp ctx = function
   (* Compile try statement *)
   | AE_try (aexp, cases, typ) ->
      let aexp_setup, ctyp, aexp_call, aexp_cleanup = compile_aexp ctx aexp in
-     let case_return_id = gensym () in
+     let try_return_id = gensym () in
      let handled_exception_label = label "handled_exception_" in
      let compile_case (apat, guard, body) =
        let trivial_guard = match guard with
@@ -1163,7 +1235,7 @@ let rec compile_aexp ctx = function
          | _ -> false
        in
        let try_label = label "try_" in
-       let exn_cval = CV_C_fragment (F_lit "*current_exception", ctyp_of_typ ctx (mk_typ (Typ_id (mk_id "exception")))) in
+       let exn_cval = CV_C_fragment (F_lit "(*current_exception)", ctyp_of_typ ctx (mk_typ (Typ_id (mk_id "exception")))) in
        let destructure, destructure_cleanup = 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
@@ -1175,18 +1247,20 @@ let rec compile_aexp ctx = function
               @ [I_if (CV_C_fragment (F_unary ("!", F_id gs), CT_bool), [I_goto try_label], [], CT_unit)]
               @ [I_comment "end guard"]
             else [])
-         @ body_setup @ [body_call (CL_id case_return_id)] @ body_cleanup
+         @ body_setup @ [body_call (CL_id try_return_id)] @ body_cleanup @ destructure_cleanup
          @ [I_goto handled_exception_label]
        in
        [I_block case_instrs; I_label try_label]
      in
-     [],
+     [I_comment "begin try catch";
+      I_decl (ctyp, try_return_id)],
      ctyp,
      (fun clexp -> I_try_block (aexp_setup @ [aexp_call clexp] @ aexp_cleanup)),
      [I_if (CV_C_fragment (F_lit "!have_exception", CT_bool), [I_goto handled_exception_label], [], CT_unit)]
      @ List.concat (List.map compile_case cases)
      @ [I_raw "sail_match_failure();"]
      @ [I_label handled_exception_label]
+     @ [I_raw "have_exception = false;"]
 
   | AE_if (aval, then_aexp, else_aexp, if_typ) ->
      let if_ctyp = ctyp_of_typ ctx if_typ in
@@ -1278,7 +1352,7 @@ let rec compile_aexp ctx = function
      (* Cleanup info will be handled by fix_exceptions *)
      let throw_setup, cval, _ = compile_aval ctx aval in
      throw_setup @ [I_throw cval],
-     CT_unit,
+     ctyp_of_typ ctx typ,
      (fun clexp -> I_copy (clexp, unit_fragment)),
      []
 
@@ -1292,13 +1366,14 @@ and compile_block ctx = function
      let gs = gensym () in
      setup @ [I_decl (CT_unit, gs); call (CL_id gs)] @ cleanup @ rest
 
-let rec pat_ids (P_aux (p_aux, _) as pat) =
+let rec pat_ids (P_aux (p_aux, (l, _)) as pat) =
   match p_aux with
   | P_id id -> [id]
   | P_tup pats -> List.concat (List.map pat_ids pats)
   | P_lit (L_aux (L_unit, _)) -> let gs = gensym () in [gs]
   | P_wild -> let gs = gensym () in [gs]
-  | _ -> failwith ("Bad pattern " ^ string_of_pat pat)
+  | P_var (pat, _) -> pat_ids pat
+  | _ -> c_error ~loc:l ("Cannot compile pattern " ^ string_of_pat pat ^ " to C")
 
 (** Compile a sail type definition into a LLcode one. Most of the
    actual work of translating the typedefs into C is done by the code
@@ -1345,7 +1420,7 @@ let generate_cleanup instrs =
   let generate_cleanup' = function
     | I_decl (ctyp, id) when not (is_stack_ctyp ctyp) -> [(id, I_clear (ctyp, id))]
     | I_alloc (ctyp, id) when not (is_stack_ctyp ctyp) -> [(id, I_clear (ctyp, id))]
-    | _ -> []
+    | instr -> []
   in
   let is_clear ids = function
     | I_clear (_, id) -> IdSet.add id ids
@@ -1366,7 +1441,9 @@ let generate_cleanup instrs =
    statements into code that sets that pointer, as well as adds extra
    control flow to cleanup heap-allocated variables correctly when a
    function terminates early. See the generate_cleanup function for
-   how this is done. *)
+   how this is done. FIXME: could be some memory leaks introduced
+   here, do we do the right thing with generate_cleanup and multiple
+   returns in the same block? *)
 let fix_early_return ret ctx instrs =
   let end_function_label = label "end_function_" in
   let is_return_recur = function
@@ -1404,6 +1481,63 @@ let fix_early_return ret ctx instrs =
   rewrite_return [] instrs
   @ [I_label end_function_label]
 
+let fix_exception_block ctx instrs =
+  let end_block_label = label "end_block_exception_" in
+  let is_exception_stop = function
+    | I_throw _ | I_if _ | I_block _ | I_funcall _ -> true
+    | _ -> false
+  in
+  let rec rewrite_exception pre_cleanup instrs =
+    match instr_split_at is_exception_stop instrs with
+    | instrs, [] -> instrs
+    | before, I_block instrs :: after ->
+       before
+       @ [I_block (rewrite_exception (pre_cleanup @ generate_cleanup before) instrs)]
+       @ rewrite_exception (pre_cleanup @ generate_cleanup before) after
+    | before, I_if (cval, then_instrs, else_instrs, ctyp) :: after ->
+       let cleanup = pre_cleanup @ generate_cleanup before in
+       before
+       @ [I_if (cval, rewrite_exception cleanup then_instrs, rewrite_exception cleanup else_instrs, ctyp)]
+       @ rewrite_exception (pre_cleanup @ generate_cleanup before) after
+    | before, I_throw cval :: after ->
+       before
+       @ [I_copy (CL_raw "current_exception", cval);
+          I_raw "have_exception = true;"]
+       @ generate_cleanup before @ pre_cleanup
+       @ [I_goto end_block_label]
+       @ rewrite_exception (pre_cleanup @ generate_cleanup before) after
+    | before, (I_funcall (x, f, args, ctyp) as funcall) :: after ->
+       let effects = match Env.get_val_spec f ctx.tc_env with
+         | _, Typ_aux (Typ_fn (_, _, effects), _) -> effects
+         | exception (Type_error _) -> no_effect (* nullary union constructor, so no val spec *)
+         | _ -> assert false (* valspec must have function type *)
+       in
+       if has_effect effects BE_escape then
+         before
+         @ [funcall;
+            I_if (CV_C_fragment (F_lit "have_exception", CT_bool), generate_cleanup before @ [I_goto end_block_label], [], CT_unit)]
+         @ rewrite_exception (pre_cleanup @ generate_cleanup before) after
+       else
+         before @ funcall :: rewrite_exception (pre_cleanup @ generate_cleanup before) after
+    | _, _ -> assert false (* unreachable *)
+  in
+  rewrite_exception [] instrs
+  @ [I_label end_block_label]
+
+let rec map_try_block f instr =
+  match instr with
+  | I_decl _ | I_alloc _ | I_init _ -> 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_convert _ | I_assign _ | 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 _ -> instr
+
+let fix_exception ctx instrs =
+  let instrs = List.map (map_try_block (fix_exception_block ctx)) instrs in
+  fix_exception_block ctx instrs
+
 (** Compile a Sail toplevel definition into an LLcode definition **)
 let compile_def ctx = function
   | DEF_reg_dec (DEC_aux (DEC_reg (typ, id), _)) ->
@@ -1422,10 +1556,12 @@ let compile_def ctx = function
           let gs = gensym () in
           if is_stack_ctyp ctyp then
             let instrs = [I_decl (ctyp, gs)] @ setup @ [call (CL_id gs)] @ cleanup @ [I_return (CV_id (gs, ctyp))] in
+            let instrs = fix_exception ctx instrs in
             [CDEF_fundef (id, None, pat_ids pat, instrs)], ctx
           else
             let instrs = setup @ [call (CL_addr (CL_id gs))] @ cleanup in
             let instrs = fix_early_return (CL_addr (CL_id gs)) ctx instrs in
+            let instrs = fix_exception ctx instrs in
             [CDEF_fundef (id, Some gs, pat_ids pat, instrs)], ctx
        | _ -> assert false
      end
@@ -1448,7 +1584,8 @@ let compile_def ctx = function
   (* Only the parser and sail pretty printer care about this. *)
   | DEF_fixity _ -> [], ctx
 
-  | _ -> assert false
+  | def ->
+     c_error ("Could not compile:\n" ^ Pretty_print_sail.to_string (Pretty_print_sail.doc_def def))
 
 (** To keep things neat we use GCC's local labels extension to limit
    the scope of labels. We do this by iterating over all the blocks
@@ -1521,11 +1658,14 @@ let sgen_clexp = function
   | CL_id id -> "&" ^ sgen_id id
   | CL_field (id, field) -> "&(" ^ sgen_id id ^ "." ^ sgen_id field ^ ")"
   | CL_addr (CL_id id) -> sgen_id id
+  | CL_raw str -> str
   | _ -> assert false
 
 let sgen_clexp_pure = function
   | CL_id id -> sgen_id id
   | CL_field (id, field) -> sgen_id id ^ "." ^ sgen_id field
+  | CL_raw str -> str
+  | CL_addr (CL_id id) -> sgen_id id
   | _ -> assert false
 
 let rec codegen_instr ctx = function
@@ -1537,6 +1677,7 @@ let rec codegen_instr ctx = function
        string (Printf.sprintf "  %s = %s;" (sgen_clexp_pure clexp) (sgen_cval cval))
      else
        string (Printf.sprintf "  set_%s(%s, %s);" (sgen_ctyp_name ctyp) (sgen_clexp clexp) (sgen_cval cval))
+  | I_assign _ -> failwith "I_assign is currently unused"
   | I_if (cval, [then_instr], [], ctyp) ->
      string (Printf.sprintf "  if (%s)" (sgen_cval cval)) ^^ hardline
      ^^ twice space ^^ codegen_instr ctx then_instr
@@ -1591,7 +1732,7 @@ let rec codegen_instr ctx = function
   | I_return cval ->
      string (Printf.sprintf "  return %s;" (sgen_cval cval))
   | I_throw cval ->
-     string "  THROW"
+     string (Printf.sprintf "  THROW(%s)" (sgen_cval cval))
   | I_comment str ->
      string ("  /* " ^ str ^ " */")
   | I_label str ->
@@ -1690,9 +1831,25 @@ let codegen_type_def ctx = function
                    rbrace
      in
      let codegen_ctor (ctor_id, ctyp) =
-       string (Printf.sprintf "void %s(struct %s *rop, %s op)" (sgen_id ctor_id) (sgen_id id) (sgen_ctyp ctyp)) ^^ hardline
+       let ctor_args, tuple =
+         let tuple_set i ctyp =
+           if is_stack_ctyp ctyp then
+             string (Printf.sprintf "op.ztup%d = op%d;" i i)
+           else
+             string (Printf.sprintf "set_%s(&op.ztup%d, op%d);" (sgen_ctyp_name ctyp) i i)
+         in
+         match ctyp with
+         | CT_tup ctyps ->
+            String.concat ", " (List.mapi (fun i ctyp -> Printf.sprintf "%s op%d" (sgen_ctyp ctyp) i) ctyps),
+            string (Printf.sprintf "%s op;" (sgen_ctyp ctyp)) ^^ hardline
+            ^^ string (Printf.sprintf "init_%s(&op);" (sgen_ctyp_name ctyp)) ^^ hardline
+            ^^ separate hardline (List.mapi tuple_set ctyps) ^^ hardline
+         | ctyp -> Printf.sprintf "%s op" (sgen_ctyp ctyp), empty
+       in
+       string (Printf.sprintf "void %s(struct %s *rop, %s)" (sgen_id ctor_id) (sgen_id id) ctor_args) ^^ hardline
        ^^ surround 2 0 lbrace
-                   (each_ctor "rop->" (clear_field "rop") (Bindings.bindings tus) ^^ hardline
+                   (tuple
+                    ^^ each_ctor "rop->" (clear_field "rop") (Bindings.bindings tus) ^^ hardline
                     ^^ string ("rop->kind = Kind_" ^ sgen_id ctor_id) ^^ semi ^^ hardline
                     ^^ if is_stack_ctyp ctyp then
                          string (Printf.sprintf "rop->%s = op;" (sgen_id ctor_id))
@@ -1748,7 +1905,7 @@ let codegen_type_def ctx = function
      (* If this is the exception type, then we setup up some global variables to deal with exceptions. *)
      ^^ if string_of_id id = "exception" then
           twice hardline
-          ^^ separate space [string "struct"; codegen_id id; string "*current_exception = NULL;"]
+          ^^ string "struct zexception *current_exception = NULL;"
           ^^ hardline
           ^^ string "bool have_exception = false;"
         else
@@ -1841,7 +1998,12 @@ let compile_ast ctx (Defs defs) =
     let postamble = separate hardline
                              [ string "int main(void)";
                                string "{";
+                               string "  current_exception = malloc(sizeof(struct zexception));";
+                               string "  init_zexception(current_exception);";
                                string "  zmain(UNIT);";
+                               string "  clear_zexception(current_exception);";
+                               string "  free(current_exception);";
+                               string "  if (have_exception) fprintf(stderr, \"Exiting due to uncaught exception\\n\");";
                                string "}" ]
     in
 
@@ -1851,29 +2013,3 @@ let compile_ast ctx (Defs defs) =
     |> print_endline
   with
     Type_error (l, err) -> prerr_endline ("Unexpected type error when compiling to C:\n" ^ string_of_type_error err)
-
-let print_compiled (setup, ctyp, call, cleanup) =
-  List.iter (fun instr -> print_endline (Pretty_print_sail.to_string (pp_instr instr))) setup;
-  print_endline (Pretty_print_sail.to_string (pp_instr (call (CL_id (mk_id ("?" ^ string_of_ctyp ctyp))))));
-  List.iter (fun instr -> print_endline (Pretty_print_sail.to_string (pp_instr instr))) cleanup
-
-let compile_exp ctx exp =
-  let aexp = anf exp in
-  let aexp = c_literals ctx aexp in
-  let aexp = map_functions (analyze_primop ctx) aexp in
-  print_endline "\n###################### COMPILED ######################\n";
-  print_compiled (compile_aexp ctx aexp);
-  print_endline "\n###################### ANF ######################\n";
-  aexp
-
-
-(*
-
-{
-  uint64_t zx = 0x000000000000F000L;
-  uint64_t v0 = (zx + 0x000000000000000FL) & 0x000000000000FFFFL;
-  uint64_t res = (v0 + 0x000000000000FFFFL) & 0x000000000000FFFFL;
-  return res;
-}
-
-*)
diff --git a/src/isail.ml b/src/isail.ml
index ffeb1442..ce17561d 100644
--- a/src/isail.ml
+++ b/src/isail.ml
@@ -294,10 +294,6 @@ let handle_input' input =
                interactive_state := initial_state !interactive_ast;
                interactive_env := env;
                vs_ids := Initial_check.val_spec_ids !interactive_ast
-            | ":compile" ->
-               let exp = Type_check.infer_exp !interactive_env (Initial_check.exp_of_string Ast_util.dec_ord arg) in
-               let anf = C_backend.compile_exp (C_backend.initial_ctx !interactive_env) exp in
-               print_endline (Pretty_print_sail.to_string (C_backend.pp_aexp anf))
             | ":u" | ":unload" ->
                interactive_ast := Ast.Defs [];
                interactive_env := Type_check.initial_env;
diff --git a/src/reporting_basic.ml b/src/reporting_basic.ml
index af1f85d0..fce7137d 100644
--- a/src/reporting_basic.ml
+++ b/src/reporting_basic.ml
@@ -259,8 +259,7 @@ let print_err_internal fatal verb_loc p_l m1 m2 =
 let print_err fatal verb_loc l m1 m2 =
   print_err_internal fatal verb_loc (Loc l) m1 m2
 
-
-type error = 
+type error =
   | Err_general of Parse_ast.l * string
   | Err_unreachable of Parse_ast.l * string
   | Err_todo of Parse_ast.l * string
diff --git a/src/specialize.ml b/src/specialize.ml
index 10c4945e..9344e661 100644
--- a/src/specialize.ml
+++ b/src/specialize.ml
@@ -52,25 +52,6 @@ open Ast
 open Ast_util
 open Rewriter
 
-let zchar c =
-  let zc c = "z" ^ String.make 1 c in
-  if Char.code c <= 41 then zc (Char.chr (Char.code c + 16))
-  else if Char.code c <= 47 then zc (Char.chr (Char.code c + 23))
-  else if Char.code c <= 57 then String.make 1 c
-  else if Char.code c <= 64 then zc (Char.chr (Char.code c + 13))
-  else if Char.code c <= 90 then String.make 1 c
-  else if Char.code c <= 94 then zc (Char.chr (Char.code c - 13))
-  else if Char.code c <= 95 then "_"
-  else if Char.code c <= 96 then zc (Char.chr (Char.code c - 13))
-  else if Char.code c <= 121 then String.make 1 c
-  else if Char.code c <= 122 then "zz"
-  else if Char.code c <= 126 then zc (Char.chr (Char.code c - 39))
-  else raise (Invalid_argument "zchar")
-
-let zencode_string str = "z" ^ List.fold_left (fun s1 s2 -> s1 ^ s2) "" (List.map zchar (Util.string_to_list str))
-
-let zencode_upper_string str = "Z" ^ List.fold_left (fun s1 s2 -> s1 ^ s2) "" (List.map zchar (Util.string_to_list str))
-
 let is_typ_ord_uvar = function
   | Type_check.U_typ _ -> true
   | Type_check.U_order _ -> true
@@ -96,7 +77,7 @@ let rec polymorphic_functions is_kopt (Defs defs) =
 
 let id_of_instantiation id instantiation =
   let string_of_binding (kid, uvar) = string_of_kid kid ^ " => " ^ Type_check.string_of_uvar uvar in
-  let str = zencode_string (Util.string_of_list ", " string_of_binding (KBindings.bindings instantiation)) ^ "#" in
+  let str = Util.zencode_string (Util.string_of_list ", " string_of_binding (KBindings.bindings instantiation)) ^ "#" in
   prepend_id str id
 
 (* Returns a list of all the instantiations of a function id in an
@@ -118,7 +99,6 @@ let rec instantiations_of id ast =
   !instantiations
 
 let rec rewrite_polymorphic_calls id ast =
-  print_endline ("Rewriting: " ^ string_of_id id);
   let vs_ids = Initial_check.val_spec_ids ast in
 
   let rewrite_e_aux = function
@@ -184,7 +164,6 @@ let specialize_id_valspec instantiations id ast =
        if IdSet.mem spec_id !spec_ids then [] else
          begin
            spec_ids := IdSet.add spec_id !spec_ids;
-           print_endline (string_of_id spec_id ^ " : " ^ string_of_typschm typschm);
            [DEF_spec (VS_aux (VS_val_spec (typschm, spec_id, externs, is_cast), annot))]
          end
      in
@@ -238,8 +217,6 @@ let remove_unused_valspecs ast =
 
   let unused = IdSet.filter (fun vs_id -> not (IdSet.mem vs_id !calls)) vs_ids in
 
-  List.iter (fun id -> print_endline (string_of_id id)) (IdSet.elements unused);
-
   let rec remove_unused (Defs defs) id =
     match defs with
     | def :: defs when is_fundef id def -> remove_unused (Defs defs) id