Make sure fresh results of methods only hide local refs

Author: odersky

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

@@ -281,7 +281,7 @@ extension (tp: Type)
 
   /** The first element of this path type */
   final def pathRoot(using Context): Type = tp.dealias match
-    case tp1: NamedType if tp1.symbol.owner.isClass => tp1.prefix.pathRoot
+    case tp1: NamedType if tp1.symbol.maybeOwner.isClass => tp1.prefix.pathRoot
     case tp1 => tp1
 
   /** If this part starts with `C.this`, the class `C`.

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

@@ -346,17 +346,19 @@ class SepChecker(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser:
             case t =>
               foldOver(c, t)
 
-    def checkParams(refsToCheck: Refs, descr: => String) =
+    def checkRefs(refsToCheck: Refs, descr: => String) =
       val badParams = mutable.ListBuffer[Symbol]()
       def currentOwner = kind.dclSym.orElse(ctx.owner)
-      for hiddenRef <- prune(refsToCheck.footprint) do
-        val refSym = hiddenRef.termSymbol
-        if refSym.is(TermParam)
-          && !refSym.hasAnnotation(defn.ConsumeAnnot)
-          && !refSym.info.derivesFrom(defn.Caps_SharedCapability)
-          && currentOwner.isContainedIn(refSym.owner)
-        then
-          badParams += refSym
+      for hiddenRef <- prune(refsToCheck) do
+        val refSym = hiddenRef.pathRoot.termSymbol // TODO also hangle ThisTypes as pathRoots
+        if refSym.exists && !refSym.info.derivesFrom(defn.Caps_SharedCapability) then
+          if currentOwner.enclosingMethodOrClass.isProperlyContainedIn(refSym.owner.enclosingMethodOrClass) then
+            report.error(em"""Separation failure: $descr non-local $refSym""", pos)
+          else if refSym.is(TermParam)
+            && !refSym.hasAnnotation(defn.ConsumeAnnot)
+            && currentOwner.isContainedIn(refSym.owner)
+          then
+            badParams += refSym
       if badParams.nonEmpty then
         def paramsStr(params: List[Symbol]): String = (params: @unchecked) match
           case p :: Nil => i"${p.name}"
@@ -368,25 +370,28 @@ class SepChecker(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser:
               |The parameter$pluralS need$singleS to be annotated with @consume to allow this.""",
             pos)
 
-    def checkParameters() = kind match
+    def checkLegalRefs() = kind match
       case TypeKind.Result(sym, _) =>
         if !sym.isAnonymousFunction // we don't check return types of anonymous functions
             && !sym.is(Case)        // We don't check so far binders in patterns since they
                                     // have inferred universal types. TODO come back to this;
                                     // either infer more precise types for such binders or
                                     // "see through them" when we look at hidden sets.
-        then checkParams(tpe.deepCaptureSet.elems.hidden, i"$typeDescr type $tpe hides")
+        then
+          val refs = tpe.deepCaptureSet.elems
+          val toCheck = refs.hidden.footprint -- refs.footprint
+          checkRefs(toCheck, i"$typeDescr type $tpe hides")
       case TypeKind.Argument(arg) =>
         if tpe.hasAnnotation(defn.ConsumeAnnot) then
           val capts = captures(arg)
           def descr(verb: String) = i"argument to @consume parameter with type ${arg.nuType} $verb"
-          checkParams(capts, descr("refers to"))
-          checkParams(capts.hidden, descr("hides"))
+          checkRefs(capts.footprint, descr("refers to"))
+          checkRefs(capts.hidden.footprint, descr("hides"))
 
     if !tpe.hasAnnotation(defn.UntrackedCapturesAnnot) then
       traverse(Captures.None, tpe)
       traverse.toCheck.foreach(checkParts)
-      checkParameters()
+      checkLegalRefs()
   end checkType
 
   private def collectMethodTypes(tp: Type): List[TermLambda] = tp match
@@ -426,10 +431,12 @@ class SepChecker(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser:
       if argss.nestedExists(_.needsSepCheck) then
         checkApply(tree, argss.flatten, dependencies(tree, argss))
 
+  def isUnsafeAssumeSeparate(tree: Tree)(using Context): Boolean = tree match
+    case tree: Apply => tree.symbol == defn.Caps_unsafeAssumeSeparate
+    case _ => false
+
   def traverse(tree: Tree)(using Context): Unit =
-    tree match
-      case tree: Apply if tree.symbol == defn.Caps_unsafeAssumeSeparate => return
-      case _ =>
+    if isUnsafeAssumeSeparate(tree) then return
     checkUse(tree)
     tree match
       case tree: GenericApply =>
@@ -446,7 +453,7 @@ class SepChecker(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser:
           defsShadow = saved
       case tree: ValOrDefDef =>
         traverseChildren(tree)
-        if !tree.symbol.isOneOf(TermParamOrAccessor) then
+        if !tree.symbol.isOneOf(TermParamOrAccessor) && !isUnsafeAssumeSeparate(tree.rhs) then
           checkType(tree.tpt, tree.symbol)
           if previousDefs.nonEmpty then
             capt.println(i"sep check def ${tree.symbol}: ${tree.tpt} with ${captures(tree.tpt).hidden.footprint}")
@@ -460,5 +467,3 @@ end SepChecker
 
 
 
-
-

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

@@ -12,3 +12,7 @@
    |             ^^^^
    |             reference ops* is not included in the allowed capture set {}
    |             of an enclosing function literal with expected type () -> Unit
+-- Error: tests/neg-custom-args/captures/delayedRunops.scala:22:16 -----------------------------------------------------
+22 |      val ops1: List[() => Unit] = ops // error
+   |                ^^^^^^^^^^^^^^^^
+   |                Separation failure: value ops1's type List[box () => Unit] hides non-local parameter ops

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

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

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

@@ -42,5 +42,4 @@
 -- Error: tests/neg-custom-args/captures/i15772.scala:34:10 ------------------------------------------------------------
 34 |  def c : C^ = new C(x) // error separation
    |          ^^
-   |          Separation failure: method c's result type C^ hides parameter x.
-   |          The parameter needs to be annotated with @consume to allow this.
+   |          Separation failure: method c's result type C^ hides non-local parameter x

tests/neg-custom-args/captures/non-local-consume.scala

@@ -0,0 +1,23 @@
+import caps.{cap, consume, Mutable}
+import language.experimental.captureChecking
+
+class Buffer extends Mutable
+
+def f1(@consume buf: Buffer^): Buffer^ =
+  val buf1: Buffer^ = buf // OK
+  buf1
+
+def f2(@consume buf: Buffer^): Buffer^ =
+  def g(): Buffer^ = buf // error
+  g()
+
+def f3(@consume buf: Buffer^): Buffer^ =
+  val buf1 = buf
+  def g(): Buffer^ = buf1 // error
+  g()
+
+def f4(@consume buf: Buffer^): Buffer^ =
+  val buf1: Buffer^ = buf
+  def g(): Buffer^ = buf1 // error
+  g()
+

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

@@ -4,18 +4,30 @@
   |          Separation failure: Illegal access to {io} which is hidden by the previous definition
   |          of value x with type () => Unit.
   |          This type hides capabilities  {io}
+-- Error: tests/neg-custom-args/captures/sep-use.scala:12:12 -----------------------------------------------------------
+12 |  def x: () => Unit = () => println(io)  // error
+   |         ^^^^^^^^^^
+   |         Separation failure: method x's result type () => Unit hides non-local parameter io
 -- Error: tests/neg-custom-args/captures/sep-use.scala:13:10 -----------------------------------------------------------
 13 |  println(io) // error
    |          ^^
    |          Separation failure: Illegal access to {io} which is hidden by the previous definition
    |          of method x with result type () => Unit.
    |          This type hides capabilities  {io}
+-- Error: tests/neg-custom-args/captures/sep-use.scala:18:10 -----------------------------------------------------------
+18 |  def xx: (y: Int) => Unit = _ => println(io)  // error
+   |          ^^^^^^^^^^^^^^^^
+   |          Separation failure: method xx's result type (y: Int) => Unit hides non-local parameter io
 -- Error: tests/neg-custom-args/captures/sep-use.scala:19:10 -----------------------------------------------------------
 19 |  println(io) // error
    |          ^^
    |          Separation failure: Illegal access to {io} which is hidden by the previous definition
    |          of method xx with result type (y: Int) => Unit.
    |          This type hides capabilities  {io}
+-- Error: tests/neg-custom-args/captures/sep-use.scala:24:19 -----------------------------------------------------------
+24 |  def xxx(y: Int): Object^ = io  // error
+   |                   ^^^^^^^
+   |                   Separation failure: method xxx's result type Object^ hides non-local parameter io
 -- Error: tests/neg-custom-args/captures/sep-use.scala:25:10 -----------------------------------------------------------
 25 |  println(io) // error
    |          ^^

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

@@ -9,19 +9,19 @@ def test1(@consume io: Object^): Unit =
 
 def test2(@consume io: Object^): Unit =
 
-  def x: () => Unit = () => println(io)
+  def x: () => Unit = () => println(io)  // error
   println(io) // error
   println(x)  // ok
 
 def test3(@consume io: Object^): Unit =
 
-  def xx: (y: Int) => Unit = _ => println(io)
+  def xx: (y: Int) => Unit = _ => println(io)  // error
   println(io) // error
   println(xx(2))  // ok
 
 def test4(@consume io: Object^): Unit =
 
-  def xxx(y: Int): Object^ = io
+  def xxx(y: Int): Object^ = io  // error
   println(io) // error
   println(xxx(2))  // ok
 

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

@@ -2,7 +2,7 @@
 import caps.consume
 
 def test1(@consume c: Object^, f: Object^ => Object^) =
-  def cc: Object^ = c
+  def cc: Object^ = c  // error
   val x1 =
     { f(cc) } // ok
   val x2 =
@@ -13,7 +13,7 @@ def test1(@consume c: Object^, f: Object^ => Object^) =
     { f(c) } // error
 
 def test2(@consume c: Object^, f: Object^ ->{c} Object^) =
-  def cc: Object^ = c
+  def cc: Object^ = c // error
   val x1 =
     { f(cc) } // error // error
   val x4: Object^ =

tests/neg-custom-args/captures/unsound-reach-6.check

@@ -6,10 +6,8 @@
 -- Error: tests/neg-custom-args/captures/unsound-reach-6.scala:11:14 ---------------------------------------------------
 11 |    val z = f(ys)   // error @consume failure
    |              ^^
-   |Separation failure: argument to @consume parameter with type (ys : List[box () ->{io} Unit]) refers to parameters ys and io.
-   |The parameters need to be annotated with @consume to allow this.
+   |Separation failure: argument to @consume parameter with type (ys : List[box () ->{io} Unit]) refers to non-local parameter ys
 -- Error: tests/neg-custom-args/captures/unsound-reach-6.scala:19:14 ---------------------------------------------------
 19 |    val z = f(ys)  // error @consume failure
    |              ^^
-   |Separation failure: argument to @consume parameter with type (ys : -> List[box () ->{io} Unit]) refers to parameter io.
-   |The parameter needs to be annotated with @consume to allow this.
+   |Separation failure: argument to @consume parameter with type (ys : -> List[box () ->{io} Unit]) refers to non-local parameter io

tests/pos-custom-args/captures/eta-expansions.scala

@@ -3,7 +3,7 @@ class Cap extends caps.Capability
 def test(d: Cap) =
   def map2(xs: List[Int])(f: Int => Int): List[Int] = xs.map(f)
   val f1 = map2                      // capture polymorphic implicit eta expansion
-  def f2c: List[Int] => (Int => Int) => List[Int] = f1
+  val f2c: List[Int] => (Int => Int) => List[Int] = f1
   val a0 = identity[Cap ->{d} Unit]  // capture monomorphic implicit eta expansion
   val a0c: (Cap ->{d} Unit) ->{d} Cap ->{d} Unit = a0
   val b0 = (x: Cap ->{d} Unit) => identity[Cap ->{d} Unit](x) // not an implicit eta expansion, hence capture polymorphic

tests/pos-custom-args/captures/skolems2.scala

@@ -1,8 +1,9 @@
 
 import caps.consume
+import caps.unsafe.unsafeAssumeSeparate
 
 def Test(@consume c: Object^, f: Object^ => Object^) =
-  def cc: Object^ = c
+  def cc: Object^ = unsafeAssumeSeparate(c)
   val x1 =
     { f(cc) }
   val x2 =