Skip to content

Commit

Permalink
Fix computation of deep capture set.
Browse files Browse the repository at this point in the history
A deep capture set should not be shortened to a reach capability `x*`
if there are elements in the underlying set that live longer than `x`.
  • Loading branch information
odersky committed Oct 14, 2024
1 parent 1836fb3 commit e007539
Show file tree
Hide file tree
Showing 5 changed files with 58 additions and 15 deletions.
34 changes: 26 additions & 8 deletions compiler/src/dotty/tools/dotc/cc/CaptureOps.scala
Original file line number Diff line number Diff line change
Expand Up @@ -222,19 +222,27 @@ extension (tp: Type)
case tp: SingletonCaptureRef => tp.captureSetOfInfo
case _ => CaptureSet.ofType(tp, followResult = false)

/** The deep capture set of a type.
* For singleton capabilities `x` and reach capabilities `x*`, this is `{x*}`, provided
* the underlying capture set resulting from traversing the type is non-empty.
* For other types this is the union of all covariant capture sets embedded
* in the type, as computed by `CaptureSet.ofTypeDeeply`.
/** The deep capture set of a type. This is by default the union of all
* covariant capture sets embedded in the widened type, as computed by
* `CaptureSet.ofTypeDeeply`. If that set is nonempty, and the type is
* a singleton capability `x` or a reach capability `x*`, the deep capture
* set can be narrowed to`{x*}`. However, A deep capture set should not be
* narrowed to a reach capability `x*` if there are elements in the underlying
* set that live longer than `x`. See `delayedRunops.scala` for a test case.
*/
def deepCaptureSet(using Context): CaptureSet =
val dcs = CaptureSet.ofTypeDeeply(tp.widen.stripCapturing)
def reachCanSubsumDcs =
dcs.isUniversal
|| dcs.elems.forall(c => c.pathOwner.isContainedIn(tp.pathOwner))
if dcs.isAlwaysEmpty then tp.captureSet
else tp match
case tp @ ReachCapability(_) => tp.singletonCaptureSet
case tp: SingletonCaptureRef if tp.isTrackableRef => tp.reach.singletonCaptureSet
case _ => tp.captureSet ++ dcs
case tp @ ReachCapability(_) if reachCanSubsumDcs =>
tp.singletonCaptureSet
case tp: SingletonCaptureRef if tp.isTrackableRef && reachCanSubsumDcs =>
tp.reach.singletonCaptureSet
case _ =>
tp.captureSet ++ dcs

/** A type capturing `ref` */
def capturing(ref: CaptureRef)(using Context): Type =
Expand Down Expand Up @@ -277,8 +285,18 @@ extension (tp: Type)
/** The first element of this path type */
final def pathRoot(using Context): Type = tp.dealias match
case tp1: NamedType if tp1.symbol.owner.isClass => tp1.prefix.pathRoot
case tp1 @ ReachCapability(tp2) => tp2.pathRoot
case _ => tp

/** If this part starts with `C.this`, the class `C`.
* Otherwise, if it starts with a reference `r`, `r`'s owner.
* Otherwise NoSymbol.
*/
final def pathOwner(using Context): Symbol = pathRoot match
case tp1: NamedType => tp1.symbol.owner
case tp1: ThisType => tp1.cls
case _ => NoSymbol

/** If this is a unboxed capturing type with nonempty capture set, its boxed version.
* Or, if type is a TypeBounds of capturing types, the version where the bounds are boxed.
* The identity for all other types.
Expand Down
9 changes: 2 additions & 7 deletions compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
Original file line number Diff line number Diff line change
Expand Up @@ -1090,13 +1090,8 @@ class CheckCaptures extends Recheck, SymTransformer:
(erefs /: erefs.elems): (erefs, eref) =>
eref match
case eref: ThisType if isPureContext(ctx.owner, eref.cls) =>
def isOuterRef(aref: Type): Boolean = aref.pathRoot match
case aref: NamedType => eref.cls.isProperlyContainedIn(aref.symbol.owner)
case aref: ThisType => eref.cls.isProperlyContainedIn(aref.cls)
case _ => false

val outerRefs = arefs.filter(isOuterRef)

val outerRefs = arefs.filter: aref =>
eref.cls.isProperlyContainedIn(aref.pathOwner)
// Include implicitly added outer references in the capture set of the class of `eref`.
for outerRef <- outerRefs.elems do
if !erefs.elems.contains(outerRef)
Expand Down
5 changes: 5 additions & 0 deletions tests/neg-custom-args/captures/delayedRunops.check
Original file line number Diff line number Diff line change
@@ -0,0 +1,5 @@
-- Error: tests/neg-custom-args/captures/delayedRunops.scala:15:13 -----------------------------------------------------
15 | runOps(ops1) // error
| ^^^^
| reference ops* is not included in the allowed capture set {}
| of an enclosing function literal with expected type () -> Unit
15 changes: 15 additions & 0 deletions tests/neg-custom-args/captures/delayedRunops.scala
Original file line number Diff line number Diff line change
@@ -0,0 +1,15 @@
import language.experimental.captureChecking

// ok
def runOps(ops: List[() => Unit]): Unit =
ops.foreach(op => op())

// ok
def delayedRunOps(ops: List[() => Unit]): () ->{ops*} Unit =
() => runOps(ops)

// unsound: impure operation pretended pure
def delayedRunOps1(ops: List[() => Unit]): () ->{} Unit =
() =>
val ops1 = ops
runOps(ops1) // error
10 changes: 10 additions & 0 deletions tests/neg-custom-args/captures/delayedRunops2.scala
Original file line number Diff line number Diff line change
@@ -0,0 +1,10 @@
import language.experimental.captureChecking

def runOps(ops: List[() => Unit]): Unit =
ops.foreach(op => op())

def app[T, U](x: T, op: T => U): () ->{op} U =
() => op(x)

def unsafeRunOps(ops: List[() => Unit]): () ->{} Unit =
app[List[() ->{ops*} Unit], Unit](ops, runOps) // error

0 comments on commit e007539

Please sign in to comment.