Ensure that read-only methods don't use exclusive capabilities

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

@@ -152,7 +152,7 @@ sealed abstract class CaptureSet extends Showable:
   final def isExclusive(using Context): Boolean =
     elems.exists(_.isExclusive)
 
-  /** Similar to isExlusive, but also includes capture set variables
+  /** Similar to isExclusive, but also includes capture set variables
    *  with unknown status.
    */
   final def maybeExclusive(using Context): Boolean = reporting.trace(i"mabe exclusive $this"):
@@ -482,9 +482,16 @@ sealed abstract class CaptureSet extends Showable:
    *  Fresh instances count as good as long as their ccOwner is outside `upto`.
    *  If `upto` is NoSymbol, all Fresh instances are admitted.
    */
-  def disallowBadRoots(upto: Symbol)(handler: () => Context ?=> Unit)(using Context): this.type =
-    if elems.exists(isBadRoot(upto, _)) then handler()
-    this
+  def disallowBadRoots(upto: Symbol)(handler: () => Context ?=> Unit)(using Context): Unit =
+    checkAddedElems: elem =>
+      if isBadRoot(upto, elem) then handler()
+
+  /** Invoke handler for each element currently in the set and each element
+   *  added to it in the future.
+   */
+  def checkAddedElems(handler: Capability => Context ?=> Unit)(using Context): Unit =
+    elems.foreach: elem =>
+      handler(elem)
 
   /** Invoke handler on the elements to ensure wellformedness of the capture set.
    *  The handler might add additional elements to the capture set.
@@ -731,8 +738,8 @@ object CaptureSet:
             elems -= empty
       this
 
-    /** A handler to be invoked if the root reference `cap` is added to this set */
-    var rootAddedHandler: () => Context ?=> Unit = () => ()
+    /** A list of handlers to be invoked when a new element is added to this set */
+    var newElemAddedHandlers: List[Capability => Context ?=> Unit] = Nil
 
     /** The limit deciding which capture roots are bad (i.e. cannot be contained in this set).
      *  @see isBadRoot for details.
@@ -761,9 +768,6 @@ object CaptureSet:
       || super.tryClassifyAs(cls)
           && { narrowClassifier(cls); true }
 
-    /** A handler to be invoked when new elems are added to this set */
-    var newElemAddedHandler: Capability => Context ?=> Unit = _ => ()
-
     var description: String = ""
 
     private var myRepr: Name | Null = null
@@ -816,8 +820,7 @@ object CaptureSet:
         catch case ex: AssertionError =>
           println(i"error for incl $elem in $this, ${summon[VarState].toString}")
           throw ex
-        if isBadRoot(elem) then
-          rootAddedHandler()
+        newElemAddedHandlers.foreach(_(elem))
         val normElem = if isMaybeSet then elem else elem.stripMaybe
         // assert(id != 5 || elems.size != 3, this)
         val res = deps.forall: dep =>
@@ -865,14 +868,13 @@ object CaptureSet:
       || isConst
       || varState.canRecord && { includeDep(cs); true }
 
-    override def disallowBadRoots(upto: Symbol)(handler: () => Context ?=> Unit)(using Context): this.type =
+    override def disallowBadRoots(upto: Symbol)(handler: () => Context ?=> Unit)(using Context): Unit =
       rootLimit = upto
-      rootAddedHandler = handler
       super.disallowBadRoots(upto)(handler)
 
-    override def ensureWellformed(handler: Capability => (Context) ?=> Unit)(using Context): this.type =
-      newElemAddedHandler = handler
-      super.ensureWellformed(handler)
+    override def checkAddedElems(handler: Capability => Context ?=> Unit)(using Context): Unit =
+      newElemAddedHandlers = handler :: newElemAddedHandlers
+      super.checkAddedElems(handler)
 
     private var computingApprox = false
 
@@ -1012,8 +1014,7 @@ object CaptureSet:
      *  Test case: Without that tweak, logger.scala would not compile.
      */
     override def disallowBadRoots(upto: Symbol)(handler: () => Context ?=> Unit)(using Context) =
-      if isRefining then this
-      else super.disallowBadRoots(upto)(handler)
+      if !isRefining then super.disallowBadRoots(upto)(handler)
 
   end ProperVar
 

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

@@ -553,6 +553,14 @@ 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 =
+        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.""",
+                tree.srcPos)
+
       def recur(cs: CaptureSet, env: Env, lastEnv: Env | Null): Unit =
         if env.kind != EnvKind.Boxed && !env.owner.isStaticOwner && !cs.isAlwaysEmpty then
           // Only captured references that are visible from the environment
@@ -570,6 +578,8 @@ class CheckCaptures extends Recheck, SymTransformer:
           if !isOfNestedMethod(env) then
             val nextEnv = nextEnvToCharge(env)
             if nextEnv != null && !nextEnv.owner.isStaticOwner then
+              if env.owner.isReadOnlyMethod && nextEnv.owner != env.owner then
+                checkReadOnlyMethod(included, env)
               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.
@@ -2093,9 +2103,7 @@ class CheckCaptures extends Recheck, SymTransformer:
               if !(pos.span.isSynthetic && ctx.reporter.errorsReported)
                 && !arg.typeSymbol.name.is(WildcardParamName)
               then
-                CheckCaptures.disallowBadRootsIn(arg, NoSymbol,
-                  "Array", "have element type", "",
-                  pos)
+                disallowBadRootsIn(arg, NoSymbol, "Array", "have element type", "", pos)
               traverseChildren(t)
             case defn.RefinedFunctionOf(rinfo: MethodType) =>
               traverse(rinfo)

docs/_docs/reference/experimental/capture-checking/mutability.md

@@ -46,7 +46,7 @@ class Ref(init: Int) extends Mutable:
   def get: Int = current
   update def set(x: Int): Unit = current = x
 ```
-`update` can only be used in classes or objects extending `Mutable`. An update method is allowed to access exclusive capabilities in the method's environment. By contrast, a normal method in a type extending `Mutable` may access exclusive capabilities only if they are defined locally or passed to it in parameters.
+`update` can only be used in classes or objects extending `Mutable`. An update method is allowed to access exclusive capabilities in the method's environment. By contrast, a normal method in a type extending `Mutable` may access exclusive capabilities only if they are defined in the method itself or passed to it in parameters.
 
 In class `Ref`, the `set` method should be declared as an update method since it accesses `this` as an exclusive write capability by writing to the variable `this.current` in its environment.
 

tests/neg-custom-args/captures/i24310.check

@@ -0,0 +1,7 @@
+-- Error: tests/neg-custom-args/captures/i24310.scala:10:16 ------------------------------------------------------------
+10 |    def run() = f() // error <- note the missing update
+   |                ^
+   |                Read-only method run accesses exclusive capability (Matrix.this.f : () => Int);
+   |                method run should be declared an update method to allow this.
+   |
+   |                where:    => refers to a fresh root capability in the type of value f

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

@@ -0,0 +1,27 @@
+import caps.*
+
+class Ref extends Mutable:
+  private var value: Int = 0
+  def get(): Int = value
+  update def set(v: Int): Unit = value = v
+
+class Matrix(val f: () => Int) extends Mutable:
+  self: Matrix^ =>
+    def run() = f() // error <- note the missing update
+    update def add(): Unit = ()
+
+
+@main def test =
+  val r: Ref^ = Ref()
+  val m: Matrix^ = Matrix(() => 42)
+  val m2: Matrix^ = Matrix(() => m.run())
+  val m3: Matrix^ = Matrix(() => r.get())
+
+  def par(f1: () => Int, f2: () => Int): Unit =
+    println(s"par results: ${f1()} and ${f2()}")
+
+  def g(m: Matrix^): Unit =
+    par(m.run, m.run) // <- should be rejected
+
+  g(m2) // ok
+  g(m3) // ok

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

@@ -22,6 +22,13 @@
    |           where:    ^ and cap refer to a fresh root capability classified as Mutable in the type of value self2
    |
    | longer explanation available when compiling with `-explain`
+-- Error: tests/neg-custom-args/captures/mutability.scala:11:13 --------------------------------------------------------
+11 |    self2.set(x) // error
+   |    ^^^^^^^^^^^^
+   |    Read-only method sneakyHide accesses exclusive capability (Ref.this : Ref[T]^);
+   |    method sneakyHide should be declared an update method to allow this.
+   |
+   |    where:    ^ refers to a fresh root capability classified as Mutable in the type of class Ref
 -- Error: tests/neg-custom-args/captures/mutability.scala:14:12 --------------------------------------------------------
 14 |    self3().set(x)  // error
    |    ^^^^^^^^^^^
@@ -42,6 +49,13 @@
    |                     ^ and cap refer to a fresh root capability classified as Mutable in the type of value self4
    |
    | longer explanation available when compiling with `-explain`
+-- Error: tests/neg-custom-args/captures/mutability.scala:16:15 --------------------------------------------------------
+16 |    self4().set(x) // error
+   |    ^^^^^^^^^^^^^^
+   |    Read-only method sneakyHide accesses exclusive capability (Ref.this : Ref[T]^);
+   |    method sneakyHide should be declared an update method to allow this.
+   |
+   |    where:    ^ refers to a fresh root capability classified as Mutable in the type of class Ref
 -- Error: tests/neg-custom-args/captures/mutability.scala:19:12 --------------------------------------------------------
 19 |    self5().set(x)  // error
    |    ^^^^^^^^^^^
@@ -61,6 +75,13 @@
    |   where:    ^ and cap refer to a fresh root capability classified as Mutable in the result type of method self6
    |
    | longer explanation available when compiling with `-explain`
+-- Error: tests/neg-custom-args/captures/mutability.scala:21:15 --------------------------------------------------------
+21 |    self6().set(x) // error
+   |    ^^^^^^^^^^^^^^
+   |    Read-only method sneakyHide accesses exclusive capability (Ref.this : Ref[T]^);
+   |    method sneakyHide should be declared an update method to allow this.
+   |
+   |    where:    ^ refers to a fresh root capability classified as Mutable in the type of class Ref
 -- Error: tests/neg-custom-args/captures/mutability.scala:25:25 --------------------------------------------------------
 25 |  def set(x: T) = this.x.set(x) // error
    |                  ^^^^^^^^^^

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

@@ -8,17 +8,17 @@ class Ref[T](init: T) extends caps.Mutable:
     val self = this
     self.set(x)  // error
     val self2: Ref[T]^ = this // error
-    self2.set(x)
+    self2.set(x) // error
 
     val self3 = () => this
     self3().set(x)  // error
     val self4: () => Ref[T]^ = () => this // error
-    self4().set(x)
+    self4().set(x) // error
 
     def self5() = this
     self5().set(x)  // error
     def self6(): Ref[T]^ = this // error
-    self6().set(x)
+    self6().set(x) // error
 
 class Ref2[T](init: T) extends caps.Mutable:
   val x = Ref[T](init)