flambda-backend: Zero alloc: assume error means never raises (#2512)

* Add Builtin_attributes.check_attribute.never_raises field

* Add a test for "assume error"

* "error" implies "div=safe"

* fmt

* Add a comment that explains the intended meaning of [never_raises]

never lets exceptions escape

* Update comment in test

Author: gretay-js

lambda/lambda.ml

@@ -640,6 +640,7 @@ type check_attribute = Builtin_attributes.check_attribute =
   | Assume of { property: property;
                 strict: bool;
                 never_returns_normally: bool;
+                never_raises: bool;
                 arity: int;
                 loc: Location.t;
               }

lambda/lambda.mli

@@ -521,6 +521,7 @@ type check_attribute = Builtin_attributes.check_attribute =
   | Assume of { property: property;
                 strict: bool;
                 never_returns_normally: bool;
+                never_raises: bool;
                 arity: int;
                 loc: Location.t;
               }

parsing/builtin_attributes.ml

@@ -691,6 +691,7 @@ type check_attribute =
   | Assume of { property: property;
                 strict: bool;
                 never_returns_normally: bool;
+                never_raises: bool;
                 arity: int;
                 loc: Location.t;
               }
@@ -825,6 +826,7 @@ let zero_alloc_lookup_table =
     (["assume"],
      fun arity loc ->
        Assume { property; strict = false; never_returns_normally = false;
+                never_raises = false;
                 arity; loc; });
     (["strict"],
      fun arity loc ->
@@ -838,18 +840,22 @@ let zero_alloc_lookup_table =
     (["assume"; "strict"],
      fun arity loc ->
        Assume { property; strict = true; never_returns_normally = false;
+                never_raises = false;
                 arity; loc; });
     (["assume"; "never_returns_normally"],
      fun arity loc ->
        Assume { property; strict = false; never_returns_normally = true;
+                never_raises = false;
                 arity; loc; });
     (["assume"; "never_returns_normally"; "strict"],
      fun arity loc ->
        Assume { property; strict = true; never_returns_normally = true;
+                never_raises = false;
                 arity; loc; });
     (["assume"; "error"],
      fun arity loc ->
-       Assume { property; strict = false; never_returns_normally = true;
+       Assume { property; strict = true; never_returns_normally = true;
+                never_raises = true;
                 arity; loc; });
     (["ignore"], fun _ _ -> Ignore_assert_all property)
   ]
@@ -926,8 +932,8 @@ let assume_zero_alloc ~is_check_allowed check : Zero_alloc_utils.Assume_info.t =
   match check with
   | Default_check -> Zero_alloc_utils.Assume_info.none
   | Ignore_assert_all Zero_alloc -> Zero_alloc_utils.Assume_info.none
-  | Assume { property=Zero_alloc; strict; never_returns_normally; } ->
-    Zero_alloc_utils.Assume_info.create ~strict ~never_returns_normally
+  | Assume { property=Zero_alloc; strict; never_returns_normally; never_raises; } ->
+    Zero_alloc_utils.Assume_info.create ~strict ~never_returns_normally ~never_raises
   | Check { property=Zero_alloc; loc; _ } ->
     if not is_check_allowed then begin
       let name = "zero_alloc" in

parsing/builtin_attributes.mli

@@ -257,6 +257,11 @@ type check_attribute =
   | Assume of { property: property;
                 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;
               }

typing/includecore.ml

@@ -117,8 +117,10 @@ let zero_alloc za1 za2 =
     | Default_check | Ignore_assert_all _ -> ZA.Assume_info.Value.top ()
     | Check { strict; _ } ->
       ZA.Assume_info.Value.of_annotation ~strict ~never_returns_normally:false
-    | Assume { strict; never_returns_normally } ->
+        ~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

typing/typecore.ml

@@ -5087,6 +5087,7 @@ let zero_alloc_of_application ~num_args attrs funct =
           property = Zero_alloc;
           strict = c.strict;
           never_returns_normally = false;
+          never_raises = false;
           arity = c.arity;
           loc = c.loc
         }

typing/typemod.ml

@@ -2816,7 +2816,8 @@ and type_structure ?(toplevel = None) funct_body anchor env sstr =
                 | Default_check | Ignore_assert_all _ -> Default_check
                 | Check _ -> zero_alloc
                 | Assume { property; strict; arity; loc;
-                           never_returns_normally = _ } ->
+                           never_returns_normally = _;
+                           never_raises = _} ->
                   Check { strict; property; arity; loc; opt = false }
               in
               let (first_loc, _, _) = List.hd id_info in

utils/zero_alloc_utils.ml

@@ -137,8 +137,9 @@ module Make (Witnesses : WS) = struct
 
     let relaxed w = { nor = V.Safe; exn = V.Top w; div = V.Top w }
 
-    let of_annotation ~strict ~never_returns_normally =
+    let of_annotation ~strict ~never_returns_normally ~never_raises =
       let res = if strict then safe else relaxed Witnesses.empty in
+      let res = if never_raises then { res with exn = V.Bot } else res in
       if never_returns_normally then { res with nor = V.Bot } else res
 
     let print ~witnesses ppf { nor; exn; div } =
@@ -211,8 +212,8 @@ module Assume_info = struct
 
   let none = No_assume
 
-  let create ~strict ~never_returns_normally =
-    Assume (Value.of_annotation ~strict ~never_returns_normally)
+  let create ~strict ~never_returns_normally ~never_raises =
+    Assume (Value.of_annotation ~strict ~never_returns_normally ~never_raises)
 
   let get_value t = match t with No_assume -> None | Assume v -> Some v
 

utils/zero_alloc_utils.mli

@@ -83,7 +83,8 @@ module Make (Witnesses : WS) : sig
     val relaxed : Witnesses.t -> t
 
     (** Constructs a value from a user annotation. The witness will be empty. *)
-    val of_annotation : strict:bool -> never_returns_normally:bool -> t
+    val of_annotation :
+      strict:bool -> never_returns_normally:bool -> never_raises:bool -> t
 
     val print : witnesses:bool -> Format.formatter -> t -> unit
 
@@ -113,7 +114,8 @@ module Assume_info : sig
 
   val none : t
 
-  val create : strict:bool -> never_returns_normally:bool -> t
+  val create :
+    strict:bool -> never_returns_normally:bool -> never_raises:bool -> t
 
   val compare : t -> t -> int