Skip to content

Commit c6e3910

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. With this fix, we don't need any special provisions to compute deep capture sets anymore.
1 parent e007539 commit c6e3910

File tree

11 files changed

+89
-54
lines changed

11 files changed

+89
-54
lines changed

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

Lines changed: 10 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -226,20 +226,15 @@ extension (tp: Type)
226226
* covariant capture sets embedded in the widened type, as computed by
227227
* `CaptureSet.ofTypeDeeply`. If that set is nonempty, and the type is
228228
* a singleton capability `x` or a reach capability `x*`, the deep capture
229-
* set can be narrowed to`{x*}`. However, A deep capture set should not be
230-
* narrowed to a reach capability `x*` if there are elements in the underlying
231-
* set that live longer than `x`. See `delayedRunops.scala` for a test case.
229+
* set can be narrowed to`{x*}`.
232230
*/
233231
def deepCaptureSet(using Context): CaptureSet =
234232
val dcs = CaptureSet.ofTypeDeeply(tp.widen.stripCapturing)
235-
def reachCanSubsumDcs =
236-
dcs.isUniversal
237-
|| dcs.elems.forall(c => c.pathOwner.isContainedIn(tp.pathOwner))
238233
if dcs.isAlwaysEmpty then tp.captureSet
239234
else tp match
240-
case tp @ ReachCapability(_) if reachCanSubsumDcs =>
235+
case tp @ ReachCapability(_) =>
241236
tp.singletonCaptureSet
242-
case tp: SingletonCaptureRef if tp.isTrackableRef && reachCanSubsumDcs =>
237+
case tp: SingletonCaptureRef if tp.isTrackableRef =>
243238
tp.reach.singletonCaptureSet
244239
case _ =>
245240
tp.captureSet ++ dcs
@@ -297,6 +292,13 @@ extension (tp: Type)
297292
case tp1: ThisType => tp1.cls
298293
case _ => NoSymbol
299294

295+
final def isParamPath(using Context): Boolean = tp.dealias match
296+
case tp1: NamedType =>
297+
tp1.prefix match
298+
case _: ThisType | NoPrefix => tp1.symbol.isOneOf(Param | ParamAccessor)
299+
case prefix => prefix.isParamPath
300+
case _ => false
301+
300302
/** If this is a unboxed capturing type with nonempty capture set, its boxed version.
301303
* Or, if type is a TypeBounds of capturing types, the version where the bounds are boxed.
302304
* The identity for all other types.

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

Lines changed: 45 additions & 31 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,20 +385,30 @@ 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.pathRoot match
389-
case ref: NamedType => isVisibleFromEnv(ref.symbol.owner, env)
390-
case ref: ThisType => isVisibleFromEnv(ref.cls, env)
391-
case _ => false
392-
checkSubset(included, env.captured, pos, provenance(env))
393-
capt.println(i"Include call or box capture $included from $cs in ${env.owner} --> ${env.captured}")
394-
395-
if !cs.isAlwaysEmpty then
396-
forallOuterEnvsUpTo(ctx.owner.topLevelClass): env =>
397-
checkSubsetEnv(cs, env)
388+
def recur(cs: CaptureSet, env: Env)(using Context): Unit =
389+
if env.isOpen && !env.owner.isStaticOwner && !cs.isAlwaysEmpty then
390+
// Only captured references that are visible from the environment
391+
// should be included.
392+
val included = cs.filter: c =>
393+
val isVisible = c.stripReach.pathRoot match
394+
case ref: NamedType => isVisibleFromEnv(ref.symbol.owner, env)
395+
case ref: ThisType => isVisibleFromEnv(ref.cls, env)
396+
case _ => false
397+
c match
398+
case ReachCapability(c1) if !isVisible && !c1.isParamPath =>
399+
// When a reach capabilty x* where `x` is not a parameter goes out
400+
// of scope, we need to continue with `x`'s underlying deep capture set.
401+
// The same is not an issue for normal capabilities since in a local
402+
// definition `val x = e`, the capabilities of `e` have already been charged.
403+
val underlying = CaptureSet.ofTypeDeeply(c1.widen)
404+
capt.println(i"Widen reach $c to $underlying in ${env.owner}")
405+
recur(underlying, env)
406+
case _ =>
407+
isVisible
408+
checkSubset(included, env.captured, pos, provenance(env))
409+
capt.println(i"Include call or box capture $included from $cs in ${env.owner} --> ${env.captured}")
410+
recur(included, nextEnvToCharge(env, !_.owner.isStaticOwner))
411+
recur(cs, curEnv)
398412
end markFree
399413

400414
/** Include references captured by the called method in the current environment stack */

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 =

tests/neg-custom-args/captures/delayedRunops.check

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -3,3 +3,13 @@
33
| ^^^^
44
| reference ops* is not included in the allowed capture set {}
55
| of an enclosing function literal with expected type () -> Unit
6+
-- Error: tests/neg-custom-args/captures/delayedRunops.scala:21:13 -----------------------------------------------------
7+
21 | runOps(ops1) // 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
11+
-- Error: tests/neg-custom-args/captures/delayedRunops.scala:27:13 -----------------------------------------------------
12+
27 | runOps(ops1) // error
13+
| ^^^^
14+
| reference ops* is not included in the allowed capture set {}
15+
| of an enclosing function literal with expected type () -> Unit

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

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -13,3 +13,15 @@ import language.experimental.captureChecking
1313
() =>
1414
val ops1 = ops
1515
runOps(ops1) // error
16+
17+
// unsound: impure operation pretended pure
18+
def delayedRunOps2(ops: List[() => Unit]): () ->{} Unit =
19+
() =>
20+
val ops1: List[() => Unit] = ops
21+
runOps(ops1) // error
22+
23+
// unsound: impure operation pretended pure
24+
def delayedRunOps3(ops: List[() => Unit]): () ->{} Unit =
25+
() =>
26+
val ops1: List[() ->{ops*} Unit] = ops
27+
runOps(ops1) // error

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

Lines changed: 0 additions & 10 deletions
This file was deleted.

tests/neg-custom-args/captures/reaches.check

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -47,8 +47,8 @@
4747
-- Error: tests/neg-custom-args/captures/reaches.scala:60:31 -----------------------------------------------------------
4848
60 | val leaked = usingFile[File^{id*}]: f => // error
4949
| ^^^
50-
| id* cannot be tracked since its capture set is empty
50+
| id* cannot be tracked since its deep capture set is empty
5151
-- Error: tests/neg-custom-args/captures/reaches.scala:61:18 -----------------------------------------------------------
5252
61 | val f1: File^{id*} = id(f) // error, since now id(f): File^ // error
5353
| ^^^
54-
| id* cannot be tracked since its capture set is empty
54+
| id* cannot be tracked since its deep capture set is empty
Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,4 @@
1+
-- Error: tests/neg-custom-args/captures/wf-reach-1.scala:2:17 ---------------------------------------------------------
2+
2 | val y: Object^{x*} = ??? // error
3+
| ^^
4+
| x* cannot be tracked since its deep capture set is empty
Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,2 @@
1+
def test(x: List[() -> Unit]) =
2+
val y: Object^{x*} = ??? // error

tests/neg/leak-problem.scala

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -27,8 +27,8 @@ def test(): Unit =
2727
t1.read()
2828

2929
val xsLambda2 = () => useBoxedAsync2(xs)
30-
val _: () ->{xs*} Unit = xsLambda
31-
val _: () -> Unit = xsLambda // error
30+
val _: () ->{xs*} Unit = xsLambda2
31+
val _: () -> Unit = xsLambda2 // error
3232

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

0 commit comments

Comments
 (0)