Skip to content

Commit 718e03d

Browse files
oderskyodersky
committed
Revise SepCheck.checkType
1 parent 0b9acb3 commit 718e03d

File tree

8 files changed

+168
-57
lines changed

8 files changed

+168
-57
lines changed

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

Lines changed: 120 additions & 27 deletions
Original file line numberDiff line numberDiff line change
@@ -10,11 +10,28 @@ import Contexts.*, Names.*, Flags.*, Symbols.*, Decorators.*
1010
import CaptureSet.{Refs, emptySet, HiddenSet}
1111
import config.Printers.capt
1212
import StdNames.nme
13-
import util.{SimpleIdentitySet, EqHashMap}
13+
import util.{SimpleIdentitySet, EqHashMap, SrcPos}
14+
15+
object SepChecker:
16+
17+
/** Enumerates kinds of captures encountered so far */
18+
enum Captures:
19+
case None
20+
case Explicit // one or more explicitly declared captures
21+
case Hidden // exacttly one hidden captures
22+
case NeedsCheck // one hidden capture and one other capture (hidden or declared)
23+
24+
def add(that: Captures): Captures =
25+
if this == None then that
26+
else if that == None then this
27+
else if this == Explicit && that == Explicit then Explicit
28+
else NeedsCheck
29+
end Captures
1430

1531
class SepChecker(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser:
1632
import tpd.*
1733
import checker.*
34+
import SepChecker.*
1835

1936
/** The set of capabilities that are hidden by a polymorphic result type
2037
* of some previous definition.
@@ -59,6 +76,10 @@ class SepChecker(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser:
5976
recur(refs)
6077
end hidden
6178

79+
private def containsHidden(using Context): Boolean =
80+
refs.exists: ref =>
81+
!hiddenByElem(ref, _ => emptySet).isEmpty
82+
6283
/** Deduct the footprint of `sym` and `sym*` from `refs` */
6384
private def deductSym(sym: Symbol)(using Context) =
6485
val ref = sym.termRef
@@ -183,6 +204,7 @@ class SepChecker(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser:
183204
for (arg, idx) <- indexedArgs do
184205
if arg.needsSepCheck then
185206
val ac = formalCaptures(arg)
207+
checkType(arg.formalType, arg.srcPos, NoSymbol, " the argument's adapted type")
186208
val hiddenInArg = ac.hidden.footprint
187209
//println(i"check sep $arg: $ac, footprint so far = $footprint, hidden = $hiddenInArg")
188210
val overlap = hiddenInArg.overlapWith(footprint).deductCapturesOf(deps(arg))
@@ -209,32 +231,103 @@ class SepChecker(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser:
209231
if !overlap.isEmpty then
210232
sepUseError(tree, usedFootprint, overlap)
211233

212-
def checkType(tpt: Tree, sym: Symbol)(using Context) =
213-
def checkSep(hidden: Refs, footprint: Refs, descr: String) =
214-
val overlap = hidden.overlapWith(footprint)
215-
if !overlap.isEmpty then
216-
report.error(
217-
em"""Separation failure: ${tpt.nuType} captures a root element hiding ${CaptureSet(hidden)}
218-
|and also $descr ${CaptureSet(footprint)}.
219-
|The two sets overlap at ${CaptureSet(overlap)}""",
220-
tpt.srcPos)
221-
222-
val capts = CaptureSet.ofTypeDeeply(tpt.nuType,
223-
union = (xs, ys) => ctx ?=> CaptureSet(xs.elems ++ ys.elems))
224-
.elems
225-
// Note: Can't use captures(...) or deepCaptureSet here because these would map
226-
// e.g (Object^{<cap hiding x}, Object^{x}) to {<cap hiding x>} and we need
227-
// {<cap hiding x>, x} instead.
228-
val explicitFootprint = capts.footprint
229-
var hiddenFootprint: Refs = emptySet
230-
//println(i"checking tp ${tpt.tpe} with $capts fp $explicitFootprint")
231-
for ref <- capts do
232-
val hidden0 = hiddenByElem(ref, _.hidden).footprint
233-
val hiddenByRef = hiddenByElem(ref, _.hidden).footprint.deductSym(sym)
234-
if !hiddenByRef.isEmpty then
235-
checkSep(hiddenByRef, explicitFootprint, "refers to")
236-
checkSep(hiddenByRef, hiddenFootprint, "captures another root element hiding")
237-
hiddenFootprint ++= hiddenByRef
234+
def checkType(tpt: Tree, sym: Symbol)(using Context): Unit =
235+
checkType(tpt.nuType, tpt.srcPos, sym, "")
236+
237+
/** Check that all parts of type `tpe` are separated.
238+
* @param tpe the type to check
239+
* @param pos position for error reporting
240+
* @param sym if `tpe` is the (result-) type of a val or def, the symbol of
241+
* this definition, otherwise NoSymbol. If `sym` exists we
242+
* deduct its associated direct and reach capabilities everywhere
243+
* from the capture sets we check.
244+
* @param what a string describing what kind of type it is
245+
*/
246+
def checkType(tpe: Type, pos: SrcPos, sym: Symbol, what: String)(using Context): Unit =
247+
248+
def checkParts(parts: List[Type]): Unit =
249+
var footprint: Refs = emptySet
250+
var hiddenSet: Refs = emptySet
251+
var checked = 0
252+
for part <- parts do
253+
254+
/** Report an error if `current` and `next` overlap.
255+
* @param current the footprint or hidden set seen so far
256+
* @param next the footprint or hidden set of the next part
257+
* @param mapRefs a function over the capture set elements of the next part
258+
* that returns the references of the same kind as `current`
259+
* (i.e. the part's footprint or hidden set)
260+
* @param prevRel a verbal description of current ("references or "hides")
261+
* @param nextRel a verbal descriiption of next
262+
*/
263+
def checkSep(current: Refs, next: Refs, mapRefs: Refs => Refs, prevRel: String, nextRel: String): Unit =
264+
val globalOverlap = current.overlapWith(next)
265+
if !globalOverlap.isEmpty then
266+
val (prevStr, prevRefs, overlap) = parts.iterator.take(checked)
267+
.map: prev =>
268+
val prevRefs = mapRefs(prev.deepCaptureSet.elems).footprint.deductSym(sym)
269+
(i", $prev , ", prevRefs, prevRefs.overlapWith(next))
270+
.dropWhile(_._3.isEmpty)
271+
.nextOption
272+
.getOrElse(("", current, globalOverlap))
273+
report.error(
274+
em"""Separation failure in$what type $tpe.
275+
|One part, $part , $nextRel ${CaptureSet(next)}.
276+
|A previous part$prevStr $prevRel ${CaptureSet(prevRefs)}.
277+
|The two sets overlap at ${CaptureSet(overlap)}.""",
278+
pos)
279+
280+
val partRefs = part.deepCaptureSet.elems
281+
val partFootprint = partRefs.footprint.deductSym(sym)
282+
val partHidden = partRefs.hidden.footprint.deductSym(sym) -- partFootprint
283+
284+
checkSep(footprint, partHidden, identity, "references", "hides")
285+
checkSep(hiddenSet, partHidden, _.hidden, "also hides", "hides")
286+
checkSep(hiddenSet, partFootprint, _.hidden, "hides", "references")
287+
288+
footprint ++= partFootprint
289+
hiddenSet ++= partHidden
290+
checked += 1
291+
end for
292+
end checkParts
293+
294+
object traverse extends TypeAccumulator[Captures]:
295+
296+
/** A stack of part lists to check. We maintain this since immediately
297+
* checking parts when traversing the type would check innermost to oputermost.
298+
* But we want to check outermost parts first since this prioritized errors
299+
* that are more obvious.
300+
*/
301+
var toCheck: List[List[Type]] = Nil
302+
303+
private val seen = util.HashSet[Symbol]()
304+
305+
def apply(c: Captures, t: Type) =
306+
if variance < 0 then c
307+
else
308+
val t1 = t.dealias
309+
t1 match
310+
case t @ AppliedType(tycon, args) =>
311+
val c1 = foldOver(Captures.None, t)
312+
if c1 == Captures.NeedsCheck then
313+
toCheck = (tycon :: args) :: toCheck
314+
c.add(c1)
315+
case t @ CapturingType(parent, cs) =>
316+
val c1 = this(c, parent)
317+
if cs.elems.containsHidden then c1.add(Captures.Hidden)
318+
else if !cs.elems.isEmpty then c1.add(Captures.Explicit)
319+
else c1
320+
case t: TypeRef if t.symbol.isAbstractOrParamType =>
321+
if seen.contains(t.symbol) then c
322+
else
323+
seen += t.symbol
324+
apply(apply(c, t.prefix), t.info.bounds.hi)
325+
case t =>
326+
foldOver(c, t)
327+
328+
if !tpe.hasAnnotation(defn.UntrackedCapturesAnnot) then
329+
traverse(Captures.None, tpe)
330+
traverse.toCheck.foreach(checkParts)
238331
end checkType
239332

240333
private def collectMethodTypes(tp: Type): List[TermLambda] = tp match

‎compiler/src/dotty/tools/dotc/core/Definitions.scala

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1063,6 +1063,7 @@ class Definitions {
10631063
@tu lazy val UncheckedCapturesAnnot: ClassSymbol = requiredClass("scala.annotation.unchecked.uncheckedCaptures")
10641064
@tu lazy val UntrackedCapturesAnnot: ClassSymbol = requiredClass("scala.caps.untrackedCaptures")
10651065
@tu lazy val UseAnnot: ClassSymbol = requiredClass("scala.caps.use")
1066+
@tu lazy val ConsumeAnnot: ClassSymbol = requiredClass("scala.caps.consume")
10661067
@tu lazy val RefineOverrideAnnot: ClassSymbol = requiredClass("scala.caps.refineOverride")
10671068
@tu lazy val VolatileAnnot: ClassSymbol = requiredClass("scala.volatile")
10681069
@tu lazy val BeanGetterMetaAnnot: ClassSymbol = requiredClass("scala.annotation.meta.beanGetter")

‎library/src/scala/caps.scala

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -77,6 +77,8 @@ import annotation.{experimental, compileTimeOnly, retainsCap}
7777
*/
7878
final class refineOverride extends annotation.StaticAnnotation
7979

80+
final class consume extends annotation.StaticAnnotation
81+
8082
object unsafe:
8183

8284
extension [T](x: T)

‎tests/neg-custom-args/captures/capt-depfun.check

Lines changed: 1 addition & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -1,13 +1,7 @@
11
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/capt-depfun.scala:10:43 ----------------------------------
2-
10 | val dc: ((Str^{y, z}) => Str^{y, z}) = ac(g()) // error // error sepcheck
2+
10 | val dc: ((Str^{y, z}) => Str^{y, z}) = ac(g()) // error
33
| ^^^^^^^
44
| Found: Str^{} ->{ac, y, z} Str^{y, z}
55
| Required: Str^{y, z} ->{fresh} Str^{y, z}
66
|
77
| longer explanation available when compiling with `-explain`
8-
-- Error: tests/neg-custom-args/captures/capt-depfun.scala:10:24 -------------------------------------------------------
9-
10 | val dc: ((Str^{y, z}) => Str^{y, z}) = ac(g()) // error // error sepcheck
10-
| ^^^^^^^^^^^^^^^^^^^^^^^^^^
11-
| Separation failure: Str^{y, z} => Str^{y, z} captures a root element hiding {ac, y, z}
12-
| and also refers to {y, z}.
13-
| The two sets overlap at {y, z}

‎tests/neg-custom-args/captures/capt-depfun.scala

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -7,4 +7,4 @@ class Str
77
def f(y: Cap, z: Cap) =
88
def g(): C @retains(y, z) = ???
99
val ac: ((x: Cap) => Str @retains(x) => Str @retains(x)) = ???
10-
val dc: ((Str^{y, z}) => Str^{y, z}) = ac(g()) // error // error sepcheck
10+
val dc: ((Str^{y, z}) => Str^{y, z}) = ac(g()) // error

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

Lines changed: 27 additions & 18 deletions
Original file line numberDiff line numberDiff line change
@@ -1,11 +1,11 @@
1-
-- Error: tests/neg-custom-args/captures/sepchecks2.scala:8:10 ---------------------------------------------------------
2-
8 | println(c) // error
3-
| ^
4-
| Separation failure: Illegal access to {c} which is hidden by the previous definition
5-
| of value xs with type List[box () => Unit].
6-
| This type hides capabilities {xs*, c}
7-
-- Error: tests/neg-custom-args/captures/sepchecks2.scala:11:33 --------------------------------------------------------
8-
11 | foo((() => println(c)) :: Nil, c) // error
1+
-- Error: tests/neg-custom-args/captures/sepchecks2.scala:10:10 --------------------------------------------------------
2+
10 | println(c) // error
3+
| ^
4+
| Separation failure: Illegal access to {c} which is hidden by the previous definition
5+
| of value xs with type List[box () => Unit].
6+
| This type hides capabilities {xs*, c}
7+
-- Error: tests/neg-custom-args/captures/sepchecks2.scala:13:33 --------------------------------------------------------
8+
13 | foo((() => println(c)) :: Nil, c) // error
99
| ^
1010
| Separation failure: argument of type (c : Object^)
1111
| to method foo: (xs: List[box () => Unit], y: Object^): Nothing
@@ -19,15 +19,24 @@
1919
| Hidden footprint of current argument : {c}
2020
| Declared footprint of current argument: {}
2121
| Undeclared overlap of footprints : {c}
22-
-- Error: tests/neg-custom-args/captures/sepchecks2.scala:12:10 --------------------------------------------------------
23-
12 | val x1: (Object^, Object^) = (c, c) // error
22+
-- Error: tests/neg-custom-args/captures/sepchecks2.scala:14:10 --------------------------------------------------------
23+
14 | val x1: (Object^, Object^) = (c, c) // error
2424
| ^^^^^^^^^^^^^^^^^^
25-
| Separation failure: (box Object^, box Object^) captures a root element hiding {c}
26-
| and also captures another root element hiding {c}.
27-
| The two sets overlap at {c}
28-
-- Error: tests/neg-custom-args/captures/sepchecks2.scala:13:10 --------------------------------------------------------
29-
13 | val x2: (Object^, Object^{d}) = (d, d) // error
25+
| Separation failure in type (box Object^, box Object^).
26+
| One part, box Object^ , hides {c}.
27+
| A previous part, box Object^ , also hides {c}.
28+
| The two sets overlap at {c}.
29+
-- Error: tests/neg-custom-args/captures/sepchecks2.scala:15:10 --------------------------------------------------------
30+
15 | val x2: (Object^, Object^{d}) = (d, d) // error
3031
| ^^^^^^^^^^^^^^^^^^^^^
31-
| Separation failure: (box Object^, box Object^{d}) captures a root element hiding {d}
32-
| and also refers to {d}.
33-
| The two sets overlap at {d}
32+
| Separation failure in type (box Object^, box Object^{d}).
33+
| One part, box Object^{d} , references {d}.
34+
| A previous part, box Object^ , hides {d}.
35+
| The two sets overlap at {d}.
36+
-- Error: tests/neg-custom-args/captures/sepchecks2.scala:27:6 ---------------------------------------------------------
37+
27 | bar((c, c)) // error
38+
| ^^^^^^
39+
| Separation failure in the argument's adapted type type (box Object^, box Object^).
40+
| One part, box Object^ , hides {c}.
41+
| A previous part, box Object^ , also hides {c}.
42+
| The two sets overlap at {c}.

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

Lines changed: 10 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,11 +3,13 @@ import language.future // sepchecks on
33

44
def foo(xs: List[() => Unit], y: Object^) = ???
55

6+
def bar(x: (Object^, Object^)): Unit = ???
7+
68
def Test(c: Object^) =
79
val xs: List[() => Unit] = (() => println(c)) :: Nil
810
println(c) // error
911

10-
def Test2(c: Object^, d: Object^) =
12+
def Test2(c: Object^, d: Object^): Unit =
1113
foo((() => println(c)) :: Nil, c) // error
1214
val x1: (Object^, Object^) = (c, c) // error
1315
val x2: (Object^, Object^{d}) = (d, d) // error
@@ -17,3 +19,10 @@ def Test3(c: Object^, d: Object^) =
1719

1820
def Test4(c: Object^, d: Object^) =
1921
val x: (Object^, Object^{c}) = (d, c) // ok
22+
23+
def Test5(c: Object^, d: Object^): Unit =
24+
bar((c, d)) // ok
25+
26+
def Test6(c: Object^, d: Object^): Unit =
27+
bar((c, c)) // error
28+

‎tests/run-custom-args/captures/colltest5/CollectionStrawManCC5_1.scala

Lines changed: 6 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -6,7 +6,8 @@ import scala.reflect.ClassTag
66
import annotation.unchecked.{uncheckedVariance, uncheckedCaptures}
77
import annotation.tailrec
88
import caps.cap
9-
import language.`3.7` // sepchecks on
9+
import caps.untrackedCaptures
10+
import language.`3.8` // sepchecks on
1011

1112
/** A strawman architecture for new collections. It contains some
1213
* example collection classes and methods with the intent to expose
@@ -68,11 +69,13 @@ object CollectionStrawMan5 {
6869
/** Base trait for strict collections */
6970
trait Buildable[+A] extends Iterable[A] {
7071
protected def newBuilder: Builder[A, Repr] @uncheckedVariance
71-
override def partition(p: A => Boolean): (Repr, Repr) = {
72+
override def partition(p: A => Boolean): (Repr, Repr) @untrackedCaptures =
73+
// Without untrackedCaptures this fails SepChecks.checkType.
74+
// But this is probably an error in the hiding logic.
75+
// TODO remove @untrackedCaptures and investigate
7276
val l, r = newBuilder
7377
iterator.foreach(x => (if (p(x)) l else r) += x)
7478
(l.result, r.result)
75-
}
7679
// one might also override other transforms here to avoid generating
7780
// iterators if it helps efficiency.
7881
}

0 commit comments

Comments
 (0)