Skip to content

Commit 9015611

Browse files
noti0na1noti0na1
committed
Add path support for cc
1 parent 65a53b5 commit 9015611

18 files changed

+314
-120
lines changed

‎compiler/src/dotty/tools/dotc/ast/untpd.scala

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -525,8 +525,8 @@ object untpd extends Trees.Instance[Untyped] with UntypedTreeInfo {
525525
def makeRetaining(parent: Tree, refs: List[Tree], annotName: TypeName)(using Context): Annotated =
526526
Annotated(parent, New(scalaAnnotationDot(annotName), List(refs)))
527527

528-
def makeCapsOf(id: Ident)(using Context): Tree =
529-
TypeApply(Select(scalaDot(nme.caps), nme.capsOf), id :: Nil)
528+
def makeCapsOf(tp: Tree)(using Context): Tree =
529+
TypeApply(Select(scalaDot(nme.caps), nme.capsOf), tp :: Nil)
530530

531531
def makeCapsBound()(using Context): Tree =
532532
makeRetaining(

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

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -194,7 +194,8 @@ extension (tp: Type)
194194
true
195195
case tp: TermRef =>
196196
((tp.prefix eq NoPrefix)
197-
|| tp.symbol.is(ParamAccessor) && tp.prefix.isThisTypeOf(tp.symbol.owner)
197+
|| tp.symbol.isField && !tp.symbol.isStatic && (
198+
tp.prefix.isThisTypeOf(tp.symbol.owner) || tp.prefix.isTrackableRef)
198199
|| tp.isRootCapability
199200
) && !tp.symbol.isOneOf(UnstableValueFlags)
200201
case tp: TypeRef =>

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

Lines changed: 58 additions & 26 deletions
Original file line numberDiff line numberDiff line change
@@ -61,18 +61,19 @@ trait CaptureRef extends TypeProxy, ValueType:
6161
case tp: TermParamRef => tp.underlying.derivesFrom(defn.Caps_Exists)
6262
case _ => false
6363

64-
/** Normalize reference so that it can be compared with `eq` for equality */
65-
final def normalizedRef(using Context): CaptureRef = this match
66-
case tp @ AnnotatedType(parent: CaptureRef, annot) if tp.isTrackableRef =>
67-
tp.derivedAnnotatedType(parent.normalizedRef, annot)
68-
case tp: TermRef if tp.isTrackableRef =>
69-
tp.symbol.termRef
70-
case _ => this
64+
// With the support of pathes, we don't need to normalize the `TermRef`s anymore.
65+
// /** Normalize reference so that it can be compared with `eq` for equality */
66+
// final def normalizedRef(using Context): CaptureRef = this match
67+
// case tp @ AnnotatedType(parent: CaptureRef, annot) if tp.isTrackableRef =>
68+
// tp.derivedAnnotatedType(parent.normalizedRef, annot)
69+
// case tp: TermRef if tp.isTrackableRef =>
70+
// tp.symbol.termRef
71+
// case _ => this
7172

7273
/** The capture set consisting of exactly this reference */
7374
final def singletonCaptureSet(using Context): CaptureSet.Const =
7475
if mySingletonCaptureSet == null then
75-
mySingletonCaptureSet = CaptureSet(this.normalizedRef)
76+
mySingletonCaptureSet = CaptureSet(this)
7677
mySingletonCaptureSet.uncheckedNN
7778

7879
/** The capture set of the type underlying this reference */
@@ -99,25 +100,56 @@ trait CaptureRef extends TypeProxy, ValueType:
99100
* x: x1.type /\ x1 subsumes y ==> x subsumes y
100101
*/
101102
final def subsumes(y: CaptureRef)(using Context): Boolean =
102-
(this eq y)
103-
|| this.isRootCapability
104-
|| y.match
105-
case y: TermRef =>
106-
(y.prefix eq this)
107-
|| y.info.match
108-
case y1: SingletonCaptureRef => this.subsumes(y1)
109-
case _ => false
110-
case MaybeCapability(y1) => this.stripMaybe.subsumes(y1)
111-
case _ => false
112-
|| this.match
113-
case ReachCapability(x1) => x1.subsumes(y.stripReach)
114-
case x: TermRef =>
115-
x.info match
116-
case x1: SingletonCaptureRef => x1.subsumes(y)
103+
def compareCaptureRefs(x: Type, y: Type): Boolean =
104+
(x eq y)
105+
|| y.match
106+
case y: CaptureRef => x.match
107+
case x: CaptureRef => x.subsumes(y)
117108
case _ => false
118-
case x: TermParamRef => subsumesExistentially(x, y)
119-
case x: TypeRef => assumedContainsOf(x).contains(y)
120-
case _ => false
109+
case _ => false
110+
111+
def compareUndelying(x: Type): Boolean = x match
112+
case x: SingletonCaptureRef => x.subsumes(y)
113+
case x: AndType => compareUndelying(x.tp1) || compareUndelying(x.tp2)
114+
case x: OrType => compareUndelying(x.tp1) && compareUndelying(x.tp2)
115+
case _ => false
116+
117+
if (this eq y) || this.isRootCapability then return true
118+
119+
// similar to compareNamed in TypeComparer
120+
y match
121+
case y: TermRef =>
122+
this match
123+
case x: TermRef =>
124+
val xSym = x.symbol
125+
val ySym = y.symbol
126+
127+
// check x.f and y.f
128+
if (xSym ne NoSymbol)
129+
&& (xSym eq ySym)
130+
&& compareCaptureRefs(x.prefix, y.prefix)
131+
|| (x.name eq y.name)
132+
&& x.isPrefixDependentMemberRef
133+
&& compareCaptureRefs(x.prefix, y.prefix)
134+
&& x.signature == y.signature
135+
&& !(xSym.isClass && ySym.isClass)
136+
then return true
137+
case _ =>
138+
139+
// shorten
140+
if compareCaptureRefs(this, y.prefix) then return true
141+
// underlying
142+
if compareCaptureRefs(this, y.info) then return true
143+
case MaybeCapability(y1) => return this.stripMaybe.subsumes(y1)
144+
case _ =>
145+
146+
return this.match
147+
case ReachCapability(x1) => x1.subsumes(y.stripReach)
148+
case x: TermRef => compareUndelying(x.info)
149+
case CapturingType(x1, _) => compareUndelying(x1)
150+
case x: TermParamRef => subsumesExistentially(x, y)
151+
case x: TypeRef => assumedContainsOf(x).contains(y)
152+
case _ => false
121153

122154
def assumedContainsOf(x: TypeRef)(using Context): SimpleIdentitySet[CaptureRef] =
123155
CaptureSet.assumedContains.getOrElse(x, SimpleIdentitySet.empty)

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

Lines changed: 6 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -374,7 +374,7 @@ object CaptureSet:
374374

375375
def apply(elems: CaptureRef*)(using Context): CaptureSet.Const =
376376
if elems.isEmpty then empty
377-
else Const(SimpleIdentitySet(elems.map(_.normalizedRef.ensuring(_.isTrackableRef))*))
377+
else Const(SimpleIdentitySet(elems.map(_.ensuring(_.isTrackableRef))*))
378378

379379
def apply(elems: Refs)(using Context): CaptureSet.Const =
380380
if elems.isEmpty then empty else Const(elems)
@@ -508,7 +508,11 @@ object CaptureSet:
508508
!noUniversal
509509
else elem match
510510
case elem: TermRef if level.isDefined =>
511-
elem.symbol.ccLevel <= level
511+
elem.prefix match
512+
case prefix: CaptureRef =>
513+
levelOK(prefix)
514+
case _ =>
515+
elem.symbol.ccLevel <= level
512516
case elem: ThisType if level.isDefined =>
513517
elem.cls.ccLevel.nextInner <= level
514518
case ReachCapability(elem1) =>

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

Lines changed: 59 additions & 47 deletions
Original file line numberDiff line numberDiff line change
@@ -122,10 +122,6 @@ object CheckCaptures:
122122
* This check is performed at Typer.
123123
*/
124124
def checkWellformed(parent: Tree, ann: Tree)(using Context): Unit =
125-
parent.tpe match
126-
case _: SingletonType =>
127-
report.error(em"Singleton type $parent cannot have capture set", parent.srcPos)
128-
case _ =>
129125
def check(elem: Tree, pos: SrcPos): Unit = elem.tpe match
130126
case ref: CaptureRef =>
131127
if !ref.isTrackableRef then
@@ -373,45 +369,54 @@ class CheckCaptures extends Recheck, SymTransformer:
373369
* the environment's owner
374370
*/
375371
def markFree(cs: CaptureSet, pos: SrcPos)(using Context): Unit =
372+
// A captured reference with the symbol `sym` is visible from the environment
373+
// if `sym` is not defined inside the owner of the environment.
374+
inline def isVisibleFromEnv(sym: Symbol, env: Env) =
375+
if env.kind == EnvKind.NestedInOwner then
376+
!sym.isProperlyContainedIn(env.owner)
377+
else
378+
!sym.isContainedIn(env.owner)
379+
380+
def checkSubsetEnv(cs: CaptureSet, env: Env)(using Context): Unit =
381+
// Only captured references that are visible from the environment
382+
// should be included.
383+
val included = cs.filter: c =>
384+
c.stripReach match
385+
case ref: NamedType =>
386+
val refSym = ref.symbol
387+
val refOwner = refSym.owner
388+
val isVisible = isVisibleFromEnv(refOwner, env)
389+
if isVisible && !ref.isRootCapability then
390+
ref match
391+
case ref: TermRef if ref.prefix `ne` NoPrefix =>
392+
// If c is a path of a class defined outside the environment,
393+
// we check the capture set of its info.
394+
checkSubsetEnv(ref.captureSetOfInfo, env)
395+
case _ =>
396+
if !isVisible
397+
&& (c.isReach || ref.isType)
398+
&& (!ccConfig.useSealed || refSym.is(Param))
399+
&& refOwner == env.owner
400+
then
401+
if refSym.hasAnnotation(defn.UnboxAnnot) then
402+
capt.println(i"exempt: $ref in $refOwner")
403+
else
404+
// Reach capabilities that go out of scope have to be approximated
405+
// by their underlying capture set, which cannot be universal.
406+
// Reach capabilities of @unboxed parameters are exempted.
407+
val cs = CaptureSet.ofInfo(c)
408+
cs.disallowRootCapability: () =>
409+
report.error(em"Local reach capability $c leaks into capture scope of ${env.ownerString}", pos)
410+
checkSubset(cs, env.captured, pos, provenance(env))
411+
isVisible
412+
case ref: ThisType => isVisibleFromEnv(ref.cls, env)
413+
case _ => false
414+
checkSubset(included, env.captured, pos, provenance(env))
415+
capt.println(i"Include call or box capture $included from $cs in ${env.owner} --> ${env.captured}")
416+
376417
if !cs.isAlwaysEmpty then
377418
forallOuterEnvsUpTo(ctx.owner.topLevelClass): env =>
378-
// Whether a symbol is defined inside the owner of the environment?
379-
inline def isContainedInEnv(sym: Symbol) =
380-
if env.kind == EnvKind.NestedInOwner then
381-
sym.isProperlyContainedIn(env.owner)
382-
else
383-
sym.isContainedIn(env.owner)
384-
// A captured reference with the symbol `sym` is visible from the environment
385-
// if `sym` is not defined inside the owner of the environment
386-
inline def isVisibleFromEnv(sym: Symbol) = !isContainedInEnv(sym)
387-
// Only captured references that are visible from the environment
388-
// should be included.
389-
val included = cs.filter: c =>
390-
c.stripReach match
391-
case ref: NamedType =>
392-
val refSym = ref.symbol
393-
val refOwner = refSym.owner
394-
val isVisible = isVisibleFromEnv(refOwner)
395-
if !isVisible
396-
&& (c.isReach || ref.isType)
397-
&& (!ccConfig.useSealed || refSym.is(Param))
398-
&& refOwner == env.owner
399-
then
400-
if refSym.hasAnnotation(defn.UnboxAnnot) then
401-
capt.println(i"exempt: $ref in $refOwner")
402-
else
403-
// Reach capabilities that go out of scope have to be approximated
404-
// by their underlying capture set, which cannot be universal.
405-
// Reach capabilities of @unboxed parameters are exempted.
406-
val cs = CaptureSet.ofInfo(c)
407-
cs.disallowRootCapability: () =>
408-
report.error(em"Local reach capability $c leaks into capture scope of ${env.ownerString}", pos)
409-
checkSubset(cs, env.captured, pos, provenance(env))
410-
isVisible
411-
case ref: ThisType => isVisibleFromEnv(ref.cls)
412-
case _ => false
413-
checkSubset(included, env.captured, pos, provenance(env))
414-
capt.println(i"Include call or box capture $included from $cs in ${env.owner} --> ${env.captured}")
419+
checkSubsetEnv(cs, env)
415420
end markFree
416421

417422
/** Include references captured by the called method in the current environment stack */
@@ -488,21 +493,28 @@ class CheckCaptures extends Recheck, SymTransformer:
488493
case _ => denot
489494

490495
val selType = recheckSelection(tree, qualType, name, disambiguate)
491-
val selCs = selType.widen.captureSet
492-
if selCs.isAlwaysEmpty
493-
|| selType.widen.isBoxedCapturing
496+
val selWiden = selType.widen
497+
def isStableSel = selType match
498+
case selType: NamedType => selType.symbol.isStableMember
499+
case _ => false
500+
501+
if pt == LhsProto
494502
|| qualType.isBoxedCapturing
495-
|| pt == LhsProto
503+
|| selType.isTrackableRef
504+
|| selWiden.isBoxedCapturing
505+
|| selWiden.captureSet.isAlwaysEmpty
496506
then
497507
selType
498508
else
499509
val qualCs = qualType.captureSet
500-
capt.println(i"pick one of $qualType, ${selType.widen}, $qualCs, $selCs in $tree")
510+
val selCs = selType.captureSet
511+
capt.println(i"pick one of $qualType, ${selType.widen}, $qualCs, $selCs ${selWiden.captureSet} in $tree")
512+
501513
if qualCs.mightSubcapture(selCs)
502514
&& !selCs.mightSubcapture(qualCs)
503515
&& !pt.stripCapturing.isInstanceOf[SingletonType]
504516
then
505-
selType.widen.stripCapturing.capturing(qualCs)
517+
selWiden.stripCapturing.capturing(qualCs)
506518
.showing(i"alternate type for select $tree: $selType --> $result, $qualCs / $selCs", capt)
507519
else
508520
selType

‎compiler/src/dotty/tools/dotc/parsing/Parsers.scala

Lines changed: 15 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -1548,21 +1548,23 @@ object Parsers {
15481548
case _ => None
15491549
}
15501550

1551-
/** CaptureRef ::= ident [`*` | `^`] | `this`
1551+
/** CaptureRef ::= (ident | `this`) [`*` | `^`]
15521552
*/
15531553
def captureRef(): Tree =
1554-
if in.token == THIS then simpleRef()
1555-
else
1556-
val id = termIdent()
1557-
if isIdent(nme.raw.STAR) then
1558-
in.nextToken()
1559-
atSpan(startOffset(id)):
1560-
PostfixOp(id, Ident(nme.CC_REACH))
1561-
else if isIdent(nme.UPARROW) then
1562-
in.nextToken()
1563-
atSpan(startOffset(id)):
1564-
makeCapsOf(cpy.Ident(id)(id.name.toTypeName))
1565-
else id
1554+
val ref = singleton()
1555+
if isIdent(nme.raw.STAR) then
1556+
in.nextToken()
1557+
atSpan(startOffset(ref)):
1558+
PostfixOp(ref, Ident(nme.CC_REACH))
1559+
else if isIdent(nme.UPARROW) then
1560+
in.nextToken()
1561+
def toTypeSel(r: Tree): Tree = r match
1562+
case id: Ident => cpy.Ident(id)(id.name.toTypeName)
1563+
case Select(qual, id) => Select(qual, id.toTypeName)
1564+
case _ => r
1565+
atSpan(startOffset(ref)):
1566+
makeCapsOf(toTypeSel(ref))
1567+
else ref
15661568

15671569
/** CaptureSet ::= `{` CaptureRef {`,` CaptureRef} `}` -- under captureChecking
15681570
*/

‎tests/neg-custom-args/captures/class-contra.check

Lines changed: 5 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -1,10 +1,7 @@
1-
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/class-contra.scala:12:39 ---------------------------------
2-
12 | def fun(x: K{val f: T^{a}}) = x.setf(a) // error
3-
| ^
4-
| Found: (a : T^{x, y})
5-
| Required: T^{}
6-
|
7-
| Note that a capability (K.this.f : T^) in a capture set appearing in contravariant position
8-
| was mapped to (x.f : T^{a}) which is not a capability. Therefore, it was under-approximated to the empty set.
1+
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/class-contra.scala:12:40 ---------------------------------
2+
12 | def fun1(k: K{val f: T^{a}}) = k.setf(a) // error
3+
| ^
4+
| Found: (a : T^{x, y})
5+
| Required: T^{k.f}
96
|
107
| longer explanation available when compiling with `-explain`

‎tests/neg-custom-args/captures/class-contra.scala

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -9,5 +9,6 @@ class T
99

1010
def test(x: Cap, y: Cap) =
1111
val a: T^{x, y} = ???
12-
def fun(x: K{val f: T^{a}}) = x.setf(a) // error
12+
def fun1(k: K{val f: T^{a}}) = k.setf(a) // error
13+
def fun2(k: K{val f: a.type}) = k.setf(a)
1314
()

‎tests/neg-custom-args/captures/explain-under-approx.check

Lines changed: 4 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -1,20 +1,14 @@
11
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/explain-under-approx.scala:12:10 -------------------------
22
12 | col.add(Future(() => 25)) // error
33
| ^^^^^^^^^^^^^^^^
4-
| Found: Future[Int]{val a: (async : Async^)}^{async}
5-
| Required: Future[Int]^{}
6-
|
7-
| Note that a capability Collector.this.futs* in a capture set appearing in contravariant position
8-
| was mapped to col.futs* which is not a capability. Therefore, it was under-approximated to the empty set.
4+
| Found: Future[Int]{val a: (async : Async^)}^{async}
5+
| Required: Future[Int]^{col.futs*}
96
|
107
| longer explanation available when compiling with `-explain`
118
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/explain-under-approx.scala:15:11 -------------------------
129
15 | col1.add(Future(() => 25)) // error
1310
| ^^^^^^^^^^^^^^^^
14-
| Found: Future[Int]{val a: (async : Async^)}^{async}
15-
| Required: Future[Int]^{}
16-
|
17-
| Note that a capability Collector.this.futs* in a capture set appearing in contravariant position
18-
| was mapped to col1.futs* which is not a capability. Therefore, it was under-approximated to the empty set.
11+
| Found: Future[Int]{val a: (async : Async^)}^{async}
12+
| Required: Future[Int]^{col1.futs*}
1913
|
2014
| longer explanation available when compiling with `-explain`

0 commit comments

Comments
 (0)