Check separation of different parts of a declared type.

Author: odersky

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

@@ -1248,14 +1248,17 @@ object CaptureSet:
    *  arguments. This have to be included to be conservative in dcs but must be
    *  excluded in narrowCaps.
    */
-  def ofTypeDeeply(tp: Type, includeTypevars: Boolean = false)(using Context): CaptureSet =
+  def ofTypeDeeply(
+      tp: Type,
+      includeTypevars: Boolean = false,
+      union: (CaptureSet, CaptureSet) => Context ?=> CaptureSet = _ ++ _)(using Context): CaptureSet =
     val collect = new TypeAccumulator[CaptureSet]:
       val seen = util.HashSet[Symbol]()
       def apply(cs: CaptureSet, t: Type) =
         if variance < 0 then cs
         else t.dealias match
           case t @ CapturingType(p, cs1) =>
-            this(cs, p) ++ cs1
+            union(this(cs, p), cs1)
           case t @ AnnotatedType(parent, ann) =>
             this(cs, parent)
           case t: TypeRef if t.symbol.isAbstractOrParamType && !seen.contains(t.symbol) =>

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

@@ -52,18 +52,10 @@ class SepChecker(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser:
 
     private def hidden(using Context): Refs =
       val seen: util.EqHashSet[CaptureRef] = new util.EqHashSet
-
-      def hiddenByElem(elem: CaptureRef): Refs =
-        if seen.add(elem) then elem match
-          case Fresh.Cap(hcs) => hcs.elems.filter(!_.isRootCapability) ++ recur(hcs.elems)
-          case ReadOnlyCapability(ref) => hiddenByElem(ref).map(_.readOnly)
-          case _ => emptySet
-        else emptySet
-
       def recur(cs: Refs): Refs =
         (emptySet /: cs): (elems, elem) =>
-          elems ++ hiddenByElem(elem)
-
+          if seen.add(elem) then elems ++ hiddenByElem(elem, recur)
+          else elems
       recur(refs)
     end hidden
 
@@ -79,6 +71,11 @@ class SepChecker(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser:
         refs -- captures(dep).footprint
   end extension
 
+  private def hiddenByElem(ref: CaptureRef, recur: Refs => Refs)(using Context): Refs = ref match
+    case Fresh.Cap(hcs) => hcs.elems.filter(!_.isRootCapability) ++ recur(hcs.elems)
+    case ReadOnlyCapability(ref1) => hiddenByElem(ref1, recur).map(_.readOnly)
+    case _ => emptySet
+
   /** The captures of an argument or prefix widened to the formal parameter, if
    *  the latter contains a cap.
    */
@@ -212,6 +209,34 @@ class SepChecker(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser:
       if !overlap.isEmpty then
         sepUseError(tree, usedFootprint, overlap)
 
+  def checkType(tpt: Tree, sym: Symbol)(using Context) =
+    def checkSep(hidden: Refs, footprint: Refs, descr: String) =
+      val overlap = hidden.overlapWith(footprint)
+      if !overlap.isEmpty then
+        report.error(
+          em"""Separation failure: ${tpt.nuType} captures a root element hiding  ${CaptureSet(hidden)}
+              |and also $descr  ${CaptureSet(footprint)}.
+              |The two sets overlap at  ${CaptureSet(overlap)}""",
+          tpt.srcPos)
+
+    val capts = CaptureSet.ofTypeDeeply(tpt.nuType,
+        union = (xs, ys) => ctx ?=> CaptureSet(xs.elems ++ ys.elems))
+      .elems
+      // Note: Can't use captures(...) or deepCaptureSet here because these would map
+      // e.g (Object^{<cap hiding x}, Object^{x}) to {<cap hiding x>} and we need
+      // {<cap hiding x>, x} instead.
+    val explicitFootprint = capts.footprint
+    var hiddenFootprint: Refs = emptySet
+    //println(i"checking tp ${tpt.tpe} with $capts fp $explicitFootprint")
+    for ref <- capts do
+      val hidden0 = hiddenByElem(ref, _.hidden).footprint
+      val hiddenByRef = hiddenByElem(ref, _.hidden).footprint.deductSym(sym)
+      if !hiddenByRef.isEmpty then
+        checkSep(hiddenByRef, explicitFootprint, "refers to")
+        checkSep(hiddenByRef, hiddenFootprint, "captures another root element hiding")
+        hiddenFootprint ++= hiddenByRef
+  end checkType
+
   private def collectMethodTypes(tp: Type): List[TermLambda] = tp match
     case tp: MethodType => tp :: collectMethodTypes(tp.resType)
     case tp: PolyType => collectMethodTypes(tp.resType)
@@ -269,11 +294,13 @@ class SepChecker(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser:
           defsShadow = saved
       case tree: ValOrDefDef =>
         traverseChildren(tree)
-        if previousDefs.nonEmpty && !tree.symbol.isOneOf(TermParamOrAccessor) then
-          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
+        if !tree.symbol.isOneOf(TermParamOrAccessor) 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}")
+            defsShadow ++= captures(tree.tpt).hidden.footprint.deductSym(tree.symbol)
+            resultType(tree.symbol) = tree.tpt.nuType
+            previousDefs.head += tree
       case _ =>
         traverseChildren(tree)
 end SepChecker

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

@@ -1,11 +1,11 @@
--- Error: tests/neg-custom-args/captures/sepchecks2.scala:7:10 ---------------------------------------------------------
-7 |  println(c) // error
+-- Error: tests/neg-custom-args/captures/sepchecks2.scala:8:10 ---------------------------------------------------------
+8 |  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
+-- Error: tests/neg-custom-args/captures/sepchecks2.scala:11:33 --------------------------------------------------------
+11 |  foo((() => println(c)) :: Nil, c) // error
    |                                 ^
    |                                 Separation failure: argument of type  (c : Object^)
    |                                 to method foo: (xs: List[box () => Unit], y: Object^): Nothing
@@ -19,3 +19,15 @@
    |                                   Hidden footprint of current argument  : {c}
    |                                   Declared footprint of current argument: {}
    |                                   Undeclared overlap of footprints      : {c}
+-- Error: tests/neg-custom-args/captures/sepchecks2.scala:12:10 --------------------------------------------------------
+12 |  val x1: (Object^, Object^) = (c, c) // error
+   |          ^^^^^^^^^^^^^^^^^^
+   |          Separation failure: (box Object^, box Object^) captures a root element hiding  {c}
+   |          and also captures another root element hiding  {c}.
+   |          The two sets overlap at  {c}
+-- Error: tests/neg-custom-args/captures/sepchecks2.scala:13:10 --------------------------------------------------------
+13 |  val x2: (Object^, Object^{d}) = (d, d) // error
+   |          ^^^^^^^^^^^^^^^^^^^^^
+   |          Separation failure: (box Object^, box Object^{d}) captures a root element hiding  {d}
+   |          and also refers to  {d}.
+   |          The two sets overlap at  {d}

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

@@ -1,10 +1,19 @@
 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^) =
+def Test2(c: Object^, d: Object^) =
   foo((() => println(c)) :: Nil, c) // error
+  val x1: (Object^, Object^) = (c, c) // error
+  val x2: (Object^, Object^{d}) = (d, d) // error
+
+def Test3(c: Object^, d: Object^) =
+  val x: (Object^, Object^) = (c, d) // ok
+
+def Test4(c: Object^, d: Object^) =
+  val x: (Object^, Object^{c}) = (d, c) // ok