Implement inference and add tests

Author: ccasin

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)

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

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,18 +371,19 @@ 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;
           never_raises = false;
           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

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
+|}]

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