Skip to content

Commit

Permalink
Allow only reach capabilities of parameters in deep capture sets
Browse files Browse the repository at this point in the history
  • Loading branch information
odersky committed Oct 15, 2024
1 parent e007539 commit af9ecad
Show file tree
Hide file tree
Showing 11 changed files with 63 additions and 13 deletions.
14 changes: 9 additions & 5 deletions compiler/src/dotty/tools/dotc/cc/CaptureOps.scala
Original file line number Diff line number Diff line change
Expand Up @@ -232,14 +232,11 @@ extension (tp: Type)
*/
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(_) if reachCanSubsumDcs =>
case tp @ ReachCapability(_) if tp.isParamPath =>
tp.singletonCaptureSet
case tp: SingletonCaptureRef if tp.isTrackableRef && reachCanSubsumDcs =>
case tp: SingletonCaptureRef if tp.isTrackableRef && tp.isParamPath =>
tp.reach.singletonCaptureSet
case _ =>
tp.captureSet ++ dcs
Expand Down Expand Up @@ -297,6 +294,13 @@ extension (tp: Type)
case tp1: ThisType => tp1.cls
case _ => NoSymbol

final def isParamPath(using Context): Boolean = tp.dealias match
case tp1: NamedType =>
tp1.prefix match
case _: ThisType | NoPrefix => tp1.symbol.isOneOf(Param | ParamAccessor)
case prefix => prefix.isParamPath
case _ => false

/** 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
8 changes: 7 additions & 1 deletion compiler/src/dotty/tools/dotc/cc/CaptureSet.scala
Original file line number Diff line number Diff line change
Expand Up @@ -1119,12 +1119,18 @@ object CaptureSet:
* replaces caps with reach capabilties.
*/
def ofTypeDeeply(tp: Type)(using Context): CaptureSet =
object ReachesMap extends IdempotentCaptRefMap:
def apply(t: Type): Type = t match
case ReachCapability(ref) if !ref.isParamPath =>
defn.Caps_CapSet.typeRef.capturing(ref.deepCaptureSet)
case _ =>
t
val collect = new TypeAccumulator[CaptureSet]:
def apply(cs: CaptureSet, t: Type) =
if variance <= 0 then cs
else t.dealias match
case t @ CapturingType(p, cs1) =>
this(cs, p) ++ cs1
this(cs, p) ++ cs1.map(ReachesMap)
case t @ AnnotatedType(parent, ann) =>
this(cs, parent)
case t @ FunctionOrMethod(args, res @ Existential(_, _))
Expand Down
3 changes: 2 additions & 1 deletion compiler/src/dotty/tools/dotc/cc/Setup.scala
Original file line number Diff line number Diff line change
Expand Up @@ -751,7 +751,8 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI:
report.warning(em"redundant capture: $dom already accounts for $ref", pos)

if ref.captureSetOfInfo.elems.isEmpty && !ref.derivesFrom(defn.Caps_Capability) then
report.error(em"$ref cannot be tracked since its capture set is empty", pos)
val deepStr = if ref.isReach then " deep" else ""
report.error(em"$ref cannot be tracked since its$deepStr capture set is empty", pos)
check(parent.captureSet, parent)

val others =
Expand Down
10 changes: 10 additions & 0 deletions tests/neg-custom-args/captures/delayedRunops.check
Original file line number Diff line number Diff line change
Expand Up @@ -3,3 +3,13 @@
| ^^^^
| reference ops* is not included in the allowed capture set {}
| of an enclosing function literal with expected type () -> Unit
-- Error: tests/neg-custom-args/captures/delayedRunops.scala:21:13 -----------------------------------------------------
21 | runOps(ops1) // error
| ^^^^
| reference (caps.cap : caps.Capability) is not included in the allowed capture set {}
| of an enclosing function literal with expected type () -> Unit
-- Error: tests/neg-custom-args/captures/delayedRunops.scala:27:13 -----------------------------------------------------
27 | runOps(ops1) // error
| ^^^^
| reference ops* is not included in the allowed capture set {}
| of an enclosing function literal with expected type () -> Unit
12 changes: 12 additions & 0 deletions tests/neg-custom-args/captures/delayedRunops.scala
Original file line number Diff line number Diff line change
Expand Up @@ -13,3 +13,15 @@ import language.experimental.captureChecking
() =>
val ops1 = ops
runOps(ops1) // error

// unsound: impure operation pretended pure
def delayedRunOps2(ops: List[() => Unit]): () ->{} Unit =
() =>
val ops1: List[() => Unit] = ops
runOps(ops1) // error

// unsound: impure operation pretended pure
def delayedRunOps3(ops: List[() => Unit]): () ->{} Unit =
() =>
val ops1: List[() ->{ops*} Unit] = ops
runOps(ops1) // error
12 changes: 12 additions & 0 deletions tests/neg-custom-args/captures/delayedRunops2.scala
Original file line number Diff line number Diff line change
Expand Up @@ -8,3 +8,15 @@ def app[T, U](x: T, op: T => U): () ->{op} U =

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

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

def unsafeRunOps2(ops: List[() => Unit]): () -> Unit =
app2[List[() => Unit], Unit](ops, runOps: List[() => Unit] -> Unit) // error




4 changes: 2 additions & 2 deletions tests/neg-custom-args/captures/reaches.check
Original file line number Diff line number Diff line change
Expand Up @@ -47,8 +47,8 @@
-- Error: tests/neg-custom-args/captures/reaches.scala:60:31 -----------------------------------------------------------
60 | val leaked = usingFile[File^{id*}]: f => // error
| ^^^
| id* cannot be tracked since its capture set is empty
| id* cannot be tracked since its deep capture set is empty
-- Error: tests/neg-custom-args/captures/reaches.scala:61:18 -----------------------------------------------------------
61 | val f1: File^{id*} = id(f) // error, since now id(f): File^ // error
| ^^^
| id* cannot be tracked since its capture set is empty
| id* cannot be tracked since its deep capture set is empty
4 changes: 4 additions & 0 deletions tests/neg-custom-args/captures/wf-reach-1.check
Original file line number Diff line number Diff line change
@@ -0,0 +1,4 @@
-- Error: tests/neg-custom-args/captures/wf-reach-1.scala:2:17 ---------------------------------------------------------
2 | val y: Object^{x*} = ??? // error
| ^^
| x* cannot be tracked since its deep capture set is empty
2 changes: 2 additions & 0 deletions tests/neg-custom-args/captures/wf-reach-1.scala
Original file line number Diff line number Diff line change
@@ -0,0 +1,2 @@
def test(x: List[() -> Unit]) =
val y: Object^{x*} = ??? // error
7 changes: 3 additions & 4 deletions tests/neg/leak-problem.scala
Original file line number Diff line number Diff line change
Expand Up @@ -15,8 +15,7 @@ def useBoxedAsync(x: Box[Async^]): Unit =

def useBoxedAsync1(x: Box[Async^]): Unit = x.get.read() // now ok

def test(): Unit =
val xs: Box[Async^] = ???
def test(xs: Box[Async^]): Unit =
val xsLambda = () => useBoxedAsync(xs)
val _: () ->{xs*} Unit = xsLambda
val _: () -> Unit = xsLambda // error
Expand All @@ -27,8 +26,8 @@ def test(): Unit =
t1.read()

val xsLambda2 = () => useBoxedAsync2(xs)
val _: () ->{xs*} Unit = xsLambda
val _: () -> Unit = xsLambda // error
val _: () ->{xs*} Unit = xsLambda2
val _: () -> Unit = xsLambda2 // error

val f: Box[Async^] => Unit = (x: Box[Async^]) => useBoxedAsync(x)

Expand Down
File renamed without changes.

0 comments on commit af9ecad

Please sign in to comment.