diff options
Diffstat (limited to 'src/c_backend.ml')
| -rw-r--r-- | src/c_backend.ml | 802 |
1 files changed, 436 insertions, 366 deletions
diff --git a/src/c_backend.ml b/src/c_backend.ml index cb732e2d..433e3d85 100644 --- a/src/c_backend.ml +++ b/src/c_backend.ml @@ -67,7 +67,6 @@ let opt_static = ref false (* Optimization flags *) let optimize_primops = ref false -let optimize_z3 = ref false let optimize_hoist_allocations = ref false let optimize_struct_updates = ref false @@ -94,9 +93,11 @@ type ctx = variants : (ctyp Bindings.t) Bindings.t; tc_env : Env.t; local_env : Env.t; + locals : (mut * ctyp) Bindings.t; letbinds : int list; recursive_functions : IdSet.t; no_raw : bool; + optimize_z3 : bool; } let initial_ctx env = @@ -105,9 +106,11 @@ let initial_ctx env = variants = Bindings.empty; tc_env = env; local_env = env; + locals = Bindings.empty; letbinds = []; recursive_functions = IdSet.empty; no_raw = false; + optimize_z3 = true; } let rec ctyp_equal ctyp1 ctyp2 = @@ -148,12 +151,11 @@ let rec ctyp_of_typ ctx typ = | Nexp_aux (Nexp_constant n, _), Nexp_aux (Nexp_constant m, _) when Big_int.less_equal min_int64 n && Big_int.less_equal m max_int64 -> CT_int64 - | n, m when !optimize_z3 -> - prerr_endline ("optimize atom " ^ string_of_nexp n ^ ", " ^ string_of_nexp m ^ " in context " ^ (Util.string_of_list ", " string_of_n_constraint (Env.get_constraints ctx.local_env))); + | n, m when ctx.optimize_z3 -> if prove ctx.local_env (nc_lteq (nconstant min_int64) n) && prove ctx.local_env (nc_lteq m (nconstant max_int64)) then - (prerr_endline "yes"; CT_int64) + CT_int64 else - (prerr_endline "no"; CT_int) + CT_int | _ -> CT_int end @@ -168,7 +170,13 @@ let rec ctyp_of_typ ctx typ = let direction = match ord with Ord_aux (Ord_dec, _) -> true | Ord_aux (Ord_inc, _) -> false | _ -> assert false in match nexp_simp n with | Nexp_aux (Nexp_constant n, _) when Big_int.less_equal n (Big_int.of_int 64) -> CT_bits64 (Big_int.to_int n, direction) + | _ when not ctx.optimize_z3 -> CT_bits direction | _ -> CT_bits direction + (* This is extremely slow :( + match solve ctx.local_env n with + | Some n when Big_int.less_equal n (Big_int.of_int 64) -> CT_bits64 (Big_int.to_int n, direction) + | _ -> CT_bits direction + *) end | Typ_app (id, [Typ_arg_aux (Typ_arg_nexp n, _); Typ_arg_aux (Typ_arg_order ord, _); @@ -190,13 +198,11 @@ let rec ctyp_of_typ ctx typ = | Typ_tup typs -> CT_tup (List.map (ctyp_of_typ ctx) typs) - | Typ_exist _ when !optimize_z3 -> + | Typ_exist _ when ctx.optimize_z3 -> (* Use Type_check.destruct_exist when optimising with z3, to ensure that we don't cause any type variable clashes in local_env. *) begin match destruct_exist ctx.local_env typ with | Some (kids, nc, typ) -> - c_debug (lazy ("optimize existential: " ^ string_of_n_constraint nc ^ ". " ^ string_of_typ typ - ^ " in context " ^ (Util.string_of_list ", " string_of_n_constraint (Env.get_constraints ctx.local_env)))); let env = add_existential l kids nc ctx.local_env in ctyp_of_typ { ctx with local_env = env } typ | None -> c_error "Existential cannot be destructured. This should be impossible!" @@ -298,12 +304,24 @@ let rec c_aval ctx = function | None -> v end | AV_C_fragment (str, typ) -> AV_C_fragment (str, typ) - (* An id can be converted to a C fragment if it's type can be stack-allocated. *) + (* An id can be converted to a C fragment if it's type can be + stack-allocated. *) | AV_id (id, lvar) as v -> begin match lvar with | Local (_, typ) when is_stack_typ ctx typ -> - AV_C_fragment (F_id id, typ) + begin + try + (* We need to check that id's type hasn't changed due to flow typing *) + let _, ctyp = Bindings.find id ctx.locals in + if is_stack_ctyp ctyp then + AV_C_fragment (F_id id, typ) + else + (prerr_endline (string_of_id id ^ " : " ^ string_of_ctyp ctyp ^ " -> " ^ string_of_ctyp (ctyp_of_typ ctx typ)); + v) (* id's type went from heap -> stack due to flow typing, so it's really still heap allocated! *) + with + Not_found -> failwith ("could not find " ^ string_of_id id ^ " in local variables") + end | Register (_, _, typ) when is_stack_typ ctx typ -> AV_C_fragment (F_id id, typ) | _ -> v @@ -324,16 +342,65 @@ let c_fragment = function let v_mask_lower i = F_lit (V_bits (Util.list_init i (fun _ -> Sail2_values.B1))) -let analyze_primop' ctx env l id args typ = +(* Map over all the functions in an aexp. *) +let rec analyze_functions ctx f (AE_aux (aexp, env, l)) = let ctx = { ctx with local_env = env } in + let aexp = match aexp with + | AE_app (id, vs, typ) -> f ctx id vs typ + + | AE_cast (aexp, typ) -> AE_cast (analyze_functions ctx f aexp, typ) + + | AE_assign (id, typ, aexp) -> AE_assign (id, typ, analyze_functions ctx f aexp) + + | AE_short_circuit (op, aval, aexp) -> AE_short_circuit (op, aval, analyze_functions ctx f aexp) + + | AE_let (mut, id, typ1, aexp1, aexp2, typ2) -> + let aexp1 = analyze_functions ctx f aexp1 in + let ctyp1 = ctyp_of_typ ctx typ1 in + let ctx = { ctx with locals = Bindings.add id (mut, ctyp1) ctx.locals } in + AE_let (mut, id, typ1, aexp1, analyze_functions ctx f aexp2, typ2) + + | AE_block (aexps, aexp, typ) -> AE_block (List.map (analyze_functions ctx f) aexps, analyze_functions ctx f aexp, typ) + + | AE_if (aval, aexp1, aexp2, typ) -> + AE_if (aval, analyze_functions ctx f aexp1, analyze_functions ctx f aexp2, typ) + + | AE_loop (loop_typ, aexp1, aexp2) -> AE_loop (loop_typ, analyze_functions ctx f aexp1, analyze_functions ctx f aexp2) + + | AE_for (id, aexp1, aexp2, aexp3, order, aexp4) -> + let aexp1 = analyze_functions ctx f aexp1 in + let aexp2 = analyze_functions ctx f aexp2 in + let aexp3 = analyze_functions ctx f aexp3 in + let aexp4 = analyze_functions ctx f aexp4 in + AE_for (id, aexp1, aexp2, aexp3, order, aexp4) + + | AE_case (aval, cases, typ) -> + let analyze_case (pat, aexp1, aexp2) = + let pat_bindings = Bindings.bindings (apat_types pat) in + let ctx = + List.fold_left (fun ctx (id, typ) -> { ctx with locals = Bindings.add id (Immutable, ctyp_of_typ ctx typ) ctx.locals }) ctx pat_bindings + in + pat, analyze_functions ctx f aexp1, analyze_functions ctx f aexp2 + in + AE_case (aval, List.map analyze_case cases, typ) + + | AE_try (aexp, cases, typ) -> + AE_try (analyze_functions ctx f aexp, List.map (fun (pat, aexp1, aexp2) -> pat, analyze_functions ctx f aexp1, analyze_functions ctx f aexp2) cases, typ) + + | AE_field _ | AE_record_update _ | AE_val _ | AE_return _ | AE_throw _ as v -> v + in + AE_aux (aexp, env, l) + +let analyze_primop' ctx id args typ = let no_change = AE_app (id, args, typ) in let args = List.map (c_aval ctx) args in let extern = if Env.is_extern id ctx.tc_env "c" then Env.get_extern id ctx.tc_env "c" else failwith "Not extern" in - (* prerr_endline ("Analysing: " ^ string_of_typ typ ^ " " ^ extern ^ Pretty_print_sail.to_string (separate_map (string ", ") pp_aval args)); *) let v_one = F_lit (V_int (Big_int.of_int 1)) in let v_int n = F_lit (V_int (Big_int.of_int n)) in + c_debug (lazy ("Analyzing primop " ^ extern ^ "(" ^ Util.string_of_list ", " (fun aval -> Pretty_print_sail.to_string (pp_aval aval)) args ^ ")")); + match extern, args with | "eq_bits", [AV_C_fragment (v1, typ1); AV_C_fragment (v2, typ2)] -> AE_val (AV_C_fragment (F_op (v1, "==", v2), typ)) @@ -352,6 +419,9 @@ let analyze_primop' ctx env l id args typ = | _ -> no_change end + | "gteq", [AV_C_fragment (v1, _); AV_C_fragment (v2, _)] -> + AE_val (AV_C_fragment (F_op (v1, ">=", v2), typ)) + | "xor_bits", [AV_C_fragment (v1, typ1); AV_C_fragment (v2, typ2)] -> AE_val (AV_C_fragment (F_op (v1, "^", v2), typ)) @@ -369,7 +439,7 @@ let analyze_primop' ctx env l id args typ = | _ -> no_change end - | "vector_subrange", [AV_C_fragment (vec, _); AV_C_fragment (f, _); AV_C_fragment (t, _)] -> + | "vector_subrange", [AV_C_fragment (vec, _); AV_C_fragment (f, _); AV_C_fragment (t, _)] when is_stack_typ ctx typ -> let len = F_op (f, "-", F_op (t, "-", v_one)) in AE_val (AV_C_fragment (F_op (F_call ("safe_rshift", [F_raw "UINT64_MAX"; F_op (v_int 64, "-", len)]), "&", F_op (vec, ">>", t)), typ)) @@ -413,13 +483,17 @@ let analyze_primop' ctx env l id args typ = | "undefined_bool", _ -> AE_val (AV_C_fragment (F_lit (V_bool false), typ)) - | _, _ -> no_change + | _, _ -> + c_debug (lazy ("No optimization routine found")); + no_change -let analyze_primop ctx env l id args typ = +let analyze_primop ctx id args typ = let no_change = AE_app (id, args, typ) in if !optimize_primops then - try analyze_primop' ctx env l id args typ with - | Failure _ -> no_change + try analyze_primop' ctx id args typ with + | Failure str -> + (c_debug (lazy ("Analyze primop failed for id " ^ string_of_id id ^ " reason: " ^ str))); + no_change else no_change @@ -456,15 +530,23 @@ let ctype_def_ctyps = function let cval_ctyp = function (_, ctyp) -> ctyp +let clexp_ctyp = function + | CL_id (_, ctyp) -> ctyp + | CL_field (_, _, ctyp) -> ctyp + | CL_addr (_, ctyp) -> ctyp + | CL_addr_field (_, _, ctyp) -> ctyp + | CL_have_exception -> CT_bool + | CL_current_exception ctyp -> ctyp + let rec map_instrs f (I_aux (instr, aux)) = let instr = match instr with | 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_convert _ | I_copy _ | 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 -> instr + | I_comment _ | I_label _ | I_goto _ | I_raw _ | I_match_failure | I_undefined _ -> instr in I_aux (instr, aux) @@ -472,14 +554,13 @@ let cval_rename from_id to_id (frag, ctyp) = (frag_rename from_id to_id frag, ct let rec instr_ctyps (I_aux (instr, aux)) = match instr with - | I_decl (ctyp, _) | I_reset (ctyp, _) | I_clear (ctyp, _) -> [ctyp] + | I_decl (ctyp, _) | I_reset (ctyp, _) | I_clear (ctyp, _) | I_undefined ctyp -> [ctyp] | I_init (ctyp, _, cval) | I_reinit (ctyp, _, cval) -> [ctyp; cval_ctyp cval] | I_if (cval, instrs1, instrs2, ctyp) -> ctyp :: cval_ctyp cval :: List.concat (List.map instr_ctyps instrs1 @ List.map instr_ctyps instrs2) - | I_funcall (_, _, _, cvals, ctyp) -> - ctyp :: List.map cval_ctyp cvals - | I_convert (_, ctyp1, _, ctyp2) -> [ctyp1; ctyp2] - | I_copy (_, cval) -> [cval_ctyp cval] + | I_funcall (clexp, _, _, cvals) -> + clexp_ctyp clexp :: List.map cval_ctyp cvals + | I_copy (clexp, cval) -> [clexp_ctyp clexp; cval_ctyp cval] | I_block instrs | I_try_block instrs -> List.concat (List.map instr_ctyps instrs) | I_throw cval | I_jump (cval, _) | I_return cval -> [cval_ctyp cval] | I_comment _ | I_label _ | I_goto _ | I_raw _ | I_match_failure -> [] @@ -546,7 +627,14 @@ let rec compile_aval ctx = function [], (frag, ctyp_of_typ ctx typ), [] | AV_id (id, typ) -> - [], (F_id id, ctyp_of_typ ctx (lvar_typ typ)), [] + begin + try + let _, ctyp = Bindings.find id ctx.locals in + [], (F_id id, ctyp), [] + with + | Not_found -> + [], (F_id 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))), [] @@ -590,7 +678,7 @@ let rec compile_aval ctx = function let gs = gensym () in setup @ [idecl tup_ctyp gs] - @ List.mapi (fun n cval -> icopy (CL_field (gs, "tup" ^ string_of_int n)) cval) cvals, + @ List.mapi (fun n cval -> icopy (CL_field (gs, "tup" ^ string_of_int n, cval_ctyp cval)) cval) cvals, (F_id gs, CT_tup (List.map cval_ctyp cvals)), [iclear tup_ctyp gs] @ cleanup @@ -601,7 +689,7 @@ let rec compile_aval ctx = function let compile_fields (id, aval) = let field_setup, cval, field_cleanup = compile_aval ctx aval in field_setup - @ [icopy (CL_field (gs, string_of_id id)) cval] + @ [icopy (CL_field (gs, string_of_id id, cval_ctyp cval)) cval] @ field_cleanup in [idecl ctyp gs] @@ -637,10 +725,9 @@ let rec compile_aval ctx = function let chunks = Util.drop (len mod 64) avals |> chunkify 64 |> List.map bitstring in let gs = gensym () in [iinit (CT_bits true) gs (first_chunk, CT_bits64 (len mod 64, true))] - @ List.map (fun chunk -> ifuncall (CL_id gs) + @ List.map (fun chunk -> ifuncall (CL_id (gs, CT_bits true)) (mk_id "append_64") - [(F_id gs, CT_bits true); (chunk, CT_bits64 (64, true))] - (CT_bits true)) chunks, + [(F_id gs, CT_bits true); (chunk, CT_bits64 (64, true))]) chunks, (F_id gs, CT_bits true), [iclear (CT_bits true) gs] @@ -661,12 +748,12 @@ let rec compile_aval ctx = function match cval with | (F_lit (V_bit Sail2_values.B0), _) -> [] | (F_lit (V_bit Sail2_values.B1), _) -> - [icopy (CL_id gs) (F_op (F_id gs, "|", F_lit (mask i)), ctyp)] + [icopy (CL_id (gs, ctyp)) (F_op (F_id gs, "|", F_lit (mask i)), ctyp)] | _ -> - setup @ [iif cval [icopy (CL_id gs) (F_op (F_id gs, "|", F_lit (mask i)), ctyp)] [] CT_unit] @ cleanup + setup @ [iif cval [icopy (CL_id (gs, ctyp)) (F_op (F_id gs, "|", F_lit (mask i)), ctyp)] [] CT_unit] @ cleanup in [idecl ctyp gs; - icopy (CL_id gs) (F_lit (V_bits (Util.list_init 64 (fun _ -> Sail2_values.B0))), ctyp)] + icopy (CL_id (gs, ctyp)) (F_lit (V_bits (Util.list_init 64 (fun _ -> Sail2_values.B0))), ctyp)] @ List.concat (List.mapi aval_mask (List.rev avals)), (F_id gs, ctyp), [] @@ -685,13 +772,13 @@ let rec compile_aval ctx = function let aval_set i aval = let setup, cval, cleanup = compile_aval ctx aval in setup - @ [iextern (CL_id gs) + @ [iextern (CL_id (gs, vector_ctyp)) (mk_id "internal_vector_update") - [(F_id gs, vector_ctyp); (F_lit (V_int (Big_int.of_int i)), CT_int64); cval] vector_ctyp] + [(F_id gs, vector_ctyp); (F_lit (V_int (Big_int.of_int i)), CT_int64); cval]] @ cleanup in [idecl vector_ctyp gs; - iextern (CL_id gs) (mk_id "internal_vector_init") [(F_lit (V_int (Big_int.of_int len)), CT_int64)] vector_ctyp] + iextern (CL_id (gs, vector_ctyp)) (mk_id "internal_vector_init") [(F_lit (V_int (Big_int.of_int len)), CT_int64)]] @ List.concat (List.mapi aval_set (if direction then List.rev avals else avals)), (F_id gs, vector_ctyp), [iclear vector_ctyp gs] @@ -707,7 +794,7 @@ let rec compile_aval ctx = function let gs = gensym () in let mk_cons aval = let setup, cval, cleanup = compile_aval ctx aval in - setup @ [ifuncall (CL_id gs) (mk_id ("cons#" ^ string_of_ctyp ctyp)) [cval; (F_id gs, CT_list ctyp)] (CT_list ctyp)] @ cleanup + setup @ [ifuncall (CL_id (gs, CT_list ctyp)) (mk_id ("cons#" ^ string_of_ctyp ctyp)) [cval; (F_id gs, CT_list ctyp)]] @ cleanup in [idecl (CT_list ctyp) gs] @ List.concat (List.map mk_cons (List.rev avals)), @@ -728,125 +815,103 @@ let compile_funcall l ctx id args typ = | Typ_fn (arg_typ, ret_typ, _) -> [arg_typ], ret_typ | _ -> assert false in - let ctx' = { ctx with local_env = add_typquant (id_loc id) quant ctx.local_env } in + let ctx' = { ctx with local_env = add_typquant (id_loc id) quant ctx.tc_env } in let arg_ctyps, ret_ctyp = List.map (ctyp_of_typ ctx') arg_typs, ctyp_of_typ ctx' ret_typ in let final_ctyp = ctyp_of_typ ctx typ in let setup_arg ctyp aval = let arg_setup, cval, arg_cleanup = compile_aval ctx aval in - setup := List.rev arg_setup @ !setup; + setup := List.rev arg_setup @ [icomment (string_of_ctyp (cval_ctyp cval))] @ !setup; cleanup := arg_cleanup @ !cleanup; let have_ctyp = cval_ctyp cval in if ctyp_equal ctyp have_ctyp then cval - else if is_stack_ctyp have_ctyp && not (is_stack_ctyp ctyp) then + else let gs = gensym () in setup := iinit ctyp gs cval :: !setup; cleanup := iclear ctyp gs :: !cleanup; (F_id gs, ctyp) - else if not (is_stack_ctyp have_ctyp) && is_stack_ctyp ctyp then - (* This is inefficient. FIXME: Remove id restriction on iconvert - instruction. Fortunatly only happens when flow typing makes a - length-polymorphic bitvector monomorphic. *) - let gs1 = gensym () in - let gs2 = gensym () in - setup := idecl have_ctyp gs1 :: !setup; - setup := icopy (CL_id gs1) cval :: !setup; - setup := idecl ctyp gs2 :: !setup; - setup := iconvert (CL_id gs2) ctyp gs1 have_ctyp :: !setup; - cleanup := iclear have_ctyp gs1 :: !cleanup; - (F_id gs2, ctyp) - else - c_error ~loc:l - (Printf.sprintf "Failure when setting up function %s arguments: %s and %s." (string_of_id id) (string_of_ctyp have_ctyp) (string_of_ctyp ctyp)) in assert (List.length arg_ctyps = List.length args); - let sargs = List.map2 setup_arg arg_ctyps args in + let setup_args = List.map2 setup_arg arg_ctyps args in - let call = - if ctyp_equal final_ctyp ret_ctyp then - fun ret -> ifuncall ret id sargs ret_ctyp - else if not (is_stack_ctyp ret_ctyp) && is_stack_ctyp final_ctyp then - let gs = gensym () in - setup := idecl ret_ctyp gs :: !setup; - setup := ifuncall (CL_id gs) id sargs ret_ctyp :: !setup; - cleanup := iclear ret_ctyp gs :: !cleanup; - fun ret -> iconvert ret final_ctyp gs ret_ctyp - else if is_stack_ctyp ret_ctyp && not (is_stack_ctyp final_ctyp) then - let gs = gensym () in - setup := idecl ret_ctyp gs :: !setup; - setup := ifuncall (CL_id gs) id sargs ret_ctyp :: !setup; - fun ret -> iconvert ret final_ctyp gs ret_ctyp - else - c_error (Printf.sprintf "Funcall call type mismatch between %s and %s" (string_of_ctyp ret_ctyp) (string_of_ctyp final_ctyp)) - in - - (List.rev !setup, final_ctyp, call, !cleanup) + List.rev !setup, + begin fun clexp -> + if ctyp_equal (clexp_ctyp clexp) ret_ctyp then + ifuncall clexp id setup_args + else + let gs = gensym () in + iblock [idecl ret_ctyp gs; + ifuncall (CL_id (gs, ret_ctyp)) id setup_args; + icopy clexp (F_id gs, ret_ctyp); + iclear ret_ctyp gs] + end, + !cleanup 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], - [] + [], + ctx + | AP_global (pid, typ), (frag, ctyp) -> let global_ctyp = ctyp_of_typ ctx typ in - if ctyp_equal global_ctyp ctyp then - [icopy (CL_id pid) cval], [] - else - begin match frag with - | F_id id -> - [iconvert (CL_id pid) global_ctyp id ctyp], [] - | _ -> c_error "Cannot compile global letbinding" - end + [icopy (CL_id (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 (CL_id pid) (frag, ctyp)], [] - | _ -> [ijump (F_op (F_id pid, "!=", frag), CT_bool) case_label], [] + | Unbound -> [idecl ctyp pid; icopy (CL_id (pid, ctyp)) (frag, ctyp)], [], ctx + | _ -> [ijump (F_op (F_id 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 - if ctyp_equal id_ctyp ctyp then - [idecl ctyp pid; icopy (CL_id pid) cval], [iclear id_ctyp pid] - else - let gs = gensym () in - [idecl id_ctyp pid; idecl ctyp gs; icopy (CL_id gs) cval; iconvert (CL_id pid) id_ctyp gs ctyp; iclear ctyp gs], [iclear id_ctyp pid] + c_debug (lazy ("Adding local " ^ string_of_id pid ^ " : " ^ string_of_ctyp id_ctyp)); + let ctx = { ctx with locals = Bindings.add pid (Immutable, id_ctyp) ctx.locals } in + [idecl ctyp pid; icopy (CL_id (pid, id_ctyp)) cval], [iclear id_ctyp pid], ctx + | AP_tup apats, (frag, ctyp) -> begin let get_tup n ctyp = (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 + let fold (instrs, cleanup, n, ctx) apat ctyp = + let instrs', cleanup', ctx = compile_match ctx apat (get_tup n ctyp) case_label in + instrs @ instrs', cleanup' @ cleanup, n + 1, ctx in match ctyp with | CT_tup ctyps -> - let instrs, cleanup, _ = List.fold_left2 fold ([], [], 0) apats ctyps in - instrs, cleanup + let instrs, cleanup, _, ctx = List.fold_left2 fold ([], [], 0, ctx) apats ctyps in + instrs, cleanup, ctx | _ -> failwith ("AP_tup with ctyp " ^ string_of_ctyp ctyp) end + | AP_app (ctor, apat), (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 instrs, cleanup = compile_match ctx apat ((F_field (frag, Util.zencode_string ctor_c_id), ctor_ctyp)) case_label 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] @ instrs, - cleanup + cleanup, + ctx | _ -> failwith "AP_app constructor with non-variant type" end - | AP_wild, _ -> [], [] + + | AP_wild, _ -> [], [], ctx | AP_cons (hd_apat, tl_apat), (frag, CT_list ctyp) -> - let hd_setup, hd_cleanup = compile_match ctx hd_apat (F_field (F_unary ("*", frag), "hd"), ctyp) case_label in - let tl_setup, tl_cleanup = compile_match ctx tl_apat (F_field (F_unary ("*", frag), "tl"), CT_list ctyp) case_label in - [ijump (F_op (frag, "==", F_lit V_null), CT_bool) case_label] @ hd_setup @ tl_setup, tl_cleanup @ hd_cleanup + let hd_setup, hd_cleanup, ctx = compile_match ctx hd_apat (F_field (F_unary ("*", frag), "hd"), ctyp) case_label in + let tl_setup, tl_cleanup, ctx = compile_match ctx tl_apat (F_field (F_unary ("*", frag), "tl"), CT_list ctyp) case_label in + [ijump (F_op (frag, "==", F_lit V_null), CT_bool) case_label] @ hd_setup @ tl_setup, tl_cleanup @ hd_cleanup, ctx + | AP_cons _, (_, _) -> c_error "Tried to pattern match cons on non list type" - | AP_nil, (frag, _) -> [ijump (F_op (frag, "!=", F_lit V_null), CT_bool) case_label], [] + | AP_nil, (frag, _) -> [ijump (F_op (frag, "!=", F_lit V_null), CT_bool) case_label], [], ctx let unit_fragment = (F_lit V_unit, CT_unit) @@ -860,34 +925,34 @@ let label str = incr label_counter; str +let pointer_assign ctyp1 ctyp2 = + match ctyp1 with + | CT_ref ctyp1 when ctyp_equal ctyp1 ctyp2 -> true + | CT_ref ctyp1 -> + c_error (Printf.sprintf "Incompatible type in pointer assignment between %s and %s" + (string_of_ctyp ctyp1) + (string_of_ctyp ctyp2)) + | _ -> false + let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) = let ctx = { ctx with local_env = env } in match aexp_aux with - | AE_let (id, _, binding, body, typ) -> - let setup, ctyp, call, cleanup = compile_aexp ctx binding in + | AE_let (mut, id, binding_typ, binding, body, body_typ) -> + let binding_ctyp = ctyp_of_typ ctx binding_typ in + let setup, call, cleanup = compile_aexp ctx binding in let letb_setup, letb_cleanup = - [idecl ctyp id; iblock (setup @ [call (CL_id id)] @ cleanup)], [iclear ctyp id] + [idecl binding_ctyp id; iblock (setup @ [call (CL_id (id, binding_ctyp))] @ cleanup)], [iclear binding_ctyp id] in - let setup, ctyp, call, cleanup = compile_aexp ctx body in - let body_ctyp = ctyp_of_typ ctx typ in - if ctyp_equal body_ctyp ctyp then - letb_setup @ setup, ctyp, call, cleanup @ letb_cleanup - else - begin - prerr_endline ("Mismatch: " ^ string_of_ctyp body_ctyp ^ " and " ^ string_of_ctyp ctyp); - let gs = gensym () in - letb_setup @ setup @ [idecl ctyp gs; call (CL_id gs)], - body_ctyp, - (fun clexp -> iconvert clexp body_ctyp gs ctyp), - [iclear ctyp gs] @ cleanup @ letb_cleanup - end + let ctx = { ctx with locals = Bindings.add id (mut, binding_ctyp) ctx.locals } in + let setup, call, cleanup = compile_aexp ctx body in + letb_setup @ setup, call, cleanup @ letb_cleanup | AE_app (id, vs, typ) -> compile_funcall l ctx id vs typ | AE_val aval -> let setup, cval, cleanup = compile_aval ctx aval in - setup, cval_ctyp cval, (fun clexp -> icopy clexp cval), cleanup + setup, (fun clexp -> icopy clexp cval), cleanup (* Compile case statements *) | AE_case (aval, cases, typ) -> @@ -903,19 +968,19 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) = in let case_label = label "case_" in c_debug (lazy ("Compiling match")); - let destructure, destructure_cleanup = compile_match ctx apat cval case_label in + let destructure, destructure_cleanup, ctx = compile_match ctx apat cval case_label in c_debug (lazy ("Compiled match")); - 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 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 case_instrs = destructure @ [icomment "end destructuring"] @ (if not trivial_guard then - guard_setup @ [idecl CT_bool gs; guard_call (CL_id gs)] @ guard_cleanup + 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)] @ body_cleanup @ destructure_cleanup + @ body_setup @ [body_call (CL_id (case_return_id, ctyp))] @ body_cleanup @ destructure_cleanup @ [igoto finish_match_label] in [iblock case_instrs; ilabel case_label] @@ -925,15 +990,15 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) = @ List.concat (List.map compile_case cases) @ [imatch_failure ()] @ [ilabel finish_match_label], - ctyp, (fun clexp -> icopy clexp (F_id case_return_id, ctyp)), - (if is_stack_ctyp ctyp then [] else [iclear ctyp case_return_id]) + [iclear ctyp case_return_id] @ aval_cleanup @ [icomment "end match"] (* Compile try statement *) | AE_try (aexp, cases, typ) -> - let aexp_setup, ctyp, aexp_call, aexp_cleanup = compile_aexp ctx aexp in + 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 handled_exception_label = label "handled_exception_" in let compile_case (apat, guard, body) = @@ -944,18 +1009,18 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) = 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 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 + 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 case_instrs = destructure @ [icomment "end destructuring"] @ (if not trivial_guard then - guard_setup @ [idecl CT_bool gs; guard_call (CL_id gs)] @ guard_cleanup + guard_setup @ [idecl CT_bool gs; guard_call (CL_id (gs, CT_bool))] @ guard_cleanup @ [ijump (F_unary ("!", F_id gs), CT_bool) try_label] @ [icomment "end guard"] else []) - @ body_setup @ [body_call (CL_id try_return_id)] @ body_cleanup @ destructure_cleanup + @ body_setup @ [body_call (CL_id (try_return_id, ctyp))] @ body_cleanup @ destructure_cleanup @ [igoto handled_exception_label] in [iblock case_instrs; ilabel try_label] @@ -963,35 +1028,23 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) = assert (ctyp_equal ctyp (ctyp_of_typ ctx typ)); [icomment "begin try catch"; idecl ctyp try_return_id; - itry_block (aexp_setup @ [aexp_call (CL_id try_return_id)] @ aexp_cleanup); + 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] @ List.concat (List.map compile_case cases) @ [imatch_failure (); ilabel handled_exception_label; icopy CL_have_exception (F_lit (V_bool false), CT_bool)], - ctyp, (fun clexp -> icopy clexp (F_id try_return_id, ctyp)), [] | AE_if (aval, then_aexp, else_aexp, if_typ) -> let if_ctyp = ctyp_of_typ ctx if_typ in let compile_branch aexp = - let setup, ctyp, call, cleanup = compile_aexp ctx aexp in - if ctyp_equal if_ctyp ctyp then - fun clexp -> setup @ [call clexp] @ cleanup - else - fun clexp -> - let gs = gensym () in - setup - @ [idecl ctyp gs; - call (CL_id gs); - iconvert clexp if_ctyp gs ctyp; - iclear ctyp gs] - @ cleanup + let setup, call, cleanup = compile_aexp ctx aexp in + fun clexp -> setup @ [call clexp] @ cleanup in let setup, cval, cleanup = compile_aval ctx aval in setup, - if_ctyp, (fun clexp -> iif cval (compile_branch then_aexp clexp) (compile_branch else_aexp clexp) @@ -1001,43 +1054,51 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) = (* FIXME: AE_record_update could be AV_record_update - would reduce some copying. *) | AE_record_update (aval, fields, typ) -> let ctyp = ctyp_of_typ ctx typ in + let ctors = match ctyp with + | CT_struct (_, ctors) -> List.fold_left (fun m (k, v) -> Bindings.add k v m) Bindings.empty ctors + | _ -> c_error "Cannot perform record update for non-record type" + in let gs = gensym () in let compile_fields (id, aval) = let field_setup, cval, field_cleanup = compile_aval ctx aval in field_setup - @ [icopy (CL_field (gs, string_of_id id)) cval] + @ [icomment (string_of_ctyp ctyp)] + @ [icopy (CL_field (gs, string_of_id id, Bindings.find id ctors)) cval] @ field_cleanup in let setup, cval, cleanup = compile_aval ctx aval in [idecl ctyp gs] @ setup - @ [icopy (CL_id gs) cval] + @ [icopy (CL_id (gs, ctyp)) cval] @ cleanup @ List.concat (List.map compile_fields (Bindings.bindings fields)), - ctyp, (fun clexp -> icopy clexp (F_id gs, ctyp)), [iclear ctyp gs] | AE_short_circuit (SC_and, aval, aexp) -> let left_setup, cval, left_cleanup = compile_aval ctx aval in - let right_setup, _, call, right_cleanup = compile_aexp ctx aexp in + let right_setup, call, right_cleanup = compile_aexp ctx aexp in let gs = gensym () in left_setup @ [ idecl CT_bool gs; - iif cval (right_setup @ [call (CL_id gs)] @ right_cleanup) [icopy (CL_id gs) (F_lit (V_bool false), CT_bool)] CT_bool ] + iif cval + (right_setup @ [call (CL_id (gs, CT_bool))] @ right_cleanup) + [icopy (CL_id (gs, CT_bool)) (F_lit (V_bool false), CT_bool)] + CT_bool ] @ left_cleanup, - CT_bool, (fun clexp -> icopy clexp (F_id gs, CT_bool)), [] | AE_short_circuit (SC_or, aval, aexp) -> let left_setup, cval, left_cleanup = compile_aval ctx aval in - let right_setup, _, call, right_cleanup = compile_aexp ctx aexp in + let right_setup, call, right_cleanup = compile_aexp ctx aexp in let gs = gensym () in left_setup @ [ idecl CT_bool gs; - iif cval [icopy (CL_id gs) (F_lit (V_bool true), CT_bool)] (right_setup @ [call (CL_id gs)] @ right_cleanup) CT_bool ] + iif cval + [icopy (CL_id (gs, CT_bool)) (F_lit (V_bool true), CT_bool)] + (right_setup @ [call (CL_id (gs, CT_bool))] @ right_cleanup) + CT_bool ] @ left_cleanup, - CT_bool, (fun clexp -> icopy clexp (F_id gs, CT_bool)), [] @@ -1049,91 +1110,64 @@ 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 ctx aval in field_setup - @ [icopy (CL_field (id, string_of_id field_id)) cval] + @ [icopy (CL_field (id, string_of_id field_id, cval_ctyp cval)) cval] @ field_cleanup in List.concat (List.map compile_fields (Bindings.bindings fields)), - CT_unit, (fun clexp -> icopy clexp unit_fragment), [] | AE_assign (id, assign_typ, aexp) -> - (* assign_ctyp is the type of the C variable we are assigning to, - ctyp is the type of the C expression being assigned. These may - be different. *) - let pointer_assign ctyp1 ctyp2 = - match ctyp1 with - | CT_ref ctyp1 when ctyp_equal ctyp1 ctyp2 -> true - | CT_ref ctyp1 -> c_error ~loc:l "Incompatible type in pointer assignment" - | _ -> false - in let assign_ctyp = ctyp_of_typ ctx assign_typ in - let setup, ctyp, call, cleanup = compile_aexp ctx aexp in - let comment = "assign " ^ string_of_ctyp assign_ctyp ^ " := " ^ string_of_ctyp ctyp in - if ctyp_equal assign_ctyp ctyp then - setup @ [call (CL_id id)], CT_unit, (fun clexp -> icopy clexp unit_fragment), cleanup - else if pointer_assign assign_ctyp ctyp then - setup @ [call (CL_addr id)], CT_unit, (fun clexp -> icopy clexp unit_fragment), cleanup - else - let gs = gensym () in - setup @ [ icomment comment; - idecl ctyp gs; - call (CL_id gs); - iconvert (CL_id id) assign_ctyp gs ctyp; - iclear ctyp gs - ], - CT_unit, - (fun clexp -> icopy clexp unit_fragment), - cleanup + let setup, call, cleanup = compile_aexp ctx aexp in + setup @ [call (CL_id (id, assign_ctyp))], (fun clexp -> icopy clexp unit_fragment), cleanup | AE_block (aexps, aexp, _) -> let block = compile_block ctx aexps in - let setup, ctyp, call, cleanup = compile_aexp ctx aexp in - block @ setup, ctyp, call, cleanup + let setup, call, cleanup = compile_aexp ctx aexp in + block @ setup, call, cleanup | AE_loop (While, cond, body) -> let loop_start_label = label "while_" in 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 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 loop_test = (F_unary ("!", F_id gs), CT_bool) in [idecl CT_bool gs; idecl CT_unit unit_gs] @ [ilabel loop_start_label] @ [iblock (cond_setup - @ [cond_call (CL_id gs)] + @ [cond_call (CL_id (gs, CT_bool))] @ cond_cleanup @ [ijump loop_test loop_end_label] @ body_setup - @ [body_call (CL_id unit_gs)] + @ [body_call (CL_id (unit_gs, CT_unit))] @ body_cleanup @ [igoto loop_start_label])] @ [ilabel loop_end_label], - CT_unit, (fun clexp -> icopy clexp unit_fragment), [] | AE_loop (Until, cond, body) -> let loop_start_label = label "repeat_" in 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 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 loop_test = (F_id gs, CT_bool) in [idecl CT_bool gs; idecl CT_unit unit_gs] @ [ilabel loop_start_label] @ [iblock (body_setup - @ [body_call (CL_id unit_gs)] + @ [body_call (CL_id (unit_gs, CT_unit))] @ body_cleanup @ cond_setup - @ [cond_call (CL_id gs)] + @ [cond_call (CL_id (gs, CT_bool))] @ cond_cleanup @ [ijump loop_test loop_end_label] @ [igoto loop_start_label])] @ [ilabel loop_end_label], - CT_unit, (fun clexp -> icopy clexp unit_fragment), [] @@ -1149,19 +1183,13 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) = let creturn = if ctyp_equal fn_return_ctyp (cval_ctyp cval) then [ireturn cval] - else if is_stack_ctyp (cval_ctyp cval) && not (is_stack_ctyp fn_return_ctyp) then - let gs1 = gensym () in - let gs2 = gensym () in - [idecl (cval_ctyp cval) gs1; - icopy (CL_id gs1) cval; - idecl fn_return_ctyp gs2; - iconvert (CL_id gs2) fn_return_ctyp gs1 (cval_ctyp cval); - ireturn (F_id gs2, fn_return_ctyp)] else - c_error ~loc:l "Can only do return type conversion from stack to heap" + let gs = gensym () in + [idecl fn_return_ctyp gs; + icopy (CL_id (gs, fn_return_ctyp)) cval; + ireturn (F_id gs, fn_return_ctyp)] in return_setup @ creturn, - ctyp_of_typ ctx typ, (fun clexp -> icomment "unreachable after return"), [] @@ -1169,7 +1197,6 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) = (* Cleanup info will be handled by fix_exceptions *) let throw_setup, cval, _ = compile_aval ctx aval in throw_setup @ [ithrow cval], - ctyp_of_typ ctx typ, (fun clexp -> icomment "unreachable after throw"), [] @@ -1177,7 +1204,6 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) = let ctyp = ctyp_of_typ ctx typ in let setup, cval, cleanup = compile_aval ctx aval in setup, - ctyp, (fun clexp -> icopy clexp (F_field (fst cval, Util.zencode_string (string_of_id id)), ctyp)), cleanup @@ -1198,43 +1224,37 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) = in (* Loop variables *) - let from_setup, from_ctyp, from_call, from_cleanup = compile_aexp ctx loop_from in + let from_setup, from_call, from_cleanup = compile_aexp ctx loop_from in let from_gs = gensym () in - let to_setup, to_ctyp, to_call, to_cleanup = compile_aexp ctx loop_to in + let to_setup, to_call, to_cleanup = compile_aexp ctx loop_to in let to_gs = gensym () in - let step_setup, step_ctyp, step_call, step_cleanup = compile_aexp ctx loop_step in + let step_setup, step_call, step_cleanup = compile_aexp ctx loop_step in let step_gs = gensym () in - let variable_init gs setup ctyp call cleanup = + let variable_init gs setup call cleanup = [idecl CT_int64 gs; - if is_stack_ctyp ctyp then - iblock (setup @ [call (CL_id gs)] @ cleanup) - else - let gs' = gensym () in - iblock (setup - @ [idecl ctyp gs'; call (CL_id gs'); iconvert (CL_id gs) CT_int64 gs' ctyp; iclear ctyp gs'] - @ cleanup)] + iblock (setup @ [call (CL_id (gs, CT_int64))] @ cleanup)] in 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_setup, body_call, body_cleanup = compile_aexp ctx body in let body_gs = gensym () in - variable_init from_gs from_setup from_ctyp from_call from_cleanup - @ variable_init to_gs to_setup to_ctyp to_call to_cleanup - @ variable_init step_gs step_setup step_ctyp step_call step_cleanup + variable_init from_gs from_setup from_call from_cleanup + @ variable_init to_gs to_setup to_call to_cleanup + @ variable_init step_gs step_setup step_call step_cleanup @ [iblock ([idecl CT_int64 loop_var; - icopy (CL_id loop_var) (F_id from_gs, CT_int64); + icopy (CL_id (loop_var, CT_int64)) (F_id from_gs, CT_int64); idecl CT_unit body_gs; iblock ([ilabel loop_start_label] @ [ijump (F_op (F_id loop_var, (if is_inc then ">" else "<"), F_id to_gs), CT_bool) loop_end_label] @ body_setup - @ [body_call (CL_id body_gs)] + @ [body_call (CL_id (body_gs, CT_unit))] @ body_cleanup - @ [icopy (CL_id loop_var) (F_op (F_id loop_var, (if is_inc then "+" else "-"), F_id step_gs), CT_int64)] + @ [icopy (CL_id (loop_var, CT_int64)) + (F_op (F_id loop_var, (if is_inc then "+" else "-"), F_id step_gs), CT_int64)] @ [igoto loop_start_label]); ilabel loop_end_label])], - CT_unit, (fun clexp -> icopy clexp unit_fragment), [] @@ -1245,10 +1265,10 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) = and compile_block ctx = function | [] -> [] | exp :: exps -> - let setup, _, call, cleanup = compile_aexp ctx exp in + let setup, call, cleanup = compile_aexp ctx exp in let rest = compile_block ctx exps in let gs = gensym () in - iblock (setup @ [idecl CT_unit gs; call (CL_id gs)] @ cleanup) :: rest + 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 actual work of translating the typedefs into C is done by the code @@ -1384,7 +1404,7 @@ let fix_early_stack_return ctx instrs = in rewrite_return [] instrs -let fix_exception_block ctx instrs = +let fix_exception_block ?return:(return=None) ctx instrs = let end_block_label = label "end_block_exception_" in let is_exception_stop (I_aux (instr, _)) = match instr with @@ -1409,12 +1429,12 @@ let fix_exception_block ctx instrs = @ rewrite_exception historic after | before, I_aux (I_throw cval, _) :: after -> before - @ [icopy CL_current_exception cval; + @ [icopy (CL_current_exception (cval_ctyp cval)) cval; icopy CL_have_exception (F_lit (V_bool true), CT_bool)] @ generate_cleanup (historic @ before) @ [igoto end_block_label] @ rewrite_exception (historic @ before) after - | before, (I_aux (I_funcall (x, _, f, args, ctyp), _) as funcall) :: after -> + | before, (I_aux (I_funcall (x, _, f, args), _) 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 *) @@ -1429,24 +1449,27 @@ let fix_exception_block ctx instrs = before @ funcall :: rewrite_exception (historic @ before) after | _, _ -> assert false (* unreachable *) in - rewrite_exception [] instrs - @ [ilabel end_block_label] - + match return with + | None -> + rewrite_exception [] instrs @ [ilabel end_block_label] + | Some ctyp -> + rewrite_exception [] instrs @ [ilabel end_block_label; iundefined ctyp] + let rec map_try_block f (I_aux (instr, aux)) = let instr = match instr with | 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_convert _ | I_copy _ | 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 -> instr + | I_comment _ | I_label _ | I_goto _ | I_raw _ | I_jump _ | I_match_failure | I_undefined _ -> instr in I_aux (instr, aux) -let fix_exception ctx instrs = +let fix_exception ?return:(return=None) ctx instrs = let instrs = List.map (map_try_block (fix_exception_block ctx)) instrs in - fix_exception_block ctx instrs + fix_exception_block ~return:return ctx instrs let rec arg_pats ctx (Typ_aux (arg_typ_aux, _) as arg_typ) (P_aux (p_aux, (l, _)) as pat) = match p_aux, arg_typ_aux with @@ -1466,7 +1489,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 gs, ctyp) label in (gs, (destructure, cleanup)) let combine_destructure_cleanup xs = List.concat (List.map fst xs), List.concat (List.rev (List.map snd xs)) @@ -1484,9 +1507,9 @@ let rec compile_def ctx = function | DEF_reg_dec (DEC_aux (DEC_reg (typ, id), _)) -> [CDEF_reg_dec (id, ctyp_of_typ ctx typ, [])], ctx | DEF_reg_dec (DEC_aux (DEC_config (id, typ, exp), _)) -> - let aexp = map_functions (analyze_primop ctx) (c_literals ctx (no_shadow IdSet.empty (anf exp))) in - let setup, ctyp, call, cleanup = compile_aexp ctx aexp in - let instrs = setup @ [call (CL_id id)] @ cleanup in + let aexp = analyze_functions ctx analyze_primop (c_literals 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 [CDEF_reg_dec (id, ctyp_of_typ ctx typ, instrs)], ctx | DEF_spec (VS_aux (VS_val_spec (_, id, _, _), _)) -> @@ -1503,30 +1526,57 @@ let rec compile_def ctx = function | DEF_fundef (FD_aux (FD_function (_, _, _, [FCL_aux (FCL_Funcl (id, Pat_aux (Pat_exp (pat, exp), _)), _)]), _)) -> c_debug (lazy ("Compiling function " ^ string_of_id id)); - let aexp = map_functions (analyze_primop ctx) (c_literals ctx (no_shadow (pat_ids pat) (anf exp))) in - let setup, ctyp, call, cleanup = compile_aexp ctx aexp in - c_debug (lazy "Compiled aexp"); - let fundef_label = label "fundef_fail_" in - let _, Typ_aux (fn_typ, _) = Env.get_val_spec id ctx.tc_env in + (* Find the function's type *) + let quant, Typ_aux (fn_typ, _) = + try Env.get_val_spec id ctx.local_env + with Type_error _ -> + c_debug (lazy ("Falling back to global env for " ^ string_of_id id)); Env.get_val_spec id ctx.tc_env + in let arg_typ, ret_typ = match fn_typ with | Typ_fn (arg_typ, ret_typ, _) -> arg_typ, ret_typ | _ -> assert false in - let compiled_args = List.map (compile_arg_pat ctx fundef_label) (arg_pats ctx arg_typ pat) in + + (* Handle the argument pattern *) + let fundef_label = label "fundef_fail_" in + let orig_ctx = ctx in + let ctx = { ctx with local_env = add_typquant (id_loc id) quant ctx.tc_env } in + let compiled_args' = arg_pats ctx arg_typ pat in + let compiled_args = List.map (compile_arg_pat ctx fundef_label) compiled_args' in + let ctx = + (* We need the primop analyzer to be aware of the function argument types, so put them in ctx *) + List.fold_left2 (fun ctx (id, _) (_, ctyp) -> { ctx with locals = Bindings.add id (Immutable, ctyp) ctx.locals }) ctx compiled_args compiled_args' + in + + if string_of_id id = "TLBTranslateC" then c_verbosity := 1 else (); + + (* Optimize and compile the expression *) + let aexp = no_shadow (pat_ids pat) (anf exp) in + c_debug (lazy (Pretty_print_sail.to_string (pp_aexp aexp))); + let aexp = analyze_functions ctx analyze_primop (c_literals ctx aexp) in + c_debug (lazy (Pretty_print_sail.to_string (pp_aexp aexp))); + let setup, call, cleanup = compile_aexp ctx aexp in + c_debug (lazy "Compiled aexp"); let gs = gensym () in let destructure, destructure_cleanup = compiled_args |> List.map snd |> combine_destructure_cleanup |> fix_destructure fundef_label in - if is_stack_ctyp ctyp then - let instrs = destructure @ [idecl ctyp gs] @ setup @ [call (CL_id gs)] @ cleanup @ destructure_cleanup @ [ireturn (F_id gs, ctyp)] in + + c_verbosity := 0; + + (* This better be true or something has gone badly wrong. *) + let ret_ctyp = ctyp_of_typ ctx ret_typ in + + if is_stack_ctyp ret_ctyp then + let instrs = destructure @ [idecl ret_ctyp gs] @ setup @ [call (CL_id (gs, ret_ctyp))] @ cleanup @ destructure_cleanup @ [ireturn (F_id gs, ret_ctyp)] in let instrs = fix_early_stack_return ctx instrs in - let instrs = fix_exception ctx instrs in - [CDEF_fundef (id, None, List.map fst compiled_args, instrs)], ctx + let instrs = fix_exception ~return:(Some ret_ctyp) ctx instrs in + [CDEF_fundef (id, None, List.map fst compiled_args, instrs)], orig_ctx else - let instrs = destructure @ setup @ [call (CL_addr gs)] @ cleanup @ destructure_cleanup in - let instrs = fix_early_return (CL_addr gs) ctx instrs in + let instrs = destructure @ setup @ [call (CL_addr (gs, ret_ctyp))] @ cleanup @ destructure_cleanup in + let instrs = fix_early_return (CL_addr (gs, ret_ctyp)) ctx instrs in let instrs = fix_exception ctx instrs in - [CDEF_fundef (id, Some gs, List.map fst compiled_args, instrs)], ctx + [CDEF_fundef (id, Some gs, List.map fst compiled_args, instrs)], orig_ctx | DEF_fundef (FD_aux (FD_function (_, _, _, []), (l, _))) -> c_error ~loc:l "Encountered function with no clauses" @@ -1543,14 +1593,15 @@ let rec compile_def ctx = function | DEF_val (LB_aux (LB_val (pat, exp), _)) -> c_debug (lazy ("Compiling letbind " ^ string_of_pat pat)); - let aexp = map_functions (analyze_primop ctx) (c_literals ctx (no_shadow IdSet.empty (anf exp))) in - let setup, ctyp, call, cleanup = compile_aexp ctx aexp in + let ctyp = ctyp_of_typ ctx (pat_typ_of pat) in + let aexp = analyze_functions ctx analyze_primop (c_literals 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 end_label = label "let_end_" in - let destructure, destructure_cleanup = compile_match ctx apat (F_id gs, ctyp) end_label in + let destructure, destructure_cleanup, _ = compile_match ctx apat (F_id gs, ctyp) end_label in let gs_setup, gs_cleanup = - [idecl ctyp gs], [iclear ctyp gs] + [idecl ctyp gs], [iclear ctyp gs] in let bindings = List.map (fun (id, typ) -> id, ctyp_of_typ ctx typ) (apat_globals apat) in let n = !letdef_count in @@ -1558,7 +1609,7 @@ let rec compile_def ctx = function let instrs = [icomment "gs_setup"] @ gs_setup @ [icomment "setup"] @ setup @ [icomment "call"] - @ [call (CL_id gs)] + @ [call (CL_id (gs, ctyp))] @ [icomment "cleanup"] @ cleanup @ [icomment "destructure"] @@ -1618,11 +1669,11 @@ let add_local_labels instrs = let clexp_rename from_id to_id = let rename id = if Id.compare id from_id = 0 then to_id else id in function - | CL_id id -> CL_id (rename id) - | CL_field (id, field) -> CL_field (rename id, field) - | CL_addr id -> CL_addr (rename id) - | CL_addr_field (id, field) -> CL_addr_field (rename id, field) - | CL_current_exception -> CL_current_exception + | CL_id (id, ctyp) -> CL_id (rename id, ctyp) + | CL_field (id, field, ctyp) -> CL_field (rename id, field, ctyp) + | CL_addr (id, ctyp) -> CL_addr (rename id, ctyp) + | CL_addr_field (id, field, ctyp) -> CL_addr_field (rename id, field, ctyp) + | CL_current_exception ctyp -> CL_current_exception ctyp | CL_have_exception -> CL_have_exception let rec instrs_rename from_id to_id = @@ -1639,17 +1690,15 @@ 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, ctyp), aux) :: instrs -> - I_aux (I_funcall (lrename clexp, extern, rename id, List.map crename cvals, ctyp), 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_convert (clexp, ctyp1, id, ctyp2), aux) :: instrs -> - I_aux (I_convert (lrename clexp, ctyp1, rename id, ctyp2), 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_label _ | I_goto _ | I_match_failure), _) as instr) :: instrs -> instr :: irename instrs + | (I_aux ((I_comment _ | I_raw _ | I_label _ | I_goto _ | I_match_failure | I_undefined _), _) as instr) :: instrs -> instr :: irename instrs | [] -> [] let hoist_ctyp = function @@ -1750,6 +1799,7 @@ let flatten_instrs ctx = | cdef -> [cdef] + (* (* When this optimization fires we know we have bytecode of the form recreate x : S; x = y; ... @@ -1762,18 +1812,18 @@ let flatten_instrs ctx = let fix_struct_updates ctx = (* FIXME need to check no remaining references *) let rec fix_updates struct_id id = function - | I_aux (I_copy (CL_field (struct_id', field), cval), aux) :: instrs + | I_aux (I_copy (CL_field (struct_id', field, ctyp), cval), aux) :: instrs when Id.compare struct_id struct_id' = 0 -> - Util.option_map (fun instrs -> I_aux (I_copy (CL_field (id, field), cval), aux) :: instrs) (fix_updates struct_id id instrs) + Util.option_map (fun instrs -> I_aux (I_copy (CL_field (id, field, ctyp), cval), aux) :: instrs) (fix_updates struct_id id instrs) | I_aux (I_copy (CL_id id', (F_id struct_id', ctyp)), aux) :: instrs when Id.compare struct_id struct_id' = 0 && Id.compare id id' = 0-> Some instrs | _ -> None in let rec fix_updates_ret struct_id id = function - | I_aux (I_copy (CL_field (struct_id', field), cval), aux) :: instrs + | I_aux (I_copy (CL_field (struct_id', field, ctyp), cval), aux) :: instrs when Id.compare struct_id struct_id' = 0 -> - Util.option_map (fun instrs -> I_aux (I_copy (CL_addr_field (id, field), cval), aux) :: instrs) (fix_updates_ret struct_id id instrs) + Util.option_map (fun instrs -> I_aux (I_copy (CL_addr_field (id, field, ctyp), cval), aux) :: instrs) (fix_updates_ret struct_id id instrs) | I_aux (I_copy (CL_addr id', (F_id struct_id', ctyp)), aux) :: instrs when Id.compare struct_id struct_id' = 0 && Id.compare id id' = 0-> Some instrs @@ -1781,10 +1831,9 @@ let fix_struct_updates ctx = in let rec opt hr = function | (I_aux (I_reset (ctyp, struct_id), _) as instr1) - :: (I_aux (I_copy (CL_id struct_id', (F_id id, ctyp')), _) as instr2) + :: (I_aux (I_copy (CL_id (struct_id', _), (F_id id, ctyp')), _) as instr2) :: instrs when is_ct_struct ctyp && ctyp_equal ctyp ctyp' && Id.compare struct_id struct_id' = 0 -> - prerr_endline ("Potential struct update " ^ string_of_id struct_id); begin match fix_updates struct_id id instrs with | None -> instr1 :: instr2 :: opt hr instrs | Some updated -> opt hr updated @@ -1793,7 +1842,6 @@ let fix_struct_updates ctx = | (I_aux (I_reset (ctyp, struct_id), _) as instr) :: instrs when is_ct_struct ctyp && Util.is_some hr -> let id = match hr with Some id -> id | None -> assert false in - prerr_endline ("Potential struct return " ^ string_of_id struct_id ^ " to " ^ string_of_id id); begin match fix_updates_ret struct_id id instrs with | None -> instr :: opt hr instrs | Some updated -> opt hr updated @@ -1811,6 +1859,7 @@ let fix_struct_updates ctx = | CDEF_fundef (function_id, heap_return, args, body) -> [CDEF_fundef (function_id, heap_return, args, opt heap_return body)] | cdef -> [cdef] + *) let concatMap f xs = List.concat (List.map f xs) @@ -1818,7 +1867,7 @@ let optimize ctx cdefs = let nothing cdefs = cdefs in cdefs |> (if !optimize_hoist_allocations then concatMap (hoist_allocations ctx) else nothing) - |> (if !optimize_struct_updates then concatMap (fix_struct_updates ctx) else nothing) +(* |> (if !optimize_struct_updates then concatMap (fix_struct_updates ctx) else nothing) *) (**************************************************************************) (* 6. Code generation *) @@ -1878,22 +1927,22 @@ let sgen_cval_param (frag, ctyp) = let sgen_cval = function (frag, _) -> string_of_fragment frag let sgen_clexp = function - | CL_id id -> "&" ^ sgen_id id - | CL_field (id, field) -> "&(" ^ sgen_id id ^ "." ^ Util.zencode_string field ^ ")" - | CL_addr id -> sgen_id id - | CL_addr_field (id, field) -> "&(" ^ sgen_id id ^ "->" ^ Util.zencode_string field ^ ")" + | CL_id (id, _) -> "&" ^ sgen_id id + | CL_field (id, field, _) -> "&(" ^ sgen_id id ^ "." ^ Util.zencode_string field ^ ")" + | CL_addr (id, _) -> sgen_id id + | CL_addr_field (id, field, _) -> "&(" ^ sgen_id id ^ "->" ^ Util.zencode_string field ^ ")" | CL_have_exception -> "have_exception" - | CL_current_exception -> "current_exception" + | CL_current_exception _ -> "current_exception" let sgen_clexp_pure = function - | CL_id id -> sgen_id id - | CL_field (id, field) -> sgen_id id ^ "." ^ Util.zencode_string field - | CL_addr id -> "*" ^ sgen_id id - | CL_addr_field (id, field) -> sgen_id id ^ "->" ^ Util.zencode_string field + | CL_id (id, _) -> sgen_id id + | CL_field (id, field, _) -> sgen_id id ^ "." ^ Util.zencode_string field + | CL_addr (id, _) -> "*" ^ sgen_id id + | CL_addr_field (id, field, _) -> sgen_id id ^ "->" ^ Util.zencode_string field | CL_have_exception -> "have_exception" - | CL_current_exception -> "current_exception" + | CL_current_exception _ -> "current_exception" -let rec codegen_instr fid ctx (I_aux (instr, _)) = +let rec codegen_instr fid ctx (I_aux (instr, (_, l))) = match instr with | I_decl (ctyp, id) when is_stack_ctyp ctyp -> string (Printf.sprintf " %s %s;" (sgen_ctyp ctyp) (sgen_id id)) @@ -1902,11 +1951,30 @@ let rec codegen_instr fid ctx (I_aux (instr, _)) = ^^ string (Printf.sprintf " CREATE(%s)(&%s);" (sgen_ctyp_name ctyp) (sgen_id id)) | I_copy (clexp, cval) -> - let ctyp = cval_ctyp cval in - if is_stack_ctyp ctyp then - string (Printf.sprintf " %s = %s;" (sgen_clexp_pure clexp) (sgen_cval cval)) + let lctyp = clexp_ctyp clexp in + let rctyp = cval_ctyp cval in + if ctyp_equal lctyp rctyp then + if is_stack_ctyp lctyp then + string (Printf.sprintf " %s = %s;" (sgen_clexp_pure clexp) (sgen_cval cval)) + else + string (Printf.sprintf " COPY(%s)(%s, %s);" (sgen_ctyp_name lctyp) (sgen_clexp clexp) (sgen_cval cval)) + else if pointer_assign lctyp rctyp then + let lctyp = match lctyp with + | CT_ref lctyp -> lctyp + | _ -> assert false + in + if is_stack_ctyp lctyp then + string (Printf.sprintf " *(%s) = %s;" (sgen_clexp_pure clexp) (sgen_cval cval)) + else + string (Printf.sprintf " COPY(%s)(*(%s), %s);" (sgen_ctyp_name lctyp) (sgen_clexp clexp) (sgen_cval cval)) else - string (Printf.sprintf " COPY(%s)(%s, %s);" (sgen_ctyp_name ctyp) (sgen_clexp clexp) (sgen_cval cval)) + if is_stack_ctyp lctyp then + string (Printf.sprintf " %s = CONVERT_OF(%s, %s)(%s);" + (sgen_clexp_pure clexp) (sgen_ctyp_name lctyp) (sgen_ctyp_name rctyp) (sgen_cval cval)) + else + string (Printf.sprintf " CONVERT_OF(%s, %s)(%s, %s);" + (sgen_ctyp_name lctyp) (sgen_ctyp_name rctyp) (sgen_clexp clexp) (sgen_cval cval)) + | I_jump (cval, label) -> string (Printf.sprintf " if (%s) goto %s;" (sgen_cval cval) label) | I_if (cval, [then_instr], [], ctyp) -> @@ -1928,8 +1996,9 @@ let rec codegen_instr fid ctx (I_aux (instr, _)) = string " { /* try */" ^^ jump 2 2 (separate_map hardline (codegen_instr fid ctx) instrs) ^^ hardline ^^ string " }" - | I_funcall (x, extern, f, args, ctyp) -> + | I_funcall (x, extern, f, args) -> let c_args = Util.string_of_list ", " sgen_cval args in + let ctyp = clexp_ctyp x in let fname = if Env.is_extern f ctx.tc_env "c" then Env.get_extern f ctx.tc_env "c" @@ -1975,10 +2044,11 @@ let rec codegen_instr fid ctx (I_aux (instr, _)) = string (Printf.sprintf " %s = *(%s);" (sgen_clexp_pure x) c_args) else string (Printf.sprintf " COPY(%s)(&%s, *(%s));" (sgen_ctyp_name ctyp) (sgen_clexp_pure x) c_args) - else if is_stack_ctyp ctyp then - string (Printf.sprintf " %s = %s(%s);" (sgen_clexp_pure x) fname c_args) else - string (Printf.sprintf " %s(%s, %s);" fname (sgen_clexp x) c_args) + if is_stack_ctyp ctyp then + string (Printf.sprintf " %s = %s(%s);" (sgen_clexp_pure x) fname c_args) + else + string (Printf.sprintf " %s(%s, %s);" fname (sgen_clexp x) c_args) | I_clear (ctyp, id) when is_stack_ctyp ctyp -> empty @@ -2009,70 +2079,54 @@ let rec codegen_instr fid ctx (I_aux (instr, _)) = | I_reset (ctyp, id) -> string (Printf.sprintf " RECREATE(%s)(&%s);" (sgen_ctyp_name ctyp) (sgen_id id)) - (* FIXME: This just covers the cases we see in our specs, need a - special conversion code-generator for full generality *) - | I_convert (x, CT_tup ctyps1, y, CT_tup ctyps2) when List.length ctyps1 = List.length ctyps2 -> - let convert i (ctyp1, ctyp2) = - if ctyp_equal ctyp1 ctyp2 then - string (Printf.sprintf " %s.ztup%i = %s.ztup%i;" (sgen_clexp_pure x) i (sgen_id y) i) - else if ctyp_equal ctyp1 ctyp2 then - c_error "heap tuple type conversion" - else if is_stack_ctyp ctyp1 then - string (Printf.sprintf " %s.ztup%i = CONVERT_OF(%s, %s)(%s.ztup%i);" - (sgen_clexp_pure x) - i - (sgen_ctyp_name ctyp1) - (sgen_ctyp_name ctyp2) - (sgen_id y) - i) - else - string (Printf.sprintf " CONVERT_OF(%s, %s)(%s.ztup%i, %s.ztup%i);" - (sgen_ctyp_name ctyp1) - (sgen_ctyp_name ctyp2) - (sgen_clexp x) - i - (sgen_id y) - i) - in - separate hardline (List.mapi convert (List.map2 (fun x y -> (x, y)) ctyps1 ctyps2)) - (* If we're converting from a bits type with a known compile time - length, pass it as an extra parameter to the conversion. *) - | I_convert (x, ctyp1, y, (CT_bits64 (n, _) as ctyp2)) -> - if is_stack_ctyp ctyp1 then - string (Printf.sprintf " %s = CONVERT_OF(%s, %s)(%s, %d);" - (sgen_clexp_pure x) - (sgen_ctyp_name ctyp1) - (sgen_ctyp_name ctyp2) - (sgen_id y) - n) - else - string (Printf.sprintf " CONVERT_OF(%s, %s)(%s, %s, %d);" - (sgen_ctyp_name ctyp1) - (sgen_ctyp_name ctyp2) - (sgen_clexp x) - (sgen_id y) - n) - | I_convert (x, ctyp1, y, ctyp2) -> - if is_stack_ctyp ctyp1 then - string (Printf.sprintf " %s = CONVERT_OF(%s, %s)(%s);" - (sgen_clexp_pure x) - (sgen_ctyp_name ctyp1) - (sgen_ctyp_name ctyp2) - (sgen_id y)) - else - string (Printf.sprintf " CONVERT_OF(%s, %s)(%s, %s);" - (sgen_ctyp_name ctyp1) - (sgen_ctyp_name ctyp2) - (sgen_clexp x) - (sgen_id y)) | I_return cval -> string (Printf.sprintf " return %s;" (sgen_cval cval)) + | I_throw cval -> c_error "I_throw reached code generator" + + | I_undefined ctyp -> + let rec codegen_exn_return ctyp = + match ctyp with + | CT_unit -> "UNIT", [] + | CT_bit -> "UINT64_C(0)", [] + | CT_int64 -> "INT64_C(0xdeadc0de)", [] + | CT_bits64 _ -> "UINT64_C(0xdeadc0de)", [] + | CT_bool -> "false", [] + | CT_enum (_, ctor :: _) -> sgen_id ctor, [] + | CT_tup ctyps when is_stack_ctyp ctyp -> + let gs = gensym () 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) + ^ Util.string_of_list ", " (fun x -> x) inits ^ " };"] @ prev + | CT_struct (id, ctors) when is_stack_ctyp ctyp -> + let gs = gensym () 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) + ^ Util.string_of_list ", " (fun x -> x) inits ^ " };"] @ prev + | ctyp -> c_error ("Cannot create undefined value for type: " ^ string_of_ctyp ctyp) + in + let ret, prev = codegen_exn_return ctyp in + separate_map hardline (fun str -> string (" " ^ str)) (List.rev prev) + ^^ hardline + ^^ string (Printf.sprintf " return %s;" ret) + | I_comment str -> string (" /* " ^ str ^ " */") + | I_label str -> string (str ^ ": ;") + | I_goto str -> string (Printf.sprintf " goto %s;" str) @@ -2084,17 +2138,26 @@ let rec codegen_instr fid ctx (I_aux (instr, _)) = string (" sail_match_failure(\"" ^ String.escaped (string_of_id fid) ^ "\");") let codegen_type_def ctx = function - | CTD_enum (id, ids) -> + | CTD_enum (id, ((first_id :: _) as ids)) -> let codegen_eq = let name = sgen_id id in string (Printf.sprintf "static bool eq_%s(enum %s op1, enum %s op2) { return op1 == op2; }" name name name) in + let codegen_undefined = + let name = sgen_id id in + string (Printf.sprintf "enum %s UNDEFINED(%s)(unit u) { return %s; }" name name (upper_sgen_id first_id)) + in string (Printf.sprintf "// enum %s" (string_of_id id)) ^^ hardline ^^ separate space [string "enum"; codegen_id id; lbrace; separate_map (comma ^^ space) upper_codegen_id ids; rbrace ^^ semi] ^^ twice hardline ^^ codegen_eq + ^^ twice hardline + ^^ codegen_undefined + + | CTD_enum (id, []) -> c_error ("Cannot compile empty enum " ^ string_of_id id) | CTD_struct (id, ctors) -> + let struct_ctyp = CT_struct (id, ctors) in (* Generate a set_T function for every struct T *) let codegen_set (id, ctyp) = if is_stack_ctyp ctyp then @@ -2143,12 +2206,14 @@ let codegen_type_def ctx = function rbrace ^^ semi ^^ twice hardline ^^ codegen_setter id (ctor_bindings ctors) - ^^ twice hardline - ^^ codegen_init "CREATE" id (ctor_bindings ctors) - ^^ twice hardline - ^^ codegen_init "RECREATE" id (ctor_bindings ctors) - ^^ twice hardline - ^^ codegen_init "KILL" id (ctor_bindings ctors) + ^^ (if not (is_stack_ctyp struct_ctyp) then + twice hardline + ^^ codegen_init "CREATE" id (ctor_bindings ctors) + ^^ twice hardline + ^^ codegen_init "RECREATE" id (ctor_bindings ctors) + ^^ twice hardline + ^^ codegen_init "KILL" id (ctor_bindings ctors) + else empty) ^^ twice hardline ^^ codegen_eq @@ -2209,7 +2274,10 @@ let codegen_type_def ctx = function | 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 "CREATE(%s)(&op);" (sgen_ctyp_name ctyp)) ^^ hardline + ^^ if not (is_stack_ctyp ctyp) then + string (Printf.sprintf "CREATE(%s)(&op);" (sgen_ctyp_name ctyp)) ^^ hardline + else + empty ^^ separate hardline (List.mapi tuple_set ctyps) ^^ hardline | ctyp -> Printf.sprintf "%s op" (sgen_ctyp ctyp), empty in @@ -2651,12 +2719,12 @@ let sgen_finish = function Printf.sprintf " finish_%s();" (sgen_id id) | _ -> assert false + (* let instrument_tracing ctx = let module StringSet = Set.Make(String) in let traceable = StringSet.of_list ["mach_bits"; "sail_string"; "sail_bits"; "sail_int"; "unit"; "bool"] in let rec instrument = function - | (I_aux (I_funcall (clexp, _, id, args, ctyp), _) as instr) :: instrs when not (Env.is_extern id ctx.tc_env "c") -> - + | (I_aux (I_funcall (clexp, _, id, args), _) as instr) :: instrs -> let trace_start = iraw (Printf.sprintf "trace_start(\"%s\");" (String.escaped (string_of_id id))) in @@ -2702,6 +2770,7 @@ let instrument_tracing ctx = | CDEF_fundef (function_id, heap_return, args, body) -> CDEF_fundef (function_id, heap_return, args, instrument body) | cdef -> cdef + *) let bytecode_ast ctx rewrites (Defs defs) = let assert_vs = Initial_check.extern_of_string dec_ord (mk_id "sail_assert") "(bool, string) -> unit effect {escape}" in @@ -2753,8 +2822,9 @@ let compile_ast ctx (Defs defs) = let cdefs = List.concat (List.rev chunks) in let cdefs = optimize ctx cdefs in + (* let cdefs = if !opt_trace then List.map (instrument_tracing ctx) cdefs else cdefs in - + *) let docs = List.map (codegen_def ctx) cdefs in let preamble = separate hardline |