Add a test for "assume error"

tests/backend/checkmach/dune.inc

@@ -940,3 +940,22 @@
  (enabled_if (= %{context_name} "main"))
  (deps test_signatures_separate.opt.output test_signatures_separate.opt.output.corrected)
  (action (diff test_signatures_separate.opt.output test_signatures_separate.opt.output.corrected)))
+
+(rule
+ (enabled_if (= %{context_name} "main"))
+ (targets test_assume_error.output.corrected)
+ (deps (:ml test_assume_error.ml) filter.sh)
+ (action
+   (with-outputs-to test_assume_error.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 -checkmach-details-cutoff 20 -O3))
+    (run "./filter.sh")
+   ))))
+
+(rule
+ (alias   runtest)
+ (enabled_if (= %{context_name} "main"))
+ (deps test_assume_error.output test_assume_error.output.corrected)
+ (action (diff test_assume_error.output test_assume_error.output.corrected)))

tests/backend/checkmach/gen/gen_dune.ml

@@ -177,4 +177,6 @@ let () =
     ~extra_flags:"-zero-alloc-check all"
     ~extra_dep:(Some "test_signatures_separate_a.cmi")
     ~exit_code:2 "test_signatures_separate_b";
+  print_test_expected_output ~cutoff:default_cutoff
+    ~extra_dep:None ~exit_code:2 "test_assume_error";
   ()

tests/backend/checkmach/test_assume_error.ml

@@ -0,0 +1,225 @@
+(* A1: zero_alloc check fails on [foo] because there is an allocation on the
+   path to exceptional return from the call to [f x].
+   This exception is handled in foo and then [foo] returns normally,
+   making this allocation on a normal return of [foo].
+*)
+module A1 = struct
+  let[@inline never][@local never] h s = [Random.int s ; Random.int s]
+
+  let[@inline never][@local never][@zero_alloc] g x =
+    if x < 0 then Sys.opaque_identity (x+1) else raise (Failure ((string_of_int) x))
+
+  let[@inline never][@local never] handle_exn exn =
+    (match exn with
+     | Failure s -> print_string s; print_newline ()
+     | _ -> failwith "Boo");
+    0
+  ;;
+
+  let[@zero_alloc] f x =
+    match g x with
+    | exception exn ->
+      (handle_exn[@zero_alloc assume never_returns_normally]) exn
+      |> h |> List.hd  (* ignore this allocation *)
+    | answer -> (answer * 2)
+
+  let[@zero_alloc] foo x =
+    try f x with
+    | _ -> 0
+end
+
+(* A2 is a more elaborate version of A1 with more allocations in [foo]
+   that are all correctly reported. *)
+module A2 = struct
+  let[@inline never][@local never] h s = [Random.int s ; Random.int s]
+
+  let[@inline never][@local never][@zero_alloc] g x =
+    if x < 0 then Sys.opaque_identity (x+1) else raise (Failure ((string_of_int) x))
+
+  let[@inline never][@local never] handle_exn exn =
+    (match exn with
+     | Failure s -> print_string s; print_newline ()
+     | _ -> failwith "Boo");
+    0
+  ;;
+
+  let[@zero_alloc] f x =
+    match g x with
+    | exception exn ->
+      (handle_exn[@zero_alloc assume never_returns_normally]) exn
+      |> h |> List.hd  (* ignore this allocation *)
+    | answer -> (answer * 2)
+
+  let[@zero_alloc] foo x =
+    try let y = f x in (x,y) with
+    | _ ->
+      Printf.printf "BOO %x" x;  (* ignore this indirect call *)
+      (x,0)
+end
+
+(* A3: shows that "assume error" causes the check to ignore allocations
+   in [foo] that come after the exceptional return from [f x]
+   and correctly report allocations that happen after normal return
+   from [f x]. *)
+module A3 = struct
+  let[@inline never][@local never] h s = [Random.int s ; Random.int s]
+
+  let[@inline never][@local never][@zero_alloc] g x =
+    if x < 0 then Sys.opaque_identity (x+1) else raise (Failure ((string_of_int) x))
+
+  let[@inline never][@local never] handle_exn exn =
+    (match exn with
+     | Failure s -> print_string s; print_newline ()
+     | _ -> failwith "Boo");
+    0
+  ;;
+
+  let[@zero_alloc] f x =
+    match g x with
+    | exception exn ->
+      (handle_exn[@zero_alloc assume error]) exn
+      |> h |> List.hd  (* ignore this allocation *)
+    | answer -> (answer * 2)
+
+  let[@zero_alloc] foo x =
+    try
+      let y = f x in
+      (x,y)  (* report this allocation *)
+    with
+    | _ ->
+      Printf.printf "BOO %x" x;  (* ignore this indirect call *)
+      (x,0)
+end
+
+(* A4: is a succesful version of A3, without allocation after normal return
+   from [f x]. *)
+module A4 = struct
+  let[@inline never][@local never] h s = [Random.int s ; Random.int s]
+
+  let[@inline never][@local never][@zero_alloc] g x =
+    if x < 0 then Sys.opaque_identity (x+1) else raise (Failure ((string_of_int) x))
+
+  let[@inline never][@local never] handle_exn exn =
+    (match exn with
+     | Failure s -> print_string s; print_newline ()
+     | _ -> failwith "Boo");
+    0
+  ;;
+
+  let[@zero_alloc] f x =
+    match g x with
+    | exception exn ->
+      (handle_exn[@zero_alloc assume error]) exn
+      |> h |> List.hd  (* ignore this allocation *)
+    | answer -> (answer * 2)
+
+  let[@zero_alloc] foo x =
+    try f x
+    with
+    | _ ->
+      Printf.printf "BOO %x" x;  (* ignore this indirect call *)
+      0
+end
+
+(* A5: same as A4 but with "assume error" on the function definition instead
+   of the call site. *)
+module A5 = struct
+  let[@inline never][@local never] h s = [Random.int s ; Random.int s]
+
+  let[@inline never][@local never][@zero_alloc] g x =
+    if x < 0 then Sys.opaque_identity (x+1) else raise (Failure ((string_of_int) x))
+
+  let[@inline never][@local never][@zero_alloc assume error] handle_exn exn =
+    (match exn with
+     | Failure s -> print_string s; print_newline ()
+     | _ -> failwith "Boo");
+    0
+  ;;
+
+  let[@zero_alloc] f x =
+    match g x with
+    | exception exn ->
+      handle_exn exn
+      |> h |> List.hd  (* ignore this allocation *)
+    | answer -> (answer * 2)
+
+  let[@zero_alloc] foo x =
+    try f x
+    with
+    | _ ->
+      Printf.printf "BOO %x" x;  (* ignore this indirect call *)
+      0
+end
+
+(* A6: shows that "assume error" is not enough to prove "strict",
+   because the call to [string_of_int] is not known to not diverge.
+*)
+module A6 = struct
+  let[@inline never][@local never] h s = [Random.int s ; Random.int s]
+
+  let[@inline never][@local never][@zero_alloc] g x =
+    if x < 0 then Sys.opaque_identity (x+1) else raise (Failure ((string_of_int) x))
+
+  let[@inline never][@local never][@zero_alloc assume error] handle_exn exn =
+    (match exn with
+     | Failure s -> print_string s; print_newline ()
+     | _ -> failwith "Boo");
+    0
+  ;;
+
+  let[@zero_alloc strict] f x =
+    match g x with
+    | exception exn ->
+      handle_exn exn
+      |> h |> List.hd  (* ignore this allocation *)
+    | answer -> (answer * 2)
+
+end
+
+(* A7 is the same as A6 but without [string_of_int] and we can prove strict annotation on
+   [f]*)
+module A7 = struct
+  let[@inline never][@local never] h s = [Random.int s ; Random.int s]
+
+  let[@inline never][@local never][@zero_alloc] g x =
+    if x < 0 then Sys.opaque_identity (x+1) else raise (Failure "boo")
+
+  let[@inline never][@local never][@zero_alloc assume error] handle_exn exn =
+    (match exn with
+     | Failure s -> print_string s; print_newline ()
+     | _ -> failwith "Boo");
+    0
+  ;;
+
+  let[@zero_alloc strict] f x =
+    match g x with
+    | exception exn ->
+      handle_exn exn
+      |> h |> List.hd  (* ignore this allocation *)
+    | answer -> (answer * 2)
+
+end
+
+(* A8 is the same as A7 but with "assume never_returns_normally" only instead of
+   "assume error" and it is not enough to prove "strict" on [f]. *)
+module A8 = struct
+  let[@inline never][@local never] h s = [Random.int s ; Random.int s]
+
+  let[@inline never][@local never][@zero_alloc] g x =
+    if x < 0 then Sys.opaque_identity (x+1) else raise (Failure "boo")
+
+  let[@inline never][@local never][@zero_alloc assume never_returns_normally] handle_exn exn =
+    (match exn with
+     | Failure s -> print_string s; print_newline ()
+     | _ -> failwith "Boo");
+    0
+  ;;
+
+  let[@zero_alloc strict] f x =
+    match g x with
+    | exception exn ->
+      handle_exn exn
+      |> h |> List.hd  (* ignore this allocation *)
+    | answer -> (answer * 2)
+
+end

tests/backend/checkmach/test_assume_error.output

@@ -0,0 +1,47 @@
+File "test_assume_error.ml", line 26, characters 7-17:
+Error: Annotation check for zero_alloc failed on function Test_assume_error.A1.foo (camlTest_assume_error.foo_HIDE_STAMP)
+
+File "test_assume_error.ml", line 27, characters 8-11:
+Error: called function may allocate (direct call camlTest_assume_error.g_HIDE_STAMP) (test_assume_error.ml:27,8--11;test_assume_error.ml:20,10--13)
+
+File "test_assume_error.ml", line 27, characters 8-11:
+Error: called function may allocate (direct call camlTest_assume_error.handle_exn_HIDE_STAMP) (test_assume_error.ml:27,8--11;test_assume_error.ml:22,6--65)
+
+File "test_assume_error.ml", line 53, characters 7-17:
+Error: Annotation check for zero_alloc failed on function Test_assume_error.A2.foo (camlTest_assume_error.foo_HIDE_STAMP)
+
+File "test_assume_error.ml", line 56, characters 6-30:
+Error: called function may allocate (direct call camlCamlinternalFormat.make_printf_HIDE_STAMP) (test_assume_error.ml:56,6--30;printf.ml:37,17--35;printf.ml:33,21--43;printf.ml:26,2--63)
+
+File "test_assume_error.ml", line 54, characters 16-19:
+Error: called function may allocate (direct call camlTest_assume_error.g_HIDE_STAMP) (test_assume_error.ml:54,16--19;test_assume_error.ml:47,10--13)
+
+File "test_assume_error.ml", line 54, characters 16-19:
+Error: called function may allocate (direct call camlTest_assume_error.handle_exn_HIDE_STAMP) (test_assume_error.ml:54,16--19;test_assume_error.ml:49,6--65)
+
+File "test_assume_error.ml", line 54, characters 23-28:
+Error: allocation of 24 bytes
+
+File "test_assume_error.ml", line 56, characters 6-30:
+Error: called function may allocate (indirect call)
+
+File "test_assume_error.ml", line 57, characters 6-11:
+Error: allocation of 24 bytes
+
+File "test_assume_error.ml", line 84, characters 7-17:
+Error: Annotation check for zero_alloc failed on function Test_assume_error.A3.foo (camlTest_assume_error.foo_HIDE_STAMP)
+
+File "test_assume_error.ml", line 87, characters 6-11:
+Error: allocation of 24 bytes
+
+File "test_assume_error.ml", line 170, characters 7-17:
+Error: Annotation check for zero_alloc strict failed on function Test_assume_error.A6.f (camlTest_assume_error.f_HIDE_STAMP)
+
+File "test_assume_error.ml", line 171, characters 10-13:
+Error: called function may allocate on a path to diverge (direct call camlTest_assume_error.g_HIDE_STAMP)
+
+File "test_assume_error.ml", line 218, characters 7-17:
+Error: Annotation check for zero_alloc strict failed on function Test_assume_error.A8.f (camlTest_assume_error.f_HIDE_STAMP)
+
+File "test_assume_error.ml", line 221, characters 6-20:
+Error: called function may allocate on a path to exceptional return (direct call camlTest_assume_error.handle_exn_HIDE_STAMP)