Skip to content

Changes to Mutable #24352

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
wants to merge 1 commit into
base: main
Choose a base branch
from
+484 −156
Open

Changes to Mutable #24352

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
8 changes: 4 additions & 4 deletions compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -573,12 +573,12 @@ class CheckCaptures extends Recheck, SymTransformer:
// fresh capabilities. We do check that they hide no parameter reach caps in checkEscapingUses
case _ =>

def checkReadOnlyMethod(included: CaptureSet, env: Env): Unit =
def checkReadOnlyMethod(included: CaptureSet, meth: Symbol): Unit =
included.checkAddedElems: elem =>
if elem.isExclusive then
report.error(
em"""Read-only ${env.owner} accesses exclusive capability $elem;
|${env.owner} should be declared an update method to allow this.""",
em"""Read-only $meth accesses exclusive capability $elem;
|$meth should be declared an update method to allow this.""",
tree.srcPos)

def recur(cs: CaptureSet, env: Env, lastEnv: Env | Null): Unit =
Expand All @@ -599,7 +599,7 @@ class CheckCaptures extends Recheck, SymTransformer:
val nextEnv = nextEnvToCharge(env)
if nextEnv != null && !nextEnv.owner.isStaticOwner then
if env.owner.isReadOnlyMethodOrLazyVal && nextEnv.owner != env.owner then
checkReadOnlyMethod(included, env)
checkReadOnlyMethod(included, env.owner)
recur(included, nextEnv, env)
// Under deferredReaches, don't propagate out of methods inside terms.
// The use set of these methods will be charged when that method is called.
Expand Down
6 changes: 4 additions & 2 deletions compiler/src/dotty/tools/dotc/cc/Mutability.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -47,7 +47,8 @@ object Mutability:

extension (sym: Symbol)
/** An update method is either a method marked with `update` or
* a setter of a non-transparent var.
* a setter of a non-transparent var. `update` is implicit for `consume` methods
* of Mutable classes.
*/
def isUpdateMethod(using Context): Boolean =
sym.isAllOf(Mutable | Method)
Expand All @@ -63,8 +64,9 @@ object Mutability:
private def inExclusivePartOf(cls: Symbol)(using Context): Exclusivity =
import Exclusivity.*
if sym == cls then OK // we are directly in `cls` or in one of its constructors
else if sym.isUpdateMethod then OK
else if sym.owner == cls then
if sym.isUpdateMethod || sym.isConstructor then OK
if sym.isConstructor then OK
else NotInUpdateMethod(sym, cls)
else if sym.isStatic then OutsideClass(cls)
else sym.owner.inExclusivePartOf(cls)
Expand Down
6 changes: 5 additions & 1 deletion compiler/src/dotty/tools/dotc/typer/Namer.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -995,8 +995,12 @@ class Namer { typer: Typer =>
end if
}

/** Add an implicit Mutable flag to consume methods in Mutable classes. This
* turns the method into an update method.
*/
private def normalizeFlags(denot: SymDenotation)(using Context): Unit =
if denot.is(Method) && denot.hasAnnotation(defn.ConsumeAnnot) then
if denot.is(Method) && denot.hasAnnotation(defn.ConsumeAnnot)
&& denot.owner.derivesFrom(defn.Caps_Mutable) then
denot.setFlag(Mutable)

/** Intentionally left without `using Context` parameter. We need
Expand Down
4 changes: 2 additions & 2 deletions library/src/scala/caps/package.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -63,7 +63,7 @@ type Shared = SharedCapability
* During separation checking, exclusive usage of marked capabilities will be enforced.
*/
@experimental
trait ExclusiveCapability extends Capability, Classifier
trait ExclusiveCapability extends Capability

@experimental
type Exclusive = ExclusiveCapability
Expand All @@ -80,7 +80,7 @@ trait Control extends SharedCapability, Classifier

/** Marker trait for classes with methods that require an exclusive reference. */
@experimental
trait Mutable extends ExclusiveCapability, Classifier
trait Mutable extends ExclusiveCapability

/** Marker trait for classes with reader methods, typically extended by Mutable classes */
@experimental
Expand Down
6 changes: 3 additions & 3 deletions tests/neg-custom-args/captures/classified-inheritance.check
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,8 +1,8 @@
-- Error: tests/neg-custom-args/captures/classified-inheritance.scala:5:6 ----------------------------------------------
5 |class C2 extends caps.Control, caps.Mutable // error
5 |class C2 extends caps.Control, caps.Read // error
| ^
| class C2 inherits two unrelated classifier traits: trait Mutable and trait Control
| class C2 inherits two unrelated classifier traits: trait Read and trait Control
-- 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 Mutable
| class C3 inherits two unrelated classifier traits: trait Control and trait Read
4 changes: 2 additions & 2 deletions tests/neg-custom-args/captures/classified-inheritance.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2,9 +2,9 @@ import language.experimental.captureChecking

class C1 extends caps.Control, caps.SharedCapability // OK

class C2 extends caps.Control, caps.Mutable // error
class C2 extends caps.Control, caps.Read // error

trait Async extends caps.Control
class Matrix extends caps.Mutable
class Matrix extends caps.Read

class C3 extends Matrix, Async // error
2 changes: 1 addition & 1 deletion tests/neg-custom-args/captures/classifiers-1.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
class M extends caps.Mutable
class M extends caps.Read

class M1(x: Int => Int) extends M // error

Expand Down
6 changes: 3 additions & 3 deletions tests/neg-custom-args/captures/i23726.check
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -14,7 +14,7 @@
| The two sets overlap at : {a}
|
|where: ^ refers to a fresh root capability classified as Mutable in the type of value a
| ^² refers to a fresh root capability classified as Mutable created in method test1 when checking argument to parameter x of method apply
| ^² refers to a fresh root capability created in method test1 when checking argument to parameter x of method apply
-- Error: tests/neg-custom-args/captures/i23726.scala:16:5 -------------------------------------------------------------
16 | f3(b) // error
| ^
Expand All @@ -31,7 +31,7 @@
| The two sets overlap at : {b}
|
|where: ^ refers to a fresh root capability classified as Mutable in the type of value b
| ^² refers to a fresh root capability classified as Mutable created in method test1 when checking argument to parameter x of method apply
| ^² refers to a fresh root capability created in method test1 when checking argument to parameter x of method apply
-- Error: tests/neg-custom-args/captures/i23726.scala:24:5 -------------------------------------------------------------
24 | f7(a) // error
| ^
Expand All @@ -48,4 +48,4 @@
| The two sets overlap at : {a}
|
|where: ^ refers to a fresh root capability classified as Mutable in the type of value a
| ^² refers to a fresh root capability classified as Mutable created in method test1 when checking argument to parameter x of method apply
| ^² refers to a fresh root capability created in method test1 when checking argument to parameter x of method apply
3 changes: 2 additions & 1 deletion tests/neg-custom-args/captures/i24310.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -11,11 +11,12 @@ class Matrix(val f: () => Int) extends Mutable:
update def add(): Unit = ()


@main def test =
def test(consume proc: () => Int) =
val r: Ref^ = Ref()
val m: Matrix^ = Matrix(() => 42)
val m2: Matrix^ = Matrix(() => m.run())
val m3: Matrix^ = Matrix(() => r.get())
val m4: Matrix^ = Matrix(proc)

def par(f1: () => Int, f2: () => Int): Unit =
println(s"par results: ${f1()} and ${f2()}")
Expand Down
4 changes: 2 additions & 2 deletions tests/neg-custom-args/captures/lazyvals-sep.check
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -34,7 +34,7 @@
|Note that {cap} is an exclusive capture set of the mutable type Ref^,
|it cannot subsume a read-only capture set of the mutable type Ref^{TestClass.this.r.rd}.
|
|where: ^ and cap refer to a fresh root capability classified as Mutable created in lazy value lazyVal8 when checking argument to parameter ref of constructor Wrapper
|where: ^ and cap refer to a fresh root capability created in lazy value lazyVal8 when checking argument to parameter ref of constructor Wrapper
|
| longer explanation available when compiling with `-explain`
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/lazyvals-sep.scala:77:12 ---------------------------------
Expand All @@ -48,7 +48,7 @@
|Note that {cap} is an exclusive capture set of the mutable type Ref^,
|it cannot subsume a read-only capture set of the mutable type Ref^{TestClass.this.r.rd}.
|
|where: ^ and cap refer to a fresh root capability classified as Mutable created in lazy value lazyVal9 when checking argument to parameter ref of constructor Wrapper
|where: ^ and cap refer to a fresh root capability created in lazy value lazyVal9 when checking argument to parameter ref of constructor Wrapper
|
| longer explanation available when compiling with `-explain`
-- Error: tests/neg-custom-args/captures/lazyvals-sep.scala:82:8 -------------------------------------------------------
Expand Down
10 changes: 5 additions & 5 deletions tests/neg-custom-args/captures/linear-buffer-2.check
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -5,35 +5,35 @@
| consume parameter or was used as a prefix to a consume method on line 11
| and therefore is no longer available.
|
| where: ^ refers to a fresh root capability classified as Mutable 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.
|
| where: ^ refers to a fresh root capability classified as Mutable 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.
|
| where: ^ refers to a fresh root capability classified as Mutable 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.
|
| where: ^ refers to a fresh root capability classified as Mutable 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.
|
| where: ^ refers to a fresh root capability classified as Mutable in the type of parameter buf
| where: ^ refers to a fresh root capability in the type of parameter buf
36 changes: 18 additions & 18 deletions tests/neg-custom-args/captures/linear-buffer.check
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,15 +1,15 @@
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/linear-buffer.scala:7:29 ---------------------------------
7 | def bar: BadBuffer[T]^ = this // error
| ^^^^
| Found: BadBuffer[T]^{BadBuffer.this.rd}
| Required: BadBuffer[T]^
| Found: BadBuffer[T]^{BadBuffer.this.rd}
| Required: BadBuffer[T]^
|
| Note that capability BadBuffer.this.rd is not included in capture set {}.
| Note that capability BadBuffer.this.rd is not included in capture set {}.
|
| Note that {cap} is an exclusive capture set of the mutable type BadBuffer[T]^,
| it cannot subsume a read-only capture set of the mutable type BadBuffer[T]^{BadBuffer.this.rd}.
| Note that {cap} is an exclusive capture set of the mutable type BadBuffer[T]^,
| it cannot subsume a read-only capture set of the mutable type BadBuffer[T]^{BadBuffer.this.rd}.
|
| where: ^ and cap refer to a fresh root capability classified as Mutable in the result type of method bar
| where: ^ and cap refer to a fresh root capability in the result type of method bar
|
| longer explanation available when compiling with `-explain`
-- Error: tests/neg-custom-args/captures/linear-buffer.scala:5:27 ------------------------------------------------------
Expand All @@ -20,11 +20,11 @@
-- Error: tests/neg-custom-args/captures/linear-buffer.scala:10:29 -----------------------------------------------------
10 | def bar: BadBuffer[T]^ = this // error // error
| ^^^^
| Separation failure: Illegal access to {BadBuffer.this} which is hidden by the previous definition
| of method append with result type BadBuffer[T]^.
| This type hides capabilities {BadBuffer.this}
| Separation failure: Illegal access to {BadBuffer.this} which is hidden by the previous definition
| of method append with result type BadBuffer[T]^.
| This type hides capabilities {BadBuffer.this}
|
| where: ^ refers to a fresh root capability classified as Mutable in the result type of method append
| where: ^ refers to a fresh root capability in the result type of method append
-- Error: tests/neg-custom-args/captures/linear-buffer.scala:10:13 -----------------------------------------------------
10 | def bar: BadBuffer[T]^ = this // error // error
| ^^^^^^^^^^^^^
Expand All @@ -33,39 +33,39 @@
-- Error: tests/neg-custom-args/captures/linear-buffer.scala:22:17 -----------------------------------------------------
22 | 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 20
| and therefore is no longer available.
| 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 20
| and therefore is no longer available.
|
| where: ^ refers to a fresh root capability classified as Mutable 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:29:17 -----------------------------------------------------
29 | 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 27
| and therefore is no longer available.
|
| where: ^ refers to a fresh root capability classified as Mutable 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:37:17 -----------------------------------------------------
37 | 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 34
| and therefore is no longer available.
|
| where: ^ refers to a fresh root capability classified as Mutable 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:47:17 -----------------------------------------------------
47 | 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 42
| and therefore is no longer available.
|
| where: ^ refers to a fresh root capability classified as Mutable 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:51:8 ------------------------------------------------------
51 | 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.
|
| where: ^ refers to a fresh root capability classified as Mutable in the type of parameter buf
| where: ^ refers to a fresh root capability in the type of parameter buf
4 changes: 2 additions & 2 deletions tests/neg-custom-args/captures/matrix.check
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -13,7 +13,7 @@
| Footprint set of third argument : {m2}
| The two sets overlap at : {m2}
|
|where: cap is a fresh root capability classified as Mutable created in method Test when checking argument to parameter y of method mul
|where: cap is a fresh root capability created in method Test when checking argument to parameter y of method mul
-- Error: tests/neg-custom-args/captures/matrix.scala:30:11 ------------------------------------------------------------
30 | mul1(m1, m2, m2) // error: will fail separation checking
| ^^
Expand All @@ -29,4 +29,4 @@
| Footprint set of third argument : {m2}
| The two sets overlap at : {m2}
|
|where: cap is a fresh root capability classified as Mutable created in method Test when checking argument to parameter y of method mul1
|where: cap is a fresh root capability created in method Test when checking argument to parameter y of method mul1
Loading
Loading