Skip to content

Commit

Permalink
Add a new attribute for allowing any mode crossing (#3424)
Browse files Browse the repository at this point in the history
* Add a new attribute for allowing any mode crossing

Replace the [@@unsafe_allow_any_kind_in_{impl,intf}] attributes with a new
[@@unsafe_allow_any_mode_crossing] attribute. This is different in that it:

1. Works on the type declaration, not the inclusion check, so is more powerful -
   it can be used to illegally mode cross types defined in the same module, or
   illegally mode cross non-abstract types in interfaces. The latter especially
   is necessary to fully subsume -allow-illegal-crossing in stdlib
2. Only allows changing the modal bounds of a kind, not the layout - it's
   unclear that anyone should ever want to unsafely change the layout of a kind;
   I personally can't think of any sound reason to do so.

Some [past discussion][0] on the specific syntax for this attribute suggested
specifying the bounds directly on the attribute, rather than using the jkind
annotation, but I and others feel reasonably strongly that this way of doing
things is a better design for the sake of consistency.

[0]: #3385 (comment)

* Print the [@@unsafe_allow_any_mode_crossing] attribute in outcomes

For types that set it, or *would have* set it (eg because the whole compilation
unit set -allow-illegal-crossing)

* Track unsafe_mode_crossing in type_kind

Add a field to (the relevant variants of) type_kind, which tracks the (extended)
modal upper bounds of a kind introduced by the usage of the
[@@unsafe_allow_any_mode_crossing] attribute. This allows us to check this in eg
the inclusion check, and forbid extending the upper bounds of a type /only/ by
constraining it to a signature. Also, this moves more towards a world where
`decl.type_jkind` is "morally" just a memo of the type's kind, where everything
about the kind /could/ ostensibly be computed by looking at the type_kind.

A few extra test cases checking that we cant do this have also been added to
`allow_any.ml`

* Be more strict about unsafe mode crossing in inclusion

Specifically, require strict equality of bounds, and the attribute present on
both sides.
  • Loading branch information
glittershark authored Jan 27, 2025
1 parent 069d613 commit 8935997
Show file tree
Hide file tree
Showing 31 changed files with 582 additions and 315 deletions.
2 changes: 1 addition & 1 deletion debugger/eval.ml
Original file line number Diff line number Diff line change
Expand Up @@ -165,7 +165,7 @@ let rec expression event env = function
Tconstr(path, _, _) ->
let tydesc = Env.find_type path env in
begin match tydesc.type_kind with
Type_record(lbl_list, _repr) ->
Type_record(lbl_list, _repr, _) ->
let (pos, ty_res) =
find_label lbl env ty path tydesc 0 lbl_list in
(Debugcom.Remote_value.field v pos, ty_res)
Expand Down
2 changes: 1 addition & 1 deletion debugger4/eval.ml
Original file line number Diff line number Diff line change
Expand Up @@ -165,7 +165,7 @@ let rec expression event env = function
Tconstr(path, _, _) ->
let tydesc = Env.find_type path env in
begin match tydesc.type_kind with
Type_record(lbl_list, _repr) ->
Type_record(lbl_list, _repr, _) ->
let (pos, ty_res) =
find_label lbl env ty path tydesc 0 lbl_list in
(Debugcom.Remote_value.field v pos, ty_res)
Expand Down
6 changes: 3 additions & 3 deletions ocamldoc/odoc_sig.ml
Original file line number Diff line number Diff line change
Expand Up @@ -450,7 +450,7 @@ module Analyser =
match type_kind with
Types.Type_abstract _ ->
Odoc_type.Type_abstract
| Types.Type_variant (l,_) ->
| Types.Type_variant (l,_,_) ->
let f {Types.cd_id=constructor_name;cd_args;cd_res=ret_type;cd_attributes} =
let constructor_name = Ident.name constructor_name in
let comment_opt =
Expand Down Expand Up @@ -481,10 +481,10 @@ module Analyser =
in
Odoc_type.Type_variant (List.map f l)

| Types.Type_record (l, _) ->
| Types.Type_record (l, _, _) ->
Odoc_type.Type_record (List.map (get_field env name_comment_list) l)

| Types.Type_record_unboxed_product (_, _) -> assert false
| Types.Type_record_unboxed_product (_, _, _) -> assert false

| Types.Type_open ->
Odoc_type.Type_open
Expand Down
16 changes: 6 additions & 10 deletions parsing/builtin_attributes.ml
Original file line number Diff line number Diff line change
Expand Up @@ -504,9 +504,8 @@ 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 has_unsafe_allow_any_mode_crossing attrs =
has_attribute "unsafe_allow_any_mode_crossing" attrs

let parse_empty_payload attr =
match attr.attr_payload with
Expand Down Expand Up @@ -609,11 +608,8 @@ let zero_alloc_attribute (attr : Parsetree.attribute) =
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 unsafe_allow_any_mode_crossing_attribute =
attribute_with_ignored_payload "unsafe_allow_any_mode_crossing"

let afl_inst_ratio_attribute attr =
clflags_attribute_with_int_payload attr
Expand All @@ -624,7 +620,7 @@ let parse_standard_interface_attributes attr =
principal_attribute attr;
noprincipal_attribute attr;
nolabels_attribute attr;
unsafe_allow_any_kind_in_intf_attribute attr
unsafe_allow_any_mode_crossing_attribute attr

let parse_standard_implementation_attributes attr =
warning_attribute attr;
Expand All @@ -636,7 +632,7 @@ let parse_standard_implementation_attributes attr =
flambda_o3_attribute attr;
flambda_oclassic_attribute attr;
zero_alloc_attribute attr;
unsafe_allow_any_kind_in_impl_attribute attr
unsafe_allow_any_mode_crossing_attribute attr

let has_no_mutable_implied_modalities attrs =
has_attribute "no_mutable_implied_modalities" attrs
Expand Down
6 changes: 2 additions & 4 deletions parsing/builtin_attributes.mli
Original file line number Diff line number Diff line change
Expand Up @@ -35,8 +35,7 @@
- ocaml.tailcall
- ocaml.tail_mod_cons
- ocaml.unboxed
- ocaml.unsafe_allow_any_kind_in_impl
- ocaml.unsafe_allow_any_kind_in_intf
- ocaml.unsafe_allow_any_mode_crossing
- ocaml.untagged
- ocaml.unrolled
- ocaml.warnerror
Expand Down Expand Up @@ -200,8 +199,7 @@ 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 has_unsafe_allow_any_mode_crossing : Parsetree.attributes -> bool

val parse_standard_interface_attributes : Parsetree.attribute -> unit
val parse_standard_implementation_attributes : Parsetree.attribute -> unit
Expand Down
Loading

0 comments on commit 8935997

Please sign in to comment.