Skip to content

Commit ea6b0a4

Browse files
authored
Add restricted capabilities x.only[C] (#23485)
Implementation along the lines of #23463 - [x] Syntax and parsing rules for `only`-capabilities. - [x] A `Classifier` base trait. - [x] Enforce restriction that a class cannot inherit two unrelated classified capability classes. - [x] A new capability class for `only`-capabilities. - [x] Implement `captureSetOfInfo` for `only` capabilities. - [x] The empty capability is `x.only[Nothing]`. It should have empty `captureSetOfInfo`. - [x] Well-formedness rules: `only` must refer to a classified capability class. - [x] Normalization rules: - it's `*`, then `.only`, then `.rd`, - multiple `.only` normalize to the smallest one if the classes are related, - multiple `.only` normalize to the empty capability if the classes are not related. - [x] define transitive capture set and cache it in a capability. The _tcs_ does not exist if a capture set in the hierarchy is still an unsolved capture set variable. - [x] Add a _classifier_ field to `FreshCap` and `ResultCap`. - [x] Modify `capToFresh` and `toResultInResults` so that the classifier field is correctly set. - [x] Using `tcs`, define when a capability is classified by a classifier class. - [x] A FreshCap with a classifier `C` can subsume only capabilities that are classified as `C`. - [x] Implement subsumption rules: - `c.as[C] <: d` if `c <: d` or `c.as[D] <: empty` - `c.as[C] <: d.as[D]` if `c <: d` and `C` derives from `D` - `c <: d.as[D]` if `c <: d` and `c` is classified as `D` - `c.as[D] <: empty` if `tcs(c)` consists of capabilities that all derive from classifier classes unrelated to `D`.
2 parents 68a6d5b + 8b66711 commit ea6b0a4

File tree

67 files changed

+723
-206
lines changed

Some content is hidden

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

67 files changed

+723
-206
lines changed

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

Lines changed: 0 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -2321,10 +2321,6 @@ object desugar {
23212321
Annotated(
23222322
AppliedTypeTree(ref(defn.SeqType), t),
23232323
New(ref(defn.RepeatedAnnot.typeRef), Nil :: Nil))
2324-
else if op.name == nme.CC_REACH then
2325-
Annotated(t, New(ref(defn.ReachCapabilityAnnot.typeRef), Nil :: Nil))
2326-
else if op.name == nme.CC_READONLY then
2327-
Annotated(t, New(ref(defn.ReadOnlyCapabilityAnnot.typeRef), Nil :: Nil))
23282324
else
23292325
assert(ctx.mode.isExpr || ctx.reporter.errorsReported || ctx.mode.is(Mode.Interactive), ctx.mode)
23302326
Select(t, op.name)

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

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -550,6 +550,15 @@ object untpd extends Trees.Instance[Untyped] with UntypedTreeInfo {
550550
annot.putAttachment(RetainsAnnot, ())
551551
Annotated(parent, annot)
552552

553+
def makeReachAnnot()(using Context): Tree =
554+
New(ref(defn.ReachCapabilityAnnot.typeRef), Nil :: Nil)
555+
556+
def makeReadOnlyAnnot()(using Context): Tree =
557+
New(ref(defn.ReadOnlyCapabilityAnnot.typeRef), Nil :: Nil)
558+
559+
def makeOnlyAnnot(qid: Tree)(using Context) =
560+
New(AppliedTypeTree(ref(defn.OnlyCapabilityAnnot.typeRef), qid :: Nil), Nil :: Nil)
561+
553562
def makeConstructor(tparams: List[TypeDef], vparamss: List[List[ValDef]], rhs: Tree = EmptyTree)(using Context): DefDef =
554563
DefDef(nme.CONSTRUCTOR, joinParams(tparams, vparamss), TypeTree(), rhs)
555564

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

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -81,6 +81,16 @@ class CCState:
8181
def start(): Unit =
8282
iterCount = 1
8383

84+
private var mySepCheck = false
85+
86+
/** Are we currently running separation checks? */
87+
def isSepCheck = mySepCheck
88+
89+
def inSepCheck(op: => Unit): Unit =
90+
val saved = mySepCheck
91+
mySepCheck = true
92+
try op finally mySepCheck = saved
93+
8494
// ------ Global counters -----------------------
8595

8696
/** Next CaptureSet.Var id */

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

Lines changed: 185 additions & 23 deletions
Large diffs are not rendered by default.

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

Lines changed: 49 additions & 25 deletions
Original file line numberDiff line numberDiff line change
@@ -80,6 +80,8 @@ extension (tp: Type)
8080
tp1.toCapability.reach
8181
case ReadOnlyCapability(tp1) =>
8282
tp1.toCapability.readOnly
83+
case OnlyCapability(tp1, cls) =>
84+
tp1.toCapability.restrict(cls)
8385
case ref: TermRef if ref.isCapRef =>
8486
GlobalCap
8587
case ref: Capability if ref.isTrackableRef =>
@@ -290,7 +292,7 @@ extension (tp: Type)
290292
def forceBoxStatus(boxed: Boolean)(using Context): Type = tp.widenDealias match
291293
case tp @ CapturingType(parent, refs) if tp.isBoxed != boxed =>
292294
val refs1 = tp match
293-
case ref: Capability if ref.isTracked || ref.isReach || ref.isReadOnly =>
295+
case ref: Capability if ref.isTracked || ref.isInstanceOf[DerivedCapability] =>
294296
ref.singletonCaptureSet
295297
case _ => refs
296298
CapturingType(parent, refs1, boxed)
@@ -376,7 +378,7 @@ extension (tp: Type)
376378

377379
def derivesFromCapability(using Context): Boolean = derivesFromCapTrait(defn.Caps_Capability)
378380
def derivesFromMutable(using Context): Boolean = derivesFromCapTrait(defn.Caps_Mutable)
379-
def derivesFromSharedCapability(using Context): Boolean = derivesFromCapTrait(defn.Caps_SharedCapability)
381+
def derivesFromSharedCapability(using Context): Boolean = derivesFromCapTrait(defn.Caps_Sharable)
380382

381383
/** Drop @retains annotations everywhere */
382384
def dropAllRetains(using Context): Type = // TODO we should drop retains from inferred types before unpickling
@@ -442,6 +444,30 @@ extension (tp: Type)
442444
def dropUseAndConsumeAnnots(using Context): Type =
443445
tp.dropAnnot(defn.UseAnnot).dropAnnot(defn.ConsumeAnnot)
444446

447+
/** If `tp` is a function or method, a type of the same kind with the given
448+
* argument and result types.
449+
*/
450+
def derivedFunctionOrMethod(argTypes: List[Type], resType: Type)(using Context): Type = tp match
451+
case tp @ AppliedType(tycon, args) if defn.isNonRefinedFunction(tp) =>
452+
val args1 = argTypes :+ resType
453+
if args.corresponds(args1)(_ eq _) then tp
454+
else tp.derivedAppliedType(tycon, args1)
455+
case tp @ defn.RefinedFunctionOf(rinfo) =>
456+
val rinfo1 = rinfo.derivedFunctionOrMethod(argTypes, resType)
457+
if rinfo1 eq rinfo then tp
458+
else if rinfo1.isInstanceOf[PolyType] then tp.derivedRefinedType(refinedInfo = rinfo1)
459+
else rinfo1.toFunctionType(alwaysDependent = true)
460+
case tp: MethodType =>
461+
tp.derivedLambdaType(paramInfos = argTypes, resType = resType)
462+
case tp: PolyType =>
463+
assert(argTypes.isEmpty)
464+
tp.derivedLambdaType(resType = resType)
465+
case _ =>
466+
tp
467+
468+
def classifier(using Context): ClassSymbol =
469+
tp.classSymbols.map(_.classifier).foldLeft(defn.AnyClass)(leastClassifier)
470+
445471
extension (tp: MethodType)
446472
/** A method marks an existential scope unless it is the prefix of a curried method */
447473
def marksExistentialScope(using Context): Boolean =
@@ -473,6 +499,16 @@ extension (cls: ClassSymbol)
473499
val selfType = bc.givenSelfType
474500
bc.is(CaptureChecked) && selfType.exists && selfType.captureSet.elems == refs.elems
475501

502+
def isClassifiedCapabilityClass(using Context): Boolean =
503+
cls.derivesFrom(defn.Caps_Capability) && cls.parentSyms.contains(defn.Caps_Classifier)
504+
505+
def classifier(using Context): ClassSymbol =
506+
if cls.derivesFrom(defn.Caps_Capability) then
507+
cls.baseClasses
508+
.filter(_.parentSyms.contains(defn.Caps_Classifier))
509+
.foldLeft(defn.AnyClass)(leastClassifier)
510+
else defn.AnyClass
511+
476512
extension (sym: Symbol)
477513

478514
/** This symbol is one of `retains` or `retainsCap` */
@@ -587,7 +623,6 @@ abstract class AnnotatedCapability(annotCls: Context ?=> ClassSymbol):
587623
def unapply(tree: AnnotatedType)(using Context): Option[Type] = tree match
588624
case AnnotatedType(parent: Type, ann) if ann.hasSymbol(annotCls) => Some(parent)
589625
case _ => None
590-
591626
end AnnotatedCapability
592627

593628
/** An extractor for `ref @readOnlyCapability`, which is used to express
@@ -605,6 +640,17 @@ object ReachCapability extends AnnotatedCapability(defn.ReachCapabilityAnnot)
605640
*/
606641
object MaybeCapability extends AnnotatedCapability(defn.MaybeCapabilityAnnot)
607642

643+
object OnlyCapability:
644+
def apply(tp: Type, cls: ClassSymbol)(using Context): AnnotatedType =
645+
AnnotatedType(tp,
646+
Annotation(defn.OnlyCapabilityAnnot.typeRef.appliedTo(cls.typeRef), Nil, util.Spans.NoSpan))
647+
648+
def unapply(tree: AnnotatedType)(using Context): Option[(Type, ClassSymbol)] = tree match
649+
case AnnotatedType(parent: Type, ann) if ann.hasSymbol(defn.OnlyCapabilityAnnot) =>
650+
Some((parent, ann.tree.tpe.argTypes.head.classSymbol.asClass))
651+
case _ => None
652+
end OnlyCapability
653+
608654
/** An extractor for all kinds of function types as well as method and poly types.
609655
* It includes aliases of function types such as `=>`. TODO: Can we do without?
610656
* @return 1st half: The argument types or empty if this is a type function
@@ -618,28 +664,6 @@ object FunctionOrMethod:
618664
case defn.RefinedFunctionOf(rinfo) => unapply(rinfo)
619665
case _ => None
620666

621-
/** If `tp` is a function or method, a type of the same kind with the given
622-
* argument and result types.
623-
*/
624-
extension (self: Type)
625-
def derivedFunctionOrMethod(argTypes: List[Type], resType: Type)(using Context): Type = self match
626-
case self @ AppliedType(tycon, args) if defn.isNonRefinedFunction(self) =>
627-
val args1 = argTypes :+ resType
628-
if args.corresponds(args1)(_ eq _) then self
629-
else self.derivedAppliedType(tycon, args1)
630-
case self @ defn.RefinedFunctionOf(rinfo) =>
631-
val rinfo1 = rinfo.derivedFunctionOrMethod(argTypes, resType)
632-
if rinfo1 eq rinfo then self
633-
else if rinfo1.isInstanceOf[PolyType] then self.derivedRefinedType(refinedInfo = rinfo1)
634-
else rinfo1.toFunctionType(alwaysDependent = true)
635-
case self: MethodType =>
636-
self.derivedLambdaType(paramInfos = argTypes, resType = resType)
637-
case self: PolyType =>
638-
assert(argTypes.isEmpty)
639-
self.derivedLambdaType(resType = resType)
640-
case _ =>
641-
self
642-
643667
/** An extractor for a contains argument */
644668
object ContainsImpl:
645669
def unapply(tree: TypeApply)(using Context): Option[(Tree, Tree)] =

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

Lines changed: 78 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -83,6 +83,14 @@ sealed abstract class CaptureSet extends Showable:
8383
*/
8484
def owner: Symbol
8585

86+
/** If this set is a variable: Drop capabilities that are known to be empty
87+
* This is called during separation checking so that capabilities that turn
88+
* out to be always empty because of conflicting clasisifiers don't contribute
89+
* to peaks. We can't do it before that since classifiers are set during
90+
* capture checking.
91+
*/
92+
def dropEmpties()(using Context): this.type
93+
8694
/** Is this capture set definitely non-empty? */
8795
final def isNotEmpty: Boolean = !elems.isEmpty
8896

@@ -210,6 +218,7 @@ sealed abstract class CaptureSet extends Showable:
210218

211219
protected def addIfHiddenOrFail(elem: Capability)(using ctx: Context, vs: VarState): Boolean =
212220
elems.exists(_.maxSubsumes(elem, canAddHidden = true))
221+
|| elem.isKnownEmpty
213222
|| failWith(IncludeFailure(this, elem))
214223

215224
/** If this is a variable, add `cs` as a dependent set */
@@ -403,11 +412,33 @@ sealed abstract class CaptureSet extends Showable:
403412

404413
def maybe(using Context): CaptureSet = map(MaybeMap())
405414

415+
def restrict(cls: ClassSymbol)(using Context): CaptureSet = map(RestrictMap(cls))
416+
406417
def readOnly(using Context): CaptureSet =
407418
val res = map(ReadOnlyMap())
408419
if mutability != Ignored then res.mutability = Reader
409420
res
410421

422+
def transClassifiers(using Context): Classifiers =
423+
def elemClassifiers =
424+
(ClassifiedAs(Nil) /: elems.map(_.transClassifiers))(joinClassifiers)
425+
if ccState.isSepCheck then
426+
dropEmpties()
427+
elemClassifiers
428+
else if isConst then
429+
elemClassifiers
430+
else
431+
UnknownClassifier
432+
433+
def tryClassifyAs(cls: ClassSymbol)(using Context): Boolean =
434+
elems.forall(_.tryClassifyAs(cls))
435+
436+
def adoptClassifier(cls: ClassSymbol)(using Context): Unit =
437+
for elem <- elems do
438+
elem.stripReadOnly match
439+
case fresh: FreshCap => fresh.hiddenSet.adoptClassifier(cls)
440+
case _ =>
441+
411442
/** A bad root `elem` is inadmissible as a member of this set. What is a bad roots depends
412443
* on the value of `rootLimit`.
413444
* If the limit is null, all capture roots are good.
@@ -557,6 +588,8 @@ object CaptureSet:
557588

558589
def owner = NoSymbol
559590

591+
def dropEmpties()(using Context) = this
592+
560593
private var isComplete = true
561594

562595
def setMutable()(using Context): Unit =
@@ -641,6 +674,16 @@ object CaptureSet:
641674

642675
def isMaybeSet = false // overridden in BiMapped
643676

677+
private var emptiesDropped = false
678+
679+
def dropEmpties()(using Context): this.type =
680+
if !emptiesDropped then
681+
emptiesDropped = true
682+
for elem <- elems do
683+
if elem.isKnownEmpty then
684+
elems -= empty
685+
this
686+
644687
/** A handler to be invoked if the root reference `cap` is added to this set */
645688
var rootAddedHandler: () => Context ?=> Unit = () => ()
646689

@@ -649,6 +692,25 @@ object CaptureSet:
649692
*/
650693
private[CaptureSet] var rootLimit: Symbol | Null = null
651694

695+
private var myClassifier: ClassSymbol = defn.AnyClass
696+
def classifier: ClassSymbol = myClassifier
697+
698+
private def narrowClassifier(cls: ClassSymbol)(using Context): Unit =
699+
val newClassifier = leastClassifier(classifier, cls)
700+
if newClassifier == defn.NothingClass then
701+
println(i"conflicting classifications for $this, was $classifier, now $cls")
702+
myClassifier = newClassifier
703+
704+
override def adoptClassifier(cls: ClassSymbol)(using Context): Unit =
705+
if !classifier.isSubClass(cls) then // serves as recursion brake
706+
narrowClassifier(cls)
707+
super.adoptClassifier(cls)
708+
709+
override def tryClassifyAs(cls: ClassSymbol)(using Context): Boolean =
710+
classifier.isSubClass(cls)
711+
|| super.tryClassifyAs(cls)
712+
&& { narrowClassifier(cls); true }
713+
652714
/** A handler to be invoked when new elems are added to this set */
653715
var newElemAddedHandler: Capability => Context ?=> Unit = _ => ()
654716

@@ -680,14 +742,15 @@ object CaptureSet:
680742
addIfHiddenOrFail(elem)
681743
else if !levelOK(elem) then
682744
failWith(IncludeFailure(this, elem, levelError = true)) // or `elem` is not visible at the level of the set.
745+
else if !elem.tryClassifyAs(classifier) then
746+
failWith(IncludeFailure(this, elem))
683747
else
684748
// id == 108 then assert(false, i"trying to add $elem to $this")
685749
assert(elem.isWellformed, elem)
686750
assert(!this.isInstanceOf[HiddenSet] || summon[VarState].isSeparating, summon[VarState])
687751
includeElem(elem)
688752
if isBadRoot(rootLimit, elem) then
689753
rootAddedHandler()
690-
newElemAddedHandler(elem)
691754
val normElem = if isMaybeSet then elem else elem.stripMaybe
692755
// assert(id != 5 || elems.size != 3, this)
693756
val res = deps.forall: dep =>
@@ -1344,9 +1407,10 @@ object CaptureSet:
13441407

13451408
/** A template for maps on capabilities where f(c) <: c and f(f(c)) = c */
13461409
private abstract class NarrowingCapabilityMap(using Context) extends BiTypeMap:
1347-
13481410
def apply(t: Type) = mapOver(t)
13491411

1412+
protected def isSameMap(other: BiTypeMap) = other.getClass == getClass
1413+
13501414
override def fuse(next: BiTypeMap)(using Context) = next match
13511415
case next: Inverse if next.inverse.getClass == getClass => Some(IdentityTypeMap)
13521416
case next: NarrowingCapabilityMap if next.getClass == getClass => Some(this)
@@ -1358,8 +1422,8 @@ object CaptureSet:
13581422
def inverse = NarrowingCapabilityMap.this
13591423
override def toString = NarrowingCapabilityMap.this.toString ++ ".inverse"
13601424
override def fuse(next: BiTypeMap)(using Context) = next match
1361-
case next: NarrowingCapabilityMap if next.inverse.getClass == getClass => Some(IdentityTypeMap)
1362-
case next: NarrowingCapabilityMap if next.getClass == getClass => Some(this)
1425+
case next: NarrowingCapabilityMap if isSameMap(next.inverse) => Some(IdentityTypeMap)
1426+
case next: NarrowingCapabilityMap if isSameMap(next) => Some(this)
13631427
case _ => None
13641428

13651429
lazy val inverse = Inverse()
@@ -1375,6 +1439,13 @@ object CaptureSet:
13751439
override def mapCapability(c: Capability, deep: Boolean) = c.readOnly
13761440
override def toString = "ReadOnly"
13771441

1442+
private class RestrictMap(val cls: ClassSymbol)(using Context) extends NarrowingCapabilityMap:
1443+
override def mapCapability(c: Capability, deep: Boolean) = c.restrict(cls)
1444+
override def toString = "Restrict"
1445+
override def isSameMap(other: BiTypeMap) = other match
1446+
case other: RestrictMap => cls == other.cls
1447+
case _ => false
1448+
13781449
/* Not needed:
13791450
def ofClass(cinfo: ClassInfo, argTypes: List[Type])(using Context): CaptureSet =
13801451
CaptureSet.empty
@@ -1402,6 +1473,9 @@ object CaptureSet:
14021473
case Reach(c1) =>
14031474
c1.widen.deepCaptureSet(includeTypevars = true)
14041475
.showing(i"Deep capture set of $c: ${c1.widen} = ${result}", capt)
1476+
case Restricted(c1, cls) =>
1477+
if cls == defn.NothingClass then CaptureSet.empty
1478+
else c1.captureSetOfInfo.restrict(cls) // todo: should we simplify using subsumption here?
14051479
case ReadOnly(c1) =>
14061480
c1.captureSetOfInfo.readOnly
14071481
case Maybe(c1) =>

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

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -40,6 +40,8 @@ object CapturingType:
4040
apply(parent1, refs ++ refs1, boxed)
4141
case _ =>
4242
if parent.derivesFromMutable then refs.setMutable()
43+
val classifier = parent.classifier
44+
refs.adoptClassifier(parent.classifier)
4345
AnnotatedType(parent, CaptureAnnotation(refs, boxed)(defn.RetainsAnnot))
4446

4547
/** An extractor for CapturingTypes. Capturing types are recognized if

0 commit comments

Comments
 (0)