Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Charge also dcs of local reaches to capture set of enclosing method #21443

Merged
merged 2 commits into from
Aug 26, 2024
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
4 changes: 4 additions & 0 deletions tests/neg-custom-args/captures/i21401.check
Original file line number Diff line number Diff line change
Expand Up @@ -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
2 changes: 1 addition & 1 deletion tests/neg-custom-args/captures/i21401.scala
Original file line number Diff line number Diff line change
Expand Up @@ -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")
8 changes: 8 additions & 0 deletions tests/neg-custom-args/captures/i21442.check
Original file line number Diff line number Diff line change
@@ -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
18 changes: 18 additions & 0 deletions tests/neg-custom-args/captures/i21442.scala
Original file line number Diff line number Diff line change
@@ -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()
22 changes: 10 additions & 12 deletions tests/neg-custom-args/captures/reaches.check
Original file line number Diff line number Diff line change
Expand Up @@ -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^
| ^^^^^
Expand All @@ -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`
2 changes: 1 addition & 1 deletion tests/neg-custom-args/captures/reaches.scala
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
5 changes: 5 additions & 0 deletions tests/neg-custom-args/captures/unsound-reach.check
Original file line number Diff line number Diff line change
@@ -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
| ^
Expand Down
2 changes: 1 addition & 1 deletion tests/neg-custom-args/captures/unsound-reach.scala
Original file line number Diff line number Diff line change
Expand Up @@ -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