Skip to content

Commit f080ad0

Browse files
oderskyodersky
committed
Whether something is mutable or not depends on the context:
 - this of a Mutable type is exclusive in update methods, read-only elsewhere - a selection from a mutable type with read-only capture set is again read-only
1 parent f98c961 commit f080ad0

File tree

8 files changed

+211
-39
lines changed

8 files changed

+211
-39
lines changed

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

Lines changed: 64 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -496,6 +496,23 @@ extension (tp: Type)
496496
def classifier(using Context): ClassSymbol =
497497
tp.classSymbols.map(_.classifier).foldLeft(defn.AnyClass)(leastClassifier)
498498

499+
def exclusivity(using Context): Exclusivity =
500+
if tp.derivesFrom(defn.Caps_Mutable) then
501+
tp match
502+
case tp: Capability if tp.isExclusive => Exclusivity.OK
503+
case _ => tp.captureSet.exclusivity(tp)
504+
else Exclusivity.OK
505+
506+
def exclusivityInContext(using Context): Exclusivity = tp match
507+
case tp: ThisType =>
508+
if tp.derivesFrom(defn.Caps_Mutable)
509+
then ctx.owner.inExclusivePartOf(tp.cls)
510+
else Exclusivity.OK
511+
case tp @ TermRef(prefix: Capability, _) =>
512+
prefix.exclusivityInContext.andAlso(tp.exclusivity)
513+
case _ =>
514+
tp.exclusivity
515+
499516
extension (tp: MethodType)
500517
/** A method marks an existential scope unless it is the prefix of a curried method */
501518
def marksExistentialScope(using Context): Boolean =
@@ -629,8 +646,22 @@ extension (sym: Symbol)
629646
sym.hasAnnotation(defn.ConsumeAnnot)
630647
|| sym.info.hasAnnotation(defn.ConsumeAnnot)
631648

649+
/** An update method is either a method marked with `update` or
650+
* a setter of a non-transparent var.
651+
*/
632652
def isUpdateMethod(using Context): Boolean =
633-
sym.isAllOf(Mutable | Method, butNot = Accessor)
653+
sym.isAllOf(Mutable | Method)
654+
&& (!sym.isSetter || sym.field.is(Transparent))
655+
656+
def inExclusivePartOf(cls: Symbol)(using Context): Exclusivity =
657+
import Exclusivity.*
658+
val encl = sym.enclosingMethodOrClass.skipConstructor
659+
if sym == cls then OK // we are directly in `cls` or in one of its constructors
660+
else if encl.owner == cls then
661+
if encl.isUpdateMethod then OK
662+
else NotInUpdateMethod(encl, cls)
663+
else if encl.isStatic then OutsideClass(cls)
664+
else encl.owner.inExclusivePartOf(cls)
634665

635666
def isReadOnlyMethod(using Context): Boolean =
636667
sym.is(Method, butNot = Mutable | Accessor) && sym.owner.derivesFrom(defn.Caps_Mutable)
@@ -769,3 +800,35 @@ abstract class DeepTypeAccumulator[T](using Context) extends TypeAccumulator[T]:
769800
foldOver(acc, t)
770801
end DeepTypeAccumulator
771802

803+
/** Either OK, or a reason why capture set cannot be exclusive */
804+
enum Exclusivity:
805+
case OK
806+
807+
/** Enclosing symbol `sym` is a method of class `cls`, but not an update method */
808+
case NotInUpdateMethod(sym: Symbol, cls: Symbol)
809+
810+
/** Access to `this` from outside its class (not sure this can happen) */
811+
case OutsideClass(cls: Symbol)
812+
813+
/** A prefix type `tp` has a read-only capture set */
814+
case ReadOnly(tp: Type)
815+
816+
def isOK: Boolean = this == OK
817+
818+
def andAlso(that: Exclusivity): Exclusivity =
819+
if this == OK then that else this
820+
821+
/** A textual description why `qualType` is not exclusive */
822+
def description(qualType: Type)(using Context): String = this.runtimeChecked match
823+
case Exclusivity.ReadOnly(tp) =>
824+
if qualType eq tp then
825+
i"its capture set ${qualType.captureSet} is read-only"
826+
else
827+
i"the capture set ${tp.captureSet} of its prefix $tp is read-only"
828+
case Exclusivity.NotInUpdateMethod(sym: Symbol, cls: Symbol) =>
829+
i"the access is in $sym, which is not an update method"
830+
case Exclusivity.OutsideClass(cls: Symbol) =>
831+
i"the access from is from ouside $cls"
832+
833+
end Exclusivity
834+

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

Lines changed: 4 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -145,6 +145,9 @@ sealed abstract class CaptureSet extends Showable:
145145
final def isExclusive(using Context): Boolean =
146146
elems.exists(_.isExclusive)
147147

148+
def exclusivity(tp: Type)(using Context): Exclusivity =
149+
if isExclusive then Exclusivity.OK else Exclusivity.ReadOnly(tp)
150+
148151
/** Similar to isExlusive, but also includes capture set variables
149152
* with unknown status.
150153
*/
@@ -1364,7 +1367,7 @@ object CaptureSet:
13641367
def description(using Context): String =
13651368
def ofType(tp: Type) = if tp.exists then i"of the mutable type $tp" else "of a mutable type"
13661369
i"""$cs is an exclusive capture set ${ofType(hi)},
1367-
|it cannot subsume a read-only capture set ${ofType(lo)}."""
1370+
|it cannot subsume a read-only capture set ${ofType(lo)}"""
13681371

13691372
/** A VarState serves as a snapshot mechanism that can undo
13701373
* additions of elements or super sets if an operation fails

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

Lines changed: 24 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -724,13 +724,16 @@ class CheckCaptures extends Recheck, SymTransformer:
724724
case _ => denot
725725

726726
// Don't allow update methods to be called unless the qualifier captures
727-
// an exclusive reference. TODO This should probably rolled into
728-
// qualifier logic once we have it.
729-
if tree.symbol.isUpdateMethod && !qualType.captureSet.isExclusive then
730-
report.error(
731-
em"""cannot call update ${tree.symbol} from $qualType,
732-
|since its capture set ${qualType.captureSet} is read-only""",
733-
tree.srcPos)
727+
// an exclusive reference.
728+
if tree.symbol.isUpdateMethod then
729+
qualType.exclusivityInContext match
730+
case Exclusivity.OK =>
731+
capt.println(i"exclusive $qualType in ${ctx.owner}, ${qualType.derivesFrom(defn.Caps_Mutable)}")
732+
case err =>
733+
report.error(
734+
em"""cannot call update ${tree.symbol} from $qualType,
735+
|since ${err.description(qualType)}""",
736+
tree.srcPos)
734737

735738
val origSelType = recheckSelection(tree, qualType, name, disambiguate)
736739
val selType = mapResultRoots(origSelType, tree.symbol)
@@ -1836,6 +1839,17 @@ class CheckCaptures extends Recheck, SymTransformer:
18361839
actual
18371840
end improveReadOnly
18381841

1842+
def adaptReadOnly(improved: Type, original: Type, expected: Type, tree: Tree)(using Context): Type = improved match
1843+
case improved @ CapturingType(parent, refs)
1844+
if parent.derivesFrom(defn.Caps_Mutable)
1845+
&& expected.isValueType
1846+
&& refs.isExclusive
1847+
&& !original.exclusivityInContext.isOK =>
1848+
improved.derivedCapturingType(parent, refs.readOnly)
1849+
.showing(i"Adapted readonly $improved for $tree with original = $original in ${ctx.owner} --> $result", capt)
1850+
case _ =>
1851+
improved
1852+
18391853
/* Currently not needed since it forms part of `adapt`
18401854
private def improve(actual: Type, prefix: Type)(using Context): Type =
18411855
val widened = actual.widen.dealiasKeepAnnots
@@ -1873,10 +1887,11 @@ class CheckCaptures extends Recheck, SymTransformer:
18731887
val widened = actual.widen.dealiasKeepAnnots.dropUseAndConsumeAnnots
18741888
val improvedVAR = improveCaptures(widened, actual)
18751889
val improved = improveReadOnly(improvedVAR, expected)
1890+
val adaptedReadOnly = adaptReadOnly(improved, actual, expected, tree)
18761891
val adapted = adaptBoxed(
1877-
improved.withReachCaptures(actual), expected, tree,
1892+
adaptedReadOnly.withReachCaptures(actual), expected, tree,
18781893
covariant = true, alwaysConst = false)
1879-
if adapted eq improvedVAR // no .rd improvement, no box-adaptation
1894+
if adapted eq improvedVAR // no .rd improvement or adaptation, no box-adaptation
18801895
then actual // might as well use actual instead of improved widened
18811896
else adapted.showing(i"adapt $actual vs $expected = $adapted", capt)
18821897
end adapt

‎tests/neg-custom-args/captures/linear-buffer.check‎

Lines changed: 41 additions & 27 deletions
Original file line numberDiff line numberDiff line change
@@ -1,55 +1,69 @@
1+
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/linear-buffer.scala:7:29 ---------------------------------
2+
7 | def bar: BadBuffer[T]^ = this // error
3+
| ^^^^
4+
| Found: BadBuffer[T]^{BadBuffer.this.rd}
5+
| Required: BadBuffer[T]^
6+
|
7+
| Note that capability BadBuffer.this.rd is not included in capture set {}.
8+
|
9+
| Note that {cap} is an exclusive capture set of the mutable type BadBuffer[T]^,
10+
| it cannot subsume a read-only capture set of the mutable type BadBuffer[T]^{BadBuffer.this.rd}.
11+
|
12+
| where: ^ and cap refer to a fresh root capability classified as Mutable in the result type of method bar
13+
|
14+
| longer explanation available when compiling with `-explain`
115
-- Error: tests/neg-custom-args/captures/linear-buffer.scala:5:27 ------------------------------------------------------
216
5 | update def append(x: T): BadBuffer[T]^ = this // error
317
| ^^^^^^^^^^^^^
418
| Separation failure: method append's result type BadBuffer[T]^ hides non-local this of class class BadBuffer.
519
| The access must be in a consume method to allow this.
6-
-- Error: tests/neg-custom-args/captures/linear-buffer.scala:7:29 ------------------------------------------------------
7-
7 | def bar: BadBuffer[T]^ = this // error // error
8-
| ^^^^
9-
| Separation failure: Illegal access to {BadBuffer.this} which is hidden by the previous definition
10-
| of method append with result type BadBuffer[T]^.
11-
| This type hides capabilities {BadBuffer.this}
12-
|
13-
| where: ^ refers to a fresh root capability classified as Mutable in the result type of method append
14-
-- Error: tests/neg-custom-args/captures/linear-buffer.scala:7:13 ------------------------------------------------------
15-
7 | def bar: BadBuffer[T]^ = this // error // error
16-
| ^^^^^^^^^^^^^
17-
| Separation failure: method bar's result type BadBuffer[T]^ hides non-local this of class class BadBuffer.
18-
| The access must be in a consume method to allow this.
19-
-- Error: tests/neg-custom-args/captures/linear-buffer.scala:19:17 -----------------------------------------------------
20-
19 | val buf3 = app(buf, 3) // error
20+
-- Error: tests/neg-custom-args/captures/linear-buffer.scala:10:29 -----------------------------------------------------
21+
10 | def bar: BadBuffer[T]^ = this // error // error
22+
| ^^^^
23+
| Separation failure: Illegal access to {BadBuffer.this} which is hidden by the previous definition
24+
| of method append with result type BadBuffer[T]^.
25+
| This type hides capabilities {BadBuffer.this}
26+
|
27+
| where: ^ refers to a fresh root capability classified as Mutable in the result type of method append
28+
-- Error: tests/neg-custom-args/captures/linear-buffer.scala:10:13 -----------------------------------------------------
29+
10 | def bar: BadBuffer[T]^ = this // error // error
30+
| ^^^^^^^^^^^^^
31+
| Separation failure: method bar's result type BadBuffer[T]^ hides non-local this of class class BadBuffer.
32+
| The access must be in a consume method to allow this.
33+
-- Error: tests/neg-custom-args/captures/linear-buffer.scala:22:17 -----------------------------------------------------
34+
22 | val buf3 = app(buf, 3) // error
2135
| ^^^
2236
| Separation failure: Illegal access to (buf : Buffer[Int]^), which was passed to a
23-
| consume parameter or was used as a prefix to a consume method on line 17
37+
| consume parameter or was used as a prefix to a consume method on line 20
2438
| and therefore is no longer available.
2539
|
2640
| where: ^ refers to a fresh root capability classified as Mutable in the type of parameter buf
27-
-- Error: tests/neg-custom-args/captures/linear-buffer.scala:26:17 -----------------------------------------------------
28-
26 | val buf3 = app(buf1, 4) // error
41+
-- Error: tests/neg-custom-args/captures/linear-buffer.scala:29:17 -----------------------------------------------------
42+
29 | val buf3 = app(buf1, 4) // error
2943
| ^^^^
3044
| Separation failure: Illegal access to (buf1 : Buffer[Int]^), which was passed to a
31-
| consume parameter or was used as a prefix to a consume method on line 24
45+
| consume parameter or was used as a prefix to a consume method on line 27
3246
| and therefore is no longer available.
3347
|
3448
| where: ^ refers to a fresh root capability classified as Mutable in the type of value buf1
35-
-- Error: tests/neg-custom-args/captures/linear-buffer.scala:34:17 -----------------------------------------------------
36-
34 | val buf3 = app(buf1, 4) // error
49+
-- Error: tests/neg-custom-args/captures/linear-buffer.scala:37:17 -----------------------------------------------------
50+
37 | val buf3 = app(buf1, 4) // error
3751
| ^^^^
3852
| Separation failure: Illegal access to (buf1 : Buffer[Int]^), which was passed to a
39-
| consume parameter or was used as a prefix to a consume method on line 31
53+
| consume parameter or was used as a prefix to a consume method on line 34
4054
| and therefore is no longer available.
4155
|
4256
| where: ^ refers to a fresh root capability classified as Mutable in the type of value buf1
43-
-- Error: tests/neg-custom-args/captures/linear-buffer.scala:44:17 -----------------------------------------------------
44-
44 | val buf3 = app(buf1, 4) // error
57+
-- Error: tests/neg-custom-args/captures/linear-buffer.scala:47:17 -----------------------------------------------------
58+
47 | val buf3 = app(buf1, 4) // error
4559
| ^^^^
4660
| Separation failure: Illegal access to (buf1 : Buffer[Int]^), which was passed to a
47-
| consume parameter or was used as a prefix to a consume method on line 39
61+
| consume parameter or was used as a prefix to a consume method on line 42
4862
| and therefore is no longer available.
4963
|
5064
| where: ^ refers to a fresh root capability classified as Mutable in the type of value buf1
51-
-- Error: tests/neg-custom-args/captures/linear-buffer.scala:48:8 ------------------------------------------------------
52-
48 | app(buf, 1) // error
65+
-- Error: tests/neg-custom-args/captures/linear-buffer.scala:51:8 ------------------------------------------------------
66+
51 | app(buf, 1) // error
5367
| ^^^
5468
| Separation failure: (buf : Buffer[Int]^) appears in a loop, therefore it cannot
5569
| be passed to a consume parameter or be used as a prefix of a consume method call.

‎tests/neg-custom-args/captures/linear-buffer.scala‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -4,6 +4,9 @@ import language.experimental.captureChecking
44
class BadBuffer[T] extends Mutable:
55
update def append(x: T): BadBuffer[T]^ = this // error
66
def foo =
7+
def bar: BadBuffer[T]^ = this // error
8+
bar
9+
update def updateFoo =
710
def bar: BadBuffer[T]^ = this // error // error
811
bar
912

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

Lines changed: 45 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,45 @@
1+
-- Error: tests/neg-custom-args/captures/mutability.scala:4:24 ---------------------------------------------------------
2+
4 | def hide(x: T) = this.set(x) // error
3+
| ^^^^^^^^
4+
| cannot call update method set from (Ref.this : Ref[T]^),
5+
| since the access is in method hide, which is not an update method
6+
|
7+
| where: ^ refers to a fresh root capability classified as Mutable in the type of class Ref
8+
-- Error: tests/neg-custom-args/captures/mutability.scala:9:9 ----------------------------------------------------------
9+
9 | self.set(x) // error
10+
| ^^^^^^^^
11+
| cannot call update method set from (self : Ref[T^{}]^{Ref.this.rd}),
12+
| since its capture set {self} is read-only
13+
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/mutability.scala:10:25 -----------------------------------
14+
10 | val self2: Ref[T]^ = this // error
15+
| ^^^^
16+
| Found: Ref[T]^{Ref.this.rd}
17+
| Required: Ref[T]^
18+
|
19+
| Note that capability Ref.this.rd is not included in capture set {}.
20+
|
21+
| Note that {cap} is an exclusive capture set of the mutable type Ref[T]^,
22+
| it cannot subsume a read-only capture set of the mutable type Ref[T]^{Ref.this.rd}.
23+
|
24+
| where: ^ and cap refer to a fresh root capability classified as Mutable in the type of value self2
25+
|
26+
| longer explanation available when compiling with `-explain`
27+
-- Error: tests/neg-custom-args/captures/mutability.scala:15:25 --------------------------------------------------------
28+
15 | def set(x: T) = this.x.set(x) // error
29+
| ^^^^^^^^^^
30+
| cannot call update method set from (Ref2.this.x : Ref[T^{}]^),
31+
| since the access is in method set, which is not an update method
32+
|
33+
| where: ^ refers to a fresh root capability classified as Mutable in the type of value x
34+
-- Error: tests/neg-custom-args/captures/mutability.scala:22:5 ---------------------------------------------------------
35+
22 | r1.set(33) // error
36+
| ^^^^^^
37+
| cannot call update method set from (r1 : Ref[Int]),
38+
| since its capture set {r1} is read-only
39+
-- Error: tests/neg-custom-args/captures/mutability.scala:27:7 ---------------------------------------------------------
40+
27 | r3.x.set(33) // error
41+
| ^^^^^^^^
42+
| cannot call update method set from (r3.x : Ref[Int]^),
43+
| since the capture set {r3} of its prefix (r3 : Ref2[Int]) is read-only
44+
|
45+
| where: ^ refers to a fresh root capability classified as Mutable in the type of value x

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

Lines changed: 29 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,29 @@
1+
class Ref[T](init: T) extends caps.Mutable:
2+
var x: T = init
3+
update def set(x: T) = this.x = x
4+
def hide(x: T) = this.set(x) // error
5+
update def hide2(x: T) = set(x) // ok
6+
7+
def sneakyHide(x: T) =
8+
val self = this
9+
self.set(x) // error
10+
val self2: Ref[T]^ = this // error
11+
self2.set(x)
12+
13+
class Ref2[T](init: T) extends caps.Mutable:
14+
val x = Ref[T](init)
15+
def set(x: T) = this.x.set(x) // error
16+
update def set2(x: T) = this.x.set(x) // ok
17+
18+
def test =
19+
val r = Ref(22)
20+
r.set(33) // ok
21+
val r1: Ref[Int] = Ref(22)
22+
r1.set(33) // error
23+
24+
val r2 = Ref2(22)
25+
r2.x.set(33) // ok
26+
val r3: Ref2[Int] = Ref2(22)
27+
r3.x.set(33) // error
28+
29+

‎tests/neg-custom-args/captures/ro-mut-conformance.check‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -12,7 +12,7 @@
1212
| Note that capability a is not included in capture set {}.
1313
|
1414
| Note that {cap} is an exclusive capture set of the mutable type Ref^,
15-
| it cannot subsume a read-only capture set of the mutable type (a : Ref)..
15+
| it cannot subsume a read-only capture set of the mutable type (a : Ref).
1616
|
1717
| where: ^ and cap refer to a fresh root capability classified as Mutable in the type of value t
1818
|

0 commit comments

Comments
 (0)