Enforce mutable field restrictions under separation checking.

Fields are only allowed in stateful classes unless marked with @untrackedCaptures.

Author: odersky

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

@@ -1170,7 +1170,7 @@ class CheckCaptures extends Recheck, SymTransformer:
                   ""
               disallowBadRootsIn(
                 tree.tpt.nuType, NoSymbol, i"Mutable $sym", "have type", addendum, sym.srcPos)
-            if ccConfig.noUnsafeMutableFields
+            if ccConfig.strictMutability
                 && sym.owner.isClass
                 && !sym.owner.derivesFrom(defn.Caps_Stateful)
                 && !sym.hasAnnotation(defn.UntrackedCapturesAnnot) then

compiler/src/dotty/tools/dotc/cc/ccConfig.scala

@@ -48,11 +48,6 @@ object ccConfig:
    */
   inline val useSpanCapset = false
 
-  /** If true force all mutable fields to be in Stateful classes, unless they
-   *  are annotated with @untrackedCaptures
-   */
-  inline val noUnsafeMutableFields = false
-
   /** If true, do level checking for FreshCap instances */
   def useFreshLevels(using Context): Boolean =
     Feature.sourceVersion.stable.isAtLeast(SourceVersion.`3.7`)
@@ -65,7 +60,10 @@ object ccConfig:
   def allowUse(using Context): Boolean =
     Feature.sourceVersion.stable.isAtMost(SourceVersion.`3.7`)
 
-  /** Treat arrays as mutable types. Enabled under separation checking */
+  /** Treat arrays as mutable types and force all mutable fields to be in Stateful
+   *  classes, unless they are annotated with @untrackedCaptures.
+   *  Enabled under separation checking
+   */
   def strictMutability(using Context): Boolean =
     Feature.enabled(Feature.separationChecking)
 

tests/neg-custom-args/captures/cc-poly-source.scala

@@ -10,7 +10,7 @@ import caps.use
   class Listener
 
   class Source[X^]:
-    private var listeners: Set[Listener^{X}] = Set.empty
+    @caps.unsafe.untrackedCaptures private var listeners: Set[Listener^{X}] = Set.empty
     def register(x: Listener^{X}): Unit =
       listeners += x
 

tests/neg-custom-args/captures/class-level-attack.check

@@ -1,13 +1,13 @@
--- [E007] Type Mismatch Error: tests/neg-custom-args/captures/class-level-attack.scala:17:26 ---------------------------
-17 |  def set(x: IO^) = r.put(x)  // error
-   |                          ^
-   |                          Found:    IO^{x}
-   |                          Required: IO^
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/class-level-attack.scala:17:33 ---------------------------
+17 |  update def set(x: IO^) = r.put(x)  // error
+   |                                 ^
+   |                                Found:    IO^{x}
+   |                                Required: IO^
    |
-   |                          Note that capability x is not included in capture set {cap}
-   |                          because (x : IO^²) in method set is not visible from cap in value r.
+   |                                Note that capability x is not included in capture set {cap}
+   |                                because (x : IO^²) in method set is not visible from cap in value r.
    |
-   |                          where:    ^ and cap refer to a fresh root capability in the type of value r
-   |                                    ^²        refers to a fresh root capability in the type of parameter x
+   |                                where:    ^ and cap refer to a fresh root capability in the type of value r
+   |                                          ^²        refers to a fresh root capability in the type of parameter x
    |
    | longer explanation available when compiling with `-explain`

tests/neg-custom-args/captures/class-level-attack.scala

@@ -3,18 +3,18 @@ import caps.*
 
 class IO
 
-class Ref[X](init: X):
+class Ref[X](init: X) extends caps.Stateful:
   var x = init
   def get: X = x
-  def put(y: X): Unit = x = y
+  update def put(y: X): Unit = x = y
 
-class C(io: IO^):
-  val r: Ref[IO^] = Ref[IO^](io)
+class C(io: IO^) extends caps.Stateful:
+  val r: Ref[IO^]^ = Ref[IO^](io)
     //Type variable X of constructor Ref cannot be instantiated to box IO^ since
     //that type captures the root capability `cap`.
     // where: ^ refers to the universal root capability
   val r2: Ref[IO^] = Ref(io)
-  def set(x: IO^) = r.put(x)  // error
+  update def set(x: IO^) = r.put(x)  // error
 
 def outer(outerio: IO^) =
   val c = C(outerio)

tests/neg-custom-args/captures/filevar-expanded.scala

@@ -23,7 +23,7 @@ object test2:
   class File:
     def write(x: String): Unit = ???
 
-  class Service(tracked val io: IO^):
+  class Service(tracked val io: IO^) extends caps.Stateful:
     var file: File^{io} = uninitialized
     def log = file.write("log")
 

tests/neg-custom-args/captures/filevar-multi-ios.scala

@@ -8,7 +8,7 @@ class File:
 
 object test1:
 
-  class Service(val io: IO, val io2: IO):
+  class Service(val io: IO, val io2: IO) extends caps.Stateful:
     var file: File^{io} = uninitialized
     var file2: File^{io2} = uninitialized
     def log = file.write("log")
@@ -25,7 +25,7 @@ object test1:
 
 object test2:
 
-  class Service(tracked val io: IO, tracked val io2: IO):
+  class Service(tracked val io: IO, tracked val io2: IO) extends caps.Stateful:
     var file: File^{io} = uninitialized
     var file2: File^{io2} = uninitialized
     def log = file.write("log")

tests/neg-custom-args/captures/filevar.scala

@@ -4,7 +4,7 @@ import compiletime.uninitialized
 class File:
   def write(x: String): Unit = ???
 
-class Service:
+class Service extends caps.Stateful:
   var file: File^ = uninitialized  //OK, was  error under sealed
   def log = file.write("log") // OK, was error under unsealed
 

tests/neg-custom-args/captures/i21920.scala

@@ -11,7 +11,7 @@ final class Cell[A](head: () => IterableOnce[A]^):
   def headIterator: Iterator[A]^{this} = head().iterator
 
 class File private ():
-  private var closed = false
+  @caps.unsafe.untrackedCaptures private var closed = false
 
   def close() = closed = true