Skip to content

Commit e36d777

Browse files
oderskyodersky
committed
Peak-based separation checking for def-use
1 parent 426b46a commit e36d777

File tree

8 files changed

+119
-92
lines changed

8 files changed

+119
-92
lines changed

Diff for: ‎compiler/src/dotty/tools/dotc/cc/CaptureRef.scala

+2
Original file line numberDiff line numberDiff line change
@@ -287,6 +287,8 @@ trait CaptureRef extends TypeProxy, ValueType:
287287
this match
288288
case MaybeCapability(x1) => x1.covers(y1)
289289
case _ => false
290+
case Fresh.Cap(hidden) =>
291+
hidden.superCaps.exists(this covers _)
290292
case _ =>
291293
false
292294

Diff for: ‎compiler/src/dotty/tools/dotc/cc/SepCheck.scala

+72-67
Original file line numberDiff line numberDiff line change
@@ -145,6 +145,8 @@ object SepCheck:
145145

146146
case class PeaksPair(actual: Refs, hidden: Refs)
147147

148+
case class DefInfo(tree: ValOrDefDef, symbol: Symbol, hidden: Refs, hiddenPeaks: Refs)
149+
148150
class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser:
149151
import checker.*
150152
import SepCheck.*
@@ -154,15 +156,10 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser:
154156
*/
155157
private var defsShadow: Refs = emptyRefs
156158

157-
/** A map from definitions to their internal result types.
158-
* Populated during separation checking traversal.
159-
*/
160-
private val resultType = EqHashMap[Symbol, Type]()
161-
162-
/** The previous val or def definitions encountered during separation checking.
163-
* These all enclose and precede the current traversal node.
159+
/** The previous val or def definitions encountered during separation checking
160+
* in reverse order. These all enclose and precede the current traversal node.
164161
*/
165-
private var previousDefs: List[mutable.ListBuffer[ValOrDefDef]] = Nil
162+
private var previousDefs: List[DefInfo] = Nil
166163

167164
/** The set of references that were consumed so far in the current method */
168165
private var consumed: MutConsumedSet = MutConsumedSet()
@@ -402,31 +399,26 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser:
402399

403400
/** Report a use/definition failure, where a previously hidden capability is
404401
* used again.
405-
* @param tree the tree where the capability is used
406-
* @param used the footprint of all uses of `tree`
407-
* @param globalOverlap the overlap between `used` and all capabilities hidden
408-
* by previous definitions
402+
* @param tree the tree where the capability is used
403+
* @param clashing the tree where the capability is previously hidden,
404+
* or emptyTree if none exists
405+
* @param used the uses of `tree`
406+
* @param hidden the hidden set of the clashing def,
407+
* or the global hidden set if no clashing def exists
409408
*/
410-
def sepUseError(tree: Tree, used: Refs, globalOverlap: Refs)(using Context): Unit =
411-
val individualChecks = for mdefs <- previousDefs.iterator; mdef <- mdefs.iterator yield
412-
val hiddenByDef = captures(mdef.tpt).hiddenSet.footprint
413-
val overlap = defUseOverlap(hiddenByDef, used, tree.symbol)
414-
if !overlap.isEmpty then
415-
def resultStr = if mdef.isInstanceOf[DefDef] then " result" else ""
416-
report.error(
417-
em"""Separation failure: Illegal access to ${CaptureSet(overlap)} which is hidden by the previous definition
418-
|of ${mdef.symbol} with$resultStr type ${mdef.tpt.nuType}.
419-
|This type hides capabilities ${CaptureSet(hiddenByDef)}""",
420-
tree.srcPos)
421-
true
422-
else false
423-
val clashes = individualChecks.filter(identity)
424-
if clashes.hasNext then clashes.next // issues error as a side effect
425-
else report.error(
426-
em"""Separation failure: Illegal access to ${CaptureSet(globalOverlap)} which is hidden by some previous definitions
427-
|No clashing definitions were found. This might point to an internal error.""",
428-
tree.srcPos)
429-
end sepUseError
409+
def sepUseError(tree: Tree, clashingDef: ValOrDefDef | Null, used: Refs, hidden: Refs)(using Context): Unit =
410+
if clashingDef != null then
411+
def resultStr = if clashingDef.isInstanceOf[DefDef] then " result" else ""
412+
report.error(
413+
em"""Separation failure: Illegal access to ${overlapStr(hidden, used)} which is hidden by the previous definition
414+
|of ${clashingDef.symbol} with$resultStr type ${clashingDef.tpt.nuType}.
415+
|This type hides capabilities ${CaptureSet(hidden)}""",
416+
tree.srcPos)
417+
else
418+
report.error(
419+
em"""Separation failure: illegal access to ${overlapStr(hidden, used)} which is hidden by some previous definitions
420+
|No clashing definitions were found. This might point to an internal error.""",
421+
tree.srcPos)
430422

431423
/** Report a failure where a previously consumed capability is used again,
432424
* @param ref the capability that is used after being consumed
@@ -531,33 +523,37 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser:
531523
currentPeaks.hidden ++ argPeaks.hidden)
532524
end checkApply
533525

534-
/** The def/use overlap between the references `hiddenByDef` hidden by
535-
* a previous definition and the `used` set of a tree with symbol `sym`.
536-
* Deduct any capabilities referred to or hidden by the (result-) type of `sym`.
537-
*/
538-
def defUseOverlap(hiddenByDef: Refs, used: Refs, sym: Symbol)(using Context): Refs =
539-
val overlap = hiddenByDef.overlapWith(used)
540-
resultType.get(sym) match
541-
case Some(tp) if !overlap.isEmpty =>
542-
val declared = tp.captureSet.elems
543-
overlap.deduct(declared.footprint).deduct(declared.hiddenSet.footprint)
544-
case _ =>
545-
overlap
546-
547526
/** 1. Check that the capabilities used at `tree` don't overlap with
548527
* capabilities hidden by a previous definition.
549528
* 2. Also check that none of the used capabilities was consumed before.
550529
*/
551-
def checkUse(tree: Tree)(using Context) =
552-
val used = tree.markedFree
553-
if !used.elems.isEmpty then
554-
val usedFootprint = used.elems.footprint
555-
val overlap = defUseOverlap(defsShadow, usedFootprint, tree.symbol)
556-
if !overlap.isEmpty then
557-
sepUseError(tree, usedFootprint, overlap)
558-
for ref <- used.elems do
530+
def checkUse(tree: Tree)(using Context): Unit =
531+
val used = tree.markedFree.elems
532+
if !used.isEmpty then
533+
val usedPeaks = used.peaks
534+
val overlap = defsShadow.peaks.sharedWith(usedPeaks)
535+
if !defsShadow.peaks.sharedWith(usedPeaks).isEmpty then
536+
val sym = tree.symbol
537+
538+
def findClashing(prevDefs: List[DefInfo]): Option[DefInfo] = prevDefs match
539+
case prevDef :: prevDefs1 =>
540+
if prevDef.symbol == sym then Some(prevDef)
541+
else if !prevDef.hiddenPeaks.sharedWith(usedPeaks).isEmpty then Some(prevDef)
542+
else findClashing(prevDefs1)
543+
case Nil =>
544+
None
545+
546+
findClashing(previousDefs) match
547+
case Some(clashing) =>
548+
if clashing.symbol != sym then
549+
sepUseError(tree, clashing.tree, used, clashing.hidden)
550+
case None =>
551+
sepUseError(tree, null, used, defsShadow)
552+
553+
for ref <- used do
559554
val pos = consumed.get(ref)
560555
if pos != null then consumeError(ref, pos, tree.srcPos)
556+
end checkUse
561557

562558
/** If `tp` denotes some version of a singleton type `x.type` the set `{x}`
563559
* otherwise the empty set.
@@ -840,6 +836,10 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser:
840836
case tree: Apply => tree.symbol == defn.Caps_unsafeAssumeSeparate
841837
case _ => false
842838

839+
def pushDef(tree: ValOrDefDef, hiddenByDef: Refs)(using Context): Unit =
840+
defsShadow ++= hiddenByDef
841+
previousDefs = DefInfo(tree, tree.symbol, hiddenByDef, hiddenByDef.peaks) :: previousDefs
842+
843843
/** Check (result-) type of `tree` for separation conditions using `checkType`.
844844
* Excluded are parameters and definitions that have an =unsafeAssumeSeparate
845845
* application as right hand sides.
@@ -848,11 +848,18 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser:
848848
def checkValOrDefDef(tree: ValOrDefDef)(using Context): Unit =
849849
if !tree.symbol.isOneOf(TermParamOrAccessor) && !isUnsafeAssumeSeparate(tree.rhs) then
850850
checkType(tree.tpt, tree.symbol)
851-
if previousDefs.nonEmpty then
852-
capt.println(i"sep check def ${tree.symbol}: ${tree.tpt} with ${captures(tree.tpt).hiddenSet.footprint}")
853-
defsShadow ++= captures(tree.tpt).hiddenSet.deductSymRefs(tree.symbol).footprint
854-
resultType(tree.symbol) = tree.tpt.nuType
855-
previousDefs.head += tree
851+
capt.println(i"sep check def ${tree.symbol}: ${tree.tpt} with ${captures(tree.tpt).hiddenSet.footprint}")
852+
pushDef(tree, captures(tree.tpt).hiddenSet.deductSymRefs(tree.symbol))
853+
854+
def inSection[T](op: => T)(using Context): T =
855+
val savedDefsShadow = defsShadow
856+
val savedPrevionsDefs = previousDefs
857+
try op
858+
finally
859+
previousDefs = savedPrevionsDefs
860+
defsShadow = savedDefsShadow
861+
862+
def traverseSection[T](tree: Tree)(using Context) = inSection(traverseChildren(tree))
856863

857864
/** Traverse `tree` and perform separation checks everywhere */
858865
def traverse(tree: Tree)(using Context): Unit =
@@ -870,19 +877,17 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser:
870877
tree.tpe match
871878
case _: MethodOrPoly =>
872879
case _ => traverseApply(tree, Nil)
873-
case tree: Block =>
874-
val saved = defsShadow
875-
previousDefs = mutable.ListBuffer() :: previousDefs
876-
try traverseChildren(tree)
877-
finally
878-
previousDefs = previousDefs.tail
879-
defsShadow = saved
880+
case _: Block | _: Template =>
881+
traverseSection(tree)
880882
case tree: ValDef =>
881883
traverseChildren(tree)
882884
checkValOrDefDef(tree)
883885
case tree: DefDef =>
884-
withFreshConsumed:
885-
traverseChildren(tree)
886+
inSection:
887+
withFreshConsumed:
888+
for params <- tree.paramss; case param: ValDef <- params do
889+
pushDef(param, emptyRefs)
890+
traverseChildren(tree)
886891
checkValOrDefDef(tree)
887892
case If(cond, thenp, elsep) =>
888893
traverse(cond)

Diff for: ‎library/src/scala/caps.scala

+1-1
Original file line numberDiff line numberDiff line change
@@ -114,7 +114,7 @@ import annotation.{experimental, compileTimeOnly, retainsCap}
114114

115115
/** A wrapper around code for which separation checks are suppressed.
116116
*/
117-
def unsafeAssumeSeparate[T](op: T): T = op
117+
def unsafeAssumeSeparate(op: Any): op.type = op
118118

119119
end unsafe
120120
end caps

Diff for: ‎scala2-library-cc/src/scala/collection/immutable/LazyListIterable.scala

+8-6
Original file line numberDiff line numberDiff line change
@@ -463,8 +463,11 @@ final class LazyListIterable[+A] private(@untrackedCaptures lazyState: () => Laz
463463
* $preservesLaziness
464464
*/
465465
override def partitionMap[A1, A2](f: A => Either[A1, A2]): (LazyListIterable[A1]^{this, f}, LazyListIterable[A2]^{this, f}) = {
466-
val (left, right) = map(f).partition(_.isLeft)
467-
(left.map(_.asInstanceOf[Left[A1, _]].value), right.map(_.asInstanceOf[Right[_, A2]].value))
466+
unsafeAssumeSeparate:
467+
val part = map(f).partition(_.isLeft)
468+
val left = part._1
469+
val right = part._2
470+
(left.map(_.asInstanceOf[Left[A1, _]].value), right.map(_.asInstanceOf[Right[_, A2]].value))
468471
}
469472

470473
/** @inheritdoc
@@ -675,17 +678,16 @@ final class LazyListIterable[+A] private(@untrackedCaptures lazyState: () => Laz
675678
override def dropRight(n: Int): LazyListIterable[A]^{this} = {
676679
if (n <= 0) this
677680
else if (knownIsEmpty) LazyListIterable.empty
678-
else newLL {
681+
else unsafeAssumeSeparate { newLL {
679682
var scout = this
680683
var remaining = n
681684
// advance scout n elements ahead (or until empty)
682685
while (remaining > 0 && !scout.isEmpty) {
683686
remaining -= 1
684687
scout = scout.tail
685688
}
686-
unsafeAssumeSeparate:
687-
dropRightState(scout)
688-
}
689+
dropRightState(scout)
690+
}}
689691
}
690692

691693
private def dropRightState(scout: LazyListIterable[_]^): State[A]^{this, scout} =

Diff for: ‎tests/neg-custom-args/captures/lazyref.check

+28-10
Original file line numberDiff line numberDiff line change
@@ -26,27 +26,45 @@
2626
| Required: LazyRef[Int]^{cap1}
2727
|
2828
| longer explanation available when compiling with `-explain`
29+
-- Error: tests/neg-custom-args/captures/lazyref.scala:8:24 ------------------------------------------------------------
30+
8 | new LazyRef(() => f(elem())) // error: separation failure
31+
| ^^^^
32+
| Separation failure: Illegal access to {LazyRef.this.elem} which is hidden by the previous definition
33+
| of value get with type () => T.
34+
| This type hides capabilities {LazyRef.this.elem}
35+
-- Error: tests/neg-custom-args/captures/lazyref.scala:23:13 -----------------------------------------------------------
36+
23 | val ref3 = ref1.map(g) // error: separation failure
37+
| ^^^^
38+
| Separation failure: Illegal access to {cap1} which is hidden by the previous definition
39+
| of value ref2 with type LazyRef[Int]{val elem: () => Int}^{cap2, ref1}.
40+
| This type hides capabilities {cap1}
2941
-- Error: tests/neg-custom-args/captures/lazyref.scala:26:9 ------------------------------------------------------------
3042
26 | if cap1 == cap2 // error: separation failure // error: separation failure
3143
| ^^^^
3244
| Separation failure: Illegal access to {cap1} which is hidden by the previous definition
33-
| of value ref2 with type LazyRef[Int]{val elem: () => Int}^{cap2, ref1}.
34-
| This type hides capabilities {ref2*, cap1, cap2, ref1}
45+
| of value ref3 with type LazyRef[Int]{val elem: () => Int}^{cap2, ref1}.
46+
| This type hides capabilities {ref2*, cap1}
3547
-- Error: tests/neg-custom-args/captures/lazyref.scala:26:17 -----------------------------------------------------------
3648
26 | if cap1 == cap2 // error: separation failure // error: separation failure
3749
| ^^^^
3850
| Separation failure: Illegal access to {cap2} which is hidden by the previous definition
39-
| of value ref2 with type LazyRef[Int]{val elem: () => Int}^{cap2, ref1}.
40-
| This type hides capabilities {ref2*, cap1, cap2, ref1}
51+
| of value ref3 with type LazyRef[Int]{val elem: () => Int}^{cap2, ref1}.
52+
| This type hides capabilities {ref2*, cap1}
4153
-- Error: tests/neg-custom-args/captures/lazyref.scala:27:11 -----------------------------------------------------------
42-
27 | then ref1 // error: separation failure
54+
27 | then ref1 // error: separation failure
4355
| ^^^^
44-
| Separation failure: Illegal access to {ref1} which is hidden by the previous definition
45-
| of value ref2 with type LazyRef[Int]{val elem: () => Int}^{cap2, ref1}.
46-
| This type hides capabilities {ref2*, cap1, cap2, ref1}
56+
| Separation failure: Illegal access to {cap1, ref1} which is hidden by the previous definition
57+
| of value ref3 with type LazyRef[Int]{val elem: () => Int}^{cap2, ref1}.
58+
| This type hides capabilities {ref2*, cap1}
59+
-- Error: tests/neg-custom-args/captures/lazyref.scala:28:11 -----------------------------------------------------------
60+
28 | else ref2) // error: separation failure
61+
| ^^^^
62+
| Separation failure: Illegal access to {cap1, cap2, ref1} which is hidden by the previous definition
63+
| of value ref3 with type LazyRef[Int]{val elem: () => Int}^{cap2, ref1}.
64+
| This type hides capabilities {ref2*, cap1}
4765
-- Error: tests/neg-custom-args/captures/lazyref.scala:29:9 ------------------------------------------------------------
4866
29 | .map(g) // error: separation failure
4967
| ^
5068
| Separation failure: Illegal access to {cap2} which is hidden by the previous definition
51-
| of value ref2 with type LazyRef[Int]{val elem: () => Int}^{cap2, ref1}.
52-
| This type hides capabilities {ref2*, cap1, cap2, ref1}
69+
| of value ref3 with type LazyRef[Int]{val elem: () => Int}^{cap2, ref1}.
70+
| This type hides capabilities {ref2*, cap1}

Diff for: ‎tests/neg-custom-args/captures/lazyref.scala

+4-4
Original file line numberDiff line numberDiff line change
@@ -5,7 +5,7 @@ type Cap = CC^
55
class LazyRef[T](val elem: () => T):
66
val get: () => T = elem
77
def map[U](f: T => U): LazyRef[U]^{f, this} =
8-
new LazyRef(() => f(elem()))
8+
new LazyRef(() => f(elem())) // error: separation failure
99

1010
def map[A, B](ref: LazyRef[A]^, f: A => B): LazyRef[B]^{f, ref} =
1111
new LazyRef(() => f(ref.elem()))
@@ -20,11 +20,11 @@ def test(cap1: Cap, cap2: Cap) =
2020
val ref1c: LazyRef[Int] = ref1 // error
2121
val ref2 = map(ref1, g)
2222
val ref2c: LazyRef[Int]^{cap2} = ref2 // error
23-
val ref3 = ref1.map(g)
23+
val ref3 = ref1.map(g) // error: separation failure
2424
val ref3c: LazyRef[Int]^{ref1} = ref3 // error
2525
val ref4 = (
2626
if cap1 == cap2 // error: separation failure // error: separation failure
27-
then ref1 // error: separation failure
28-
else ref2)
27+
then ref1 // error: separation failure
28+
else ref2) // error: separation failure
2929
.map(g) // error: separation failure
3030
val ref4c: LazyRef[Int]^{cap1} = ref4 // error

Diff for: ‎tests/neg-custom-args/captures/sepchecks2.check

+1-1
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@
33
| ^
44
| Separation failure: Illegal access to {c} which is hidden by the previous definition
55
| of value xs with type List[box () => Unit].
6-
| This type hides capabilities {xs*, c}
6+
| This type hides capabilities {c}
77
-- Error: tests/neg-custom-args/captures/sepchecks2.scala:13:7 ---------------------------------------------------------
88
13 | foo((() => println(c)) :: Nil, c) // error
99
| ^^^^^^^^^^^^^^^^^^^^^^^^

Diff for: ‎tests/pos-custom-args/captures/path-use.scala

+3-3
Original file line numberDiff line numberDiff line change
@@ -2,15 +2,15 @@ import language.experimental.namedTuples
22

33
class IO
44

5-
class C(val f: IO^):
5+
class C(val ff: IO^):
66
val procs: List[Proc] = ???
77

88
type Proc = () => Unit
99

1010
def test(io: IO^) =
1111
val c = C(io)
12-
val f = () => println(c.f)
13-
val _: () ->{c.f} Unit = f
12+
val f = () => println(c.ff)
13+
val _: () ->{c.ff} Unit = f
1414

1515
val x = c.procs
1616
val _: List[() ->{c.procs*} Unit] = x

0 commit comments

Comments
 (0)