Skip to content

Commit 6513b52

Browse files
authored
Change retains annotation from using term arguments to using type arguments (#22909)
Fix #22842 This PR updates the retains annotation to use type arguments rather than term arguments, streamlining capture set representations and related type checking. It replaces usages of ConstructorProxy with PhantomSymbol, adjusts annotation construction in several compiler phases, and introduces dummy term capture parameters. * Updated flag checks and use` PhantomSymbol` for dummy symbols. * Removing term parameter for retains annotation and `capsOf`. * Modifying annotation construction in RetainingType, CaptureAnnotation, and associated AST desugarings. For example, ```scala def f[C^](x: A^): B @retains[x.type | C] // B^{x, C} ```
2 parents 49286a9 + cc2b60a commit 6513b52

File tree

73 files changed

+431
-381
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

73 files changed

+431
-381
lines changed

compiler/src/dotty/tools/dotc/ast/Desugar.scala

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -2263,9 +2263,9 @@ object desugar {
22632263
AppliedTypeTree(ref(defn.SeqType), t),
22642264
New(ref(defn.RepeatedAnnot.typeRef), Nil :: Nil))
22652265
else if op.name == nme.CC_REACH then
2266-
Apply(ref(defn.Caps_reachCapability), t :: Nil)
2266+
Annotated(t, New(ref(defn.ReachCapabilityAnnot.typeRef), Nil :: Nil))
22672267
else if op.name == nme.CC_READONLY then
2268-
Apply(ref(defn.Caps_readOnlyCapability), t :: Nil)
2268+
Annotated(t, New(ref(defn.ReadOnlyCapabilityAnnot.typeRef), Nil :: Nil))
22692269
else
22702270
assert(ctx.mode.isExpr || ctx.reporter.errorsReported || ctx.mode.is(Mode.Interactive), ctx.mode)
22712271
Select(t, op.name)

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

Lines changed: 22 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -388,6 +388,8 @@ object untpd extends Trees.Instance[Untyped] with UntypedTreeInfo {
388388
/** Property key for contextual Apply trees of the form `fn given arg` */
389389
val KindOfApply: Property.StickyKey[ApplyKind] = Property.StickyKey()
390390

391+
val RetainsAnnot: Property.StickyKey[Unit] = Property.StickyKey()
392+
391393
// ------ Creation methods for untyped only -----------------
392394

393395
def Ident(name: Name)(implicit src: SourceFile): Ident = new Ident(name)
@@ -530,10 +532,23 @@ object untpd extends Trees.Instance[Untyped] with UntypedTreeInfo {
530532
Select(scalaDot(nme.caps), nme.CAPTURE_ROOT)
531533

532534
def makeRetaining(parent: Tree, refs: List[Tree], annotName: TypeName)(using Context): Annotated =
533-
Annotated(parent, New(scalaAnnotationDot(annotName), List(refs)))
534-
535-
def makeCapsOf(tp: RefTree)(using Context): Tree =
536-
TypeApply(capsInternalDot(nme.capsOf), tp :: Nil)
535+
var annot: Tree = scalaAnnotationDot(annotName)
536+
if annotName == tpnme.retainsCap then
537+
annot = New(annot, Nil)
538+
else
539+
val trefs =
540+
if refs.isEmpty then
541+
// The NothingType is used to represent the empty capture set.
542+
ref(defn.NothingType)
543+
else
544+
// Treat all references as term references before typing.
545+
// A dummy term symbol will be created for each capture variable,
546+
// and references to them will be replaced with the corresponding
547+
// type references during typing.
548+
refs.map(SingletonTypeTree).reduce[Tree]((a, b) => makeOrType(a, b))
549+
annot = New(AppliedTypeTree(annot, trefs :: Nil), Nil)
550+
annot.putAttachment(RetainsAnnot, ())
551+
Annotated(parent, annot)
537552

538553
def makeConstructor(tparams: List[TypeDef], vparamss: List[List[ValDef]], rhs: Tree = EmptyTree)(using Context): DefDef =
539554
DefDef(nme.CONSTRUCTOR, joinParams(tparams, vparamss), TypeTree(), rhs)
@@ -557,6 +572,9 @@ object untpd extends Trees.Instance[Untyped] with UntypedTreeInfo {
557572
def makeAndType(left: Tree, right: Tree)(using Context): AppliedTypeTree =
558573
AppliedTypeTree(ref(defn.andType.typeRef), left :: right :: Nil)
559574

575+
def makeOrType(left: Tree, right: Tree)(using Context): AppliedTypeTree =
576+
AppliedTypeTree(ref(defn.orType.typeRef), left :: right :: Nil)
577+
560578
def makeParameter(pname: TermName, tpe: Tree, mods: Modifiers, isBackquoted: Boolean = false)(using Context): ValDef = {
561579
val vdef = ValDef(pname, tpe, EmptyTree)
562580
if (isBackquoted) vdef.pushAttachment(Backquoted, ())

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

Lines changed: 15 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -603,6 +603,21 @@ object Capabilities:
603603
def assumedContainsOf(x: TypeRef)(using Context): SimpleIdentitySet[Capability] =
604604
CaptureSet.assumedContains.getOrElse(x, SimpleIdentitySet.empty)
605605

606+
/** The type representing this capability.
607+
* Note this method does not distinguish different `RootCapability` instances,
608+
* and should only be used for printing or phases not related to CC.
609+
*/
610+
def toType(using Context): Type = this match
611+
case c: RootCapability => defn.captureRoot.termRef
612+
case c: CoreCapability => c
613+
case c: DerivedCapability =>
614+
val c1 = c.underlying.toType
615+
c match
616+
case _: ReadOnly => ReadOnlyCapability(c1)
617+
case _: Reach => ReachCapability(c1)
618+
case _: Maybe => MaybeCapability(c1)
619+
case _ => c1
620+
606621
def toText(printer: Printer): Text = printer.toTextCapability(this)
607622
end Capability
608623

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

Lines changed: 8 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -39,15 +39,14 @@ case class CaptureAnnotation(refs: CaptureSet, boxed: Boolean)(cls: Symbol) exte
3939

4040
/** Reconstitute annotation tree from capture set */
4141
override def tree(using Context) =
42-
val elems = refs.elems.toList.map {
43-
case c: TermRef => ref(c)
44-
case c: TermParamRef => untpd.Ident(c.paramName).withType(c)
45-
case c: ThisType => This(c.cls)
46-
case c: RootCapability => ref(defn.captureRoot)
47-
// TODO: Will crash if the type is an annotated type, for example `cap.rd`
48-
}
49-
val arg = repeated(elems, TypeTree(defn.AnyType))
50-
New(symbol.typeRef, arg :: Nil)
42+
if symbol == defn.RetainsCapAnnot then
43+
New(symbol.typeRef, Nil)
44+
else
45+
val elems = refs.elems.toList.map(_.toType)
46+
val trefs =
47+
if elems.isEmpty then defn.NothingType
48+
else elems.reduce((a, b) => OrType(a, b, soft = false))
49+
New(AppliedType(symbol.typeRef, trefs :: Nil), Nil)
5150

5251
override def symbol(using Context) = cls
5352

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

Lines changed: 59 additions & 53 deletions
Original file line numberDiff line numberDiff line change
@@ -47,57 +47,59 @@ def ccState(using Context): CCState =
4747

4848
extension (tree: Tree)
4949

50-
/** Map tree with a Capability type to the corresponding capability,
51-
* map CapSet^{refs} to the `refs` references,
52-
* throw IllegalCaptureRef otherwise
53-
*/
54-
def toCapabilities(using Context): List[Capability] = tree match
55-
case ReachCapabilityApply(arg) =>
56-
arg.toCapabilities.map(_.reach)
57-
case ReadOnlyCapabilityApply(arg) =>
58-
arg.toCapabilities.map(_.readOnly)
59-
case CapsOfApply(arg) =>
60-
arg.toCapabilities
61-
case _ => tree.tpe.dealiasKeepAnnots match
62-
case ref: TermRef if ref.isCapRef =>
63-
GlobalCap :: Nil
64-
case ref: Capability if ref.isTrackableRef =>
65-
ref :: Nil
66-
case AnnotatedType(parent, ann)
67-
if ann.symbol.isRetains && parent.derivesFrom(defn.Caps_CapSet) =>
68-
ann.tree.toCaptureSet.elems.toList
69-
case tpe =>
70-
throw IllegalCaptureRef(tpe) // if this was compiled from cc syntax, problem should have been reported at Typer
71-
7250
/** Convert a @retains or @retainsByName annotation tree to the capture set it represents.
7351
* For efficience, the result is cached as an Attachment on the tree.
7452
*/
7553
def toCaptureSet(using Context): CaptureSet =
7654
tree.getAttachment(Captures) match
7755
case Some(refs) => refs
7856
case None =>
79-
val refs = CaptureSet(tree.retainedElems.flatMap(_.toCapabilities)*)
80-
//.showing(i"toCaptureSet $tree --> $result", capt)
57+
val refs = CaptureSet(tree.retainedSet.retainedElements*)
8158
tree.putAttachment(Captures, refs)
8259
refs
8360

84-
/** The arguments of a @retains, @retainsCap or @retainsByName annotation */
85-
def retainedElems(using Context): List[Tree] = tree match
86-
case Apply(_, Typed(SeqLiteral(elems, _), _) :: Nil) =>
87-
elems
88-
case _ =>
89-
if tree.symbol.maybeOwner == defn.RetainsCapAnnot
90-
then ref(defn.captureRoot) :: Nil
91-
else Nil
61+
/** The type representing the capture set of @retains, @retainsCap or @retainsByName annotation. */
62+
def retainedSet(using Context): Type =
63+
tree match
64+
case Apply(TypeApply(_, refs :: Nil), _) => refs.tpe
65+
case _ =>
66+
if tree.symbol.maybeOwner == defn.RetainsCapAnnot
67+
then defn.captureRoot.termRef else NoType
9268

9369
extension (tp: Type)
9470

71+
def toCapability(using Context): Capability = tp match
72+
case ReachCapability(tp1) =>
73+
tp1.toCapability.reach
74+
case ReadOnlyCapability(tp1) =>
75+
tp1.toCapability.readOnly
76+
case ref: TermRef if ref.isCapRef =>
77+
GlobalCap
78+
case ref: Capability if ref.isTrackableRef =>
79+
ref
80+
case _ =>
81+
// if this was compiled from cc syntax, problem should have been reported at Typer
82+
throw IllegalCaptureRef(tp)
83+
84+
/** A list of raw elements of a retained set.
85+
* This will not crash even if it contains a non-wellformed Capability.
86+
*/
87+
def retainedElementsRaw(using Context): List[Type] = tp match
88+
case OrType(tp1, tp2) =>
89+
tp1.retainedElementsRaw ++ tp2.retainedElementsRaw
90+
case tp =>
91+
// Nothing is a special type to represent the empty set
92+
if tp.isNothingType then Nil
93+
else tp :: Nil // should be checked by wellformedness
94+
95+
/** A list of capabilities of a retained set. */
96+
def retainedElements(using Context): List[Capability] =
97+
retainedElementsRaw.map(_.toCapability)
98+
9599
/** Is this type a Capability that can be tracked?
96100
* This is true for
97101
* - all ThisTypes and all TermParamRef,
98102
* - stable TermRefs with NoPrefix or ThisTypes as prefixes,
99-
* - the root capability `caps.cap`
100-
* - abstract or parameter TypeRefs that derive from caps.CapSet
101103
* - annotated types that represent reach or maybe capabilities
102104
*/
103105
final def isTrackableRef(using Context): Boolean = tp match
@@ -408,7 +410,7 @@ extension (cls: ClassSymbol)
408410
|| bc.is(CaptureChecked)
409411
&& bc.givenSelfType.dealiasKeepAnnots.match
410412
case CapturingType(_, refs) => refs.isAlwaysEmpty
411-
case RetainingType(_, refs) => refs.isEmpty
413+
case RetainingType(_, refs) => refs.retainedElements.isEmpty
412414
case selfType =>
413415
isCaptureChecking // At Setup we have not processed self types yet, so
414416
// unless a self type is explicitly given, we can't tell
@@ -523,32 +525,36 @@ class CleanupRetains(using Context) extends TypeMap:
523525
def apply(tp: Type): Type =
524526
tp match
525527
case AnnotatedType(tp, annot) if annot.symbol == defn.RetainsAnnot || annot.symbol == defn.RetainsByNameAnnot =>
526-
RetainingType(tp, Nil, byName = annot.symbol == defn.RetainsByNameAnnot)
528+
RetainingType(tp, defn.NothingType, byName = annot.symbol == defn.RetainsByNameAnnot)
527529
case _ => mapOver(tp)
528530

529-
/** An extractor for `caps.reachCapability(ref)`, which is used to express a reach
530-
* capability as a tree in a @retains annotation.
531+
/** A base class for extractors that match annotated types with a specific
532+
* Capability annotation.
531533
*/
532-
object ReachCapabilityApply:
533-
def unapply(tree: Apply)(using Context): Option[Tree] = tree match
534-
case Apply(reach, arg :: Nil) if reach.symbol == defn.Caps_reachCapability => Some(arg)
534+
abstract class AnnotatedCapability(annotCls: Context ?=> ClassSymbol):
535+
def apply(tp: Type)(using Context): AnnotatedType =
536+
AnnotatedType(tp, Annotation(annotCls, util.Spans.NoSpan))
537+
538+
def unapply(tree: AnnotatedType)(using Context): Option[Type] = tree match
539+
case AnnotatedType(parent: Type, ann) if ann.hasSymbol(annotCls) => Some(parent)
535540
case _ => None
536541

537-
/** An extractor for `caps.readOnlyCapability(ref)`, which is used to express a read-only
538-
* capability as a tree in a @retains annotation.
542+
end AnnotatedCapability
543+
544+
/** An extractor for `ref @readOnlyCapability`, which is used to express
545+
* the read-only capability `ref.rd` as a type.
539546
*/
540-
object ReadOnlyCapabilityApply:
541-
def unapply(tree: Apply)(using Context): Option[Tree] = tree match
542-
case Apply(ro, arg :: Nil) if ro.symbol == defn.Caps_readOnlyCapability => Some(arg)
543-
case _ => None
547+
object ReadOnlyCapability extends AnnotatedCapability(defn.ReadOnlyCapabilityAnnot)
544548

545-
/** An extractor for `caps.capsOf[X]`, which is used to express a generic capture set
546-
* as a tree in a @retains annotation.
549+
/** An extractor for `ref @reachCapability`, which is used to express
550+
* the reach capability `ref*` as a type.
547551
*/
548-
object CapsOfApply:
549-
def unapply(tree: TypeApply)(using Context): Option[Tree] = tree match
550-
case TypeApply(capsOf, arg :: Nil) if capsOf.symbol == defn.Caps_capsOf => Some(arg)
551-
case _ => None
552+
object ReachCapability extends AnnotatedCapability(defn.ReachCapabilityAnnot)
553+
554+
/** An extractor for `ref @amaybeCapability`, which is used to express
555+
* the maybe capability `ref?` as a type.
556+
*/
557+
object MaybeCapability extends AnnotatedCapability(defn.MaybeCapabilityAnnot)
552558

553559
/** An extractor for all kinds of function types as well as method and poly types.
554560
* It includes aliases of function types such as `=>`. TODO: Can we do without?

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

Lines changed: 12 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -100,25 +100,24 @@ object CheckCaptures:
100100
* This check is performed at Typer.
101101
*/
102102
def checkWellformed(parent: Tree, ann: Tree)(using Context): Unit =
103-
def check(elem: Tree, pos: SrcPos): Unit = elem.tpe match
103+
def check(elem: Type, pos: SrcPos): Unit = elem match
104104
case ref: Capability =>
105105
if !ref.isTrackableRef && !ref.isCapRef then
106106
report.error(em"$elem cannot be tracked since it is not a parameter or local value", pos)
107107
case tpe =>
108108
report.error(em"$elem: $tpe is not a legal element of a capture set", pos)
109-
for elem <- ann.retainedElems do
109+
for elem <- ann.retainedSet.retainedElementsRaw do
110110
elem match
111-
case CapsOfApply(arg) =>
112-
def isLegalCapsOfArg =
113-
arg.symbol.isType && arg.symbol.info.derivesFrom(defn.Caps_CapSet)
114-
if !isLegalCapsOfArg then
115-
report.error(
116-
em"""$arg is not a legal prefix for `^` here,
117-
|is must be a type parameter or abstract type with a caps.CapSet upper bound.""",
118-
elem.srcPos)
119-
case ReachCapabilityApply(arg) => check(arg, elem.srcPos)
120-
case ReadOnlyCapabilityApply(arg) => check(arg, elem.srcPos)
121-
case _ => check(elem, elem.srcPos)
111+
case ref: TypeRef =>
112+
val refSym = ref.symbol
113+
if refSym.isType && !refSym.info.derivesFrom(defn.Caps_CapSet) then
114+
report.error(em"$elem is not a legal element of a capture set", ann.srcPos)
115+
case ReachCapability(ref) =>
116+
check(ref, ann.srcPos)
117+
case ReadOnlyCapability(ref) =>
118+
check(ref, ann.srcPos)
119+
case _ =>
120+
check(elem, ann.srcPos)
122121

123122
/** Under the sealed policy, report an error if some part of `tp` contains the
124123
* root capability in its capture set or if it refers to a type parameter that

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

Lines changed: 4 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -12,24 +12,20 @@ import Decorators.i
1212
*/
1313
object RetainingType:
1414

15-
def apply(tp: Type, refs: List[Tree], byName: Boolean = false)(using Context): Type =
15+
def apply(tp: Type, typeElems: Type, byName: Boolean = false)(using Context): Type =
1616
val annotCls = if byName then defn.RetainsByNameAnnot else defn.RetainsAnnot
17-
val annotTree =
18-
New(annotCls.typeRef,
19-
Typed(
20-
SeqLiteral(refs, TypeTree(defn.AnyType)),
21-
TypeTree(defn.RepeatedParamClass.typeRef.appliedTo(defn.AnyType))) :: Nil)
17+
val annotTree = New(AppliedType(annotCls.typeRef, typeElems :: Nil), Nil)
2218
AnnotatedType(tp, Annotation(annotTree))
2319

24-
def unapply(tp: AnnotatedType)(using Context): Option[(Type, List[Tree])] =
20+
def unapply(tp: AnnotatedType)(using Context): Option[(Type, Type)] =
2521
val sym = tp.annot.symbol
2622
if sym.isRetainsLike then
2723
tp.annot match
2824
case _: CaptureAnnotation =>
2925
assert(ctx.mode.is(Mode.IgnoreCaptures), s"bad retains $tp at ${ctx.phase}")
3026
None
3127
case ann =>
32-
Some((tp.parent, ann.tree.retainedElems))
28+
Some((tp.parent, ann.tree.retainedSet))
3329
else
3430
None
3531
end RetainingType

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

Lines changed: 11 additions & 16 deletions
Original file line numberDiff line numberDiff line change
@@ -806,7 +806,7 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI:
806806
case CapturingType(_, refs) =>
807807
!refs.isAlwaysEmpty
808808
case RetainingType(parent, refs) =>
809-
!refs.isEmpty
809+
!refs.retainedElements.isEmpty
810810
case tp: (TypeRef | AppliedType) =>
811811
val sym = tp.typeSymbol
812812
if sym.isClass
@@ -852,7 +852,7 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI:
852852
&& !refs.isUniversal // if refs is {cap}, an added variable would not change anything
853853
case RetainingType(parent, refs) =>
854854
needsVariable(parent)
855-
&& !refs.tpes.exists:
855+
&& !refs.retainedElements.exists:
856856
case ref: TermRef => ref.isCapRef
857857
case _ => false
858858
case AnnotatedType(parent, _) =>
@@ -947,19 +947,13 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI:
947947
* @param tpt the tree for which an error or warning should be reported
948948
*/
949949
private def checkWellformed(parent: Type, ann: Tree, tpt: Tree)(using Context): Unit =
950-
capt.println(i"checkWF post $parent ${ann.retainedElems} in $tpt")
951-
var retained = ann.retainedElems.toArray
952-
for i <- 0 until retained.length do
953-
val refTree = retained(i)
954-
val refs =
955-
try refTree.toCapabilities
956-
catch case ex: IllegalCaptureRef =>
957-
report.error(em"Illegal capture reference: ${ex.getMessage}", refTree.srcPos)
958-
Nil
959-
for ref <- refs do
950+
capt.println(i"checkWF post $parent ${ann.retainedSet} in $tpt")
951+
try
952+
var retained = ann.retainedSet.retainedElements.toArray
953+
for i <- 0 until retained.length do
954+
val ref = retained(i)
960955
def pos =
961-
if refTree.span.exists then refTree.srcPos
962-
else if ann.span.exists then ann.srcPos
956+
if ann.span.exists then ann.srcPos
963957
else tpt.srcPos
964958

965959
def check(others: CaptureSet, dom: Type | CaptureSet): Unit =
@@ -976,13 +970,14 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI:
976970
val others =
977971
for
978972
j <- 0 until retained.length if j != i
979-
r <- retained(j).toCapabilities
973+
r = retained(j)
980974
if !r.isTerminalCapability
981975
yield r
982976
val remaining = CaptureSet(others*)
983977
check(remaining, remaining)
984978
end for
985-
end for
979+
catch case ex: IllegalCaptureRef =>
980+
report.error(em"Illegal capture reference: ${ex.getMessage}", tpt.srcPos)
986981
end checkWellformed
987982

988983
/** Check well formed at post check time. We need to wait until after

0 commit comments

Comments
 (0)