Skip to content

Commit

Permalink
Charge also dcs of local reaches to capture set of enclosing method (#…
Browse files Browse the repository at this point in the history
  • Loading branch information
Linyxus authored Aug 26, 2024
2 parents dd37503 + 98a41c2 commit c0cfd0f
Show file tree
Hide file tree
Showing 9 changed files with 49 additions and 16 deletions.
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

0 comments on commit c0cfd0f

Please sign in to comment.