Skip to content

Commit

Permalink
flambda-backend: Fix unsound modes in typecore (#2699)
Browse files Browse the repository at this point in the history
* fix modes in typecore

* fix tests
  • Loading branch information
riaqn authored Jun 24, 2024
1 parent 79bb2d8 commit 937f821
Show file tree
Hide file tree
Showing 6 changed files with 132 additions and 72 deletions.
22 changes: 22 additions & 0 deletions testsuite/tests/typing-modes/class.ml
Original file line number Diff line number Diff line change
Expand Up @@ -172,3 +172,25 @@ Line 3, characters 17-20:
^^^
Error: This value is nonportable but expected to be portable.
|}]

let foo () =
let x = object end in
portable_use x
[%%expect{|
Line 3, characters 17-18:
3 | portable_use x
^
Error: This value is nonportable but expected to be portable.
|}]

class cla = object
method m =
let o = {< >} in
portable_use o
end
[%%expect{|
Line 4, characters 21-22:
4 | portable_use o
^
Error: This value is nonportable but expected to be portable.
|}]
6 changes: 4 additions & 2 deletions testsuite/tests/typing-modes/lazy.ml
Original file line number Diff line number Diff line change
Expand Up @@ -6,9 +6,11 @@
let u =
let _x @ portable = lazy "hello" in
()
(* CR zqian: this should fail. *)
[%%expect{|
val u : unit = ()
Line 2, characters 24-36:
2 | let _x @ portable = lazy "hello" in
^^^^^^^^^^^^
Error: This value is nonportable but expected to be portable.
|}]

(* lazy body is legacy *)
Expand Down
95 changes: 95 additions & 0 deletions testsuite/tests/typing-modes/letop.ml
Original file line number Diff line number Diff line change
@@ -0,0 +1,95 @@
(* TEST
expect;
*)

let portable_use : _ @ portable -> unit = fun _ -> ()

let ( let* ) o f =
match o with
| None -> None
| Some x -> f x

let ( and* ) a b =
match a, b with
| Some a, Some b -> Some (a, b)
| _ -> None

[%%expect{|
val portable_use : 'a @ portable -> unit = <fun>
val ( let* ) : 'a option -> ('a -> 'b option) -> 'b option = <fun>
val ( and* ) : 'a option -> 'b option -> ('a * 'b) option = <fun>
|}]

(* bindings are required to be legacy *)
let foo () =
let* a = local_ "hello" in
()
[%%expect{|
Line 2, characters 13-27:
2 | let* a = local_ "hello" in
^^^^^^^^^^^^^^
Error: This value escapes its region.
|}]

let foo () =
let* a = Some "hello"
and* b = local_ "hello" in
()
[%%expect{|
Line 3, characters 13-27:
3 | and* b = local_ "hello" in
^^^^^^^^^^^^^^
Error: This value escapes its region.
|}]

(* Bindings are avialable as legacy *)
let foo () =
let* a = Some (fun x -> x)
and* b = Some (fun x -> x) in
portable_use a
[%%expect{|
Line 4, characters 17-18:
4 | portable_use a
^
Error: This value is nonportable but expected to be portable.
|}]

let foo () =
let* a = Some (fun x -> x)
and* b = Some (fun x -> x) in
portable_use b
[%%expect{|
Line 4, characters 17-18:
4 | portable_use b
^
Error: This value is nonportable but expected to be portable.
|}]

(* Body required to be legacy *)
let foo () =
let _ =
let* a = Some (fun x -> x) in
local_ "hello"
in
()
[%%expect{|
Line 4, characters 8-22:
4 | local_ "hello"
^^^^^^^^^^^^^^
Error: This value escapes its region.
|}]

(* The whole letop is available as legacy *)
let foo () =
portable_use (
let* a = Some (fun x -> x) in
fun x -> x
)
[%%expect{|
Lines 2-5, characters 17-5:
2 | .................(
3 | let* a = Some (fun x -> x) in
4 | fun x -> x
5 | )
Error: This value is nonportable but expected to be portable.
|}]
6 changes: 4 additions & 2 deletions testsuite/tests/typing-modes/module.ml
Original file line number Diff line number Diff line change
Expand Up @@ -117,9 +117,11 @@ val u : unit = ()

(* first class modules are produced at legacy *)
let x = ((module M : SL) : _ @@ portable)
(* CR zqian: this should fail *)
[%%expect{|
val x : (module SL) = <module>
Line 1, characters 9-24:
1 | let x = ((module M : SL) : _ @@ portable)
^^^^^^^^^^^^^^^
Error: This value is nonportable but expected to be portable.
|}]

(* first class modules are consumed at legacy *)
Expand Down
56 changes: 0 additions & 56 deletions testsuite/tests/typing-unique/unique_analysis.ml
Original file line number Diff line number Diff line change
Expand Up @@ -555,62 +555,6 @@ let foo () =
val foo : unit -> unit = <fun>
|}]


(* testing Tpat_lazy *)
let foo () =
match lazy (unique_ "hello") with
| (lazy y) as x -> ignore (shared_id x)
[%%expect{|
val foo : unit -> unit = <fun>
|}]


let foo () =
match lazy (unique_ "hello") with
| (lazy y) as x -> ignore (unique_id x)

[%%expect{|
Line 3, characters 37-38:
3 | | (lazy y) as x -> ignore (unique_id x)
^
Error: This value is used here as unique, but it has already been used:
Line 3, characters 2-10:
3 | | (lazy y) as x -> ignore (unique_id x)
^^^^^^^^

|}]

type 'a r_lazy = {x_lazy : 'a Lazy.t; y : string}

let foo () =
match {x_lazy = lazy (unique_ "hello"); y = "world"} with
| {x_lazy = lazy y} as r -> ignore (unique_id r.x_lazy)
[%%expect{|
type 'a r_lazy = { x_lazy : 'a Lazy.t; y : string; }
Line 5, characters 48-56:
5 | | {x_lazy = lazy y} as r -> ignore (unique_id r.x_lazy)
^^^^^^^^
Error: This value is used here as unique, but it has already been used:
Line 5, characters 14-20:
5 | | {x_lazy = lazy y} as r -> ignore (unique_id r.x_lazy)
^^^^^^

|}]

let foo () =
match {x_lazy = lazy (unique_ "hello"); y = "world"} with
| {x_lazy = lazy y} as r -> ignore (shared_id r.x_lazy)
[%%expect{|
val foo : unit -> unit = <fun>
|}]

let foo () =
match {x_lazy = lazy (unique_ "hello"); y = "world"} with
| {x_lazy = lazy y} as r -> ignore (unique_id r.y)
[%%expect{|
val foo : unit -> unit = <fun>
|}]

(* Testing modalities in records *)
type r_shared = {x : string; y : string @@ shared many}
[%%expect{|
Expand Down
19 changes: 7 additions & 12 deletions typing/typecore.ml
Original file line number Diff line number Diff line change
Expand Up @@ -427,9 +427,6 @@ let meet_regional mode =
let mode = Value.disallow_left mode in
Value.meet [mode; (Value.max_with (Comonadic Areality) Regionality.regional)]

let meet_global mode =
Value.meet [mode; (Value.max_with (Comonadic Areality) Regionality.global)]

let value_regional_to_local mode =
mode
|> value_to_alloc_r2l
Expand Down Expand Up @@ -477,10 +474,6 @@ let mode_with_position mode position =
let mode_max_with_position position =
{ mode_max with position }

let mode_global expected_mode =
let mode = meet_global expected_mode.mode in
{expected_mode with mode}

let mode_exclave expected_mode =
let mode =
Value.join_with (Comonadic Areality)
Expand Down Expand Up @@ -550,10 +543,6 @@ let mode_argument ~funct ~index ~position_and_mode ~partial_app marg =
mode_tailcall_argument vmode, vmode
end

let mode_lazy expected_mode =
{ (mode_global expected_mode) with
position = RTail (Regionality.disallow_left Regionality.global, FTail) }

(* expected_mode.closure_context explains why expected_mode.mode is low;
shared_context explains why mode.uniqueness is high *)
let submode ~loc ~env ?(reason = Other) ?shared_context mode expected_mode =
Expand Down Expand Up @@ -6045,6 +6034,7 @@ and type_expect_
raise(Error(loc, env, Instance_variable_not_mutable lab.txt))
end
| Pexp_override lst ->
submode ~loc ~env Value.legacy expected_mode;
let _ =
List.fold_right
(fun (lab, _) l ->
Expand Down Expand Up @@ -6177,13 +6167,14 @@ and type_expect_
exp_env = env;
}
| Pexp_lazy e ->
submode ~loc ~env Value.legacy expected_mode;
let ty = newgenvar (Jkind.value ~why:Lazy_expression) in
let to_unify = Predef.type_lazy_t ty in
with_explanation (fun () ->
unify_exp_types loc env to_unify (generic_instance ty_expected));
let env = Env.add_escape_lock Lazy env in
let env = Env.add_share_lock Lazy env in
let arg = type_expect env (mode_lazy expected_mode) e (mk_expected ty) in
let arg = type_expect env mode_legacy e (mk_expected ty) in
re {
exp_desc = Texp_lazy arg;
exp_loc = loc; exp_extra = [];
Expand All @@ -6192,6 +6183,7 @@ and type_expect_
exp_env = env;
}
| Pexp_object s ->
submode ~loc ~env Value.legacy expected_mode;
let desc, meths = !type_object env loc s in
rue {
exp_desc = Texp_object (desc, meths);
Expand Down Expand Up @@ -6253,6 +6245,8 @@ and type_expect_
type_newtype_expr ~loc ~env ~expected_mode ~rue ~attributes:sexp.pexp_attributes
name None sbody
| Pexp_pack m ->
(* CR zqian: pass [expected_mode] to [type_package] *)
submode ~loc ~env Value.legacy expected_mode;
let (p, fl) =
match get_desc (Ctype.expand_head env (instance ty_expected)) with
Tpackage (p, fl) ->
Expand Down Expand Up @@ -6292,6 +6286,7 @@ and type_expect_
exp_env = env;
}
| Pexp_letop{ let_ = slet; ands = sands; body = sbody } ->
submode ~loc ~env Value.legacy expected_mode;
let rec loop spat_acc ty_acc ty_acc_sort sands =
match sands with
| [] -> spat_acc, ty_acc, ty_acc_sort
Expand Down

0 comments on commit 937f821

Please sign in to comment.