Treat local mutable vars as capabilities

odersky · odersky · commit cd61affe6acf · 2025-12-22T13:05:39.000+01:00
diff --git a/compiler/src/dotty/tools/dotc/cc/CCState.scala b/compiler/src/dotty/tools/dotc/cc/CCState.scala
@@ -79,6 +79,11 @@ class CCState:
   object Unrecorded extends VarState.Unrecorded
   object ClosedUnrecorded extends VarState.ClosedUnrecorded
 
+  // ----- Mirrors for local vars -------------------------
+
+  /** A cache for mirrors of local mutable vars */
+  val varMirrors = util.EqHashMap[Symbol, Symbol]()
+
   // ------ Context info accessed from companion object when isCaptureCheckingOrSetup is true
 
   private var openExistentialScopes: List[MethodType] = Nil
diff --git a/compiler/src/dotty/tools/dotc/cc/Capability.scala b/compiler/src/dotty/tools/dotc/cc/Capability.scala
@@ -459,6 +459,18 @@ object Capabilities:
       case self: CoreCapability => self.isTrackableRef
       case _ => true
 
+    /** Under separatiion checking: Is this a mutable var owned by a term that is
+     *  not annotated with @untrackedCaptures? Such mutable variables need to be
+     *  tracked as capabilities. Since mutable variables are not trackable, we do
+     *  this by adding a varMirror symbol to such variables which represents the capability.
+     */
+    final def isLocalMutable(using Context): Boolean = this match
+      case tp @ TermRef(NoPrefix, _) =>
+        ccConfig.newScheme && ccConfig.strictMutability
+        && tp.symbol.isMutableVar
+        && !tp.symbol.hasAnnotation(defn.UntrackedCapturesAnnot)
+      case _ => false
+
     /** The non-derived capability underlying this capability */
     final def core: CoreCapability | RootCapability = this match
       case self: (CoreCapability | RootCapability) => self
diff --git a/compiler/src/dotty/tools/dotc/cc/CaptureOps.scala b/compiler/src/dotty/tools/dotc/cc/CaptureOps.scala
@@ -86,6 +86,8 @@ extension (tp: Type)
       GlobalCap
     case ref: Capability if ref.isTrackableRef =>
       ref
+    case ref: TermRef if ref.isLocalMutable =>
+      ref.mapLocalMutable
     case _ =>
       // if this was compiled from cc syntax, problem should have been reported at Typer
       throw IllegalCaptureRef(tp)
@@ -503,6 +505,12 @@ extension (tp: MethodType)
   def marksExistentialScope(using Context): Boolean =
     !tp.resType.isInstanceOf[MethodOrPoly]
 
+extension (ref: TermRef | ThisType)
+  /** Map a local mutable var to its mirror */
+  def mapLocalMutable(using Context): TermRef | ThisType = ref match
+    case ref: TermRef if ref.isLocalMutable => ref.symbol.varMirror.termRef
+    case _ => ref
+
 extension (cls: ClassSymbol)
 
   def pureBaseClass(using Context): Option[Symbol] =
@@ -670,6 +678,13 @@ extension (sym: Symbol)
   def isDisallowedInCapset(using Context): Boolean =
     sym.isOneOf(if ccConfig.newScheme && ccConfig.strictMutability then Method else UnstableValueFlags)
 
+  def varMirror(using Context): Symbol =
+    ccState.varMirrors.getOrElseUpdate(sym,
+      sym.copy(
+        flags = Flags.EmptyFlags,
+        info = defn.Caps_Var.typeRef.appliedTo(sym.info)
+            .capturing(FreshCap(sym, Origin.InDecl(sym)))))
+
 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/CheckCaptures.scala b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
@@ -106,14 +106,14 @@ object CheckCaptures:
   /** Check that a @retains annotation only mentions references that can be tracked.
    *  This check is performed at Typer.
    */
-  def checkWellformed(parent: Tree, ann: Tree)(using Context): Unit =
+  def checkWellformedRetains(parent: Tree, ann: Tree)(using Context): Unit =
     def check(elem: Type): Unit = elem match
       case ref: TypeRef =>
         val refSym = ref.symbol
         if refSym.isType && !refSym.info.derivesFrom(defn.Caps_CapSet) then
           report.error(em"$elem is not a legal element of a capture set", ann.srcPos)
       case ref: CoreCapability =>
-        if !ref.isTrackableRef && !ref.isCapRef then
+        if !ref.isTrackableRef && !ref.isCapRef && !ref.isLocalMutable then
           report.error(em"$elem cannot be tracked since it is not a parameter or local value", ann.srcPos)
       case ReachCapability(ref) =>
         check(ref)
@@ -306,7 +306,7 @@ class CheckCaptures extends Recheck, SymTransformer:
      */
     private val useInfos = mutable.ArrayBuffer[(Tree, CaptureSet, Env)]()
 
-    private var usedSet = util.EqHashMap[Tree, CaptureSet]()
+    private val usedSet = util.EqHashMap[Tree, CaptureSet]()
 
     /** The set of symbols that were rechecked via a completer */
     private val completed = new mutable.HashSet[Symbol]
@@ -720,7 +720,7 @@ class CheckCaptures extends Recheck, SymTransformer:
         val sel = ref.select(pt.selector).asInstanceOf[TermRef]
         markPathFree(sel, pt.pt, pt.select)
       case _ =>
-        markFree(ref.adjustReadOnly(pt), tree)
+        markFree(ref.mapLocalMutable.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
@@ -1069,7 +1069,7 @@ class CheckCaptures extends Recheck, SymTransformer:
       recheck(tree.rhs, lhsType.widen)
       lhsType match
         case lhsType @ TermRef(qualType, _)
-        if (qualType ne NoPrefix) && !lhsType.symbol.hasAnnotation(defn.UntrackedCapturesAnnot) =>
+        if !lhsType.symbol.hasAnnotation(defn.UntrackedCapturesAnnot) =>
           checkUpdate(qualType, tree.srcPos)(i"Cannot assign to field ${lhsType.name} of ${qualType.showRef}")
         case _ =>
       defn.UnitType
@@ -1142,6 +1142,13 @@ class CheckCaptures extends Recheck, SymTransformer:
         openClosures = openClosures.tail
     end recheckClosureBlock
 
+    /** Add var mirrors to the list of block-local symbols to avoid */
+    override def avoidLocals(tp: Type, symsToAvoid: => List[Symbol])(using Context): Type =
+      val locals = symsToAvoid
+      val varMirrors = locals.collect:
+        case local if local.termRef.isLocalMutable => local.varMirror
+      super.avoidLocals(tp, varMirrors ++ locals)
+
     /** Elements of a SeqLiteral instantiate a Seq or Array parameter, so they
      *  should be boxed.
      */
diff --git a/compiler/src/dotty/tools/dotc/cc/Mutability.scala b/compiler/src/dotty/tools/dotc/cc/Mutability.scala
@@ -121,7 +121,7 @@ object Mutability:
         && (!tp.isStatefulType || tp.captureSet.mutability == CaptureSet.Mutability.Reader)
 
   extension (ref: TermRef | ThisType)
-    /** Map `ref` to `ref.readOnly` if its type extends Mutble, and one of the
+    /** Map `ref` to `ref.readOnly` if its type extends Mutable, and one of the
      *  following is true:
      *    - it appears in a non-exclusive context,
      *    - the expected type is a value type that is not a stateful type,
diff --git a/compiler/src/dotty/tools/dotc/cc/SepCheck.scala b/compiler/src/dotty/tools/dotc/cc/SepCheck.scala
@@ -744,7 +744,9 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser:
       val captured = genPart.deepCaptureSet.elems
       val hiddenSet = captured.transHiddenSet.pruned
       val clashSet = otherPart.deepCaptureSet.elems
-      val deepClashSet = clashSet.completeFootprint.nonPeaks.pruned
+      var deepClashSet = clashSet.completeFootprint.nonPeaks.pruned
+      if deepClashSet.isEmpty then
+        deepClashSet = clashSet.completeFootprint.pruned
       report.error(
         em"""Separation failure in ${role.description} $tpe.
             |One part,  $genPart, hides capabilities  ${CaptureSet(hiddenSet)}.
diff --git a/compiler/src/dotty/tools/dotc/cc/ccConfig.scala b/compiler/src/dotty/tools/dotc/cc/ccConfig.scala
@@ -54,7 +54,7 @@ object ccConfig:
 
   /** Not used currently. Handy for trying out new features */
   def newScheme(using ctx: Context): Boolean =
-    Feature.sourceVersion.stable.isAtLeast(SourceVersion.`3.7`)
+    Feature.sourceVersion.stable.isAtLeast(SourceVersion.`3.8`)
 
   /** Allow @use annotations */
   def allowUse(using Context): Boolean =
diff --git a/compiler/src/dotty/tools/dotc/core/Definitions.scala b/compiler/src/dotty/tools/dotc/core/Definitions.scala
@@ -1030,6 +1030,7 @@ class Definitions {
     @tu lazy val Caps_ContainsModule: Symbol = requiredModule("scala.caps.Contains")
     @tu lazy val Caps_containsImpl: TermSymbol = Caps_ContainsModule.requiredMethod("containsImpl")
     @tu lazy val Caps_freeze: TermSymbol = CapsModule.requiredMethod("freeze")
+    @tu lazy val Caps_Var: ClassSymbol = requiredClass("scala.caps.internal.Var")
 
   @tu lazy val PureClass: ClassSymbol = requiredClass("scala.caps.Pure")
 
@@ -1990,7 +1991,7 @@ class Definitions {
     Caps_Shared, RequiresCapabilityAnnot,
     captureRoot, Caps_CapSet, Caps_ContainsTrait, Caps_ContainsModule, Caps_ContainsModule.moduleClass,
     ConsumeAnnot, UseAnnot, ReserveAnnot,
-    CapsUnsafeModule, CapsUnsafeModule.moduleClass, Caps_freeze,
+    CapsUnsafeModule, CapsUnsafeModule.moduleClass, Caps_freeze, Caps_Var,
     CapsInternalModule, CapsInternalModule.moduleClass,
     RetainsAnnot, RetainsCapAnnot, RetainsByNameAnnot)
 
diff --git a/compiler/src/dotty/tools/dotc/core/TypeOps.scala b/compiler/src/dotty/tools/dotc/core/TypeOps.scala
@@ -566,9 +566,7 @@ object TypeOps:
   def avoid(tp: Type, symsToAvoid: => List[Symbol])(using Context): Type = {
     val widenMap = new AvoidMap {
       @threadUnsafe lazy val forbidden = symsToAvoid.toSet
-      def toAvoid(tp: NamedType) =
-        val sym = tp.symbol
-        forbidden.contains(sym)
+      def toAvoid(tp: NamedType) = forbidden.contains(tp.symbol)
 
       override def apply(tp: Type): Type = tp match
         case tp: TypeVar if mapCtx.typerState.constraint.contains(tp) =>
diff --git a/compiler/src/dotty/tools/dotc/transform/Recheck.scala b/compiler/src/dotty/tools/dotc/transform/Recheck.scala
@@ -392,10 +392,13 @@ abstract class Recheck extends Phase, SymTransformer:
       recheck(tree.rhs, lhsType.widen)
       defn.UnitType
 
+    protected def avoidLocals(tp: Type, symsToAvoid: => List[Symbol])(using Context): Type =
+      TypeOps.avoid(tp, symsToAvoid)
+
     private def recheckBlock(stats: List[Tree], expr: Tree, pt: Type)(using Context): Type =
       recheckStats(stats)
       val exprType = recheck(expr, pt)
-      TypeOps.avoid(exprType, localSyms(stats).filterConserve(_.isTerm))
+      avoidLocals(exprType, localSyms(stats).filterConserve(_.isTerm))
 
     def recheckBlock(tree: Block, pt: Type)(using Context): Type = tree match
       case Block((mdef : DefDef) :: Nil, closure: Closure) =>
@@ -439,7 +442,7 @@ abstract class Recheck extends Phase, SymTransformer:
       // for blocks since a case branch is of the form `return[MatchResultN] { ... }`
       // For source-level returns from methods, there's nothing to avoid, since the
       // result type of a method with a return must be given explicitly.
-      def avoidMap = new TypeOps.AvoidMap:
+      val avoidMap = new TypeOps.AvoidMap:
         def toAvoid(tp: NamedType) =
            tp.symbol.is(Case) && tp.symbol.owner.isContainedIn(ctx.owner)
 
diff --git a/compiler/src/dotty/tools/dotc/typer/Typer.scala b/compiler/src/dotty/tools/dotc/typer/Typer.scala
@@ -3602,7 +3602,7 @@ class Typer(@constructorOnly nestingLevel: Int = 0) extends Namer
     if (ctx.mode is Mode.Type) {
       val cls = annot1.symbol.maybeOwner
       if Feature.ccEnabled && cls.isRetainsLike then
-        CheckCaptures.checkWellformed(arg1, annot1)
+        CheckCaptures.checkWellformedRetains(arg1, annot1)
       if arg1.isType then
         assignType(cpy.Annotated(tree)(arg1, annot1), arg1, annot1)
       else
diff --git a/library/src/scala/caps/package.scala b/library/src/scala/caps/package.scala
@@ -191,6 +191,12 @@ object internal:
    */
   def erasedValue[T]: T = ???
 
+  /** A trait for capabilities representing usage of mutable vars in capture sets.
+   */
+  trait Var[T] extends Mutable:
+    def get: T
+    update def set(x: T): Unit
+
 end internal
 
 /** A wrapper that strips all covariant capture sets from Mutable types in the
diff --git a/tests/neg-custom-args/captures/i23431.check b/tests/neg-custom-args/captures/i23431.check
@@ -27,16 +27,18 @@
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/i23431.scala:12:12 ---------------------------------------
 12 |    withIO: io3 =>  // error
    |            ^
-   |Found:    (io3: IO^'s1) ->'s2 Unit
+   |Found:    (io3: IO^'s1) ->{myIO} Unit
    |Required: IO^ => Unit
    |
    |Note that capability cap is not included in capture set {cap²}
-   |because cap in an enclosing function is not visible from cap² in variable myIO.
+   |because cap in an enclosing function is not visible from cap² in variable myIO².
    |
-   |where:    =>   refers to a fresh root capability created in anonymous function of type (io1: IO^): Unit when checking argument to parameter op of method withIO
-   |          ^    refers to the universal root capability
-   |          cap  is a fresh root capability created in anonymous function of type (io3: IO^'s1): Unit of parameter parameter io3² of method $anonfun
-   |          cap² is a fresh root capability in the type of variable myIO
+   |where:    =>    refers to a fresh root capability created in anonymous function of type (io1: IO^): Unit when checking argument to parameter op of method withIO
+   |          ^     refers to the universal root capability
+   |          cap   is a fresh root capability created in anonymous function of type (io3: IO^'s1): Unit of parameter parameter io3² of method $anonfun
+   |          cap²  is a fresh root capability in the type of variable myIO²
+   |          myIO  is a value in an anonymous function in method test
+   |          myIO² is a variable in an anonymous function in method test
    |
 13 |      myIO = io3
    |
diff --git a/tests/neg-custom-args/captures/indirect-avoid.check b/tests/neg-custom-args/captures/indirect-avoid.check
@@ -0,0 +1,41 @@
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/indirect-avoid.scala:16:4 --------------------------------
+16 |    nll // error
+   |    ^^^
+   |    Found:    Test.LL^{nll}
+   |    Required: Test.LL^{ll}
+   |
+   |    Note that capability nll is not included in capture set {ll}.
+   |
+   | longer explanation available when compiling with `-explain`
+-- Warning: tests/neg-custom-args/captures/indirect-avoid.scala:24:6 ---------------------------------------------------
+24 |  val x1 = filterImpl1(LL())
+   |      ^^
+   |      value x1 has a non-empty capture set but will not be added as
+   |      a capability to computed capture sets since it is globally accessible
+   |      as a member of static object Test. Global values cannot be capabilities.
+-- Warning: tests/neg-custom-args/captures/indirect-avoid.scala:25:6 ---------------------------------------------------
+25 |  val _: LL^{cap.rd}= x1
+   |      ^
+   |      value _$1 has a non-empty capture set but will not be added as
+   |      a capability to computed capture sets since it is globally accessible
+   |      as a member of static object Test. Global values cannot be capabilities.
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/indirect-avoid.scala:26:14 -------------------------------
+26 |  val _: LL = x1 // error
+   |              ^^
+   |Found:    (Test.x1 : Test.LL^{cap.rd})
+   |Required: Test.LL
+   |
+   |Note that capability cap.rd is not included in capture set {}.
+   |
+   |where:    cap is a fresh root capability created in value x1 when instantiating method filterImpl1's type (ll: Test.LL^): Test.LL^{cap².rd, ll}
+   |
+   | longer explanation available when compiling with `-explain`
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/indirect-avoid.scala:32:4 --------------------------------
+32 |    nll // error
+   |    ^^^
+   |    Found:    Test.LL^{nll}
+   |    Required: Test.LL^{ll}
+   |
+   |    Note that capability nll is not included in capture set {ll}.
+   |
+   | longer explanation available when compiling with `-explain`
diff --git a/tests/neg-custom-args/captures/indirect-avoid.scala b/tests/neg-custom-args/captures/indirect-avoid.scala
@@ -0,0 +1,32 @@
+import caps.*
+
+class Ref[T](init: T) extends Mutable:
+  private var cur: T = init
+  def get(): T = cur
+  update def set(x: T): Unit = cur = x
+
+object Test:
+
+  class LL
+
+  def filterImpl(ll: LL^): LL^{ll} =
+    var x: LL^{ll} = ???
+    val cl: () ->{x, x.rd, ll} LL^{ll} = ???
+    val nll: LL^{cl} = ???
+    nll // error
+
+  def filterImpl1(ll: LL^) =
+    val x: Ref[LL^{ll}] = ???
+    val cl: () ->{x, x.rd, ll} LL^{ll} = ???
+    val nll: LL^{cl} = ???
+    nll
+
+  val x1 = filterImpl1(LL())
+  val _: LL^{cap.rd}= x1
+  val _: LL = x1 // error
+
+  def filterImpl2(ll: LL^): LL^{ll} =
+    val x: Ref[LL^{ll}] = ???
+    val cl: () ->{x, x.rd, ll} LL^{ll} = ???
+    val nll: LL^{cl} = ???
+    nll // error
diff --git a/tests/neg-custom-args/captures/local-mutables-2.check b/tests/neg-custom-args/captures/local-mutables-2.check
@@ -0,0 +1,21 @@
+-- Error: tests/neg-custom-args/captures/local-mutables-2.scala:7:9 ----------------------------------------------------
+7 |def foo() = // error: separation failure
+  |         ^
+  |Separation failure in method foo's inferred result type (() ->{cap.rd} Int, Int => Unit)^{}.
+  |One part,  () ->{cap.rd} Int, hides capabilities  {cap².rd}.
+  |Another part,  Int => Unit,  captures capabilities  {cap³, cap, cap²}.
+  |The two sets overlap at  {cap of value r}.
+  |
+  |where:    => and cap³ refer to a fresh root capability classified as Unscoped in the result type of method foo
+  |          cap         is a fresh root capability classified as Unscoped in the type of value r
+  |          cap²        is a fresh root capability classified as Unscoped created in value r when constructing instance Ref
+-- Error: tests/neg-custom-args/captures/local-mutables-2.scala:11:10 --------------------------------------------------
+11 |def foo2() = // error: separation failure
+   |          ^
+   |        Separation failure in method foo2's inferred result type (() ->{cap.rd} Int, Int => Unit)^{}.
+   |        One part,  Int => Unit, hides capabilities  {cap}.
+   |        Another part,  () ->{cap.rd} Int,  captures capabilities  {cap.rd}.
+   |        The two sets overlap at  {cap of variable r}.
+   |
+   |        where:    =>  refers to a fresh root capability classified as Unscoped in the result type of method foo2
+   |                  cap is a fresh root capability classified as Unscoped in the type of variable r
diff --git a/tests/neg-custom-args/captures/local-mutables-2.scala b/tests/neg-custom-args/captures/local-mutables-2.scala
@@ -0,0 +1,20 @@
+import caps.*
+class Ref extends Mutable:
+  var cur = 0
+  def get: Int = cur
+  update def set(x: Int): Unit = cur = x
+
+def foo() = // error: separation failure
+  val r = Ref()
+  (() => r.get, (x: Int) => r.set(x))
+
+def foo2() = // error: separation failure
+  var r: Int = 0
+  (() => r, (x: Int) => r = x)
+
+class Struct:
+  private val r: Ref^ = Ref()
+  val getter = () => r.get
+  val setter = (x: Int) => r.set(x)
+
+def bar() = Struct()  // ok
diff --git a/tests/neg-custom-args/captures/local-mutables.check b/tests/neg-custom-args/captures/local-mutables.check
diff --git a/tests/neg-custom-args/captures/local-mutables.scala b/tests/neg-custom-args/captures/local-mutables.scala
diff --git a/tests/neg-custom-args/captures/reaches.check b/tests/neg-custom-args/captures/reaches.check
diff --git a/tests/neg-custom-args/captures/vars.check b/tests/neg-custom-args/captures/vars.check
diff --git a/tests/neg-custom-args/captures/vars.scala b/tests/neg-custom-args/captures/vars.scala
diff --git a/tests/pos-custom-args/captures/capt-wf2.scala b/tests/pos-custom-args/captures/capt-wf2.scala
diff --git a/tests/pos-custom-args/captures/untracked-captures.scala b/tests/pos-custom-args/captures/untracked-captures.scala
diff --git a/tests/pos-custom-args/captures/vars.scala b/tests/pos-custom-args/captures/vars.scala
