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

Fix soundness hole of forgotten reach capabilities #20524

Merged
merged 1 commit into from
Jun 4, 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
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
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The following test failed in nightly with Scala 2 libary CC TASTy.

Wrong number of errors encountered when compiling tests/neg/i20503.scala
expected: 1, actual: 2
Unfulfilled expectations:

Unexpected errors:
tests/neg/i20503.scala:3
-> following the errors:
 at 3: Reach capability cap and universal capability cap cannot both
appear in the type [U](f: box (() ->{ops*} Unit) => U): Unit of this expression
 at 6: Found:    (ops: List[box () ->? Unit]^?) => Unit
Required: (ops: List[box () => Unit]) -> Unit

See: https://github.com/scala/scala3/actions/runs/9377502987/job/25819168381

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Fixed by #20528

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