Skip to content

Commit 913c5bb

Browse files
committed
Handle reach capabilities correctly in markFree
The correct point to address charging reach capabilities is in markFree itself: When a reach capability goes out of scope, and that capability is not a parameter, we need to continue with the underlying capture set.
1 parent f6f178b commit 913c5bb

25 files changed

+323
-114
lines changed

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

Lines changed: 30 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -221,19 +221,22 @@ extension (tp: Type)
221221
case tp: SingletonCaptureRef => tp.captureSetOfInfo
222222
case _ => CaptureSet.ofType(tp, followResult = false)
223223

224-
/** The deep capture set of a type.
225-
* For singleton capabilities `x` and reach capabilities `x*`, this is `{x*}`, provided
226-
* the underlying capture set resulting from traversing the type is non-empty.
227-
* For other types this is the union of all covariant capture sets embedded
228-
* in the type, as computed by `CaptureSet.ofTypeDeeply`.
224+
/** The deep capture set of a type. This is by default the union of all
225+
* covariant capture sets embedded in the widened type, as computed by
226+
* `CaptureSet.ofTypeDeeply`. If that set is nonempty, and the type is
227+
* a singleton capability `x` or a reach capability `x*`, the deep capture
228+
* set can be narrowed to`{x*}`.
229229
*/
230230
def deepCaptureSet(using Context): CaptureSet =
231231
val dcs = CaptureSet.ofTypeDeeply(tp.widen.stripCapturing)
232232
if dcs.isAlwaysEmpty then tp.captureSet
233233
else tp match
234-
case tp @ ReachCapability(_) => tp.singletonCaptureSet
235-
case tp: SingletonCaptureRef if tp.isTrackableRef => tp.reach.singletonCaptureSet
236-
case _ => tp.captureSet ++ dcs
234+
case tp @ ReachCapability(_) =>
235+
tp.singletonCaptureSet
236+
case tp: SingletonCaptureRef if tp.isTrackableRef =>
237+
tp.reach.singletonCaptureSet
238+
case _ =>
239+
tp.captureSet ++ dcs
237240

238241
/** A type capturing `ref` */
239242
def capturing(ref: CaptureRef)(using Context): Type =
@@ -274,10 +277,28 @@ extension (tp: Type)
274277
tp
275278

276279
/** The first element of this path type */
277-
final def pathRoot(using Context): Type = tp.dealias match
280+
final def pathRoot(using Context): Type = tp.dealiasKeepAnnots match
278281
case tp1: NamedType if tp1.symbol.owner.isClass => tp1.prefix.pathRoot
282+
case ReachCapability(tp1) => tp1.pathRoot
279283
case _ => tp
280284

285+
/** If this part starts with `C.this`, the class `C`.
286+
* Otherwise, if it starts with a reference `r`, `r`'s owner.
287+
* Otherwise NoSymbol.
288+
*/
289+
final def pathOwner(using Context): Symbol = pathRoot match
290+
case tp1: NamedType => tp1.symbol.owner
291+
case tp1: ThisType => tp1.cls
292+
case _ => NoSymbol
293+
294+
final def isParamPath(using Context): Boolean = tp.dealias match
295+
case tp1: NamedType =>
296+
tp1.prefix match
297+
case _: ThisType | NoPrefix =>
298+
tp1.symbol.is(Param) || tp1.symbol.is(ParamAccessor)
299+
case prefix => prefix.isParamPath
300+
case _ => false
301+
281302
/** If this is a unboxed capturing type with nonempty capture set, its boxed version.
282303
* Or, if type is a TypeBounds of capturing types, the version where the bounds are boxed.
283304
* The identity for all other types.

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

Lines changed: 70 additions & 64 deletions
Original file line numberDiff line numberDiff line change
@@ -328,20 +328,22 @@ class CheckCaptures extends Recheck, SymTransformer:
328328
then CaptureSet.Var(sym.owner, level = sym.ccLevel)
329329
else CaptureSet.empty)
330330

331-
/** For all nested environments up to `limit` or a closed environment perform `op`,
332-
* but skip environmenrts directly enclosing environments of kind ClosureResult.
331+
/** The next environment enclosing `env` that needs to be charged
332+
* with free references.
333+
* Skips environments directly enclosing environments of kind ClosureResult.
334+
* @param included Whether an environment is included in the range of
335+
* environments to charge. Once `included` is false, no
336+
* more environments need to be charged.
333337
*/
334-
def forallOuterEnvsUpTo(limit: Symbol)(op: Env => Unit)(using Context): Unit =
335-
def recur(env: Env, skip: Boolean): Unit =
336-
if env.isOpen && env.owner != limit then
337-
if !skip then op(env)
338-
if !env.isOutermost then
339-
var nextEnv = env.outer
340-
if env.owner.isConstructor then
341-
if nextEnv.owner != limit && !nextEnv.isOutermost then
342-
nextEnv = nextEnv.outer
343-
recur(nextEnv, skip = env.kind == EnvKind.ClosureResult)
344-
recur(curEnv, skip = false)
338+
def nextEnvToCharge(env: Env, included: Env => Boolean)(using Context): Env =
339+
var nextEnv = env.outer
340+
if env.owner.isConstructor then
341+
if included(nextEnv) then nextEnv = nextEnv.outer
342+
if env.kind == EnvKind.ClosureResult then
343+
// skip this one
344+
nextEnvToCharge(nextEnv, included)
345+
else
346+
nextEnv
345347

346348
/** A description where this environment comes from */
347349
private def provenance(env: Env)(using Context): String =
@@ -355,7 +357,6 @@ class CheckCaptures extends Recheck, SymTransformer:
355357
else
356358
i"\nof the enclosing ${owner.showLocated}"
357359

358-
359360
/** Include `sym` in the capture sets of all enclosing environments nested in the
360361
* the environment in which `sym` is defined.
361362
*/
@@ -364,9 +365,12 @@ class CheckCaptures extends Recheck, SymTransformer:
364365

365366
def markFree(sym: Symbol, ref: TermRef, pos: SrcPos)(using Context): Unit =
366367
if sym.exists && ref.isTracked then
367-
forallOuterEnvsUpTo(sym.enclosure): env =>
368-
capt.println(i"Mark $sym with cs ${ref.captureSet} free in ${env.owner}")
369-
checkElem(ref, env.captured, pos, provenance(env))
368+
def recur(env: Env): Unit =
369+
if env.isOpen && env.owner != sym.enclosure then
370+
capt.println(i"Mark $sym with cs ${ref.captureSet} free in ${env.owner}")
371+
checkElem(ref, env.captured, pos, provenance(env))
372+
recur(nextEnvToCharge(env, _.owner != sym.enclosure))
373+
recur(curEnv)
370374

371375
/** Make sure (projected) `cs` is a subset of the capture sets of all enclosing
372376
* environments. At each stage, only include references from `cs` that are outside
@@ -381,46 +385,53 @@ class CheckCaptures extends Recheck, SymTransformer:
381385
else
382386
!sym.isContainedIn(env.owner)
383387

384-
def checkSubsetEnv(cs: CaptureSet, env: Env)(using Context): Unit =
385-
// Only captured references that are visible from the environment
386-
// should be included.
387-
val included = cs.filter: c =>
388-
c.stripReach match
389-
case ref: NamedType =>
390-
val refSym = ref.symbol
391-
val refOwner = refSym.owner
392-
val isVisible = isVisibleFromEnv(refOwner, env)
393-
if isVisible && !ref.isRootCapability then
394-
ref match
395-
case ref: TermRef if ref.prefix `ne` NoPrefix =>
396-
// If c is a path of a class defined outside the environment,
397-
// we check the capture set of its info.
398-
checkSubsetEnv(ref.captureSetOfInfo, env)
399-
case _ =>
400-
if !isVisible
401-
&& (c.isReach || ref.isType)
402-
&& (!ccConfig.useSealed || refSym.is(Param))
403-
&& refOwner == env.owner
404-
then
405-
if refSym.hasAnnotation(defn.UnboxAnnot) then
406-
capt.println(i"exempt: $ref in $refOwner")
407-
else
408-
// Reach capabilities that go out of scope have to be approximated
409-
// by their underlying capture set, which cannot be universal.
410-
// Reach capabilities of @unboxed parameters are exempted.
411-
val cs = CaptureSet.ofInfo(c)
412-
cs.disallowRootCapability: () =>
413-
report.error(em"Local reach capability $c leaks into capture scope of ${env.ownerString}", pos)
414-
checkSubset(cs, env.captured, pos, provenance(env))
415-
isVisible
416-
case ref: ThisType => isVisibleFromEnv(ref.cls, env)
417-
case _ => false
418-
checkSubset(included, env.captured, pos, provenance(env))
419-
capt.println(i"Include call or box capture $included from $cs in ${env.owner} --> ${env.captured}")
420-
421-
if !cs.isAlwaysEmpty then
422-
forallOuterEnvsUpTo(ctx.owner.topLevelClass): env =>
423-
checkSubsetEnv(cs, env)
388+
def checkUseDeclared(c: CaptureRef, env: Env) =
389+
c.pathRoot match
390+
case ref: NamedType if !ref.symbol.hasAnnotation(defn.UnboxAnnot) =>
391+
val what = if ref.isType then "Capture set parameter" else "Local reach capability"
392+
report.error(
393+
em"""$what $c leaks into capture scope of ${env.ownerString}.
394+
|To allow this, the ${ref.symbol} should be declared with a @use annotation""", pos)
395+
case _ =>
396+
397+
def recur(cs: CaptureSet, env: Env)(using Context): Unit =
398+
if env.isOpen && !env.owner.isStaticOwner && !cs.isAlwaysEmpty then
399+
// Only captured references that are visible from the environment
400+
// should be included.
401+
val included = cs.filter: c =>
402+
val isVisible = c.pathRoot match
403+
case ref: NamedType => isVisibleFromEnv(ref.symbol.owner, env)
404+
case ref: ThisType => isVisibleFromEnv(ref.cls, env)
405+
case ref =>
406+
false
407+
if !isVisible then
408+
c match
409+
case ReachCapability(c1) =>
410+
if c1.isParamPath then
411+
checkUseDeclared(c, env)
412+
else
413+
// When a reach capabilty x* where `x` is not a parameter goes out
414+
// of scope, we need to continue with `x`'s underlying deep capture set.
415+
// It is an error if that set contains cap.
416+
// The same is not an issue for normal capabilities since in a local
417+
// definition `val x = e`, the capabilities of `e` have already been charged.
418+
// Note: It's not true that the underlying capture set of a reach capability
419+
// is always cap. Reach capabilities over paths depend on the prefix, which
420+
// might turn a cap into something else.
421+
// The path-use.scala neg test contains an example.
422+
val underlying = CaptureSet.ofTypeDeeply(c1.widen)
423+
capt.println(i"Widen reach $c to $underlying in ${env.owner}")
424+
underlying.disallowRootCapability: () =>
425+
report.error(em"Local reach capability $c leaks into capture scope of ${env.ownerString}", pos)
426+
recur(underlying, env)
427+
case c: TypeRef if c.isParamPath =>
428+
checkUseDeclared(c, env)
429+
case _ =>
430+
isVisible
431+
checkSubset(included, env.captured, pos, provenance(env))
432+
capt.println(i"Include call or box capture $included from $cs in ${env.owner} --> ${env.captured}")
433+
recur(included, nextEnvToCharge(env, !_.owner.isStaticOwner))
434+
recur(cs, curEnv)
424435
end markFree
425436

426437
/** Include references captured by the called method in the current environment stack */
@@ -1139,13 +1150,8 @@ class CheckCaptures extends Recheck, SymTransformer:
11391150
(erefs /: erefs.elems): (erefs, eref) =>
11401151
eref match
11411152
case eref: ThisType if isPureContext(ctx.owner, eref.cls) =>
1142-
def isOuterRef(aref: Type): Boolean = aref.pathRoot match
1143-
case aref: NamedType => eref.cls.isProperlyContainedIn(aref.symbol.owner)
1144-
case aref: ThisType => eref.cls.isProperlyContainedIn(aref.cls)
1145-
case _ => false
1146-
1147-
val outerRefs = arefs.filter(isOuterRef)
1148-
1153+
val outerRefs = arefs.filter: aref =>
1154+
eref.cls.isProperlyContainedIn(aref.pathOwner)
11491155
// Include implicitly added outer references in the capture set of the class of `eref`.
11501156
for outerRef <- outerRefs.elems do
11511157
if !erefs.elems.contains(outerRef)

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

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -751,7 +751,8 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI:
751751
report.warning(em"redundant capture: $dom already accounts for $ref", pos)
752752

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

757758
val others =

scala2-library-cc/src/scala/collection/Iterator.scala

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1159,7 +1159,8 @@ object Iterator extends IterableFactory[Iterator] {
11591159
// If we advanced the current iterator to a ConcatIterator, merge it into this one
11601160
@tailrec def merge(): Unit =
11611161
if (current.isInstanceOf[ConcatIterator[_]]) {
1162-
val c = current.asInstanceOf[ConcatIterator[A]]
1162+
val c: ConcatIterator[A] { val from: Iterator[A] }
1163+
= current.asInstanceOf
11631164
current = c.current.asInstanceOf // !!! CC unsafe op
11641165
currentHasNextChecked = c.currentHasNextChecked
11651166
if (c.tail != null) {
Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
1+
-- Error: tests/neg-custom-args/captures/delayedRunops.scala:16:13 -----------------------------------------------------
2+
16 | runOps(ops1) // error
3+
| ^^^^
4+
| reference ops* is not included in the allowed capture set {}
5+
| of an enclosing function literal with expected type () -> Unit
6+
-- Error: tests/neg-custom-args/captures/delayedRunops.scala:22:13 -----------------------------------------------------
7+
22 | runOps(ops1) // error
8+
| ^^^^
9+
| Local reach capability ops1* leaks into capture scope of enclosing function
10+
-- Error: tests/neg-custom-args/captures/delayedRunops.scala:28:13 -----------------------------------------------------
11+
28 | runOps(ops1) // error
12+
| ^^^^
13+
| reference ops* is not included in the allowed capture set {}
14+
| of an enclosing function literal with expected type () -> Unit
Lines changed: 28 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,28 @@
1+
import language.experimental.captureChecking
2+
import caps.unbox
3+
4+
// ok
5+
def runOps(@unbox ops: List[() => Unit]): Unit =
6+
ops.foreach(op => op())
7+
8+
// ok
9+
def delayedRunOps(@unbox ops: List[() => Unit]): () ->{ops*} Unit = // @unbox should not be necessary in the future
10+
() => runOps(ops)
11+
12+
// unsound: impure operation pretended pure
13+
def delayedRunOps1(ops: List[() => Unit]): () ->{} Unit =
14+
() =>
15+
val ops1 = ops
16+
runOps(ops1) // error
17+
18+
// unsound: impure operation pretended pure
19+
def delayedRunOps2(ops: List[() => Unit]): () ->{} Unit =
20+
() =>
21+
val ops1: List[() => Unit] = ops
22+
runOps(ops1) // error
23+
24+
// unsound: impure operation pretended pure
25+
def delayedRunOps3(ops: List[() => Unit]): () ->{} Unit =
26+
() =>
27+
val ops1: List[() ->{ops*} Unit] = ops
28+
runOps(ops1) // error
Lines changed: 55 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,55 @@
1+
-- Error: tests/neg-custom-args/captures/i16114.scala:18:12 ------------------------------------------------------------
2+
18 | expect[Cap^] { // error
3+
| ^^^^^^^^^^^^
4+
| Sealed type variable T cannot be instantiated to box Cap^ since
5+
| that type captures the root capability `cap`.
6+
| This is often caused by a local capability in an argument of method expect
7+
| leaking as part of its result.
8+
-- Error: tests/neg-custom-args/captures/i16114.scala:20:8 -------------------------------------------------------------
9+
20 | fs // error (limitation)
10+
| ^^
11+
| (fs : Cap^) cannot be referenced here; it is not included in the allowed capture set {io}
12+
| of an enclosing function literal with expected type Unit ->{io} Unit
13+
-- Error: tests/neg-custom-args/captures/i16114.scala:24:12 ------------------------------------------------------------
14+
24 | expect[Cap^] { // error
15+
| ^^^^^^^^^^^^
16+
| Sealed type variable T cannot be instantiated to box Cap^ since
17+
| that type captures the root capability `cap`.
18+
| This is often caused by a local capability in an argument of method expect
19+
| leaking as part of its result.
20+
-- Error: tests/neg-custom-args/captures/i16114.scala:26:8 -------------------------------------------------------------
21+
26 | io // error (limitation)
22+
| ^^
23+
| (io : Cap^) cannot be referenced here; it is not included in the allowed capture set {fs}
24+
| of an enclosing function literal with expected type Unit ->{fs} Unit
25+
-- Error: tests/neg-custom-args/captures/i16114.scala:30:12 ------------------------------------------------------------
26+
30 | expect[Cap^] { // error
27+
| ^^^^^^^^^^^^
28+
| Sealed type variable T cannot be instantiated to box Cap^ since
29+
| that type captures the root capability `cap`.
30+
| This is often caused by a local capability in an argument of method expect
31+
| leaking as part of its result.
32+
-- Error: tests/neg-custom-args/captures/i16114.scala:36:12 ------------------------------------------------------------
33+
36 | expect[Cap^](io) // error
34+
| ^^^^^^^^^^^^
35+
| Sealed type variable T cannot be instantiated to box Cap^ since
36+
| that type captures the root capability `cap`.
37+
| This is often caused by a local capability in an argument of method expect
38+
| leaking as part of its result.
39+
-- Error: tests/neg-custom-args/captures/i16114.scala:39:12 ------------------------------------------------------------
40+
39 | expect[Cap^] { // error
41+
| ^^^^^^^^^^^^
42+
| Sealed type variable T cannot be instantiated to box Cap^ since
43+
| that type captures the root capability `cap`.
44+
| This is often caused by a local capability in an argument of method expect
45+
| leaking as part of its result.
46+
-- Error: tests/neg-custom-args/captures/i16114.scala:40:8 -------------------------------------------------------------
47+
40 | io.use() // error
48+
| ^^
49+
| (io : Cap^) cannot be referenced here; it is not included in the allowed capture set {}
50+
| of an enclosing function literal with expected type Unit -> Unit
51+
-- Error: tests/neg-custom-args/captures/i16114.scala:41:8 -------------------------------------------------------------
52+
41 | io // error
53+
| ^^
54+
| (io : Cap^) cannot be referenced here; it is not included in the allowed capture set {}
55+
| of an enclosing function literal with expected type Unit -> Unit
Lines changed: 4 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -1,15 +1,12 @@
11
-- Error: tests/neg-custom-args/captures/i21347.scala:4:15 -------------------------------------------------------------
22
4 | ops.foreach: op => // error
33
| ^
4-
| Local reach capability C leaks into capture scope of method runOps
4+
| Capture set parameter C leaks into capture scope of method runOps.
5+
| To allow this, the type C should be declared with a @use annotation
56
5 | op()
6-
-- Error: tests/neg-custom-args/captures/i21347.scala:8:14 -------------------------------------------------------------
7-
8 | () => runOps(f :: Nil) // error
8-
| ^^^^^^^^^^^^^^^^
9-
| reference (caps.cap : caps.Capability) is not included in the allowed capture set {}
10-
| of an enclosing function literal with expected type () -> Unit
117
-- Error: tests/neg-custom-args/captures/i21347.scala:11:15 ------------------------------------------------------------
128
11 | ops.foreach: op => // error
139
| ^
14-
| Local reach capability ops* leaks into capture scope of method runOpsAlt
10+
| Local reach capability ops* leaks into capture scope of method runOpsAlt.
11+
| To allow this, the parameter ops should be declared with a @use annotation
1512
12 | op()

tests/neg-custom-args/captures/i21347.scala

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -5,7 +5,7 @@ def runOps[C^](ops: List[() ->{C^} Unit]): Unit =
55
op()
66

77
def boom(f: () => Unit): () -> Unit =
8-
() => runOps(f :: Nil) // error
8+
() => runOps(f :: Nil) // now ok
99

1010
def runOpsAlt(ops: List[() => Unit]): Unit =
1111
ops.foreach: op => // error

0 commit comments

Comments
 (0)