Make Arrays mutable types under separation checking

odersky · odersky · commit 7a7a18f26c62 · 2025-12-03T15:54:49.000+01:00
diff --git a/compiler/src/dotty/tools/dotc/cc/CaptureOps.scala b/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
diff --git a/compiler/src/dotty/tools/dotc/cc/CaptureSet.scala b/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
diff --git a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
@@ -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)
 
@@ -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.
      */
diff --git a/compiler/src/dotty/tools/dotc/cc/Mutability.scala b/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 =
diff --git a/compiler/src/dotty/tools/dotc/cc/Setup.scala b/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) =
diff --git a/compiler/src/dotty/tools/dotc/cc/ccConfig.scala b/compiler/src/dotty/tools/dotc/cc/ccConfig.scala
@@ -61,9 +61,12 @@ 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. Enabled under separation checking */
+  def strictMutability(using Context): Boolean =
+    Feature.enabled(Feature.separationChecking)
 
 end ccConfig
diff --git a/compiler/src/dotty/tools/dotc/core/SymDenotations.scala b/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
     }
diff --git a/library/src/scala/caps/package.scala b/library/src/scala/caps/package.scala
@@ -195,7 +195,7 @@ end internal
  *  result of pure operation `op`, turning them into immutable types.
  */
 @experimental
-def freeze(@internal.consume x: Mutable): x.type = x
+def freeze(@internal.consume x: Mutable | Array[?]): x.type = x
 
 @experimental
 object unsafe:
diff --git a/tests/neg-custom-args/captures/existential-mapping.check b/tests/neg-custom-args/captures/existential-mapping.check
@@ -1,10 +1,10 @@
 -- Error: tests/neg-custom-args/captures/existential-mapping.scala:46:10 -----------------------------------------------
 46 |  val z2: (x: A^) => Array[C^] = ??? // error
    |          ^^^^^^^^^^^^^^^^^^^^
-   |          Array[C^] captures the root capability `cap` in invariant position.
+   |          Array[C^]^{cap.rd} captures the root capability `cap` in invariant position.
    |          This capability cannot be converted to an existential in the result type of a function.
    |
-   |          where:    ^ refers to the universal root capability
+   |          where:    ^ and cap refer to the universal root capability
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/existential-mapping.scala:9:25 ---------------------------
 9 |  val _:  (x: C^) -> C = x1 // error
   |                         ^^
diff --git a/tests/neg-custom-args/captures/freeze-double-flip.check b/tests/neg-custom-args/captures/freeze-double-flip.check
@@ -2,6 +2,6 @@
 15 |    (x: Ref^) => (op: Ref^ => IRef) => op(x) // error
    |    ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
    |    Found:    Ref^ -> (Ref^ => IRef) -> IRef
-   |    Required: scala.caps.Mutable
+   |    Required: scala.caps.Mutable | Array[?]
    |
    | longer explanation available when compiling with `-explain`
diff --git a/tests/neg-custom-args/captures/freeze.check b/tests/neg-custom-args/captures/freeze.check
@@ -2,6 +2,6 @@
 11 |  val b = freeze((a, a)) // error
    |                 ^^^^^^
    |                 Found:    (Arr[String], Arr[String])
-   |                 Required: scala.caps.Mutable
+   |                 Required: scala.caps.Mutable | Array[?]
    |
    | longer explanation available when compiling with `-explain`
diff --git a/tests/neg-custom-args/captures/freeze.scala b/tests/neg-custom-args/captures/freeze.scala
@@ -1,7 +1,7 @@
 import caps.*
 
 class Arr[T: reflect.ClassTag](len: Int) extends Mutable:
-  private val arr: Array[T] = new Array[T](len)
+  private val arr: Array[T]^ = new Array[T](len)
   def get(i: Int): T = arr(i)
   update def update(i: Int, x: T): Unit = arr(i) = x
 
diff --git a/tests/neg-custom-args/captures/mut-widen-empty.check b/tests/neg-custom-args/captures/mut-widen-empty.check
@@ -10,3 +10,15 @@
    |              where:    ^ and cap refer to a fresh root capability classified as Unscoped in the type of value c
    |
    | longer explanation available when compiling with `-explain`
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/mut-widen-empty.scala:18:26 ------------------------------
+18 |  val c: Array[String]^ = b  // error
+   |                          ^
+   |              Found:    (b : Array[String]^{})
+   |              Required: Array[String]^
+   |
+   |              Note that {cap} is an exclusive capture set of the stateful type Array[String]^,
+   |              it cannot subsume a read-only capture set of the stateful type Array[String]^{}.
+   |
+   |              where:    ^ and cap refer to a fresh root capability classified as Unscoped in the type of value c
+   |
+   | longer explanation available when compiling with `-explain`
diff --git a/tests/neg-custom-args/captures/mut-widen-empty.scala b/tests/neg-custom-args/captures/mut-widen-empty.scala
@@ -1,7 +1,7 @@
 import caps.*
 
 class Arr[T: reflect.ClassTag](len: Int) extends Mutable:
-  private val arr: Array[T] = new Array[T](len)
+  private val arr: Array[T]^ = new Array[T](len)
   def get(i: Int): T = arr(i)
   update def update(i: Int, x: T): Unit = arr(i) = x
 
@@ -12,3 +12,9 @@ def test2 =
   val c: Arr[String]^ = b  // error
   c(2) = "a"   // boom!
 
+def test3 =
+  val a = new Array[String](2)
+  val b: Array[String]^{} = ???
+  val c: Array[String]^ = b  // error
+  c(2) = "a"   // boom!
+
diff --git a/tests/new/test.scala b/tests/new/test.scala
@@ -1,27 +1,18 @@
-import caps.*
-
-class Ref[T](init: T) extends caps.Stateful, Unscoped:
-  var x = init
-  def get: T = x
-  update def put(y: T): Unit = x = y
-
-class File:
-  def read(): String = ???
-
-def withFile[T](op: (f: File^) => T): T =
-  op(new File)
-
-def withFileAndRef[T](op: (f: File^, r: Ref[String]^) => T): T =
-  op(File(), Ref(""))
-
-def Test =
-/*
-  withFileAndRef: (f, r: Ref[String]^) =>
-    r.put(f.read())
-*/
-
-  withFileAndRef: (f, r) =>
-    r.put(f.read())
-
-
-
+import caps.unsafe.untrackedCaptures
+
+class ArrayBuffer[A] private (@untrackedCaptures initElems: Array[AnyRef]^, initLength: Int):
+  private var elems: Array[AnyRef]^ = initElems
+  private var start = 0
+  private var end = initLength
+
+  def +=(elem: A): this.type =
+    elems(end) = elem.asInstanceOf[AnyRef]
+    this
+
+  override def toString =
+    val slice = elems.slice(start, end)
+    val wrapped = wrapRefArray(slice)
+    //val wrapped2 = collection.mutable.ArraySeq.ofRef(slice)
+    val str = wrapped.mkString(", ")
+    str
+    //s"ArrayBuffer(${elems.slice(start, end).mkString(", ")})"
diff --git a/tests/pos-custom-args/captures/capt-depfun2.scala b/tests/pos-custom-args/captures/capt-depfun2.scala
@@ -3,9 +3,11 @@ import annotation.retains
 class C
 type Cap = C @retains[caps.cap.type]
 
+class Arr[T]
+
 class STR
 def f(consume y: Cap, consume z: Cap) =
   def g(): C @retains[y.type | z.type] = ???
-  val ac: ((x: Cap) -> Array[STR @retains[x.type]]) = ???
-  val dc: Array[? >: STR <: STR^]^{y, z} = ac(g()) // needs to be inferred
+  val ac: ((x: Cap) => Arr[STR @retains[x.type]]^{x}) = ???
+  val dc: Arr[? >: STR <: STR^]^{y, z} = ac(g()) // needs to be inferred
   val ec = ac(y)
diff --git a/tests/pos-custom-args/captures/freeze.scala b/tests/pos-custom-args/captures/freeze.scala
diff --git a/tests/pos-custom-args/captures/mut-arrays.scala b/tests/pos-custom-args/captures/mut-arrays.scala
diff --git a/tests/pos-custom-args/captures/ro-array.scala b/tests/pos-custom-args/captures/ro-array.scala
diff --git a/tests/pos-custom-args/captures/sealed-value-class.scala b/tests/pos-custom-args/captures/sealed-value-class.scala
diff --git a/tests/pos-custom-args/captures/steppers.scala b/tests/pos-custom-args/captures/steppers.scala
diff --git a/tests/run-custom-args/captures/colltest5/CollectionStrawManCC5_1.scala b/tests/run-custom-args/captures/colltest5/CollectionStrawManCC5_1.scala
diff --git a/tests/run-custom-args/captures/minicheck-mutable.scala b/tests/run-custom-args/captures/minicheck-mutable.scala

Original file line number	Diff line number	Diff line change
`@@ -1886,7 +1886,7 @@ object SymDenotations {`
`1886`	`1886`	`myBaseTypeCache.nn`
`1887`	`1887`	`}`
`1888`	`1888`
`1889`		`- private def invalidateBaseDataCache() = {`
	`1889`	`+ def invalidateBaseDataCache() = {`
`1890`	`1890`	`baseDataCache.invalidate()`
`1891`	`1891`	`baseDataCache = BaseData.None`
`1892`	`1892`	`}`
Original file line number	Diff line number	Diff line change
`@@ -2,6 +2,6 @@`
`2`	`2`	`15 \| (x: Ref^) => (op: Ref^ => IRef) => op(x) // error`
`3`	`3`	`\| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^`
`4`	`4`	`\| Found: Ref^ -> (Ref^ => IRef) -> IRef`
`5`		`- \| Required: scala.caps.Mutable`
	`5`	`+ \| Required: scala.caps.Mutable \| Array[?]`
`6`	`6`	`\|`
`7`	`7`	\| longer explanation available when compiling with `-explain`