-
Notifications
You must be signed in to change notification settings - Fork 1.1k
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
base: main
Are you sure you want to change the base?
Changes from all commits
74b6bf6
ddba608
440c053
45df152
263d6eb
152710b
c20ae8f
cb6605c
27929fe
File filter
Filter by extension
Conversations
Jump to
Diff view
Diff view
There are no files selected for viewing
Original file line number | Diff line number | Diff line change |
---|---|---|
|
@@ -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.* | ||
|
@@ -122,10 +122,6 @@ object CheckCaptures: | |
* This check is performed at Typer. | ||
*/ | ||
def checkWellformed(parent: Tree, ann: Tree)(using Context): Unit = | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Why was this check removed? There was a problem hiding this comment. Choose a reason for hiding this commentThe 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. There was a problem hiding this comment. Choose a reason for hiding this commentThe 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? There was a problem hiding this comment. Choose a reason for hiding this commentThe 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 |
||
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 | ||
|
@@ -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 => | ||
|
||
|
@@ -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 */ | ||
|
@@ -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} | ||
|
@@ -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 | ||
|
@@ -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 | ||
|
||
|
There was a problem hiding this comment.
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: