From 28eb166a04bd02754247029ba61a8fd3771deea1 Mon Sep 17 00:00:00 2001 From: odersky Date: Mon, 29 Sep 2025 13:07:02 +0200 Subject: [PATCH 01/14] Disallow nested capabilitirs in self types of classes Also: Factor out Vars that are part of inferred types of vals and defs as ProperVars. --- compiler/src/dotty/tools/dotc/cc/CaptureSet.scala | 4 ++++ compiler/src/dotty/tools/dotc/cc/Setup.scala | 4 ++-- 2 files changed, 6 insertions(+), 2 deletions(-) diff --git a/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala b/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala index 464114a2b672..acd79d663ab7 100644 --- a/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala +++ b/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala @@ -954,6 +954,10 @@ object CaptureSet: class RefiningVar(owner: Symbol)(using Context) extends Var(owner): override def disallowBadRoots(upto: Symbol)(handler: () => Context ?=> Unit)(using Context) = this + /** Variables created in types of inferred type trees */ + class ProperVar(override val owner: Symbol, initialElems: Refs, nestedOK: Boolean)(using /*@constructorOnly*/ ictx: Context) + extends Var(owner, initialElems, nestedOK) + /** A variable that is derived from some other variable via a map or filter. */ abstract class DerivedVar(owner: Symbol, initialElems: Refs)(using @constructorOnly ctx: Context) extends Var(owner, initialElems): diff --git a/compiler/src/dotty/tools/dotc/cc/Setup.scala b/compiler/src/dotty/tools/dotc/cc/Setup.scala index b9606738731e..f44b44bd7df7 100644 --- a/compiler/src/dotty/tools/dotc/cc/Setup.scala +++ b/compiler/src/dotty/tools/dotc/cc/Setup.scala @@ -685,7 +685,7 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI: // Infer the self type for the rest, which is all classes without explicit // self types (to which we also add nested module classes), provided they are // neither pure, nor are publicily extensible with an unconstrained self type. - val cs = CaptureSet.Var(cls) + val cs = CaptureSet.ProperVar(cls, CaptureSet.emptyRefs, nestedOK = false) if cls.derivesFrom(defn.Caps_Capability) then // If cls is a capability class, we need to add a fresh readonly capability to // ensure we cannot treat the class as pure. @@ -852,7 +852,7 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI: /** Add a capture set variable to `tp` if necessary. */ private def addVar(tp: Type, owner: Symbol)(using Context): Type = - decorate(tp, CaptureSet.Var(owner, _, nestedOK = !ctx.mode.is(Mode.CCPreciseOwner))) + decorate(tp, CaptureSet.ProperVar(owner, _, nestedOK = !ctx.mode.is(Mode.CCPreciseOwner))) /** A map that adds capture sets at all contra- and invariant positions * in a type where a capture set would be needed. This is used to make types From cd0bc944abe1598efd2655e4bae5cae25ba64235 Mon Sep 17 00:00:00 2001 From: odersky Date: Tue, 30 Sep 2025 13:43:27 +0200 Subject: [PATCH 02/14] SepCheck: Record span capture sets instead of deep capture sets --- compiler/src/dotty/tools/dotc/cc/CaptureOps.scala | 13 ++++++++----- compiler/src/dotty/tools/dotc/cc/CaptureSet.scala | 12 ++++++++---- compiler/src/dotty/tools/dotc/cc/SepCheck.scala | 8 ++++++-- tests/neg-custom-args/captures/sepchecks2.check | 8 -------- tests/neg-custom-args/captures/sepchecks2.scala | 2 +- .../neg-custom-args/captures/unsound-reach-6.check | 4 ---- .../neg-custom-args/captures/unsound-reach-6.scala | 2 +- 7 files changed, 24 insertions(+), 25 deletions(-) diff --git a/compiler/src/dotty/tools/dotc/cc/CaptureOps.scala b/compiler/src/dotty/tools/dotc/cc/CaptureOps.scala index 420e6e1ab253..a3ccd748bcfb 100644 --- a/compiler/src/dotty/tools/dotc/cc/CaptureOps.scala +++ b/compiler/src/dotty/tools/dotc/cc/CaptureOps.scala @@ -157,8 +157,8 @@ extension (tp: Type) * a singleton capability `x` or a reach capability `x*`, the deep capture * set can be narrowed to`{x*}`. */ - def deepCaptureSet(includeTypevars: Boolean)(using Context): CaptureSet = - val dcs = CaptureSet.ofTypeDeeply(tp.widen.stripCapturing, includeTypevars) + def deepCaptureSet(includeTypevars: Boolean, includeBoxed: Boolean = true)(using Context): CaptureSet = + val dcs = CaptureSet.ofTypeDeeply(tp.widen.stripCapturing, includeTypevars, includeBoxed) if dcs.isAlwaysEmpty then tp.captureSet else tp match case tp: ObjectCapability if tp.isTrackableRef => tp.reach.singletonCaptureSet @@ -167,6 +167,9 @@ extension (tp: Type) def deepCaptureSet(using Context): CaptureSet = deepCaptureSet(includeTypevars = false) + def spanCaptureSet(using Context): CaptureSet = + deepCaptureSet(includeTypevars = false, includeBoxed = false) + /** A type capturing `ref` */ def capturing(ref: Capability)(using Context): Type = if tp.captureSet.accountsFor(ref) then tp @@ -362,7 +365,7 @@ extension (tp: Type) */ def derivesFromCapTraitDeeply(cls: ClassSymbol)(using Context): Boolean = val accumulate = new DeepTypeAccumulator[Boolean]: - def capturingCase(acc: Boolean, parent: Type, refs: CaptureSet) = + def capturingCase(acc: Boolean, parent: Type, refs: CaptureSet, boxed: Boolean) = this(acc, parent) && (parent.derivesFromCapTrait(cls) || refs.isConst && refs.elems.forall(_.derivesFromCapTrait(cls))) @@ -734,7 +737,7 @@ object ContainsParam: abstract class DeepTypeAccumulator[T](using Context) extends TypeAccumulator[T]: val seen = util.HashSet[Symbol]() - protected def capturingCase(acc: T, parent: Type, refs: CaptureSet): T + protected def capturingCase(acc: T, parent: Type, refs: CaptureSet, boxed: Boolean): T protected def abstractTypeCase(acc: T, t: TypeRef, upperBound: Type): T @@ -742,7 +745,7 @@ abstract class DeepTypeAccumulator[T](using Context) extends TypeAccumulator[T]: if variance < 0 then acc else t.dealias match case t @ CapturingType(parent, cs) => - capturingCase(acc, parent, cs) + capturingCase(acc, parent, cs, t.isBoxed) case t: TypeRef if t.symbol.isAbstractOrParamType && !seen.contains(t.symbol) => seen += t.symbol abstractTypeCase(acc, t, t.info.bounds.hi) diff --git a/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala b/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala index acd79d663ab7..c6c197da6723 100644 --- a/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala +++ b/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala @@ -957,7 +957,7 @@ object CaptureSet: /** Variables created in types of inferred type trees */ class ProperVar(override val owner: Symbol, initialElems: Refs, nestedOK: Boolean)(using /*@constructorOnly*/ ictx: Context) extends Var(owner, initialElems, nestedOK) - + /** A variable that is derived from some other variable via a map or filter. */ abstract class DerivedVar(owner: Symbol, initialElems: Refs)(using @constructorOnly ctx: Context) extends Var(owner, initialElems): @@ -1619,13 +1619,17 @@ object CaptureSet: /** The deep capture set of a type is the union of all covariant occurrences of * capture sets. Nested existential sets are approximated with `cap`. */ - def ofTypeDeeply(tp: Type, includeTypevars: Boolean = false)(using Context): CaptureSet = + def ofTypeDeeply(tp: Type, includeTypevars: Boolean = false, includeBoxed: Boolean = true)(using Context): CaptureSet = val collect = new DeepTypeAccumulator[CaptureSet]: - def capturingCase(acc: CaptureSet, parent: Type, refs: CaptureSet) = - this(acc, parent) ++ refs + + def capturingCase(acc: CaptureSet, parent: Type, refs: CaptureSet, boxed: Boolean) = + if includeBoxed || !boxed then this(acc, parent) ++ refs + else this(acc, parent) + def abstractTypeCase(acc: CaptureSet, t: TypeRef, upperBound: Type) = if includeTypevars && upperBound.isExactlyAny then fresh(Origin.DeepCS(t)) else this(acc, upperBound) + collect(CaptureSet.empty, tp) type AssumedContains = immutable.Map[TypeRef, SimpleIdentitySet[Capability]] diff --git a/compiler/src/dotty/tools/dotc/cc/SepCheck.scala b/compiler/src/dotty/tools/dotc/cc/SepCheck.scala index 5c05d27943f6..6250dc18783b 100644 --- a/compiler/src/dotty/tools/dotc/cc/SepCheck.scala +++ b/compiler/src/dotty/tools/dotc/cc/SepCheck.scala @@ -312,8 +312,12 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser: private def formalCaptures(arg: Tree)(using Context): Refs = arg.formalType.orElse(arg.nuType).deepCaptureSet.elems - /** The deep capture set if the type of `tree` */ + /** The span capture set if the type of `tree` */ private def captures(tree: Tree)(using Context): Refs = + tree.nuType.spanCaptureSet.elems + + /** The deep capture set if the type of `tree` */ + private def deepCaptures(tree: Tree)(using Context): Refs = tree.nuType.deepCaptureSet.elems // ---- Error reporting TODO Once these are stabilized, move to messages -----" + @@ -376,7 +380,7 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser: if clashIdx == 0 && !isShowableMethod then "" // we already mentioned the type in `funStr` else i" with type ${clashing.nuType}" val hiddenSet = formalCaptures(polyArg).hiddenSet - val clashSet = captures(clashing) + val clashSet = deepCaptures(clashing) report.error( em"""Separation failure: argument of type ${polyArg.nuType} |to $funStr diff --git a/tests/neg-custom-args/captures/sepchecks2.check b/tests/neg-custom-args/captures/sepchecks2.check index 5529c2a6d1c8..98e45a4e23b4 100644 --- a/tests/neg-custom-args/captures/sepchecks2.check +++ b/tests/neg-custom-args/captures/sepchecks2.check @@ -1,11 +1,3 @@ --- Error: tests/neg-custom-args/captures/sepchecks2.scala:10:10 -------------------------------------------------------- -10 | println(c) // error - | ^ - | Separation failure: Illegal access to {c} which is hidden by the previous definition - | of value xs with type List[() => Unit]. - | This type hides capabilities {c} - | - | where: => refers to a fresh root capability in the type of value xs -- Error: tests/neg-custom-args/captures/sepchecks2.scala:13:7 --------------------------------------------------------- 13 | foo((() => println(c)) :: Nil, c) // error | ^^^^^^^^^^^^^^^^^^^^^^^^ diff --git a/tests/neg-custom-args/captures/sepchecks2.scala b/tests/neg-custom-args/captures/sepchecks2.scala index d3310fc8b3ca..a255b4059902 100644 --- a/tests/neg-custom-args/captures/sepchecks2.scala +++ b/tests/neg-custom-args/captures/sepchecks2.scala @@ -7,7 +7,7 @@ def bar(x: (Object^, Object^)): Unit = ??? def Test(consume c: Object^) = val xs: List[() => Unit] = (() => println(c)) :: Nil - println(c) // error + println(c) def Test2(c: Object^, d: Object^): Unit = foo((() => println(c)) :: Nil, c) // error diff --git a/tests/neg-custom-args/captures/unsound-reach-6.check b/tests/neg-custom-args/captures/unsound-reach-6.check index b9e9b287dace..4f72a93d3015 100644 --- a/tests/neg-custom-args/captures/unsound-reach-6.check +++ b/tests/neg-custom-args/captures/unsound-reach-6.check @@ -26,7 +26,3 @@ | ^^ | Local reach capability ys* leaks into capture scope of method test. | You could try to abstract the capabilities referred to by ys* in a capset variable. --- Error: tests/neg-custom-args/captures/unsound-reach-6.scala:19:14 --------------------------------------------------- -19 | val z = f(ys) // error consume failure - | ^^ - |Separation failure: argument to consume parameter with type List[() ->{io} Unit] refers to non-local parameter io diff --git a/tests/neg-custom-args/captures/unsound-reach-6.scala b/tests/neg-custom-args/captures/unsound-reach-6.scala index 0d737828d466..4ccd9f4c5795 100644 --- a/tests/neg-custom-args/captures/unsound-reach-6.scala +++ b/tests/neg-custom-args/captures/unsound-reach-6.scala @@ -16,7 +16,7 @@ def test(io: IO^)(ys: List[() ->{io} Unit]) = def test(io: IO^) = def ys: List[() ->{io} Unit] = ??? val x = () => - val z = f(ys) // error consume failure + val z = f(ys) // ok, was error consume failure z() val _: () -> Unit = x // error () From 8de92b975417bf843c9c6f3f3246873dd8f7edff Mon Sep 17 00:00:00 2001 From: odersky Date: Tue, 30 Sep 2025 18:24:35 +0200 Subject: [PATCH 03/14] SepCheck: Revise definition of peaks New definition does not go upwards from hidden to hiding, but does go into hidden sets. Except for a variant `exposedPeaks` which does not do that. This is currently very rough. There's a switch to go from old to new behavior based on source version. Todo: Polish and then drop the switch if we are convinced verything works as expected. --- .../src/dotty/tools/dotc/cc/Capability.scala | 13 ++- .../src/dotty/tools/dotc/cc/SepCheck.scala | 105 ++++++++++++++---- .../captures/cc-poly-varargs.scala | 4 +- .../colltest5/CollectionStrawManCC5_1.scala | 2 +- 4 files changed, 99 insertions(+), 25 deletions(-) rename tests/{pos-custom-args => neg-custom-args}/captures/cc-poly-varargs.scala (77%) diff --git a/compiler/src/dotty/tools/dotc/cc/Capability.scala b/compiler/src/dotty/tools/dotc/cc/Capability.scala index 5a6fb7df5511..35c2910ab171 100644 --- a/compiler/src/dotty/tools/dotc/cc/Capability.scala +++ b/compiler/src/dotty/tools/dotc/cc/Capability.scala @@ -12,7 +12,7 @@ import CCState.* import Periods.{NoRunId, RunWidth} import compiletime.uninitialized import StdNames.nme -import CaptureSet.VarState +import CaptureSet.{Refs, emptyRefs, VarState} import Annotations.Annotation import Flags.* import config.Printers.capt @@ -547,6 +547,17 @@ object Capabilities: captureSetValid = currentId computed + /** The elements hidden by this capability, if this is a FreshCap + * or a derived version of one. Read-only status is transferred from + * the capability to its hidden set. TODO Should classifiers also be + * transferred? + */ + def hiddenElems(using Context): Refs = this.stripRestricted.stripReadOnly match + case self: FreshCap => + val hidden = self.hiddenSet.elems + if isReadOnly then hidden.map(_.readOnly) else hidden + case _ => emptyRefs + /** The transitive classifiers of this capability. */ def transClassifiers(using Context): Classifiers = def toClassifiers(cls: ClassSymbol): Classifiers = diff --git a/compiler/src/dotty/tools/dotc/cc/SepCheck.scala b/compiler/src/dotty/tools/dotc/cc/SepCheck.scala index 6250dc18783b..ae1215723e45 100644 --- a/compiler/src/dotty/tools/dotc/cc/SepCheck.scala +++ b/compiler/src/dotty/tools/dotc/cc/SepCheck.scala @@ -98,7 +98,7 @@ object SepCheck: var refs: Array[Capability] = new Array(4) var locs: Array[SrcPos] = new Array(4) var size = 0 - var peaks: Refs = emptyRefs + var exposedPeaks: Refs = emptyRefs private def double[T <: AnyRef : ClassTag](xs: Array[T]): Array[T] = val xs1 = new Array[T](xs.length * 2) @@ -117,10 +117,10 @@ object SepCheck: if i < size then locs(i) else null def clashing(ref: Capability)(using Context): SrcPos | Null = - val refPeaks = ref.peaks - if !peaks.sharedWith(refPeaks).isEmpty then + val refPeaks = ref.exposedPeaks + if !exposedPeaks.sharedWith(refPeaks).isEmpty then var i = 0 - while i < size && refs(i).peaks.sharedWith(refPeaks).isEmpty do + while i < size && refs(i).exposedPeaks.sharedWith(refPeaks).isEmpty do i += 1 assert(i < size) locs(i) @@ -133,7 +133,7 @@ object SepCheck: refs(size) = ref locs(size) = loc size += 1 - peaks = peaks ++ ref.peaks + exposedPeaks = exposedPeaks ++ ref.exposedPeaks /** Add all references with their associated positions from `that` which * are not yet in the set. @@ -146,14 +146,14 @@ object SepCheck: */ def segment(op: => Unit): ConsumedSet = val start = size - val savedPeaks = peaks + val savedPeaks = exposedPeaks try op if size == start then EmptyConsumedSet else ConstConsumedSet(refs.slice(start, size), locs.slice(start, size)) finally size = start - peaks = savedPeaks + exposedPeaks = savedPeaks end MutConsumedSet val EmptyConsumedSet = ConstConsumedSet(Array(), Array()) @@ -164,6 +164,9 @@ object SepCheck: extension (refs: Refs) + private def peaks_(using Context): Refs = + refs.filter(_.isTerminalCapability) + /** The footprint of a set of references `refs` the smallest set `F` such that * 1. all capabilities in `refs` satisfying (1) are in `F` * 2. if `f in F` then the footprint of `f`'s info is also in `F`. @@ -179,6 +182,26 @@ object SepCheck: val elems: Refs = refs.filter(retain) recur(elems, elems.toList) + private def exposedPeaks(using Context): Refs = + footPrint(followHidden = false).peaks_ + + private def footPrint(followHidden: Boolean)(using Context): Refs = + def recur(seen: Refs, acc: Refs, newElems: List[Capability]): Refs = trace(i"peaks $acc, $newElems = "): + newElems match + case newElem :: newElems1 => + if seen.contains(newElem) then + recur(seen, acc, newElems1) + else newElem.stripRestricted.stripReadOnly match + case _: FreshCap if !newElem.isKnownClassifiedAs(defn.Caps_SharedCapability) => + val hiddens = if followHidden then newElem.hiddenElems.toList else Nil + recur(seen + newElem, acc + newElem, hiddens ++ newElems1) + case _ if newElem.isTerminalCapability => + recur(seen + newElem, acc, newElems1) + case _ => + recur(seen + newElem, acc, newElem.captureSetOfInfo.dropEmpties().elems.toList ++ newElems1) + case Nil => acc + recur(emptyRefs, emptyRefs, refs.toList) + private def peaks(using Context): Refs = def recur(seen: Refs, acc: Refs, newElems: List[Capability]): Refs = trace(i"peaks $acc, $newElems = "): newElems match @@ -199,15 +222,43 @@ object SepCheck: then recur(seen + newElem, acc, newElems1) else recur(seen + newElem, acc, newElem.captureSetOfInfo.dropEmpties().elems.toList ++ newElems1) case Nil => acc - recur(emptyRefs, emptyRefs, refs.toList) + if ccConfig.newScheme then footPrint(followHidden = true).peaks_ + else recur(emptyRefs, emptyRefs, refs.toList) - /** The shared peaks between `refs` and `other` */ + /** The shared elements between `refs` and `other`. + * These are the core capabilities and fresh capabilities that appear + * in a (possibly classified or readOnly) version in both sets and that + * that appear in a non-readOnly version in at least one of the sets. + */ private def sharedWith(other: Refs)(using Context): Refs = def common(refs1: Refs, refs2: Refs) = - refs1.filter: ref => - !ref.isReadOnly && refs2.exists(_.stripReadOnly eq ref) + var acc: Refs = emptyRefs + refs1.foreach: ref => + if !ref.isReadOnly then + val coreRef = ref.stripRestricted + if refs2.exists(_.stripRestricted.stripReadOnly eq coreRef) then + acc += coreRef + acc common(refs, other) ++ common(other, refs) + /** The shared peaks between `refs` and `other` */ + private def sharedPeaks(other: Refs)(using Context): Refs = + refs.peaks_.sharedWith(other.peaks_) + + /** Reduce a non-empty footprint set to + * 1. all its non-terminial capabilities if that set is nonempty, or + * 2. one of its non-hidden capabilities if one exists, or + * 3. one of its capabilities. + */ + def reduced(using Context): Refs = + assert(!refs.isEmpty) + val concrete = refs.filter(!_.isTerminalCapability) + if !concrete.isEmpty then concrete + else + val notHidden = refs -- refs.flatMap(_.hiddenElems) + if !notHidden.isEmpty then SimpleIdentitySet(notHidden.nth(0)) + else SimpleIdentitySet(refs.nth(0)) + /** The overlap of two footprint sets F1 and F2. This contains all exclusive references `r` * such that one of the following is true: * 1. @@ -282,6 +333,7 @@ object SepCheck: extension (ref: Capability) def peaks(using Context): Refs = SimpleIdentitySet(ref).peaks + def exposedPeaks(using Context): Refs = SimpleIdentitySet(ref).exposedPeaks class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser: import checker.* @@ -313,7 +365,7 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser: arg.formalType.orElse(arg.nuType).deepCaptureSet.elems /** The span capture set if the type of `tree` */ - private def captures(tree: Tree)(using Context): Refs = + private def spanCaptures(tree: Tree)(using Context): Refs = tree.nuType.spanCaptureSet.elems /** The deep capture set if the type of `tree` */ @@ -480,7 +532,7 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser: capt.println( i"""check separate $fn($args), fnCaptures = $fnCaptures, | formalCaptures = ${args.map(arg => CaptureSet(formalCaptures(arg)))}, - | actualCaptures = ${args.map(arg => CaptureSet(captures(arg)))}, + | actualCaptures = ${args.map(arg => CaptureSet(spanCaptures(arg)))}, | resultPeaks = ${resultPeaks}, | deps = ${deps.toList}""") val parts = qual :: args @@ -488,7 +540,7 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser: for arg <- args do val argPeaks = PeaksPair( - captures(arg).peaks, + spanCaptures(arg).peaks, if arg.needsSepCheck then formalCaptures(arg).hiddenSet.peaks else emptyRefs) val argDeps = deps(arg) @@ -516,7 +568,7 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser: val clashing = clashingPart(argPeaks.hidden, _.actual) if !clashing.isEmpty then if !reported.contains(clashing) then - //println(i"CLASH $arg / ${argPeaks.formal} vs $clashing / ${peaksOfTree(clashing).actual} / ${captures(clashing).peaks}") + //println(i"CLASH $arg / ${argPeaks.formal} vs $clashing / ${peaksOfTree(clashing).actual} / ${spanCaptures(clashing).peaks}") sepApplyError(fn, parts, arg, clashing) else assert(!argDeps.isEmpty) @@ -563,7 +615,9 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser: for ref <- used do val pos = consumed.clashing(ref) - if pos != null then consumeError(ref, pos, tree.srcPos) + if pos != null then + // println(i"consumed so far ${consumed.refs.toList} with peaks ${consumed.exposedPeaks.toList}, used = $used, exposed = ${ref.exposedPeaks}") + consumeError(ref, pos, tree.srcPos) end checkUse /** If `tp` denotes some version of a singleton capability `x.type` the set `{x, x*}` @@ -776,7 +830,7 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser: checkConsumedRefs(toCheck, tpe, role, i"${role.description} $tpe hides", pos) case TypeRole.Argument(arg) => if tpe.hasAnnotation(defn.ConsumeAnnot) then - val capts = captures(arg).footprint + val capts = spanCaptures(arg).footprint checkConsumedRefs(capts, tpe, role, i"argument to consume parameter with type ${arg.nuType} refers to", pos) case _ => @@ -901,8 +955,8 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser: def checkValOrDefDef(tree: ValOrDefDef)(using Context): Unit = if !tree.symbol.isOneOf(TermParamOrAccessor) && !isUnsafeAssumeSeparate(tree.rhs) then checkType(tree.tpt, tree.symbol) - capt.println(i"sep check def ${tree.symbol}: ${tree.tpt} with ${captures(tree.tpt).hiddenSet.footprint}") - pushDef(tree, captures(tree.tpt).hiddenSet.deductSymRefs(tree.symbol)) + capt.println(i"sep check def ${tree.symbol}: ${tree.tpt} with ${spanCaptures(tree.tpt).hiddenSet.footprint}") + pushDef(tree, spanCaptures(tree.tpt).hiddenSet.deductSymRefs(tree.symbol)) def inSection[T](op: => T)(using Context): T = val savedDefsShadow = defsShadow @@ -918,8 +972,17 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser: */ def skippable(sym: Symbol)(using Context): Boolean = sym.isInlineMethod - // We currently skip inline method bodies since these seem to generan + // We currently skip inline method bodies since these seem to generate // spurious recheck completions. Test case is i20237.scala + || sym.is(Synthetic) && sym.name.startsWith("_") + // Approximation of case class getters _1, _2, ... . We can't separation check them + // or colltest5/CollectionStrawManCC5_1.scala would fail with an error in + // case class Filter. TODO Investigate to decide what needs to be done + // - Can we make the accessors work somehow? + // - If not, should we disable just accessors or all synthetic methods? + // Reporting an error in a synthetic method is very frustrating since we don't have + // a position with source code to show. On the other hand, skipping all synthetic members + // might cause soundness issues. /** Traverse `tree` and perform separation checks everywhere */ def traverse(tree: Tree)(using Context): Unit = @@ -929,7 +992,7 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser: case tree @ Select(qual, _) if tree.symbol.is(Method) && tree.symbol.isConsumeParam => traverseChildren(tree) checkConsumedRefs( - captures(qual).footprint, qual.nuType, + spanCaptures(qual).footprint, qual.nuType, TypeRole.Qualifier(qual, tree.symbol), i"call prefix of consume ${tree.symbol} refers to", qual.srcPos) case tree: GenericApply => diff --git a/tests/pos-custom-args/captures/cc-poly-varargs.scala b/tests/neg-custom-args/captures/cc-poly-varargs.scala similarity index 77% rename from tests/pos-custom-args/captures/cc-poly-varargs.scala rename to tests/neg-custom-args/captures/cc-poly-varargs.scala index d39d4a9c30e5..6907bc7f91fa 100644 --- a/tests/pos-custom-args/captures/cc-poly-varargs.scala +++ b/tests/neg-custom-args/captures/cc-poly-varargs.scala @@ -8,6 +8,6 @@ def race[T, Cap^](sources: Source[T, {Cap}]^{Cap}*): Source[T, {Cap}]^{Cap} = ?? def either[T1, T2, Cap^]( src1: Source[T1, {Cap}]^{Cap}, src2: Source[T2, {Cap}]^{Cap}): Source[Either[T1, T2], {Cap}]^{Cap} = - val left = src1.transformValuesWith(Left(_)) - val right = src2.transformValuesWith(Right(_)) + val left = src1.transformValuesWith(Left(_)) // error + val right = src2.transformValuesWith(Right(_)) // error race(left, right) diff --git a/tests/run-custom-args/captures/colltest5/CollectionStrawManCC5_1.scala b/tests/run-custom-args/captures/colltest5/CollectionStrawManCC5_1.scala index 1143cdb30d5e..2de3ba603507 100644 --- a/tests/run-custom-args/captures/colltest5/CollectionStrawManCC5_1.scala +++ b/tests/run-custom-args/captures/colltest5/CollectionStrawManCC5_1.scala @@ -532,7 +532,7 @@ object CollectionStrawMan5 { } -1 } - def filter(p: A => Boolean): Iterator[A]^{this, p} = new Iterator[A] { + def filter(p: A ->{cap, this} Boolean): Iterator[A]^{this, p} = new Iterator[A] { private var hd: A = compiletime.uninitialized private var hdDefined: Boolean = false From a968863b1747345d94e7ffbe2eab0ed1f326ca01 Mon Sep 17 00:00:00 2001 From: odersky Date: Wed, 1 Oct 2025 12:06:19 +0200 Subject: [PATCH 04/14] Refactorings and renamings --- .../src/dotty/tools/dotc/cc/Capability.scala | 19 +- .../src/dotty/tools/dotc/cc/SepCheck.scala | 182 ++++++++++-------- 2 files changed, 110 insertions(+), 91 deletions(-) diff --git a/compiler/src/dotty/tools/dotc/cc/Capability.scala b/compiler/src/dotty/tools/dotc/cc/Capability.scala index 35c2910ab171..27294d42fd54 100644 --- a/compiler/src/dotty/tools/dotc/cc/Capability.scala +++ b/compiler/src/dotty/tools/dotc/cc/Capability.scala @@ -548,14 +548,19 @@ object Capabilities: computed /** The elements hidden by this capability, if this is a FreshCap - * or a derived version of one. Read-only status is transferred from - * the capability to its hidden set. TODO Should classifiers also be - * transferred? + * or a derived version of one. Read-only status and restrictions + * are transferred from the capability to its hidden set. */ - def hiddenElems(using Context): Refs = this.stripRestricted.stripReadOnly match - case self: FreshCap => - val hidden = self.hiddenSet.elems - if isReadOnly then hidden.map(_.readOnly) else hidden + def hiddenSet(using Context): Refs = computeHiddenSet(identity) + + /** Compute hidden set of this capability. + * Restrictions and read-only status transfer from the capability to its + * hidden set. + */ + def computeHiddenSet(f: Refs => Refs)(using Context): Refs = this match + case self: FreshCap => f(self.hiddenSet.elems) + case Restricted(elem1, cls) => elem1.computeHiddenSet(f).map(_.restrict(cls)) + case ReadOnly(elem1) => elem1.computeHiddenSet(f).map(_.readOnly) case _ => emptyRefs /** The transitive classifiers of this capability. */ diff --git a/compiler/src/dotty/tools/dotc/cc/SepCheck.scala b/compiler/src/dotty/tools/dotc/cc/SepCheck.scala index ae1215723e45..e20a382e9bad 100644 --- a/compiler/src/dotty/tools/dotc/cc/SepCheck.scala +++ b/compiler/src/dotty/tools/dotc/cc/SepCheck.scala @@ -98,7 +98,7 @@ object SepCheck: var refs: Array[Capability] = new Array(4) var locs: Array[SrcPos] = new Array(4) var size = 0 - var exposedPeaks: Refs = emptyRefs + var directPeaks : Refs = emptyRefs private def double[T <: AnyRef : ClassTag](xs: Array[T]): Array[T] = val xs1 = new Array[T](xs.length * 2) @@ -117,10 +117,10 @@ object SepCheck: if i < size then locs(i) else null def clashing(ref: Capability)(using Context): SrcPos | Null = - val refPeaks = ref.exposedPeaks - if !exposedPeaks.sharedWith(refPeaks).isEmpty then + val refPeaks = ref.directPeaks + if !directPeaks .sharedPeaks(refPeaks).isEmpty then var i = 0 - while i < size && refs(i).exposedPeaks.sharedWith(refPeaks).isEmpty do + while i < size && refs(i).directPeaks .sharedPeaks(refPeaks).isEmpty do i += 1 assert(i < size) locs(i) @@ -133,7 +133,7 @@ object SepCheck: refs(size) = ref locs(size) = loc size += 1 - exposedPeaks = exposedPeaks ++ ref.exposedPeaks + directPeaks = directPeaks ++ ref.directPeaks /** Add all references with their associated positions from `that` which * are not yet in the set. @@ -146,14 +146,14 @@ object SepCheck: */ def segment(op: => Unit): ConsumedSet = val start = size - val savedPeaks = exposedPeaks + val savedPeaks = directPeaks try op if size == start then EmptyConsumedSet else ConstConsumedSet(refs.slice(start, size), locs.slice(start, size)) finally size = start - exposedPeaks = savedPeaks + directPeaks = savedPeaks end MutConsumedSet val EmptyConsumedSet = ConstConsumedSet(Array(), Array()) @@ -164,14 +164,17 @@ object SepCheck: extension (refs: Refs) - private def peaks_(using Context): Refs = + private def peaks(using Context): Refs = refs.filter(_.isTerminalCapability) + private def nonPeaks(using Context): Refs = + refs.filter(!_.isTerminalCapability) + /** The footprint of a set of references `refs` the smallest set `F` such that * 1. all capabilities in `refs` satisfying (1) are in `F` * 2. if `f in F` then the footprint of `f`'s info is also in `F`. */ - private def footprint(using Context): Refs = + private def oldFootprint(using Context): Refs = def retain(ref: Capability) = !ref.isTerminalCapability def recur(elems: Refs, newElems: List[Capability]): Refs = newElems match case newElem :: newElems1 => @@ -182,10 +185,12 @@ object SepCheck: val elems: Refs = refs.filter(retain) recur(elems, elems.toList) - private def exposedPeaks(using Context): Refs = - footPrint(followHidden = false).peaks_ - - private def footPrint(followHidden: Boolean)(using Context): Refs = + /** The footprint of a set of capabilities `refs` is the closure + * of `refs` under `_.captureSetOfInfo`, dropping any shared terminal + * capabilities. If `followHidden` is true, we close under both + * `_.captureSetOfInfo` and `_.hiddenElems`. + */ + private def computeFootprint(followHidden: Boolean)(using Context): Refs = def recur(seen: Refs, acc: Refs, newElems: List[Capability]): Refs = trace(i"peaks $acc, $newElems = "): newElems match case newElem :: newElems1 => @@ -193,7 +198,7 @@ object SepCheck: recur(seen, acc, newElems1) else newElem.stripRestricted.stripReadOnly match case _: FreshCap if !newElem.isKnownClassifiedAs(defn.Caps_SharedCapability) => - val hiddens = if followHidden then newElem.hiddenElems.toList else Nil + val hiddens = if followHidden then newElem.hiddenSet.toList else Nil recur(seen + newElem, acc + newElem, hiddens ++ newElems1) case _ if newElem.isTerminalCapability => recur(seen + newElem, acc, newElems1) @@ -202,7 +207,22 @@ object SepCheck: case Nil => acc recur(emptyRefs, emptyRefs, refs.toList) - private def peaks(using Context): Refs = + /** The direct footprint of a set of capabilities `refs` is the closure + * of `refs` under `_.captureSetOfInfo`, dropping any shared terminal + * capabilities. + */ + private def directFootprint(using Context): Refs = + computeFootprint(followHidden = false) + + /** The hidden footprint of a set of capabilities `refs` is the closure + * of `refs` under `_.captureSetOfInfo` and `_.hiddenElems`, dropping any shared terminal + * capabilities. + */ + private def hiddenFootprint(using Context): Refs = + computeFootprint(followHidden = true) + + /** Same as hiddenFootprint.peaks under new scheme. Was maximal elements before */ + private def transPeaks(using Context): Refs = def recur(seen: Refs, acc: Refs, newElems: List[Capability]): Refs = trace(i"peaks $acc, $newElems = "): newElems match case newElem :: newElems1 => @@ -222,15 +242,15 @@ object SepCheck: then recur(seen + newElem, acc, newElems1) else recur(seen + newElem, acc, newElem.captureSetOfInfo.dropEmpties().elems.toList ++ newElems1) case Nil => acc - if ccConfig.newScheme then footPrint(followHidden = true).peaks_ + if ccConfig.newScheme then hiddenFootprint.peaks else recur(emptyRefs, emptyRefs, refs.toList) - /** The shared elements between `refs` and `other`. + /** The shared elements between the peak sets `refs` and `other`. * These are the core capabilities and fresh capabilities that appear * in a (possibly classified or readOnly) version in both sets and that * that appear in a non-readOnly version in at least one of the sets. */ - private def sharedWith(other: Refs)(using Context): Refs = + private def sharedPeaks(other: Refs)(using Context): Refs = def common(refs1: Refs, refs2: Refs) = var acc: Refs = emptyRefs refs1.foreach: ref => @@ -239,26 +259,10 @@ object SepCheck: if refs2.exists(_.stripRestricted.stripReadOnly eq coreRef) then acc += coreRef acc + assert(refs.forall(_.isTerminalCapability)) + assert(other.forall(_.isTerminalCapability)) common(refs, other) ++ common(other, refs) - /** The shared peaks between `refs` and `other` */ - private def sharedPeaks(other: Refs)(using Context): Refs = - refs.peaks_.sharedWith(other.peaks_) - - /** Reduce a non-empty footprint set to - * 1. all its non-terminial capabilities if that set is nonempty, or - * 2. one of its non-hidden capabilities if one exists, or - * 3. one of its capabilities. - */ - def reduced(using Context): Refs = - assert(!refs.isEmpty) - val concrete = refs.filter(!_.isTerminalCapability) - if !concrete.isEmpty then concrete - else - val notHidden = refs -- refs.flatMap(_.hiddenElems) - if !notHidden.isEmpty then SimpleIdentitySet(notHidden.nth(0)) - else SimpleIdentitySet(refs.nth(0)) - /** The overlap of two footprint sets F1 and F2. This contains all exclusive references `r` * such that one of the following is true: * 1. @@ -298,25 +302,35 @@ object SepCheck: common(refs, other) ++ common(other, refs) end overlapWith - /** The non-maximal elements hidden directly or indirectly by a maximal + /** Reduce a non-empty footprint set to + * 1. all its non-terminial capabilities if that set is nonempty, or + * 2. all its non-hidden capabilities if that set is nonempty, or + * 3. the set itself if it consists only of hidden terminal capabilities. + */ + def reduced(using Context): Refs = + assert(!refs.isEmpty) + val concrete = refs.nonPeaks + if !concrete.isEmpty then concrete + else + val notHidden = refs -- refs.flatMap(_.hiddenSet) + if !notHidden.isEmpty then notHidden + else refs + + /** The non-terminal elements hidden directly or indirectly by a terminal * capability in `refs`. E g. if `R = {x, >}` then * its hidden set is `{y, z}`. */ - private def hiddenSet(using Context): Refs = + private def transHiddenSet(using Context): Refs = val seen: util.EqHashSet[Capability] = new util.EqHashSet - def hiddenByElem(elem: Capability): Refs = elem match - case elem: FreshCap => elem.hiddenSet.elems ++ recur(elem.hiddenSet.elems) - case Restricted(elem1, cls) => hiddenByElem(elem1).map(_.restrict(cls)) - case ReadOnly(elem1) => hiddenByElem(elem1).map(_.readOnly) - case _ => emptyRefs - def recur(refs: Refs): Refs = (emptyRefs /: refs): (elems, elem) => - if seen.add(elem) then elems ++ hiddenByElem(elem) else elems + if seen.add(elem) + then elems ++ elem.computeHiddenSet(refs => refs ++ recur(refs)) + else elems recur(refs) - end hiddenSet + end transHiddenSet /** Subtract all elements that are covered by some element in `others` from this set. */ private def deduct(others: Refs)(using Context): Refs = @@ -332,8 +346,8 @@ object SepCheck: end extension extension (ref: Capability) - def peaks(using Context): Refs = SimpleIdentitySet(ref).peaks - def exposedPeaks(using Context): Refs = SimpleIdentitySet(ref).exposedPeaks + def directPeaks (using Context): Refs = + SimpleIdentitySet(ref).directFootprint.peaks class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser: import checker.* @@ -382,14 +396,14 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser: i"$other" def overlapStr(hiddenSet: Refs, clashSet: Refs)(using Context): String = - val hiddenFootprint = hiddenSet.footprint - val clashFootprint = clashSet.footprint + val hiddenFootprint = hiddenSet.oldFootprint + val clashFootprint = clashSet.oldFootprint // The overlap of footprints, or, of this empty the set of shared peaks. // We prefer footprint overlap since it tends to be more informative. val overlap = hiddenFootprint.overlapWith(clashFootprint) if !overlap.isEmpty then i"${CaptureSet(overlap)}" else - val sharedPeaks = hiddenSet.peaks.sharedWith(clashSet.peaks) + val sharedPeaks = hiddenSet.transPeaks.sharedPeaks(clashSet.transPeaks) assert(!sharedPeaks.isEmpty, i"no overlap for $hiddenSet vs $clashSet") sharedPeaksStr(sharedPeaks) @@ -431,7 +445,7 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser: def clashTypeStr = if clashIdx == 0 && !isShowableMethod then "" // we already mentioned the type in `funStr` else i" with type ${clashing.nuType}" - val hiddenSet = formalCaptures(polyArg).hiddenSet + val hiddenSet = formalCaptures(polyArg).transHiddenSet val clashSet = deepCaptures(clashing) report.error( em"""Separation failure: argument of type ${polyArg.nuType} @@ -441,9 +455,9 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser: |Some of these overlap with the captures of the ${clashArgStr.trim}$clashTypeStr. | | Hidden set of current argument : ${CaptureSet(hiddenSet)} - | Hidden footprint of current argument : ${CaptureSet(hiddenSet.footprint)} + | Hidden footprint of current argument : ${CaptureSet(hiddenSet.oldFootprint)} | Capture set of $clashArgStr : ${CaptureSet(clashSet)} - | Footprint set of $clashArgStr : ${CaptureSet(clashSet.footprint)} + | Footprint set of $clashArgStr : ${CaptureSet(clashSet.oldFootprint)} | The two sets overlap at : ${overlapStr(hiddenSet, clashSet)}""", polyArg.srcPos) @@ -526,7 +540,7 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser: val (qual, fnCaptures) = methPart(fn) match case Select(qual, _) => (qual, qual.nuType.captureSet) case _ => (fn, CaptureSet.empty) - var currentPeaks = PeaksPair(fnCaptures.elems.peaks, emptyRefs) + var currentPeaks = PeaksPair(fnCaptures.elems.transPeaks, emptyRefs) val partsWithPeaks = mutable.ListBuffer[(Tree, PeaksPair)]() += (qual -> currentPeaks) capt.println( @@ -540,20 +554,20 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser: for arg <- args do val argPeaks = PeaksPair( - spanCaptures(arg).peaks, - if arg.needsSepCheck then formalCaptures(arg).hiddenSet.peaks else emptyRefs) + spanCaptures(arg).transPeaks, + if arg.needsSepCheck then formalCaptures(arg).transHiddenSet.transPeaks else emptyRefs) val argDeps = deps(arg) def clashingPart(argPeaks: Refs, selector: PeaksPair => Refs): Tree = partsWithPeaks.find: (prev, prevPeaks) => !argDeps.contains(prev) - && !selector(prevPeaks).sharedWith(argPeaks).isEmpty + && !selector(prevPeaks).sharedPeaks(argPeaks).isEmpty match case Some(prev, _) => prev case None => EmptyTree // 1. test argPeaks.actual against previously captured hidden sets - if !argPeaks.actual.sharedWith(currentPeaks.hidden).isEmpty then + if !argPeaks.actual.sharedPeaks(currentPeaks.hidden).isEmpty then val clashing = clashingPart(argPeaks.actual, _.hidden) if !clashing.isEmpty then sepApplyError(fn, parts, clashing, arg) @@ -564,7 +578,7 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser: //println(i"testing $arg, formal = ${arg.formalType}, peaks = ${argPeaks.actual}/${argPeaks.hidden} against ${currentPeaks.actual}") checkType(arg.formalType, arg.srcPos, TypeRole.Argument(arg)) // 2. test argPeaks.hidden against previously captured actuals - if !argPeaks.hidden.sharedWith(currentPeaks.actual).isEmpty then + if !argPeaks.hidden.sharedPeaks(currentPeaks.actual).isEmpty then val clashing = clashingPart(argPeaks.hidden, _.actual) if !clashing.isEmpty then if !reported.contains(clashing) then @@ -581,7 +595,7 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser: if !resultPeaks.isEmpty then lazy val partPeaks = partsWithPeaks.toMap for arg <- args do - if arg.needsSepCheck && !partPeaks(arg).hidden.sharedWith(resultPeaks).isEmpty then + if arg.needsSepCheck && !partPeaks(arg).hidden.sharedPeaks(resultPeaks).isEmpty then sepApplyError(fn, parts, arg, app) end checkApply @@ -593,15 +607,15 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser: val used = tree.markedFree.elems if !used.isEmpty then capt.println(i"check use $tree: $used") - val usedPeaks = used.peaks - val overlap = defsShadow.peaks.sharedWith(usedPeaks) - if !defsShadow.peaks.sharedWith(usedPeaks).isEmpty then + val usedPeaks = used.transPeaks + val overlap = defsShadow.transPeaks.sharedPeaks(usedPeaks) + if !defsShadow.transPeaks.sharedPeaks(usedPeaks).isEmpty then val sym = tree.symbol def findClashing(prevDefs: List[DefInfo]): Option[DefInfo] = prevDefs match case prevDef :: prevDefs1 => if prevDef.symbol == sym then Some(prevDef) - else if !prevDef.hiddenPeaks.sharedWith(usedPeaks).isEmpty then Some(prevDef) + else if !prevDef.hiddenPeaks.sharedPeaks(usedPeaks).isEmpty then Some(prevDef) else findClashing(prevDefs1) case Nil => None @@ -616,7 +630,7 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser: for ref <- used do val pos = consumed.clashing(ref) if pos != null then - // println(i"consumed so far ${consumed.refs.toList} with peaks ${consumed.exposedPeaks.toList}, used = $used, exposed = ${ref.exposedPeaks}") + // println(i"consumed so far ${consumed.refs.toList} with peaks ${consumed.directPeaks .toList}, used = $used, exposed = ${ref.directPeaks }") consumeError(ref, pos, tree.srcPos) end checkUse @@ -636,7 +650,7 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser: * which one applies is determined by the role parameter. * * This entails the following checks: - * - The reference must be defined in the same as method or class as + * - The reference must be defined in the same method or class as * the access. * - If the reference is to a term parameter, that parameter must be * marked as consume as well. @@ -647,7 +661,7 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser: * As a side effect, add all checked references with the given position `pos` * to the global `consumed` map. * - * @param refsToCheck the referencves to check + * @param refsToCheck the references to check * @param tpe the type containing those references * @param role the role in which the type apears * @param descr a textual description of the type and its relationship with the checked reference @@ -656,10 +670,10 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser: def checkConsumedRefs(refsToCheck: Refs, tpe: Type, role: TypeRole, descr: => String, pos: SrcPos)(using Context) = val badParams = mutable.ListBuffer[Symbol]() def currentOwner = role.dclSym.orElse(ctx.owner) - for hiddenRef <- refsToCheck.deductSymRefs(role.dclSym).deduct(explicitRefs(tpe)) do + for hiddenRef <- refsToCheck.deduct(explicitRefs(tpe)) do if !hiddenRef.isKnownClassifiedAs(defn.Caps_SharedCapability) then hiddenRef.pathRoot match - case ref: TermRef => + case ref: TermRef if ref.symbol != role.dclSym => val refSym = ref.symbol if currentOwner.enclosingMethodOrClass.isProperlyContainedIn(refSym.maybeOwner.enclosingMethodOrClass) then report.error(em"""Separation failure: $descr non-local $refSym""", pos) @@ -721,9 +735,9 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser: def sepTypeError(parts: List[Type], genPart: Type, otherPart: Type): Unit = val captured = genPart.deepCaptureSet.elems - val hiddenSet = captured.hiddenSet.pruned + val hiddenSet = captured.transHiddenSet.pruned val clashSet = otherPart.deepCaptureSet.elems - val deepClashSet = (clashSet.footprint ++ clashSet.hiddenSet).pruned + val deepClashSet = (clashSet.oldFootprint ++ clashSet.transHiddenSet).pruned report.error( em"""Separation failure in ${role.description} $tpe. |One part, $genPart, hides capabilities ${CaptureSet(hiddenSet)}. @@ -741,9 +755,9 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser: for part <- parts do val captured = part.deepCaptureSet.elems.pruned - val hidden = captured.hiddenSet.pruned + val hidden = captured.transHiddenSet.pruned val actual = captured ++ hidden - val partPeaks = PeaksPair(actual.peaks, hidden.peaks) + val partPeaks = PeaksPair(actual.transPeaks, hidden.transPeaks) /* println(i"""check parts $parts |current = ${currentPeaks.actual}/${currentPeaks.hidden} @@ -753,18 +767,18 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser: def clashingPart(argPeaks: Refs, selector: PeaksPair => Refs): Type = partsWithPeaks.find: (prev, prevPeaks) => - !selector(prevPeaks).sharedWith(argPeaks).isEmpty + !selector(prevPeaks).sharedPeaks(argPeaks).isEmpty match case Some(prev, _) => prev case None => NoType - if !partPeaks.actual.sharedWith(currentPeaks.hidden).isEmpty then + if !partPeaks.actual.sharedPeaks(currentPeaks.hidden).isEmpty then //println(i"CLASH ${partPeaks.actual} with ${currentPeaks.hidden}") val clashing = clashingPart(partPeaks.actual, _.hidden) //println(i"CLASH ${partPeaks.actual} with ${currentPeaks.hidden}") if clashing.exists then sepTypeError(parts, clashing, part) - if !partPeaks.hidden.sharedWith(currentPeaks.actual).isEmpty then + if !partPeaks.hidden.sharedPeaks(currentPeaks.actual).isEmpty then val clashing = clashingPart(partPeaks.hidden, _.actual) if clashing.exists then sepTypeError(parts, part, clashing) @@ -826,11 +840,11 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser: // "see through them" when we look at hidden sets. then val refs = tpe.deepCaptureSet.elems - val toCheck = refs.hiddenSet.footprint.deduct(refs.footprint) + val toCheck = refs.transHiddenSet.oldFootprint.deduct(refs.oldFootprint) checkConsumedRefs(toCheck, tpe, role, i"${role.description} $tpe hides", pos) case TypeRole.Argument(arg) => if tpe.hasAnnotation(defn.ConsumeAnnot) then - val capts = spanCaptures(arg).footprint + val capts = spanCaptures(arg).oldFootprint checkConsumedRefs(capts, tpe, role, i"argument to consume parameter with type ${arg.nuType} refers to", pos) case _ => @@ -919,7 +933,7 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser: val resultType = mtpe.finalResultType val resultCaptures = (resultArgCaptures(resultType) ++ resultType.deepCaptureSet.elems).filter(!isLocalRef(_)) - val resultPeaks = resultCaptures.peaks + val resultPeaks = resultCaptures.transPeaks capt.println(i"deps for $app = ${deps.toList}") (deps, resultPeaks) @@ -945,7 +959,7 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser: def pushDef(tree: ValOrDefDef, hiddenByDef: Refs)(using Context): Unit = defsShadow ++= hiddenByDef - previousDefs = DefInfo(tree, tree.symbol, hiddenByDef, hiddenByDef.peaks) :: previousDefs + previousDefs = DefInfo(tree, tree.symbol, hiddenByDef, hiddenByDef.transPeaks) :: previousDefs /** Check (result-) type of `tree` for separation conditions using `checkType`. * Excluded are parameters and definitions that have an =unsafeAssumeSeparate @@ -955,8 +969,8 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser: def checkValOrDefDef(tree: ValOrDefDef)(using Context): Unit = if !tree.symbol.isOneOf(TermParamOrAccessor) && !isUnsafeAssumeSeparate(tree.rhs) then checkType(tree.tpt, tree.symbol) - capt.println(i"sep check def ${tree.symbol}: ${tree.tpt} with ${spanCaptures(tree.tpt).hiddenSet.footprint}") - pushDef(tree, spanCaptures(tree.tpt).hiddenSet.deductSymRefs(tree.symbol)) + capt.println(i"sep check def ${tree.symbol}: ${tree.tpt} with ${spanCaptures(tree.tpt).transHiddenSet.oldFootprint}") + pushDef(tree, spanCaptures(tree.tpt).transHiddenSet.deductSymRefs(tree.symbol)) def inSection[T](op: => T)(using Context): T = val savedDefsShadow = defsShadow @@ -992,7 +1006,7 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser: case tree @ Select(qual, _) if tree.symbol.is(Method) && tree.symbol.isConsumeParam => traverseChildren(tree) checkConsumedRefs( - spanCaptures(qual).footprint, qual.nuType, + spanCaptures(qual).oldFootprint, qual.nuType, TypeRole.Qualifier(qual, tree.symbol), i"call prefix of consume ${tree.symbol} refers to", qual.srcPos) case tree: GenericApply => From 7a7f7477a60f504c424e49f2eb7c20e69f80b6c8 Mon Sep 17 00:00:00 2001 From: odersky Date: Wed, 1 Oct 2025 20:21:28 +0200 Subject: [PATCH 05/14] Normalize fresh caps in result types Ensure that capset variables in types of vals and result types of non-anonymous functions contain only a single FreshCap, and furthermore that that FreshCap has as origin InDecl(owner), where owner is the val or def for which the type is defined. --- .../src/dotty/tools/dotc/cc/Capability.scala | 2 +- .../src/dotty/tools/dotc/cc/CaptureSet.scala | 73 ++++++++++++++++--- .../dotty/tools/dotc/cc/CheckCaptures.scala | 5 +- compiler/src/dotty/tools/dotc/cc/Setup.scala | 23 +++--- tests/neg-custom-args/captures/cc-this5.check | 5 -- tests/neg-custom-args/captures/cc-this5.scala | 2 +- tests/neg-custom-args/captures/i23726.check | 6 +- .../captures/reference-cc.check | 5 -- .../captures/reference-cc.scala | 2 +- .../captures/scope-extrude-mut.check | 16 ++-- .../captures/sep-counter.check | 15 ++-- tests/new/test.scala | 10 +-- .../captures/drop-refinement.scala | 18 +++++ 13 files changed, 120 insertions(+), 62 deletions(-) create mode 100644 tests/pos-custom-args/captures/drop-refinement.scala diff --git a/compiler/src/dotty/tools/dotc/cc/Capability.scala b/compiler/src/dotty/tools/dotc/cc/Capability.scala index 27294d42fd54..bb2beda531b2 100644 --- a/compiler/src/dotty/tools/dotc/cc/Capability.scala +++ b/compiler/src/dotty/tools/dotc/cc/Capability.scala @@ -147,7 +147,7 @@ object Capabilities: * @param origin an indication where and why the FreshCap was created, used * for diagnostics */ - case class FreshCap private (owner: Symbol, origin: Origin)(using @constructorOnly ctx: Context) extends RootCapability: + case class FreshCap (owner: Symbol, origin: Origin)(using @constructorOnly ctx: Context) extends RootCapability: val hiddenSet = CaptureSet.HiddenSet(owner, this: @unchecked) // fails initialization check without the @unchecked diff --git a/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala b/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala index c6c197da6723..e2e0dc33bae2 100644 --- a/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala +++ b/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala @@ -777,7 +777,7 @@ object CaptureSet: assert(elem.subsumes(elem1), i"Skipped map ${tm.getClass} maps newly added $elem to $elem1 in $this") - protected def includeElem(elem: Capability)(using Context): Unit = + protected def includeElem(elem: Capability)(using Context, VarState): Unit = if !elems.contains(elem) then if debugVars && id == debugTarget then println(i"###INCLUDE $elem in $this") @@ -803,7 +803,10 @@ object CaptureSet: // id == 108 then assert(false, i"trying to add $elem to $this") assert(elem.isWellformed, elem) assert(!this.isInstanceOf[HiddenSet] || summon[VarState].isSeparating, summon[VarState]) - includeElem(elem) + try includeElem(elem) + catch case ex: AssertionError => + println(i"error for incl $elem in $this, ${summon[VarState].toString}") + throw ex if isBadRoot(elem) then rootAddedHandler() val normElem = if isMaybeSet then elem else elem.stripMaybe @@ -947,16 +950,66 @@ object CaptureSet: override def toString = s"Var$id$elems" end Var - /** Variables that represent refinements of class parameters can have the universal - * capture set, since they represent only what is the result of the constructor. - * Test case: Without that tweak, logger.scala would not compile. - */ - class RefiningVar(owner: Symbol)(using Context) extends Var(owner): - override def disallowBadRoots(upto: Symbol)(handler: () => Context ?=> Unit)(using Context) = this + inline val strictFreshLevels = true /** Variables created in types of inferred type trees */ - class ProperVar(override val owner: Symbol, initialElems: Refs, nestedOK: Boolean)(using /*@constructorOnly*/ ictx: Context) - extends Var(owner, initialElems, nestedOK) + class ProperVar(override val owner: Symbol, initialElems: Refs = emptyRefs, nestedOK: Boolean = true, isRefining: Boolean)(using /*@constructorOnly*/ ictx: Context) + extends Var(owner, initialElems, nestedOK): + + /** Make sure that capset variables in types of vals and result types of + * non-anonymous functions contain only a single FreshCap, and furthermore + * that that FreshCap has as origin InDecl(owner), where owner is the val + * or def for which the type is defined. + * Note: This currently does not apply to classified or read-only fresh caps. + */ + override def includeElem(elem: Capability)(using ctx: Context, vs: VarState): Unit = elem match + case elem: FreshCap + if !nestedOK + && !elems.contains(elem) + && !owner.isAnonymousFunction + && ccConfig.newScheme => + def fail = i"attempting to add $elem to $this" + def hideIn(fc: FreshCap): Unit = + assert(elem.tryClassifyAs(fc.hiddenSet.classifier), fail) + if strictFreshLevels && !isRefining then + // If a variable is added by addCaptureRefinements in a synthetic + // refinement of a class type, don't do level checking. The problem is + // that the variable might be matched against a type that does not have + // a refinement, in which case FreshCaps of the class definition would + // leak out in the corresponding places. This will fail level checking. + // The disallowBadRoots override below has a similar reason. + // TODO: We should instead mark the variable as impossible to instantiate + // and drop the refinement later in the inferred type. + // Test case is drop-refinement.scala. + assert(fc.acceptsLevelOf(elem), + i"level failure, cannot add $elem with ${elem.levelOwner} to $owner / $getClass / $fail") + fc.hiddenSet.add(elem) + val isSubsumed = (false /: elems): (isSubsumed, prev) => + prev match + case prev: FreshCap => + hideIn(prev) + true + case _ => isSubsumed + if !isSubsumed then + if elem.origin != Origin.InDecl(owner) || elem.hiddenSet.isConst then + val fc = new FreshCap(owner, Origin.InDecl(owner)) + assert(fc.tryClassifyAs(elem.hiddenSet.classifier), fail) + hideIn(fc) + super.includeElem(fc) + else + super.includeElem(elem) + case _ => + super.includeElem(elem) + + /** Variables that represent refinements of class parameters can have the universal + * capture set, since they represent only what is the result of the constructor. + * Test case: Without that tweak, logger.scala would not compile. + */ + override def disallowBadRoots(upto: Symbol)(handler: () => Context ?=> Unit)(using Context) = + if isRefining then this + else super.disallowBadRoots(upto)(handler) + + end ProperVar /** A variable that is derived from some other variable via a map or filter. */ abstract class DerivedVar(owner: Symbol, initialElems: Refs)(using @constructorOnly ctx: Context) diff --git a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala index 42e7f67de460..d5cc2811f264 100644 --- a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala +++ b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala @@ -1376,7 +1376,10 @@ class CheckCaptures extends Recheck, SymTransformer: * where local capture roots are instantiated to root variables. */ override def checkConformsExpr(actual: Type, expected: Type, tree: Tree, addenda: Addenda)(using Context): Type = - testAdapted(actual, expected, tree, addenda)(err.typeMismatch) + try testAdapted(actual, expected, tree, addenda)(err.typeMismatch) + catch case ex: AssertionError => + println(i"error while checking $tree: $actual against $expected") + throw ex @annotation.tailrec private def findImpureUpperBound(tp: Type)(using Context): Type = tp match diff --git a/compiler/src/dotty/tools/dotc/cc/Setup.scala b/compiler/src/dotty/tools/dotc/cc/Setup.scala index f44b44bd7df7..d1b0f0c5cc72 100644 --- a/compiler/src/dotty/tools/dotc/cc/Setup.scala +++ b/compiler/src/dotty/tools/dotc/cc/Setup.scala @@ -252,7 +252,7 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI: * Polytype bounds are only cleaned using step 1, but not otherwise transformed. */ private def transformInferredType(tp: Type)(using Context): Type = - def mapInferred(refine: Boolean): TypeMap = new TypeMap with SetupTypeMap: + def mapInferred(inCaptureRefinement: Boolean): TypeMap = new TypeMap with SetupTypeMap: override def toString = "map inferred" var refiningNames: Set[Name] = Set() @@ -262,23 +262,23 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI: * where CV_1, ..., CV_n are fresh capture set variables. */ def addCaptureRefinements(tp: Type): Type = tp match - case _: TypeRef | _: AppliedType if refine && tp.typeParams.isEmpty => + case _: TypeRef | _: AppliedType if !inCaptureRefinement && tp.typeParams.isEmpty => tp.typeSymbol match case cls: ClassSymbol if !defn.isFunctionClass(cls) && cls.is(CaptureChecked) => - cls.paramGetters.foldLeft(tp) { (core, getter) => + cls.paramGetters.foldLeft(tp): (core, getter) => if atPhase(thisPhase.next)(getter.hasTrackedParts) && getter.isRefiningParamAccessor && !refiningNames.contains(getter.name) // Don't add a refinement if we have already an explicit one for the same name then val getterType = - mapInferred(refine = false)(tp.memberInfo(getter)).strippedDealias + mapInferred(inCaptureRefinement = true)(tp.memberInfo(getter)).strippedDealias RefinedType(core, getter.name, - CapturingType(getterType, new CaptureSet.RefiningVar(ctx.owner))) + CapturingType(getterType, + CaptureSet.ProperVar(ctx.owner, isRefining = true))) .showing(i"add capture refinement $tp --> $result", capt) else core - } case _ => tp case _ => tp @@ -302,11 +302,12 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI: mapFollowingAliases(tp) addVar( addCaptureRefinements(normalizeCaptures(normalizeFunctions(tp1, tp))), - ctx.owner) + ctx.owner, + isRefining = inCaptureRefinement) end mapInferred try - val tp1 = mapInferred(refine = true)(tp) + val tp1 = mapInferred(inCaptureRefinement = false)(tp) val tp2 = toResultInResults(NoSymbol, _ => assert(false))(tp1) if tp2 ne tp then capt.println(i"expanded inferred in ${ctx.owner}: $tp --> $tp1 --> $tp2") tp2 @@ -685,7 +686,7 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI: // Infer the self type for the rest, which is all classes without explicit // self types (to which we also add nested module classes), provided they are // neither pure, nor are publicily extensible with an unconstrained self type. - val cs = CaptureSet.ProperVar(cls, CaptureSet.emptyRefs, nestedOK = false) + val cs = CaptureSet.ProperVar(cls, CaptureSet.emptyRefs, nestedOK = false, isRefining = false) if cls.derivesFrom(defn.Caps_Capability) then // If cls is a capability class, we need to add a fresh readonly capability to // ensure we cannot treat the class as pure. @@ -851,8 +852,8 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI: else maybeAdd(tp, tp) /** Add a capture set variable to `tp` if necessary. */ - private def addVar(tp: Type, owner: Symbol)(using Context): Type = - decorate(tp, CaptureSet.ProperVar(owner, _, nestedOK = !ctx.mode.is(Mode.CCPreciseOwner))) + private def addVar(tp: Type, owner: Symbol, isRefining: Boolean)(using Context): Type = + decorate(tp, CaptureSet.ProperVar(owner, _, nestedOK = !ctx.mode.is(Mode.CCPreciseOwner), isRefining)) /** A map that adds capture sets at all contra- and invariant positions * in a type where a capture set would be needed. This is used to make types diff --git a/tests/neg-custom-args/captures/cc-this5.check b/tests/neg-custom-args/captures/cc-this5.check index 1a291edd15e7..f6e63544ab95 100644 --- a/tests/neg-custom-args/captures/cc-this5.check +++ b/tests/neg-custom-args/captures/cc-this5.check @@ -1,8 +1,3 @@ --- Error: tests/neg-custom-args/captures/cc-this5.scala:16:20 ---------------------------------------------------------- -16 | def f = println(c) // error - | ^ - | reference (c : Cap) is not included in the allowed capture set {} - | of the enclosing class A -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/cc-this5.scala:21:15 ------------------------------------- 21 | val x: A = this // error | ^^^^ diff --git a/tests/neg-custom-args/captures/cc-this5.scala b/tests/neg-custom-args/captures/cc-this5.scala index 811b1e1f8922..8d74f27bc25c 100644 --- a/tests/neg-custom-args/captures/cc-this5.scala +++ b/tests/neg-custom-args/captures/cc-this5.scala @@ -13,7 +13,7 @@ def foo(c: Cap) = def test(c: Cap) = class A: val x: A = this - def f = println(c) // error + def f = println(c) def test2(c: Cap) = class A: diff --git a/tests/neg-custom-args/captures/i23726.check b/tests/neg-custom-args/captures/i23726.check index 8c8ac94a61e0..1e359316a84a 100644 --- a/tests/neg-custom-args/captures/i23726.check +++ b/tests/neg-custom-args/captures/i23726.check @@ -13,7 +13,7 @@ | Footprint set of function result : {a} | The two sets overlap at : {a} | - |where: ^ refers to a fresh root capability classified as Mutable created in value a when constructing mutable Ref + |where: ^ refers to a fresh root capability classified as Mutable in the type of value a | ^² refers to a fresh root capability classified as Mutable created in method test1 when checking argument to parameter x of method apply -- Error: tests/neg-custom-args/captures/i23726.scala:15:5 ------------------------------------------------------------- 15 | f3(b) // error @@ -30,7 +30,7 @@ | Footprint set of function result : {op, b} | The two sets overlap at : {b} | - |where: ^ refers to a fresh root capability classified as Mutable created in value b when constructing mutable Ref + |where: ^ refers to a fresh root capability classified as Mutable in the type of value b | ^² refers to a fresh root capability classified as Mutable created in method test1 when checking argument to parameter x of method apply -- Error: tests/neg-custom-args/captures/i23726.scala:23:5 ------------------------------------------------------------- 23 | f7(a) // error @@ -47,5 +47,5 @@ | Footprint set of function prefix : {f7*, a, b} | The two sets overlap at : {a} | - |where: ^ refers to a fresh root capability classified as Mutable created in value a when constructing mutable Ref + |where: ^ refers to a fresh root capability classified as Mutable in the type of value a | ^² refers to a fresh root capability classified as Mutable created in method test1 when checking argument to parameter x of method apply diff --git a/tests/neg-custom-args/captures/reference-cc.check b/tests/neg-custom-args/captures/reference-cc.check index d557a37039b8..be30a566d0cc 100644 --- a/tests/neg-custom-args/captures/reference-cc.check +++ b/tests/neg-custom-args/captures/reference-cc.check @@ -1,8 +1,3 @@ --- Error: tests/neg-custom-args/captures/reference-cc.scala:42:20 ------------------------------------------------------ -42 | def f = println(c) // error - | ^ - | reference (c : Cap) is not included in the allowed capture set {} - | of the enclosing class A -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/reference-cc.scala:44:29 --------------------------------- 44 | val later = usingLogFile { file => () => file.write(0) } // error | ^^^^^^^^^^^^^^^^^^^^^^^^^^^ diff --git a/tests/neg-custom-args/captures/reference-cc.scala b/tests/neg-custom-args/captures/reference-cc.scala index c94ad207bb04..8426cd0ce303 100644 --- a/tests/neg-custom-args/captures/reference-cc.scala +++ b/tests/neg-custom-args/captures/reference-cc.scala @@ -39,7 +39,7 @@ class Cap extends caps.SharedCapability def test(c: Cap) = class A: val x: A = this - def f = println(c) // error + def f = println(c) val later = usingLogFile { file => () => file.write(0) } // error later() // crash diff --git a/tests/neg-custom-args/captures/scope-extrude-mut.check b/tests/neg-custom-args/captures/scope-extrude-mut.check index 9835c004054d..0d79f4f66fbc 100644 --- a/tests/neg-custom-args/captures/scope-extrude-mut.check +++ b/tests/neg-custom-args/captures/scope-extrude-mut.check @@ -1,15 +1,15 @@ -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/scope-extrude-mut.scala:9:8 ------------------------------ 9 | a = a1 // error | ^^ - |Found: (a1 : A^) - |Required: A^² + | Found: (a1 : A^) + | Required: A^² | - |Note that capability cap is not included in capture set {cap²} - |because cap in method b is not visible from cap² in variable a. + | Note that capability cap is not included in capture set {cap²} + | because cap in method b is not visible from cap² in variable a. | - |where: ^ refers to a fresh root capability classified as Mutable created in value a1 when constructing mutable A - | ^² refers to a fresh root capability classified as Mutable in the type of variable a - | cap is a fresh root capability classified as Mutable created in value a1 when constructing mutable A - | cap² is a fresh root capability classified as Mutable in the type of variable a + | where: ^ refers to a fresh root capability classified as Mutable in the type of value a1 + | ^² refers to a fresh root capability classified as Mutable in the type of variable a + | cap is a fresh root capability classified as Mutable in the type of value a1 + | cap² is a fresh root capability classified as Mutable in the type of variable a | | longer explanation available when compiling with `-explain` diff --git a/tests/neg-custom-args/captures/sep-counter.check b/tests/neg-custom-args/captures/sep-counter.check index c9d2b1895aee..a42b405fd727 100644 --- a/tests/neg-custom-args/captures/sep-counter.check +++ b/tests/neg-custom-args/captures/sep-counter.check @@ -1,11 +1,12 @@ -- Error: tests/neg-custom-args/captures/sep-counter.scala:12:19 ------------------------------------------------------- 12 | def mkCounter(): Pair[Ref^, Ref^] = // error | ^^^^^^^^^^^^^^^^ - | Separation failure in method mkCounter's result type Pair[Ref^, Ref^²]. - | One part, Ref^, hides capabilities {c, cap}. - | Another part, Ref^², captures capabilities {c, cap}. - | The two sets overlap at {c}. + |Separation failure in method mkCounter's result type Pair[Ref^, Ref^²]. + |One part, Ref^, hides capabilities {c, cap, cap²}. + |Another part, Ref^², captures capabilities {c, cap, cap²}. + |The two sets overlap at {c}. | - | where: ^ refers to a fresh root capability classified as Mutable in the result type of method mkCounter - | ^² refers to a fresh root capability classified as Mutable in the result type of method mkCounter - | cap is a fresh root capability classified as Mutable created in value c when constructing mutable Ref + |where: ^ refers to a fresh root capability classified as Mutable in the result type of method mkCounter + | ^² refers to a fresh root capability classified as Mutable in the result type of method mkCounter + | cap is a fresh root capability classified as Mutable in the type of value c + | cap² is a fresh root capability classified as Mutable created in value c when constructing mutable Ref diff --git a/tests/new/test.scala b/tests/new/test.scala index 632ef3493662..00174769a0f0 100644 --- a/tests/new/test.scala +++ b/tests/new/test.scala @@ -1,9 +1 @@ -object e: - def foldRL(f: Int => Int)(g: String => Int) = ??? - - -val xs = e.foldRL - : i => i + 1 - : s => s.length - - +object Test diff --git a/tests/pos-custom-args/captures/drop-refinement.scala b/tests/pos-custom-args/captures/drop-refinement.scala new file mode 100644 index 000000000000..f7e922b88012 --- /dev/null +++ b/tests/pos-custom-args/captures/drop-refinement.scala @@ -0,0 +1,18 @@ +import scala.annotation.unchecked.uncheckedVariance + +private final class ConcatIterator[+A](val from: Iterator[A @uncheckedVariance]^) { + self: ConcatIterator[A]^ => + def hasNext: Boolean = ??? + def next(): A = ??? + + def concat[B >: A](that: => IterableOnce[B]^): ConcatIterator[B]^{this, that} = { + val c = new ConcatIteratorCell[B](that, null).asInstanceOf[ConcatIteratorCell[A]] + // crashes without special exemption for isRefining in CaptureSet.ProperVar$includeElem. + this + } +} + +private final class ConcatIteratorCell[A](head: => IterableOnce[A]^, var tail: ConcatIteratorCell[A]^) { + def headIterator: Iterator[A]^{this} = head.iterator +} + From 403165e2ab9b82b25b34d6d30a388bc13fb97be7 Mon Sep 17 00:00:00 2001 From: odersky Date: Thu, 2 Oct 2025 10:42:44 +0200 Subject: [PATCH 06/14] Drop alias detection for HiddenSets That was needed only to order fresh caps to find the peak of peaks but we don't do that anymore. --- .../src/dotty/tools/dotc/cc/CaptureSet.scala | 60 ++----------------- 1 file changed, 5 insertions(+), 55 deletions(-) diff --git a/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala b/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala index e2e0dc33bae2..061c7c2b4fc8 100644 --- a/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala +++ b/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala @@ -1220,6 +1220,9 @@ object CaptureSet: */ class HiddenSet(initialOwner: Symbol, val owningCap: FreshCap)(using @constructorOnly ictx: Context) extends Var(initialOwner): + + // Updated by anchorCaps in CheckCaptures, but owner can be changed only + // if it was NoSymbol before. var givenOwner: Symbol = initialOwner override def owner = givenOwner @@ -1228,62 +1231,9 @@ object CaptureSet: description = i"of elements subsumed by a fresh cap in $initialOwner" - private def aliasRef: FreshCap | Null = - if myElems.size == 1 then - myElems.nth(0) match - case alias: FreshCap if deps.contains(alias.hiddenSet) => alias - case _ => null - else null - - private def aliasSet: HiddenSet = - if myElems.size == 1 then - myElems.nth(0) match - case alias: FreshCap if deps.contains(alias.hiddenSet) => alias.hiddenSet - case _ => this - else this - - def superCaps: List[FreshCap] = - deps.toList.map(_.asInstanceOf[HiddenSet].owningCap) - - override def elems: Refs = - val al = aliasSet - if al eq this then super.elems else al.elems - - override def elems_=(refs: Refs) = - val al = aliasSet - if al eq this then super.elems_=(refs) else al.elems_=(refs) - - /** Add element to hidden set. Also add it to all supersets (as indicated by - * deps of this set). Follow aliases on both hidden set and added element - * before adding. If the added element is also a Fresh instance with - * hidden set H which is a superset of this set, then make this set an - * alias of H. - */ + /** Add element to hidden set. */ def add(elem: Capability)(using ctx: Context, vs: VarState): Unit = - val alias = aliasSet - if alias ne this then alias.add(elem) - else - def addToElems() = - assert(!isConst) - includeElem(elem) - deps.foreach: dep => - assert(dep != this) - vs.addHidden(dep.asInstanceOf[HiddenSet], elem) - elem match - case elem: FreshCap => - if this ne elem.hiddenSet then - val alias = elem.hiddenSet.aliasRef - if alias != null then - add(alias) - else if deps.contains(elem.hiddenSet) then // make this an alias of elem - capt.println(i"Alias $this to ${elem.hiddenSet}") - elems = SimpleIdentitySet(elem) - deps = SimpleIdentitySet(elem.hiddenSet) - else - addToElems() - elem.hiddenSet.includeDep(this) - case _ => - addToElems() + includeElem(elem) /** Apply function `f` to `elems` while setting `elems` to empty for the * duration. This is used to escape infinite recursions if two Freshs From 5e4fed2d4143e124fb84ac4a2127545007d9c968 Mon Sep 17 00:00:00 2001 From: odersky Date: Thu, 2 Oct 2025 11:40:39 +0200 Subject: [PATCH 07/14] Extends "covers" between capability to classified capabilities Classifiers are ignored in covers. --- .../src/dotty/tools/dotc/cc/Capability.scala | 8 ++- .../src/dotty/tools/dotc/cc/SepCheck.scala | 50 ++++++------------- 2 files changed, 21 insertions(+), 37 deletions(-) diff --git a/compiler/src/dotty/tools/dotc/cc/Capability.scala b/compiler/src/dotty/tools/dotc/cc/Capability.scala index bb2beda531b2..8c6ff1e09235 100644 --- a/compiler/src/dotty/tools/dotc/cc/Capability.scala +++ b/compiler/src/dotty/tools/dotc/cc/Capability.scala @@ -769,6 +769,7 @@ object Capabilities: * x covers x * x covers y ==> x covers y.f * x covers y ==> x* covers y*, x? covers y? + * x covers y ==> x.only[C] covers y, x covers y.only[C] * TODO what other clauses from subsumes do we need to port here? */ final def covers(y: Capability)(using Context): Boolean = @@ -784,10 +785,13 @@ object Capabilities: this match case Maybe(x1) => x1.covers(y1) case _ => false - case y: FreshCap => - y.hiddenSet.superCaps.exists(this.covers(_)) + case Restricted(y1, _) => + this.covers(y1) case _ => false + || this.match + case Restricted(x1, _) => x1.covers(y) + case _ => false def assumedContainsOf(x: TypeRef)(using Context): SimpleIdentitySet[Capability] = CaptureSet.assumedContains.getOrElse(x, SimpleIdentitySet.empty) diff --git a/compiler/src/dotty/tools/dotc/cc/SepCheck.scala b/compiler/src/dotty/tools/dotc/cc/SepCheck.scala index e20a382e9bad..111cee9f8b67 100644 --- a/compiler/src/dotty/tools/dotc/cc/SepCheck.scala +++ b/compiler/src/dotty/tools/dotc/cc/SepCheck.scala @@ -214,36 +214,16 @@ object SepCheck: private def directFootprint(using Context): Refs = computeFootprint(followHidden = false) - /** The hidden footprint of a set of capabilities `refs` is the closure + /** The complete footprint of a set of capabilities `refs` is the closure * of `refs` under `_.captureSetOfInfo` and `_.hiddenElems`, dropping any shared terminal * capabilities. */ - private def hiddenFootprint(using Context): Refs = + private def completeFootprint(using Context): Refs = computeFootprint(followHidden = true) - /** Same as hiddenFootprint.peaks under new scheme. Was maximal elements before */ - private def transPeaks(using Context): Refs = - def recur(seen: Refs, acc: Refs, newElems: List[Capability]): Refs = trace(i"peaks $acc, $newElems = "): - newElems match - case newElem :: newElems1 => - if seen.contains(newElem) then - recur(seen, acc, newElems1) - else newElem.stripRestricted.stripReadOnly match - case elem: FreshCap if !elem.isKnownClassifiedAs(defn.Caps_SharedCapability) => - if elem.hiddenSet.deps.isEmpty then recur(seen + newElem, acc + newElem, newElems1) - else - val superCaps = - if newElem.isReadOnly then elem.hiddenSet.superCaps.map(_.readOnly) - else elem.hiddenSet.superCaps - recur(seen + newElem, acc, superCaps ++ newElems) - case _ => - if newElem.isTerminalCapability - //|| newElem.isInstanceOf[TypeRef | TypeParamRef] - then recur(seen + newElem, acc, newElems1) - else recur(seen + newElem, acc, newElem.captureSetOfInfo.dropEmpties().elems.toList ++ newElems1) - case Nil => acc - if ccConfig.newScheme then hiddenFootprint.peaks - else recur(emptyRefs, emptyRefs, refs.toList) + /** Same as completeFootprint.peaks under new scheme. Was maximal elements before */ + private def allPeaks(using Context): Refs = + completeFootprint.peaks /** The shared elements between the peak sets `refs` and `other`. * These are the core capabilities and fresh capabilities that appear @@ -403,7 +383,7 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser: val overlap = hiddenFootprint.overlapWith(clashFootprint) if !overlap.isEmpty then i"${CaptureSet(overlap)}" else - val sharedPeaks = hiddenSet.transPeaks.sharedPeaks(clashSet.transPeaks) + val sharedPeaks = hiddenSet.allPeaks.sharedPeaks(clashSet.allPeaks) assert(!sharedPeaks.isEmpty, i"no overlap for $hiddenSet vs $clashSet") sharedPeaksStr(sharedPeaks) @@ -540,7 +520,7 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser: val (qual, fnCaptures) = methPart(fn) match case Select(qual, _) => (qual, qual.nuType.captureSet) case _ => (fn, CaptureSet.empty) - var currentPeaks = PeaksPair(fnCaptures.elems.transPeaks, emptyRefs) + var currentPeaks = PeaksPair(fnCaptures.elems.allPeaks, emptyRefs) val partsWithPeaks = mutable.ListBuffer[(Tree, PeaksPair)]() += (qual -> currentPeaks) capt.println( @@ -554,8 +534,8 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser: for arg <- args do val argPeaks = PeaksPair( - spanCaptures(arg).transPeaks, - if arg.needsSepCheck then formalCaptures(arg).transHiddenSet.transPeaks else emptyRefs) + spanCaptures(arg).allPeaks, + if arg.needsSepCheck then formalCaptures(arg).transHiddenSet.allPeaks else emptyRefs) val argDeps = deps(arg) def clashingPart(argPeaks: Refs, selector: PeaksPair => Refs): Tree = @@ -607,9 +587,9 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser: val used = tree.markedFree.elems if !used.isEmpty then capt.println(i"check use $tree: $used") - val usedPeaks = used.transPeaks - val overlap = defsShadow.transPeaks.sharedPeaks(usedPeaks) - if !defsShadow.transPeaks.sharedPeaks(usedPeaks).isEmpty then + val usedPeaks = used.allPeaks + val overlap = defsShadow.allPeaks.sharedPeaks(usedPeaks) + if !defsShadow.allPeaks.sharedPeaks(usedPeaks).isEmpty then val sym = tree.symbol def findClashing(prevDefs: List[DefInfo]): Option[DefInfo] = prevDefs match @@ -757,7 +737,7 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser: val captured = part.deepCaptureSet.elems.pruned val hidden = captured.transHiddenSet.pruned val actual = captured ++ hidden - val partPeaks = PeaksPair(actual.transPeaks, hidden.transPeaks) + val partPeaks = PeaksPair(actual.allPeaks, hidden.allPeaks) /* println(i"""check parts $parts |current = ${currentPeaks.actual}/${currentPeaks.hidden} @@ -933,7 +913,7 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser: val resultType = mtpe.finalResultType val resultCaptures = (resultArgCaptures(resultType) ++ resultType.deepCaptureSet.elems).filter(!isLocalRef(_)) - val resultPeaks = resultCaptures.transPeaks + val resultPeaks = resultCaptures.allPeaks capt.println(i"deps for $app = ${deps.toList}") (deps, resultPeaks) @@ -959,7 +939,7 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser: def pushDef(tree: ValOrDefDef, hiddenByDef: Refs)(using Context): Unit = defsShadow ++= hiddenByDef - previousDefs = DefInfo(tree, tree.symbol, hiddenByDef, hiddenByDef.transPeaks) :: previousDefs + previousDefs = DefInfo(tree, tree.symbol, hiddenByDef, hiddenByDef.allPeaks) :: previousDefs /** Check (result-) type of `tree` for separation conditions using `checkType`. * Excluded are parameters and definitions that have an =unsafeAssumeSeparate From d62d3d16de392eb6f3d9238a7d789e470b1658f5 Mon Sep 17 00:00:00 2001 From: odersky Date: Thu, 2 Oct 2025 11:44:09 +0200 Subject: [PATCH 08/14] Make footprint also include non-terminal capabilities --- compiler/src/dotty/tools/dotc/cc/SepCheck.scala | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/compiler/src/dotty/tools/dotc/cc/SepCheck.scala b/compiler/src/dotty/tools/dotc/cc/SepCheck.scala index 111cee9f8b67..20dae9354d38 100644 --- a/compiler/src/dotty/tools/dotc/cc/SepCheck.scala +++ b/compiler/src/dotty/tools/dotc/cc/SepCheck.scala @@ -203,7 +203,7 @@ object SepCheck: case _ if newElem.isTerminalCapability => recur(seen + newElem, acc, newElems1) case _ => - recur(seen + newElem, acc, newElem.captureSetOfInfo.dropEmpties().elems.toList ++ newElems1) + recur(seen + newElem, acc + newElem, newElem.captureSetOfInfo.dropEmpties().elems.toList ++ newElems1) case Nil => acc recur(emptyRefs, emptyRefs, refs.toList) From cba62c9539109dba4c01f2beeb8e055a26d13d5a Mon Sep 17 00:00:00 2001 From: odersky Date: Thu, 2 Oct 2025 11:45:32 +0200 Subject: [PATCH 09/14] Drop old footprint computation --- .../src/dotty/tools/dotc/cc/SepCheck.scala | 21 +++++++++++-------- tests/neg-custom-args/captures/lazyref.check | 2 +- 2 files changed, 13 insertions(+), 10 deletions(-) diff --git a/compiler/src/dotty/tools/dotc/cc/SepCheck.scala b/compiler/src/dotty/tools/dotc/cc/SepCheck.scala index 20dae9354d38..dc5ec8c5ecb5 100644 --- a/compiler/src/dotty/tools/dotc/cc/SepCheck.scala +++ b/compiler/src/dotty/tools/dotc/cc/SepCheck.scala @@ -175,15 +175,18 @@ object SepCheck: * 2. if `f in F` then the footprint of `f`'s info is also in `F`. */ private def oldFootprint(using Context): Refs = - def retain(ref: Capability) = !ref.isTerminalCapability - def recur(elems: Refs, newElems: List[Capability]): Refs = newElems match - case newElem :: newElems1 => - val superElems = newElem.captureSetOfInfo.elems.filter: superElem => - retain(superElem) && !elems.contains(superElem) - recur(elems ++ superElems, newElems1 ++ superElems.toList) - case Nil => elems - val elems: Refs = refs.filter(retain) - recur(elems, elems.toList) + if ccConfig.newScheme then + directFootprint.nonPeaks + else + def retain(ref: Capability) = !ref.isTerminalCapability + def recur(elems: Refs, newElems: List[Capability]): Refs = newElems match + case newElem :: newElems1 => + val superElems = newElem.captureSetOfInfo.elems.filter: superElem => + retain(superElem) && !elems.contains(superElem) + recur(elems ++ superElems, newElems1 ++ superElems.toList) + case Nil => elems + val elems: Refs = refs.filter(retain) + recur(elems, elems.toList) /** The footprint of a set of capabilities `refs` is the closure * of `refs` under `_.captureSetOfInfo`, dropping any shared terminal diff --git a/tests/neg-custom-args/captures/lazyref.check b/tests/neg-custom-args/captures/lazyref.check index 8a22613551c2..52e787f66553 100644 --- a/tests/neg-custom-args/captures/lazyref.check +++ b/tests/neg-custom-args/captures/lazyref.check @@ -54,7 +54,7 @@ | Hidden set of current argument : {cap2} | Hidden footprint of current argument : {cap2} | Capture set of function prefix : {ref1, ref2, ref2*} - | Footprint set of function prefix : {ref1, ref2, ref2*, cap1, cap2} + | Footprint set of function prefix : {ref1, cap1, ref2, cap2, ref2*} | The two sets overlap at : {cap2} | |where: => refers to a fresh root capability created in value ref4 when checking argument to parameter f of method map From bab1ef724e9868a12bef99a24b0e0f36bd6003b5 Mon Sep 17 00:00:00 2001 From: odersky Date: Thu, 2 Oct 2025 14:06:19 +0200 Subject: [PATCH 10/14] Make covers work also for FreshCaps --- .../src/dotty/tools/dotc/cc/Capability.scala | 48 +++++++++++-------- 1 file changed, 29 insertions(+), 19 deletions(-) diff --git a/compiler/src/dotty/tools/dotc/cc/Capability.scala b/compiler/src/dotty/tools/dotc/cc/Capability.scala index 8c6ff1e09235..e41cf8e6fb5d 100644 --- a/compiler/src/dotty/tools/dotc/cc/Capability.scala +++ b/compiler/src/dotty/tools/dotc/cc/Capability.scala @@ -770,28 +770,38 @@ object Capabilities: * x covers y ==> x covers y.f * x covers y ==> x* covers y*, x? covers y? * x covers y ==> x.only[C] covers y, x covers y.only[C] + * x covers y ==> covers y * TODO what other clauses from subsumes do we need to port here? */ final def covers(y: Capability)(using Context): Boolean = - (this eq y) - || y.match - case y @ TermRef(ypre: Capability, _) => - this.covers(ypre) - case Reach(y1) => - this match - case Reach(x1) => x1.covers(y1) - case _ => false - case Maybe(y1) => - this match - case Maybe(x1) => x1.covers(y1) - case _ => false - case Restricted(y1, _) => - this.covers(y1) - case _ => - false - || this.match - case Restricted(x1, _) => x1.covers(y) - case _ => false + val seen: util.EqHashSet[FreshCap] = new util.EqHashSet + + def recur(x: Capability, y: Capability): Boolean = + (x eq y) + || y.match + case y @ TermRef(ypre: Capability, _) => + recur(x, ypre) + case Reach(y1) => + x match + case Reach(x1) => recur(x1, y1) + case _ => false + case Maybe(y1) => + x match + case Maybe(x1) => recur(x1, y1) + case _ => false + case Restricted(y1, _) => + recur(x, y1) + case _ => + false + || x.match + case x: FreshCap if !seen.contains(x) => + seen.add(x) + x.hiddenSet.exists(recur(_, y)) + case Restricted(x1, _) => recur(x1, y) + case _ => false + + recur(this, y) + end covers def assumedContainsOf(x: TypeRef)(using Context): SimpleIdentitySet[Capability] = CaptureSet.assumedContains.getOrElse(x, SimpleIdentitySet.empty) From bc93c9e048adb41898c5637b68b86a263b6b2555 Mon Sep 17 00:00:00 2001 From: odersky Date: Thu, 2 Oct 2025 16:02:27 +0200 Subject: [PATCH 11/14] Drop old footprint and overlap logic. --- .../src/dotty/tools/dotc/cc/SepCheck.scala | 57 ++++++------------- .../captures/sep-counter.check | 2 +- .../neg-custom-args/captures/sep-pairs.check | 4 +- 3 files changed, 19 insertions(+), 44 deletions(-) diff --git a/compiler/src/dotty/tools/dotc/cc/SepCheck.scala b/compiler/src/dotty/tools/dotc/cc/SepCheck.scala index dc5ec8c5ecb5..bce5a2a46eab 100644 --- a/compiler/src/dotty/tools/dotc/cc/SepCheck.scala +++ b/compiler/src/dotty/tools/dotc/cc/SepCheck.scala @@ -170,24 +170,6 @@ object SepCheck: private def nonPeaks(using Context): Refs = refs.filter(!_.isTerminalCapability) - /** The footprint of a set of references `refs` the smallest set `F` such that - * 1. all capabilities in `refs` satisfying (1) are in `F` - * 2. if `f in F` then the footprint of `f`'s info is also in `F`. - */ - private def oldFootprint(using Context): Refs = - if ccConfig.newScheme then - directFootprint.nonPeaks - else - def retain(ref: Capability) = !ref.isTerminalCapability - def recur(elems: Refs, newElems: List[Capability]): Refs = newElems match - case newElem :: newElems1 => - val superElems = newElem.captureSetOfInfo.elems.filter: superElem => - retain(superElem) && !elems.contains(superElem) - recur(elems ++ superElems, newElems1 ++ superElems.toList) - case Nil => elems - val elems: Refs = refs.filter(retain) - recur(elems, elems.toList) - /** The footprint of a set of capabilities `refs` is the closure * of `refs` under `_.captureSetOfInfo`, dropping any shared terminal * capabilities. If `followHidden` is true, we close under both @@ -371,24 +353,15 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser: // ---- Error reporting TODO Once these are stabilized, move to messages -----" + - def sharedPeaksStr(shared: Refs)(using Context): String = + def overlapStr(hiddenSet: Refs, clashSet: Refs)(using Context): String = + val hiddenFootprint = hiddenSet.directFootprint + val clashFootprint = clashSet.directFootprint + val shared = hiddenFootprint.overlapWith(clashFootprint).reduced shared.nth(0) match case fresh: FreshCap => if fresh.hiddenSet.owner.exists then i"$fresh of ${fresh.hiddenSet.owner}" else i"$fresh" - case other => - i"$other" - - def overlapStr(hiddenSet: Refs, clashSet: Refs)(using Context): String = - val hiddenFootprint = hiddenSet.oldFootprint - val clashFootprint = clashSet.oldFootprint - // The overlap of footprints, or, of this empty the set of shared peaks. - // We prefer footprint overlap since it tends to be more informative. - val overlap = hiddenFootprint.overlapWith(clashFootprint) - if !overlap.isEmpty then i"${CaptureSet(overlap)}" - else - val sharedPeaks = hiddenSet.allPeaks.sharedPeaks(clashSet.allPeaks) - assert(!sharedPeaks.isEmpty, i"no overlap for $hiddenSet vs $clashSet") - sharedPeaksStr(sharedPeaks) + case _ => + i"${CaptureSet(shared)}" /** Report a separation failure in an application `fn(args)` * @param fn the function @@ -430,6 +403,8 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser: else i" with type ${clashing.nuType}" val hiddenSet = formalCaptures(polyArg).transHiddenSet val clashSet = deepCaptures(clashing) + val hiddenFootprint = hiddenSet.directFootprint + val clashFootprint = clashSet.directFootprint report.error( em"""Separation failure: argument of type ${polyArg.nuType} |to $funStr @@ -438,10 +413,10 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser: |Some of these overlap with the captures of the ${clashArgStr.trim}$clashTypeStr. | | Hidden set of current argument : ${CaptureSet(hiddenSet)} - | Hidden footprint of current argument : ${CaptureSet(hiddenSet.oldFootprint)} + | Hidden footprint of current argument : ${CaptureSet(hiddenFootprint.nonPeaks)} | Capture set of $clashArgStr : ${CaptureSet(clashSet)} - | Footprint set of $clashArgStr : ${CaptureSet(clashSet.oldFootprint)} - | The two sets overlap at : ${overlapStr(hiddenSet, clashSet)}""", + | Footprint set of $clashArgStr : ${CaptureSet(clashFootprint.nonPeaks)} + | The two sets overlap at : ${overlapStr(hiddenFootprint, clashFootprint)}""", polyArg.srcPos) /** Report a use/definition failure, where a previously hidden capability is @@ -720,7 +695,7 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser: val captured = genPart.deepCaptureSet.elems val hiddenSet = captured.transHiddenSet.pruned val clashSet = otherPart.deepCaptureSet.elems - val deepClashSet = (clashSet.oldFootprint ++ clashSet.transHiddenSet).pruned + val deepClashSet = clashSet.completeFootprint.nonPeaks.pruned report.error( em"""Separation failure in ${role.description} $tpe. |One part, $genPart, hides capabilities ${CaptureSet(hiddenSet)}. @@ -823,11 +798,11 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser: // "see through them" when we look at hidden sets. then val refs = tpe.deepCaptureSet.elems - val toCheck = refs.transHiddenSet.oldFootprint.deduct(refs.oldFootprint) + val toCheck = refs.transHiddenSet.directFootprint.nonPeaks.deduct(refs.directFootprint.nonPeaks) checkConsumedRefs(toCheck, tpe, role, i"${role.description} $tpe hides", pos) case TypeRole.Argument(arg) => if tpe.hasAnnotation(defn.ConsumeAnnot) then - val capts = spanCaptures(arg).oldFootprint + val capts = spanCaptures(arg).directFootprint.nonPeaks checkConsumedRefs(capts, tpe, role, i"argument to consume parameter with type ${arg.nuType} refers to", pos) case _ => @@ -952,7 +927,7 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser: def checkValOrDefDef(tree: ValOrDefDef)(using Context): Unit = if !tree.symbol.isOneOf(TermParamOrAccessor) && !isUnsafeAssumeSeparate(tree.rhs) then checkType(tree.tpt, tree.symbol) - capt.println(i"sep check def ${tree.symbol}: ${tree.tpt} with ${spanCaptures(tree.tpt).transHiddenSet.oldFootprint}") + capt.println(i"sep check def ${tree.symbol}: ${tree.tpt} with ${spanCaptures(tree.tpt).transHiddenSet.directFootprint}") pushDef(tree, spanCaptures(tree.tpt).transHiddenSet.deductSymRefs(tree.symbol)) def inSection[T](op: => T)(using Context): T = @@ -989,7 +964,7 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser: case tree @ Select(qual, _) if tree.symbol.is(Method) && tree.symbol.isConsumeParam => traverseChildren(tree) checkConsumedRefs( - spanCaptures(qual).oldFootprint, qual.nuType, + spanCaptures(qual).directFootprint.nonPeaks, qual.nuType, TypeRole.Qualifier(qual, tree.symbol), i"call prefix of consume ${tree.symbol} refers to", qual.srcPos) case tree: GenericApply => diff --git a/tests/neg-custom-args/captures/sep-counter.check b/tests/neg-custom-args/captures/sep-counter.check index a42b405fd727..44e4a897a565 100644 --- a/tests/neg-custom-args/captures/sep-counter.check +++ b/tests/neg-custom-args/captures/sep-counter.check @@ -3,7 +3,7 @@ | ^^^^^^^^^^^^^^^^ |Separation failure in method mkCounter's result type Pair[Ref^, Ref^²]. |One part, Ref^, hides capabilities {c, cap, cap²}. - |Another part, Ref^², captures capabilities {c, cap, cap²}. + |Another part, Ref^², captures capabilities {c}. |The two sets overlap at {c}. | |where: ^ refers to a fresh root capability classified as Mutable in the result type of method mkCounter diff --git a/tests/neg-custom-args/captures/sep-pairs.check b/tests/neg-custom-args/captures/sep-pairs.check index 43429b08a3bc..69909cf4f648 100644 --- a/tests/neg-custom-args/captures/sep-pairs.check +++ b/tests/neg-custom-args/captures/sep-pairs.check @@ -13,7 +13,7 @@ | ^^^^^^^^^^^^^^^^ | Separation failure in method bad's result type Pair[Ref^, Ref^²]. | One part, Ref^, hides capabilities {r1*, cap, cap², r0}. - | Another part, Ref^², captures capabilities {r1*, cap, cap², r0}. + | Another part, Ref^², captures capabilities {r1*, r0}. | The two sets overlap at {r1*, r0}. | | where: ^ refers to a fresh root capability classified as Mutable in the result type of method bad @@ -25,7 +25,7 @@ | ^^^^^^^^^^^^^^^^ | Separation failure in value sameToPair's type Pair[Ref^, Ref^²]. | One part, Ref^, hides capabilities {fstSame}. - | Another part, Ref^², captures capabilities {sndSame}. + | Another part, Ref^², captures capabilities {sndSame, same.snd*}. | The two sets overlap at cap of value same. | | where: ^ refers to a fresh root capability classified as Mutable in the type of value sameToPair From 77f60a146f4ff70456938f6fc63682423a195c47 Mon Sep 17 00:00:00 2001 From: odersky Date: Thu, 2 Oct 2025 16:45:23 +0200 Subject: [PATCH 12/14] Make formalCaptures use the spanCaptureSet --- compiler/src/dotty/tools/dotc/cc/SepCheck.scala | 7 ++++--- tests/neg-custom-args/captures/sepchecks2.check | 16 ---------------- tests/neg-custom-args/captures/sepchecks2.scala | 2 +- 3 files changed, 5 insertions(+), 20 deletions(-) diff --git a/compiler/src/dotty/tools/dotc/cc/SepCheck.scala b/compiler/src/dotty/tools/dotc/cc/SepCheck.scala index bce5a2a46eab..6a607da5cca7 100644 --- a/compiler/src/dotty/tools/dotc/cc/SepCheck.scala +++ b/compiler/src/dotty/tools/dotc/cc/SepCheck.scala @@ -341,7 +341,7 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser: * the latter contains a cap. */ private def formalCaptures(arg: Tree)(using Context): Refs = - arg.formalType.orElse(arg.nuType).deepCaptureSet.elems + arg.formalType.orElse(arg.nuType).spanCaptureSet.elems /** The span capture set if the type of `tree` */ private def spanCaptures(tree: Tree)(using Context): Refs = @@ -402,7 +402,7 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser: if clashIdx == 0 && !isShowableMethod then "" // we already mentioned the type in `funStr` else i" with type ${clashing.nuType}" val hiddenSet = formalCaptures(polyArg).transHiddenSet - val clashSet = deepCaptures(clashing) + val clashSet = if clashIdx == -1 then deepCaptures(clashing) else spanCaptures(clashing) val hiddenFootprint = hiddenSet.directFootprint val clashFootprint = clashSet.directFootprint report.error( @@ -891,10 +891,11 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser: val resultType = mtpe.finalResultType val resultCaptures = (resultArgCaptures(resultType) ++ resultType.deepCaptureSet.elems).filter(!isLocalRef(_)) + // See i23726.scala why deepCaptureSet is needed here. val resultPeaks = resultCaptures.allPeaks capt.println(i"deps for $app = ${deps.toList}") (deps, resultPeaks) - + end dependencies /** Decompose an application into a function prefix and a list of argument lists. * If some of the arguments need a separation check because they are capture polymorphic, diff --git a/tests/neg-custom-args/captures/sepchecks2.check b/tests/neg-custom-args/captures/sepchecks2.check index 98e45a4e23b4..6e991003c5a2 100644 --- a/tests/neg-custom-args/captures/sepchecks2.check +++ b/tests/neg-custom-args/captures/sepchecks2.check @@ -1,19 +1,3 @@ --- Error: tests/neg-custom-args/captures/sepchecks2.scala:13:7 --------------------------------------------------------- -13 | foo((() => println(c)) :: Nil, c) // error - | ^^^^^^^^^^^^^^^^^^^^^^^^ - |Separation failure: argument of type List[() ->{c} Unit] - |to method foo: (xs: List[() => Unit], y: Object^): Nothing - |corresponds to capture-polymorphic formal parameter xs of type List[() => Unit] - |and hides capabilities {c}. - |Some of these overlap with the captures of the second argument with type (c : Object^). - | - | Hidden set of current argument : {c} - | Hidden footprint of current argument : {c} - | Capture set of second argument : {c} - | Footprint set of second argument : {c} - | The two sets overlap at : {c} - | - |where: => refers to a fresh root capability created in method Test2 when checking argument to parameter xs of method foo -- Error: tests/neg-custom-args/captures/sepchecks2.scala:14:10 -------------------------------------------------------- 14 | val x1: (Object^, Object^) = (c, c) // error | ^^^^^^^^^^^^^^^^^^ diff --git a/tests/neg-custom-args/captures/sepchecks2.scala b/tests/neg-custom-args/captures/sepchecks2.scala index a255b4059902..02162f74a61a 100644 --- a/tests/neg-custom-args/captures/sepchecks2.scala +++ b/tests/neg-custom-args/captures/sepchecks2.scala @@ -10,7 +10,7 @@ def Test(consume c: Object^) = println(c) def Test2(c: Object^, d: Object^): Unit = - foo((() => println(c)) :: Nil, c) // error + foo((() => println(c)) :: Nil, c) // ok val x1: (Object^, Object^) = (c, c) // error val x2: (Object^, Object^{d}) = (d, d) // error From f67c6fb2bf84b48682b4461852881db74339f4aa Mon Sep 17 00:00:00 2001 From: odersky Date: Fri, 3 Oct 2025 12:11:51 +0200 Subject: [PATCH 13/14] Add some more doc comments --- .../src/dotty/tools/dotc/cc/Capability.scala | 3 ++- .../src/dotty/tools/dotc/cc/CaptureOps.scala | 21 +++++++++++++++---- .../src/dotty/tools/dotc/cc/CaptureSet.scala | 6 ++---- 3 files changed, 21 insertions(+), 9 deletions(-) diff --git a/compiler/src/dotty/tools/dotc/cc/Capability.scala b/compiler/src/dotty/tools/dotc/cc/Capability.scala index e41cf8e6fb5d..8ded3b14755d 100644 --- a/compiler/src/dotty/tools/dotc/cc/Capability.scala +++ b/compiler/src/dotty/tools/dotc/cc/Capability.scala @@ -553,9 +553,10 @@ object Capabilities: */ def hiddenSet(using Context): Refs = computeHiddenSet(identity) - /** Compute hidden set of this capability. + /** Compute result based on hidden set of this capability. * Restrictions and read-only status transfer from the capability to its * hidden set. + * @param f a function that gets applied to all detected hidden sets */ def computeHiddenSet(f: Refs => Refs)(using Context): Refs = this match case self: FreshCap => f(self.hiddenSet.elems) diff --git a/compiler/src/dotty/tools/dotc/cc/CaptureOps.scala b/compiler/src/dotty/tools/dotc/cc/CaptureOps.scala index a3ccd748bcfb..bb667c3af14a 100644 --- a/compiler/src/dotty/tools/dotc/cc/CaptureOps.scala +++ b/compiler/src/dotty/tools/dotc/cc/CaptureOps.scala @@ -151,24 +151,37 @@ extension (tp: Type) case tp: ObjectCapability => tp.captureSetOfInfo case _ => CaptureSet.ofType(tp, followResult = false) - /** The deep capture set of a type. This is by default the union of all + /** Compute a captureset by traversing parts of this type. This is by default the union of all * covariant capture sets embedded in the widened type, as computed by * `CaptureSet.ofTypeDeeply`. If that set is nonempty, and the type is * a singleton capability `x` or a reach capability `x*`, the deep capture * set can be narrowed to`{x*}`. + * @param includeTypevars if true, return a new FreshCap for every type parameter + * or abstract type with an Any upper bound. Types with + * defined upper bound are always mapped to the dcs of their bound + * @param includeBoxed if true, include capture sets found in boxed parts of this type */ - def deepCaptureSet(includeTypevars: Boolean, includeBoxed: Boolean = true)(using Context): CaptureSet = + def computeDeepCaptureSet(includeTypevars: Boolean, includeBoxed: Boolean = true)(using Context): CaptureSet = val dcs = CaptureSet.ofTypeDeeply(tp.widen.stripCapturing, includeTypevars, includeBoxed) if dcs.isAlwaysEmpty then tp.captureSet else tp match case tp: ObjectCapability if tp.isTrackableRef => tp.reach.singletonCaptureSet case _ => tp.captureSet ++ dcs + /** The deep capture set of a type. This is by default the union of all + * covariant capture sets embedded in the widened type, as computed by + * `CaptureSet.ofTypeDeeply`. If that set is nonempty, and the type is + * a singleton capability `x` or a reach capability `x*`, the deep capture + * set can be narrowed to`{x*}`. + */ def deepCaptureSet(using Context): CaptureSet = - deepCaptureSet(includeTypevars = false) + computeDeepCaptureSet(includeTypevars = false) + /** The span capture set of a type. This is analogous to deepCaptureSet but ignoring + * capture sets in boxed parts. + */ def spanCaptureSet(using Context): CaptureSet = - deepCaptureSet(includeTypevars = false, includeBoxed = false) + computeDeepCaptureSet(includeTypevars = false, includeBoxed = false) /** A type capturing `ref` */ def capturing(ref: Capability)(using Context): Type = diff --git a/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala b/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala index 061c7c2b4fc8..86c502b489f8 100644 --- a/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala +++ b/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala @@ -950,8 +950,6 @@ object CaptureSet: override def toString = s"Var$id$elems" end Var - inline val strictFreshLevels = true - /** Variables created in types of inferred type trees */ class ProperVar(override val owner: Symbol, initialElems: Refs = emptyRefs, nestedOK: Boolean = true, isRefining: Boolean)(using /*@constructorOnly*/ ictx: Context) extends Var(owner, initialElems, nestedOK): @@ -971,7 +969,7 @@ object CaptureSet: def fail = i"attempting to add $elem to $this" def hideIn(fc: FreshCap): Unit = assert(elem.tryClassifyAs(fc.hiddenSet.classifier), fail) - if strictFreshLevels && !isRefining then + if !isRefining then // If a variable is added by addCaptureRefinements in a synthetic // refinement of a class type, don't do level checking. The problem is // that the variable might be matched against a type that does not have @@ -1560,7 +1558,7 @@ object CaptureSet: /** The capture set of the type underlying the capability `c` */ def ofInfo(c: Capability)(using Context): CaptureSet = c match case Reach(c1) => - c1.widen.deepCaptureSet(includeTypevars = true) + c1.widen.computeDeepCaptureSet(includeTypevars = true) .showing(i"Deep capture set of $c: ${c1.widen} = ${result}", capt) case Restricted(c1, cls) => if cls == defn.NothingClass then CaptureSet.empty From c492a63ca67ced5473b88f29f0461ce831142fb0 Mon Sep 17 00:00:00 2001 From: odersky Date: Fri, 3 Oct 2025 18:05:52 +0200 Subject: [PATCH 14/14] Address review suggestions --- .../src/dotty/tools/dotc/cc/Capability.scala | 7 +++- .../src/dotty/tools/dotc/cc/SepCheck.scala | 17 +++++----- .../captures/cc-poly-varargs.check | 34 +++++++++++++++++++ 3 files changed, 48 insertions(+), 10 deletions(-) create mode 100644 tests/neg-custom-args/captures/cc-poly-varargs.check diff --git a/compiler/src/dotty/tools/dotc/cc/Capability.scala b/compiler/src/dotty/tools/dotc/cc/Capability.scala index 8ded3b14755d..d665e8d4bd3c 100644 --- a/compiler/src/dotty/tools/dotc/cc/Capability.scala +++ b/compiler/src/dotty/tools/dotc/cc/Capability.scala @@ -770,9 +770,14 @@ object Capabilities: * x covers x * x covers y ==> x covers y.f * x covers y ==> x* covers y*, x? covers y? - * x covers y ==> x.only[C] covers y, x covers y.only[C] * x covers y ==> covers y + * x covers y ==> x.only[C] covers y, x covers y.only[C] + * * TODO what other clauses from subsumes do we need to port here? + * The last clause is a conservative over-approximation: basically, we can't achieve + * separation by having different classifiers for now. It would be good to + * have a test that would expect such separation, then we can try to refine + * the clause to make the test pass. */ final def covers(y: Capability)(using Context): Boolean = val seen: util.EqHashSet[FreshCap] = new util.EqHashSet diff --git a/compiler/src/dotty/tools/dotc/cc/SepCheck.scala b/compiler/src/dotty/tools/dotc/cc/SepCheck.scala index 6a607da5cca7..65aa2fdce124 100644 --- a/compiler/src/dotty/tools/dotc/cc/SepCheck.scala +++ b/compiler/src/dotty/tools/dotc/cc/SepCheck.scala @@ -118,9 +118,9 @@ object SepCheck: def clashing(ref: Capability)(using Context): SrcPos | Null = val refPeaks = ref.directPeaks - if !directPeaks .sharedPeaks(refPeaks).isEmpty then + if !directPeaks.sharedPeaks(refPeaks).isEmpty then var i = 0 - while i < size && refs(i).directPeaks .sharedPeaks(refPeaks).isEmpty do + while i < size && refs(i).directPeaks.sharedPeaks(refPeaks).isEmpty do i += 1 assert(i < size) locs(i) @@ -232,13 +232,12 @@ object SepCheck: * such that one of the following is true: * 1. * - one of the sets contains `r` - * - the other contains a capability `s` or `s.rd` where `s` _covers_ `r` + * - the other contains a capability `s` or `s.rd` where `s` covers `r` * 2. * - one of the sets contains `r.rd` - * - the other contains a capability `s` where `s` _covers_ `r` + * - the other contains a capability `s` where `s` covers `r` * - * A capability `s` covers `r` if `r` can be seen as a path extension of `s`. E.g. - * if `s = x.a` and `r = x.a.b.c` then `s` covers `a`. + * @see covers in Capability */ private def overlapWith(other: Refs)(using Context): Refs = val refs1 = refs @@ -343,11 +342,11 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser: private def formalCaptures(arg: Tree)(using Context): Refs = arg.formalType.orElse(arg.nuType).spanCaptureSet.elems - /** The span capture set if the type of `tree` */ + /** The span capture set of the type of `tree` */ private def spanCaptures(tree: Tree)(using Context): Refs = tree.nuType.spanCaptureSet.elems - /** The deep capture set if the type of `tree` */ + /** The deep capture set of the type of `tree` */ private def deepCaptures(tree: Tree)(using Context): Refs = tree.nuType.deepCaptureSet.elems @@ -588,7 +587,7 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser: for ref <- used do val pos = consumed.clashing(ref) if pos != null then - // println(i"consumed so far ${consumed.refs.toList} with peaks ${consumed.directPeaks .toList}, used = $used, exposed = ${ref.directPeaks }") + // println(i"consumed so far ${consumed.refs.toList} with peaks ${consumed.directPeaks.toList}, used = $used, exposed = ${ref.directPeaks }") consumeError(ref, pos, tree.srcPos) end checkUse diff --git a/tests/neg-custom-args/captures/cc-poly-varargs.check b/tests/neg-custom-args/captures/cc-poly-varargs.check new file mode 100644 index 000000000000..764274813faf --- /dev/null +++ b/tests/neg-custom-args/captures/cc-poly-varargs.check @@ -0,0 +1,34 @@ +-- Error: tests/neg-custom-args/captures/cc-poly-varargs.scala:11:13 --------------------------------------------------- +11 | val left = src1.transformValuesWith(Left(_)) // error + | ^^^^ + |Separation failure: argument of type (src1 : Source[T1, scala.caps.CapSet^{Cap}]^{Cap}) + |to method transformValuesWith: [T, Cap >: scala.caps.CapSet <: scala.caps.CapSet^] + | (src: Source[T, scala.caps.CapSet^{Cap}]^)[U](f: T ->{Cap} U): Source[U, scala.caps.CapSet^{Cap}]^{src, f} + |corresponds to capture-polymorphic formal parameter src of type Source[T1^'s3, scala.caps.CapSet^{Cap}]^ + |and hides capabilities {src1}. + |Some of these overlap with the captures of the function result with type Source[Left[T1^'s1, Nothing]^'s2, scala.caps.CapSet^{Cap}]^{src1}. + | + | Hidden set of current argument : {src1} + | Hidden footprint of current argument : {src1, Cap} + | Capture set of function result : {src1, Cap} + | Footprint set of function result : {src1, Cap} + | The two sets overlap at : {src1, Cap} + | + |where: ^ refers to a fresh root capability created in value left when checking argument to parameter src of method transformValuesWith +-- Error: tests/neg-custom-args/captures/cc-poly-varargs.scala:12:14 --------------------------------------------------- +12 | val right = src2.transformValuesWith(Right(_)) // error + | ^^^^ + |Separation failure: argument of type (src2 : Source[T2, scala.caps.CapSet^{Cap}]^{Cap}) + |to method transformValuesWith: [T, Cap >: scala.caps.CapSet <: scala.caps.CapSet^] + | (src: Source[T, scala.caps.CapSet^{Cap}]^)[U](f: T ->{Cap} U): Source[U, scala.caps.CapSet^{Cap}]^{src, f} + |corresponds to capture-polymorphic formal parameter src of type Source[T2^'s6, scala.caps.CapSet^{Cap}]^ + |and hides capabilities {src2}. + |Some of these overlap with the captures of the function result with type Source[Right[Nothing, T2^'s4]^'s5, scala.caps.CapSet^{Cap}]^{src2}. + | + | Hidden set of current argument : {src2} + | Hidden footprint of current argument : {src2, Cap} + | Capture set of function result : {src2, Cap} + | Footprint set of function result : {src2, Cap} + | The two sets overlap at : {src2, Cap} + | + |where: ^ refers to a fresh root capability created in value right when checking argument to parameter src of method transformValuesWith