Skip to content

Commit

Permalink
Add attributes to (unsafely) skip jkind check (ocaml-flambda#3385)
Browse files Browse the repository at this point in the history
* Add attributes to (unsafely) skip jkind check

Add a pair of attributes, [@@unsafe_allow_any_kind_in_intf] and
[@@unsafe_allow_any_kind_in_impl], which if set on both the impl and the intf
respectively, skip checking the jkind of the type in a signature against the
jkind of the type in a struct entirely. This is a more-selective version of the
`--allow-illegal-crossing` flag, and likely eventually subsumes it.

Signed-off-by: Aspen Smith <aspsmith@janestreet.com>

* Emit a warning when unsafe_allow_any_kind is added unnecessarily

Note that this is /only/ done if the attribute is set in both signatures but not
used - also this is a little over-sensitive (sadly) since this is done during
sigature inclusion too. A new test covers the over-sensitivity.

Signed-off-by: Aspen Smith <aspsmith@janestreet.com>

---------

Signed-off-by: Aspen Smith <aspsmith@janestreet.com>
  • Loading branch information
glittershark authored Dec 28, 2024
1 parent 862ced2 commit fe97beb
Show file tree
Hide file tree
Showing 6 changed files with 243 additions and 11 deletions.
19 changes: 17 additions & 2 deletions parsing/builtin_attributes.ml
Original file line number Diff line number Diff line change
Expand Up @@ -504,6 +504,10 @@ let has_unboxed attrs = has_attribute "unboxed" attrs

let has_boxed attrs = has_attribute "boxed" attrs

let has_unsafe_allow_any_kind_in_intf attrs = has_attribute "unsafe_allow_any_kind_in_intf" attrs

let has_unsafe_allow_any_kind_in_impl attrs = has_attribute "unsafe_allow_any_kind_in_impl" attrs

let parse_empty_payload attr =
match attr.attr_payload with
| PStr [] -> Some ()
Expand Down Expand Up @@ -602,6 +606,15 @@ let zero_alloc_attribute (attr : Parsetree.attribute) =
warn_payload attr.attr_loc attr.attr_name.txt
"Only 'all', 'check', 'check_opt', 'check_all', and 'check_none' are supported")

let attribute_with_ignored_payload name attr =
when_attribute_is [name; "ocaml." ^ name] attr ~f:(fun () -> ())

let unsafe_allow_any_kind_in_impl_attribute =
attribute_with_ignored_payload "unsafe_allow_any_kind_in_impl"

let unsafe_allow_any_kind_in_intf_attribute =
attribute_with_ignored_payload "unsafe_allow_any_kind_in_intf"

let afl_inst_ratio_attribute attr =
clflags_attribute_with_int_payload attr
~name:"afl_inst_ratio" Clflags.afl_inst_ratio
Expand All @@ -610,7 +623,8 @@ let parse_standard_interface_attributes attr =
warning_attribute attr;
principal_attribute attr;
noprincipal_attribute attr;
nolabels_attribute attr
nolabels_attribute attr;
unsafe_allow_any_kind_in_intf_attribute attr

let parse_standard_implementation_attributes attr =
warning_attribute attr;
Expand All @@ -621,7 +635,8 @@ let parse_standard_implementation_attributes attr =
afl_inst_ratio_attribute attr;
flambda_o3_attribute attr;
flambda_oclassic_attribute attr;
zero_alloc_attribute attr
zero_alloc_attribute attr;
unsafe_allow_any_kind_in_impl_attribute attr

let has_no_mutable_implied_modalities attrs =
has_attribute "no_mutable_implied_modalities" attrs
Expand Down
5 changes: 5 additions & 0 deletions parsing/builtin_attributes.mli
Original file line number Diff line number Diff line change
Expand Up @@ -35,6 +35,8 @@
- ocaml.tailcall
- ocaml.tail_mod_cons
- ocaml.unboxed
- ocaml.unsafe_allow_any_kind_in_impl
- ocaml.unsafe_allow_any_kind_in_intf
- ocaml.untagged
- ocaml.unrolled
- ocaml.warnerror
Expand Down Expand Up @@ -198,6 +200,9 @@ val explicit_arity: Parsetree.attributes -> bool
val has_unboxed: Parsetree.attributes -> bool
val has_boxed: Parsetree.attributes -> bool

val has_unsafe_allow_any_kind_in_impl: Parsetree.attributes -> bool
val has_unsafe_allow_any_kind_in_intf: Parsetree.attributes -> bool

val parse_standard_interface_attributes : Parsetree.attribute -> unit
val parse_standard_implementation_attributes : Parsetree.attribute -> unit

Expand Down
190 changes: 190 additions & 0 deletions testsuite/tests/typing-layouts/allow_any.ml
Original file line number Diff line number Diff line change
@@ -0,0 +1,190 @@
(* TEST
flags = "-extension layouts_beta";
expect;
*)

(* Baseline: if the jkind doesn't match, we should get an error. *)
module Mismatched_no_attrs : sig
type t : float64
end = struct
type t = string
end
[%%expect{|
Lines 3-5, characters 6-3:
3 | ......struct
4 | type t = string
5 | end
Error: Signature mismatch:
Modules do not match:
sig type t = string end
is not included in
sig type t : float64 end
Type declarations do not match:
type t = string
is not included in
type t : float64
The layout of the first is value
because it is the primitive type string.
But the layout of the first must be a sublayout of float64
because of the definition of t at line 2, characters 2-18.
|}]

(* On the other hand, if we set the correct attributes on both the impl and the intf, we
shouldn't get an error (though, obviously, this is completely unsound!) *)
module Mismatched_with_both_attrs : sig
type t : float64
[@@unsafe_allow_any_kind_in_impl "I love segfaults"]
end = struct
type t = string
[@@unsafe_allow_any_kind_in_intf "I love segfaults"]
end
[%%expect{|
module Mismatched_with_both_attrs : sig type t : float64 end
|}]

(* If we set the attributes but *don't* get a kind mismatch, we ought to be fine *)
module Matching : sig
type t : value
[@@unsafe_allow_any_kind_in_impl "I love segfaults"]
end = struct
type t = string
[@@unsafe_allow_any_kind_in_intf "I love segfaults"]
end
[%%expect{|
Lines 2-3, characters 2-54:
2 | ..type t : value
3 | [@@unsafe_allow_any_kind_in_impl "I love segfaults"]
Warning 212 [unnecessary-allow-any-kind]: [@@allow_any_kind_in_intf] and [@@allow_any_kind_in_impl] set on a
type, but the kind matches. The attributes can be removed.

module Matching : sig type t end
|}]

(* If the attr is only on the signature we should get an error *)
module Mismatched_with_attr_on_intf : sig
type t : float64
[@@unsafe_allow_any_kind_in_impl "I love segfaults"]
end = struct
type t = string
end
[%%expect{|
Lines 4-6, characters 6-3:
4 | ......struct
5 | type t = string
6 | end
Error: Signature mismatch:
Modules do not match:
sig type t = string end
is not included in
sig type t : float64 end
Type declarations do not match:
type t = string
is not included in
type t : float64
The layout of the first is value
because it is the primitive type string.
But the layout of the first must be a sublayout of float64
because of the definition of t at lines 2-3, characters 2-54.
|}]

(* If the attr is only on the struct we should get an error *)
module Mismatched_with_attr_on_impl : sig
type t : float64
end = struct
type t = string
[@@unsafe_allow_any_kind_in_intf "I love segfaults"]
end
[%%expect{|
Lines 3-6, characters 6-3:
3 | ......struct
4 | type t = string
5 | [@@unsafe_allow_any_kind_in_intf "I love segfaults"]
6 | end
Error: Signature mismatch:
Modules do not match:
sig type t = string end
is not included in
sig type t : float64 end
Type declarations do not match:
type t = string
is not included in
type t : float64
The layout of the first is value
because it is the primitive type string.
But the layout of the first must be a sublayout of float64
because of the definition of t at line 2, characters 2-18.
|}]

(* Some more complex stuff with functors *)

module type S1 = sig
type t : value
end

module type S2 = sig
type t : float64
[@@unsafe_allow_any_kind_in_impl]
end

module type S1 = sig
type t : value
[@@unsafe_allow_any_kind_in_intf]
end

module F1 (X : S1) : S2 = X

[%%expect{|
module type S1 = sig type t end
module type S2 = sig type t : float64 end
module type S1 = sig type t end
module F1 : functor (X : S1) -> S2
|}]

module F2 (X : S2) : S1 = X
[%%expect{|
Line 1, characters 26-27:
1 | module F2 (X : S2) : S1 = X
^
Error: Signature mismatch:
Modules do not match: sig type t = X.t end is not included in S1
Type declarations do not match: type t = X.t is not included in type t
The layout of the first is float64
because of the definition of t at lines 6-7, characters 2-35.
But the layout of the first must be a sublayout of value
because of the definition of t at lines 11-12, characters 2-35.
|}]

(* Non-abstract types can be annotated with [@@unsafe_allow_any_kind_in_intf] too, and get
checked against signatures during inclusion. *)

module M1 : sig
type t : value = string [@@unsafe_allow_any_kind_in_intf]
end = struct
type t = string
end

module M2 : S2 = M1

[%%expect{|
module M1 : sig type t = string end
module M2 : S2
|}]

module type S3 = sig
type t : value
[@@unsafe_allow_any_kind_in_impl]
end

module M3 : S3 = M1
(* CR aspsmith: This is somewhat unfortunate, if S3 and M1 are defined far away, but it's
unclear how to squash the warning *)
[%%expect{|
module type S3 = sig type t end
Lines 2-3, characters 2-35:
2 | ..type t : value
3 | [@@unsafe_allow_any_kind_in_impl]
Warning 212 [unnecessary-allow-any-kind]: [@@allow_any_kind_in_intf] and [@@allow_any_kind_in_impl] set on a
type, but the kind matches. The attributes can be removed.

module M3 : S3
|}]
28 changes: 19 additions & 9 deletions typing/includecore.ml
Original file line number Diff line number Diff line change
Expand Up @@ -1348,15 +1348,25 @@ let type_declarations ?(equality = false) ~loc env ~mark name
rep1 rep2
in
let err = match (decl1.type_kind, decl2.type_kind) with
(_, Type_abstract _) ->
(* Note that [decl2.type_jkind] is an upper bound.
If it isn't tight, [decl2] must
have a manifest, which we're already checking for equality
above. Similarly, [decl1]'s kind may conservatively approximate its
jkind, but [check_decl_jkind] will expand its manifest. *)
(match Ctype.check_decl_jkind env decl1 decl2.type_jkind with
| Ok _ -> None
| Error v -> Some (Jkind v))
(_, Type_abstract _) -> begin
(* If both the intf has "allow any kind in impl" *and* the impl has "allow any
kind in intf", don't check the jkind at all. *)
let allow_any =
Builtin_attributes.has_unsafe_allow_any_kind_in_impl decl2.type_attributes
&& Builtin_attributes.has_unsafe_allow_any_kind_in_intf decl1.type_attributes
in
(* Note that [decl2.type_jkind] is an upper bound. If it isn't tight, [decl2] must
have a manifest, which we're already checking for equality above. Similarly,
[decl1]'s kind may conservatively approximate its jkind, but [check_decl_jkind]
will expand its manifest. *)
match Ctype.check_decl_jkind env decl1 decl2.type_jkind with
| Ok _ ->
(if allow_any
then Location.prerr_warning decl2.type_loc (Warnings.Unnecessary_allow_any_kind));
None
| Error _ when allow_any -> None
| Error v -> Some (Jkind v)
end
| (Type_variant (cstrs1, rep1), Type_variant (cstrs2, rep2)) ->
if mark then begin
let mark usage cstrs =
Expand Down
11 changes: 11 additions & 0 deletions utils/warnings.ml
Original file line number Diff line number Diff line change
Expand Up @@ -129,6 +129,7 @@ type t =
| Unchecked_zero_alloc_attribute (* 199 *)
| Unboxing_impossible (* 210 *)
| Mod_by_top of string (* 211 *)
| Unnecessary_allow_any_kind (* 212 *)

(* If you remove a warning, leave a hole in the numbering. NEVER change
the numbers of existing warnings.
Expand Down Expand Up @@ -217,6 +218,7 @@ let number = function
| Unchecked_zero_alloc_attribute -> 199
| Unboxing_impossible -> 210
| Mod_by_top _ -> 211
| Unnecessary_allow_any_kind -> 212
;;
(* DO NOT REMOVE the ;; above: it is used by
the testsuite/ests/warnings/mnemonics.mll test to determine where
Expand Down Expand Up @@ -592,6 +594,11 @@ let descriptions = [
names = ["mod-by-top"];
description = "Including the top-most element of an axis in a kind's modifiers is a no-op.";
since = since 4 14 };
{ number = 212;
names = ["unnecessary-allow-any-kind"];
description = "[@@unsafe_allow_any_kind_in_{impl,intf}] attributes included \
on a type and a signature with matching kinds";
since = since 5 1 };
]

let name_to_number =
Expand Down Expand Up @@ -1235,6 +1242,10 @@ let message = function
"%s is the top-most modifier.\n\
Modifying by a top element is a no-op."
modifier
| Unnecessary_allow_any_kind ->
Printf.sprintf
"[@@allow_any_kind_in_intf] and [@@allow_any_kind_in_impl] set on a \n\
type, but the kind matches. The attributes can be removed."
;;

let nerrors = ref 0
Expand Down
1 change: 1 addition & 0 deletions utils/warnings.mli
Original file line number Diff line number Diff line change
Expand Up @@ -135,6 +135,7 @@ type t =
| Unchecked_zero_alloc_attribute (* 199 *)
| Unboxing_impossible (* 210 *)
| Mod_by_top of string (* 211 *)
| Unnecessary_allow_any_kind (* 212 *)

type alert = {kind:string; message:string; def:loc; use:loc}

Expand Down

0 comments on commit fe97beb

Please sign in to comment.