Skip to content

Commit d27f2bb

Browse files
oderskyodersky
committed
Make cap not subsume anything by default.
Exceptions are bracketed in `withCapAsRoot` calls.
1 parent f7484ce commit d27f2bb

17 files changed

+159
-89
lines changed

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

Lines changed: 71 additions & 32 deletions
Original file line numberDiff line numberDiff line change
@@ -100,6 +100,8 @@ class CCState:
100100

101101
private var openExistentialScopes: List[MethodType] = Nil
102102

103+
private var capIsRoot: Boolean = false
104+
103105
object CCState:
104106

105107
opaque type Level = Int
@@ -144,6 +146,21 @@ object CCState:
144146
else
145147
op
146148

149+
/** Run `op` under the assumption that `cap` can subsume all other capabilties
150+
* except Result capabilities. Every use of this method should be scrutinized
151+
* for whether it introduces an unsoundness hole.
152+
*/
153+
inline def withCapAsRoot[T](op: => T)(using Context): T =
154+
if isCaptureCheckingOrSetup then
155+
val ccs = ccState
156+
val saved = ccs.capIsRoot
157+
ccs.capIsRoot = true
158+
try op finally ccs.capIsRoot = saved
159+
else op
160+
161+
/** Is `caps.cap` a root capability that is allowed to subsume other capabilities? */
162+
def capIsRoot(using Context): Boolean = ccState.capIsRoot
163+
147164
/** The currently opened existential scopes */
148165
def openExistentialScopes(using Context): List[MethodType] = ccState.openExistentialScopes
149166

@@ -441,14 +458,30 @@ extension (tp: Type)
441458
case AppliedType(tycon, _) => !defn.isFunctionSymbol(tycon.typeSymbol)
442459
case _ => false
443460

444-
/** Tests whether the type derives from `caps.Capability`, which means
445-
* references of this type are maximal capabilities.
446-
*/
447-
def derivesFromCapTrait(cls: ClassSymbol)(using Context): Boolean = tp.dealias match
461+
/** Tests whether all CapturingType parts of the type that are traversed for
462+
* dcs computation satisfy at least one of two conditions:
463+
* 1. They decorate classes that extend the given capability class `cls`, or
464+
* 2. Their capture set is constant and consists only of capabilities
465+
* the derive from `cls` in the sense of `derivesFromCapTrait`.
466+
*/
467+
def derivesFromCapTraitDeeply(cls: ClassSymbol)(using Context): Boolean =
468+
val accumulate = new DeepTypeAccumulator[Boolean]:
469+
def capturingCase(acc: Boolean, parent: Type, refs: CaptureSet) =
470+
this(acc, parent)
471+
&& (parent.derivesFromCapTrait(cls)
472+
|| refs.isConst && refs.elems.forall(_.derivesFromCapTrait(cls)))
473+
def abstractTypeCase(acc: Boolean, t: TypeRef, upperBound: Type) =
474+
this(acc, upperBound)
475+
accumulate(true, tp)
476+
477+
/** Tests whether the type derives from capability class `cls`. */
478+
def derivesFromCapTrait(cls: ClassSymbol)(using Context): Boolean = tp.dealiasKeepAnnots match
448479
case tp: (TypeRef | AppliedType) =>
449480
val sym = tp.typeSymbol
450481
if sym.isClass then sym.derivesFrom(cls)
451482
else tp.superType.derivesFromCapTrait(cls)
483+
case ReachCapability(tp1) =>
484+
tp1.widen.derivesFromCapTraitDeeply(cls)
452485
case tp: (TypeProxy & ValueType) =>
453486
tp.superType.derivesFromCapTrait(cls)
454487
case tp: AndType =>
@@ -545,7 +578,7 @@ extension (tp: Type)
545578
var change = false
546579
def apply(t: Type) =
547580
if variance <= 0 then t
548-
else t.dealiasKeepAnnots match
581+
else t.dealias match
549582
case t @ CapturingType(p, cs) if cs.containsRootCapability =>
550583
change = true
551584
val reachRef = if cs.isReadOnly then ref.reach.readOnly else ref.reach
@@ -804,33 +837,6 @@ object ReadOnlyCapability extends AnnotatedCapability(defn.ReadOnlyCapabilityAnn
804837
object ReachCapability extends AnnotatedCapability(defn.ReachCapabilityAnnot):
805838
protected def unwrappable(using Context) = Set(defn.MaybeCapabilityAnnot, defn.ReadOnlyCapabilityAnnot)
806839

807-
/** Offers utility method to be used for type maps that follow aliases */
808-
trait ConservativeFollowAliasMap(using Context) extends TypeMap:
809-
810-
/** If `mapped` is a type alias, apply the map to the alias, while keeping
811-
* annotations. If the result is different, return it, otherwise return `mapped`.
812-
* Furthermore, if `original` is a LazyRef or TypeVar and the mapped result is
813-
* the same as the underlying type, keep `original`. This avoids spurious differences
814-
* which would lead to spurious dealiasing in the result
815-
*/
816-
protected def applyToAlias(original: Type, mapped: Type) =
817-
val mapped1 = mapped match
818-
case t: (TypeRef | AppliedType) =>
819-
val t1 = t.dealiasKeepAnnots
820-
if t1 eq t then t
821-
else
822-
// If we see a type alias, map the alias type and keep it if it's different
823-
val t2 = apply(t1)
824-
if t2 ne t1 then t2 else t
825-
case _ =>
826-
mapped
827-
original match
828-
case original: (LazyRef | TypeVar) if mapped1 eq original.underlying =>
829-
original
830-
case _ =>
831-
mapped1
832-
end ConservativeFollowAliasMap
833-
834840
/** An extractor for all kinds of function types as well as method and poly types.
835841
* It includes aliases of function types such as `=>`. TODO: Can we do without?
836842
* @return 1st half: The argument types or empty if this is a type function
@@ -884,3 +890,36 @@ object ContainsParam:
884890
if tycon.typeSymbol == defn.Caps_ContainsTrait
885891
&& cs.typeSymbol.isAbstractOrParamType => Some((cs, ref))
886892
case _ => None
893+
894+
/** A class encapsulating the assumulator logic needed for `CaptureSet.ofTypeDeeply`
895+
* and `derivesFromCapTraitDeeply`.
896+
* NOTE: The traversal logic needs to be in sync with narrowCaps in CaptureOps, which
897+
* replaces caps with reach capabilties. There are two exceptions, however.
898+
* - First, invariant arguments. These have to be included to be conservative
899+
* in dcs but must be excluded in narrowCaps.
900+
* - Second, unconstrained type variables are handled specially in `ofTypeDeeply`.
901+
*/
902+
abstract class DeepTypeAccumulator[T](using Context) extends TypeAccumulator[T]:
903+
val seen = util.HashSet[Symbol]()
904+
905+
protected def capturingCase(acc: T, parent: Type, refs: CaptureSet): T
906+
907+
protected def abstractTypeCase(acc: T, t: TypeRef, upperBound: Type): T
908+
909+
def apply(acc: T, t: Type) =
910+
if variance < 0 then acc
911+
else t.dealias match
912+
case t @ CapturingType(p, cs1) =>
913+
capturingCase(acc, p, cs1)
914+
case t: TypeRef if t.symbol.isAbstractOrParamType && !seen.contains(t.symbol) =>
915+
seen += t.symbol
916+
abstractTypeCase(acc, t, t.info.bounds.hi)
917+
case AnnotatedType(parent, _) =>
918+
this(acc, parent)
919+
case t @ FunctionOrMethod(args, res) =>
920+
if args.forall(_.isAlwaysPure) then this(acc, root.resultToFresh(res))
921+
else acc
922+
case _ =>
923+
foldOver(acc, t)
924+
end DeepTypeAccumulator
925+

‎compiler/src/dotty/tools/dotc/cc/CaptureRef.scala

Lines changed: 14 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -260,10 +260,20 @@ trait CaptureRef extends TypeProxy, ValueType:
260260
ccState.existentialSubsumesFailure.orElse(Some(this, y))
261261
false
262262
case _ =>
263-
this.isCap && !yIsExistential && canAddHidden && vs != VarState.HardSeparate
264-
|| y.match
265-
case ReadOnlyCapability(y1) => this.stripReadOnly.maxSubsumes(y1, canAddHidden)
266-
case _ => false
263+
y match
264+
case ReadOnlyCapability(y1) => this.stripReadOnly.maxSubsumes(y1, canAddHidden)
265+
case _ if this.isCap =>
266+
y.isCap
267+
|| y.derivesFromSharedCapability
268+
|| !yIsExistential
269+
&& canAddHidden
270+
&& vs != VarState.HardSeparate
271+
&& (CCState.capIsRoot
272+
// || { println(i"no longer $this maxSubsumes $y, ${y.isCap}"); false } // debug
273+
)
274+
|| false
275+
case _ =>
276+
false
267277

268278
/** `x covers y` if we should retain `y` when computing the overlap of
269279
* two footprints which have `x` respectively `y` as elements.

‎compiler/src/dotty/tools/dotc/cc/CaptureSet.scala

Lines changed: 17 additions & 32 deletions
Original file line numberDiff line numberDiff line change
@@ -206,7 +206,8 @@ sealed abstract class CaptureSet extends Showable:
206206
*/
207207
def mightAccountFor(x: CaptureRef)(using Context): Boolean =
208208
reporting.trace(i"$this mightAccountFor $x, ${x.captureSetOfInfo}?", show = true):
209-
elems.exists(_.subsumes(x)(using ctx, VarState.ClosedUnrecorded))
209+
CCState.withCapAsRoot: // OK here since we opportunistically choose an alternative which gets checked later
210+
elems.exists(_.subsumes(x)(using ctx, VarState.ClosedUnrecorded))
210211
|| !x.isRootCapability
211212
&& {
212213
val elems = x.captureSetOfInfo.elems
@@ -639,14 +640,15 @@ object CaptureSet:
639640
*/
640641
def solve()(using Context): Unit =
641642
if !isConst then
642-
val approx = upperApprox(empty)
643-
.map(root.CapToFresh(NoSymbol).inverse) // Fresh --> cap
644-
.showing(i"solve $this = $result", capt)
645-
//println(i"solving var $this $approx ${approx.isConst} deps = ${deps.toList}")
646-
val newElems = approx.elems -- elems
647-
given VarState()
648-
if tryInclude(newElems, empty).isOK then
649-
markSolved()
643+
CCState.withCapAsRoot: // // OK here since we infer parameter types that get checked later
644+
val approx = upperApprox(empty)
645+
.map(root.CapToFresh(NoSymbol).inverse) // Fresh --> cap
646+
.showing(i"solve $this = $result", capt)
647+
//println(i"solving var $this $approx ${approx.isConst} deps = ${deps.toList}")
648+
val newElems = approx.elems -- elems
649+
given VarState()
650+
if tryInclude(newElems, empty).isOK then
651+
markSolved()
650652

651653
/** Mark set as solved and propagate this info to all dependent sets */
652654
def markSolved()(using Context): Unit =
@@ -1356,31 +1358,14 @@ object CaptureSet:
13561358

13571359
/** The deep capture set of a type is the union of all covariant occurrences of
13581360
* capture sets. Nested existential sets are approximated with `cap`.
1359-
* NOTE: The traversal logic needs to be in sync with narrowCaps in CaptureOps, which
1360-
* replaces caps with reach capabilties. The one exception to this is invariant
1361-
* arguments. These have to be included to be conservative in dcs but must be
1362-
* excluded in narrowCaps.
13631361
*/
13641362
def ofTypeDeeply(tp: Type, includeTypevars: Boolean = false)(using Context): CaptureSet =
1365-
val collect = new TypeAccumulator[CaptureSet]:
1366-
val seen = util.HashSet[Symbol]()
1367-
def apply(cs: CaptureSet, t: Type) =
1368-
if variance < 0 then cs
1369-
else t.dealias match
1370-
case t @ CapturingType(p, cs1) =>
1371-
this(cs, p) ++ cs1
1372-
case t @ AnnotatedType(parent, ann) =>
1373-
this(cs, parent)
1374-
case t: TypeRef if t.symbol.isAbstractOrParamType && !seen.contains(t.symbol) =>
1375-
seen += t.symbol
1376-
val upper = t.info.bounds.hi
1377-
if includeTypevars && upper.isExactlyAny then CaptureSet.fresh(t.symbol)
1378-
else this(cs, upper)
1379-
case t @ FunctionOrMethod(args, res) =>
1380-
if args.forall(_.isAlwaysPure) then this(cs, root.resultToFresh(res))
1381-
else cs
1382-
case _ =>
1383-
foldOver(cs, t)
1363+
val collect = new DeepTypeAccumulator[CaptureSet]:
1364+
def capturingCase(acc: CaptureSet, parent: Type, refs: CaptureSet) =
1365+
this(acc, parent) ++ refs
1366+
def abstractTypeCase(acc: CaptureSet, t: TypeRef, upperBound: Type) =
1367+
if includeTypevars && upperBound.isExactlyAny then CaptureSet.fresh(t.symbol)
1368+
else this(acc, upperBound)
13841369
collect(CaptureSet.empty, tp)
13851370

13861371
type AssumedContains = immutable.Map[TypeRef, SimpleIdentitySet[CaptureRef]]

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

Lines changed: 8 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -698,7 +698,7 @@ class CheckCaptures extends Recheck, SymTransformer:
698698
val meth = tree.fun.symbol
699699
if meth == defn.Caps_unsafeAssumePure then
700700
val arg :: Nil = tree.args: @unchecked
701-
val argType0 = recheck(arg, pt.stripCapturing.capturing(CaptureSet.universal))
701+
val argType0 = recheck(arg, pt.stripCapturing.capturing(root.Fresh()))
702702
val argType =
703703
if argType0.captureSet.isAlwaysEmpty then argType0
704704
else argType0.widen.stripCapturing
@@ -1105,7 +1105,8 @@ class CheckCaptures extends Recheck, SymTransformer:
11051105
for param <- cls.paramGetters do
11061106
if !param.hasAnnotation(defn.ConstructorOnlyAnnot)
11071107
&& !param.hasAnnotation(defn.UntrackedCapturesAnnot) then
1108-
checkSubset(param.termRef.captureSet, thisSet, param.srcPos) // (3)
1108+
CCState.withCapAsRoot: // OK? We need this here since self types use `cap` instead of `fresh`
1109+
checkSubset(param.termRef.captureSet, thisSet, param.srcPos) // (3)
11091110
for pureBase <- cls.pureBaseClass do // (4)
11101111
def selfTypeTree = impl.body
11111112
.collect:
@@ -1452,7 +1453,9 @@ class CheckCaptures extends Recheck, SymTransformer:
14521453
val cs = actual.captureSet
14531454
if covariant then cs ++ leaked
14541455
else
1455-
if !leaked.subCaptures(cs).isOK then
1456+
if CCState.withCapAsRoot: // Not sure this is OK, actually
1457+
!leaked.subCaptures(cs).isOK
1458+
then
14561459
report.error(
14571460
em"""$expected cannot be box-converted to ${actual.capturing(leaked)}
14581461
|since the additional capture set $leaked resulted from box conversion is not allowed in $actual""", tree.srcPos)
@@ -1854,7 +1857,8 @@ class CheckCaptures extends Recheck, SymTransformer:
18541857
val normArgs = args.lazyZip(tl.paramInfos).map: (arg, bounds) =>
18551858
arg.withType(arg.nuType.forceBoxStatus(
18561859
bounds.hi.isBoxedCapturing | bounds.lo.isBoxedCapturing))
1857-
checkBounds(normArgs, tl)
1860+
CCState.withCapAsRoot: // OK? We need this since bounds use `cap` instead of `fresh`
1861+
checkBounds(normArgs, tl)
18581862
args.lazyZip(tl.paramNames).foreach(healTypeParam(_, _, fun.symbol))
18591863
case _ =>
18601864
case _ =>

‎compiler/src/dotty/tools/dotc/typer/RefChecks.scala

Lines changed: 4 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -21,7 +21,7 @@ import config.MigrationVersion
2121
import config.Printers.refcheck
2222
import reporting.*
2323
import Constants.Constant
24-
import cc.{stripCapturing, isUpdateMethod}
24+
import cc.{stripCapturing, isUpdateMethod, CCState}
2525

2626
object RefChecks {
2727
import tpd.*
@@ -107,7 +107,9 @@ object RefChecks {
107107
def checkSelfConforms(other: ClassSymbol) =
108108
var otherSelf = other.declaredSelfTypeAsSeenFrom(cls.thisType)
109109
if otherSelf.exists then
110-
if !(cinfo.selfType <:< otherSelf) then
110+
if !CCState.withCapAsRoot: // OK? We need this here since self types use `cap` instead of `fresh`
111+
cinfo.selfType <:< otherSelf
112+
then
111113
report.error(DoesNotConformToSelfType("illegal inheritance", cinfo.selfType, cls, otherSelf, "parent", other),
112114
cls.srcPos)
113115

‎tests/neg-custom-args/captures/box-adapt-cs.scala

Lines changed: 4 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -5,7 +5,10 @@ def test1(io: Cap^): Unit = {
55

66
val x: Id[Cap^{io}] = ???
77
val f: (Cap^) -> Unit = ???
8-
x(f) // ok
8+
x(f) // error
9+
10+
val g: (Cap^{io}) -> Unit = ???
11+
x(g) // ok
912
}
1013

1114
def test2(io: Cap^): Unit = {

‎tests/pos-custom-args/captures/cc-poly-source.scala renamed to ‎tests/neg-custom-args/captures/cc-poly-source.scala

Lines changed: 4 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -27,7 +27,10 @@ import caps.use
2727

2828
def test2(@use lbls: List[Label^]) =
2929
def makeListener(lbl: Label^): Listener^{lbl} = ???
30-
val listeners = lbls.map(makeListener)
30+
val listeners = lbls.map(makeListener) // error
31+
// we get an error here because we no longer allow contravariant cap
32+
// to subsume other capabilities. The problem can be solved by declaring
33+
// Label a SharedCapability, see cc-poly-source-capability.scala
3134
val src = Source[CapSet^{lbls*}]
3235
for l <- listeners do
3336
src.register(l)

‎tests/neg-custom-args/captures/i19330-alt2.scala

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -11,5 +11,5 @@ trait Foo:
1111
def foo: this.T =
1212
val leaked = usingLogger[T]: l => // error
1313
val t: () => Logger^ = () => l // error separation
14-
t: T
14+
t: T // error
1515
leaked

‎tests/neg-custom-args/captures/i19330.check

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -3,6 +3,13 @@
33
| ^^^
44
| Type variable T of method usingLogger cannot be instantiated to x.T since
55
| the part () => Logger^ of that type captures the root capability `cap`.
6+
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/i19330.scala:17:4 ----------------------------------------
7+
17 | t: x.T // error
8+
| ^
9+
| Found: () ->{t} Logger^{t*}
10+
| Required: x.T
11+
|
12+
| longer explanation available when compiling with `-explain`
613
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/i19330.scala:22:22 ---------------------------------------
714
22 | val bad: bar.T = foo(bar) // error
815
| ^^^^^^^^

‎tests/neg-custom-args/captures/i19330.scala

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -14,7 +14,7 @@ class Bar extends Foo:
1414
def foo(x: Foo): x.T =
1515
val leaked = usingLogger[x.T]: l => // error
1616
val t: () => Logger^ = () => l // error
17-
t: x.T
17+
t: x.T // error
1818
leaked
1919

2020
def test(): Unit =

‎tests/neg-custom-args/captures/i21614.check

Lines changed: 8 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,11 @@
1-
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/i21614.scala:12:33 ---------------------------------------
1+
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/i21614.scala:12:12 ---------------------------------------
22
12 | files.map((f: F) => new Logger(f)) // error, Q: can we make this pass (see #19076)?
3-
| ^
4-
| Found: (f : F)
5-
| Required: File^
3+
| ^^^^^^^^^^^^^^^^^^^^^^^
4+
| Found: (f: F) ->{files*.rd} box Logger{val f²: File^?}^?
5+
| Required: (f: box F^{files*.rd}) ->{fresh} box Logger{val f²: File^?}^?
6+
|
7+
| where: f is a reference to a value parameter
8+
| f² is a value in class Logger
69
|
710
| longer explanation available when compiling with `-explain`
811
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/i21614.scala:15:12 ---------------------------------------
@@ -11,7 +14,7 @@
1114
| Found: (_$1: box File^{files*}) ->{files*} box Logger{val f: File^{_$1}}^{localcap.rd, _$1}
1215
| Required: (_$1: box File^{files*}) ->{fresh} box Logger{val f: File^?}^?
1316
|
14-
| Note that reference <cap of (f: box F^{files*.rd}): box Logger{val f: File^?}^?>.rd
17+
| Note that reference <cap of (_$1: box File^{files*}): box Logger{val f: File^?}^?>.rd
1518
| cannot be included in outer capture set ?
1619
|
1720
| longer explanation available when compiling with `-explain`

‎tests/neg-custom-args/captures/sep-curried.check

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,10 @@
1+
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/sep-curried.scala:48:43 ----------------------------------
2+
48 | val f: (y: Ref[Int]^{a}) ->{a} Unit = foo(a) // error
3+
| ^^^^^^
4+
| Found: (y: Ref[Int]^) ->{a} Unit
5+
| Required: (y: Ref[Int]^{a}) ->{a} Unit
6+
|
7+
| longer explanation available when compiling with `-explain`
18
-- Error: tests/neg-custom-args/captures/sep-curried.scala:16:6 --------------------------------------------------------
29
16 | foo(a)(a) // error
310
| ^

‎tests/neg-custom-args/captures/sep-curried.scala

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -45,5 +45,5 @@ def test5(): Unit =
4545
val a: Ref[Int]^ = Ref(0)
4646
val foo: (x: Ref[Int]^) -> (y: Ref[Int]^) ->{x} Unit =
4747
x => y => swap(x, y)
48-
val f: (y: Ref[Int]^{a}) ->{a} Unit = foo(a) // should be error, but we don't check params
48+
val f: (y: Ref[Int]^{a}) ->{a} Unit = foo(a) // error
4949
f(a)

0 commit comments

Comments
 (0)