Skip to content

Use level checking for Fresh instances #23101

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

Merged
merged 19 commits into from
May 13, 2025
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
19 commits
Select commit Hold shift + click to select a range
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
18 changes: 18 additions & 0 deletions compiler/src/dotty/tools/dotc/cc/CCState.scala
Original file line number Diff line number Diff line change
Expand Up @@ -118,6 +118,8 @@ class CCState:

private var capIsRoot: Boolean = false

private var ignoreFreshLevels: Boolean = false

object CCState:

opaque type Level = Int
Expand Down Expand Up @@ -162,4 +164,20 @@ object CCState:
/** Is `caps.cap` a root capability that is allowed to subsume other capabilities? */
def capIsRoot(using Context): Boolean = ccState.capIsRoot

/** Run `op` under the assumption that all root.Fresh instances are equal.
* Needed to make override checking of types containing fresh work.
* Asserted in override checking, tested in maxSubsumes.
* Is this sound? Test case is neg-custom-args/captures/leaked-curried.scala.
*/
inline def ignoringFreshLevels[T](op: => T)(using Context): T =
if isCaptureCheckingOrSetup then
val ccs = ccState
val saved = ccs.ignoreFreshLevels
ccs.ignoreFreshLevels = true
try op finally ccs.ignoreFreshLevels = saved
else op

/** Should all root.Fresh instances be treated equal? */
def ignoreFreshLevels(using Context): Boolean = ccState.ignoreFreshLevels

end CCState
23 changes: 17 additions & 6 deletions compiler/src/dotty/tools/dotc/cc/CaptureOps.scala
Original file line number Diff line number Diff line change
Expand Up @@ -4,20 +4,18 @@ package cc

import core.*
import Types.*, Symbols.*, Contexts.*, Annotations.*, Flags.*
import Names.TermName
import Names.{Name, TermName}
import ast.{tpd, untpd}
import Decorators.*, NameOps.*
import config.Printers.capt
import util.Property.Key
import tpd.*
import Annotations.Annotation
import CaptureSet.VarState

/** Attachment key for capturing type trees */
private val Captures: Key[CaptureSet] = Key()

/** Context property to print root.Fresh(...) as "fresh" instead of "cap" */
val PrintFresh: Key[Unit] = Key()

/** Are we at checkCaptures phase? */
def isCaptureChecking(using Context): Boolean =
ctx.phaseId == Phases.checkCapturesPhase.id
Expand Down Expand Up @@ -465,7 +463,9 @@ extension (tp: Type)
if args.forall(_.isAlwaysPure) then
// Also map existentials in results to reach capabilities if all
// preceding arguments are known to be always pure
t.derivedFunctionOrMethod(args, apply(root.resultToFresh(res)))
t.derivedFunctionOrMethod(
args,
apply(root.resultToFresh(res, root.Origin.ResultInstance(t, NoSymbol))))
else
t
case _ =>
Expand Down Expand Up @@ -505,6 +505,10 @@ extension (tp: Type)
case tp: ThisType => ccState.symLevel(tp.cls).nextInner
case _ => CCState.undefinedLevel

def refinedOverride(name: Name, rinfo: Type)(using Context): Type =
RefinedType(tp, name,
AnnotatedType(rinfo, Annotation(defn.RefineOverrideAnnot, util.Spans.NoSpan)))

extension (tp: MethodType)
/** A method marks an existential scope unless it is the prefix of a curried method */
def marksExistentialScope(using Context): Boolean =
Expand Down Expand Up @@ -694,6 +698,12 @@ abstract class AnnotatedCapability(annotCls: Context ?=> ClassSymbol):
protected def unwrappable(using Context): Set[Symbol]
end AnnotatedCapability

object QualifiedCapability:
def unapply(tree: AnnotatedType)(using Context): Option[CaptureRef] = tree match
case AnnotatedType(parent: CaptureRef, ann)
if defn.capabilityQualifierAnnots.contains(ann.symbol) => Some(parent)
case _ => None

/** An extractor for `ref @maybeCapability`, which is used to express
* the maybe capability `ref?` as a type.
*/
Expand Down Expand Up @@ -792,7 +802,8 @@ abstract class DeepTypeAccumulator[T](using Context) extends TypeAccumulator[T]:
case AnnotatedType(parent, _) =>
this(acc, parent)
case t @ FunctionOrMethod(args, res) =>
if args.forall(_.isAlwaysPure) then this(acc, root.resultToFresh(res))
if args.forall(_.isAlwaysPure) then
this(acc, root.resultToFresh(res, root.Origin.ResultInstance(t, NoSymbol)))
else acc
case _ =>
foldOver(acc, t)
Expand Down
56 changes: 52 additions & 4 deletions compiler/src/dotty/tools/dotc/cc/CaptureRef.scala
Original file line number Diff line number Diff line change
Expand Up @@ -14,7 +14,9 @@ import compiletime.uninitialized
import StdNames.nme
import CaptureSet.VarState
import Annotations.Annotation
import Flags.*
import config.Printers.capt
import CCState.{Level, undefinedLevel}

object CaptureRef:
opaque type Validity = Int
Expand Down Expand Up @@ -106,6 +108,10 @@ trait CaptureRef extends TypeProxy, ValueType:
case root.Fresh(_) => true
case _ => false

final def isResultRoot(using Context): Boolean = this match
case root.Result(_) => true
case _ => false

/** Is this reference the generic root capability `cap` or a Fresh instance? */
final def isCapOrFresh(using Context): Boolean = isCap || isFresh

Expand All @@ -122,6 +128,41 @@ trait CaptureRef extends TypeProxy, ValueType:
final def isExclusive(using Context): Boolean =
!isReadOnly && (isRootCapability || captureSetOfInfo.isExclusive)

/** The owning symbol associated with a capability this is
* - for Fresh capabilities: the owner of the hidden set
* - for TermRefs and TypeRefs: the symbol it refers to
* - for derived and path capabilities: the owner of the underlying capability
* - otherwise NoSymbol
*/
final def ccOwner(using Context): Symbol = this match
case root.Fresh(hidden) =>
hidden.owner
case ref: NamedType =>
if ref.isCap then NoSymbol
else ref.prefix match
case prefix: CaptureRef => prefix.ccOwner
case _ => ref.symbol
case ref: ThisType =>
ref.cls
case QualifiedCapability(ref1) =>
ref1.ccOwner
case _ =>
NoSymbol

/** The symbol that represents the level closest-enclosing ccOwner.
* Symbols representing levels are
* - class symbols, but not inner (non-static) module classes
* - method symbols, but not accessors or constructors
*/
final def levelOwner(using Context): Symbol =
def adjust(owner: Symbol): Symbol =
if !owner.exists
|| owner.isClass && (!owner.is(Flags.Module) || owner.isStatic)
|| owner.is(Flags.Method, butNot = Flags.Accessor) && !owner.isConstructor
then owner
else adjust(owner.owner)
adjust(ccOwner)

// With the support of paths, 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
Expand Down Expand Up @@ -263,11 +304,18 @@ trait CaptureRef extends TypeProxy, ValueType:
case _ => false
(this eq y)
|| this.match
case root.Fresh(hidden) =>
vs.ifNotSeen(this)(hidden.elems.exists(_.subsumes(y)))
|| !y.stripReadOnly.isCap
case x @ root.Fresh(hidden) =>
def levelOK =
if ccConfig.useFreshLevels && !CCState.ignoreFreshLevels then
val yOwner = y.levelOwner
yOwner.isStaticOwner || x.ccOwner.isContainedIn(yOwner)
else
!y.stripReadOnly.isCap
&& !yIsExistential
&& !y.isInstanceOf[TermParamRef]
&& !y.isInstanceOf[ParamRef]

vs.ifNotSeen(this)(hidden.elems.exists(_.subsumes(y)))
|| levelOK
&& canAddHidden
&& vs.addHidden(hidden, y)
case x @ root.Result(binder) =>
Expand Down
Loading
Loading