Skip to content

Commit 7abb3d9

Browse files
authored
Fix soundness hole of forgotten reach capabilities (#20524)
Fixes #20503
2 parents c51345f + 6e6f3be commit 7abb3d9

File tree

6 files changed

+40
-8
lines changed

6 files changed

+40
-8
lines changed

compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala

+12-5
Original file line numberDiff line numberDiff line change
@@ -371,11 +371,18 @@ class CheckCaptures extends Recheck, SymTransformer:
371371
inline def isVisibleFromEnv(sym: Symbol) = !isContainedInEnv(sym)
372372
// Only captured references that are visible from the environment
373373
// should be included.
374-
val included = cs.filter:
375-
case ref: TermRef => isVisibleFromEnv(ref.symbol.owner)
376-
case ref: ThisType => isVisibleFromEnv(ref.cls)
377-
case _ => false
378-
capt.println(i"Include call capture $included in ${env.owner}")
374+
val included = cs.filter: c =>
375+
c.stripReach match
376+
case ref: TermRef =>
377+
val isVisible = isVisibleFromEnv(ref.symbol.owner)
378+
if !isVisible && c.isReach then
379+
// Reach capabilities that go out of scope have to be approximated
380+
// by their underlyiong capture set. See i20503.scala.
381+
checkSubset(CaptureSet.ofInfo(c), env.captured, pos, provenance(env))
382+
isVisible
383+
case ref: ThisType => isVisibleFromEnv(ref.cls)
384+
case _ => false
385+
capt.println(i"Include call or box capture $included from $cs in ${env.owner}")
379386
checkSubset(included, env.captured, pos, provenance(env))
380387

381388
/** Include references captured by the called method in the current environment stack */
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
-- Error: tests/neg-custom-args/captures/reaches2.scala:8:10 -----------------------------------------------------------
2+
8 | ps.map((x, y) => compose1(x, y)) // error // error
3+
| ^
4+
|reference (ps : List[(box A => A, box A => A)]) @reachCapability is not included in the allowed capture set {}
5+
|of an enclosing function literal with expected type ((box A ->{ps*} A, box A ->{ps*} A)) -> box (x$0: A^?) ->? A^?
6+
-- Error: tests/neg-custom-args/captures/reaches2.scala:8:13 -----------------------------------------------------------
7+
8 | ps.map((x, y) => compose1(x, y)) // error // error
8+
| ^
9+
|reference (ps : List[(box A => A, box A => A)]) @reachCapability is not included in the allowed capture set {}
10+
|of an enclosing function literal with expected type ((box A ->{ps*} A, box A ->{ps*} A)) -> box (x$0: A^?) ->? A^?
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
class List[+A]:
2+
def map[B](f: A -> B): List[B] = ???
3+
4+
def compose1[A, B, C](f: A => B, g: B => C): A ->{f, g} C =
5+
z => g(f(z))
6+
7+
def mapCompose[A](ps: List[(A => A, A => A)]): List[A ->{ps*} A] =
8+
ps.map((x, y) => compose1(x, y)) // error // error
9+

tests/neg/i20503.scala

+6
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,6 @@
1+
import language.experimental.captureChecking
2+
def runOps(ops: List[() => Unit]): Unit =
3+
ops.foreach(op => op())
4+
5+
def main(): Unit =
6+
val f: List[() => Unit] -> Unit = runOps // error

tests/neg/unsound-reach-2.scala

+1-1
Original file line numberDiff line numberDiff line change
@@ -19,7 +19,7 @@ def bad(): Unit =
1919
var escaped: File^{backdoor*} = null
2020
withFile("hello.txt"): f =>
2121
boom.use(f): // error
22-
new Consumer[File^{backdoor*}]:
22+
new Consumer[File^{backdoor*}]: // error
2323
def apply(f1: File^{backdoor*}) =
2424
escaped = f1
2525

tests/pos-custom-args/captures/reaches.scala

+2-2
Original file line numberDiff line numberDiff line change
@@ -45,8 +45,8 @@ def compose1[A, B, C](f: A => B, g: B => C): A ->{f, g} C =
4545
def compose2[A, B, C](f: A => B, g: B => C): A => C =
4646
z => g(f(z))
4747

48-
def mapCompose[A](ps: List[(A => A, A => A)]): List[A ->{ps*} A] =
49-
ps.map((x, y) => compose1(x, y)) // Does not work if map takes an impure function, see reaches in neg
48+
//def mapCompose[A](ps: List[(A => A, A => A)]): List[A ->{ps*} A] =
49+
// ps.map((x, y) => compose1(x, y)) // Does not work, see neg-customargs/../reaches2.scala
5050

5151
class IO extends caps.Capability
5252

0 commit comments

Comments
 (0)