Skip to content

Commit

Permalink
Refine FrozenState categorizations
Browse files Browse the repository at this point in the history
 - In ++, use a FrozenSepState in order not to pollute hidden sets
 - This avoids two spurious separation failures in stdlib
  • Loading branch information
odersky committed Dec 21, 2024
1 parent 0a73a26 commit 76178ed
Show file tree
Hide file tree
Showing 8 changed files with 58 additions and 40 deletions.
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 @@ -16,6 +16,7 @@ import config.Feature
import collection.mutable
import CCState.*
import reporting.Message
import CaptureSet.Frozen

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

Expand Down Expand Up @@ -244,7 +245,7 @@ extension (tp: 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)
if (cs.isAlwaysEmpty || cs.isConst && cs.subCaptures(tp.captureSet, Frozen.All).isOK)
&& !cs.keepAlways
then tp
else tp match
Expand Down
4 changes: 2 additions & 2 deletions compiler/src/dotty/tools/dotc/cc/CaptureRef.scala
Original file line number Diff line number Diff line change
Expand Up @@ -134,7 +134,7 @@ trait CaptureRef extends TypeProxy, ValueType:
final def invalidateCaches() =
myCaptureSetRunId = NoRunId

import CaptureSet.{VarState, FrozenSepState}
import CaptureSet.{VarState, FrozenAllState}

/** x subsumes x
* x =:= y ==> x subsumes y
Expand All @@ -150,7 +150,7 @@ trait CaptureRef extends TypeProxy, ValueType:
*
* TODO: Move to CaptureSet
*/
final def subsumes(y: CaptureRef)(using ctx: Context, vs: VarState = FrozenSepState): Boolean =
final def subsumes(y: CaptureRef)(using ctx: Context, vs: VarState = FrozenAllState): Boolean =

def subsumingRefs(x: Type, y: Type): Boolean = x match
case x: CaptureRef => y match
Expand Down
62 changes: 38 additions & 24 deletions compiler/src/dotty/tools/dotc/cc/CaptureSet.scala
Original file line number Diff line number Diff line change
Expand Up @@ -142,7 +142,7 @@ sealed abstract class CaptureSet extends Showable:
* capture set.
*/
protected final def addNewElem(elem: CaptureRef)(using Context, VarState): CompareResult =
if elem.isMaxCapability || summon[VarState].isInstanceOf[FrozenState] then
if elem.isMaxCapability || summon[VarState].isInstanceOf[FrozenVarState] then
addThisElem(elem)
else
addThisElem(elem).orElse:
Expand Down Expand Up @@ -173,7 +173,7 @@ sealed abstract class CaptureSet extends Showable:
/** {x} <:< this where <:< is subcapturing, but treating all variables
* as frozen.
*/
def accountsFor(x: CaptureRef)(using ctx: Context, vs: VarState = FrozenSepState): Boolean =
def accountsFor(x: CaptureRef)(using ctx: Context, vs: VarState = FrozenAllState): Boolean =

/** Like `refs.exists(p)`, but testing fresh cap instances in refs last */
def existsElem(refs: SimpleIdentitySet[CaptureRef], p: CaptureRef => Boolean): Boolean =
Expand All @@ -191,7 +191,10 @@ sealed abstract class CaptureSet extends Showable:
existsElem(elems, _.subsumes(x))
|| !x.isMaxCapability
&& !x.derivesFrom(defn.Caps_CapSet)
&& x.captureSetOfInfo.subCaptures(this, frozen = true).isOK
&& x.captureSetOfInfo.subCaptures(this)(using ctx,
vs match
case vs: FrozenVarState => vs
case _ => FrozenVarState()).isOK

comparer match
case comparer: ExplainingTypeComparer => comparer.traceIndented(debugInfo)(test)
Expand All @@ -207,7 +210,7 @@ sealed abstract class CaptureSet extends Showable:
*/
def mightAccountFor(x: CaptureRef)(using Context): Boolean =
reporting.trace(i"$this mightAccountFor $x, ${x.captureSetOfInfo}?", show = true):
elems.exists(_.subsumes(x)(using ctx, FrozenState()))
elems.exists(_.subsumes(x)(using ctx, FrozenVarState()))
|| !x.isMaxCapability
&& {
val elems = x.captureSetOfInfo.elems
Expand All @@ -228,8 +231,12 @@ sealed abstract class CaptureSet extends Showable:
* be added when making this test. An attempt to add either
* will result in failure.
*/
final def subCaptures(that: CaptureSet, frozen: Boolean)(using Context): CompareResult =
subCaptures(that)(using ctx, if frozen then FrozenState() else VarState())
final def subCaptures(that: CaptureSet, frozen: Frozen)(using Context): CompareResult =
val state = frozen match
case Frozen.None => VarState()
case Frozen.Vars => FrozenVarState()
case Frozen.All => FrozenAllState
subCaptures(that)(using ctx, state)

/** The subcapturing test, using a given VarState */
private def subCaptures(that: CaptureSet)(using Context, VarState): CompareResult =
Expand All @@ -246,16 +253,16 @@ sealed abstract class CaptureSet extends Showable:
* in a frozen state.
*/
def =:= (that: CaptureSet)(using Context): Boolean =
this.subCaptures(that, frozen = true).isOK
&& that.subCaptures(this, frozen = true).isOK
this.subCaptures(that, Frozen.All).isOK
&& that.subCaptures(this, Frozen.All).isOK

/** The smallest capture set (via <:<) that is a superset of both
* `this` and `that`
*/
def ++ (that: CaptureSet)(using Context): CaptureSet =
if this.subCaptures(that, frozen = true).isOK then
if this.subCaptures(that, Frozen.All).isOK then
if that.isAlwaysEmpty && this.keepAlways then this else that
else if that.subCaptures(this, frozen = true).isOK then this
else if that.subCaptures(this, Frozen.All).isOK then this
else if this.isConst && that.isConst then Const(this.elems ++ that.elems)
else Union(this, that)

Expand All @@ -267,8 +274,8 @@ sealed abstract class CaptureSet extends Showable:
/** The largest capture set (via <:<) that is a subset of both `this` and `that`
*/
def **(that: CaptureSet)(using Context): CaptureSet =
if this.subCaptures(that, frozen = true).isOK then this
else if that.subCaptures(this, frozen = true).isOK then that
if this.subCaptures(that, Frozen.Vars).isOK then this
else if that.subCaptures(this, Frozen.Vars).isOK then that
else if this.isConst && that.isConst then Const(elemIntersection(this, that))
else Intersection(this, that)

Expand Down Expand Up @@ -395,6 +402,12 @@ object CaptureSet:
type Vars = SimpleIdentitySet[Var]
type Deps = SimpleIdentitySet[CaptureSet]

/** An enum indicating a Frozen degree for subCapturing tests */
enum Frozen:
case None // operations are performed in a regular VarState
case Vars // operations are performed in a FrozenVarState
case All // operations are performed in FrozenAllState

@sharable private var varId = 0

/** If set to `true`, capture stack traces that tell us where sets are created */
Expand Down Expand Up @@ -538,7 +551,7 @@ object CaptureSet:
else
//if id == 34 then assert(!elem.isUniversalRootCapability)
assert(elem.isTrackableRef, elem)
assert(!this.isInstanceOf[HiddenSet] || summon[VarState] == FrozenSepState, summon[VarState])
assert(!this.isInstanceOf[HiddenSet] || summon[VarState] == FrozenAllState, summon[VarState])
elems += elem
if elem.isRootCapability then
rootAddedHandler()
Expand Down Expand Up @@ -1043,7 +1056,7 @@ object CaptureSet:
def getElems(v: Var): Option[Refs] = elemsMap.get(v)

/** Record elements, return whether this was allowed.
* By default, recording is allowed but the special state FrozenState
* By default, recording is allowed in regular both not in frozen states.
* overrides this.
*/
def putElems(v: Var, elems: Refs): Boolean = { elemsMap(v) = elems; true }
Expand All @@ -1055,14 +1068,14 @@ object CaptureSet:
def getDeps(v: Var): Option[Deps] = depsMap.get(v)

/** Record dependent sets, return whether this was allowed.
* By default, recording is allowed but the special state FrozenState
* By default, recording is allowed in regular both not in frozen states.
* overrides this.
*/
def putDeps(v: Var, deps: Deps): Boolean = { depsMap(v) = deps; true }

/** Record hidden elements in elemsMap of hidden set `v`,
* return whether this was allowed. By default, recording is allowed
* but the special state FrozenSepState overrides this.
* but the special state FrozenAllState overrides this.
*/
def putHidden(v: HiddenSet, elems: Refs): Boolean = { elemsMap(v) = elems; true }

Expand All @@ -1080,21 +1093,22 @@ object CaptureSet:
else false
end VarState

/** A special state that does not allow to record elements or dependent sets.
/** A class for states that do not allow to record elements or dependent sets.
* In effect this means that no new elements or dependent sets can be added
* in this state (since the previous state cannot be recorded in a snapshot)
* On the other hand, this state does allow by default Fresh.Cap to subsume arbitary
* types, which are then recorded in its hidden set.
* in these states (since the previous state cannot be recorded in a snapshot)
* On the other hand, these states do allow by default Fresh.Cap instances to
* subsume arbitary types, which are then recorded in their hidden sets.
*/
class FrozenState extends VarState:
class FrozenVarState extends VarState:
override def putElems(v: Var, refs: Refs) = false
override def putDeps(v: Var, deps: Deps) = false

@sharable
/** A frozen state that allows a Fresh.Cap instncce to subsume a
* reference `r` only if `r` is present in the hidden set of the instance.
/** A frozen state that allows a Fresh.Cap instancce to subsume a
* reference `r` only if `r` is already present in the hidden set of the instance.
* No new references can be added.
*/
object FrozenSepState extends FrozenState:
object FrozenAllState extends FrozenVarState:
override def putHidden(v: HiddenSet, elems: Refs): Boolean = false

@sharable
Expand Down
12 changes: 6 additions & 6 deletions compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
Original file line number Diff line number Diff line change
Expand Up @@ -18,7 +18,7 @@ import util.{SimpleIdentitySet, EqHashMap, EqHashSet, SrcPos, Property}
import transform.{Recheck, PreRecheck, CapturedVars}
import Recheck.*
import scala.collection.mutable
import CaptureSet.{withCaptureSetsExplained, IdempotentCaptRefMap, CompareResult}
import CaptureSet.{withCaptureSetsExplained, IdempotentCaptRefMap, CompareResult, Frozen}
import CCState.*
import StdNames.nme
import NameKinds.{DefaultGetterName, WildcardParamName, UniqueNameKind}
Expand Down Expand Up @@ -320,7 +320,7 @@ class CheckCaptures extends Recheck, SymTransformer:

/** Assert subcapturing `cs1 <: cs2` (available for debugging, otherwise unused) */
def assertSub(cs1: CaptureSet, cs2: CaptureSet)(using Context) =
assert(cs1.subCaptures(cs2, frozen = false).isOK, i"$cs1 is not a subset of $cs2")
assert(cs1.subCaptures(cs2, Frozen.None).isOK, i"$cs1 is not a subset of $cs2")

/** If `res` is not CompareResult.OK, report an error */
def checkOK(res: CompareResult, prefix: => String, pos: SrcPos, provenance: => String = "")(using Context): Unit =
Expand All @@ -334,15 +334,15 @@ class CheckCaptures extends Recheck, SymTransformer:
/** Check subcapturing `{elem} <: cs`, report error on failure */
def checkElem(elem: CaptureRef, cs: CaptureSet, pos: SrcPos, provenance: => String = "")(using Context) =
checkOK(
elem.singletonCaptureSet.subCaptures(cs, frozen = false),
elem.singletonCaptureSet.subCaptures(cs, Frozen.None),
i"$elem cannot be referenced here; it is not",
pos, provenance)

/** Check subcapturing `cs1 <: cs2`, report error on failure */
def checkSubset(cs1: CaptureSet, cs2: CaptureSet, pos: SrcPos,
provenance: => String = "", cs1description: String = "")(using Context) =
checkOK(
cs1.subCaptures(cs2, frozen = false),
cs1.subCaptures(cs2, Frozen.None),
if cs1.elems.size == 1 then i"reference ${cs1.elems.toList.head}$cs1description is not"
else i"references $cs1$cs1description are not all",
pos, provenance)
Expand Down Expand Up @@ -1390,7 +1390,7 @@ class CheckCaptures extends Recheck, SymTransformer:
val cs = actual.captureSet
if covariant then cs ++ leaked
else
if !leaked.subCaptures(cs, frozen = false).isOK then
if !leaked.subCaptures(cs, Frozen.None).isOK then
report.error(
em"""$expected cannot be box-converted to ${actual.capturing(leaked)}
|since the additional capture set $leaked resulted from box conversion is not allowed in $actual""", pos)
Expand Down Expand Up @@ -1713,7 +1713,7 @@ class CheckCaptures extends Recheck, SymTransformer:
val widened = ref.captureSetOfInfo
val added = widened.filter(isAllowed(_))
capt.println(i"heal $ref in $cs by widening to $added")
if !added.subCaptures(cs, frozen = false).isOK then
if !added.subCaptures(cs, Frozen.None).isOK then
val location = if meth.exists then i" of ${meth.showLocated}" else ""
val paramInfo =
if ref.paramName.info.kind.isInstanceOf[UniqueNameKind]
Expand Down
9 changes: 6 additions & 3 deletions compiler/src/dotty/tools/dotc/core/TypeComparer.scala
Original file line number Diff line number Diff line change
Expand Up @@ -2889,10 +2889,13 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
end inverse
end MapExistentials

protected def frozenDegree(frozen: Boolean) =
if frozen then CaptureSet.Frozen.Vars else CaptureSet.Frozen.None

protected def subCaptures(refs1: CaptureSet, refs2: CaptureSet, frozen: Boolean)(using Context): CaptureSet.CompareResult =
try
if assocExistentials.isEmpty then
refs1.subCaptures(refs2, frozen)
refs1.subCaptures(refs2, frozenDegree(frozen))
else
val mapped = refs1.map(MapExistentials(assocExistentials))
if mapped.elems.exists(Existential.isBadExistential)
Expand All @@ -2903,15 +2906,15 @@ class TypeComparer(@constructorOnly initctx: Context) extends ConstraintHandling
throw ex

protected def subCapturesMapped(refs1: CaptureSet, refs2: CaptureSet, frozen: Boolean)(using Context): CaptureSet.CompareResult =
refs1.subCaptures(refs2, frozen)
refs1.subCaptures(refs2, frozenDegree(frozen))

/** Is the boxing status of tp1 and tp2 the same, or alternatively, is
* the capture sets `refs1` of `tp1` a subcapture of the empty set?
* In the latter case, boxing status does not matter.
*/
protected def sameBoxed(tp1: Type, tp2: Type, refs1: CaptureSet)(using Context): Boolean =
(tp1.isBoxedCapturing == tp2.isBoxedCapturing)
|| refs1.subCaptures(CaptureSet.empty, frozenConstraint).isOK
|| refs1.subCaptures(CaptureSet.empty, frozenDegree(frozenConstraint)).isOK

// ----------- Diagnostics --------------------------------------------------

Expand Down
4 changes: 2 additions & 2 deletions compiler/src/dotty/tools/dotc/core/TypeOps.scala
Original file line number Diff line number Diff line change
Expand Up @@ -19,7 +19,7 @@ import typer.Inferencing.*
import typer.IfBottom
import reporting.TestingReporter
import cc.{CapturingType, derivedCapturingType, CaptureSet, captureSet, isBoxed, isBoxedCapturing}
import CaptureSet.{CompareResult, IdempotentCaptRefMap, IdentityCaptRefMap}
import CaptureSet.{CompareResult, IdempotentCaptRefMap, IdentityCaptRefMap, Frozen}

import scala.annotation.internal.sharable
import scala.annotation.threadUnsafe
Expand Down Expand Up @@ -161,7 +161,7 @@ object TypeOps:
TypeComparer.lub(simplify(l, theMap), simplify(r, theMap), isSoft = tp.isSoft)
case tp @ CapturingType(parent, refs) =>
if !ctx.mode.is(Mode.Type)
&& refs.subCaptures(parent.captureSet, frozen = true).isOK
&& refs.subCaptures(parent.captureSet, Frozen.All).isOK
&& (tp.isBoxed || !parent.isBoxedCapturing)
// fuse types with same boxed status and outer boxed with any type
then
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -136,7 +136,7 @@ object IndexedSeqView {

@SerialVersionUID(3L)
class Concat[A](prefix: SomeIndexedSeqOps[A]^, suffix: SomeIndexedSeqOps[A]^)
extends SeqView.Concat[A](prefix, caps.unsafe.unsafeAssumeSeparate(suffix)) with IndexedSeqView[A]
extends SeqView.Concat[A](prefix, suffix) with IndexedSeqView[A]

@SerialVersionUID(3L)
class Take[A](underlying: SomeIndexedSeqOps[A]^, n: Int)
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -75,7 +75,7 @@ private[mutable] object CheckedIndexedSeqView {

@SerialVersionUID(3L)
class Concat[A](prefix: SomeIndexedSeqOps[A]^, suffix: SomeIndexedSeqOps[A]^)(protected val mutationCount: () => Int)
extends IndexedSeqView.Concat[A](prefix, caps.unsafe.unsafeAssumeSeparate(suffix)) with CheckedIndexedSeqView[A]
extends IndexedSeqView.Concat[A](prefix, suffix) with CheckedIndexedSeqView[A]

@SerialVersionUID(3L)
class Take[A](underlying: SomeIndexedSeqOps[A]^, n: Int)(protected val mutationCount: () => Int)
Expand Down

0 comments on commit 76178ed

Please sign in to comment.