Skip to content

Commit 42b545b

Browse files
alanechangalanechang
authored
flambda-backend: Mark layouts extension as erasable and limit the use of immediate/immediate64 (#2286)
* immediate/immediate64 annotations are not always erasable * fix typo * remove unnecessary flag and add more tests
1 parent bf6ad3e commit 42b545b

12 files changed

+369
-26
lines changed

‎testsuite/tests/typing-layouts-float64/unboxed_floats.ml

+4-6
Original file line numberDiff line numberDiff line change
@@ -11,18 +11,16 @@
1111
flags = "-extension layouts_beta"
1212
** bytecode
1313
flags = "-extension layouts_beta"
14+
** native
15+
flags = "-only-erasable-extensions"
16+
** bytecode
17+
flags = "-only-erasable-extensions"
1418
** setup-ocamlc.byte-build-env
1519
ocamlc_byte_exit_status = "2"
1620
*** ocamlc.byte
1721
flags = "-disable-all-extensions"
1822
compiler_reference = "${test_source_directory}/unboxed_floats_disabled.compilers.reference"
1923
**** check-ocamlc.byte-output
20-
** setup-ocamlc.byte-build-env
21-
ocamlc_byte_exit_status = "2"
22-
*** ocamlc.byte
23-
flags = "-only-erasable-extensions"
24-
compiler_reference = "${test_source_directory}/unboxed_floats_disabled.compilers.reference"
25-
**** check-ocamlc.byte-output
2624
*)
2725

2826
(* CR layouts v2.6: Layouts should be erasable and we can remove the

‎testsuite/tests/typing-layouts-float64/unboxed_floats_disabled.compilers.reference

+2-2
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
File "unboxed_floats.ml", line 65, characters 11-16:
2-
65 | let pi = #3.14 in
1+
File "unboxed_floats.ml", line 63, characters 11-16:
2+
63 | let pi = #3.14 in
33
^^^^^
44
Error: This construct requires the stable version of the extension "layouts", which is disabled and cannot be used

‎testsuite/tests/typing-layouts/erasable_annot.ml

+265
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,265 @@
1+
(* TEST
2+
* expect
3+
flags = "-only-erasable-extensions"
4+
*)
5+
6+
(* Upstream compatible usages of immediate/immediate64 are allowed *)
7+
module type S1 = sig
8+
type t_immediate : immediate
9+
type t_immediate64 : immediate64
10+
end;;
11+
[%%expect {|
12+
module type S1 =
13+
sig type t_immediate : immediate type t_immediate64 : immediate64 end
14+
|}];;
15+
16+
(* Same is not true when constraining type vars *)
17+
(* immediate *)
18+
module type S = sig
19+
val f_immediate : ('a : immediate). 'a -> 'a -> 'a
20+
end;;
21+
[%%expect {|
22+
Line 2, characters 2-52:
23+
2 | val f_immediate : ('a : immediate). 'a -> 'a -> 'a
24+
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
25+
Error: Usage of layout immediate/immediate64 in f_immediate can't be erased.
26+
This error is produced due to the use of -only-erasable-extensions.
27+
|}];;
28+
29+
module type S = sig
30+
val f_immediate : ('a : immediate) -> 'a -> 'a
31+
end;;
32+
[%%expect {|
33+
Line 2, characters 2-48:
34+
2 | val f_immediate : ('a : immediate) -> 'a -> 'a
35+
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
36+
Error: Usage of layout immediate/immediate64 in f_immediate can't be erased.
37+
This error is produced due to the use of -only-erasable-extensions.
38+
|}];;
39+
40+
module type S = sig
41+
type ('a : immediate) t
42+
end;;
43+
[%%expect {|
44+
Line 2, characters 2-25:
45+
2 | type ('a : immediate) t
46+
^^^^^^^^^^^^^^^^^^^^^^^
47+
Error: Usage of layout immediate/immediate64 in t can't be erased.
48+
This error is produced due to the use of -only-erasable-extensions.
49+
|}];;
50+
51+
module type S = sig
52+
type _ g = | MkG : ('a : immediate). 'a g
53+
end;;
54+
[%%expect {|
55+
Line 2, characters 2-43:
56+
2 | type _ g = | MkG : ('a : immediate). 'a g
57+
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
58+
Error: Usage of layout immediate/immediate64 in g can't be erased.
59+
This error is produced due to the use of -only-erasable-extensions.
60+
|}];;
61+
62+
let f (type a : immediate): a -> a = fun x -> x
63+
[%%expect {|
64+
Line 1, characters 4-5:
65+
1 | let f (type a : immediate): a -> a = fun x -> x
66+
^
67+
Error: Usage of layout immediate/immediate64 in f can't be erased.
68+
This error is produced due to the use of -only-erasable-extensions.
69+
|}];;
70+
71+
let f x = (x : (_ : immediate))
72+
[%%expect {|
73+
Line 1, characters 4-5:
74+
1 | let f x = (x : (_ : immediate))
75+
^
76+
Error: Usage of layout immediate/immediate64 in f can't be erased.
77+
This error is produced due to the use of -only-erasable-extensions.
78+
|}];;
79+
80+
let f v: ((_ : immediate)[@error_message "Custom message"]) = v
81+
[%%expect {|
82+
Line 1, characters 4-5:
83+
1 | let f v: ((_ : immediate)[@error_message "Custom message"]) = v
84+
^
85+
Error: Usage of layout immediate/immediate64 in f can't be erased.
86+
This error is produced due to the use of -only-erasable-extensions.
87+
|}];;
88+
89+
(* immediate64 *)
90+
module type S = sig
91+
val f_immediate64 : ('a : immediate64). 'a -> 'a -> 'a
92+
end;;
93+
[%%expect {|
94+
Line 2, characters 2-56:
95+
2 | val f_immediate64 : ('a : immediate64). 'a -> 'a -> 'a
96+
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
97+
Error: Usage of layout immediate/immediate64 in f_immediate64 can't be erased.
98+
This error is produced due to the use of -only-erasable-extensions.
99+
|}];;
100+
101+
module type S = sig
102+
val f_immediate64 : ('a : immediate64) -> 'a -> 'a
103+
end;;
104+
[%%expect {|
105+
Line 2, characters 2-52:
106+
2 | val f_immediate64 : ('a : immediate64) -> 'a -> 'a
107+
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
108+
Error: Usage of layout immediate/immediate64 in f_immediate64 can't be erased.
109+
This error is produced due to the use of -only-erasable-extensions.
110+
|}];;
111+
112+
module type S = sig
113+
type ('a : immediate64) t
114+
end;;
115+
[%%expect {|
116+
Line 2, characters 2-27:
117+
2 | type ('a : immediate64) t
118+
^^^^^^^^^^^^^^^^^^^^^^^^^
119+
Error: Usage of layout immediate/immediate64 in t can't be erased.
120+
This error is produced due to the use of -only-erasable-extensions.
121+
|}];;
122+
123+
module type S = sig
124+
type _ g = | MkG : ('a : immediate64). 'a g
125+
end;;
126+
[%%expect {|
127+
Line 2, characters 2-45:
128+
2 | type _ g = | MkG : ('a : immediate64). 'a g
129+
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
130+
Error: Usage of layout immediate/immediate64 in g can't be erased.
131+
This error is produced due to the use of -only-erasable-extensions.
132+
|}];;
133+
134+
let f (type a : immediate64): a -> a = fun x -> x
135+
[%%expect {|
136+
Line 1, characters 4-5:
137+
1 | let f (type a : immediate64): a -> a = fun x -> x
138+
^
139+
Error: Usage of layout immediate/immediate64 in f can't be erased.
140+
This error is produced due to the use of -only-erasable-extensions.
141+
|}];;
142+
143+
let f x = (x : (_ : immediate64))
144+
[%%expect {|
145+
Line 1, characters 4-5:
146+
1 | let f x = (x : (_ : immediate64))
147+
^
148+
Error: Usage of layout immediate/immediate64 in f can't be erased.
149+
This error is produced due to the use of -only-erasable-extensions.
150+
|}];;
151+
152+
let f v: ((_ : immediate64)[@error_message "Custom message"]) = v
153+
[%%expect {|
154+
Line 1, characters 4-5:
155+
1 | let f v: ((_ : immediate64)[@error_message "Custom message"]) = v
156+
^
157+
Error: Usage of layout immediate/immediate64 in f can't be erased.
158+
This error is produced due to the use of -only-erasable-extensions.
159+
|}];;
160+
161+
(* CR layouts: This message should change after we fix the package hack.
162+
But it should still be an error under [-only-erasable-extensions]. *)
163+
module type S = sig
164+
type t[@@immediate64]
165+
end
166+
167+
module type K = sig
168+
val f : 'a -> (module S with type t = 'a) -> 'a
169+
end
170+
171+
[%%expect {|
172+
module type S = sig type t : immediate64 end
173+
Line 6, characters 16-43:
174+
6 | val f : 'a -> (module S with type t = 'a) -> 'a
175+
^^^^^^^^^^^^^^^^^^^^^^^^^^^
176+
Error: In this `with' constraint, the new definition of t
177+
does not match its original definition in the constrained signature:
178+
Type declarations do not match:
179+
type t
180+
is not included in
181+
type t : immediate64
182+
The layout of the first is value, because
183+
it's a type declaration in a first-class module.
184+
But the layout of the first must be a sublayout of immediate64, because
185+
of the definition of t at line 2, characters 2-23.
186+
|}];;
187+
188+
(* Annotations here do nothing and should be accepted *)
189+
module type S = sig
190+
val f : (int as (_ : immediate)) -> (int as (_ : immediate64))
191+
end
192+
193+
[%%expect {|
194+
module type S = sig val f : int -> int end
195+
|}];;
196+
197+
198+
(* Annotation would affect ['a] and should be rejected *)
199+
module type S = sig
200+
type 'b id = 'b
201+
val f : ('a id as (_ : immediate)) -> 'a
202+
end
203+
204+
[%%expect {|
205+
Line 3, characters 2-42:
206+
3 | val f : ('a id as (_ : immediate)) -> 'a
207+
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
208+
Error: Usage of layout immediate/immediate64 in f can't be erased.
209+
This error is produced due to the use of -only-erasable-extensions.
210+
|}];;
211+
212+
(* Other annotations are not effected by this flag *)
213+
module type S = sig
214+
val f_any : ('a : any). ('a : any) -> (('a : any)[@error_message ""])
215+
type ('a : any) t_any : any
216+
type (_ : any) t_any_ = MkG : ('a : any). 'a t_any_
217+
val f_bits64 : ('a : bits64). ('a : bits64) -> (('a : bits64)[@error_message ""])
218+
type ('a : bits64) t_bits64 : bits64
219+
type (_ : bits64) t_bits64_ = MkG : ('a : bits64). 'a t_bits64_
220+
val f_bits32 : ('a : bits32). ('a : bits32) -> (('a : bits32)[@error_message ""])
221+
type ('a : bits32) t_bits32 : bits32
222+
type (_ : bits32) t_bits32_ = MkG : ('a : bits32). 'a t_bits32_
223+
val f_float64 : ('a : float64). ('a : float64) -> (('a : float64)[@error_message ""])
224+
type ('a : float64) t_float64 : float64
225+
type (_ : float64) t_float64_ = MkG : ('a : float64). 'a t_float64_
226+
val f_word : ('a : word). ('a : word) -> (('a : word)[@error_message ""])
227+
type ('a : word) t_word : word
228+
type (_ : word) t_word_ = MkG : ('a : word). 'a t_word_
229+
end
230+
231+
module M = struct
232+
let f_any (type a : any) = ()
233+
let f_bits64 (type a : bits64) = ()
234+
let f_bits32 (type a : bits32) = ()
235+
let f_float64 (type a : float64) = ()
236+
let f_word (type a : word) = ()
237+
end
238+
[%%expect {|
239+
module type S =
240+
sig
241+
val f_any : ('a : any). 'a -> 'a
242+
type ('a : any) t_any : any
243+
type (_ : any) t_any_ = MkG : ('a : any). 'a t_any_
244+
val f_bits64 : ('a : bits64). 'a -> 'a
245+
type ('a : bits64) t_bits64 : bits64
246+
type (_ : bits64) t_bits64_ = MkG : ('a : bits64). 'a t_bits64_
247+
val f_bits32 : ('a : bits32). 'a -> 'a
248+
type ('a : bits32) t_bits32 : bits32
249+
type (_ : bits32) t_bits32_ = MkG : ('a : bits32). 'a t_bits32_
250+
val f_float64 : ('a : float64). 'a -> 'a
251+
type ('a : float64) t_float64 : float64
252+
type (_ : float64) t_float64_ = MkG : ('a : float64). 'a t_float64_
253+
val f_word : ('a : word). 'a -> 'a
254+
type ('a : word) t_word : word
255+
type (_ : word) t_word_ = MkG : ('a : word). 'a t_word_
256+
end
257+
module M :
258+
sig
259+
val f_any : unit
260+
val f_bits64 : unit
261+
val f_bits32 : unit
262+
val f_float64 : unit
263+
val f_word : unit
264+
end
265+
|}];;

‎typing/ctype.ml

+44-4
Original file line numberDiff line numberDiff line change
@@ -2018,7 +2018,7 @@ let rec estimate_type_jkind env ty =
20182018
This notably prevents [constrain_type_jkind] from changing layout
20192019
[any] to a sort or changing the externality once the Tvar gets
20202020
generalized.
2021-
2021+
20222022
This, however, still allows sort variables to get instantiated. *)
20232023
Jkind jkind
20242024
| Tvar { jkind } -> TyVar (jkind, ty)
@@ -2162,16 +2162,56 @@ let unification_jkind_check env ty jkind =
21622162
| Delay_checks r -> r := (ty,jkind) :: !r
21632163
| Skip_checks -> ()
21642164

2165-
let update_generalized_ty_jkind_reason ty reason =
2165+
exception Incompatible_with_erasability_requirements of
2166+
Ident.t option * Location.t
2167+
2168+
let () =
2169+
Location.register_error_of_exn (function
2170+
| Incompatible_with_erasability_requirements (id, loc) ->
2171+
let format_id ppf = function
2172+
| Some id -> Format.fprintf ppf " in %s" (Ident.name id)
2173+
| None -> ()
2174+
in
2175+
Some (Location.errorf ~loc
2176+
"@[Usage of layout immediate/immediate64%a can't be erased.@;\
2177+
This error is produced due to the use of -only-erasable-extensions.@]"
2178+
format_id id)
2179+
| _ -> None)
2180+
2181+
let check_and_update_generalized_ty_jkind ?name ~loc ty =
2182+
let immediacy_check jkind =
2183+
let is_immediate jkind =
2184+
let snap = Btype.snapshot () in
2185+
let result =
2186+
Result.is_ok (
2187+
Jkind.sub
2188+
jkind
2189+
(Jkind.immediate64 ~why:Erasability_check))
2190+
in
2191+
Btype.backtrack snap;
2192+
result
2193+
in
2194+
if Language_extension.erasable_extensions_only ()
2195+
&& is_immediate jkind
2196+
then
2197+
raise (Incompatible_with_erasability_requirements (name, loc))
2198+
else ()
2199+
in
21662200
let rec inner ty =
21672201
let level = get_level ty in
21682202
if level = generic_level && try_mark_node ty then begin
21692203
begin match get_desc ty with
21702204
| Tvar ({ jkind; _ } as r) ->
2171-
let new_jkind = Jkind.(update_reason jkind reason) in
2205+
immediacy_check jkind;
2206+
let new_jkind =
2207+
Jkind.(update_reason jkind (Generalized (name, loc)))
2208+
in
21722209
set_type_desc ty (Tvar {r with jkind = new_jkind})
21732210
| Tunivar ({ jkind; _ } as r) ->
2174-
let new_jkind = Jkind.(update_reason jkind reason) in
2211+
immediacy_check jkind;
2212+
let new_jkind =
2213+
Jkind.(update_reason jkind (Generalized (name, loc)))
2214+
in
21752215
set_type_desc ty (Tunivar {r with jkind = new_jkind})
21762216
| _ -> ()
21772217
end;

0 commit comments

Comments
 (0)