Tighten consume checks

 1. Strip readonly modifier before checking o=for overlaps
 2. Don't reset consume to empty before entering defs

Author: odersky

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

@@ -482,6 +482,8 @@ extension (tp: Type)
       else tp.superType.derivesFromCapTrait(cls)
     case ReachCapability(tp1) =>
       tp1.widen.derivesFromCapTraitDeeply(cls)
+    case ReadOnlyCapability(tp1) =>
+      tp1.derivesFromCapTrait(cls)
     case tp: (TypeProxy & ValueType) =>
       tp.superType.derivesFromCapTrait(cls)
     case tp: AndType =>

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

@@ -164,13 +164,6 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser:
   /** The set of references that were consumed so far in the current method */
   private var consumed: MutConsumedSet = MutConsumedSet()
 
-  /** Run `op`` with a fresh, initially empty consumed set. */
-  private def withFreshConsumed(op: => Unit): Unit =
-    val saved = consumed
-    consumed = MutConsumedSet()
-    op
-    consumed = saved
-
   /** Infos aboput Labeled expressions enclosing the current traversal point.
    *  For each labeled expression, it's label name, and a list buffer containing
    *  all consumed sets of return expressions referring to that label.
@@ -499,7 +492,7 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser:
         else assert(!argDeps.isEmpty)
 
       if arg.needsSepCheck then
-        //println(i"testing $arg, ${argPeaks.actual}/${argPeaks.formal} against ${currentPeaks.actual}")
+        //println(i"testing $arg, formal = ${arg.formalType}, peaks = ${argPeaks.actual}/${argPeaks.hidden} against ${currentPeaks.actual}")
         checkType(arg.formalType, arg.srcPos, TypeRole.Argument(arg))
         // 2. test argPeaks.hidden against previously captured actuals
         if !argPeaks.hidden.sharedWith(currentPeaks.actual).isEmpty then
@@ -548,6 +541,7 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser:
   def checkUse(tree: Tree)(using Context): Unit =
     val used = tree.markedFree.elems
     if !used.isEmpty then
+      capt.println(i"check use $tree: $used")
       val usedPeaks = used.peaks
       val overlap = defsShadow.peaks.sharedWith(usedPeaks)
       if !defsShadow.peaks.sharedWith(usedPeaks).isEmpty then
@@ -569,7 +563,7 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser:
             sepUseError(tree, null, used, defsShadow)
 
       for ref <- used do
-        val pos = consumed.get(ref)
+        val pos = consumed.get(ref.stripReadOnly)
         if pos != null then consumeError(ref, pos, tree.srcPos)
   end checkUse
 
@@ -656,7 +650,7 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser:
       case _: TypeRole.Argument | _: TypeRole.Qualifier =>
         for ref <- refsToCheck do
           if !ref.derivesFromSharedCapability then
-            consumed.put(ref, pos)
+            consumed.put(ref.stripReadOnly, pos)
       case _ =>
   end checkConsumedRefs
 
@@ -913,7 +907,7 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser:
           checkValOrDefDef(tree)
         case tree: DefDef =>
           inSection:
-            withFreshConsumed:
+            consumed.segment:
               for params <- tree.paramss; case param: ValDef <- params do
                 pushDef(param, emptyRefs)
               traverseChildren(tree)
@@ -945,7 +939,7 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser:
           val caseConsumed = for cas <- cases yield consumed.segment(traverse(cas))
           caseConsumed.foreach(consumed ++= _)
         case tree: TypeDef if tree.symbol.isClass =>
-          withFreshConsumed:
+          consumed.segment:
             traverseChildren(tree)
         case tree: WhileDo =>
           val loopConsumed = consumed.segment(traverseChildren(tree))

tests/neg-custom-args/captures/sep-consume.check

@@ -0,0 +1,28 @@
+-- Error: tests/neg-custom-args/captures/sep-consume.scala:17:2 --------------------------------------------------------
+17 |  x.put(42)  // error
+   |  ^
+   |  Separation failure: Illegal access to (x : Ref^), which was passed to a
+   |  @consume parameter or was used as a prefix to a @consume method on line 16
+   |  and therefore is no longer available.
+-- Error: tests/neg-custom-args/captures/sep-consume.scala:18:2 --------------------------------------------------------
+18 |  x.get      // error
+   |  ^
+   |  Separation failure: Illegal access to x.rd, which was passed to a
+   |  @consume parameter or was used as a prefix to a @consume method on line 16
+   |  and therefore is no longer available.
+-- Error: tests/neg-custom-args/captures/sep-consume.scala:19:16 -------------------------------------------------------
+19 |  par(rx, () => x.put(42))  // error
+   |                ^
+   |                Separation failure: Illegal access to (x : Ref^), which was passed to a
+   |                @consume parameter or was used as a prefix to a @consume method on line 16
+   |                and therefore is no longer available.
+-- Error: tests/neg-custom-args/captures/sep-consume.scala:20:16 -------------------------------------------------------
+20 |  par(rx, () => x.get)  // error
+   |                ^
+   |                Separation failure: Illegal access to x.rd, which was passed to a
+   |                @consume parameter or was used as a prefix to a @consume method on line 16
+   |                and therefore is no longer available.
+-- Error: tests/neg-custom-args/captures/sep-consume.scala:24:16 -------------------------------------------------------
+24 |  def foo = bad(f) // error
+   |                ^
+   | Separation failure: argument to @consume parameter with type (f : () ->{x.rd} Unit) refers to non-local value f

tests/neg-custom-args/captures/sep-consume.scala

@@ -0,0 +1,26 @@
+import language.experimental.captureChecking
+import caps.*
+
+class Ref extends Mutable:
+  private var _data = 0
+  def get: Int = _data
+  mut def put(x: Int): Unit = _data = x
+
+// require f and g to be non-interfering
+def par(f: () => Unit, g: () => Unit): Unit = ???
+
+def bad(@consume op: () ->{cap.rd} Unit): () => Unit = op
+
+def test2(@consume x: Ref^): Unit =
+  val f: () ->{x.rd} Unit = () => x.get
+  val rx: () => Unit = bad(f)  // hides x.rd in the resulting `cap`
+  x.put(42)  // error
+  x.get      // error
+  par(rx, () => x.put(42))  // error
+  par(rx, () => x.get)  // error
+
+def test3(@consume x: Ref^): Unit =
+  val f: () ->{x.rd} Unit = () => x.get
+  def foo = bad(f) // error
+  foo()
+  foo()

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

@@ -8,3 +8,9 @@
    |             ^^
    |             Separation failure: argument to @consume parameter with type (io : Object^) refers to parameter io.
    |             The parameter needs to be annotated with @consume to allow this.
+-- Error: tests/neg-custom-args/captures/sepchecks5.scala:20:24 --------------------------------------------------------
+20 |  par(f2)(() => println(io))  // error
+   |                        ^^
+   |                        Separation failure: Illegal access to (io : Object^), which was passed to a
+   |                        @consume parameter or was used as a prefix to a @consume method on line 19
+   |                        and therefore is no longer available.

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

@@ -17,5 +17,5 @@ def test(io: Object^): Unit =
   par(f1)(() => println(io))  // !!! separation failure
 
   val f2 = g(io)              // error
-  par(f2)(() => println(io))  // !!! separation failure
+  par(f2)(() => println(io))  // error