Skip to content

Commit d2e276c

Browse files
committed
Fine-tune pruning for consume checks of arguments
Deduct explicit refs of actual as opposed to formal argument type.
1 parent a6f1ab2 commit d2e276c

File tree

3 files changed

+49
-27
lines changed

3 files changed

+49
-27
lines changed

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

Lines changed: 14 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -567,24 +567,16 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser:
567567
if pos != null then consumeError(ref, pos, tree.srcPos)
568568
end checkUse
569569

570-
/** If `tp` denotes some version of a singleton type `x.type` the set `{x}`
570+
/** If `tp` denotes some version of a singleton capture ref `x.type` the set `{x, x*}`
571571
* otherwise the empty set.
572572
*/
573-
def explicitRefs(tp: Type): Refs = tp match
574-
case tp: (TermRef | ThisType) => SimpleIdentitySet(tp)
573+
def explicitRefs(tp: Type)(using Context): Refs = tp match
574+
case tp: (TermRef | ThisType) if tp.isTrackableRef => SimpleIdentitySet(tp, tp.reach)
575575
case AnnotatedType(parent, _) => explicitRefs(parent)
576576
case AndType(tp1, tp2) => explicitRefs(tp1) ++ explicitRefs(tp2)
577577
case OrType(tp1, tp2) => explicitRefs(tp1) ** explicitRefs(tp2)
578578
case _ => emptyRefs
579579

580-
/** Deduct some elements from `refs` according to the role of the checked type `tpe`:
581-
* - If the the type apears as a (result-) type of a definition of `x`, deduct
582-
* `x` and `x*`.
583-
* - If `tpe` is morally a singleton type deduct it as well.
584-
*/
585-
def prune(refs: Refs, tpe: Type, role: TypeRole)(using Context): Refs =
586-
refs.deductSymFootprint(role.dclSym).deduct(explicitRefs(tpe))
587-
588580
/** Check validity of consumed references `refsToCheck`. The references are consumed
589581
* because they are hidden in a Fresh result type or they are referred
590582
* to in an argument to a @consume parameter or in a prefix of a @consume method --
@@ -611,7 +603,7 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser:
611603
def checkConsumedRefs(refsToCheck: Refs, tpe: Type, role: TypeRole, descr: => String, pos: SrcPos)(using Context) =
612604
val badParams = mutable.ListBuffer[Symbol]()
613605
def currentOwner = role.dclSym.orElse(ctx.owner)
614-
for hiddenRef <- prune(refsToCheck, tpe, role) do
606+
for hiddenRef <- refsToCheck.deductSymRefs(role.dclSym).deduct(explicitRefs(tpe)) do
615607
if !hiddenRef.derivesFromSharedCapability then
616608
hiddenRef.pathRoot match
617609
case ref: TermRef =>
@@ -662,8 +654,17 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser:
662654
*/
663655
def checkType(tpe: Type, pos: SrcPos, role: TypeRole)(using Context): Unit =
664656

657+
/** Deduct some elements from `refs` according to the role of the checked type `tpe`:
658+
* - If the the type apears as a (result-) type of a definition of `x`, deduct
659+
* `x` and `x*`.
660+
* - If the checked type (or, for arguments, the actual type of the argument)
661+
* is morally a singleton type `y.type` deduct `y` and `y*` as well.
662+
*/
665663
extension (refs: Refs) def pruned =
666-
refs.deductSymRefs(role.dclSym).deduct(explicitRefs(tpe))
664+
val deductedType = role match
665+
case TypeRole.Argument(arg) => arg.tpe
666+
case _ => tpe
667+
refs.deductSymRefs(role.dclSym).deduct(explicitRefs(deductedType))
667668

668669
def sepTypeError(parts: List[Type], genPart: Type, otherPart: Type): Unit =
669670
val captured = genPart.deepCaptureSet.elems
Lines changed: 20 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -1,28 +1,34 @@
1-
-- Error: tests/neg-custom-args/captures/sep-consume.scala:17:2 --------------------------------------------------------
2-
17 | x.put(42) // error
1+
-- Error: tests/neg-custom-args/captures/sep-consume.scala:19:2 --------------------------------------------------------
2+
19 | x.put(42) // error
33
| ^
44
| Separation failure: Illegal access to (x : Ref^), which was passed to a
5-
| @consume parameter or was used as a prefix to a @consume method on line 16
5+
| @consume parameter or was used as a prefix to a @consume method on line 18
66
| and therefore is no longer available.
7-
-- Error: tests/neg-custom-args/captures/sep-consume.scala:18:2 --------------------------------------------------------
8-
18 | x.get // error
7+
-- Error: tests/neg-custom-args/captures/sep-consume.scala:20:2 --------------------------------------------------------
8+
20 | x.get // error
99
| ^
1010
| Separation failure: Illegal access to x.rd, which was passed to a
11-
| @consume parameter or was used as a prefix to a @consume method on line 16
11+
| @consume parameter or was used as a prefix to a @consume method on line 18
1212
| and therefore is no longer available.
13-
-- Error: tests/neg-custom-args/captures/sep-consume.scala:19:16 -------------------------------------------------------
14-
19 | par(rx, () => x.put(42)) // error
13+
-- Error: tests/neg-custom-args/captures/sep-consume.scala:21:16 -------------------------------------------------------
14+
21 | par(rx, () => x.put(42)) // error
1515
| ^
1616
| Separation failure: Illegal access to (x : Ref^), which was passed to a
17-
| @consume parameter or was used as a prefix to a @consume method on line 16
17+
| @consume parameter or was used as a prefix to a @consume method on line 18
1818
| and therefore is no longer available.
19-
-- Error: tests/neg-custom-args/captures/sep-consume.scala:20:16 -------------------------------------------------------
20-
20 | par(rx, () => x.get) // error
19+
-- Error: tests/neg-custom-args/captures/sep-consume.scala:22:16 -------------------------------------------------------
20+
22 | par(rx, () => x.get) // error
2121
| ^
2222
| Separation failure: Illegal access to x.rd, which was passed to a
23-
| @consume parameter or was used as a prefix to a @consume method on line 16
23+
| @consume parameter or was used as a prefix to a @consume method on line 18
2424
| and therefore is no longer available.
25-
-- Error: tests/neg-custom-args/captures/sep-consume.scala:24:16 -------------------------------------------------------
26-
24 | def foo = bad(f) // error
25+
-- Error: tests/neg-custom-args/captures/sep-consume.scala:26:16 -------------------------------------------------------
26+
26 | def foo = bad(f) // error
2727
| ^
2828
| Separation failure: argument to @consume parameter with type (f : () ->{x.rd} Unit) refers to non-local value f
29+
-- Error: tests/neg-custom-args/captures/sep-consume.scala:34:12 -------------------------------------------------------
30+
34 | println(p.fst.get) // errorSep
31+
| ^^^^^
32+
| Separation failure: Illegal access to p.fst*, which was passed to a
33+
| @consume parameter or was used as a prefix to a @consume method on line 33
34+
| and therefore is no longer available.

tests/neg-custom-args/captures/sep-consume.scala

Lines changed: 15 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -6,6 +6,8 @@ class Ref extends Mutable:
66
def get: Int = _data
77
mut def put(x: Int): Unit = _data = x
88

9+
case class Pair[+A, +B](fst: A, snd: B)
10+
911
// require f and g to be non-interfering
1012
def par(f: () => Unit, g: () => Unit): Unit = ???
1113

@@ -24,3 +26,16 @@ def test3(@consume x: Ref^): Unit =
2426
def foo = bad(f) // error
2527
foo()
2628
foo()
29+
30+
def test4(@consume @use p: Pair[Ref^, Ref^]): Unit =
31+
val x: Ref^{p.fst*} = p.fst
32+
val y: Ref^{p.snd*} = p.snd
33+
badp(Pair(x, y))
34+
println(p.fst.get) // errorSep
35+
36+
def badp(@consume p: Pair[Ref^, Ref^]): Unit = ()
37+
38+
def test5(@consume @use p: Pair[Ref^, Ref^]): Unit =
39+
badp(p) // ok
40+
println(p.fst.get) // ok, but should be error
41+

0 commit comments

Comments
 (0)