zero alloc: warning 198 about assume

ocaml/lambda/translattribute.ml

@@ -297,24 +297,45 @@ let get_local_attribute l =
   let attr = find_attribute is_local_attribute l in
   parse_local_attribute attr
 
-let get_property_attribute l p =
+let get_property_attribute l p ~fun_attr =
   let attr = find_attribute (is_property_attribute p) l in
   let res = parse_property_attribute attr p in
   (match attr, res with
    | None, Default_check -> ()
    | _, Default_check -> ()
    | None, (Check _ | Ignore_assert_all _ ) -> assert false
    | Some _, Ignore_assert_all _ -> ()
-   | Some attr, Check _ ->
+   | Some attr, Check { assume; _ } ->
      if !Clflags.zero_alloc_check && !Clflags.native_code then
        (* The warning for unchecked functions will not trigger if the check is requested
           through the [@@@zero_alloc all] top-level annotation rather than through the
           function annotation [@zero_alloc]. *)
-       Builtin_attributes.register_property attr.attr_name);
+       if assume then begin
+         (* [attr.inline] and [attr.specialise] must be set before the
+            check for [Warnings.Misplaced_assume_attribute].
+            For attributes from the same list, it's fine because
+            [add_check_attribute] is called after
+            [add_inline_attribute] and [add_specialise_attribute].
+            The warning will spuriously fire in the following case:
+            let[@inline never][@specialise never] f =
+              fun[@zero_alloc assume] x -> ..
+         *)
+         let never_specialise =
+           if Config.flambda then
+              fun_attr.specialise = Never_specialise
+           else
+              (* closure drops [@specialise never] and never specialises *)
+              (* flambda2 does not have specialisation support yet *)
+              true
+         in
+         if not ((fun_attr.inline = Never_inline) && never_specialise) then
+          Location.prerr_warning attr.attr_name.loc
+            (Warnings.Misplaced_assume_attribute attr.attr_name.txt)
+       end
+       else
+         Builtin_attributes.register_property attr.attr_name);
    res
 
-let get_check_attribute l = get_property_attribute l Zero_alloc
-
 let get_poll_attribute l =
   let attr = find_attribute is_poll_attribute l in
   parse_poll_attribute attr
@@ -425,7 +446,7 @@ let add_check_attribute expr loc attributes =
   in
   match expr with
   | Lfunction({ attr = { stub = false } as attr; } as funct) ->
-    begin match get_check_attribute attributes with
+    begin match get_property_attribute attributes Zero_alloc ~fun_attr:attr with
     | Default_check -> expr
     | (Ignore_assert_all p | Check { property = p; _ }) as check ->
       begin match attr.check with

ocaml/utils/warnings.ml

@@ -108,6 +108,7 @@ type t =
   | Unused_tmc_attribute                    (* 71 *)
   | Tmc_breaks_tailcall                     (* 72 *)
   | Probe_name_too_long of string           (* 190 *)
+  | Misplaced_assume_attribute of string    (* 198 *)
   | Unchecked_property_attribute of string  (* 199 *)
 ;;
 
@@ -192,6 +193,7 @@ let number = function
   | Unused_tmc_attribute -> 71
   | Tmc_breaks_tailcall -> 72
   | Probe_name_too_long _ -> 190
+  | Misplaced_assume_attribute _  -> 198
   | Unchecked_property_attribute _ -> 199
 ;;
 
@@ -453,6 +455,10 @@ let descriptions = [
   { number = 190;
     names = ["probe-name-too-long"];
     description = "Probe name must be at most 100 characters long." };
+  { number = 198;
+    names = ["misplaced-assume-attribute"];
+    description = "Assume of a property is ignored \
+                   if the function is inlined or specialised." };
   { number = 199;
     names = ["unchecked-property-attribute"];
     description = "A property of a function that was \
@@ -1060,6 +1066,12 @@ let message = function
       Printf.sprintf
         "This probe name is too long: `%s'. \
          Probe names must be at most 100 characters long." name
+  | Misplaced_assume_attribute property ->
+      Printf.sprintf
+        "the \"%s assume\" attribute will be ignored by the check \
+         when the function is inlined or specialised.\n\
+         Mark this function as [@inline never][@specialise never]."
+      property
   | Unchecked_property_attribute property ->
       Printf.sprintf "the %S attribute cannot be checked.\n\
       The function it is attached to was optimized away. \n\

ocaml/utils/warnings.mli

@@ -111,6 +111,7 @@ type t =
   | Tmc_breaks_tailcall                     (* 72 *)
 (* Flambda_backend specific warnings: numbers should go down from 199 *)
   | Probe_name_too_long of string           (* 190 *)
+  | Misplaced_assume_attribute of string    (* 198 *)
   | Unchecked_property_attribute of string  (* 199 *)
 ;;
 

tests/backend/checkmach/dune.inc

@@ -471,3 +471,41 @@
  (enabled_if (and (= %{context_name} "main") %{ocaml-config:flambda}))
  (deps t1.ml)
  (action (run %{bin:ocamlopt.opt} %{deps} -g -c -zero-alloc-check -dcse -dcheckmach -dump-into-file -O3)))
+
+(rule
+ (enabled_if (= %{context_name} "main"))
+ (targets test_warning198.output.corrected)
+ (deps (:ml test_warning198.ml) filter.sh)
+ (action
+   (with-outputs-to test_warning198.output.corrected
+    (pipe-outputs
+    (with-accepted-exit-codes 0
+     (run %{bin:ocamlopt.opt} %{ml} -g -color never -error-style short -c
+          -zero-alloc-check -checkmach-details-cutoff 20 -O3))
+    (run "./filter.sh")
+   ))))
+
+(rule
+ (alias   runtest)
+ (enabled_if (= %{context_name} "main"))
+ (deps test_warning198.output test_warning198.output.corrected)
+ (action (diff test_warning198.output test_warning198.output.corrected)))
+
+(rule
+ (enabled_if (and (= %{context_name} "main") %{ocaml-config:flambda}))
+ (targets test_warning199.output.corrected)
+ (deps (:ml test_warning199.mli test_warning199.ml) filter.sh)
+ (action
+   (with-outputs-to test_warning199.output.corrected
+    (pipe-outputs
+    (with-accepted-exit-codes 0
+     (run %{bin:ocamlopt.opt} %{ml} -g -color never -error-style short -c
+          -zero-alloc-check -checkmach-details-cutoff 20 -O3))
+    (run "./filter.sh")
+   ))))
+
+(rule
+ (alias   runtest)
+ (enabled_if (and (= %{context_name} "main") %{ocaml-config:flambda}))
+ (deps test_warning199.output test_warning199.output.corrected)
+ (action (diff test_warning199.output test_warning199.output.corrected)))

tests/backend/checkmach/gen/gen_dune.ml

@@ -114,3 +114,7 @@ let () =
   (* flambda2 generates an indirect call but we don't yet have a way to exclude it
      without excluding closure. *)
   print_test ~flambda_only:true ~deps:"t1.ml";
+  print_test_expected_output ~cutoff:default_cutoff ~flambda_only:false ~extra_dep:None ~exit_code:0
+    "test_warning198";
+  (* closure does not delete dead functions *)
+  print_test_expected_output ~cutoff:default_cutoff ~flambda_only:true ~extra_dep:(Some "test_warning199.mli") ~exit_code:0 "test_warning199";

tests/backend/checkmach/t5.ml

@@ -1,9 +1,9 @@
-let[@zero_alloc strict assume][@inline never] test x = [x;x+1]
+let[@zero_alloc strict assume][@inline never][@specialise never] test x = [x;x+1]
 (* The test below to make sure "noalloc" on external is still handled correctly. *)
 external external_test_noalloc : unit -> unit = "test" [@@noalloc]
 external external_test : unit -> unit = "test"
 
-let[@zero_alloc assume][@inline never] test4 x =
+let[@zero_alloc assume][@inline never][@specialise never] test4 x =
   if x > (-100)
   then x
   else raise (Failure ("don't be so negative, "^(string_of_int x)))

tests/backend/checkmach/t6.ml

@@ -12,16 +12,16 @@ let[@zero_alloc strict] pass3 x y = x + y
 let[@zero_alloc ignore] test1 x = (x, x)
 
 (* assume still works *)
-let[@zero_alloc assume][@inline never] fail_loud x = [ x; x+1 ]
+let[@zero_alloc assume][@inline never][@specialise never] fail_loud x = [ x; x+1 ]
 
 let call_loud x = fail_loud (x*2)
 
 (* assume strict still works *)
-let[@inline never][@zero_alloc strict assume] fail_loud2 x = raise (Exn (x,x))
+let[@inline never][@specialise never][@zero_alloc strict assume] fail_loud2 x = raise (Exn (x,x))
 
 let[@zero_alloc strict] call_loud2 x = fail_loud2 (x+1)
 
 (* For duplicate attributes we get a warning and the first one takes effect. *)
-let[@inline never][@zero_alloc strict assume][@zero_alloc ignore] fail_loud1 x = raise (Exn (x,x))
+let[@inline never][@specialise never][@zero_alloc strict assume][@zero_alloc ignore] fail_loud1 x = raise (Exn (x,x))
 
 let[@zero_alloc strict] call_loud1 x = fail_loud1 (x+1)

tests/backend/checkmach/t6.output

@@ -1,2 +1,2 @@
-File "t6.ml", line 25, characters 47-57:
+File "t6.ml", line 25, characters 66-76:
 Warning 54 [duplicated-attribute]: the "zero_alloc" attribute is used more than once on this expression

tests/backend/checkmach/test_assume.ml

@@ -1,4 +1,4 @@
-let[@zero_alloc strict assume][@inline never] test1 n = (n,n)
+let[@zero_alloc strict assume][@inline never][@specialise never] test1 n = (n,n)
 let[@zero_alloc strict] test2 n = test1 (n+1)
 let[@zero_alloc strict] test3 n = T5.test n
 let no_annotations x y = x * y

tests/backend/checkmach/test_attribute_error_duplicate.ml

@@ -1,5 +1,5 @@
 let[@zero_alloc strict][@zero_alloc strict] test1 x = x,x
-let[@zero_alloc strict assume][@zero_alloc strict] test2 x = x,x
+let[@inline never][@specialise never][@zero_alloc strict assume][@zero_alloc strict] test2 x = x,x
 let[@zero_alloc strict check] test3 x = x,x
 let[@zero_alloc check] test4 x = x,x
 let[@zero_alloc all] test5 x = x,x

tests/backend/checkmach/test_attribute_error_duplicate.output

@@ -1,6 +1,6 @@
 File "test_attribute_error_duplicate.ml", line 1, characters 25-35:
 Warning 54 [duplicated-attribute]: the "zero_alloc" attribute is used more than once on this expression
-File "test_attribute_error_duplicate.ml", line 2, characters 32-42:
+File "test_attribute_error_duplicate.ml", line 2, characters 66-76:
 Warning 54 [duplicated-attribute]: the "zero_alloc" attribute is used more than once on this expression
 File "test_attribute_error_duplicate.ml", line 3, characters 5-15:
 Warning 47 [attribute-payload]: illegal payload for attribute 'zero_alloc'.

tests/backend/checkmach/test_warning198.ml

@@ -0,0 +1,2 @@
+let[@zero_alloc assume] bar y = (y+1,y)
+

tests/backend/checkmach/test_warning198.output

@@ -0,0 +1,3 @@
+File "test_warning198.ml", line 1, characters 5-15:
+Warning 198 [misplaced-assume-attribute]: the "zero_alloc assume" attribute will be ignored by the check when the function is inlined or specialised.
+Mark this function as [@inline never][@specialise never].

tests/backend/checkmach/test_warning199.ml

@@ -0,0 +1,3 @@
+let[@zero_alloc][@inline always] baz y = snd y
+
+let[@zero_alloc] foo x = baz (x-1,x)

tests/backend/checkmach/test_warning199.mli

@@ -0,0 +1 @@
+val foo : int -> int

tests/backend/checkmach/test_warning199.output

@@ -0,0 +1,5 @@
+File "test_warning199.ml", line 1, characters 5-15:
+Warning 199 [unchecked-property-attribute]: the "zero_alloc" attribute cannot be checked.
+The function it is attached to was optimized away. 
+You can try to mark this function as [@inline never] 
+or move the attribute to the relevant callers of this function.