Skip to content

Go back towards a pure capability system #21764

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Closed
wants to merge 17 commits into from
Closed
Show file tree
Hide file tree
Changes from 1 commit
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Prev Previous commit
Next Next commit
Always charge deep capture set of function arguments to cv
Also: In Recheck-apply, use deep capture sets of arguments in computing the
result alternative.

Drop restrictions on leaking reach capabilities in markFree.

Revise visibility criterion for paths.

Together these changes now implement a classical capability system with reach capabilities.
References that are used later after passing some arguments are already recorded in capture sets
of earlier stages (exception: closure results).
  • Loading branch information
odersky committed Oct 14, 2024
commit 16f86f044d601dffb9fed1bbaf28a90a13f862a2
5 changes: 5 additions & 0 deletions compiler/src/dotty/tools/dotc/cc/CaptureOps.scala
Original file line number Diff line number Diff line change
Expand Up @@ -274,6 +274,11 @@ extension (tp: Type)
case _ =>
tp

/** The first element of this path type */
final def pathRoot(using Context): Type = tp.dealias match
case tp1: NamedType if tp1.symbol.owner.isClass => tp1.prefix.pathRoot
case _ => tp

/** If this is a unboxed capturing type with nonempty capture set, its boxed version.
* Or, if type is a TypeBounds of capturing types, the version where the bounds are boxed.
* The identity for all other types.
Expand Down
140 changes: 30 additions & 110 deletions compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
Original file line number Diff line number Diff line change
Expand Up @@ -385,34 +385,8 @@ class CheckCaptures extends Recheck, SymTransformer:
// Only captured references that are visible from the environment
// should be included.
val included = cs.filter: c =>
c.stripReach match
case ref: NamedType =>
val refSym = ref.symbol
val refOwner = refSym.owner
val isVisible = isVisibleFromEnv(refOwner, env)
if isVisible && !ref.isRootCapability then
ref match
case ref: TermRef if ref.prefix `ne` NoPrefix =>
// If c is a path of a class defined outside the environment,
// we check the capture set of its info.
checkSubsetEnv(ref.captureSetOfInfo, env)
case _ =>
if !isVisible
&& (c.isReach || ref.isType)
&& (!ccConfig.useSealed || refSym.is(Param))
&& refOwner == env.owner
then
if refSym.hasAnnotation(defn.UnboxAnnot) then
capt.println(i"exempt: $ref in $refOwner")
else
// Reach capabilities that go out of scope have to be approximated
// by their underlying capture set, which cannot be universal.
// Reach capabilities of @unboxed parameters are exempted.
val cs = CaptureSet.ofInfo(c)
cs.disallowRootCapability: () =>
report.error(em"Local reach capability $c leaks into capture scope of ${env.ownerString}", pos)
checkSubset(cs, env.captured, pos, provenance(env))
isVisible
c.stripReach.pathRoot match
case ref: NamedType => isVisibleFromEnv(ref.symbol.owner, env)
case ref: ThisType => isVisibleFromEnv(ref.cls, env)
case _ => false
checkSubset(included, env.captured, pos, provenance(env))
Expand All @@ -424,48 +398,14 @@ class CheckCaptures extends Recheck, SymTransformer:
end markFree

/** Include references captured by the called method in the current environment stack */
def includeCallCaptures(sym: Symbol, pos: SrcPos)(using Context): Unit =
if sym.exists && curEnv.isOpen then markFree(capturedVars(sym), pos)

private val prefixCalls = util.EqHashSet[GenericApply]()
private val unboxedArgs = util.EqHashSet[Tree]()

def handleCall(meth: Symbol, call: GenericApply, eval: () => Type)(using Context): Type =
if prefixCalls.remove(call) then return eval()

val unboxedParamNames =
meth.rawParamss.flatMap: params =>
params.collect:
case param if param.hasAnnotation(defn.UnboxAnnot) =>
param.name
.toSet

def markUnboxedArgs(call: GenericApply): Unit = call.fun.tpe.widen match
case MethodType(pnames) =>
for (pname, arg) <- pnames.lazyZip(call.args) do
if unboxedParamNames.contains(pname) then
unboxedArgs.add(arg)
case _ =>

def markPrefixCalls(tree: Tree): Unit = tree match
case tree: GenericApply =>
prefixCalls.add(tree)
markUnboxedArgs(tree)
markPrefixCalls(tree.fun)
case _ =>

markUnboxedArgs(call)
markPrefixCalls(call.fun)
val res = eval()
includeCallCaptures(meth, call.srcPos)
res
end handleCall
def includeCallCaptures(sym: Symbol, resType: Type, pos: SrcPos)(using Context): Unit = resType match
case _: MethodOrPoly => // wait until method is fully applied
case _ =>
if sym.exists && curEnv.isOpen then markFree(capturedVars(sym), pos)

override def recheckIdent(tree: Ident, pt: Type)(using Context): Type =
if tree.symbol.is(Method) then
if tree.symbol.info.isParameterless then
// there won't be an apply; need to include call captures now
includeCallCaptures(tree.symbol, tree.srcPos)
includeCallCaptures(tree.symbol, tree.symbol.info, tree.srcPos)
else if !tree.symbol.isStatic then
//debugShowEnvs()
def addSelects(ref: TermRef, pt: Type): TermRef = pt match
Expand Down Expand Up @@ -570,15 +510,16 @@ class CheckCaptures extends Recheck, SymTransformer:
tp.derivedCapturingType(forceBox(parent), refs)
mapArgUsing(forceBox)
else
handleCall(meth, tree, () => super.recheckApply(tree, pt))
val res = super.recheckApply(tree, pt)
includeCallCaptures(meth, res, tree.srcPos)
res
end recheckApply

protected override
def recheckArg(arg: Tree, formal: Type)(using Context): Type =
val argType = recheck(arg, formal)
if unboxedArgs.contains(arg) then
capt.println(i"charging deep capture set of $arg: ${argType} = ${argType.deepCaptureSet}")
markFree(argType.deepCaptureSet, arg.srcPos)
capt.println(i"charging deep capture set of $arg: ${argType} = ${argType.deepCaptureSet}")
markFree(argType.deepCaptureSet, arg.srcPos)
argType

/** A specialized implementation of the apply rule.
Expand All @@ -589,27 +530,18 @@ class CheckCaptures extends Recheck, SymTransformer:
* ---------------------
* E |- f(a): Tr^C
*
* If the function `f` does not have an `@unboxed` parameter, then
* any unboxing it does would be charged to the environment of the function
* so they have to appear in Cq. Since any capabilities of the result of the
* application must already be present in the application, an upper
* approximation of the result capture set is Cq \union Ca, where `Ca`
* is the capture set of the argument.
* If the function `f` does have an `@unboxed` parameter, then it could in addition
* unbox reach capabilities over its formal parameter. Therefore, the approximation
* would be `Cq \union dcs(Ca)` instead.
* If the type of the function `f` does not mention any formal parameters
* any capabilities of the result of the application must already be present in
* the application. So an upper approximation of the result capture set is Cq \union Ca,
* where `Ca` is the deep capture set of the argument.
* If the approximation is known to subcapture the declared result Cr, we pick it for C
* otherwise we pick Cr.
* otherwise we pick Cr. ???
*/
protected override
def recheckApplication(tree: Apply, qualType: Type, funType: MethodType, argTypes: List[Type])(using Context): Type =
val appType = Existential.toCap(super.recheckApplication(tree, qualType, funType, argTypes))
val qualCaptures = qualType.captureSet
val argCaptures =
for (arg, argType) <- tree.args.lazyZip(argTypes) yield
if unboxedArgs.remove(arg) // need to ensure the remove happens, that's why argCaptures is computed even if not needed.
then argType.deepCaptureSet
else argType.captureSet
val argCaptures = argTypes.map(_.deepCaptureSet)
appType match
case appType @ CapturingType(appType1, refs)
if qualType.exists
Expand Down Expand Up @@ -704,8 +636,10 @@ class CheckCaptures extends Recheck, SymTransformer:
i"Sealed type variable $pname", "be instantiated to",
i"This is often caused by a local capability$where\nleaking as part of its result.",
tree.srcPos)
try handleCall(meth, tree, () => Existential.toCap(super.recheckTypeApply(tree, pt)))
finally checkContains(tree)
val res = Existential.toCap(super.recheckTypeApply(tree, pt))
includeCallCaptures(meth, res, tree.srcPos)
checkContains(tree)
res
end recheckTypeApply

/** Faced with a tree of form `caps.contansImpl[CS, r.type]`, check that `R` is a tracked
Expand Down Expand Up @@ -1156,12 +1090,7 @@ class CheckCaptures extends Recheck, SymTransformer:
(erefs /: erefs.elems): (erefs, eref) =>
eref match
case eref: ThisType if isPureContext(ctx.owner, eref.cls) =>

def pathRoot(aref: Type): Type = aref match
case aref: NamedType if aref.symbol.owner.isClass => pathRoot(aref.prefix)
case _ => aref

def isOuterRef(aref: Type): Boolean = pathRoot(aref) match
def isOuterRef(aref: Type): Boolean = aref.pathRoot match
case aref: NamedType => eref.cls.isProperlyContainedIn(aref.symbol.owner)
case aref: ThisType => eref.cls.isProperlyContainedIn(aref.cls)
case _ => false
Expand All @@ -1171,7 +1100,7 @@ class CheckCaptures extends Recheck, SymTransformer:
// Include implicitly added outer references in the capture set of the class of `eref`.
for outerRef <- outerRefs.elems do
if !erefs.elems.contains(outerRef)
&& !pathRoot(outerRef).isInstanceOf[ThisType]
&& !outerRef.pathRoot.isInstanceOf[ThisType]
// we don't need to add outer ThisTypes as these are anyway added as path
// prefixes at the use site. And this exemption is required since capture sets
// of non-local classes are always empty, so we can't add an outer this to them.
Expand Down Expand Up @@ -1328,6 +1257,12 @@ class CheckCaptures extends Recheck, SymTransformer:

/** If actual is a tracked CaptureRef `a` and widened is a capturing type T^C,
* improve `T^C` to `T^{a}`, following the VAR rule of CC.
* TODO: We probably should do this also for other top-level occurrences of captures
* E.g.
* class Foo { def a: C^{io}; val def: C^{async} }
* val foo: Foo^{io, async}
* Then
* foo: Foo { def a: C^{foo}; def b: C^{foo} }^{foo}
*/
private def improveCaptures(widened: Type, actual: Type)(using Context): Type = actual match
case ref: CaptureRef if ref.isTracked =>
Expand Down Expand Up @@ -1388,21 +1323,6 @@ class CheckCaptures extends Recheck, SymTransformer:
!setup.isPreCC(overriding) && !setup.isPreCC(overridden)

override def checkInheritedTraitParameters: Boolean = false

/** Check that overrides don't change the @unbox status of their parameters */
override def additionalChecks(member: Symbol, other: Symbol)(using Context): Unit =
for
(params1, params2) <- member.rawParamss.lazyZip(other.rawParamss)
(param1, param2) <- params1.lazyZip(params2)
do
if param1.hasAnnotation(defn.UnboxAnnot) != param2.hasAnnotation(defn.UnboxAnnot) then
report.error(
OverrideError(
i"has a parameter ${param1.name} with different @unbox status than the corresponding parameter in the overridden definition",
self, member, other, self.memberInfo(member), self.memberInfo(other)
),
if member.owner == clazz then member.srcPos else clazz.srcPos
)
end OverridingPairsCheckerCC

def traverse(t: Tree)(using Context) =
Expand Down
1 change: 0 additions & 1 deletion compiler/src/dotty/tools/dotc/core/Definitions.scala
Original file line number Diff line number Diff line change
Expand Up @@ -1057,7 +1057,6 @@ class Definitions {
@tu lazy val ExperimentalAnnot: ClassSymbol = requiredClass("scala.annotation.experimental")
@tu lazy val ThrowsAnnot: ClassSymbol = requiredClass("scala.throws")
@tu lazy val TransientAnnot: ClassSymbol = requiredClass("scala.transient")
@tu lazy val UnboxAnnot: ClassSymbol = requiredClass("scala.caps.unbox")
@tu lazy val UncheckedAnnot: ClassSymbol = requiredClass("scala.unchecked")
@tu lazy val UncheckedStableAnnot: ClassSymbol = requiredClass("scala.annotation.unchecked.uncheckedStable")
@tu lazy val UncheckedVarianceAnnot: ClassSymbol = requiredClass("scala.annotation.unchecked.uncheckedVariance")
Expand Down
2 changes: 1 addition & 1 deletion compiler/src/dotty/tools/dotc/core/Types.scala
Original file line number Diff line number Diff line change
Expand Up @@ -1796,7 +1796,7 @@ object Types extends TypeUtils {

/** Is this either not a method at all, or a parameterless method? */
final def isParameterless(using Context): Boolean = stripPoly match {
case mt: MethodType => false
case mt: MethodOrPoly => false
case _ => true
}

Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -384,7 +384,7 @@ final class LazyListIterable[+A] private(@untrackedCaptures lazyState: () => Laz
* @param suffix The collection that gets appended to this lazy list
* @return The lazy list containing elements of this lazy list and the iterable object.
*/
def lazyAppendedAll[B >: A](suffix: => collection.IterableOnce[B]^): LazyListIterable[B]^{this, suffix} =
def lazyAppendedAll[B >: A](suffix: => collection.IterableOnce[B]^): LazyListIterable[B]^{this, suffix*} =
newLL {
if (isEmpty) suffix match {
case lazyList: LazyListIterable[B] => lazyList.state // don't recompute the LazyListIterable
Expand Down Expand Up @@ -497,7 +497,7 @@ final class LazyListIterable[+A] private(@untrackedCaptures lazyState: () => Laz
*
* $preservesLaziness
*/
def prepended[B >: A](elem: B): LazyListIterable[B] = newLL(sCons(elem, this))
def prepended[B >: A](elem: B): LazyListIterable[B]^{this} = newLL(sCons(elem, this))

/** @inheritdoc
*
Expand Down Expand Up @@ -1137,7 +1137,7 @@ object LazyListIterable extends IterableFactory[LazyListIterable] {
/** Construct a LazyListIterable consisting of the concatenation of the given LazyListIterable and
* another LazyListIterable.
*/
def #:::[B >: A](prefix: LazyListIterable[B]^): LazyListIterable[B]^{prefix, l} = prefix lazyAppendedAll l
def #:::[B >: A](prefix: LazyListIterable[B]^): LazyListIterable[B]^{prefix, l*} = prefix lazyAppendedAll l

object #:: {
def unapply[A](s: LazyListIterable[A]^): Option[(A, LazyListIterable[A]^{s})] =
Expand All @@ -1155,7 +1155,7 @@ object LazyListIterable extends IterableFactory[LazyListIterable] {
/** Creates a State from an Iterator, with another State appended after the Iterator
* is empty.
*/
private def stateFromIteratorConcatSuffix[A](it: Iterator[A]^)(suffix: => State[A]^): State[A]^{it, suffix} =
private def stateFromIteratorConcatSuffix[A](it: Iterator[A]^)(suffix: => State[A]^): State[A]^{it, suffix*} =
if (it.hasNext) sCons(it.next(), newLL(stateFromIteratorConcatSuffix(it)(suffix)))
else suffix

Expand Down
2 changes: 1 addition & 1 deletion tests/neg-custom-args/captures/cc-selftype-unsound.scala
Original file line number Diff line number Diff line change
Expand Up @@ -11,5 +11,5 @@ def magic(l: Logger^): Logger =
Boxed[Logger^{this}](l) // error
val x = new Foo
val y = x.foo.unbox // y: Logger^{x}
val z: Logger = y // now the capability becomes pure
val z: Logger = y // error
z
29 changes: 0 additions & 29 deletions tests/neg-custom-args/captures/effect-swaps-explicit.check

This file was deleted.

76 changes: 0 additions & 76 deletions tests/neg-custom-args/captures/effect-swaps-explicit.scala

This file was deleted.

Loading