From adcf36d6f1ac140c306a6dffeb451329b3dc8da1 Mon Sep 17 00:00:00 2001 From: Chris Casinghino Date: Mon, 24 Jun 2024 20:01:30 -0400 Subject: [PATCH 1/8] Refactoring: Delay translating some za attributes to semantics --- ocaml/lambda/translcore.ml | 48 ++++++++++++++++++++++++--- ocaml/parsing/builtin_attributes.ml | 34 ++++++++++--------- ocaml/parsing/builtin_attributes.mli | 8 +++-- ocaml/typing/printtyped.ml | 16 +++++++-- ocaml/typing/typecore.ml | 49 ++++------------------------ ocaml/typing/typedtree.ml | 2 +- ocaml/typing/typedtree.mli | 10 +++--- 7 files changed, 92 insertions(+), 75 deletions(-) diff --git a/ocaml/lambda/translcore.ml b/ocaml/lambda/translcore.ml index 4ae6f9e9c54..31f6d525fae 100644 --- a/ocaml/lambda/translcore.ml +++ b/ocaml/lambda/translcore.ml @@ -350,6 +350,42 @@ let can_apply_primitive p pmode pos args = end end +let zero_alloc_of_application + ~num_args (annotation : Builtin_attributes.zero_alloc_attribute) funct = + let zero_alloc = + match annotation with + | Assume _ -> + (* The user wrote a zero_alloc attribute on the application - keep it. *) + annotation + | Ignore_assert_all | Check _ -> + (* These are rejected in typecore *) + Misc.fatal_error "Translcore.zero_alloc_of_application: illegal attr" + | Default_zero_alloc -> + (* We assume the call is zero_alloc if the function is known to be + zero_alloc. If the function is zero_alloc opt, then we need to be sure + that the opt checks were run to license this assumption. We judge + whether the opt checks were run based on the argument to the + [-zero-alloc-check] command line flag. *) + let use_opt = + match !Clflags.zero_alloc_check with + | Check_default | No_check -> false + | Check_all | Check_opt_only -> true + in + match funct.exp_desc with + | Texp_ident (_, _, { val_zero_alloc = (Check c); _ }, _, _) + when c.arity = num_args && (use_opt || not c.opt) -> + Builtin_attributes.Assume { + strict = c.strict; + never_returns_normally = false; + never_raises = false; + arity = c.arity; + loc = c.loc + } + | _ -> Builtin_attributes.Default_zero_alloc + + in + Builtin_attributes.assume_zero_alloc zero_alloc + let rec transl_exp ~scopes sort e = transl_exp1 ~scopes ~in_new_scope:false sort e @@ -387,7 +423,7 @@ and transl_exp0 ~in_new_scope ~scopes sort e = | Texp_apply({ exp_desc = Texp_ident(path, _, {val_kind = Val_prim p}, Id_prim (pmode, psort), _); exp_type = prim_type; } as funct, - oargs, pos, ap_mode, assume_zero_alloc) + oargs, pos, ap_mode, zero_alloc) when can_apply_primitive p pmode pos oargs -> let rec cut_args prim_repr oargs = match prim_repr, oargs with @@ -409,6 +445,7 @@ and transl_exp0 ~in_new_scope ~scopes sort e = if extra_args = [] then transl_apply_position pos else Rc_normal in + let assume_zero_alloc = Builtin_attributes.assume_zero_alloc zero_alloc in let lam = let loc = map_scopes (update_assume_zero_alloc ~assume_zero_alloc) @@ -433,7 +470,7 @@ and transl_exp0 ~in_new_scope ~scopes sort e = ~position ~mode ~result_layout lam extra_args (of_location ~scopes e.exp_loc)) end - | Texp_apply(funct, oargs, position, ap_mode, assume_zero_alloc) + | Texp_apply(funct, oargs, position, ap_mode, zero_alloc) -> let tailcall = Translattribute.get_tailcall_attribute funct in let inlined = Translattribute.get_inlined_attribute funct in @@ -441,6 +478,9 @@ and transl_exp0 ~in_new_scope ~scopes sort e = let result_layout = layout_exp sort e in let position = transl_apply_position position in let mode = transl_locality_mode_l ap_mode in + let assume_zero_alloc = + zero_alloc_of_application ~num_args:(List.length oargs) zero_alloc funct + in event_after ~scopes e (transl_apply ~scopes ~tailcall ~inlined ~specialised ~assume_zero_alloc @@ -1579,9 +1619,7 @@ and transl_function ~in_new_scope ~scopes e params body ~zero_alloc = let attrs = e.exp_attributes in let mode = transl_alloc_mode_r alloc_mode in - let assume_zero_alloc = - Builtin_attributes.assume_zero_alloc ~is_check_allowed:true zero_alloc - in + let assume_zero_alloc = Builtin_attributes.assume_zero_alloc zero_alloc in let scopes = if in_new_scope then update_assume_zero_alloc ~scopes ~assume_zero_alloc diff --git a/ocaml/parsing/builtin_attributes.ml b/ocaml/parsing/builtin_attributes.ml index 2b74f27471f..9eb34a194ee 100644 --- a/ocaml/parsing/builtin_attributes.ml +++ b/ocaml/parsing/builtin_attributes.ml @@ -923,25 +923,27 @@ let get_zero_alloc_attribute ~in_signature ~default_arity l = register_zero_alloc_attribute attr.attr_name); res -let assume_zero_alloc ~is_check_allowed check : Zero_alloc_utils.Assume_info.t = +let zero_alloc_attribute_may_not_be_check za = + match za with + | Default_zero_alloc | Ignore_assert_all | Assume _ -> za + | Check { loc; _ } -> + let name = "zero_alloc" in + let msg = "Only the following combinations are supported in this context: \ + 'zero_alloc assume', \ + `zero_alloc assume strict`, \ + `zero_alloc assume error`,\ + `zero_alloc assume never_returns_normally`,\ + `zero_alloc assume never_returns_normally strict`." + in + Location.prerr_warning loc (Warnings.Attribute_payload (name, msg)); + Default_zero_alloc + +let assume_zero_alloc check : Zero_alloc_utils.Assume_info.t = match check with - | Default_zero_alloc -> Zero_alloc_utils.Assume_info.none - | Ignore_assert_all -> Zero_alloc_utils.Assume_info.none + | Default_zero_alloc | Ignore_assert_all | Check _ -> + Zero_alloc_utils.Assume_info.none | Assume { strict; never_returns_normally; never_raises; } -> Zero_alloc_utils.Assume_info.create ~strict ~never_returns_normally ~never_raises - | Check { loc; _ } -> - if not is_check_allowed then begin - let name = "zero_alloc" in - let msg = "Only the following combinations are supported in this context: \ - 'zero_alloc assume', \ - `zero_alloc assume strict`, \ - `zero_alloc assume error`,\ - `zero_alloc assume never_returns_normally`,\ - `zero_alloc assume never_returns_normally strict`." - in - Location.prerr_warning loc (Warnings.Attribute_payload (name, msg)) - end; - Zero_alloc_utils.Assume_info.none type tracing_probe = { name : string; diff --git a/ocaml/parsing/builtin_attributes.mli b/ocaml/parsing/builtin_attributes.mli index d84e09b5af3..1f04b36e082 100644 --- a/ocaml/parsing/builtin_attributes.mli +++ b/ocaml/parsing/builtin_attributes.mli @@ -271,8 +271,12 @@ val get_zero_alloc_attribute : in_signature:bool -> default_arity:int -> Parsetree.attributes -> zero_alloc_attribute -val assume_zero_alloc : - is_check_allowed:bool -> zero_alloc_attribute -> Zero_alloc_utils.Assume_info.t +(* If the input attribute is [Check], this issues a warning and returns + [Default_zero_alloc]. Otherwise, it is the identity. *) +val zero_alloc_attribute_may_not_be_check : + zero_alloc_attribute -> zero_alloc_attribute + +val assume_zero_alloc : zero_alloc_attribute -> Zero_alloc_utils.Assume_info.t type tracing_probe = { name : string; diff --git a/ocaml/typing/printtyped.ml b/ocaml/typing/printtyped.ml index 21ee0e68083..186a8e8a377 100644 --- a/ocaml/typing/printtyped.ml +++ b/ocaml/typing/printtyped.ml @@ -224,6 +224,18 @@ let attributes i ppf l = let jkind_annotation i ppf (jkind, _) = line i ppf "%a" Jkind.Const.format jkind +let application_zero_alloc i ppf (za : Builtin_attributes.zero_alloc_attribute) = + match za with + | Default_zero_alloc -> () + | Assume { strict; never_returns_normally; never_raises; arity; loc = _ } -> + line i ppf "assume_zero_alloc arity=%d%s%s%s\n" + arity + (if strict then " strict" else "") + (if never_returns_normally then " never_returns_normally" else "") + (if never_raises then " never_raises" else "") + | Ignore_assert_all | Check _ -> + Misc.fatal_error "printtyped: application_zero_alloc" + let rec core_type i ppf x = line i ppf "core_type %a\n" fmt_location x.ctyp_loc; attributes i ppf x.ctyp_attributes; @@ -452,9 +464,7 @@ and expression i ppf x = | Nontail -> "Nontail" | Default -> "Default"); locality_mode i ppf am; - if not (Zero_alloc_utils.Assume_info.is_none za) then - line i ppf "assume_zero_alloc %a\n" - Zero_alloc_utils.Assume_info.print za; + application_zero_alloc i ppf za; expression i ppf e; list i label_x_apply_arg ppf l; | Texp_match (e, sort, l, _partial) -> diff --git a/ocaml/typing/typecore.ml b/ocaml/typing/typecore.ml index 1d806743da5..24924793dfb 100644 --- a/ocaml/typing/typecore.ml +++ b/ocaml/typing/typecore.ml @@ -5109,44 +5109,6 @@ let add_check_attribute expr attributes = end | _ -> expr -let zero_alloc_of_application ~num_args attrs funct = - let zero_alloc = - Builtin_attributes.get_zero_alloc_attribute ~in_signature:false - ~default_arity:num_args attrs - in - let zero_alloc = - match zero_alloc with - | Assume _ | Ignore_assert_all | Check _ -> - (* The user wrote a zero_alloc attribute on the application - keep it. - (Note that `ignore` and `check` aren't really allowed here, and will be - rejected by the call to `Builtin_attributes.assume_zero_alloc` below.) - *) - zero_alloc - | Default_zero_alloc -> - (* We assume the call is zero_alloc if the function is known to be - zero_alloc. If the function is zero_alloc opt, then we need to be sure - that the opt checks were run to license this assumption. We judge - whether the opt checks were run based on the argument to the - [-zero-alloc-check] command line flag. *) - let use_opt = - match !Clflags.zero_alloc_check with - | Check_default | No_check -> false - | Check_all | Check_opt_only -> true - in - match funct.exp_desc with - | Texp_ident (_, _, { val_zero_alloc = (Check c); _ }, _, _) - when c.arity = num_args && (use_opt || not c.opt) -> - Builtin_attributes.Assume { - strict = c.strict; - never_returns_normally = false; - never_raises = false; - arity = c.arity; - loc = c.loc - } - | _ -> Builtin_attributes.Default_zero_alloc - in - Builtin_attributes.assume_zero_alloc ~is_check_allowed:false zero_alloc - let rec type_exp ?recarg env expected_mode sexp = (* We now delegate everything to type_expect *) type_expect ?recarg env expected_mode sexp @@ -5475,14 +5437,15 @@ and type_expect_ let (args, ty_res, ap_mode, pm) = type_application env loc expected_mode pm funct funct_mode sargs rt in - let assume_zero_alloc = - zero_alloc_of_application ~num_args:(List.length args) - sfunct.pexp_attributes funct + let zero_alloc = + Builtin_attributes.get_zero_alloc_attribute ~in_signature:false + ~default_arity:(List.length args) sfunct.pexp_attributes + |> Builtin_attributes.zero_alloc_attribute_may_not_be_check in rue { exp_desc = Texp_apply(funct, args, pm.apply_position, ap_mode, - assume_zero_alloc); + zero_alloc); exp_loc = loc; exp_extra = []; exp_type = ty_res; exp_attributes = sexp.pexp_attributes; @@ -7520,7 +7483,7 @@ and type_argument ?explanation ?recarg env (mode : expected_mode) sarg |> Value.proj (Comonadic Areality) |> regional_to_global |> Locality.disallow_right, - Zero_alloc_utils.Assume_info.none)} + Builtin_attributes.Default_zero_alloc)} in let cases = [ case eta_pat e ] in let cases_loc = { texp.exp_loc with loc_ghost = true } in diff --git a/ocaml/typing/typedtree.ml b/ocaml/typing/typedtree.ml index e621d5ba9f0..69a8a9a36c3 100644 --- a/ocaml/typing/typedtree.ml +++ b/ocaml/typing/typedtree.ml @@ -150,7 +150,7 @@ and expression_desc = } | Texp_apply of expression * (arg_label * apply_arg) list * apply_position * - Mode.Locality.l * Zero_alloc_utils.Assume_info.t + Mode.Locality.l * Builtin_attributes.zero_alloc_attribute | Texp_match of expression * Jkind.sort * computation case list * partial | Texp_try of expression * value case list | Texp_tuple of (string option * expression) list * Mode.Alloc.r diff --git a/ocaml/typing/typedtree.mli b/ocaml/typing/typedtree.mli index 6d9d8f4baf3..fa09e1eea07 100644 --- a/ocaml/typing/typedtree.mli +++ b/ocaml/typing/typedtree.mli @@ -280,7 +280,7 @@ and expression_desc = *) | Texp_apply of expression * (arg_label * apply_arg) list * apply_position * - Mode.Locality.l * Zero_alloc_utils.Assume_info.t + Mode.Locality.l * Builtin_attributes.zero_alloc_attribute (** E0 ~l1:E1 ... ~ln:En The expression can be Omitted if the expression is abstracted over @@ -296,10 +296,10 @@ and expression_desc = (Labelled "y", Some (Texp_constant Const_int 3)) ]) - The [Zero_alloc_utils.Assume_info.t] records the optional - [@zero_alloc assume] attribute that may appear on applications. If - that attribute is absent, it is [Assume_info.none]. - *) + The [zero_alloc_attribute] records the optional [@zero_alloc assume] + attribute that may appear on applications. Invariant: it is either + [Default_zero_alloc] (if the user wrote no attribute) or [Assume] + (if they did). *) | Texp_match of expression * Jkind.sort * computation case list * partial (** match E0 with | P1 -> E1 From 458d2933a144e315de0ab5a9f4bcd5c5a746b647 Mon Sep 17 00:00:00 2001 From: Chris Casinghino Date: Thu, 27 Jun 2024 09:52:07 -0400 Subject: [PATCH 2/8] Refactoring: Make file for zero_alloc typing stuff --- ocaml/compilerlibs/Makefile.compilerlibs | 1 + ocaml/dune | 4 +- ocaml/otherlibs/dynlink/Makefile | 1 + ocaml/otherlibs/dynlink/dune | 5 ++ ocaml/typing/includecore.ml | 86 ++----------------- ocaml/typing/includecore.mli | 3 +- ocaml/typing/typedtree.ml | 4 +- ocaml/typing/typedtree.mli | 4 +- ocaml/typing/types.ml | 2 +- ocaml/typing/types.mli | 2 +- ocaml/typing/zero_alloc.ml | 102 +++++++++++++++++++++++ ocaml/typing/zero_alloc.mli | 24 ++++++ 12 files changed, 148 insertions(+), 90 deletions(-) create mode 100644 ocaml/typing/zero_alloc.ml create mode 100644 ocaml/typing/zero_alloc.mli diff --git a/ocaml/compilerlibs/Makefile.compilerlibs b/ocaml/compilerlibs/Makefile.compilerlibs index 0e1f54d07e0..8b6022bfa97 100644 --- a/ocaml/compilerlibs/Makefile.compilerlibs +++ b/ocaml/compilerlibs/Makefile.compilerlibs @@ -89,6 +89,7 @@ TYPING = \ typing/jkind_types.cmo \ typing/primitive.cmo \ typing/shape.cmo \ + typing/zero_alloc.cmo \ typing/types.cmo \ typing/jkind.cmo \ typing/btype.cmo \ diff --git a/ocaml/dune b/ocaml/dune index 32d657d558b..c01eb070979 100644 --- a/ocaml/dune +++ b/ocaml/dune @@ -88,7 +88,8 @@ jane_syntax ; manual update: mli only files asttypes parsetree ;; TYPING - ident path jkind primitive shape shape_reduce types btype oprint subst predef datarepr + ident path jkind primitive shape shape_reduce zero_alloc types btype oprint subst + predef datarepr global_module cmi_format persistent_env env errortrace mode jkind_types jkind_intf typedtree printtyped ctype printtyp includeclass mtype envaux includecore tast_iterator tast_mapper signature_group cmt_format cms_format untypeast @@ -291,6 +292,7 @@ (jkind.mli as compiler-libs/jkind.mli) (jkind_types.mli as compiler-libs/jkind_types.mli) (primitive.mli as compiler-libs/primitive.mli) + (zero_alloc.mli as compiler-libs/zero_alloc.mli) (types.mli as compiler-libs/types.mli) (btype.mli as compiler-libs/btype.mli) (binutils.mli as compiler-libs/binutils.mli) diff --git a/ocaml/otherlibs/dynlink/Makefile b/ocaml/otherlibs/dynlink/Makefile index 94861ee6077..d731fccf642 100644 --- a/ocaml/otherlibs/dynlink/Makefile +++ b/ocaml/otherlibs/dynlink/Makefile @@ -121,6 +121,7 @@ COMPILERLIBS_SOURCES=\ typing/shape.ml \ typing/jkind_types.ml \ typing/primitive.ml \ + typing/zero_alloc.ml \ typing/types.ml \ typing/jkind.ml \ typing/typedtree.ml \ diff --git a/ocaml/otherlibs/dynlink/dune b/ocaml/otherlibs/dynlink/dune index f965c9794f7..910d36b7972 100644 --- a/ocaml/otherlibs/dynlink/dune +++ b/ocaml/otherlibs/dynlink/dune @@ -94,6 +94,7 @@ jkind_intf jkind_types primitive + zero_alloc types jkind value_rec_types @@ -198,6 +199,7 @@ (copy_files ../../typing/solver.ml) (copy_files ../../typing/shape_reduce.ml) (copy_files ../../typing/mode.ml) +(copy_files ../../typing/zero_alloc.ml) (copy_files ../../typing/types.ml) (copy_files ../../typing/btype.ml) (copy_files ../../typing/subst.ml) @@ -267,6 +269,7 @@ (copy_files ../../typing/solver.mli) (copy_files ../../typing/shape_reduce.mli) (copy_files ../../typing/mode.mli) +(copy_files ../../typing/zero_alloc.mli) (copy_files ../../typing/types.mli) (copy_files ../../typing/btype.mli) (copy_files ../../typing/subst.mli) @@ -379,6 +382,7 @@ .dynlink_compilerlibs.objs/byte/dynlink_compilerlibs__Mode.cmo .dynlink_compilerlibs.objs/byte/dynlink_compilerlibs__Jkind_intf.cmo .dynlink_compilerlibs.objs/byte/dynlink_compilerlibs__Jkind_types.cmo + .dynlink_compilerlibs.objs/byte/dynlink_compilerlibs__Zero_alloc.cmo .dynlink_compilerlibs.objs/byte/dynlink_compilerlibs__Types.cmo .dynlink_compilerlibs.objs/byte/dynlink_compilerlibs__Attr_helper.cmo .dynlink_compilerlibs.objs/byte/dynlink_compilerlibs__Primitive.cmo @@ -462,6 +466,7 @@ .dynlink_compilerlibs.objs/native/dynlink_compilerlibs__Mode.cmx .dynlink_compilerlibs.objs/native/dynlink_compilerlibs__Jkind_intf.cmx .dynlink_compilerlibs.objs/native/dynlink_compilerlibs__Jkind_types.cmx + .dynlink_compilerlibs.objs/native/dynlink_compilerlibs__Zero_alloc.cmx .dynlink_compilerlibs.objs/native/dynlink_compilerlibs__Types.cmx .dynlink_compilerlibs.objs/native/dynlink_compilerlibs__Attr_helper.cmx .dynlink_compilerlibs.objs/native/dynlink_compilerlibs__Primitive.cmx diff --git a/ocaml/typing/includecore.ml b/ocaml/typing/includecore.ml index c38c31387ee..f70bdbfce56 100644 --- a/ocaml/typing/includecore.ml +++ b/ocaml/typing/includecore.ml @@ -23,8 +23,6 @@ open Typedtree type position = Errortrace.position = First | Second -module ZA = Zero_alloc_utils - (* Inclusion between value descriptions *) type primitive_mismatch = @@ -43,8 +41,7 @@ type value_mismatch = | Primitive_mismatch of primitive_mismatch | Not_a_primitive | Type of Errortrace.moregen_error - | Zero_alloc of { missing_entirely : bool } - | Zero_alloc_arity of int * int + | Zero_alloc of Zero_alloc.error | Modality of Mode.Modality.Value.error exception Dont_match of value_mismatch @@ -92,72 +89,6 @@ let primitive_descriptions pd1 pd2 = else native_repr_args pd1.prim_native_repr_args pd2.prim_native_repr_args -let zero_alloc za1 za2 = - (* The core of the check here is that we translate both attributes into the - abstract domain and use the existing inclusion check from there, ensuring - what we do in the typechecker matches the backend. - - There are a few additional details: - - - [opt] is not captured by the abstract domain, so we need a special check - for it. But it doesn't interact at all with the abstract domain - it's - just about whether or not the check happens - so this special check can - be fully separate. - - [arity] is also not captured by the abstract domain - it exists only for - use here, in typechecking. If the arities do not match, we issue an - error. It's essential for the soundness of the way we (will, in the next - PR) use zero_alloc in signatures that the apparent arity of the type in - the signature matches the syntactic arity of the function. - - [ignore] can not appear in zero_alloc attributes in signatures, and is - erased from structure items when computing their signature, so we don't - need to consider it here. - *) - let open Builtin_attributes in - (* abstract domain check *) - let abstract_value za = - match za with - | Default_zero_alloc | Ignore_assert_all -> ZA.Assume_info.Value.top () - | Check { strict; _ } -> - ZA.Assume_info.Value.of_annotation ~strict ~never_returns_normally:false - ~never_raises:false - | Assume { strict; never_returns_normally; never_raises; } -> - ZA.Assume_info.Value.of_annotation ~strict ~never_returns_normally - ~never_raises - in - let v1 = abstract_value za1 in - let v2 = abstract_value za2 in - if not (ZA.Assume_info.Value.lessequal v1 v2) then - begin let missing_entirely = - match za1 with - | Default_zero_alloc -> true - | Ignore_assert_all | Check _ | Assume _ -> false - in - raise (Dont_match (Zero_alloc {missing_entirely})) - end; - (* opt check *) - begin match za1, za2 with - | Check { opt = opt1; _ }, Check { opt = opt2; _ } -> - if opt1 && not opt2 then - raise (Dont_match (Zero_alloc {missing_entirely = false})) - | (Check _ | Default_zero_alloc | Assume _ | Ignore_assert_all), _ -> () - end; - (* arity check *) - let get_arity = function - | Check { arity; _ } | Assume { arity; _ } -> Some arity - | Default_zero_alloc | Ignore_assert_all -> None - in - match get_arity za1, get_arity za2 with - | Some arity1, Some arity2 -> - (* Check *) - if not (arity1 = arity2) then - raise (Dont_match (Zero_alloc_arity (arity1, arity2))) - | Some _, None -> () - (* Forgetting zero_alloc info is fine *) - | None, Some _ -> - (* Fabricating it is not, but earlier cases should have ruled this out *) - Misc.fatal_error "Includecore.check_attributes" - | None, None -> () - let value_descriptions ~loc env name (vd1 : Types.value_description) (vd2 : Types.value_description) = @@ -167,7 +98,9 @@ let value_descriptions ~loc env name loc vd1.val_attributes vd2.val_attributes name; - zero_alloc vd1.val_zero_alloc vd2.val_zero_alloc; + begin try Zero_alloc.sub_exn vd1.val_zero_alloc vd2.val_zero_alloc with + | Zero_alloc.Error e -> raise (Dont_match (Zero_alloc e)) + end; begin match Mode.Modality.Value.sub vd1.val_modalities vd2.val_modalities with | Ok () -> () | Error e -> raise (Dont_match (Modality e)) @@ -386,16 +319,7 @@ let report_value_mismatch first second env ppf err = Printtyp.report_moregen_error ppf Type_scheme env trace (fun ppf -> Format.fprintf ppf "The type") (fun ppf -> Format.fprintf ppf "is not compatible with the type") - | Zero_alloc { missing_entirely } -> - pr "The former provides a weaker \"zero_alloc\" guarantee than the latter."; - if missing_entirely then - pr "@ Hint: Add a \"zero_alloc\" attribute to the implementation." - | Zero_alloc_arity (n1, n2) -> - pr "zero_alloc arity mismatch:@ \ - When using \"zero_alloc\" in a signature, the syntactic arity of@ \ - the implementation must match the function type in the interface.@ \ - Here the former is %d and the latter is %d." - n1 n2 + | Zero_alloc e -> Zero_alloc.print_error ppf e | Modality e -> report_modality_sub_error first second ppf e let report_type_inequality env ppf err = diff --git a/ocaml/typing/includecore.mli b/ocaml/typing/includecore.mli index 77501addea5..00f5466f07b 100644 --- a/ocaml/typing/includecore.mli +++ b/ocaml/typing/includecore.mli @@ -36,8 +36,7 @@ type value_mismatch = | Primitive_mismatch of primitive_mismatch | Not_a_primitive | Type of Errortrace.moregen_error - | Zero_alloc of { missing_entirely : bool } - | Zero_alloc_arity of int * int + | Zero_alloc of Zero_alloc.error | Modality of Mode.Modality.Value.error exception Dont_match of value_mismatch diff --git a/ocaml/typing/typedtree.ml b/ocaml/typing/typedtree.ml index 69a8a9a36c3..f571938654e 100644 --- a/ocaml/typing/typedtree.ml +++ b/ocaml/typing/typedtree.ml @@ -146,7 +146,7 @@ and expression_desc = ret_mode : Mode.Alloc.l; ret_sort : Jkind.sort; alloc_mode : Mode.Alloc.r; - zero_alloc : Builtin_attributes.zero_alloc_attribute; + zero_alloc : Zero_alloc.t; } | Texp_apply of expression * (arg_label * apply_arg) list * apply_position * @@ -1093,7 +1093,7 @@ let let_bound_idents_with_modes_sorts_and_checks bindings = (fun (id, _, _, _) -> let zero_alloc = Option.value (Ident.Map.find_opt id checks) - ~default:Builtin_attributes.Default_zero_alloc + ~default:Zero_alloc.Default_zero_alloc in id, List.rev (Ident.Tbl.find_all modes_and_sorts id), zero_alloc) (rev_let_bound_idents_full bindings) diff --git a/ocaml/typing/typedtree.mli b/ocaml/typing/typedtree.mli index fa09e1eea07..c729e2f625d 100644 --- a/ocaml/typing/typedtree.mli +++ b/ocaml/typing/typedtree.mli @@ -266,7 +266,7 @@ and expression_desc = ret_sort : Jkind.sort; alloc_mode : Mode.Alloc.r; (* Mode at which the closure is allocated *) - zero_alloc : Builtin_attributes.zero_alloc_attribute + zero_alloc : Zero_alloc.t; (* zero-alloc attributes *) } (** fun P0 P1 -> function p1 -> e1 | p2 -> e2 (body = Tfunction_cases _) @@ -1157,7 +1157,7 @@ val let_bound_idents_full: val let_bound_idents_with_modes_sorts_and_checks: value_binding list -> (Ident.t * (Location.t * Mode.Value.l * Jkind.sort) list - * Builtin_attributes.zero_alloc_attribute) list + * Zero_alloc.t) list (** Alpha conversion of patterns *) val alpha_pat: diff --git a/ocaml/typing/types.ml b/ocaml/typing/types.ml index c550cdd6465..88057ae476c 100644 --- a/ocaml/typing/types.ml +++ b/ocaml/typing/types.ml @@ -441,7 +441,7 @@ module type Wrapped = sig val_modalities : Mode.Modality.Value.t; (* Modalities on the value *) val_kind: value_kind; val_loc: Location.t; - val_zero_alloc: Builtin_attributes.zero_alloc_attribute; + val_zero_alloc: Zero_alloc.t; val_attributes: Parsetree.attributes; val_uid: Uid.t; } diff --git a/ocaml/typing/types.mli b/ocaml/typing/types.mli index 97132fea756..6b812c1d03b 100644 --- a/ocaml/typing/types.mli +++ b/ocaml/typing/types.mli @@ -746,7 +746,7 @@ module type Wrapped = sig val_modalities: Mode.Modality.Value.t; (* Modalities on the value *) val_kind: value_kind; val_loc: Location.t; - val_zero_alloc: Builtin_attributes.zero_alloc_attribute; + val_zero_alloc: Zero_alloc.t; val_attributes: Parsetree.attributes; val_uid: Uid.t; } diff --git a/ocaml/typing/zero_alloc.ml b/ocaml/typing/zero_alloc.ml new file mode 100644 index 00000000000..dcbb38c231f --- /dev/null +++ b/ocaml/typing/zero_alloc.ml @@ -0,0 +1,102 @@ +module ZA = Zero_alloc_utils + +type t = Builtin_attributes.zero_alloc_attribute = + | Default_zero_alloc + | Ignore_assert_all + | Check of { strict: bool; + opt: bool; + arity: int; + loc: Location.t; + } + | Assume of { strict: bool; + never_returns_normally: bool; + never_raises: bool; + arity: int; + loc: Location.t; + } + +type error = + | Less_general of { missing_entirely : bool } + | Arity_mismatch of int * int + +exception Error of error + +let print_error ppf error = + let pr fmt = Format.fprintf ppf fmt in + match error with + | Less_general { missing_entirely } -> + pr "The former provides a weaker \"zero_alloc\" guarantee than the latter."; + if missing_entirely then + pr "@ Hint: Add a \"zero_alloc\" attribute to the implementation." + | Arity_mismatch (n1, n2) -> + pr "zero_alloc arity mismatch:@ \ + When using \"zero_alloc\" in a signature, the syntactic arity of@ \ + the implementation must match the function type in the interface.@ \ + Here the former is %d and the latter is %d." + n1 n2 + +let sub_exn za1 za2 = + (* The core of the check here is that we translate both attributes into the + abstract domain and use the existing inclusion check from there, ensuring + what we do in the typechecker matches the backend. + + There are a few additional details: + + - [opt] is not captured by the abstract domain, so we need a special check + for it. But it doesn't interact at all with the abstract domain - it's + just about whether or not the check happens - so this special check can + be fully separate. + - [arity] is also not captured by the abstract domain - it exists only for + use here, in typechecking. If the arities do not match, we issue an + error. It's essential for the soundness of the way we (will, in the next + PR) use zero_alloc in signatures that the apparent arity of the type in + the signature matches the syntactic arity of the function. + - [ignore] can not appear in zero_alloc attributes in signatures, and is + erased from structure items when computing their signature, so we don't + need to consider it here. + *) + let open Builtin_attributes in + (* abstract domain check *) + let abstract_value za = + match za with + | Default_zero_alloc | Ignore_assert_all -> ZA.Assume_info.Value.top () + | Check { strict; _ } -> + ZA.Assume_info.Value.of_annotation ~strict ~never_returns_normally:false + ~never_raises:false + | Assume { strict; never_returns_normally; never_raises; } -> + ZA.Assume_info.Value.of_annotation ~strict ~never_returns_normally + ~never_raises + in + let v1 = abstract_value za1 in + let v2 = abstract_value za2 in + if not (ZA.Assume_info.Value.lessequal v1 v2) then + begin let missing_entirely = + match za1 with + | Default_zero_alloc -> true + | Ignore_assert_all | Check _ | Assume _ -> false + in + raise (Error (Less_general {missing_entirely})) + end; + (* opt check *) + begin match za1, za2 with + | Check { opt = opt1; _ }, Check { opt = opt2; _ } -> + if opt1 && not opt2 then + raise (Error (Less_general {missing_entirely = false})) + | (Check _ | Default_zero_alloc | Assume _ | Ignore_assert_all), _ -> () + end; + (* arity check *) + let get_arity = function + | Check { arity; _ } | Assume { arity; _ } -> Some arity + | Default_zero_alloc | Ignore_assert_all -> None + in + match get_arity za1, get_arity za2 with + | Some arity1, Some arity2 -> + (* Check *) + if not (arity1 = arity2) then + raise (Error (Arity_mismatch (arity1, arity2))) + | Some _, None -> () + (* Forgetting zero_alloc info is fine *) + | None, Some _ -> + (* Fabricating it is not, but earlier cases should have ruled this out *) + Misc.fatal_error "Zero_alloc: sub" + | None, None -> () diff --git a/ocaml/typing/zero_alloc.mli b/ocaml/typing/zero_alloc.mli new file mode 100644 index 00000000000..61e8660c23a --- /dev/null +++ b/ocaml/typing/zero_alloc.mli @@ -0,0 +1,24 @@ +type t = Builtin_attributes.zero_alloc_attribute = + | Default_zero_alloc + | Ignore_assert_all + | Check of { strict: bool; + opt: bool; + arity: int; + loc: Location.t; + } + | Assume of { strict: bool; + never_returns_normally: bool; + never_raises: bool; + arity: int; + loc: Location.t; + } + +type error + +exception Error of error + +val print_error : Format.formatter -> error -> unit + +(* [sub_exn t1 t2] checks whether the zero_alloc check t1 is stronger than the + zero_alloc check t2. If not, it raises [Error]. *) +val sub_exn : t -> t -> unit From f56e3b772a3a6564011d81b8954c5ee9ac622416 Mon Sep 17 00:00:00 2001 From: Chris Casinghino Date: Thu, 27 Jun 2024 12:06:31 -0400 Subject: [PATCH 3/8] Implement inference and add tests --- chamelon/compat.jst.ml | 10 +- native_toplevel/opttoploop.ml | 2 +- ocaml/lambda/translcore.ml | 20 +- .../tests/typing-zero-alloc/cmi_test.ml | 77 ++++ .../tests/typing-zero-alloc/cmi_test_lib.ml | 16 + .../tests/typing-zero-alloc/signatures.ml | 410 +++++++++++++----- ocaml/typing/printtyp.ml | 2 +- ocaml/typing/subst.ml | 12 +- ocaml/typing/typeclass.ml | 8 +- ocaml/typing/typecore.ml | 30 +- ocaml/typing/typedecl.ml | 24 +- ocaml/typing/typedtree.ml | 30 +- ocaml/typing/typemod.ml | 52 ++- ocaml/typing/types.ml | 5 +- ocaml/typing/zero_alloc.ml | 83 +++- ocaml/typing/zero_alloc.mli | 34 +- tests/backend/zero_alloc_checker/dune.inc | 38 ++ .../zero_alloc_checker/gen/gen_dune.ml | 9 + .../zero_alloc_checker/test_inference.ml | 84 ++++ .../zero_alloc_checker/test_inference.mli | 25 ++ .../test_inference.opt.output | 65 +++ .../zero_alloc_checker/test_inference.output | 47 ++ 22 files changed, 889 insertions(+), 194 deletions(-) create mode 100644 ocaml/testsuite/tests/typing-zero-alloc/cmi_test.ml create mode 100644 ocaml/testsuite/tests/typing-zero-alloc/cmi_test_lib.ml create mode 100644 tests/backend/zero_alloc_checker/test_inference.ml create mode 100644 tests/backend/zero_alloc_checker/test_inference.mli create mode 100644 tests/backend/zero_alloc_checker/test_inference.opt.output create mode 100644 tests/backend/zero_alloc_checker/test_inference.output diff --git a/chamelon/compat.jst.ml b/chamelon/compat.jst.ml index 919596f2bbe..d1f5b959456 100644 --- a/chamelon/compat.jst.ml +++ b/chamelon/compat.jst.ml @@ -19,13 +19,13 @@ let mkTexp_ident ?id:(ident_kind, uu = (Id_value, shared_many_use)) type nonrec apply_arg = apply_arg type texp_apply_identifier = - apply_position * Locality.l * Zero_alloc_utils.Assume_info.t + apply_position * Locality.l * Builtin_attributes.zero_alloc_attribute let mkTexp_apply ?id:(pos, mode, za = ( Default, Locality.disallow_right Locality.legacy, - Zero_alloc_utils.Assume_info.none )) (exp, args) = + Builtin_attributes.Default_zero_alloc )) (exp, args) = let args = List.map (fun (label, x) -> (Typetexp.transl_label label None, x)) args in @@ -92,7 +92,7 @@ type texp_function_identifier = { ret_sort : Jkind.sort; region : bool; ret_mode : Alloc.l; - zero_alloc : Builtin_attributes.zero_alloc_attribute; + zero_alloc : Zero_alloc.t; } let texp_function_cases_identifier_defaults = @@ -119,7 +119,7 @@ let texp_function_defaults = ret_sort = Jkind.Sort.value; ret_mode = Alloc.disallow_right Alloc.legacy; region = false; - zero_alloc = Builtin_attributes.Default_zero_alloc; + zero_alloc = Zero_alloc.default; } let mkTexp_function ?(id = texp_function_defaults) @@ -403,7 +403,7 @@ let mk_value_description ~val_type ~val_kind ~val_attributes = val_modalities = Mode.Modality.Value.id; val_attributes; val_uid = Uid.internal_not_actually_unique; - val_zero_alloc = Default_zero_alloc; + val_zero_alloc = Zero_alloc.default; } let mkTtyp_any = Ttyp_var (None, None) diff --git a/native_toplevel/opttoploop.ml b/native_toplevel/opttoploop.ml index a7138a460f5..5e90335f5e7 100644 --- a/native_toplevel/opttoploop.ml +++ b/native_toplevel/opttoploop.ml @@ -344,7 +344,7 @@ let name_expression ~loc ~attrs sort exp = val_kind = Val_reg; val_loc = loc; val_attributes = attrs; - val_zero_alloc = Default_zero_alloc; + val_zero_alloc = Zero_alloc.default; val_modalities = Mode.Modality.Value.id; val_uid = Uid.internal_not_actually_unique; } in diff --git a/ocaml/lambda/translcore.ml b/ocaml/lambda/translcore.ml index 31f6d525fae..2b996880a3b 100644 --- a/ocaml/lambda/translcore.ml +++ b/ocaml/lambda/translcore.ml @@ -353,14 +353,14 @@ let can_apply_primitive p pmode pos args = let zero_alloc_of_application ~num_args (annotation : Builtin_attributes.zero_alloc_attribute) funct = let zero_alloc = - match annotation with - | Assume _ -> + match annotation, funct.exp_desc with + | Assume _, _ -> (* The user wrote a zero_alloc attribute on the application - keep it. *) annotation - | Ignore_assert_all | Check _ -> + | (Ignore_assert_all | Check _), _ -> (* These are rejected in typecore *) Misc.fatal_error "Translcore.zero_alloc_of_application: illegal attr" - | Default_zero_alloc -> + | Default_zero_alloc, Texp_ident (_, _, { val_zero_alloc; _ }, _, _) -> (* We assume the call is zero_alloc if the function is known to be zero_alloc. If the function is zero_alloc opt, then we need to be sure that the opt checks were run to license this assumption. We judge @@ -371,9 +371,8 @@ let zero_alloc_of_application | Check_default | No_check -> false | Check_all | Check_opt_only -> true in - match funct.exp_desc with - | Texp_ident (_, _, { val_zero_alloc = (Check c); _ }, _, _) - when c.arity = num_args && (use_opt || not c.opt) -> + begin match Zero_alloc.get val_zero_alloc with + | Check c when c.arity = num_args && (use_opt || not c.opt) -> Builtin_attributes.Assume { strict = c.strict; never_returns_normally = false; @@ -381,8 +380,10 @@ let zero_alloc_of_application arity = c.arity; loc = c.loc } - | _ -> Builtin_attributes.Default_zero_alloc - + | Check _ | Default_zero_alloc | Ignore_assert_all | Assume _ -> + Builtin_attributes.Default_zero_alloc + end + | Default_zero_alloc, _ -> Builtin_attributes.Default_zero_alloc in Builtin_attributes.assume_zero_alloc zero_alloc @@ -1619,6 +1620,7 @@ and transl_function ~in_new_scope ~scopes e params body ~zero_alloc = let attrs = e.exp_attributes in let mode = transl_alloc_mode_r alloc_mode in + let zero_alloc = Zero_alloc.get zero_alloc in let assume_zero_alloc = Builtin_attributes.assume_zero_alloc zero_alloc in let scopes = if in_new_scope then diff --git a/ocaml/testsuite/tests/typing-zero-alloc/cmi_test.ml b/ocaml/testsuite/tests/typing-zero-alloc/cmi_test.ml new file mode 100644 index 00000000000..2bc3006afb9 --- /dev/null +++ b/ocaml/testsuite/tests/typing-zero-alloc/cmi_test.ml @@ -0,0 +1,77 @@ +(* TEST + readonly_files = "cmi_test_lib.ml"; + setup-ocamlc.byte-build-env; + module = "cmi_test_lib.ml"; + ocamlc.byte; + flags += "-I ocamlc.byte"; + expect; +*) + +(* Here we show the signatures of [cmi_test_a] and the modules within it do not + have zero_alloc variables - we can't add further zero_alloc constraints. *) +module M1 : sig + val[@zero_alloc] f_unconstrained_variable : int -> int +end = Cmi_test_lib +[%%expect{| +Line 3, characters 6-18: +3 | end = Cmi_test_lib + ^^^^^^^^^^^^ +Error: Signature mismatch: + Modules do not match: + sig + val f_unconstrained_variable : int -> int + module M_constrained_variable = + Cmi_test_lib.M_constrained_variable + module M_no_variable = Cmi_test_lib.M_no_variable + end + is not included in + sig val f_unconstrained_variable : int -> int [@@zero_alloc] end + Values do not match: + val f_unconstrained_variable : int -> int + is not included in + val f_unconstrained_variable : int -> int [@@zero_alloc] + The former provides a weaker "zero_alloc" guarantee than the latter. + Hint: Add a "zero_alloc" attribute to the implementation. + File "cmi_test_lib.ml", line 4, characters 4-28: Actual declaration +|}] + +module M2 : sig + val[@zero_alloc strict] f : int -> int +end = Cmi_test_lib.M_constrained_variable +[%%expect{| +Line 3, characters 6-41: +3 | end = Cmi_test_lib.M_constrained_variable + ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ +Error: Signature mismatch: + Modules do not match: + sig val f : int -> int [@@zero_alloc] end + is not included in + sig val f : int -> int [@@zero_alloc strict] end + Values do not match: + val f : int -> int [@@zero_alloc] + is not included in + val f : int -> int [@@zero_alloc strict] + The former provides a weaker "zero_alloc" guarantee than the latter. + File "cmi_test_lib.ml", line 7, characters 6-7: Actual declaration +|}] + +module M3 : sig + val[@zero_alloc] f : int -> int +end = Cmi_test_lib.M_no_variable +[%%expect{| +Line 3, characters 6-32: +3 | end = Cmi_test_lib.M_no_variable + ^^^^^^^^^^^^^^^^^^^^^^^^^^ +Error: Signature mismatch: + Modules do not match: + sig val f : int -> int end + is not included in + sig val f : int -> int [@@zero_alloc] end + Values do not match: + val f : int -> int + is not included in + val f : int -> int [@@zero_alloc] + The former provides a weaker "zero_alloc" guarantee than the latter. + Hint: Add a "zero_alloc" attribute to the implementation. + File "cmi_test_lib.ml", line 13, characters 2-20: Actual declaration +|}] diff --git a/ocaml/testsuite/tests/typing-zero-alloc/cmi_test_lib.ml b/ocaml/testsuite/tests/typing-zero-alloc/cmi_test_lib.ml new file mode 100644 index 00000000000..6f50699f052 --- /dev/null +++ b/ocaml/testsuite/tests/typing-zero-alloc/cmi_test_lib.ml @@ -0,0 +1,16 @@ +(* This file is part of a test that zero_alloc variables don't remain in + cmis. *) + +let f_unconstrained_variable x = x+1 + +module M_constrained_variable = struct + let f x = x+2 +end + +module _ : sig val[@zero_alloc] f : int -> int end = M_constrained_variable + +module M_no_variable : sig + val f : int -> int +end = struct + let f x = x+3 +end diff --git a/ocaml/testsuite/tests/typing-zero-alloc/signatures.ml b/ocaml/testsuite/tests/typing-zero-alloc/signatures.ml index 0add10a1ee5..ce5c7527f65 100644 --- a/ocaml/testsuite/tests/typing-zero-alloc/signatures.ml +++ b/ocaml/testsuite/tests/typing-zero-alloc/signatures.ml @@ -62,6 +62,12 @@ module type S_good_inc_base = sig val[@zero_alloc] f : 'a -> 'a end +module M_absent : S_good_inc_base = struct + (* This one works by inferring the annotation on [f], tested further + elsewhere. *) + let f x = x +end + module M_base : S_good_inc_base = struct let[@zero_alloc] f x = x end @@ -88,6 +94,7 @@ end [%%expect{| module type S_good_inc_base = sig val f : 'a -> 'a [@@zero_alloc] end +module M_absent : S_good_inc_base module M_base : S_good_inc_base module M_assume : S_good_inc_base module M_assume_nrn : S_good_inc_base @@ -100,6 +107,12 @@ module type S_good_inc_opt = sig val[@zero_alloc opt] f : 'a -> 'a end +module M_absent : S_good_inc_opt = struct + (* This one works by inferring the annotation on [f], tested further + elsewhere. *) + let f x = x +end + module M_base : S_good_inc_opt = struct let[@zero_alloc] f x = x end @@ -134,6 +147,7 @@ end [%%expect{| module type S_good_inc_opt = sig val f : 'a -> 'a [@@zero_alloc opt] end +module M_absent : S_good_inc_opt module M_base : S_good_inc_opt module M_opt : S_good_inc_opt module M_assume : S_good_inc_opt @@ -148,6 +162,12 @@ module type S_good_inc_strict = sig val[@zero_alloc strict] f : 'a -> 'a end +module M_absent : S_good_inc_strict = struct + (* This one works by inferring the annotation on [f], tested further + elsewhere. *) + let f x = x +end + module M_strict : S_good_inc_strict = struct let[@zero_alloc strict] f x = x end @@ -163,6 +183,7 @@ end [%%expect{| module type S_good_inc_strict = sig val f : 'a -> 'a [@@zero_alloc strict] end +module M_absent : S_good_inc_strict module M_strict : S_good_inc_strict module M_assume_strict : S_good_inc_strict module M_assume_strict_nrn : S_good_inc_strict @@ -172,6 +193,12 @@ module type S_good_inc_strict_opt = sig val[@zero_alloc strict opt] f : 'a -> 'a end +module M_absent : S_good_inc_strict_opt = struct + (* This one works by inferring the annotation on [f], tested further + elsewhere. *) + let f x = x +end + module M_strict : S_good_inc_strict_opt = struct let[@zero_alloc strict] f x = x end @@ -191,6 +218,7 @@ end [%%expect{| module type S_good_inc_strict_opt = sig val f : 'a -> 'a [@@zero_alloc strict opt] end +module M_absent : S_good_inc_strict_opt module M_strict : S_good_inc_strict_opt module M_strict_opt : S_good_inc_strict_opt module M_assume_strict : S_good_inc_strict_opt @@ -205,38 +233,16 @@ module type S_bad_inc_base = sig val[@zero_alloc] f : 'a -> 'a end -module M_absent : S_bad_inc_base = struct - let f x = x -end - -[%%expect{| -module type S_bad_inc_base = sig val f : 'a -> 'a [@@zero_alloc] end -Lines 5-7, characters 35-3: -5 | ...................................struct -6 | let f x = x -7 | end -Error: Signature mismatch: - Modules do not match: - sig val f : 'a -> 'a end - is not included in - S_bad_inc_base - Values do not match: - val f : 'a -> 'a - is not included in - val f : 'a -> 'a [@@zero_alloc] - The former provides a weaker "zero_alloc" guarantee than the latter. - Hint: Add a "zero_alloc" attribute to the implementation. -|}] - module M_opt : S_bad_inc_base = struct let[@zero_alloc opt] f x = x end [%%expect{| -Lines 1-3, characters 32-3: -1 | ................................struct -2 | let[@zero_alloc opt] f x = x -3 | end +module type S_bad_inc_base = sig val f : 'a -> 'a [@@zero_alloc] end +Lines 5-7, characters 32-3: +5 | ................................struct +6 | let[@zero_alloc opt] f x = x +7 | end Error: Signature mismatch: Modules do not match: sig val f : 'a -> 'a [@@zero_alloc opt] end @@ -249,68 +255,19 @@ Error: Signature mismatch: The former provides a weaker "zero_alloc" guarantee than the latter. |}] -module type S_bad_inc_opt = sig - val[@zero_alloc opt] f : 'a -> 'a -end - -module M_absent : S_bad_inc_opt = struct - let f x = x -end - -[%%expect{| -module type S_bad_inc_opt = sig val f : 'a -> 'a [@@zero_alloc opt] end -Lines 5-7, characters 34-3: -5 | ..................................struct -6 | let f x = x -7 | end -Error: Signature mismatch: - Modules do not match: - sig val f : 'a -> 'a end - is not included in - S_bad_inc_opt - Values do not match: - val f : 'a -> 'a - is not included in - val f : 'a -> 'a [@@zero_alloc opt] - The former provides a weaker "zero_alloc" guarantee than the latter. - Hint: Add a "zero_alloc" attribute to the implementation. -|}] - module type S_bad_inc_strict = sig val[@zero_alloc strict] f : 'a -> 'a end -module M_absent : S_bad_inc_strict = struct - let f x = x -end - -[%%expect{| -module type S_bad_inc_strict = sig val f : 'a -> 'a [@@zero_alloc strict] end -Lines 5-7, characters 37-3: -5 | .....................................struct -6 | let f x = x -7 | end -Error: Signature mismatch: - Modules do not match: - sig val f : 'a -> 'a end - is not included in - S_bad_inc_strict - Values do not match: - val f : 'a -> 'a - is not included in - val f : 'a -> 'a [@@zero_alloc strict] - The former provides a weaker "zero_alloc" guarantee than the latter. - Hint: Add a "zero_alloc" attribute to the implementation. -|}] - module M_base : S_bad_inc_strict = struct let[@zero_alloc] f x = x end [%%expect{| -Lines 1-3, characters 35-3: -1 | ...................................struct -2 | let[@zero_alloc] f x = x -3 | end +module type S_bad_inc_strict = sig val f : 'a -> 'a [@@zero_alloc strict] end +Lines 5-7, characters 35-3: +5 | ...................................struct +6 | let[@zero_alloc] f x = x +7 | end Error: Signature mismatch: Modules do not match: sig val f : 'a -> 'a [@@zero_alloc] end @@ -411,38 +368,16 @@ module type S_strict_opt = sig val[@zero_alloc strict opt] f : 'a -> 'a end -module M_absent : S_strict_opt = struct - let f x = x +module M_assume : S_strict_opt = struct + let[@zero_alloc assume] f x = x end [%%expect{| module type S_strict_opt = sig val f : 'a -> 'a [@@zero_alloc strict opt] end Lines 5-7, characters 33-3: 5 | .................................struct -6 | let f x = x +6 | let[@zero_alloc assume] f x = x 7 | end -Error: Signature mismatch: - Modules do not match: - sig val f : 'a -> 'a end - is not included in - S_strict_opt - Values do not match: - val f : 'a -> 'a - is not included in - val f : 'a -> 'a [@@zero_alloc strict opt] - The former provides a weaker "zero_alloc" guarantee than the latter. - Hint: Add a "zero_alloc" attribute to the implementation. -|}] - -module M_assume : S_strict_opt = struct - let[@zero_alloc assume] f x = x -end - -[%%expect{| -Lines 1-3, characters 33-3: -1 | .................................struct -2 | let[@zero_alloc assume] f x = x -3 | end Error: Signature mismatch: Modules do not match: sig val f : 'a -> 'a [@@zero_alloc] end @@ -920,7 +855,7 @@ module M_mto_base_good : S_base_mto = struct end module M_mto_base_bad : S_base_mto = struct - let f x = x + 3 + let[@zero_alloc opt] f x = x + 3 end [%%expect{| @@ -929,19 +864,18 @@ module type S_base_mto = sig val f : int -> int [@@zero_alloc] end module M_mto_base_good : S_base_mto Lines 11-13, characters 37-3: 11 | .....................................struct -12 | let f x = x + 3 +12 | let[@zero_alloc opt] f x = x + 3 13 | end Error: Signature mismatch: Modules do not match: - sig val f : int -> int end + sig val f : int -> int [@@zero_alloc opt] end is not included in S_base_mto Values do not match: - val f : int -> int + val f : int -> int [@@zero_alloc opt] is not included in val f : int -> int [@@zero_alloc] The former provides a weaker "zero_alloc" guarantee than the latter. - Hint: Add a "zero_alloc" attribute to the implementation. |}] module M_strict_for_mto = struct @@ -1002,3 +936,257 @@ module type S_no_assume = sig val f : int -> int * int [@@zero_alloc] end module M_nrn_for_mto : sig val f : int -> int * int [@@zero_alloc] end module type S_no_nrn = sig val f : int -> int * int [@@zero_alloc] end |}] + +(**********************************************) +(* Test 11: inference from signatures, basics *) + +(* As mentioned above, we aren't testing here that the functions whose need to + be checked for zero_alloc is inferred actually get checked. That is done in + the backend tests. Here we are just showing that type system's view of the + zero_allocness of a function is inferrable. +*) + +(* Should work by setting zero_alloc variables in f and g. *) +module M_infer1 : sig + val[@zero_alloc] f : int -> int + val g : int -> int +end = struct + let f x = x + let g x = x +end + +(* Should be rejected because the signature we have for M_infer1 doesn't have + vars in it (and its zero_alloc values are too weak). *) +module M_infer1' : sig + val[@zero_alloc] f : int -> int + val[@zero_alloc] g : int -> int +end = M_infer1 +[%%expect{| +module M_infer1 : + sig val f : int -> int [@@zero_alloc] val g : int -> int end +Line 14, characters 6-14: +14 | end = M_infer1 + ^^^^^^^^ +Error: Signature mismatch: + Modules do not match: + sig val f : int -> int [@@zero_alloc] val g : int -> int end + is not included in + sig + val f : int -> int [@@zero_alloc] + val g : int -> int [@@zero_alloc] + end + Values do not match: + val g : int -> int + is not included in + val g : int -> int [@@zero_alloc] + The former provides a weaker "zero_alloc" guarantee than the latter. + Hint: Add a "zero_alloc" attribute to the implementation. +|}] + +module M_infer2 = struct + let f x = x + let g x = x +end + +(* Should work by updating the variables. *) +module M_infer2' : sig + val[@zero_alloc opt] f : int -> int + val[@zero_alloc] g : int -> int +end = M_infer2 (* 1 *) + +(* Should work by zero-alloc subtyping. *) +module M_infer2'' : sig + val[@zero_alloc opt] f : int -> int + val[@zero_alloc opt] g : int -> int +end = M_infer2 (* 2 *) + +(* Should work by updating the variables again. *) +module M_infer2''' : sig + val[@zero_alloc] f : int -> int + val[@zero_alloc] g : int -> int +end = M_infer2 (* 3 *) + +(* Here we update the variable on [f] but [g] works by subtyping. *) +module M_infer2'''' : sig + val[@zero_alloc strict] f : int -> int + val[@zero_alloc opt] g : int -> int +end = M_infer2 (* 4 *) +[%%expect{| +module M_infer2 : sig val f : 'a -> 'a val g : 'a -> 'a end +module M_infer2' : + sig + val f : int -> int [@@zero_alloc opt] + val g : int -> int [@@zero_alloc] + end +module M_infer2'' : + sig + val f : int -> int [@@zero_alloc opt] + val g : int -> int [@@zero_alloc opt] + end +module M_infer2''' : + sig val f : int -> int [@@zero_alloc] val g : int -> int [@@zero_alloc] end +module M_infer2'''' : + sig + val f : int -> int [@@zero_alloc strict] + val g : int -> int [@@zero_alloc opt] + end +|}] + +(* At this point, the inferred signature for [M_infer2] has the accumulated + constraints. Note that its final signature has the strictest version of the + checks done on [f] and [g] individually, even though we never compared + against exactly that combined signature. This shows, for example, that when + the constraint for [M_infer2''''] was done we modified [f]'s variable but + didn't accidentally weaken the variable on [g]. *) +module type S = module type of M_infer2 +[%%expect{| +module type S = + sig + val f : 'a -> 'a [@@zero_alloc strict] + val g : 'a -> 'a [@@zero_alloc] + end +|}] + +(********************************************) +(* Test 12: inference plays well with arity *) + +(* If the arity doesn't match the signature, you get an error. *) +module M_inf_too_many_args = struct + type t = int -> int + let f : int -> t = fun x _ -> x +end + +module _ : sig + type t + val[@zero_alloc] f : int -> t +end = M_inf_too_many_args +[%%expect{| +module M_inf_too_many_args : sig type t = int -> int val f : int -> t end +Line 9, characters 6-25: +9 | end = M_inf_too_many_args + ^^^^^^^^^^^^^^^^^^^ +Error: Signature mismatch: + Modules do not match: + sig type t = int -> int val f : int -> t end + is not included in + sig type t val f : int -> t [@@zero_alloc] end + Values do not match: + val f : int -> t + is not included in + val f : int -> t [@@zero_alloc] + zero_alloc arity mismatch: + When using "zero_alloc" in a signature, the syntactic arity of + the implementation must match the function type in the interface. + Here the former is 2 and the latter is 1. +|}] + +module M_inf_too_few_args = struct + let f x = fun y -> x + y +end + +module _ : sig + val[@zero_alloc] f : int -> int -> int +end = M_inf_too_few_args +[%%expect{| +module M_inf_too_few_args : sig val f : int -> int -> int end +Line 7, characters 6-24: +7 | end = M_inf_too_few_args + ^^^^^^^^^^^^^^^^^^ +Error: Signature mismatch: + Modules do not match: + sig val f : int -> int -> int end + is not included in + sig val f : int -> int -> int [@@zero_alloc] end + Values do not match: + val f : int -> int -> int + is not included in + val f : int -> int -> int [@@zero_alloc] + zero_alloc arity mismatch: + When using "zero_alloc" in a signature, the syntactic arity of + the implementation must match the function type in the interface. + Here the former is 1 and the latter is 2. +|}] + +(* You can fix it with an explicit arity. *) +module M_explicit_arity_2 = struct + type t = int -> int + let f : int -> t = fun x _ -> x +end + +module _ : sig + type t + val[@zero_alloc (arity 2)] f : int -> t +end = M_explicit_arity_2 + +module type S = module type of M_explicit_arity_2 +[%%expect{| +module M_explicit_arity_2 : sig type t = int -> int val f : int -> t end +module type S = + sig type t = int -> int val f : int -> t [@@zero_alloc arity 2] end +|}] + +(***************************) +(* Test 13: module type of *) + +(* When you take the module type of a module, you get the current state of its + variables. The computed signature itself has no variables, and the original + module keeps its variables (but changing them won't change the signature you + got the first time, just the signature you'll get if you do [module type of] + again). *) +module M_for_mto = struct + let f x = x+1 +end + +(* The current state of the variales is "no check" *) +module type S = module type of M_for_mto +[%%expect{| +module M_for_mto : sig val f : int -> int end +module type S = sig val f : int -> int end +|}] + +(* [S] itself is fixed. *) +module F (X : S) : sig val[@zero_alloc] f : int -> int end = X +[%%expect{| +Line 1, characters 61-62: +1 | module F (X : S) : sig val[@zero_alloc] f : int -> int end = X + ^ +Error: Signature mismatch: + Modules do not match: + sig val f : int -> int end + is not included in + sig val f : int -> int [@@zero_alloc] end + Values do not match: + val f : int -> int + is not included in + val f : int -> int [@@zero_alloc] + The former provides a weaker "zero_alloc" guarantee than the latter. + Hint: Add a "zero_alloc" attribute to the implementation. +|}] + +(* But [M_for_mto] retains its variables. Changing them changes what you get + next time you do [module type of] on it, but not [S]. *) +module _ : sig + val[@zero_alloc] f : int -> int +end = M_for_mto + +module type S' = module type of M_for_mto +module F' (X : S') : sig val[@zero_alloc] f : int -> int end = X +module F (X : S) : sig val[@zero_alloc] f : int -> int end = X +[%%expect{| +module type S' = sig val f : int -> int [@@zero_alloc] end +module F' : functor (X : S') -> sig val f : int -> int [@@zero_alloc] end +Line 7, characters 61-62: +7 | module F (X : S) : sig val[@zero_alloc] f : int -> int end = X + ^ +Error: Signature mismatch: + Modules do not match: + sig val f : int -> int end + is not included in + sig val f : int -> int [@@zero_alloc] end + Values do not match: + val f : int -> int + is not included in + val f : int -> int [@@zero_alloc] + The former provides a weaker "zero_alloc" guarantee than the latter. + Hint: Add a "zero_alloc" attribute to the implementation. +|}] diff --git a/ocaml/typing/printtyp.ml b/ocaml/typing/printtyp.ml index d69aceb8c69..c50487ee75a 100644 --- a/ocaml/typing/printtyp.ml +++ b/ocaml/typing/printtyp.ml @@ -2067,7 +2067,7 @@ let tree_of_value_description id decl = count 0 decl.val_type in let attrs = - match decl.val_zero_alloc with + match Zero_alloc.get decl.val_zero_alloc with | Default_zero_alloc | Ignore_assert_all -> [] | Check { strict; opt; arity; _ } -> [{ oattr_name = diff --git a/ocaml/typing/subst.ml b/ocaml/typing/subst.ml index 1892c1122f8..fec27310bc1 100644 --- a/ocaml/typing/subst.ml +++ b/ocaml/typing/subst.ml @@ -746,7 +746,17 @@ let rec subst_lazy_value_description s descr = val_modalities = descr.val_modalities; val_kind = descr.val_kind; val_loc = loc s descr.val_loc; - val_zero_alloc = descr.val_zero_alloc; + val_zero_alloc = + (* When saving a cmi file, we replace zero_alloc variables with constants. + This is necessary because users of the library can't change the + zero_alloc check that was done on functions in it, and safe because all + type inference is done by the time we write the cmi file (and anyway + additional inference steps could only cause the funtion to get checked + more strictly than the signature indicates, which is sound). *) + (match s.additional_action with + | Prepare_for_saving _ -> + Zero_alloc.create (Zero_alloc.get descr.val_zero_alloc) + | _ -> descr.val_zero_alloc); val_attributes = attrs s descr.val_attributes; val_uid = descr.val_uid; } diff --git a/ocaml/typing/typeclass.ml b/ocaml/typing/typeclass.ml index f12f26c5ac0..4caaf005ad0 100644 --- a/ocaml/typing/typeclass.ml +++ b/ocaml/typing/typeclass.ml @@ -490,7 +490,7 @@ let enter_ancestor_met ~loc name ~sign ~meths ~cl_num ~ty ~attrs met_env = let desc = { val_type = ty; val_modalities = Modality.Value.id; val_kind = kind; val_attributes = attrs; - val_zero_alloc = Builtin_attributes.Default_zero_alloc; + val_zero_alloc = Zero_alloc.default; Types.val_loc = loc; val_uid = Uid.mk ~current_unit:(Env.get_unit_name ()) } in @@ -506,7 +506,7 @@ let add_self_met loc id sign self_var_kind vars cl_num let desc = { val_type = ty; val_modalities = Modality.Value.id; val_kind = kind; val_attributes = attrs; - val_zero_alloc = Builtin_attributes.Default_zero_alloc; + val_zero_alloc = Zero_alloc.default; Types.val_loc = loc; val_uid = Uid.mk ~current_unit:(Env.get_unit_name ()) } in @@ -523,7 +523,7 @@ let add_instance_var_met loc label id sign cl_num attrs met_env = { val_type = ty; val_modalities = Modality.Value.id; val_kind = kind; val_attributes = attrs; Types.val_loc = loc; - val_zero_alloc = Builtin_attributes.Default_zero_alloc; + val_zero_alloc = Zero_alloc.default; val_uid = Uid.mk ~current_unit:(Env.get_unit_name ()) } in Env.add_value ~mode:Mode.Value.legacy id desc met_env @@ -1467,7 +1467,7 @@ and class_expr_aux cl_num val_env met_env virt self_scope scl = val_modalities = Modality.Value.id; val_kind = Val_ivar (Immutable, cl_num); val_attributes = []; - val_zero_alloc = Builtin_attributes.Default_zero_alloc; + val_zero_alloc = Zero_alloc.default; Types.val_loc = vd.val_loc; val_uid = vd.val_uid; } diff --git a/ocaml/typing/typecore.ml b/ocaml/typing/typecore.ml index 24924793dfb..271aa58d0f4 100644 --- a/ocaml/typing/typecore.ml +++ b/ocaml/typing/typecore.ml @@ -1121,7 +1121,7 @@ let add_pattern_variables ?check ?check_as env pv = Env.add_value ?check ~mode:pv_mode pv_id {val_type = pv_type; val_kind = Val_reg; Types.val_loc = pv_loc; val_attributes = pv_attributes; val_modalities = Modality.Value.id; - val_zero_alloc = Builtin_attributes.Default_zero_alloc; + val_zero_alloc = Zero_alloc.default; val_uid = pv_uid } env ) @@ -2916,7 +2916,7 @@ let type_class_arg_pattern cl_num val_env met_env l spat = { val_type = pv_type ; val_kind = Val_reg ; val_attributes = pv_attributes - ; val_zero_alloc = Builtin_attributes.Default_zero_alloc + ; val_zero_alloc = Zero_alloc.default ; val_modalities = Modality.Value.id ; val_loc = pv_loc ; val_uid = pv_uid @@ -2928,7 +2928,7 @@ let type_class_arg_pattern cl_num val_env met_env l spat = { val_type = pv_type ; val_kind = Val_ivar (Immutable, cl_num) ; val_attributes = pv_attributes - ; val_zero_alloc = Builtin_attributes.Default_zero_alloc + ; val_zero_alloc = Zero_alloc.default ; val_modalities = Modality.Value.id ; val_loc = pv_loc ; val_uid = pv_uid @@ -5076,7 +5076,7 @@ let pat_modes ~force_toplevel rec_mode_var (attrs, spat) = in attrs, pat_mode, exp_mode, spat -let add_check_attribute expr attributes = +let add_zero_alloc_attribute expr attributes = let open Builtin_attributes in let to_string : zero_alloc_attribute -> string = function | Check { strict; loc = _} -> @@ -5097,14 +5097,17 @@ let add_check_attribute expr attributes = in begin match za with | Default_zero_alloc -> expr - | (Ignore_assert_all | Check _ | Assume _) as check -> - begin match fn.zero_alloc with + | Ignore_assert_all | Check _ | Assume _ -> + begin match Zero_alloc.get fn.zero_alloc with | Default_zero_alloc -> () | Ignore_assert_all | Assume _ | Check _ -> Location.prerr_warning expr.exp_loc - (Warnings.Duplicated_attribute (to_string fn.zero_alloc)); + (Warnings.Duplicated_attribute (to_string za)); end; - let exp_desc = Texp_function { fn with zero_alloc = check } in + (* Here, we may be throwing away a zero_alloc variable. There's no need + to set it, because it can't have gotten anywhere else yet. *) + let zero_alloc = Zero_alloc.create za in + let exp_desc = Texp_function { fn with zero_alloc } in { expr with exp_desc } end | _ -> expr @@ -7437,7 +7440,7 @@ and type_argument ?explanation ?recarg env (mode : expected_mode) sarg let desc = { val_type = ty; val_kind = Val_reg; val_attributes = []; - val_zero_alloc = Builtin_attributes.Default_zero_alloc; + val_zero_alloc = Zero_alloc.default; val_modalities = Modality.Value.id; val_loc = Location.none; val_uid = Uid.mk ~current_unit:(Env.get_unit_name ()); @@ -7503,7 +7506,7 @@ and type_argument ?explanation ?recarg env (mode : expected_mode) sarg ret_sort; alloc_mode; region = false; - zero_alloc = Default_zero_alloc + zero_alloc = Zero_alloc.default } } in @@ -8514,7 +8517,7 @@ and type_let ?check ?check_strict ?(force_toplevel = false) (fun (s, ((_,p,_), (e, _))) pvb -> (* We check for [zero_alloc] attributes written on the [let] and move them to the function. *) - let e = add_check_attribute e pvb.pvb_attributes in + let e = add_zero_alloc_attribute e pvb.pvb_attributes in (* vb_rec_kind will be computed later for recursive bindings *) {vb_pat=p; vb_expr=e; vb_sort = s; vb_attributes=pvb.pvb_attributes; vb_loc=pvb.pvb_loc; vb_rec_kind = Dynamic; @@ -8907,6 +8910,11 @@ and type_n_ary_function Builtin_attributes.get_zero_alloc_attribute ~in_signature:false ~default_arity:syntactic_arity attributes in + let zero_alloc = + match zero_alloc with + | Default_zero_alloc -> Zero_alloc.create_var loc syntactic_arity + | (Check _ | Assume _ | Ignore_assert_all) -> Zero_alloc.create zero_alloc + in re { exp_desc = Texp_function diff --git a/ocaml/typing/typedecl.ml b/ocaml/typing/typedecl.ml index 3976c11e7ef..0d3f301f9c6 100644 --- a/ocaml/typing/typedecl.ml +++ b/ocaml/typing/typedecl.ml @@ -2912,16 +2912,18 @@ let transl_value_decl env loc valdecl = Builtin_attributes.get_zero_alloc_attribute ~in_signature:true ~default_arity valdecl.pval_attributes in - begin match zero_alloc with - | Default_zero_alloc -> () - | Check za -> - if default_arity = 0 && za.arity <= 0 then - raise (Error(valdecl.pval_loc, Zero_alloc_attr_non_function)); - if za.arity <= 0 then - raise (Error(valdecl.pval_loc, Zero_alloc_attr_bad_user_arity)); - | Assume _ | Ignore_assert_all -> - raise (Error(valdecl.pval_loc, Zero_alloc_attr_unsupported zero_alloc)) - end; + let zero_alloc = + match zero_alloc with + | Default_zero_alloc -> Zero_alloc.default + | Check za -> + if default_arity = 0 && za.arity <= 0 then + raise (Error(valdecl.pval_loc, Zero_alloc_attr_non_function)); + if za.arity <= 0 then + raise (Error(valdecl.pval_loc, Zero_alloc_attr_bad_user_arity)); + Zero_alloc.create zero_alloc + | Assume _ | Ignore_assert_all -> + raise (Error(valdecl.pval_loc, Zero_alloc_attr_unsupported zero_alloc)) + in { val_type = ty; val_kind = Val_reg; Types.val_loc = loc; val_attributes = valdecl.pval_attributes; val_modalities = modalities; val_zero_alloc = zero_alloc; @@ -2969,7 +2971,7 @@ let transl_value_decl env loc valdecl = check_unboxable env loc ty; { val_type = ty; val_kind = Val_prim prim; Types.val_loc = loc; val_attributes = valdecl.pval_attributes; val_modalities = modalities; - val_zero_alloc = Builtin_attributes.Default_zero_alloc; + val_zero_alloc = Zero_alloc.default; val_uid = Uid.mk ~current_unit:(Env.get_unit_name ()); } in diff --git a/ocaml/typing/typedtree.ml b/ocaml/typing/typedtree.ml index f571938654e..2d62684c33f 100644 --- a/ocaml/typing/typedtree.ml +++ b/ocaml/typing/typedtree.ml @@ -1068,32 +1068,34 @@ let let_bound_idents_with_modes_sorts_and_checks bindings = iter_pattern_full ~both_sides_of_or:true f vb.vb_sort vb.vb_pat; match vb.vb_pat.pat_desc, vb.vb_expr.exp_desc with | Tpat_var (id, _, _, _), Texp_function fn -> - let zero_alloc : Builtin_attributes.zero_alloc_attribute = - match fn.zero_alloc with - | Ignore_assert_all | Check _ | Assume _ -> fn.zero_alloc - | Default_zero_alloc when !Clflags.zero_alloc_check_assert_all -> + let zero_alloc = + match Zero_alloc.get fn.zero_alloc with + | Default_zero_alloc -> (* We fabricate a "Check" attribute if a top-level annotation specifies that all functions should be checked for zero - alloc. *) + alloc. There is no need to update the zero_alloc variable on the + function - if it remains [Default_zero_alloc], translcore adds + the check. *) let arity = function_arity fn.params fn.body in - if arity > 0 then - Check { strict = false; - arity; - loc = Location.none; - opt = false } + if !Clflags.zero_alloc_check_assert_all && arity > 0 then + Zero_alloc.create (Check { strict = false; + arity; + loc = Location.none; + opt = false }) else - Default_zero_alloc - | Default_zero_alloc -> Default_zero_alloc + fn.zero_alloc + | Ignore_assert_all | Check _ | Assume _ -> fn.zero_alloc in Ident.Map.add id zero_alloc checks + (* CR ccasinghino: we could copy the zero-allocness if the vb_expr + is an ident. *) | _ -> checks ) Ident.Map.empty bindings in List.rev_map (fun (id, _, _, _) -> let zero_alloc = - Option.value (Ident.Map.find_opt id checks) - ~default:Zero_alloc.Default_zero_alloc + Option.value (Ident.Map.find_opt id checks) ~default:Zero_alloc.default in id, List.rev (Ident.Tbl.find_all modes_and_sorts id), zero_alloc) (rev_let_bound_idents_full bindings) diff --git a/ocaml/typing/typemod.ml b/ocaml/typing/typemod.ml index 27524c79ac4..835cd818e1d 100644 --- a/ocaml/typing/typemod.ml +++ b/ocaml/typing/typemod.ml @@ -2119,44 +2119,56 @@ let remove_mode_and_jkind_variables env sg = let rm _env ty = Ctype.remove_mode_and_jkind_variables ty; None in List.find_map (nongen_signature_item env rm) sg |> ignore -let rec map_inferred_modalities_sg env map sg = +let rec remove_modality_and_zero_alloc_variables_sg env ~zap_modality sg = let sg_item = function | Sig_value (id, desc, vis) -> let val_modalities = desc.val_modalities - |> map |> Mode.Modality.Value.of_const + |> zap_modality |> Mode.Modality.Value.of_const in - let desc = {desc with val_modalities} in + let val_zero_alloc = + Zero_alloc.create (Zero_alloc.get desc.val_zero_alloc) + in + let desc = {desc with val_modalities; val_zero_alloc} in Sig_value (id, desc, vis) | Sig_module (id, pres, md, re, vis) -> - let md_type = map_inferred_modalities_mty env map md.md_type in + let md_type = + remove_modality_and_zero_alloc_variables_mty env ~zap_modality + md.md_type + in let md = {md with md_type} in Sig_module (id, pres, md, re, vis) | item -> item in List.map sg_item sg -and map_inferred_modalities_mty env map mty = +and remove_modality_and_zero_alloc_variables_mty env ~zap_modality mty = match mty with | Mty_ident _ | Mty_alias _ -> (* module types with names can't have inferred modalities. *) mty - | Mty_signature sg -> Mty_signature (map_inferred_modalities_sg env map sg) + | Mty_signature sg -> + Mty_signature + (remove_modality_and_zero_alloc_variables_sg env ~zap_modality sg) | Mty_functor (param, mty) -> let param : Types.functor_parameter = match param with | Named (id, mty) -> let mty = - map_inferred_modalities_mty env Mode.Modality.Value.to_const_exn mty + remove_modality_and_zero_alloc_variables_mty env + ~zap_modality:Mode.Modality.Value.to_const_exn mty in Named (id, mty) | Unit -> Unit in - let mty = map_inferred_modalities_mty env map mty in + let mty = + remove_modality_and_zero_alloc_variables_mty env ~zap_modality mty + in Mty_functor (param, mty) | Mty_strengthen (mty, path, alias) -> - let mty = map_inferred_modalities_mty - env Mode.Modality.Value.to_const_exn mty + let mty = + remove_modality_and_zero_alloc_variables_mty env + ~zap_modality:Mode.Modality.Value.to_const_exn mty in Mty_strengthen (mty, path, alias) @@ -2898,13 +2910,13 @@ and type_structure ?(toplevel = None) funct_body anchor env sstr = convert "Assume"s in structures to the equivalent "Check" for the signature. *) let open Builtin_attributes in - match[@warning "+9"] zero_alloc with - | Default_zero_alloc | Ignore_assert_all -> Default_zero_alloc - | Check _ -> zero_alloc + match[@warning "+9"] Zero_alloc.get zero_alloc with + | Default_zero_alloc | Check _ -> zero_alloc | Assume { strict; arity; loc; never_returns_normally = _; never_raises = _} -> - Check { strict; arity; loc; opt = false } + Zero_alloc.create (Check { strict; arity; loc; opt = false }) + | Ignore_assert_all -> Zero_alloc.default in let (first_loc, _, _) = List.hd id_info in Signature_names.check_value names first_loc id; @@ -3305,7 +3317,10 @@ let type_module_type_of env smod = check_nongen_modtype env smod.pmod_loc mty; (* for [module type of], we zap to identity modality for best legacy compatibility *) - let mty = map_inferred_modalities_mty env Mode.Modality.Value.zap_to_id mty in + let mty = + remove_modality_and_zero_alloc_variables_mty env + ~zap_modality:Mode.Modality.Value.zap_to_id mty + in tmty, mty (* For Typecore *) @@ -3521,7 +3536,8 @@ let type_implementation ~sourcefile outputprefix modulename initial_env ast = let simple_sg = (* Printing [.mli] from [.ml], we zap to identity modality for legacy compatibility. *) - map_inferred_modalities_sg finalenv Mode.Modality.Value.zap_to_id simple_sg + remove_modality_and_zero_alloc_variables_sg finalenv + ~zap_modality:Mode.Modality.Value.zap_to_id simple_sg in Typecore.force_delayed_checks (); Typecore.optimise_allocations (); @@ -3620,8 +3636,8 @@ let type_implementation ~sourcefile outputprefix modulename initial_env ast = let simple_sg = (* Generating [cmi] without [mli]. This [cmi] will only be on the LHS of inclusion check, so we zap to floor (strongest). *) - map_inferred_modalities_sg finalenv Mode.Modality.Value.zap_to_floor - simple_sg + remove_modality_and_zero_alloc_variables_sg finalenv + ~zap_modality:Mode.Modality.Value.zap_to_floor simple_sg in normalize_signature simple_sg; let argument_interface = diff --git a/ocaml/typing/types.ml b/ocaml/typing/types.ml index 88057ae476c..d718708406c 100644 --- a/ocaml/typing/types.ml +++ b/ocaml/typing/types.ml @@ -777,6 +777,7 @@ type change = | Cuniv : type_expr option ref * type_expr option -> change | Cmodes : Mode.changes -> change | Csort : Jkind_types.Sort.change -> change + | Czero_alloc : Zero_alloc.change -> change type changes = Change of change * changes ref @@ -792,7 +793,8 @@ let log_change ch = let () = Mode.set_append_changes (fun changes -> log_change (Cmodes !changes)); - Jkind_types.Sort.set_change_log (fun change -> log_change (Csort change)) + Jkind_types.Sort.set_change_log (fun change -> log_change (Csort change)); + Zero_alloc.set_change_log (fun change -> log_change (Czero_alloc change)) (* constructor and accessors for [field_kind] *) @@ -1043,6 +1045,7 @@ let undo_change = function | Cuniv (r, v) -> r := v | Cmodes c -> Mode.undo_changes c | Csort change -> Jkind_types.Sort.undo_change change + | Czero_alloc c -> Zero_alloc.undo_change c type snapshot = changes ref * int let last_snapshot = Local_store.s_ref 0 diff --git a/ocaml/typing/zero_alloc.ml b/ocaml/typing/zero_alloc.ml index dcbb38c231f..bd59bcad37d 100644 --- a/ocaml/typing/zero_alloc.ml +++ b/ocaml/typing/zero_alloc.ml @@ -1,6 +1,6 @@ module ZA = Zero_alloc_utils -type t = Builtin_attributes.zero_alloc_attribute = +type const = Builtin_attributes.zero_alloc_attribute = | Default_zero_alloc | Ignore_assert_all | Check of { strict: bool; @@ -15,6 +15,40 @@ type t = Builtin_attributes.zero_alloc_attribute = loc: Location.t; } +type desc = { strict : bool; opt : bool } + +type var = + { loc : Location.t; + arity : int; + mutable desc : desc option; + (* None indicates the default case (no check will be done). If the desc is + present this var has been constrained by some signature that requires a + check. *) + } + +type t = + | Const of const + | Var of var + +(* For backtracking *) +type change = desc option * var +let undo_change (d, v) = v.desc <- d +let log_change = ref (fun _ -> ()) +let set_change_log f = log_change := f + +let create x = Const x +let create_var loc arity = Var { loc; arity; desc = None } +let default = Const Default_zero_alloc + +let get (t : t) = + match t with + | Const c -> c + | Var { loc; arity; desc } -> + match desc with + | None -> Default_zero_alloc + | Some { strict; opt } -> + Check { loc; arity; strict; opt } + type error = | Less_general of { missing_entirely : bool } | Arity_mismatch of int * int @@ -35,7 +69,7 @@ let print_error ppf error = Here the former is %d and the latter is %d." n1 n2 -let sub_exn za1 za2 = +let sub_const_const_exn za1 za2 = (* The core of the check here is that we translate both attributes into the abstract domain and use the existing inclusion check from there, ensuring what we do in the typechecker matches the backend. @@ -98,5 +132,48 @@ let sub_exn za1 za2 = (* Forgetting zero_alloc info is fine *) | None, Some _ -> (* Fabricating it is not, but earlier cases should have ruled this out *) - Misc.fatal_error "Zero_alloc: sub" + Misc.fatal_error "Zero_alloc: sub_const_exn" | None, None -> () + +let sub_var_const_exn v c = + (* This can only fail due to an arity mismatch. We have a linear order and can + always constrain the var lower to make the sub succeed. *) + match v, c with + | _, (Default_zero_alloc | Ignore_assert_all | Assume _) -> assert false + | { arity = arity1; _ }, Check { arity = arity2; _ } + when arity1 <> arity2 -> + raise (Error (Arity_mismatch (arity1, arity2))) + | { desc = None; _ }, Check { strict; opt; _ } -> + !log_change (None, v); + v.desc <- Some { strict; opt } + | { desc = (Some { strict = strict1; opt = opt1 } as desc); _ }, + Check { strict = strict2; opt = opt2 } -> + let strict = strict1 || strict2 in + let opt = opt1 && opt2 in + if strict <> strict1 || opt <> opt1 then begin + !log_change (desc, v); + v.desc <- Some { strict; opt } + end + +let sub_exn za1 za2 = + match za1, za2 with + | _, Var _ -> + (* A fully inferred signature will never have a variable in it, so we almost + never have to constrain by a variable, but there is one special case: + + The typing of modules (e.g., the [Pmod_structure] case of + [Typemod.type_module_aux]) works by (1) computing a naive signature + containing every definition in the module, (2) constructing a simplfied + signature that, for example, removes shadowed things, and (3) + constraining the original signature by the simplfied signature. These + signatures _do_ have variables in them, so we allow the special case of + constraining a variable by itself (which is obviously sound in any + event). + *) + if not (za1 == za2) then + Misc.fatal_error "zero_alloc: variable constraint" + | _, Const (Ignore_assert_all | Assume _) -> + Misc.fatal_error "zero_alloc: invalid constraint" + | _, (Const Default_zero_alloc) -> () + | Var v, Const c -> sub_var_const_exn v c + | Const c1, Const c2 -> sub_const_const_exn c1 c2 diff --git a/ocaml/typing/zero_alloc.mli b/ocaml/typing/zero_alloc.mli index 61e8660c23a..c1f390f300a 100644 --- a/ocaml/typing/zero_alloc.mli +++ b/ocaml/typing/zero_alloc.mli @@ -1,4 +1,4 @@ -type t = Builtin_attributes.zero_alloc_attribute = +type const = Builtin_attributes.zero_alloc_attribute = | Default_zero_alloc | Ignore_assert_all | Check of { strict: bool; @@ -13,12 +13,38 @@ type t = Builtin_attributes.zero_alloc_attribute = loc: Location.t; } -type error +(* This type represents whether or not a function will be checked for + zero-alloc-ness, and with what configuration (strict, opt, etc). It can be a + variable which will be filled in when the module the function is in is + compared against its signature, allowing to infer zero-alloc checks. *) +type t -exception Error of error +(* [default] corresponds to [Default_zero_alloc], meaning no check will be + done. *) +val default : t + +val create : const -> t + +(* [create_var loc n] creates a variable. [loc] is the location of the function + you are creating a variable for, and [n] is its syntactic arity of the + function the variable is being created for. *) +val create_var : Location.t -> int -> t +(* In the case [t] is a variable, [get t] returns its current contents as a + [const] and has no effect. *) +val get : t -> const + +(* For types.ml's backtracking mechanism. *) +type change +val set_change_log : (change -> unit) -> unit +val undo_change : change -> unit + +(* These are the errors that may be raised by [sub_exn] below. *) +type error +exception Error of error val print_error : Format.formatter -> error -> unit (* [sub_exn t1 t2] checks whether the zero_alloc check t1 is stronger than the - zero_alloc check t2. If not, it raises [Error]. *) + zero_alloc check t2. If not, it raises [Error]. If [t1] is a variable, it may + be set to make the relation hold. *) val sub_exn : t -> t -> unit diff --git a/tests/backend/zero_alloc_checker/dune.inc b/tests/backend/zero_alloc_checker/dune.inc index 27723d9ba2c..539ab10f266 100644 --- a/tests/backend/zero_alloc_checker/dune.inc +++ b/tests/backend/zero_alloc_checker/dune.inc @@ -1073,3 +1073,41 @@ (enabled_if (= %{context_name} "main")) (deps test_bounded_join4.output test_bounded_join4.output.corrected) (action (diff test_bounded_join4.output test_bounded_join4.output.corrected))) + +(rule + (enabled_if (= %{context_name} "main")) + (targets test_inference.output.corrected) + (deps (:ml test_inference.mli test_inference.ml) filter.sh) + (action + (with-outputs-to test_inference.output.corrected + (pipe-outputs + (with-accepted-exit-codes 2 + (run %{bin:ocamlopt.opt} %{ml} -g -color never -error-style short -c + -zero-alloc-check default -zero-alloc-checker-details-cutoff 20 -O3)) + (run "./filter.sh") + )))) + +(rule + (alias runtest) + (enabled_if (= %{context_name} "main")) + (deps test_inference.output test_inference.output.corrected) + (action (diff test_inference.output test_inference.output.corrected))) + +(rule + (enabled_if (= %{context_name} "main")) + (targets test_inference.opt.output.corrected) + (deps (:ml test_inference.mli test_inference.ml) filter.sh) + (action + (with-outputs-to test_inference.opt.output.corrected + (pipe-outputs + (with-accepted-exit-codes 2 + (run %{bin:ocamlopt.opt} %{ml} -g -color never -error-style short -c + -zero-alloc-check all -zero-alloc-checker-details-cutoff 20 -O3)) + (run "./filter.sh") + )))) + +(rule + (alias runtest) + (enabled_if (= %{context_name} "main")) + (deps test_inference.opt.output test_inference.opt.output.corrected) + (action (diff test_inference.opt.output test_inference.opt.output.corrected))) diff --git a/tests/backend/zero_alloc_checker/gen/gen_dune.ml b/tests/backend/zero_alloc_checker/gen/gen_dune.ml index 761c6c370be..d8a574b4860 100644 --- a/tests/backend/zero_alloc_checker/gen/gen_dune.ml +++ b/tests/backend/zero_alloc_checker/gen/gen_dune.ml @@ -197,4 +197,13 @@ let () = print_test_expected_output ~cutoff:3 ~extra_flags:"-zero-alloc-check default -zero-alloc-checker-join 0" ~extra_dep:None ~exit_code:2 "test_bounded_join4"; + print_test_expected_output ~cutoff:default_cutoff + ~output:"test_inference.output" + ~extra_dep:(Some "test_inference.mli") + ~exit_code:2 "test_inference"; + print_test_expected_output ~cutoff:default_cutoff + ~output:"test_inference.opt.output" + ~extra_dep:(Some "test_inference.mli") + ~extra_flags:"-zero-alloc-check all" + ~exit_code:2 "test_inference"; () diff --git a/tests/backend/zero_alloc_checker/test_inference.ml b/tests/backend/zero_alloc_checker/test_inference.ml new file mode 100644 index 00000000000..1a75ec5d8d3 --- /dev/null +++ b/tests/backend/zero_alloc_checker/test_inference.ml @@ -0,0 +1,84 @@ +(* Both these functions are marked zero_alloc in the mli. We expect them to get + checked, even though they aren't marked zero-alloc here, and should get an + error for the second. *) +let[@inline never] f_zero_alloc x = x + +let[@inline never] f_alloc x = (x, x) + +(* Here, [M_alloc_var.f_alloc2] allocates, and the mli marks it as zero_alloc, + so we'll get an error for it. But we don't get an error for its use in + f_call_var (because the translation to lambda sees the variable on + [M_alloc_var.f_alloc2] has been instantiated to show it will be checked, and + puts an assume on [f_call_var]. This is maybe sad, but mirrors the existing + behavior if [M_alloc_var.f_alloc2] had been explicitly marked zero_alloc. +*) +module M_alloc_var = struct + let[@inline never] f_alloc2 x = (x, x) +end + +let[@zero_alloc] f_call_var x = M_alloc_var.f_alloc2 x + + +(* Arity: The typing tests show that if we just give this function the signature + [val[@zero_alloc] f_arity_one : int -> int -> int] we'll get a type error. + Here we show that if we give it a signature that passes the typechecker (the + mli has [val[@zero_alloc (arity 1)] f_arity_one : int -> int -> int]), it + correctly gets checked and gives a zero_alloc backend error. *) +let f_arity_one x = fun y -> x + y + + +(* Shadowing: the mli marks [f_shadow] zero_alloc. That check should only apply + to the last such function in the file, so we get no error even though there + is an earlier function with the same name and type that allocates. *) +let f_shadow x = (x, x+1) + +let f_shadow _x = (42, 43) (* doesn't allocate because this is static. *) + +(* Shadowing: the other way. This time the function exposed in the signature + does allocate, and we should get an error for it. *) +let f_shadow_alloc _x = (42, 43) + +let f_shadow_alloc x = (x, x) + +(* Shadowing: This time both allocate. We should only get an error the second. *) +let f_shadow_alloc_both x = (x, x) + +let f_shadow_alloc_both x = (x, x+1) + +(* And now the boring part - just a test that we check each function below with + the exact parameters implied by the signature (opt, strict). *) + +(* these are tagged just [@zero_alloc] in the mli *) +exception E of string +let f_basic_success x = + if x = 42 then () else + let s = Printf.sprintf "%d\n" x in + raise (E s) + +let f_basic_fail x = (x, x) + +(* These are tagged [@zero_alloc strict] in the mli *) +let f_strict_success x = x + 1 + +let f_strict_fail x = + if x = 42 then () else + let s = Printf.sprintf "%d\n" x in + raise (E s) + +(* These are tagged [@zero_alloc opt] in the mli - the latter should fail just + when the flag to check opt things is passed. *) +let f_opt_success x = + if x = 42 then () else + let s = Printf.sprintf "%d\n" x in + raise (E s) + +let f_opt_fail x = (x, x) + +(* These are tagged [@zero_alloc struct opt] in the mli - the latter should fail + just when the flag to check for opt is passed. *) +let f_strict_opt_success x = x + +let f_strict_opt_fail x = + if x = 42 then () else + let s = Printf.sprintf "%d\n" x in + raise (E s) diff --git a/tests/backend/zero_alloc_checker/test_inference.mli b/tests/backend/zero_alloc_checker/test_inference.mli new file mode 100644 index 00000000000..ba2359d119e --- /dev/null +++ b/tests/backend/zero_alloc_checker/test_inference.mli @@ -0,0 +1,25 @@ +val[@zero_alloc] f_zero_alloc : 'a -> 'a +val[@zero_alloc] f_alloc : 'a -> 'a * 'a + +module M_alloc_var : sig + val[@zero_alloc] f_alloc2 : 'a -> 'a * 'a +end +val f_call_var : 'a -> 'a * 'a + +val[@zero_alloc (arity 1)] f_arity_one : int -> int -> int + +val[@zero_alloc] f_shadow : int -> int * int +val[@zero_alloc] f_shadow_alloc : int -> int * int +val[@zero_alloc] f_shadow_alloc_both : int -> int * int + +val[@zero_alloc] f_basic_success : int -> unit +val[@zero_alloc] f_basic_fail : 'a -> 'a * 'a + +val[@zero_alloc strict] f_strict_success : int -> int +val[@zero_alloc strict] f_strict_fail : int -> unit + +val[@zero_alloc opt] f_opt_success : int -> unit +val[@zero_alloc opt] f_opt_fail : int -> int * int + +val[@zero_alloc strict opt] f_strict_opt_success : int -> int +val[@zero_alloc strict opt] f_strict_opt_fail : int -> unit diff --git a/tests/backend/zero_alloc_checker/test_inference.opt.output b/tests/backend/zero_alloc_checker/test_inference.opt.output new file mode 100644 index 00000000000..7f637a8be25 --- /dev/null +++ b/tests/backend/zero_alloc_checker/test_inference.opt.output @@ -0,0 +1,65 @@ +File "test_inference.ml", line 6, characters 27-37: +Error: Annotation check for zero_alloc failed on function Test_inference.f_alloc (camlTest_inference.f_alloc_HIDE_STAMP) + +File "test_inference.ml", line 6, characters 31-37: +Error: allocation of 24 bytes + +File "test_inference.ml", line 16, characters 30-40: +Error: Annotation check for zero_alloc failed on function Test_inference.M_alloc_var.f_alloc2 (camlTest_inference.f_alloc2_HIDE_STAMP) + +File "test_inference.ml", line 16, characters 34-40: +Error: allocation of 24 bytes + +File "test_inference.ml", line 27, characters 16-34: +Error: Annotation check for zero_alloc failed on function Test_inference.f_arity_one (camlTest_inference.f_arity_one_HIDE_STAMP) + +File "test_inference.ml", line 27, characters 20-34: +Error: allocation of 32 bytes + +File "test_inference.ml", line 41, characters 19-29: +Error: Annotation check for zero_alloc failed on function Test_inference.f_shadow_alloc (camlTest_inference.f_shadow_alloc_HIDE_STAMP) + +File "test_inference.ml", line 41, characters 23-29: +Error: allocation of 24 bytes + +File "test_inference.ml", line 46, characters 24-36: +Error: Annotation check for zero_alloc failed on function Test_inference.f_shadow_alloc_both (camlTest_inference.f_shadow_alloc_both_HIDE_STAMP) + +File "test_inference.ml", line 46, characters 28-36: +Error: allocation of 24 bytes + +File "test_inference.ml", line 58, characters 17-27: +Error: Annotation check for zero_alloc failed on function Test_inference.f_basic_fail (camlTest_inference.f_basic_fail_HIDE_STAMP) + +File "test_inference.ml", line 58, characters 21-27: +Error: allocation of 24 bytes + +File "test_inference.ml", lines 63-66, characters 18-15: +Error: Annotation check for zero_alloc strict failed on function Test_inference.f_strict_fail (camlTest_inference.f_strict_fail_HIDE_STAMP) + +File "test_inference.ml", line 65, characters 12-35: +Error: called function may allocate on a path to exceptional return (direct call camlCamlinternalFormat.make_printf_HIDE_STAMP) (test_inference.ml:65,12--35;printf.ml:48,18--43;printf.ml:46,2--31) + +File "test_inference.ml", line 65, characters 12-35: +Error: called function may allocate on a path to exceptional return (indirect call) + +File "test_inference.ml", line 66, characters 10-15: +Error: allocation of 24 bytes on a path to exceptional return + +File "test_inference.ml", line 75, characters 15-25: +Error: Annotation check for zero_alloc failed on function Test_inference.f_opt_fail (camlTest_inference.f_opt_fail_HIDE_STAMP) + +File "test_inference.ml", line 75, characters 19-25: +Error: allocation of 24 bytes + +File "test_inference.ml", lines 81-84, characters 22-15: +Error: Annotation check for zero_alloc strict failed on function Test_inference.f_strict_opt_fail (camlTest_inference.f_strict_opt_fail_HIDE_STAMP) + +File "test_inference.ml", line 83, characters 12-35: +Error: called function may allocate on a path to exceptional return (direct call camlCamlinternalFormat.make_printf_HIDE_STAMP) (test_inference.ml:83,12--35;printf.ml:48,18--43;printf.ml:46,2--31) + +File "test_inference.ml", line 83, characters 12-35: +Error: called function may allocate on a path to exceptional return (indirect call) + +File "test_inference.ml", line 84, characters 10-15: +Error: allocation of 24 bytes on a path to exceptional return diff --git a/tests/backend/zero_alloc_checker/test_inference.output b/tests/backend/zero_alloc_checker/test_inference.output new file mode 100644 index 00000000000..e71ceddc8ca --- /dev/null +++ b/tests/backend/zero_alloc_checker/test_inference.output @@ -0,0 +1,47 @@ +File "test_inference.ml", line 6, characters 27-37: +Error: Annotation check for zero_alloc failed on function Test_inference.f_alloc (camlTest_inference.f_alloc_HIDE_STAMP) + +File "test_inference.ml", line 6, characters 31-37: +Error: allocation of 24 bytes + +File "test_inference.ml", line 16, characters 30-40: +Error: Annotation check for zero_alloc failed on function Test_inference.M_alloc_var.f_alloc2 (camlTest_inference.f_alloc2_HIDE_STAMP) + +File "test_inference.ml", line 16, characters 34-40: +Error: allocation of 24 bytes + +File "test_inference.ml", line 27, characters 16-34: +Error: Annotation check for zero_alloc failed on function Test_inference.f_arity_one (camlTest_inference.f_arity_one_HIDE_STAMP) + +File "test_inference.ml", line 27, characters 20-34: +Error: allocation of 32 bytes + +File "test_inference.ml", line 41, characters 19-29: +Error: Annotation check for zero_alloc failed on function Test_inference.f_shadow_alloc (camlTest_inference.f_shadow_alloc_HIDE_STAMP) + +File "test_inference.ml", line 41, characters 23-29: +Error: allocation of 24 bytes + +File "test_inference.ml", line 46, characters 24-36: +Error: Annotation check for zero_alloc failed on function Test_inference.f_shadow_alloc_both (camlTest_inference.f_shadow_alloc_both_HIDE_STAMP) + +File "test_inference.ml", line 46, characters 28-36: +Error: allocation of 24 bytes + +File "test_inference.ml", line 58, characters 17-27: +Error: Annotation check for zero_alloc failed on function Test_inference.f_basic_fail (camlTest_inference.f_basic_fail_HIDE_STAMP) + +File "test_inference.ml", line 58, characters 21-27: +Error: allocation of 24 bytes + +File "test_inference.ml", lines 63-66, characters 18-15: +Error: Annotation check for zero_alloc strict failed on function Test_inference.f_strict_fail (camlTest_inference.f_strict_fail_HIDE_STAMP) + +File "test_inference.ml", line 65, characters 12-35: +Error: called function may allocate on a path to exceptional return (direct call camlCamlinternalFormat.make_printf_HIDE_STAMP) (test_inference.ml:65,12--35;printf.ml:48,18--43;printf.ml:46,2--31) + +File "test_inference.ml", line 65, characters 12-35: +Error: called function may allocate on a path to exceptional return (indirect call) + +File "test_inference.ml", line 66, characters 10-15: +Error: allocation of 24 bytes on a path to exceptional return From a316fdd62d0f3fc93287b2f036cd1e0661e9efa3 Mon Sep 17 00:00:00 2001 From: Chris Casinghino Date: Tue, 2 Jul 2024 21:04:33 -0400 Subject: [PATCH 4/8] nits --- ocaml/testsuite/tests/typing-zero-alloc/cmi_test.ml | 12 ++++++++++-- .../testsuite/tests/typing-zero-alloc/signatures.ml | 2 +- ocaml/typing/typedtree.ml | 4 ++-- ocaml/typing/zero_alloc.ml | 2 +- tests/backend/zero_alloc_checker/test_inference.ml | 12 ++++++++++++ .../zero_alloc_checker/test_inference.opt.output | 6 ++++++ .../backend/zero_alloc_checker/test_inference.output | 6 ++++++ 7 files changed, 38 insertions(+), 6 deletions(-) diff --git a/ocaml/testsuite/tests/typing-zero-alloc/cmi_test.ml b/ocaml/testsuite/tests/typing-zero-alloc/cmi_test.ml index 2bc3006afb9..f1e2a2c6fb9 100644 --- a/ocaml/testsuite/tests/typing-zero-alloc/cmi_test.ml +++ b/ocaml/testsuite/tests/typing-zero-alloc/cmi_test.ml @@ -3,12 +3,13 @@ setup-ocamlc.byte-build-env; module = "cmi_test_lib.ml"; ocamlc.byte; - flags += "-I ocamlc.byte"; + flags += "-I ocamlc.byte ocamlc.byte/cmi_test_lib.cmo"; expect; *) (* Here we show the signatures of [cmi_test_a] and the modules within it do not - have zero_alloc variables - we can't add further zero_alloc constraints. *) + have zero_alloc variables - we can't add further zero_alloc constraints, but + we do get the ones already present in the cmi. *) module M1 : sig val[@zero_alloc] f_unconstrained_variable : int -> int end = Cmi_test_lib @@ -57,6 +58,13 @@ Error: Signature mismatch: module M3 : sig val[@zero_alloc] f : int -> int +end = Cmi_test_lib.M_constrained_variable + [%%expect{| +module M3 : sig val f : int -> int [@@zero_alloc] end +|}] + +module M4 : sig + val[@zero_alloc] f : int -> int end = Cmi_test_lib.M_no_variable [%%expect{| Line 3, characters 6-32: diff --git a/ocaml/testsuite/tests/typing-zero-alloc/signatures.ml b/ocaml/testsuite/tests/typing-zero-alloc/signatures.ml index ce5c7527f65..8847fb85f85 100644 --- a/ocaml/testsuite/tests/typing-zero-alloc/signatures.ml +++ b/ocaml/testsuite/tests/typing-zero-alloc/signatures.ml @@ -1137,7 +1137,7 @@ module M_for_mto = struct let f x = x+1 end -(* The current state of the variales is "no check" *) +(* The current state of the variables is "no check" *) module type S = module type of M_for_mto [%%expect{| module M_for_mto : sig val f : int -> int end diff --git a/ocaml/typing/typedtree.ml b/ocaml/typing/typedtree.ml index 2d62684c33f..c2ac5dc5140 100644 --- a/ocaml/typing/typedtree.ml +++ b/ocaml/typing/typedtree.ml @@ -1087,8 +1087,8 @@ let let_bound_idents_with_modes_sorts_and_checks bindings = | Ignore_assert_all | Check _ | Assume _ -> fn.zero_alloc in Ident.Map.add id zero_alloc checks - (* CR ccasinghino: we could copy the zero-allocness if the vb_expr - is an ident. *) + (* CR ccasinghino: To keep the zero-alloc annotation info aliases, it + may be enough to copy it if the vb_expr is an ident. *) | _ -> checks ) Ident.Map.empty bindings in diff --git a/ocaml/typing/zero_alloc.ml b/ocaml/typing/zero_alloc.ml index bd59bcad37d..58e0c774bd6 100644 --- a/ocaml/typing/zero_alloc.ml +++ b/ocaml/typing/zero_alloc.ml @@ -163,7 +163,7 @@ let sub_exn za1 za2 = The typing of modules (e.g., the [Pmod_structure] case of [Typemod.type_module_aux]) works by (1) computing a naive signature - containing every definition in the module, (2) constructing a simplfied + containing every definition in the module, (2) constructing a simplified signature that, for example, removes shadowed things, and (3) constraining the original signature by the simplfied signature. These signatures _do_ have variables in them, so we allow the special case of diff --git a/tests/backend/zero_alloc_checker/test_inference.ml b/tests/backend/zero_alloc_checker/test_inference.ml index 1a75ec5d8d3..4ded5641cdc 100644 --- a/tests/backend/zero_alloc_checker/test_inference.ml +++ b/tests/backend/zero_alloc_checker/test_inference.ml @@ -82,3 +82,15 @@ let f_strict_opt_fail x = if x = 42 then () else let s = Printf.sprintf "%d\n" x in raise (E s) + +(* Spooky action a distance: the fact that [f] gets checked for zero_alloc is + very non-local to its definition. It would be a nice improvement for the + error to reflect the location of the attribute that, via inference, resulted + in the check. *) +module type S = functor () -> sig val[@zero_alloc] f : 'a -> 'a option end + +module F () = struct + let f x = Some x +end + +module _ : S = F diff --git a/tests/backend/zero_alloc_checker/test_inference.opt.output b/tests/backend/zero_alloc_checker/test_inference.opt.output index 7f637a8be25..f2285a27ee0 100644 --- a/tests/backend/zero_alloc_checker/test_inference.opt.output +++ b/tests/backend/zero_alloc_checker/test_inference.opt.output @@ -63,3 +63,9 @@ Error: called function may allocate on a path to exceptional return (indirect ca File "test_inference.ml", line 84, characters 10-15: Error: allocation of 24 bytes on a path to exceptional return + +File "test_inference.ml", line 93, characters 8-18: +Error: Annotation check for zero_alloc failed on function Test_inference.F.f (camlTest_inference.f_HIDE_STAMP) + +File "test_inference.ml", line 93, characters 12-18: +Error: allocation of 16 bytes diff --git a/tests/backend/zero_alloc_checker/test_inference.output b/tests/backend/zero_alloc_checker/test_inference.output index e71ceddc8ca..da7e9a187c0 100644 --- a/tests/backend/zero_alloc_checker/test_inference.output +++ b/tests/backend/zero_alloc_checker/test_inference.output @@ -45,3 +45,9 @@ Error: called function may allocate on a path to exceptional return (indirect ca File "test_inference.ml", line 66, characters 10-15: Error: allocation of 24 bytes on a path to exceptional return + +File "test_inference.ml", line 93, characters 8-18: +Error: Annotation check for zero_alloc failed on function Test_inference.F.f (camlTest_inference.f_HIDE_STAMP) + +File "test_inference.ml", line 93, characters 12-18: +Error: allocation of 16 bytes From ccd41d34bd07feff3947fbaf2f96af0756789aac Mon Sep 17 00:00:00 2001 From: Chris Casinghino Date: Tue, 2 Jul 2024 21:05:46 -0400 Subject: [PATCH 5/8] create -> create_const --- ocaml/typing/subst.ml | 2 +- ocaml/typing/typecore.ml | 5 +++-- ocaml/typing/typedecl.ml | 2 +- ocaml/typing/typedtree.ml | 9 +++++---- ocaml/typing/typemod.ml | 4 ++-- ocaml/typing/zero_alloc.ml | 2 +- ocaml/typing/zero_alloc.mli | 2 +- 7 files changed, 14 insertions(+), 12 deletions(-) diff --git a/ocaml/typing/subst.ml b/ocaml/typing/subst.ml index fec27310bc1..f1f5be4c3a7 100644 --- a/ocaml/typing/subst.ml +++ b/ocaml/typing/subst.ml @@ -755,7 +755,7 @@ let rec subst_lazy_value_description s descr = more strictly than the signature indicates, which is sound). *) (match s.additional_action with | Prepare_for_saving _ -> - Zero_alloc.create (Zero_alloc.get descr.val_zero_alloc) + Zero_alloc.create_const (Zero_alloc.get descr.val_zero_alloc) | _ -> descr.val_zero_alloc); val_attributes = attrs s descr.val_attributes; val_uid = descr.val_uid; diff --git a/ocaml/typing/typecore.ml b/ocaml/typing/typecore.ml index 271aa58d0f4..52aecc0909a 100644 --- a/ocaml/typing/typecore.ml +++ b/ocaml/typing/typecore.ml @@ -5106,7 +5106,7 @@ let add_zero_alloc_attribute expr attributes = end; (* Here, we may be throwing away a zero_alloc variable. There's no need to set it, because it can't have gotten anywhere else yet. *) - let zero_alloc = Zero_alloc.create za in + let zero_alloc = Zero_alloc.create_const za in let exp_desc = Texp_function { fn with zero_alloc } in { expr with exp_desc } end @@ -8913,7 +8913,8 @@ and type_n_ary_function let zero_alloc = match zero_alloc with | Default_zero_alloc -> Zero_alloc.create_var loc syntactic_arity - | (Check _ | Assume _ | Ignore_assert_all) -> Zero_alloc.create zero_alloc + | (Check _ | Assume _ | Ignore_assert_all) -> + Zero_alloc.create_const zero_alloc in re { exp_desc = diff --git a/ocaml/typing/typedecl.ml b/ocaml/typing/typedecl.ml index 0d3f301f9c6..eee75f92d27 100644 --- a/ocaml/typing/typedecl.ml +++ b/ocaml/typing/typedecl.ml @@ -2920,7 +2920,7 @@ let transl_value_decl env loc valdecl = raise (Error(valdecl.pval_loc, Zero_alloc_attr_non_function)); if za.arity <= 0 then raise (Error(valdecl.pval_loc, Zero_alloc_attr_bad_user_arity)); - Zero_alloc.create zero_alloc + Zero_alloc.create_const zero_alloc | Assume _ | Ignore_assert_all -> raise (Error(valdecl.pval_loc, Zero_alloc_attr_unsupported zero_alloc)) in diff --git a/ocaml/typing/typedtree.ml b/ocaml/typing/typedtree.ml index c2ac5dc5140..2430ebfd90e 100644 --- a/ocaml/typing/typedtree.ml +++ b/ocaml/typing/typedtree.ml @@ -1078,10 +1078,11 @@ let let_bound_idents_with_modes_sorts_and_checks bindings = the check. *) let arity = function_arity fn.params fn.body in if !Clflags.zero_alloc_check_assert_all && arity > 0 then - Zero_alloc.create (Check { strict = false; - arity; - loc = Location.none; - opt = false }) + Zero_alloc.create_const + (Check { strict = false; + arity; + loc = Location.none; + opt = false }) else fn.zero_alloc | Ignore_assert_all | Check _ | Assume _ -> fn.zero_alloc diff --git a/ocaml/typing/typemod.ml b/ocaml/typing/typemod.ml index 835cd818e1d..d1d5ea3e6cd 100644 --- a/ocaml/typing/typemod.ml +++ b/ocaml/typing/typemod.ml @@ -2127,7 +2127,7 @@ let rec remove_modality_and_zero_alloc_variables_sg env ~zap_modality sg = |> zap_modality |> Mode.Modality.Value.of_const in let val_zero_alloc = - Zero_alloc.create (Zero_alloc.get desc.val_zero_alloc) + Zero_alloc.create_const (Zero_alloc.get desc.val_zero_alloc) in let desc = {desc with val_modalities; val_zero_alloc} in Sig_value (id, desc, vis) @@ -2915,7 +2915,7 @@ and type_structure ?(toplevel = None) funct_body anchor env sstr = | Assume { strict; arity; loc; never_returns_normally = _; never_raises = _} -> - Zero_alloc.create (Check { strict; arity; loc; opt = false }) + Zero_alloc.create_const (Check { strict; arity; loc; opt = false }) | Ignore_assert_all -> Zero_alloc.default in let (first_loc, _, _) = List.hd id_info in diff --git a/ocaml/typing/zero_alloc.ml b/ocaml/typing/zero_alloc.ml index 58e0c774bd6..feab0c8bcae 100644 --- a/ocaml/typing/zero_alloc.ml +++ b/ocaml/typing/zero_alloc.ml @@ -36,7 +36,7 @@ let undo_change (d, v) = v.desc <- d let log_change = ref (fun _ -> ()) let set_change_log f = log_change := f -let create x = Const x +let create_const x = Const x let create_var loc arity = Var { loc; arity; desc = None } let default = Const Default_zero_alloc diff --git a/ocaml/typing/zero_alloc.mli b/ocaml/typing/zero_alloc.mli index c1f390f300a..2933c250f40 100644 --- a/ocaml/typing/zero_alloc.mli +++ b/ocaml/typing/zero_alloc.mli @@ -23,7 +23,7 @@ type t done. *) val default : t -val create : const -> t +val create_const : const -> t (* [create_var loc n] creates a variable. [loc] is the location of the function you are creating a variable for, and [n] is its syntactic arity of the From d1035bed4f50ca698774b2a2edfde73af0f0111e Mon Sep 17 00:00:00 2001 From: Chris Casinghino Date: Wed, 3 Jul 2024 08:48:14 -0400 Subject: [PATCH 6/8] confine exception to zero_alloc --- ocaml/typing/includecore.ml | 5 +++-- ocaml/typing/zero_alloc.ml | 7 +++++++ ocaml/typing/zero_alloc.mli | 9 ++++----- 3 files changed, 14 insertions(+), 7 deletions(-) diff --git a/ocaml/typing/includecore.ml b/ocaml/typing/includecore.ml index f70bdbfce56..468f32c28fb 100644 --- a/ocaml/typing/includecore.ml +++ b/ocaml/typing/includecore.ml @@ -98,8 +98,9 @@ let value_descriptions ~loc env name loc vd1.val_attributes vd2.val_attributes name; - begin try Zero_alloc.sub_exn vd1.val_zero_alloc vd2.val_zero_alloc with - | Zero_alloc.Error e -> raise (Dont_match (Zero_alloc e)) + begin match Zero_alloc.sub vd1.val_zero_alloc vd2.val_zero_alloc with + | Ok () -> () + | Error e -> raise (Dont_match (Zero_alloc e)) end; begin match Mode.Modality.Value.sub vd1.val_modalities vd2.val_modalities with | Ok () -> () diff --git a/ocaml/typing/zero_alloc.ml b/ocaml/typing/zero_alloc.ml index feab0c8bcae..b2f90b3b948 100644 --- a/ocaml/typing/zero_alloc.ml +++ b/ocaml/typing/zero_alloc.ml @@ -177,3 +177,10 @@ let sub_exn za1 za2 = | _, (Const Default_zero_alloc) -> () | Var v, Const c -> sub_var_const_exn v c | Const c1, Const c2 -> sub_const_const_exn c1 c2 + +let sub za1 za2 = + try + sub_exn za1 za2; + Ok () + with + | Error e -> Result.Error e diff --git a/ocaml/typing/zero_alloc.mli b/ocaml/typing/zero_alloc.mli index 2933c250f40..e87b535eb8c 100644 --- a/ocaml/typing/zero_alloc.mli +++ b/ocaml/typing/zero_alloc.mli @@ -41,10 +41,9 @@ val undo_change : change -> unit (* These are the errors that may be raised by [sub_exn] below. *) type error -exception Error of error val print_error : Format.formatter -> error -> unit -(* [sub_exn t1 t2] checks whether the zero_alloc check t1 is stronger than the - zero_alloc check t2. If not, it raises [Error]. If [t1] is a variable, it may - be set to make the relation hold. *) -val sub_exn : t -> t -> unit +(* [sub t1 t2] checks whether the zero_alloc check t1 is stronger than the + zero_alloc check t2. It returns [Ok ()] if so, and [Error e] if not. If [t1] + is a variable, it may be set to make the relation hold. *) +val sub : t -> t -> (unit, error) Result.t From 642c069cd52551c50bbed933dfd615e12e899921 Mon Sep 17 00:00:00 2001 From: Chris Casinghino Date: Wed, 3 Jul 2024 10:55:48 -0400 Subject: [PATCH 7/8] Make texp_apply's zero_alloc info clearer --- ocaml/lambda/translcore.ml | 73 +++++++++++++++------------- ocaml/parsing/builtin_attributes.ml | 43 ++++++++-------- ocaml/parsing/builtin_attributes.mli | 58 ++++++++++++---------- ocaml/typing/printtyped.ml | 10 ++-- ocaml/typing/typecore.ml | 4 +- ocaml/typing/typedtree.ml | 2 +- ocaml/typing/typedtree.mli | 8 ++- ocaml/typing/zero_alloc.ml | 29 ++++++----- ocaml/typing/zero_alloc.mli | 28 ++++++----- 9 files changed, 139 insertions(+), 116 deletions(-) diff --git a/ocaml/lambda/translcore.ml b/ocaml/lambda/translcore.ml index 2b996880a3b..6017079fb5e 100644 --- a/ocaml/lambda/translcore.ml +++ b/ocaml/lambda/translcore.ml @@ -351,41 +351,36 @@ let can_apply_primitive p pmode pos args = end let zero_alloc_of_application - ~num_args (annotation : Builtin_attributes.zero_alloc_attribute) funct = - let zero_alloc = - match annotation, funct.exp_desc with - | Assume _, _ -> - (* The user wrote a zero_alloc attribute on the application - keep it. *) - annotation - | (Ignore_assert_all | Check _), _ -> - (* These are rejected in typecore *) - Misc.fatal_error "Translcore.zero_alloc_of_application: illegal attr" - | Default_zero_alloc, Texp_ident (_, _, { val_zero_alloc; _ }, _, _) -> - (* We assume the call is zero_alloc if the function is known to be - zero_alloc. If the function is zero_alloc opt, then we need to be sure - that the opt checks were run to license this assumption. We judge - whether the opt checks were run based on the argument to the - [-zero-alloc-check] command line flag. *) - let use_opt = - match !Clflags.zero_alloc_check with - | Check_default | No_check -> false - | Check_all | Check_opt_only -> true - in - begin match Zero_alloc.get val_zero_alloc with - | Check c when c.arity = num_args && (use_opt || not c.opt) -> - Builtin_attributes.Assume { - strict = c.strict; + ~num_args (annotation : Zero_alloc.assume option) funct = + match annotation, funct.exp_desc with + | Some assume, _ -> + (* The user wrote a zero_alloc attribute on the application - keep it. *) + Builtin_attributes.assume_zero_alloc assume + | None, Texp_ident (_, _, { val_zero_alloc; _ }, _, _) -> + (* We assume the call is zero_alloc if the function is known to be + zero_alloc. If the function is zero_alloc opt, then we need to be sure + that the opt checks were run to license this assumption. We judge + whether the opt checks were run based on the argument to the + [-zero-alloc-check] command line flag. *) + let use_opt = + match !Clflags.zero_alloc_check with + | Check_default | No_check -> false + | Check_all | Check_opt_only -> true + in + begin match Zero_alloc.get val_zero_alloc with + | Check c when c.arity = num_args && (use_opt || not c.opt) -> + let assume : Zero_alloc.assume = + { strict = c.strict; never_returns_normally = false; never_raises = false; arity = c.arity; - loc = c.loc - } - | Check _ | Default_zero_alloc | Ignore_assert_all | Assume _ -> - Builtin_attributes.Default_zero_alloc - end - | Default_zero_alloc, _ -> Builtin_attributes.Default_zero_alloc - in - Builtin_attributes.assume_zero_alloc zero_alloc + loc = c.loc } + in + Builtin_attributes.assume_zero_alloc assume + | Check _ | Default_zero_alloc | Ignore_assert_all | Assume _ -> + Zero_alloc_utils.Assume_info.none + end + | None, _ -> Zero_alloc_utils.Assume_info.none let rec transl_exp ~scopes sort e = transl_exp1 ~scopes ~in_new_scope:false sort e @@ -446,7 +441,11 @@ and transl_exp0 ~in_new_scope ~scopes sort e = if extra_args = [] then transl_apply_position pos else Rc_normal in - let assume_zero_alloc = Builtin_attributes.assume_zero_alloc zero_alloc in + let assume_zero_alloc = + match zero_alloc with + | None -> Zero_alloc_utils.Assume_info.none + | Some assume -> Builtin_attributes.assume_zero_alloc assume + in let lam = let loc = map_scopes (update_assume_zero_alloc ~assume_zero_alloc) @@ -1621,7 +1620,13 @@ and transl_function ~in_new_scope ~scopes e params body let attrs = e.exp_attributes in let mode = transl_alloc_mode_r alloc_mode in let zero_alloc = Zero_alloc.get zero_alloc in - let assume_zero_alloc = Builtin_attributes.assume_zero_alloc zero_alloc in + let assume_zero_alloc = + match zero_alloc with + | Default_zero_alloc | Check _ | Ignore_assert_all -> + Zero_alloc_utils.Assume_info.none + | Assume assume -> + Builtin_attributes.assume_zero_alloc assume + in let scopes = if in_new_scope then update_assume_zero_alloc ~scopes ~assume_zero_alloc diff --git a/ocaml/parsing/builtin_attributes.ml b/ocaml/parsing/builtin_attributes.ml index 9eb34a194ee..e5b3aea43eb 100644 --- a/ocaml/parsing/builtin_attributes.ml +++ b/ocaml/parsing/builtin_attributes.ml @@ -681,20 +681,26 @@ let error_message_attr l = | _ -> None in List.find_map inner l +type zero_alloc_check = + { strict: bool; + opt: bool; + arity: int; + loc: Location.t; + } + +type zero_alloc_assume = + { strict: bool; + never_returns_normally: bool; + never_raises: bool; + arity: int; + loc: Location.t; + } + type zero_alloc_attribute = | Default_zero_alloc | Ignore_assert_all - | Check of { strict: bool; - opt: bool; - arity: int; - loc: Location.t; - } - | Assume of { strict: bool; - never_returns_normally: bool; - never_raises: bool; - arity: int; - loc: Location.t; - } + | Check of zero_alloc_check + | Assume of zero_alloc_assume let is_zero_alloc_check_enabled ~opt = match !Clflags.zero_alloc_check with @@ -923,9 +929,10 @@ let get_zero_alloc_attribute ~in_signature ~default_arity l = register_zero_alloc_attribute attr.attr_name); res -let zero_alloc_attribute_may_not_be_check za = +let zero_alloc_attribute_only_assume_allowed za = match za with - | Default_zero_alloc | Ignore_assert_all | Assume _ -> za + | Assume assume -> Some assume + | Default_zero_alloc | Ignore_assert_all -> None | Check { loc; _ } -> let name = "zero_alloc" in let msg = "Only the following combinations are supported in this context: \ @@ -936,13 +943,11 @@ let zero_alloc_attribute_may_not_be_check za = `zero_alloc assume never_returns_normally strict`." in Location.prerr_warning loc (Warnings.Attribute_payload (name, msg)); - Default_zero_alloc + None -let assume_zero_alloc check : Zero_alloc_utils.Assume_info.t = - match check with - | Default_zero_alloc | Ignore_assert_all | Check _ -> - Zero_alloc_utils.Assume_info.none - | Assume { strict; never_returns_normally; never_raises; } -> +let assume_zero_alloc assume : Zero_alloc_utils.Assume_info.t = + match assume with + | { strict; never_returns_normally; never_raises; } -> Zero_alloc_utils.Assume_info.create ~strict ~never_returns_normally ~never_raises type tracing_probe = diff --git a/ocaml/parsing/builtin_attributes.mli b/ocaml/parsing/builtin_attributes.mli index 1f04b36e082..34e13ae4f9a 100644 --- a/ocaml/parsing/builtin_attributes.mli +++ b/ocaml/parsing/builtin_attributes.mli @@ -237,30 +237,36 @@ val parse_optional_id_payload : string -> Location.t -> empty:'a -> (string * 'a) list -> Parsetree.payload -> ('a,unit) Result.t -(* Support for property attributes like zero_alloc *) +(* Support for zero_alloc *) +type zero_alloc_check = + { strict: bool; + (* [strict=true] property holds on all paths. + [strict=false] if the function returns normally, + then the property holds (but property violations on + exceptional returns or diverging loops are ignored). + This definition may not be applicable to new properties. *) + opt: bool; + arity: int; + loc: Location.t; + } + +type zero_alloc_assume = + { strict: bool; + never_returns_normally: bool; + never_raises: bool; + (* [never_raises=true] the function never returns + via an exception. The function (directly or transitively) + may raise exceptions that do not escape, i.e., + handled before the function returns. *) + arity: int; + loc: Location.t; + } + type zero_alloc_attribute = | Default_zero_alloc | Ignore_assert_all - | Check of { strict: bool; - (* [strict=true] property holds on all paths. - [strict=false] if the function returns normally, - then the property holds (but property violations on - exceptional returns or diverging loops are ignored). - This definition may not be applicable to new properties. *) - opt: bool; - arity: int; - loc: Location.t; - } - | Assume of { strict: bool; - never_returns_normally: bool; - never_raises: bool; - (* [never_raises=true] the function never returns - via an exception. The function (directly or transitively) - may raise exceptions that do not escape, i.e., - handled before the function returns. *) - arity: int; - loc: Location.t; - } + | Check of zero_alloc_check + | Assume of zero_alloc_assume val is_zero_alloc_check_enabled : opt:bool -> bool @@ -271,12 +277,12 @@ val get_zero_alloc_attribute : in_signature:bool -> default_arity:int -> Parsetree.attributes -> zero_alloc_attribute -(* If the input attribute is [Check], this issues a warning and returns - [Default_zero_alloc]. Otherwise, it is the identity. *) -val zero_alloc_attribute_may_not_be_check : - zero_alloc_attribute -> zero_alloc_attribute +(* This returns the [zero_alloc_assume] if the input is an assume. Otherwise, + it returns None. If the input attribute is [Check], this issues a warning. *) +val zero_alloc_attribute_only_assume_allowed : + zero_alloc_attribute -> zero_alloc_assume option -val assume_zero_alloc : zero_alloc_attribute -> Zero_alloc_utils.Assume_info.t +val assume_zero_alloc : zero_alloc_assume -> Zero_alloc_utils.Assume_info.t type tracing_probe = { name : string; diff --git a/ocaml/typing/printtyped.ml b/ocaml/typing/printtyped.ml index 186a8e8a377..69cc212cdef 100644 --- a/ocaml/typing/printtyped.ml +++ b/ocaml/typing/printtyped.ml @@ -224,17 +224,13 @@ let attributes i ppf l = let jkind_annotation i ppf (jkind, _) = line i ppf "%a" Jkind.Const.format jkind -let application_zero_alloc i ppf (za : Builtin_attributes.zero_alloc_attribute) = - match za with - | Default_zero_alloc -> () - | Assume { strict; never_returns_normally; never_raises; arity; loc = _ } -> +let zero_alloc_assume i ppf : Zero_alloc.assume -> unit = function + { strict; never_returns_normally; never_raises; arity; loc = _ } -> line i ppf "assume_zero_alloc arity=%d%s%s%s\n" arity (if strict then " strict" else "") (if never_returns_normally then " never_returns_normally" else "") (if never_raises then " never_raises" else "") - | Ignore_assert_all | Check _ -> - Misc.fatal_error "printtyped: application_zero_alloc" let rec core_type i ppf x = line i ppf "core_type %a\n" fmt_location x.ctyp_loc; @@ -464,7 +460,7 @@ and expression i ppf x = | Nontail -> "Nontail" | Default -> "Default"); locality_mode i ppf am; - application_zero_alloc i ppf za; + Option.iter (zero_alloc_assume i ppf) za; expression i ppf e; list i label_x_apply_arg ppf l; | Texp_match (e, sort, l, _partial) -> diff --git a/ocaml/typing/typecore.ml b/ocaml/typing/typecore.ml index 52aecc0909a..d8f4254dbb5 100644 --- a/ocaml/typing/typecore.ml +++ b/ocaml/typing/typecore.ml @@ -5443,7 +5443,7 @@ and type_expect_ let zero_alloc = Builtin_attributes.get_zero_alloc_attribute ~in_signature:false ~default_arity:(List.length args) sfunct.pexp_attributes - |> Builtin_attributes.zero_alloc_attribute_may_not_be_check + |> Builtin_attributes.zero_alloc_attribute_only_assume_allowed in rue { @@ -7486,7 +7486,7 @@ and type_argument ?explanation ?recarg env (mode : expected_mode) sarg |> Value.proj (Comonadic Areality) |> regional_to_global |> Locality.disallow_right, - Builtin_attributes.Default_zero_alloc)} + None)} in let cases = [ case eta_pat e ] in let cases_loc = { texp.exp_loc with loc_ghost = true } in diff --git a/ocaml/typing/typedtree.ml b/ocaml/typing/typedtree.ml index 2430ebfd90e..9810efdf1e3 100644 --- a/ocaml/typing/typedtree.ml +++ b/ocaml/typing/typedtree.ml @@ -150,7 +150,7 @@ and expression_desc = } | Texp_apply of expression * (arg_label * apply_arg) list * apply_position * - Mode.Locality.l * Builtin_attributes.zero_alloc_attribute + Mode.Locality.l * Zero_alloc.assume option | Texp_match of expression * Jkind.sort * computation case list * partial | Texp_try of expression * value case list | Texp_tuple of (string option * expression) list * Mode.Alloc.r diff --git a/ocaml/typing/typedtree.mli b/ocaml/typing/typedtree.mli index c729e2f625d..5f2fe4ef1f1 100644 --- a/ocaml/typing/typedtree.mli +++ b/ocaml/typing/typedtree.mli @@ -280,7 +280,7 @@ and expression_desc = *) | Texp_apply of expression * (arg_label * apply_arg) list * apply_position * - Mode.Locality.l * Builtin_attributes.zero_alloc_attribute + Mode.Locality.l * Zero_alloc.assume option (** E0 ~l1:E1 ... ~ln:En The expression can be Omitted if the expression is abstracted over @@ -296,10 +296,8 @@ and expression_desc = (Labelled "y", Some (Texp_constant Const_int 3)) ]) - The [zero_alloc_attribute] records the optional [@zero_alloc assume] - attribute that may appear on applications. Invariant: it is either - [Default_zero_alloc] (if the user wrote no attribute) or [Assume] - (if they did). *) + The [Zero_alloc.assume option] records the optional [@zero_alloc + assume] attribute that may appear on applications. *) | Texp_match of expression * Jkind.sort * computation case list * partial (** match E0 with | P1 -> E1 diff --git a/ocaml/typing/zero_alloc.ml b/ocaml/typing/zero_alloc.ml index b2f90b3b948..7b559f696aa 100644 --- a/ocaml/typing/zero_alloc.ml +++ b/ocaml/typing/zero_alloc.ml @@ -1,19 +1,26 @@ module ZA = Zero_alloc_utils +(* Support for zero_alloc *) +type check = Builtin_attributes.zero_alloc_check = + { strict: bool; + opt: bool; + arity: int; + loc: Location.t; + } + +type assume = Builtin_attributes.zero_alloc_assume = + { strict: bool; + never_returns_normally: bool; + never_raises: bool; + arity: int; + loc: Location.t; + } + type const = Builtin_attributes.zero_alloc_attribute = | Default_zero_alloc | Ignore_assert_all - | Check of { strict: bool; - opt: bool; - arity: int; - loc: Location.t; - } - | Assume of { strict: bool; - never_returns_normally: bool; - never_raises: bool; - arity: int; - loc: Location.t; - } + | Check of check + | Assume of assume type desc = { strict : bool; opt : bool } diff --git a/ocaml/typing/zero_alloc.mli b/ocaml/typing/zero_alloc.mli index e87b535eb8c..cdbe220ec4d 100644 --- a/ocaml/typing/zero_alloc.mli +++ b/ocaml/typing/zero_alloc.mli @@ -1,17 +1,23 @@ +type check = Builtin_attributes.zero_alloc_check = + { strict: bool; + opt: bool; + arity: int; + loc: Location.t; + } + +type assume = Builtin_attributes.zero_alloc_assume = + { strict: bool; + never_returns_normally: bool; + never_raises: bool; + arity: int; + loc: Location.t; + } + type const = Builtin_attributes.zero_alloc_attribute = | Default_zero_alloc | Ignore_assert_all - | Check of { strict: bool; - opt: bool; - arity: int; - loc: Location.t; - } - | Assume of { strict: bool; - never_returns_normally: bool; - never_raises: bool; - arity: int; - loc: Location.t; - } + | Check of check + | Assume of assume (* This type represents whether or not a function will be checked for zero-alloc-ness, and with what configuration (strict, opt, etc). It can be a From f08213d7486ac367e194cfc545a025bae6ffab92 Mon Sep 17 00:00:00 2001 From: Chris Casinghino Date: Wed, 3 Jul 2024 11:18:48 -0400 Subject: [PATCH 8/8] chamelon --- chamelon/compat.jst.ml | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) diff --git a/chamelon/compat.jst.ml b/chamelon/compat.jst.ml index d1f5b959456..621b9649f6c 100644 --- a/chamelon/compat.jst.ml +++ b/chamelon/compat.jst.ml @@ -19,13 +19,11 @@ let mkTexp_ident ?id:(ident_kind, uu = (Id_value, shared_many_use)) type nonrec apply_arg = apply_arg type texp_apply_identifier = - apply_position * Locality.l * Builtin_attributes.zero_alloc_attribute + apply_position * Locality.l * Builtin_attributes.zero_alloc_assume option let mkTexp_apply ?id:(pos, mode, za = - ( Default, - Locality.disallow_right Locality.legacy, - Builtin_attributes.Default_zero_alloc )) (exp, args) = + (Default, Locality.disallow_right Locality.legacy, None)) (exp, args) = let args = List.map (fun (label, x) -> (Typetexp.transl_label label None, x)) args in