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

Refactorings around CaptureRef #20893

Closed
wants to merge 35 commits into from
Closed
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
35 commits
Select commit Hold shift + click to select a range
e77657f
More robust level handling
odersky Jun 5, 2024
8e23712
Add existential capabilities, 2nd draft
odersky Jun 5, 2024
16907ec
Generalize isAlwaysEmpty and streamline isBoxedCaptured
odersky Jun 6, 2024
0a60670
Refine class refinements
odersky Jun 7, 2024
df0c7b1
Improve handling of no-cap-under-box/unbox errors
odersky Jun 7, 2024
3ce1f31
Go back to original no cap in box/unbox restrictions
odersky Jun 7, 2024
37dc2d5
More robust scheme to re-check definitions once.
odersky Jun 10, 2024
61b6647
Show unsuccessful subCapture tests in TypeMismatch explanations
odersky Jun 10, 2024
f0ddb50
Enable existential capabilities
odersky Jun 10, 2024
c50e01c
Tighten rules against escaping local references
odersky Jun 13, 2024
03a3e41
Go back to expansion of capability class references at Setup
odersky Jun 13, 2024
ab63489
Drop expandedUniversalSet
odersky Jun 13, 2024
a8a92e1
Adapt new capability class scheme to existentials
odersky Jun 13, 2024
3b09cb3
Map capability classes to existentials
odersky Jun 13, 2024
5c527b6
Change encoding of impure dependent function types
odersky Jun 14, 2024
21bd994
Fix mapping of cap to existentials
odersky Jun 15, 2024
c870c97
Let only value types derive from Capabilities
odersky Jun 15, 2024
29d01c2
Type inference for existentials
odersky Jun 17, 2024
dddd6bc
Drop checkReachCapsIsolated restriction
odersky Jun 17, 2024
c547c2a
Drop no universal in deep capture set test everywhere from source 3.5
odersky Jun 17, 2024
5ade6a4
Disallow to box or unbox existentials
odersky Jun 17, 2024
516df7c
Fix existential mapping of non-dependent impure function aliases =>
odersky Jun 17, 2024
bca3978
Drop restrictions in widenReachCaptures
odersky Jun 17, 2024
87e34ed
Cleanup ccConfig settings
odersky Jun 18, 2024
ec1e66d
Don't add ^ to singleton capabilities during Setup
odersky Jun 18, 2024
de4e56f
Refine parameter accessors that have nonempty deep capture sets
odersky Jun 21, 2024
ea182f2
More precise capture set unions
odersky Jun 23, 2024
60b0486
First implementation of capture polymorphism
odersky Jun 26, 2024
38cf302
Reclassify maximal capabilities
odersky Jun 27, 2024
dd4a60a
Bring back RefiningVar
odersky Jun 27, 2024
185f177
Allow for embedded CapSet^{refs} entries in capture sets
odersky Jun 27, 2024
27126ae
Improve printing of capture sets before cc
odersky Jun 28, 2024
e8167e4
Add some neg tests
odersky Jun 28, 2024
4f1d91a
Refactor CaptureRef operations
odersky Jun 28, 2024
c971af4
Break out CaptureRef into a separate file
odersky Jun 28, 2024
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
11 changes: 8 additions & 3 deletions compiler/src/dotty/tools/dotc/ast/untpd.scala
Original file line number Diff line number Diff line change
Expand Up @@ -521,12 +521,17 @@ object untpd extends Trees.Instance[Untyped] with UntypedTreeInfo {
def captureRoot(using Context): Select =
Select(scalaDot(nme.caps), nme.CAPTURE_ROOT)

def captureRootIn(using Context): Select =
Select(scalaDot(nme.caps), nme.capIn)

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 makeCapsBound()(using Context): Tree =
makeRetaining(
Select(scalaDot(nme.caps), tpnme.CapSet),
Nil, tpnme.retainsCap)

def makeConstructor(tparams: List[TypeDef], vparamss: List[List[ValDef]], rhs: Tree = EmptyTree)(using Context): DefDef =
DefDef(nme.CONSTRUCTOR, joinParams(tparams, vparamss), TypeTree(), rhs)

Expand Down
252 changes: 201 additions & 51 deletions compiler/src/dotty/tools/dotc/cc/CaptureOps.scala
Original file line number Diff line number Diff line change
Expand Up @@ -14,6 +14,8 @@ import tpd.*
import StdNames.nme
import config.Feature
import collection.mutable
import CCState.*
import reporting.Message

private val Captures: Key[CaptureSet] = Key()

Expand All @@ -25,11 +27,19 @@ object ccConfig:
*/
inline val allowUnsoundMaps = false

/** If true, use `sealed` as encapsulation mechanism instead of the
* previous global retriction that `cap` can't be boxed or unboxed.
/** If true, use existential capture set variables */
def useExistentials(using Context) =
Feature.sourceVersion.stable.isAtLeast(SourceVersion.`3.5`)

/** If true, use "sealed" as encapsulation mechanism, meaning that we
* check that type variable instantiations don't have `cap` in any of
* their capture sets. This is an alternative of the original restriction
* that `cap` can't be boxed or unboxed. It is used in 3.3 and 3.4 but
* dropped again in 3.5.
*/
def allowUniversalInBoxed(using Context) =
Feature.sourceVersion.isAtLeast(SourceVersion.`3.3`)
def useSealed(using Context) =
Feature.sourceVersion.stable == SourceVersion.`3.3`
|| Feature.sourceVersion.stable == SourceVersion.`3.4`
end ccConfig


Expand All @@ -54,7 +64,7 @@ def depFun(args: List[Type], resultType: Type, isContextual: Boolean, paramNames
mt.toFunctionType(alwaysDependent = true)

/** An exception thrown if a @retains argument is not syntactically a CaptureRef */
class IllegalCaptureRef(tpe: Type) extends Exception(tpe.toString)
class IllegalCaptureRef(tpe: Type)(using Context) extends Exception(tpe.show)

/** Capture checking state, which is known to other capture checking components */
class CCState:
Expand All @@ -64,25 +74,74 @@ class CCState:
*/
var levelError: Option[CaptureSet.CompareResult.LevelError] = None

/** Warnings relating to upper approximations of capture sets with
* existentially bound variables.
*/
val approxWarnings: mutable.ListBuffer[Message] = mutable.ListBuffer()

private var curLevel: Level = outermostLevel
private val symLevel: mutable.Map[Symbol, Int] = mutable.Map()

object CCState:

opaque type Level = Int

val undefinedLevel: Level = -1

val outermostLevel: Level = 0

/** The level of the current environment. Levels start at 0 and increase for
* each nested function or class. -1 means the level is undefined.
*/
def currentLevel(using Context): Level = ccState.curLevel

inline def inNestedLevel[T](inline op: T)(using Context): T =
val ccs = ccState
val saved = ccs.curLevel
ccs.curLevel = ccs.curLevel.nextInner
try op finally ccs.curLevel = saved

inline def inNestedLevelUnless[T](inline p: Boolean)(inline op: T)(using Context): T =
val ccs = ccState
val saved = ccs.curLevel
if !p then ccs.curLevel = ccs.curLevel.nextInner
try op finally ccs.curLevel = saved

extension (x: Level)
def isDefined: Boolean = x >= 0
def <= (y: Level) = (x: Int) <= y
def nextInner: Level = if isDefined then x + 1 else x

extension (sym: Symbol)(using Context)
def ccLevel: Level = ccState.symLevel.getOrElse(sym, -1)
def recordLevel() = ccState.symLevel(sym) = currentLevel
end CCState

/** The currently valid CCState */
def ccState(using Context) =
Phases.checkCapturesPhase.asInstanceOf[CheckCaptures].ccState
Phases.checkCapturesPhase.asInstanceOf[CheckCaptures].ccState1

class NoCommonRoot(rs: Symbol*)(using Context) extends Exception(
i"No common capture root nested in ${rs.mkString(" and ")}"
)

extension (tree: Tree)

/** Map tree with CaptureRef type to its type, throw IllegalCaptureRef otherwise */
def toCaptureRef(using Context): CaptureRef = tree match
/** Map tree with CaptureRef type to its type,
* map CapSet^{refs} to the `refs` references,
* throw IllegalCaptureRef otherwise
*/
def toCaptureRefs(using Context): List[CaptureRef] = tree match
case ReachCapabilityApply(arg) =>
arg.toCaptureRef.reach
case _ => tree.tpe match
arg.toCaptureRefs.map(_.reach)
case CapsOfApply(arg) =>
arg.toCaptureRefs
case _ => tree.tpe.dealiasKeepAnnots match
case ref: CaptureRef if ref.isTrackableRef =>
ref
ref :: Nil
case AnnotatedType(parent, ann)
if ann.symbol.isRetains && parent.derivesFrom(defn.Caps_CapSet) =>
ann.tree.toCaptureSet.elems.toList
case tpe =>
throw IllegalCaptureRef(tpe) // if this was compiled from cc syntax, problem should have been reported at Typer

Expand All @@ -93,8 +152,8 @@ extension (tree: Tree)
tree.getAttachment(Captures) match
case Some(refs) => refs
case None =>
val refs = CaptureSet(tree.retainedElems.map(_.toCaptureRef)*)
.showing(i"toCaptureSet $tree --> $result", capt)
val refs = CaptureSet(tree.retainedElems.flatMap(_.toCaptureRefs)*)
//.showing(i"toCaptureSet $tree --> $result", capt)
tree.putAttachment(Captures, refs)
refs

Expand All @@ -109,6 +168,60 @@ extension (tree: Tree)

extension (tp: Type)

/** Is this type a CaptureRef that can be tracked?
* This is true for
* - all ThisTypes and all TermParamRef,
* - stable TermRefs with NoPrefix or ThisTypes as prefixes,
* - the root capability `caps.cap`
* - abstract or parameter TypeRefs that derive from caps.CapSet
* - annotated types that represent reach or maybe capabilities
*/
final def isTrackableRef(using Context): Boolean = tp match
case _: (ThisType | TermParamRef) =>
true
case tp: TermRef =>
((tp.prefix eq NoPrefix)
|| tp.symbol.is(ParamAccessor) && tp.prefix.isThisTypeOf(tp.symbol.owner)
|| tp.isRootCapability
) && !tp.symbol.isOneOf(UnstableValueFlags)
case tp: TypeRef =>
tp.symbol.isAbstractOrParamType && tp.derivesFrom(defn.Caps_CapSet)
case tp: TypeParamRef =>
tp.derivesFrom(defn.Caps_CapSet)
case AnnotatedType(parent, annot) =>
annot.symbol == defn.ReachCapabilityAnnot
|| annot.symbol == defn.MaybeCapabilityAnnot
case _ =>
false

/** The capture set of a type. This is:
* - For trackable capture references: The singleton capture set consisting of
* just the reference, provided the underlying capture set of their info is not empty.
* - For other capture references: The capture set of their info
* - For all other types: The result of CaptureSet.ofType
*/
final def captureSet(using Context): CaptureSet = tp match
case tp: CaptureRef if tp.isTrackableRef =>
val cs = tp.captureSetOfInfo
if cs.isAlwaysEmpty then cs else tp.singletonCaptureSet
case tp: SingletonCaptureRef => tp.captureSetOfInfo
case _ => CaptureSet.ofType(tp, followResult = false)

/** A type capturing `ref` */
def capturing(ref: CaptureRef)(using Context): Type =
if tp.captureSet.accountsFor(ref) then tp
else CapturingType(tp, ref.singletonCaptureSet)

/** A type capturing the capture set `cs`. If this type is already a capturing type
* the two capture sets are combined.
*/
def capturing(cs: CaptureSet)(using Context): Type =
if cs.isAlwaysEmpty || cs.isConst && cs.subCaptures(tp.captureSet, frozen = true).isOK
then tp
else tp match
case CapturingType(parent, cs1) => parent.capturing(cs1 ++ cs)
case _ => CapturingType(tp, cs)

/** @pre `tp` is a CapturingType */
def derivedCapturingType(parent: Type, refs: CaptureSet)(using Context): Type = tp match
case tp @ CapturingType(p, r) =>
Expand Down Expand Up @@ -158,7 +271,15 @@ extension (tp: Type)
getBoxed(tp)

/** Is the boxedCaptureSet of this type nonempty? */
def isBoxedCapturing(using Context) = !tp.boxedCaptureSet.isAlwaysEmpty
def isBoxedCapturing(using Context): Boolean =
tp match
case tp @ CapturingType(parent, refs) =>
tp.isBoxed && !refs.isAlwaysEmpty || parent.isBoxedCapturing
case tp: TypeRef if tp.symbol.isAbstractOrParamType => false
case tp: TypeProxy => tp.superType.isBoxedCapturing
case tp: AndType => tp.tp1.isBoxedCapturing && tp.tp2.isBoxedCapturing
case tp: OrType => tp.tp1.isBoxedCapturing || tp.tp2.isBoxedCapturing
case _ => false

/** If this type is a capturing type, the version with boxed statues as given by `boxed`.
* If it is a TermRef of a capturing type, and the box status flips, widen to a capturing
Expand Down Expand Up @@ -211,7 +332,7 @@ extension (tp: Type)
val sym = tp.typeSymbol
if sym.isClass then sym.derivesFrom(defn.Caps_Capability)
else tp.superType.derivesFromCapability
case tp: TypeProxy =>
case tp: (TypeProxy & ValueType) =>
tp.superType.derivesFromCapability
case tp: AndType =>
tp.tp1.derivesFromCapability || tp.tp2.derivesFromCapability
Expand Down Expand Up @@ -307,6 +428,7 @@ extension (tp: Type)
ok = false
case _ =>
traverseChildren(t)
end CheckContraCaps

object narrowCaps extends TypeMap:
/** Has the variance been flipped at this point? */
Expand All @@ -319,16 +441,25 @@ extension (tp: Type)
t.dealias match
case t1 @ CapturingType(p, cs) if cs.isUniversal && !isFlipped =>
t1.derivedCapturingType(apply(p), ref.reach.singletonCaptureSet)
case t1 @ FunctionOrMethod(args, res @ Existential(_, _))
if args.forall(_.isAlwaysPure) =>
// Also map existentials in results to reach capabilities if all
// preceding arguments are known to be always pure
apply(t1.derivedFunctionOrMethod(args, Existential.toCap(res)))
case Existential(_, _) =>
t
case _ => t match
case t @ CapturingType(p, cs) =>
t.derivedCapturingType(apply(p), cs) // don't map capture set variables
case t =>
mapOver(t)
finally isFlipped = saved
end narrowCaps

ref match
case ref: CaptureRef if ref.isTrackableRef =>
val checker = new CheckContraCaps
checker.traverse(tp)
if !ccConfig.useExistentials then checker.traverse(tp)
if checker.ok then
val tp1 = narrowCaps(tp)
if tp1 ne tp then capt.println(i"narrow $tp of $ref to $tp1")
Expand All @@ -339,6 +470,12 @@ extension (tp: Type)
case _ =>
tp

def level(using Context): Level =
tp match
case tp: TermRef => tp.symbol.ccLevel
case tp: ThisType => tp.cls.ccLevel.nextInner
case _ => undefinedLevel

extension (cls: ClassSymbol)

def pureBaseClass(using Context): Option[Symbol] =
Expand Down Expand Up @@ -414,43 +551,20 @@ extension (sym: Symbol)
&& !sym.allowsRootCapture
&& sym != defn.Caps_unsafeBox
&& sym != defn.Caps_unsafeUnbox
&& !defn.isPolymorphicAfterErasure(sym)

/** Does this symbol define a level where we do not want to let local variables
* escape into outer capture sets?
*/
def isLevelOwner(using Context): Boolean =
sym.isClass
|| sym.is(Method, butNot = Accessor)

/** 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.Capability, or they are the rhs of a val definition.
* - classes, if they are not staticOwners
* - _root_
*/
def levelOwner(using Context): Symbol =
def recur(sym: Symbol): Symbol =
if !sym.exists || sym.isRoot || sym.isStaticOwner then defn.RootClass
else if sym.isLevelOwner then sym
else recur(sym.owner)
recur(sym)

/** The outermost symbol owned by both `sym` and `other`. if none exists
* since the owning scopes of `sym` and `other` are not nested, invoke
* `onConflict` to return a symbol.
*/
def maxNested(other: Symbol, onConflict: (Symbol, Symbol) => Context ?=> Symbol)(using Context): Symbol =
if !sym.exists || other.isContainedIn(sym) then other
else if !other.exists || sym.isContainedIn(other) then sym
else onConflict(sym, other)
def isRefiningParamAccessor(using Context): Boolean =
sym.is(ParamAccessor)
&& {
val param = sym.owner.primaryConstructor.paramSymss
.nestedFind(_.name == sym.name)
.getOrElse(NoSymbol)
!param.hasAnnotation(defn.ConstructorOnlyAnnot)
&& !param.hasAnnotation(defn.UntrackedCapturesAnnot)
}

/** The innermost symbol owning both `sym` and `other`.
*/
def minNested(other: Symbol)(using Context): Symbol =
if !other.exists || other.isContainedIn(sym) then sym
else if !sym.exists || sym.isContainedIn(other) then other
else sym.owner.minNested(other.owner)
def hasTrackedParts(using Context): Boolean =
!CaptureSet.deepCaptureSet(sym.info).isAlwaysEmpty

extension (tp: AnnotatedType)
/** Is this a boxed capturing type? */
Expand All @@ -474,6 +588,14 @@ object ReachCapabilityApply:
case Apply(reach, arg :: Nil) if reach.symbol == defn.Caps_reachCapability => Some(arg)
case _ => None

/** An extractor for `caps.capsOf[X]`, which is used to express a generic capture set
* as a tree in a @retains annotation.
*/
object CapsOfApply:
def unapply(tree: TypeApply)(using Context): Option[Tree] = tree match
case TypeApply(capsOf, arg :: Nil) if capsOf.symbol == defn.Caps_capsOf => Some(arg)
case _ => None

class AnnotatedCapability(annot: Context ?=> ClassSymbol):
def apply(tp: Type)(using Context) =
AnnotatedType(tp, Annotation(annot, util.Spans.NoSpan))
Expand All @@ -491,7 +613,35 @@ object ReachCapability extends AnnotatedCapability(defn.ReachCapabilityAnnot)
*/
object MaybeCapability extends AnnotatedCapability(defn.MaybeCapabilityAnnot)

/** Offers utility method to be used for type maps that follow aliases */
trait ConservativeFollowAliasMap(using Context) extends TypeMap:

/** If `mapped` is a type alias, apply the map to the alias, while keeping
* annotations. If the result is different, return it, otherwise return `mapped`.
* Furthermore, if `original` is a LazyRef or TypeVar and the mapped result is
* the same as the underlying type, keep `original`. This avoids spurious differences
* which would lead to spurious dealiasing in the result
*/
protected def applyToAlias(original: Type, mapped: Type) =
val mapped1 = mapped match
case t: (TypeRef | AppliedType) =>
val t1 = t.dealiasKeepAnnots
if t1 eq t then t
else
// If we see a type alias, map the alias type and keep it if it's different
val t2 = apply(t1)
if t2 ne t1 then t2 else t
case _ =>
mapped
original match
case original: (LazyRef | TypeVar) if mapped1 eq original.underlying =>
original
case _ =>
mapped1
end ConservativeFollowAliasMap

/** An extractor for all kinds of function types as well as method and poly types.
* It includes aliases of function types such as `=>`. TODO: Can we do without?
* @return 1st half: The argument types or empty if this is a type function
* 2nd half: The result type
*/
Expand Down
Loading