Use deep capturesets for separation checking.

When checking whether two items overlap we should always check their deep capture sets.
Buried aliases should count as well.

Author: odersky

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

@@ -1051,7 +1051,7 @@ object CaptureSet:
     def getElems(v: Var): Option[Refs] = elemsMap.get(v)
 
     /** Record elements, return whether this was allowed.
-     *  By default, recording is allowed in regular both not in frozen states.
+     *  By default, recording is allowed in regular but not in frozen states.
      */
     def putElems(v: Var, elems: Refs): Boolean = { elemsMap(v) = elems; true }
 
@@ -1062,7 +1062,7 @@ object CaptureSet:
     def getDeps(v: Var): Option[Deps] = depsMap.get(v)
 
     /** Record dependent sets, return whether this was allowed.
-     *  By default, recording is allowed in regular both not in frozen states.
+     *  By default, recording is allowed in regular but not in frozen states.
      */
     def putDeps(v: Var, deps: Deps): Boolean = { depsMap(v) = deps; true }
 

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

@@ -66,21 +66,28 @@ class SepChecker(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser:
 
       recur(refs)
     end hidden
+
+    /** Deduct the footprint of `sym` and `sym*` from `refs` */
+    private def deductSym(sym: Symbol)(using Context) =
+      val ref = sym.termRef
+      if ref.isTrackableRef then refs -- CaptureSet(ref, ref.reach).elems.footprint
+      else refs
+
+    /** Deduct the footprint of all captures of `deps` from `refs` */
+    private def deductCapturesOf(deps: List[Tree])(using Context): Refs =
+      deps.foldLeft(refs): (refs, dep) =>
+        refs -- captures(dep).footprint
   end extension
 
   /** The captures of an argument or prefix widened to the formal parameter, if
    *  the latter contains a cap.
    */
   private def formalCaptures(arg: Tree)(using Context): Refs =
-    val argType = arg.formalType.orElse(arg.nuType)
-    (if argType.hasUseAnnot then argType.deepCaptureSet else argType.captureSet)
-      .elems
+    arg.formalType.orElse(arg.nuType).deepCaptureSet.elems
 
    /** The captures of a node */
   private def captures(tree: Tree)(using Context): Refs =
-    val tpe = tree.nuType
-    (if tree.formalType.hasUseAnnot then tpe.deepCaptureSet else tpe.captureSet)
-      .elems
+   tree.nuType.deepCaptureSet.elems
 
   private def sepApplyError(fn: Tree, args: List[Tree], argIdx: Int,
       overlap: Refs, hiddenInArg: Refs, footprints: List[(Refs, Int)],
@@ -144,7 +151,7 @@ class SepChecker(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser:
 
   def sepUseError(tree: Tree, used: Refs, globalOverlap: Refs)(using Context): Unit =
     val individualChecks = for mdefs <- previousDefs.iterator; mdef <- mdefs.iterator yield
-      val hiddenByDef = captures(mdef.tpt).hidden
+      val hiddenByDef = captures(mdef.tpt).hidden.footprint
       val overlap = defUseOverlap(hiddenByDef, used, tree.symbol)
       if !overlap.isEmpty then
         def resultStr = if mdef.isInstanceOf[DefDef] then " result" else ""
@@ -172,20 +179,16 @@ class SepChecker(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser:
     val footprints = mutable.ListBuffer[(Refs, Int)]((footprint, 0))
     val indexedArgs = args.zipWithIndex
 
-    def subtractDeps(elems: Refs, arg: Tree): Refs =
-      deps(arg).foldLeft(elems): (elems, dep) =>
-        elems -- captures(dep).footprint
-
     for (arg, idx) <- indexedArgs do
       if !arg.needsSepCheck then
-        footprint = footprint ++ subtractDeps(captures(arg).footprint, arg)
+        footprint = footprint ++ captures(arg).footprint.deductCapturesOf(deps(arg))
         footprints += ((footprint, idx + 1))
     for (arg, idx) <- indexedArgs do
       if arg.needsSepCheck then
         val ac = formalCaptures(arg)
         val hiddenInArg = ac.hidden.footprint
         //println(i"check sep $arg: $ac, footprint so far = $footprint, hidden = $hiddenInArg")
-        val overlap = subtractDeps(hiddenInArg.overlapWith(footprint), arg)
+        val overlap = hiddenInArg.overlapWith(footprint).deductCapturesOf(deps(arg))
         if !overlap.isEmpty then
           sepApplyError(fn, args, idx, overlap, hiddenInArg, footprints.toList, deps)
         footprint ++= captures(arg).footprint
@@ -267,7 +270,8 @@ class SepChecker(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser:
       case tree: ValOrDefDef =>
         traverseChildren(tree)
         if previousDefs.nonEmpty && !tree.symbol.isOneOf(TermParamOrAccessor) then
-          defsShadow ++= captures(tree.tpt).hidden.footprint
+          capt.println(i"sep check def ${tree.symbol}: ${tree.tpt} with ${captures(tree.tpt).hidden.footprint}")
+          defsShadow ++= captures(tree.tpt).hidden.footprint.deductSym(tree.symbol)
           resultType(tree.symbol) = tree.tpt.nuType
           previousDefs.head += tree
       case _ =>

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

@@ -35,9 +35,9 @@
    |and captures {cap2}, but this capability is also passed separately
    |in the function prefix with type  (LazyRef[Int]{val elem: () ->{ref2*} Int} | (ref1 : LazyRef[Int]{val elem: () ->{cap1} Int}^{cap1}))^{ref2}.
    |
-   |  Capture set of function prefix        : {ref1, ref2}
+   |  Capture set of function prefix        : {ref1, ref2, ref2*}
    |  Hidden set of current argument        : {cap2}
-   |  Footprint of function prefix          : {ref1, ref2, cap1, cap2}
+   |  Footprint of function prefix          : {ref1, ref2, ref2*, cap1, cap2}
    |  Hidden footprint of current argument  : {cap2}
    |  Declared footprint of current argument: {}
    |  Undeclared overlap of footprints      : {cap2}

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

@@ -0,0 +1,21 @@
+-- Error: tests/neg-custom-args/captures/sepchecks2.scala:7:10 ---------------------------------------------------------
+7 |  println(c) // error
+  |          ^
+  |          Separation failure: Illegal access to {c} which is hidden by the previous definition
+  |          of value xs with type List[box () => Unit].
+  |          This type hides capabilities  {xs*, c}
+-- Error: tests/neg-custom-args/captures/sepchecks2.scala:10:33 --------------------------------------------------------
+10 |  foo((() => println(c)) :: Nil, c) // error
+   |                                 ^
+   |                                 Separation failure: argument of type  (c : Object^)
+   |                                 to method foo: (xs: List[box () => Unit], y: Object^): Nothing
+   |                                 corresponds to capture-polymorphic formal parameter y of type  Object^
+   |                                 and captures {c}, but this capability is also passed separately
+   |                                 in the first argument with type  List[box () ->{c} Unit].
+   |
+   |                                   Capture set of first argument         : {c}
+   |                                   Hidden set of current argument        : {c}
+   |                                   Footprint of first argument           : {c}
+   |                                   Hidden footprint of current argument  : {c}
+   |                                   Declared footprint of current argument: {}
+   |                                   Undeclared overlap of footprints      : {c}

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

@@ -0,0 +1,10 @@
+import language.future // sepchecks on
+
+def foo(xs: List[() => Unit], y: Object^) = ???
+
+def Test(c: Object^) =
+  val xs: List[() => Unit] = (() => println(c)) :: Nil
+  println(c) // error
+
+def Test2(c: Object^) =
+  foo((() => println(c)) :: Nil, c) // error