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.

Sign up for GitHub

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

Test timeout #22559

Closed
wants to merge 5 commits into from
Closed

Test timeout #22559

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
5 commits
Select commit Hold shift + click to select a range
d843f70
Test timeout
odersky Feb 8, 2025
fd1f3e7
Revert "Address review comments"
odersky Feb 8, 2025
2bfafe5
Revert "Polish and document separation checker (2)"
odersky Feb 8, 2025
edfe896
Revert "Polishings"
odersky Feb 8, 2025
e803dbb
Handle paths extending SharableCapablity
odersky Feb 9, 2025
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
36 changes: 6 additions & 30 deletions compiler/src/dotty/tools/dotc/cc/CaptureOps.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -232,9 +232,7 @@ extension (tp: Type)
case tp @ ReachCapability(_) =>
tp.singletonCaptureSet
case ReadOnlyCapability(ref) =>
val refDcs = ref.deepCaptureSet(includeTypevars)
if refDcs.isConst then CaptureSet(refDcs.elems.map(_.readOnly))
else refDcs // this case should not happen for correct programs
ref.deepCaptureSet(includeTypevars)
case tp: SingletonCaptureRef if tp.isTrackableRef =>
tp.reach.singletonCaptureSet
case _ =>
Expand Down Expand Up @@ -281,24 +279,12 @@ extension (tp: Type)
case _ =>
tp

/** The first element of this path type. Note that class parameter references
* are of the form this.C but their pathroot is still this.C, not this.
*/
/** The first element of this path type */
final def pathRoot(using Context): Type = tp.dealias match
case tp1: TermRef if tp1.symbol.maybeOwner.isClass => tp1.prefix.pathRoot
case tp1: TypeRef if !tp1.symbol.is(Param) => tp1.prefix.pathRoot
case tp1: NamedType if tp1.symbol.maybeOwner.isClass && !tp1.symbol.is(TypeParam) =>
tp1.prefix.pathRoot
case tp1 => tp1

/** The first element of a path type, but stop at references extending
* SharedCapability.
*/
final def pathRootOrShared(using Context): Type =
if tp.derivesFromSharedCapability then tp
else tp.dealias match
case tp1: TermRef if tp1.symbol.maybeOwner.isClass => tp1.prefix.pathRoot
case tp1: TypeRef if !tp1.symbol.is(Param) => tp1.prefix.pathRoot
case tp1 => tp1

/** If this part starts with `C.this`, the class `C`.
* Otherwise, if it starts with a reference `r`, `r`'s owner.
* Otherwise NoSymbol.
Expand Down Expand Up @@ -431,7 +417,6 @@ extension (tp: Type)

def derivesFromCapability(using Context): Boolean = derivesFromCapTrait(defn.Caps_Capability)
def derivesFromMutable(using Context): Boolean = derivesFromCapTrait(defn.Caps_Mutable)
def derivesFromSharedCapability(using Context): Boolean = derivesFromCapTrait(defn.Caps_SharedCapability)

/** Drop @retains annotations everywhere */
def dropAllRetains(using Context): Type = // TODO we should drop retains from inferred types before unpickling
Expand Down Expand Up @@ -471,11 +456,6 @@ extension (tp: Type)
* is the union of all capture sets that appear in covariant position in the
* type of `x`. If `x` and `y` are different variables then `{x*}` and `{y*}`
* are unrelated.
*
* Reach capabilities cannot wrap read-only capabilities or maybe capabilities.
* We have
* (x.rd).reach = x*.rd
* (x.rd)? = (x*)?
*/
def reach(using Context): CaptureRef = tp match
case tp @ AnnotatedType(tp1: CaptureRef, annot)
Expand All @@ -493,10 +473,6 @@ extension (tp: Type)
/** If `x` is a capture ref, its read-only capability `x.rd`, represented internally
* as `x @readOnlyCapability`. We have {x.rd} <: {x}. If `x` is a reach capability `y*`,
* then its read-only version is `x.rd*`.
*
* Read-only capabilities cannot wrap maybe capabilities
* but they can wrap reach capabilities. We have
* (x?).readOnly = (x.rd)?
*/
def readOnly(using Context): CaptureRef = tp match
case tp @ AnnotatedType(tp1: CaptureRef, annot)
Expand All @@ -508,7 +484,7 @@ extension (tp: Type)
case _ =>
ReadOnlyCapability(tp)

/** If `x` is a capture ref, replace all no-flip covariant occurrences of `cap`
/** If `x` is a capture ref, replacxe all no-flip covariant occurrences of `cap`
* in type `tp` with `x*`.
*/
def withReachCaptures(ref: Type)(using Context): Type =
Expand Down Expand Up @@ -758,7 +734,7 @@ object MaybeCapability extends AnnotatedCapability(defn.MaybeCapabilityAnnot):
protected def unwrappable(using Context) = Set()

/** An extractor for `ref @readOnlyCapability`, which is used to express
* the read-only capability `ref.rd` as a type.
* the rad-only capability `ref.rd` as a type.
*/
object ReadOnlyCapability extends AnnotatedCapability(defn.ReadOnlyCapabilityAnnot):
protected def unwrappable(using Context) = Set(defn.MaybeCapabilityAnnot)
Expand Down
18 changes: 7 additions & 11 deletions compiler/src/dotty/tools/dotc/cc/CaptureRef.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -100,29 +100,23 @@ trait CaptureRef extends TypeProxy, ValueType:
/** Is this reference the generic root capability `cap` or a Fresh.Cap instance? */
final def isCapOrFresh(using Context): Boolean = isCap || isFresh

/** Is this reference one of the generic root capabilities `cap` or `cap.rd` ? */
/** Is this reference one the generic root capabilities `cap` or `cap.rd` ? */
final def isRootCapability(using Context): Boolean = this match
case ReadOnlyCapability(tp1) => tp1.isCapOrFresh
case _ => isCapOrFresh

/** Is this reference a capability that does not derive from another capability?
* Includes read-only versions of maximal capabilities.
*/
/** Is this reference capability that does not derive from another capability ? */
final def isMaxCapability(using Context): Boolean = this match
case tp: TermRef => tp.isCap || tp.info.derivesFrom(defn.Caps_Exists)
case tp: TermParamRef => tp.underlying.derivesFrom(defn.Caps_Exists)
case Fresh.Cap(_) => true
case ReadOnlyCapability(tp1) => tp1.isMaxCapability
case _ => false

/** An exclusive capability is a capability that derives
* indirectly from a maximal capability without going through
* a read-only capability first.
*/
final def isExclusive(using Context): Boolean =
!isReadOnly && (isMaxCapability || captureSetOfInfo.isExclusive)

// With the support of paths, we don't need to normalize the `TermRef`s anymore.
// 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 =>
Expand Down Expand Up @@ -165,6 +159,8 @@ trait CaptureRef extends TypeProxy, ValueType:
* X: CapSet^c1...CapSet^c2, (CapSet^c1) subsumes y ==> X subsumes y
* Y: CapSet^c1...CapSet^c2, x subsumes (CapSet^c2) ==> x subsumes Y
* Contains[X, y] ==> X subsumes y
*
* TODO: Move to CaptureSet
*/
final def subsumes(y: CaptureRef)(using ctx: Context, vs: VarState = VarState.Separate): Boolean =

Expand Down Expand Up @@ -242,8 +238,8 @@ trait CaptureRef extends TypeProxy, ValueType:
case _ => false
end subsumes

/** This is a maximal capability that subsumes `y` in given context and VarState.
* @param canAddHidden If true we allow maximal capabilities to subsume all other capabilities.
/** This is a maximal capabaility that subsumes `y` in given context and VarState.
* @param canAddHidden If true we allow maximal capabilties to subsume all other capabilities.
* We add those capabilities to the hidden set if this is Fresh.Cap
* If false we only accept `y` elements that are already in the
* hidden set of this Fresh.Cap. The idea is that in a VarState that
Expand Down
28 changes: 15 additions & 13 deletions compiler/src/dotty/tools/dotc/cc/CaptureSet.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -227,7 +227,11 @@ sealed abstract class CaptureSet extends Showable:
elems.forall(that.mightAccountFor)
&& !that.elems.forall(this.mightAccountFor)

/** The subcapturing test, taking an explicit VarState. */
/** The subcapturing test.
* @param frozen if true, no new variables or dependent sets are allowed to
* be added when making this test. An attempt to add either
* will result in failure.
*/
final def subCaptures(that: CaptureSet, vs: VarState)(using Context): CompareResult =
subCaptures(that)(using ctx, vs)

Expand Down Expand Up @@ -388,7 +392,7 @@ sealed abstract class CaptureSet extends Showable:
override def toText(printer: Printer): Text =
printer.toTextCaptureSet(this) ~~ description

/** Apply function `f` to the elements. Typically used for printing.
/** Apply function `f` to the elements. Typcially used for printing.
* Overridden in HiddenSet so that we don't run into infinite recursions
*/
def processElems[T](f: Refs => T): T = f(elems)
Expand All @@ -403,10 +407,10 @@ object CaptureSet:
/** If set to `true`, capture stack traces that tell us where sets are created */
private final val debugSets = false

val emptyRefs: Refs = SimpleIdentitySet.empty
val emptySet = SimpleIdentitySet.empty

/** The empty capture set `{}` */
val empty: CaptureSet.Const = Const(emptyRefs)
val empty: CaptureSet.Const = Const(emptySet)

/** The universal capture set `{cap}` */
def universal(using Context): CaptureSet =
Expand Down Expand Up @@ -462,7 +466,7 @@ object CaptureSet:
* nulls, this provides more lenient checking against compilation units that
* were not yet compiled with capture checking on.
*/
object Fluid extends Const(emptyRefs):
object Fluid extends Const(emptySet):
override def isAlwaysEmpty = false
override def addThisElem(elem: CaptureRef)(using Context, VarState) = CompareResult.OK
override def accountsFor(x: CaptureRef)(using Context, VarState): Boolean = true
Expand All @@ -471,7 +475,7 @@ object CaptureSet:
end Fluid

/** The subclass of captureset variables with given initial elements */
class Var(override val owner: Symbol = NoSymbol, initialElems: Refs = emptyRefs, val level: Level = undefinedLevel, underBox: Boolean = false)(using @constructorOnly ictx: Context) extends CaptureSet:
class Var(override val owner: Symbol = NoSymbol, initialElems: Refs = emptySet, val level: Level = undefinedLevel, underBox: Boolean = false)(using @constructorOnly ictx: Context) extends CaptureSet:

/** A unique identification number for diagnostics */
val id =
Expand All @@ -489,7 +493,7 @@ object CaptureSet:
/** The sets currently known to be dependent sets (i.e. new additions to this set
* are propagated to these dependent sets.)
*/
var deps: Deps = SimpleIdentitySet.empty
var deps: Deps = emptySet

def isConst = isSolved
def isAlwaysEmpty = isSolved && elems.isEmpty
Expand Down Expand Up @@ -632,8 +636,7 @@ object CaptureSet:
*/
def solve()(using Context): Unit =
if !isConst then
val approx = upperApprox(empty)
.map(Fresh.FromCap(NoSymbol).inverse) // Fresh.Cap --> cap
val approx = upperApprox(empty).map(Fresh.FromCap(NoSymbol).inverse)
.showing(i"solve $this = $result", capt)
//println(i"solving var $this $approx ${approx.isConst} deps = ${deps.toList}")
val newElems = approx.elems -- elems
Expand Down Expand Up @@ -923,16 +926,16 @@ object CaptureSet:
cs1.elems.filter(cs2.mightAccountFor) ++ cs2.elems.filter(cs1.mightAccountFor)

/** A capture set variable used to record the references hidden by a Fresh.Cap instance */
class HiddenSet(initialHidden: Refs = emptyRefs)(using @constructorOnly ictx: Context)
class HiddenSet(initialHidden: Refs = emptySet)(using @constructorOnly ictx: Context)
extends Var(initialElems = initialHidden):

/** Apply function `f` to `elems` while setting `elems` to empty for the
* duration. This is used to escape infinite recursions if two Fresh.Caps
* duration. This is used to escape infinite recursions if two Frash.Caps
* refer to each other in their hidden sets.
*/
override def processElems[T](f: Refs => T): T =
val savedElems = elems
elems = emptyRefs
elems = emptySet
try f(savedElems)
finally elems = savedElems
end HiddenSet
Expand Down Expand Up @@ -1136,7 +1139,6 @@ object CaptureSet:

/** A template for maps on capabilities where f(c) <: c and f(f(c)) = c */
private abstract class NarrowingCapabilityMap(using Context) extends BiTypeMap:

def mapRef(ref: CaptureRef): CaptureRef

def apply(t: Type) = t match
Expand Down
Loading
Loading