Treat local mutable vars as capabilities (#24815)

Under separation checking: A mutable var owned by a term that is not
annotated with @untrackedCaptures gives rise to a Mutable capability.
Since a mutable variable is not trackable, we do this by adding a
varMirror symbol to the variable which represents the capability.

Author: odersky

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

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

@@ -459,6 +459,18 @@ object Capabilities:
       case self: CoreCapability => self.isTrackableRef
       case _ => true
 
+    /** Under separation 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

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

@@ -74,6 +74,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)
@@ -493,6 +495,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] =
@@ -666,6 +674,16 @@ extension (sym: Symbol)
   def isArrayUnderStrictMut(using Context): Boolean =
     sym == defn.ArrayClass && ccConfig.strictMutability
 
+  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

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]
@@ -690,8 +690,15 @@ class CheckCaptures extends Recheck, SymTransformer:
         // Lazy vals are like parameterless methods: accessing them may trigger initialization
         // that uses captured references.
         includeCallCaptures(sym, sym.info, tree)
-      else if sym.exists && !sym.isStatic then
-        markPathFree(sym.termRef, pt, tree)
+      else
+        if sym.isMutableVar && sym.owner.isTerm && pt != LhsProto then
+          // When we have `var x: A^{c} = ...` where `x` is a local variable then
+          // when dereferencing `x` we also need to charge `c`.
+          // For fields it's not a problem since `c` would already have been
+          // charged for the prefix `p` in `p.x`.
+          markFree(sym.info.captureSet, tree)
+        if sym.exists && !sym.isStatic then
+          markPathFree(sym.termRef, pt, tree)
       mapResultRoots(super.recheckIdent(tree, pt), tree.symbol)
 
     override def recheckThis(tree: This, pt: Type)(using Context): Type =
@@ -713,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
@@ -1062,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
@@ -1135,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.
      */

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,

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)}.

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 =

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

@@ -1027,9 +1027,11 @@ class Definitions {
     @tu lazy val Caps_unsafeDiscardUses: Symbol = CapsUnsafeModule.requiredMethod("unsafeDiscardUses")
     @tu lazy val Caps_unsafeErasedValue: Symbol = CapsUnsafeModule.requiredMethod("unsafeErasedValue")
     @tu lazy val Caps_ContainsTrait: TypeSymbol = CapsModule.requiredType("Contains")
+    @tu lazy val Caps_Shared: TypeSymbol = CapsModule.requiredType("Shared")
     @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")
 
@@ -1988,10 +1990,10 @@ class Definitions {
     CapsModule, CapsModule.moduleClass, PureClass,
     /* Caps_Classifier, Caps_SharedCapability, Caps_Control, -- already stable */
     Caps_ExclusiveCapability, Caps_Mutable, Caps_Read, Caps_Unscoped, Caps_Stateful, Caps_Separate,
-    RequiresCapabilityAnnot,
+    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)
 

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

@@ -799,13 +799,12 @@ object SymDenotations {
       *
       * Note, (f: => T) is treated as a stable TermRef only in Capture Sets.
       */
-    final def isStableMember(using Context): Boolean = {
+    final def isStableMember(using Context): Boolean =
       def isUnstableValue =
         isOneOf(UnstableValueFlags)
-        || !ctx.mode.is(Mode.InCaptureSet) && info.isInstanceOf[ExprType]
+        || info.isInstanceOf[ExprType]
         || isAllOf(InlineParam)
       isType || is(StableRealizable) || exists && !isUnstableValue
-    }
 
     /** Is this a denotation of a real class that does not have - either direct or inherited -
      *  initialization code?

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) =>