From f38d9263bd3f15f15ff429e9033cfd6d8196d209 Mon Sep 17 00:00:00 2001 From: odersky Date: Thu, 25 Sep 2025 15:25:22 +0200 Subject: [PATCH 1/2] Turn level checking off for DerivedVars --- compiler/src/dotty/tools/dotc/cc/CaptureSet.scala | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala b/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala index e275fd76b774..fd9b34c22818 100644 --- a/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala +++ b/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala @@ -828,11 +828,11 @@ object CaptureSet: def levelOK(elem: Capability)(using Context): Boolean = elem match case elem @ ResultCap(binder) => - rootLimit == null && (this.isInstanceOf[BiMapped] || isPartOf(binder.resType)) + rootLimit == null && isPartOf(binder.resType) case GlobalCap => rootLimit == null case elem: ParamRef => - this.isInstanceOf[BiMapped] || isPartOf(elem.binder.resType) + isPartOf(elem.binder.resType) case _ => if owner.exists then val elemVis = elem.visibility @@ -950,6 +950,9 @@ object CaptureSet: abstract class DerivedVar(owner: Symbol, initialElems: Refs)(using @constructorOnly ctx: Context) extends Var(owner, initialElems): + override def levelOK(elem: Capability)(using Context): Boolean = + true + // For debugging: A trace where a set was created. Note that logically it would make more // sense to place this variable in Mapped, but that runs afoul of the initialization checker. // val stack = if debugSets && this.isInstanceOf[Mapped] then (new Throwable).getStackTrace().take(20) else null From 9b20ddfbfe2d8c7be875d539a6fa1b132ddbcee0 Mon Sep 17 00:00:00 2001 From: odersky Date: Thu, 25 Sep 2025 18:26:50 +0200 Subject: [PATCH 2/2] Distinguish between certain capset vars with same owner A capset var that is defined in the result type of a val or def cannot accept any capabilities defined on the RHS. By contrast, a capset defined in the RHS (but not in local definitions of the RHS) can accept other capabilities defined in that RHS. Both of these capsets have the same owner, so we need an additional piece of information to perform level checking correctly. Fixes #24039. --- .../src/dotty/tools/dotc/cc/CaptureSet.scala | 18 +++++++++++++++--- .../dotty/tools/dotc/cc/CheckCaptures.scala | 2 +- compiler/src/dotty/tools/dotc/cc/Setup.scala | 5 +++-- compiler/src/dotty/tools/dotc/core/Mode.scala | 9 +++++++++ tests/neg-custom-args/captures/branding.scala | 6 +++--- .../captures/capset-members4.scala | 8 ++++---- tests/neg-custom-args/captures/i15772.check | 8 ++++---- tests/neg-custom-args/captures/i23207.check | 8 ++++---- tests/neg-custom-args/captures/leaky.check | 8 ++++---- tests/neg-custom-args/captures/real-try.check | 10 ++++------ .../neg-custom-args/captures/sep-counter.check | 6 +++--- tests/neg-custom-args/captures/sep-pairs.check | 6 +++--- tests/neg-custom-args/captures/vars.check | 14 ++++++-------- tests/pos-custom-args/captures/i24039.scala | 9 +++++++++ 14 files changed, 72 insertions(+), 45 deletions(-) create mode 100644 tests/pos-custom-args/captures/i24039.scala diff --git a/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala b/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala index fd9b34c22818..464114a2b672 100644 --- a/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala +++ b/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala @@ -655,8 +655,15 @@ object CaptureSet: inline val debugVars = false inline val debugTarget = 1745 - /** The subclass of captureset variables with given initial elements */ - class Var(initialOwner: Symbol = NoSymbol, initialElems: Refs = emptyRefs, underBox: Boolean = false)(using /*@constructorOnly*/ ictx: Context) extends CaptureSet: + /** The subclass of captureset variables with given initial elements + * @param initialOwner the initial owner. This is the real owner, except that + * it can be change in HiddenSets. Used for level checking + * if different from NoSymbol. + * @param initialElems the initial elements + * @param nestedOK relevant only if owner != NoSymbol. If true the set accepts + * elements that are directly owned by owner. + */ + class Var(initialOwner: Symbol = NoSymbol, initialElems: Refs = emptyRefs, nestedOK: Boolean = true)(using /*@constructorOnly*/ ictx: Context) extends CaptureSet: override def owner = initialOwner @@ -682,7 +689,7 @@ object CaptureSet: protected var myElems: Refs = initialElems if debugVars && id == debugTarget then - println(i"###INIT ELEMS of $id to $initialElems") + println(i"###INIT ELEMS of $id of class $getClass in $initialOwner, $nestedOK to $initialElems") assert(false) def elems: Refs = myElems @@ -837,6 +844,7 @@ object CaptureSet: if owner.exists then val elemVis = elem.visibility !elemVis.isProperlyContainedIn(owner) + || nestedOK && elemVis.owner == owner else true def addDependent(cs: CaptureSet)(using Context, VarState): Boolean = @@ -998,6 +1006,10 @@ object CaptureSet: (val source: Var, val bimap: BiTypeMap, initialElems: Refs)(using @constructorOnly ctx: Context) extends DerivedVar(source.owner, initialElems): + if debugVars && id == debugTarget then + println(i"variable $id is derived from $source") + assert(false) + override def tryInclude(elem: Capability, origin: CaptureSet)(using Context, VarState): Boolean = if origin eq source then val mappedElem = bimap.mapCapability(elem) diff --git a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala index d352baa071b9..42e7f67de460 100644 --- a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala +++ b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala @@ -430,7 +430,7 @@ class CheckCaptures extends Recheck, SymTransformer: def capturedVars(sym: Symbol)(using Context): CaptureSet = myCapturedVars.getOrElseUpdate(sym, if sym.isTerm || !sym.owner.isStaticOwner - then CaptureSet.Var(sym) + then CaptureSet.Var(sym, nestedOK = false) else CaptureSet.empty) // ---- Record Uses with MarkFree ---------------------------------------------------- diff --git a/compiler/src/dotty/tools/dotc/cc/Setup.scala b/compiler/src/dotty/tools/dotc/cc/Setup.scala index 4864c837dd45..b9606738731e 100644 --- a/compiler/src/dotty/tools/dotc/cc/Setup.scala +++ b/compiler/src/dotty/tools/dotc/cc/Setup.scala @@ -495,7 +495,8 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI: def transformResultType(tpt: TypeTree, sym: Symbol)(using Context): Unit = // First step: Transform the type and record it as knownType of tpt. try - transformTT(tpt, sym, boxed = false) + inContext(ctx.addMode(Mode.CCPreciseOwner)): + transformTT(tpt, sym, boxed = false) catch case ex: IllegalCaptureRef => capt.println(i"fail while transforming result type $tpt of $sym") throw ex @@ -851,7 +852,7 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI: /** Add a capture set variable to `tp` if necessary. */ private def addVar(tp: Type, owner: Symbol)(using Context): Type = - decorate(tp, CaptureSet.Var(owner, _)) + decorate(tp, CaptureSet.Var(owner, _, nestedOK = !ctx.mode.is(Mode.CCPreciseOwner))) /** A map that adds capture sets at all contra- and invariant positions * in a type where a capture set would be needed. This is used to make types diff --git a/compiler/src/dotty/tools/dotc/core/Mode.scala b/compiler/src/dotty/tools/dotc/core/Mode.scala index 44efbedf0f68..66c4e0264fdc 100644 --- a/compiler/src/dotty/tools/dotc/core/Mode.scala +++ b/compiler/src/dotty/tools/dotc/core/Mode.scala @@ -141,6 +141,15 @@ object Mode { */ val InPackageClauseName: Mode = newMode(19, "InPackageClauseName") + /** When creating capset Vars in cc.Setup, mark the variable to be in + * the result type of the context's owner, so that nested vals cannot + * be included in it. + * Reuses the value of InPackageClauseName to save Mode bits. + * This is OK since InPackageClauseName is only set and tested during Typer, + * and CCPreciseOwner only has an effect during phase CheckCaptures. + */ + val CCPreciseOwner = InPackageClauseName + /** We are in the IDE */ val Interactive: Mode = newMode(20, "Interactive") diff --git a/tests/neg-custom-args/captures/branding.scala b/tests/neg-custom-args/captures/branding.scala index 744fdf065d91..9d5ad25e82bc 100644 --- a/tests/neg-custom-args/captures/branding.scala +++ b/tests/neg-custom-args/captures/branding.scala @@ -22,14 +22,14 @@ def main() = val untrustedLogger: Logger^ = ??? val untrustedChannel: Channel[String]^ = ??? - runSecure: () => // error (???, arose after changing level checking) + runSecure: () => trustedLogger.log("Hello from trusted code") // ok - runSecure: () => // error (???, arose after changing level checking) + runSecure: () => trustedChannel.send("I can send") trustedLogger.log(trustedChannel.recv()) // ok - runSecure: () => // error (???, arose after changing level checking) + runSecure: () => "I am pure" // ok runSecure: () => // error diff --git a/tests/neg-custom-args/captures/capset-members4.scala b/tests/neg-custom-args/captures/capset-members4.scala index 338e0e99acb2..7539e6ef0a21 100644 --- a/tests/neg-custom-args/captures/capset-members4.scala +++ b/tests/neg-custom-args/captures/capset-members4.scala @@ -11,8 +11,8 @@ def test = type C^ >: {z,x} <: {x,y,z} val foo: Foo = ??? - onlyWithZ[{foo.C}] // error - onlyWithZ[{z}] // error - onlyWithZ[{x,z}] // error - onlyWithZ[{x,y,z}] // error + onlyWithZ[{foo.C}] // ok + onlyWithZ[{z}] // ok + onlyWithZ[{x,z}] // ok + onlyWithZ[{x,y,z}] // ok onlyWithZ[{x,y}] // error \ No newline at end of file diff --git a/tests/neg-custom-args/captures/i15772.check b/tests/neg-custom-args/captures/i15772.check index c7644791925b..b167580f548c 100644 --- a/tests/neg-custom-args/captures/i15772.check +++ b/tests/neg-custom-args/captures/i15772.check @@ -5,8 +5,8 @@ -- Error: tests/neg-custom-args/captures/i15772.scala:22:46 ------------------------------------------------------------ 22 | val boxed1 : ((C^) => Unit) -> Unit = box1(c) // error | ^^^^^^^ - |C^ => Unit cannot be box-converted to C{val arg: C^²}^{c} ->{cap, x} Unit - |since the additional capture set {x} resulting from box conversion is not allowed in C{val arg: C^²}^{c} => Unit + |C^ => Unit cannot be box-converted to C{val arg: C^²}^{c} ->{cap, c} Unit + |since the additional capture set {c} resulting from box conversion is not allowed in C{val arg: C^²}^{c} => Unit | |where: => refers to the universal root capability | ^ refers to the universal root capability @@ -15,8 +15,8 @@ -- Error: tests/neg-custom-args/captures/i15772.scala:29:35 ------------------------------------------------------------ 29 | val boxed2 : Observe[C^] = box2(c) // error | ^^^^^^^ - |C^ => Unit cannot be box-converted to C{val arg: C^²}^{c} ->{cap, x} Unit - |since the additional capture set {x} resulting from box conversion is not allowed in C{val arg: C^²}^{c} => Unit + |C^ => Unit cannot be box-converted to C{val arg: C^²}^{c} ->{cap, c} Unit + |since the additional capture set {c} resulting from box conversion is not allowed in C{val arg: C^²}^{c} => Unit | |where: => refers to the universal root capability | ^ refers to the universal root capability diff --git a/tests/neg-custom-args/captures/i23207.check b/tests/neg-custom-args/captures/i23207.check index d76ae4d39af1..626655686d87 100644 --- a/tests/neg-custom-args/captures/i23207.check +++ b/tests/neg-custom-args/captures/i23207.check @@ -19,18 +19,18 @@ -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/i23207.scala:19:2 ---------------------------------------- 19 | c // error | ^ - | Found: A^{io} + | Found: A^{c} | Required: A | - | Note that capability io is not included in capture set {}. + | Note that capability c is not included in capture set {}. | | longer explanation available when compiling with `-explain` -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/i23207.scala:27:2 ---------------------------------------- 27 | c // error | ^ - | Found: A^{io} + | Found: A^{c} | Required: A | - | Note that capability io is not included in capture set {}. + | Note that capability c is not included in capture set {}. | | longer explanation available when compiling with `-explain` diff --git a/tests/neg-custom-args/captures/leaky.check b/tests/neg-custom-args/captures/leaky.check index 463a941545cf..b6fb368aa757 100644 --- a/tests/neg-custom-args/captures/leaky.check +++ b/tests/neg-custom-args/captures/leaky.check @@ -10,18 +10,18 @@ -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/leaky.scala:24:2 ----------------------------------------- 24 | x // error | ^ - | Found: test.runnable.Transform{val fun: Any ->{a} Any}^{a} + | Found: test.runnable.Transform{val fun: Any ->{f} Any}^{x} | Required: test.runnable.Transform | - | Note that capability a is not included in capture set {}. + | Note that capability x is not included in capture set {}. | | longer explanation available when compiling with `-explain` -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/leaky.scala:31:2 ----------------------------------------- 31 | x // error | ^ - | Found: test.runnable.Transform{val fun: Any ->{a} Any}^{a} + | Found: test.runnable.Transform{val fun: Any ->{f} Any}^{x} | Required: test.runnable.Transform | - | Note that capability a is not included in capture set {}. + | Note that capability x is not included in capture set {}. | | longer explanation available when compiling with `-explain` diff --git a/tests/neg-custom-args/captures/real-try.check b/tests/neg-custom-args/captures/real-try.check index a665939ba1e9..684dcb7c982d 100644 --- a/tests/neg-custom-args/captures/real-try.check +++ b/tests/neg-custom-args/captures/real-try.check @@ -39,12 +39,10 @@ -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/real-try.scala:33:8 -------------------------------------- 33 | Cell(() => foo(1)) // error | ^^^^^^^^^^^^^^^^^^ - | Found: Cell[() => Unit] - | Required: Cell[() ->'s5 Unit]^'s6 + | Found: Cell[() ->{canThrow$4} Unit] + | Required: Cell[() ->'s5 Unit]^'s6 | - | Note that capability cap cannot be included in outer capture set 's5 of value b. - | - | where: => refers to a fresh root capability classified as Control in the type of given instance canThrow$4 - | cap is a fresh root capability classified as Control in the type of given instance canThrow$4 + | Note that capability canThrow$4, defined in method try$4 + | cannot be included in outer capture set 's5 of value b. | | longer explanation available when compiling with `-explain` diff --git a/tests/neg-custom-args/captures/sep-counter.check b/tests/neg-custom-args/captures/sep-counter.check index f46d3fa03dfc..c9d2b1895aee 100644 --- a/tests/neg-custom-args/captures/sep-counter.check +++ b/tests/neg-custom-args/captures/sep-counter.check @@ -2,9 +2,9 @@ 12 | def mkCounter(): Pair[Ref^, Ref^] = // error | ^^^^^^^^^^^^^^^^ | Separation failure in method mkCounter's result type Pair[Ref^, Ref^²]. - | One part, Ref^, hides capabilities {cap}. - | Another part, Ref^², captures capabilities {cap}. - | The two sets overlap at cap of method mkCounter. + | One part, Ref^, hides capabilities {c, cap}. + | Another part, Ref^², captures capabilities {c, cap}. + | The two sets overlap at {c}. | | where: ^ refers to a fresh root capability classified as Mutable in the result type of method mkCounter | ^² refers to a fresh root capability classified as Mutable in the result type of method mkCounter diff --git a/tests/neg-custom-args/captures/sep-pairs.check b/tests/neg-custom-args/captures/sep-pairs.check index 79a9e8ddf108..43429b08a3bc 100644 --- a/tests/neg-custom-args/captures/sep-pairs.check +++ b/tests/neg-custom-args/captures/sep-pairs.check @@ -12,9 +12,9 @@ 13 |def bad: Pair[Ref^, Ref^] = // error: overlap at r1*, r0 | ^^^^^^^^^^^^^^^^ | Separation failure in method bad's result type Pair[Ref^, Ref^²]. - | One part, Ref^, hides capabilities {cap, cap², r0}. - | Another part, Ref^², captures capabilities {cap, cap², r0}. - | The two sets overlap at {r0}. + | One part, Ref^, hides capabilities {r1*, cap, cap², r0}. + | Another part, Ref^², captures capabilities {r1*, cap, cap², r0}. + | The two sets overlap at {r1*, r0}. | | where: ^ refers to a fresh root capability classified as Mutable in the result type of method bad | ^² refers to a fresh root capability classified as Mutable in the result type of method bad diff --git a/tests/neg-custom-args/captures/vars.check b/tests/neg-custom-args/captures/vars.check index f0e82a9dfff6..c992228ca26d 100644 --- a/tests/neg-custom-args/captures/vars.check +++ b/tests/neg-custom-args/captures/vars.check @@ -28,16 +28,14 @@ -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/vars.scala:36:10 ----------------------------------------- 36 | local { cap3 => // error | ^ - |Found: (cap3: CC^) ->'s1 String => String - |Required: CC^ -> String =>² String + | Found: (cap3: CC^) ->'s1 String ->{cap3} String + | Required: CC^ -> String ->{cap3²} String | - |Note that capability cap cannot be included in outer capture set {cap²}. + | Note that capability cap3 cannot be included in outer capture set {cap3²}. | - |where: => refers to a root capability associated with the result type of (cap3: CC^): String => String - | =>² refers to a fresh root capability created in method test of parameter parameter cap3² of method $anonfun - | ^ refers to the universal root capability - | cap is a root capability associated with the result type of (cap3: CC^): String =>² String - | cap² is a fresh root capability created in method test of parameter parameter cap3² of method $anonfun + | where: ^ refers to the universal root capability + | cap3 is a reference to a value parameter + | cap3² is a parameter in an anonymous function in method test 37 | def g(x: String): String = if cap3 == cap3 then "" else "a" 38 | g | diff --git a/tests/pos-custom-args/captures/i24039.scala b/tests/pos-custom-args/captures/i24039.scala new file mode 100644 index 000000000000..c00242c4d432 --- /dev/null +++ b/tests/pos-custom-args/captures/i24039.scala @@ -0,0 +1,9 @@ +import language.experimental.captureChecking +import caps.* +def test1() = + val z: Any^ = ??? + def onlyWithZ[C^](using c: Contains[C, z.type]) = ??? + onlyWithZ[{z}] // error, but should be ok +def test2(z: Any^) = + def onlyWithZ[C^](using c: Contains[C, z.type]) = ??? + onlyWithZ[{z}] // ok