Skip to content

Commit b9fdf60

Browse files
oderskyodersky
committed
Simplify footprint in SepChecks
1 parent 98fc4b6 commit b9fdf60

File tree

3 files changed

+33
-27
lines changed

3 files changed

+33
-27
lines changed

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

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1231,7 +1231,8 @@ class CheckCaptures extends Recheck, SymTransformer:
12311231
val saved = curEnv
12321232
tree match
12331233
case _: RefTree | closureDef(_) if pt.isBoxedCapturing =>
1234-
curEnv = Env(curEnv.owner, EnvKind.Boxed, CaptureSet.Var(curEnv.owner, level = ccState.currentLevel), curEnv)
1234+
curEnv = Env(curEnv.owner, EnvKind.Boxed,
1235+
CaptureSet.Var(curEnv.owner, level = ccState.currentLevel), curEnv)
12351236
case _ =>
12361237
val res =
12371238
try
@@ -1575,6 +1576,7 @@ class CheckCaptures extends Recheck, SymTransformer:
15751576
&& !expected.isSingleton
15761577
&& !expected.isBoxedCapturing =>
15771578
actual.derivedCapturingType(parent, refs.readOnly)
1579+
.showing(i"improv ro $actual vs $expected = $result", capt)
15781580
case _ =>
15791581
actual
15801582

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

Lines changed: 29 additions & 25 deletions
Original file line numberDiff line numberDiff line change
@@ -165,12 +165,11 @@ object SepCheck:
165165
extension (refs: Refs)
166166

167167
/** The footprint of a set of references `refs` the smallest set `F` such that
168-
* 1. if includeMax is false then no maximal capability is in `F`
169-
* 2. all capabilities in `refs` satisfying (1) are in `F`
170-
* 3. if `f in F` then the footprint of `f`'s info is also in `F`.
168+
* 1. all capabilities in `refs` satisfying (1) are in `F`
169+
* 2. if `f in F` then the footprint of `f`'s info is also in `F`.
171170
*/
172-
private def footprint(includeMax: Boolean = false)(using Context): Refs =
173-
def retain(ref: Capability) = includeMax || !ref.isTerminalCapability
171+
private def footprint(using Context): Refs =
172+
def retain(ref: Capability) = !ref.isTerminalCapability
174173
def recur(elems: Refs, newElems: List[Capability]): Refs = newElems match
175174
case newElem :: newElems1 =>
176175
val superElems = newElem.captureSetOfInfo.elems.filter: superElem =>
@@ -326,15 +325,14 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser:
326325
i"$other"
327326

328327
def overlapStr(hiddenSet: Refs, clashSet: Refs)(using Context): String =
329-
val hiddenFootprint = hiddenSet.footprint()
330-
val clashFootprint = clashSet.footprint()
328+
val hiddenFootprint = hiddenSet.footprint
329+
val clashFootprint = clashSet.footprint
331330
// The overlap of footprints, or, of this empty the set of shared peaks.
332331
// We prefer footprint overlap since it tends to be more informative.
333332
val overlap = hiddenFootprint.overlapWith(clashFootprint)
334333
if !overlap.isEmpty then i"${CaptureSet(overlap)}"
335334
else
336-
val sharedPeaks = hiddenSet.footprint(includeMax = true).sharedWith:
337-
clashSet.footprint(includeMax = true)
335+
val sharedPeaks = hiddenSet.peaks.sharedWith(clashSet.peaks)
338336
assert(!sharedPeaks.isEmpty, i"no overlap for $hiddenSet vs $clashSet")
339337
sharedPeaksStr(sharedPeaks)
340338

@@ -386,9 +384,9 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser:
386384
|Some of these overlap with the captures of the ${clashArgStr.trim}$clashTypeStr.
387385
|
388386
| Hidden set of current argument : ${CaptureSet(hiddenSet)}
389-
| Hidden footprint of current argument : ${CaptureSet(hiddenSet.footprint())}
387+
| Hidden footprint of current argument : ${CaptureSet(hiddenSet.footprint)}
390388
| Capture set of $clashArgStr : ${CaptureSet(clashSet)}
391-
| Footprint set of $clashArgStr : ${CaptureSet(clashSet.footprint())}
389+
| Footprint set of $clashArgStr : ${CaptureSet(clashSet.footprint)}
392390
| The two sets overlap at : ${overlapStr(hiddenSet, clashSet)}""",
393391
polyArg.srcPos)
394392

@@ -679,7 +677,7 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser:
679677
val captured = genPart.deepCaptureSet.elems
680678
val hiddenSet = captured.hiddenSet.pruned
681679
val clashSet = otherPart.deepCaptureSet.elems
682-
val deepClashSet = (clashSet.footprint() ++ clashSet.hiddenSet).pruned
680+
val deepClashSet = (clashSet.footprint ++ clashSet.hiddenSet).pruned
683681
report.error(
684682
em"""Separation failure in ${role.description} $tpe.
685683
|One part, $genPart, hides capabilities ${CaptureSet(hiddenSet)}.
@@ -782,11 +780,11 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser:
782780
// "see through them" when we look at hidden sets.
783781
then
784782
val refs = tpe.deepCaptureSet.elems
785-
val toCheck = refs.hiddenSet.footprint().deduct(refs.footprint())
783+
val toCheck = refs.hiddenSet.footprint.deduct(refs.footprint)
786784
checkConsumedRefs(toCheck, tpe, role, i"${role.description} $tpe hides", pos)
787785
case TypeRole.Argument(arg) =>
788786
if tpe.hasAnnotation(defn.ConsumeAnnot) then
789-
val capts = captures(arg).footprint()
787+
val capts = captures(arg).footprint
790788
checkConsumedRefs(capts, tpe, role, i"argument to @consume parameter with type ${arg.nuType} refers to", pos)
791789
case _ =>
792790

@@ -881,7 +879,7 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser:
881879
def checkValOrDefDef(tree: ValOrDefDef)(using Context): Unit =
882880
if !tree.symbol.isOneOf(TermParamOrAccessor) && !isUnsafeAssumeSeparate(tree.rhs) then
883881
checkType(tree.tpt, tree.symbol)
884-
capt.println(i"sep check def ${tree.symbol}: ${tree.tpt} with ${captures(tree.tpt).hiddenSet.footprint()}")
882+
capt.println(i"sep check def ${tree.symbol}: ${tree.tpt} with ${captures(tree.tpt).hiddenSet.footprint}")
885883
pushDef(tree, captures(tree.tpt).hiddenSet.deductSymRefs(tree.symbol))
886884

887885
def inSection[T](op: => T)(using Context): T =
@@ -894,6 +892,13 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser:
894892

895893
def traverseSection[T](tree: Tree)(using Context) = inSection(traverseChildren(tree))
896894

895+
/** Should separatiion checking be disabled for the body of this method?
896+
*/
897+
def skippable(sym: Symbol)(using Context): Boolean =
898+
sym.isInlineMethod
899+
// We currently skip inline method bodies since these seem to generan
900+
// spurious recheck completions. Test case is i20237.scala
901+
897902
/** Traverse `tree` and perform separation checks everywhere */
898903
def traverse(tree: Tree)(using Context): Unit =
899904
if !isUnsafeAssumeSeparate(tree) then trace(i"checking separate $tree"):
@@ -902,7 +907,7 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser:
902907
case tree @ Select(qual, _) if tree.symbol.is(Method) && tree.symbol.isConsumeParam =>
903908
traverseChildren(tree)
904909
checkConsumedRefs(
905-
captures(qual).footprint(), qual.nuType,
910+
captures(qual).footprint, qual.nuType,
906911
TypeRole.Qualifier(qual, tree.symbol),
907912
i"call prefix of @consume ${tree.symbol} refers to", qual.srcPos)
908913
case tree: GenericApply =>
@@ -916,15 +921,14 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser:
916921
traverseChildren(tree)
917922
checkValOrDefDef(tree)
918923
case tree: DefDef =>
919-
if tree.symbol.isInlineMethod then
920-
// We currently skip inline method since these seem to generate
921-
// spurious recheck completions. Test case is i20237.scala
922-
capt.println(i"skipping sep check of inline def ${tree.symbol}")
923-
else inSection:
924-
consumed.segment:
925-
for params <- tree.paramss; case param: ValDef <- params do
926-
pushDef(param, emptyRefs)
927-
traverseChildren(tree)
924+
if skippable(tree.symbol) then
925+
capt.println(i"skipping sep check of ${tree.symbol}")
926+
else
927+
inSection:
928+
consumed.segment:
929+
for params <- tree.paramss; case param: ValDef <- params do
930+
pushDef(param, emptyRefs)
931+
traverseChildren(tree)
928932
checkValOrDefDef(tree)
929933
case If(cond, thenp, elsep) =>
930934
traverse(cond)

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

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

0 commit comments

Comments
 (0)