Skip to content

Commit 8aeec6a

Browse files
committed
Use the whole selection tree for markFree
Needed for use checking, since if we just take the leftmost prefix we sometimes end up with a `this`.
1 parent 339581e commit 8aeec6a

File tree

6 files changed

+88
-17
lines changed

6 files changed

+88
-17
lines changed

compiler/src/dotty/tools/dotc/cc/CaptureSet.scala

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -966,8 +966,7 @@ object CaptureSet:
966966
case elem: FreshCap
967967
if !nestedOK
968968
&& !elems.contains(elem)
969-
&& !owner.isAnonymousFunction
970-
&& ccConfig.newScheme =>
969+
&& !owner.isAnonymousFunction =>
971970
def fail = i"attempting to add $elem to $this"
972971
def hideIn(fc: FreshCap): Unit =
973972
assert(elem.tryClassifyAs(fc.hiddenSet.classifier), fail)

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

Lines changed: 31 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -102,7 +102,7 @@ object CheckCaptures:
102102
end SubstParamsMap
103103

104104
/** A prototype that indicates selection with an immutable value */
105-
class PathSelectionProto(val sym: Symbol, val pt: Type)(using Context) extends WildcardSelectionProto
105+
class PathSelectionProto(val select: Select, val pt: Type)(using Context) extends WildcardSelectionProto
106106

107107
/** Check that a @retains annotation only mentions references that can be tracked.
108108
* This check is performed at Typer.
@@ -653,11 +653,15 @@ class CheckCaptures extends Recheck, SymTransformer:
653653
// If ident refers to a parameterless method, charge its cv to the environment
654654
includeCallCaptures(sym, sym.info, tree)
655655
else if !sym.isStatic then
656-
markFree(sym, pathRef(sym.termRef, pt), tree)
656+
if ccConfig.newScheme && sym.exists
657+
then markPathFree(sym.termRef, pt, tree)
658+
else markFree(sym, pathRef(sym.termRef, pt), tree)
657659
mapResultRoots(super.recheckIdent(tree, pt), tree.symbol)
658660

659661
override def recheckThis(tree: This, pt: Type)(using Context): Type =
660-
markFree(pathRef(tree.tpe.asInstanceOf[ThisType], pt), tree)
662+
if ccConfig.newScheme
663+
then markPathFree(tree.tpe.asInstanceOf[ThisType], pt, tree)
664+
else markFree(pathRef(tree.tpe.asInstanceOf[ThisType], pt), tree)
661665
super.recheckThis(tree, pt)
662666

663667
/** Add all selections and also any `.rd modifier implied by the expected
@@ -668,18 +672,38 @@ class CheckCaptures extends Recheck, SymTransformer:
668672
private def pathRef(base: TermRef | ThisType, pt: Type)(using Context): Capability =
669673
def addSelects(ref: TermRef | ThisType, pt: Type): Capability = pt match
670674
case pt: PathSelectionProto if ref.isTracked =>
671-
if pt.sym.isReadOnlyMethod then
675+
if pt.select.symbol.isReadOnlyMethod then
672676
ref.readOnly
673677
else
674678
// if `ref` is not tracked then the selection could not give anything new
675679
// class SerializationProxy in stdlib-cc/../LazyListIterable.scala has an example where this matters.
676-
addSelects(ref.select(pt.sym).asInstanceOf[TermRef], pt.pt)
680+
addSelects(ref.select(pt.select.symbol).asInstanceOf[TermRef], pt.pt)
677681
case _ => ref
678682
val ref: Capability = addSelects(base, pt)
679683
if ref.derivesFromMutable && pt.isValueType && !pt.isMutableType
680684
then ref.readOnly
681685
else ref
682686

687+
/** Add all selections and also any `.rd modifier implied by the expected
688+
* type `pt` to `base`. Example:
689+
* If we have `x` and the expected type says we select that with `.a.b`
690+
* where `b` is a read-only method, we charge `x.a.b.rd` instead of `x`.
691+
*/
692+
private def markPathFree(ref: TermRef | ThisType, pt: Type, tree: Tree)(using Context): Unit =
693+
pt match
694+
case pt: PathSelectionProto if ref.isTracked =>
695+
// if `ref` is not tracked then the selection could not give anything new
696+
// class SerializationProxy in stdlib-cc/../LazyListIterable.scala has an example where this matters.
697+
if pt.select.symbol.isReadOnlyMethod then
698+
markFree(ref.readOnly, tree)
699+
else
700+
markPathFree(ref.select(pt.select.symbol).asInstanceOf[TermRef], pt.pt, pt.select)
701+
case _ =>
702+
if ref.derivesFromMutable && pt.isValueType && !pt.isMutableType then
703+
markFree(ref.readOnly, tree)
704+
else
705+
markFree(ref, tree)
706+
683707
/** The expected type for the qualifier of a selection. If the selection
684708
* could be part of a capability path or is a a read-only method, we return
685709
* a PathSelectionProto.
@@ -688,7 +712,7 @@ class CheckCaptures extends Recheck, SymTransformer:
688712
val sym = tree.symbol
689713
if !sym.isOneOf(UnstableValueFlags) && !sym.isStatic
690714
|| sym.isReadOnlyMethod
691-
then PathSelectionProto(sym, pt)
715+
then PathSelectionProto(tree, pt)
692716
else super.selectionProto(tree, pt)
693717

694718
/** A specialized implementation of the selection rule.
@@ -1820,7 +1844,7 @@ class CheckCaptures extends Recheck, SymTransformer:
18201844
private def noWiden(actual: Type, expected: Type)(using Context): Boolean =
18211845
actual.isSingleton
18221846
&& expected.match
1823-
case expected: PathSelectionProto => !expected.sym.isOneOf(UnstableValueFlags)
1847+
case expected: PathSelectionProto => !expected.select.symbol.isOneOf(UnstableValueFlags)
18241848
case _ => expected.stripCapturing.isSingleton || expected == LhsProto
18251849

18261850
/** Adapt `actual` type to `expected` type. This involves:

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

Lines changed: 13 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -431,6 +431,7 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser:
431431
def sepUseError(tree: Tree, clashingDef: ValOrDefDef | Null, used: Refs, hidden: Refs)(using Context): Unit =
432432
if clashingDef != null then
433433
def resultStr = if clashingDef.isInstanceOf[DefDef] then " result" else ""
434+
//println(i"sep use error: previous ${clashingDef.tpt.nuType}, ref = $used")
434435
report.error(
435436
em"""Separation failure: Illegal access to ${overlapStr(hidden, used)} which is hidden by the previous definition
436437
|of ${clashingDef.symbol} with$resultStr type ${clashingDef.tpt.nuType}.
@@ -568,22 +569,30 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser:
568569
val usedPeaks = used.allPeaks
569570
val overlap = defsShadow.allPeaks.sharedPeaks(usedPeaks)
570571
if !defsShadow.allPeaks.sharedPeaks(usedPeaks).isEmpty then
571-
val sym = tree.symbol
572-
572+
// Drop all Selects unless they select from a `this`
573+
def pathRoot(tree: Tree): Tree = tree match
574+
case Select(This(_), _) => tree
575+
case Select(prefix, _) => pathRoot(prefix)
576+
case _ => tree
577+
578+
val rootSym = pathRoot(tree).symbol
579+
573580
def findClashing(prevDefs: List[DefInfo]): Option[DefInfo] = prevDefs match
574581
case prevDef :: prevDefs1 =>
575-
if prevDef.symbol == sym then Some(prevDef)
582+
if prevDef.symbol == rootSym then Some(prevDef)
576583
else if !prevDef.hiddenPeaks.sharedPeaks(usedPeaks).isEmpty then Some(prevDef)
577584
else findClashing(prevDefs1)
578585
case Nil =>
579586
None
580587

581588
findClashing(previousDefs) match
582589
case Some(clashing) =>
583-
if clashing.symbol != sym then
590+
//println(i"check use $tree, $used, $rootSym, ${clashing.symbol}")
591+
if clashing.symbol != rootSym then
584592
sepUseError(tree, clashing.tree, used, clashing.hidden)
585593
case None =>
586594
sepUseError(tree, null, used, defsShadow)
595+
end if
587596

588597
for ref <- used do
589598
val pos = consumed.clashing(ref)
Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,16 @@
1+
-- Error: tests/neg-custom-args/captures/fresh-counter.scala:22:6 ------------------------------------------------------
2+
22 | par(i, d) // error: separation failure
3+
| ^
4+
|Separation failure: argument of type (i : () ->{c.incr} Unit)
5+
|to method par: (p1: () => Unit, p2: () => Unit): Unit
6+
|corresponds to capture-polymorphic formal parameter p1 of type () => Unit
7+
|and hides capabilities {i}.
8+
|Some of these overlap with the captures of the second argument with type (d : () ->{c.decr} Unit).
9+
|
10+
| Hidden set of current argument : {i}
11+
| Hidden footprint of current argument : {i, c.incr, c.count}
12+
| Capture set of second argument : {d}
13+
| Footprint set of second argument : {d, c.decr, c.count}
14+
| The two sets overlap at : {c.count}
15+
|
16+
|where: => refers to a fresh root capability created in method test when checking argument to parameter p1 of method par
Lines changed: 23 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,23 @@
1+
import caps.Mutable
2+
import caps.cap
3+
4+
class Ref extends Mutable:
5+
var x = 0
6+
def get: Int = x
7+
update def put(y: Int): Unit = x = y
8+
9+
class Counter:
10+
private val count: Ref^ = Ref()
11+
val incr = () =>
12+
count.put(count.get + 1)
13+
val decr = () =>
14+
count.put(count.get - 1)
15+
16+
def par(p1: () => Unit, p2: () => Unit) = ()
17+
18+
def test() =
19+
val c = Counter()
20+
val i = c.incr
21+
val d = c.decr
22+
par(i, d) // error: separation failure
23+

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

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -68,17 +68,17 @@
6868
| ^² refers to a fresh root capability classified as Mutable in the type of value snd
6969
| ^³ refers to a fresh root capability in the type of value two
7070
| ^⁴ refers to a fresh root capability created in value twisted when checking argument to parameter x of method swapped
71-
-- Error: tests/neg-custom-args/captures/sep-pairs-unboxed.scala:58:22 -------------------------------------------------
71+
-- Error: tests/neg-custom-args/captures/sep-pairs-unboxed.scala:58:26 -------------------------------------------------
7272
58 | val twoOther = Pair(two.fst, two.snd) // error // error
73-
| ^^^
73+
| ^^^^^^^
7474
| Separation failure: Illegal access to {two.fst} which is hidden by the previous definition
7575
| of value twoCopy with type Pair^.
7676
| This type hides capabilities {two.fst, two.snd}
7777
|
7878
| where: ^ refers to a fresh root capability in the type of value twoCopy
79-
-- Error: tests/neg-custom-args/captures/sep-pairs-unboxed.scala:58:31 -------------------------------------------------
79+
-- Error: tests/neg-custom-args/captures/sep-pairs-unboxed.scala:58:35 -------------------------------------------------
8080
58 | val twoOther = Pair(two.fst, two.snd) // error // error
81-
| ^^^
81+
| ^^^^^^^
8282
| Separation failure: Illegal access to {two.snd} which is hidden by the previous definition
8383
| of value twoCopy with type Pair^.
8484
| This type hides capabilities {two.fst, two.snd}

0 commit comments

Comments
 (0)