diff --git a/chamelon/compat.jst.ml b/chamelon/compat.jst.ml index 919596f2bbe..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 * Zero_alloc_utils.Assume_info.t + apply_position * Locality.l * Builtin_attributes.zero_alloc_assume option let mkTexp_apply ?id:(pos, mode, za = - ( Default, - Locality.disallow_right Locality.legacy, - Zero_alloc_utils.Assume_info.none )) (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 @@ -92,7 +90,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 +117,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 +401,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/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/lambda/translcore.ml b/ocaml/lambda/translcore.ml index 4ae6f9e9c54..6017079fb5e 100644 --- a/ocaml/lambda/translcore.ml +++ b/ocaml/lambda/translcore.ml @@ -350,6 +350,38 @@ let can_apply_primitive p pmode pos args = end end +let zero_alloc_of_application + ~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 } + 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 @@ -387,7 +419,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 +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 = + 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) @@ -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,8 +1619,13 @@ 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 ~is_check_allowed:true 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 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/parsing/builtin_attributes.ml b/ocaml/parsing/builtin_attributes.ml index 2b74f27471f..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,25 +929,26 @@ 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 = - match check with - | Default_zero_alloc -> Zero_alloc_utils.Assume_info.none - | Ignore_assert_all -> 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 +let zero_alloc_attribute_only_assume_allowed za = + match za with + | Assume assume -> Some assume + | Default_zero_alloc | Ignore_assert_all -> None | 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 + 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)); + None + +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 = { name : string; diff --git a/ocaml/parsing/builtin_attributes.mli b/ocaml/parsing/builtin_attributes.mli index d84e09b5af3..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,8 +277,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 +(* 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_assume -> Zero_alloc_utils.Assume_info.t type tracing_probe = { name : string; 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..f1e2a2c6fb9 --- /dev/null +++ b/ocaml/testsuite/tests/typing-zero-alloc/cmi_test.ml @@ -0,0 +1,85 @@ +(* TEST + readonly_files = "cmi_test_lib.ml"; + setup-ocamlc.byte-build-env; + module = "cmi_test_lib.ml"; + 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, 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 +[%%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_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: +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..8847fb85f85 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 variables 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/includecore.ml b/ocaml/typing/includecore.ml index c38c31387ee..468f32c28fb 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,10 @@ 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 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 () -> () | Error e -> raise (Dont_match (Modality e)) @@ -386,16 +320,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/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/printtyped.ml b/ocaml/typing/printtyped.ml index 21ee0e68083..69cc212cdef 100644 --- a/ocaml/typing/printtyped.ml +++ b/ocaml/typing/printtyped.ml @@ -224,6 +224,14 @@ let attributes i ppf l = let jkind_annotation i ppf (jkind, _) = line i ppf "%a" Jkind.Const.format jkind +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 "") + 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 +460,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; + 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/subst.ml b/ocaml/typing/subst.ml index 1892c1122f8..f1f5be4c3a7 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_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/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 1d806743da5..d8f4254dbb5 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,56 +5097,21 @@ 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_const za in + let exp_desc = Texp_function { fn with zero_alloc } in { expr with exp_desc } 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 +5440,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_only_assume_allowed 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; @@ -7474,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 ()); @@ -7520,7 +7486,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)} + None)} in let cases = [ case eta_pat e ] in let cases_loc = { texp.exp_loc with loc_ghost = true } in @@ -7540,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 @@ -8551,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; @@ -8944,6 +8910,12 @@ 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_const zero_alloc + in re { exp_desc = Texp_function diff --git a/ocaml/typing/typedecl.ml b/ocaml/typing/typedecl.ml index 3976c11e7ef..eee75f92d27 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_const 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 e621d5ba9f0..9810efdf1e3 100644 --- a/ocaml/typing/typedtree.ml +++ b/ocaml/typing/typedtree.ml @@ -146,11 +146,11 @@ 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 * - Mode.Locality.l * Zero_alloc_utils.Assume_info.t + 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 @@ -1068,32 +1068,35 @@ 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_const + (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: 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 List.rev_map (fun (id, _, _, _) -> let zero_alloc = - Option.value (Ident.Map.find_opt id checks) - ~default:Builtin_attributes.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/typedtree.mli b/ocaml/typing/typedtree.mli index 6d9d8f4baf3..5f2fe4ef1f1 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 _) @@ -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 * 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_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.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 @@ -1157,7 +1155,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/typemod.ml b/ocaml/typing/typemod.ml index 27524c79ac4..d1d5ea3e6cd 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_const (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_const (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 c550cdd6465..d718708406c 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; } @@ -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/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..7b559f696aa --- /dev/null +++ b/ocaml/typing/zero_alloc.ml @@ -0,0 +1,193 @@ +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 check + | Assume of assume + +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_const 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 + +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_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. + + 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_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 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 + 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 + +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 new file mode 100644 index 00000000000..cdbe220ec4d --- /dev/null +++ b/ocaml/typing/zero_alloc.mli @@ -0,0 +1,55 @@ +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 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 + 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 + +(* [default] corresponds to [Default_zero_alloc], meaning no check will be + done. *) +val default : 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 + 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 +val print_error : Format.formatter -> error -> 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 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..4ded5641cdc --- /dev/null +++ b/tests/backend/zero_alloc_checker/test_inference.ml @@ -0,0 +1,96 @@ +(* 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) + +(* 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.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..f2285a27ee0 --- /dev/null +++ b/tests/backend/zero_alloc_checker/test_inference.opt.output @@ -0,0 +1,71 @@ +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 + +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 new file mode 100644 index 00000000000..da7e9a187c0 --- /dev/null +++ b/tests/backend/zero_alloc_checker/test_inference.output @@ -0,0 +1,53 @@ +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 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