From 992889aafb6dde8eaf3bd4fdfbcfa2efe68b386d Mon Sep 17 00:00:00 2001 From: Nicolas Chataing Date: Thu, 17 Jun 2021 19:15:40 +0200 Subject: [PATCH 01/45] Add head_shape type --- lambda/matching.ml | 4 ++-- lambda/translcore.ml | 2 +- toplevel/genprintval.ml | 3 ++- typing/datarepr.ml | 6 ++++-- typing/parmatch.ml | 6 +++--- typing/rec_check.ml | 4 ++-- typing/typecore.ml | 2 +- typing/types.ml | 26 +++++++++++++++++++++++--- typing/types.mli | 21 +++++++++++++++++++-- 9 files changed, 57 insertions(+), 17 deletions(-) diff --git a/lambda/matching.ml b/lambda/matching.ml index 0e143dd6a61d..8f2409213111 100644 --- a/lambda/matching.ml +++ b/lambda/matching.ml @@ -1777,7 +1777,7 @@ let get_expr_args_constr ~scopes head (arg, _mut) rem = | Cstr_constant _ | Cstr_block _ -> make_field_accesses Alias 0 (cstr.cstr_arity - 1) rem - | Cstr_unboxed -> (arg, Alias) :: rem + | Cstr_unboxed _ -> (arg, Alias) :: rem | Cstr_extension _ -> make_field_accesses Alias 1 cstr.cstr_arity rem let divide_constructor ~scopes ctx pm = @@ -2742,7 +2742,7 @@ let split_cases tag_lambda_list = match cstr_tag with | Cstr_constant n -> ((n, act) :: consts, nonconsts) | Cstr_block n -> (consts, (n, act) :: nonconsts) - | Cstr_unboxed -> (consts, (0, act) :: nonconsts) + | Cstr_unboxed _ -> (consts, (0, act) :: nonconsts) | Cstr_extension _ -> assert false ) in diff --git a/lambda/translcore.ml b/lambda/translcore.ml index e9a3f659ee91..84874ec65ff4 100644 --- a/lambda/translcore.ml +++ b/lambda/translcore.ml @@ -333,7 +333,7 @@ and transl_exp0 ~in_new_scope ~scopes e = end else begin match cstr.cstr_tag with Cstr_constant n -> Lconst(const_int n) - | Cstr_unboxed -> + | Cstr_unboxed _ -> (match ll with [v] -> v | _ -> assert false) | Cstr_block n -> begin try diff --git a/toplevel/genprintval.ml b/toplevel/genprintval.ml index dd8bb73049b9..15eb404977d4 100644 --- a/toplevel/genprintval.ml +++ b/toplevel/genprintval.ml @@ -388,7 +388,8 @@ module Make(O : OBJ)(EVP : EVALPATH with type valu = O.t) = struct | {type_kind = Type_variant (constr_list,rep)} -> let unbx = (rep = Variant_unboxed) in let tag = - if unbx then Cstr_unboxed + if unbx then (* XXX unboxing Cstr_unboxed [] *) + assert false else if O.is_block obj then Cstr_block(O.tag obj) else Cstr_constant(O.obj obj) in diff --git a/typing/datarepr.ml b/typing/datarepr.ml index 9d51817bc0f4..5e925ed957dd 100644 --- a/typing/datarepr.ml +++ b/typing/datarepr.ml @@ -111,7 +111,8 @@ let constructor_descrs ~current_unit ty_path decl cstrs rep = match cd_args, rep with | _, Variant_unboxed -> assert (rem = []); - (Cstr_unboxed, []) + failwith "TODO" + (* (Cstr_unboxed, []) *) | Cstr_tuple [], Variant_regular -> (Cstr_constant idx_const, describe_constructors (idx_const+1) idx_nonconst rem) @@ -218,7 +219,8 @@ let rec find_constr tag num_const num_nonconst = function then c else find_constr tag (num_const + 1) num_nonconst rem | c :: rem -> - if tag = Cstr_block num_nonconst || tag = Cstr_unboxed + if tag = Cstr_block num_nonconst (* || tag = Cstr_unboxed [] *) + (* XXX changes needed in the check above *) then c else find_constr tag num_const (num_nonconst + 1) rem diff --git a/typing/parmatch.ml b/typing/parmatch.ml index 10fc10a00921..2294dc3806ba 100644 --- a/typing/parmatch.ml +++ b/typing/parmatch.ml @@ -793,7 +793,7 @@ let should_extend ext env = match ext with | (p,_)::_ -> let open Patterns.Head in begin match p.pat_desc with - | Construct {cstr_tag=(Cstr_constant _|Cstr_block _|Cstr_unboxed)} -> + | Construct {cstr_tag=(Cstr_constant _|Cstr_block _|Cstr_unboxed _)} -> let path = get_constructor_type_path p.pat_type p.pat_env in Path.same path ext | Construct {cstr_tag=(Cstr_extension _)} -> false @@ -882,7 +882,7 @@ let build_other_constrs env p = match p.pat_desc with | Construct ({ cstr_tag = Cstr_extension _ }) -> extra_pat | Construct - ({ cstr_tag = Cstr_constant _ | Cstr_block _ | Cstr_unboxed } as c) -> + ({ cstr_tag = Cstr_constant _ | Cstr_block _ | Cstr_unboxed _ } as c) -> let constr = { p with pat_desc = c } in let get_constr q = match q.pat_desc with @@ -2004,7 +2004,7 @@ let extendable_path path = Path.same path Predef.path_option) let rec collect_paths_from_pat r p = match p.pat_desc with -| Tpat_construct(_, {cstr_tag=(Cstr_constant _|Cstr_block _|Cstr_unboxed)}, +| Tpat_construct(_, {cstr_tag=(Cstr_constant _|Cstr_block _|Cstr_unboxed _)}, ps, _) -> let path = get_constructor_type_path p.pat_type p.pat_env in List.fold_left diff --git a/typing/rec_check.ml b/typing/rec_check.ml index 75091497a378..2d0be0a1ebda 100644 --- a/typing/rec_check.ml +++ b/typing/rec_check.ml @@ -157,7 +157,7 @@ let classify_expression : Typedtree.expression -> sd = | Texp_letexception (_, e) -> classify_expression env e - | Texp_construct (_, {cstr_tag = Cstr_unboxed}, [e]) -> + | Texp_construct (_, {cstr_tag = Cstr_unboxed _}, [e]) -> classify_expression env e | Texp_construct _ -> Static @@ -606,7 +606,7 @@ let rec expression : Typedtree.expression -> term_judg = | _ -> empty in let m' = match desc.cstr_tag with - | Cstr_unboxed -> + | Cstr_unboxed _ -> Return | Cstr_constant _ | Cstr_block _ | Cstr_extension _ -> Guard diff --git a/typing/typecore.ml b/typing/typecore.ml index 7595d7dc6e93..b2b485546acd 100644 --- a/typing/typecore.ml +++ b/typing/typecore.ml @@ -4753,7 +4753,7 @@ and type_construct env loc lid sarg ty_expected_explained attrs = begin match constr.cstr_tag with | Cstr_extension _ -> raise(Error(loc, env, Private_constructor (constr, ty_res))) - | Cstr_constant _ | Cstr_block _ | Cstr_unboxed -> + | Cstr_constant _ | Cstr_block _ | Cstr_unboxed _ -> raise (Error(loc, env, Private_type ty_res)); end; (* NOTE: shouldn't we call "re" on this final expression? -- AF *) diff --git a/typing/types.ml b/typing/types.ml index 8be5bebf24cc..e42c0fb5e06c 100644 --- a/typing/types.ml +++ b/typing/types.ml @@ -417,18 +417,38 @@ type constructor_description = and constructor_tag = Cstr_constant of int (* Constant constructor (an int) *) | Cstr_block of int (* Regular constructor (a block) *) - | Cstr_unboxed (* Constructor of an unboxed type *) + | Cstr_unboxed of unboxed_data (* Constructor of an unboxed type *) | Cstr_extension of Path.t * bool (* Extension constructor true if a constant false if a block*) +and unboxed_data = + { unboxed_ty: type_expr; + unboxed_shape: head_shape option ref; + } + +and head_shape = + { head_imm : imm shape; (* set of immediates the head can be *) + head_blocks : tag shape; (* set of tags the head can have *) + } + +and 'a shape = + (* TODO add some comment *) + | Shape_set of 'a list + | Shape_any + +and imm = int +and tag = int let equal_tag t1 t2 = match (t1, t2) with | Cstr_constant i1, Cstr_constant i2 -> i2 = i1 | Cstr_block i1, Cstr_block i2 -> i2 = i1 - | Cstr_unboxed, Cstr_unboxed -> true + | Cstr_unboxed c1, Cstr_unboxed c2 -> + (* Possible tags of different unboxed constructors are disjoint, + so in particular their types must be different. *) + c1.unboxed_shape == c2.unboxed_shape | Cstr_extension (path1, b1), Cstr_extension (path2, b2) -> Path.same path1 path2 && b1 = b2 - | (Cstr_constant _|Cstr_block _|Cstr_unboxed|Cstr_extension _), _ -> false + | (Cstr_constant _|Cstr_block _|Cstr_unboxed _|Cstr_extension _), _ -> false let may_equal_constr c1 c2 = c1.cstr_arity = c2.cstr_arity diff --git a/typing/types.mli b/typing/types.mli index 6bfdae6b6bdc..890763d48590 100644 --- a/typing/types.mli +++ b/typing/types.mli @@ -592,12 +592,29 @@ type constructor_description = cstr_uid: Uid.t; } -and constructor_tag = + and constructor_tag = Cstr_constant of int (* Constant constructor (an int) *) | Cstr_block of int (* Regular constructor (a block) *) - | Cstr_unboxed (* Constructor of an unboxed type *) + | Cstr_unboxed of unboxed_data (* Constructor of an unboxed type *) | Cstr_extension of Path.t * bool (* Extension constructor true if a constant false if a block*) +and unboxed_data = + { unboxed_ty: type_expr; + unboxed_shape: head_shape option ref; + } + +and head_shape = + { head_imm : imm shape; (* set of immediates the head can be *) + head_blocks : tag shape; (* set of tags the head can have *) + } + +and 'a shape = + (* TODO add some comment *) + | Shape_set of 'a list + | Shape_any + +and imm = int +and tag = int (* Constructors are the same *) val equal_tag : constructor_tag -> constructor_tag -> bool From e98725842a4b099367637a5559b29c91622f24aa Mon Sep 17 00:00:00 2001 From: Nicolas Chataing Date: Thu, 17 Jun 2021 19:54:41 +0200 Subject: [PATCH 02/45] Adapt datarepr to generate head_shape thunks in unboxed constructors --- typing/datarepr.ml | 33 ++++++++++++++++++++++----------- 1 file changed, 22 insertions(+), 11 deletions(-) diff --git a/typing/datarepr.ml b/typing/datarepr.ml index 5e925ed957dd..0101e2fb04cd 100644 --- a/typing/datarepr.ml +++ b/typing/datarepr.ml @@ -20,6 +20,11 @@ open Asttypes open Types open Btype +type error = + | Multiple_args_unboxed_constructor of Ident.t + +exception Error of Location.t * error + (* Simplified version of Ctype.free_vars *) let free_vars ?(param=false) ty = let ret = ref TypeSet.empty in @@ -94,6 +99,7 @@ let constructor_args ~current_unit priv cd_args cd_res path rep = let constructor_descrs ~current_unit ty_path decl cstrs rep = let ty_res = newgenconstr ty_path decl.type_params in + let variant_unboxed = Builtin_attributes.has_unboxed decl.type_attributes in let num_consts = ref 0 and num_nonconsts = ref 0 in List.iter (fun {cd_args; _} -> @@ -107,18 +113,23 @@ let constructor_descrs ~current_unit ty_path decl cstrs rep = | Some ty_res' -> ty_res' | None -> ty_res in + (* A constructor is unboxed if the whole declaration has the + [@@unboxed] attr, or if it has the [@unboxed] attr *) + let cstr_is_unboxed = variant_unboxed || + Builtin_attributes.has_unboxed cd_attributes + in let (tag, descr_rem) = - match cd_args, rep with - | _, Variant_unboxed -> - assert (rem = []); - failwith "TODO" - (* (Cstr_unboxed, []) *) - | Cstr_tuple [], Variant_regular -> - (Cstr_constant idx_const, - describe_constructors (idx_const+1) idx_nonconst rem) - | _, Variant_regular -> - (Cstr_block idx_nonconst, - describe_constructors idx_const (idx_nonconst+1) rem) in + match cstr_is_unboxed, cd_args with + | true, Cstr_tuple [ty] + | true, Cstr_record [{ld_type=ty; _}] -> + (Cstr_unboxed {unboxed_ty = ty; unboxed_shape = ref None}, + describe_constructors idx_const idx_nonconst rem) + | true, _ -> + raise (Error (cd_loc, Multiple_args_unboxed_constructor cd_id)) + | false, Cstr_tuple [] -> (Cstr_constant idx_const, + describe_constructors (idx_const+1) idx_nonconst rem) + | false, _ -> (Cstr_block idx_nonconst, + describe_constructors idx_const (idx_nonconst+1) rem) in let cstr_name = Ident.name cd_id in let existentials, cstr_args, cstr_inlined = let representation = From 462656adf8afb015f9402922848d2812d3cae76f Mon Sep 17 00:00:00 2001 From: Nicolas Chataing Date: Thu, 17 Jun 2021 20:06:43 +0200 Subject: [PATCH 03/45] Add dump option for head shapes --- driver/main_args.ml | 11 +++++++++++ driver/main_args.mli | 1 + utils/clflags.ml | 1 + utils/clflags.mli | 1 + 4 files changed, 14 insertions(+) diff --git a/driver/main_args.ml b/driver/main_args.ml index 07acf216439d..70dc20219192 100644 --- a/driver/main_args.ml +++ b/driver/main_args.ml @@ -844,6 +844,10 @@ let mk_dinterval f = "-dinterval", Arg.Unit f, " (undocumented)" ;; +let mk_dheadshape f = + "-dheadshape", Arg.Unit f, " (undocumented)" +;; + let mk_dstartup f = "-dstartup", Arg.Unit f, " (undocumented)" ;; @@ -950,6 +954,7 @@ module type Core_options = sig val _dtypedtree : unit -> unit val _drawlambda : unit -> unit val _dlambda : unit -> unit + val _dheadshape : unit -> unit end @@ -1244,6 +1249,7 @@ struct mk_dparsetree F._dparsetree; mk_dtypedtree F._dtypedtree; mk_drawlambda F._drawlambda; + mk_dheadshape F._dheadshape; mk_dlambda F._dlambda; mk_dinstr F._dinstr; mk_dcamlprimc F._dcamlprimc; @@ -1310,6 +1316,7 @@ struct mk_dsource F._dsource; mk_dparsetree F._dparsetree; mk_dtypedtree F._dtypedtree; + mk_dheadshape F._dheadshape; mk_drawlambda F._drawlambda; mk_dlambda F._dlambda; mk_dinstr F._dinstr; @@ -1441,6 +1448,7 @@ struct mk_dsource F._dsource; mk_dparsetree F._dparsetree; mk_dtypedtree F._dtypedtree; + mk_dheadshape F._dheadshape; mk_drawlambda F._drawlambda; mk_dlambda F._dlambda; mk_drawclambda F._drawclambda; @@ -1551,6 +1559,7 @@ module Make_opttop_options (F : Opttop_options) = struct mk_dsource F._dsource; mk_dparsetree F._dparsetree; mk_dtypedtree F._dtypedtree; + mk_dheadshape F._dheadshape; mk_drawlambda F._drawlambda; mk_drawclambda F._drawclambda; mk_dclambda F._dclambda; @@ -1715,6 +1724,7 @@ module Default = struct let _drawlambda = set dump_rawlambda let _dsource = set dump_source let _dtypedtree = set dump_typedtree + let _dheadshape = set dump_headshape let _dunique_ids = set unique_ids let _dno_unique_ids = clear unique_ids let _dlocations = set locations @@ -1747,6 +1757,7 @@ module Default = struct let _dflambda_verbose () = set dump_flambda (); set dump_flambda_verbose () let _dinterval = set dump_interval + let _dheadshape = set dump_headshape let _dinterf = set dump_interf let _dlinear = set dump_linear let _dlive () = dump_live := true diff --git a/driver/main_args.mli b/driver/main_args.mli index 236111d33d79..aa25e20ed5f6 100644 --- a/driver/main_args.mli +++ b/driver/main_args.mli @@ -67,6 +67,7 @@ module type Core_options = sig val _dtypedtree : unit -> unit val _drawlambda : unit -> unit val _dlambda : unit -> unit + val _dheadshape : unit -> unit end diff --git a/utils/clflags.ml b/utils/clflags.ml index b9f60cb0861c..634531804ae4 100644 --- a/utils/clflags.ml +++ b/utils/clflags.ml @@ -128,6 +128,7 @@ let dump_reload = ref false (* -dreload *) let dump_scheduling = ref false (* -dscheduling *) let dump_linear = ref false (* -dlinear *) let dump_interval = ref false (* -dinterval *) +let dump_headshape = ref false (* -dheadshape *) let keep_startup_file = ref false (* -dstartup *) let dump_combine = ref false (* -dcombine *) let profile_columns : Profile.column list ref = ref [] (* -dprofile/-dtimings *) diff --git a/utils/clflags.mli b/utils/clflags.mli index 06b478d3b63c..8d26c1bf9690 100644 --- a/utils/clflags.mli +++ b/utils/clflags.mli @@ -153,6 +153,7 @@ val dump_reload : bool ref val dump_scheduling : bool ref val dump_linear : bool ref val dump_interval : bool ref +val dump_headshape : bool ref val keep_startup_file : bool ref val dump_combine : bool ref val native_code : bool ref From 50137826d18f2a2c64046ad3f95de0fbd57197ae Mon Sep 17 00:00:00 2001 From: Nicolas Chataing Date: Tue, 29 Jun 2021 16:54:33 +0200 Subject: [PATCH 04/45] Add head_shape computing algorithm --- .depend | 17 +++ lambda/matching.ml | 175 ++++++++++++++++++----- typing/btype.ml | 2 + typing/btype.mli | 2 + typing/datarepr.ml | 12 +- typing/parmatch.ml | 3 +- typing/typedecl.ml | 2 + typing/typedecl_unboxed.ml | 269 ++++++++++++++++++++++++++++++++++++ typing/typedecl_unboxed.mli | 12 ++ typing/types.ml | 1 + typing/types.mli | 1 + 11 files changed, 458 insertions(+), 38 deletions(-) diff --git a/.depend b/.depend index d7a12f33b634..f9a33cbe7940 100644 --- a/.depend +++ b/.depend @@ -558,6 +558,7 @@ typing/datarepr.cmo : \ typing/path.cmi \ parsing/location.cmi \ typing/ident.cmi \ + parsing/builtin_attributes.cmi \ typing/btype.cmi \ parsing/asttypes.cmi \ typing/datarepr.cmi @@ -566,6 +567,7 @@ typing/datarepr.cmx : \ typing/path.cmx \ parsing/location.cmx \ typing/ident.cmx \ + parsing/builtin_attributes.cmx \ typing/btype.cmx \ parsing/asttypes.cmi \ typing/datarepr.cmi @@ -1543,18 +1545,33 @@ typing/typedecl_separability.cmi : \ typing/env.cmi typing/typedecl_unboxed.cmo : \ typing/types.cmi \ + typing/printtyp.cmi \ typing/predef.cmi \ + typing/path.cmi \ + parsing/location.cmi \ + typing/ident.cmi \ typing/env.cmi \ typing/ctype.cmi \ + utils/config.cmi \ + utils/clflags.cmi \ + typing/btype.cmi \ typing/typedecl_unboxed.cmi typing/typedecl_unboxed.cmx : \ typing/types.cmx \ + typing/printtyp.cmx \ typing/predef.cmx \ + typing/path.cmx \ + parsing/location.cmx \ + typing/ident.cmx \ typing/env.cmx \ typing/ctype.cmx \ + utils/config.cmx \ + utils/clflags.cmx \ + typing/btype.cmx \ typing/typedecl_unboxed.cmi typing/typedecl_unboxed.cmi : \ typing/types.cmi \ + typing/ident.cmi \ typing/env.cmi typing/typedecl_variance.cmo : \ typing/types.cmi \ diff --git a/lambda/matching.ml b/lambda/matching.ml index 8f2409213111..a5cb8bbb2f02 100644 --- a/lambda/matching.ml +++ b/lambda/matching.ml @@ -2734,20 +2734,81 @@ let combine_constant loc arg cst partial ctx def in (lambda1, Jumps.union local_jumps total) +module Cases = struct + type t = { + consts: (int * lambda) list; + nonconsts: (int * lambda) list; + any_const: lambda option; + any_nonconst: lambda option; + } + + let empty = { + consts = []; + nonconsts = []; + any_const = None; + any_nonconst = None; + } + + let add_const tag act cases = + { cases with consts = (tag, act) :: cases.consts } + + let add_nonconst tag act cases = + { cases with nonconsts = (tag, act) :: cases.nonconsts } + + let add_any_const act cases = + { cases with any_const = + match cases.any_const with + | Some _ -> invalid_arg "Cases.add_any_const" + | None -> Some act + } + + let add_any_nonconst act cases = + { cases with any_nonconst = + match cases.any_nonconst with + | Some _ -> invalid_arg "Cases.add_any_nonconst" + | None -> Some act + } +end + let split_cases tag_lambda_list = let rec split_rec = function - | [] -> ([], []) + | [] -> Cases.empty | (cstr_tag, act) :: rem -> ( - let consts, nonconsts = split_rec rem in + let cases = split_rec rem in match cstr_tag with - | Cstr_constant n -> ((n, act) :: consts, nonconsts) - | Cstr_block n -> (consts, (n, act) :: nonconsts) - | Cstr_unboxed _ -> (consts, (0, act) :: nonconsts) + | Cstr_constant n -> Cases.add_const n act cases + | Cstr_block n -> Cases.add_nonconst n act cases + | Cstr_unboxed {unboxed_shape; _} -> + let head_shape = + match !unboxed_shape with + | None -> + invalid_arg "Matching.split_cases: missing head shape" + | Some shape -> shape + in + let cases = + match head_shape.head_imm with + | Shape_set s -> + List.fold_left + (fun cases n -> Cases.add_const n act cases) + cases s + | Shape_any -> Cases.add_any_const act cases + in + let cases = + match head_shape.head_blocks with + | Shape_set s -> + List.fold_left + (fun cases n -> Cases.add_nonconst n act cases) + cases s + | Shape_any -> Cases.add_any_nonconst act cases + in cases | Cstr_extension _ -> assert false ) in - let const, nonconst = split_rec tag_lambda_list in - (sort_int_lambda_list const, sort_int_lambda_list nonconst) + let cases = split_rec tag_lambda_list in + { cases with + consts = sort_int_lambda_list cases.consts; + nonconsts = sort_int_lambda_list cases.nonconsts; + } let split_extension_cases tag_lambda_list = let rec split_rec = function @@ -2819,48 +2880,92 @@ let combine_constructor loc arg pat_env cstr partial ctx def mk_failaction_pos partial constrs ctx def in let descr_lambda_list = fails @ descr_lambda_list in - let consts, nonconsts = - split_cases (List.map tag_lambda descr_lambda_list) in let lambda1 = match (fail_opt, same_actions descr_lambda_list) with | None, Some act -> act (* Identical actions, no failure *) | _ -> ( + let cases = split_cases (List.map tag_lambda descr_lambda_list) in match - (cstr.cstr_consts, cstr.cstr_nonconsts, consts, nonconsts) + (cstr.cstr_consts, cstr.cstr_nonconsts, cases) with - | 1, 1, [ (0, act1) ], [ (0, act2) ] -> + | 1, 1, { consts = [ (0, act1) ]; nonconsts = [ (0, act2) ] } (* Typically, match on lists, will avoid isint primitive in that case *) + | 1, 0, { consts = [ (0, act1) ]; any_nonconst = Some act2 } -> Lifthenelse (arg, act2, act1) - | n, 0, _, [] -> + | n, 0, { consts; any_const; nonconsts=[]; any_nonconst=None } -> (* The type defines constant constructors only *) - call_switcher loc fail_opt arg 0 (n - 1) consts - | n, _, _, _ -> ( - let act0 = - (* = Some act when all non-const constructors match to act *) - match (fail_opt, nonconsts) with - | Some a, [] -> Some a - | Some _, _ -> - if List.length nonconsts = cstr.cstr_nonconsts then - same_actions nonconsts + begin match any_const with + | Some act -> act + | None -> + call_switcher loc fail_opt arg 0 (n - 1) consts + end + | n, _, _ -> ( + let single_action any_case cases complete_case_count = + (* = Some act when all actions are the same, + either on constant or non-constant domain *) + match (fail_opt, any_case, cases) with + | Some a, None, [] + | _, Some a, _ -> Some a + | None, None, nonconsts -> same_actions nonconsts + | Some _, None, cases -> + (* FIXME: today cstr.cstr_{non,}consts does not count + unboxed constructors so it cannot be correctly used + to decide exhaustiveness. + + TODO: have a version of cstr_nonconsts that counts + not the number of different constructors, but the number + of possible head tags (in the non-any case); then we can + in fact compare this number to the length of the list + -- given that split_cases will expand several-tag + constructors into several list items. *) + if List.length cases = complete_case_count then + same_actions cases else None - | None, _ -> same_actions nonconsts in - match act0 with - | Some act -> - Lifthenelse - ( Lprim (Pisint, [ arg ], loc), - call_switcher loc fail_opt arg 0 (n - 1) consts, - act ) + let single_nonconst_act = + single_action + cases.any_nonconst cases.nonconsts cstr.cstr_nonconsts in + let single_const_act = + single_action + cases.any_const cases.consts cstr.cstr_consts in + let test_isint const_act nonconst_act = + Lifthenelse + ( Lprim (Pisint, [ arg ], loc), const_act, nonconst_act ) + in + (* We check specifically for single_nonconst_act, not for + single_const_act: for constant constructors we can generate + better code than a switch in some cases, but for tests on + non-constant constructors we prefer to always emit a switch, + as bytecode implements this sophisticated instruction. *) + match single_nonconst_act with + | Some nonconst_act -> + (* Note: we already checked that not all actions are + identical, so the constant-constructor actions cannot + be empty. *) + let int_actions = + match single_const_act with + | Some const_act -> const_act + | None -> + call_switcher loc fail_opt arg 0 (n - 1) cases.consts + in test_isint int_actions nonconst_act | None -> - (* Emit a switch, as bytecode implements this sophisticated - instruction *) + let fail_opt = + match fail_opt, cases.any_const with + | None, None -> None + | Some a, None + | None, Some a -> + Some a + | Some fail_act, Some a -> + Some (test_isint a fail_act) + in + (* FIXME: are the use of cstr_(non,)consts here correct? *) let sw = { sw_numconsts = cstr.cstr_consts; - sw_consts = consts; + sw_consts = cases.consts; sw_numblocks = cstr.cstr_nonconsts; - sw_blocks = nonconsts; + sw_blocks = cases.nonconsts; sw_failaction = fail_opt } in @@ -2920,7 +3025,11 @@ let combine_variant loc row arg partial ctx def (tag_lambda_list, total1, _pats) else mk_failaction_neg partial ctx def in - let consts, nonconsts = split_cases tag_lambda_list in + let Cases.{consts; nonconsts; any_const; any_nonconst} = + split_cases tag_lambda_list in + (* We assume there are no unboxed constructors for polymorphic variants *) + assert (any_const = None); + assert (any_nonconst = None); let lambda1 = match (fail, one_action) with | None, Some act -> act diff --git a/typing/btype.ml b/typing/btype.ml index 62e8195368be..a839f1ce23eb 100644 --- a/typing/btype.ml +++ b/typing/btype.ml @@ -40,6 +40,7 @@ module TypeMap = struct include TransientTypeMap let add ty = wrap_repr add ty let find ty = wrap_repr find ty + let mem ty = wrap_repr mem ty let singleton ty = wrap_repr singleton ty let fold f = TransientTypeMap.fold (wrap_type_expr f) end @@ -48,6 +49,7 @@ module TypeHash = struct include TransientTypeHash let add hash = wrap_repr (add hash) let find hash = wrap_repr (find hash) + let mem hash = wrap_repr (mem hash) let iter f = TransientTypeHash.iter (wrap_type_expr f) end module TransientTypePairs = diff --git a/typing/btype.mli b/typing/btype.mli index 08ee2f13209e..e3eafd8ac34d 100644 --- a/typing/btype.mli +++ b/typing/btype.mli @@ -34,6 +34,7 @@ module TypeMap : sig and type 'a t = 'a TransientTypeMap.t val add: type_expr -> 'a -> 'a t -> 'a t val find: type_expr -> 'a t -> 'a + val mem: type_expr -> 'a t -> bool val singleton: type_expr -> 'a -> 'a t val fold: (type_expr -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b end @@ -41,6 +42,7 @@ module TypeHash : sig include Hashtbl.S with type key = transient_expr val add: 'a t -> type_expr -> 'a -> unit val find: 'a t -> type_expr -> 'a + val mem: 'a t -> type_expr -> bool val iter: (type_expr -> 'a -> unit) -> 'a t -> unit end module TypePairs : sig diff --git a/typing/datarepr.ml b/typing/datarepr.ml index 0101e2fb04cd..ba14d906db51 100644 --- a/typing/datarepr.ml +++ b/typing/datarepr.ml @@ -100,11 +100,13 @@ let constructor_args ~current_unit priv cd_args cd_res path rep = let constructor_descrs ~current_unit ty_path decl cstrs rep = let ty_res = newgenconstr ty_path decl.type_params in let variant_unboxed = Builtin_attributes.has_unboxed decl.type_attributes in - let num_consts = ref 0 and num_nonconsts = ref 0 in + let num_consts = ref 0 and num_nonconsts = ref 0 and num_unboxed = ref 0 in List.iter - (fun {cd_args; _} -> - if cd_args = Cstr_tuple [] then incr num_consts else incr num_nonconsts) - cstrs; + (fun {cd_args; cd_attributes; _} -> + if Builtin_attributes.has_unboxed cd_attributes then incr num_unboxed + else if cd_args = Cstr_tuple [] then incr num_consts + else incr num_nonconsts; + ) cstrs; let rec describe_constructors idx_const idx_nonconst = function [] -> [] | {cd_id; cd_args; cd_res; cd_loc; cd_attributes; cd_uid} :: rem -> @@ -149,6 +151,7 @@ let constructor_descrs ~current_unit ty_path decl cstrs rep = cstr_tag = tag; cstr_consts = !num_consts; cstr_nonconsts = !num_nonconsts; + cstr_unboxed = !num_unboxed; cstr_private = decl.type_private; cstr_generalized = cd_res <> None; cstr_loc = cd_loc; @@ -178,6 +181,7 @@ let extension_descr ~current_unit path_ext ext = cstr_consts = -1; cstr_nonconsts = -1; cstr_private = ext.ext_private; + cstr_unboxed = -1; cstr_generalized = ext.ext_ret_type <> None; cstr_loc = ext.ext_loc; cstr_attributes = ext.ext_attributes; diff --git a/typing/parmatch.ml b/typing/parmatch.ml index 2294dc3806ba..bb522f3291e8 100644 --- a/typing/parmatch.ml +++ b/typing/parmatch.ml @@ -749,7 +749,8 @@ let full_match closing env = match env with match discr.pat_desc with | Any -> assert false | Construct { cstr_tag = Cstr_extension _ ; _ } -> false - | Construct c -> List.length env = c.cstr_consts + c.cstr_nonconsts + | Construct c -> + List.length env = c.cstr_consts + c.cstr_nonconsts + c.cstr_unboxed | Variant { type_row; _ } -> let fields = List.map diff --git a/typing/typedecl.ml b/typing/typedecl.ml index 7ca17507b9c7..26ae14dd0144 100644 --- a/typing/typedecl.ml +++ b/typing/typedecl.ml @@ -979,6 +979,8 @@ let transl_type_decl env rec_flag sdecl_list = let final_env = add_types_to_env decls env in (* Check re-exportation *) List.iter2 (check_abbrev final_env) sdecl_list decls; + (* Check head shape conflicts *) + List.iter (Typedecl_unboxed.Head_shape.check_typedecl final_env) decls; (* Keep original declaration *) let final_decls = List.map2 diff --git a/typing/typedecl_unboxed.ml b/typing/typedecl_unboxed.ml index 85a4273382ee..5ae3bada7aed 100644 --- a/typing/typedecl_unboxed.ml +++ b/typing/typedecl_unboxed.ml @@ -51,3 +51,272 @@ let get_unboxed_type_representation env ty = (* Do not give too much fuel: PR#7424 *) get_unboxed_type_representation env ty 100 ;; + +type primitive_type = + | Int + | Float + | String + | Bytes + | Array + | Floatarray + | Lazy + | Custom + +let match_primitive_type p = + let open Predef in + let tbl = [ + (path_int, Int); + (path_float, Float); + (path_string, String); + (path_bytes, Bytes); + (path_array, Array); + (path_floatarray, Floatarray); + (path_lazy_t, Lazy); + (path_nativeint, Custom); + (path_int32, Custom); + (path_int64, Custom); + ] in + List.find_opt (fun (p', _) -> Path.same p p') tbl |> Option.map snd + +module Head_shape = struct + + exception Conflict + + type t = head_shape + + let pp_shape ppf = function + | Shape_any -> Format.fprintf ppf "Shape_any" + | Shape_set l -> + Format.fprintf ppf "Shape_set [%a]" + (Format.pp_print_list + ~pp_sep:(fun ppf () -> Format.fprintf ppf "; ") + Format.pp_print_int) l + + let pp ppf {head_imm; head_blocks} = + Format.fprintf ppf "{head_imm = %a; head_blocks = %a}" + pp_shape head_imm + pp_shape head_blocks + + let any = { head_imm = Shape_any; head_blocks = Shape_any } + + let none = { head_imm = Shape_set []; head_blocks = Shape_set [] } + + let block_shape tags = + { head_imm = Shape_set []; head_blocks = Shape_set tags } + + let cstrs_shape ~num_consts ~num_nonconsts = + let int_list n = List.init n Fun.id in + { + head_imm = Shape_set (int_list num_consts); + head_blocks = Shape_set (int_list num_nonconsts) + } + + let disjoint_union hd1 hd2 = + let union s1 s2 = match s1, s2 with + | Shape_any, Shape_set [] | Shape_set [], Shape_any -> Shape_any + | Shape_any, _ | _, Shape_any -> raise Conflict + | Shape_set l1, Shape_set l2 -> + (* invariant : l1 and l2 are sorted *) + let rec merge l1 l2 = match l1, l2 with + | [], l | l, [] -> l + | x :: xx, y :: yy -> + if x = y then raise Conflict + else if x < y then x :: (merge xx l2) + else y :: (merge l1 yy) + in Shape_set (merge l1 l2) + in + { + head_imm = union hd1.head_imm hd2.head_imm; + head_blocks = union hd1.head_blocks hd2.head_blocks + } + + module Callstack = struct + type t = Path.t list + + module TypeMap = Btype.TypeMap + type map = t TypeMap.t + + let visit p callstack : t = + p :: callstack + + let visited p callstack = + List.exists (Path.same p) callstack + + let head (callstack_map : map) ty = + TypeMap.find ty callstack_map + + let rec extend callstack_map ty new_callstack = + if TypeMap.mem ty callstack_map then callstack_map + else + let callstack_map = TypeMap.add ty new_callstack callstack_map in + Btype.fold_type_expr (fun callstack_map ty' -> + extend callstack_map ty' new_callstack + ) callstack_map ty + + let fill ty callstack = extend TypeMap.empty ty callstack + end + + (* Useful to interactively debug 'of_type' below. *) + let _print_annotations ty callstack_map = + Format.eprintf "@[CALLSTACK(%a): @[" + Printtyp.type_expr ty; + let pp_sep ppf () = Format.fprintf ppf ",@ " in + Callstack.TypeMap.to_rev_seq callstack_map |> Seq.iter + (fun (ty, callstack) -> + Format.eprintf "@ @[%a@ [%a]@]" + Printtyp.type_expr (Types.Transient_expr.type_expr ty) + (Format.pp_print_list ~pp_sep Printtyp.path) callstack + ); + Format.eprintf "@]@]@."; + () + + let check_annotated ty callstack = + let hash = Btype.TypeHash.create 42 in + let rec loop ty = + if Btype.TypeHash.mem hash ty then () + else begin + Btype.TypeHash.add hash ty (); + assert (Btype.TypeMap.mem ty callstack); + Btype.iter_type_expr loop ty; + end + in loop ty + + let ty_of_poly ty = match get_desc ty with + | Tpoly (t, _) -> t + | _ -> ty + + let rec of_type env ty callstack_map = + check_annotated ty callstack_map; + match get_desc ty with + | Tvar _ | Tunivar _ -> any + | Tconstr (p, args, _abbrev) -> + begin match match_primitive_type p with + | Some Int -> { head_imm = Shape_any; head_blocks = Shape_set [] } + | Some Float -> block_shape [Obj.double_tag] + | Some String + | Some Bytes -> block_shape [Obj.string_tag] + | Some Array -> + block_shape + (if Config.flat_float_array then [0] + else [0; Obj.double_array_tag]) + | Some Floatarray -> block_shape [Obj.double_array_tag] + | Some Lazy -> any + (* Lazy values can 'shortcut' the lazy block, and thus have many + different tags. When Config.flat_float_array, they + cannot be floats, so we might want to refine that if there + are strong use-cases. *) + | Some Custom -> block_shape [Obj.custom_tag] + | None -> + let head_callstack = Callstack.head callstack_map ty in + if Callstack.visited p head_callstack then + let loc = + match Env.find_type p env with + | decl -> Some decl.type_loc + | exception Not_found -> None in + Location.raise_errorf ?loc + "Cyclic type expansion during [@unboxed] verification.@ \ + %a appears unboxed at the head of its own definition." + Path.print p + else match Env.find_type_descrs p env, Env.find_type p env with + | exception Not_found -> any + | descr, decl -> + of_typedescr env descr decl ~args callstack_map + (Callstack.visit p head_callstack) + end + | Ttuple _ -> block_shape [0] + | Tarrow _ | Tpackage _ | Tobject _ | Tnil | Tvariant _ -> (* XXX *) any + | Tlink _ | Tsubst _ | Tpoly _ | Tfield _ -> + assert false + + + and of_typedescr env ty_descr ty_decl ~args + callstack_map new_callstack = + let of_type_with_params ty = + (* We instantiate the formal type variables with the + type expression parameters at use site. + + We build a callstack for this new type by mapping all new + nodes, corresponding to the spine of 'ty', to the current + call stack. *) + let ty = ty_of_poly ty in + let params = ty_decl.type_params in + let ty = Ctype.apply env params ty args in + let callstack_map = + Callstack.extend callstack_map ty new_callstack in + of_type env ty callstack_map + in + match ty_descr with + | Type_abstract -> + begin match ty_decl.type_manifest with + | None -> any + | Some ty -> of_type_with_params ty + end + | Type_record (_, Record_regular) -> block_shape [0] + | Type_record (_, Record_float) -> block_shape [Obj.double_array_tag] + | Type_record (fields, Record_unboxed _) -> + begin match fields with + | [{lbl_arg = ty; _}] -> of_type_with_params ty + | _ -> assert false + end + | Type_record (_, Record_inlined _) + | Type_record (_, Record_extension _) -> assert false + | Type_open -> block_shape [0] + | Type_variant ([],_) -> none + | Type_variant ((fst_descr :: _) as cstr_descrs,_) -> + (* the head shape of boxed constructors is equivalent to the nb of + constant constructors and the nb of non constant constructors *) + let num_consts = fst_descr.cstr_consts in + let num_nonconsts = fst_descr.cstr_nonconsts in + let boxed_shape = cstrs_shape ~num_consts ~num_nonconsts in + let unboxed_shapes = List.filter_map + (fun descr -> + match descr.cstr_tag with + | Cstr_constant _ | Cstr_block _ | Cstr_extension _ -> None + | Cstr_unboxed {unboxed_ty; _}-> + Some (of_type_with_params unboxed_ty) + ) cstr_descrs + in + (* now checking that the unboxed constructors are compatible with the + base head shape of boxed constructors *) + List.fold_left disjoint_union boxed_shape unboxed_shapes + + let get env {unboxed_ty; unboxed_shape} = + match !unboxed_shape with + | Some shape -> shape + | None -> + let ty = ty_of_poly unboxed_ty in + let callstacks = Callstack.fill ty [] in + let shape = of_type env ty callstacks in + unboxed_shape := Some shape; + shape + + let fill_cache env unboxed_data = ignore (get env unboxed_data) + + let check_typedecl env (id,decl) = + let path = Path.Pident id in + match Env.find_type_descrs path env with + | exception Not_found -> failwith "XXX" + | Type_variant (cstrs, _repr) -> begin + try begin + cstrs |> List.iter (fun {cstr_tag; _} -> match cstr_tag with + | Cstr_unboxed cache -> fill_cache env cache + | _ -> () + ); + (* now check the whole shape for conflict between variants *) + let params = decl.type_params in + let ty = Btype.newgenty (Tconstr (path, params, ref Mnil)) in + let callstack_map = Callstack.fill ty [] in + let shape = of_type env ty callstack_map in + if !Clflags.dump_headshape then + Format.fprintf Format.err_formatter "SHAPE(%a) %a@." + Ident.print id + pp shape + end + with Conflict -> + if !Clflags.dump_headshape then + Format.fprintf Format.err_formatter "SHAPE(%a) CONFLICT@." + Ident.print id + end + | _ -> () + +end diff --git a/typing/typedecl_unboxed.mli b/typing/typedecl_unboxed.mli index 9afd38e87975..c025e770ebb1 100644 --- a/typing/typedecl_unboxed.mli +++ b/typing/typedecl_unboxed.mli @@ -23,3 +23,15 @@ type t = (* for typeopt.ml *) val get_unboxed_type_representation: Env.t -> type_expr -> t + +module Head_shape : sig + exception Conflict + + type t = Types.head_shape + + val check_typedecl : Env.t -> Ident.t * Types.type_declaration -> unit + + val get : Env.t -> Types.unboxed_data -> head_shape + + val fill_cache : Env.t -> Types.unboxed_data -> unit +end diff --git a/typing/types.ml b/typing/types.ml index e42c0fb5e06c..20267f45d2fe 100644 --- a/typing/types.ml +++ b/typing/types.ml @@ -406,6 +406,7 @@ type constructor_description = cstr_tag: constructor_tag; (* Tag for heap blocks *) cstr_consts: int; (* Number of constant constructors *) cstr_nonconsts: int; (* Number of non-const constructors *) + cstr_unboxed: int; (* Number of unboxed constructors *) cstr_generalized: bool; (* Constrained return type? *) cstr_private: private_flag; (* Read-only constructor? *) cstr_loc: Location.t; diff --git a/typing/types.mli b/typing/types.mli index 890763d48590..30a4721dbe8d 100644 --- a/typing/types.mli +++ b/typing/types.mli @@ -584,6 +584,7 @@ type constructor_description = cstr_tag: constructor_tag; (* Tag for heap blocks *) cstr_consts: int; (* Number of constant constructors *) cstr_nonconsts: int; (* Number of non-const constructors *) + cstr_unboxed: int; (* Number of unboxed constructors *) cstr_generalized: bool; (* Constrained return type? *) cstr_private: private_flag; (* Read-only constructor? *) cstr_loc: Location.t; From 86da52064463f949fb62cfe2f395cfa6c3f835d3 Mon Sep 17 00:00:00 2001 From: Nicolas Chataing Date: Tue, 29 Jun 2021 16:14:52 +0200 Subject: [PATCH 05/45] sw_num{non}consts fix --- .depend | 2 ++ lambda/matching.ml | 50 ++++++++++++++++++++---------- lambda/translcore.ml | 3 +- typing/datarepr.ml | 24 ++++++++++---- typing/parmatch.ml | 7 +++-- typing/typedecl.ml | 5 ++- typing/typedecl_unboxed.ml | 62 ++++++++++++++++++++++++++----------- typing/typedecl_unboxed.mli | 5 ++- typing/types.ml | 15 +++++++-- typing/types.mli | 17 +++++++--- 10 files changed, 136 insertions(+), 54 deletions(-) diff --git a/.depend b/.depend index f9a33cbe7940..34166f56b27a 100644 --- a/.depend +++ b/.depend @@ -3442,6 +3442,7 @@ lambda/matching.cmo : \ typing/types.cmi \ typing/typeopt.cmi \ typing/typedtree.cmi \ + typing/typedecl_unboxed.cmi \ lambda/switch.cmi \ typing/printpat.cmi \ lambda/printlambda.cmi \ @@ -3464,6 +3465,7 @@ lambda/matching.cmx : \ typing/types.cmx \ typing/typeopt.cmx \ typing/typedtree.cmx \ + typing/typedecl_unboxed.cmx \ lambda/switch.cmx \ typing/printpat.cmx \ lambda/printlambda.cmx \ diff --git a/lambda/matching.ml b/lambda/matching.ml index a5cb8bbb2f02..037670c0eaae 100644 --- a/lambda/matching.ml +++ b/lambda/matching.ml @@ -2770,7 +2770,7 @@ module Cases = struct } end -let split_cases tag_lambda_list = +let split_cases pat_env tag_lambda_list = let rec split_rec = function | [] -> Cases.empty | (cstr_tag, act) :: rem -> ( @@ -2778,12 +2778,9 @@ let split_cases tag_lambda_list = match cstr_tag with | Cstr_constant n -> Cases.add_const n act cases | Cstr_block n -> Cases.add_nonconst n act cases - | Cstr_unboxed {unboxed_shape; _} -> + | Cstr_unboxed cache -> let head_shape = - match !unboxed_shape with - | None -> - invalid_arg "Matching.split_cases: missing head shape" - | Some shape -> shape + Typedecl_unboxed.Head_shape.get pat_env cache in let cases = match head_shape.head_imm with @@ -2867,8 +2864,9 @@ let combine_constructor loc arg pat_env cstr partial ctx def (lambda1, Jumps.union local_jumps total1) | _ -> (* Regular concrete type *) + let vd = cstr.cstr_variants in let ncases = List.length descr_lambda_list - and nconstrs = cstr.cstr_consts + cstr.cstr_nonconsts in + and nconstrs = vd.vd_consts + vd.vd_nonconsts + vd.vd_unboxed in let sig_complete = ncases = nconstrs in let fail_opt, fails, local_jumps = if sig_complete then @@ -2884,9 +2882,10 @@ let combine_constructor loc arg pat_env cstr partial ctx def match (fail_opt, same_actions descr_lambda_list) with | None, Some act -> act (* Identical actions, no failure *) | _ -> ( - let cases = split_cases (List.map tag_lambda descr_lambda_list) in + let cases = split_cases pat_env + (List.map tag_lambda descr_lambda_list) in match - (cstr.cstr_consts, cstr.cstr_nonconsts, cases) + (vd.vd_consts, vd.vd_nonconsts, cases) with | 1, 1, { consts = [ (0, act1) ]; nonconsts = [ (0, act2) ] } (* Typically, match on lists, will avoid isint primitive in that @@ -2926,10 +2925,10 @@ let combine_constructor loc arg pat_env cstr partial ctx def in let single_nonconst_act = single_action - cases.any_nonconst cases.nonconsts cstr.cstr_nonconsts in + cases.any_nonconst cases.nonconsts vd.vd_nonconsts in let single_const_act = single_action - cases.any_const cases.consts cstr.cstr_consts in + cases.any_const cases.consts vd.vd_consts in let test_isint const_act nonconst_act = Lifthenelse ( Lprim (Pisint, [ arg ], loc), const_act, nonconst_act ) @@ -2960,11 +2959,27 @@ let combine_constructor loc arg pat_env cstr partial ctx def | Some fail_act, Some a -> Some (test_isint a fail_act) in - (* FIXME: are the use of cstr_(non,)consts here correct? *) + let numconsts, numblocks = + let bounds = match vd.vd_max_values with + | Some bounds -> bounds + | None -> + (* The values are not filled e.g in case a type is + imported from a foreign cmi interface; we need to + recompute them here *) + if vd.vd_unboxed = 0 then + Max vd.vd_consts, Max vd.vd_nonconsts + else + Typedecl_unboxed.Head_shape.max_val_of_cstr_descr + pat_env cstr + in match bounds with + | Max imm, Max tag -> imm, tag + | Unbounded, _ | _, Unbounded -> + invalid_arg "Matching.combine_constructors" + in let sw = - { sw_numconsts = cstr.cstr_consts; + { sw_numconsts = numconsts + 1; sw_consts = cases.consts; - sw_numblocks = cstr.cstr_nonconsts; + sw_numblocks = numblocks + 1; sw_blocks = cases.nonconsts; sw_failaction = fail_opt } @@ -2993,7 +3008,8 @@ let call_switcher_variant_constr loc fail arg int_lambda_list = Lprim (Pfield 0, [ arg ], loc), call_switcher loc fail (Lvar v) min_int max_int int_lambda_list ) -let combine_variant loc row arg partial ctx def (tag_lambda_list, total1, _pats) +let combine_variant loc row arg pat_env partial ctx def + (tag_lambda_list, total1, _pats) = let row = Btype.row_repr row in let num_constr = ref 0 in @@ -3026,7 +3042,7 @@ let combine_variant loc row arg partial ctx def (tag_lambda_list, total1, _pats) mk_failaction_neg partial ctx def in let Cases.{consts; nonconsts; any_const; any_nonconst} = - split_cases tag_lambda_list in + split_cases pat_env tag_lambda_list in (* We assume there are no unboxed constructors for polymorphic variants *) assert (any_const = None); assert (any_nonconst = None); @@ -3413,7 +3429,7 @@ and do_compile_matching ~scopes repr partial ctx pmh = compile_test (compile_match ~scopes repr partial) partial (divide_variant ~scopes !row) - (combine_variant ploc !row arg partial) + (combine_variant ploc !row arg ph.pat_env partial) ctx pm ) | PmVar { inside = pmh } -> diff --git a/lambda/translcore.ml b/lambda/translcore.ml index 84874ec65ff4..0541eac0f9d6 100644 --- a/lambda/translcore.ml +++ b/lambda/translcore.ml @@ -103,7 +103,8 @@ let rec trivial_pat pat = Tpat_var _ | Tpat_any -> true | Tpat_construct (_, cd, [], _) -> - not cd.cstr_generalized && cd.cstr_consts = 1 && cd.cstr_nonconsts = 0 + let vd = cd.cstr_variants in + not cd.cstr_generalized && vd.vd_consts = 1 && vd.vd_nonconsts = 0 | Tpat_tuple patl -> List.for_all trivial_pat patl | _ -> false diff --git a/typing/datarepr.ml b/typing/datarepr.ml index ba14d906db51..8af9eb93b4d3 100644 --- a/typing/datarepr.ml +++ b/typing/datarepr.ml @@ -107,6 +107,14 @@ let constructor_descrs ~current_unit ty_path decl cstrs rep = else if cd_args = Cstr_tuple [] then incr num_consts else incr num_nonconsts; ) cstrs; + let variant_data = + { + vd_consts = !num_consts; + vd_nonconsts = !num_nonconsts; + vd_unboxed = !num_unboxed; + vd_max_values = None; + } + in let rec describe_constructors idx_const idx_nonconst = function [] -> [] | {cd_id; cd_args; cd_res; cd_loc; cd_attributes; cd_uid} :: rem -> @@ -149,9 +157,7 @@ let constructor_descrs ~current_unit ty_path decl cstrs rep = cstr_args; cstr_arity = List.length cstr_args; cstr_tag = tag; - cstr_consts = !num_consts; - cstr_nonconsts = !num_nonconsts; - cstr_unboxed = !num_unboxed; + cstr_variants = variant_data; cstr_private = decl.type_private; cstr_generalized = cd_res <> None; cstr_loc = cd_loc; @@ -171,6 +177,14 @@ let extension_descr ~current_unit path_ext ext = let existentials, cstr_args, cstr_inlined = constructor_args ~current_unit ext.ext_private ext.ext_args ext.ext_ret_type path_ext (Record_extension path_ext) + in + let variant_data = + { + vd_consts = -1; + vd_nonconsts = -1; + vd_unboxed = -1; + vd_max_values = None; + } in { cstr_name = Path.last path_ext; cstr_res = ty_res; @@ -178,10 +192,8 @@ let extension_descr ~current_unit path_ext ext = cstr_args; cstr_arity = List.length cstr_args; cstr_tag = Cstr_extension(path_ext, cstr_args = []); - cstr_consts = -1; - cstr_nonconsts = -1; + cstr_variants = variant_data; cstr_private = ext.ext_private; - cstr_unboxed = -1; cstr_generalized = ext.ext_ret_type <> None; cstr_loc = ext.ext_loc; cstr_attributes = ext.ext_attributes; diff --git a/typing/parmatch.ml b/typing/parmatch.ml index bb522f3291e8..030e0d3ff02c 100644 --- a/typing/parmatch.ml +++ b/typing/parmatch.ml @@ -121,8 +121,8 @@ let all_coherent column = let coherent_heads hp1 hp2 = match hp1.pat_desc, hp2.pat_desc with | Construct c, Construct c' -> - c.cstr_consts = c'.cstr_consts - && c.cstr_nonconsts = c'.cstr_nonconsts + c.cstr_variants.vd_consts = c'.cstr_variants.vd_consts + && c.cstr_variants.vd_nonconsts = c'.cstr_variants.vd_nonconsts | Constant c1, Constant c2 -> begin match c1, c2 with | Const_char _, Const_char _ @@ -750,7 +750,8 @@ let full_match closing env = match env with | Any -> assert false | Construct { cstr_tag = Cstr_extension _ ; _ } -> false | Construct c -> - List.length env = c.cstr_consts + c.cstr_nonconsts + c.cstr_unboxed + let vd = c.cstr_variants in + List.length env = vd.vd_consts + vd.vd_nonconsts + vd.vd_unboxed | Variant { type_row; _ } -> let fields = List.map diff --git a/typing/typedecl.ml b/typing/typedecl.ml index 26ae14dd0144..ec1aa56f9896 100644 --- a/typing/typedecl.ml +++ b/typing/typedecl.ml @@ -980,7 +980,10 @@ let transl_type_decl env rec_flag sdecl_list = (* Check re-exportation *) List.iter2 (check_abbrev final_env) sdecl_list decls; (* Check head shape conflicts *) - List.iter (Typedecl_unboxed.Head_shape.check_typedecl final_env) decls; + List.iter (fun (id, decl) -> + let path = Path.Pident id in + Typedecl_unboxed.Head_shape.check_typedecl final_env (path, decl) + ) decls; (* Keep original declaration *) let final_decls = List.map2 diff --git a/typing/typedecl_unboxed.ml b/typing/typedecl_unboxed.ml index 5ae3bada7aed..6d698e96f1ed 100644 --- a/typing/typedecl_unboxed.ml +++ b/typing/typedecl_unboxed.ml @@ -97,9 +97,9 @@ module Head_shape = struct pp_shape head_imm pp_shape head_blocks - let any = { head_imm = Shape_any; head_blocks = Shape_any } + let any_shape = { head_imm = Shape_any; head_blocks = Shape_any } - let none = { head_imm = Shape_set []; head_blocks = Shape_set [] } + let empty_shape = { head_imm = Shape_set []; head_blocks = Shape_set [] } let block_shape tags = { head_imm = Shape_set []; head_blocks = Shape_set tags } @@ -186,9 +186,10 @@ module Head_shape = struct | _ -> ty let rec of_type env ty callstack_map = + (* TODO : try the Ctype.expand_head_opt version here *) check_annotated ty callstack_map; match get_desc ty with - | Tvar _ | Tunivar _ -> any + | Tvar _ | Tunivar _ -> any_shape | Tconstr (p, args, _abbrev) -> begin match match_primitive_type p with | Some Int -> { head_imm = Shape_any; head_blocks = Shape_set [] } @@ -200,7 +201,7 @@ module Head_shape = struct (if Config.flat_float_array then [0] else [0; Obj.double_array_tag]) | Some Floatarray -> block_shape [Obj.double_array_tag] - | Some Lazy -> any + | Some Lazy -> any_shape (* Lazy values can 'shortcut' the lazy block, and thus have many different tags. When Config.flat_float_array, they cannot be floats, so we might want to refine that if there @@ -218,13 +219,14 @@ module Head_shape = struct %a appears unboxed at the head of its own definition." Path.print p else match Env.find_type_descrs p env, Env.find_type p env with - | exception Not_found -> any + | exception Not_found -> any_shape | descr, decl -> of_typedescr env descr decl ~args callstack_map (Callstack.visit p head_callstack) end | Ttuple _ -> block_shape [0] - | Tarrow _ | Tpackage _ | Tobject _ | Tnil | Tvariant _ -> (* XXX *) any + | Tarrow _ | Tpackage _ | Tobject _ | Tnil | Tvariant _ -> (* XXX *) + any_shape | Tlink _ | Tsubst _ | Tpoly _ | Tfield _ -> assert false @@ -248,7 +250,7 @@ module Head_shape = struct match ty_descr with | Type_abstract -> begin match ty_decl.type_manifest with - | None -> any + | None -> any_shape | Some ty -> of_type_with_params ty end | Type_record (_, Record_regular) -> block_shape [0] @@ -259,14 +261,16 @@ module Head_shape = struct | _ -> assert false end | Type_record (_, Record_inlined _) - | Type_record (_, Record_extension _) -> assert false + | Type_record (_, Record_extension _) -> failwith "TODO" | Type_open -> block_shape [0] - | Type_variant ([],_) -> none + | Type_variant ([],_) -> empty_shape | Type_variant ((fst_descr :: _) as cstr_descrs,_) -> + (* we compute the shape of all boxed constructors, then the shapes of + each unboxed constructors *) + let num_consts = fst_descr.cstr_variants.vd_consts in + let num_nonconsts = fst_descr.cstr_variants.vd_nonconsts in (* the head shape of boxed constructors is equivalent to the nb of constant constructors and the nb of non constant constructors *) - let num_consts = fst_descr.cstr_consts in - let num_nonconsts = fst_descr.cstr_nonconsts in let boxed_shape = cstrs_shape ~num_consts ~num_nonconsts in let unboxed_shapes = List.filter_map (fun descr -> @@ -277,7 +281,7 @@ module Head_shape = struct ) cstr_descrs in (* now checking that the unboxed constructors are compatible with the - base head shape of boxed constructors *) + shape of boxed constructors *) List.fold_left disjoint_union boxed_shape unboxed_shapes let get env {unboxed_ty; unboxed_shape} = @@ -292,8 +296,7 @@ module Head_shape = struct let fill_cache env unboxed_data = ignore (get env unboxed_data) - let check_typedecl env (id,decl) = - let path = Path.Pident id in + let check ~print env (path,decl) = match Env.find_type_descrs path env with | exception Not_found -> failwith "XXX" | Type_variant (cstrs, _repr) -> begin @@ -307,16 +310,39 @@ module Head_shape = struct let ty = Btype.newgenty (Tconstr (path, params, ref Mnil)) in let callstack_map = Callstack.fill ty [] in let shape = of_type env ty callstack_map in - if !Clflags.dump_headshape then + let bound_of_shape = function + | Shape_set l -> Types.Max (List.fold_left max 0 l) + | Shape_any -> Types.Unbounded + in + match cstrs with + | [] -> () + | cstr :: _ -> begin + let vd = cstr.cstr_variants in + let imm_bound = bound_of_shape shape.head_imm in + let tag_bound = bound_of_shape shape.head_blocks in + vd.vd_max_values <- Some (imm_bound, tag_bound) + end; + if print && !Clflags.dump_headshape then Format.fprintf Format.err_formatter "SHAPE(%a) %a@." - Ident.print id + Path.print path pp shape end with Conflict -> - if !Clflags.dump_headshape then + if print && !Clflags.dump_headshape then Format.fprintf Format.err_formatter "SHAPE(%a) CONFLICT@." - Ident.print id + Path.print path end | _ -> () + let check_typedecl env (id,decl) = check ~print:true env (id,decl) + + let max_val_of_cstr_descr env cstr = + let variant_path = match get_desc cstr.cstr_res with + | Tconstr (p, _, _) -> p + | _ -> assert false (* XXX *) + in + let variant_decl = Env.find_type variant_path env in + check ~print:false env (variant_path,variant_decl); + let variant = cstr.cstr_variants in + Option.get variant.vd_max_values end diff --git a/typing/typedecl_unboxed.mli b/typing/typedecl_unboxed.mli index c025e770ebb1..375ed1d2bf02 100644 --- a/typing/typedecl_unboxed.mli +++ b/typing/typedecl_unboxed.mli @@ -29,7 +29,10 @@ module Head_shape : sig type t = Types.head_shape - val check_typedecl : Env.t -> Ident.t * Types.type_declaration -> unit + val check_typedecl : Env.t -> Path.t * Types.type_declaration -> unit + + val max_val_of_cstr_descr : Env.t -> constructor_description -> + int bound * int bound val get : Env.t -> Types.unboxed_data -> head_shape diff --git a/typing/types.ml b/typing/types.ml index 20267f45d2fe..6b463c72d4a1 100644 --- a/typing/types.ml +++ b/typing/types.ml @@ -404,9 +404,7 @@ type constructor_description = cstr_args: type_expr list; (* Type of the arguments *) cstr_arity: int; (* Number of arguments *) cstr_tag: constructor_tag; (* Tag for heap blocks *) - cstr_consts: int; (* Number of constant constructors *) - cstr_nonconsts: int; (* Number of non-const constructors *) - cstr_unboxed: int; (* Number of unboxed constructors *) + cstr_variants: variant_data; (* Datatype-related information *) cstr_generalized: bool; (* Constrained return type? *) cstr_private: private_flag; (* Read-only constructor? *) cstr_loc: Location.t; @@ -415,6 +413,17 @@ type constructor_description = cstr_uid: Uid.t; } +and variant_data = + { vd_consts: int; (* Number of constant constructors *) + vd_nonconsts: int; (* Number of non-const constructors *) + vd_unboxed: int; (* Number of unboxed constructors *) + mutable vd_max_values: (int bound * int bound) option; + (* Maximum immediate value and block tags taking into account unboxed + constructors (only available after head-shape analysis) *) + } + +and 'a bound = Unbounded | Max of 'a + and constructor_tag = Cstr_constant of int (* Constant constructor (an int) *) | Cstr_block of int (* Regular constructor (a block) *) diff --git a/typing/types.mli b/typing/types.mli index 30a4721dbe8d..ac084740fa8a 100644 --- a/typing/types.mli +++ b/typing/types.mli @@ -582,9 +582,7 @@ type constructor_description = cstr_args: type_expr list; (* Type of the arguments *) cstr_arity: int; (* Number of arguments *) cstr_tag: constructor_tag; (* Tag for heap blocks *) - cstr_consts: int; (* Number of constant constructors *) - cstr_nonconsts: int; (* Number of non-const constructors *) - cstr_unboxed: int; (* Number of unboxed constructors *) + cstr_variants: variant_data; (* Datatype-related information *) cstr_generalized: bool; (* Constrained return type? *) cstr_private: private_flag; (* Read-only constructor? *) cstr_loc: Location.t; @@ -593,7 +591,18 @@ type constructor_description = cstr_uid: Uid.t; } - and constructor_tag = + and variant_data = + { vd_consts: int; (* Number of constant constructors *) + vd_nonconsts: int; (* Number of non-const constructors *) + vd_unboxed: int; (* Number of unboxed constructors *) + mutable vd_max_values: (int bound * int bound) option; + (* Maximum immediate value and block tags taking into account unboxed + constructors (only available after head-shape analysis) *) + } + +and 'a bound = Unbounded | Max of 'a + +and constructor_tag = Cstr_constant of int (* Constant constructor (an int) *) | Cstr_block of int (* Regular constructor (a block) *) | Cstr_unboxed of unboxed_data (* Constructor of an unboxed type *) From 7841d3062df112ab9b5b5305ed86006733bfbfd4 Mon Sep 17 00:00:00 2001 From: Nicolas Chataing Date: Tue, 22 Jun 2021 14:16:39 +0200 Subject: [PATCH 06/45] Add tests --- .../test_unboxed_constr.ml | 68 +++++++++++++++++++ .../test_unboxed_constr_matching.ml | 28 ++++++++ 2 files changed, 96 insertions(+) create mode 100644 testsuite/tests/typing-unboxed-types/test_unboxed_constr.ml create mode 100644 testsuite/tests/typing-unboxed-types/test_unboxed_constr_matching.ml diff --git a/testsuite/tests/typing-unboxed-types/test_unboxed_constr.ml b/testsuite/tests/typing-unboxed-types/test_unboxed_constr.ml new file mode 100644 index 000000000000..13ac27641949 --- /dev/null +++ b/testsuite/tests/typing-unboxed-types/test_unboxed_constr.ml @@ -0,0 +1,68 @@ +(* TEST + flags = "-dheadshape" + * expect +*) + +(* Check the unboxing of constructors *) +type t = A of int | B;; +[%%expect{| +SHAPE(t/88[1]) {head_imm = Shape_set [0]; head_blocks = Shape_set [0]} +type t = A of int | B +|}];; + +type t = A of int | B of float | C | D;; +[%%expect{| +SHAPE(t/91[2]) {head_imm = Shape_set [0; 1]; head_blocks = Shape_set [0; 1]} +type t = A of int | B of float | C | D +|}];; + +type t = A of int [@unboxed] | B;; +[%%expect{| +SHAPE(t/96[3]) CONFLICT +type t = A of int | B +|}];; + +type t = A of float [@unboxed] | B;; +[%%expect{| +SHAPE(t/99[4]) {head_imm = Shape_set [0]; head_blocks = Shape_set [253]} +type t = A of float | B +|}];; + +type t = A of float [@unboxed] | B of string [@unboxed] | C | D of int;; +[%%expect{| +SHAPE(t/102[5]) {head_imm = Shape_set [0]; head_blocks = Shape_set [0; 252; 253]} +type t = A of float | B of string | C | D of int +|}];; + +type t = K of int u u [@unboxed] +and 'a u = 'a id +and 'a id = Id of 'a [@unboxed];; +[%%expect{| +SHAPE(t/107[6]) {head_imm = Shape_any; head_blocks = Shape_set []} +SHAPE(id/109[6]) {head_imm = Shape_any; head_blocks = Shape_any} +type t = K of int u u +and 'a u = 'a id +and 'a id = Id of 'a +|}];; + +type t = { a : int } [@@unboxed] +and tt = A of t [@unboxed];; +[%%expect{| +SHAPE(tt/113[7]) {head_imm = Shape_any; head_blocks = Shape_set []} +type t = { a : int; } [@@unboxed] +and tt = A of t +|}];; + +type t = A of { a : int } [@unboxed];; +[%%expect{| +SHAPE(t/116[8]) {head_imm = Shape_any; head_blocks = Shape_set []} +type t = A of { a : int; } +|}];; + +type ('a, 'r) u = 'r +and 'a t = A of { body : 'r. ('a, 'r) u } [@unboxed];; +[%%expect{| +SHAPE(t/120[9]) {head_imm = Shape_any; head_blocks = Shape_any} +type ('a, 'r) u = 'r +and 'a t = A of { body : 'r. ('a, 'r) u; } +|}];; diff --git a/testsuite/tests/typing-unboxed-types/test_unboxed_constr_matching.ml b/testsuite/tests/typing-unboxed-types/test_unboxed_constr_matching.ml new file mode 100644 index 000000000000..3dbbc8e8b793 --- /dev/null +++ b/testsuite/tests/typing-unboxed-types/test_unboxed_constr_matching.ml @@ -0,0 +1,28 @@ +(* TEST +*) + +module A = struct + type t = A of int | B of float [@unboxed] + + let f = function A _ -> 0 | B _ -> 1 + + let test () = + assert (f (A 0) = 0); + assert (f (B 0.) = 1) +end + +let () = A.test () + +module B = struct + type t = A of int | B of float + type tt = A' of t [@unboxed] | B' + + let f = function A' _ -> 0 | B' -> 1 + + let test () = + assert (f (A' (A 0)) = 0); + assert (f (A' (B 0.)) = 0); + assert (f B' = 1) +end + +let () = B.test () From 6f61925bd22c022fabef5459af5036df60ecc65e Mon Sep 17 00:00:00 2001 From: collaprog Date: Wed, 30 Jun 2021 11:29:51 +0200 Subject: [PATCH 07/45] WIP: restrict matching test to ocamlc.byte-only --- .../typing-unboxed-types/test_unboxed_constr_matching.ml | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/testsuite/tests/typing-unboxed-types/test_unboxed_constr_matching.ml b/testsuite/tests/typing-unboxed-types/test_unboxed_constr_matching.ml index 3dbbc8e8b793..a03c363d785d 100644 --- a/testsuite/tests/typing-unboxed-types/test_unboxed_constr_matching.ml +++ b/testsuite/tests/typing-unboxed-types/test_unboxed_constr_matching.ml @@ -1,4 +1,9 @@ (* TEST + * setup-ocamlc.byte-build-env + ** ocamlc.byte + *** check-ocamlc.byte-output + **** run + ***** check-program-output *) module A = struct From c79987f8e1b8f5944e06ca8237bdb0f64afd5c6a Mon Sep 17 00:00:00 2001 From: Nicolas Chataing Date: Fri, 9 Jul 2021 10:49:13 +0200 Subject: [PATCH 08/45] Variant data refactoring --- .depend | 6 +- lambda/matching.ml | 68 ++++++++----------- lambda/translcore.ml | 3 +- testsuite/tests/typing-unboxed-types/test.ml | 31 +++++++-- .../test_unboxed_constr_matching.ml | 6 ++ typing/datarepr.ml | 27 +++----- typing/parmatch.ml | 7 +- typing/typedecl.ml | 25 +++++++ typing/typedecl.mli | 8 +++ typing/typedecl_unboxed.ml | 47 +++++++------ typing/typedecl_unboxed.mli | 8 ++- typing/types.ml | 28 ++++---- typing/types.mli | 24 +++---- 13 files changed, 165 insertions(+), 123 deletions(-) diff --git a/.depend b/.depend index 34166f56b27a..cb5514d3361d 100644 --- a/.depend +++ b/.depend @@ -1549,7 +1549,6 @@ typing/typedecl_unboxed.cmo : \ typing/predef.cmi \ typing/path.cmi \ parsing/location.cmi \ - typing/ident.cmi \ typing/env.cmi \ typing/ctype.cmi \ utils/config.cmi \ @@ -1562,7 +1561,6 @@ typing/typedecl_unboxed.cmx : \ typing/predef.cmx \ typing/path.cmx \ parsing/location.cmx \ - typing/ident.cmx \ typing/env.cmx \ typing/ctype.cmx \ utils/config.cmx \ @@ -1571,7 +1569,7 @@ typing/typedecl_unboxed.cmx : \ typing/typedecl_unboxed.cmi typing/typedecl_unboxed.cmi : \ typing/types.cmi \ - typing/ident.cmi \ + typing/path.cmi \ typing/env.cmi typing/typedecl_variance.cmo : \ typing/types.cmi \ @@ -3443,6 +3441,7 @@ lambda/matching.cmo : \ typing/typeopt.cmi \ typing/typedtree.cmi \ typing/typedecl_unboxed.cmi \ + typing/typedecl.cmi \ lambda/switch.cmi \ typing/printpat.cmi \ lambda/printlambda.cmi \ @@ -3466,6 +3465,7 @@ lambda/matching.cmx : \ typing/typeopt.cmx \ typing/typedtree.cmx \ typing/typedecl_unboxed.cmx \ + typing/typedecl.cmx \ lambda/switch.cmx \ typing/printpat.cmx \ lambda/printlambda.cmx \ diff --git a/lambda/matching.ml b/lambda/matching.ml index 037670c0eaae..729c0c5e8793 100644 --- a/lambda/matching.ml +++ b/lambda/matching.ml @@ -2864,9 +2864,9 @@ let combine_constructor loc arg pat_env cstr partial ctx def (lambda1, Jumps.union local_jumps total1) | _ -> (* Regular concrete type *) - let vd = cstr.cstr_variants in let ncases = List.length descr_lambda_list - and nconstrs = vd.vd_consts + vd.vd_nonconsts + vd.vd_unboxed in + and nconstrs = + cstr.cstr_consts + cstr.cstr_nonconsts + cstr.cstr_unboxed in let sig_complete = ncases = nconstrs in let fail_opt, fails, local_jumps = if sig_complete then @@ -2885,7 +2885,7 @@ let combine_constructor loc arg pat_env cstr partial ctx def let cases = split_cases pat_env (List.map tag_lambda descr_lambda_list) in match - (vd.vd_consts, vd.vd_nonconsts, cases) + (cstr.cstr_consts, cstr.cstr_nonconsts, cases) with | 1, 1, { consts = [ (0, act1) ]; nonconsts = [ (0, act2) ] } (* Typically, match on lists, will avoid isint primitive in that @@ -2908,27 +2908,24 @@ let combine_constructor loc arg pat_env cstr partial ctx def | _, Some a, _ -> Some a | None, None, nonconsts -> same_actions nonconsts | Some _, None, cases -> - (* FIXME: today cstr.cstr_{non,}consts does not count - unboxed constructors so it cannot be correctly used - to decide exhaustiveness. - - TODO: have a version of cstr_nonconsts that counts - not the number of different constructors, but the number - of possible head tags (in the non-any case); then we can - in fact compare this number to the length of the list - -- given that split_cases will expand several-tag - constructors into several list items. *) - if List.length cases = complete_case_count then - same_actions cases - else - None + match complete_case_count with + | Some count -> + if List.length cases = count then + same_actions cases + else + None + | None -> assert false in let single_nonconst_act = - single_action - cases.any_nonconst cases.nonconsts vd.vd_nonconsts in + let numnonconsts = + Typedecl.cstr_unboxed_numnonconsts pat_env cstr in + single_action cases.any_nonconst cases.nonconsts numnonconsts + in let single_const_act = - single_action - cases.any_const cases.consts vd.vd_consts in + let numconsts = + Typedecl.cstr_unboxed_numconsts pat_env cstr in + single_action cases.any_const cases.consts numconsts + in let test_isint const_act nonconst_act = Lifthenelse ( Lprim (Pisint, [ arg ], loc), const_act, nonconst_act ) @@ -2959,27 +2956,20 @@ let combine_constructor loc arg pat_env cstr partial ctx def | Some fail_act, Some a -> Some (test_isint a fail_act) in - let numconsts, numblocks = - let bounds = match vd.vd_max_values with - | Some bounds -> bounds - | None -> - (* The values are not filled e.g in case a type is - imported from a foreign cmi interface; we need to - recompute them here *) - if vd.vd_unboxed = 0 then - Max vd.vd_consts, Max vd.vd_nonconsts - else - Typedecl_unboxed.Head_shape.max_val_of_cstr_descr - pat_env cstr - in match bounds with - | Max imm, Max tag -> imm, tag - | Unbounded, _ | _, Unbounded -> - invalid_arg "Matching.combine_constructors" + let sw_numconsts = + match Typedecl.cstr_max_imm_value pat_env cstr with + | Some n -> n + 1 + | None -> 1 (* XXX *) + in + let sw_numblocks = + match Typedecl.cstr_max_block_tag pat_env cstr with + | Some n -> n + 1 + | None -> invalid_arg "Matching.combine_constructors" in let sw = - { sw_numconsts = numconsts + 1; + { sw_numconsts; sw_consts = cases.consts; - sw_numblocks = numblocks + 1; + sw_numblocks; sw_blocks = cases.nonconsts; sw_failaction = fail_opt } diff --git a/lambda/translcore.ml b/lambda/translcore.ml index 0541eac0f9d6..84874ec65ff4 100644 --- a/lambda/translcore.ml +++ b/lambda/translcore.ml @@ -103,8 +103,7 @@ let rec trivial_pat pat = Tpat_var _ | Tpat_any -> true | Tpat_construct (_, cd, [], _) -> - let vd = cd.cstr_variants in - not cd.cstr_generalized && vd.vd_consts = 1 && vd.vd_nonconsts = 0 + not cd.cstr_generalized && cd.cstr_consts = 1 && cd.cstr_nonconsts = 0 | Tpat_tuple patl -> List.for_all trivial_pat patl | _ -> false diff --git a/testsuite/tests/typing-unboxed-types/test.ml b/testsuite/tests/typing-unboxed-types/test.ml index 5e81a3d75faa..32e32a7859fe 100644 --- a/testsuite/tests/typing-unboxed-types/test.ml +++ b/testsuite/tests/typing-unboxed-types/test.ml @@ -94,14 +94,19 @@ Error: This type cannot be unboxed because (* let rec must be rejected *) type t10 = A of t10 [@@ocaml.unboxed];; [%%expect{| -type t10 = A of t10 [@@unboxed] +Line 1, characters 0-37: +1 | type t10 = A of t10 [@@ocaml.unboxed];; + ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ +Error: Cyclic type expansion during [@unboxed] verification. + t10/188[22] appears unboxed at the head of its own definition. |}];; let rec x = A x;; [%%expect{| -Line 1, characters 12-15: +Line 1, characters 14-15: 1 | let rec x = A x;; - ^^^ -Error: This kind of expression is not allowed as right-hand side of `let rec' + ^ +Error: This expression has type t1 but an expression was expected of type + string |}];; (* Representation mismatch between module and signature must be rejected *) @@ -260,17 +265,29 @@ in assert (f x = L 3.14);; (* Check for a potential infinite loop in the typing algorithm. *) type 'a t12 = M of 'a t12 [@@ocaml.unboxed];; [%%expect{| -type 'a t12 = M of 'a t12 [@@unboxed] +Line 1, characters 0-43: +1 | type 'a t12 = M of 'a t12 [@@ocaml.unboxed];; + ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ +Error: Cyclic type expansion during [@unboxed] verification. + t12/553[43] appears unboxed at the head of its own definition. |}];; let f (a : int t12 array) = a.(0);; [%%expect{| -val f : int t12 array -> int t12 = +Line 1, characters 15-18: +1 | let f (a : int t12 array) = a.(0);; + ^^^ +Error: Unbound type constructor t12 +Hint: Did you mean t1, t11 or t2? |}];; (* Check for another possible loop *) type t13 = A : _ t12 -> t13 [@@ocaml.unboxed];; [%%expect{| -type t13 = A : 'a t12 -> t13 [@@unboxed] +Line 1, characters 17-20: +1 | type t13 = A : _ t12 -> t13 [@@ocaml.unboxed];; + ^^^ +Error: Unbound type constructor t12 +Hint: Did you mean t1, t11, t13 or t2? |}];; diff --git a/testsuite/tests/typing-unboxed-types/test_unboxed_constr_matching.ml b/testsuite/tests/typing-unboxed-types/test_unboxed_constr_matching.ml index a03c363d785d..e9e68907afc5 100644 --- a/testsuite/tests/typing-unboxed-types/test_unboxed_constr_matching.ml +++ b/testsuite/tests/typing-unboxed-types/test_unboxed_constr_matching.ml @@ -31,3 +31,9 @@ module B = struct end let () = B.test () + +module C = struct + type t = I of int [@unboxed] | C1 of unit | C2 of unit + + let f = function I i -> i | C1 () -> 0 | C2 () -> 1 +end diff --git a/typing/datarepr.ml b/typing/datarepr.ml index 8af9eb93b4d3..bdace68f54e8 100644 --- a/typing/datarepr.ml +++ b/typing/datarepr.ml @@ -101,20 +101,13 @@ let constructor_descrs ~current_unit ty_path decl cstrs rep = let ty_res = newgenconstr ty_path decl.type_params in let variant_unboxed = Builtin_attributes.has_unboxed decl.type_attributes in let num_consts = ref 0 and num_nonconsts = ref 0 and num_unboxed = ref 0 in + let variant_data = ref None in List.iter (fun {cd_args; cd_attributes; _} -> if Builtin_attributes.has_unboxed cd_attributes then incr num_unboxed else if cd_args = Cstr_tuple [] then incr num_consts else incr num_nonconsts; ) cstrs; - let variant_data = - { - vd_consts = !num_consts; - vd_nonconsts = !num_nonconsts; - vd_unboxed = !num_unboxed; - vd_max_values = None; - } - in let rec describe_constructors idx_const idx_nonconst = function [] -> [] | {cd_id; cd_args; cd_res; cd_loc; cd_attributes; cd_uid} :: rem -> @@ -157,7 +150,10 @@ let constructor_descrs ~current_unit ty_path decl cstrs rep = cstr_args; cstr_arity = List.length cstr_args; cstr_tag = tag; - cstr_variants = variant_data; + cstr_consts = !num_consts; + cstr_nonconsts = !num_nonconsts; + cstr_unboxed = !num_unboxed; + cstr_variant = variant_data; cstr_private = decl.type_private; cstr_generalized = cd_res <> None; cstr_loc = cd_loc; @@ -177,14 +173,6 @@ let extension_descr ~current_unit path_ext ext = let existentials, cstr_args, cstr_inlined = constructor_args ~current_unit ext.ext_private ext.ext_args ext.ext_ret_type path_ext (Record_extension path_ext) - in - let variant_data = - { - vd_consts = -1; - vd_nonconsts = -1; - vd_unboxed = -1; - vd_max_values = None; - } in { cstr_name = Path.last path_ext; cstr_res = ty_res; @@ -192,7 +180,10 @@ let extension_descr ~current_unit path_ext ext = cstr_args; cstr_arity = List.length cstr_args; cstr_tag = Cstr_extension(path_ext, cstr_args = []); - cstr_variants = variant_data; + cstr_consts = -1; + cstr_nonconsts = -1; + cstr_unboxed = -1; + cstr_variant = ref None; cstr_private = ext.ext_private; cstr_generalized = ext.ext_ret_type <> None; cstr_loc = ext.ext_loc; diff --git a/typing/parmatch.ml b/typing/parmatch.ml index 030e0d3ff02c..bb522f3291e8 100644 --- a/typing/parmatch.ml +++ b/typing/parmatch.ml @@ -121,8 +121,8 @@ let all_coherent column = let coherent_heads hp1 hp2 = match hp1.pat_desc, hp2.pat_desc with | Construct c, Construct c' -> - c.cstr_variants.vd_consts = c'.cstr_variants.vd_consts - && c.cstr_variants.vd_nonconsts = c'.cstr_variants.vd_nonconsts + c.cstr_consts = c'.cstr_consts + && c.cstr_nonconsts = c'.cstr_nonconsts | Constant c1, Constant c2 -> begin match c1, c2 with | Const_char _, Const_char _ @@ -750,8 +750,7 @@ let full_match closing env = match env with | Any -> assert false | Construct { cstr_tag = Cstr_extension _ ; _ } -> false | Construct c -> - let vd = c.cstr_variants in - List.length env = vd.vd_consts + vd.vd_nonconsts + vd.vd_unboxed + List.length env = c.cstr_consts + c.cstr_nonconsts + c.cstr_unboxed | Variant { type_row; _ } -> let fields = List.map diff --git a/typing/typedecl.ml b/typing/typedecl.ml index ec1aa56f9896..078afbf2af86 100644 --- a/typing/typedecl.ml +++ b/typing/typedecl.ml @@ -1924,3 +1924,28 @@ let () = | _ -> None ) + +let get_variant_data env cstr_desc = + match !(cstr_desc.cstr_variant) with + | Some data-> data + | None -> + let open Typedecl_unboxed in + let variant_data = + let path = Btype.cstr_type_path cstr_desc in + let shape = Head_shape.of_type env path in + Head_shape.variant_data_of_shape shape + in + cstr_desc.cstr_variant := Some variant_data; + variant_data + +let cstr_max_block_tag env cstr_desc = + (get_variant_data env cstr_desc).vd_max_block_tag + +let cstr_max_imm_value env cstr_desc = + (get_variant_data env cstr_desc).vd_max_imm_value + +let cstr_unboxed_numconsts env cstr_desc = + (get_variant_data env cstr_desc).vd_unboxed_numconsts + +let cstr_unboxed_numnonconsts env cstr_desc = + (get_variant_data env cstr_desc).vd_unboxed_numnonconsts diff --git a/typing/typedecl.mli b/typing/typedecl.mli index 067319f041a8..9587ed87b8e2 100644 --- a/typing/typedecl.mli +++ b/typing/typedecl.mli @@ -108,3 +108,11 @@ type error = exception Error of Location.t * error val report_error: formatter -> error -> unit + +val cstr_max_block_tag : Env.t -> constructor_description -> int option + +val cstr_max_imm_value : Env.t -> constructor_description -> int option + +val cstr_unboxed_numconsts : Env.t -> constructor_description -> int option + +val cstr_unboxed_numnonconsts : Env.t -> constructor_description -> int option diff --git a/typing/typedecl_unboxed.ml b/typing/typedecl_unboxed.ml index 6d698e96f1ed..53ef4d80b785 100644 --- a/typing/typedecl_unboxed.ml +++ b/typing/typedecl_unboxed.ml @@ -267,8 +267,8 @@ module Head_shape = struct | Type_variant ((fst_descr :: _) as cstr_descrs,_) -> (* we compute the shape of all boxed constructors, then the shapes of each unboxed constructors *) - let num_consts = fst_descr.cstr_variants.vd_consts in - let num_nonconsts = fst_descr.cstr_variants.vd_nonconsts in + let num_consts = fst_descr.cstr_consts in + let num_nonconsts = fst_descr.cstr_nonconsts in (* the head shape of boxed constructors is equivalent to the nb of constant constructors and the nb of non constant constructors *) let boxed_shape = cstrs_shape ~num_consts ~num_nonconsts in @@ -296,6 +296,22 @@ module Head_shape = struct let fill_cache env unboxed_data = ignore (get env unboxed_data) + let variant_data_of_shape shape = + let bound_of_shape = function + | Shape_set l -> Some (List.fold_left max 0 l) + | Shape_any -> None + in + let num_of_shape = function + | Shape_set l -> Some (List.length l) + | Shape_any -> None + in + { + vd_max_imm_value = bound_of_shape shape.head_imm; + vd_max_block_tag = bound_of_shape shape.head_blocks; + vd_unboxed_numconsts = num_of_shape shape.head_imm; + vd_unboxed_numnonconsts = num_of_shape shape.head_blocks; + } + let check ~print env (path,decl) = match Env.find_type_descrs path env with | exception Not_found -> failwith "XXX" @@ -310,18 +326,11 @@ module Head_shape = struct let ty = Btype.newgenty (Tconstr (path, params, ref Mnil)) in let callstack_map = Callstack.fill ty [] in let shape = of_type env ty callstack_map in - let bound_of_shape = function - | Shape_set l -> Types.Max (List.fold_left max 0 l) - | Shape_any -> Types.Unbounded - in + (* Fill the variant data *) match cstrs with | [] -> () - | cstr :: _ -> begin - let vd = cstr.cstr_variants in - let imm_bound = bound_of_shape shape.head_imm in - let tag_bound = bound_of_shape shape.head_blocks in - vd.vd_max_values <- Some (imm_bound, tag_bound) - end; + | cstr :: _ -> + cstr.cstr_variant := Some (variant_data_of_shape shape); if print && !Clflags.dump_headshape then Format.fprintf Format.err_formatter "SHAPE(%a) %a@." Path.print path @@ -336,13 +345,9 @@ module Head_shape = struct let check_typedecl env (id,decl) = check ~print:true env (id,decl) - let max_val_of_cstr_descr env cstr = - let variant_path = match get_desc cstr.cstr_res with - | Tconstr (p, _, _) -> p - | _ -> assert false (* XXX *) - in - let variant_decl = Env.find_type variant_path env in - check ~print:false env (variant_path,variant_decl); - let variant = cstr.cstr_variants in - Option.get variant.vd_max_values + let of_type env path = + let decl = Env.find_type path env in + let ty = Btype.newgenty (Tconstr (path, decl.type_params, ref Mnil)) in + let callstacks = Callstack.fill ty [] in + of_type env ty callstacks end diff --git a/typing/typedecl_unboxed.mli b/typing/typedecl_unboxed.mli index 375ed1d2bf02..6828140291b6 100644 --- a/typing/typedecl_unboxed.mli +++ b/typing/typedecl_unboxed.mli @@ -31,10 +31,12 @@ module Head_shape : sig val check_typedecl : Env.t -> Path.t * Types.type_declaration -> unit - val max_val_of_cstr_descr : Env.t -> constructor_description -> - int bound * int bound - + (* Functions to process Cstr_unboxed cache *) val get : Env.t -> Types.unboxed_data -> head_shape val fill_cache : Env.t -> Types.unboxed_data -> unit + + val of_type : Env.t -> Path.t -> t + + val variant_data_of_shape : t -> Types.variant_data end diff --git a/typing/types.ml b/typing/types.ml index 6b463c72d4a1..e99b611aa80b 100644 --- a/typing/types.ml +++ b/typing/types.ml @@ -404,7 +404,11 @@ type constructor_description = cstr_args: type_expr list; (* Type of the arguments *) cstr_arity: int; (* Number of arguments *) cstr_tag: constructor_tag; (* Tag for heap blocks *) - cstr_variants: variant_data; (* Datatype-related information *) + cstr_consts: int; (* Number of constant constructors *) + cstr_nonconsts: int; (* Number of non-const constructors *) + cstr_unboxed: int; (* Number of unboxed constructors *) + cstr_variant: variant_data option ref; + (* Variant type related data *) cstr_generalized: bool; (* Constrained return type? *) cstr_private: private_flag; (* Read-only constructor? *) cstr_loc: Location.t; @@ -413,17 +417,6 @@ type constructor_description = cstr_uid: Uid.t; } -and variant_data = - { vd_consts: int; (* Number of constant constructors *) - vd_nonconsts: int; (* Number of non-const constructors *) - vd_unboxed: int; (* Number of unboxed constructors *) - mutable vd_max_values: (int bound * int bound) option; - (* Maximum immediate value and block tags taking into account unboxed - constructors (only available after head-shape analysis) *) - } - -and 'a bound = Unbounded | Max of 'a - and constructor_tag = Cstr_constant of int (* Constant constructor (an int) *) | Cstr_block of int (* Regular constructor (a block) *) @@ -436,8 +429,8 @@ and unboxed_data = } and head_shape = - { head_imm : imm shape; (* set of immediates the head can be *) - head_blocks : tag shape; (* set of tags the head can have *) + { head_imm: imm shape; (* set of immediates the head can be *) + head_blocks: tag shape; (* set of tags the head can have *) } and 'a shape = @@ -448,6 +441,13 @@ and 'a shape = and imm = int and tag = int +and variant_data = + { vd_max_block_tag: int option; + vd_max_imm_value: int option; + vd_unboxed_numconsts: int option; + vd_unboxed_numnonconsts: int option; + } + let equal_tag t1 t2 = match (t1, t2) with | Cstr_constant i1, Cstr_constant i2 -> i2 = i1 diff --git a/typing/types.mli b/typing/types.mli index ac084740fa8a..05886c82b69d 100644 --- a/typing/types.mli +++ b/typing/types.mli @@ -582,7 +582,11 @@ type constructor_description = cstr_args: type_expr list; (* Type of the arguments *) cstr_arity: int; (* Number of arguments *) cstr_tag: constructor_tag; (* Tag for heap blocks *) - cstr_variants: variant_data; (* Datatype-related information *) + cstr_consts: int; (* Number of constant constructors *) + cstr_nonconsts: int; (* Number of non-const constructors *) + cstr_unboxed: int; (* Number of unboxed constructors *) + cstr_variant: variant_data option ref; + (* Variant type related data *) cstr_generalized: bool; (* Constrained return type? *) cstr_private: private_flag; (* Read-only constructor? *) cstr_loc: Location.t; @@ -591,17 +595,6 @@ type constructor_description = cstr_uid: Uid.t; } - and variant_data = - { vd_consts: int; (* Number of constant constructors *) - vd_nonconsts: int; (* Number of non-const constructors *) - vd_unboxed: int; (* Number of unboxed constructors *) - mutable vd_max_values: (int bound * int bound) option; - (* Maximum immediate value and block tags taking into account unboxed - constructors (only available after head-shape analysis) *) - } - -and 'a bound = Unbounded | Max of 'a - and constructor_tag = Cstr_constant of int (* Constant constructor (an int) *) | Cstr_block of int (* Regular constructor (a block) *) @@ -626,6 +619,13 @@ and 'a shape = and imm = int and tag = int +and variant_data = + { vd_max_block_tag: int option; + vd_max_imm_value: int option; + vd_unboxed_numconsts: int option; + vd_unboxed_numnonconsts: int option; + } + (* Constructors are the same *) val equal_tag : constructor_tag -> constructor_tag -> bool From d9cb31d8ef94bed79d300615adaf33d1db0f738b Mon Sep 17 00:00:00 2001 From: Nicolas Chataing Date: Tue, 13 Jul 2021 09:40:00 +0200 Subject: [PATCH 09/45] Move variant_data binding (and add comment) --- typing/datarepr.ml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/typing/datarepr.ml b/typing/datarepr.ml index bdace68f54e8..a3f7d09f6771 100644 --- a/typing/datarepr.ml +++ b/typing/datarepr.ml @@ -101,13 +101,14 @@ let constructor_descrs ~current_unit ty_path decl cstrs rep = let ty_res = newgenconstr ty_path decl.type_params in let variant_unboxed = Builtin_attributes.has_unboxed decl.type_attributes in let num_consts = ref 0 and num_nonconsts = ref 0 and num_unboxed = ref 0 in - let variant_data = ref None in List.iter (fun {cd_args; cd_attributes; _} -> if Builtin_attributes.has_unboxed cd_attributes then incr num_unboxed else if cd_args = Cstr_tuple [] then incr num_consts else incr num_nonconsts; ) cstrs; + (* Variant data is shared among constructors of the same variant type *) + let variant_data = ref None in let rec describe_constructors idx_const idx_nonconst = function [] -> [] | {cd_id; cd_args; cd_res; cd_loc; cd_attributes; cd_uid} :: rem -> From e2f46e406ca7e80ba7f1d6d4394b1760bae12549 Mon Sep 17 00:00:00 2001 From: Nicolas Chataing Date: Tue, 13 Jul 2021 09:42:44 +0200 Subject: [PATCH 10/45] replace invalid arg by an assert false --- lambda/matching.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lambda/matching.ml b/lambda/matching.ml index 729c0c5e8793..629b9d38a650 100644 --- a/lambda/matching.ml +++ b/lambda/matching.ml @@ -2964,7 +2964,7 @@ let combine_constructor loc arg pat_env cstr partial ctx def let sw_numblocks = match Typedecl.cstr_max_block_tag pat_env cstr with | Some n -> n + 1 - | None -> invalid_arg "Matching.combine_constructors" + | None -> assert false in let sw = { sw_numconsts; From 29437d69f3f99c4e5df2fb46ac3bd31e3f040505 Mon Sep 17 00:00:00 2001 From: Gabriel Scherer Date: Tue, 13 Jul 2021 10:41:42 +0200 Subject: [PATCH 11/45] document typing/types.mli + renamings --- typing/datarepr.ml | 8 ++-- typing/typedecl.ml | 20 ++++---- typing/typedecl.mli | 5 +- typing/typedecl_unboxed.ml | 13 ++--- typing/typedecl_unboxed.mli | 4 +- typing/types.ml | 15 +++--- typing/types.mli | 94 +++++++++++++++++++++++++++++++------ 7 files changed, 113 insertions(+), 46 deletions(-) diff --git a/typing/datarepr.ml b/typing/datarepr.ml index a3f7d09f6771..e5e303816f42 100644 --- a/typing/datarepr.ml +++ b/typing/datarepr.ml @@ -107,8 +107,8 @@ let constructor_descrs ~current_unit ty_path decl cstrs rep = else if cd_args = Cstr_tuple [] then incr num_consts else incr num_nonconsts; ) cstrs; - (* Variant data is shared among constructors of the same variant type *) - let variant_data = ref None in + (* Unboxed type data is shared among constructors of the same variant type *) + let unboxed_type_data = ref None in let rec describe_constructors idx_const idx_nonconst = function [] -> [] | {cd_id; cd_args; cd_res; cd_loc; cd_attributes; cd_uid} :: rem -> @@ -154,7 +154,7 @@ let constructor_descrs ~current_unit ty_path decl cstrs rep = cstr_consts = !num_consts; cstr_nonconsts = !num_nonconsts; cstr_unboxed = !num_unboxed; - cstr_variant = variant_data; + cstr_unboxed_type_data = unboxed_type_data; cstr_private = decl.type_private; cstr_generalized = cd_res <> None; cstr_loc = cd_loc; @@ -184,7 +184,7 @@ let extension_descr ~current_unit path_ext ext = cstr_consts = -1; cstr_nonconsts = -1; cstr_unboxed = -1; - cstr_variant = ref None; + cstr_unboxed_type_data = ref None; cstr_private = ext.ext_private; cstr_generalized = ext.ext_ret_type <> None; cstr_loc = ext.ext_loc; diff --git a/typing/typedecl.ml b/typing/typedecl.ml index 078afbf2af86..8afcab2c0722 100644 --- a/typing/typedecl.ml +++ b/typing/typedecl.ml @@ -1925,27 +1925,27 @@ let () = None ) -let get_variant_data env cstr_desc = - match !(cstr_desc.cstr_variant) with +let get_unboxed_type_data env cstr_desc = + match !(cstr_desc.cstr_unboxed_type_data) with | Some data-> data | None -> let open Typedecl_unboxed in - let variant_data = + let unboxed_type_data = let path = Btype.cstr_type_path cstr_desc in let shape = Head_shape.of_type env path in - Head_shape.variant_data_of_shape shape + Head_shape.unboxed_type_data_of_shape shape in - cstr_desc.cstr_variant := Some variant_data; - variant_data + cstr_desc.cstr_unboxed_type_data := Some unboxed_type_data; + unboxed_type_data let cstr_max_block_tag env cstr_desc = - (get_variant_data env cstr_desc).vd_max_block_tag + (get_unboxed_type_data env cstr_desc).utd_max_block_tag let cstr_max_imm_value env cstr_desc = - (get_variant_data env cstr_desc).vd_max_imm_value + (get_unboxed_type_data env cstr_desc).utd_max_imm_value let cstr_unboxed_numconsts env cstr_desc = - (get_variant_data env cstr_desc).vd_unboxed_numconsts + (get_unboxed_type_data env cstr_desc).utd_unboxed_numconsts let cstr_unboxed_numnonconsts env cstr_desc = - (get_variant_data env cstr_desc).vd_unboxed_numnonconsts + (get_unboxed_type_data env cstr_desc).utd_unboxed_numnonconsts diff --git a/typing/typedecl.mli b/typing/typedecl.mli index 9587ed87b8e2..063f75a8c6a3 100644 --- a/typing/typedecl.mli +++ b/typing/typedecl.mli @@ -109,9 +109,10 @@ exception Error of Location.t * error val report_error: formatter -> error -> unit -val cstr_max_block_tag : Env.t -> constructor_description -> int option +(* See [unboxed_type_data] in types.mli *) +val cstr_max_imm_value : Env.t -> constructor_description -> Types.imm option -val cstr_max_imm_value : Env.t -> constructor_description -> int option +val cstr_max_block_tag : Env.t -> constructor_description -> Types.tag option val cstr_unboxed_numconsts : Env.t -> constructor_description -> int option diff --git a/typing/typedecl_unboxed.ml b/typing/typedecl_unboxed.ml index 53ef4d80b785..8728f08a865c 100644 --- a/typing/typedecl_unboxed.ml +++ b/typing/typedecl_unboxed.ml @@ -296,7 +296,7 @@ module Head_shape = struct let fill_cache env unboxed_data = ignore (get env unboxed_data) - let variant_data_of_shape shape = + let unboxed_type_data_of_shape shape = let bound_of_shape = function | Shape_set l -> Some (List.fold_left max 0 l) | Shape_any -> None @@ -306,10 +306,10 @@ module Head_shape = struct | Shape_any -> None in { - vd_max_imm_value = bound_of_shape shape.head_imm; - vd_max_block_tag = bound_of_shape shape.head_blocks; - vd_unboxed_numconsts = num_of_shape shape.head_imm; - vd_unboxed_numnonconsts = num_of_shape shape.head_blocks; + utd_max_imm_value = bound_of_shape shape.head_imm; + utd_max_block_tag = bound_of_shape shape.head_blocks; + utd_unboxed_numconsts = num_of_shape shape.head_imm; + utd_unboxed_numnonconsts = num_of_shape shape.head_blocks; } let check ~print env (path,decl) = @@ -330,7 +330,8 @@ module Head_shape = struct match cstrs with | [] -> () | cstr :: _ -> - cstr.cstr_variant := Some (variant_data_of_shape shape); + cstr.cstr_unboxed_type_data := + Some (unboxed_type_data_of_shape shape); if print && !Clflags.dump_headshape then Format.fprintf Format.err_formatter "SHAPE(%a) %a@." Path.print path diff --git a/typing/typedecl_unboxed.mli b/typing/typedecl_unboxed.mli index 6828140291b6..6fb0ede8ec93 100644 --- a/typing/typedecl_unboxed.mli +++ b/typing/typedecl_unboxed.mli @@ -34,9 +34,7 @@ module Head_shape : sig (* Functions to process Cstr_unboxed cache *) val get : Env.t -> Types.unboxed_data -> head_shape - val fill_cache : Env.t -> Types.unboxed_data -> unit - val of_type : Env.t -> Path.t -> t - val variant_data_of_shape : t -> Types.variant_data + val unboxed_type_data_of_shape : t -> Types.unboxed_type_data end diff --git a/typing/types.ml b/typing/types.ml index e99b611aa80b..fdc7f7dddd00 100644 --- a/typing/types.ml +++ b/typing/types.ml @@ -407,8 +407,9 @@ type constructor_description = cstr_consts: int; (* Number of constant constructors *) cstr_nonconsts: int; (* Number of non-const constructors *) cstr_unboxed: int; (* Number of unboxed constructors *) - cstr_variant: variant_data option ref; - (* Variant type related data *) + cstr_unboxed_type_data: unboxed_type_data option ref; + (* Type-global data that depends + on unboxing / head-shape information. *) cstr_generalized: bool; (* Constrained return type? *) cstr_private: private_flag; (* Read-only constructor? *) cstr_loc: Location.t; @@ -441,11 +442,11 @@ and 'a shape = and imm = int and tag = int -and variant_data = - { vd_max_block_tag: int option; - vd_max_imm_value: int option; - vd_unboxed_numconsts: int option; - vd_unboxed_numnonconsts: int option; +and unboxed_type_data = + { utd_max_imm_value: int option; + utd_max_block_tag: int option; + utd_unboxed_numconsts: int option; + utd_unboxed_numnonconsts: int option; } let equal_tag t1 t2 = diff --git a/typing/types.mli b/typing/types.mli index 05886c82b69d..3891872bdf67 100644 --- a/typing/types.mli +++ b/typing/types.mli @@ -582,49 +582,115 @@ type constructor_description = cstr_args: type_expr list; (* Type of the arguments *) cstr_arity: int; (* Number of arguments *) cstr_tag: constructor_tag; (* Tag for heap blocks *) + + (* The following group of fields store information not on this constructor, + but on all constructors of the variant, for pattern-matching compilation + purposes. *) cstr_consts: int; (* Number of constant constructors *) cstr_nonconsts: int; (* Number of non-const constructors *) cstr_unboxed: int; (* Number of unboxed constructors *) - cstr_variant: variant_data option ref; - (* Variant type related data *) + cstr_unboxed_type_data: unboxed_type_data option ref; + (* This mutable reference is shared among all + constructor_description for the same type, and depends on its + head shape. It is computed "later" (when a type environment + is available) by Typedecl.get_unboxed_type_data. *) + cstr_generalized: bool; (* Constrained return type? *) cstr_private: private_flag; (* Read-only constructor? *) cstr_loc: Location.t; cstr_attributes: Parsetree.attributes; cstr_inlined: type_declaration option; cstr_uid: Uid.t; - } + } and constructor_tag = Cstr_constant of int (* Constant constructor (an int) *) | Cstr_block of int (* Regular constructor (a block) *) - | Cstr_unboxed of unboxed_data (* Constructor of an unboxed type *) + | Cstr_unboxed of unboxed_data (* Unboxed constructor *) | Cstr_extension of Path.t * bool (* Extension constructor true if a constant false if a block*) and unboxed_data = - { unboxed_ty: type_expr; - unboxed_shape: head_shape option ref; + { unboxed_ty: type_expr; (* type of the constructor parameter *) + unboxed_shape: + head_shape option ref; + (* The head-shape information is not available at type-declaration + construction time. It is computed later, from the type + environment, see Typedecl_unboxed.Head_Shape.get; either at + tpe-declaration checking time or (for types imported from + a .cmi) at first query of the information by the + pattern-matching compiler. *) } +(* Over-approximation of the possible values of a type, + used to verify and compile unboxed head constructors. + + We represent the "head" of the values: their value if + it is an immediate, or their tag if is a block. + A head "shape" is a set of possible heads. +*) and head_shape = { head_imm : imm shape; (* set of immediates the head can be *) head_blocks : tag shape; (* set of tags the head can have *) } +(* A description of a set of ['a] elements. *) and 'a shape = - (* TODO add some comment *) - | Shape_set of 'a list - | Shape_any + | Shape_set of 'a list (* An element among a finite list. *) + | Shape_any (* Any element (Top/Unknown). *) and imm = int and tag = int -and variant_data = - { vd_max_block_tag: int option; - vd_max_imm_value: int option; - vd_unboxed_numconsts: int option; - vd_unboxed_numnonconsts: int option; +(* Type-global data that depends on unboxing / head-shape information. + + Note: the fields below should not be accessed directly, but through + the helper functions in Typedecl + + cstr_max_block_tag : Env.t -> constructor_description -> Types.tag option + cstr_max_imm_value : Env.t -> constructor_description -> Types.imm option + cstr_unboxed_numconsts : Env.t -> constructor_description -> int option + cstr_unboxed_numnonconsts : Env.t -> constructor_description -> int option + + which take care of caching the [unboxed_type_data] field. +*) +and unboxed_type_data = + { utd_max_imm_value: int option; + (* The maximal immediate value at this type after unboxing; + None is used in the Shape_any case -- any immediate can occur.*) + + utd_max_block_tag: int option; + (* The maximal block tag at this type after unboxing; + None is used in the Shape_any case -- any tag can occur.*) + + utd_unboxed_numconsts: int option; + (* The number of constant constructors after unboxing. *) + + utd_unboxed_numnonconsts: int option; + (* The number of non-constant constructors after unboxing. *) } +(* + Consider for example + + type t = + | Int of int [@unboxed] + | List of t list + | Str of string [@unboxed + + After unboxing, the representations of values at this type may be: + - any immediate value (coming from Int) + - a block of tag 0 (for List) + - a string value of tag String_tag (252) + + We have: { + utd_max_imm_value = None; + utd_max_block_tag = Some 252; + utd_unboxed_numconsts = None; + utd_unboxed_numnonconsts = Some 2; + } + + This information is needed by lambda/matching.ml to compile switches + on these constructors. +*) (* Constructors are the same *) val equal_tag : constructor_tag -> constructor_tag -> bool From 658e62772accc2223576f82786a64b33a78735f7 Mon Sep 17 00:00:00 2001 From: Gabriel Scherer Date: Tue, 13 Jul 2021 12:11:28 +0200 Subject: [PATCH 12/45] document typedecl_unboxed.ml{,i} --- typing/datarepr.ml | 1 + typing/typedecl_unboxed.ml | 91 ++++++++++++++++++++++++++++++------- typing/typedecl_unboxed.mli | 16 +++++-- 3 files changed, 89 insertions(+), 19 deletions(-) diff --git a/typing/datarepr.ml b/typing/datarepr.ml index e5e303816f42..ea17a48411e0 100644 --- a/typing/datarepr.ml +++ b/typing/datarepr.ml @@ -20,6 +20,7 @@ open Asttypes open Types open Btype +(* TODO: register an error printer for this type. *) type error = | Multiple_args_unboxed_constructor of Ident.t diff --git a/typing/typedecl_unboxed.ml b/typing/typedecl_unboxed.ml index 8728f08a865c..4d4709813a74 100644 --- a/typing/typedecl_unboxed.ml +++ b/typing/typedecl_unboxed.ml @@ -81,6 +81,8 @@ let match_primitive_type p = module Head_shape = struct exception Conflict + (* TODO: add more information to be able to display proper + error messages. *) type t = head_shape @@ -156,7 +158,7 @@ module Head_shape = struct let fill ty callstack = extend TypeMap.empty ty callstack end - (* Useful to interactively debug 'of_type' below. *) + (* Useful to interactively debug 'of_type_expr' below. *) let _print_annotations ty callstack_map = Format.eprintf "@[CALLSTACK(%a): @[" Printtyp.type_expr ty; @@ -185,7 +187,7 @@ module Head_shape = struct | Tpoly (t, _) -> t | _ -> ty - let rec of_type env ty callstack_map = + let rec of_type_expr env ty callstack_map = (* TODO : try the Ctype.expand_head_opt version here *) check_annotated ty callstack_map; match get_desc ty with @@ -233,7 +235,7 @@ module Head_shape = struct and of_typedescr env ty_descr ty_decl ~args callstack_map new_callstack = - let of_type_with_params ty = + let of_type_expr_with_params ty = (* We instantiate the formal type variables with the type expression parameters at use site. @@ -245,19 +247,19 @@ module Head_shape = struct let ty = Ctype.apply env params ty args in let callstack_map = Callstack.extend callstack_map ty new_callstack in - of_type env ty callstack_map + of_type_expr env ty callstack_map in match ty_descr with | Type_abstract -> begin match ty_decl.type_manifest with | None -> any_shape - | Some ty -> of_type_with_params ty + | Some ty -> of_type_expr_with_params ty end | Type_record (_, Record_regular) -> block_shape [0] | Type_record (_, Record_float) -> block_shape [Obj.double_array_tag] | Type_record (fields, Record_unboxed _) -> begin match fields with - | [{lbl_arg = ty; _}] -> of_type_with_params ty + | [{lbl_arg = ty; _}] -> of_type_expr_with_params ty | _ -> assert false end | Type_record (_, Record_inlined _) @@ -277,24 +279,70 @@ module Head_shape = struct match descr.cstr_tag with | Cstr_constant _ | Cstr_block _ | Cstr_extension _ -> None | Cstr_unboxed {unboxed_ty; _}-> - Some (of_type_with_params unboxed_ty) + Some (of_type_expr_with_params unboxed_ty) ) cstr_descrs in (* now checking that the unboxed constructors are compatible with the shape of boxed constructors *) List.fold_left disjoint_union boxed_shape unboxed_shapes - let get env {unboxed_ty; unboxed_shape} = + (* Remark on the life cycle of [unboxed_shape] information. + + The [cstr_tag] data that contains [unboxed_shape] is created + un-initialized by Datarepr, when entering a type declaration + inside the current typing environment. We cannot compute the + head-shape at this point: Env depends on Datarepr, so Datarepr + functions cannot depend on Env.t. + + Type declarations coming from the user code are "checked" after + being entered in the environment by the Typedecl module; at this + point the [check_typedecl] function below is called, and the + [unboxed_shape] information for their unboxed constructors is + computed and cached at this point. Conflicts are turned into + proper user-facing errors. + + However, the environment can also be extended by type + declarations coming from other compilation units (signatures in + .cmi files), and the head-shape information is not present or + computed at this point -- we are still within Env, and cannot + call [of_type] below without creating cyclic dependencies. Note + that these type-declarations have already been checked when + compiling their own module, so they must not contain head-shape + conflicts. In this case a type declaration can leave the + type-checking phase with its [head_shape] field still + un-initialized. + + When compiling variant constructors in pattern-matching, we need + the head-shape information again. It is obtained by calling the + [get] function below, which will re-compute and cache this + information if the [unboxed_shape] field is still + un-initialized. The typing environment used for computation at + this point is the [pat_env] environment of the pattern-matching, + which we assume is an extension of the environment used at + variant constructor declaration time. + + Error handling: [check_typedecl] handles Conflict exceptions by + showing a proper error to the user -- the error is in the user + code. On the other hand, [get] and [of_type] must never see + a shape conflict, as we assume the only un-initialized + [unboxed_shape] fields come from already-checked imported + declarations. If a conflict arises in those functions, it is + a programming error in the compiler codebase: a type declaration + has somehow been entered in the environment without being + validated by [check_typedecl] first. + *) + let fill_and_get env {unboxed_ty; unboxed_shape} = match !unboxed_shape with | Some shape -> shape | None -> let ty = ty_of_poly unboxed_ty in let callstacks = Callstack.fill ty [] in - let shape = of_type env ty callstacks in + let shape = of_type_expr env ty callstacks in unboxed_shape := Some shape; shape - let fill_cache env unboxed_data = ignore (get env unboxed_data) + let fill_cache env unboxed_cache = + ignore (fill_and_get env unboxed_cache) let unboxed_type_data_of_shape shape = let bound_of_shape = function @@ -312,7 +360,7 @@ module Head_shape = struct utd_unboxed_numnonconsts = num_of_shape shape.head_blocks; } - let check ~print env (path,decl) = + let check_typedecl env (path,decl) = match Env.find_type_descrs path env with | exception Not_found -> failwith "XXX" | Type_variant (cstrs, _repr) -> begin @@ -325,30 +373,41 @@ module Head_shape = struct let params = decl.type_params in let ty = Btype.newgenty (Tconstr (path, params, ref Mnil)) in let callstack_map = Callstack.fill ty [] in - let shape = of_type env ty callstack_map in + let shape = of_type_expr env ty callstack_map in (* Fill the variant data *) match cstrs with | [] -> () | cstr :: _ -> cstr.cstr_unboxed_type_data := Some (unboxed_type_data_of_shape shape); - if print && !Clflags.dump_headshape then + if !Clflags.dump_headshape then + (* TODO improve the printing to something nicer. *) Format.fprintf Format.err_formatter "SHAPE(%a) %a@." Path.print path pp shape end with Conflict -> - if print && !Clflags.dump_headshape then + (* TODO raise a fatal error with a registered printer, + instead of what is below. *) + if !Clflags.dump_headshape then Format.fprintf Format.err_formatter "SHAPE(%a) CONFLICT@." Path.print path end | _ -> () - let check_typedecl env (id,decl) = check ~print:true env (id,decl) + let get env unboxed_data = + match fill_and_get env unboxed_data with + | exception Conflict -> + Misc.fatal_error + "Head_shape.get: check_typedecl should have run first." + | shape -> shape let of_type env path = let decl = Env.find_type path env in let ty = Btype.newgenty (Tconstr (path, decl.type_params, ref Mnil)) in let callstacks = Callstack.fill ty [] in - of_type env ty callstacks + try of_type_expr env ty callstacks + with Conflict -> + Misc.fatal_error + "Head_shape.of_type: check_typedecl should have run first." end diff --git a/typing/typedecl_unboxed.mli b/typing/typedecl_unboxed.mli index 6fb0ede8ec93..1eb5fce6a377 100644 --- a/typing/typedecl_unboxed.mli +++ b/typing/typedecl_unboxed.mli @@ -25,15 +25,25 @@ type t = val get_unboxed_type_representation: Env.t -> type_expr -> t module Head_shape : sig - exception Conflict - type t = Types.head_shape + (** Check a new type decalaration, that may be a variant type + containing unboxed constructors, to verify that the unboxing + requests respect the "disjointness" requirement of constructor + unboxing -- the values of two constructors must not conflict. + + This function fails with a fatal error if the declaration is + unsafe. *) val check_typedecl : Env.t -> Path.t * Types.type_declaration -> unit - (* Functions to process Cstr_unboxed cache *) + (** Returns the head shape information of an unboxed constructor, + computing it on the fly if necessary. The typing environment must + be an extension of the environment in which the unboxed + constructor was declared. *) val get : Env.t -> Types.unboxed_data -> head_shape + (** Returns the head shape information of variant type path, + similarly to [get] above. *) val of_type : Env.t -> Path.t -> t val unboxed_type_data_of_shape : t -> Types.unboxed_type_data From 56150054a55f9858437996e5fcc3c8d74f129cd1 Mon Sep 17 00:00:00 2001 From: Gabriel Scherer Date: Tue, 13 Jul 2021 14:36:20 +0200 Subject: [PATCH 13/45] document changes in lambda/matching.ml --- lambda/matching.ml | 88 ++++++++++++++++++++++++++++++++++------------ 1 file changed, 66 insertions(+), 22 deletions(-) diff --git a/lambda/matching.ml b/lambda/matching.ml index 629b9d38a650..fc12f0cd72b1 100644 --- a/lambda/matching.ml +++ b/lambda/matching.ml @@ -2734,6 +2734,25 @@ let combine_constant loc arg cst partial ctx def in (lambda1, Jumps.union local_jumps total) + +(* The [split_cases] function below is in charge of taking a shallow + pattern-matching on a variant type, and splitting the corresponding + constructor+action pairs into constant constructor cases and + non-constant constructor cases. + + In the presence of unboxed constructors: + + - A matching on a single source-level unboxed constructor may turn + into several cases, one for each possible head of the constructor + parameter. + + - If the head shape of an unboxed constructor contains Shape_any + (for immediate values or block tags), it must be compiled + specially. + + The Cases.t datastructure tracks such [any_const] or [any_nonconst] + actions. Note that if [any_const] is Some, then [consts] must be empty. +*) module Cases = struct type t = { consts: (int * lambda) list; @@ -2820,6 +2839,16 @@ let split_extension_cases tag_lambda_list = in split_rec tag_lambda_list +let split_variant_cases pat_env tag_lambda_list = + let Cases.{consts; nonconsts; any_const; any_nonconst} = + split_cases pat_env tag_lambda_list in + (* We assume there are no unboxed constructors + for polymorphic variants *) + assert (any_const = None); + assert (any_nonconst = None); + (consts, nonconsts) + + let combine_constructor loc arg pat_env cstr partial ctx def (descr_lambda_list, total1, pats) = let tag_lambda (cstr, act) = (cstr.cstr_tag, act) in @@ -2888,9 +2917,9 @@ let combine_constructor loc arg pat_env cstr partial ctx def (cstr.cstr_consts, cstr.cstr_nonconsts, cases) with | 1, 1, { consts = [ (0, act1) ]; nonconsts = [ (0, act2) ] } - (* Typically, match on lists, will avoid isint primitive in that - case *) | 1, 0, { consts = [ (0, act1) ]; any_nonconst = Some act2 } -> + (* Typically, match on lists, will avoid isint primitive in that + case *) Lifthenelse (arg, act2, act1) | n, 0, { consts; any_const; nonconsts=[]; any_nonconst=None } -> (* The type defines constant constructors only *) @@ -2902,30 +2931,40 @@ let combine_constructor loc arg pat_env cstr partial ctx def | n, _, _ -> ( let single_action any_case cases complete_case_count = (* = Some act when all actions are the same, - either on constant or non-constant domain *) + either on constant or non-constant domain. + + [any_case] is either [any_const] or + [any_nonconst]; it is None if all values of this + domain are accepted. In this case + complete_case_count is also None, otherwise it + must be the total number of heads at this domain. + *) match (fail_opt, any_case, cases) with | Some a, None, [] | _, Some a, _ -> Some a | None, None, nonconsts -> same_actions nonconsts | Some _, None, cases -> - match complete_case_count with - | Some count -> - if List.length cases = count then - same_actions cases - else - None - | None -> assert false - in - let single_nonconst_act = - let numnonconsts = - Typedecl.cstr_unboxed_numnonconsts pat_env cstr in - single_action cases.any_nonconst cases.nonconsts numnonconsts + (* if any_case is None, complete_case_count must be Some *) + let count = Option.get complete_case_count in + if List.length cases = count then + same_actions cases + else + None in + (* [numconsts] and [numnonconsts] count the number + of valid head constructors at this type in the domain + (only constant constructors, or only + non-constant constructors). *) let single_const_act = let numconsts = Typedecl.cstr_unboxed_numconsts pat_env cstr in single_action cases.any_const cases.consts numconsts in + let single_nonconst_act = + let numnonconsts = + Typedecl.cstr_unboxed_numnonconsts pat_env cstr in + single_action cases.any_nonconst cases.nonconsts numnonconsts + in let test_isint const_act nonconst_act = Lifthenelse ( Lprim (Pisint, [ arg ], loc), const_act, nonconst_act ) @@ -2956,15 +2995,23 @@ let combine_constructor loc arg pat_env cstr partial ctx def | Some fail_act, Some a -> Some (test_isint a fail_act) in + (* Switch is a low-level control-flow construct that must handle + an interval of contiguous values (on both domains); [sw_numconsts] + and [sw_numblocks] correspond to the size of this interval, + from 0 to the maximum head value + 1. *) let sw_numconsts = match Typedecl.cstr_max_imm_value pat_env cstr with | Some n -> n + 1 - | None -> 1 (* XXX *) + | None -> 1 (* XXX TODO *) in let sw_numblocks = match Typedecl.cstr_max_block_tag pat_env cstr with | Some n -> n + 1 - | None -> assert false + | None -> + (* single_nonconst_act is None, so there must be at least + two distinct non-constant actions, + any_nonconst is impossible. *) + assert false in let sw = { sw_numconsts; @@ -3031,11 +3078,8 @@ let combine_variant loc row arg pat_env partial ctx def else mk_failaction_neg partial ctx def in - let Cases.{consts; nonconsts; any_const; any_nonconst} = - split_cases pat_env tag_lambda_list in - (* We assume there are no unboxed constructors for polymorphic variants *) - assert (any_const = None); - assert (any_nonconst = None); + let (consts, nonconsts) = + split_variant_cases pat_env tag_lambda_list in let lambda1 = match (fail, one_action) with | None, Some act -> act From 3c2c631e44ac18d697826fae0982f2e636ac4dac Mon Sep 17 00:00:00 2001 From: Gabriel Scherer Date: Tue, 13 Jul 2021 15:11:45 +0200 Subject: [PATCH 14/45] document our disappointing bytecode generation --- lambda/matching.ml | 23 ++++++++++++++++++++++- 1 file changed, 22 insertions(+), 1 deletion(-) diff --git a/lambda/matching.ml b/lambda/matching.ml index fc12f0cd72b1..f4a1b10bb022 100644 --- a/lambda/matching.ml +++ b/lambda/matching.ml @@ -3006,7 +3006,28 @@ let combine_constructor loc arg pat_env cstr partial ctx def in let sw_numblocks = match Typedecl.cstr_max_block_tag pat_env cstr with - | Some n -> n + 1 + | Some n -> + n + 1 + (* Remark: in presence of constructor unboxing, + some block tags may be above + Obj.last_non_constant_constructor_tag (245): + + type t = + | Unit of unit (* tag 0 *) + | Bool of bool (* tag 1 *) + | String of string [@unboxed] (* tag String_tag = 252 *) + + With the native-code compiler, the Switcher + will cluster the cases into two dense clusters + and generate good code. But in bytecode, the compiler + will always produce a single Switch instruction, + generating a switch of around 256 cases, which is wasteful. + + We are not sure how to generate better code + -- for example, generating a test for tags above 245 + may duplicate the computation of the value tag. + *) + | None -> (* single_nonconst_act is None, so there must be at least two distinct non-constant actions, From 8d1058a8d6be274d042c829ea59c50e96239c35d Mon Sep 17 00:00:00 2001 From: Gabriel Scherer Date: Tue, 13 Jul 2021 15:27:23 +0200 Subject: [PATCH 15/45] a TODO item with a concrete proposal for more compact bytecode --- lambda/matching.ml | 12 ++++++++++++ 1 file changed, 12 insertions(+) diff --git a/lambda/matching.ml b/lambda/matching.ml index f4a1b10bb022..eab109559b66 100644 --- a/lambda/matching.ml +++ b/lambda/matching.ml @@ -3026,6 +3026,18 @@ let combine_constructor loc arg pat_env cstr partial ctx def We are not sure how to generate better code -- for example, generating a test for tags above 245 may duplicate the computation of the value tag. + + TODO: try the following strategy: here (in this function), + if we detect that max_block_tag is above 245, generate either + + if isint v then + + else let n = Obj.tag v in + + + This should generate slower bytecode, but much more compact bytecode. + (slower: typically 2-4 instructions executed instead of 1) + (more compact: typically ~10 integers instead of ~256) *) | None -> From aa6192afa51d61dd44664239ade64a42dccaa011 Mon Sep 17 00:00:00 2001 From: Nicolas Chataing Date: Tue, 13 Jul 2021 18:57:16 +0200 Subject: [PATCH 16/45] Compile switch with a Pisint if the any_const case action is Some. --- lambda/matching.ml | 77 +++++++++++++++++++++++++++++----------------- 1 file changed, 49 insertions(+), 28 deletions(-) diff --git a/lambda/matching.ml b/lambda/matching.ml index eab109559b66..97455185368a 100644 --- a/lambda/matching.ml +++ b/lambda/matching.ml @@ -2944,7 +2944,8 @@ let combine_constructor loc arg pat_env cstr partial ctx def | _, Some a, _ -> Some a | None, None, nonconsts -> same_actions nonconsts | Some _, None, cases -> - (* if any_case is None, complete_case_count must be Some *) + (* if any_case is None, complete_case_count + must be Some *) let count = Option.get complete_case_count in if List.length cases = count then same_actions cases @@ -2974,8 +2975,8 @@ let combine_constructor loc arg pat_env cstr partial ctx def better code than a switch in some cases, but for tests on non-constant constructors we prefer to always emit a switch, as bytecode implements this sophisticated instruction. *) - match single_nonconst_act with - | Some nonconst_act -> + match single_nonconst_act, cases.any_const with + | Some nonconst_act, _ -> (* Note: we already checked that not all actions are identical, so the constant-constructor actions cannot be empty. *) @@ -2985,24 +2986,18 @@ let combine_constructor loc arg pat_env cstr partial ctx def | None -> call_switcher loc fail_opt arg 0 (n - 1) cases.consts in test_isint int_actions nonconst_act - | None -> - let fail_opt = - match fail_opt, cases.any_const with - | None, None -> None - | Some a, None - | None, Some a -> - Some a - | Some fail_act, Some a -> - Some (test_isint a fail_act) - in - (* Switch is a low-level control-flow construct that must handle - an interval of contiguous values (on both domains); [sw_numconsts] - and [sw_numblocks] correspond to the size of this interval, - from 0 to the maximum head value + 1. *) + | None, None -> + (* Switch is a low-level control-flow construct that must + handle an interval of contiguous values (on + both domains); [sw_numconsts] and [sw_numblocks] + correspond to the size of this interval, from 0 to the + maximum head value + 1. *) let sw_numconsts = match Typedecl.cstr_max_imm_value pat_env cstr with | Some n -> n + 1 - | None -> 1 (* XXX TODO *) + | None -> + (* cases.any_const is None *) + assert false in let sw_numblocks = match Typedecl.cstr_max_block_tag pat_env cstr with @@ -3015,34 +3010,39 @@ let combine_constructor loc arg pat_env cstr partial ctx def type t = | Unit of unit (* tag 0 *) | Bool of bool (* tag 1 *) - | String of string [@unboxed] (* tag String_tag = 252 *) + | String of string [@unboxed] + (* tag String_tag = 252 *) With the native-code compiler, the Switcher will cluster the cases into two dense clusters and generate good code. But in bytecode, the compiler will always produce a single Switch instruction, - generating a switch of around 256 cases, which is wasteful. + generating a switch of around 256 cases, which is + wasteful. We are not sure how to generate better code -- for example, generating a test for tags above 245 may duplicate the computation of the value tag. - TODO: try the following strategy: here (in this function), - if we detect that max_block_tag is above 245, generate either + TODO: try the following strategy: here (in + this function), if we detect that max_block_tag is + above 245, generate either if isint v then - + else let n = Obj.tag v in - This should generate slower bytecode, but much more compact bytecode. - (slower: typically 2-4 instructions executed instead of 1) - (more compact: typically ~10 integers instead of ~256) + This should generate slower bytecode, but much more + compact bytecode. (slower: typically 2-4 instructions + executed instead of 1) (more compact: typically + ~10 integers instead of ~256) *) | None -> - (* single_nonconst_act is None, so there must be at least - two distinct non-constant actions, + (* single_nonconst_act is None, so there must be at + least two distinct non-constant actions, any_nonconst is impossible. *) assert false in @@ -3057,6 +3057,27 @@ let combine_constructor loc arg pat_env cstr partial ctx def let hs, sw = share_actions_sw sw in let sw = reintroduce_fail sw in hs (Lswitch (arg, sw, loc)) + | None, Some const_act -> + (* Generate a switch on nonconst_act under a Pisint test + to handle the any_const action *) + let sw_numblocks = + match Typedecl.cstr_max_block_tag pat_env cstr with + | Some n -> n + 1 + | None -> assert false (* same as above *) + in + let nonconst_act = + Lswitch + ( arg, + { sw_numconsts = 0; + sw_consts = []; + sw_numblocks; + sw_blocks = cases.nonconsts; + sw_failaction = fail_opt; + }, + loc + ) + in + test_isint const_act nonconst_act ) ) in From 75330c0acf9044a99ac86bf3c9e7c2284b26dbbf Mon Sep 17 00:00:00 2001 From: Gabriel Scherer Date: Wed, 14 Jul 2021 06:46:25 +0200 Subject: [PATCH 17/45] refactoring commit --- lambda/matching.ml | 159 +++++++++++++++++++++------------------------ 1 file changed, 73 insertions(+), 86 deletions(-) diff --git a/lambda/matching.ml b/lambda/matching.ml index 97455185368a..05422de3a309 100644 --- a/lambda/matching.ml +++ b/lambda/matching.ml @@ -2970,82 +2970,90 @@ let combine_constructor loc arg pat_env cstr partial ctx def Lifthenelse ( Lprim (Pisint, [ arg ], loc), const_act, nonconst_act ) in - (* We check specifically for single_nonconst_act, not for - single_const_act: for constant constructors we can generate + (* Remark: for constant constructors we can generate better code than a switch in some cases, but for tests on non-constant constructors we prefer to always emit a switch, as bytecode implements this sophisticated instruction. *) - match single_nonconst_act, cases.any_const with - | Some nonconst_act, _ -> - (* Note: we already checked that not all actions are - identical, so the constant-constructor actions cannot - be empty. *) - let int_actions = - match single_const_act with - | Some const_act -> const_act - | None -> - call_switcher loc fail_opt arg 0 (n - 1) cases.consts - in test_isint int_actions nonconst_act + match single_const_act, single_nonconst_act with + | Some const_act, Some nonconst_act -> + test_isint const_act nonconst_act + | None, Some nonconst_act -> + let const_act = + (* Note: we already checked that not all actions are the same, + so cases.consts cannot be empty. *) + call_switcher loc fail_opt arg 0 (n - 1) cases.consts in + test_isint const_act nonconst_act + | Some const_act, None -> + let nonconst_act = + let max_block_tag = + Typedecl.cstr_max_block_tag pat_env cstr in + let sw_numblocks = + (* if single_const_act is None, + then any_const must be None, so + cstr_max_block_tag is Some. *) + Option.get max_block_tag + 1 in + Lswitch + ( arg, + { sw_numconsts = 0; + sw_consts = []; + sw_numblocks; + sw_blocks = cases.nonconsts; + sw_failaction = fail_opt; + }, + loc + ) + in + test_isint const_act nonconst_act | None, None -> (* Switch is a low-level control-flow construct that must handle an interval of contiguous values (on both domains); [sw_numconsts] and [sw_numblocks] correspond to the size of this interval, from 0 to the maximum head value + 1. *) + let max_imm_value = + Typedecl.cstr_max_imm_value pat_env cstr in + let max_block_tag = + Typedecl.cstr_max_block_tag pat_env cstr in let sw_numconsts = - match Typedecl.cstr_max_imm_value pat_env cstr with - | Some n -> n + 1 - | None -> - (* cases.any_const is None *) - assert false - in + Option.get max_imm_value + 1 in let sw_numblocks = - match Typedecl.cstr_max_block_tag pat_env cstr with - | Some n -> - n + 1 - (* Remark: in presence of constructor unboxing, - some block tags may be above - Obj.last_non_constant_constructor_tag (245): - - type t = - | Unit of unit (* tag 0 *) - | Bool of bool (* tag 1 *) - | String of string [@unboxed] - (* tag String_tag = 252 *) - - With the native-code compiler, the Switcher - will cluster the cases into two dense clusters - and generate good code. But in bytecode, the compiler - will always produce a single Switch instruction, - generating a switch of around 256 cases, which is - wasteful. - - We are not sure how to generate better code - -- for example, generating a test for tags above 245 - may duplicate the computation of the value tag. - - TODO: try the following strategy: here (in - this function), if we detect that max_block_tag is - above 245, generate either - - if isint v then - - else let n = Obj.tag v in - - - This should generate slower bytecode, but much more - compact bytecode. (slower: typically 2-4 instructions - executed instead of 1) (more compact: typically - ~10 integers instead of ~256) - *) - - | None -> - (* single_nonconst_act is None, so there must be at - least two distinct non-constant actions, - any_nonconst is impossible. *) - assert false - in + Option.get max_block_tag + 1 in + (* Remark: in presence of constructor unboxing, + some block tags may be above + Obj.last_non_constant_constructor_tag (245): + + type t = + | Unit of unit (* tag 0 *) + | Bool of bool (* tag 1 *) + | String of string [@unboxed] + (* tag String_tag = 252 *) + + With the native-code compiler, the Switcher + will cluster the cases into two dense clusters + and generate good code. But in bytecode, the compiler + will always produce a single Switch instruction, + generating a switch of around 256 cases, which is + wasteful. + + We are not sure how to generate better code + -- for example, generating a test for tags above 245 + may duplicate the computation of the value tag. + + TODO: try the following strategy: here (in + this function), if we detect that max_block_tag is + above 245, generate either + + if isint v then + + else let n = Obj.tag v in + + + This should generate slower bytecode, but much more + compact bytecode. (slower: typically 2-4 instructions + executed instead of 1) (more compact: typically + ~10 integers instead of ~256) + *) let sw = { sw_numconsts; sw_consts = cases.consts; @@ -3057,27 +3065,6 @@ let combine_constructor loc arg pat_env cstr partial ctx def let hs, sw = share_actions_sw sw in let sw = reintroduce_fail sw in hs (Lswitch (arg, sw, loc)) - | None, Some const_act -> - (* Generate a switch on nonconst_act under a Pisint test - to handle the any_const action *) - let sw_numblocks = - match Typedecl.cstr_max_block_tag pat_env cstr with - | Some n -> n + 1 - | None -> assert false (* same as above *) - in - let nonconst_act = - Lswitch - ( arg, - { sw_numconsts = 0; - sw_consts = []; - sw_numblocks; - sw_blocks = cases.nonconsts; - sw_failaction = fail_opt; - }, - loc - ) - in - test_isint const_act nonconst_act ) ) in From 5674bfee3b0bd6531a8b4f70a5be0ffe23e4e227 Mon Sep 17 00:00:00 2001 From: Gabriel Scherer Date: Wed, 14 Jul 2021 17:13:28 +0200 Subject: [PATCH 18/45] Revert "refactoring commit" This reverts commit 56dd15e1018883b6a9423a9265185402d4fcb37d. I am not sure about this commit, because it causes the compiler to generate worse bytecode in some cases: if any_const is None but single_const_action is Some, then we will generate a test followed by a switch (in the nonconst case) instead of a single switch. --- lambda/matching.ml | 159 ++++++++++++++++++++++++--------------------- 1 file changed, 86 insertions(+), 73 deletions(-) diff --git a/lambda/matching.ml b/lambda/matching.ml index 05422de3a309..97455185368a 100644 --- a/lambda/matching.ml +++ b/lambda/matching.ml @@ -2970,90 +2970,82 @@ let combine_constructor loc arg pat_env cstr partial ctx def Lifthenelse ( Lprim (Pisint, [ arg ], loc), const_act, nonconst_act ) in - (* Remark: for constant constructors we can generate + (* We check specifically for single_nonconst_act, not for + single_const_act: for constant constructors we can generate better code than a switch in some cases, but for tests on non-constant constructors we prefer to always emit a switch, as bytecode implements this sophisticated instruction. *) - match single_const_act, single_nonconst_act with - | Some const_act, Some nonconst_act -> - test_isint const_act nonconst_act - | None, Some nonconst_act -> - let const_act = - (* Note: we already checked that not all actions are the same, - so cases.consts cannot be empty. *) - call_switcher loc fail_opt arg 0 (n - 1) cases.consts in - test_isint const_act nonconst_act - | Some const_act, None -> - let nonconst_act = - let max_block_tag = - Typedecl.cstr_max_block_tag pat_env cstr in - let sw_numblocks = - (* if single_const_act is None, - then any_const must be None, so - cstr_max_block_tag is Some. *) - Option.get max_block_tag + 1 in - Lswitch - ( arg, - { sw_numconsts = 0; - sw_consts = []; - sw_numblocks; - sw_blocks = cases.nonconsts; - sw_failaction = fail_opt; - }, - loc - ) - in - test_isint const_act nonconst_act + match single_nonconst_act, cases.any_const with + | Some nonconst_act, _ -> + (* Note: we already checked that not all actions are + identical, so the constant-constructor actions cannot + be empty. *) + let int_actions = + match single_const_act with + | Some const_act -> const_act + | None -> + call_switcher loc fail_opt arg 0 (n - 1) cases.consts + in test_isint int_actions nonconst_act | None, None -> (* Switch is a low-level control-flow construct that must handle an interval of contiguous values (on both domains); [sw_numconsts] and [sw_numblocks] correspond to the size of this interval, from 0 to the maximum head value + 1. *) - let max_imm_value = - Typedecl.cstr_max_imm_value pat_env cstr in - let max_block_tag = - Typedecl.cstr_max_block_tag pat_env cstr in let sw_numconsts = - Option.get max_imm_value + 1 in + match Typedecl.cstr_max_imm_value pat_env cstr with + | Some n -> n + 1 + | None -> + (* cases.any_const is None *) + assert false + in let sw_numblocks = - Option.get max_block_tag + 1 in - (* Remark: in presence of constructor unboxing, - some block tags may be above - Obj.last_non_constant_constructor_tag (245): - - type t = - | Unit of unit (* tag 0 *) - | Bool of bool (* tag 1 *) - | String of string [@unboxed] - (* tag String_tag = 252 *) - - With the native-code compiler, the Switcher - will cluster the cases into two dense clusters - and generate good code. But in bytecode, the compiler - will always produce a single Switch instruction, - generating a switch of around 256 cases, which is - wasteful. - - We are not sure how to generate better code - -- for example, generating a test for tags above 245 - may duplicate the computation of the value tag. - - TODO: try the following strategy: here (in - this function), if we detect that max_block_tag is - above 245, generate either - - if isint v then - - else let n = Obj.tag v in - - - This should generate slower bytecode, but much more - compact bytecode. (slower: typically 2-4 instructions - executed instead of 1) (more compact: typically - ~10 integers instead of ~256) - *) + match Typedecl.cstr_max_block_tag pat_env cstr with + | Some n -> + n + 1 + (* Remark: in presence of constructor unboxing, + some block tags may be above + Obj.last_non_constant_constructor_tag (245): + + type t = + | Unit of unit (* tag 0 *) + | Bool of bool (* tag 1 *) + | String of string [@unboxed] + (* tag String_tag = 252 *) + + With the native-code compiler, the Switcher + will cluster the cases into two dense clusters + and generate good code. But in bytecode, the compiler + will always produce a single Switch instruction, + generating a switch of around 256 cases, which is + wasteful. + + We are not sure how to generate better code + -- for example, generating a test for tags above 245 + may duplicate the computation of the value tag. + + TODO: try the following strategy: here (in + this function), if we detect that max_block_tag is + above 245, generate either + + if isint v then + + else let n = Obj.tag v in + + + This should generate slower bytecode, but much more + compact bytecode. (slower: typically 2-4 instructions + executed instead of 1) (more compact: typically + ~10 integers instead of ~256) + *) + + | None -> + (* single_nonconst_act is None, so there must be at + least two distinct non-constant actions, + any_nonconst is impossible. *) + assert false + in let sw = { sw_numconsts; sw_consts = cases.consts; @@ -3065,6 +3057,27 @@ let combine_constructor loc arg pat_env cstr partial ctx def let hs, sw = share_actions_sw sw in let sw = reintroduce_fail sw in hs (Lswitch (arg, sw, loc)) + | None, Some const_act -> + (* Generate a switch on nonconst_act under a Pisint test + to handle the any_const action *) + let sw_numblocks = + match Typedecl.cstr_max_block_tag pat_env cstr with + | Some n -> n + 1 + | None -> assert false (* same as above *) + in + let nonconst_act = + Lswitch + ( arg, + { sw_numconsts = 0; + sw_consts = []; + sw_numblocks; + sw_blocks = cases.nonconsts; + sw_failaction = fail_opt; + }, + loc + ) + in + test_isint const_act nonconst_act ) ) in From e4c7ccc7688c6a41eda8bc5c9d3f157634495f0a Mon Sep 17 00:00:00 2001 From: Gabriel Scherer Date: Wed, 25 Aug 2021 18:06:22 +0200 Subject: [PATCH 19/45] RAEDME.head_shape.md: prepare a description for PR submission --- README.head_shape.md | 152 +++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 152 insertions(+) create mode 100644 README.head_shape.md diff --git a/README.head_shape.md b/README.head_shape.md new file mode 100644 index 000000000000..aa6359371d37 --- /dev/null +++ b/README.head_shape.md @@ -0,0 +1,152 @@ +# Constructor unboxing: PR description + +This PR implements a variant of the "constructor unboxing" feature proposed by Jeremy Yallop in [RFC #14](https://github.com/ocaml/RFCs/pull/14), which extends the current `[@@unboxed]` annotation for single-constructor variant types (or single-field record types). The PR was implemented by @nchataing during an internship supervised by @gasche. + +## Short example + +The following is now accepted: + +``` +type bignum = + | Short of int [@unboxed] (* represented directly by an integer *) + | Long of Gmp.t (* Block of tag 0 (first non-unboxed constructor) *) +``` + +In a [small benchmark](https://github.com/gasche/ocaml/pull/10), we tested that this representation provides the same performances as the current Zarith implementation when computations remain in the "short integer" range -- Zarith uses [dirty unsafe tricks](https://github.com/ocaml/Zarith/blob/2be3c25/z.ml#L28-L37) to avoid boxing short integers, which we can replace with [natural OCaml code](https://github.com/gasche/ocaml/blob/head_shape_zarith/Zarith/test.ml#L110-L125). + +(Note: Zarith does not box the Long case either, checking for a Custom tag instead. We do not support this yet, but it would be a natural extension of this PR.) + +The intent of the currently presented work is to do the simplest possible step in the direction of more unboxing. Most advanced aspects were left to future work. We believe that it would be reasonable to integrate the PR with its current feature scope: it provides values for users, and should not hamper further extensions. + + +## Precise specification + +We define the *head* of an OCaml value as follows: +- the head of an immediate value `v` is the pair `(Imm, v)` +- the head of a heap block with tag `t` is the pair `(Block, t)`. + +(In other words, the head tracks whether a value is immediate or a block, and for blocks only keeps the tag.) + +The "head shape" of a type is a (slight over-approximation of) the set of heads of all possible values of this type. + +Now consider a variant type declaration containing one or several constructors annotated with `[@unboxed]`: + +```ocaml +type ('a, 'b, ...) t = + | Const0 (* some constant constructors *) + | Const1 + | ... + | Const{m} + | NonConst0 of t00 * t01 * ... + | Nonconst1 of t10 * t11 * ... + | ... + | NonConst{n} of t{n}0 * t{n}1 * ... + | Unboxed1 of u0 [@unboxed] + | Unboxed2 of u1 [@unboxed] + | ... + | Unboxed{l} of u{l} [@unboxed] +``` + +(For simplicity we wrote above all constant constructors first, then all non-constant constructors then all unboxed constructors. But in fact we support arbitrary interleaving of these categories, and the representation is exactly the same as long as the ordering within constant constructors and within non-constant constructors is preserved.) + +The compiled representation of this type is as follows: +- as before, constant constructors `Const{k}` are represented by the immediate number `k` +- as before, non-constant constructors `Nonconst{k} of ...` are represented by a heap block with tag `k` +- unboxed constructors `Unboxed{k} of u{k}` are represented directly by the value of type `u{k}`, without + any boxing + +This definition is *rejected* statically if the unboxed constructors overlap with the other values of the type, in the following precise sense: + +1. We compute the "boxed head shape" `BS` of this type *without* the unboxed constructors; by definition of the head shape, this is the set `{(Imm, 0), (Imm, 1), ..., (Imm, m)} ∪ {(Block, 0), (Block, 1), ,.., (Block, n)}`. + +2. Then we compute the "unboxed shapes" `US{k}` of each unboxed constructor, that is the head shape of `u{k}`. + +3. The type is accepted if and only if the shapes `BS, US0, US1, ..., US{l}` are disjoint from each other. The head shape of the whole shape is then the disjoint union `BS ⊎ US0 ⊎ US1 ⊎ ... ⊎ US{l}`. + +Unknown/abstract types are assumed to have a "top" shape with containing potentially all heads. (This should be refined when the abstract type is used to represent an FFI type with a precise shape implemented in C; supporting head shape assertions on abstract types is future work.) + +### Examples + +```ocaml +(* rejected *) +type t = + | Int of int [@unboxed] (* shape: (Imm, _) *) + | Unit (* shape: (Imm, 0), conflicts with Int above *) + +(* accepted *) +type t = + | Int of int [@unboxed] (* shape: (Imm, _) *) + | Box of t (* shape: (Block, 0), as the first non-constant non-unboxed constructor *) + (* shape(t): (Imm, _) ∪ {(Block, 0)} *) + +(* accepted *) +type prod = t * t +and t = + | Int of int [@unboxed] (* shape: (Imm, _): any immediate *) + | String of string [@unboxed] (* shape: (Block, Obj.string_tag) (Obj.string_tag is 252) *) + | Prod of prod [@unboxed] (* shape: (Block, 0) *) + (* shape(t): (Imm, _) ∪ {(Block, 0), (Block, Obj.string_tag)} *) + + +(** With abstract types *) + +type abstract + +(* accepted *) +type t = + | Int of int [@unboxed] (* shape: (Imm, _) *) + | Abs of abstract (* shape: (Block, 0) *) + (* shape(t): (Imm, _) ∪ {(Block, 0)} *) + +(* rejected *) +type t = + | Int of int (* shape: (Block, 0) *) + | Abs of abstract [@unboxed] (* any shape, conflicts with Int *) + + +(** Nested unboxing *) + +type t1 = + | Int of int [@unboxed] + | Block of unit + (* shape(t1): (Imm, _) ∪ {(Block, 0)} *) + +(* rejected *) +type t2 = + | T1 of t1 [@unboxed] (* shape: (Imm, _) ∪ {(Block, 0)} *) + | S of string (* shape: (Block, 0), conflicts with T1 *) + +(* accepted *) +type t3 = + | T1 of t1 [@unboxed] (* shape: {(Imm, _), (Block, 0)} *) + | S of string [@unboxed] (* shape: (Block, Obj.stringₜag) *) + (* shape(t3): (Imm, _) ∪ {(Block, 0)} ∪ {(Block, Obj.string_tag)} *) +``` + + +### Comparison with Yallop's proposal [RFC#14](https://github.com/ocaml/RFCs/pull/14) + +Jeremy Yallop's proposal uses a global annotation `[@@unboxed]` on all constructors at once, we use a per-constructor annotation `[@unboxed]`. (The RFC mentions this as a possible extension in "Extension: partial unboxing".) It would be easy to interpret `[@@unboxed]` as just "[@unboxed] on all constructors", but we have not implemented this yet. + +A major difference is that the RFC#14 specification suggests renumbering constructors in some cases, where the representation of `C of foo [@unboxed]` is taken to be different from the representation of `foo`, in order to avoid conflicts with other constructors at this type. We do not support any such renumbering: +- the representation of `Unboxed of foo [@unboxed]` is always the representation of `foo` +- the representation of `Boxed of foo` always uses the block tag consecutive/next/succedent to the previous boxed-constructor tag in the declaration (filtering out unboxed constructors). + +(Note: @stedolan calls this aspect of RFC#14 "[conflating inlining and disjointness](https://github.com/ocaml/RFCs/pull/14#issuecomment-603867960)". We only deal with disjointness.) + + +## Implementation strategy + +TODO: explain how/when we compute head-shape information. + +### Pointers for code review + +TODO: point at various places in the codebase + +## In scope for this PR, but not yet implemented + +TODO: explain that we want to get the review train rolling, but that there is still stuff missing before this can be merged. + +## Future work + +TODO: things we know about but that we do *not* want in this PR. From 4c669570a588c75d794586a8f4644514e69be6bf Mon Sep 17 00:00:00 2001 From: Gabriel Scherer Date: Thu, 26 Aug 2021 11:42:53 +0200 Subject: [PATCH 20/45] PR description: describe the implementation --- README.head_shape.md | 300 ++++++++++++++++++++++++++++++++++++++++++- 1 file changed, 293 insertions(+), 7 deletions(-) diff --git a/README.head_shape.md b/README.head_shape.md index aa6359371d37..6591d10544c2 100644 --- a/README.head_shape.md +++ b/README.head_shape.md @@ -1,4 +1,4 @@ -# Constructor unboxing: PR description +# Constructor unboxing This PR implements a variant of the "constructor unboxing" feature proposed by Jeremy Yallop in [RFC #14](https://github.com/ocaml/RFCs/pull/14), which extends the current `[@@unboxed]` annotation for single-constructor variant types (or single-field record types). The PR was implemented by @nchataing during an internship supervised by @gasche. @@ -34,7 +34,7 @@ Now consider a variant type declaration containing one or several constructors a ```ocaml type ('a, 'b, ...) t = | Const0 (* some constant constructors *) - | Const1 + | Const1 | ... | Const{m} | NonConst0 of t00 * t01 * ... @@ -134,19 +134,305 @@ A major difference is that the RFC#14 specification suggests renumbering constru (Note: @stedolan calls this aspect of RFC#14 "[conflating inlining and disjointness](https://github.com/ocaml/RFCs/pull/14#issuecomment-603867960)". We only deal with disjointness.) +### Leftover question: how close to the compiler-distribution runtime should the specification be? + +We define static accept/reject decisions for partially-unboxed types using "head shapes", which are defined in terms of the value-representation strategy of the main OCaml implementation. Should we have a more abstract definition, that leaves more room to other representations in alternative implementations? + +We have not studied this question yet and we believe it is a pressing question. In particular, any choice that would end up being merged in the language probably MUST support the js_of_ocaml value representation. (Do you know of a reference document that describes the js_of_ocaml value representation? Pointers are welcome are we are not jsoo experts ourselves. cc @hhugo.) + +Our intuition is that we could fine a "weakening" of our current specification that distinguishes less different sort of shapes -- thus rejects more definitions -- and gives good flexibility for alternative implementations. Here are some things we could do: + +- We could stop making assumptions about the shape of function closures (currently: {Closure_tag, Infix_tag}), preventing the unboxing of closure-holding constructors. +- We could also weaken our assumptions about built-in containers (string/byte, arrays, double-arrays, etc.) +- We could stop distinguishing "float" from immediates (ouch!) if jsoo does this. What about Int32, Int64, should they be known as custom values? + +In other words: what amount of runtime type information should we require from OCaml implementations? + +At the limit, one extreme choice would be to only reason on the tag of variant constructors (constant or not), which are distinguishable from each other in any OCaml implementation, and not make any other assumption about head shapes (map all types except variants to the "top" shape). This would reject most unboxing definitions, leave maximal freedom for langauge implementations. Unfortunately this would also prevent the actually-interesting uses of the feature we know about, which mostly resolve around unboxing an `int`-carrying constructor. + +This is an aspect of our design on which we need external feedback from people with a good taste for these matters. (cc @xavierleroy, @damiendoligez, @stedolan, @lpw25, @let-def, etc.). + ## Implementation strategy -TODO: explain how/when we compute head-shape information. +The main components required for this feature are: +1. We need to compute head shape information for unboxed constructors, which in turn requires computing head shape information for whole type. +2. At type-declaration time, we need to check disjointness of head shapes and reject invalid declarations. +3. We need to compile unboxed constructors in expressions. +4. We need to compile unboxed constructors in patterns. + +(3) is in fact very easy: unboxed constructors in expressions are implemented by doing [nothing at all](https://github.com/gasche/ocaml/blob/head_shape/lambda/translcore.ml#L336-L337). + +(1) and (2) proved fairly difficult to implement cleanly due in large part to accidental complexity. + +### Head shapes + +Representing head shapes by their set of possible values is not practical, as `(Imm, _)` (the shape of all immediate values) would be too large a set. Instead we use a representation with an explicit "any" value in either domains (for immediates or for tags): + +``` +(* Over-approximation of the possible values of a type, + used to verify and compile unboxed head constructors. + + We represent the "head" of the values: their value if + it is an immediate, or their tag if is a block. + A head "shape" is a set of possible heads. +*) +and head_shape = + { head_imm : imm shape; (* set of immediates the head can be *) + head_blocks : tag shape; (* set of tags the head can have *) + } + +(* A description of a set of ['a] elements. *) +and 'a shape = + | Shape_set of 'a list (* An element among a finite list. *) + | Shape_any (* Any element (Top/Unknown). *) + +and imm = int +and tag = int +``` + +TODO: turn Imm and Tag into one-constructor types + +This definition is found in typing/types.mli: https://github.com/gasche/ocaml/blob/head_shape/typing/types.mli#L624-L642 + +Remark: in practice we don't know of any use type in OCaml that contains the `(Block, _)` shape without also allowing `(Imm, _)`. (So we could do without `(Block, _)` and have two tops, "any immediate" or "any value whatsoever") No type describes "any block but not immediates". Allowing it in the compiler implementation makes the code more regular, and it could come handy in the future (if we wanted, say, to assign shapes to Cmm-level types) or for weird FFI projects. + +### Compiling unboxed constructors in pattern-matching + +Pattern-matching compilation is done in [lambda/matching.ml](https://github.com/gasche/ocaml/blob/head_shape/lambda/matching.ml). + +Remark: The other pattern-matching-heavy module, [typing/parmatch.ml](https://github.com/gasche/ocaml/blob/head_shape/typing/parmatch.ml), is in charge of checking for exhaustiveness and other type-checking-time warnings; it required basically no change, given that unboxing a constructor does not change the observable behavior of pattern-matching, unboxed constructors are handled just like usual constructors for exhaustiveness and all other static-analysis purpose. + +The pattern-matching compiler works by decomposing pattern-matching clauses into a lower-level representation built from "switches", a lower-level control-flow construct that just dispatches on the value of immediates and tags of a head block. Those switches are then lowered further to Lambda constructs (`Lifthenelse` + tag accesses, or a native `Lswitch` instruction used for the bytecode compiler). + +A switch is a list of switch clauses, which are of the form `(cstr_tag, action)`, where `cstr_tag` is either an immediate value or a block tag, and actions are pieces of lambda-code. Our implementation adds a new sort of `cstr_tag`, morally `Cstr_unboxed of head_shape` (representation details in the next section); these "unboxed tags" are "expanded away" by replacing clauses witch unboxed tags by clauses for the underlying elements of the head shape. + +For example, consider the following type declarations: + +```ocaml +type internal = Foo | Bar of string [@unboxed] (* head shape: {(Imm, 0); (Block, 252)} *) +type t = First of int | Second of internal [@unboxed] +``` + +An exhaustive switch on a value of type `t` may look like + +```ocaml +| Cstr_block 0 -> act1 +| Cstr_unboxed [{(Imm, 0); (Block, 252)}] -> act2) +``` + +and we expand it to a switch without unboxed constructors, to be compiled by the existing machinery: + +```ocaml +| Cstr_block 0 -> act1 +| Cstr_constant 0 -> act2 +| Cstr_block 252 -> act2 +``` + +This is the general idea, but in fact we need slightly more sophistication to deal with `(Imm, _)` or `(Block, _)` shapes. Instead of a list of clauses, we represent a switch as a product structure which may contain: +- an action for all immediates (the `any_const` action) +- or a list of specific actions for some immediates +- an action for all blocks (the `any_nonconst` action) +- or a list of specific actions for some block tags + +TODO: writing this explanation, I really have the impression that we should try again to use a sum type to clarify that we either have `any` or some immediates. This makes `split_cases` harder to write, but the consumer easier to read, and the consumer is more important here -- it is the subtle piece of code that does the pattern-matching compilation of those switches. + +The code that lowers switches into `Lifthenelse` or `Lswitch` has to be adapted to deal with this new structure. If We changed the code in such a way that it should be easy to check that, in absence of unboxed constructors, the code generated is the same as it was previously. (The cost of this approach is that sometimes the code is more verbose / less regular than it could be if written from scratch, accepting some changes in compilation.) + +Remark: To emit `Lswitch` instructions, the compiler needs to know of the range of possible immediate values and tags (when we don't have `any_{const,nonconst}` actions). More precisely, we want the maximal possible immediate constructor and block tag at this type (minimal values are always assumed to be 0). + +This new representation of switches with "any immediate" or "any block tag" cases is in a new `Cases` submodule: +https://github.com/gasche/ocaml/blob/head_shape/lambda/matching.ml#L2738-L2790 + +The expansion of unboxed constructors in switches is performed in the `split_cases` function: +https://github.com/gasche/ocaml/blob/head_shape/lambda/matching.ml#L2792-L2827 + +Finally, the lowering of those switches to Lambda code is done in the `combine_constructor` function: +https://github.com/gasche/ocaml/blob/head_shape/lambda/matching.ml#L2914-L3080 + + +### General approach to computing head shapes + +We use the "on-demand" approach advertised by @lpw25 and @stedolan to compute type properties on-demand, at each type declaration with unboxed constructors, instead of trying to compute the property modularly for all type definitions (which may or may not occur in the type of an unboxed constructor later). + +Here "demand" is defined as either: +- a type declaration using some unboxed constructors is processed by the type-checker + (this "demands" computing the shape of each unboxed constructor) +- the pattern-matching compiler encounters an unboxed constructor + +In particular, it can happen that an unboxed-constructor is compiled *without* the type-checker having processed its declaration first! This is the case where the type declaration comes from a .cmi – it has been checked by a previous run of the compiler, and is then imported as-is into the environment without being re-checked. + +The head shape computed for an unboxed constructor is cached on first demand, and will not be recomputed several times. The computation requires a typing environment -- which must be an extension of the environment in which the constructor was defined -- to unfold the definition of typing constructors used in the unboxed constructor parameter type, and further constructions reachable from them. + +The details of how we perform repeated expansion of type constructors while ensuring termination are tricky, they are discussed in [this ML Workshop extended abstract](http://gallium.inria.fr/~scherer/research/constructor-unboxing/constructor-unboxing-ml-workshop-2021.pdf) and [PR #10479](https://github.com/ocaml/ocaml/pull/10479). + +The computation of the head shape is done in the functions `of_type_expr` and `of_typedescr` in a new `Head_shape` module of [typing/typedecl_unboxed.ml](https://github.com/gasche/ocaml/blob/head_shape/typing/typedecl_unboxed.ml). + +In particular, the definition of head shape on "base types" relies on a [`match_primitive`](https://github.com/gasche/ocaml/blob/head_shape/typing/typedecl_unboxed.ml#L65) function recognized a set of builtin type paths (we borrowed the logic from [Typeopt.classify](https://github.com/gasche/ocaml/blob/head_shape/typing/typeopt.ml#L75)). + +TODO: an auxiliary function `of_primitive_type` would help describe where to find the mapping from `primitive_type` to head shapes. +TODO: there is no special support for `Tarrow` for now, it returns `any_shape` instead of {Closure,Infix}. (Is it by explicit choice?) + + +### Storing unboxing information in type descriptions + +This, surprisingly, turned out to be the most difficult part of the PR to get right. + +As discussed above, we need to store two different kind of information for compilation: +- per-unboxed-constructor information: what is the shape of the unboxed constructor argument +- per-sum-type information: how many unboxed constructors are there, + what is the maximal value of the immediates and block tags they contain + +The existing codebase already computes per-constructor information (imm/tag values) and per-sum-type information (the number of constant and non-constant constructors) in [typing/datarepr.ml : constructor_descrs](https://github.com/gasche/ocaml/blob/head_shape_base/typing/datarepr.ml#L95). This function is called (through `Datarepr.constructors_of_type`) from the `Env` module, which is in the business of converting type *declarations* (as provided by the user) into type *descriptions* (with extra information for compilation) as stored in the typing environment. -### Pointers for code review +Unfortunately, this scheme cannot be extended for our unboxing-related information. Computing the head shape of an unboxed constructor requires unfolding type constructors from the typing environment, so in particular the function doing the computation needs an Env.t argument and depends on the Env module. It cannot be put in the module Datarepr that itself is called from Env, as this would be create a circular dependency. -TODO: point at various places in the codebase +We tried many ways to avoid this cyclic dependency (for example we went half-way through large refactorings trying to compute type descriptions in Typedecl, and pass it to Env-extending functions, instead of computing them within Env). + +In the end we settled on a very simple approach: the per-unboxed-constructor information has type `head_shape option ref`, and the per-sum-type information has type `unboxed_type_data option ref`, they are initialized to `ref None` by the Datarepr module, and then filled on-demand -- from a module that *can* depend on Env. Caching the on-demand computation is hidden under accessor-style functions (that fills the cache if the value was not computed yet): +- per-unboxed-constructor information are accessed using [Typedecl_unboxed.Head_shape.get](https://github.com/gasche/ocaml/blob/head_shape/typing/typedecl_unboxed.ml#L398); it is also computed and cached for all unboxed constructors of a given type by [Typedecl_unboxed.Head_shape.check_typedecl]. +- per-sum-type information is placed in an `unboxed_type_data option ref` [field](https://github.com/gasche/ocaml/blob/head_shape/typing/types.mli#L592) of the `Types.constructor_description` type -- we sheepishly extended the dubious existing approach of storing per-sum-type information in each of its constructors. It is computed by [Typedecl_unboxed.unboxed_type_data_of_shape](https://github.com/gasche/ocaml/blob/head_shape/typing/typedecl_unboxed.ml#L347). + +Note: the `unboxed_type_data option ref` field is not meant to be accessed directly, but through helper functions in Typedecl, that export its content as fields: + +```ocaml +cstr_max_block_tag : Env.t -> constructor_description -> Types.tag option +cstr_max_imm_value : Env.t -> constructor_description -> Types.imm option +cstr_unboxed_numconsts : Env.t -> constructor_description -> int option +cstr_unboxed_numnonconsts : Env.t -> constructor_description -> int option +``` + +Morally those are fields of a constructor description; the main difference is that, unlike other fields, they can only be computed "later than Datarepr", when a typing environment is available. We first tried having each of them be a mutable field, but this made it difficult to give a type to a function computing all of them at once, as [unboxed_type_data_of_shape] does. + +## Testing + +TODO: describe our testing approach and testsuite ## In scope for this PR, but not yet implemented -TODO: explain that we want to get the review train rolling, but that there is still stuff missing before this can be merged. +We are submitting this PR in the interest of gathering feedback, and getting the review train rolling. (We know it takes a while from people reading about the work to actually reviewing it. Please start right now!) There are still a few things *we* want to changes before we consider it mergeable -- and surely other suggestions from the reviewers. + + +### Handle cyclic types in the termination checker + +The termination-checking algorithm currently does not take cyclic +types into account, and may non-terminate on those. This should be +fixed easily by keeping track of the set of type nodes we have already +encountered in head position during reduction. + + +### Distinguish "good" from "bad" cycles + +Our cycle-detection algorithm will sometimes reject definitions that indeed are cyclic, but do admit a valid fixpoint: + +``` +(* this bad declaration should be rejected *) +type t = Loop of t [@unboxed] | Other +(* because `Other` and `Loop Other` would have the same representation *) + +(* this weird declaration could be accepted +type t = Loop of t [@unboxed] +(* because it is just an empty type *) +``` + +"Good cycle" types have no value of their own and they can go to hell as far as we are concerned. However, Stephen Dolan (@stedolan) pointed out that they can be introduced by revealing the definition of an abstract type: `type t = Loop of abstract [@unboxed]` (accepted, even though we could have `abstract = t`). This introduces a case where revealing type abstractions makes a definition rejected, breaking some reasonable properties of the type system. + +It would be nice to put in the work to distinguish "good cycles" from "bad cycles" to avoid this small defect of the current strategy of rejecting *all* cycles. + + +### TODO enforce "separability" of resulting types + +It is unsound in presence of the flat-float-array optimization to have types that contain both floating-point values and non-floating-point values. Our current approach does not enforce this, so it will allow this unsound definition: + +```ocaml +type t = Float of float [@unboxed] | Other +``` + +The simplest possible idea to solve this is to give `float` the "top" shape (instead of Double_tag), which should reject all such definitions. (But the error message will be disappointing.) + +A more elaborate fix to this issue is to add to the head shape a boolean flag, "separated". A "separated" shape guarantees that it is the over-approximation of a separable type, while a non-separated shape may be the shape of a non-separated type. So for example we have a "Separated Top" value (which can be inhabited by any value, but either contains float and nothing else or no floats) and a "Non-separated top" value (any value, possibly floats and other stuff at the same time). It may be possible to compute this bit simply by giving existential variables in GADTs the "non-separated top" shape, and then to reject all non-separated type declarations. This would allow removing the current separability-computation machinery, which could bring a substantial simplification of this corner of the type-checker. + + ## Future work -TODO: things we know about but that we do *not* want in this PR. +We know about some improvements that we are interested in working on eventually, but we believe are out of scope for this PR. + +### Nice shape-conflict error messages + +If a type definition is rejected due to shape conflict, it would be nice to give a clear explanation to the user, with the location of the two constructors (possibly both in different variant declarations than the one being checked) that introduce the incompatibility. One way to do this is to track, for each part of the shape, the location of the constructor that introduced it in the shape. + +### GADTs + +Finer-grained shape computations for GADTs: to compute the shape of a type `foo t` when `t` is a GADT, instead of taking the disjoint union of the shape of all constructors, we can filter only the constructors that are "compatible" with `foo` (we cannot prove that the types are disjoint). This is simple enough and gives good, interesting results in practice, but it also requires refining the termination-checking strategy for GADTs (in addition to the head type constructor, we need to track the set of compatible constructors for the particular expansion that was done). For now we punt on this by not doing any special handling of GADTs, even though it is less precise. + +### Shape annotations on abstract types + +If an abstract type is meant to be defined through the FFI, the OCaml-side could come with an annotation restricting its shape from the pessimal default "{ (Imm, _); (Block, _) }" to the actual shape of FFI-produced values for this type. This requires blindly trusting the programmer, but this blind trust is the foundation of our FFI model already. + +Having shape annotations on abstract types means that shape-inclusion has to be checked when verifying that a type definition in a module matches a type declaration in its interface. (Currently we don't have any work there, because means of abstractions always either preserve the head shape or turn it into "top".) + +### Compilation strategy + +The pattern-matching compilation strategy could be improved in some cases, at the cost of substantial changes to our current implementation. Consider `type t = Int of int [@unboxed] | String of string [@unboxed] and u = T of t [@unboxed] | Float of float [@unboxed]`. A matching of the form + +```ocaml +match arg with +| Float _ -> 0 +| T (Int _) -> 1 +| T (String _) -> 2 +``` + +will generate two nested switches: + +``` +match-shape arg with +| (Block, Obj.double_tag) -> 0 +| (Imm, _) | (Block, Obj.string_tag) -> + match-shape arg with + | (Imm, _) -> 1 + | (Block, Obj.string_tag) -> 2 +``` + +(This is the exact same generated-code shape that we would have without unboxing, except that one dereference is gone, but the first switch is now more expensive as the now-unboxed input values are not in a small consecutive interval of tags.) + +It would of course be better to generate a single switch instead. We see two approaches to do this: + +1. We could "merge" some switches after the fact. +2. We could remove unboxed constructors much earlier in the pattern-matching compiler, before matrix decomposition, so that morally `T (Int _)` is handled as having a single head constructor `T ∘ Int`. + +We are not considering either of those ambitious changes a priority, because: +1. We expect the performance wins from unboxing (if any) to come from tighter memory representations; + the pattern-matching branches are comparatively unexpansive +2. In practice most examples of unboxed constructors we have in mind do *not* hit this bad situation. + +In particular, if you unboxed a constructor with only immediate +values, then the generated code will split the query space by checking +`Obj.is_int`, which is the optimal strategy in any case (what the +native compiler will do for the merged switch as well). For example, +these produce exactly the same native code: + +```ocaml +(* what we get today *) +match-shape arg with +| (Imm, _) -> -1 +| (Block, 0) | (Block, 1) -> + match-shape arg with + | (Block, 0) -> 0 + | (Block, 1) -> 1 + +(* what switch-merging would give *) +match-shape arg with +| (Imm, _) -> -1 +| (Block, 0) -> 0 +| (Block, 1) -> 1 +``` + +The two forms get compiled to the following + +```ocaml +if Obj.is_int arg then -1 +else match Obj.tag arg with + | 0 -> 0 + | 1 -> 1 +``` \ No newline at end of file From 13548e64945eb89b7f67492eec154b1231ac843d Mon Sep 17 00:00:00 2001 From: Gabriel Scherer Date: Sun, 29 Aug 2021 18:06:48 +0200 Subject: [PATCH 21/45] spec: why we are not turning imm/tag into constructed types --- README.head_shape.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/README.head_shape.md b/README.head_shape.md index 6591d10544c2..4e87e7c51511 100644 --- a/README.head_shape.md +++ b/README.head_shape.md @@ -191,10 +191,10 @@ and imm = int and tag = int ``` -TODO: turn Imm and Tag into one-constructor types - This definition is found in typing/types.mli: https://github.com/gasche/ocaml/blob/head_shape/typing/types.mli#L624-L642 +Remark: we tried turning `imm` and `tag` into single-constructor variants for more safety, but this proved very cumbersome as many auxiliary functions happily process either sorts of tags to compute numeric aggregates. + Remark: in practice we don't know of any use type in OCaml that contains the `(Block, _)` shape without also allowing `(Imm, _)`. (So we could do without `(Block, _)` and have two tops, "any immediate" or "any value whatsoever") No type describes "any block but not immediates". Allowing it in the compiler implementation makes the code more regular, and it could come handy in the future (if we wanted, say, to assign shapes to Cmm-level types) or for weird FFI projects. ### Compiling unboxed constructors in pattern-matching From 678ac93640fa717b011d90a102652a4bffe08f74 Mon Sep 17 00:00:00 2001 From: Gabriel Scherer Date: Sun, 29 Aug 2021 18:10:44 +0200 Subject: [PATCH 22/45] [minor] typedecl_unboxed: refactor into Head_shape.of_primitive_type --- README.head_shape.md | 1 - typing/typedecl_unboxed.ml | 33 ++++++++++++++++++--------------- 2 files changed, 18 insertions(+), 16 deletions(-) diff --git a/README.head_shape.md b/README.head_shape.md index 4e87e7c51511..2418419f0452 100644 --- a/README.head_shape.md +++ b/README.head_shape.md @@ -270,7 +270,6 @@ The computation of the head shape is done in the functions `of_type_expr` and `o In particular, the definition of head shape on "base types" relies on a [`match_primitive`](https://github.com/gasche/ocaml/blob/head_shape/typing/typedecl_unboxed.ml#L65) function recognized a set of builtin type paths (we borrowed the logic from [Typeopt.classify](https://github.com/gasche/ocaml/blob/head_shape/typing/typeopt.ml#L75)). -TODO: an auxiliary function `of_primitive_type` would help describe where to find the mapping from `primitive_type` to head shapes. TODO: there is no special support for `Tarrow` for now, it returns `any_shape` instead of {Closure,Infix}. (Is it by explicit choice?) diff --git a/typing/typedecl_unboxed.ml b/typing/typedecl_unboxed.ml index 4d4709813a74..a56ea08194b1 100644 --- a/typing/typedecl_unboxed.ml +++ b/typing/typedecl_unboxed.ml @@ -187,6 +187,23 @@ module Head_shape = struct | Tpoly (t, _) -> t | _ -> ty + let of_primitive_type = function + | Int -> { head_imm = Shape_any; head_blocks = Shape_set [] } + | Float -> block_shape [Obj.double_tag] + | String + | Bytes -> block_shape [Obj.string_tag] + | Array -> + block_shape + (if Config.flat_float_array then [0] + else [0; Obj.double_array_tag]) + | Floatarray -> block_shape [Obj.double_array_tag] + | Lazy -> any_shape + (* Lazy values can 'shortcut' the lazy block, and thus have many + different tags. When Config.flat_float_array, they + cannot be floats, so we might want to refine that if there + are strong use-cases. *) + | Custom -> block_shape [Obj.custom_tag] + let rec of_type_expr env ty callstack_map = (* TODO : try the Ctype.expand_head_opt version here *) check_annotated ty callstack_map; @@ -194,21 +211,7 @@ module Head_shape = struct | Tvar _ | Tunivar _ -> any_shape | Tconstr (p, args, _abbrev) -> begin match match_primitive_type p with - | Some Int -> { head_imm = Shape_any; head_blocks = Shape_set [] } - | Some Float -> block_shape [Obj.double_tag] - | Some String - | Some Bytes -> block_shape [Obj.string_tag] - | Some Array -> - block_shape - (if Config.flat_float_array then [0] - else [0; Obj.double_array_tag]) - | Some Floatarray -> block_shape [Obj.double_array_tag] - | Some Lazy -> any_shape - (* Lazy values can 'shortcut' the lazy block, and thus have many - different tags. When Config.flat_float_array, they - cannot be floats, so we might want to refine that if there - are strong use-cases. *) - | Some Custom -> block_shape [Obj.custom_tag] + | Some prim_type -> of_primitive_type prim_type | None -> let head_callstack = Callstack.head callstack_map ty in if Callstack.visited p head_callstack then From a7abc2a29914fd1d4bc6a1296be04adae1ce2ece Mon Sep 17 00:00:00 2001 From: Gabriel Scherer Date: Sun, 29 Aug 2021 23:00:09 +0200 Subject: [PATCH 23/45] [minor] matching.ml: sum/product refactoring for Cases --- lambda/matching.ml | 127 +++++++++++++++++++++++++-------------------- 1 file changed, 70 insertions(+), 57 deletions(-) diff --git a/lambda/matching.ml b/lambda/matching.ml index 97455185368a..715aaf91e056 100644 --- a/lambda/matching.ml +++ b/lambda/matching.ml @@ -2754,39 +2754,49 @@ let combine_constant loc arg cst partial ctx def actions. Note that if [any_const] is Some, then [consts] must be empty. *) module Cases = struct + type 'k domain_cases = + | Any of lambda + | Set of ('k * lambda) list + + let add_case k act = function + | Any _ -> invalid_arg "Cases.add_case: Any" + | Set li -> Set ((k, act) :: li) + + let add_any act = function + | Set [] -> Any act + | Any _ -> invalid_arg "Cases.add_any: already Any" + | Set (_ :: _) -> invalid_arg "Cases.add_any: Set (_ :: _)" + + let sort_domain = function + | Any act -> Any act + | Set li -> Set (sort_int_lambda_list li) + type t = { - consts: (int * lambda) list; - nonconsts: (int * lambda) list; - any_const: lambda option; - any_nonconst: lambda option; + consts: imm domain_cases; + nonconsts: tag domain_cases; } let empty = { - consts = []; - nonconsts = []; - any_const = None; - any_nonconst = None; + consts = Set []; + nonconsts = Set []; } let add_const tag act cases = - { cases with consts = (tag, act) :: cases.consts } + { cases with consts = add_case tag act cases.consts } let add_nonconst tag act cases = - { cases with nonconsts = (tag, act) :: cases.nonconsts } + { cases with nonconsts = add_case tag act cases.nonconsts } let add_any_const act cases = - { cases with any_const = - match cases.any_const with - | Some _ -> invalid_arg "Cases.add_any_const" - | None -> Some act - } + { cases with consts = add_any act cases.consts } let add_any_nonconst act cases = - { cases with any_nonconst = - match cases.any_nonconst with - | Some _ -> invalid_arg "Cases.add_any_nonconst" - | None -> Some act - } + { cases with nonconsts = add_any act cases.nonconsts } + + let sort cases = { + consts = sort_domain cases.consts; + nonconsts = sort_domain cases.nonconsts; + } end let split_cases pat_env tag_lambda_list = @@ -2820,11 +2830,7 @@ let split_cases pat_env tag_lambda_list = | Cstr_extension _ -> assert false ) in - let cases = split_rec tag_lambda_list in - { cases with - consts = sort_int_lambda_list cases.consts; - nonconsts = sort_int_lambda_list cases.nonconsts; - } + Cases.sort (split_rec tag_lambda_list) let split_extension_cases tag_lambda_list = let rec split_rec = function @@ -2840,14 +2846,15 @@ let split_extension_cases tag_lambda_list = split_rec tag_lambda_list let split_variant_cases pat_env tag_lambda_list = - let Cases.{consts; nonconsts; any_const; any_nonconst} = + let Cases.{consts; nonconsts} = split_cases pat_env tag_lambda_list in - (* We assume there are no unboxed constructors - for polymorphic variants *) - assert (any_const = None); - assert (any_nonconst = None); - (consts, nonconsts) - + match consts, nonconsts with + | Any _, _ | _, Any _ -> + (* We assume there are no unboxed constructors + for polymorphic variants *) + assert false + | Set consts, Set nonconsts -> + (consts, nonconsts) let combine_constructor loc arg pat_env cstr partial ctx def (descr_lambda_list, total1, pats) = @@ -2916,20 +2923,20 @@ let combine_constructor loc arg pat_env cstr partial ctx def match (cstr.cstr_consts, cstr.cstr_nonconsts, cases) with - | 1, 1, { consts = [ (0, act1) ]; nonconsts = [ (0, act2) ] } - | 1, 0, { consts = [ (0, act1) ]; any_nonconst = Some act2 } -> + | 1, 1, { consts = Set [ (0, act1) ]; nonconsts = (Set [ (0, act2) ]) } + | 1, 0, { consts = Set [ (0, act1) ]; nonconsts = Any act2 } -> (* Typically, match on lists, will avoid isint primitive in that case *) Lifthenelse (arg, act2, act1) - | n, 0, { consts; any_const; nonconsts=[]; any_nonconst=None } -> + | n, 0, { consts; nonconsts= Set []; } -> (* The type defines constant constructors only *) - begin match any_const with - | Some act -> act - | None -> + begin match consts with + | Any act -> act + | Set consts -> call_switcher loc fail_opt arg 0 (n - 1) consts end | n, _, _ -> ( - let single_action any_case cases complete_case_count = + let single_action cases complete_case_count = (* = Some act when all actions are the same, either on constant or non-constant domain. @@ -2939,18 +2946,24 @@ let combine_constructor loc arg pat_env cstr partial ctx def complete_case_count is also None, otherwise it must be the total number of heads at this domain. *) - match (fail_opt, any_case, cases) with - | Some a, None, [] - | _, Some a, _ -> Some a - | None, None, nonconsts -> same_actions nonconsts - | Some _, None, cases -> + let same_actions cases = + match same_actions cases with + | Some act -> Ok act + | None -> Error cases + in + match (fail_opt, cases) with + | Some act, Cases.Set [] + | _, Cases.Any act -> Ok act + | None, Cases.Set cases -> + same_actions cases + | Some _, Cases.Set cases -> (* if any_case is None, complete_case_count must be Some *) let count = Option.get complete_case_count in if List.length cases = count then same_actions cases else - None + Error cases in (* [numconsts] and [numnonconsts] count the number of valid head constructors at this type in the domain @@ -2959,12 +2972,12 @@ let combine_constructor loc arg pat_env cstr partial ctx def let single_const_act = let numconsts = Typedecl.cstr_unboxed_numconsts pat_env cstr in - single_action cases.any_const cases.consts numconsts + single_action cases.consts numconsts in let single_nonconst_act = let numnonconsts = Typedecl.cstr_unboxed_numnonconsts pat_env cstr in - single_action cases.any_nonconst cases.nonconsts numnonconsts + single_action cases.nonconsts numnonconsts in let test_isint const_act nonconst_act = Lifthenelse @@ -2975,18 +2988,18 @@ let combine_constructor loc arg pat_env cstr partial ctx def better code than a switch in some cases, but for tests on non-constant constructors we prefer to always emit a switch, as bytecode implements this sophisticated instruction. *) - match single_nonconst_act, cases.any_const with - | Some nonconst_act, _ -> + match single_nonconst_act, cases.consts with + | Ok nonconst_act, _ -> (* Note: we already checked that not all actions are identical, so the constant-constructor actions cannot be empty. *) let int_actions = match single_const_act with - | Some const_act -> const_act - | None -> - call_switcher loc fail_opt arg 0 (n - 1) cases.consts + | Ok const_act -> const_act + | Error const_acts -> + call_switcher loc fail_opt arg 0 (n - 1) const_acts in test_isint int_actions nonconst_act - | None, None -> + | Error nonconsts, Set consts -> (* Switch is a low-level control-flow construct that must handle an interval of contiguous values (on both domains); [sw_numconsts] and [sw_numblocks] @@ -3048,16 +3061,16 @@ let combine_constructor loc arg pat_env cstr partial ctx def in let sw = { sw_numconsts; - sw_consts = cases.consts; + sw_consts = consts; sw_numblocks; - sw_blocks = cases.nonconsts; + sw_blocks = nonconsts; sw_failaction = fail_opt } in let hs, sw = share_actions_sw sw in let sw = reintroduce_fail sw in hs (Lswitch (arg, sw, loc)) - | None, Some const_act -> + | Error nonconsts, Any const_act -> (* Generate a switch on nonconst_act under a Pisint test to handle the any_const action *) let sw_numblocks = @@ -3071,7 +3084,7 @@ let combine_constructor loc arg pat_env cstr partial ctx def { sw_numconsts = 0; sw_consts = []; sw_numblocks; - sw_blocks = cases.nonconsts; + sw_blocks = nonconsts; sw_failaction = fail_opt; }, loc From d71b6f5d8e9d2d316fb22c818eb28d91a5d79ee2 Mon Sep 17 00:00:00 2001 From: Gabriel Scherer Date: Sun, 29 Aug 2021 23:02:26 +0200 Subject: [PATCH 24/45] update README.head_shape --- README.head_shape.md | 12 ++++-------- 1 file changed, 4 insertions(+), 8 deletions(-) diff --git a/README.head_shape.md b/README.head_shape.md index 2418419f0452..5ae8ada4263d 100644 --- a/README.head_shape.md +++ b/README.head_shape.md @@ -229,15 +229,11 @@ and we expand it to a switch without unboxed constructors, to be compiled by the | Cstr_block 252 -> act2 ``` -This is the general idea, but in fact we need slightly more sophistication to deal with `(Imm, _)` or `(Block, _)` shapes. Instead of a list of clauses, we represent a switch as a product structure which may contain: -- an action for all immediates (the `any_const` action) -- or a list of specific actions for some immediates -- an action for all blocks (the `any_nonconst` action) -- or a list of specific actions for some block tags +This is the general idea, but in fact we need slightly more sophistication to deal with `(Imm, _)` or `(Block, _)` shapes. We change the definition of clauses to contain both: +- either a list of specific actions for some immediates, or an "any" action for all immediates, and +- either a list of specific actions for some block tags, or an "any" action for all blocks -TODO: writing this explanation, I really have the impression that we should try again to use a sum type to clarify that we either have `any` or some immediates. This makes `split_cases` harder to write, but the consumer easier to read, and the consumer is more important here -- it is the subtle piece of code that does the pattern-matching compilation of those switches. - -The code that lowers switches into `Lifthenelse` or `Lswitch` has to be adapted to deal with this new structure. If We changed the code in such a way that it should be easy to check that, in absence of unboxed constructors, the code generated is the same as it was previously. (The cost of this approach is that sometimes the code is more verbose / less regular than it could be if written from scratch, accepting some changes in compilation.) +The code that lowers switches into `Lifthenelse` or `Lswitch` has to be adapted to deal with this new structure. We tried to make it possible/easy to check that, in absence of unboxed constructors, the code generated is the same as it was previously. (The cost of this approach is that sometimes the code is more verbose / less regular than it could be if written from scratch, accepting some changes in compilation.) Remark: To emit `Lswitch` instructions, the compiler needs to know of the range of possible immediate values and tags (when we don't have `any_{const,nonconst}` actions). More precisely, we want the maximal possible immediate constructor and block tag at this type (minimal values are always assumed to be 0). From b9feb70e3370e4a4951a5aaf2a870fad371e06e2 Mon Sep 17 00:00:00 2001 From: Gabriel Scherer Date: Mon, 30 Aug 2021 22:20:57 +0200 Subject: [PATCH 25/45] split the head-shape spec in two files, specification (-> RFC) and implementation (-> PR) --- README.head_shape.md => HEAD_SHAPE.impl.md | 133 +----------------- HEAD_SHAPE.spec.md | 155 +++++++++++++++++++++ 2 files changed, 156 insertions(+), 132 deletions(-) rename README.head_shape.md => HEAD_SHAPE.impl.md (73%) create mode 100644 HEAD_SHAPE.spec.md diff --git a/README.head_shape.md b/HEAD_SHAPE.impl.md similarity index 73% rename from README.head_shape.md rename to HEAD_SHAPE.impl.md index 5ae8ada4263d..0c534a42a04f 100644 --- a/README.head_shape.md +++ b/HEAD_SHAPE.impl.md @@ -18,140 +18,9 @@ In a [small benchmark](https://github.com/gasche/ocaml/pull/10), we tested that The intent of the currently presented work is to do the simplest possible step in the direction of more unboxing. Most advanced aspects were left to future work. We believe that it would be reasonable to integrate the PR with its current feature scope: it provides values for users, and should not hamper further extensions. - ## Precise specification -We define the *head* of an OCaml value as follows: -- the head of an immediate value `v` is the pair `(Imm, v)` -- the head of a heap block with tag `t` is the pair `(Block, t)`. - -(In other words, the head tracks whether a value is immediate or a block, and for blocks only keeps the tag.) - -The "head shape" of a type is a (slight over-approximation of) the set of heads of all possible values of this type. - -Now consider a variant type declaration containing one or several constructors annotated with `[@unboxed]`: - -```ocaml -type ('a, 'b, ...) t = - | Const0 (* some constant constructors *) - | Const1 - | ... - | Const{m} - | NonConst0 of t00 * t01 * ... - | Nonconst1 of t10 * t11 * ... - | ... - | NonConst{n} of t{n}0 * t{n}1 * ... - | Unboxed1 of u0 [@unboxed] - | Unboxed2 of u1 [@unboxed] - | ... - | Unboxed{l} of u{l} [@unboxed] -``` - -(For simplicity we wrote above all constant constructors first, then all non-constant constructors then all unboxed constructors. But in fact we support arbitrary interleaving of these categories, and the representation is exactly the same as long as the ordering within constant constructors and within non-constant constructors is preserved.) - -The compiled representation of this type is as follows: -- as before, constant constructors `Const{k}` are represented by the immediate number `k` -- as before, non-constant constructors `Nonconst{k} of ...` are represented by a heap block with tag `k` -- unboxed constructors `Unboxed{k} of u{k}` are represented directly by the value of type `u{k}`, without - any boxing - -This definition is *rejected* statically if the unboxed constructors overlap with the other values of the type, in the following precise sense: - -1. We compute the "boxed head shape" `BS` of this type *without* the unboxed constructors; by definition of the head shape, this is the set `{(Imm, 0), (Imm, 1), ..., (Imm, m)} ∪ {(Block, 0), (Block, 1), ,.., (Block, n)}`. - -2. Then we compute the "unboxed shapes" `US{k}` of each unboxed constructor, that is the head shape of `u{k}`. - -3. The type is accepted if and only if the shapes `BS, US0, US1, ..., US{l}` are disjoint from each other. The head shape of the whole shape is then the disjoint union `BS ⊎ US0 ⊎ US1 ⊎ ... ⊎ US{l}`. - -Unknown/abstract types are assumed to have a "top" shape with containing potentially all heads. (This should be refined when the abstract type is used to represent an FFI type with a precise shape implemented in C; supporting head shape assertions on abstract types is future work.) - -### Examples - -```ocaml -(* rejected *) -type t = - | Int of int [@unboxed] (* shape: (Imm, _) *) - | Unit (* shape: (Imm, 0), conflicts with Int above *) - -(* accepted *) -type t = - | Int of int [@unboxed] (* shape: (Imm, _) *) - | Box of t (* shape: (Block, 0), as the first non-constant non-unboxed constructor *) - (* shape(t): (Imm, _) ∪ {(Block, 0)} *) - -(* accepted *) -type prod = t * t -and t = - | Int of int [@unboxed] (* shape: (Imm, _): any immediate *) - | String of string [@unboxed] (* shape: (Block, Obj.string_tag) (Obj.string_tag is 252) *) - | Prod of prod [@unboxed] (* shape: (Block, 0) *) - (* shape(t): (Imm, _) ∪ {(Block, 0), (Block, Obj.string_tag)} *) - - -(** With abstract types *) - -type abstract - -(* accepted *) -type t = - | Int of int [@unboxed] (* shape: (Imm, _) *) - | Abs of abstract (* shape: (Block, 0) *) - (* shape(t): (Imm, _) ∪ {(Block, 0)} *) - -(* rejected *) -type t = - | Int of int (* shape: (Block, 0) *) - | Abs of abstract [@unboxed] (* any shape, conflicts with Int *) - - -(** Nested unboxing *) - -type t1 = - | Int of int [@unboxed] - | Block of unit - (* shape(t1): (Imm, _) ∪ {(Block, 0)} *) - -(* rejected *) -type t2 = - | T1 of t1 [@unboxed] (* shape: (Imm, _) ∪ {(Block, 0)} *) - | S of string (* shape: (Block, 0), conflicts with T1 *) - -(* accepted *) -type t3 = - | T1 of t1 [@unboxed] (* shape: {(Imm, _), (Block, 0)} *) - | S of string [@unboxed] (* shape: (Block, Obj.stringₜag) *) - (* shape(t3): (Imm, _) ∪ {(Block, 0)} ∪ {(Block, Obj.string_tag)} *) -``` - - -### Comparison with Yallop's proposal [RFC#14](https://github.com/ocaml/RFCs/pull/14) - -Jeremy Yallop's proposal uses a global annotation `[@@unboxed]` on all constructors at once, we use a per-constructor annotation `[@unboxed]`. (The RFC mentions this as a possible extension in "Extension: partial unboxing".) It would be easy to interpret `[@@unboxed]` as just "[@unboxed] on all constructors", but we have not implemented this yet. - -A major difference is that the RFC#14 specification suggests renumbering constructors in some cases, where the representation of `C of foo [@unboxed]` is taken to be different from the representation of `foo`, in order to avoid conflicts with other constructors at this type. We do not support any such renumbering: -- the representation of `Unboxed of foo [@unboxed]` is always the representation of `foo` -- the representation of `Boxed of foo` always uses the block tag consecutive/next/succedent to the previous boxed-constructor tag in the declaration (filtering out unboxed constructors). - -(Note: @stedolan calls this aspect of RFC#14 "[conflating inlining and disjointness](https://github.com/ocaml/RFCs/pull/14#issuecomment-603867960)". We only deal with disjointness.) - -### Leftover question: how close to the compiler-distribution runtime should the specification be? - -We define static accept/reject decisions for partially-unboxed types using "head shapes", which are defined in terms of the value-representation strategy of the main OCaml implementation. Should we have a more abstract definition, that leaves more room to other representations in alternative implementations? - -We have not studied this question yet and we believe it is a pressing question. In particular, any choice that would end up being merged in the language probably MUST support the js_of_ocaml value representation. (Do you know of a reference document that describes the js_of_ocaml value representation? Pointers are welcome are we are not jsoo experts ourselves. cc @hhugo.) - -Our intuition is that we could fine a "weakening" of our current specification that distinguishes less different sort of shapes -- thus rejects more definitions -- and gives good flexibility for alternative implementations. Here are some things we could do: - -- We could stop making assumptions about the shape of function closures (currently: {Closure_tag, Infix_tag}), preventing the unboxing of closure-holding constructors. -- We could also weaken our assumptions about built-in containers (string/byte, arrays, double-arrays, etc.) -- We could stop distinguishing "float" from immediates (ouch!) if jsoo does this. What about Int32, Int64, should they be known as custom values? - -In other words: what amount of runtime type information should we require from OCaml implementations? - -At the limit, one extreme choice would be to only reason on the tag of variant constructors (constant or not), which are distinguishable from each other in any OCaml implementation, and not make any other assumption about head shapes (map all types except variants to the "top" shape). This would reject most unboxing definitions, leave maximal freedom for langauge implementations. Unfortunately this would also prevent the actually-interesting uses of the feature we know about, which mostly resolve around unboxing an `int`-carrying constructor. - -This is an aspect of our design on which we need external feedback from people with a good taste for these matters. (cc @xavierleroy, @damiendoligez, @stedolan, @lpw25, @let-def, etc.). - +See [HEAD_SHAPE.spec.md](HEAD_SHAPE.spec.md). ## Implementation strategy diff --git a/HEAD_SHAPE.spec.md b/HEAD_SHAPE.spec.md new file mode 100644 index 000000000000..43977fc01404 --- /dev/null +++ b/HEAD_SHAPE.spec.md @@ -0,0 +1,155 @@ +# Constructor unboxing specification + +We (@nchataing as intern, @gasche as advisor) implemented a variant of @yallop's constructor-unboxing specification as an experimental branch that we would now like to discuss and consider for upstreaming. + +Our intent was to implement the simplest possible form of unboxing in presence of several constructors, and leave more advanced aspects -- anything that could be left off -- to further work. + +We support a per-constructor `[@unboxed]` attribute, that can be used in a variant type as long as the set of values corresponding to each constructor (boxed or unboxed) remain disjoint. + +For example: + +```ocaml +type bignum = + | Short of int [@unboxed] (* represented directly by an integer *) + | Long of Gmp.t (* Block of tag 0 (first non-unboxed constructor) *) +``` + +## Precise specification + +We define the *head* of an OCaml value as follows: +- the head of an immediate value `v` is the pair `(Imm, v)` +- the head of a heap block with tag `t` is the pair `(Block, t)`. + +(In other words, the head tracks whether a value is immediate or a block, and for blocks only keeps the tag.) + +The "head shape" of a type is a (slight over-approximation of) the set of heads of all possible values of this type. + +Now consider a variant type declaration containing one or several constructors annotated with `[@unboxed]`: + +```ocaml +type ('a, 'b, ...) t = + | Const0 (* some constant constructors *) + | Const1 + | ... + | Const{m} + | NonConst0 of t00 * t01 * ... + | Nonconst1 of t10 * t11 * ... + | ... + | NonConst{n} of t{n}0 * t{n}1 * ... + | Unboxed1 of u0 [@unboxed] + | Unboxed2 of u1 [@unboxed] + | ... + | Unboxed{l} of u{l} [@unboxed] +``` + +(For simplicity we wrote above all constant constructors first, then all non-constant constructors then all unboxed constructors. But in fact we support arbitrary interleaving of these categories, and the representation is exactly the same as long as the ordering within constant constructors and within non-constant constructors is preserved.) + +The compiled representation of this type is as follows: +- as before, constant constructors `Const{k}` are represented by the immediate number `k` +- as before, non-constant constructors `Nonconst{k} of ...` are represented by a heap block with tag `k` +- unboxed constructors `Unboxed{k} of u{k}` are represented directly by the value of type `u{k}`, without + any boxing + +This definition is *rejected* statically if the unboxed constructors overlap with the other values of the type, in the following precise sense: + +1. We compute the "boxed head shape" `BS` of this type *without* the unboxed constructors; by definition of the head shape, this is the set `{(Imm, 0), (Imm, 1), ..., (Imm, m)} ∪ {(Block, 0), (Block, 1), ,.., (Block, n)}`. + +2. Then we compute the "unboxed shapes" `US{k}` of each unboxed constructor, that is the head shape of `u{k}`. + +3. The type is accepted if and only if the shapes `BS, US0, US1, ..., US{l}` are disjoint from each other. The head shape of the whole shape is then the disjoint union `BS ⊎ US0 ⊎ US1 ⊎ ... ⊎ US{l}`. + +Unknown/abstract types are assumed to have a "top" shape with containing potentially all heads. (This should be refined when the abstract type is used to represent an FFI type with a precise shape implemented in C; supporting head shape assertions on abstract types is future work.) + + +## Examples + +```ocaml +(* rejected *) +type t = + | Int of int [@unboxed] (* shape: (Imm, _) *) + | Unit (* shape: (Imm, 0), conflicts with Int above *) + +(* accepted *) +type t = + | Int of int [@unboxed] (* shape: (Imm, _) *) + | Box of t (* shape: (Block, 0), as the first non-constant non-unboxed constructor *) + (* shape(t): (Imm, _) ∪ {(Block, 0)} *) + +(* accepted *) +type prod = t * t +and t = + | Int of int [@unboxed] (* shape: (Imm, _): any immediate *) + | String of string [@unboxed] (* shape: (Block, Obj.string_tag) (Obj.string_tag is 252) *) + | Prod of prod [@unboxed] (* shape: (Block, 0) *) + (* shape(t): (Imm, _) ∪ {(Block, 0), (Block, Obj.string_tag)} *) + + +(** With abstract types *) + +type abstract + +(* accepted *) +type t = + | Int of int [@unboxed] (* shape: (Imm, _) *) + | Abs of abstract (* shape: (Block, 0) *) + (* shape(t): (Imm, _) ∪ {(Block, 0)} *) + +(* rejected *) +type t = + | Int of int (* shape: (Block, 0) *) + | Abs of abstract [@unboxed] (* any shape, conflicts with Int *) + + +(** Nested unboxing *) + +type t1 = + | Int of int [@unboxed] + | Block of unit + (* shape(t1): (Imm, _) ∪ {(Block, 0)} *) + +(* rejected *) +type t2 = + | T1 of t1 [@unboxed] (* shape: (Imm, _) ∪ {(Block, 0)} *) + | S of string (* shape: (Block, 0), conflicts with T1 *) + +(* accepted *) +type t3 = + | T1 of t1 [@unboxed] (* shape: {(Imm, _), (Block, 0)} *) + | S of string [@unboxed] (* shape: (Block, Obj.stringₜag) *) + (* shape(t3): (Imm, _) ∪ {(Block, 0)} ∪ {(Block, Obj.string_tag)} *) +``` + + +### Comparison with Yallop's proposal [RFC#14](https://github.com/ocaml/RFCs/pull/14) + +Jeremy Yallop's proposal uses a global annotation `[@@unboxed]` on all constructors at once, we use a per-constructor annotation `[@unboxed]`. (The RFC mentions this as a possible extension in "Extension: partial unboxing".) It would be easy to interpret `[@@unboxed]` as just "[@unboxed] on all constructors", but we have not implemented this yet. + +A major difference is that the RFC#14 specification suggests renumbering constructors in some cases, where the representation of `C of foo [@unboxed]` is taken to be different from the representation of `foo`, in order to avoid conflicts with other constructors at this type. We do not support any such renumbering: +- the representation of `Unboxed of foo [@unboxed]` is always the representation of `foo` +- the representation of `Boxed of foo` always uses the block tag consecutive/next/succedent to the previous boxed-constructor tag in the declaration (filtering out unboxed constructors). + +(Note: @stedolan calls this aspect of RFC#14 "[conflating inlining and disjointness](https://github.com/ocaml/RFCs/pull/14#issuecomment-603867960)". We only deal with disjointness.) + + +## TODO separability + +TODO explain how our approach ensures separability of types (see still-TODO proposal in [HEAD_SHAPE.impl.md](HEAD_SHAPE.impl.md). + + +## Leftover question: how close to the compiler-distribution runtime should the specification be? + +We define static accept/reject decisions for partially-unboxed types using "head shapes", which are defined in terms of the value-representation strategy of the main OCaml implementation. Should we have a more abstract definition, that leaves more room to other representations in alternative implementations? + +We have not studied this question yet and we believe it is a pressing question. In particular, any choice that would end up being merged in the language probably MUST support the js_of_ocaml value representation. (Do you know of a reference document that describes the js_of_ocaml value representation? Pointers are welcome are we are not jsoo experts ourselves. cc @hhugo.) + +Our intuition is that we could fine a "weakening" of our current specification that distinguishes less different sort of shapes -- thus rejects more definitions -- and gives good flexibility for alternative implementations. Here are some things we could do: + +- We could stop making assumptions about the shape of function closures (currently: {Closure_tag, Infix_tag}), preventing the unboxing of closure-holding constructors. +- We could also weaken our assumptions about built-in containers (string/byte, arrays, double-arrays, etc.) +- We could stop distinguishing "float" from immediates (ouch!) if jsoo does this. What about Int32, Int64, should they be known as custom values? + +In other words: what amount of runtime type information should we require from OCaml implementations? + +At the limit, one extreme choice would be to only reason on the tag of variant constructors (constant or not), which are distinguishable from each other in any OCaml implementation, and not make any other assumption about head shapes (map all types except variants to the "top" shape). This would reject most unboxing definitions, leave maximal freedom for langauge implementations. Unfortunately this would also prevent the actually-interesting uses of the feature we know about, which mostly resolve around unboxing an `int`-carrying constructor. + +This is an aspect of our design on which we need external feedback from people with a good taste for these matters. (cc @xavierleroy, @damiendoligez, @yallop, @stedolan, @lpw25, @let-def, etc.). From f3a88389a89f3d37f91658a2ed446d3a3a1f7118 Mon Sep 17 00:00:00 2001 From: Gabriel Scherer Date: Fri, 3 Sep 2021 16:17:58 +0200 Subject: [PATCH 26/45] rephrase the separability proposal --- HEAD_SHAPE.impl.md | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) diff --git a/HEAD_SHAPE.impl.md b/HEAD_SHAPE.impl.md index 0c534a42a04f..2061821402cc 100644 --- a/HEAD_SHAPE.impl.md +++ b/HEAD_SHAPE.impl.md @@ -212,11 +212,13 @@ It is unsound in presence of the flat-float-array optimization to have types tha type t = Float of float [@unboxed] | Other ``` -The simplest possible idea to solve this is to give `float` the "top" shape (instead of Double_tag), which should reject all such definitions. (But the error message will be disappointing.) - -A more elaborate fix to this issue is to add to the head shape a boolean flag, "separated". A "separated" shape guarantees that it is the over-approximation of a separable type, while a non-separated shape may be the shape of a non-separated type. So for example we have a "Separated Top" value (which can be inhabited by any value, but either contains float and nothing else or no floats) and a "Non-separated top" value (any value, possibly floats and other stuff at the same time). It may be possible to compute this bit simply by giving existential variables in GADTs the "non-separated top" shape, and then to reject all non-separated type declarations. This would allow removing the current separability-computation machinery, which could bring a substantial simplification of this corner of the type-checker. - +One possibility to fix this: +- extend the domain of shapes, in addition to "imm" and "block" we add a "poison" domain, which is a single bit (true/false), which indicates whether the type is separated (poison=false) or non-separateed (poison-true) +- when taking the disjoint union of two shapes, compute the "poison" bit (take the disjunction of the two poison bits, and also set to 'true' if the resulting domain contains 'Obj.double_tag' and anything else) +- existential variables of GADT constructors do not get the current "top" shape (poison=false), but a "poisoned top" with poison=true. +- if a type declaration has a poisoned final shape, reject the declaration +Question: would it be possible to just get rid of the current separability computation for type declarations, and use this shape analysis instead? (This would be a nice simplification to the type-checker coebase.) We could try this by implementing the 'poison' logic, disabling the 'separability' check, and running the separability testsuite. ## Future work From a6691d174dc3cb205ad2efe24dbf29ec649c207c Mon Sep 17 00:00:00 2001 From: Nicolas Chataing Date: Sat, 4 Sep 2021 19:16:08 +0200 Subject: [PATCH 27/45] Update HEAD_SHAPE.spec.md --- HEAD_SHAPE.spec.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/HEAD_SHAPE.spec.md b/HEAD_SHAPE.spec.md index 43977fc01404..30ac6057a80d 100644 --- a/HEAD_SHAPE.spec.md +++ b/HEAD_SHAPE.spec.md @@ -150,6 +150,6 @@ Our intuition is that we could fine a "weakening" of our current specification t In other words: what amount of runtime type information should we require from OCaml implementations? -At the limit, one extreme choice would be to only reason on the tag of variant constructors (constant or not), which are distinguishable from each other in any OCaml implementation, and not make any other assumption about head shapes (map all types except variants to the "top" shape). This would reject most unboxing definitions, leave maximal freedom for langauge implementations. Unfortunately this would also prevent the actually-interesting uses of the feature we know about, which mostly resolve around unboxing an `int`-carrying constructor. +At the limit, one extreme choice would be to only reason on the tag of variant constructors (constant or not), which are distinguishable from each other in any OCaml implementation, and not make any other assumption about head shapes (map all types except variants to the "top" shape). This would reject most unboxing definitions, leave maximal freedom for language implementations. Unfortunately this would also prevent the actually-interesting uses of the feature we know about, which mostly resolve around unboxing an `int`-carrying constructor. This is an aspect of our design on which we need external feedback from people with a good taste for these matters. (cc @xavierleroy, @damiendoligez, @yallop, @stedolan, @lpw25, @let-def, etc.). From cede37e0d3273695bda4622410928e45e34008c4 Mon Sep 17 00:00:00 2001 From: Gabriel Scherer Date: Tue, 7 Sep 2021 14:16:53 +0200 Subject: [PATCH 28/45] [minor] more code markers --- HEAD_SHAPE.impl.md | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/HEAD_SHAPE.impl.md b/HEAD_SHAPE.impl.md index 2061821402cc..a384a9d94efd 100644 --- a/HEAD_SHAPE.impl.md +++ b/HEAD_SHAPE.impl.md @@ -6,7 +6,7 @@ This PR implements a variant of the "constructor unboxing" feature proposed by J The following is now accepted: -``` +```ocaml type bignum = | Short of int [@unboxed] (* represented directly by an integer *) | Long of Gmp.t (* Block of tag 0 (first non-unboxed constructor) *) @@ -38,7 +38,7 @@ The main components required for this feature are: Representing head shapes by their set of possible values is not practical, as `(Imm, _)` (the shape of all immediate values) would be too large a set. Instead we use a representation with an explicit "any" value in either domains (for immediates or for tags): -``` +```ocaml (* Over-approximation of the possible values of a type, used to verify and compile unboxed head constructors. @@ -189,7 +189,7 @@ encountered in head position during reduction. Our cycle-detection algorithm will sometimes reject definitions that indeed are cyclic, but do admit a valid fixpoint: -``` +```ocaml (* this bad declaration should be rejected *) type t = Loop of t [@unboxed] | Other (* because `Other` and `Loop Other` would have the same representation *) From 3143ee5530f71726464c9c64ca41c2a0c69fde5d Mon Sep 17 00:00:00 2001 From: Gabriel Scherer Date: Tue, 7 Sep 2021 15:53:21 +0200 Subject: [PATCH 29/45] slightly more in .impl.md --- HEAD_SHAPE.impl.md | 33 ++++++++++++++++++++++++++++----- 1 file changed, 28 insertions(+), 5 deletions(-) diff --git a/HEAD_SHAPE.impl.md b/HEAD_SHAPE.impl.md index a384a9d94efd..46be67c10d2f 100644 --- a/HEAD_SHAPE.impl.md +++ b/HEAD_SHAPE.impl.md @@ -213,12 +213,21 @@ type t = Float of float [@unboxed] | Other ``` One possibility to fix this: -- extend the domain of shapes, in addition to "imm" and "block" we add a "poison" domain, which is a single bit (true/false), which indicates whether the type is separated (poison=false) or non-separateed (poison-true) -- when taking the disjoint union of two shapes, compute the "poison" bit (take the disjunction of the two poison bits, and also set to 'true' if the resulting domain contains 'Obj.double_tag' and anything else) -- existential variables of GADT constructors do not get the current "top" shape (poison=false), but a "poisoned top" with poison=true. -- if a type declaration has a poisoned final shape, reject the declaration +- Extend the domain of shapes, in addition to "imm" and "block" we add a "separated" domain, which is a single bit (true/false), which indicates whether the set of values we approximate is separated. + (a set of OCaml values is "separated" if it contains either (1) only `float` values or (2) no `float` value.) +- When taking the disjoint union of two shapes, compute the "separated" bit (take the conjunction of the two input bits, and also set to 'false' if the resulting domain contains both 'Obj.double_tag' and something else). +- Existential variables of GADT constructors do not get the current "top" shape (separated=true), but a "non-separated top" with separated=false. +- If a type declaration has a non-separated final shape, reject the declaration. -Question: would it be possible to just get rid of the current separability computation for type declarations, and use this shape analysis instead? (This would be a nice simplification to the type-checker coebase.) We could try this by implementing the 'poison' logic, disabling the 'separability' check, and running the separability testsuite. +Question: would it be possible to just get rid of the current separability computation for type declarations, and use this shape analysis instead? (This would be a nice simplification to the type-checker codebase.) We could try this by implementing this logic, disabling the pre-existing 'separability' check, and running the separability testsuite. + +Remark: without this extension, shapes have a natural denotational semantics, where each shape is interpreted by a set of OCaml values. + + interp(s) = { v | head(v) ∈ s } + +With this extension, shapes can be interpreted as *sets of sets* of OCaml values: + + interp(s) = { S | ∀v∈S, head(v) ∈ s /\ s.separated <=> is_separated(S) } ## Future work @@ -232,12 +241,26 @@ If a type definition is rejected due to shape conflict, it would be nice to give Finer-grained shape computations for GADTs: to compute the shape of a type `foo t` when `t` is a GADT, instead of taking the disjoint union of the shape of all constructors, we can filter only the constructors that are "compatible" with `foo` (we cannot prove that the types are disjoint). This is simple enough and gives good, interesting results in practice, but it also requires refining the termination-checking strategy for GADTs (in addition to the head type constructor, we need to track the set of compatible constructors for the particular expansion that was done). For now we punt on this by not doing any special handling of GADTs, even though it is less precise. + ### Shape annotations on abstract types If an abstract type is meant to be defined through the FFI, the OCaml-side could come with an annotation restricting its shape from the pessimal default "{ (Imm, _); (Block, _) }" to the actual shape of FFI-produced values for this type. This requires blindly trusting the programmer, but this blind trust is the foundation of our FFI model already. Having shape annotations on abstract types means that shape-inclusion has to be checked when verifying that a type definition in a module matches a type declaration in its interface. (Currently we don't have any work there, because means of abstractions always either preserve the head shape or turn it into "top".) +### Arity tracking + +Another information we could add to our "head shape" approximation is the size of the block. For example, in theory we could allow this: + +```ocaml +type 'a pair = ('a * 'a) +type 'a triple = ('a * 'a * 'a) + +type 'a t = + | Pair of 'a pair [@unboxed] (* tag 0, size 2 *) + | Triple of 'a triple [@unboxed] (* tag 0, size 3 *) +``` + ### Compilation strategy The pattern-matching compilation strategy could be improved in some cases, at the cost of substantial changes to our current implementation. Consider `type t = Int of int [@unboxed] | String of string [@unboxed] and u = T of t [@unboxed] | Float of float [@unboxed]`. A matching of the form From 6d238a51fac00ba4c43a29aac7f7b6e4f2a2c666 Mon Sep 17 00:00:00 2001 From: Gabriel Scherer Date: Tue, 7 Sep 2021 15:57:06 +0200 Subject: [PATCH 30/45] mention separability in the spec --- HEAD_SHAPE.impl.md | 2 +- HEAD_SHAPE.spec.md | 8 ++++++-- 2 files changed, 7 insertions(+), 3 deletions(-) diff --git a/HEAD_SHAPE.impl.md b/HEAD_SHAPE.impl.md index 46be67c10d2f..cfe78538e756 100644 --- a/HEAD_SHAPE.impl.md +++ b/HEAD_SHAPE.impl.md @@ -204,7 +204,7 @@ type t = Loop of t [@unboxed] It would be nice to put in the work to distinguish "good cycles" from "bad cycles" to avoid this small defect of the current strategy of rejecting *all* cycles. -### TODO enforce "separability" of resulting types +### Enforce "separability" of resulting types It is unsound in presence of the flat-float-array optimization to have types that contain both floating-point values and non-floating-point values. Our current approach does not enforce this, so it will allow this unsound definition: diff --git a/HEAD_SHAPE.spec.md b/HEAD_SHAPE.spec.md index 30ac6057a80d..fc055b8a21cf 100644 --- a/HEAD_SHAPE.spec.md +++ b/HEAD_SHAPE.spec.md @@ -131,9 +131,13 @@ A major difference is that the RFC#14 specification suggests renumbering constru (Note: @stedolan calls this aspect of RFC#14 "[conflating inlining and disjointness](https://github.com/ocaml/RFCs/pull/14#issuecomment-603867960)". We only deal with disjointness.) -## TODO separability +## separability -TODO explain how our approach ensures separability of types (see still-TODO proposal in [HEAD_SHAPE.impl.md](HEAD_SHAPE.impl.md). +When the compiler is in `flat-float-array` mode, soundness relies on the property that all OCaml types are "separated": they contain either (1) only `float` values, or (2) no `float` value. New forms of unboxing must preserve this property. + +We can track separatedness as part of the head-shape computation for unboxed type declaration, by adding to head-shape data a "separated" bit (see the details in [HEAD_SHAPE.impl.md](HEAD_SHAPE.impl.md)). We reject type declarations whose head-shape is not separated (when in `flat-float-array` mode). + +It may be that this tracking is precise enough to entirely replace the pre-existing "separability analysis" of the type-checker. We have not implemented it yet, and have not evaluated this possibility. ## Leftover question: how close to the compiler-distribution runtime should the specification be? From a3702ed9003d473acb051005d977e1da13b5ea68 Mon Sep 17 00:00:00 2001 From: Gabriel Scherer Date: Thu, 9 Sep 2021 23:21:09 +0200 Subject: [PATCH 31/45] HEAD_SHAPE.impl.md: add genprintval handling in the TODO --- HEAD_SHAPE.impl.md | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/HEAD_SHAPE.impl.md b/HEAD_SHAPE.impl.md index cfe78538e756..ce19c7675418 100644 --- a/HEAD_SHAPE.impl.md +++ b/HEAD_SHAPE.impl.md @@ -185,6 +185,11 @@ fixed easily by keeping track of the set of type nodes we have already encountered in head position during reduction. +### Handle unboxed constructors in `genprintval` + +`genprintval` performs type-directed pretty-printing of values (represented as `Obj.t`). For variants it accesses the tag to know which constructor to print, and how to print the argument(s). We need to adapt this code to deal with unboxed constructors: the constructor to print is the one whose head shape contains the head of the value being printed. + + ### Distinguish "good" from "bad" cycles Our cycle-detection algorithm will sometimes reject definitions that indeed are cyclic, but do admit a valid fixpoint: From cacade1d1c6671ff073c7257af1c857728e19f5b Mon Sep 17 00:00:00 2001 From: Gabriel Scherer Date: Thu, 9 Sep 2021 23:36:44 +0200 Subject: [PATCH 32/45] [minor] genprintval.ml: helper functions to print variant/record values --- toplevel/genprintval.ml | 110 +++++++++++++++++++++------------------- 1 file changed, 58 insertions(+), 52 deletions(-) diff --git a/toplevel/genprintval.ml b/toplevel/genprintval.ml index 15eb404977d4..d588386d95e0 100644 --- a/toplevel/genprintval.ml +++ b/toplevel/genprintval.ml @@ -385,59 +385,10 @@ module Make(O : OBJ)(EVP : EVALPATH with type valu = O.t) = struct | {type_kind = Type_abstract; type_manifest = Some body} -> tree_of_val depth obj (instantiate_type env decl.type_params ty_list body) - | {type_kind = Type_variant (constr_list,rep)} -> - let unbx = (rep = Variant_unboxed) in - let tag = - if unbx then (* XXX unboxing Cstr_unboxed [] *) - assert false - else if O.is_block obj - then Cstr_block(O.tag obj) - else Cstr_constant(O.obj obj) in - let {cd_id;cd_args;cd_res} = - Datarepr.find_constr_by_tag tag constr_list in - let type_params = - match cd_res with - Some t -> - begin match get_desc t with - Tconstr (_,params,_) -> - params - | _ -> assert false end - | None -> decl.type_params - in - begin - match cd_args with - | Cstr_tuple l -> - let ty_args = - instantiate_types env type_params ty_list l in - tree_of_constr_with_args (tree_of_constr env path) - (Ident.name cd_id) false 0 depth obj - ty_args unbx - | Cstr_record lbls -> - let r = - tree_of_record_fields depth - env path type_params ty_list - lbls 0 obj unbx - in - Oval_constr(tree_of_constr env path - (Out_name.create (Ident.name cd_id)), - [ r ]) - end + | {type_kind = Type_variant (constr_list, rep)} -> + tree_of_variant depth env decl path ty_list obj constr_list rep | {type_kind = Type_record(lbl_list, rep)} -> - begin match check_depth depth obj ty with - Some x -> x - | None -> - let pos = - match rep with - | Record_extension _ -> 1 - | _ -> 0 - in - let unbx = - match rep with Record_unboxed _ -> true | _ -> false - in - tree_of_record_fields depth - env path decl.type_params ty_list - lbl_list pos obj unbx - end + tree_of_record depth env decl path ty_list obj lbl_list rep | {type_kind = Type_open} -> tree_of_extension path ty_list depth obj with @@ -482,6 +433,61 @@ module Make(O : OBJ)(EVP : EVALPATH with type valu = O.t) = struct Oval_stuff "" end + and tree_of_variant depth env decl path ty_list obj constr_list rep = + let unbx = (rep = Variant_unboxed) in + let tag = + if unbx then (* XXX unboxing Cstr_unboxed [] *) + assert false + else if O.is_block obj + then Cstr_block(O.tag obj) + else Cstr_constant(O.obj obj) in + let {cd_id;cd_args;cd_res} = + Datarepr.find_constr_by_tag tag constr_list in + let type_params = + match cd_res with + Some t -> + begin match get_desc t with + Tconstr (_,params,_) -> + params + | _ -> assert false end + | None -> decl.type_params + in + begin + match cd_args with + | Cstr_tuple l -> + let ty_args = + instantiate_types env type_params ty_list l in + tree_of_constr_with_args (tree_of_constr env path) + (Ident.name cd_id) false 0 depth obj + ty_args unbx + | Cstr_record lbls -> + let r = + tree_of_record_fields depth + env path type_params ty_list + lbls 0 obj unbx + in + Oval_constr(tree_of_constr env path + (Out_name.create (Ident.name cd_id)), + [ r ]) + end + + and tree_of_record depth env decl path ty_list obj lbl_list rep = + match check_depth depth obj ty with + | Some x -> x + | None -> + let pos = + match rep with + | Record_extension _ -> 1 + | _ -> 0 + in + let unbx = + match rep with Record_unboxed _ -> true | _ -> false + in + tree_of_record_fields depth + env path decl.type_params ty_list + lbl_list pos obj unbx + + and tree_of_record_fields depth env path type_params ty_list lbl_list pos obj unboxed = let rec tree_of_fields pos = function From e0aa9104444b96cedff473d7b34bf601e5a24884 Mon Sep 17 00:00:00 2001 From: Gabriel Scherer Date: Fri, 10 Sep 2021 22:16:54 +0200 Subject: [PATCH 33/45] [minor] genprintval.ml: clarify exception flow --- toplevel/genprintval.ml | 72 ++++++++++++++++++++--------------------- 1 file changed, 36 insertions(+), 36 deletions(-) diff --git a/toplevel/genprintval.ml b/toplevel/genprintval.ml index d588386d95e0..08b257e04c74 100644 --- a/toplevel/genprintval.ml +++ b/toplevel/genprintval.ml @@ -377,8 +377,10 @@ module Make(O : OBJ)(EVP : EVALPATH with type valu = O.t) = struct Oval_constr (Oide_ident (Out_name.create "lazy"), [v]) end | Tconstr(path, ty_list, _) -> begin - try - let decl = Env.find_type path env in + match Env.find_type path env with + | exception Not_found -> + Oval_stuff "" + | decl -> begin match decl with | {type_kind = Type_abstract; type_manifest = None} -> Oval_stuff "" @@ -391,11 +393,7 @@ module Make(O : OBJ)(EVP : EVALPATH with type valu = O.t) = struct tree_of_record depth env decl path ty_list obj lbl_list rep | {type_kind = Type_open} -> tree_of_extension path ty_list depth obj - with - Not_found -> (* raised by Env.find_type *) - Oval_stuff "" - | Datarepr.Constr_not_found -> (* raised by find_constr_by_tag *) - Oval_stuff "" + end end | Tvariant row -> let row = Btype.row_repr row in @@ -441,35 +439,37 @@ module Make(O : OBJ)(EVP : EVALPATH with type valu = O.t) = struct else if O.is_block obj then Cstr_block(O.tag obj) else Cstr_constant(O.obj obj) in - let {cd_id;cd_args;cd_res} = - Datarepr.find_constr_by_tag tag constr_list in - let type_params = - match cd_res with - Some t -> - begin match get_desc t with - Tconstr (_,params,_) -> - params - | _ -> assert false end - | None -> decl.type_params - in - begin - match cd_args with - | Cstr_tuple l -> - let ty_args = - instantiate_types env type_params ty_list l in - tree_of_constr_with_args (tree_of_constr env path) - (Ident.name cd_id) false 0 depth obj - ty_args unbx - | Cstr_record lbls -> - let r = - tree_of_record_fields depth - env path type_params ty_list - lbls 0 obj unbx - in - Oval_constr(tree_of_constr env path - (Out_name.create (Ident.name cd_id)), - [ r ]) - end + match Datarepr.find_constr_by_tag tag constr_list with + | exception Datarepr.Constr_not_found -> (* raised by find_constr_by_tag *) + Oval_stuff "" + | {cd_id;cd_args;cd_res} -> + let type_params = + match cd_res with + | Some t -> + begin match get_desc t with + Tconstr (_,params,_) -> + params + | _ -> assert false end + | None -> decl.type_params + in + begin + match cd_args with + | Cstr_tuple l -> + let ty_args = + instantiate_types env type_params ty_list l in + tree_of_constr_with_args (tree_of_constr env path) + (Ident.name cd_id) false 0 depth obj + ty_args unbx + | Cstr_record lbls -> + let r = + tree_of_record_fields depth + env path type_params ty_list + lbls 0 obj unbx + in + Oval_constr(tree_of_constr env path + (Out_name.create (Ident.name cd_id)), + [ r ]) + end and tree_of_record depth env decl path ty_list obj lbl_list rep = match check_depth depth obj ty with From 66bf6959502a48d4d4878f7f082f8f206aba7ee6 Mon Sep 17 00:00:00 2001 From: Gabriel Scherer Date: Tue, 14 Sep 2021 10:50:28 +0200 Subject: [PATCH 34/45] [WIP] Typedecl_unboxed: new operations on head shapes We introduce explicitly the "head" of a value; head shapes are finite approximations of sets of heads. We can compute the head of a value and check whether a head is included in a given head shape. This will be useful for toplevel/genprintval.ml which must dynamically decide the (possibly unboxed) constructor of a dynamic value of known type. TODO: we should discuss the placement of the types and operations, and document them; - maybe move the type of heads in types.mli - or maybe it's time to introduce dedicated compilation units, Head_shape_types (on which Types depends) and Head_shape (on which other units depend)? --- typing/typedecl_unboxed.ml | 32 ++++++++++++++++++++++++++++++++ typing/typedecl_unboxed.mli | 16 ++++++++++++++++ 2 files changed, 48 insertions(+) diff --git a/typing/typedecl_unboxed.ml b/typing/typedecl_unboxed.ml index a56ea08194b1..bc111eb45669 100644 --- a/typing/typedecl_unboxed.ml +++ b/typing/typedecl_unboxed.ml @@ -78,6 +78,26 @@ let match_primitive_type p = ] in List.find_opt (fun (p', _) -> Path.same p p') tbl |> Option.map snd +module Head = struct + type t = + | Imm of imm + | Block of tag + + let of_val (obj : Obj.t) = + if Obj.is_block obj + then Block (Obj.tag obj) + else Imm (Obj.obj obj : int) + + let mem head shape = + let mem h = function + | Shape_any -> true + | Shape_set hs -> List.mem h hs + in + match head with + | Imm n -> mem n shape.head_imm + | Block t -> mem t shape.head_blocks +end + module Head_shape = struct exception Conflict @@ -103,6 +123,9 @@ module Head_shape = struct let empty_shape = { head_imm = Shape_set []; head_blocks = Shape_set [] } + let imm_shape vals = + { head_imm = Shape_set vals; head_blocks = Shape_set [] } + let block_shape tags = { head_imm = Shape_set []; head_blocks = Shape_set tags } @@ -347,6 +370,15 @@ module Head_shape = struct let fill_cache env unboxed_cache = ignore (fill_and_get env unboxed_cache) + let of_cstr env = function + | Cstr_constant n -> imm_shape [n] + | Cstr_block t -> block_shape [t] + | Cstr_unboxed data -> fill_and_get env data + | Cstr_extension (_t, constant) -> + if constant + then block_shape [Obj.object_tag] + else block_shape [0] + let unboxed_type_data_of_shape shape = let bound_of_shape = function | Shape_set l -> Some (List.fold_left max 0 l) diff --git a/typing/typedecl_unboxed.mli b/typing/typedecl_unboxed.mli index 1eb5fce6a377..f34583c524b4 100644 --- a/typing/typedecl_unboxed.mli +++ b/typing/typedecl_unboxed.mli @@ -24,6 +24,18 @@ type t = (* for typeopt.ml *) val get_unboxed_type_representation: Env.t -> type_expr -> t +module Head : sig + type t = + | Imm of imm + | Block of tag + + val of_val : Obj.t -> t + + val mem : t -> Types.head_shape -> bool + (** [mem head head_shape] checks whether the [head] is included + in the set of heads represented by the [head_shape] approximation. *) +end + module Head_shape : sig type t = Types.head_shape @@ -46,5 +58,9 @@ module Head_shape : sig similarly to [get] above. *) val of_type : Env.t -> Path.t -> t + (** Returns the head shape information corresponding to the tag + of a datatype constructor. *) + val of_cstr : Env.t -> constructor_tag -> t + val unboxed_type_data_of_shape : t -> Types.unboxed_type_data end From 76c0062ca31a20c2d1599a90f9ad4bd2d2bf240d Mon Sep 17 00:00:00 2001 From: Gabriel Scherer Date: Tue, 14 Sep 2021 15:53:57 +0200 Subject: [PATCH 35/45] head_shape: expose printer for debugging --- typing/typedecl_unboxed.mli | 2 ++ 1 file changed, 2 insertions(+) diff --git a/typing/typedecl_unboxed.mli b/typing/typedecl_unboxed.mli index f34583c524b4..f86db2669903 100644 --- a/typing/typedecl_unboxed.mli +++ b/typing/typedecl_unboxed.mli @@ -39,6 +39,8 @@ end module Head_shape : sig type t = Types.head_shape + val pp : Format.formatter -> t -> unit + (** Check a new type decalaration, that may be a variant type containing unboxed constructors, to verify that the unboxing requests respect the "disjointness" requirement of constructor From e705659dd1b9d488e6876cc9b30bd017d1105515 Mon Sep 17 00:00:00 2001 From: Gabriel Scherer Date: Tue, 14 Sep 2021 15:54:28 +0200 Subject: [PATCH 36/45] toplevel/genprintval.ml: support unboxed constructors --- testsuite/tests/tool-toplevel/printval.ml | 27 +++++++++++++++ toplevel/genprintval.ml | 40 +++++++++++++++++------ 2 files changed, 57 insertions(+), 10 deletions(-) diff --git a/testsuite/tests/tool-toplevel/printval.ml b/testsuite/tests/tool-toplevel/printval.ml index 17c2744440b9..4b660c20389a 100644 --- a/testsuite/tests/tool-toplevel/printval.ml +++ b/testsuite/tests/tool-toplevel/printval.ml @@ -58,3 +58,30 @@ T 'x' type _ t += T : 'a -> ('a * bool) t - : (char * bool) t = T 'x' |}] + + +(* printing of unboxed constructors *) +type t = + | Int of int [@unboxed] + | Str of string [@unboxed] + | Pair of t * t + | Proxy of t +;; +[%%expect {| +type t = Int of int | Str of string | Pair of t * t | Proxy of t +|}];; + +Int 42;; +[%%expect {| +- : t = Int 42 +|}];; + +Str "foo";; +[%%expect {| +- : t = Str "foo" +|}];; + +Pair (Int 42, Proxy (Str "foo"));; +[%%expect {| +- : t = Pair (Int 42, Proxy (Str "foo")) +|}] diff --git a/toplevel/genprintval.ml b/toplevel/genprintval.ml index 08b257e04c74..1965d2ceb30b 100644 --- a/toplevel/genprintval.ml +++ b/toplevel/genprintval.ml @@ -431,18 +431,33 @@ module Make(O : OBJ)(EVP : EVALPATH with type valu = O.t) = struct Oval_stuff "" end - and tree_of_variant depth env decl path ty_list obj constr_list rep = + and tree_of_variant depth env decl path ty_list obj constr_decl_list rep = + let constr_descr_list = + match Env.find_type_descrs path env with + | exception Not_found -> assert false + | Type_variant (constr_list, _) -> constr_list + | Type_abstract | Type_record _ | Type_open -> assert false + in let unbx = (rep = Variant_unboxed) in - let tag = - if unbx then (* XXX unboxing Cstr_unboxed [] *) - assert false - else if O.is_block obj - then Cstr_block(O.tag obj) - else Cstr_constant(O.obj obj) in - match Datarepr.find_constr_by_tag tag constr_list with - | exception Datarepr.Constr_not_found -> (* raised by find_constr_by_tag *) + let obj_head = + (* We cannot use Typedecl_unbodex.Head.of_val directly + as we are functorized over the implementation of Obj. *) + let module Head = Typedecl_unboxed.Head in + if O.is_block obj + then Head.Block (O.tag obj) + else Head.Imm (O.obj obj : int) + in + let cstr_info = + List.combine constr_decl_list constr_descr_list + |> List.find_opt (fun (_decl, descr) -> + let cstr_shape = Typedecl_unboxed.Head_shape.of_cstr env descr.cstr_tag in + Typedecl_unboxed.Head.mem obj_head cstr_shape + ) + in + match cstr_info with + | None -> Oval_stuff "" - | {cd_id;cd_args;cd_res} -> + | Some ({cd_id; cd_args; cd_res; _}, {cstr_tag; _}) -> let type_params = match cd_res with | Some t -> @@ -452,6 +467,11 @@ module Make(O : OBJ)(EVP : EVALPATH with type valu = O.t) = struct | _ -> assert false end | None -> decl.type_params in + let unbx = + unbx || match cstr_tag with + | Cstr_unboxed _ -> true + | Cstr_constant _ | Cstr_block _ | Cstr_extension _ -> false + in begin match cd_args with | Cstr_tuple l -> From 22c5041e0cf13f026aa0433560118759989e9982 Mon Sep 17 00:00:00 2001 From: Gabriel Scherer Date: Tue, 14 Sep 2021 21:20:58 +0200 Subject: [PATCH 37/45] [refactoring] Outcometree: introduce a record type for constructors --- typing/oprint.ml | 31 +++++++++++++++++++++++-------- typing/oprint.mli | 3 +-- typing/outcometree.mli | 10 ++++++++-- typing/printtyp.ml | 18 +++++++++++++++--- 4 files changed, 47 insertions(+), 15 deletions(-) diff --git a/typing/oprint.ml b/typing/oprint.ml index 7a47cab446e3..eb4c7b173565 100644 --- a/typing/oprint.ml +++ b/typing/oprint.ml @@ -495,6 +495,15 @@ let collect_functor_args mty = let l, rest = collect_functor_args [] mty in List.rev l, rest +let constructor_of_extension_constructor + (ext : out_extension_constructor) : out_constructor += + { + ocstr_name = ext.oext_name; + ocstr_args = ext.oext_args; + ocstr_return_type = ext.oext_ret_type; + } + let split_anon_functor_arguments params = let rec uncollect_anonymous_suffix acc rest = match acc with | Some (None, mty_arg) :: acc -> @@ -560,13 +569,13 @@ and print_out_signature ppf = match items with Osig_typext(ext, Oext_next) :: items -> gather_extensions - ((ext.oext_name, ext.oext_args, ext.oext_ret_type) :: acc) + (constructor_of_extension_constructor ext :: acc) items | _ -> (List.rev acc, items) in let exts, items = gather_extensions - [(ext.oext_name, ext.oext_args, ext.oext_ret_type)] + [constructor_of_extension_constructor ext] items in let te = @@ -592,7 +601,7 @@ and print_out_sig_item ppf = name !out_class_type clt | Osig_typext (ext, Oext_exception) -> fprintf ppf "@[<2>exception %a@]" - print_out_constr (ext.oext_name, ext.oext_args, ext.oext_ret_type) + print_out_constr (constructor_of_extension_constructor ext) | Osig_typext (ext, _es) -> print_out_extension_constructor ppf ext | Osig_modtype (name, Omty_abstract) -> @@ -702,13 +711,18 @@ and print_out_type_decl kwd ppf td = print_immediate print_unboxed -and print_out_constr ppf (name, tyl,ret_type_opt) = +and print_out_constr ppf constr = + let { + ocstr_name = name; + ocstr_args = tyl; + ocstr_return_type = return_type; + } = constr in let name = match name with | "::" -> "(::)" (* #7200 *) | s -> s in - match ret_type_opt with + match return_type with | None -> begin match tyl with | [] -> @@ -745,7 +759,8 @@ and print_out_extension_constructor ppf ext = fprintf ppf "@[type %t +=%s@;<1 2>%a@]" print_extended_type (if ext.oext_private = Asttypes.Private then " private" else "") - print_out_constr (ext.oext_name, ext.oext_args, ext.oext_ret_type) + print_out_constr + (constructor_of_extension_constructor ext) and print_out_type_extension ppf te = let print_extended_type ppf = @@ -795,13 +810,13 @@ let rec print_items ppf = match items with (Osig_typext(ext, Oext_next), None) :: items -> gather_extensions - ((ext.oext_name, ext.oext_args, ext.oext_ret_type) :: acc) + (constructor_of_extension_constructor ext :: acc) items | _ -> (List.rev acc, items) in let exts, items = gather_extensions - [(ext.oext_name, ext.oext_args, ext.oext_ret_type)] + [constructor_of_extension_constructor ext] items in let te = diff --git a/typing/oprint.mli b/typing/oprint.mli index bafd17ccf126..baa733d82457 100644 --- a/typing/oprint.mli +++ b/typing/oprint.mli @@ -20,8 +20,7 @@ val out_ident : (formatter -> out_ident -> unit) ref val out_value : (formatter -> out_value -> unit) ref val out_label : (formatter -> string * bool * out_type -> unit) ref val out_type : (formatter -> out_type -> unit) ref -val out_constr : - (formatter -> string * out_type list * out_type option -> unit) ref +val out_constr : (formatter -> out_constructor -> unit) ref val out_class_type : (formatter -> out_class_type -> unit) ref val out_module_type : (formatter -> out_module_type -> unit) ref val out_sig_item : (formatter -> out_sig_item -> unit) ref diff --git a/typing/outcometree.mli b/typing/outcometree.mli index d9b4f04c1c71..8e8dfcac3e89 100644 --- a/typing/outcometree.mli +++ b/typing/outcometree.mli @@ -69,7 +69,7 @@ type out_type = | Otyp_object of (string * out_type) list * bool option | Otyp_record of (string * bool * out_type) list | Otyp_stuff of string - | Otyp_sum of (string * out_type list * out_type option) list + | Otyp_sum of out_constructor list | Otyp_tuple of out_type list | Otyp_var of bool * string | Otyp_variant of @@ -78,6 +78,12 @@ type out_type = | Otyp_module of out_ident * (string * out_type) list | Otyp_attribute of out_type * out_attribute +and out_constructor = { + ocstr_name: string; + ocstr_args: out_type list; + ocstr_return_type: out_type option; +} + and out_variant = | Ovar_fields of (string * bool * out_type list) list | Ovar_typ of out_type @@ -128,7 +134,7 @@ and out_extension_constructor = and out_type_extension = { otyext_name: string; otyext_params: string list; - otyext_constructors: (string * out_type list * out_type option) list; + otyext_constructors: out_constructor list; otyext_private: Asttypes.private_flag } and out_val_decl = { oval_name: string; diff --git a/typing/printtyp.ml b/typing/printtyp.ml index c35b7e8a1e21..719979e90563 100644 --- a/typing/printtyp.ml +++ b/typing/printtyp.ml @@ -1421,12 +1421,20 @@ and tree_of_constructor cd = let name = Ident.name cd.cd_id in let arg () = tree_of_constructor_arguments cd.cd_args in match cd.cd_res with - | None -> (name, arg (), None) + | None -> { + ocstr_name = name; + ocstr_args = arg (); + ocstr_return_type = None; + } | Some res -> Names.with_local_names (fun () -> let ret = tree_of_typexp Type res in let args = arg () in - (name, args, Some ret)) + { + ocstr_name = name; + ocstr_args = args; + ocstr_return_type = Some ret; + }) and tree_of_label l = (Ident.name l.ld_id, l.ld_mutable = Mutable, tree_of_typexp Type l.ld_type) @@ -1511,7 +1519,11 @@ let extension_only_constructor id ppf ext = ext.ext_ret_type in Format.fprintf ppf "@[%a@]" - !Oprint.out_constr (name, args, ret) + !Oprint.out_constr { + ocstr_name = name; + ocstr_args = args; + ocstr_return_type = ret; + } (* Print a value declaration *) From 58260e3d11d566168e75fa1dd192882165181dc7 Mon Sep 17 00:00:00 2001 From: Gabriel Scherer Date: Tue, 14 Sep 2021 21:37:33 +0200 Subject: [PATCH 38/45] outcometree: print [@unboxed] attributes --- testsuite/tests/tool-toplevel/printval.ml | 6 +++++- typing/oprint.ml | 16 +++++++++++++--- typing/outcometree.mli | 1 + typing/printtyp.ml | 4 ++++ 4 files changed, 23 insertions(+), 4 deletions(-) diff --git a/testsuite/tests/tool-toplevel/printval.ml b/testsuite/tests/tool-toplevel/printval.ml index 4b660c20389a..b7f220dd3ba6 100644 --- a/testsuite/tests/tool-toplevel/printval.ml +++ b/testsuite/tests/tool-toplevel/printval.ml @@ -68,7 +68,11 @@ type t = | Proxy of t ;; [%%expect {| -type t = Int of int | Str of string | Pair of t * t | Proxy of t +type t = + Int of int [@unboxed] + | Str of string [@unboxed] + | Pair of t * t + | Proxy of t |}];; Int 42;; diff --git a/typing/oprint.ml b/typing/oprint.ml index eb4c7b173565..eba942d11b56 100644 --- a/typing/oprint.ml +++ b/typing/oprint.ml @@ -502,6 +502,7 @@ let constructor_of_extension_constructor ocstr_name = ext.oext_name; ocstr_args = ext.oext_args; ocstr_return_type = ext.oext_ret_type; + ocstr_unboxed = false; } let split_anon_functor_arguments params = @@ -716,29 +717,38 @@ and print_out_constr ppf constr = ocstr_name = name; ocstr_args = tyl; ocstr_return_type = return_type; + ocstr_unboxed = unboxed; } = constr in let name = match name with | "::" -> "(::)" (* #7200 *) | s -> s in + let pp_unboxed ppf = function + | false -> () + | true -> fprintf ppf "@ [@unboxed]" + in match return_type with | None -> begin match tyl with | [] -> pp_print_string ppf name | _ -> - fprintf ppf "@[<2>%s of@ %a@]" name + fprintf ppf "@[<2>%s of@ %a%a@]" name (print_typlist print_simple_out_type " *") tyl + pp_unboxed unboxed end | Some ret_type -> begin match tyl with | [] -> - fprintf ppf "@[<2>%s :@ %a@]" name print_simple_out_type ret_type + fprintf ppf "@[<2>%s :@ %a%a@]" name + print_simple_out_type ret_type + pp_unboxed unboxed | _ -> - fprintf ppf "@[<2>%s :@ %a -> %a@]" name + fprintf ppf "@[<2>%s :@ %a -> %a%a@]" name (print_typlist print_simple_out_type " *") tyl print_simple_out_type ret_type + pp_unboxed unboxed end and print_out_extension_constructor ppf ext = diff --git a/typing/outcometree.mli b/typing/outcometree.mli index 8e8dfcac3e89..bd6e7e0bcf7a 100644 --- a/typing/outcometree.mli +++ b/typing/outcometree.mli @@ -82,6 +82,7 @@ and out_constructor = { ocstr_name: string; ocstr_args: out_type list; ocstr_return_type: out_type option; + ocstr_unboxed: bool; } and out_variant = diff --git a/typing/printtyp.ml b/typing/printtyp.ml index 719979e90563..16c43c5056c7 100644 --- a/typing/printtyp.ml +++ b/typing/printtyp.ml @@ -1420,11 +1420,13 @@ and tree_of_constructor_arguments = function and tree_of_constructor cd = let name = Ident.name cd.cd_id in let arg () = tree_of_constructor_arguments cd.cd_args in + let unboxed = Builtin_attributes.has_unboxed cd.cd_attributes in match cd.cd_res with | None -> { ocstr_name = name; ocstr_args = arg (); ocstr_return_type = None; + ocstr_unboxed = unboxed; } | Some res -> Names.with_local_names (fun () -> @@ -1434,6 +1436,7 @@ and tree_of_constructor cd = ocstr_name = name; ocstr_args = args; ocstr_return_type = Some ret; + ocstr_unboxed = unboxed; }) and tree_of_label l = @@ -1523,6 +1526,7 @@ let extension_only_constructor id ppf ext = ocstr_name = name; ocstr_args = args; ocstr_return_type = ret; + ocstr_unboxed = false; } (* Print a value declaration *) From 717e88bc62af14141392f2d7b63bbfe0a40bb3f8 Mon Sep 17 00:00:00 2001 From: Gabriel Scherer Date: Thu, 16 Sep 2021 18:48:52 +0200 Subject: [PATCH 39/45] oops: restore the fatal error when declaring conflicting types (report from Guillaume Munch-Maccagnoni) --- typing/typedecl_unboxed.ml | 11 ++++++++--- 1 file changed, 8 insertions(+), 3 deletions(-) diff --git a/typing/typedecl_unboxed.ml b/typing/typedecl_unboxed.ml index bc111eb45669..158a96a40d16 100644 --- a/typing/typedecl_unboxed.ml +++ b/typing/typedecl_unboxed.ml @@ -422,11 +422,16 @@ module Head_shape = struct pp shape end with Conflict -> - (* TODO raise a fatal error with a registered printer, - instead of what is below. *) if !Clflags.dump_headshape then Format.fprintf Format.err_formatter "SHAPE(%a) CONFLICT@." - Path.print path + Path.print path; + (* TODO raise a fatal error with a registered printer, + instead of what is below. *) + Location.raise_errorf ~loc:decl.type_loc + "%a" + Format.pp_print_text + "This declaration is invalid, some [@unboxed] annotations \ + introduce overlapping representations." end | _ -> () From 7ad168f8202f4c7ecb9ada05cc7509e0f73e512d Mon Sep 17 00:00:00 2001 From: Gabriel Scherer Date: Thu, 16 Sep 2021 18:53:55 +0200 Subject: [PATCH 40/45] more precise head shape for function types (suggestion from Guillaume Munch-Maccagnoni) --- HEAD_SHAPE.impl.md | 3 --- typing/typedecl_unboxed.ml | 3 ++- 2 files changed, 2 insertions(+), 4 deletions(-) diff --git a/HEAD_SHAPE.impl.md b/HEAD_SHAPE.impl.md index ce19c7675418..09d03442cafc 100644 --- a/HEAD_SHAPE.impl.md +++ b/HEAD_SHAPE.impl.md @@ -135,9 +135,6 @@ The computation of the head shape is done in the functions `of_type_expr` and `o In particular, the definition of head shape on "base types" relies on a [`match_primitive`](https://github.com/gasche/ocaml/blob/head_shape/typing/typedecl_unboxed.ml#L65) function recognized a set of builtin type paths (we borrowed the logic from [Typeopt.classify](https://github.com/gasche/ocaml/blob/head_shape/typing/typeopt.ml#L75)). -TODO: there is no special support for `Tarrow` for now, it returns `any_shape` instead of {Closure,Infix}. (Is it by explicit choice?) - - ### Storing unboxing information in type descriptions This, surprisingly, turned out to be the most difficult part of the PR to get right. diff --git a/typing/typedecl_unboxed.ml b/typing/typedecl_unboxed.ml index 158a96a40d16..ec5eb9424e5e 100644 --- a/typing/typedecl_unboxed.ml +++ b/typing/typedecl_unboxed.ml @@ -253,7 +253,8 @@ module Head_shape = struct (Callstack.visit p head_callstack) end | Ttuple _ -> block_shape [0] - | Tarrow _ | Tpackage _ | Tobject _ | Tnil | Tvariant _ -> (* XXX *) + | Tarrow _ -> block_shape [Obj.closure_tag; Obj.infix_tag] + | Tpackage _ | Tobject _ | Tnil | Tvariant _ -> (* XXX *) any_shape | Tlink _ | Tsubst _ | Tpoly _ | Tfield _ -> assert false From 5c5336da4a0ac285620f50b6fa54ac1f6271e7c0 Mon Sep 17 00:00:00 2001 From: Nicolas Chataing Date: Tue, 21 Sep 2021 21:11:30 +0200 Subject: [PATCH 41/45] separability --- testsuite/tests/typing-unboxed-types/test.ml | 20 ++++++ .../test_unboxed_constr.ml | 38 ++++++------ typing/typedecl_unboxed.ml | 61 +++++++++++++++---- typing/types.ml | 1 + typing/types.mli | 1 + 5 files changed, 92 insertions(+), 29 deletions(-) diff --git a/testsuite/tests/typing-unboxed-types/test.ml b/testsuite/tests/typing-unboxed-types/test.ml index 32e32a7859fe..e336c9447e90 100644 --- a/testsuite/tests/typing-unboxed-types/test.ml +++ b/testsuite/tests/typing-unboxed-types/test.ml @@ -252,6 +252,7 @@ Error: Signature mismatch: (* Check interference with representation of float arrays. *) type t11 = L of float [@@ocaml.unboxed];; [%%expect{| +t11/225[42] IS NOT SEPARABLE type t11 = L of float [@@unboxed] |}];; let x = Array.make 10 (L 3.14) (* represented as a flat array *) @@ -309,6 +310,25 @@ end = struct type u = { f1 : t; f2 : t } end;; [%%expect{| +t/562[54] IS NOT SEPARABLE +Lines 4-7, characters 6-3: +4 | ......struct +5 | type t = A of float [@@ocaml.unboxed] +6 | type u = { f1 : t; f2 : t } +7 | end.. +Error: Signature mismatch: + Modules do not match: + sig type t = A of float [@@unboxed] type u = { f1 : t; f2 : t; } end + is not included in + sig type t type u = { f1 : t; f2 : t; } end + Type declarations do not match: + type u = { f1 : t; f2 : t; } + is not included in + type u = { f1 : t; f2 : t; } + Their internal representations differ: + the first declaration uses unboxed float representation. +|}, Principal{| +t/562[55] IS NOT SEPARABLE Lines 4-7, characters 6-3: 4 | ......struct 5 | type t = A of float [@@ocaml.unboxed] diff --git a/testsuite/tests/typing-unboxed-types/test_unboxed_constr.ml b/testsuite/tests/typing-unboxed-types/test_unboxed_constr.ml index 13ac27641949..559efd0fb26e 100644 --- a/testsuite/tests/typing-unboxed-types/test_unboxed_constr.ml +++ b/testsuite/tests/typing-unboxed-types/test_unboxed_constr.ml @@ -6,63 +6,67 @@ (* Check the unboxing of constructors *) type t = A of int | B;; [%%expect{| -SHAPE(t/88[1]) {head_imm = Shape_set [0]; head_blocks = Shape_set [0]} +SHAPE(t/88[1]) {head_imm = Shape_set [0]; head_blocks = Shape_set [0]; head_separated = true} type t = A of int | B |}];; type t = A of int | B of float | C | D;; [%%expect{| -SHAPE(t/91[2]) {head_imm = Shape_set [0; 1]; head_blocks = Shape_set [0; 1]} +SHAPE(t/91[2]) {head_imm = Shape_set [0; 1]; head_blocks = Shape_set [0; 1]; head_separated = true} type t = A of int | B of float | C | D |}];; type t = A of int [@unboxed] | B;; [%%expect{| SHAPE(t/96[3]) CONFLICT -type t = A of int | B +type t = A of int [@unboxed] | B |}];; type t = A of float [@unboxed] | B;; [%%expect{| -SHAPE(t/99[4]) {head_imm = Shape_set [0]; head_blocks = Shape_set [253]} -type t = A of float | B +t/99[4] IS NOT SEPARABLE +SHAPE(t/99[4]) {head_imm = Shape_set [0]; head_blocks = Shape_set [253]; head_separated = false} +type t = A of float [@unboxed] | B |}];; type t = A of float [@unboxed] | B of string [@unboxed] | C | D of int;; [%%expect{| -SHAPE(t/102[5]) {head_imm = Shape_set [0]; head_blocks = Shape_set [0; 252; 253]} -type t = A of float | B of string | C | D of int +t/102[5] IS NOT SEPARABLE +SHAPE(t/102[5]) {head_imm = Shape_set [0]; head_blocks = Shape_set [0; 252; 253]; head_separated = false} +type t = A of float [@unboxed] | B of string [@unboxed] | C | D of int |}];; type t = K of int u u [@unboxed] and 'a u = 'a id and 'a id = Id of 'a [@unboxed];; [%%expect{| -SHAPE(t/107[6]) {head_imm = Shape_any; head_blocks = Shape_set []} -SHAPE(id/109[6]) {head_imm = Shape_any; head_blocks = Shape_any} -type t = K of int u u +SHAPE(t/107[6]) {head_imm = Shape_any; head_blocks = Shape_set []; head_separated = true} +id/109[6] IS NOT SEPARABLE +SHAPE(id/109[6]) {head_imm = Shape_any; head_blocks = Shape_any; head_separated = false} +type t = K of int u u [@unboxed] and 'a u = 'a id -and 'a id = Id of 'a +and 'a id = Id of 'a [@unboxed] |}];; type t = { a : int } [@@unboxed] and tt = A of t [@unboxed];; [%%expect{| -SHAPE(tt/113[7]) {head_imm = Shape_any; head_blocks = Shape_set []} +SHAPE(tt/113[7]) {head_imm = Shape_any; head_blocks = Shape_set []; head_separated = true} type t = { a : int; } [@@unboxed] -and tt = A of t +and tt = A of t [@unboxed] |}];; type t = A of { a : int } [@unboxed];; [%%expect{| -SHAPE(t/116[8]) {head_imm = Shape_any; head_blocks = Shape_set []} -type t = A of { a : int; } +SHAPE(t/116[8]) {head_imm = Shape_any; head_blocks = Shape_set []; head_separated = true} +type t = A of { a : int; } [@unboxed] |}];; type ('a, 'r) u = 'r and 'a t = A of { body : 'r. ('a, 'r) u } [@unboxed];; [%%expect{| -SHAPE(t/120[9]) {head_imm = Shape_any; head_blocks = Shape_any} +t/120[9] IS NOT SEPARABLE +SHAPE(t/120[9]) {head_imm = Shape_any; head_blocks = Shape_any; head_separated = false} type ('a, 'r) u = 'r -and 'a t = A of { body : 'r. ('a, 'r) u; } +and 'a t = A of { body : 'r. ('a, 'r) u; } [@unboxed] |}];; diff --git a/typing/typedecl_unboxed.ml b/typing/typedecl_unboxed.ml index ec5eb9424e5e..8ca7907f6100 100644 --- a/typing/typedecl_unboxed.ml +++ b/typing/typedecl_unboxed.ml @@ -114,26 +114,42 @@ module Head_shape = struct ~pp_sep:(fun ppf () -> Format.fprintf ppf "; ") Format.pp_print_int) l - let pp ppf {head_imm; head_blocks} = - Format.fprintf ppf "{head_imm = %a; head_blocks = %a}" + let pp ppf {head_imm; head_blocks; head_separated} = + Format.fprintf ppf "{head_imm = %a; head_blocks = %a; head_separated = %b}" pp_shape head_imm pp_shape head_blocks + head_separated - let any_shape = { head_imm = Shape_any; head_blocks = Shape_any } + let any_shape = + { head_imm = Shape_any; head_blocks = Shape_any; head_separated = false } - let empty_shape = { head_imm = Shape_set []; head_blocks = Shape_set [] } + let empty_shape = + { + head_imm = Shape_set []; + head_blocks = Shape_set []; + head_separated = true; + } let imm_shape vals = - { head_imm = Shape_set vals; head_blocks = Shape_set [] } + { + head_imm = Shape_set vals; + head_blocks = Shape_set []; + head_separated = true; + } let block_shape tags = - { head_imm = Shape_set []; head_blocks = Shape_set tags } + let head_separated = + List.for_all (fun x -> x = Obj.double_tag) tags || + List.for_all (fun x -> x <> Obj.double_tag) tags + in + { head_imm = Shape_set []; head_blocks = Shape_set tags; head_separated } let cstrs_shape ~num_consts ~num_nonconsts = let int_list n = List.init n Fun.id in { head_imm = Shape_set (int_list num_consts); - head_blocks = Shape_set (int_list num_nonconsts) + head_blocks = Shape_set (int_list num_nonconsts); + head_separated = true; } let disjoint_union hd1 hd2 = @@ -150,10 +166,23 @@ module Head_shape = struct else y :: (merge l1 yy) in Shape_set (merge l1 l2) in - { - head_imm = union hd1.head_imm hd2.head_imm; - head_blocks = union hd1.head_blocks hd2.head_blocks - } + let head_imm = union hd1.head_imm hd2.head_imm in + let head_blocks = union hd1.head_blocks hd2.head_blocks in + let head_separated = + hd1.head_separated && + hd2.head_separated && + match head_blocks with + | Shape_any -> false + | Shape_set tags -> + ( + head_imm = Shape_set [] && + List.for_all (fun x -> x = Obj.double_tag) tags + ) || + ( + List.for_all (fun x -> x <> Obj.double_tag) tags + ) + in + { head_imm; head_blocks; head_separated } module Callstack = struct type t = Path.t list @@ -211,7 +240,12 @@ module Head_shape = struct | _ -> ty let of_primitive_type = function - | Int -> { head_imm = Shape_any; head_blocks = Shape_set [] } + | Int -> + { + head_imm = Shape_any; + head_blocks = Shape_set []; + head_separated = true; + } | Float -> block_shape [Obj.double_tag] | String | Bytes -> block_shape [Obj.string_tag] @@ -410,6 +444,9 @@ module Head_shape = struct let ty = Btype.newgenty (Tconstr (path, params, ref Mnil)) in let callstack_map = Callstack.fill ty [] in let shape = of_type_expr env ty callstack_map in + if Config.flat_float_array && not shape.head_separated then + Format.fprintf Format.err_formatter "%a IS NOT SEPARABLE@." + Path.print path; (* Fill the variant data *) match cstrs with | [] -> () diff --git a/typing/types.ml b/typing/types.ml index fdc7f7dddd00..bc40bdb9b4df 100644 --- a/typing/types.ml +++ b/typing/types.ml @@ -432,6 +432,7 @@ and unboxed_data = and head_shape = { head_imm: imm shape; (* set of immediates the head can be *) head_blocks: tag shape; (* set of tags the head can have *) + head_separated: bool; (* is the set of values separated? *) } and 'a shape = diff --git a/typing/types.mli b/typing/types.mli index 3891872bdf67..15bd0d98b584 100644 --- a/typing/types.mli +++ b/typing/types.mli @@ -631,6 +631,7 @@ and unboxed_data = and head_shape = { head_imm : imm shape; (* set of immediates the head can be *) head_blocks : tag shape; (* set of tags the head can have *) + head_separated : bool; (* is the set of value separated? *) } (* A description of a set of ['a] elements. *) From 45f2c11d0f2f028ff53f10a92b3267f5a3aa4d6e Mon Sep 17 00:00:00 2001 From: Nicolas Chataing Date: Tue, 21 Sep 2021 22:00:57 +0200 Subject: [PATCH 42/45] fix bug with global [@@unboxed] annotation --- typing/datarepr.ml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/typing/datarepr.ml b/typing/datarepr.ml index ea17a48411e0..817fa997bc14 100644 --- a/typing/datarepr.ml +++ b/typing/datarepr.ml @@ -104,7 +104,8 @@ let constructor_descrs ~current_unit ty_path decl cstrs rep = let num_consts = ref 0 and num_nonconsts = ref 0 and num_unboxed = ref 0 in List.iter (fun {cd_args; cd_attributes; _} -> - if Builtin_attributes.has_unboxed cd_attributes then incr num_unboxed + if variant_unboxed || Builtin_attributes.has_unboxed cd_attributes + then incr num_unboxed else if cd_args = Cstr_tuple [] then incr num_consts else incr num_nonconsts; ) cstrs; From 6a8c98e79fbf566beb6d2051669508aaffd2b543 Mon Sep 17 00:00:00 2001 From: Gabriel Scherer Date: Tue, 21 Sep 2021 22:13:10 +0200 Subject: [PATCH 43/45] update the testsuite --- testsuite/tests/letrec-check/unboxed.ml | 14 +++--- testsuite/tests/typing-unboxed-types/test.ml | 43 ++++++++++--------- .../tests/typing-unboxed-types/test_flat.ml | 13 ++++++ .../test_unboxed_constr.ml | 6 ++- .../test_unboxed_constr_matching.ml | 4 +- testsuite/tests/typing-unboxed/test.ml | 6 ++- 6 files changed, 57 insertions(+), 29 deletions(-) diff --git a/testsuite/tests/letrec-check/unboxed.ml b/testsuite/tests/letrec-check/unboxed.ml index 7c04199ec986..0449e01bbe5e 100644 --- a/testsuite/tests/letrec-check/unboxed.ml +++ b/testsuite/tests/letrec-check/unboxed.ml @@ -20,14 +20,18 @@ Line 2, characters 12-19: Error: This kind of expression is not allowed as right-hand side of `let rec' |}];; +(* Note: this declaration is currently rejected by the + termination criterion, but ideally we would want to allow it + as it is a case of benign cycle that can occur by revealing + an abstract type. See #10485. *) type r = A of r [@@unboxed] let rec y = A y;; [%%expect{| -type r = A of r [@@unboxed] -Line 2, characters 12-15: -2 | let rec y = A y;; - ^^^ -Error: This kind of expression is not allowed as right-hand side of `let rec' +Line 1, characters 0-27: +1 | type r = A of r [@@unboxed] + ^^^^^^^^^^^^^^^^^^^^^^^^^^^ +Error: Cyclic type expansion during [@unboxed] verification. + r/95[3] appears unboxed at the head of its own definition. |}];; (* This test is not allowed if 'a' is unboxed, but should be accepted diff --git a/testsuite/tests/typing-unboxed-types/test.ml b/testsuite/tests/typing-unboxed-types/test.ml index e336c9447e90..70ee16f20d34 100644 --- a/testsuite/tests/typing-unboxed-types/test.ml +++ b/testsuite/tests/typing-unboxed-types/test.ml @@ -252,7 +252,6 @@ Error: Signature mismatch: (* Check interference with representation of float arrays. *) type t11 = L of float [@@ocaml.unboxed];; [%%expect{| -t11/225[42] IS NOT SEPARABLE type t11 = L of float [@@unboxed] |}];; let x = Array.make 10 (L 3.14) (* represented as a flat array *) @@ -297,6 +296,11 @@ type t14;; type t15 = A of t14 [@@ocaml.unboxed];; [%%expect{| type t14 +t15/560[52] IS NOT SEPARABLE +type t15 = A of t14 [@@unboxed] +|}, Principal{| +type t14 +t15/560[53] IS NOT SEPARABLE type t15 = A of t14 [@@unboxed] |}];; @@ -310,25 +314,6 @@ end = struct type u = { f1 : t; f2 : t } end;; [%%expect{| -t/562[54] IS NOT SEPARABLE -Lines 4-7, characters 6-3: -4 | ......struct -5 | type t = A of float [@@ocaml.unboxed] -6 | type u = { f1 : t; f2 : t } -7 | end.. -Error: Signature mismatch: - Modules do not match: - sig type t = A of float [@@unboxed] type u = { f1 : t; f2 : t; } end - is not included in - sig type t type u = { f1 : t; f2 : t; } end - Type declarations do not match: - type u = { f1 : t; f2 : t; } - is not included in - type u = { f1 : t; f2 : t; } - Their internal representations differ: - the first declaration uses unboxed float representation. -|}, Principal{| -t/562[55] IS NOT SEPARABLE Lines 4-7, characters 6-3: 4 | ......struct 5 | type t = A of float [@@ocaml.unboxed] @@ -367,6 +352,12 @@ type 'a packed = T : ('a, _) t -> 'a packed [@@unboxed] [%%expect{| type 'a s type ('a, 'p) t = private 'a s +packed/579[63] IS NOT SEPARABLE +type 'a packed = T : ('a, 'b) t -> 'a packed [@@unboxed] +|}, Principal{| +type 'a s +type ('a, 'p) t = private 'a s +packed/579[64] IS NOT SEPARABLE type 'a packed = T : ('a, 'b) t -> 'a packed [@@unboxed] |}];; @@ -387,6 +378,11 @@ type 'a t [@@immediate];; type u = U : 'a t -> u [@@unboxed];; [%%expect{| type 'a t [@@immediate] +u/587[66] IS NOT SEPARABLE +type u = U : 'a t -> u [@@unboxed] +|}, Principal{| +type 'a t [@@immediate] +u/587[67] IS NOT SEPARABLE type u = U : 'a t -> u [@@unboxed] |}];; @@ -395,6 +391,13 @@ type u = U : 'a t -> u [@@unboxed] type ('a, 'b) t = K : 'c -> (bool, 'c) t [@@unboxed] and t1 = T1 : (bool, int) t -> t1 [@@unboxed] [%%expect{| +t/589[67] IS NOT SEPARABLE +t1/590[67] IS NOT SEPARABLE +type ('a, 'b) t = K : 'c -> (bool, 'c) t [@@unboxed] +and t1 = T1 : (bool, int) t -> t1 [@@unboxed] +|}, Principal{| +t/589[68] IS NOT SEPARABLE +t1/590[68] IS NOT SEPARABLE type ('a, 'b) t = K : 'c -> (bool, 'c) t [@@unboxed] and t1 = T1 : (bool, int) t -> t1 [@@unboxed] |}];; diff --git a/testsuite/tests/typing-unboxed-types/test_flat.ml b/testsuite/tests/typing-unboxed-types/test_flat.ml index c093efe1089f..3014f7acb5c5 100644 --- a/testsuite/tests/typing-unboxed-types/test_flat.ml +++ b/testsuite/tests/typing-unboxed-types/test_flat.ml @@ -34,6 +34,7 @@ Error: This type cannot be unboxed because type 'a s = S : 'a -> 'a s [@@unboxed];; type t = T : 'a s -> t [@@unboxed];; [%%expect{| +s/93[4] IS NOT SEPARABLE type 'a s = S : 'a -> 'a s [@@unboxed] Line 2, characters 0-34: 2 | type t = T : 'a s -> t [@@unboxed];; @@ -48,6 +49,7 @@ Error: This type cannot be unboxed because type 'a s = S : 'a -> 'a option s [@@unboxed];; type t = T : 'a s -> t [@@unboxed];; [%%expect{| +s/97[6] IS NOT SEPARABLE type 'a s = S : 'a -> 'a option s [@@unboxed] Line 2, characters 0-34: 2 | type t = T : 'a s -> t [@@unboxed];; @@ -86,6 +88,7 @@ Error: This type cannot be unboxed because (* accept *) type 'a s = S : (unit -> 'a) M.r -> 'a option s [@@unboxed];; [%%expect{| +s/110[12] IS NOT SEPARABLE type 'a s = S : (unit -> 'a) M.r -> 'a option s [@@unboxed] |}];; @@ -104,6 +107,7 @@ Error: This type cannot be unboxed because (* accept *) type 'a t = T : 'a s -> 'a t [@@unboxed];; [%%expect{| +t/114[14] IS NOT SEPARABLE type 'a t = T : 'a s -> 'a t [@@unboxed] |}];; @@ -118,6 +122,7 @@ end = struct let inj x = K x end;; [%%expect{| +r/116[16] IS NOT SEPARABLE module N : sig type 'a r val inj : 'b -> (unit -> 'b) r end |}];; @@ -136,6 +141,7 @@ Error: This type cannot be unboxed because (* accept *) type 'a s = S : (unit -> 'a) N.r -> 'a option s [@@unboxed];; [%%expect{| +s/126[19] IS NOT SEPARABLE type 'a s = S : (unit -> 'a) N.r -> 'a option s [@@unboxed] |}];; @@ -153,6 +159,7 @@ and _ t = T : 'a -> 'a s t type 'a s = S : 'a -> 'a s [@@unboxed];; type t = T : 'a s -> t [@@unboxed];; [%%expect{| +s/132[21] IS NOT SEPARABLE type 'a s = S : 'a -> 'a s [@@unboxed] Line 2, characters 0-34: 2 | type t = T : 'a s -> t [@@unboxed];; @@ -167,6 +174,7 @@ Error: This type cannot be unboxed because type 'a s = S : 'a -> 'a option s [@@unboxed];; type t = T : 'a s -> t [@@unboxed];; [%%expect{| +s/136[23] IS NOT SEPARABLE type 'a s = S : 'a -> 'a option s [@@unboxed] Line 2, characters 0-34: 2 | type t = T : 'a s -> t [@@unboxed];; @@ -204,6 +212,7 @@ Error: This type cannot be unboxed because type 'a s = S : (unit -> 'a) M.r -> 'a option s [@@unboxed];; [%%expect{| +s/149[29] IS NOT SEPARABLE type 'a s = S : (unit -> 'a) M.r -> 'a option s [@@unboxed] |}];; @@ -222,6 +231,7 @@ Error: This type cannot be unboxed because (* accept *) type 'a t = T : 'a s -> 'a t [@@unboxed];; [%%expect{| +t/153[31] IS NOT SEPARABLE type 'a t = T : 'a s -> 'a t [@@unboxed] |}];; @@ -253,6 +263,7 @@ and _ t = T : 'a -> 'a s t *) type (_, _) almost_eq = Almost_refl : 'a -> ('a, 'a) almost_eq [@@unboxed] [%%expect{| +almost_eq/159[33] IS NOT SEPARABLE type (_, _) almost_eq = Almost_refl : 'a -> ('a, 'a) almost_eq [@@unboxed] |}];; @@ -269,6 +280,7 @@ Error: This type cannot be unboxed because |}];; type valid2 = Any : (int, 'a) almost_eq -> valid2 [@@unboxed];; [%%expect{| +valid2/163[35] IS NOT SEPARABLE type valid2 = Any : (int, 'a) almost_eq -> valid2 [@@unboxed] |}];; @@ -307,6 +319,7 @@ type safe_again = Any : 'a stream -> safe_again type 'a id = Id of 'a [@@unboxed] type cycle = cycle id [%%expect{| +id/173[41] IS NOT SEPARABLE type 'a id = Id of 'a [@@unboxed] Line 2, characters 0-21: 2 | type cycle = cycle id diff --git a/testsuite/tests/typing-unboxed-types/test_unboxed_constr.ml b/testsuite/tests/typing-unboxed-types/test_unboxed_constr.ml index 559efd0fb26e..77fb46088929 100644 --- a/testsuite/tests/typing-unboxed-types/test_unboxed_constr.ml +++ b/testsuite/tests/typing-unboxed-types/test_unboxed_constr.ml @@ -19,7 +19,11 @@ type t = A of int | B of float | C | D type t = A of int [@unboxed] | B;; [%%expect{| SHAPE(t/96[3]) CONFLICT -type t = A of int [@unboxed] | B +Line 1, characters 0-32: +1 | type t = A of int [@unboxed] | B;; + ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ +Error: This declaration is invalid, some [@unboxed] annotations introduce + overlapping representations. |}];; type t = A of float [@unboxed] | B;; diff --git a/testsuite/tests/typing-unboxed-types/test_unboxed_constr_matching.ml b/testsuite/tests/typing-unboxed-types/test_unboxed_constr_matching.ml index e9e68907afc5..9a598f606a39 100644 --- a/testsuite/tests/typing-unboxed-types/test_unboxed_constr_matching.ml +++ b/testsuite/tests/typing-unboxed-types/test_unboxed_constr_matching.ml @@ -7,13 +7,13 @@ *) module A = struct - type t = A of int | B of float [@unboxed] + type t = A of int | B of string [@unboxed] let f = function A _ -> 0 | B _ -> 1 let test () = assert (f (A 0) = 0); - assert (f (B 0.) = 1) + assert (f (B "0") = 1) end let () = A.test () diff --git a/testsuite/tests/typing-unboxed/test.ml b/testsuite/tests/typing-unboxed/test.ml index 850713cf6ae5..c3b0c90b752b 100644 --- a/testsuite/tests/typing-unboxed/test.ml +++ b/testsuite/tests/typing-unboxed/test.ml @@ -744,7 +744,11 @@ Error: [@The native code version of the primitive is mandatory (* PR#7424 *) type 'a b = B of 'a b b [@@unboxed];; [%%expect{| -type 'a b = B of 'a b b [@@unboxed] +Line 1, characters 0-35: +1 | type 'a b = B of 'a b b [@@unboxed];; + ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ +Error: Cyclic type expansion during [@unboxed] verification. + b/182[29] appears unboxed at the head of its own definition. |}] From 44dc5852c5dee1d3237325fd80ca25e630a8021b Mon Sep 17 00:00:00 2001 From: Gabriel Scherer Date: Tue, 21 Sep 2021 23:06:05 +0200 Subject: [PATCH 44/45] head_shape: change separability computation (still unfinished) --- testsuite/tests/typing-unboxed-types/test.ml | 23 ------ .../tests/typing-unboxed-types/test_flat.ml | 13 ---- .../test_unboxed_constr.ml | 6 +- typing/typedecl_unboxed.ml | 78 ++++++++++++++----- 4 files changed, 60 insertions(+), 60 deletions(-) diff --git a/testsuite/tests/typing-unboxed-types/test.ml b/testsuite/tests/typing-unboxed-types/test.ml index 70ee16f20d34..32e32a7859fe 100644 --- a/testsuite/tests/typing-unboxed-types/test.ml +++ b/testsuite/tests/typing-unboxed-types/test.ml @@ -296,11 +296,6 @@ type t14;; type t15 = A of t14 [@@ocaml.unboxed];; [%%expect{| type t14 -t15/560[52] IS NOT SEPARABLE -type t15 = A of t14 [@@unboxed] -|}, Principal{| -type t14 -t15/560[53] IS NOT SEPARABLE type t15 = A of t14 [@@unboxed] |}];; @@ -352,12 +347,6 @@ type 'a packed = T : ('a, _) t -> 'a packed [@@unboxed] [%%expect{| type 'a s type ('a, 'p) t = private 'a s -packed/579[63] IS NOT SEPARABLE -type 'a packed = T : ('a, 'b) t -> 'a packed [@@unboxed] -|}, Principal{| -type 'a s -type ('a, 'p) t = private 'a s -packed/579[64] IS NOT SEPARABLE type 'a packed = T : ('a, 'b) t -> 'a packed [@@unboxed] |}];; @@ -378,11 +367,6 @@ type 'a t [@@immediate];; type u = U : 'a t -> u [@@unboxed];; [%%expect{| type 'a t [@@immediate] -u/587[66] IS NOT SEPARABLE -type u = U : 'a t -> u [@@unboxed] -|}, Principal{| -type 'a t [@@immediate] -u/587[67] IS NOT SEPARABLE type u = U : 'a t -> u [@@unboxed] |}];; @@ -391,13 +375,6 @@ type u = U : 'a t -> u [@@unboxed] type ('a, 'b) t = K : 'c -> (bool, 'c) t [@@unboxed] and t1 = T1 : (bool, int) t -> t1 [@@unboxed] [%%expect{| -t/589[67] IS NOT SEPARABLE -t1/590[67] IS NOT SEPARABLE -type ('a, 'b) t = K : 'c -> (bool, 'c) t [@@unboxed] -and t1 = T1 : (bool, int) t -> t1 [@@unboxed] -|}, Principal{| -t/589[68] IS NOT SEPARABLE -t1/590[68] IS NOT SEPARABLE type ('a, 'b) t = K : 'c -> (bool, 'c) t [@@unboxed] and t1 = T1 : (bool, int) t -> t1 [@@unboxed] |}];; diff --git a/testsuite/tests/typing-unboxed-types/test_flat.ml b/testsuite/tests/typing-unboxed-types/test_flat.ml index 3014f7acb5c5..c093efe1089f 100644 --- a/testsuite/tests/typing-unboxed-types/test_flat.ml +++ b/testsuite/tests/typing-unboxed-types/test_flat.ml @@ -34,7 +34,6 @@ Error: This type cannot be unboxed because type 'a s = S : 'a -> 'a s [@@unboxed];; type t = T : 'a s -> t [@@unboxed];; [%%expect{| -s/93[4] IS NOT SEPARABLE type 'a s = S : 'a -> 'a s [@@unboxed] Line 2, characters 0-34: 2 | type t = T : 'a s -> t [@@unboxed];; @@ -49,7 +48,6 @@ Error: This type cannot be unboxed because type 'a s = S : 'a -> 'a option s [@@unboxed];; type t = T : 'a s -> t [@@unboxed];; [%%expect{| -s/97[6] IS NOT SEPARABLE type 'a s = S : 'a -> 'a option s [@@unboxed] Line 2, characters 0-34: 2 | type t = T : 'a s -> t [@@unboxed];; @@ -88,7 +86,6 @@ Error: This type cannot be unboxed because (* accept *) type 'a s = S : (unit -> 'a) M.r -> 'a option s [@@unboxed];; [%%expect{| -s/110[12] IS NOT SEPARABLE type 'a s = S : (unit -> 'a) M.r -> 'a option s [@@unboxed] |}];; @@ -107,7 +104,6 @@ Error: This type cannot be unboxed because (* accept *) type 'a t = T : 'a s -> 'a t [@@unboxed];; [%%expect{| -t/114[14] IS NOT SEPARABLE type 'a t = T : 'a s -> 'a t [@@unboxed] |}];; @@ -122,7 +118,6 @@ end = struct let inj x = K x end;; [%%expect{| -r/116[16] IS NOT SEPARABLE module N : sig type 'a r val inj : 'b -> (unit -> 'b) r end |}];; @@ -141,7 +136,6 @@ Error: This type cannot be unboxed because (* accept *) type 'a s = S : (unit -> 'a) N.r -> 'a option s [@@unboxed];; [%%expect{| -s/126[19] IS NOT SEPARABLE type 'a s = S : (unit -> 'a) N.r -> 'a option s [@@unboxed] |}];; @@ -159,7 +153,6 @@ and _ t = T : 'a -> 'a s t type 'a s = S : 'a -> 'a s [@@unboxed];; type t = T : 'a s -> t [@@unboxed];; [%%expect{| -s/132[21] IS NOT SEPARABLE type 'a s = S : 'a -> 'a s [@@unboxed] Line 2, characters 0-34: 2 | type t = T : 'a s -> t [@@unboxed];; @@ -174,7 +167,6 @@ Error: This type cannot be unboxed because type 'a s = S : 'a -> 'a option s [@@unboxed];; type t = T : 'a s -> t [@@unboxed];; [%%expect{| -s/136[23] IS NOT SEPARABLE type 'a s = S : 'a -> 'a option s [@@unboxed] Line 2, characters 0-34: 2 | type t = T : 'a s -> t [@@unboxed];; @@ -212,7 +204,6 @@ Error: This type cannot be unboxed because type 'a s = S : (unit -> 'a) M.r -> 'a option s [@@unboxed];; [%%expect{| -s/149[29] IS NOT SEPARABLE type 'a s = S : (unit -> 'a) M.r -> 'a option s [@@unboxed] |}];; @@ -231,7 +222,6 @@ Error: This type cannot be unboxed because (* accept *) type 'a t = T : 'a s -> 'a t [@@unboxed];; [%%expect{| -t/153[31] IS NOT SEPARABLE type 'a t = T : 'a s -> 'a t [@@unboxed] |}];; @@ -263,7 +253,6 @@ and _ t = T : 'a -> 'a s t *) type (_, _) almost_eq = Almost_refl : 'a -> ('a, 'a) almost_eq [@@unboxed] [%%expect{| -almost_eq/159[33] IS NOT SEPARABLE type (_, _) almost_eq = Almost_refl : 'a -> ('a, 'a) almost_eq [@@unboxed] |}];; @@ -280,7 +269,6 @@ Error: This type cannot be unboxed because |}];; type valid2 = Any : (int, 'a) almost_eq -> valid2 [@@unboxed];; [%%expect{| -valid2/163[35] IS NOT SEPARABLE type valid2 = Any : (int, 'a) almost_eq -> valid2 [@@unboxed] |}];; @@ -319,7 +307,6 @@ type safe_again = Any : 'a stream -> safe_again type 'a id = Id of 'a [@@unboxed] type cycle = cycle id [%%expect{| -id/173[41] IS NOT SEPARABLE type 'a id = Id of 'a [@@unboxed] Line 2, characters 0-21: 2 | type cycle = cycle id diff --git a/testsuite/tests/typing-unboxed-types/test_unboxed_constr.ml b/testsuite/tests/typing-unboxed-types/test_unboxed_constr.ml index 77fb46088929..7e9de2a0dd6c 100644 --- a/testsuite/tests/typing-unboxed-types/test_unboxed_constr.ml +++ b/testsuite/tests/typing-unboxed-types/test_unboxed_constr.ml @@ -45,8 +45,7 @@ and 'a u = 'a id and 'a id = Id of 'a [@unboxed];; [%%expect{| SHAPE(t/107[6]) {head_imm = Shape_any; head_blocks = Shape_set []; head_separated = true} -id/109[6] IS NOT SEPARABLE -SHAPE(id/109[6]) {head_imm = Shape_any; head_blocks = Shape_any; head_separated = false} +SHAPE(id/109[6]) {head_imm = Shape_any; head_blocks = Shape_any; head_separated = true} type t = K of int u u [@unboxed] and 'a u = 'a id and 'a id = Id of 'a [@unboxed] @@ -69,8 +68,7 @@ type t = A of { a : int; } [@unboxed] type ('a, 'r) u = 'r and 'a t = A of { body : 'r. ('a, 'r) u } [@unboxed];; [%%expect{| -t/120[9] IS NOT SEPARABLE -SHAPE(t/120[9]) {head_imm = Shape_any; head_blocks = Shape_any; head_separated = false} +SHAPE(t/120[9]) {head_imm = Shape_any; head_blocks = Shape_any; head_separated = true} type ('a, 'r) u = 'r and 'a t = A of { body : 'r. ('a, 'r) u; } [@unboxed] |}];; diff --git a/typing/typedecl_unboxed.ml b/typing/typedecl_unboxed.ml index 8ca7907f6100..059a206f5b9a 100644 --- a/typing/typedecl_unboxed.ml +++ b/typing/typedecl_unboxed.ml @@ -120,8 +120,41 @@ module Head_shape = struct pp_shape head_blocks head_separated - let any_shape = - { head_imm = Shape_any; head_blocks = Shape_any; head_separated = false } + let has_float ~blocks = + match blocks with + | Shape_any -> true + | Shape_set tags -> List.mem Obj.double_tag tags + + let has_nonfloat ~imm ~blocks = + match imm with + | Shape_set (_ :: _) + | Shape_any -> true + | Shape_set [] -> + match blocks with + | Shape_any -> true + | Shape_set tags -> + List.exists (fun t -> t <> Obj.double_tag) tags + + let separated ~imm ~blocks = + not (has_float ~blocks && has_nonfloat ~imm ~blocks) + + let head_has_float hd = + has_float ~blocks:hd.head_blocks + + let head_has_nonfloat hd = + has_nonfloat ~imm:hd.head_imm ~blocks:hd.head_blocks + + let any_shape = { + head_imm = Shape_any; + head_blocks = Shape_any; + head_separated = true; + } + + let _poison_shape = { + head_imm = Shape_any; + head_blocks = Shape_any; + head_separated = false; + } let empty_shape = { @@ -138,18 +171,22 @@ module Head_shape = struct } let block_shape tags = - let head_separated = - List.for_all (fun x -> x = Obj.double_tag) tags || - List.for_all (fun x -> x <> Obj.double_tag) tags - in - { head_imm = Shape_set []; head_blocks = Shape_set tags; head_separated } + let imm = Shape_set [] in + let blocks = Shape_set tags in + { + head_imm = imm; + head_blocks = blocks; + head_separated = separated ~imm ~blocks; + } let cstrs_shape ~num_consts ~num_nonconsts = let int_list n = List.init n Fun.id in { head_imm = Shape_set (int_list num_consts); head_blocks = Shape_set (int_list num_nonconsts); - head_separated = true; + head_separated = + (assert (num_nonconsts < Obj.double_tag); + true); } let disjoint_union hd1 hd2 = @@ -171,16 +208,8 @@ module Head_shape = struct let head_separated = hd1.head_separated && hd2.head_separated && - match head_blocks with - | Shape_any -> false - | Shape_set tags -> - ( - head_imm = Shape_set [] && - List.for_all (fun x -> x = Obj.double_tag) tags - ) || - ( - List.for_all (fun x -> x <> Obj.double_tag) tags - ) + not (head_has_float hd1 && head_has_nonfloat hd2) && + not (head_has_float hd2 && head_has_nonfloat hd1) in { head_imm; head_blocks; head_separated } @@ -265,7 +294,11 @@ module Head_shape = struct (* TODO : try the Ctype.expand_head_opt version here *) check_annotated ty callstack_map; match get_desc ty with - | Tvar _ | Tunivar _ -> any_shape + | Tvar _ | Tunivar _ -> + (* FIXME: variables that are universally quantified (including type parameters) + should get [any_shape] as here, but GADT variables that are existentially quantified + should get [poison_shape] instead -- they are not separated. *) + any_shape | Tconstr (p, args, _abbrev) -> begin match match_primitive_type p with | Some prim_type -> of_primitive_type prim_type @@ -281,7 +314,12 @@ module Head_shape = struct %a appears unboxed at the head of its own definition." Path.print p else match Env.find_type_descrs p env, Env.find_type p env with - | exception Not_found -> any_shape + | exception Not_found -> + (* FIXME: if one of the parameters is non-separated, then + this unknown type should be considered non-separated as well. + (It may be a projection into this parameter.) + This corresponds to the DeepSep case of the separability analysis. *) + any_shape | descr, decl -> of_typedescr env descr decl ~args callstack_map (Callstack.visit p head_callstack) From d983c43e6a3022cf0f75b30a7eecd5b62be9ed1a Mon Sep 17 00:00:00 2001 From: Gabriel Scherer Date: Tue, 22 Mar 2022 11:50:18 +0100 Subject: [PATCH 45/45] head-shape spec: genprintval is done --- HEAD_SHAPE.impl.md | 5 ----- 1 file changed, 5 deletions(-) diff --git a/HEAD_SHAPE.impl.md b/HEAD_SHAPE.impl.md index 09d03442cafc..ba89bffdaa2b 100644 --- a/HEAD_SHAPE.impl.md +++ b/HEAD_SHAPE.impl.md @@ -182,11 +182,6 @@ fixed easily by keeping track of the set of type nodes we have already encountered in head position during reduction. -### Handle unboxed constructors in `genprintval` - -`genprintval` performs type-directed pretty-printing of values (represented as `Obj.t`). For variants it accesses the tag to know which constructor to print, and how to print the argument(s). We need to adapt this code to deal with unboxed constructors: the constructor to print is the one whose head shape contains the head of the value being printed. - - ### Distinguish "good" from "bad" cycles Our cycle-detection algorithm will sometimes reject definitions that indeed are cyclic, but do admit a valid fixpoint: