Make Arrays mutable types under separation checking (#24649)

Also: enforce that mutable fields can only be declared in `Stateful`
classes, unless they are annotated with `untrackedCaptures`.

Author: odersky

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

@@ -394,11 +394,18 @@ extension (tp: Type)
     case _ =>
       false
 
-  def derivesFromCapability(using Context): Boolean = derivesFromCapTrait(defn.Caps_Capability)
-  def derivesFromStateful(using Context): Boolean = derivesFromCapTrait(defn.Caps_Stateful)
-  def derivesFromShared(using Context): Boolean = derivesFromCapTrait(defn.Caps_SharedCapability)
-  def derivesFromUnscoped(using Context): Boolean = derivesFromCapTrait(defn.Caps_Unscoped)
-  def derivesFromMutable(using Context): Boolean = derivesFromCapTrait(defn.Caps_Mutable)
+  def derivesFromCapability(using Context): Boolean =
+    derivesFromCapTrait(defn.Caps_Capability) || isArrayUnderStrictMut
+  def derivesFromStateful(using Context): Boolean =
+    derivesFromCapTrait(defn.Caps_Stateful) || isArrayUnderStrictMut
+  def derivesFromShared(using Context): Boolean =
+    derivesFromCapTrait(defn.Caps_SharedCapability)
+  def derivesFromUnscoped(using Context): Boolean =
+    derivesFromCapTrait(defn.Caps_Unscoped) || isArrayUnderStrictMut
+  def derivesFromMutable(using Context): Boolean =
+    derivesFromCapTrait(defn.Caps_Mutable) || isArrayUnderStrictMut
+
+  def isArrayUnderStrictMut(using Context): Boolean = tp.classSymbol.isArrayUnderStrictMut
 
   /** Drop @retains annotations everywhere */
   def dropAllRetains(using Context): Type = // TODO we should drop retains from inferred types before unpickling
@@ -488,7 +495,8 @@ extension (tp: Type)
       tp
 
   def inheritedClassifier(using Context): ClassSymbol =
-    tp.classSymbols.map(_.classifier).foldLeft(defn.AnyClass)(leastClassifier)
+    if tp.isArrayUnderStrictMut then defn.Caps_Unscoped
+    else tp.classSymbols.map(_.classifier).foldLeft(defn.AnyClass)(leastClassifier)
 
 extension (tp: MethodType)
   /** A method marks an existential scope unless it is the prefix of a curried method */
@@ -553,10 +561,13 @@ extension (sym: Symbol)
    *   - or it is a value class
    *   - or it is an exception
    *   - or it is one of Nothing, Null, or String
+   *  Arrays are not pure under strict mutability even though their self type is declared pure
+   *  in Arrays.scala.
    */
   def isPureClass(using Context): Boolean = sym match
     case cls: ClassSymbol =>
-      cls.pureBaseClass.isDefined || defn.pureSimpleClasses.contains(cls)
+      (cls.pureBaseClass.isDefined || defn.pureSimpleClasses.contains(cls))
+      && !cls.isArrayUnderStrictMut
     case _ =>
       false
 
@@ -588,8 +599,8 @@ extension (sym: Symbol)
     && !defn.isPolymorphicAfterErasure(sym)
     && !defn.isTypeTestOrCast(sym)
 
-  /** It's a parameter accessor that is not annotated @constructorOnly or @uncheckedCaptures
-   *  and that is not a consume accessor.
+  /** It's a parameter accessor for a parameter that that is not annotated
+   *  @constructorOnly or @uncheckedCaptures and that is not a consume parameter.
    */
   def isRefiningParamAccessor(using Context): Boolean =
     sym.is(ParamAccessor)
@@ -600,6 +611,17 @@ extension (sym: Symbol)
       && !param.hasAnnotation(defn.ConsumeAnnot)
     }
 
+  /** It's a parameter accessor that is tracked for capture checking. Excluded are
+   *  accessors for parameters annotated with constructorOnly or @uncheckedCaptures.
+   */
+  def isTrackedParamAccessor(using Context): Boolean =
+    sym.is(ParamAccessor)
+    && {
+      val param = sym.owner.primaryConstructor.paramNamed(sym.name)
+      !param.hasAnnotation(defn.ConstructorOnlyAnnot)
+      && !param.hasAnnotation(defn.UntrackedCapturesAnnot)
+    }
+
   def hasTrackedParts(using Context): Boolean =
     !CaptureSet.ofTypeDeeply(sym.info).isAlwaysEmpty
 
@@ -642,6 +664,9 @@ extension (sym: Symbol)
     else if sym.name.is(TryOwnerName) then i"an enclosing try expression"
     else sym.show
 
+  def isArrayUnderStrictMut(using Context): Boolean =
+    sym == defn.ArrayClass && ccConfig.strictMutability
+
 extension (tp: AnnotatedType)
   /** Is this a boxed capturing type? */
   def isBoxed(using Context): Boolean = tp.annot match

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

@@ -666,13 +666,33 @@ object CaptureSet:
       then i" under-approximating the result of mapping $ref to $mapped"
       else ""
 
-  private def capImpliedByCapability(parent: Type)(using Context): Capability =
-    if parent.derivesFromStateful then GlobalCap.readOnly else GlobalCap
+  private def capImpliedByCapability(parent: Type, sym: Symbol, variance: Int)(using Context): Capability =
+    // Since standard library classes are not compiled with separation checking,
+    // they treat Array as a Pure class. That means, no effort is made to distinguish
+    // between exclusive and read-only arrays. To compensate in code compiled under
+    // strict mutability, we treat contravariant arrays in signatures of stdlib
+    // members as read-only (so all arrays may be passed to them), and co- and
+    // invariant arrays as exclusive.
+    // TODO This scheme should also apply whenever code under strict mutability interfaces
+    // with code compiled without. To do that we will need to store in the Tasty format
+    // a flag whether code was compiled with separation checking on. This will have
+    // to wait until 3.10.
+    def isArrayFromScalaPackage =
+      parent.classSymbol == defn.ArrayClass
+      && ccConfig.strictMutability
+      && variance >= 0
+      && sym.isContainedIn(defn.ScalaPackageClass)
+    if parent.derivesFromStateful && !isArrayFromScalaPackage
+    then GlobalCap.readOnly
+    else GlobalCap
 
   /* The same as {cap} but generated implicitly for references of Capability subtypes.
+   *  @param parent   the type to which the capture set will be attached
+   *  @param sym      the symbol carrying that type
+   *  @param variance the variance in which `parent` appears in the type of `sym`
    */
-  class CSImpliedByCapability(parent: Type)(using @constructorOnly ctx: Context)
-  extends Const(SimpleIdentitySet(capImpliedByCapability(parent)))
+  class CSImpliedByCapability(parent: Type, sym: Symbol, variance: Int)(using @constructorOnly ctx: Context)
+  extends Const(SimpleIdentitySet(capImpliedByCapability(parent, sym, variance)))
 
   /** A special capture set that gets added to the types of symbols that were not
    *  themselves capture checked, in order to admit arbitrary corresponding capture

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
@@ -1410,9 +1410,7 @@ class CheckCaptures extends Recheck, SymTransformer:
 
         // (3) Capture set of self type includes capture sets of parameters
         for param <- cls.paramGetters do
-          if !param.hasAnnotation(defn.ConstructorOnlyAnnot)
-              && !param.hasAnnotation(defn.UntrackedCapturesAnnot)
-          then
+          if param.isTrackedParamAccessor then
             withCapAsRoot: // OK? We need this here since self types use `cap` instead of `fresh`
               checkSubset(param.termRef.captureSet, thisSet, param.srcPos)
 
@@ -1581,7 +1579,7 @@ class CheckCaptures extends Recheck, SymTransformer:
      *  where local capture roots are instantiated to root variables.
      */
     override def checkConformsExpr(actual: Type, expected: Type, tree: Tree, notes: List[Note])(using Context): Type =
-      try testAdapted(actual, expected, tree, notes: List[Note])(err.typeMismatch)
+      try testAdapted(actual, expected, tree, notes)(err.typeMismatch)
       catch case ex: AssertionError =>
         println(i"error while checking $tree: $actual against $expected")
         throw ex
@@ -2148,26 +2146,6 @@ class CheckCaptures extends Recheck, SymTransformer:
         checker.traverse(tree.nuType)
     end checkTypeParam
 
-    /** Under the unsealed policy: Arrays are like vars, check that their element types
-     *  do not contains `cap` (in fact it would work also to check on array creation
-     *  like we do under sealed).
-     */
-    def checkArraysAreSealedIn(tp: Type, pos: SrcPos)(using Context): Unit =
-      val check = new TypeTraverser:
-        def traverse(t: Type): Unit =
-          t match
-            case AppliedType(tycon, arg :: Nil) if tycon.typeSymbol == defn.ArrayClass =>
-              if !(pos.span.isSynthetic && ctx.reporter.errorsReported)
-                && !arg.typeSymbol.name.is(WildcardParamName)
-              then
-                disallowBadRootsIn(arg, NoSymbol, "Array", "have element type", "", pos)
-              traverseChildren(t)
-            case defn.RefinedFunctionOf(rinfo: MethodType) =>
-              traverse(rinfo)
-            case _ =>
-              traverseChildren(t)
-      check.traverse(tp)
-
     /** Check that no uses refer to reach capabilities of parameters of enclosing
      *  methods or classes.
      */

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

@@ -10,6 +10,7 @@ import config.Printers.capt
 import config.Feature
 import ast.tpd.Tree
 import typer.ProtoTypes.LhsProto
+import StdNames.nme
 
 /** Handling mutability and read-only access
  */
@@ -59,6 +60,7 @@ object Mutability:
               && !sym.field.hasAnnotation(defn.UntrackedCapturesAnnot)
             else true
            )
+      || ccConfig.strictMutability && sym.name == nme.update && sym == defn.Array_update
 
     /** A read-only member is a lazy val or a method that is not an update method. */
     def isReadOnlyMember(using Context): Boolean =

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

@@ -165,9 +165,14 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI:
     if !pastRecheck && Feature.ccEnabledSomewhere then
       val sym = symd.symbol
       def mappedInfo =
-        if toBeUpdated.contains(sym)
-        then symd.info // don't transform symbols that will anyway be updated
-        else transformExplicitType(symd.info, sym)
+        if toBeUpdated.contains(sym) then
+          symd.info // don't transform symbols that will anyway be updated
+        else if sym.isArrayUnderStrictMut then
+          val cinfo: ClassInfo = sym.info.asInstanceOf
+          cinfo.derivedClassInfo(
+            declaredParents = cinfo.declaredParents :+ defn.Caps_Mutable.typeRef)
+        else
+          transformExplicitType(symd.info, sym)
       if Synthetics.needsTransform(symd) then
         Synthetics.transform(symd, mappedInfo)
       else if isPreCC(sym) then
@@ -425,7 +430,7 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI:
         then
           normalizeCaptures(mapOver(t)) match
             case t1 @ CapturingType(_, _) => t1
-            case t1 => CapturingType(t1, CaptureSet.CSImpliedByCapability(t1), boxed = false)
+            case t1 => CapturingType(t1, CaptureSet.CSImpliedByCapability(t1, sym, variance), boxed = false)
         else normalizeCaptures(mapFollowingAliases(t))
 
       def innerApply(t: Type) =

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`)
@@ -61,9 +56,15 @@ object ccConfig:
   def newScheme(using ctx: Context): Boolean =
     Feature.sourceVersion.stable.isAtLeast(SourceVersion.`3.7`)
 
+  /** Allow @use annotations */
   def allowUse(using Context): Boolean =
     Feature.sourceVersion.stable.isAtMost(SourceVersion.`3.7`)
 
-
+  /** 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)
 
 end ccConfig

compiler/src/dotty/tools/dotc/core/SymDenotations.scala

@@ -1886,7 +1886,7 @@ object SymDenotations {
       myBaseTypeCache.nn
     }
 
-    private def invalidateBaseDataCache() = {
+    def invalidateBaseDataCache() = {
       baseDataCache.invalidate()
       baseDataCache = BaseData.None
     }

compiler/src/dotty/tools/dotc/typer/ErrorReporting.scala

@@ -14,6 +14,7 @@ import config.Feature
 import reporting.*
 import Message.Note
 import collection.mutable
+import cc.isCaptureChecking
 
 object ErrorReporting {
 
@@ -190,7 +191,13 @@ object ErrorReporting {
         case _ =>
           Nil
 
-      errorTree(tree, TypeMismatch(treeTp, expectedTp, Some(tree), notes ++ missingElse))
+      def badTreeNote =
+        val span = tree.span
+        if tree.span.isZeroExtent && isCaptureChecking then
+          Note(i"\n\nThe error occurred for a synthesized tree:  $tree") :: Nil
+        else Nil
+
+      errorTree(tree, TypeMismatch(treeTp, expectedTp, Some(tree), notes ++ missingElse ++ badTreeNote))
     }
 
     /** A subtype log explaining why `found` does not conform to `expected` */

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

@@ -239,6 +239,20 @@ class Arr[T](n: Int) extends Mutable:
 An example of a `Stateful` and `Unscoped` capability that is _not_ `Separate` would be a
 facade class that reveals some part of an underlying `Mutable` capability.
 
+## Arrays
+
+The class `scala.Array` is considered a `Mutable` class if [separation checking](./separation-checking.md) is enabled. In that context, class Array can be considered to be declared roughly as follows:
+```scala
+class Array[T] extends Mutable:
+  def length: Int
+  def apply(i: Int): T
+  update def update(i: Int, x: T): Unit
+```
+In fact, for technical reasons `Array` cannot extend `Mutable` or any other new traits beyond what is supported by the JVM. But for the purposes of capture and separation checking, it is still a considered a `Mutable` class.
+
+By contrast, none of the mutable collections in the Scala standard library extend currently `Stateful` or `Mutable`. So to experiment with mutable collections, an
+alternative class library has to be used.
+
 ## Read-only Capabilities
 
 If `x` is an exclusive capability of a type extending `Stateful`, `x.rd` is its associated _read-only_ capability.
@@ -388,7 +402,9 @@ ro.set(22)        // disallowed, since `ro` is read-only access
 
 ## Untracked Vars
 
-Sometimes, disallowing assignments to mutable fields from normal methods is too restrictive. For instance:
+Under [separation checking](./separation-checking.md), mutable fields are allowed to be declared only in `Stateful` classes. Updates to these fields can then only happen in update methods of these classes.
+
+But sometimes, disallowing assignments to mutable fields from normal methods is too restrictive. For instance:
 ```scala
 import caps.unsafe.untrackedCaptures
 
@@ -401,17 +417,12 @@ class Cache[T](eval: () -> T):
       known = true
     x
 ```
-Note that, even though `Cache` has mutable variables, it is not declared as a `Stateful` class. In this case, the mutable field `x` is used to store the result of a pure function `eval` and field `known` reflects whether `eval` was called. This is equivalent to just calling `eval()` directly but can be more efficient since the cached value is evaluated at most once. So from a semantic standpoint, it should not be necessary to make `force` an update method, even though it does assign to `x`.
+Note that `Cache` is not declared as a `Stateful` class, even though it has mutable fields. In this case, the mutable field `x` is used to store the result of a pure function `eval` and field `known` reflects whether `eval` was called. This is equivalent to just calling `eval()` directly but can be more efficient since the cached value is evaluated at most once. So from a semantic standpoint, it should not be necessary to make `Cache` a `Stateful` class with `force` as an update method, even though `force` does assign to `x`.
 
-We can avoid the need for update methods by annotating mutable fields with `@untrackedCaptures`. Assignments to untracked mutable field are then not checked for read-only restrictions. The `@untrackedCaptures` annotation can be imported from the `scala.caps.unsafe` object. It is up to the developer
+We can avoid the need for stateful classes and update methods by annotating mutable fields with `@untrackedCaptures`. Assignments to untracked mutable fields are then not checked for read-only restrictions. The `@untrackedCaptures` annotation can be imported from the `scala.caps.unsafe` object. It is up to the developer
 to use `@untrackedCaptures` responsibly so that it does not hide visible side effects on mutable state.
 
-Note that at the moment an assignment to a variable is restricted _only_ if the variable is a field of a `Stateful` class. Fields of other classes and local variables are currently not checked. So the `Cache` class above would in fact
-currently compile without the addition of `@untrackedCaptures`.
-
-But is planned to tighten the rules in the future so that mutable fields that are not annotated with `@untrackedCaptures` can be declared only in classes extending `Stateful`. This means that all assignments to mutable fields would be checked with the read-only restriction, and `@untrackedCapture`s would become essential as an escape hatch.
-
-By contrast, it is not planned to check assignments to local mutable variables, which are not fields of some class. So `@untrackedCaptures` is disallowed for such local variables.
+Note that the are no restrictions on assignments to local mutable variables, which are not fields of some class. So `@untrackedCaptures` is disallowed for such local variables.
 
 The `untrackedCaptures` annotation can also be used in some other contexts unrelated to mutable variables. These are described in its [doc comment](https://www.scala-lang.org/api/current/scala/caps/unsafe$$untrackedCaptures.html).
 

library/src/scala/caps/package.scala

@@ -4,6 +4,7 @@ package caps
 import language.experimental.captureChecking
 
 import annotation.{experimental, compileTimeOnly, retainsCap}
+import annotation.meta.*
 
 /**
  * Base trait for classes that represent capabilities in the
@@ -157,6 +158,7 @@ object internal:
   /** An annotation to reflect that a parameter or method carries the `consume`
    *  soft modifier.
    */
+  @getter @param
   final class consume extends annotation.StaticAnnotation
 
   /** An internal annotation placed on a refinement created by capture checking.
@@ -193,20 +195,22 @@ end internal
 
 /** A wrapper that strips all covariant capture sets from Mutable types in the
  *  result of pure operation `op`, turning them into immutable types.
+ *  Array[?] is also included since it counts as a Mutable type for
+ *  separation checking.
  */
 @experimental
-def freeze(@internal.consume x: Mutable): x.type = x
+def freeze(@internal.consume x: Mutable | Array[?]): x.type = x
 
 @experimental
 object unsafe:
-  /** Two usages:
+  /** Three usages:
    *
    *   1. Marks the constructor parameter as untracked.
    *      The capture set of this parameter will not be included in
    *      the capture set of the constructed object.
    *
-   *   2. Marks a class field that has a cap in its capture set, so that
-   *      the cap is not contributed to the class instance.
+   *   2. Marks a class field that has a root capability in its capture set, so
+   *      that the root capability is not contributed to the class instance.
    *      Example:
    *
    *          class A { val b B^ = ... }; new A()
@@ -217,9 +221,13 @@ object unsafe:
    *
    *      has type A. The `b` field does not contribute its cap.
    *
+   *   3. Allows a field to be declarewd in a class that does not extend Stateful,
+   *      and suppresses checks for updates to the field.
+   *
    * @note This should go into annotations. For now it is here, so that we
    *  can experiment with it quickly between minor releases
    */
+  @getter @param
   final class untrackedCaptures extends annotation.StaticAnnotation
 
   extension [T](x: T)