diff --git a/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala b/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala index e275fd76b774..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 @@ -828,15 +835,16 @@ 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 !elemVis.isProperlyContainedIn(owner) + || nestedOK && elemVis.owner == owner else true def addDependent(cs: CaptureSet)(using Context, VarState): Boolean = @@ -950,6 +958,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 @@ -995,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