Rely on hidden sets for use checking

Two changes:

 1. We don't distinguish anymore according to separation checking in markFree.
    We use the same logic regardless of this option. This improves expressiveness
    because we now admit local reach capabilities that do not refer to parameters.
    Previously, these were only admitted under separation checking, which is a
    severe loss of expressiveness.
 2. We do trace hidden sets to check that a local reach capability does not refer
    indirectly through a fresh to a parameter reach. This has to be done after
    regular capture checking, since hidden sets need to be completely known.
    This fixes a soundness hole that would have opened once we add `cap.only[Sharable]`
    capabilities which escape separation checking.

Fixes #23579

Author: odersky

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]
@@ -270,7 +275,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.
@@ -459,28 +464,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
@@ -498,32 +492,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 ccConfig.useSepChecks 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 =
@@ -539,15 +523,28 @@ class CheckCaptures extends Recheck, SymTransformer:
             isVisible
           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) || true then
+          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
@@ -1988,6 +1985,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 =
@@ -2016,7 +2055,11 @@ class CheckCaptures extends Recheck, SymTransformer:
       end checker
 
       checker.traverse(unit)(using ctx.withOwner(defn.RootClass))
-      if ccConfig.useSepChecks then SepCheck(this).traverse(unit)
+      checkEscapingUses()
+      if ccConfig.useSepChecks 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/reaches.check

@@ -90,11 +90,16 @@
 72 |    f1
    |
    | longer explanation available when compiling with `-explain`
--- Error: tests/neg-custom-args/captures/reaches.scala:88:10 -----------------------------------------------------------
+-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/reaches.scala:88:10 --------------------------------------
 88 |  ps.map((x, y) => compose1(x, y)) // error
-   |          ^
-   |          Local reach capability ps* leaks into capture scope of method mapCompose.
-   |          To allow this, the parameter ps should be declared with a @use annotation
+   |          ^^^^^^^^^^^^^^^^^^^^^^^
+   |Found:    (x$1: (A^ ->? A^?, A^ ->? A^?)^?) ->? A^? ->? A^?
+   |Required: ((A ->{ps*} A, A ->{ps*} A)) => A^? ->? A^?
+   |
+   |where:    => refers to a fresh root capability created in method mapCompose when checking argument to parameter f of method map
+   |          ^  refers to the universal root capability
+   |
+   | longer explanation available when compiling with `-explain`
 -- [E007] Type Mismatch Error: tests/neg-custom-args/captures/reaches.scala:91:10 --------------------------------------
 91 |  ps.map((x, y) => compose1(x, y)) // error
    |          ^^^^^^^^^^^^^^^^^^^^^^^
@@ -105,3 +110,8 @@
    |          ^  refers to the universal root capability
    |
    | longer explanation available when compiling with `-explain`
+-- Error: tests/neg-custom-args/captures/reaches.scala:39:31 -----------------------------------------------------------
+39 |    val next: () => Unit = cur.head   // error
+   |                           ^^^^^^^^
+   |                           Local reach capability xs* leaks into capture scope of method runAll2.
+   |                           To allow this, the parameter xs should be declared with a @use annotation

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

@@ -36,7 +36,7 @@ def runAll1(@use xs: List[Proc]): Unit =
 def runAll2(@consume xs: List[Proc]): Unit =
   var cur: List[Proc] = xs
   while cur.nonEmpty do
-    val next: () => Unit = cur.head   // was error, now OK
+    val next: () => Unit = cur.head   // error
     next()
     cur = cur.tail