Skip to content
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

Add path support for capture checking #21445

Open
wants to merge 9 commits into
base: main
Choose a base branch
from
Open
Show file tree
Hide file tree
Changes from 7 commits
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
4 changes: 2 additions & 2 deletions compiler/src/dotty/tools/dotc/ast/untpd.scala
Original file line number Diff line number Diff line change
Expand Up @@ -525,8 +525,8 @@ object untpd extends Trees.Instance[Untyped] with UntypedTreeInfo {
def makeRetaining(parent: Tree, refs: List[Tree], annotName: TypeName)(using Context): Annotated =
Annotated(parent, New(scalaAnnotationDot(annotName), List(refs)))

def makeCapsOf(id: Ident)(using Context): Tree =
TypeApply(Select(scalaDot(nme.caps), nme.capsOf), id :: Nil)
def makeCapsOf(tp: RefTree)(using Context): Tree =
TypeApply(Select(scalaDot(nme.caps), nme.capsOf), tp :: Nil)

def makeCapsBound()(using Context): Tree =
makeRetaining(
Expand Down
2 changes: 1 addition & 1 deletion compiler/src/dotty/tools/dotc/cc/CaptureOps.scala
Original file line number Diff line number Diff line change
Expand Up @@ -194,7 +194,7 @@ extension (tp: Type)
true
case tp: TermRef =>
((tp.prefix eq NoPrefix)
|| tp.symbol.is(ParamAccessor) && tp.prefix.isThisTypeOf(tp.symbol.owner)
|| tp.symbol.isField && !tp.symbol.isStatic && tp.prefix.isTrackableRef
|| tp.isRootCapability
) && !tp.symbol.isOneOf(UnstableValueFlags)
case tp: TypeRef =>
Expand Down
49 changes: 34 additions & 15 deletions compiler/src/dotty/tools/dotc/cc/CaptureRef.scala
Original file line number Diff line number Diff line change
Expand Up @@ -61,18 +61,19 @@ trait CaptureRef extends TypeProxy, ValueType:
case tp: TermParamRef => tp.underlying.derivesFrom(defn.Caps_Exists)
case _ => false

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

/** The capture set consisting of exactly this reference */
final def singletonCaptureSet(using Context): CaptureSet.Const =
if mySingletonCaptureSet == null then
mySingletonCaptureSet = CaptureSet(this.normalizedRef)
mySingletonCaptureSet = CaptureSet(this)
mySingletonCaptureSet.uncheckedNN

/** The capture set of the type underlying this reference */
Expand All @@ -97,27 +98,45 @@ trait CaptureRef extends TypeProxy, ValueType:
* 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
* TODO: Document path cases
*/
final def subsumes(y: CaptureRef)(using Context): Boolean =
Copy link
Contributor

@odersky odersky Sep 24, 2024

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

We need to get better reassurance that this does the right thing. It looks too complicated to be able to argue it's obviously correct. What would help:

  • A formal set of rules for subcapturing.
  • A rendition of these rules as a doc comment for this method. It's a shame that the old doc comment was not updated in any way.
  • More extensive tests that try to test all combinations. I saw we have neg tests but no new pos tests.


def subsumingRefs(x: Type, y: Type): Boolean = x match
case x: CaptureRef => y match
case y: CaptureRef => x.subsumes(y)
case _ => false
case _ => false

def viaInfo(info: Type)(test: Type => Boolean): Boolean = info.match
case info: SingletonCaptureRef => test(info)
case info: AndType => test(info.tp1) || test(info.tp2)
case info: OrType => test(info.tp1) && test(info.tp2)
Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

We can recur on left and right tress as well.

case _ => false

(this eq y)
|| this.isRootCapability
|| y.match
case y: TermRef =>
(y.prefix eq this)
|| y.info.match
case y1: SingletonCaptureRef => this.subsumes(y1)
y.prefix.match
case ypre: CaptureRef =>
this.subsumes(ypre)
|| this.match
case x @ TermRef(xpre: CaptureRef, _) if x.symbol == y.symbol =>
subsumingRefs(xpre, ypre) && subsumingRefs(ypre, xpre)
Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

If x.symbol == y.symbol, then x.prefix must equivalent to y.prefix in order to show x subsumes y. Is it simpler to just use TypeCompare to check them? I think we have to prove (x subsumes y) && (y subsumes x) ==> x =:= y.

case _ =>
false
case _ => false
|| viaInfo(y.info)(subsumingRefs(this, _))
case MaybeCapability(y1) => this.stripMaybe.subsumes(y1)
case _ => false
|| this.match
case ReachCapability(x1) => x1.subsumes(y.stripReach)
case x: TermRef =>
x.info match
case x1: SingletonCaptureRef => x1.subsumes(y)
case _ => false
case x: TermRef => viaInfo(x.info)(subsumingRefs(_, y))
case x: TermParamRef => subsumesExistentially(x, y)
case x: TypeRef => assumedContainsOf(x).contains(y)
case _ => false
end subsumes

def assumedContainsOf(x: TypeRef)(using Context): SimpleIdentitySet[CaptureRef] =
CaptureSet.assumedContains.getOrElse(x, SimpleIdentitySet.empty)
Expand Down
8 changes: 6 additions & 2 deletions compiler/src/dotty/tools/dotc/cc/CaptureSet.scala
Original file line number Diff line number Diff line change
Expand Up @@ -374,7 +374,7 @@ object CaptureSet:

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

def apply(elems: Refs)(using Context): CaptureSet.Const =
if elems.isEmpty then empty else Const(elems)
Expand Down Expand Up @@ -508,7 +508,11 @@ object CaptureSet:
!noUniversal
else elem match
case elem: TermRef if level.isDefined =>
elem.symbol.ccLevel <= level
elem.prefix match
case prefix: CaptureRef =>
levelOK(prefix)
case _ =>
elem.symbol.ccLevel <= level
case elem: ThisType if level.isDefined =>
elem.cls.ccLevel.nextInner <= level
case ReachCapability(elem1) =>
Expand Down
149 changes: 90 additions & 59 deletions compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
Original file line number Diff line number Diff line change
Expand Up @@ -13,7 +13,7 @@ import Trees.*
import typer.RefChecks.{checkAllOverrides, checkSelfAgainstParents, OverridingPairsChecker}
import typer.Checking.{checkBounds, checkAppliedTypesIn}
import typer.ErrorReporting.{Addenda, NothingToAdd, err}
import typer.ProtoTypes.{AnySelectionProto, LhsProto}
import typer.ProtoTypes.{LhsProto, WildcardSelectionProto}
import util.{SimpleIdentitySet, EqHashMap, EqHashSet, SrcPos, Property}
import transform.{Recheck, PreRecheck, CapturedVars}
import Recheck.*
Expand Down Expand Up @@ -122,10 +122,6 @@ object CheckCaptures:
* This check is performed at Typer.
*/
def checkWellformed(parent: Tree, ann: Tree)(using Context): Unit =
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Why was this check removed?

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

When implementing the path, I considered the rule for a singleton type with a capture set. I don't think this check is necessary, as we can already achieve the same result by creating a type alias with a capture set.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

So you are saying the rule is incomplete? But then maybe we should dealias before we check? What is the argument for removing it?

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

What I mean is it is okey to let users add a capture set to a singleton type, if they just want to explicitly indicate what the underlying type capturing (for example, in the member function signature def f: this.file^{this.io}).

parent.tpe match
case _: SingletonType =>
report.error(em"Singleton type $parent cannot have capture set", parent.srcPos)
case _ =>
def check(elem: Tree, pos: SrcPos): Unit = elem.tpe match
case ref: CaptureRef =>
if !ref.isTrackableRef then
Expand Down Expand Up @@ -187,6 +183,9 @@ object CheckCaptures:
/** Attachment key for bodies of closures, provided they are values */
val ClosureBodyValue = Property.Key[Unit]

/** A prototype that indicates selection with an immutable value */
class PathSelectionProto(val sym: Symbol, val pt: Type)(using Context) extends WildcardSelectionProto

class CheckCaptures extends Recheck, SymTransformer:
thisPhase =>

Expand Down Expand Up @@ -361,57 +360,67 @@ class CheckCaptures extends Recheck, SymTransformer:
* the environment in which `sym` is defined.
*/
def markFree(sym: Symbol, pos: SrcPos)(using Context): Unit =
if sym.exists then
val ref = sym.termRef
if ref.isTracked then
forallOuterEnvsUpTo(sym.enclosure): env =>
capt.println(i"Mark $sym with cs ${ref.captureSet} free in ${env.owner}")
checkElem(ref, env.captured, pos, provenance(env))
markFree(sym, sym.termRef, pos)

def markFree(sym: Symbol, ref: TermRef, pos: SrcPos)(using Context): Unit =
if sym.exists && ref.isTracked then
forallOuterEnvsUpTo(sym.enclosure): env =>
capt.println(i"Mark $sym with cs ${ref.captureSet} free in ${env.owner}")
checkElem(ref, env.captured, pos, provenance(env))

/** Make sure (projected) `cs` is a subset of the capture sets of all enclosing
* environments. At each stage, only include references from `cs` that are outside
* the environment's owner
*/
def markFree(cs: CaptureSet, pos: SrcPos)(using Context): Unit =
// A captured reference with the symbol `sym` is visible from the environment
// if `sym` is not defined inside the owner of the environment.
inline def isVisibleFromEnv(sym: Symbol, env: Env) =
if env.kind == EnvKind.NestedInOwner then
!sym.isProperlyContainedIn(env.owner)
else
!sym.isContainedIn(env.owner)

def checkSubsetEnv(cs: CaptureSet, env: Env)(using Context): Unit =
// 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
case ref: ThisType => isVisibleFromEnv(ref.cls, env)
case _ => false
checkSubset(included, env.captured, pos, provenance(env))
capt.println(i"Include call or box capture $included from $cs in ${env.owner} --> ${env.captured}")

if !cs.isAlwaysEmpty then
forallOuterEnvsUpTo(ctx.owner.topLevelClass): env =>
// Whether a symbol is defined inside the owner of the environment?
inline def isContainedInEnv(sym: Symbol) =
if env.kind == EnvKind.NestedInOwner then
sym.isProperlyContainedIn(env.owner)
else
sym.isContainedIn(env.owner)
// A captured reference with the symbol `sym` is visible from the environment
// if `sym` is not defined inside the owner of the environment
inline def isVisibleFromEnv(sym: Symbol) = !isContainedInEnv(sym)
// 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)
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
case ref: ThisType => isVisibleFromEnv(ref.cls)
case _ => false
checkSubset(included, env.captured, pos, provenance(env))
capt.println(i"Include call or box capture $included from $cs in ${env.owner} --> ${env.captured}")
checkSubsetEnv(cs, env)
end markFree

/** Include references captured by the called method in the current environment stack */
Expand Down Expand Up @@ -457,11 +466,26 @@ class CheckCaptures extends Recheck, SymTransformer:
if tree.symbol.info.isParameterless then
// there won't be an apply; need to include call captures now
includeCallCaptures(tree.symbol, tree.srcPos)
else
else if !tree.symbol.isStatic then
//debugShowEnvs()
markFree(tree.symbol, tree.srcPos)
def addSelects(ref: TermRef, pt: Type): TermRef = pt match
case pt: PathSelectionProto if ref.isTracked =>
// if `ref` is not tracked then the selection could not give anything new
// class SerializationProxy in stdlib-cc/../LazyListIterable.scala has an example where this matters.
addSelects(ref.select(pt.sym).asInstanceOf[TermRef], pt.pt)
case _ => ref
val ref = tree.symbol.termRef
val pathRef = addSelects(ref, pt)
//if pathRef ne ref then
// println(i"add selects $ref --> $pathRef")
markFree(tree.symbol, if false then ref else pathRef, tree.srcPos)
super.recheckIdent(tree, pt)

override def selectionProto(tree: Select, pt: Type)(using Context): Type =
val sym = tree.symbol
if !sym.isOneOf(UnstableValueFlags) && !sym.isStatic then PathSelectionProto(sym, pt)
else super.selectionProto(tree, pt)

/** A specialized implementation of the selection rule.
*
* E |- f: T{ m: R^Cr }^{f}
Expand All @@ -488,21 +512,25 @@ class CheckCaptures extends Recheck, SymTransformer:
case _ => denot

val selType = recheckSelection(tree, qualType, name, disambiguate)
val selCs = selType.widen.captureSet
if selCs.isAlwaysEmpty
|| selType.widen.isBoxedCapturing
val selWiden = selType.widen

if pt == LhsProto
|| qualType.isBoxedCapturing
|| pt == LhsProto
|| selType.isTrackableRef
|| selWiden.isBoxedCapturing
|| selWiden.captureSet.isAlwaysEmpty
then
selType
else
val qualCs = qualType.captureSet
capt.println(i"pick one of $qualType, ${selType.widen}, $qualCs, $selCs in $tree")
val selCs = selType.captureSet
capt.println(i"pick one of $qualType, ${selType.widen}, $qualCs, $selCs ${selWiden.captureSet} in $tree")

if qualCs.mightSubcapture(selCs)
&& !selCs.mightSubcapture(qualCs)
&& !pt.stripCapturing.isInstanceOf[SingletonType]
then
selType.widen.stripCapturing.capturing(qualCs)
selWiden.stripCapturing.capturing(qualCs)
.showing(i"alternate type for select $tree: $selType --> $result, $qualCs / $selCs", capt)
else
selType
Expand Down Expand Up @@ -1121,11 +1149,14 @@ class CheckCaptures extends Recheck, SymTransformer:
(erefs /: erefs.elems): (erefs, eref) =>
eref match
case eref: ThisType if isPureContext(ctx.owner, eref.cls) =>
erefs ++ arefs.filter {
case aref: TermRef => eref.cls.isProperlyContainedIn(aref.symbol.owner)
def isOuterRef(aref: Type): Boolean = aref match
case aref: TermRef =>
val owner = aref.symbol.owner
if owner.isClass then isOuterRef(aref.prefix)
else eref.cls.isProperlyContainedIn(owner)
case aref: ThisType => eref.cls.isProperlyContainedIn(aref.cls)
case _ => false
}
erefs ++ arefs.filter(isOuterRef)
case _ =>
erefs

Expand Down
5 changes: 5 additions & 0 deletions compiler/src/dotty/tools/dotc/cc/Setup.scala
Original file line number Diff line number Diff line change
Expand Up @@ -518,6 +518,11 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI:
info match
case mt: MethodOrPoly =>
val psyms = psymss.head
// TODO: the substitution does not work for param-dependent method types.
// For example, `(x: T, y: x.f.type) => Unit`. In this case, when we
// substitute `x.f.type`, `x` becomes a `TermParamRef`. But the new method
// type is still under initialization and `paramInfos` is still `null`,
// so the new `NamedType` will not have a denoation.
mt.companion(mt.paramNames)(
mt1 =>
if !paramSignatureChanges && !mt.isParamDependent && prevLambdas.isEmpty then
Expand Down
26 changes: 13 additions & 13 deletions compiler/src/dotty/tools/dotc/parsing/Parsers.scala
Original file line number Diff line number Diff line change
Expand Up @@ -1548,21 +1548,21 @@ object Parsers {
case _ => None
}

/** CaptureRef ::= ident [`*` | `^`] | `this`
/** CaptureRef ::= SimpleRef { `.` id } [`*` | `^`]
*/
def captureRef(): Tree =
if in.token == THIS then simpleRef()
else
val id = termIdent()
if isIdent(nme.raw.STAR) then
in.nextToken()
atSpan(startOffset(id)):
PostfixOp(id, Ident(nme.CC_REACH))
else if isIdent(nme.UPARROW) then
in.nextToken()
atSpan(startOffset(id)):
makeCapsOf(cpy.Ident(id)(id.name.toTypeName))
else id
val ref = dotSelectors(simpleRef())
if isIdent(nme.raw.STAR) then
in.nextToken()
atSpan(startOffset(ref)):
PostfixOp(ref, Ident(nme.CC_REACH))
else if isIdent(nme.UPARROW) then
in.nextToken()
atSpan(startOffset(ref)):
convertToTypeId(ref) match
case ref: RefTree => makeCapsOf(ref)
case ref => ref
else ref

/** CaptureSet ::= `{` CaptureRef {`,` CaptureRef} `}` -- under captureChecking
*/
Expand Down
Loading
Loading