Add capture root levels -- first draft

Author: odersky

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

@@ -26,6 +26,18 @@ private[cc] def retainedElems(tree: Tree)(using Context): List[Tree] = tree matc
   case Apply(_, Typed(SeqLiteral(elems, _), _) :: Nil) => elems
   case _ => Nil
 
+/** Map @retain'ed arguments with a Symbol->Symbol function, keeping the same trees
+ *  but with mapped symbols.
+ */
+private[cc] def mapRetainedElems(tree: Tree)(f: Symbol => Symbol)(using Context): Tree = tree match
+  case Apply(fn, (typd @ Typed(seqlit @ SeqLiteral(elems, tpt1), tpt2)) :: Nil) =>
+    val elems1 = elems.mapConserve: elem =>
+      val sym1 = f(elem.symbol)
+      if sym1 ne elem.symbol then elem.withType(sym1.namedType) else elem
+    if elems1 ne elems then
+      cpy.Apply(tree)(fn, cpy.Typed(typd)(cpy.SeqLiteral(seqlit)(elems1, tpt1), tpt2) :: Nil)
+    else tree
+
 def allowUniversalInBoxed(using Context) =
   Feature.sourceVersion.isAtLeast(SourceVersion.`3.3`)
 
@@ -253,6 +265,10 @@ extension (sym: Symbol)
     && sym != defn.Caps_unsafeBox
     && sym != defn.Caps_unsafeUnbox
 
+  /** The nesting level of `sym` according to capture checking */
+  def ccNestingLevel(using Context): Int =
+    Setup.ccNestingLevel(sym)
+
 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

@@ -16,6 +16,7 @@ import util.{SimpleIdentitySet, Property}
 import util.common.alwaysTrue
 import scala.collection.mutable
 import config.Config.ccAllowUnsoundMaps
+import config.Printers.{captLevels, noPrinter}
 import transform.SymUtils.{maxNested, minNested}
 
 /** A class for capture sets. Capture sets can be constants or variables.
@@ -74,11 +75,10 @@ sealed abstract class CaptureSet extends Showable:
     asInstanceOf[Var]
 
   /** Does this capture set contain the root reference `cap` as element? */
-  final def isUniversal(using Context) =
-    elems.exists {
-      case ref: TermRef => ref.symbol == defn.captureRoot
-      case _ => false
-    }
+  final def isUniversal(using Context) = elems.exists(_.isGlobalRootCapability)
+
+  /** Does this capture set contain a global or local root references as elements? */
+  final def isRoot(using Context) = elems.exists(_.isRootCapability)
 
   /** Add new elements to this capture set if allowed.
    *  @pre `newElems` is not empty and does not overlap with `this.elems`.
@@ -120,17 +120,31 @@ sealed abstract class CaptureSet extends Showable:
     private def subsumes(y: CaptureRef) =
       (x eq y)
       || y.match
-          case y: TermRef => y.prefix eq x
+          case y: TermRef => (y.prefix eq x) || x.isRootIncluding(y)
           case _ => false
 
+    private def isRootIncluding(y: CaptureRef) =
+      x.isRootCapability && y.isRootCapability && {
+        val xsym = x.termSymbol
+        val ysym = y.termSymbol
+        xsym == defn.captureRoot    // roots without level are compatible with all other roots
+        || ysym == defn.captureRoot
+        || xsym.ccNestingLevel >= ysym.ccNestingLevel
+      }
+  end extension
+
   /** {x} <:< this   where <:< is subcapturing, but treating all variables
    *                 as frozen.
    */
   def accountsFor(x: CaptureRef)(using Context): Boolean =
-    reporting.trace(i"$this accountsFor $x, ${x.captureSetOfInfo}?", show = true) {
-      elems.exists(_.subsumes(x))
-      || !x.isRootCapability && x.captureSetOfInfo.subCaptures(this, frozen = true).isOK
-    }
+    if comparer.isInstanceOf[ExplainingTypeComparer] then // !!! DEBUG
+      reporting.trace.force(i"$this accountsFor $x, ${x.captureSetOfInfo}?", show = true):
+        elems.exists(_.subsumes(x))
+        || !x.isRootCapability && x.captureSetOfInfo.subCaptures(this, frozen = true).isOK
+    else
+      reporting.trace(i"$this accountsFor $x, ${x.captureSetOfInfo}?", show = true):
+        elems.exists(_.subsumes(x))
+        || !x.isRootCapability && x.captureSetOfInfo.subCaptures(this, frozen = true).isOK
 
   /** A more optimistic version of accountsFor, which does not take variable supersets
    *  of the `x` reference into account. A set might account for `x` if it accounts
@@ -278,7 +292,9 @@ sealed abstract class CaptureSet extends Showable:
 
   /** Invoke handler if this set has (or later aquires) the root capability `cap` */
   def disallowRootCapability(handler: () => Context ?=> Unit)(using Context): this.type =
-    if isUniversal then handler()
+    if
+      if allowUniversalInBoxed then isUniversal else isRoot
+    then handler()
     this
 
   /** Invoke handler on the elements to ensure wellformedness of the capture set.
@@ -433,10 +449,32 @@ object CaptureSet:
     def resetDeps()(using state: VarState): Unit =
       deps = state.deps(this)
 
+    /** If `root` is a local root, check that its level is not smaller than
+     *  the set's owner's nesting level.
+     *  @param ref The actually checked reference to be use in the error message.
+     *             Currently always the same as `root`.
+     */
+    private def checkLevel(ref: CaptureRef, root: CaptureRef)(using Context): Unit =
+      if root.isLocalRootCapability then
+        if root.termSymbol.ccNestingLevel > owner.ccNestingLevel then
+          throw LevelException(owner, ref)
+
     def addNewElems(newElems: Refs, origin: CaptureSet)(using Context, VarState): CompareResult =
+      //println(i"ADD ${newElems.toList} to $this in $owner")
       if !isConst && recordElemsState() then
         elems ++= newElems
-        if isUniversal then rootAddedHandler()
+        for elem <- newElems do
+          if elem.isLocalRootCapability then
+            checkLevel(elem, elem)
+          else if elem.isGlobalRootCapability then
+            rootAddedHandler()
+          else if false then
+            // Disabled since it gives spurious errors for references that end up
+            // being avoided through healing. TODO: enable it when level-checking
+            // and avoidance is better integrated.
+            for superElem <- elem.captureSetOfInfo.elems.toList do
+              checkLevel(elem, superElem)
+
         newElemAddedHandler(newElems.toList)
         // assert(id != 5 || elems.size != 3, this)
         (CompareResult.OK /: deps) { (r, dep) =>
@@ -950,4 +988,8 @@ object CaptureSet:
             println(i"  ${cv.show.padTo(20, ' ')} :: ${cv.deps.toList}%, %")
       }
     else op
+
+  class LevelException(val owner: Symbol, val ref: CaptureRef) extends Exception {
+    if captLevels ne noPrinter then printStackTrace()
+  }
 end CaptureSet

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

@@ -17,10 +17,10 @@ import transform.SymUtils.*
 import transform.{Recheck, PreRecheck}
 import Recheck.*
 import scala.collection.mutable
-import CaptureSet.{withCaptureSetsExplained, IdempotentCaptRefMap}
+import CaptureSet.{withCaptureSetsExplained, IdempotentCaptRefMap, LevelException}
 import StdNames.nme
 import NameKinds.DefaultGetterName
-import reporting.{trace, ClosureParameterMismatch}
+import reporting.*
 
 /** The capture checker */
 object CheckCaptures:
@@ -157,6 +157,10 @@ object CheckCaptures:
   /** Attachment key for bodies of closures, provided they are values */
   val ClosureBodyValue = Property.Key[Unit]
 
+  /** Report level violation */
+  def levelError[T](ex: LevelException, pos: SrcPos)(using Context): Unit =
+    report.error(em"local reference ${ex.ref} escapes into outer capture set of ${ex.owner}", pos)
+
 class CheckCaptures extends Recheck, SymTransformer:
   thisPhase =>
 
@@ -203,6 +207,15 @@ class CheckCaptures extends Recheck, SymTransformer:
           case _ =>
             traverseChildren(t)
 
+    /** Map all occurrences of `cap` in a type to the currently valid local capture root. */
+    private def mapRootsIn(using Context) = new IdempotentCaptRefMap:
+      def apply(t: Type) = t.dealiasKeepAnnots match
+        case CapturingType(parent, refs) if refs.isUniversal =>
+          val parent1 = apply(parent)
+          CapturingType(parent1, CaptureSet(setup.localRoot(setup.currentScopeOwner)))
+        case _ =>
+          mapOver(t)
+
     /** If `tpt` is an inferred type, interpolate capture set variables appearing contra-
      *  variantly in it.
      */
@@ -504,11 +517,16 @@ class CheckCaptures extends Recheck, SymTransformer:
           mdef.rhs.putAttachment(ClosureBodyValue, ())
         case _ =>
 
+      val mapRoots = mapRootsIn(using ctx.withOwner(mdef.symbol))
+
+      def checkCompatible(lower: Type, upper: Type, tree: Tree, msgFn: (Type, Type) => TypeMismatchMsg): Unit =
+        withMode(Mode.CCIgnoreBoxing):
+          if !isCompatible(lower, upper, tree) then
+            report.error(msgFn(lower, upper), tree.srcPos)
+
       def constrainParams(ptformals: List[Type], params: ParamClause) =
-        for (param, ptformal) <- params.lazyZip(ptformals) do
-          withMode(Mode.CCIgnoreBoxing):
-            if !isCompatible(ptformal, param.symbol.info, param) then
-              report.error(ClosureParameterMismatch(ptformal, param.symbol.info), param.srcPos)
+        for (param, ptformal) <- params.lazyZip(ptformals.mapConserve(mapRoots)) do
+          checkCompatible(ptformal, param.symbol.info, param, ClosureParameterMismatch(_, _))
 
       def constrain(pt: Type, paramss: List[ParamClause]): Unit = (pt: @unchecked) match
         case RefinedType(_, nme.apply, rinfo) =>
@@ -521,10 +539,11 @@ class CheckCaptures extends Recheck, SymTransformer:
           constrainParams(ptformals, paramss.head)
         case _ =>
 
-      //println(i"recheck closure $mdef with $pt")
       constrain(pt.dealias.stripCapturing, mdef.paramss)
       recheckDef(mdef, mdef.symbol)
-      recheckClosure(expr, pt)
+      val clt = recheckClosure(expr, pt)
+      inContext(ctx.withOwner(mdef.symbol)):
+        mapRootsIn(clt)
     end recheckClosureBlock
 
     override def recheckValDef(tree: ValDef, sym: Symbol)(using Context): Unit =
@@ -621,19 +640,23 @@ class CheckCaptures extends Recheck, SymTransformer:
      *  adding all references in the boxed capture set to the current environment.
      */
     override def recheck(tree: Tree, pt: Type = WildcardType)(using Context): Type =
-      val saved = curEnv
-      tree match
-        case _: RefTree | closureDef(_) if pt.isBoxedCapturing =>
-          curEnv = Env(curEnv.owner, EnvKind.Boxed, CaptureSet.Var(curEnv.owner), curEnv)
-        case _ if tree.hasAttachment(ClosureBodyValue) =>
-          curEnv = Env(curEnv.owner, EnvKind.ClosureResult, CaptureSet.Var(curEnv.owner), curEnv)
-        case _ =>
-      val res =
-        try super.recheck(tree, pt)
-        finally curEnv = saved
-      if tree.isTerm && !pt.isBoxedCapturing then
-        markFree(res.boxedCaptureSet, tree.srcPos)
-      res
+      try
+        val saved = curEnv
+        tree match
+          case _: RefTree | closureDef(_) if pt.isBoxedCapturing =>
+            curEnv = Env(curEnv.owner, EnvKind.Boxed, CaptureSet.Var(curEnv.owner), curEnv)
+          case _ if tree.hasAttachment(ClosureBodyValue) =>
+            curEnv = Env(curEnv.owner, EnvKind.ClosureResult, CaptureSet.Var(curEnv.owner), curEnv)
+          case _ =>
+        val res =
+          try super.recheck(tree, pt)
+          finally curEnv = saved
+        if tree.isTerm && !pt.isBoxedCapturing then
+          markFree(res.boxedCaptureSet, tree.srcPos)
+        res
+      catch case ex: LevelException =>
+        levelError(ex, tree.srcPos)
+        UnspecifiedErrorType
 
     /** If `tree` is a reference or an application where the result type refers
      *  to an enclosing class or method parameter of the reference, check that the result type
@@ -941,7 +964,8 @@ class CheckCaptures extends Recheck, SymTransformer:
       def traverse(t: Tree)(using Context) =
         t match
           case t: Template =>
-            checkAllOverrides(ctx.owner.asClass, OverridingPairsCheckerCC(_, _, t))
+            try checkAllOverrides(ctx.owner.asClass, OverridingPairsCheckerCC(_, _, t))
+            catch case ex: LevelException => levelError(ex, t.srcPos)
           case _ =>
         traverseChildren(t)
 
@@ -1014,7 +1038,7 @@ class CheckCaptures extends Recheck, SymTransformer:
           capt.println(i"checked $root with $selfType")
     end checkSelfTypes
 
-    /** Heal ill-formed capture sets in the type parameter.
+    /** Heal ill-formed capture sets in the type parameter of function `meth`
      *
      *  We can push parameter refs into a capture set in type parameters
      *  that this type parameter can't see.
@@ -1032,28 +1056,32 @@ class CheckCaptures extends Recheck, SymTransformer:
      *  compensate this by pushing the widened capture set of `f` into ?1.
      *  This solves the soundness issue caused by the ill-formness of ?1.
      */
-    private def healTypeParam(tree: Tree)(using Context): Unit =
+    private def healTypeParam(meth: Symbol, tree: Tree)(using Context): Unit =
       val checker = new TypeTraverser:
         private var allowed: SimpleIdentitySet[TermParamRef] = SimpleIdentitySet.empty
 
         private def isAllowed(ref: CaptureRef): Boolean = ref match
           case ref: TermParamRef => allowed.contains(ref)
+          case ref: TermRef => !(ref.isLocalRootCapability && ref.symbol.owner == meth)
           case _ => true
 
         private def healCaptureSet(cs: CaptureSet): Unit =
           cs.ensureWellformed: elems =>
             ctx ?=>
               var seen = new util.HashSet[CaptureRef]
-              def recur(elems: List[CaptureRef]): Unit =
+              def recur(elems: List[CaptureRef], prev: Option[CaptureRef]): Unit =
                 for ref <- elems do
                   if !isAllowed(ref) && !seen.contains(ref) then
+                    if ref.isLocalRootCapability
+                      && ref.termSymbol.nestingLevel > cs.owner.nestingLevel then
+                        throw LevelException(cs.owner, prev.getOrElse(ref))
                     seen += ref
                     val widened = ref.captureSetOfInfo
                     val added = widened.filter(isAllowed(_))
                     capt.println(i"heal $ref in $cs by widening to $added")
                     checkSubset(added, cs, tree.srcPos)
-                    recur(widened.elems.toList)
-              recur(elems)
+                    recur(widened.elems.toList, Some(ref))
+              recur(elems, None)
 
         def traverse(tp: Type) =
           tp match
@@ -1144,7 +1172,9 @@ class CheckCaptures extends Recheck, SymTransformer:
                 checkBounds(normArgs, tl)
               case _ =>
 
-            args.foreach(healTypeParam(_))
+            args.foreach: arg =>
+              try healTypeParam(fun.symbol, arg)
+              catch case ex: LevelException => levelError(ex, arg.srcPos)
           case _ =>
         end check
       end checker