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
odersky committed Aug 26, 2024
1 parent a2c53a1 commit fc497ee
Show file tree
Hide file tree
Showing 7 changed files with 44 additions and 15 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
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 fc497ee

Please sign in to comment.