Skip to content

Commit

Permalink
Drop @capability annotations (#20396)
Browse files Browse the repository at this point in the history
Replace with references that inherit trait `Capability`. 

Also: Handle tracked vals in classes.

As a next step, addCaptureRefinements should use the tracked logic for
all capturing parameters. Right now, we create a fresh capture set
variable instead, but that is too loose.
  • Loading branch information
odersky authored Jun 4, 2024
2 parents c6fbe6f + 81cf8d8 commit c51345f
Show file tree
Hide file tree
Showing 74 changed files with 565 additions and 219 deletions.
19 changes: 18 additions & 1 deletion compiler/src/dotty/tools/dotc/cc/CaptureOps.scala
Original file line number Diff line number Diff line change
Expand Up @@ -203,6 +203,23 @@ extension (tp: Type)
case _ =>
false

/** Tests whether the type derives from `caps.Capability`, which means
* references of this type are maximal capabilities.
*/
def derivesFromCapability(using Context): Boolean = tp.dealias match
case tp: (TypeRef | AppliedType) =>
val sym = tp.typeSymbol
if sym.isClass then sym.derivesFrom(defn.Caps_Capability)
else tp.superType.derivesFromCapability
case tp: TypeProxy =>
tp.superType.derivesFromCapability
case tp: AndType =>
tp.tp1.derivesFromCapability || tp.tp2.derivesFromCapability
case tp: OrType =>
tp.tp1.derivesFromCapability && tp.tp2.derivesFromCapability
case _ =>
false

/** Drop @retains annotations everywhere */
def dropAllRetains(using Context): Type = // TODO we should drop retains from inferred types before unpickling
val tm = new TypeMap:
Expand Down Expand Up @@ -408,7 +425,7 @@ extension (sym: Symbol)
/** The owner of the current level. Qualifying owners are
* - methods other than constructors and anonymous functions
* - anonymous functions, provided they either define a local
* root of type caps.Cap, or they are the rhs of a val definition.
* root of type caps.Capability, or they are the rhs of a val definition.
* - classes, if they are not staticOwners
* - _root_
*/
Expand Down
31 changes: 22 additions & 9 deletions compiler/src/dotty/tools/dotc/cc/CaptureSet.scala
Original file line number Diff line number Diff line change
Expand Up @@ -115,7 +115,7 @@ sealed abstract class CaptureSet extends Showable:
* capture set.
*/
protected final def addNewElem(elem: CaptureRef)(using Context, VarState): CompareResult =
if elem.isRootCapability || summon[VarState] == FrozenState then
if elem.isMaxCapability || summon[VarState] == FrozenState then
addThisElem(elem)
else
addThisElem(elem).orElse:
Expand Down Expand Up @@ -147,17 +147,26 @@ sealed abstract class CaptureSet extends Showable:
* this subsumes this.f
* x subsumes y ==> x* subsumes y, x subsumes y?
* x subsumes y ==> x* subsumes y*, x? subsumes y?
* x: x1.type /\ x1 subsumes y ==> x subsumes y
*/
extension (x: CaptureRef)
private def subsumes(y: CaptureRef)(using Context): Boolean =
(x eq y)
|| x.isRootCapability
|| y.match
case y: TermRef => y.prefix eq x
case y: TermRef =>
(y.prefix eq x)
|| y.info.match
case y1: CaptureRef => x.subsumes(y1)
case _ => false
case MaybeCapability(y1) => x.stripMaybe.subsumes(y1)
case _ => false
|| x.match
case ReachCapability(x1) => x1.subsumes(y.stripReach)
case x: TermRef =>
x.info match
case x1: CaptureRef => x1.subsumes(y)
case _ => false
case _ => false

/** {x} <:< this where <:< is subcapturing, but treating all variables
Expand All @@ -167,11 +176,11 @@ sealed abstract class CaptureSet extends Showable:
if comparer.isInstanceOf[ExplainingTypeComparer] then // !!! DEBUG
reporting.trace.force(i"$this accountsFor $x, ${x.captureSetOfInfo}?", show = true):
elems.exists(_.subsumes(x))
|| !x.isRootCapability && x.captureSetOfInfo.subCaptures(this, frozen = true).isOK
|| !x.isMaxCapability && x.captureSetOfInfo.subCaptures(this, frozen = true).isOK
else
reporting.trace(i"$this accountsFor $x, ${x.captureSetOfInfo}?", show = true):
elems.exists(_.subsumes(x))
|| !x.isRootCapability && x.captureSetOfInfo.subCaptures(this, frozen = true).isOK
|| !x.isMaxCapability && x.captureSetOfInfo.subCaptures(this, frozen = true).isOK

/** A more optimistic version of accountsFor, which does not take variable supersets
* of the `x` reference into account. A set might account for `x` if it accounts
Expand All @@ -183,7 +192,7 @@ sealed abstract class CaptureSet extends Showable:
def mightAccountFor(x: CaptureRef)(using Context): Boolean =
reporting.trace(i"$this mightAccountFor $x, ${x.captureSetOfInfo}?", show = true) {
elems.exists(_.subsumes(x))
|| !x.isRootCapability
|| !x.isMaxCapability
&& {
val elems = x.captureSetOfInfo.elems
!elems.isEmpty && elems.forall(mightAccountFor)
Expand Down Expand Up @@ -383,7 +392,7 @@ object CaptureSet:

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

def apply(elems: Refs)(using Context): CaptureSet.Const =
if elems.isEmpty then empty else Const(elems)
Expand Down Expand Up @@ -491,6 +500,7 @@ object CaptureSet:
CompareResult.LevelError(this, elem)
else
//if id == 34 then assert(!elem.isUniversalRootCapability)
assert(elem.isTrackableRef, elem)
elems += elem
if elem.isRootCapability then
rootAddedHandler()
Expand Down Expand Up @@ -1032,7 +1042,9 @@ object CaptureSet:

/** The capture set of the type underlying CaptureRef */
def ofInfo(ref: CaptureRef)(using Context): CaptureSet = ref match
case ref: TermRef if ref.isRootCapability => ref.singletonCaptureSet
case ref: (TermRef | TermParamRef) if ref.isMaxCapability =>
if ref.isTrackableRef then ref.singletonCaptureSet
else CaptureSet.universal
case ReachCapability(ref1) => deepCaptureSet(ref1.widen)
.showing(i"Deep capture set of $ref: ${ref1.widen} = $result", capt)
case _ => ofType(ref.underlying, followResult = true)
Expand All @@ -1046,7 +1058,8 @@ object CaptureSet:
case tp: TermParamRef =>
tp.captureSet
case tp: TypeRef =>
if tp.typeSymbol == defn.Caps_Cap then universal else empty
if tp.derivesFromCapability then universal // TODO: maybe return another value that indicates that the underltinf ref is maximal?
else empty
case _: TypeParamRef =>
empty
case CapturingType(parent, refs) =>
Expand Down Expand Up @@ -1074,7 +1087,7 @@ object CaptureSet:
case _ =>
empty
recur(tp)
.showing(i"capture set of $tp = $result", captDebug)
//.showing(i"capture set of $tp = $result", captDebug)

private def deepCaptureSet(tp: Type)(using Context): CaptureSet =
val collect = new TypeAccumulator[CaptureSet]:
Expand Down
49 changes: 35 additions & 14 deletions compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
Original file line number Diff line number Diff line change
Expand Up @@ -157,15 +157,17 @@ object CheckCaptures:
case _ =>
case AnnotatedType(_, ann) if ann.symbol == defn.UncheckedCapturesAnnot =>
()
case t =>
case CapturingType(parent, refs) =>
if variance >= 0 then
t.captureSet.disallowRootCapability: () =>
refs.disallowRootCapability: () =>
def part = if t eq tp then "" else i"the part $t of "
report.error(
em"""$what cannot $have $tp since
|${part}that type captures the root capability `cap`.
|$addendum""",
pos)
traverse(parent)
case t =>
traverseChildren(t)
check.traverse(tp)
end disallowRootCapabilitiesIn
Expand Down Expand Up @@ -537,8 +539,8 @@ class CheckCaptures extends Recheck, SymTransformer:
*/
def addParamArgRefinements(core: Type, initCs: CaptureSet): (Type, CaptureSet) =
var refined: Type = core
var allCaptures: CaptureSet = if setup.isCapabilityClassRef(core)
then CaptureSet.universal else initCs
var allCaptures: CaptureSet =
if core.derivesFromCapability then CaptureSet.universal else initCs
for (getterName, argType) <- mt.paramNames.lazyZip(argTypes) do
val getter = cls.info.member(getterName).suchThat(_.is(ParamAccessor)).symbol
if getter.termRef.isTracked && !getter.is(Private) then
Expand Down Expand Up @@ -572,8 +574,10 @@ class CheckCaptures extends Recheck, SymTransformer:
val TypeApply(fn, args) = tree
val polyType = atPhase(thisPhase.prev):
fn.tpe.widen.asInstanceOf[TypeLambda]
def isExempt(sym: Symbol) =
sym.isTypeTestOrCast || sym == defn.Compiletime_erasedValue
for case (arg: TypeTree, formal, pname) <- args.lazyZip(polyType.paramRefs).lazyZip((polyType.paramNames)) do
if !tree.symbol.isTypeTestOrCast then
if !isExempt(tree.symbol) then
def where = if fn.symbol.exists then i" in an argument of ${fn.symbol}" else ""
disallowRootCapabilitiesIn(arg.knownType, NoSymbol,
i"Sealed type variable $pname", "be instantiated to",
Expand Down Expand Up @@ -1004,7 +1008,7 @@ class CheckCaptures extends Recheck, SymTransformer:
if (ares1 eq ares) && (aargs1 eq aargs) then actual
else reconstruct(aargs1, ares1)

(resTp, curEnv.captured)
(resTp, CaptureSet(curEnv.captured.elems))
end adaptFun

/** Adapt type function type `actual` to the expected type.
Expand All @@ -1026,14 +1030,14 @@ class CheckCaptures extends Recheck, SymTransformer:
if ares1 eq ares then actual
else reconstruct(ares1)

(resTp, curEnv.captured)
(resTp, CaptureSet(curEnv.captured.elems))
end adaptTypeFun

def adaptInfo(actual: Type, expected: Type, covariant: Boolean): String =
val arrow = if covariant then "~~>" else "<~~"
i"adapting $actual $arrow $expected"

def adapt(actual: Type, expected: Type, covariant: Boolean): Type = trace(adaptInfo(actual, expected, covariant), recheckr, show = true) {
def adapt(actual: Type, expected: Type, covariant: Boolean): Type = trace(adaptInfo(actual, expected, covariant), recheckr, show = true):
if expected.isInstanceOf[WildcardType] then actual
else
// Decompose the actual type into the inner shape type, the capture set and the box status
Expand Down Expand Up @@ -1113,7 +1117,22 @@ class CheckCaptures extends Recheck, SymTransformer:
adaptedType(!boxed)
else
adaptedType(boxed)
}
end adapt

/** If result derives from caps.Capability, yet is not a capturing type itself,
* make its capture set explicit.
*/
def makeCaptureSetExplicit(result: Type) = result match
case CapturingType(_, _) => result
case _ =>
if result.derivesFromCapability then
val cap: CaptureRef = actual match
case ref: CaptureRef if ref.isTracked =>
ref
case _ =>
defn.captureRoot.termRef // TODO: skolemize?
CapturingType(result, cap.singletonCaptureSet)
else result

if expected == LhsProto || expected.isSingleton && actual.isSingleton then
actual
Expand All @@ -1129,10 +1148,12 @@ class CheckCaptures extends Recheck, SymTransformer:
case _ =>
case _ =>
val adapted = adapt(actualw.withReachCaptures(actual), expected, covariant = true)
if adapted ne actualw then
capt.println(i"adapt boxed $actual vs $expected ===> $adapted")
adapted
else actual
makeCaptureSetExplicit:
if adapted ne actualw then
capt.println(i"adapt boxed $actual vs $expected ===> $adapted")
adapted
else
actual
end adaptBoxed

/** Check overrides again, taking capture sets into account.
Expand Down Expand Up @@ -1305,7 +1326,7 @@ class CheckCaptures extends Recheck, SymTransformer:
case ref: TermParamRef
if !allowed.contains(ref) && !seen.contains(ref) =>
seen += ref
if ref.underlying.isRef(defn.Caps_Cap) then
if ref.underlying.isRef(defn.Caps_Capability) then
report.error(i"escaping local reference $ref", tree.srcPos)
else
val widened = ref.captureSetOfInfo
Expand Down
54 changes: 20 additions & 34 deletions compiler/src/dotty/tools/dotc/cc/Setup.scala
Original file line number Diff line number Diff line change
Expand Up @@ -23,7 +23,6 @@ trait SetupAPI:
def setupUnit(tree: Tree, recheckDef: DefRecheck)(using Context): Unit
def isPreCC(sym: Symbol)(using Context): Boolean
def postCheck()(using Context): Unit
def isCapabilityClassRef(tp: Type)(using Context): Boolean

object Setup:

Expand Down Expand Up @@ -58,8 +57,21 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI:
private val toBeUpdated = new mutable.HashSet[Symbol]

private def newFlagsFor(symd: SymDenotation)(using Context): FlagSet =
if symd.isAllOf(PrivateParamAccessor) && symd.owner.is(CaptureChecked) && !symd.hasAnnotation(defn.ConstructorOnlyAnnot)
then symd.flags &~ Private | Recheck.ResetPrivate

object containsCovarRetains extends TypeAccumulator[Boolean]:
def apply(x: Boolean, tp: Type): Boolean =
if x then true
else if tp.derivesFromCapability && variance >= 0 then true
else tp match
case AnnotatedType(_, ann) if ann.symbol.isRetains && variance >= 0 => true
case _ => foldOver(x, tp)
def apply(tp: Type): Boolean = apply(false, tp)

if symd.isAllOf(PrivateParamAccessor)
&& symd.owner.is(CaptureChecked)
&& !symd.hasAnnotation(defn.ConstructorOnlyAnnot)
&& containsCovarRetains(symd.symbol.originDenotation.info)
then symd.flags &~ Private
else symd.flags

def isPreCC(sym: Symbol)(using Context): Boolean =
Expand All @@ -68,31 +80,6 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI:
&& !sym.owner.is(CaptureChecked)
&& !defn.isFunctionSymbol(sym.owner)

private val capabilityClassMap = new util.HashMap[Symbol, Boolean]

/** Check if the class is capability, which means:
* 1. the class has a capability annotation,
* 2. or at least one of its parent type has universal capability.
*/
def isCapabilityClassRef(tp: Type)(using Context): Boolean = tp.dealiasKeepAnnots match
case _: TypeRef | _: AppliedType =>
val sym = tp.classSymbol
def checkSym: Boolean =
sym.hasAnnotation(defn.CapabilityAnnot)
|| sym.info.parents.exists(hasUniversalCapability)
sym.isClass && capabilityClassMap.getOrElseUpdate(sym, checkSym)
case _ => false

private def hasUniversalCapability(tp: Type)(using Context): Boolean = tp.dealiasKeepAnnots match
case CapturingType(parent, refs) =>
refs.isUniversal || hasUniversalCapability(parent)
case AnnotatedType(parent, ann) =>
if ann.symbol.isRetains then
try ann.tree.toCaptureSet.isUniversal || hasUniversalCapability(parent)
catch case ex: IllegalCaptureRef => false
else hasUniversalCapability(parent)
case tp => isCapabilityClassRef(tp)

private def fluidify(using Context) = new TypeMap with IdempotentCaptRefMap:
def apply(t: Type): Type = t match
case t: MethodType =>
Expand Down Expand Up @@ -196,7 +183,9 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI:
case cls: ClassSymbol
if !defn.isFunctionClass(cls) && cls.is(CaptureChecked) =>
cls.paramGetters.foldLeft(tp) { (core, getter) =>
if atPhase(thisPhase.next)(getter.termRef.isTracked) then
if atPhase(thisPhase.next)(getter.termRef.isTracked)
&& !getter.is(Tracked)
then
val getterType =
mapInferred(refine = false)(tp.memberInfo(getter)).strippedDealias
RefinedType(core, getter.name,
Expand Down Expand Up @@ -317,10 +306,7 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI:
case t: TypeVar =>
this(t.underlying)
case t =>
// Map references to capability classes C to C^
if isCapabilityClassRef(t)
then CapturingType(t, defn.expandedUniversalSet, boxed = false)
else recur(t)
recur(t)
end expandAliases

val tp1 = expandAliases(tp) // TODO: Do we still need to follow aliases?
Expand Down Expand Up @@ -592,7 +578,7 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI:
if sym.isClass then
!sym.isPureClass
else
sym != defn.Caps_Cap && instanceCanBeImpure(tp.superType)
sym != defn.Caps_Capability && instanceCanBeImpure(tp.superType)
case tp: (RefinedOrRecType | MatchType) =>
instanceCanBeImpure(tp.underlying)
case tp: AndType =>
Expand Down
5 changes: 2 additions & 3 deletions compiler/src/dotty/tools/dotc/core/Definitions.scala
Original file line number Diff line number Diff line change
Expand Up @@ -991,7 +991,7 @@ class Definitions {

@tu lazy val CapsModule: Symbol = requiredModule("scala.caps")
@tu lazy val captureRoot: TermSymbol = CapsModule.requiredValue("cap")
@tu lazy val Caps_Cap: TypeSymbol = CapsModule.requiredType("Cap")
@tu lazy val Caps_Capability: TypeSymbol = CapsModule.requiredType("Capability")
@tu lazy val Caps_reachCapability: TermSymbol = CapsModule.requiredMethod("reachCapability")
@tu lazy val CapsUnsafeModule: Symbol = requiredModule("scala.caps.unsafe")
@tu lazy val Caps_unsafeAssumePure: Symbol = CapsUnsafeModule.requiredMethod("unsafeAssumePure")
Expand All @@ -1014,7 +1014,6 @@ class Definitions {
@tu lazy val BeanPropertyAnnot: ClassSymbol = requiredClass("scala.beans.BeanProperty")
@tu lazy val BooleanBeanPropertyAnnot: ClassSymbol = requiredClass("scala.beans.BooleanBeanProperty")
@tu lazy val BodyAnnot: ClassSymbol = requiredClass("scala.annotation.internal.Body")
@tu lazy val CapabilityAnnot: ClassSymbol = requiredClass("scala.annotation.capability")
@tu lazy val ChildAnnot: ClassSymbol = requiredClass("scala.annotation.internal.Child")
@tu lazy val ContextResultCountAnnot: ClassSymbol = requiredClass("scala.annotation.internal.ContextResultCount")
@tu lazy val ProvisionalSuperClassAnnot: ClassSymbol = requiredClass("scala.annotation.internal.ProvisionalSuperClass")
Expand Down Expand Up @@ -2033,7 +2032,7 @@ class Definitions {
*/
@tu lazy val ccExperimental: Set[Symbol] = Set(
CapsModule, CapsModule.moduleClass, PureClass,
CapabilityAnnot, RequiresCapabilityAnnot,
RequiresCapabilityAnnot,
RetainsAnnot, RetainsCapAnnot, RetainsByNameAnnot)

/** Experimental language features defined in `scala.runtime.stdLibPatches.language.experimental`.
Expand Down
Loading

0 comments on commit c51345f

Please sign in to comment.