Rely on hidden sets for use checking

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

@@ -26,6 +26,7 @@ import reporting.{trace, Message, OverrideError}
 import Annotations.Annotation
 import Capabilities.*
 import dotty.tools.dotc.cc.CaptureSet.MutAdaptFailure
+import dotty.tools.dotc.util.common.alwaysTrue
 
 /** The capture checker */
 object CheckCaptures:
@@ -253,8 +254,12 @@ class CheckCaptures extends Recheck, SymTransformer:
      */
     private val sepCheckFormals = util.EqHashMap[Tree, Type]()
 
-    /** The references used at identifier or application trees */
-    private val usedSet = util.EqHashMap[Tree, CaptureSet]()
+    /** The references used at identifier or application trees, including the
+     *  environment at the reference point.
+     */
+    private val useInfos = mutable.ArrayBuffer[(Tree, CaptureSet, Env)]()
+
+    private var usedSet = util.EqHashMap[Tree, CaptureSet]()
 
     /** The set of symbols that were rechecked via a completer */
     private val completed = new mutable.HashSet[Symbol]
@@ -273,7 +278,7 @@ class CheckCaptures extends Recheck, SymTransformer:
     extension [T <: Tree](tree: T)
       def needsSepCheck: Boolean = sepCheckFormals.contains(tree)
       def formalType: Type = sepCheckFormals.getOrElse(tree, NoType)
-      def markedFree = usedSet.getOrElse(tree, CaptureSet.empty)
+      def markedFree: CaptureSet = usedSet.getOrElse(tree, CaptureSet.empty)
 
     /** Instantiate capture set variables appearing contra-variantly to their
      *  upper approximation.
@@ -427,11 +432,13 @@ class CheckCaptures extends Recheck, SymTransformer:
       else
         i"\nof the enclosing ${owner.showLocated}"
 
-    /** Does the given environment belong to a method that is (a) nested in a term
+    /** Under deferredReaches:
+     *  Does the given environment belong to a method that is (a) nested in a term
      *  and (b) not the method of an anonymous function?
      */
     def isOfNestedMethod(env: Env | Null)(using Context) =
-      env != null
+      ccConfig.deferredReaches
+      && env != null
       && env.owner.is(Method)
       && env.owner.owner.isTerm
       && !env.owner.isAnonymousFunction
@@ -460,28 +467,17 @@ class CheckCaptures extends Recheck, SymTransformer:
             !sym.isContainedIn(env.owner)
         }
 
-      /** If capability `c` refers to a parameter that is not @use declared, report an error.
-       *  Exception under deferredReaches: If use comes from a nested closure, accept it.
-       */
-      def checkUseDeclared(c: Capability, env: Env, lastEnv: Env | Null) =
-        if lastEnv != null && env.nestedClosure.exists && env.nestedClosure == lastEnv.owner then
-          assert(ccConfig.deferredReaches) // access is from a nested closure under deferredReaches, so it's OK
-        else c.paramPathRoot match
-          case ref: NamedType if !ref.symbol.isUseParam =>
-            val what = if ref.isType then "Capture set parameter" else "Local reach capability"
-            report.error(
-              em"""$what $c leaks into capture scope of ${env.ownerString}.
-                  |To allow this, the ${ref.symbol} should be declared with a @use annotation""", tree.srcPos)
-          case _ =>
-
       /** Avoid locally defined capability by charging the underlying type
        *  (which may not be cap). This scheme applies only under the deferredReaches setting.
        */
       def avoidLocalCapability(c: Capability, env: Env, lastEnv: Env | Null): Unit =
         if c.isParamPath then
           c match
             case Reach(_) | _: TypeRef =>
-              checkUseDeclared(c, env, lastEnv)
+              val accessFromNestedClosure =
+                lastEnv != null && env.nestedClosure.exists && env.nestedClosure == lastEnv.owner
+              if !accessFromNestedClosure then
+                checkUseDeclared(c, tree.srcPos)
             case _ =>
         else
           val underlying = c match
@@ -499,32 +495,22 @@ class CheckCaptures extends Recheck, SymTransformer:
        *  parameter. This is the default.
        */
       def avoidLocalReachCapability(c: Capability, env: Env): Unit = c match
-        case Reach(c1) =>
-          if c1.isParamPath then
-            checkUseDeclared(c, env, null)
-          else
-            // When a reach capabilty x* where `x` is not a parameter goes out
-            // of scope, we need to continue with `x`'s underlying deep capture set.
-            // It is an error if that set contains cap.
-            // The same is not an issue for normal capabilities since in a local
-            // definition `val x = e`, the capabilities of `e` have already been charged.
-            // Note: It's not true that the underlying capture set of a reach capability
-            // is always cap. Reach capabilities over paths depend on the prefix, which
-            // might turn a cap into something else.
-            // The path-use.scala neg test contains an example.
-            val underlying = CaptureSet.ofTypeDeeply(c1.widen)
-            capt.println(i"Widen reach $c to $underlying in ${env.owner}")
-            if sepChecksEnabled then
-              recur(underlying.filter(!_.isTerminalCapability), env, null)
-                // we don't want to disallow underlying Fresh instances, since these are typically locally created
-                // fresh capabilities. We don't need to also follow the hidden set since separation
-                // checking makes ure that locally hidden references need to go to @consume parameters.
-            else
-              underlying.disallowRootCapability(ctx.owner): () =>
-                report.error(em"Local reach capability $c leaks into capture scope of ${env.ownerString}", tree.srcPos)
-              recur(underlying, env, null)
-        case c: TypeRef if c.isParamPath =>
-          checkUseDeclared(c, env, null)
+        case Reach(c1) if !c1.isParamPath =>
+          // Parameter reaches are rejected in checkEscapingUses.
+          // When a reach capabilty x* where `x` is not a parameter goes out
+          // of scope, we need to continue with `x`'s underlying deep capture set.
+          // It is an error if that set contains cap.
+          // The same is not an issue for normal capabilities since in a local
+          // definition `val x = e`, the capabilities of `e` have already been charged.
+          // Note: It's not true that the underlying capture set of a reach capability
+          // is always cap. Reach capabilities over paths depend on the prefix, which
+          // might turn a cap into something else.
+          // The path-use.scala neg test contains an example.
+          val underlying = CaptureSet.ofTypeDeeply(c1.widen)
+          capt.println(i"Widen reach $c to $underlying in ${env.owner}")
+          recur(underlying.filter(!_.isTerminalCapability), env, null)
+            // we don't want to disallow underlying Fresh instances, since these are typically locally created
+            // fresh capabilities. We do check that they hide no parameter reach caps in checkEscapingUses
         case _ =>
 
       def recur(cs: CaptureSet, env: Env, lastEnv: Env | Null): Unit =
@@ -542,13 +528,26 @@ class CheckCaptures extends Recheck, SymTransformer:
           capt.println(i"Include call or box capture $included from $cs in ${env.owner} --> ${env.captured}")
           if !isOfNestedMethod(env) then
             recur(included, nextEnvToCharge(env, !_.owner.isStaticOwner), env)
-          // Don't propagate out of methods inside terms. The use set of these methods
-          // will be charged when that method is called.
+          	// Under deferredReaches, don't propagate out of methods inside terms.
+          	// The use set of these methods will be charged when that method is called.
 
       recur(cs, curEnv, null)
-      usedSet(tree) = tree.markedFree ++ cs
+      useInfos += ((tree, cs, curEnv))
     end markFree
 
+    /** If capability `c` refers to a parameter that is not @use declared, report an error.
+     */
+    def checkUseDeclared(c: Capability, pos: SrcPos)(using Context): Unit =
+      c.paramPathRoot match
+        case ref: NamedType if !ref.symbol.isUseParam =>
+          val what = if ref.isType then "Capture set parameter" else "Local reach capability"
+          val owner = ref.symbol.owner
+          val ownerStr = if owner.isAnonymousFunction then "enclosing function" else owner.show
+          report.error(
+            em"""$what $c leaks into capture scope of $ownerStr.
+                |To allow this, the ${ref.symbol} should be declared with a @use annotation""", pos)
+        case _ =>
+
     /** Include references captured by the called method in the current environment stack */
     def includeCallCaptures(sym: Symbol, resType: Type, tree: Tree)(using Context): Unit = resType match
       case _: MethodOrPoly => // wait until method is fully applied
@@ -1990,6 +1989,48 @@ class CheckCaptures extends Recheck, SymTransformer:
               traverseChildren(t)
       check.traverse(tp)
 
+    /** Check that no uses refer to reach capabilities of parameters of enclosing
+     *  methods or classes.
+     */
+    def checkEscapingUses()(using Context) =
+      for (tree, uses, env) <- useInfos do
+        val seen = util.EqHashSet[Capability]()
+
+        // The owner of the innermost environment of kind Boxed
+        def boxedOwner(env: Env): Symbol =
+          if env.kind == EnvKind.Boxed then env.owner
+          else if isOfNestedMethod(env) then env.owner.owner
+          else if env.owner.isStaticOwner then NoSymbol
+          else boxedOwner(nextEnvToCharge(env, alwaysTrue))
+
+        def checkUseUnlessBoxed(c: Capability, croot: NamedType) =
+          if !boxedOwner(env).isContainedIn(croot.symbol.owner) then
+            checkUseDeclared(c, tree.srcPos)
+
+        def check(cs: CaptureSet): Unit = cs.elems.foreach(checkElem)
+
+        def checkElem(c: Capability): Unit =
+          if !seen.contains(c) then
+            seen += c
+            c match
+              case Reach(c1) =>
+                c1.paramPathRoot match
+                  case croot: NamedType => checkUseUnlessBoxed(c, croot)
+                  case _ => check(CaptureSet.ofTypeDeeply(c1.widen))
+              case c: TypeRef =>
+                c.paramPathRoot match
+                  case croot: NamedType => checkUseUnlessBoxed(c, croot)
+                  case _ =>
+              case c: DerivedCapability =>
+                checkElem(c.underlying)
+              case c: FreshCap =>
+                check(c.hiddenSet)
+              case _ =>
+
+        check(uses)
+      end for
+    end checkEscapingUses
+
     /** Check that arguments of TypeApplys and AppliedTypes conform to their bounds.
      */
     def postCheck(unit: tpd.Tree)(using Context): Unit =
@@ -2018,7 +2059,11 @@ class CheckCaptures extends Recheck, SymTransformer:
       end checker
 
       checker.traverse(unit)(using ctx.withOwner(defn.RootClass))
-      if sepChecksEnabled then SepCheck(this).traverse(unit)
+      checkEscapingUses()
+      if sepChecksEnabled then
+        for (tree, cs, env) <- useInfos do
+          usedSet(tree) = tree.markedFree ++ cs
+        SepCheck(this).traverse(unit)
       if !ctx.reporter.errorsReported then
         // We dont report errors here if previous errors were reported, because other
         // errors often result in bad applied types, but flagging these bad types gives

tests/neg-custom-args/captures/dcs-tvar.check

@@ -1,10 +1,14 @@
--- Error: tests/neg-custom-args/captures/dcs-tvar.scala:6:15 -----------------------------------------------------------
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/dcs-tvar.scala:6:2 ---------------------------------------
 6 |  () => runOps(xs) // error
-  |               ^^
-  |               Local reach capability xs* leaks into capture scope of method f.
-  |               To allow this, the parameter xs should be declared with a @use annotation
--- Error: tests/neg-custom-args/captures/dcs-tvar.scala:9:15 -----------------------------------------------------------
+  |  ^^^^^^^^^^^^^^^^
+  |  Found:    () ->{xs*} Unit
+  |  Required: () -> Unit
+  |
+  | longer explanation available when compiling with `-explain`
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/dcs-tvar.scala:9:2 ---------------------------------------
 9 |  () => runOps(xs) // error
-  |               ^^
-  |               Local reach capability xs* leaks into capture scope of method g.
-  |               To allow this, the parameter xs should be declared with a @use annotation
+  |  ^^^^^^^^^^^^^^^^
+  |  Found:    () ->{xs*} Unit
+  |  Required: () -> Unit
+  |
+  | longer explanation available when compiling with `-explain`

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

@@ -1,12 +1,25 @@
--- Error: tests/neg-custom-args/captures/delayedRunops.scala:17:13 -----------------------------------------------------
-17 |      runOps(ops1)  // error
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/delayedRunops.scala:15:4 ---------------------------------
+15 |    () => // error
+   |    ^
+   |    Found:    () ->{ops*} Unit
+   |    Required: () -> Unit
+16 |      val ops1 = ops
+17 |      runOps(ops1)
+   |
+   | longer explanation available when compiling with `-explain`
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/delayedRunops.scala:27:4 ---------------------------------
+27 |    () => // error
+   |    ^
+   |    Found:    () ->{ops*} Unit
+   |    Required: () -> Unit
+28 |      val ops1: List[() ->{ops*} Unit] = ops
+29 |      runOps(ops1)
+   |
+   | longer explanation available when compiling with `-explain`
+-- Error: tests/neg-custom-args/captures/delayedRunops.scala:23:13 -----------------------------------------------------
+23 |      runOps(ops1)  // error
    |             ^^^^
-   |             Local reach capability ops* leaks into capture scope of method delayedRunOps1.
-   |             To allow this, the parameter ops should be declared with a @use annotation
--- Error: tests/neg-custom-args/captures/delayedRunops.scala:29:13 -----------------------------------------------------
-29 |      runOps(ops1)  // error
-   |             ^^^^
-   |             Local reach capability ops* leaks into capture scope of method delayedRunOps3.
+   |             Local reach capability ops* leaks into capture scope of method delayedRunOps2.
    |             To allow this, the parameter ops should be declared with a @use annotation
 -- Error: tests/neg-custom-args/captures/delayedRunops.scala:22:16 -----------------------------------------------------
 22 |      val ops1: List[() => Unit] = ops // error

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

@@ -12,18 +12,18 @@ import caps.{use, consume}
 
   // unsound: impure operation pretended pure
   def delayedRunOps1(ops: List[() => Unit]): () ->{} Unit =
-    () =>
+    () => // error
       val ops1 = ops
-      runOps(ops1)  // error
+      runOps(ops1)
 
   // unsound: impure operation pretended pure
   def delayedRunOps2(@consume ops: List[() => Unit]): () ->{} Unit =
     () =>
       val ops1: List[() => Unit] = ops // error
-      runOps(ops1)  // was error
+      runOps(ops1)  // error
 
   // unsound: impure operation pretended pure
   def delayedRunOps3(ops: List[() => Unit]): () ->{} Unit =
-    () =>
+    () => // error
       val ops1: List[() ->{ops*} Unit] = ops
-      runOps(ops1)  // error
+      runOps(ops1)

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

@@ -3,6 +3,11 @@
    |           ^^^^^^^
    |           Local reach capability x.unbox* leaks into capture scope of method foo.
    |           To allow this, the parameter x should be declared with a @use annotation
+-- Error: tests/neg-custom-args/captures/i21442.scala:18:14 ------------------------------------------------------------
+18 |  val io = x1.unbox // error
+   |           ^^^^^^^^
+   |           Local reach capability x* leaks into capture scope of method bar.
+   |           To allow this, the parameter x should be declared with a @use annotation
 -- Error: tests/neg-custom-args/captures/i21442.scala:17:10 ------------------------------------------------------------
 17 |  val x1: Boxed[IO^] = x // error
    |          ^^^^^^^^^^

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

@@ -15,5 +15,5 @@ def foo(x: Boxed[IO^]): Unit =
 // But, no type error reported.
 def bar(x: Boxed[IO^]): Unit =
   val x1: Boxed[IO^] = x // error
-  val io = x1.unbox // was error
+  val io = x1.unbox // error
   io.use()

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

@@ -0,0 +1,20 @@
+-- Error: tests/neg-custom-args/captures/localReaches.scala:24:30 ------------------------------------------------------
+24 |  var x: () ->{xs*} Unit = ys.head // error
+   |                           ^^^^^^^
+   |                           Local reach capability ops* leaks into capture scope of method localReach3.
+   |                           To allow this, the parameter ops should be declared with a @use annotation
+-- Error: tests/neg-custom-args/captures/localReaches.scala:27:11 ------------------------------------------------------
+27 |    x = ys.head  // error
+   |        ^^^^^^^
+   |        Local reach capability ops* leaks into capture scope of method localReach3.
+   |        To allow this, the parameter ops should be declared with a @use annotation
+-- Error: tests/neg-custom-args/captures/localReaches.scala:14:10 ------------------------------------------------------
+14 |  val xs: List[() => Unit] = op :: Nil // error
+   |          ^^^^^^^^^^^^^^^^
+   |          Separation failure: value xs's type List[() => Unit] hides parameter op.
+   |          The parameter needs to be annotated with @consume to allow this.
+-- Error: tests/neg-custom-args/captures/localReaches.scala:22:10 ------------------------------------------------------
+22 |  val xs: List[() => Unit] = ops // error
+   |          ^^^^^^^^^^^^^^^^
+   |          Separation failure: value xs's type List[() => Unit] hides parameter ops.
+   |          The parameter needs to be annotated with @consume to allow this.

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

@@ -0,0 +1,28 @@
+import language.experimental.captureChecking
+// no separation checking
+import caps.consume
+
+def localReach() =
+  val xs: List[() => Unit] = ???
+  var ys: List[() ->{xs*} Unit] = xs
+  var x: () ->{xs*} Unit = ys.head
+  while ys.nonEmpty do
+    ys = ys.tail
+    x = ys.head
+
+def localReach2(op: () => Unit) =
+  val xs: List[() => Unit] = op :: Nil // error
+  var ys: List[() ->{xs*} Unit] = xs
+  var x: () ->{xs*} Unit = ys.head
+  while ys.nonEmpty do
+    ys = ys.tail
+    x = ys.head
+
+def localReach3(ops: List[() => Unit]) =
+  val xs: List[() => Unit] = ops // error
+  var ys: List[() ->{xs*} Unit] = xs
+  var x: () ->{xs*} Unit = ys.head // error
+  while ys.nonEmpty do
+    ys = ys.tail
+    x = ys.head  // error
+

tests/neg-custom-args/captures/method-uses.scala

@@ -2,9 +2,9 @@ def test(xs: List[() => Unit]) =
   xs.head // error
 
   def foo =
-    xs.head // ok
+    xs.head // error, ok under deferredReaches
   def bar() =
-    xs.head // ok
+    xs.head // error, ok under deferredReaches
 
   class Foo:
     println(xs.head) // error, but could be OK
@@ -14,7 +14,7 @@ def test(xs: List[() => Unit]) =
   Foo() // OK, but could be error
 
 def test2(xs: List[() => Unit]) =
-  def foo = xs.head // ok
+  def foo = xs.head // error, ok under deferredReaches
   ()
 
 def test3(xs: List[() => Unit]): () ->{xs*} Unit = () =>