Skip to content

Commit bc93c9e

Browse files
oderskyodersky
committed
Drop old footprint and overlap logic.
1 parent bab1ef7 commit bc93c9e

File tree

3 files changed

+19
-44
lines changed

3 files changed

+19
-44
lines changed

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

Lines changed: 16 additions & 41 deletions
Original file line numberDiff line numberDiff line change
@@ -170,24 +170,6 @@ object SepCheck:
170170
private def nonPeaks(using Context): Refs =
171171
refs.filter(!_.isTerminalCapability)
172172

173-
/** The footprint of a set of references `refs` the smallest set `F` such that
174-
* 1. all capabilities in `refs` satisfying (1) are in `F`
175-
* 2. if `f in F` then the footprint of `f`'s info is also in `F`.
176-
*/
177-
private def oldFootprint(using Context): Refs =
178-
if ccConfig.newScheme then
179-
directFootprint.nonPeaks
180-
else
181-
def retain(ref: Capability) = !ref.isTerminalCapability
182-
def recur(elems: Refs, newElems: List[Capability]): Refs = newElems match
183-
case newElem :: newElems1 =>
184-
val superElems = newElem.captureSetOfInfo.elems.filter: superElem =>
185-
retain(superElem) && !elems.contains(superElem)
186-
recur(elems ++ superElems, newElems1 ++ superElems.toList)
187-
case Nil => elems
188-
val elems: Refs = refs.filter(retain)
189-
recur(elems, elems.toList)
190-
191173
/** The footprint of a set of capabilities `refs` is the closure
192174
* of `refs` under `_.captureSetOfInfo`, dropping any shared terminal
193175
* capabilities. If `followHidden` is true, we close under both
@@ -371,24 +353,15 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser:
371353

372354
// ---- Error reporting TODO Once these are stabilized, move to messages -----" +
373355

374-
def sharedPeaksStr(shared: Refs)(using Context): String =
356+
def overlapStr(hiddenSet: Refs, clashSet: Refs)(using Context): String =
357+
val hiddenFootprint = hiddenSet.directFootprint
358+
val clashFootprint = clashSet.directFootprint
359+
val shared = hiddenFootprint.overlapWith(clashFootprint).reduced
375360
shared.nth(0) match
376361
case fresh: FreshCap =>
377362
if fresh.hiddenSet.owner.exists then i"$fresh of ${fresh.hiddenSet.owner}" else i"$fresh"
378-
case other =>
379-
i"$other"
380-
381-
def overlapStr(hiddenSet: Refs, clashSet: Refs)(using Context): String =
382-
val hiddenFootprint = hiddenSet.oldFootprint
383-
val clashFootprint = clashSet.oldFootprint
384-
// The overlap of footprints, or, of this empty the set of shared peaks.
385-
// We prefer footprint overlap since it tends to be more informative.
386-
val overlap = hiddenFootprint.overlapWith(clashFootprint)
387-
if !overlap.isEmpty then i"${CaptureSet(overlap)}"
388-
else
389-
val sharedPeaks = hiddenSet.allPeaks.sharedPeaks(clashSet.allPeaks)
390-
assert(!sharedPeaks.isEmpty, i"no overlap for $hiddenSet vs $clashSet")
391-
sharedPeaksStr(sharedPeaks)
363+
case _ =>
364+
i"${CaptureSet(shared)}"
392365

393366
/** Report a separation failure in an application `fn(args)`
394367
* @param fn the function
@@ -430,6 +403,8 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser:
430403
else i" with type ${clashing.nuType}"
431404
val hiddenSet = formalCaptures(polyArg).transHiddenSet
432405
val clashSet = deepCaptures(clashing)
406+
val hiddenFootprint = hiddenSet.directFootprint
407+
val clashFootprint = clashSet.directFootprint
433408
report.error(
434409
em"""Separation failure: argument of type ${polyArg.nuType}
435410
|to $funStr
@@ -438,10 +413,10 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser:
438413
|Some of these overlap with the captures of the ${clashArgStr.trim}$clashTypeStr.
439414
|
440415
| Hidden set of current argument : ${CaptureSet(hiddenSet)}
441-
| Hidden footprint of current argument : ${CaptureSet(hiddenSet.oldFootprint)}
416+
| Hidden footprint of current argument : ${CaptureSet(hiddenFootprint.nonPeaks)}
442417
| Capture set of $clashArgStr : ${CaptureSet(clashSet)}
443-
| Footprint set of $clashArgStr : ${CaptureSet(clashSet.oldFootprint)}
444-
| The two sets overlap at : ${overlapStr(hiddenSet, clashSet)}""",
418+
| Footprint set of $clashArgStr : ${CaptureSet(clashFootprint.nonPeaks)}
419+
| The two sets overlap at : ${overlapStr(hiddenFootprint, clashFootprint)}""",
445420
polyArg.srcPos)
446421

447422
/** Report a use/definition failure, where a previously hidden capability is
@@ -720,7 +695,7 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser:
720695
val captured = genPart.deepCaptureSet.elems
721696
val hiddenSet = captured.transHiddenSet.pruned
722697
val clashSet = otherPart.deepCaptureSet.elems
723-
val deepClashSet = (clashSet.oldFootprint ++ clashSet.transHiddenSet).pruned
698+
val deepClashSet = clashSet.completeFootprint.nonPeaks.pruned
724699
report.error(
725700
em"""Separation failure in ${role.description} $tpe.
726701
|One part, $genPart, hides capabilities ${CaptureSet(hiddenSet)}.
@@ -823,11 +798,11 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser:
823798
// "see through them" when we look at hidden sets.
824799
then
825800
val refs = tpe.deepCaptureSet.elems
826-
val toCheck = refs.transHiddenSet.oldFootprint.deduct(refs.oldFootprint)
801+
val toCheck = refs.transHiddenSet.directFootprint.nonPeaks.deduct(refs.directFootprint.nonPeaks)
827802
checkConsumedRefs(toCheck, tpe, role, i"${role.description} $tpe hides", pos)
828803
case TypeRole.Argument(arg) =>
829804
if tpe.hasAnnotation(defn.ConsumeAnnot) then
830-
val capts = spanCaptures(arg).oldFootprint
805+
val capts = spanCaptures(arg).directFootprint.nonPeaks
831806
checkConsumedRefs(capts, tpe, role, i"argument to consume parameter with type ${arg.nuType} refers to", pos)
832807
case _ =>
833808

@@ -952,7 +927,7 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser:
952927
def checkValOrDefDef(tree: ValOrDefDef)(using Context): Unit =
953928
if !tree.symbol.isOneOf(TermParamOrAccessor) && !isUnsafeAssumeSeparate(tree.rhs) then
954929
checkType(tree.tpt, tree.symbol)
955-
capt.println(i"sep check def ${tree.symbol}: ${tree.tpt} with ${spanCaptures(tree.tpt).transHiddenSet.oldFootprint}")
930+
capt.println(i"sep check def ${tree.symbol}: ${tree.tpt} with ${spanCaptures(tree.tpt).transHiddenSet.directFootprint}")
956931
pushDef(tree, spanCaptures(tree.tpt).transHiddenSet.deductSymRefs(tree.symbol))
957932

958933
def inSection[T](op: => T)(using Context): T =
@@ -989,7 +964,7 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser:
989964
case tree @ Select(qual, _) if tree.symbol.is(Method) && tree.symbol.isConsumeParam =>
990965
traverseChildren(tree)
991966
checkConsumedRefs(
992-
spanCaptures(qual).oldFootprint, qual.nuType,
967+
spanCaptures(qual).directFootprint.nonPeaks, qual.nuType,
993968
TypeRole.Qualifier(qual, tree.symbol),
994969
i"call prefix of consume ${tree.symbol} refers to", qual.srcPos)
995970
case tree: GenericApply =>

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@
33
| ^^^^^^^^^^^^^^^^
44
|Separation failure in method mkCounter's result type Pair[Ref^, Ref^²].
55
|One part, Ref^, hides capabilities {c, cap, cap²}.
6-
|Another part, Ref^², captures capabilities {c, cap, cap²}.
6+
|Another part, Ref^², captures capabilities {c}.
77
|The two sets overlap at {c}.
88
|
99
|where: ^ refers to a fresh root capability classified as Mutable in the result type of method mkCounter

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

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -13,7 +13,7 @@
1313
| ^^^^^^^^^^^^^^^^
1414
| Separation failure in method bad's result type Pair[Ref^, Ref^²].
1515
| One part, Ref^, hides capabilities {r1*, cap, cap², r0}.
16-
| Another part, Ref^², captures capabilities {r1*, cap, cap², r0}.
16+
| Another part, Ref^², captures capabilities {r1*, r0}.
1717
| The two sets overlap at {r1*, r0}.
1818
|
1919
| where: ^ refers to a fresh root capability classified as Mutable in the result type of method bad
@@ -25,7 +25,7 @@
2525
| ^^^^^^^^^^^^^^^^
2626
| Separation failure in value sameToPair's type Pair[Ref^, Ref^²].
2727
| One part, Ref^, hides capabilities {fstSame}.
28-
| Another part, Ref^², captures capabilities {sndSame}.
28+
| Another part, Ref^², captures capabilities {sndSame, same.snd*}.
2929
| The two sets overlap at cap of value same.
3030
|
3131
| where: ^ refers to a fresh root capability classified as Mutable in the type of value sameToPair

0 commit comments

Comments
 (0)