Skip to content

Commit c5bad2c

Browse files
oderskyodersky
committed
Also include nested caps when computing hidden members of a capture set
1 parent bc622f5 commit c5bad2c

File tree

4 files changed

+49
-36
lines changed

4 files changed

+49
-36
lines changed

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

+24-34
Original file line numberDiff line numberDiff line change
@@ -180,18 +180,19 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser:
180180
extension (refs: Refs)
181181

182182
/** The footprint of a set of references `refs` the smallest set `F` such that
183-
* - no maximal capability is in `F`
184-
* - all non-maximal capabilities in `refs` are in `F`
185-
* - if `f in F` then the footprint of `f`'s info is also in `F`.
183+
* 1. if includeMax is false then no maximal capability is in `F`
184+
* 2. all capabilities in `refs` satisfying (1) are in `F`
185+
* 3. if `f in F` then the footprint of `f`'s info is also in `F`.
186186
*/
187-
private def footprint(using Context): Refs =
187+
private def footprint(includeMax: Boolean = false)(using Context): Refs =
188+
def retain(ref: CaptureRef) = includeMax || !ref.isMaxCapability
188189
def recur(elems: Refs, newElems: List[CaptureRef]): Refs = newElems match
189190
case newElem :: newElems1 =>
190191
val superElems = newElem.captureSetOfInfo.elems.filter: superElem =>
191-
!superElem.isMaxCapability && !elems.contains(superElem)
192+
retain(superElem) && !elems.contains(superElem)
192193
recur(elems ++ superElems, newElems1 ++ superElems.toList)
193194
case Nil => elems
194-
val elems: Refs = refs.filter(!_.isMaxCapability)
195+
val elems: Refs = refs.filter(retain)
195196
recur(elems, elems.toList)
196197

197198
private def peaks(using Context): Refs =
@@ -269,7 +270,7 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser:
269270
val seen: util.EqHashSet[CaptureRef] = new util.EqHashSet
270271

271272
def hiddenByElem(elem: CaptureRef): Refs = elem match
272-
case Fresh.Cap(hcs) => hcs.elems.filter(!_.isRootCapability) ++ recur(hcs.elems)
273+
case Fresh.Cap(hcs) => hcs.elems ++ recur(hcs.elems)
273274
case ReadOnlyCapability(ref1) => hiddenByElem(ref1).map(_.readOnly)
274275
case _ => emptyRefs
275276

@@ -280,20 +281,6 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser:
280281
recur(refs)
281282
end hiddenSet
282283

283-
/** Same as !refs.hidden.isEmpty but more efficient */
284-
private def containsHidden(using Context): Boolean =
285-
val seen: util.EqHashSet[CaptureRef] = new util.EqHashSet
286-
287-
def recur(refs: Refs): Boolean = refs.exists: ref =>
288-
seen.add(ref) && ref.stripReadOnly.match
289-
case Fresh.Cap(hcs) =>
290-
hcs.elems.exists(!_.isRootCapability) || recur(hcs.elems)
291-
case _ =>
292-
false
293-
294-
recur(refs)
295-
end containsHidden
296-
297284
/** Subtract all elements that are covered by some element in `others` from this set. */
298285
private def deduct(others: Refs)(using Context): Refs =
299286
refs.filter: ref =>
@@ -302,7 +289,7 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser:
302289
/** Deduct the footprint of `sym` and `sym*` from `refs` */
303290
private def deductSymFootprint(sym: Symbol)(using Context): Refs =
304291
val ref = sym.termRef
305-
if ref.isTrackableRef then refs.deduct(CaptureSet(ref, ref.reach).elems.footprint)
292+
if ref.isTrackableRef then refs.deduct(CaptureSet(ref, ref.reach).elems.footprint())
306293
else refs
307294

308295
/** Deduct `sym` and `sym*` from `refs` */
@@ -314,7 +301,7 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser:
314301
/** Deduct the footprint of all captures of trees in `deps` from `refs` */
315302
private def deductCapturesOf(deps: List[Tree])(using Context): Refs =
316303
deps.foldLeft(refs): (refs, dep) =>
317-
refs.deduct(captures(dep).footprint)
304+
refs.deduct(captures(dep).footprint())
318305
end extension
319306

320307
/** The deep capture set of an argument or prefix widened to the formal parameter, if
@@ -333,16 +320,19 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser:
333320
shared.nth(0) match
334321
case fresh @ Fresh.Cap(hidden) =>
335322
if hidden.owner.exists then i"$fresh of ${hidden.owner}" else i"$fresh"
323+
case other =>
324+
i"$other"
336325

337326
def overlapStr(hiddenSet: Refs, clashSet: Refs)(using Context): String =
338-
val hiddenFootprint = hiddenSet.footprint
339-
val clashFootprint = clashSet.footprint
327+
val hiddenFootprint = hiddenSet.footprint()
328+
val clashFootprint = clashSet.footprint()
340329
// The overlap of footprints, or, of this empty the set of shared peaks.
341330
// We prefer footprint overlap since it tends to be more informative.
342331
val overlap = hiddenFootprint.overlapWith(clashFootprint)
343332
if !overlap.isEmpty then i"${CaptureSet(overlap)}"
344333
else
345-
val sharedPeaks = hiddenSet.peaks.sharedWith(clashSet.peaks)
334+
val sharedPeaks = hiddenSet.footprint(includeMax = true).sharedWith:
335+
clashSet.footprint(includeMax = true)
346336
assert(!sharedPeaks.isEmpty, i"no overlap for $hiddenSet vs $clashSet")
347337
sharedPeaksStr(sharedPeaks)
348338

@@ -391,9 +381,9 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser:
391381
|Some of these overlap with the captures of the ${clashArgStr.trim}$clashTypeStr.
392382
|
393383
| Hidden set of current argument : ${CaptureSet(hiddenSet)}
394-
| Hidden footprint of current argument : ${CaptureSet(hiddenSet.footprint)}
384+
| Hidden footprint of current argument : ${CaptureSet(hiddenSet.footprint())}
395385
| Capture set of $clashArgStr : ${CaptureSet(clashSet)}
396-
| Footprint set of $clashArgStr : ${CaptureSet(clashSet.footprint)}
386+
| Footprint set of $clashArgStr : ${CaptureSet(clashSet.footprint())}
397387
| The two sets overlap at : ${overlapStr(hiddenSet, clashSet)}""",
398388
polyArg.srcPos)
399389

@@ -657,7 +647,7 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser:
657647
val captured = genPart.deepCaptureSet.elems
658648
val hiddenSet = captured.hiddenSet.pruned
659649
val clashSet = otherPart.deepCaptureSet.elems
660-
val deepClashSet = (clashSet.footprint ++ clashSet.hiddenSet).pruned
650+
val deepClashSet = (clashSet.footprint() ++ clashSet.hiddenSet).pruned
661651
report.error(
662652
em"""Separation failure in ${role.description} $tpe.
663653
|One part, $genPart, hides capabilities ${CaptureSet(hiddenSet)}.
@@ -735,7 +725,7 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser:
735725
c.add(c1)
736726
case t @ CapturingType(parent, cs) =>
737727
val c1 = this(c, parent)
738-
if cs.elems.containsHidden then c1.add(Captures.Hidden)
728+
if cs.elems.exists(_.stripReadOnly.isFresh) then c1.add(Captures.Hidden)
739729
else if !cs.elems.isEmpty then c1.add(Captures.Explicit)
740730
else c1
741731
case t: TypeRef if t.symbol.isAbstractOrParamType =>
@@ -760,11 +750,11 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser:
760750
// "see through them" when we look at hidden sets.
761751
then
762752
val refs = tpe.deepCaptureSet.elems
763-
val toCheck = refs.hiddenSet.footprint.deduct(refs.footprint)
753+
val toCheck = refs.hiddenSet.footprint().deduct(refs.footprint())
764754
checkConsumedRefs(toCheck, tpe, role, i"${role.description} $tpe hides", pos)
765755
case TypeRole.Argument(arg) =>
766756
if tpe.hasAnnotation(defn.ConsumeAnnot) then
767-
val capts = captures(arg).footprint
757+
val capts = captures(arg).footprint()
768758
checkConsumedRefs(capts, tpe, role, i"argument to @consume parameter with type ${arg.nuType} refers to", pos)
769759
case _ =>
770760

@@ -848,7 +838,7 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser:
848838
def checkValOrDefDef(tree: ValOrDefDef)(using Context): Unit =
849839
if !tree.symbol.isOneOf(TermParamOrAccessor) && !isUnsafeAssumeSeparate(tree.rhs) then
850840
checkType(tree.tpt, tree.symbol)
851-
capt.println(i"sep check def ${tree.symbol}: ${tree.tpt} with ${captures(tree.tpt).hiddenSet.footprint}")
841+
capt.println(i"sep check def ${tree.symbol}: ${tree.tpt} with ${captures(tree.tpt).hiddenSet.footprint()}")
852842
pushDef(tree, captures(tree.tpt).hiddenSet.deductSymRefs(tree.symbol))
853843

854844
def inSection[T](op: => T)(using Context): T =
@@ -869,7 +859,7 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser:
869859
case tree @ Select(qual, _) if tree.symbol.is(Method) && tree.symbol.hasAnnotation(defn.ConsumeAnnot) =>
870860
traverseChildren(tree)
871861
checkConsumedRefs(
872-
captures(qual).footprint, qual.nuType,
862+
captures(qual).footprint(), qual.nuType,
873863
TypeRole.Qualifier(qual, tree.symbol),
874864
i"call prefix of @consume ${tree.symbol} refers to", qual.srcPos)
875865
case tree: GenericApply =>

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

+7
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
-- Error: tests/neg-custom-args/captures/sep-counter.scala:12:19 -------------------------------------------------------
2+
12 | def mkCounter(): Pair[Ref^, Ref^] = // error
3+
| ^^^^^^^^^^^^^^^^
4+
| Separation failure in method mkCounter's result type Pair[box Ref^, box Ref^].
5+
| One part, box Ref^, hides capabilities {cap}.
6+
| Another part, box Ref^, captures capabilities {cap}.
7+
| The two sets overlap at cap of value c.

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

+16
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,16 @@
1+
import caps.Mutable
2+
import caps.cap
3+
4+
class Ref extends Mutable:
5+
var x = 0
6+
def get: Int = x
7+
mut def put(y: Int): Unit = x = y
8+
9+
class Pair[+X, +Y](val fst: X, val snd: Y)
10+
11+
def test() =
12+
def mkCounter(): Pair[Ref^, Ref^] = // error
13+
val c = Ref()
14+
val p: Pair[Ref^{c}, Ref^{c}] = Pair(c, c)
15+
//val q: Pair[Ref^, Ref^] = p
16+
p

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

+2-2
Original file line numberDiff line numberDiff line change
@@ -29,8 +29,8 @@
2929
13 |def bad: Pair[Ref^, Ref^] = // error: overlap at r1*, r0
3030
| ^^^^^^^^^^^^^^^^
3131
| Separation failure in method bad's result type Pair[box Ref^, box Ref^].
32-
| One part, box Ref^, hides capabilities {r1*, r0}.
33-
| Another part, box Ref^, captures capabilities {r1*, r0}.
32+
| One part, box Ref^, hides capabilities {cap, cap, r1*, r0}.
33+
| Another part, box Ref^, captures capabilities {cap, cap, r1*, r0}.
3434
| The two sets overlap at {r1*, r0}.
3535
-- Error: tests/neg-custom-args/captures/sep-pairs.scala:44:18 ---------------------------------------------------------
3636
44 | val sameToPair: Pair[Ref^, Ref^] = Pair(fstSame, sndSame) // error

0 commit comments

Comments
 (0)