Skip to content

Commit

Permalink
Fix soundness hole of forgotten reach capabilities
Browse files Browse the repository at this point in the history
  • Loading branch information
odersky committed Jun 4, 2024
1 parent 9b5ab2e commit 6e6f3be
Show file tree
Hide file tree
Showing 6 changed files with 40 additions and 8 deletions.
17 changes: 12 additions & 5 deletions compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
Original file line number Diff line number Diff line change
Expand Up @@ -369,11 +369,18 @@ class CheckCaptures extends Recheck, SymTransformer:
inline def isVisibleFromEnv(sym: Symbol) = !isContainedInEnv(sym)
// Only captured references that are visible from the environment
// should be included.
val included = cs.filter:
case ref: TermRef => isVisibleFromEnv(ref.symbol.owner)
case ref: ThisType => isVisibleFromEnv(ref.cls)
case _ => false
capt.println(i"Include call capture $included in ${env.owner}")
val included = cs.filter: c =>
c.stripReach match
case ref: TermRef =>
val isVisible = isVisibleFromEnv(ref.symbol.owner)
if !isVisible && c.isReach then
// Reach capabilities that go out of scope have to be approximated
// by their underlyiong capture set. See i20503.scala.
checkSubset(CaptureSet.ofInfo(c), env.captured, pos, provenance(env))
isVisible
case ref: ThisType => isVisibleFromEnv(ref.cls)
case _ => false
capt.println(i"Include call or box capture $included from $cs in ${env.owner}")
checkSubset(included, env.captured, pos, provenance(env))

/** Include references captured by the called method in the current environment stack */
Expand Down
10 changes: 10 additions & 0 deletions tests/neg-custom-args/captures/reaches2.check
Original file line number Diff line number Diff line change
@@ -0,0 +1,10 @@
-- Error: tests/neg-custom-args/captures/reaches2.scala:8:10 -----------------------------------------------------------
8 | ps.map((x, y) => compose1(x, y)) // error // error
| ^
|reference (ps : List[(box A => A, box A => A)]) @reachCapability is not included in the allowed capture set {}
|of an enclosing function literal with expected type ((box A ->{ps*} A, box A ->{ps*} A)) -> box (x$0: A^?) ->? A^?
-- Error: tests/neg-custom-args/captures/reaches2.scala:8:13 -----------------------------------------------------------
8 | ps.map((x, y) => compose1(x, y)) // error // error
| ^
|reference (ps : List[(box A => A, box A => A)]) @reachCapability is not included in the allowed capture set {}
|of an enclosing function literal with expected type ((box A ->{ps*} A, box A ->{ps*} A)) -> box (x$0: A^?) ->? A^?
9 changes: 9 additions & 0 deletions tests/neg-custom-args/captures/reaches2.scala
Original file line number Diff line number Diff line change
@@ -0,0 +1,9 @@
class List[+A]:
def map[B](f: A -> B): List[B] = ???

def compose1[A, B, C](f: A => B, g: B => C): A ->{f, g} C =
z => g(f(z))

def mapCompose[A](ps: List[(A => A, A => A)]): List[A ->{ps*} A] =
ps.map((x, y) => compose1(x, y)) // error // error

6 changes: 6 additions & 0 deletions tests/neg/i20503.scala
Original file line number Diff line number Diff line change
@@ -0,0 +1,6 @@
import language.experimental.captureChecking
def runOps(ops: List[() => Unit]): Unit =
ops.foreach(op => op())

def main(): Unit =
val f: List[() => Unit] -> Unit = runOps // error
2 changes: 1 addition & 1 deletion tests/neg/unsound-reach-2.scala
Original file line number Diff line number Diff line change
Expand Up @@ -19,7 +19,7 @@ def bad(): Unit =
var escaped: File^{backdoor*} = null
withFile("hello.txt"): f =>
boom.use(f): // error
new Consumer[File^{backdoor*}]:
new Consumer[File^{backdoor*}]: // error
def apply(f1: File^{backdoor*}) =
escaped = f1

4 changes: 2 additions & 2 deletions tests/pos-custom-args/captures/reaches.scala
Original file line number Diff line number Diff line change
Expand Up @@ -45,8 +45,8 @@ def compose1[A, B, C](f: A => B, g: B => C): A ->{f, g} C =
def compose2[A, B, C](f: A => B, g: B => C): A => C =
z => g(f(z))

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

@annotation.capability class IO

Expand Down

0 comments on commit 6e6f3be

Please sign in to comment.