Improvements to read-only handling

 - Allow to charge read-only set on unboxing (previously it was always the exclusive set that
   was charged).
 - Treat also methods outside Mutable types as read-only members. Previously we charged
   read-only when calling a read-only method of a mutable type, but not when calling an inherited
   method such as `eq`.
 - Use the same criterion for read-only everywhere.
 - Distinguish between read- and write-accesses to mutable fields.

Author: odersky

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

@@ -15,7 +15,8 @@ import CaptureSet.VarState
 import Capabilities.*
 import StdNames.nme
 import config.Feature
-import dotty.tools.dotc.core.NameKinds.TryOwnerName
+import NameKinds.TryOwnerName
+import typer.ProtoTypes.WildcardSelectionProto
 
 /** Attachment key for capturing type trees */
 private val Captures: Key[CaptureSet] = Key()
@@ -639,6 +640,10 @@ extension (tp: AnnotatedType)
     case ann: CaptureAnnotation => ann.boxed
     case _ => false
 
+/** A prototype that indicates selection */
+class PathSelectionProto(val select: Select, val pt: Type) extends typer.ProtoTypes.WildcardSelectionProto:
+  def selector(using Context): Symbol = select.symbol
+
 /** Drop retains annotations in the inferred type if CC is not enabled
  *  or transform them into RetainingTypes if CC is enabled.
  */

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

@@ -103,9 +103,6 @@ object CheckCaptures:
     override def toString = "SubstParamsMap"
   end SubstParamsMap
 
-  /** A prototype that indicates selection with an immutable value */
-  class PathSelectionProto(val select: Select, val pt: Type)(using Context) extends WildcardSelectionProto
-
   /** Check that a @retains annotation only mentions references that can be tracked.
    *  This check is performed at Typer.
    */
@@ -598,7 +595,10 @@ class CheckCaptures extends Recheck, SymTransformer:
           if !isOfNestedMethod(env) then
             val nextEnv = nextEnvToCharge(env)
             if nextEnv != null && !nextEnv.owner.isStaticOwner then
-              if env.owner.isReadOnlyMethodOrLazyVal && nextEnv.owner != env.owner then
+              if nextEnv.owner != env.owner
+                  && env.owner.isReadOnlyMember
+                  && env.owner.owner.derivesFrom(defn.Caps_Mutable)
+              then
                 checkReadOnlyMethod(included, env.owner)
               recur(included, nextEnv, env)
           	// Under deferredReaches, don't propagate out of methods inside terms.
@@ -705,29 +705,23 @@ class CheckCaptures extends Recheck, SymTransformer:
      *  where `b` is a read-only method, we charge `x.a.b.rd` for tree `x.a.b`
      *  instead of just charging `x`.
      */
-    private def markPathFree(ref: TermRef | ThisType, pt: Type, tree: Tree)(using Context): Unit =
-      pt match
-        case pt: PathSelectionProto if ref.isTracked =>
-          // if `ref` is not tracked then the selection could not give anything new
-          // class SerializationProxy in stdlib-cc/../LazyListIterable.scala has an example where this matters.
-          if pt.select.symbol.isReadOnlyMethodOrLazyVal then
-            markFree(ref.readOnly, tree)
-          else
-            val sel = ref.select(pt.select.symbol).asInstanceOf[TermRef]
-            markPathFree(sel, pt.pt, pt.select)
-        case _ =>
-          markFree(ref.adjustReadOnly(pt), tree)
+    private def markPathFree(ref: TermRef | ThisType, pt: Type, tree: Tree)(using Context): Unit = pt match
+      case pt: PathSelectionProto
+      if ref.isTracked && !pt.selector.isOneOf(MethodOrLazyOrMutable) =>
+        // if `ref` is not tracked then the selection could not give anything new
+        // class SerializationProxy in stdlib-cc/../LazyListIterable.scala has an example where this matters.
+        val sel = ref.select(pt.selector).asInstanceOf[TermRef]
+        markPathFree(sel, pt.pt, pt.select)
+      case _ =>
+        markFree(ref.adjustReadOnly(pt), tree)
 
     /** The expected type for the qualifier of a selection. If the selection
      *  could be part of a capability path or is a a read-only method, we return
      *  a PathSelectionProto.
      */
     override def selectionProto(tree: Select, pt: Type)(using Context): Type =
-      val sym = tree.symbol
-      if !sym.isOneOf(MethodOrLazyOrMutable) && !sym.isStatic
-          || sym.isReadOnlyMethodOrLazyVal
-      then PathSelectionProto(tree, pt)
-      else super.selectionProto(tree, pt)
+      if tree.symbol.isStatic then super.selectionProto(tree, pt)
+      else PathSelectionProto(tree, pt)
 
     /** A specialized implementation of the selection rule.
      *
@@ -1131,21 +1125,30 @@ class CheckCaptures extends Recheck, SymTransformer:
       try
         if sym.is(Module) then sym.info // Modules are checked by checking the module class
         else
-          if sym.is(Mutable) && !sym.hasAnnotation(defn.UncheckedCapturesAnnot) then
-            val addendum = setup.capturedBy.get(sym) match
-              case Some(encl) =>
-                val enclStr =
-                  if encl.isAnonymousFunction then
-                    val location = setup.anonFunCallee.get(encl) match
-                      case Some(meth) if meth.exists => i" argument in a call to $meth"
-                      case _ => ""
-                    s"an anonymous function$location"
-                  else encl.show
-                i"\n\nNote that $sym does not count as local since it is captured by $enclStr"
-              case _ =>
-                ""
-            disallowBadRootsIn(
-              tree.tpt.nuType, NoSymbol, i"Mutable $sym", "have type", addendum, sym.srcPos)
+          if sym.is(Mutable) then
+            if !sym.hasAnnotation(defn.UncheckedCapturesAnnot) then
+              val addendum = setup.capturedBy.get(sym) match
+                case Some(encl) =>
+                  val enclStr =
+                    if encl.isAnonymousFunction then
+                      val location = setup.anonFunCallee.get(encl) match
+                        case Some(meth) if meth.exists => i" argument in a call to $meth"
+                        case _ => ""
+                      s"an anonymous function$location"
+                    else encl.show
+                  i"\n\nNote that $sym does not count as local since it is captured by $enclStr"
+                case _ =>
+                  ""
+              disallowBadRootsIn(
+                tree.tpt.nuType, NoSymbol, i"Mutable $sym", "have type", addendum, sym.srcPos)
+            if sepChecksEnabled && false
+                && sym.owner.isClass
+                && !sym.owner.derivesFrom(defn.Caps_Mutable)
+                && !sym.hasAnnotation(defn.UntrackedCapturesAnnot) then
+              report.error(
+                em"""Mutable $sym is defined in a class that does not extend `Mutable`.
+                    |The variable needs to be annotated with `untrackedCaptures` to allow this.""",
+                tree.namePos)
 
           // Lazy vals need their own environment to track captures from their RHS,
           // similar to how methods work
@@ -1793,7 +1796,10 @@ class CheckCaptures extends Recheck, SymTransformer:
 
         if needsAdaptation && !insertBox then // we are unboxing
           val criticalSet =          // the set with which we unbox
-            if covariant then captures   // covariant: we box with captures of actual type plus captures leaked by inner adapation
+            if covariant then
+              if expected.expectsReadOnly && actual.derivesFromMutable
+              then captures.readOnly
+              else captures
             else expected.captureSet     // contravarant: we unbox with captures of epected type
             //debugShowEnvs()
           markFree(criticalSet, tree)

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

@@ -8,6 +8,7 @@ import Capabilities.*
 import util.SrcPos
 import config.Printers.capt
 import ast.tpd.Tree
+import typer.ProtoTypes.LhsProto
 
 /** Handling mutability and read-only access
  */
@@ -58,12 +59,9 @@ object Mutability:
             else true
            )
 
-    /** A read-only method is a real method (not an accessor) in a type extending
-     *  Mutable that is not an update method. Included are also lazy vals in such types.
-     */
-    def isReadOnlyMethodOrLazyVal(using Context): Boolean =
-      sym.isOneOf(MethodOrLazy, butNot = Mutable | Accessor)
-      && sym.owner.derivesFrom(defn.Caps_Mutable)
+    /** A read-only member is a lazy val or a method that is not an update method. */
+    def isReadOnlyMember(using Context): Boolean =
+      sym.isOneOf(MethodOrLazy) && !sym.isUpdateMethod
 
     private def inExclusivePartOf(cls: Symbol)(using Context): Exclusivity =
       import Exclusivity.*
@@ -104,19 +102,25 @@ object Mutability:
       case _ =>
         tp.exclusivity
 
+    def expectsReadOnly(using Context): Boolean = tp match
+      case tp: PathSelectionProto =>
+        tp.selector.isReadOnlyMember || tp.selector.isMutableVar && tp.pt != LhsProto
+      case _ => tp.isValueType && !tp.isMutableType
+
   extension (cs: CaptureSet)
     private def exclusivity(tp: Type)(using Context): Exclusivity =
       if cs.isExclusive then Exclusivity.OK else Exclusivity.ReadOnly(tp)
 
   extension (ref: TermRef | ThisType)
     /** Map `ref` to `ref.readOnly` if its type extends Mutble, and one of the
-     *  following is true: it appears in a non-exclusive context, or the expected
-     *  type is a value type that is not a mutable type.
+     *  following is true:
+     *    - it appears in a non-exclusive context,
+     *    - the expected type is a value type that is not a mutable type,
+     *    - the expected type is a read-only selection
      */
     def adjustReadOnly(pt: Type)(using Context): Capability =
       if ref.derivesFromMutable
-          && (pt.isValueType && !pt.isMutableType
-              || ref.exclusivityInContext != Exclusivity.OK)
+          && (pt.expectsReadOnly || ref.exclusivityInContext != Exclusivity.OK)
       then ref.readOnly
       else ref
 
@@ -148,7 +152,6 @@ object Mutability:
             && expected.isValueType
             && (!expected.derivesFromMutable || expected.captureSet.isAlwaysReadOnly)
             && !expected.isSingleton
-            && actual.isBoxedCapturing == expected.isBoxedCapturing
         then refs.readOnly
         else refs
       actual.derivedCapturingType(parent1, refs1)

compiler/src/dotty/tools/dotc/printing/RefinedPrinter.scala

@@ -333,6 +333,8 @@ class RefinedPrinter(_ctx: Context) extends PlainPrinter(_ctx) {
       case tp: LazyRef if !printDebug =>
         try toText(tp.ref)
         catch case ex: Throwable => "..."
+      case sel: cc.PathSelectionProto =>
+        "?.{ " ~ toText(sel.select.symbol) ~ "}"
       case AnySelectionProto =>
         "a type that can be selected or applied"
       case tp: SelectionProto =>

tests/neg-custom-args/captures/var-access.check

@@ -0,0 +1,18 @@
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/var-access.scala:9:21 ------------------------------------
+9 |  val _: () -> Int = f   // error
+  |                     ^
+  |                     Found:    (f : () ->{a.rd} Int)
+  |                     Required: () -> Int
+  |
+  |                     Note that capability a.rd is not included in capture set {}.
+  |
+  | longer explanation available when compiling with `-explain`
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/var-access.scala:12:22 -----------------------------------
+12 |  val _: () -> Unit = g   // error
+   |                      ^
+   |                      Found:    (g : () ->{a} Unit)
+   |                      Required: () -> Unit
+   |
+   |                      Note that capability a is not included in capture set {}.
+   |
+   | longer explanation available when compiling with `-explain`

tests/neg-custom-args/captures/var-access.scala

@@ -0,0 +1,18 @@
+import caps.*
+class A extends Mutable:
+  var x: Int = 0
+
+def test =
+  val a = A()
+  val f = () => a.x
+  val _: () ->{a.rd} Int = f
+  val _: () -> Int = f   // error
+  val g = () => a.x += 1
+  val _: () ->{a} Unit = g
+  val _: () -> Unit = g   // error
+
+
+
+
+
+

tests/pos-custom-args/captures/mark-free-ro.scala

@@ -0,0 +1,13 @@
+import caps.{cap, Mutable}
+import caps.unsafe.untrackedCaptures
+
+class Test extends Mutable:
+  var ctxStack: Array[FreshCtx^] = new Array(10)
+
+  class FreshCtx(level: Int) extends Mutable:
+    this: FreshCtx^ =>
+    def detached: Boolean =
+      val c: FreshCtx^{cap.rd} = ctxStack(level)
+      (c eq this)
+    def detached2 =
+      ctxStack(level) eq this