Skip to content

Commit

Permalink
Add path support for cc
Browse files Browse the repository at this point in the history
  • Loading branch information
noti0na1 committed Sep 18, 2024
1 parent 65a53b5 commit 9015611
Show file tree
Hide file tree
Showing 18 changed files with 314 additions and 120 deletions.
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: Tree)(using Context): Tree =
TypeApply(Select(scalaDot(nme.caps), nme.capsOf), tp :: Nil)

def makeCapsBound()(using Context): Tree =
makeRetaining(
Expand Down
3 changes: 2 additions & 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,8 @@ 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.isThisTypeOf(tp.symbol.owner) || tp.prefix.isTrackableRef)
|| tp.isRootCapability
) && !tp.symbol.isOneOf(UnstableValueFlags)
case tp: TypeRef =>
Expand Down
84 changes: 58 additions & 26 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 @@ -99,25 +100,56 @@ trait CaptureRef extends TypeProxy, ValueType:
* x: x1.type /\ x1 subsumes y ==> x subsumes y
*/
final def subsumes(y: CaptureRef)(using Context): Boolean =
(this eq y)
|| this.isRootCapability
|| y.match
case y: TermRef =>
(y.prefix eq this)
|| y.info.match
case y1: SingletonCaptureRef => this.subsumes(y1)
case _ => false
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)
def compareCaptureRefs(x: Type, y: Type): Boolean =
(x eq y)
|| y.match
case y: CaptureRef => x.match
case x: CaptureRef => x.subsumes(y)
case _ => false
case x: TermParamRef => subsumesExistentially(x, y)
case x: TypeRef => assumedContainsOf(x).contains(y)
case _ => false
case _ => false

def compareUndelying(x: Type): Boolean = x match
case x: SingletonCaptureRef => x.subsumes(y)
case x: AndType => compareUndelying(x.tp1) || compareUndelying(x.tp2)
case x: OrType => compareUndelying(x.tp1) && compareUndelying(x.tp2)
case _ => false

if (this eq y) || this.isRootCapability then return true

// similar to compareNamed in TypeComparer
y match
case y: TermRef =>
this match
case x: TermRef =>
val xSym = x.symbol
val ySym = y.symbol

// check x.f and y.f
if (xSym ne NoSymbol)
&& (xSym eq ySym)
&& compareCaptureRefs(x.prefix, y.prefix)
|| (x.name eq y.name)
&& x.isPrefixDependentMemberRef
&& compareCaptureRefs(x.prefix, y.prefix)
&& x.signature == y.signature
&& !(xSym.isClass && ySym.isClass)
then return true
case _ =>

// shorten
if compareCaptureRefs(this, y.prefix) then return true
// underlying
if compareCaptureRefs(this, y.info) then return true
case MaybeCapability(y1) => return this.stripMaybe.subsumes(y1)
case _ =>

return this.match
case ReachCapability(x1) => x1.subsumes(y.stripReach)
case x: TermRef => compareUndelying(x.info)
case CapturingType(x1, _) => compareUndelying(x1)
case x: TermParamRef => subsumesExistentially(x, y)
case x: TypeRef => assumedContainsOf(x).contains(y)
case _ => false

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
106 changes: 59 additions & 47 deletions compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
Original file line number Diff line number Diff line change
Expand Up @@ -122,10 +122,6 @@ object CheckCaptures:
* This check is performed at Typer.
*/
def checkWellformed(parent: Tree, ann: Tree)(using Context): Unit =
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 @@ -373,45 +369,54 @@ class CheckCaptures extends Recheck, SymTransformer:
* 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 @@ -488,21 +493,28 @@ 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
def isStableSel = selType match
case selType: NamedType => selType.symbol.isStableMember
case _ => false

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
28 changes: 15 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,23 @@ object Parsers {
case _ => None
}

/** CaptureRef ::= ident [`*` | `^`] | `this`
/** CaptureRef ::= (ident | `this`) [`*` | `^`]
*/
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 = singleton()
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()
def toTypeSel(r: Tree): Tree = r match
case id: Ident => cpy.Ident(id)(id.name.toTypeName)
case Select(qual, id) => Select(qual, id.toTypeName)
case _ => r
atSpan(startOffset(ref)):
makeCapsOf(toTypeSel(ref))
else ref

/** CaptureSet ::= `{` CaptureRef {`,` CaptureRef} `}` -- under captureChecking
*/
Expand Down
13 changes: 5 additions & 8 deletions tests/neg-custom-args/captures/class-contra.check
Original file line number Diff line number Diff line change
@@ -1,10 +1,7 @@
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/class-contra.scala:12:39 ---------------------------------
12 | def fun(x: K{val f: T^{a}}) = x.setf(a) // error
| ^
| Found: (a : T^{x, y})
| Required: T^{}
|
| Note that a capability (K.this.f : T^) in a capture set appearing in contravariant position
| was mapped to (x.f : T^{a}) which is not a capability. Therefore, it was under-approximated to the empty set.
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/class-contra.scala:12:40 ---------------------------------
12 | def fun1(k: K{val f: T^{a}}) = k.setf(a) // error
| ^
| Found: (a : T^{x, y})
| Required: T^{k.f}
|
| longer explanation available when compiling with `-explain`
3 changes: 2 additions & 1 deletion tests/neg-custom-args/captures/class-contra.scala
Original file line number Diff line number Diff line change
Expand Up @@ -9,5 +9,6 @@ class T

def test(x: Cap, y: Cap) =
val a: T^{x, y} = ???
def fun(x: K{val f: T^{a}}) = x.setf(a) // error
def fun1(k: K{val f: T^{a}}) = k.setf(a) // error
def fun2(k: K{val f: a.type}) = k.setf(a)
()
14 changes: 4 additions & 10 deletions tests/neg-custom-args/captures/explain-under-approx.check
Original file line number Diff line number Diff line change
@@ -1,20 +1,14 @@
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/explain-under-approx.scala:12:10 -------------------------
12 | col.add(Future(() => 25)) // error
| ^^^^^^^^^^^^^^^^
| Found: Future[Int]{val a: (async : Async^)}^{async}
| Required: Future[Int]^{}
|
| Note that a capability Collector.this.futs* in a capture set appearing in contravariant position
| was mapped to col.futs* which is not a capability. Therefore, it was under-approximated to the empty set.
| Found: Future[Int]{val a: (async : Async^)}^{async}
| Required: Future[Int]^{col.futs*}
|
| longer explanation available when compiling with `-explain`
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/explain-under-approx.scala:15:11 -------------------------
15 | col1.add(Future(() => 25)) // error
| ^^^^^^^^^^^^^^^^
| Found: Future[Int]{val a: (async : Async^)}^{async}
| Required: Future[Int]^{}
|
| Note that a capability Collector.this.futs* in a capture set appearing in contravariant position
| was mapped to col1.futs* which is not a capability. Therefore, it was under-approximated to the empty set.
| Found: Future[Int]{val a: (async : Async^)}^{async}
| Required: Future[Int]^{col1.futs*}
|
| longer explanation available when compiling with `-explain`
Loading

0 comments on commit 9015611

Please sign in to comment.