From 2ade0a599f759b0f769a9b32e67b3b7871be8ca7 Mon Sep 17 00:00:00 2001 From: odersky Date: Sun, 16 Nov 2025 19:19:13 +0100 Subject: [PATCH 01/10] Add Unscoped classifier - FreshCaps with Unscoped classifier are assumed to be owned by the enclosing toplevel class - FreshCaps with unscoped classifier are not turned into ResultCaps in the return types of anonymous functions. --- .../src/dotty/tools/dotc/cc/Capability.scala | 26 +++++++++++-------- .../dotty/tools/dotc/core/Definitions.scala | 3 ++- library/src/scala/caps/package.scala | 6 +++++ .../captures/ref-with-file.scala | 19 ++++++++++++++ 4 files changed, 42 insertions(+), 12 deletions(-) create mode 100644 tests/pos-custom-args/captures/ref-with-file.scala diff --git a/compiler/src/dotty/tools/dotc/cc/Capability.scala b/compiler/src/dotty/tools/dotc/cc/Capability.scala index e0abaf100d0e..240a57463c6b 100644 --- a/compiler/src/dotty/tools/dotc/cc/Capability.scala +++ b/compiler/src/dotty/tools/dotc/cc/Capability.scala @@ -276,9 +276,10 @@ object Capabilities: * if separation checks are turned off). * @pre The capability's origin was not yet set. */ - def setOrigin(freshOrigin: FreshCap | GlobalCap.type): Unit = + def setOrigin(freshOrigin: FreshCap | GlobalCap.type): this.type = assert(myOrigin eq GlobalCap) myOrigin = freshOrigin + this /** If the current capability was created via a chain of `derivedResult` calls * from an original ResultCap `r`, that `r`. Otherwise `this`. @@ -517,6 +518,8 @@ object Capabilities: case prefix: ThisType if setOwner.isTerm && setOwner.owner == prefix.cls => setOwner case prefix: Capability => prefix.ccOwner + case NoPrefix if classifier.derivesFrom(defn.Caps_Unscoped) => + ctx.owner.topLevelClass case _ => setOwner case _ /* : GlobalCap | ResultCap | ParamRef */ => NoSymbol @@ -1168,7 +1171,7 @@ object Capabilities: case _ => super.mapOver(t) - class ToResult(localResType: Type, mt: MethodicType, fail: Message => Unit)(using Context) extends CapMap: + class ToResult(localResType: Type, mt: MethodicType, sym: Symbol, fail: Message => Unit)(using Context) extends CapMap: def apply(t: Type) = t match case defn.FunctionNOf(args, res, contextual) if t.typeSymbol.name.isImpureFunction => @@ -1183,11 +1186,12 @@ object Capabilities: override def mapCapability(c: Capability, deep: Boolean) = c match case c: (FreshCap | GlobalCap.type) => if variance > 0 then - val res = ResultCap(mt) c match - case c: FreshCap => res.setOrigin(c) - case _ => - res + case c: FreshCap => + if sym.isAnonymousFunction && c.classifier.derivesFrom(defn.Caps_Unscoped) + then c + else ResultCap(mt).setOrigin(c) + case _ => ResultCap(mt) else if variance == 0 then fail(em"""$localResType captures the root capability `cap` in invariant position. @@ -1227,8 +1231,8 @@ object Capabilities: * variable bound by `mt`. * Stop at function or method types since these have been mapped before. */ - def toResult(tp: Type, mt: MethodicType, fail: Message => Unit)(using Context): Type = - ToResult(tp, mt, fail)(tp) + def toResult(tp: Type, mt: MethodicType, sym: Symbol, fail: Message => Unit)(using Context): Type = + ToResult(tp, mt, sym, fail)(tp) /** Map global roots in function results to result roots. Also, * map roots in the types of def methods that are parameterless @@ -1244,7 +1248,7 @@ object Capabilities: else apply(mt)) case t: MethodType if variance > 0 && t.marksExistentialScope => val t1 = mapOver(t).asInstanceOf[MethodType] - t1.derivedLambdaType(resType = toResult(t1.resType, t1, fail)) + t1.derivedLambdaType(resType = toResult(t1.resType, t1, sym, fail)) case CapturingType(parent, refs) => t.derivedCapturingType(this(parent), refs) case t: (LazyRef | TypeVar) => @@ -1259,7 +1263,7 @@ object Capabilities: m(tp) match case tp1: ExprType if sym.is(Method, butNot = Accessor) => // Map the result of parameterless `def` methods. - tp1.derivedExprType(toResult(tp1.resType, tp1, fail)) + tp1.derivedExprType(toResult(tp1.resType, tp1, sym, fail)) case tp1: PolyType if !tp1.resType.isInstanceOf[MethodicType] => // Map also the result type of method with only type parameters. // This way, the `^` in the following method will be mapped to a `ResultCap`: @@ -1269,7 +1273,7 @@ object Capabilities: // ``` // This is more desirable than interpreting `^` as a `Fresh` at the level of `Buffer.empty` // in most cases. - tp1.derivedLambdaType(resType = toResult(tp1.resType, tp1, fail)) + tp1.derivedLambdaType(resType = toResult(tp1.resType, tp1, sym, fail)) case tp1 => tp1 end toResultInResults diff --git a/compiler/src/dotty/tools/dotc/core/Definitions.scala b/compiler/src/dotty/tools/dotc/core/Definitions.scala index ce8af0801c3e..f2ce43cecd24 100644 --- a/compiler/src/dotty/tools/dotc/core/Definitions.scala +++ b/compiler/src/dotty/tools/dotc/core/Definitions.scala @@ -1014,6 +1014,7 @@ class Definitions { @tu lazy val Caps_Control: ClassSymbol = requiredClass("scala.caps.Control") @tu lazy val Caps_Mutable: ClassSymbol = requiredClass("scala.caps.Mutable") @tu lazy val Caps_Read: ClassSymbol = requiredClass("scala.caps.Read") + @tu lazy val Caps_Unscoped: ClassSymbol = requiredClass("scala.caps.Unscoped") @tu lazy val Caps_CapSet: ClassSymbol = requiredClass("scala.caps.CapSet") @tu lazy val CapsInternalModule: Symbol = requiredModule("scala.caps.internal") @tu lazy val Caps_erasedValue: Symbol = CapsInternalModule.requiredMethod("erasedValue") @@ -2090,7 +2091,7 @@ class Definitions { @tu lazy val ccExperimental: Set[Symbol] = Set( CapsModule, CapsModule.moduleClass, PureClass, /* Caps_Classifier, Caps_SharedCapability, Caps_Control, -- already stable */ - Caps_ExclusiveCapability, Caps_Mutable, Caps_Read, + Caps_ExclusiveCapability, Caps_Mutable, Caps_Read, Caps_Unscoped, RequiresCapabilityAnnot, captureRoot, Caps_CapSet, Caps_ContainsTrait, Caps_ContainsModule, Caps_ContainsModule.moduleClass, ConsumeAnnot, UseAnnot, ReserveAnnot, diff --git a/library/src/scala/caps/package.scala b/library/src/scala/caps/package.scala index 6fbb0a9a0f93..c4914549a75c 100644 --- a/library/src/scala/caps/package.scala +++ b/library/src/scala/caps/package.scala @@ -86,6 +86,12 @@ trait Mutable extends ExclusiveCapability @experimental trait Read extends Mutable, Classifier +/** Marker trait for classes that are not subject to scoping restrictions + * of captured capabilities. + */ +@experimental +trait Unscoped extends ExclusiveCapability, Classifier + /** Carrier trait for capture set type parameters */ @experimental trait CapSet extends Any diff --git a/tests/pos-custom-args/captures/ref-with-file.scala b/tests/pos-custom-args/captures/ref-with-file.scala new file mode 100644 index 000000000000..1922a52f0c88 --- /dev/null +++ b/tests/pos-custom-args/captures/ref-with-file.scala @@ -0,0 +1,19 @@ +import caps.* + +class Ref[T](init: T) extends Mutable, Unscoped: + var x = init + def get: T = x + update def put(y: T): Unit = x = y + +class File: + def read(): String = ??? + +def withFile[T](op: (f: File^) => T): T = + op(new File) + +def Test = + withFile: f => + val r = Ref(f.read()) + r + + From 394f958d0bc7a681947415994bb7f1a42b85bf87 Mon Sep 17 00:00:00 2001 From: odersky Date: Mon, 17 Nov 2025 13:47:32 +0100 Subject: [PATCH 02/10] Revert "Represent read-only with a classifier" This reverts commit 9abbb03f4957147b2f098c874548c13860e81109. This reverts commit 0a0e666db3a1327e60931604699a9133652c54bc. This reverts commit 67ba9b51d930d1e8671234a072120b4dc0ae8129. Read-only cannot be a classifier anymore, since it would overlap with Unscoped, but neither subsumes the other. --- .../src/dotty/tools/dotc/cc/Capability.scala | 48 ++++++++++++------- .../src/dotty/tools/dotc/cc/CaptureSet.scala | 2 + .../src/dotty/tools/dotc/cc/SepCheck.scala | 4 +- compiler/src/dotty/tools/dotc/cc/Setup.scala | 2 +- .../src/dotty/tools/dotc/core/Types.scala | 5 ++ .../captures/check-inferred.check | 10 ++-- .../captures/classified-inheritance2.check | 13 ++++- .../captures/classified-inheritance2.scala | 2 +- 8 files changed, 59 insertions(+), 27 deletions(-) diff --git a/compiler/src/dotty/tools/dotc/cc/Capability.scala b/compiler/src/dotty/tools/dotc/cc/Capability.scala index 240a57463c6b..36a03ececc96 100644 --- a/compiler/src/dotty/tools/dotc/cc/Capability.scala +++ b/compiler/src/dotty/tools/dotc/cc/Capability.scala @@ -90,9 +90,18 @@ object Capabilities: */ case class Maybe(underlying: Capability) extends DerivedCapability + /** The readonly capability `x.rd`. We have {x.rd} <: {x}. + * + * Read-only capabilities cannot wrap maybe capabilities + * but they can wrap reach capabilities. We have + * (x?).readOnly = (x.rd)? + */ + case class ReadOnly(underlying: CoreCapability | RootCapability | Reach | Restricted) + extends DerivedCapability + /** The restricted capability `x.only[C]`. We have {x.only[C]} <: {x}. * - * Restricted capabilities cannot wrap maybe capabilities + * Restricted capabilities cannot wrap maybe capabilities or read-only capabilities * but they can wrap reach capabilities. We have * (x?).restrict[T] = (x.restrict[T])? * (x.rd).restrict[T] = (x.restrict[T]).rd @@ -100,15 +109,6 @@ object Capabilities: case class Restricted(underlying: CoreCapability | RootCapability | Reach, cls: ClassSymbol) extends DerivedCapability - /** An extractor for the read-only capability `x.rd`. `x.rd` is represented as - * `c.only[caps.Read]`. - */ - object ReadOnly: - def apply(underlying: CoreCapability | RootCapability | Reach | Restricted)(using Context): Restricted = - Restricted(underlying.stripRestricted.asInstanceOf, defn.Caps_Read) - def unapply(ref: Restricted)(using Context): Option[CoreCapability | RootCapability | Reach] = - if ref.cls == defn.Caps_Read then Some(ref.underlying) else None - /** If `x` is a capability, its reach capability `x*`. `x*` stands for all * capabilities reachable through `x`. * We have `{x} <: {x*} <: dcs(x)}` where the deep capture set `dcs(x)` of `x` @@ -116,7 +116,7 @@ object Capabilities: * type of `x`. If `x` and `y` are different variables then `{x*}` and `{y*}` * are unrelated. * - * Reach capabilities cannot wrap restricted capabilities or maybe capabilities. + * Reach capabilities cannot wrap read-only capabilities or maybe capabilities. * We have * (x?).reach = (x.reach)? * (x.rd).reach = (x.reach).rd @@ -132,7 +132,7 @@ object Capabilities: object GlobalCap extends RootCapability: def descr(using Context) = "the universal root capability" override val maybe = Maybe(this) - override def readOnly(using Context) = ReadOnly(this) + override val readOnly = ReadOnly(this) override def restrict(cls: ClassSymbol)(using Context) = Restricted(this, cls) override def reach = unsupported("cap.reach") override def singletonCaptureSet(using Context) = CaptureSet.universal @@ -347,21 +347,23 @@ object Capabilities: case self: Maybe => self case _ => cached(Maybe(this)) - def readOnly(using Context): Restricted | Maybe = this match + def readOnly: ReadOnly | Maybe = this match case Maybe(ref1) => Maybe(ref1.readOnly) - case self @ ReadOnly(_) => self + case self: ReadOnly => self case self: (CoreCapability | RootCapability | Reach | Restricted) => cached(ReadOnly(self)) - def restrict(cls: ClassSymbol)(using Context): Restricted | Maybe = this match + def restrict(cls: ClassSymbol)(using Context): Restricted | ReadOnly | Maybe = this match case Maybe(ref1) => Maybe(ref1.restrict(cls)) + case ReadOnly(ref1) => ReadOnly(ref1.restrict(cls).asInstanceOf[Restricted]) case self @ Restricted(ref1, prevCls) => val combinedCls = leastClassifier(prevCls, cls) if combinedCls == prevCls then self else cached(Restricted(ref1, combinedCls)) case self: (CoreCapability | RootCapability | Reach) => cached(Restricted(self, cls)) - def reach: Reach | Restricted | Maybe = this match + def reach: Reach | Restricted | ReadOnly | Maybe = this match case Maybe(ref1) => Maybe(ref1.reach) + case ReadOnly(ref1) => ReadOnly(ref1.reach.asInstanceOf[Reach | Restricted]) case Restricted(ref1, cls) => Restricted(ref1.reach.asInstanceOf[Reach], cls) case self: Reach => self case self: ObjectCapability => cached(Reach(self)) @@ -382,6 +384,7 @@ object Capabilities: */ final def classifier(using Context): Symbol = this match case Restricted(_, cls) => cls + case ReadOnly(ref1) => ref1.classifier case Maybe(ref1) => ref1.classifier case self: FreshCap => self.hiddenSet.classifier case _ => NoSymbol @@ -400,9 +403,10 @@ object Capabilities: case Maybe(ref1) => ref1.stripReadOnly.maybe case _ => this - /** Drop restrictions with class `cls` or a superclass of `cls` */ + /** Drop restrictions with clss `cls` or a superclass of `cls` */ final def stripRestricted(cls: ClassSymbol)(using Context): Capability = this match case Restricted(ref1, cls1) if cls.isSubClass(cls1) => ref1 + case ReadOnly(ref1) => ref1.stripRestricted(cls).readOnly case Maybe(ref1) => ref1.stripRestricted(cls).maybe case _ => this @@ -411,6 +415,7 @@ object Capabilities: final def stripReach(using Context): Capability = this match case Reach(ref1) => ref1 + case ReadOnly(ref1) => ref1.stripReach.readOnly case Restricted(ref1, cls) => ref1.stripReach.restrict(cls) case Maybe(ref1) => ref1.stripReach.maybe case _ => this @@ -596,6 +601,7 @@ object Capabilities: 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. */ @@ -613,6 +619,8 @@ object Capabilities: assert(cls != defn.AnyClass) if cls == defn.NothingClass then ClassifiedAs(Nil) else ClassifiedAs(cls :: Nil) + case ReadOnly(ref1) => + ref1.transClassifiers case Maybe(ref1) => ref1.transClassifiers case Reach(_) => @@ -636,6 +644,8 @@ object Capabilities: case Restricted(_, cls1) => assert(cls != defn.AnyClass) cls1.isSubClass(cls) + case ReadOnly(ref1) => + ref1.tryClassifyAs(cls) case Maybe(ref1) => ref1.tryClassifyAs(cls) case Reach(_) => @@ -656,6 +666,7 @@ object Capabilities: cs.forall(c => leastClassifier(c, cls) == defn.NothingClass) case _ => false isEmpty || ref1.isKnownEmpty + case ReadOnly(ref1) => ref1.isKnownEmpty case Maybe(ref1) => ref1.isKnownEmpty case _ => false @@ -716,6 +727,7 @@ object Capabilities: case _ => false || viaInfo(y.info)(subsumingRefs(this, _)) case Maybe(y1) => this.stripMaybe.subsumes(y1) + case ReadOnly(y1) => this.stripReadOnly.subsumes(y1) case Restricted(y1, cls) => this.stripRestricted(cls).subsumes(y1) case y: TypeRef if y.derivesFrom(defn.Caps_CapSet) => // The upper and lower bounds don't have to be in the form of `CapSet^{...}`. @@ -799,6 +811,7 @@ object Capabilities: y.isKnownClassifiedAs(cls) && x1.maxSubsumes(y, canAddHidden) case _ => y match + case ReadOnly(y1) => this.stripReadOnly.maxSubsumes(y1, canAddHidden) case Restricted(y1, cls) => this.stripRestricted(cls).maxSubsumes(y1, canAddHidden) case _ => false @@ -886,6 +899,7 @@ object Capabilities: case c: DerivedCapability => val c1 = c.underlying.toType c match + case _: ReadOnly => ReadOnlyCapability(c1) case Restricted(_, cls) => OnlyCapability(c1, cls) case _: Reach => ReachCapability(c1) case _: Maybe => MaybeCapability(c1) diff --git a/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala b/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala index 1924540f678f..903553214936 100644 --- a/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala +++ b/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala @@ -1625,6 +1625,8 @@ object CaptureSet: case Restricted(c1, cls) => if cls == defn.NothingClass then CaptureSet.empty else c1.captureSetOfInfo.restrict(cls) // todo: should we simplify using subsumption here? + case ReadOnly(c1) => + c1.captureSetOfInfo.readOnly case Maybe(c1) => c1.captureSetOfInfo.maybe case c: RootCapability => diff --git a/compiler/src/dotty/tools/dotc/cc/SepCheck.scala b/compiler/src/dotty/tools/dotc/cc/SepCheck.scala index a40e7699c953..0de12c7cd1e9 100644 --- a/compiler/src/dotty/tools/dotc/cc/SepCheck.scala +++ b/compiler/src/dotty/tools/dotc/cc/SepCheck.scala @@ -180,7 +180,7 @@ object SepCheck: case newElem :: newElems1 => if seen.contains(newElem) then recur(seen, acc, newElems1) - else newElem.stripRestricted match + else newElem.stripRestricted.stripReadOnly match case _: FreshCap if !newElem.isKnownClassifiedAs(defn.Caps_SharedCapability) => val hiddens = if followHidden then newElem.hiddenSet.toList else Nil recur(seen + newElem, acc + newElem, hiddens ++ newElems1) @@ -220,7 +220,7 @@ object SepCheck: refs1.foreach: ref => if !ref.isReadOnly then val coreRef = ref.stripRestricted - if refs2.exists(_.stripRestricted.coversFresh(coreRef)) then + if refs2.exists(_.stripRestricted.stripReadOnly.coversFresh(coreRef)) then acc += coreRef acc assert(refs.forall(_.isTerminalCapability)) diff --git a/compiler/src/dotty/tools/dotc/cc/Setup.scala b/compiler/src/dotty/tools/dotc/cc/Setup.scala index 1dac9de52f80..61956cd25ca7 100644 --- a/compiler/src/dotty/tools/dotc/cc/Setup.scala +++ b/compiler/src/dotty/tools/dotc/cc/Setup.scala @@ -955,7 +955,7 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI: case Nil => recur(cls.baseClasses.filter(_.isClassifiedCapabilityClass).distinct) if cls.derivesFrom(defn.Caps_SharedCapability) && cls.derivesFrom(defn.Caps_Mutable) then - report.error(em"$cls cannot inheit from both SharaedCapability and Mutable", cls.srcPos) + report.error(em"$cls cannot inheit from both SharedCapability and Mutable", cls.srcPos) // ------ Checks to run after main capture checking -------------------------- diff --git a/compiler/src/dotty/tools/dotc/core/Types.scala b/compiler/src/dotty/tools/dotc/core/Types.scala index 6bf19c5a27a1..ca9eda247cc0 100644 --- a/compiler/src/dotty/tools/dotc/core/Types.scala +++ b/compiler/src/dotty/tools/dotc/core/Types.scala @@ -6402,6 +6402,11 @@ object Types extends TypeUtils { mapCapability(c1) match case c2: Capability => c2.restrict(cls) case (cs: CaptureSet, exact) => (cs.restrict(cls), exact) + case ReadOnly(c1) => + assert(!deep) + mapCapability(c1) match + case c2: Capability => c2.readOnly + case (cs: CaptureSet, exact) => (cs.readOnly, exact) case Maybe(c1) => assert(!deep) mapCapability(c1) match diff --git a/tests/neg-custom-args/captures/check-inferred.check b/tests/neg-custom-args/captures/check-inferred.check index 8615fdcb218d..578b06508fd3 100644 --- a/tests/neg-custom-args/captures/check-inferred.check +++ b/tests/neg-custom-args/captures/check-inferred.check @@ -45,12 +45,12 @@ -- Error: tests/neg-custom-args/captures/check-inferred.scala:49:15 ---------------------------------------------------- 49 | private val y = ??? : (() => A^{cap.only[caps.Read]}) // error | ^ - | value y needs an explicit type because it captures a root capability in its type () => test.A^{cap.rd}. - | Fields capturing a root capability need to be given an explicit type unless the capability is already - | subsumed by the computed capability of the enclosing class. + | value y needs an explicit type because it captures a root capability in its type () => test.A^{cap.only[Read]}. + | Fields capturing a root capability need to be given an explicit type unless the capability is already + | subsumed by the computed capability of the enclosing class. | - | where: => refers to a fresh root capability in the type of value y - | cap is a fresh root capability created in value y + | where: => refers to a fresh root capability in the type of value y + | cap is a fresh root capability created in value y -- Error: tests/neg-custom-args/captures/check-inferred.scala:29:21 ---------------------------------------------------- 29 | private val count = Ref() // error | ^ diff --git a/tests/neg-custom-args/captures/classified-inheritance2.check b/tests/neg-custom-args/captures/classified-inheritance2.check index 49d079ee3840..87455916c072 100644 --- a/tests/neg-custom-args/captures/classified-inheritance2.check +++ b/tests/neg-custom-args/captures/classified-inheritance2.check @@ -1,4 +1,15 @@ -- Error: tests/neg-custom-args/captures/classified-inheritance2.scala:4:6 --------------------------------------------- 4 |class Logger extends SharedCapability, Mutable: // error (1) does this make sense? | ^ - | class Logger cannot inheit from both SharaedCapability and Mutable + | class Logger cannot inheit from both SharedCapability and Mutable +-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/classified-inheritance2.scala:12:27 ---------------------- +12 | val t: Logger^{} = Logger() // error + | ^^^^^^^^ + |Found: Logger^{cap.rd} + |Required: Logger^{} + | + |Note that capability cap.rd is not included in capture set {}. + | + |where: cap is a fresh root capability classified as SharedCapability created in value t when constructing instance Logger + | + | longer explanation available when compiling with `-explain` diff --git a/tests/neg-custom-args/captures/classified-inheritance2.scala b/tests/neg-custom-args/captures/classified-inheritance2.scala index 9281d44594af..301fb9fb473d 100644 --- a/tests/neg-custom-args/captures/classified-inheritance2.scala +++ b/tests/neg-custom-args/captures/classified-inheritance2.scala @@ -9,4 +9,4 @@ def onlyShared(x: Object^{cap.only[SharedCapability]}): Unit = () def main(): Unit = onlyShared(Logger()) // even if we allow (1), why would this type check? - val t: Logger^{} = Logger() // and this type checks too, thus the above line I guess \ No newline at end of file + val t: Logger^{} = Logger() // error \ No newline at end of file From aa4eeeaaacad034ff19873b5743d1ba421527a8c Mon Sep 17 00:00:00 2001 From: odersky Date: Mon, 17 Nov 2025 14:44:47 +0100 Subject: [PATCH 03/10] Expand level owner of unscoped fresh caps only where necessary --- .../src/dotty/tools/dotc/cc/Capability.scala | 23 ++++++++++++------- 1 file changed, 15 insertions(+), 8 deletions(-) diff --git a/compiler/src/dotty/tools/dotc/cc/Capability.scala b/compiler/src/dotty/tools/dotc/cc/Capability.scala index 36a03ececc96..b52737b11d02 100644 --- a/compiler/src/dotty/tools/dotc/cc/Capability.scala +++ b/compiler/src/dotty/tools/dotc/cc/Capability.scala @@ -512,35 +512,42 @@ object Capabilities: final def isParamPath(using Context): Boolean = paramPathRoot.exists - final def ccOwner(using Context): Symbol = this match + /** Compute ccOwner or (part of level owner). + * @param mapUnscoped if true, return the nclosing toplevel class for FreshCaps + * classified as Unscoped that don't have a prefix + */ + private def computeOwner(mapUnscoped: Boolean)(using Context): Symbol = this match case self: ThisType => self.cls - case TermRef(prefix: Capability, _) => prefix.ccOwner + case TermRef(prefix: Capability, _) => prefix.computeOwner(mapUnscoped) case self: NamedType => self.symbol - case self: DerivedCapability => self.underlying.ccOwner + case self: DerivedCapability => self.underlying.computeOwner(mapUnscoped) case self: FreshCap => val setOwner = self.hiddenSet.owner self.prefix match case prefix: ThisType if setOwner.isTerm && setOwner.owner == prefix.cls => setOwner - case prefix: Capability => prefix.ccOwner - case NoPrefix if classifier.derivesFrom(defn.Caps_Unscoped) => + case prefix: Capability => prefix.computeOwner(mapUnscoped) + case NoPrefix if mapUnscoped && classifier.derivesFrom(defn.Caps_Unscoped) => ctx.owner.topLevelClass case _ => setOwner case _ /* : GlobalCap | ResultCap | ParamRef */ => NoSymbol + final def ccOwner(using Context): Symbol = computeOwner(mapUnscoped = false) + final def visibility(using Context): Symbol = this match - case self: FreshCap => adjustOwner(ccOwner) + case self: FreshCap => adjustOwner(computeOwner(mapUnscoped = true)) case _ => - val vis = ccOwner + val vis = computeOwner(mapUnscoped = true) if vis.is(Param) then vis.owner else vis /** The symbol that represents the level closest-enclosing ccOwner. * Symbols representing levels are * - class symbols, but not inner (non-static) module classes * - method symbols, but not accessors or constructors + * For Unscoped FreshCaps the level owner is the top-level class. */ final def levelOwner(using Context): Symbol = - adjustOwner(ccOwner) + adjustOwner(computeOwner(mapUnscoped = true)) private def adjustOwner(owner: Symbol)(using Context): Symbol = if !owner.exists From 2e033a2dc6673606107f654fb2a486a465362318 Mon Sep 17 00:00:00 2001 From: odersky Date: Tue, 18 Nov 2025 13:35:53 +0100 Subject: [PATCH 04/10] Consume Unscoped caps assigned to outer variables Also: Improve consume message --- .../src/dotty/tools/dotc/cc/Capability.scala | 2 +- .../src/dotty/tools/dotc/cc/SepCheck.scala | 100 +++++++++++++----- .../captures/classified-inheritance.check | 2 +- .../captures/classified-inheritance.scala | 2 +- tests/neg-custom-args/captures/i24373.check | 17 ++- tests/neg-custom-args/captures/i24373a.check | 38 +++---- .../captures/linear-buffer-2.check | 30 +++--- .../captures/linear-buffer.check | 35 +++--- .../captures/sep-consume.check | 12 +-- .../captures/sep-curried-par.check | 7 +- .../neg-custom-args/captures/sepchecks5.check | 7 +- .../captures/unscoped-classifier.check | 30 ++++++ .../captures/unscoped-classifier.scala | 21 ++++ .../captures/unscoped-extrude.check | 7 ++ .../captures/unscoped-extrude.scala | 16 +++ 15 files changed, 210 insertions(+), 116 deletions(-) create mode 100644 tests/neg-custom-args/captures/unscoped-classifier.check create mode 100644 tests/neg-custom-args/captures/unscoped-classifier.scala create mode 100644 tests/neg-custom-args/captures/unscoped-extrude.check create mode 100644 tests/neg-custom-args/captures/unscoped-extrude.scala diff --git a/compiler/src/dotty/tools/dotc/cc/Capability.scala b/compiler/src/dotty/tools/dotc/cc/Capability.scala index b52737b11d02..b451242d410d 100644 --- a/compiler/src/dotty/tools/dotc/cc/Capability.scala +++ b/compiler/src/dotty/tools/dotc/cc/Capability.scala @@ -549,7 +549,7 @@ object Capabilities: final def levelOwner(using Context): Symbol = adjustOwner(computeOwner(mapUnscoped = true)) - private def adjustOwner(owner: Symbol)(using Context): Symbol = + final def adjustOwner(owner: Symbol)(using Context): Symbol = if !owner.exists || owner.isClass && (!owner.is(Flags.Module) || owner.isStatic) || owner.is(Flags.Method, butNot = Flags.Accessor) diff --git a/compiler/src/dotty/tools/dotc/cc/SepCheck.scala b/compiler/src/dotty/tools/dotc/cc/SepCheck.scala index 0de12c7cd1e9..645f7b96a3c2 100644 --- a/compiler/src/dotty/tools/dotc/cc/SepCheck.scala +++ b/compiler/src/dotty/tools/dotc/cc/SepCheck.scala @@ -46,8 +46,9 @@ object SepCheck: /** The role in which a checked type appears, used for composing error messages */ enum TypeRole: case Result(sym: Symbol, inferred: Boolean) - case Argument(arg: Tree) + case Argument(arg: Tree, meth: Symbol) case Qualifier(qual: Tree, meth: Symbol) + case RHS(rhs: Tree, mvar: Symbol) /** If this is a Result tole, the associated symbol, otherwise NoSymbol */ def dclSym = this match @@ -59,11 +60,20 @@ object SepCheck: case Result(sym, inferred) => def inferredStr = if inferred then " inferred" else "" def resultStr = if sym.info.isInstanceOf[MethodicType] then " result" else "" - i"$sym's$inferredStr$resultStr type" - case TypeRole.Argument(_) => + i"${sym.sanitizedDescription}'s$inferredStr$resultStr type" + case TypeRole.Argument(_, _) => "the argument's adapted type" case TypeRole.Qualifier(_, meth) => - i"the type of the prefix to a call of $meth" + i"the type of the prefix to a call of ${meth.sanitizedDescription}" + case RHS(rhs, lhsSym) => + i"the type of the value assigned to $lhsSym" + + /** A description how a reference was consumed in this role */ + def howConsumed(using Context): String = this match + case TypeRole.Result(meth, _) => i"returned in the result of ${meth.sanitizedDescription}" + case TypeRole.Argument(_, meth) => i"passed as a consume parameter to ${meth.sanitizedDescription}" + case TypeRole.Qualifier(_, meth) => i"used as a prefix to consume ${meth.sanitizedDescription}" + case TypeRole.RHS(_, mvar) => i"consumed in an assignment to $mvar" end TypeRole /** A class for segmented sets of consumed references. @@ -74,13 +84,13 @@ object SepCheck: /** The references in the set. The array should be treated as immutable in client code */ def refs: Array[Capability] - /** The associated source positoons. The array should be treated as immutable in client code */ - def locs: Array[SrcPos] + /** The associated source positoons and type roles. The array should be treated as immutable in client code */ + def locs: Array[(SrcPos, TypeRole)] /** The number of references in the set */ def size: Int - def toMap: Map[Capability, SrcPos] = refs.take(size).zip(locs).toMap + def toMap: Map[Capability, (SrcPos, TypeRole)] = refs.take(size).zip(locs).toMap def show(using Context) = s"[${toMap.map((ref, loc) => i"$ref -> $loc").toList}]" @@ -89,13 +99,13 @@ object SepCheck: /** A fixed consumed set consisting of the given references `refs` and * associated source positions `locs` */ - class ConstConsumedSet(val refs: Array[Capability], val locs: Array[SrcPos]) extends ConsumedSet: + class ConstConsumedSet(val refs: Array[Capability], val locs: Array[(SrcPos, TypeRole)]) extends ConsumedSet: def size = refs.size /** A mutable consumed set, which is initially empty */ class MutConsumedSet extends ConsumedSet: var refs: Array[Capability] = new Array(4) - var locs: Array[SrcPos] = new Array(4) + var locs: Array[(SrcPos, TypeRole)] = new Array(4) var size = 0 var directPeaks : Refs = emptyRefs @@ -110,12 +120,12 @@ object SepCheck: locs = double(locs) /** If `ref` is in the set, its associated source position, otherwise `null` */ - def get(ref: Capability): SrcPos | Null = + def get(ref: Capability): (SrcPos, TypeRole) | Null = var i = 0 while i < size && (refs(i) ne ref) do i += 1 if i < size then locs(i) else null - def clashing(ref: Capability)(using Context): SrcPos | Null = + def clashing(ref: Capability)(using Context): (SrcPos, TypeRole) | Null = val refPeaks = ref.directPeaks if !directPeaks.sharedPeaks(refPeaks).isEmpty then var i = 0 @@ -126,7 +136,7 @@ object SepCheck: else null /** If `ref` is not yet in the set, add it with given source position */ - def put(ref: Capability, loc: SrcPos)(using Context): Unit = + def put(ref: Capability, loc: (SrcPos, TypeRole))(using Context): Unit = if get(ref) == null then ensureCapacity(1) refs(size) = ref @@ -448,21 +458,22 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser: * @param loc the position where the capability was consumed * @param pos the position where the capability was used again */ - def consumeError(ref: Capability, loc: SrcPos, pos: SrcPos)(using Context): Unit = + def consumeError(ref: Capability, loc: (SrcPos, TypeRole), pos: SrcPos)(using Context): Unit = + val (locPos, role) = loc report.error( - em"""Separation failure: Illegal access to $ref, which was passed to a - |consume parameter or was used as a prefix to a consume method on line ${loc.line + 1} - |and therefore is no longer available.""", + em"""Separation failure: Illegal access to $ref, which was ${role.howConsumed} + |on line ${locPos.line + 1} and therefore is no longer available.""", pos) /** Report a failure where a capability is consumed in a loop. * @param ref the capability * @param pos the position where the capability was consumed */ - def consumeInLoopError(ref: Capability, pos: SrcPos)(using Context): Unit = + def consumeInLoopError(ref: Capability, loc: (SrcPos, TypeRole))(using Context): Unit = + val (pos, role) = loc report.error( em"""Separation failure: $ref appears in a loop, therefore it cannot - |be passed to a consume parameter or be used as a prefix of a consume method call.""", + |be ${role.howConsumed}.""", pos) // ------------ Checks ----------------------------------------------------- @@ -535,7 +546,7 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser: if arg.needsSepCheck then //println(i"testing $arg, formal = ${arg.formalType}, peaks = ${argPeaks.actual}/${argPeaks.hidden} against ${currentPeaks.actual}") - checkType(arg.formalType, arg.srcPos, TypeRole.Argument(arg)) + checkType(arg.formalType, arg.srcPos, TypeRole.Argument(arg, fn.symbol)) // 2. test argPeaks.hidden against previously captured actuals if !argPeaks.hidden.sharedPeaks(currentPeaks.actual).isEmpty then val clashing = clashingPart(argPeaks.hidden, _.actual) @@ -558,6 +569,35 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser: sepApplyError(fn, parts, arg, app) end checkApply + def checkAssign(tree: Assign)(using Context): Unit = + val Assign(lhs, rhs) = tree + lhs.nuType match + case lhsType: ObjectCapability if lhsType.pathOwner.exists => + val lhsOwner = lhsType.pathOwner + + /** A reference escapes into an outer var if it would have produced a + * level error if it did not have an Unscoped, unprefixed FreshCap + * in some underlying capture set. + */ + def escapes(ref: Capability): Boolean = ref.pathRoot match + case ref @ FreshCap(NoPrefix) + if ref.classifier.derivesFrom(defn.Caps_Unscoped) => + // we have an escaping reference if the FreshCap's adjustded owner + // is properly contained inside the scope of the variable. + ref.adjustOwner(ref.ccOwner).isProperlyContainedIn(lhsOwner) + case _ => + ref.visibility.isProperlyContainedIn(lhsOwner) // ref itself is not levelOK + && !ref.isTerminalCapability // ... and ... + && ref.captureSetOfInfo.elems.exists(escapes) // some underlying capability escapes + + val escaping = spanCaptures(rhs).filter(escapes) + capt.println(i"check assign $tree, $lhsOwner, escaping = $escaping, ${escaping.directFootprint.nonPeaks}") + checkConsumedRefs(escaping.directFootprint.nonPeaks, rhs.nuType, + TypeRole.RHS(rhs, lhs.symbol), + s"the value assigned to ${lhs.symbol} refers to", tree.srcPos) + case _ => + end checkAssign + /** 1. Check that the capabilities used at `tree` don't overlap with * capabilities hidden by a previous definition. * 2. Also check that none of the used capabilities was consumed before. @@ -567,7 +607,6 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser: if !used.isEmpty then capt.println(i"check use $tree: $used") val usedPeaks = used.allPeaks - val overlap = defsShadow.allPeaks.sharedPeaks(usedPeaks) if !defsShadow.allPeaks.sharedPeaks(usedPeaks).isEmpty then // Drop all Selects unless they select from a `this` def pathRoot(tree: Tree): Tree = tree match @@ -595,10 +634,10 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser: end if for ref <- used do - val pos = consumed.clashing(ref) - if pos != null then + val loc = consumed.clashing(ref) + if loc != null then // println(i"consumed so far ${consumed.refs.toList} with peaks ${consumed.directPeaks.toList}, used = $used, exposed = ${ref.directPeaks }") - consumeError(ref, pos, tree.srcPos) + consumeError(ref, loc, tree.srcPos) end checkUse /** If `tp` denotes some version of a singleton capability `x.type` the set `{x, x*}` @@ -673,10 +712,10 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser: pos) role match - case _: TypeRole.Argument | _: TypeRole.Qualifier => + case _: TypeRole.Argument | _: TypeRole.Qualifier | _: TypeRole.RHS => for ref <- refsToCheck do if !ref.stripReadOnly.isKnownClassifiedAs(defn.Caps_SharedCapability) then - consumed.put(ref, pos) + consumed.put(ref, (pos, role)) case _ => end checkConsumedRefs @@ -696,7 +735,7 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser: */ extension (refs: Refs) def pruned = val deductedType = role match - case TypeRole.Argument(arg) => arg.tpe + case TypeRole.Argument(arg, _) => arg.tpe case _ => tpe refs.deductSymRefs(role.dclSym).deduct(explicitRefs(deductedType)) @@ -809,7 +848,7 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser: val refs = tpe.deepCaptureSet.elems val toCheck = refs.transHiddenSet.directFootprint.nonPeaks.deduct(refs.directFootprint.nonPeaks) checkConsumedRefs(toCheck, tpe, role, i"${role.description} $tpe hides", pos) - case TypeRole.Argument(arg) => + case TypeRole.Argument(arg, _) => if tpe.hasAnnotation(defn.ConsumeAnnot) then val capts = spanCaptures(arg).directFootprint.nonPeaks checkConsumedRefs(capts, tpe, role, i"argument to consume parameter with type ${arg.nuType} refers to", pos) @@ -982,6 +1021,9 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser: tree.tpe match case _: MethodOrPoly => case _ => traverseApply(tree) + case tree: Assign => + traverseChildren(tree) + checkAssign(tree) case _: Block | _: Template => traverseSection(tree) case tree: ValDef => @@ -1029,8 +1071,8 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser: case tree: WhileDo => val loopConsumed = consumed.segment(traverseChildren(tree)) if loopConsumed.size != 0 then - val (ref, pos) = loopConsumed.toMap.head - consumeInLoopError(ref, pos) + val (ref, loc) = loopConsumed.toMap.head + consumeInLoopError(ref, loc) case _ => traverseChildren(tree) end SepCheck diff --git a/tests/neg-custom-args/captures/classified-inheritance.check b/tests/neg-custom-args/captures/classified-inheritance.check index 6f34d52a4b7a..aa182bfafce4 100644 --- a/tests/neg-custom-args/captures/classified-inheritance.check +++ b/tests/neg-custom-args/captures/classified-inheritance.check @@ -5,4 +5,4 @@ -- Error: tests/neg-custom-args/captures/classified-inheritance.scala:10:6 --------------------------------------------- 10 |class C3 extends Matrix, Async // error | ^ - | class C3 inherits two unrelated classifier traits: trait Control and trait Read + | class C3 inherits two unrelated classifier traits: trait Control and trait Unscoped diff --git a/tests/neg-custom-args/captures/classified-inheritance.scala b/tests/neg-custom-args/captures/classified-inheritance.scala index 78ac5c779271..d48f410b4f7d 100644 --- a/tests/neg-custom-args/captures/classified-inheritance.scala +++ b/tests/neg-custom-args/captures/classified-inheritance.scala @@ -5,6 +5,6 @@ class C1 extends caps.Control, caps.SharedCapability // OK class C2 extends caps.Control, caps.Read // error trait Async extends caps.Control -class Matrix extends caps.Read +class Matrix extends caps.Unscoped class C3 extends Matrix, Async // error diff --git a/tests/neg-custom-args/captures/i24373.check b/tests/neg-custom-args/captures/i24373.check index 9a2dcbc646f4..08e196fc1dc9 100644 --- a/tests/neg-custom-args/captures/i24373.check +++ b/tests/neg-custom-args/captures/i24373.check @@ -1,24 +1,21 @@ -- Error: tests/neg-custom-args/captures/i24373.scala:28:2 ------------------------------------------------------------- 28 | x1.sink1 // error | ^^ - | Separation failure: Illegal access to (x1 : Foo^), which was passed to a - | consume parameter or was used as a prefix to a consume method on line 27 - | and therefore is no longer available. + | Separation failure: Illegal access to (x1 : Foo^), which was used as a prefix to consume method sink1 + | on line 27 and therefore is no longer available. | | where: ^ refers to a fresh root capability in the type of value x1 -- Error: tests/neg-custom-args/captures/i24373.scala:32:2 ------------------------------------------------------------- 32 | x2.sink2 // error | ^^ - | Separation failure: Illegal access to (x2 : Bar^), which was passed to a - | consume parameter or was used as a prefix to a consume method on line 31 - | and therefore is no longer available. + | Separation failure: Illegal access to (x2 : Bar^), which was used as a prefix to consume method sink2 + | on line 31 and therefore is no longer available. | | where: ^ refers to a fresh root capability in the type of value x2 -- Error: tests/neg-custom-args/captures/i24373.scala:49:8 ------------------------------------------------------------- 49 | sink6(x6) // error | ^^ - | Separation failure: Illegal access to (x6 : Bar^), which was passed to a - | consume parameter or was used as a prefix to a consume method on line 48 - | and therefore is no longer available. + | Separation failure: Illegal access to (x6 : Bar^), which was passed as a consume parameter to method sink6 + | on line 48 and therefore is no longer available. | - | where: ^ refers to a fresh root capability in the type of value x6 + | where: ^ refers to a fresh root capability in the type of value x6 diff --git a/tests/neg-custom-args/captures/i24373a.check b/tests/neg-custom-args/captures/i24373a.check index 5c6c12a746f2..61198e8cc676 100644 --- a/tests/neg-custom-args/captures/i24373a.check +++ b/tests/neg-custom-args/captures/i24373a.check @@ -1,44 +1,38 @@ -- Error: tests/neg-custom-args/captures/i24373a.scala:15:8 ------------------------------------------------------------ 15 | sink2(x1) // error | ^^ - | Separation failure: Illegal access to (x1 : Bar^), which was passed to a - | consume parameter or was used as a prefix to a consume method on line 13 - | and therefore is no longer available. + | Separation failure: Illegal access to (x1 : Bar^), which was passed as a consume parameter to method sink1 + | on line 13 and therefore is no longer available. | - | where: ^ refers to a fresh root capability in the type of value x1 + | where: ^ refers to a fresh root capability in the type of value x1 -- Error: tests/neg-custom-args/captures/i24373a.scala:19:8 ------------------------------------------------------------ 19 | sink1(x2) // error | ^^ - | Separation failure: Illegal access to x2.rd, which was passed to a - | consume parameter or was used as a prefix to a consume method on line 18 - | and therefore is no longer available. + | Separation failure: Illegal access to x2.rd, which was passed as a consume parameter to method sink2 + | on line 18 and therefore is no longer available. -- Error: tests/neg-custom-args/captures/i24373a.scala:20:8 ------------------------------------------------------------ 20 | sink2(x2) // error | ^^ - | Separation failure: Illegal access to (x2 : Bar^), which was passed to a - | consume parameter or was used as a prefix to a consume method on line 18 - | and therefore is no longer available. + | Separation failure: Illegal access to (x2 : Bar^), which was passed as a consume parameter to method sink2 + | on line 18 and therefore is no longer available. | - | where: ^ refers to a fresh root capability in the type of value x2 + | where: ^ refers to a fresh root capability in the type of value x2 -- Error: tests/neg-custom-args/captures/i24373a.scala:25:8 ------------------------------------------------------------ 25 | sink2(x3) // error | ^^ - | Separation failure: Illegal access to (x3 : Bar^), which was passed to a - | consume parameter or was used as a prefix to a consume method on line 23 - | and therefore is no longer available. + | Separation failure: Illegal access to (x3 : Bar^), which was passed as a consume parameter to method sink3 + | on line 23 and therefore is no longer available. | - | where: ^ refers to a fresh root capability in the type of value x3 + | where: ^ refers to a fresh root capability in the type of value x3 -- Error: tests/neg-custom-args/captures/i24373a.scala:29:8 ------------------------------------------------------------ 29 | sink3(x4) // error | ^^ - | Separation failure: Illegal access to x4.rd, which was passed to a - | consume parameter or was used as a prefix to a consume method on line 28 - | and therefore is no longer available. + | Separation failure: Illegal access to x4.rd, which was passed as a consume parameter to method sink2 + | on line 28 and therefore is no longer available. -- Error: tests/neg-custom-args/captures/i24373a.scala:30:8 ------------------------------------------------------------ 30 | sink2(x4) // error | ^^ - | Separation failure: Illegal access to (x4 : Bar^), which was passed to a - | consume parameter or was used as a prefix to a consume method on line 28 - | and therefore is no longer available. + | Separation failure: Illegal access to (x4 : Bar^), which was passed as a consume parameter to method sink2 + | on line 28 and therefore is no longer available. | - | where: ^ refers to a fresh root capability in the type of value x4 + | where: ^ refers to a fresh root capability in the type of value x4 diff --git a/tests/neg-custom-args/captures/linear-buffer-2.check b/tests/neg-custom-args/captures/linear-buffer-2.check index 63cb8472fc05..ae70cb3aa249 100644 --- a/tests/neg-custom-args/captures/linear-buffer-2.check +++ b/tests/neg-custom-args/captures/linear-buffer-2.check @@ -1,39 +1,35 @@ -- Error: tests/neg-custom-args/captures/linear-buffer-2.scala:13:13 --------------------------------------------------- 13 | val buf3 = buf.append(3) // error | ^^^ - | Separation failure: Illegal access to (buf : Buffer[Int]^), which was passed to a - | consume parameter or was used as a prefix to a consume method on line 11 - | and therefore is no longer available. + | Separation failure: Illegal access to (buf : Buffer[Int]^), which was used as a prefix to consume method append + | on line 11 and therefore is no longer available. | - | where: ^ refers to a fresh root capability in the type of parameter buf + | where: ^ refers to a fresh root capability in the type of parameter buf -- Error: tests/neg-custom-args/captures/linear-buffer-2.scala:20:13 --------------------------------------------------- 20 | val buf3 = buf1.append(4) // error | ^^^^ - | Separation failure: Illegal access to (buf1 : Buffer[Int]^), which was passed to a - | consume parameter or was used as a prefix to a consume method on line 18 - | and therefore is no longer available. + |Separation failure: Illegal access to (buf1 : Buffer[Int]^), which was used as a prefix to consume method append + |on line 18 and therefore is no longer available. | - | where: ^ refers to a fresh root capability in the type of value buf1 + |where: ^ refers to a fresh root capability in the type of value buf1 -- Error: tests/neg-custom-args/captures/linear-buffer-2.scala:28:13 --------------------------------------------------- 28 | val buf3 = buf1.append(4) // error | ^^^^ - | Separation failure: Illegal access to (buf1 : Buffer[Int]^), which was passed to a - | consume parameter or was used as a prefix to a consume method on line 25 - | and therefore is no longer available. + |Separation failure: Illegal access to (buf1 : Buffer[Int]^), which was used as a prefix to consume method append + |on line 25 and therefore is no longer available. | - | where: ^ refers to a fresh root capability in the type of value buf1 + |where: ^ refers to a fresh root capability in the type of value buf1 -- Error: tests/neg-custom-args/captures/linear-buffer-2.scala:38:13 --------------------------------------------------- 38 | val buf3 = buf1.append(4) // error | ^^^^ - | Separation failure: Illegal access to (buf1 : Buffer[Int]^), which was passed to a - | consume parameter or was used as a prefix to a consume method on line 33 - | and therefore is no longer available. + |Separation failure: Illegal access to (buf1 : Buffer[Int]^), which was used as a prefix to consume method append + |on line 33 and therefore is no longer available. | - | where: ^ refers to a fresh root capability in the type of value buf1 + |where: ^ refers to a fresh root capability in the type of value buf1 -- Error: tests/neg-custom-args/captures/linear-buffer-2.scala:42:4 ---------------------------------------------------- 42 | buf.append(1) // error | ^^^ | Separation failure: (buf : Buffer[Int]^) appears in a loop, therefore it cannot - | be passed to a consume parameter or be used as a prefix of a consume method call. + | be used as a prefix to consume method append. | | where: ^ refers to a fresh root capability in the type of parameter buf diff --git a/tests/neg-custom-args/captures/linear-buffer.check b/tests/neg-custom-args/captures/linear-buffer.check index 8cda7660cd5b..97d0409e55ed 100644 --- a/tests/neg-custom-args/captures/linear-buffer.check +++ b/tests/neg-custom-args/captures/linear-buffer.check @@ -36,45 +36,40 @@ -- Error: tests/neg-custom-args/captures/linear-buffer.scala:23:17 ----------------------------------------------------- 23 | val buf3 = app(buf, 3) // error | ^^^ - | Separation failure: Illegal access to (buf : Buffer[Int]^), which was passed to a - | consume parameter or was used as a prefix to a consume method on line 21 - | and therefore is no longer available. + |Separation failure: Illegal access to (buf : Buffer[Int]^), which was passed as a consume parameter to method app + |on line 21 and therefore is no longer available. | - | where: ^ refers to a fresh root capability in the type of parameter buf + |where: ^ refers to a fresh root capability in the type of parameter buf -- Error: tests/neg-custom-args/captures/linear-buffer.scala:30:17 ----------------------------------------------------- 30 | val buf3 = app(buf1, 4) // error | ^^^^ - | Separation failure: Illegal access to (buf1 : Buffer[Int]^), which was passed to a - | consume parameter or was used as a prefix to a consume method on line 28 - | and therefore is no longer available. + |Separation failure: Illegal access to (buf1 : Buffer[Int]^), which was passed as a consume parameter to method app + |on line 28 and therefore is no longer available. | - | where: ^ refers to a fresh root capability in the type of value buf1 + |where: ^ refers to a fresh root capability in the type of value buf1 -- Error: tests/neg-custom-args/captures/linear-buffer.scala:38:17 ----------------------------------------------------- 38 | val buf3 = app(buf1, 4) // error | ^^^^ - | Separation failure: Illegal access to (buf1 : Buffer[Int]^), which was passed to a - | consume parameter or was used as a prefix to a consume method on line 35 - | and therefore is no longer available. + |Separation failure: Illegal access to (buf1 : Buffer[Int]^), which was passed as a consume parameter to method app + |on line 35 and therefore is no longer available. | - | where: ^ refers to a fresh root capability in the type of value buf1 + |where: ^ refers to a fresh root capability in the type of value buf1 -- Error: tests/neg-custom-args/captures/linear-buffer.scala:48:17 ----------------------------------------------------- 48 | val buf3 = app(buf1, 4) // error | ^^^^ - | Separation failure: Illegal access to (buf1 : Buffer[Int]^), which was passed to a - | consume parameter or was used as a prefix to a consume method on line 43 - | and therefore is no longer available. + |Separation failure: Illegal access to (buf1 : Buffer[Int]^), which was passed as a consume parameter to method app + |on line 43 and therefore is no longer available. | - | where: ^ refers to a fresh root capability in the type of value buf1 + |where: ^ refers to a fresh root capability in the type of value buf1 -- Error: tests/neg-custom-args/captures/linear-buffer.scala:52:8 ------------------------------------------------------ 52 | app(buf, 1) // error | ^^^ | Separation failure: (buf : Buffer[Int]^) appears in a loop, therefore it cannot - | be passed to a consume parameter or be used as a prefix of a consume method call. + | be passed as a consume parameter to method app. | | where: ^ refers to a fresh root capability in the type of parameter buf -- Error: tests/neg-custom-args/captures/linear-buffer.scala:62:20 ----------------------------------------------------- 62 | val c3 = contents(buf) // error | ^^^ - | Separation failure: Illegal access to buf.rd, which was passed to a - | consume parameter or was used as a prefix to a consume method on line 59 - | and therefore is no longer available. + | Separation failure: Illegal access to buf.rd, which was passed as a consume parameter to method app + | on line 59 and therefore is no longer available. diff --git a/tests/neg-custom-args/captures/sep-consume.check b/tests/neg-custom-args/captures/sep-consume.check index 0d1a4df1e98e..5854c52cd84b 100644 --- a/tests/neg-custom-args/captures/sep-consume.check +++ b/tests/neg-custom-args/captures/sep-consume.check @@ -1,19 +1,17 @@ -- Error: tests/neg-custom-args/captures/sep-consume.scala:19:2 -------------------------------------------------------- 19 | x.put(42) // error | ^ - | Separation failure: Illegal access to (x : Ref^), which was passed to a - | consume parameter or was used as a prefix to a consume method on line 18 - | and therefore is no longer available. + | Separation failure: Illegal access to (x : Ref^), which was passed as a consume parameter to method bad + | on line 18 and therefore is no longer available. | | where: ^ refers to a fresh root capability in the type of parameter x -- Error: tests/neg-custom-args/captures/sep-consume.scala:21:16 ------------------------------------------------------- 21 | par(rx, () => x.put(42)) // error | ^ - | Separation failure: Illegal access to (x : Ref^), which was passed to a - | consume parameter or was used as a prefix to a consume method on line 18 - | and therefore is no longer available. + | Separation failure: Illegal access to (x : Ref^), which was passed as a consume parameter to method bad + | on line 18 and therefore is no longer available. | - | where: ^ refers to a fresh root capability in the type of parameter x + | where: ^ refers to a fresh root capability in the type of parameter x -- Error: tests/neg-custom-args/captures/sep-consume.scala:26:16 ------------------------------------------------------- 26 | def foo = bad(f) // error | ^ diff --git a/tests/neg-custom-args/captures/sep-curried-par.check b/tests/neg-custom-args/captures/sep-curried-par.check index 746b5d041338..2172c5699fa8 100644 --- a/tests/neg-custom-args/captures/sep-curried-par.check +++ b/tests/neg-custom-args/captures/sep-curried-par.check @@ -36,11 +36,10 @@ -- Error: tests/neg-custom-args/captures/sep-curried-par.scala:18:16 --------------------------------------------------- 18 | parCurried(p)(p) // error: consume failure | ^ - | Separation failure: Illegal access to (p : () => Unit), which was passed to a - | consume parameter or was used as a prefix to a consume method on line 18 - | and therefore is no longer available. + |Separation failure: Illegal access to (p : () => Unit), which was passed as a consume parameter to method parCurried + |on line 18 and therefore is no longer available. | - | where: => refers to a fresh root capability in the type of value p + |where: => refers to a fresh root capability in the type of value p -- Error: tests/neg-custom-args/captures/sep-curried-par.scala:21:9 ---------------------------------------------------- 21 | foo(c)(c) // error: separation | ^ diff --git a/tests/neg-custom-args/captures/sepchecks5.check b/tests/neg-custom-args/captures/sepchecks5.check index 9f76ef21f46d..ab7ae86a9cef 100644 --- a/tests/neg-custom-args/captures/sepchecks5.check +++ b/tests/neg-custom-args/captures/sepchecks5.check @@ -11,8 +11,7 @@ -- Error: tests/neg-custom-args/captures/sepchecks5.scala:20:24 -------------------------------------------------------- 20 | par(f2)(() => println(io)) // error | ^^ - | Separation failure: Illegal access to (io : Object^), which was passed to a - | consume parameter or was used as a prefix to a consume method on line 19 - | and therefore is no longer available. + | Separation failure: Illegal access to (io : Object^), which was passed as a consume parameter to method g + | on line 19 and therefore is no longer available. | - | where: ^ refers to a fresh root capability in the type of parameter io + | where: ^ refers to a fresh root capability in the type of parameter io diff --git a/tests/neg-custom-args/captures/unscoped-classifier.check b/tests/neg-custom-args/captures/unscoped-classifier.check new file mode 100644 index 000000000000..c14a151105e5 --- /dev/null +++ b/tests/neg-custom-args/captures/unscoped-classifier.check @@ -0,0 +1,30 @@ +-- Error: tests/neg-custom-args/captures/unscoped-classifier.scala:5:8 ------------------------------------------------- +5 |class A(a: Async) extends caps.Unscoped // error but msg could be better + | ^ + | reference (A.this.a : Async) is not included in the allowed capture set {cap} of the self type of class A + | + | where: cap is a fresh root capability classified as Unscoped in the type of class A +-- Error: tests/neg-custom-args/captures/unscoped-classifier.scala:10:8 ------------------------------------------------ +10 |class C(f: () => Unit) extends caps.Unscoped // error but msg could be better + | ^ + | reference (C.this.f : () => Unit) is not included in the allowed capture set {cap} of the self type of class C + | + | where: cap is a fresh root capability classified as Unscoped in the type of class C +-- Error: tests/neg-custom-args/captures/unscoped-classifier.scala:17:15 ----------------------------------------------- +17 | def gg() = g() // error but msg could be better + | ^ + | reference (g : () => Unit) is not included in the allowed capture set {cap} of the self type of class E + | + | where: cap is a fresh root capability classified as Unscoped in the type of class E +-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/unscoped-classifier.scala:19:11 -------------------------- +19 | val b = B() // error but msg could be better + | ^^^ + |Found: B^ + |Required: B^'s1 + | + |Note that capability cap is not classified as trait Unscoped, therefore it + |cannot be included in capture set 's1 of value b of Unscoped elements. + | + |where: ^ and cap refer to a fresh root capability classified as Nothing created in value b when constructing instance B + | + | longer explanation available when compiling with `-explain` diff --git a/tests/neg-custom-args/captures/unscoped-classifier.scala b/tests/neg-custom-args/captures/unscoped-classifier.scala new file mode 100644 index 000000000000..12493963b827 --- /dev/null +++ b/tests/neg-custom-args/captures/unscoped-classifier.scala @@ -0,0 +1,21 @@ +import caps.* + +trait Async extends Control + +class A(a: Async) extends caps.Unscoped // error but msg could be better + +class B extends caps.Unscoped: + val a: Async^ = new Async {} // ok (should this be an error instead?) + +class C(f: () => Unit) extends caps.Unscoped // error but msg could be better + +class D extends caps.Unscoped: + val f: () => Unit = ??? // ok (should this be an error instead?) + +def test(g: () => Unit) = + class E extends caps.Unscoped: + def gg() = g() // error but msg could be better + + val b = B() // error but msg could be better + val d = D() // ok (?) + val _: D^{cap.only[Unscoped]} = d diff --git a/tests/neg-custom-args/captures/unscoped-extrude.check b/tests/neg-custom-args/captures/unscoped-extrude.check new file mode 100644 index 000000000000..b59c6bc2fb48 --- /dev/null +++ b/tests/neg-custom-args/captures/unscoped-extrude.check @@ -0,0 +1,7 @@ +-- Error: tests/neg-custom-args/captures/unscoped-extrude.scala:13:4 --------------------------------------------------- +13 | r // error + | ^ + | Separation failure: Illegal access to (r : Ref[String]^), which was consumed in an assignment to variable x + | on line 12 and therefore is no longer available. + | + | where: ^ refers to a fresh root capability classified as Unscoped in the type of value r diff --git a/tests/neg-custom-args/captures/unscoped-extrude.scala b/tests/neg-custom-args/captures/unscoped-extrude.scala new file mode 100644 index 000000000000..20179e4d84ba --- /dev/null +++ b/tests/neg-custom-args/captures/unscoped-extrude.scala @@ -0,0 +1,16 @@ +import caps.* + +class Ref[T](init: T) extends Mutable, Unscoped: + var x = init + def get: T = x + update def put(y: T): Unit = x = y + +def Test = + var x: Ref[String]^ = Ref("x") + def foo(): Ref[String]^ = + val r = Ref("y") + x = r // should be consumed here + r // error + + + From 8f96f289d1889457bef5fd94dd279bb87219ca3b Mon Sep 17 00:00:00 2001 From: odersky Date: Tue, 18 Nov 2025 13:54:17 +0100 Subject: [PATCH 05/10] Drop `Read` as a classifier --- library/src/scala/caps/package.scala | 3 ++- tests/neg-custom-args/captures/check-inferred.check | 12 ++++++------ tests/neg-custom-args/captures/check-inferred.scala | 2 +- .../captures/classified-inheritance.check | 4 ++-- .../captures/classified-inheritance.scala | 2 +- tests/neg-custom-args/captures/classifiers-1.scala | 2 +- tests/pos-custom-args/captures/restrict-try.scala | 4 ++-- .../stdlibExperimentalDefinitions.scala | 1 + 8 files changed, 16 insertions(+), 14 deletions(-) diff --git a/library/src/scala/caps/package.scala b/library/src/scala/caps/package.scala index c4914549a75c..a04a5690df7d 100644 --- a/library/src/scala/caps/package.scala +++ b/library/src/scala/caps/package.scala @@ -84,7 +84,8 @@ trait Mutable extends ExclusiveCapability /** Marker trait for classes with reader methods, typically extended by Mutable classes */ @experimental -trait Read extends Mutable, Classifier +@deprecated +trait Read extends Mutable /** Marker trait for classes that are not subject to scoping restrictions * of captured capabilities. diff --git a/tests/neg-custom-args/captures/check-inferred.check b/tests/neg-custom-args/captures/check-inferred.check index 578b06508fd3..968aa9dfe244 100644 --- a/tests/neg-custom-args/captures/check-inferred.check +++ b/tests/neg-custom-args/captures/check-inferred.check @@ -43,14 +43,14 @@ | | where: ^ refers to a fresh root capability in the type of value y -- Error: tests/neg-custom-args/captures/check-inferred.scala:49:15 ---------------------------------------------------- -49 | private val y = ??? : (() => A^{cap.only[caps.Read]}) // error +49 | private val y = ??? : (() => A^{cap.only[caps.Unscoped]}) // error | ^ - | value y needs an explicit type because it captures a root capability in its type () => test.A^{cap.only[Read]}. - | Fields capturing a root capability need to be given an explicit type unless the capability is already - | subsumed by the computed capability of the enclosing class. + |value y needs an explicit type because it captures a root capability in its type () => test.A^{cap.only[Unscoped]}. + |Fields capturing a root capability need to be given an explicit type unless the capability is already + |subsumed by the computed capability of the enclosing class. | - | where: => refers to a fresh root capability in the type of value y - | cap is a fresh root capability created in value y + |where: => refers to a fresh root capability in the type of value y + | cap is a fresh root capability created in value y -- Error: tests/neg-custom-args/captures/check-inferred.scala:29:21 ---------------------------------------------------- 29 | private val count = Ref() // error | ^ diff --git a/tests/neg-custom-args/captures/check-inferred.scala b/tests/neg-custom-args/captures/check-inferred.scala index a520e8f64db8..4ed3b8fb88c6 100644 --- a/tests/neg-custom-args/captures/check-inferred.scala +++ b/tests/neg-custom-args/captures/check-inferred.scala @@ -46,5 +46,5 @@ class C: class D: val x: A^{cap.only[caps.Control]} = ??? - private val y = ??? : (() => A^{cap.only[caps.Read]}) // error + private val y = ??? : (() => A^{cap.only[caps.Unscoped]}) // error diff --git a/tests/neg-custom-args/captures/classified-inheritance.check b/tests/neg-custom-args/captures/classified-inheritance.check index aa182bfafce4..047fa36ccb04 100644 --- a/tests/neg-custom-args/captures/classified-inheritance.check +++ b/tests/neg-custom-args/captures/classified-inheritance.check @@ -1,7 +1,7 @@ -- Error: tests/neg-custom-args/captures/classified-inheritance.scala:5:6 ---------------------------------------------- -5 |class C2 extends caps.Control, caps.Read // error +5 |class C2 extends caps.Control, caps.Unscoped // error | ^ - | class C2 inherits two unrelated classifier traits: trait Read and trait Control + | class C2 inherits two unrelated classifier traits: trait Unscoped and trait Control -- Error: tests/neg-custom-args/captures/classified-inheritance.scala:10:6 --------------------------------------------- 10 |class C3 extends Matrix, Async // error | ^ diff --git a/tests/neg-custom-args/captures/classified-inheritance.scala b/tests/neg-custom-args/captures/classified-inheritance.scala index d48f410b4f7d..b7f553fcd581 100644 --- a/tests/neg-custom-args/captures/classified-inheritance.scala +++ b/tests/neg-custom-args/captures/classified-inheritance.scala @@ -2,7 +2,7 @@ import language.experimental.captureChecking class C1 extends caps.Control, caps.SharedCapability // OK -class C2 extends caps.Control, caps.Read // error +class C2 extends caps.Control, caps.Unscoped // error trait Async extends caps.Control class Matrix extends caps.Unscoped diff --git a/tests/neg-custom-args/captures/classifiers-1.scala b/tests/neg-custom-args/captures/classifiers-1.scala index ce0ca8890923..e6a77276c2f7 100644 --- a/tests/neg-custom-args/captures/classifiers-1.scala +++ b/tests/neg-custom-args/captures/classifiers-1.scala @@ -1,4 +1,4 @@ -class M extends caps.Read +class M extends caps.Unscoped class M1(x: Int => Int) extends M // error diff --git a/tests/pos-custom-args/captures/restrict-try.scala b/tests/pos-custom-args/captures/restrict-try.scala index b6be00f69fd7..5e61219ae1a3 100644 --- a/tests/pos-custom-args/captures/restrict-try.scala +++ b/tests/pos-custom-args/captures/restrict-try.scala @@ -1,10 +1,10 @@ -import caps.{SharedCapability, Control, Read} +import caps.{SharedCapability, Control, Unscoped} class Try[+T] case class Ok[T](x: T) extends Try[T] case class Fail(ex: Exception) extends Try[Nothing] -trait Matrix extends Read: +trait Matrix extends Unscoped: def get(): Unit trait Label extends Control: diff --git a/tests/run-tasty-inspector/stdlibExperimentalDefinitions.scala b/tests/run-tasty-inspector/stdlibExperimentalDefinitions.scala index c249721f6a6d..13b1c9f46fe2 100644 --- a/tests/run-tasty-inspector/stdlibExperimentalDefinitions.scala +++ b/tests/run-tasty-inspector/stdlibExperimentalDefinitions.scala @@ -38,6 +38,7 @@ val experimentalDefinitionInLibrary = Set( "scala.caps.ExclusiveCapability", "scala.caps.Mutable", "scala.caps.Read", + "scala.caps.Unscoped", "scala.caps.internal", "scala.caps.internal$", "scala.caps.cap", From 3f874bcac6444f70edce53fdacf82eba611c4205 Mon Sep 17 00:00:00 2001 From: odersky Date: Tue, 18 Nov 2025 23:24:26 +0100 Subject: [PATCH 06/10] Fix parsing of derived capabilities Allow both .only[C] and .rd (in this order). --- .../dotty/tools/dotc/parsing/Parsers.scala | 41 ++++++++++--------- 1 file changed, 22 insertions(+), 19 deletions(-) diff --git a/compiler/src/dotty/tools/dotc/parsing/Parsers.scala b/compiler/src/dotty/tools/dotc/parsing/Parsers.scala index c92fb852b11e..f44703a562f1 100644 --- a/compiler/src/dotty/tools/dotc/parsing/Parsers.scala +++ b/compiler/src/dotty/tools/dotc/parsing/Parsers.scala @@ -1644,37 +1644,40 @@ object Parsers { } /** CaptureRef ::= { SimpleRef `.` } SimpleRef [`*`] [CapFilter] [`.` `rd`] -- under captureChecking - * CapFilter ::= `.` `as` `[` QualId `]` + * CapFilter ::= `.` `only` `[` QualId `]` */ def captureRef(): Tree = - def derived(ref: Tree): Tree = - atSpan(startOffset(ref)): - if in.isIdent(nme.raw.STAR) then + def reachOpt(ref: Tree): Tree = + if in.isIdent(nme.raw.STAR) then + atSpan(startOffset(ref)): in.nextToken() Annotated(ref, makeReachAnnot()) - else if in.isIdent(nme.rd) then + else ref + + def restrictedOpt(ref: Tree): Tree = + if in.token == DOT && in.lookahead.isIdent(nme.only) then + atSpan(startOffset(ref)): in.nextToken() - Annotated(ref, makeReadOnlyAnnot()) - else if in.isIdent(nme.only) then in.nextToken() Annotated(ref, makeOnlyAnnot(inBrackets(convertToTypeId(qualId())))) - else assert(false) + else ref - def recur(ref: Tree): Tree = - if in.token == DOT then - in.nextToken() - if in.isIdent(nme.rd) || in.isIdent(nme.only) then derived(ref) - else recur(selector(ref)) - else if in.isIdent(nme.raw.STAR) then - val reachRef = derived(ref) - val next = in.lookahead - if in.token == DOT && (next.isIdent(nme.rd) || next.isIdent(nme.only)) then + def readOnlyOpt(ref: Tree): Tree = + if in.token == DOT && in.lookahead.isIdent(nme.rd) then + atSpan(startOffset(ref)): in.nextToken() - derived(reachRef) - else reachRef + in.nextToken() + Annotated(ref, makeReadOnlyAnnot()) else ref + def recur(ref: Tree): Tree = + val ref1 = readOnlyOpt(restrictedOpt(reachOpt(ref))) + if (ref1 eq ref) && in.token == DOT then + in.nextToken() + recur(selector(ref)) + else ref1 + recur(simpleRef()) end captureRef From 5dc9c66cceb28db0b4d69c19deeddb33497857b2 Mon Sep 17 00:00:00 2001 From: odersky Date: Wed, 19 Nov 2025 09:46:50 +0100 Subject: [PATCH 07/10] Let implied class capabilities respect read-only If a class has fresh fields and all fields are read-only, only imply `cap.rd`, not `cap`. --- .../dotty/tools/dotc/cc/CheckCaptures.scala | 44 ++++++++++++++----- 1 file changed, 33 insertions(+), 11 deletions(-) diff --git a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala index 083d467a96a2..d84ef761cb3f 100644 --- a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala +++ b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala @@ -939,17 +939,22 @@ class CheckCaptures extends Recheck, SymTransformer: .showing(i"constr type $mt with $argTypes%, % in $constr = $result", capt) end refineConstructorInstance - /** If `mbr` is a field that has (possibly restricted) FreshCaps in its span capture set, - * their classifiers, otherwise the empty list. - */ - private def classifiersOfFreshInType(mbr: Symbol)(using Context): List[ClassSymbol] = + private def memberCaps(mbr: Symbol)(using Context): List[Capability] = if contributesFreshToClass(mbr) then mbr.info.spanCaptureSet.elems .filter(_.isTerminalCapability) .toList - .map(_.classifier.asClass) else Nil + /** If `mbr` is a field that has (possibly restricted) FreshCaps in its span capture set, + * their classifiers, otherwise the empty list. + */ + private def classifiersOfFreshInType(mbr: Symbol)(using Context): List[ClassSymbol] = + memberCaps(mbr).map(_.classifier.asClass) + + private def allFreshInTypeAreRO(mbr: Symbol)(using Context): Boolean = + memberCaps(mbr).forall(_.isReadOnly) + /** The additional capture set implied by the capture sets of its fields. This * is either empty or, if some fields have a terminal capability in their span * capture sets, it consists of a single fresh cap that subsumes all these terminal @@ -962,14 +967,18 @@ class CheckCaptures extends Recheck, SymTransformer: def pushInfo(msg: => String) = if ctx.settings.YccVerbose.value then infos = msg :: infos + def knownFields(cls: ClassSymbol) = + setup.fieldsWithExplicitTypes // pick fields with explicit types for classes in this compilation unit + .getOrElse(cls, cls.info.decls.toList) // pick all symbols in class scope for other classes + + val isSeparate = cls.typeRef.isMutableType + /** The classifiers of the fresh caps in the span capture sets of all fields * in the given class `cls`. */ def impliedClassifiers(cls: Symbol): List[ClassSymbol] = cls match case cls: ClassSymbol => - var fieldClassifiers = setup.fieldsWithExplicitTypes // pick fields with explicit types for classes in this compilation unit - .getOrElse(cls, cls.info.decls.toList) // pick all symbols in class scope for other classes - .flatMap(classifiersOfFreshInType) + var fieldClassifiers = knownFields(cls).flatMap(classifiersOfFreshInType) if cls.typeRef.isMutableType then fieldClassifiers = cls.classifier :: fieldClassifiers val parentClassifiers = @@ -979,19 +988,32 @@ class CheckCaptures extends Recheck, SymTransformer: else parentClassifiers.foldLeft(fieldClassifiers.distinct)(dominators) case _ => Nil + def impliedReadOnly(cls: Symbol): Boolean = cls match + case cls: ClassSymbol => + val fieldsRO = knownFields(cls).forall(allFreshInTypeAreRO) + val parentsRO = cls.parentSyms.forall(impliedReadOnly) + fieldsRO && parentsRO + case _ => + false + + def maybeRO(ref: Capability) = + if !isSeparate && impliedReadOnly(cls) then ref.readOnly else ref + def fresh = FreshCap(Origin.NewInstance(core)).tap: fresh => if ctx.settings.YccVerbose.value then pushInfo(i"Note: instance of $cls captures a $fresh that comes from a field") report.echo(infos.mkString("\n"), ctx.owner.srcPos) - knownFresh.getOrElseUpdate(cls, impliedClassifiers(cls)) match + var implied = impliedClassifiers(cls) + if isSeparate then implied = cls.classifier :: implied + knownFresh.getOrElseUpdate(cls, implied) match case Nil => CaptureSet.empty case cl :: Nil => val result = fresh result.hiddenSet.adoptClassifier(cl) - result.singletonCaptureSet - case _ => fresh.singletonCaptureSet + maybeRO(result).singletonCaptureSet + case _ => maybeRO(fresh).singletonCaptureSet end captureSetImpliedByFields /** Recheck type applications: From de76524da9bdcd3756f489e5bbc71db910d98649 Mon Sep 17 00:00:00 2001 From: odersky Date: Wed, 19 Nov 2025 09:56:49 +0100 Subject: [PATCH 08/10] Don't consider `val _: T = e` as a binding in SepChecks Treat it like an expression `e` instead. --- compiler/src/dotty/tools/dotc/cc/SepCheck.scala | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/compiler/src/dotty/tools/dotc/cc/SepCheck.scala b/compiler/src/dotty/tools/dotc/cc/SepCheck.scala index 645f7b96a3c2..7442b44cf07f 100644 --- a/compiler/src/dotty/tools/dotc/cc/SepCheck.scala +++ b/compiler/src/dotty/tools/dotc/cc/SepCheck.scala @@ -7,6 +7,7 @@ import collection.mutable import core.* import Symbols.*, Types.*, Flags.*, Contexts.*, Names.*, Decorators.* import CaptureSet.{Refs, emptyRefs, HiddenSet} +import NameKinds.WildcardParamName import config.Printers.capt import StdNames.nme import util.{SimpleIdentitySet, EqHashMap, SrcPos} @@ -1028,7 +1029,8 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser: traverseSection(tree) case tree: ValDef => traverseChildren(tree) - checkValOrDefDef(tree) + if !tree.name.is(WildcardParamName) then + checkValOrDefDef(tree) case tree: DefDef => if skippable(tree.symbol) then capt.println(i"skipping sep check of ${tree.symbol}") From 4636639924ba2c94e4452229ac2996f70746de9c Mon Sep 17 00:00:00 2001 From: odersky Date: Wed, 19 Nov 2025 18:44:38 +0100 Subject: [PATCH 09/10] Require that consume parameters are covered by a FreshCap --- .../src/dotty/tools/dotc/cc/CaptureOps.scala | 4 + .../dotty/tools/dotc/cc/CheckCaptures.scala | 73 +++++++++++++++---- .../captures/consume-in-constructor.check | 30 ++++++++ .../captures/consume-in-constructor.scala | 32 ++++++++ .../neg-custom-args/captures/implied-ro.check | 11 +++ .../neg-custom-args/captures/implied-ro.scala | 12 +++ 6 files changed, 148 insertions(+), 14 deletions(-) create mode 100644 tests/neg-custom-args/captures/consume-in-constructor.check create mode 100644 tests/neg-custom-args/captures/consume-in-constructor.scala create mode 100644 tests/neg-custom-args/captures/implied-ro.check create mode 100644 tests/neg-custom-args/captures/implied-ro.scala diff --git a/compiler/src/dotty/tools/dotc/cc/CaptureOps.scala b/compiler/src/dotty/tools/dotc/cc/CaptureOps.scala index 22a91a3e190b..56b15b4ac637 100644 --- a/compiler/src/dotty/tools/dotc/cc/CaptureOps.scala +++ b/compiler/src/dotty/tools/dotc/cc/CaptureOps.scala @@ -13,6 +13,7 @@ import tpd.* import Annotations.Annotation import CaptureSet.VarState import Capabilities.* +import Mutability.isMutableType import StdNames.nme import config.Feature import NameKinds.TryOwnerName @@ -529,6 +530,9 @@ extension (cls: ClassSymbol) .foldLeft(defn.AnyClass)(leastClassifier) else defn.AnyClass + def isSeparate(using Context): Boolean = + cls.typeRef.isMutableType + extension (sym: Symbol) /** This symbol is one of `retains` or `retainsCap` */ diff --git a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala index d84ef761cb3f..9ddcb7cce332 100644 --- a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala +++ b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala @@ -21,7 +21,7 @@ import util.chaining.tap import transform.{Recheck, PreRecheck, CapturedVars} import Recheck.* import scala.collection.mutable -import CaptureSet.{withCaptureSetsExplained, IncludeFailure, MutAdaptFailure} +import CaptureSet.{withCaptureSetsExplained, IncludeFailure, MutAdaptFailure, VarState} import CCState.* import StdNames.nme import NameKinds.{DefaultGetterName, WildcardParamName, UniqueNameKind} @@ -916,7 +916,10 @@ class CheckCaptures extends Recheck, SymTransformer: val getter = cls.info.member(getterName).suchThat(_.isRefiningParamAccessor).symbol if !getter.is(Private) && getter.hasTrackedParts then refined = refined.refinedOverride(getterName, argType.unboxed) // Yichen you might want to check this - allCaptures ++= argType.captureSet + if getter.hasAnnotation(defn.ConsumeAnnot) then + () // We make sure in checkClassDef, point (6), that consume parameters don't + // contribute to the class capture set + else allCaptures ++= argType.captureSet (refined, allCaptures) /** Augment result type of constructor with refinements and captures. @@ -971,8 +974,6 @@ class CheckCaptures extends Recheck, SymTransformer: setup.fieldsWithExplicitTypes // pick fields with explicit types for classes in this compilation unit .getOrElse(cls, cls.info.decls.toList) // pick all symbols in class scope for other classes - val isSeparate = cls.typeRef.isMutableType - /** The classifiers of the fresh caps in the span capture sets of all fields * in the given class `cls`. */ @@ -997,7 +998,7 @@ class CheckCaptures extends Recheck, SymTransformer: false def maybeRO(ref: Capability) = - if !isSeparate && impliedReadOnly(cls) then ref.readOnly else ref + if !cls.isSeparate && impliedReadOnly(cls) then ref.readOnly else ref def fresh = FreshCap(Origin.NewInstance(core)).tap: fresh => @@ -1006,7 +1007,7 @@ class CheckCaptures extends Recheck, SymTransformer: report.echo(infos.mkString("\n"), ctx.owner.srcPos) var implied = impliedClassifiers(cls) - if isSeparate then implied = cls.classifier :: implied + if cls.isSeparate then implied = dominators(cls.classifier :: Nil, implied) knownFresh.getOrElseUpdate(cls, implied) match case Nil => CaptureSet.empty case cl :: Nil => @@ -1377,29 +1378,47 @@ class CheckCaptures extends Recheck, SymTransformer: /** Recheck classDef by enforcing the following class-specific capture set relations: * 1. The capture set of a class includes the capture sets of its parents. * 2. The capture set of the self type of a class includes the capture set of the class. - * 3. The capture set of the self type of a class includes the capture set of every class parameter, - * unless the parameter is marked @constructorOnly or @untrackedCaptures. + * 3. The capture set of the self type of a class includes the capture set of every class + * parameter, unless the parameter is marked @constructorOnly or @untrackedCaptures. * 4. If the class extends a pure base class, the capture set of the self type must be empty. - * Also, check that trait parents represented as applied types don't have cap in their - * type arguments. Other generic parents are represented as TypeApplys, where the same check - * is already done in the TypeApply. + * 5. Check that trait parents represented as applied types don't have cap in their + * type arguments. Charge deep capture sets of type arguments to non-reserved typevars + * to the environment. Other generic parents are represented as TypeApplys, where the + * same check is already done in the TypeApply. + * 6. Consume parameters are only allowed for classes producing a fresh cap + * for their constructor, and they don't contribute to the capture set. Example: + * + * class A(consume val x: B^) extends caps.Separate + * val a = A(b) + * + * Here, `a` is of type A{val x: B^}^, and the outer `^` does not hide `b`. + * That's necessary since we would otherwise get consume/use conflicts on `b`. */ override def recheckClassDef(tree: TypeDef, impl: Template, cls: ClassSymbol)(using Context): Type = if Feature.enabled(Feature.separationChecking) then sepChecksEnabled = true val localSet = capturedVars(cls) + + // (1) Capture set of a class includes the capture sets of its parents for parent <- impl.parents do // (1) checkSubset(capturedVars(parent.tpe.classSymbol), localSet, parent.srcPos, i"\nof the references allowed to be captured by $cls") + val saved = curEnv curEnv = Env(cls, EnvKind.Regular, localSet, curEnv) try + // (2) Capture set of self type includes capture set of class val thisSet = cls.classInfo.selfType.captureSet.withDescription(i"of the self type of $cls") - checkSubset(localSet, thisSet, tree.srcPos) // (2) + checkSubset(localSet, thisSet, tree.srcPos) + + // (3) Capture set of self type includes capture sets of parameters for param <- cls.paramGetters do if !param.hasAnnotation(defn.ConstructorOnlyAnnot) - && !param.hasAnnotation(defn.UntrackedCapturesAnnot) then + && !param.hasAnnotation(defn.UntrackedCapturesAnnot) + then withCapAsRoot: // OK? We need this here since self types use `cap` instead of `fresh` - checkSubset(param.termRef.captureSet, thisSet, param.srcPos) // (3) + checkSubset(param.termRef.captureSet, thisSet, param.srcPos) + + // (4) If class extends Pure, capture set of self type is empty for pureBase <- cls.pureBaseClass do // (4) def selfTypeTree = impl.body .collect: @@ -1410,15 +1429,41 @@ class CheckCaptures extends Recheck, SymTransformer: checkSubset(thisSet, CaptureSet.empty.withDescription(i"of pure base class $pureBase"), selfTypeTree.srcPos, cs1description = " captured by this self type") + + // (5) Check AppliedType parents for case tpt: TypeTree <- impl.parents do tpt.tpe match case AppliedType(fn, args) => markFreeTypeArgs(tpt, fn.typeSymbol, args.map(TypeTree(_))) case _ => + + // (6) Check that consume parameters are covered by an implied FreshCap + for getter <- cls.paramGetters do + if !getter.is(Private) // Setup makes sure that getters with capture sets are not private + && getter.hasAnnotation(defn.ConsumeAnnot) + then + val implied = captureSetImpliedByFields(cls, cls.appliedRef) + val getterCS = getter.info.captureSet + + val hasCoveringFresh = implied.elems.exists: + case fresh: FreshCap => + getterCS.elems.forall: elem => + given VarState = VarState.Unrecorded // make sure we don't add to fresh's hidden set + fresh.maxSubsumes(elem, canAddHidden = true) + case _ => + false + + if !hasCoveringFresh then + report.error( + em"""A consume parameter is only allowed for classes producing a `cap` in their constructor. + |This can be achieved by having the class extend caps.Separate.""", + getter.srcPos) + super.recheckClassDef(tree, impl, cls) finally completed += cls curEnv = saved + end recheckClassDef /** If type is of the form `T @requiresCapability(x)`, * mark `x` as free in the current environment. This is used to require the diff --git a/tests/neg-custom-args/captures/consume-in-constructor.check b/tests/neg-custom-args/captures/consume-in-constructor.check new file mode 100644 index 000000000000..d684517a1d9c --- /dev/null +++ b/tests/neg-custom-args/captures/consume-in-constructor.check @@ -0,0 +1,30 @@ +-- Error: tests/neg-custom-args/captures/consume-in-constructor.scala:11:21 -------------------------------------------- +11 |class A3(consume val b: B^) // error + | ^ + | A consume parameter is only allowed for classes producing a `cap` in their constructor. + | This can be achieved by having the class extend caps.Separate. +-- Error: tests/neg-custom-args/captures/consume-in-constructor.scala:20:10 -------------------------------------------- +20 | println(b) // error + | ^ + |Separation failure: Illegal access to (b : B^), which was passed as a consume parameter to constructor of class A2 + |on line 18 and therefore is no longer available. + | + |where: ^ refers to a fresh root capability in the type of value b +-- Error: tests/neg-custom-args/captures/consume-in-constructor.scala:21:10 -------------------------------------------- +21 | println(a1) // error, since `b` was consumed before + | ^^ + |Separation failure: Illegal access to (a1 : A1{val b: B^{b²}}^{cap, b²}), which was passed as a consume parameter to constructor of class A2 + |on line 18 and therefore is no longer available. + | + |where: b is a value in class A1 + | b² is a value in method Test + | cap is a fresh root capability in the type of value a1 +-- Error: tests/neg-custom-args/captures/consume-in-constructor.scala:27:10 -------------------------------------------- +27 | println(b) // error, b is hidden in the type of a1 + | ^ + | Separation failure: Illegal access to {b} which is hidden by the previous definition + | of value a1 with type A1^. + | This type hides capabilities {cap, b} + | + | where: ^ refers to a fresh root capability in the type of value a1 + | cap is a fresh root capability created in value a1 when constructing instance A1 diff --git a/tests/neg-custom-args/captures/consume-in-constructor.scala b/tests/neg-custom-args/captures/consume-in-constructor.scala new file mode 100644 index 000000000000..0786a4c2def0 --- /dev/null +++ b/tests/neg-custom-args/captures/consume-in-constructor.scala @@ -0,0 +1,32 @@ +import caps.{cap, Mutable} + +class B + +class A1(val b: B^): + val bb: B^ = B() + +class A2(consume val b: B^): + val bb: B^ = B() + +class A3(consume val b: B^) // error +class A4(consume val b: B^) extends Mutable { var x: Int = 1 } // ok +def Test = + val b: B^ = B() + val a1 = A1(b) + val _: A1^{cap, b} = a1 + println(b) // OK since a1's type mentions `b` explicitly + val a2 = A2(b) + val _: A2^{cap, b} = a2 + println(b) // error + println(a1) // error, since `b` was consumed before + println(a2) // OK since b belongs to a2 + +def Test2 = + val b: B^ = B() + val a1: A1^ = A1(b) + println(b) // error, b is hidden in the type of a1 + + + + + diff --git a/tests/neg-custom-args/captures/implied-ro.check b/tests/neg-custom-args/captures/implied-ro.check new file mode 100644 index 000000000000..c11bf580c0ea --- /dev/null +++ b/tests/neg-custom-args/captures/implied-ro.check @@ -0,0 +1,11 @@ +-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/implied-ro.scala:12:16 ----------------------------------- +12 | val _: C^{} = c // error + | ^ + | Found: (c : C^{cap.rd}) + | Required: C + | + | Note that capability cap.rd is not included in capture set {}. + | + | where: cap is a fresh root capability classified as Unscoped created in value c when constructing instance C + | + | longer explanation available when compiling with `-explain` diff --git a/tests/neg-custom-args/captures/implied-ro.scala b/tests/neg-custom-args/captures/implied-ro.scala new file mode 100644 index 000000000000..d1bf81519054 --- /dev/null +++ b/tests/neg-custom-args/captures/implied-ro.scala @@ -0,0 +1,12 @@ +import caps.* +class Ref extends Mutable, Unscoped + +class C: + val r: Ref = Ref() + +def test = + val c = C() + val _: C^{cap.rd} = c + val _: C^{cap.only[Unscoped]} = c + val _: C^{cap.only[Unscoped].rd} = c + val _: C^{} = c // error From d43dfe3763b65d851cc5a32adec0806ffbabc1ba Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Oliver=20Bra=C4=8Devac?= Date: Wed, 19 Nov 2025 20:48:32 +0100 Subject: [PATCH 10/10] Add tests for consume in constructor parameters --- .../captures/paths-derivedcaps-consume.scala | 53 ++++++++++++ .../captures/paths-complex-consume.scala | 80 +++++++++++++++++++ .../captures/paths-deep-consume.scala | 24 ++++++ .../captures/paths-nested-consume.scala | 33 ++++++++ .../paths-simple-suffix-consume.scala | 37 +++++++++ 5 files changed, 227 insertions(+) create mode 100644 tests/neg-custom-args/captures/paths-derivedcaps-consume.scala create mode 100644 tests/pos-custom-args/captures/paths-complex-consume.scala create mode 100644 tests/pos-custom-args/captures/paths-deep-consume.scala create mode 100644 tests/pos-custom-args/captures/paths-nested-consume.scala create mode 100644 tests/pos-custom-args/captures/paths-simple-suffix-consume.scala diff --git a/tests/neg-custom-args/captures/paths-derivedcaps-consume.scala b/tests/neg-custom-args/captures/paths-derivedcaps-consume.scala new file mode 100644 index 000000000000..6be6d7b74477 --- /dev/null +++ b/tests/neg-custom-args/captures/paths-derivedcaps-consume.scala @@ -0,0 +1,53 @@ +import language.experimental.captureChecking +import language.experimental.separationChecking +import caps.* + +class Foo extends ExclusiveCapability, Classifier + +// Testing with various DerivedCapabilities +class D +class C(val d: D) +class B(val c: C) extends Foo, Mutable: + update def foo() = println("foo") +class A(consume val b: B^) extends Mutable: + update def bar() = b.foo() +class A2(consume val b: B^) +class A3(consume var b: B^) +class A4(consume val b: A2^{cap.only[Foo]}) + +// Test: Access nested fields (suffix paths) after consume +def testSuffixPaths = + val d: D = D() + val c: C = C(d) + val b: B^ = B(c) + val a1 = A(b) + val b2: B^ = B(c) + val a2 = A2(b2) // the difference is that we pass b2.rd + val b3: B^ = B(c) + val a3 = A3(b3) + val b4: B^ = B(c) + val a22 = A2(b4) + val a4 = A4(a22) + val b5: B^{cap.only[Foo]} = B(c) + val a5 = A(b5) + val b6: B^{cap.only[Foo]} = B(c) + val a222 = A2(b6) + val a6 = A4(a222) + + + println(a1.b) // ok + println(a2.b) // ok + println(a3.b) // ok + println(a4.b) // ok + println(a4.b.b) // ok + println(a5.b) // ok + println(a6.b) // ok + println(a6.b.b) // ok + + println(b) // error + println(b2) // error + println(b3) // error + println(b4) // error + //println(b5) // should error (currently accepted!!!) + //println(b6) // should error (currently accepted!!!) + //println(a222) // should error (currently accepted!!!) \ No newline at end of file diff --git a/tests/pos-custom-args/captures/paths-complex-consume.scala b/tests/pos-custom-args/captures/paths-complex-consume.scala new file mode 100644 index 000000000000..f4fbc0ca7c11 --- /dev/null +++ b/tests/pos-custom-args/captures/paths-complex-consume.scala @@ -0,0 +1,80 @@ +import language.experimental.captureChecking +import language.experimental.separationChecking +import caps.cap + +// Create a deeper nesting structure +class D() +class C(val d: D^) +class B(val c: C^) +class A(consume val b: B^) + +// Test 1: Accessing nested fields through a consumed path +def testNestedFieldsAfterConsume = + val d: D^ = D() + val c: C^ = C(d) + val b: B^ = B(c) + val a = A(b) + + // After a consumed b, we should be able to access: + println(a.b) // OK - a owns b + println(a.b.c) // OK - accessing field of consumed b through a + println(a.b.c.d) // OK - deeper nesting through consumed path + +// Test 2: Non-trivial prefix accessing a consumed field +class Container(consume val a: A^): + val other: A^ = A(B(C(D()))) + +class Outer(consume val container: Container^) + +def testComplexPrefix = + val d1: D^ = D() + val c1: C^ = C(d1) + val b1: B^ = B(c1) + val a1 = A(b1) + val container1 = Container(a1) + val outer = Outer(container1) + + // Non-trivial prefix: outer.container.a (where 'a' was consumed by container) + println(outer.container) // OK - outer consumed container + println(outer.container.a) // OK - accessing consumed field through prefix + println(outer.container.a.b) // OK - and then its nested fields + println(outer.container.a.b.c) // OK - even deeper + println(outer.container.a.b.c.d) // OK - deepest level + +// Test 3: Multiple consume parameters with nested access +class Multi(consume val b1: B^, consume val b2: B^): + val b3: B^ = B(C(D())) + +def testMultipleConsume = + val b1: B^ = B(C(D())) + val b2: B^ = B(C(D())) + val multi = Multi(b1, b2) + + // All of these should work: + println(multi.b1) // OK + println(multi.b1.c) // OK - nested field of consumed b1 + println(multi.b1.c.d) // OK - deeper nesting + println(multi.b2) // OK + println(multi.b2.c) // OK - nested field of consumed b2 + println(multi.b2.c.d) // OK - deeper nesting + println(multi.b3.c.d) // OK - non-consumed field + +// Test 4: Consume at multiple levels with complex paths +class Top(consume val outer: Outer^) + +def testMultiLevelConsume = + val d2: D^ = D() + val c2: C^ = C(d2) + val b2: B^ = B(c2) + val a2 = A(b2) + val container2 = Container(a2) + val outer2 = Outer(container2) + val top = Top(outer2) + + // Very deep path through multiple consume levels: + println(top.outer) // OK - top consumed outer + println(top.outer.container) // OK - continue through path + println(top.outer.container.a) // OK - container consumed a + println(top.outer.container.a.b) // OK - a consumed b + println(top.outer.container.a.b.c) // OK - nested field + println(top.outer.container.a.b.c.d) // OK - deepest field diff --git a/tests/pos-custom-args/captures/paths-deep-consume.scala b/tests/pos-custom-args/captures/paths-deep-consume.scala new file mode 100644 index 000000000000..6a890b934ec4 --- /dev/null +++ b/tests/pos-custom-args/captures/paths-deep-consume.scala @@ -0,0 +1,24 @@ +import language.experimental.captureChecking +import language.experimental.separationChecking +import caps.cap + +class B + +class A(consume val b: B^): + val bb: B^ = B() + +class C(consume val a: A^): + val aa: A^ = A(B()) + +// Test deep nested access paths +def testDeepPaths = + val b: B^ = B() + val a = A(b) + val c = C(a) + + // All these should work - accessing through ownership chain + println(c.a) // c owns a + println(c.a.b) // c owns a, a owns b + println(c.a.bb) // c owns a, accessing other field + println(c.aa) // accessing other field of c + println(c.aa.b) // accessing nested field through c.aa diff --git a/tests/pos-custom-args/captures/paths-nested-consume.scala b/tests/pos-custom-args/captures/paths-nested-consume.scala new file mode 100644 index 000000000000..7caa46a28426 --- /dev/null +++ b/tests/pos-custom-args/captures/paths-nested-consume.scala @@ -0,0 +1,33 @@ +import language.experimental.captureChecking +import language.experimental.separationChecking +import caps.cap + +class B + +class A(consume val b: B^): + val bb: B^ = B() + +class C(consume val a: A^): + val aa: A^ = A(B()) + +// Test: After consuming b into a, then consuming a into c, +// we should be able to access c.a.b (nested field selection) +def testNestedAccess = + val b: B^ = B() + val a = A(b) + println(a.b) // OK - a consumed b, accessing through a + val c = C(a) + println(c.a) // Should be OK - c consumed a, accessing through c + println(c.a.b) // Should be OK - accessing b through c.a, where c owns a and a owns b + +// Test: The deeper path c.a.b should work even though a was consumed +def testDeepPath = + val b: B^ = B() + val a = A(b) + val c = C(a) + // At this point: + // - b was consumed by a (so we can't use b directly) + // - a was consumed by c (so we can't use a directly) + // But we should be able to access: + println(c.a.b) // OK - full path through ownership chain + println(c.a.bb) // OK - other field of c.a diff --git a/tests/pos-custom-args/captures/paths-simple-suffix-consume.scala b/tests/pos-custom-args/captures/paths-simple-suffix-consume.scala new file mode 100644 index 000000000000..02b8e78197be --- /dev/null +++ b/tests/pos-custom-args/captures/paths-simple-suffix-consume.scala @@ -0,0 +1,37 @@ +import language.experimental.captureChecking +import language.experimental.separationChecking +import caps.cap + +// Create a deep nesting structure for testing suffix paths +class D +class C(val d: D^) +class B(val c: C^) +class A(consume val b: B^) + +// Test 1: Simple suffix paths after consume +def test1 = + val d: D^ = D() + val c: C^ = C(d) + val b: B^ = B(c) + val a = A(b) + + // After 'a' consumes 'b', access nested fields: + println(a.b) // OK - consumed field + println(a.b.c) // OK - suffix: .c after consumed field + println(a.b.c.d) // OK - suffix: .c.d after consumed field + +// Test 2: Non-consume wrapper with consumed inner field +class Holder(val a: A^) // Note: NOT consume + +def test2 = + val d: D^ = D() + val c: C^ = C(d) + val b: B^ = B(c) + val a = A(b) + val holder = Holder(a) + + // Access through holder.a.b where b was consumed by a: + println(holder.a) // OK - not consumed + println(holder.a.b) // OK - accessing consumed field through prefix + println(holder.a.b.c) // OK - suffix .c + println(holder.a.b.c.d) // OK - suffix .c.d