diff options
Diffstat (limited to 'src/jib/jib_compile.ml')
| -rw-r--r-- | src/jib/jib_compile.ml | 748 |
1 files changed, 459 insertions, 289 deletions
diff --git a/src/jib/jib_compile.ml b/src/jib/jib_compile.ml index c13b814f..051f5c19 100644 --- a/src/jib/jib_compile.ml +++ b/src/jib/jib_compile.ml @@ -57,10 +57,11 @@ open Value2 open Anf -let opt_debug_function = ref "" -let opt_debug_flow_graphs = ref false let opt_memo_cache = ref false +let optimize_aarch64_fast_struct = ref false + +let (gensym, reset_gensym_counter) = symbol_generator "gs" let ngensym () = name (gensym ()) (**************************************************************************) @@ -132,7 +133,11 @@ let is_ct_ref = function | CT_ref _ -> true | _ -> false -let ctor_bindings = List.fold_left (fun map (id, ctyp) -> Bindings.add id ctyp map) Bindings.empty +let iblock1 = function + | [instr] -> instr + | instrs -> iblock instrs + +let ctor_bindings = List.fold_left (fun map (uid, ctyp) -> UBindings.add uid ctyp map) UBindings.empty (** The context type contains two type-checking environments. ctx.local_env contains the closest typechecking @@ -142,32 +147,42 @@ let ctor_bindings = List.fold_left (fun map (id, ctyp) -> Bindings.add id ctyp m in ctx.locals, so we know when their type changes due to flow typing. *) type ctx = - { records : (ctyp Bindings.t) Bindings.t; + { records : (ctyp UBindings.t) Bindings.t; enums : IdSet.t Bindings.t; - variants : (ctyp Bindings.t) Bindings.t; - tc_env : Env.t; + variants : (ctyp UBindings.t) Bindings.t; + valspecs : (ctyp list * ctyp) Bindings.t; local_env : Env.t; + tc_env : Env.t; locals : (mut * ctyp) Bindings.t; letbinds : int list; no_raw : bool; - convert_typ : ctx -> typ -> ctyp; - optimize_anf : ctx -> typ aexp -> typ aexp } -let initial_ctx ~convert_typ:convert_typ ~optimize_anf:optimize_anf env = +let initial_ctx env = { records = Bindings.empty; enums = Bindings.empty; variants = Bindings.empty; - tc_env = env; + valspecs = Bindings.empty; local_env = env; + tc_env = env; locals = Bindings.empty; letbinds = []; no_raw = false; - convert_typ = convert_typ; - optimize_anf = optimize_anf } -let ctyp_of_typ ctx typ = ctx.convert_typ ctx typ +module type Config = sig + val convert_typ : ctx -> typ -> ctyp + val optimize_anf : ctx -> typ aexp -> typ aexp + val unroll_loops : unit -> int option + val specialize_calls : bool + val ignore_64 : bool + val struct_value : bool + val use_real : bool +end + +module Make(C: Config) = struct + +let ctyp_of_typ ctx typ = C.convert_typ ctx typ let rec chunkify n xs = match Util.take n xs, Util.drop n xs with @@ -175,53 +190,66 @@ let rec chunkify n xs = | xs, ys -> xs :: chunkify n ys let rec compile_aval l ctx = function - | AV_C_fragment (frag, typ, ctyp) -> + | AV_cval (cval, typ) -> + let ctyp = cval_ctyp cval in let ctyp' = ctyp_of_typ ctx typ in if not (ctyp_equal ctyp ctyp') then - raise (Reporting.err_unreachable l __POS__ (string_of_ctyp ctyp ^ " != " ^ string_of_ctyp ctyp')); - [], (frag, ctyp_of_typ ctx typ), [] + let gs = ngensym () in + [iinit ctyp' gs cval], V_id (gs, ctyp'), [iclear ctyp' gs] + else + [], cval, [] | AV_id (id, typ) -> begin try let _, ctyp = Bindings.find id ctx.locals in - [], (F_id (name id), ctyp), [] + [], V_id (name id, ctyp), [] with | Not_found -> - [], (F_id (name id), ctyp_of_typ ctx (lvar_typ typ)), [] + [], V_id (name id, ctyp_of_typ ctx (lvar_typ typ)), [] end | AV_ref (id, typ) -> - [], (F_ref (name id), CT_ref (ctyp_of_typ ctx (lvar_typ typ))), [] + [], V_lit (VL_ref (string_of_id id), CT_ref (ctyp_of_typ ctx (lvar_typ typ))), [] | AV_lit (L_aux (L_string str, _), typ) -> - [], (F_lit (V_string (String.escaped str)), ctyp_of_typ ctx typ), [] + [], V_lit ((VL_string (String.escaped str)), ctyp_of_typ ctx typ), [] + + | AV_lit (L_aux (L_num n, _), typ) when C.ignore_64 -> + [], V_lit ((VL_int n), ctyp_of_typ ctx typ), [] | AV_lit (L_aux (L_num n, _), typ) when Big_int.less_equal (min_int 64) n && Big_int.less_equal n (max_int 64) -> let gs = ngensym () in - [iinit CT_lint gs (F_lit (V_int n), CT_fint 64)], - (F_id gs, CT_lint), + [iinit CT_lint gs (V_lit (VL_int n, CT_fint 64))], + V_id (gs, CT_lint), [iclear CT_lint gs] | AV_lit (L_aux (L_num n, _), typ) -> let gs = ngensym () in - [iinit CT_lint gs (F_lit (V_string (Big_int.to_string n)), CT_string)], - (F_id gs, CT_lint), + [iinit CT_lint gs (V_lit (VL_string (Big_int.to_string n), CT_string))], + V_id (gs, CT_lint), [iclear CT_lint gs] - | AV_lit (L_aux (L_zero, _), _) -> [], (F_lit (V_bit Sail2_values.B0), CT_bit), [] - | AV_lit (L_aux (L_one, _), _) -> [], (F_lit (V_bit Sail2_values.B1), CT_bit), [] + | AV_lit (L_aux (L_zero, _), _) -> [], V_lit (VL_bit Sail2_values.B0, CT_bit), [] + | AV_lit (L_aux (L_one, _), _) -> [], V_lit (VL_bit Sail2_values.B1, CT_bit), [] - | AV_lit (L_aux (L_true, _), _) -> [], (F_lit (V_bool true), CT_bool), [] - | AV_lit (L_aux (L_false, _), _) -> [], (F_lit (V_bool false), CT_bool), [] + | AV_lit (L_aux (L_true, _), _) -> [], V_lit (VL_bool true, CT_bool), [] + | AV_lit (L_aux (L_false, _), _) -> [], V_lit (VL_bool false, CT_bool), [] | AV_lit (L_aux (L_real str, _), _) -> - let gs = ngensym () in - [iinit CT_real gs (F_lit (V_string str), CT_string)], - (F_id gs, CT_real), - [iclear CT_real gs] + if C.use_real then + [], V_lit (VL_real str, CT_real), [] + else + let gs = ngensym () in + [iinit CT_real gs (V_lit (VL_string str, CT_string))], + V_id (gs, CT_real), + [iclear CT_real gs] - | AV_lit (L_aux (L_unit, _), _) -> [], (F_lit V_unit, CT_unit), [] + | AV_lit (L_aux (L_unit, _), _) -> [], V_lit (VL_unit, CT_unit), [] + + | AV_lit (L_aux (L_undef, _), typ) -> + let ctyp = ctyp_of_typ ctx typ in + [], V_lit (VL_undefined, ctyp), [] | AV_lit (L_aux (_, l) as lit, _) -> raise (Reporting.err_general l ("Encountered unexpected literal " ^ string_of_lit lit ^ " when converting ANF represention into IR")) @@ -236,37 +264,64 @@ let rec compile_aval l ctx = function setup @ [idecl tup_ctyp gs] @ List.mapi (fun n cval -> icopy l (CL_tuple (CL_id (gs, tup_ctyp), n)) cval) cvals, - (F_id gs, CT_tup (List.map cval_ctyp cvals)), + V_id (gs, CT_tup (List.map cval_ctyp cvals)), [iclear tup_ctyp gs] @ cleanup + | AV_record (fields, typ) when C.struct_value -> + let ctyp = ctyp_of_typ ctx typ in + let gs = ngensym () in + let compile_fields (id, aval) = + let field_setup, cval, field_cleanup = compile_aval l ctx aval in + field_setup, + ((id, []), cval), + field_cleanup + in + let field_triples = List.map compile_fields (Bindings.bindings fields) in + let setup = List.concat (List.map (fun (s, _, _) -> s) field_triples) in + let fields = List.map (fun (_, f, _) -> f) field_triples in + let cleanup = List.concat (List.map (fun (_, _, c) -> c) field_triples) in + [idecl ctyp gs], + V_struct (fields, ctyp), + [iclear ctyp gs] + | AV_record (fields, typ) -> let ctyp = ctyp_of_typ ctx typ in let gs = ngensym () in let compile_fields (id, aval) = let field_setup, cval, field_cleanup = compile_aval l ctx aval in field_setup - @ [icopy l (CL_field (CL_id (gs, ctyp), string_of_id id)) cval] + @ [icopy l (CL_field (CL_id (gs, ctyp), (id, []))) cval] @ field_cleanup in [idecl ctyp gs] @ List.concat (List.map compile_fields (Bindings.bindings fields)), - (F_id gs, ctyp), + V_id (gs, ctyp), [iclear ctyp gs] - | AV_vector ([], _) -> - raise (Reporting.err_general l "Encountered empty vector literal") + | AV_vector ([], typ) -> + let vector_ctyp = ctyp_of_typ ctx typ in + begin match ctyp_of_typ ctx typ with + | CT_fbits (0, ord) -> + [], V_lit (VL_bits ([], ord), vector_ctyp), [] + | _ -> + let gs = ngensym () in + [idecl vector_ctyp gs; + iextern (CL_id (gs, vector_ctyp)) (mk_id "internal_vector_init", []) [V_lit (VL_int Big_int.zero, CT_fint 64)]], + V_id (gs, vector_ctyp), + [iclear vector_ctyp gs] + end (* Convert a small bitvector to a uint64_t literal. *) - | AV_vector (avals, typ) when is_bitvector avals && List.length avals <= 64 -> + | AV_vector (avals, typ) when is_bitvector avals && (List.length avals <= 64 || C.ignore_64) -> begin - let bitstring = F_lit (V_bits (List.map value_of_aval_bit avals)) in + let bitstring = List.map value_of_aval_bit avals in let len = List.length avals in - match destruct_vector ctx.tc_env typ with - | Some (_, Ord_aux (Ord_inc, _), _) -> - [], (bitstring, CT_fbits (len, false)), [] - | Some (_, Ord_aux (Ord_dec, _), _) -> - [], (bitstring, CT_fbits (len, true)), [] + match destruct_bitvector ctx.tc_env typ with + | Some (_, Ord_aux (Ord_inc, _)) -> + [], V_lit (VL_bits (bitstring, false), CT_fbits (len, false)), [] + | Some (_, Ord_aux (Ord_dec, _)) -> + [], V_lit (VL_bits (bitstring, true), CT_fbits (len, true)), [] | Some _ -> raise (Reporting.err_general l "Encountered order polymorphic bitvector literal") | None -> @@ -277,20 +332,20 @@ let rec compile_aval l ctx = function variable size bitvector, converting it in 64-bit chunks. *) | AV_vector (avals, typ) when is_bitvector avals -> let len = List.length avals in - let bitstring avals = F_lit (V_bits (List.map value_of_aval_bit avals)) in + let bitstring avals = VL_bits (List.map value_of_aval_bit avals, true) in let first_chunk = bitstring (Util.take (len mod 64) avals) in let chunks = Util.drop (len mod 64) avals |> chunkify 64 |> List.map bitstring in let gs = ngensym () in - [iinit (CT_lbits true) gs (first_chunk, CT_fbits (len mod 64, true))] + [iinit (CT_lbits true) gs (V_lit (first_chunk, CT_fbits (len mod 64, true)))] @ List.map (fun chunk -> ifuncall (CL_id (gs, CT_lbits true)) - (mk_id "append_64") - [(F_id gs, CT_lbits true); (chunk, CT_fbits (64, true))]) chunks, - (F_id gs, CT_lbits true), + (mk_id "append_64", []) + [V_id (gs, CT_lbits true); V_lit (chunk, CT_fbits (64, true))]) chunks, + V_id (gs, CT_lbits true), [iclear (CT_lbits true) gs] (* If we have a bitvector value, that isn't a literal then we need to set bits individually. *) - | AV_vector (avals, Typ_aux (Typ_app (id, [_; A_aux (A_order ord, _); A_aux (A_typ (Typ_aux (Typ_id bit_id, _)), _)]), _)) - when string_of_id bit_id = "bit" && string_of_id id = "vector" && List.length avals <= 64 -> + | AV_vector (avals, Typ_aux (Typ_app (id, [_; A_aux (A_order ord, _)]), _)) + when string_of_id id = "bitvector" && List.length avals <= 64 -> let len = List.length avals in let direction = match ord with | Ord_aux (Ord_inc, _) -> false @@ -299,20 +354,21 @@ let rec compile_aval l ctx = function in let gs = ngensym () in let ctyp = CT_fbits (len, direction) in - let mask i = V_bits (Util.list_init (63 - i) (fun _ -> Sail2_values.B0) @ [Sail2_values.B1] @ Util.list_init i (fun _ -> Sail2_values.B0)) in + let mask i = VL_bits (Util.list_init (63 - i) (fun _ -> Sail2_values.B0) @ [Sail2_values.B1] @ Util.list_init i (fun _ -> Sail2_values.B0), direction) in let aval_mask i aval = let setup, cval, cleanup = compile_aval l ctx aval in match cval with - | (F_lit (V_bit Sail2_values.B0), _) -> [] - | (F_lit (V_bit Sail2_values.B1), _) -> - [icopy l (CL_id (gs, ctyp)) (F_op (F_id gs, "|", F_lit (mask i)), ctyp)] + | V_lit (VL_bit Sail2_values.B0, _) -> [] + | V_lit (VL_bit Sail2_values.B1, _) -> + [icopy l (CL_id (gs, ctyp)) (V_call (Bvor, [V_id (gs, ctyp); V_lit (mask i, ctyp)]))] | _ -> - setup @ [iif cval [icopy l (CL_id (gs, ctyp)) (F_op (F_id gs, "|", F_lit (mask i)), ctyp)] [] CT_unit] @ cleanup + (* FIXME: Make this work in C *) + setup @ [iif (V_call (Bit_to_bool, [cval])) [icopy l (CL_id (gs, ctyp)) (V_call (Bvor, [V_id (gs, ctyp); V_lit (mask i, ctyp)]))] [] CT_unit] @ cleanup in [idecl ctyp gs; - icopy l (CL_id (gs, ctyp)) (F_lit (V_bits (Util.list_init 64 (fun _ -> Sail2_values.B0))), ctyp)] + icopy l (CL_id (gs, ctyp)) (V_lit (VL_bits (Util.list_init 64 (fun _ -> Sail2_values.B0), direction), ctyp))] @ List.concat (List.mapi aval_mask (List.rev avals)), - (F_id gs, ctyp), + V_id (gs, ctyp), [] (* Compiling a vector literal that isn't a bitvector *) @@ -330,18 +386,18 @@ let rec compile_aval l ctx = function let setup, cval, cleanup = compile_aval l ctx aval in setup @ [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_fint 64); cval]] + (mk_id "internal_vector_update", []) + [V_id (gs, vector_ctyp); V_lit (VL_int (Big_int.of_int i), CT_fint 64); cval]] @ cleanup in [idecl vector_ctyp gs; - iextern (CL_id (gs, vector_ctyp)) (mk_id "internal_vector_init") [(F_lit (V_int (Big_int.of_int len)), CT_fint 64)]] + iextern (CL_id (gs, vector_ctyp)) (mk_id "internal_vector_init", []) [V_lit (VL_int (Big_int.of_int len), CT_fint 64)]] @ List.concat (List.mapi aval_set (if direction then List.rev avals else avals)), - (F_id gs, vector_ctyp), + V_id (gs, vector_ctyp), [iclear vector_ctyp gs] | AV_vector _ as aval -> - raise (Reporting.err_general l ("Have AV_vector: " ^ Pretty_print_sail.to_string (pp_aval aval) ^ " which is not a vector type")) + raise (Reporting.err_general l ("Have AVL_vector: " ^ Pretty_print_sail.to_string (pp_aval aval) ^ " which is not a vector type")) | AV_list (avals, Typ_aux (typ, _)) -> let ctyp = match typ with @@ -351,14 +407,62 @@ let rec compile_aval l ctx = function let gs = ngensym () in let mk_cons aval = let setup, cval, cleanup = compile_aval l ctx aval in - setup @ [ifuncall (CL_id (gs, CT_list ctyp)) (mk_id ("cons#" ^ string_of_ctyp ctyp)) [cval; (F_id gs, CT_list ctyp)]] @ cleanup + setup @ [ifuncall (CL_id (gs, CT_list ctyp)) (mk_id ("cons#" ^ string_of_ctyp ctyp), []) [cval; V_id (gs, CT_list ctyp)]] @ cleanup in [idecl (CT_list ctyp) gs] @ List.concat (List.map mk_cons (List.rev avals)), - (F_id gs, CT_list ctyp), + V_id (gs, CT_list ctyp), [iclear (CT_list ctyp) gs] -let compile_funcall l ctx id args typ = +let optimize_call l ctx clexp id args arg_ctyps ret_ctyp = + let call () = + let setup = ref [] in + let cleanup = ref [] in + let cast_args = + List.map2 + (fun ctyp cval -> + let have_ctyp = cval_ctyp cval in + if is_polymorphic ctyp then + V_poly (cval, have_ctyp) + else if C.specialize_calls || ctyp_equal ctyp have_ctyp then + cval + else + let gs = ngensym () in + setup := iinit ctyp gs cval :: !setup; + cleanup := iclear ctyp gs :: !cleanup; + V_id (gs, ctyp)) + arg_ctyps args + in + if C.specialize_calls || ctyp_equal (clexp_ctyp clexp) ret_ctyp then + !setup @ [ifuncall clexp id cast_args] @ !cleanup + else + let gs = ngensym () in + List.rev !setup + @ [idecl ret_ctyp gs; + ifuncall (CL_id (gs, ret_ctyp)) id cast_args; + icopy l clexp (V_id (gs, ret_ctyp)); + iclear ret_ctyp gs] + @ !cleanup + in + if not C.specialize_calls && Env.is_extern (fst id) ctx.tc_env "c" then + let extern = Env.get_extern (fst id) ctx.tc_env "c" in + begin match extern, List.map cval_ctyp args, clexp_ctyp clexp with + | "slice", [CT_fbits _; CT_lint; _], CT_fbits (n, _) -> + let start = ngensym () in + [iinit (CT_fint 64) start (List.nth args 1); + icopy l clexp (V_call (Slice n, [List.nth args 0; V_id (start, CT_fint 64)]))] + | "sail_unsigned", [CT_fbits _], CT_fint 64 -> + [icopy l clexp (V_call (Unsigned 64, [List.nth args 0]))] + | "sail_signed", [CT_fbits _], CT_fint 64 -> + [icopy l clexp (V_call (Signed 64, [List.nth args 0]))] + | "set_slice", [_; _; CT_fbits (n, _); CT_fint 64; CT_fbits (m, _)], CT_fbits (n', _) when n = n' -> + [icopy l clexp (V_call (Set_slice, [List.nth args 2; List.nth args 3; List.nth args 4]))] + | _, _, _ -> + call () + end + else call () + +let compile_funcall l ctx id args = let setup = ref [] in let cleanup = ref [] in @@ -374,38 +478,21 @@ let compile_funcall l ctx id args typ = 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 + + assert (List.length arg_ctyps = List.length args); let setup_arg ctyp aval = let arg_setup, cval, arg_cleanup = compile_aval l ctx aval in setup := List.rev arg_setup @ !setup; cleanup := arg_cleanup @ !cleanup; - let have_ctyp = cval_ctyp cval in - if is_polymorphic ctyp then - (F_poly (fst cval), have_ctyp) - else if ctyp_equal ctyp have_ctyp then - cval - else - let gs = ngensym () in - setup := iinit ctyp gs cval :: !setup; - cleanup := iclear ctyp gs :: !cleanup; - (F_id gs, ctyp) + cval in - assert (List.length arg_ctyps = List.length args); - let setup_args = List.map2 setup_arg arg_ctyps args in List.rev !setup, begin fun clexp -> - if ctyp_equal (clexp_ctyp clexp) ret_ctyp then - ifuncall clexp id setup_args - else - let gs = ngensym () in - iblock [idecl ret_ctyp gs; - ifuncall (CL_id (gs, ret_ctyp)) id setup_args; - icopy l clexp (F_id gs, ret_ctyp); - iclear ret_ctyp gs] + iblock1 (optimize_call l ctx clexp (id, []) setup_args arg_ctyps ret_ctyp) end, !cleanup @@ -420,39 +507,39 @@ let rec apat_ctyp ctx (AP_aux (apat, _, _)) = 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], + let ctyp = cval_ctyp cval in + match apat_aux with + | AP_id (pid, _) when Env.is_union_constructor pid ctx.tc_env -> + [ijump (V_ctor_kind (cval, pid, [], cval_ctyp cval)) case_label], [], ctx - | AP_global (pid, typ), (frag, ctyp) -> + | AP_global (pid, typ) -> let global_ctyp = ctyp_of_typ ctx typ in [icopy l (CL_id (name pid, global_ctyp)) cval], [], ctx - | AP_id (pid, _), (frag, ctyp) when is_ct_enum ctyp -> + | AP_id (pid, _) when is_ct_enum ctyp -> begin match Env.lookup_id pid ctx.tc_env with - | Unbound -> [idecl ctyp (name pid); icopy l (CL_id (name pid, ctyp)) (frag, ctyp)], [], ctx - | _ -> [ijump (F_op (F_id (name pid), "!=", frag), CT_bool) case_label], [], ctx + | Unbound -> [idecl ctyp (name pid); icopy l (CL_id (name pid, ctyp)) cval], [], ctx + | _ -> [ijump (V_call (Neq, [V_id (name pid, ctyp); cval])) case_label], [], ctx end - | AP_id (pid, typ), _ -> - let ctyp = cval_ctyp cval in + | AP_id (pid, typ) -> let id_ctyp = ctyp_of_typ ctx typ in let ctx = { ctx with locals = Bindings.add pid (Immutable, id_ctyp) ctx.locals } in [idecl id_ctyp (name pid); icopy l (CL_id (name pid, id_ctyp)) cval], [iclear id_ctyp (name pid)], ctx - | AP_as (apat, id, typ), _ -> + | AP_as (apat, id, typ) -> let id_ctyp = ctyp_of_typ ctx typ in let instrs, cleanup, ctx = compile_match ctx apat cval case_label in let ctx = { ctx with locals = Bindings.add id (Immutable, id_ctyp) ctx.locals } in instrs @ [idecl id_ctyp (name id); icopy l (CL_id (name id, id_ctyp)) cval], iclear id_ctyp (name id) :: cleanup, ctx - | AP_tup apats, (frag, ctyp) -> + | AP_tup apats -> begin - let get_tup n ctyp = (F_field (frag, "ztup" ^ string_of_int n), ctyp) in + let get_tup n = V_tuple_member (cval, List.length apats, n) in let fold (instrs, cleanup, n, ctx) apat ctyp = - let instrs', cleanup', ctx = compile_match ctx apat (get_tup n ctyp) case_label in + let instrs', cleanup', ctx = compile_match ctx apat (get_tup n) case_label in instrs @ instrs', cleanup' @ cleanup, n + 1, ctx in match ctyp with @@ -462,28 +549,24 @@ let rec compile_match ctx (AP_aux (apat_aux, env, l)) cval case_label = | _ -> failwith ("AP_tup with ctyp " ^ string_of_ctyp ctyp) end - | AP_app (ctor, apat, variant_typ), (frag, ctyp) -> + | AP_app (ctor, apat, variant_typ) -> 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 ctor_ctyp = UBindings.find (ctor, []) (ctor_bindings ctors) in + let pat_ctyp = apat_ctyp ctx apat in (* These should really be the same, something has gone wrong if they are not. *) if ctyp_equal ctor_ctyp (ctyp_of_typ ctx variant_typ) then raise (Reporting.err_general l (Printf.sprintf "%s is not the same type as %s" (string_of_ctyp ctor_ctyp) (string_of_ctyp (ctyp_of_typ ctx variant_typ)))) else (); - let ctor_c_id, ctor_ctyp = + let unifiers, ctor_ctyp = if is_polymorphic ctor_ctyp then - let unification = List.map ctyp_suprema (ctyp_unify ctor_ctyp (apat_ctyp ctx apat)) in - (if List.length unification > 0 then - ctor_c_id ^ "_" ^ Util.string_of_list "_" (fun ctyp -> Util.zencode_string (string_of_ctyp ctyp)) unification - else - ctor_c_id), - ctyp_suprema (apat_ctyp ctx apat) + let unifiers = List.map ctyp_suprema (ctyp_unify ctor_ctyp pat_ctyp) in + unifiers, ctyp_suprema pat_ctyp else - ctor_c_id, ctor_ctyp + [], ctor_ctyp in - let instrs, cleanup, ctx = compile_match ctx apat ((F_field (frag, Util.zencode_string ctor_c_id), ctor_ctyp)) case_label in - [ijump (F_op (F_field (frag, "kind"), "!=", F_lit (V_ctor_kind ctor_c_id)), CT_bool) case_label] + let instrs, cleanup, ctx = compile_match ctx apat (V_ctor_unwrap (ctor, cval, unifiers, ctor_ctyp)) case_label in + [ijump (V_ctor_kind (cval, ctor, unifiers, pat_ctyp)) case_label] @ instrs, cleanup, ctx @@ -491,23 +574,25 @@ let rec compile_match ctx (AP_aux (apat_aux, env, l)) cval case_label = raise (Reporting.err_general l (Printf.sprintf "Variant constructor %s : %s matching against non-variant type %s : %s" (string_of_id ctor) (string_of_typ variant_typ) - (string_of_fragment ~zencode:false frag) + (string_of_cval cval) (string_of_ctyp ctyp))) end - | AP_wild _, _ -> [], [], ctx + | AP_wild _ -> [], [], ctx - | AP_cons (hd_apat, tl_apat), (frag, CT_list ctyp) -> - 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 _, (_, _) -> - raise (Reporting.err_general l "Tried to pattern match cons on non list type") + | AP_cons (hd_apat, tl_apat) -> + begin match ctyp with + | CT_list ctyp -> + let hd_setup, hd_cleanup, ctx = compile_match ctx hd_apat (V_call (List_hd, [cval])) case_label in + let tl_setup, tl_cleanup, ctx = compile_match ctx tl_apat (V_call (List_tl, [cval])) case_label in + [ijump (V_call (Eq, [cval; V_lit (VL_empty_list, CT_list ctyp)])) case_label] @ hd_setup @ tl_setup, tl_cleanup @ hd_cleanup, ctx + | _ -> + raise (Reporting.err_general l "Tried to pattern match cons on non list type") + end - | AP_nil _, (frag, _) -> [ijump (F_op (frag, "!=", F_lit V_null), CT_bool) case_label], [], ctx + | AP_nil _ -> [ijump (V_call (Neq, [cval; V_lit (VL_empty_list, ctyp)])) case_label], [], ctx -let unit_fragment = (F_lit V_unit, CT_unit) +let unit_cval = V_lit (VL_unit, CT_unit) let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) = let ctx = { ctx with local_env = env } in @@ -517,15 +602,15 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) = let setup, call, cleanup = compile_aexp ctx binding in let letb_setup, letb_cleanup = [idecl binding_ctyp (name id); - iblock (setup @ [call (CL_id (name id, binding_ctyp))] @ cleanup)], + iblock1 (setup @ [call (CL_id (name id, binding_ctyp))] @ cleanup)], [iclear binding_ctyp (name id)] in let ctx = { ctx with locals = Bindings.add id (mut, binding_ctyp) ctx.locals } in let setup, call, cleanup = compile_aexp ctx body in letb_setup @ setup, call, cleanup @ letb_cleanup - | AE_app (id, vs, typ) -> - compile_funcall l ctx id vs typ + | AE_app (id, vs, _) -> + compile_funcall l ctx id vs | AE_val aval -> let setup, cval, cleanup = compile_aval l ctx aval in @@ -540,7 +625,7 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) = let compile_case (apat, guard, body) = let trivial_guard = match guard with | AE_aux (AE_val (AV_lit (L_aux (L_true, _), _)), _, _) - | AE_aux (AE_val (AV_C_fragment (F_lit (V_bool true), _, _)), _, _) -> true + | AE_aux (AE_val (AV_cval (V_lit (VL_bool true, CT_bool), _)), _, _) -> true | _ -> false in let case_label = label "case_" in @@ -549,11 +634,10 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) = let body_setup, body_call, body_cleanup = compile_aexp ctx body in let gs = ngensym () in let case_instrs = - destructure @ [icomment "end destructuring"] + destructure @ (if not trivial_guard then guard_setup @ [idecl CT_bool gs; guard_call (CL_id (gs, CT_bool))] @ guard_cleanup - @ [iif (F_unary ("!", F_id gs), CT_bool) (destructure_cleanup @ [igoto case_label]) [] CT_unit] - @ [icomment "end guard"] + @ [iif (V_call (Bnot, [V_id (gs, CT_bool)])) (destructure_cleanup @ [igoto case_label]) [] CT_unit] else []) @ body_setup @ [body_call (CL_id (case_return_id, ctyp))] @ body_cleanup @ destructure_cleanup @ [igoto finish_match_label] @@ -563,15 +647,13 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) = else [iblock case_instrs; ilabel case_label] in - [icomment "begin match"] - @ aval_setup @ [idecl ctyp case_return_id] + aval_setup @ [idecl ctyp case_return_id] @ List.concat (List.map compile_case cases) @ [imatch_failure ()] @ [ilabel finish_match_label], - (fun clexp -> icopy l clexp (F_id case_return_id, ctyp)), + (fun clexp -> icopy l clexp (V_id (case_return_id, ctyp))), [iclear ctyp case_return_id] @ aval_cleanup - @ [icomment "end match"] (* Compile try statement *) | AE_try (aexp, cases, typ) -> @@ -583,11 +665,11 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) = let compile_case (apat, guard, body) = let trivial_guard = match guard with | AE_aux (AE_val (AV_lit (L_aux (L_true, _), _)), _, _) - | AE_aux (AE_val (AV_C_fragment (F_lit (V_bool true), _, _)), _, _) -> true + | AE_aux (AE_val (AV_cval (V_lit (VL_bool true, CT_bool), _)), _, _) -> true | _ -> false in let try_label = label "try_" in - let exn_cval = (F_id current_exception, ctyp_of_typ ctx (mk_typ (Typ_id (mk_id "exception")))) in + let exn_cval = V_id (current_exception, ctyp_of_typ ctx (mk_typ (Typ_id (mk_id "exception")))) in let destructure, destructure_cleanup, ctx = compile_match ctx apat exn_cval try_label in let guard_setup, guard_call, guard_cleanup = compile_aexp ctx guard in let body_setup, body_call, body_cleanup = compile_aexp ctx body in @@ -596,7 +678,7 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) = destructure @ [icomment "end destructuring"] @ (if not trivial_guard then guard_setup @ [idecl CT_bool gs; guard_call (CL_id (gs, CT_bool))] @ guard_cleanup - @ [ijump (F_unary ("!", F_id gs), CT_bool) try_label] + @ [ijump (V_call (Bnot, [V_id (gs, CT_bool)])) try_label] @ [icomment "end guard"] else []) @ body_setup @ [body_call (CL_id (try_return_id, ctyp))] @ body_cleanup @ destructure_cleanup @@ -607,13 +689,13 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) = assert (ctyp_equal ctyp (ctyp_of_typ ctx typ)); [idecl ctyp try_return_id; itry_block (aexp_setup @ [aexp_call (CL_id (try_return_id, ctyp))] @ aexp_cleanup); - ijump (F_unary ("!", F_id have_exception), CT_bool) handled_exception_label] + ijump (V_call (Bnot, [V_id (have_exception, CT_bool)])) handled_exception_label] @ List.concat (List.map compile_case cases) @ [igoto fallthrough_label; ilabel handled_exception_label; - icopy l (CL_id (have_exception, CT_bool)) (F_lit (V_bool false), CT_bool); + icopy l (CL_id (have_exception, CT_bool)) (V_lit (VL_bool false, CT_bool)); ilabel fallthrough_label], - (fun clexp -> icopy l clexp (F_id try_return_id, ctyp)), + (fun clexp -> icopy l clexp (V_id (try_return_id, ctyp))), [] | AE_if (aval, then_aexp, else_aexp, if_typ) -> @@ -639,14 +721,14 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) = | 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 + | CT_struct (_, ctors) -> List.fold_left (fun m (k, v) -> UBindings.add k v m) UBindings.empty ctors | _ -> raise (Reporting.err_general l "Cannot perform record update for non-record type") in let gs = ngensym () in let compile_fields (id, aval) = let field_setup, cval, field_cleanup = compile_aval l ctx aval in field_setup - @ [icopy l (CL_field (CL_id (gs, ctyp), string_of_id id)) cval] + @ [icopy l (CL_field (CL_id (gs, ctyp), (id, []))) cval] @ field_cleanup in let setup, cval, cleanup = compile_aval l ctx aval in @@ -655,7 +737,7 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) = @ [icopy l (CL_id (gs, ctyp)) cval] @ cleanup @ List.concat (List.map compile_fields (Bindings.bindings fields)), - (fun clexp -> icopy l clexp (F_id gs, ctyp)), + (fun clexp -> icopy l clexp (V_id (gs, ctyp))), [iclear ctyp gs] | AE_short_circuit (SC_and, aval, aexp) -> @@ -666,10 +748,10 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) = @ [ idecl CT_bool gs; iif cval (right_setup @ [call (CL_id (gs, CT_bool))] @ right_cleanup) - [icopy l (CL_id (gs, CT_bool)) (F_lit (V_bool false), CT_bool)] + [icopy l (CL_id (gs, CT_bool)) (V_lit (VL_bool false, CT_bool))] CT_bool ] @ left_cleanup, - (fun clexp -> icopy l clexp (F_id gs, CT_bool)), + (fun clexp -> icopy l clexp (V_id (gs, CT_bool))), [] | AE_short_circuit (SC_or, aval, aexp) -> let left_setup, cval, left_cleanup = compile_aval l ctx aval in @@ -678,11 +760,11 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) = left_setup @ [ idecl CT_bool gs; iif cval - [icopy l (CL_id (gs, CT_bool)) (F_lit (V_bool true), CT_bool)] + [icopy l (CL_id (gs, CT_bool)) (V_lit (VL_bool true, CT_bool))] (right_setup @ [call (CL_id (gs, CT_bool))] @ right_cleanup) CT_bool ] @ left_cleanup, - (fun clexp -> icopy l clexp (F_id gs, CT_bool)), + (fun clexp -> icopy l clexp (V_id (gs, CT_bool))), [] (* This is a faster assignment rule for updating fields of a @@ -692,11 +774,11 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) = let compile_fields (field_id, aval) = let field_setup, cval, field_cleanup = compile_aval l ctx aval in field_setup - @ [icopy l (CL_field (CL_id (name id, ctyp_of_typ ctx typ), string_of_id field_id)) cval] + @ [icopy l (CL_field (CL_id (name id, ctyp_of_typ ctx typ), (field_id, []))) cval] @ field_cleanup in List.concat (List.map compile_fields (Bindings.bindings fields)), - (fun clexp -> icopy l clexp unit_fragment), + (fun clexp -> icopy l clexp unit_cval), [] | AE_assign (id, assign_typ, aexp) -> @@ -706,7 +788,16 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) = | None -> ctyp_of_typ ctx assign_typ in let setup, call, cleanup = compile_aexp ctx aexp in - setup @ [call (CL_id (name id, assign_ctyp))], (fun clexp -> icopy l clexp unit_fragment), cleanup + setup @ [call (CL_id (name id, assign_ctyp))], (fun clexp -> icopy l clexp unit_cval), cleanup + + | AE_write_ref (id, assign_typ, aexp) -> + let assign_ctyp = + match Bindings.find_opt id ctx.locals with + | Some (_, ctyp) -> ctyp + | None -> ctyp_of_typ ctx assign_typ + in + let setup, call, cleanup = compile_aexp ctx aexp in + setup @ [call (CL_addr (CL_id (name id, assign_ctyp)))], (fun clexp -> icopy l clexp unit_cval), cleanup | AE_block (aexps, aexp, _) -> let block = compile_block ctx aexps in @@ -720,7 +811,7 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) = let body_setup, body_call, body_cleanup = compile_aexp ctx body in let gs = ngensym () in let unit_gs = ngensym () in - let loop_test = (F_unary ("!", F_id gs), CT_bool) in + let loop_test = V_call (Bnot, [V_id (gs, CT_bool)]) in [idecl CT_bool gs; idecl CT_unit unit_gs] @ [ilabel loop_start_label] @ [iblock (cond_setup @@ -732,7 +823,7 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) = @ body_cleanup @ [igoto loop_start_label])] @ [ilabel loop_end_label], - (fun clexp -> icopy l clexp unit_fragment), + (fun clexp -> icopy l clexp unit_cval), [] | AE_loop (Until, cond, body) -> @@ -742,7 +833,7 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) = let body_setup, body_call, body_cleanup = compile_aexp ctx body in let gs = ngensym () in let unit_gs = ngensym () in - let loop_test = (F_id gs, CT_bool) in + let loop_test = V_id (gs, CT_bool) in [idecl CT_bool gs; idecl CT_unit unit_gs] @ [ilabel loop_start_label] @ [iblock (body_setup @@ -754,7 +845,7 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) = @ [ijump loop_test loop_end_label] @ [igoto loop_start_label])] @ [ilabel loop_end_label], - (fun clexp -> icopy l clexp unit_fragment), + (fun clexp -> icopy l clexp unit_cval), [] | AE_cast (aexp, typ) -> compile_aexp ctx aexp @@ -773,7 +864,7 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) = let gs = ngensym () in [idecl fn_return_ctyp gs; icopy l (CL_id (gs, fn_return_ctyp)) cval; - ireturn (F_id gs, fn_return_ctyp)] + ireturn (V_id (gs, fn_return_ctyp))] in return_setup @ creturn, (fun clexp -> icomment "unreachable after return"), @@ -786,11 +877,12 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) = (fun clexp -> icomment "unreachable after throw"), [] - | AE_field (aval, id, _) -> + | AE_field (aval, id, typ) -> + let aval_ctyp = ctyp_of_typ ctx typ in let setup, cval, cleanup = compile_aval l ctx aval in let ctyp = match cval_ctyp cval with | CT_struct (struct_id, fields) -> - begin match Util.assoc_compare_opt Id.compare id fields with + begin match Util.assoc_compare_opt UId.compare (id, []) fields with | Some ctyp -> ctyp | None -> raise (Reporting.err_unreachable l __POS__ @@ -799,8 +891,15 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) = | _ -> raise (Reporting.err_unreachable l __POS__ "Field access on non-struct type in ANF representation!") in + let unifiers, ctyp = + if is_polymorphic ctyp then + let unifiers = List.map ctyp_suprema (ctyp_unify ctyp aval_ctyp) in + unifiers, ctyp_suprema aval_ctyp + else + [], ctyp + in setup, - (fun clexp -> icopy l clexp (F_field (fst cval, Util.zencode_string (string_of_id id)), ctyp)), + (fun clexp -> icopy l clexp (V_field (cval, (id, unifiers)))), cleanup | AE_for (loop_var, loop_from, loop_to, loop_step, Ord_aux (ord, _), body) -> @@ -832,22 +931,30 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) = let loop_var = name loop_var in + let loop_body prefix continue = + prefix + @ [iblock ([ijump (V_call ((if is_inc then Igt else Ilt), [V_id (loop_var, CT_fint 64); V_id (to_gs, CT_fint 64)])) loop_end_label] + @ body_setup + @ [body_call (CL_id (body_gs, CT_unit))] + @ body_cleanup + @ [icopy l (CL_id (loop_var, (CT_fint 64))) + (V_call ((if is_inc then Iadd else Isub), [V_id (loop_var, CT_fint 64); V_id (step_gs, CT_fint 64)]))] + @ continue ())] + in + (* We can either generate an actual loop body for C, or unroll the body for SMT *) + let actual = loop_body [ilabel loop_start_label] (fun () -> [igoto loop_start_label]) in + let rec unroll max n = loop_body [] (fun () -> if n < max then unroll max (n + 1) else [imatch_failure ()]) in + let body = match C.unroll_loops () with Some times -> unroll times 0 | None -> actual in + variable_init from_gs from_setup from_call from_cleanup @ variable_init to_gs to_setup to_call to_cleanup @ variable_init step_gs step_setup step_call step_cleanup @ [iblock ([idecl (CT_fint 64) loop_var; - icopy l (CL_id (loop_var, (CT_fint 64))) (F_id from_gs, (CT_fint 64)); - 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, CT_unit))] - @ body_cleanup - @ [icopy l (CL_id (loop_var, (CT_fint 64))) - (F_op (F_id loop_var, (if is_inc then "+" else "-"), F_id step_gs), (CT_fint 64))] - @ [igoto loop_start_label]); - ilabel loop_end_label])], - (fun clexp -> icopy l clexp unit_fragment), + icopy l (CL_id (loop_var, (CT_fint 64))) (V_id (from_gs, CT_fint 64)); + idecl CT_unit body_gs] + @ body + @ [ilabel loop_end_label])], + (fun clexp -> icopy l clexp unit_cval), [] and compile_block ctx = function @@ -858,6 +965,10 @@ and compile_block ctx = function let gs = ngensym () in iblock (setup @ [idecl CT_unit gs; call (CL_id (gs, CT_unit))] @ cleanup) :: rest +let fast_int = function + | CT_lint when !optimize_aarch64_fast_struct -> CT_fint 64 + | ctyp -> ctyp + (** 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 generator, as it's easy to keep track of structs, tuples and unions @@ -874,9 +985,9 @@ let compile_type_def ctx (TD_aux (type_def, (l, _))) = | TD_record (id, typq, ctors, _) -> let record_ctx = { ctx with local_env = add_typquant l typq ctx.local_env } in let ctors = - List.fold_left (fun ctors (typ, id) -> Bindings.add id (ctyp_of_typ record_ctx typ) ctors) Bindings.empty ctors + List.fold_left (fun ctors (typ, id) -> UBindings.add (id, []) (fast_int (ctyp_of_typ record_ctx typ)) ctors) UBindings.empty ctors in - CTD_struct (id, Bindings.bindings ctors), + CTD_struct (id, UBindings.bindings ctors), { ctx with records = Bindings.add id ctors ctx.records } | TD_variant (id, typq, tus, _) -> @@ -885,8 +996,8 @@ let compile_type_def ctx (TD_aux (type_def, (l, _))) = let ctx = { ctx with local_env = add_typquant (id_loc id) typq ctx.local_env } in ctyp_of_typ ctx typ, id in - let ctus = List.fold_left (fun ctus (ctyp, id) -> Bindings.add id ctyp ctus) Bindings.empty (List.map compile_tu tus) in - CTD_variant (id, Bindings.bindings ctus), + let ctus = List.fold_left (fun ctus (ctyp, id) -> UBindings.add (id, []) ctyp ctus) UBindings.empty (List.map compile_tu tus) in + CTD_variant (id, UBindings.bindings ctus), { ctx with variants = Bindings.add id ctus ctx.variants } (* Will be re-written before here, see bitfield.ml *) @@ -941,12 +1052,12 @@ let fix_exception_block ?return:(return=None) ctx instrs = | before, I_aux (I_throw cval, (_, l)) :: after -> before @ [icopy l (CL_id (current_exception, cval_ctyp cval)) cval; - icopy l (CL_id (have_exception, CT_bool)) (F_lit (V_bool true), CT_bool)] + icopy l (CL_id (have_exception, CT_bool)) (V_lit (VL_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), _) as funcall) :: after -> - let effects = match Env.get_val_spec f ctx.tc_env with + let effects = match Env.get_val_spec (fst f) ctx.tc_env with | _, Typ_aux (Typ_fn (_, _, effects), _) -> effects | exception (Type_error _) -> no_effect (* nullary union constructor, so no val spec *) | _ -> assert false (* valspec must have function type *) @@ -954,7 +1065,7 @@ let fix_exception_block ?return:(return=None) ctx instrs = if has_effect effects BE_escape then before @ [funcall; - iif (F_id have_exception, CT_bool) (generate_cleanup (historic @ before) @ [igoto end_block_label]) [] CT_unit] + iif (V_id (have_exception, CT_bool)) (generate_cleanup (historic @ before) @ [igoto end_block_label]) [] CT_unit] @ rewrite_exception (historic @ before) after else before @ funcall :: rewrite_exception (historic @ before) after @@ -974,7 +1085,7 @@ let rec map_try_block f (I_aux (instr, aux)) = | I_funcall _ | I_copy _ | I_clear _ | I_throw _ | I_return _ -> instr | I_block instrs -> I_block (List.map (map_try_block f) instrs) | I_try_block instrs -> I_try_block (f (List.map (map_try_block f) instrs)) - | I_comment _ | I_label _ | I_goto _ | I_raw _ | I_jump _ | I_match_failure | I_undefined _ | I_end -> instr + | I_comment _ | I_label _ | I_goto _ | I_raw _ | I_jump _ | I_match_failure | I_undefined _ | I_end _ -> instr in I_aux (instr, aux) @@ -992,7 +1103,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 (name gs), ctyp) label in + let destructure, cleanup, _ = compile_match ctx apat (V_id (name gs, ctyp)) label in (gs, (destructure, cleanup)) let rec compile_arg_pats ctx label (P_aux (p_aux, (l, _)) as pat) ctyps = @@ -1008,7 +1119,7 @@ let rec compile_arg_pats ctx label (P_aux (p_aux, (l, _)) as pat) ctyps = let new_ids = List.map (fun ctyp -> gensym (), ctyp) ctyps in destructure @ [idecl (CT_tup ctyps) (name arg_id)] - @ List.mapi (fun i (id, ctyp) -> icopy l (CL_tuple (CL_id (name arg_id, CT_tup ctyps), i)) (F_id (name id), ctyp)) new_ids, + @ List.mapi (fun i (id, ctyp) -> icopy l (CL_tuple (CL_id (name arg_id, CT_tup ctyps), i)) (V_id (name id, ctyp))) new_ids, List.map (fun (id, _) -> id, ([], [])) new_ids, [iclear (CT_tup ctyps) (name arg_id)] @ cleanup @@ -1034,12 +1145,16 @@ let fix_early_return ret instrs = let end_function_label = label "end_function_" in let is_return_recur (I_aux (instr, _)) = match instr with - | I_return _ | I_undefined _ | I_if _ | I_block _ -> true + | I_return _ | I_undefined _ | I_if _ | I_block _ | I_try_block _ -> true | _ -> false in let rec rewrite_return historic instrs = match instr_split_at is_return_recur instrs with | instrs, [] -> instrs + | before, I_aux (I_try_block instrs, _) :: after -> + before + @ [itry_block (rewrite_return (historic @ before) instrs)] + @ rewrite_return (historic @ before) after | before, I_aux (I_block instrs, _) :: after -> before @ [iblock (rewrite_return (historic @ before) instrs)] @@ -1080,6 +1195,64 @@ let fix_early_return ret instrs = let letdef_count = ref 0 +let compile_funcl ctx id pat guard exp = + (* Find the function's type. *) + let quant, Typ_aux (fn_typ, _) = + try Env.get_val_spec id ctx.local_env with Type_error _ -> Env.get_val_spec id ctx.tc_env + in + let arg_typs, ret_typ = match fn_typ with + | Typ_fn (arg_typs, ret_typ, _) -> arg_typs, ret_typ + | _ -> assert false + in + + (* Handle the argument pattern. *) + let fundef_label = label "fundef_fail_" in + let orig_ctx = ctx in + (* The context must be updated before we call ctyp_of_typ on the argument types. *) + let ctx = { ctx with local_env = add_typquant (id_loc id) quant ctx.tc_env } in + + let arg_ctyps = List.map (ctyp_of_typ ctx) arg_typs in + let ret_ctyp = ctyp_of_typ ctx ret_typ in + + (* Compile the function arguments as patterns. *) + let arg_setup, compiled_args, arg_cleanup = compile_arg_pats ctx fundef_label pat arg_ctyps 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 arg_ctyps + in + + let guard_instrs = match guard with + | Some guard -> + let guard_aexp = C.optimize_anf ctx (no_shadow (pat_ids pat) (anf guard)) in + let guard_setup, guard_call, guard_cleanup = compile_aexp ctx guard_aexp in + let guard_label = label "guard_" in + let gs = ngensym () in + [iblock ( + [idecl CT_bool gs] + @ guard_setup + @ [guard_call (CL_id (gs, CT_bool))] + @ guard_cleanup + @ [ijump (V_id (gs, CT_bool)) guard_label; + imatch_failure (); + ilabel guard_label] + )] + | None -> [] + in + + (* Optimize and compile the expression to ANF. *) + let aexp = C.optimize_anf ctx (no_shadow (pat_ids pat) (anf exp)) in + + let setup, call, cleanup = compile_aexp ctx aexp in + let destructure, destructure_cleanup = + compiled_args |> List.map snd |> combine_destructure_cleanup |> fix_destructure fundef_label + in + + let instrs = arg_setup @ destructure @ guard_instrs @ setup @ [call (CL_id (return, ret_ctyp))] @ cleanup @ destructure_cleanup @ arg_cleanup in + let instrs = fix_early_return (CL_id (return, ret_ctyp)) instrs in + let instrs = fix_exception ~return:(Some ret_ctyp) ctx instrs in + + [CDEF_fundef (id, None, List.map fst compiled_args, instrs)], orig_ctx + (** Compile a Sail toplevel definition into an IR definition **) let rec compile_def n total ctx def = match def with @@ -1119,7 +1292,7 @@ and compile_def' n total ctx = function | DEF_reg_dec (DEC_aux (DEC_reg (_, _, typ, id), _)) -> [CDEF_reg_dec (id, ctyp_of_typ ctx typ, [])], ctx | DEF_reg_dec (DEC_aux (DEC_config (id, typ, exp), _)) -> - let aexp = ctx.optimize_anf ctx (no_shadow IdSet.empty (anf exp)) in + let aexp = C.optimize_anf ctx (no_shadow IdSet.empty (anf exp)) in let setup, call, cleanup = compile_aexp ctx aexp in let instrs = setup @ [call (CL_id (name id, ctyp_of_typ ctx typ))] @ cleanup in [CDEF_reg_dec (id, ctyp_of_typ ctx typ, instrs)], ctx @@ -1129,86 +1302,33 @@ and compile_def' n total ctx = function | DEF_spec (VS_aux (VS_val_spec (_, id, _, _), _)) -> let quant, Typ_aux (fn_typ, _) = Env.get_val_spec id ctx.tc_env in + let extern = + if Env.is_extern id ctx.tc_env "c" then + Some (Env.get_extern id ctx.tc_env "c") + else + None + in let arg_typs, ret_typ = match fn_typ with | Typ_fn (arg_typs, ret_typ, _) -> arg_typs, ret_typ | _ -> assert false in let ctx' = { ctx with local_env = add_typquant (id_loc id) quant ctx.local_env } in let arg_ctyps, ret_ctyp = List.map (ctyp_of_typ ctx') arg_typs, ctyp_of_typ ctx' ret_typ in - [CDEF_spec (id, arg_ctyps, ret_ctyp)], ctx + [CDEF_spec (id, extern, arg_ctyps, ret_ctyp)], + { ctx with valspecs = Bindings.add id (arg_ctyps, ret_ctyp) ctx.valspecs } | DEF_fundef (FD_aux (FD_function (_, _, _, [FCL_aux (FCL_Funcl (id, Pat_aux (Pat_exp (pat, exp), _)), _)]), _)) -> Util.progress "Compiling " (string_of_id id) n total; + compile_funcl ctx id pat None exp - (* Find the function's type. *) - let quant, Typ_aux (fn_typ, _) = - try Env.get_val_spec id ctx.local_env with Type_error _ -> Env.get_val_spec id ctx.tc_env - in - let arg_typs, ret_typ = match fn_typ with - | Typ_fn (arg_typs, ret_typ, _) -> arg_typs, ret_typ - | _ -> assert false - in - - (* Handle the argument pattern. *) - let fundef_label = label "fundef_fail_" in - let orig_ctx = ctx in - (* The context must be updated before we call ctyp_of_typ on the argument types. *) - let ctx = { ctx with local_env = add_typquant (id_loc id) quant ctx.tc_env } in - - let arg_ctyps = List.map (ctyp_of_typ ctx) arg_typs in - let ret_ctyp = ctyp_of_typ ctx ret_typ in - - (* Compile the function arguments as patterns. *) - let arg_setup, compiled_args, arg_cleanup = compile_arg_pats ctx fundef_label pat arg_ctyps 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 arg_ctyps - in - - (* Optimize and compile the expression to ANF. *) - let aexp = no_shadow (pat_ids pat) (anf exp) in - let aexp = ctx.optimize_anf ctx aexp in - - let setup, call, cleanup = compile_aexp ctx aexp in - let destructure, destructure_cleanup = - compiled_args |> List.map snd |> combine_destructure_cleanup |> fix_destructure fundef_label - in - - let instrs = arg_setup @ destructure @ setup @ [call (CL_id (return, ret_ctyp))] @ cleanup @ destructure_cleanup @ arg_cleanup in - let instrs = fix_early_return (CL_id (return, ret_ctyp)) instrs in - let instrs = fix_exception ~return:(Some ret_ctyp) ctx instrs in - - if Id.compare (mk_id !opt_debug_function) id = 0 then - let header = - Printf.sprintf "Sail IR for %s %s(%s) : (%s) -> %s" Util.("function" |> red |> clear) (string_of_id id) - (Util.string_of_list ", " string_of_id (List.map fst compiled_args)) - (Util.string_of_list ", " (fun ctyp -> Util.(string_of_ctyp ctyp |> yellow |> clear)) arg_ctyps) - Util.(string_of_ctyp ret_ctyp |> yellow |> clear) - in - prerr_endline (Util.header header (List.length arg_ctyps + 2)); - prerr_endline (Pretty_print_sail.to_string PPrint.(separate_map hardline pp_instr instrs)) - else (); - - if !opt_debug_flow_graphs then - begin - let instrs = Jib_optimize.(instrs |> optimize_unit |> flatten_instrs) in - let root, _, cfg = Jib_ssa.control_flow_graph instrs in - let idom = Jib_ssa.immediate_dominators cfg root in - let cfg = Jib_ssa.ssa instrs in - let out_chan = open_out (Util.zencode_string (string_of_id id) ^ ".gv") in - Jib_ssa.make_dot out_chan cfg; - close_out out_chan; - let out_chan = open_out (Util.zencode_string (string_of_id id) ^ ".dom.gv") in - Jib_ssa.make_dominators_dot out_chan idom cfg; - close_out out_chan; - end; - - [CDEF_fundef (id, None, List.map fst compiled_args, instrs)], orig_ctx + | DEF_fundef (FD_aux (FD_function (_, _, _, [FCL_aux (FCL_Funcl (id, Pat_aux (Pat_when (pat, guard, exp), _)), _)]), _)) -> + Util.progress "Compiling " (string_of_id id) n total; + compile_funcl ctx id pat (Some guard) exp | DEF_fundef (FD_aux (FD_function (_, _, _, []), (l, _))) -> raise (Reporting.err_general l "Encountered function with no clauses") - | DEF_fundef (FD_aux (FD_function (_, _, _, funcls), (l, _))) -> + | DEF_fundef (FD_aux (FD_function (_, _, _, _ :: _ :: _), (l, _))) -> raise (Reporting.err_general l "Encountered function with multiple clauses") (* All abbreviations should expanded by the typechecker, so we don't @@ -1221,12 +1341,12 @@ and compile_def' n total ctx = function | DEF_val (LB_aux (LB_val (pat, exp), _)) -> let ctyp = ctyp_of_typ ctx (typ_of_pat pat) in - let aexp = ctx.optimize_anf ctx (no_shadow IdSet.empty (anf exp)) in + let aexp = C.optimize_anf ctx (no_shadow IdSet.empty (anf exp)) in let setup, call, cleanup = compile_aexp ctx aexp in let apat = anf_pat ~global:true pat in let gs = ngensym () in 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 (V_id (gs, ctyp)) end_label in let gs_setup, gs_cleanup = [idecl ctyp gs], [iclear ctyp gs] in @@ -1259,6 +1379,7 @@ and compile_def' n total ctx = function (* Termination measures only needed for Coq, and other theorem prover output *) | DEF_measure _ -> [], ctx + | DEF_loop_measures _ -> [], ctx | DEF_internal_mutrec fundefs -> let defs = List.map (fun fdef -> DEF_fundef fdef) fundefs in @@ -1269,39 +1390,41 @@ and compile_def' n total ctx = function raise (Reporting.err_general Parse_ast.Unknown ("Could not compile:\n" ^ Pretty_print_sail.to_string (Pretty_print_sail.doc_def def))) let rec specialize_variants ctx prior = - let unifications = ref (Bindings.empty) in + let unifications = ref (UBindings.empty) in let fix_variant_ctyp var_id new_ctors = function | CT_variant (id, ctors) when Id.compare id var_id = 0 -> CT_variant (id, new_ctors) | ctyp -> ctyp in + let fix_struct_ctyp struct_id new_fields = function + | CT_struct (id, ctors) when Id.compare id struct_id = 0 -> CT_struct (id, new_fields) + | ctyp -> ctyp + in - let specialize_constructor ctx ctor_id ctyp = + (* specialize_constructor is called on all instructions when we find + a constructor in a union type that is polymorphic. It's job is to + record all uses of that constructor so we can monomorphise it. *) + let specialize_constructor ctx (ctor_id, existing_unifiers) ctyp = + assert (existing_unifiers = []); function - | I_aux (I_funcall (clexp, extern, id, [cval]), ((_, l) as aux)) as instr when Id.compare id ctor_id = 0 -> + | I_aux (I_funcall (clexp, extern, id, [cval]), ((_, l) as aux)) as instr when UId.compare id (ctor_id, []) = 0 -> (* Work out how each call to a constructor in instantiated and add that to unifications *) - let unification = List.map ctyp_suprema (ctyp_unify ctyp (cval_ctyp cval)) in - let mono_id = append_id ctor_id ("_" ^ Util.string_of_list "_" (fun ctyp -> Util.zencode_string (string_of_ctyp ctyp)) unification) in - unifications := Bindings.add mono_id (ctyp_suprema (cval_ctyp cval)) !unifications; + let unifiers = List.map ctyp_suprema (ctyp_unify ctyp (cval_ctyp cval)) in + let mono_id = (ctor_id, unifiers) in + unifications := UBindings.add mono_id (ctyp_suprema (cval_ctyp cval)) !unifications; (* We need to cast each cval to it's ctyp_suprema in order to put it in the most general constructor *) - let casts = - let cast_to_suprema (frag, ctyp) = - let suprema = ctyp_suprema ctyp in - if ctyp_equal ctyp suprema then - [], (unpoly frag, ctyp), [] - else - let gs = ngensym () in - [idecl suprema gs; - icopy l (CL_id (gs, suprema)) (unpoly frag, ctyp)], - (F_id gs, suprema), - [iclear suprema gs] - in - List.map cast_to_suprema [cval] + let setup, cval, cleanup = + let suprema = ctyp_suprema (cval_ctyp cval) in + if ctyp_equal ctyp suprema then + [], unpoly cval, [] + else + let gs = ngensym () in + [idecl suprema gs; + icopy l (CL_id (gs, suprema)) (unpoly cval)], + V_id (gs, suprema), + [iclear suprema gs] in - let setup = List.concat (List.map (fun (setup, _, _) -> setup) casts) in - let cvals = List.map (fun (_, cval, _) -> cval) casts in - let cleanup = List.concat (List.map (fun (_, _, cleanup) -> cleanup) casts) in let mk_funcall instr = if List.length setup = 0 then @@ -1310,11 +1433,29 @@ let rec specialize_variants ctx prior = iblock (setup @ [instr] @ cleanup) in - mk_funcall (I_aux (I_funcall (clexp, extern, mono_id, cvals), aux)) + mk_funcall (I_aux (I_funcall (clexp, extern, mono_id, [cval]), aux)) - | I_aux (I_funcall (clexp, extern, id, cvals), ((_, l) as aux)) as instr when Id.compare id ctor_id = 0 -> + | I_aux (I_funcall (clexp, extern, id, cvals), ((_, l) as aux)) as instr when UId.compare id (ctor_id, []) = 0 -> Reporting.unreachable l __POS__ "Multiple argument constructor found" + (* We have to be careful this is the only place where an V_ctor_kind can appear before calling specialize variants *) + | I_aux (I_jump (V_ctor_kind (_, id, unifiers, pat_ctyp), _), _) as instr when Id.compare id ctor_id = 0 -> + unifications := UBindings.add (ctor_id, unifiers) (ctyp_suprema pat_ctyp) !unifications; + instr + + | instr -> instr + in + + (* specialize_field performs the same job as specialize_constructor, + but for struct fields rather than union constructors. *) + let specialize_field ctx (field_id, existing_unifiers) ctyp = + assert (existing_unifiers = []); + function + | I_aux (I_copy (CL_field (clexp, field), cval), aux) when UId.compare (field_id, []) field = 0 -> + let unifiers = List.map ctyp_suprema (ctyp_unify ctyp (cval_ctyp cval)) in + let mono_id = (field_id, unifiers) in + unifications := UBindings.add mono_id (ctyp_suprema (cval_ctyp cval)) !unifications; + I_aux (I_copy (CL_field (clexp, mono_id), cval), aux) | instr -> instr in @@ -1323,18 +1464,19 @@ let rec specialize_variants ctx prior = let polymorphic_ctors = List.filter (fun (_, ctyp) -> is_polymorphic ctyp) ctors in let cdefs = - List.fold_left (fun cdefs (ctor_id, ctyp) -> List.map (cdef_map_instr (specialize_constructor ctx ctor_id ctyp)) cdefs) - cdefs - polymorphic_ctors + List.fold_left + (fun cdefs (ctor_id, ctyp) -> List.map (cdef_map_instr (specialize_constructor ctx ctor_id ctyp)) cdefs) + cdefs + polymorphic_ctors in let monomorphic_ctors = List.filter (fun (_, ctyp) -> not (is_polymorphic ctyp)) ctors in - let specialized_ctors = Bindings.bindings !unifications in + let specialized_ctors = UBindings.bindings !unifications in let new_ctors = monomorphic_ctors @ specialized_ctors in let ctx = { ctx with variants = Bindings.add var_id - (List.fold_left (fun m (id, ctyp) -> Bindings.add id ctyp m) !unifications monomorphic_ctors) + (List.fold_left (fun m (uid, ctyp) -> UBindings.add uid ctyp m) !unifications monomorphic_ctors) ctx.variants } in @@ -1342,11 +1484,35 @@ let rec specialize_variants ctx prior = let prior = List.map (cdef_map_ctyp (map_ctyp (fix_variant_ctyp var_id new_ctors))) prior in specialize_variants ctx (CDEF_type (CTD_variant (var_id, new_ctors)) :: prior) cdefs - | cdef :: cdefs -> + | (CDEF_type (CTD_struct (struct_id, fields)) as cdef) :: cdefs -> + let polymorphic_fields = List.filter (fun (_, ctyp) -> is_polymorphic ctyp) fields in + + let cdefs = + List.fold_left + (fun cdefs (field_id, ctyp) -> List.map (cdef_map_instr (specialize_field ctx field_id ctyp)) cdefs) + cdefs + polymorphic_fields + in + + let monomorphic_fields = List.filter (fun (_, ctyp) -> not (is_polymorphic ctyp)) fields in + let specialized_fields = UBindings.bindings !unifications in + let new_fields = monomorphic_fields @ specialized_fields in + + let ctx = { + ctx with records = Bindings.add struct_id + (List.fold_left (fun m (uid, ctyp) -> UBindings.add uid ctyp m) !unifications monomorphic_fields) + ctx.records + } in + + let cdefs = List.map (cdef_map_ctyp (map_ctyp (fix_struct_ctyp struct_id new_fields))) cdefs in + let prior = List.map (cdef_map_ctyp (map_ctyp (fix_struct_ctyp struct_id new_fields))) prior in + specialize_variants ctx (CDEF_type (CTD_struct (struct_id, new_fields)) :: prior) cdefs + + | cdef :: cdefs -> let remove_poly (I_aux (instr, aux)) = match instr with - | I_copy (clexp, (frag, ctyp)) when is_polymorphic ctyp -> - I_aux (I_copy (clexp, (frag, ctyp_suprema (clexp_ctyp clexp))), aux) + | I_copy (clexp, cval) when is_polymorphic (cval_ctyp cval) -> + I_aux (I_copy (clexp, unpoly cval), aux) | instr -> I_aux (instr, aux) in let cdef = cdef_map_instr remove_poly cdef in @@ -1396,11 +1562,6 @@ let sort_ctype_defs cdefs = ctype_defs @ cdefs let compile_ast ctx (Defs defs) = - let assert_vs = Initial_check.extern_of_string (mk_id "sail_assert") "(bool, string) -> unit effect {escape}" in - let exit_vs = Initial_check.extern_of_string (mk_id "sail_exit") "unit -> unit effect {escape}" in - - let ctx = { ctx with tc_env = snd (Type_error.check ctx.tc_env (Defs [assert_vs; exit_vs])) } in - if !opt_memo_cache then (try if Sys.is_directory "_sbuild" then @@ -1419,3 +1580,12 @@ let compile_ast ctx (Defs defs) = let cdefs, ctx = specialize_variants ctx [] cdefs in let cdefs = sort_ctype_defs cdefs in cdefs, ctx + +end + +let add_special_functions env = + let assert_vs = Initial_check.extern_of_string (mk_id "sail_assert") "(bool, string) -> unit" in + let exit_vs = Initial_check.extern_of_string (mk_id "sail_exit") "unit -> unit" in + let cons_vs = Initial_check.extern_of_string (mk_id "sail_cons") "forall ('a : Type). ('a, list('a)) -> list('a)" in + + snd (Type_error.check env (Defs [assert_vs; exit_vs; cons_vs])) |