Exclude caps consumed in paths in checkUse

Author: bracevac

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

@@ -559,6 +559,62 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser:
           sepApplyError(fn, parts, arg, app)
   end checkApply
 
+  /** Compute the set of capabilities that are consumed along a selection path.
+   *  For example, if we have the path `a.b` where `b` is a consume field with type `B^{x}`,
+   *  this returns the actual consumed capabilities `{x}` from the type's capture set.
+   *
+   *  This walks the path and for each consume field encountered, collects the capabilities
+   *  from that field's widened type's capture set.
+   *
+   *  @param cap  The capability to analyze (e.g., `a.b`)
+   *  @return     The set of actual consumed capabilities from all consume fields along the path
+   */
+  def consumedByPath(cap: Capability)(using Context): Refs = cap match
+    case ref: TermRef =>
+      def recur(tp: Type, acc: Refs): Refs = tp match
+        case ref: TermRef =>
+          // This is a selection like a.b, or just a reference like a
+          val fieldSym = ref.symbol
+          val accWithCurrent =
+            if fieldSym.exists && fieldSym.isConsumeParam then
+              // This field is a consume parameter. Collect capabilities from its type's capture set.
+              acc ++ ref.widen.captureSet.elems
+            else
+              acc
+          // Also check if the current reference's type has consume fields
+          val accWithConsumeFields = accWithCurrent ++ capsFromConsumeFields(ref)
+          // Recurse on the prefix if it's a selection
+          if ref.prefix ne NoPrefix then
+            recur(ref.prefix, accWithConsumeFields)
+          else
+            accWithConsumeFields
+        case _ =>
+          acc
+
+      def capsFromConsumeFields(ref: TermRef): Refs =
+        // For types with consume fields, use the capture set of the reference itself
+        // and recursively check what those capabilities consume
+        val tpe = ref.widen.dealias
+        val cls = tpe.classSymbol
+        if cls.exists then
+          // Check if this class has any consume fields
+          val hasConsumeFields = cls.info.decls.exists(m => m.isConsumeParam && m.isTerm)
+          if hasConsumeFields then
+            // Use the capture set of the reference itself (e.g., {a} for holder.a : A^{a})
+            // Return both the capabilities in the capture set AND what they transitively consume
+            var result = ref.widen.captureSet.elems
+            for cap <- ref.widen.captureSet.elems do
+              result = result ++ consumedByPath(cap)
+            result
+          else
+            emptyRefs
+        else
+          emptyRefs
+
+      recur(ref, emptyRefs)
+    case _ =>
+      emptyRefs
+
   /** 1. Check that the capabilities used at `tree` don't overlap with
    *     capabilities hidden by a previous definition.
    *  2. Also check that none of the used capabilities was consumed before.
@@ -598,8 +654,15 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser:
       for ref <- used do
         val pos = consumed.clashing(ref)
         if pos != null then
-          // println(i"consumed so far ${consumed.refs.toList} with peaks ${consumed.directPeaks.toList}, used = $used, exposed = ${ref.directPeaks }")
-          consumeError(ref, pos, tree.srcPos)
+          // Check if this reference should be exempted because consume fields along
+          // the path own the consumed capabilities.
+          val pathConsumed = consumedByPath(ref)
+
+          // Check if any capability consumed by the path was consumed at position `pos`.
+          val shouldExempt = pathConsumed.exists(consumed.get(_) == pos)
+
+          if !shouldExempt then
+            consumeError(ref, pos, tree.srcPos)
   end checkUse
 
   /** If `tp` denotes some version of a singleton capability `x.type` the set `{x, x*}`

tests/neg-custom-args/captures/consume-in-constructor.check

@@ -1,5 +1,5 @@
--- Error: tests/neg-custom-args/captures/consume-in-constructor.scala:18:10 --------------------------------------------
-18 |  println(b) // error
+-- Error: tests/neg-custom-args/captures/consume-in-constructor.scala:20:10 --------------------------------------------
+20 |  println(b) // error
    |          ^
    |          Separation failure: Illegal access to {b} which is hidden by the previous definition
    |          of value a2 with type A2{val b: B^{b²}}^.
@@ -9,8 +9,8 @@
    |                    b   is a value in class A2
    |                    b²  is a value in method Test
    |                    cap is a fresh root capability created in value a2 when constructing instance A2
--- Error: tests/neg-custom-args/captures/consume-in-constructor.scala:19:10 --------------------------------------------
-19 |  println(a1) // error, since `b` was consumed before
+-- Error: tests/neg-custom-args/captures/consume-in-constructor.scala:21:10 --------------------------------------------
+21 |  println(a1) // error, since `b` was consumed before
    |          ^^
    |          Separation failure: Illegal access to {b} which is hidden by the previous definition
    |          of value a2 with type A2{val b: B^{b²}}^.
@@ -20,8 +20,8 @@
    |                    b   is a value in class A2
    |                    b²  is a value in method Test
    |                    cap is a fresh root capability created in value a2 when constructing instance A2
--- Error: tests/neg-custom-args/captures/consume-in-constructor.scala:25:10 --------------------------------------------
-25 |  println(b) // error, b is hidden in the type of a1
+-- Error: tests/neg-custom-args/captures/consume-in-constructor.scala:28:10 --------------------------------------------
+28 |  println(b) // error, b is hidden in the type of a1
    |          ^
    |          Separation failure: Illegal access to {b} which is hidden by the previous definition
    |          of value a1 with type A1^.

tests/neg-custom-args/captures/consume-in-constructor.scala

@@ -1,3 +1,5 @@
+import language.experimental.captureChecking
+import language.experimental.separationChecking
 import caps.cap
 
 class B
@@ -18,6 +20,7 @@ def Test =
   println(b) // error
   println(a1) // error, since `b` was consumed before
   println(a2) // OK since b belongs to a2
+  println(a2.b) // OK since b belongs to a2
 
 def Test2 =
   val b: B^ = B()