@@ -388,6 +388,52 @@ class CheckCaptures extends Recheck, SymTransformer:
388
388
|To allow this, the ${ref.symbol} should be declared with a @use annotation """ , pos)
389
389
case _ =>
390
390
391
+ /** Avoid locally defined capability by charging the underlying type
392
+ * (which may not be cap). This scheme applies only under the deferredReaches setting.
393
+ */
394
+ def avoidLocalCapability (c : CaptureRef , env : Env , lastEnv : Env | Null ): Unit =
395
+ if c.isParamPath then
396
+ c match
397
+ case ReachCapability (_) | _ : TypeRef =>
398
+ checkUseDeclared(c, env, lastEnv)
399
+ case _ =>
400
+ else
401
+ val underlying = c match
402
+ case ReachCapability (c1) =>
403
+ CaptureSet .ofTypeDeeply(c1.widen)
404
+ case _ =>
405
+ CaptureSet .ofType(c.widen, followResult = false )
406
+ capt.println(i " Widen reach $c to $underlying in ${env.owner}" )
407
+ underlying.disallowRootCapability: () =>
408
+ report.error(em " Local capability $c in ${env.ownerString} cannot have `cap` as underlying capture set " , pos)
409
+ recur(underlying, env, lastEnv)
410
+
411
+ /** Avoid locally defined capability if it is a reach capability or capture set
412
+ * parameter. This is the default.
413
+ */
414
+ def avoidLocalReachCapability (c : CaptureRef , env : Env ): Unit = c match
415
+ case ReachCapability (c1) =>
416
+ if c1.isParamPath then
417
+ checkUseDeclared(c, env, null )
418
+ else
419
+ // When a reach capabilty x* where `x` is not a parameter goes out
420
+ // of scope, we need to continue with `x`'s underlying deep capture set.
421
+ // It is an error if that set contains cap.
422
+ // The same is not an issue for normal capabilities since in a local
423
+ // definition `val x = e`, the capabilities of `e` have already been charged.
424
+ // Note: It's not true that the underlying capture set of a reach capability
425
+ // is always cap. Reach capabilities over paths depend on the prefix, which
426
+ // might turn a cap into something else.
427
+ // The path-use.scala neg test contains an example.
428
+ val underlying = CaptureSet .ofTypeDeeply(c1.widen)
429
+ capt.println(i " Widen reach $c to $underlying in ${env.owner}" )
430
+ underlying.disallowRootCapability: () =>
431
+ report.error(em " Local reach capability $c leaks into capture scope of ${env.ownerString}" , pos)
432
+ recur(underlying, env, null )
433
+ case c : TypeRef if c.isParamPath =>
434
+ checkUseDeclared(c, env, null )
435
+ case _ =>
436
+
391
437
def recur (cs : CaptureSet , env : Env , lastEnv : Env | Null ): Unit =
392
438
if env.isOpen && ! env.owner.isStaticOwner && ! cs.isAlwaysEmpty then
393
439
// Only captured references that are visible from the environment
@@ -399,45 +445,9 @@ class CheckCaptures extends Recheck, SymTransformer:
399
445
case ref =>
400
446
false
401
447
if ! isVisible then
402
- // println(i"out of scope: $c")
403
- if ccConfig.deferredReaches then // avoid all locally bound capabilities
404
- if c.isParamPath then
405
- c match
406
- case ReachCapability (_) | _ : TypeRef =>
407
- checkUseDeclared(c, env, lastEnv)
408
- case _ =>
409
- else
410
- val underlying = c match
411
- case ReachCapability (c1) =>
412
- CaptureSet .ofTypeDeeply(c1.widen)
413
- case _ =>
414
- CaptureSet .ofType(c.widen, followResult = false )
415
- capt.println(i " Widen reach $c to $underlying in ${env.owner}" )
416
- underlying.disallowRootCapability: () =>
417
- report.error(em " Local capability $c in ${env.ownerString} cannot have `cap` as underlying capture set " , pos)
418
- recur(underlying, env, lastEnv)
419
- else c match // avoid only reach capabilities and capture sets
420
- case ReachCapability (c1) =>
421
- if c1.isParamPath then
422
- checkUseDeclared(c, env, lastEnv)
423
- else
424
- // When a reach capabilty x* where `x` is not a parameter goes out
425
- // of scope, we need to continue with `x`'s underlying deep capture set.
426
- // It is an error if that set contains cap.
427
- // The same is not an issue for normal capabilities since in a local
428
- // definition `val x = e`, the capabilities of `e` have already been charged.
429
- // Note: It's not true that the underlying capture set of a reach capability
430
- // is always cap. Reach capabilities over paths depend on the prefix, which
431
- // might turn a cap into something else.
432
- // The path-use.scala neg test contains an example.
433
- val underlying = CaptureSet .ofTypeDeeply(c1.widen)
434
- capt.println(i " Widen reach $c to $underlying in ${env.owner}" )
435
- underlying.disallowRootCapability: () =>
436
- report.error(em " Local reach capability $c leaks into capture scope of ${env.ownerString}" , pos)
437
- recur(underlying, env, lastEnv)
438
- case c : TypeRef if c.isParamPath =>
439
- checkUseDeclared(c, env, lastEnv)
440
- case _ =>
448
+ if ccConfig.deferredReaches
449
+ then avoidLocalCapability(c, env, lastEnv)
450
+ else avoidLocalReachCapability(c, env)
441
451
isVisible
442
452
checkSubset(included, env.captured, pos, provenance(env))
443
453
capt.println(i " Include call or box capture $included from $cs in ${env.owner} --> ${env.captured}" )
0 commit comments