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

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

Fixes #24310

Author: odersky

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"):
@@ -486,6 +486,13 @@ sealed abstract class CaptureSet extends Showable:
     if elems.exists(isBadRoot(upto, _)) then handler()
     this
 
+  /** 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.
    */
@@ -734,6 +741,10 @@ object CaptureSet:
     /** A handler to be invoked if the root reference `cap` is added to this set */
     var rootAddedHandler: () => Context ?=> Unit = () => ()
 
+    /** A handler to be invoked when a new element is added to this set */
+    var checkAddedElemHandler: Capability => Context ?=> Unit =
+      elem => ()
+
     /** The limit deciding which capture roots are bad (i.e. cannot be contained in this set).
      *  @see isBadRoot for details.
      */
@@ -816,6 +827,7 @@ object CaptureSet:
         catch case ex: AssertionError =>
           println(i"error for incl $elem in $this, ${summon[VarState].toString}")
           throw ex
+        checkAddedElemHandler(elem)
         if isBadRoot(elem) then
           rootAddedHandler()
         val normElem = if isMaybeSet then elem else elem.stripMaybe
@@ -870,6 +882,14 @@ object CaptureSet:
       rootAddedHandler = handler
       super.disallowBadRoots(upto)(handler)
 
+    override def checkAddedElems(handler: Capability => Context ?=> Unit)(using Context): Unit =
+      val prevHandler = checkAddedElemHandler
+      checkAddedElemHandler =
+        elem =>
+          prevHandler(elem)
+          handler(elem)
+      super.checkAddedElems(handler)
+
     override def ensureWellformed(handler: Capability => (Context) ?=> Unit)(using Context): this.type =
       newElemAddedHandler = handler
       super.ensureWellformed(handler)

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.

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)