Switch level checking for capsets to owner-based scheme

The previous scheme was too coarse since it treated all vaks in a method the same.

Author: odersky

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

@@ -484,6 +484,12 @@ object Capabilities:
       case self: FreshCap => self.hiddenSet.owner
       case _ /* : GlobalCap | ResultCap | ParamRef */ => NoSymbol
 
+    final def visibility(using Context): Symbol = this match
+      case self: FreshCap => ccOwner.enclosingMethodOrClass
+      case _ =>
+        val vis = ccOwner
+        if vis.is(Param) then vis.owner else vis
+
     /** The symbol that represents the level closest-enclosing ccOwner.
      *  Symbols representing levels are
      *   - class symbols, but not inner (non-static) module classes

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

@@ -660,7 +660,7 @@ object CaptureSet:
 
   /** If true emit info when var with id debugTarget is created or gets a new element */
   inline val debugVars = false
-  inline val debugTarget = 22
+  inline val debugTarget = 1745
 
   /** The subclass of captureset variables with given initial elements */
   class Var(initialOwner: Symbol = NoSymbol, initialElems: Refs = emptyRefs, val level: Level = undefinedLevel, underBox: Boolean = false)(using /*@constructorOnly*/ ictx: Context) extends CaptureSet:
@@ -690,6 +690,7 @@ object CaptureSet:
 
     if debugVars && id == debugTarget then
       println(i"###INIT ELEMS of $id to $initialElems")
+      assert(false)
 
     def elems: Refs = myElems
     def elems_=(refs: Refs): Unit =
@@ -832,7 +833,7 @@ object CaptureSet:
             case _ => foldOver(b, t)
       find(false, binder)
 
-    def levelOK(elem: Capability)(using Context): Boolean = elem match
+    def levelOKold(elem: Capability)(using Context): Boolean = elem match
       case _: FreshCap =>
         !level.isDefined
         || ccState.symLevel(elem.ccOwner) <= level
@@ -865,6 +866,29 @@ object CaptureSet:
       case _ =>
         true
 
+    def levelOKnew(elem: Capability)(using Context): Boolean = elem match
+      case elem @ ResultCap(binder) =>
+        rootLimit == null && (this.isInstanceOf[BiMapped] || isPartOf(binder.resType))
+      case GlobalCap =>
+        rootLimit == null
+      case elem: ParamRef =>
+        this.isInstanceOf[BiMapped] || isPartOf(elem.binder.resType)
+      case _ =>
+        if owner.exists then
+          val elemVis = elem.visibility
+          !elemVis.isProperlyContainedIn(owner)
+        else true
+
+    inline val debugLevelChecking = false
+
+    def levelOK(elem: Capability)(using Context): Boolean =
+      val now = levelOKnew(elem)
+      if debugLevelChecking then
+        val was = levelOKold(elem)
+        if was != now then
+          println(i"LEVEL DIFF for $this / $getClass in ${owner.ownersIterator.toList} and elem $elem in ${elem.ccOwner}, was $was")
+      now
+
     def addDependent(cs: CaptureSet)(using Context, VarState): Boolean =
       (cs eq this)
       || cs.isUniversal

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

@@ -28,6 +28,7 @@ import reporting.{trace, Message, OverrideError}
 import Annotations.Annotation
 import Capabilities.*
 import util.common.alwaysTrue
+import scala.annotation.constructorOnly
 
 /** The capture checker */
 object CheckCaptures:
@@ -56,7 +57,13 @@ object CheckCaptures:
       kind: EnvKind,
       captured: CaptureSet,
       outer0: Env | Null,
-      nestedClosure: Symbol = NoSymbol):
+      nestedClosure: Symbol = NoSymbol)(using @constructorOnly ictx: Context):
+
+    assert(definesEnv(owner))
+    captured match
+      case captured: CaptureSet.Var => assert(captured.owner == owner,
+        i"owner discrepancy env owner = $owner but its captureset $captured has owner ${captured.owner}")
+      case _ =>
 
     def outer = outer0.nn
 
@@ -71,6 +78,9 @@ object CheckCaptures:
         res
   end Env
 
+  def definesEnv(sym: Symbol)(using Context): Boolean =
+    sym.is(Method) || sym.isClass
+
   /** Similar normal substParams, but this is an approximating type map that
    *  maps parameters in contravariant capture sets to the empty set.
    */
@@ -364,21 +374,28 @@ class CheckCaptures extends Recheck, SymTransformer:
       assert(cs1.subCaptures(cs2), i"$cs1 is not a subset of $cs2")
 
     /** If `res` is not CompareResult.OK, report an error */
-    def checkOK(res: TypeComparer.CompareResult, prefix: => String, added: Capability | CaptureSet, target: CaptureSet, pos: SrcPos, provenance: => String = "")(using Context): Unit =
+    def checkOK(res: TypeComparer.CompareResult,
+        prefix: => String,
+        added: Capability | CaptureSet,
+        target: CaptureSet,
+        pos: SrcPos,
+        provenance: => String = "")(using Context): Unit =
       res match
         case TypeComparer.CompareResult.Fail(notes) =>
-          val ((res: IncludeFailure) :: Nil, otherNotes) =
-            notes.partition(_.isInstanceOf[IncludeFailure]): @unchecked
+          val (includeFailures, otherNotes) = notes.partition(_.isInstanceOf[IncludeFailure])
+          val realTarget = includeFailures match
+            case (fail: IncludeFailure) :: _ => fail.cs
+            case _ => target
           def msg(provisional: Boolean) =
             def toAdd: String = errorNotes(otherNotes).toAdd.mkString
             def descr: String =
-              val d = res.cs.description
+              val d = realTarget.description
               if d.isEmpty then provenance else ""
             def kind = if provisional then "previously estimated\n" else "allowed "
-            em"$prefix included in the ${kind}capture set ${res.cs}$descr$toAdd"
+            em"$prefix included in the ${kind}capture set $realTarget$descr$toAdd"
           target match
             case target: CaptureSet.Var
-            if res.cs.isProvisionallySolved =>
+            if realTarget.isProvisionallySolved =>
               report.warning(
                 msg(provisional = true)
                   .prepend(i"Another capture checking run needs to be scheduled because\n"),
@@ -413,7 +430,7 @@ class CheckCaptures extends Recheck, SymTransformer:
     def capturedVars(sym: Symbol)(using Context): CaptureSet =
       myCapturedVars.getOrElseUpdate(sym,
         if sym.isTerm || !sym.owner.isStaticOwner
-        then CaptureSet.Var(sym.owner, level = ccState.symLevel(sym))
+        then CaptureSet.Var(sym, level = ccState.symLevel(sym))
         else CaptureSet.empty)
 
 // ---- Record Uses with MarkFree ----------------------------------------------------
@@ -535,6 +552,7 @@ class CheckCaptures extends Recheck, SymTransformer:
               then avoidLocalCapability(c, env, lastEnv)
               else avoidLocalReachCapability(c, env)
             isVisible
+          //println(i"Include call or box capture $included from $cs in ${env.owner}/${env.captured}/${env.captured.owner}/${env.kind}")
           checkSubset(included, env.captured, tree.srcPos, provenance(env))
           capt.println(i"Include call or box capture $included from $cs in ${env.owner} --> ${env.captured}")
           if !isOfNestedMethod(env) then
@@ -1151,11 +1169,13 @@ class CheckCaptures extends Recheck, SymTransformer:
           .map(e => (e.owner, e))
           .toMap
         def restoreEnvFor(sym: Symbol): Env =
-          val localSet = capturedVars(sym)
-          if localSet eq CaptureSet.empty then rootEnv
-          else envForOwner.get(sym) match
-            case Some(e) => e
-            case None => Env(sym, EnvKind.Regular, localSet, restoreEnvFor(sym.owner))
+          if definesEnv(sym) then
+            val localSet = capturedVars(sym)
+            if localSet eq CaptureSet.empty then rootEnv
+            else envForOwner.get(sym) match
+              case Some(e) => e
+              case None => Env(sym, EnvKind.Regular, localSet, restoreEnvFor(sym.owner))
+          else restoreEnvFor(sym.owner)
         curEnv = restoreEnvFor(sym.owner)
         capt.println(i"Complete $sym in ${curEnv.outersIterator.toList.map(_.owner)}")
         try recheckDef(tree, sym)

tests/neg-custom-args/captures/boundary.check

@@ -12,7 +12,7 @@
    |          cap  is a fresh root capability classified as Control created in value local when constructing Capability instance scala.util.boundary.Label[Object^'s1]
    |          cap² is the universal root capability
  6 |      boundary[Unit]: l2 ?=>
- 7 |        boundary.break(l2)(using l1)
+ 7 |        boundary.break(l2)(using l1) // error
  8 |      ???
    |--------------------------------------------------------------------------------------------------------------------
    |Inline stack trace
@@ -23,6 +23,21 @@
     --------------------------------------------------------------------------------------------------------------------
    |
    | longer explanation available when compiling with `-explain`
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/boundary.scala:7:33 --------------------------------------
+7 |        boundary.break(l2)(using l1) // error
+  |                                 ^^
+  |Found:    (local : scala.util.boundary.Label[Object^])
+  |Required: scala.util.boundary.Label[scala.util.boundary.Label[Unit]^²]^³
+  |
+  |Note that capability cap is not included in capture set {cap²}.
+  |
+  |where:    ^    refers to the universal root capability
+  |          ^²   refers to a fresh root capability classified as Control in the type of value local²
+  |          ^³   refers to a fresh root capability classified as Control created in package <empty> when checking argument to parameter label of method break
+  |          cap  is a fresh root capability classified as Control in the type of value local
+  |          cap² is a fresh root capability classified as Control created in package <empty> when checking argument to parameter label of method break
+  |
+  | longer explanation available when compiling with `-explain`
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/boundary.scala:5:4 ---------------------------------------
  4 |  boundary[AnyRef^]:
  5 |    l1 ?=> // error // error
@@ -37,7 +52,7 @@
    |            cap  is a fresh root capability created in package <empty>
    |            cap² is the universal root capability
  6 |      boundary[Unit]: l2 ?=>
- 7 |        boundary.break(l2)(using l1)
+ 7 |        boundary.break(l2)(using l1) // error
  8 |      ???
    |--------------------------------------------------------------------------------------------------------------------
    |Inline stack trace

tests/neg-custom-args/captures/boundary.scala

@@ -4,5 +4,5 @@ object test:
   boundary[AnyRef^]:
     l1 ?=> // error // error
       boundary[Unit]: l2 ?=>
-        boundary.break(l2)(using l1)
+        boundary.break(l2)(using l1) // error
       ???

tests/neg-custom-args/captures/branding.scala

@@ -22,14 +22,14 @@ def main() =
   val untrustedLogger: Logger^ = ???
   val untrustedChannel: Channel[String]^ = ???
 
-  runSecure: () =>
+  runSecure: () => // error (???, arose after changing level checking)
     trustedLogger.log("Hello from trusted code") // ok
 
-  runSecure: () =>
+  runSecure: () => // error (???, arose after changing level checking)
     trustedChannel.send("I can send")
     trustedLogger.log(trustedChannel.recv()) // ok
 
-  runSecure: () =>
+  runSecure: () => // error (???, arose after changing level checking)
     "I am pure"                             // ok
 
   runSecure: () => // error

tests/neg-custom-args/captures/capset-members4.scala

@@ -11,8 +11,8 @@ def test =
     type C^ >: {z,x} <: {x,y,z}
 
   val foo: Foo = ???
-  onlyWithZ[{foo.C}]
-  onlyWithZ[{z}]
-  onlyWithZ[{x,z}]
-  onlyWithZ[{x,y,z}]
-  onlyWithZ[{x,y}] // error
+  onlyWithZ[{foo.C}] // error
+  onlyWithZ[{z}]     // error
+  onlyWithZ[{x,z}]   // error
+  onlyWithZ[{x,y,z}] // error
+  onlyWithZ[{x,y}]   // error

tests/neg-custom-args/captures/i15772.check

@@ -1,8 +1,8 @@
 -- Error: tests/neg-custom-args/captures/i15772.scala:22:46 ------------------------------------------------------------
 22 |    val boxed1 : ((C^) => Unit) -> Unit = box1(c)  // error
    |                                          ^^^^^^^
-   |C^ => Unit cannot be box-converted to C{val arg: C^²}^{c} ->{cap, c} Unit
-   |since the additional capture set {c} resulting from box conversion is not allowed in C{val arg: C^²}^{c} => Unit
+   |C^ => Unit cannot be box-converted to C{val arg: C^²}^{c} ->{cap, x} Unit
+   |since the additional capture set {x} resulting from box conversion is not allowed in C{val arg: C^²}^{c} => Unit
    |
    |where:    =>  refers to the universal root capability
    |          ^   refers to the universal root capability
@@ -11,8 +11,8 @@
 -- Error: tests/neg-custom-args/captures/i15772.scala:29:35 ------------------------------------------------------------
 29 |    val boxed2 : Observe[C^] = box2(c)  // error
    |                               ^^^^^^^
-   |C^ => Unit cannot be box-converted to C{val arg: C^²}^{c} ->{cap, c} Unit
-   |since the additional capture set {c} resulting from box conversion is not allowed in C{val arg: C^²}^{c} => Unit
+   |C^ => Unit cannot be box-converted to C{val arg: C^²}^{c} ->{cap, x} Unit
+   |since the additional capture set {x} resulting from box conversion is not allowed in C{val arg: C^²}^{c} => Unit
    |
    |where:    =>  refers to the universal root capability
    |          ^   refers to the universal root capability

tests/neg-custom-args/captures/i15922.scala

@@ -13,6 +13,6 @@ def withCap[X](op: (Cap^) => X): X = {
 def leaking(c: Cap^): Id[Cap^{c}] = mkId(c)
 
 def test =
-  val ll = (c: Cap^) => leaking(c)
-  val bad1 = withCap(ll)       // error
+  val ll = (c: Cap^) => leaking(c)  // error
+  val bad1 = withCap(ll)
   val bad2 = withCap(leaking)  // error

tests/neg-custom-args/captures/i21614.check

@@ -1,5 +1,5 @@
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/i21614.scala:12:33 ---------------------------------------
-12 |  files.map((f: F) => new Logger(f)) // error, Q: can we make this pass (see #19076)?
+12 |  files.map((f: F) => new Logger(f)) // error // error, Q: can we make this pass (see #19076)?
    |                                 ^
    |Found:    (f : F)
    |Required: File^
@@ -11,16 +11,25 @@
    |          cap² is a fresh root capability classified as SharedCapability created in anonymous function of type (f²: F): Logger when checking argument to parameter f of constructor Logger
    |
    | longer explanation available when compiling with `-explain`
+-- Error: tests/neg-custom-args/captures/i21614.scala:12:8 -------------------------------------------------------------
+12 |  files.map((f: F) => new Logger(f)) // error // error, Q: can we make this pass (see #19076)?
+   |  ^^^^^^^^^
+   |Type variable U of method map cannot be instantiated to Logger{val f: File^'s1}^{cap.rd} since
+   |that type captures the root capability `cap`.
+   |This is often caused by a local capability in an argument of method map
+   |leaking as part of its result.
+   |
+   |where:    cap is a root capability associated with the result type of (f²: F^{files*}): Logger{val f: File^'s1}^'s2
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/i21614.scala:15:12 ---------------------------------------
 15 |  files.map(new Logger(_)) // error, Q: can we improve the error message?
    |            ^^^^^^^^^^^^^
-   |Found:    (_$1: File^'s1) ->{C} Logger{val f: File^{_$1}}^{cap.rd, _$1}
-   |Required: File^{C} => Logger{val f: File^'s2}^'s3
+   |Found:    (_$1: File^'s3) ->{C} Logger{val f: File^{_$1}}^{cap.rd, _$1}
+   |Required: File^{C} => Logger{val f: File^'s4}^'s5
    |
    |Note that capability C is not classified as trait SharedCapability, therefore it
-   |cannot be included in capture set 's1 of parameter _$1 of SharedCapability elements.
+   |cannot be included in capture set 's3 of parameter _$1 of SharedCapability elements.
    |
    |where:    =>  refers to a fresh root capability created in method mkLoggers2 when checking argument to parameter f of method map
-   |          cap is a root capability associated with the result type of (_$1: File^'s1): Logger{val f: File^{_$1}}^{cap.rd, _$1}
+   |          cap is a root capability associated with the result type of (_$1: File^'s3): Logger{val f: File^{_$1}}^{cap.rd, _$1}
    |
    | longer explanation available when compiling with `-explain`