Skip to content

Commit db9b45f

Browse files
authored
Prevent fatal errors related to regions (#2096)
1 parent 17a7795 commit db9b45f

File tree

10 files changed

+119
-39
lines changed

10 files changed

+119
-39
lines changed

middle_end/flambda2/simplify/inlining/inlining_transforms.ml

Lines changed: 47 additions & 35 deletions
Original file line numberDiff line numberDiff line change
@@ -114,38 +114,50 @@ let inline dacc ~apply ~unroll_to ~was_inline_always function_decl =
114114
| Need_meet -> Rec_info_expr.unknown
115115
| Invalid -> (* CR vlaviron: ? *) Rec_info_expr.do_not_inline
116116
in
117-
let denv =
118-
DE.enter_inlined_apply ~called_code:code ~apply ~was_inline_always denv
119-
in
120-
let params_and_body = Code.params_and_body code in
121-
Function_params_and_body.pattern_match params_and_body
122-
~f:(fun
123-
~return_continuation
124-
~exn_continuation
125-
params
126-
~body
127-
~my_closure
128-
~is_my_closure_used:_
129-
~my_region
130-
~my_depth
131-
~free_names_of_body:_
132-
->
133-
let make_inlined_body () =
134-
make_inlined_body ~callee ~region_inlined_into ~unroll_to
135-
~params:(Bound_parameters.to_list params)
136-
~args ~my_closure ~my_region ~my_depth ~rec_info ~body
137-
~exn_continuation ~return_continuation
138-
in
139-
let expr =
140-
match Exn_continuation.extra_args apply_exn_continuation with
141-
| [] ->
142-
make_inlined_body ()
143-
~apply_exn_continuation:
144-
(Exn_continuation.exn_handler apply_exn_continuation)
145-
~apply_return_continuation
146-
| extra_args ->
147-
wrap_inlined_body_for_exn_extra_args ~extra_args
148-
~apply_exn_continuation ~apply_return_continuation
149-
~result_arity:(Code.result_arity code) ~make_inlined_body
150-
in
151-
DA.with_denv dacc denv, expr)
117+
match region_inlined_into, Code.result_mode code with
118+
| Heap, Alloc_local ->
119+
(* The alloc_mode of the application and of the code are incompatible. This
120+
should have been prevented by the typer; therefore we are in GADT-caused
121+
unreachable code; we replace the inlined body by [Invalid]. *)
122+
( dacc,
123+
Expr.create_invalid
124+
(Flambda.Invalid.Calling_local_returning_closure_with_normal_apply apply)
125+
)
126+
| Local _, Alloc_heap (* This is allowed by subtyping *)
127+
| Local _, Alloc_local
128+
| Heap, Alloc_heap ->
129+
let denv =
130+
DE.enter_inlined_apply ~called_code:code ~apply ~was_inline_always denv
131+
in
132+
let params_and_body = Code.params_and_body code in
133+
Function_params_and_body.pattern_match params_and_body
134+
~f:(fun
135+
~return_continuation
136+
~exn_continuation
137+
params
138+
~body
139+
~my_closure
140+
~is_my_closure_used:_
141+
~my_region
142+
~my_depth
143+
~free_names_of_body:_
144+
->
145+
let make_inlined_body () =
146+
make_inlined_body ~callee ~region_inlined_into ~unroll_to
147+
~params:(Bound_parameters.to_list params)
148+
~args ~my_closure ~my_region ~my_depth ~rec_info ~body
149+
~exn_continuation ~return_continuation
150+
in
151+
let expr =
152+
match Exn_continuation.extra_args apply_exn_continuation with
153+
| [] ->
154+
make_inlined_body ()
155+
~apply_exn_continuation:
156+
(Exn_continuation.exn_handler apply_exn_continuation)
157+
~apply_return_continuation
158+
| extra_args ->
159+
wrap_inlined_body_for_exn_extra_args ~extra_args
160+
~apply_exn_continuation ~apply_return_continuation
161+
~result_arity:(Code.result_arity code) ~make_inlined_body
162+
in
163+
DA.with_denv dacc denv, expr)

middle_end/flambda2/simplify/simplify_apply_expr.ml

Lines changed: 18 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -421,14 +421,28 @@ let simplify_direct_partial_application ~simplify_expr dacc apply
421421
let new_closure_alloc_mode, first_complex_local_param =
422422
if num_non_unarized_args <= first_complex_local_param
423423
then
424+
(* At this point, we *have* to allocate the closure on the heap, even if
425+
the alloc_mode of the application was local. Indeed, consider a
426+
three-argument function, of type [string -> string -> string ->
427+
string], coerced to [string -> local_ t] where [type t = string ->
428+
string -> string].
429+
430+
If we apply this function twice to single arguments, the first
431+
application will have a local alloc_mode. However, the second
432+
application has a heap alloc_mode, and contains a reference to the
433+
partial closure made by the first application. Due to this, the first
434+
application must have a closure allocated on the heap as well, even
435+
though it was with a local alloc_mode. *)
424436
( Alloc_mode.For_allocations.heap,
425437
first_complex_local_param - num_non_unarized_args )
426438
else
427439
match (apply_alloc_mode : Alloc_mode.For_allocations.t) with
428440
| Heap ->
429-
Misc.fatal_errorf "Partial application of %a with wrong mode at %s"
430-
Code_id.print callee's_code_id
431-
(Debuginfo.to_string (Apply.dbg apply))
441+
Misc.fatal_errorf
442+
"Partial application of %a with wrong mode:@.apply = \
443+
%a@callee's_code_metadata = %a@."
444+
Code_id.print callee's_code_id Apply.print apply Code_metadata.print
445+
callee's_code_metadata
432446
| Local _ -> apply_alloc_mode, 0
433447
in
434448
(match closure_alloc_mode_from_type with
@@ -637,7 +651,7 @@ let simplify_direct_partial_application ~simplify_expr dacc apply
637651
applied_values
638652
|> Value_slot.Map.of_list
639653
in
640-
( Set_of_closures.create ~value_slots apply_alloc_mode function_decls,
654+
( Set_of_closures.create ~value_slots new_closure_alloc_mode function_decls,
641655
dacc,
642656
code_id,
643657
code )

middle_end/flambda2/terms/flambda.ml

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1432,6 +1432,7 @@ module Invalid = struct
14321432
| Apply_cont_of_unreachable_continuation of Continuation.t
14331433
| Defining_expr_of_let of Bound_pattern.t * Named.t
14341434
| Closure_type_was_invalid of Apply_expr.t
1435+
| Calling_local_returning_closure_with_normal_apply of Apply_expr.t
14351436
| Zero_switch_arms
14361437
| Code_not_rebuilt
14371438
| To_cmm_dummy_body
@@ -1456,6 +1457,11 @@ module Invalid = struct
14561457
Format.asprintf
14571458
"@[<hov 1>(Closure_type_was_invalid@ @[<hov 1>(apply_expr@ %a)@])@]"
14581459
Apply_expr.print apply_expr
1460+
| Calling_local_returning_closure_with_normal_apply apply_expr ->
1461+
Format.asprintf
1462+
"@[<hov 1>(Calling_local_returning_closure_with_normal_apply@ @[<hov \
1463+
1>(apply_expr@ %a)@])@]"
1464+
Apply_expr.print apply_expr
14591465
| Zero_switch_arms -> "Zero_switch_arms"
14601466
| Code_not_rebuilt -> "Code_not_rebuilt"
14611467
| To_cmm_dummy_body -> "To_cmm_dummy_body"

middle_end/flambda2/terms/flambda.mli

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -106,6 +106,7 @@ module Invalid : sig
106106
| Apply_cont_of_unreachable_continuation of Continuation.t
107107
| Defining_expr_of_let of Bound_pattern.t * named
108108
| Closure_type_was_invalid of Apply_expr.t
109+
| Calling_local_returning_closure_with_normal_apply of Apply_expr.t
109110
| Zero_switch_arms
110111
| Code_not_rebuilt
111112
| To_cmm_dummy_body
Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
1+
(* TEST *)
2+
3+
type (_, _) eq = Eq : ('a, 'a) eq
4+
5+
let[@inline always] cast (type a b) (x : a) (Eq : (a, b) eq) : b = x
6+
7+
let test (f : local_ 'a -> local_ 'b) (eq : (local_ 'a -> local_ 'b, 'a -> 'b) eq) (x : 'a) : 'b =
8+
(cast f eq) x
9+
10+
type 'a box = Box of 'a
11+
12+
let localf : (local_ 'a -> local_ 'a box) = fun x -> exclave_ (local_ (Box x))
13+
14+
let g eq x = test localf eq x

ocaml/testsuite/tests/typing-local/local_gadt.reference

Whitespace-only changes.
Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
(* TEST *)
2+
3+
type 'a box = Box of 'a
4+
module X : sig
5+
val f : int -> string -> local_ int box
6+
end = struct
7+
let[@inline never] f x y = exclave_ (local_ (Box x))
8+
end
9+
10+
let[@inline always] h x = x
11+
12+
let g a = (h X.f) a

ocaml/testsuite/tests/typing-local/partial_app_bug.reference

Whitespace-only changes.
Lines changed: 20 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,20 @@
1+
(* TEST *)
2+
3+
type 'a box = Box of 'a
4+
5+
let[@inline never] f x y z =
6+
match x, y, z with Box x, Box y, Box z -> x + y + z
7+
8+
type t = int box -> int box -> int
9+
let[@inline always] h x = x
10+
let g = (h f :> int box -> local_ t)
11+
12+
let[@inline never] go a b c =
13+
let local_ g1 = (g a) in
14+
let g2 = (g1 b) in
15+
g2 c
16+
17+
let[@inline never] test () =
18+
Format.eprintf "%d@." (go (Box 1) (Box 2) (Box 3))
19+
20+
let () = test ()
Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
6

0 commit comments

Comments
 (0)