From 0b08c981dacf7295980c234ac461e6af1c75b11d Mon Sep 17 00:00:00 2001 From: odersky Date: Mon, 26 Aug 2024 20:58:13 +0200 Subject: [PATCH 1/2] Charge also dcs of local reaches to capture set of enclosing method Fixes #21442 --- .../dotty/tools/dotc/cc/CheckCaptures.scala | 2 +- tests/neg-custom-args/captures/i21442.check | 8 +++++++ tests/neg-custom-args/captures/i21442.scala | 18 +++++++++++++++ tests/neg-custom-args/captures/reaches.check | 22 +++++++++---------- tests/neg-custom-args/captures/reaches.scala | 2 +- .../captures/unsound-reach.check | 5 +++++ .../captures/unsound-reach.scala | 2 +- 7 files changed, 44 insertions(+), 15 deletions(-) create mode 100644 tests/neg-custom-args/captures/i21442.check create mode 100644 tests/neg-custom-args/captures/i21442.scala diff --git a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala index 384c6e1f29ef..ec134149eb49 100644 --- a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala +++ b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala @@ -394,7 +394,7 @@ class CheckCaptures extends Recheck, SymTransformer: val isVisible = isVisibleFromEnv(refOwner) if !isVisible && (c.isReach || ref.isType) - && refSym.is(Param) + && (!ccConfig.useSealed || refSym.is(Param)) && refOwner == env.owner then if refSym.hasAnnotation(defn.UnboxAnnot) then diff --git a/tests/neg-custom-args/captures/i21442.check b/tests/neg-custom-args/captures/i21442.check new file mode 100644 index 000000000000..a3bbf65c5988 --- /dev/null +++ b/tests/neg-custom-args/captures/i21442.check @@ -0,0 +1,8 @@ +-- Error: tests/neg-custom-args/captures/i21442.scala:9:13 ------------------------------------------------------------- +9 | val io = x.unbox // error: local reach capability {x*} leaks + | ^^^^^^^ + | Local reach capability x* leaks into capture scope of method foo +-- Error: tests/neg-custom-args/captures/i21442.scala:17:14 ------------------------------------------------------------ +17 | val io = x1.unbox // error + | ^^^^^^^^ + | Local reach capability x1* leaks into capture scope of method bar diff --git a/tests/neg-custom-args/captures/i21442.scala b/tests/neg-custom-args/captures/i21442.scala new file mode 100644 index 000000000000..c9fa7d152fae --- /dev/null +++ b/tests/neg-custom-args/captures/i21442.scala @@ -0,0 +1,18 @@ +import language.experimental.captureChecking +trait IO: + def use(): Unit +case class Boxed[+T](unbox: T) + +// `foo` is a function that unboxes its parameter +// and uses the capability boxed inside the parameter. +def foo(x: Boxed[IO^]): Unit = + val io = x.unbox // error: local reach capability {x*} leaks + io.use() + +// `bar` is a function that does the same thing in a +// slightly different way. +// But, no type error reported. +def bar(x: Boxed[IO^]): Unit = + val x1: Boxed[IO^] = x + val io = x1.unbox // error + io.use() diff --git a/tests/neg-custom-args/captures/reaches.check b/tests/neg-custom-args/captures/reaches.check index aa45c738dcc5..f00fea09ed8c 100644 --- a/tests/neg-custom-args/captures/reaches.check +++ b/tests/neg-custom-args/captures/reaches.check @@ -25,18 +25,10 @@ | ^^^^^^^^^^^^ | The expression's type box () => Unit is not allowed to capture the root capability `cap`. | This usually means that a capability persists longer than its allowed lifetime. --- [E007] Type Mismatch Error: tests/neg-custom-args/captures/reaches.scala:53:2 --------------------------------------- -53 | val id: Id[Proc, Proc] = new Id[Proc, () -> Unit] // error - | ^ - | Found: box () => Unit - | Required: () => Unit - | - | Note that box () => Unit cannot be box-converted to () => Unit - | since at least one of their capture sets contains the root capability `cap` -54 | usingFile: f => -55 | id(() => f.write()) - | - | longer explanation available when compiling with `-explain` +-- Error: tests/neg-custom-args/captures/reaches.scala:55:6 ------------------------------------------------------------ +55 | id(() => f.write()) // error + | ^^^^^^^^^^^^^^^^^^^ + | Local reach capability id* leaks into capture scope of method test -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/reaches.scala:62:27 -------------------------------------- 62 | val f1: File^{id*} = id(f) // error, since now id(f): File^ | ^^^^^ @@ -52,3 +44,9 @@ 79 | ps.map((x, y) => compose1(x, y)) // error // error | ^ | Local reach capability ps* leaks into capture scope of method mapCompose +-- [E057] Type Mismatch Error: tests/neg-custom-args/captures/reaches.scala:53:51 -------------------------------------- +53 | val id: Id[Proc, Proc] = new Id[Proc, () -> Unit] // error + | ^ + | Type argument () -> Unit does not conform to lower bound () => Unit + | + | longer explanation available when compiling with `-explain` diff --git a/tests/neg-custom-args/captures/reaches.scala b/tests/neg-custom-args/captures/reaches.scala index c2d8001e2a7c..c33ba80a668b 100644 --- a/tests/neg-custom-args/captures/reaches.scala +++ b/tests/neg-custom-args/captures/reaches.scala @@ -52,7 +52,7 @@ class Id[-A, +B >: A](): def test = val id: Id[Proc, Proc] = new Id[Proc, () -> Unit] // error usingFile: f => - id(() => f.write()) + id(() => f.write()) // error def attack2 = val id: File^ -> File^ = x => x diff --git a/tests/neg-custom-args/captures/unsound-reach.check b/tests/neg-custom-args/captures/unsound-reach.check index f0e4c4deeb41..4a6793d204c5 100644 --- a/tests/neg-custom-args/captures/unsound-reach.check +++ b/tests/neg-custom-args/captures/unsound-reach.check @@ -1,3 +1,8 @@ +-- Error: tests/neg-custom-args/captures/unsound-reach.scala:18:21 ----------------------------------------------------- +18 | boom.use(f): (f1: File^{backdoor*}) => // error + | ^ + | Local reach capability backdoor* leaks into capture scope of method bad +19 | escaped = f1 -- [E164] Declaration Error: tests/neg-custom-args/captures/unsound-reach.scala:10:8 ----------------------------------- 10 | def use(x: File^)(op: File^ => Unit): Unit = op(x) // error, was OK using sealed checking | ^ diff --git a/tests/neg-custom-args/captures/unsound-reach.scala b/tests/neg-custom-args/captures/unsound-reach.scala index 22ed4614b71b..c3c31a7f32ff 100644 --- a/tests/neg-custom-args/captures/unsound-reach.scala +++ b/tests/neg-custom-args/captures/unsound-reach.scala @@ -15,6 +15,6 @@ def bad(): Unit = var escaped: File^{backdoor*} = null withFile("hello.txt"): f => - boom.use(f): (f1: File^{backdoor*}) => // was error before existentials + boom.use(f): (f1: File^{backdoor*}) => // error escaped = f1 From 98a41c2efcdfeb4999429d51356a5d3b643f49b7 Mon Sep 17 00:00:00 2001 From: odersky Date: Mon, 26 Aug 2024 23:17:32 +0200 Subject: [PATCH 2/2] Fix test --- tests/neg-custom-args/captures/i21401.check | 4 ++++ tests/neg-custom-args/captures/i21401.scala | 2 +- 2 files changed, 5 insertions(+), 1 deletion(-) diff --git a/tests/neg-custom-args/captures/i21401.check b/tests/neg-custom-args/captures/i21401.check index e9a5fbd4678c..e204540358ce 100644 --- a/tests/neg-custom-args/captures/i21401.check +++ b/tests/neg-custom-args/captures/i21401.check @@ -8,3 +8,7 @@ | ^^^^^^^^^^^^^^^^^^^ | The expression's type Res is not allowed to capture the root capability `cap` in its part box IO^. | This usually means that a capability persists longer than its allowed lifetime. +-- Error: tests/neg-custom-args/captures/i21401.scala:18:21 ------------------------------------------------------------ +18 | val y: IO^{x*} = x.unbox // error + | ^^^^^^^ + | Local reach capability x* leaks into capture scope of method test2 diff --git a/tests/neg-custom-args/captures/i21401.scala b/tests/neg-custom-args/captures/i21401.scala index 07d407a79809..8284c601cd5f 100644 --- a/tests/neg-custom-args/captures/i21401.scala +++ b/tests/neg-custom-args/captures/i21401.scala @@ -15,5 +15,5 @@ def test2() = val a = usingIO[IO^](x => x) // error: The expression's type IO^ is not allowed to capture the root capability `cap` val leaked: [R, X <: Boxed[IO^] -> R] -> (op: X) -> R = usingIO[Res](mkRes) // error: The expression's type Res is not allowed to capture the root capability `cap` in its part box IO^ val x: Boxed[IO^] = leaked[Boxed[IO^], Boxed[IO^] -> Boxed[IO^]](x => x) - val y: IO^{x*} = x.unbox + val y: IO^{x*} = x.unbox // error y.println("boom")