Skip to content

Commit 0ec9468

Browse files
oderskyodersky
authored
Level checking: distinguish between certain capset vars with same owner (#24077)
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.
2 parents dc33947 + 9b20ddf commit 0ec9468

File tree

14 files changed

+77
-47
lines changed

14 files changed

+77
-47
lines changed

‎compiler/src/dotty/tools/dotc/cc/CaptureSet.scala‎

Lines changed: 20 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -655,8 +655,15 @@ object CaptureSet:
655655
inline val debugVars = false
656656
inline val debugTarget = 1745
657657

658-
/** The subclass of captureset variables with given initial elements */
659-
class Var(initialOwner: Symbol = NoSymbol, initialElems: Refs = emptyRefs, underBox: Boolean = false)(using /*@constructorOnly*/ ictx: Context) extends CaptureSet:
658+
/** The subclass of captureset variables with given initial elements
659+
* @param initialOwner the initial owner. This is the real owner, except that
660+
* it can be change in HiddenSets. Used for level checking
661+
* if different from NoSymbol.
662+
* @param initialElems the initial elements
663+
* @param nestedOK relevant only if owner != NoSymbol. If true the set accepts
664+
* elements that are directly owned by owner.
665+
*/
666+
class Var(initialOwner: Symbol = NoSymbol, initialElems: Refs = emptyRefs, nestedOK: Boolean = true)(using /*@constructorOnly*/ ictx: Context) extends CaptureSet:
660667

661668
override def owner = initialOwner
662669

@@ -682,7 +689,7 @@ object CaptureSet:
682689
protected var myElems: Refs = initialElems
683690

684691
if debugVars && id == debugTarget then
685-
println(i"###INIT ELEMS of $id to $initialElems")
692+
println(i"###INIT ELEMS of $id of class $getClass in $initialOwner, $nestedOK to $initialElems")
686693
assert(false)
687694

688695
def elems: Refs = myElems
@@ -828,15 +835,16 @@ object CaptureSet:
828835

829836
def levelOK(elem: Capability)(using Context): Boolean = elem match
830837
case elem @ ResultCap(binder) =>
831-
rootLimit == null && (this.isInstanceOf[BiMapped] || isPartOf(binder.resType))
838+
rootLimit == null && isPartOf(binder.resType)
832839
case GlobalCap =>
833840
rootLimit == null
834841
case elem: ParamRef =>
835-
this.isInstanceOf[BiMapped] || isPartOf(elem.binder.resType)
842+
isPartOf(elem.binder.resType)
836843
case _ =>
837844
if owner.exists then
838845
val elemVis = elem.visibility
839846
!elemVis.isProperlyContainedIn(owner)
847+
|| nestedOK && elemVis.owner == owner
840848
else true
841849

842850
def addDependent(cs: CaptureSet)(using Context, VarState): Boolean =
@@ -950,6 +958,9 @@ object CaptureSet:
950958
abstract class DerivedVar(owner: Symbol, initialElems: Refs)(using @constructorOnly ctx: Context)
951959
extends Var(owner, initialElems):
952960

961+
override def levelOK(elem: Capability)(using Context): Boolean =
962+
true
963+
953964
// For debugging: A trace where a set was created. Note that logically it would make more
954965
// sense to place this variable in Mapped, but that runs afoul of the initialization checker.
955966
// val stack = if debugSets && this.isInstanceOf[Mapped] then (new Throwable).getStackTrace().take(20) else null
@@ -995,6 +1006,10 @@ object CaptureSet:
9951006
(val source: Var, val bimap: BiTypeMap, initialElems: Refs)(using @constructorOnly ctx: Context)
9961007
extends DerivedVar(source.owner, initialElems):
9971008

1009+
if debugVars && id == debugTarget then
1010+
println(i"variable $id is derived from $source")
1011+
assert(false)
1012+
9981013
override def tryInclude(elem: Capability, origin: CaptureSet)(using Context, VarState): Boolean =
9991014
if origin eq source then
10001015
val mappedElem = bimap.mapCapability(elem)

‎compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -430,7 +430,7 @@ class CheckCaptures extends Recheck, SymTransformer:
430430
def capturedVars(sym: Symbol)(using Context): CaptureSet =
431431
myCapturedVars.getOrElseUpdate(sym,
432432
if sym.isTerm || !sym.owner.isStaticOwner
433-
then CaptureSet.Var(sym)
433+
then CaptureSet.Var(sym, nestedOK = false)
434434
else CaptureSet.empty)
435435

436436
// ---- Record Uses with MarkFree ----------------------------------------------------

‎compiler/src/dotty/tools/dotc/cc/Setup.scala‎

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -495,7 +495,8 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI:
495495
def transformResultType(tpt: TypeTree, sym: Symbol)(using Context): Unit =
496496
// First step: Transform the type and record it as knownType of tpt.
497497
try
498-
transformTT(tpt, sym, boxed = false)
498+
inContext(ctx.addMode(Mode.CCPreciseOwner)):
499+
transformTT(tpt, sym, boxed = false)
499500
catch case ex: IllegalCaptureRef =>
500501
capt.println(i"fail while transforming result type $tpt of $sym")
501502
throw ex
@@ -851,7 +852,7 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI:
851852

852853
/** Add a capture set variable to `tp` if necessary. */
853854
private def addVar(tp: Type, owner: Symbol)(using Context): Type =
854-
decorate(tp, CaptureSet.Var(owner, _))
855+
decorate(tp, CaptureSet.Var(owner, _, nestedOK = !ctx.mode.is(Mode.CCPreciseOwner)))
855856

856857
/** A map that adds <fluid> capture sets at all contra- and invariant positions
857858
* in a type where a capture set would be needed. This is used to make types

‎compiler/src/dotty/tools/dotc/core/Mode.scala‎

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -141,6 +141,15 @@ object Mode {
141141
*/
142142
val InPackageClauseName: Mode = newMode(19, "InPackageClauseName")
143143

144+
/** When creating capset Vars in cc.Setup, mark the variable to be in
145+
* the result type of the context's owner, so that nested vals cannot
146+
* be included in it.
147+
* Reuses the value of InPackageClauseName to save Mode bits.
148+
* This is OK since InPackageClauseName is only set and tested during Typer,
149+
* and CCPreciseOwner only has an effect during phase CheckCaptures.
150+
*/
151+
val CCPreciseOwner = InPackageClauseName
152+
144153
/** We are in the IDE */
145154
val Interactive: Mode = newMode(20, "Interactive")
146155

‎tests/neg-custom-args/captures/branding.scala‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -22,14 +22,14 @@ def main() =
2222
val untrustedLogger: Logger^ = ???
2323
val untrustedChannel: Channel[String]^ = ???
2424

25-
runSecure: () => // error (???, arose after changing level checking)
25+
runSecure: () =>
2626
trustedLogger.log("Hello from trusted code") // ok
2727

28-
runSecure: () => // error (???, arose after changing level checking)
28+
runSecure: () =>
2929
trustedChannel.send("I can send")
3030
trustedLogger.log(trustedChannel.recv()) // ok
3131

32-
runSecure: () => // error (???, arose after changing level checking)
32+
runSecure: () =>
3333
"I am pure" // ok
3434

3535
runSecure: () => // error

‎tests/neg-custom-args/captures/capset-members4.scala‎

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -11,8 +11,8 @@ def test =
1111
type C^ >: {z,x} <: {x,y,z}
1212

1313
val foo: Foo = ???
14-
onlyWithZ[{foo.C}] // error
15-
onlyWithZ[{z}] // error
16-
onlyWithZ[{x,z}] // error
17-
onlyWithZ[{x,y,z}] // error
14+
onlyWithZ[{foo.C}] // ok
15+
onlyWithZ[{z}] // ok
16+
onlyWithZ[{x,z}] // ok
17+
onlyWithZ[{x,y,z}] // ok
1818
onlyWithZ[{x,y}] // error

‎tests/neg-custom-args/captures/i15772.check‎

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -5,8 +5,8 @@
55
-- Error: tests/neg-custom-args/captures/i15772.scala:22:46 ------------------------------------------------------------
66
22 | val boxed1 : ((C^) => Unit) -> Unit = box1(c) // error
77
| ^^^^^^^
8-
|C^ => Unit cannot be box-converted to C{val arg: C^²}^{c} ->{cap, x} Unit
9-
|since the additional capture set {x} resulting from box conversion is not allowed in C{val arg: C^²}^{c} => Unit
8+
|C^ => Unit cannot be box-converted to C{val arg: C^²}^{c} ->{cap, c} Unit
9+
|since the additional capture set {c} resulting from box conversion is not allowed in C{val arg: C^²}^{c} => Unit
1010
|
1111
|where: => refers to the universal root capability
1212
| ^ refers to the universal root capability
@@ -15,8 +15,8 @@
1515
-- Error: tests/neg-custom-args/captures/i15772.scala:29:35 ------------------------------------------------------------
1616
29 | val boxed2 : Observe[C^] = box2(c) // error
1717
| ^^^^^^^
18-
|C^ => Unit cannot be box-converted to C{val arg: C^²}^{c} ->{cap, x} Unit
19-
|since the additional capture set {x} resulting from box conversion is not allowed in C{val arg: C^²}^{c} => Unit
18+
|C^ => Unit cannot be box-converted to C{val arg: C^²}^{c} ->{cap, c} Unit
19+
|since the additional capture set {c} resulting from box conversion is not allowed in C{val arg: C^²}^{c} => Unit
2020
|
2121
|where: => refers to the universal root capability
2222
| ^ refers to the universal root capability

‎tests/neg-custom-args/captures/i23207.check‎

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -19,18 +19,18 @@
1919
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/i23207.scala:19:2 ----------------------------------------
2020
19 | c // error
2121
| ^
22-
| Found: A^{io}
22+
| Found: A^{c}
2323
| Required: A
2424
|
25-
| Note that capability io is not included in capture set {}.
25+
| Note that capability c is not included in capture set {}.
2626
|
2727
| longer explanation available when compiling with `-explain`
2828
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/i23207.scala:27:2 ----------------------------------------
2929
27 | c // error
3030
| ^
31-
| Found: A^{io}
31+
| Found: A^{c}
3232
| Required: A
3333
|
34-
| Note that capability io is not included in capture set {}.
34+
| Note that capability c is not included in capture set {}.
3535
|
3636
| longer explanation available when compiling with `-explain`

‎tests/neg-custom-args/captures/leaky.check‎

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -10,18 +10,18 @@
1010
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/leaky.scala:24:2 -----------------------------------------
1111
24 | x // error
1212
| ^
13-
| Found: test.runnable.Transform{val fun: Any ->{a} Any}^{a}
13+
| Found: test.runnable.Transform{val fun: Any ->{f} Any}^{x}
1414
| Required: test.runnable.Transform
1515
|
16-
| Note that capability a is not included in capture set {}.
16+
| Note that capability x is not included in capture set {}.
1717
|
1818
| longer explanation available when compiling with `-explain`
1919
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/leaky.scala:31:2 -----------------------------------------
2020
31 | x // error
2121
| ^
22-
| Found: test.runnable.Transform{val fun: Any ->{a} Any}^{a}
22+
| Found: test.runnable.Transform{val fun: Any ->{f} Any}^{x}
2323
| Required: test.runnable.Transform
2424
|
25-
| Note that capability a is not included in capture set {}.
25+
| Note that capability x is not included in capture set {}.
2626
|
2727
| longer explanation available when compiling with `-explain`

‎tests/neg-custom-args/captures/real-try.check‎

Lines changed: 4 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -39,12 +39,10 @@
3939
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/real-try.scala:33:8 --------------------------------------
4040
33 | Cell(() => foo(1)) // error
4141
| ^^^^^^^^^^^^^^^^^^
42-
| Found: Cell[() => Unit]
43-
| Required: Cell[() ->'s5 Unit]^'s6
42+
| Found: Cell[() ->{canThrow$4} Unit]
43+
| Required: Cell[() ->'s5 Unit]^'s6
4444
|
45-
| Note that capability cap cannot be included in outer capture set 's5 of value b.
46-
|
47-
| where: => refers to a fresh root capability classified as Control in the type of given instance canThrow$4
48-
| cap is a fresh root capability classified as Control in the type of given instance canThrow$4
45+
| Note that capability canThrow$4, defined in method try$4
46+
| cannot be included in outer capture set 's5 of value b.
4947
|
5048
| longer explanation available when compiling with `-explain`

0 commit comments

Comments
 (0)