Refactoring: Make file for zero_alloc typing stuff

Author: ccasin

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 \

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)

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 \

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

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,9 @@ 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 try Zero_alloc.sub_exn vd1.val_zero_alloc vd2.val_zero_alloc with
+  | Zero_alloc.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 +319,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 =

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

ocaml/typing/typedtree.ml

@@ -146,7 +146,7 @@ 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 *
@@ -1093,7 +1093,7 @@ let let_bound_idents_with_modes_sorts_and_checks bindings =
     (fun (id, _, _, _) ->
        let zero_alloc =
          Option.value (Ident.Map.find_opt id checks)
-           ~default:Builtin_attributes.Default_zero_alloc
+           ~default:Zero_alloc.Default_zero_alloc
        in
        id, List.rev (Ident.Tbl.find_all modes_and_sorts id), zero_alloc)
     (rev_let_bound_idents_full bindings)

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 _)
@@ -1157,7 +1157,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:

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;
     }

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;
     }

ocaml/typing/zero_alloc.ml

@@ -0,0 +1,102 @@
+module ZA = Zero_alloc_utils
+
+type t = Builtin_attributes.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;
+              }
+
+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_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"
+  | None, None -> ()

ocaml/typing/zero_alloc.mli

@@ -0,0 +1,24 @@
+type t = Builtin_attributes.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;
+              }
+
+type error
+
+exception Error of error
+
+val print_error : Format.formatter -> error -> unit
+
+(* [sub_exn t1 t2] checks whether the zero_alloc check t1 is stronger than the
+   zero_alloc check t2. If not, it raises [Error]. *)
+val sub_exn : t -> t -> unit