Skip to content

Commit 339581e

Browse files
oderskyodersky
committed
Establish a "covers" relation between a fresh for an object
and a fresh for one of its fields.
1 parent ba1ef96 commit 339581e

File tree

6 files changed

+179
-5
lines changed

6 files changed

+179
-5
lines changed

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

Lines changed: 30 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -691,6 +691,8 @@ object Capabilities:
691691

692692
try (this eq y)
693693
|| maxSubsumes(y, canAddHidden = !vs.isOpen)
694+
// if vs is open, we should add new elements to the set containing `this`
695+
// instead of adding them to the hidden set of of `this`.
694696
|| y.match
695697
case y: TermRef =>
696698
y.prefix.match
@@ -773,6 +775,7 @@ object Capabilities:
773775
false
774776

775777
vs.ifNotSeen(this)(x.hiddenSet.elems.exists(_.subsumes(y)))
778+
|| x.coversFresh(y)
776779
|| x.acceptsLevelOf(y)
777780
&& classifierOK
778781
&& canAddHidden
@@ -839,15 +842,39 @@ object Capabilities:
839842
case _ =>
840843
false
841844
|| x.match
842-
case x: FreshCap if !seen.contains(x) =>
843-
seen.add(x)
844-
x.hiddenSet.exists(recur(_, y))
845+
case x: FreshCap =>
846+
if x.coversFresh(y) then true
847+
else if !seen.contains(x) then
848+
seen.add(x)
849+
x.hiddenSet.exists(recur(_, y))
850+
else false
845851
case Restricted(x1, _) => recur(x1, y)
846852
case _ => false
847853

848854
recur(this, y)
849855
end covers
850856

857+
/** `x eq y` or `x` is a fresh cap, `y` is a fresh cap with prefix
858+
* `p`, and there is a prefix of `p` that contains `x` in its
859+
* capture set.
860+
*/
861+
final def coversFresh(y: Capability)(using Context): Boolean =
862+
(this eq y) || this.match
863+
case x: FreshCap => y match
864+
case y: FreshCap =>
865+
x.origin match
866+
case Origin.InDecl(sym) =>
867+
def occursInPrefix(pre: Type): Boolean = pre match
868+
case pre @ TermRef(pre1, _) =>
869+
pre.symbol == sym
870+
&& pre.info.captureSet.elems.contains(x)
871+
|| occursInPrefix(pre1)
872+
case _ => false
873+
occursInPrefix(y.prefix)
874+
case _ => false
875+
case _ => false
876+
case _ => false
877+
851878
def assumedContainsOf(x: TypeRef)(using Context): SimpleIdentitySet[Capability] =
852879
CaptureSet.assumedContains.getOrElse(x, SimpleIdentitySet.empty)
853880

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

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1236,6 +1236,7 @@ object CaptureSet:
12361236

12371237
/** Add element to hidden set. */
12381238
def add(elem: Capability)(using ctx: Context, vs: VarState): Unit =
1239+
assert(elem ne owningCap)
12391240
includeElem(elem)
12401241

12411242
/** Apply function `f` to `elems` while setting `elems` to empty for the

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -221,7 +221,7 @@ object SepCheck:
221221
refs1.foreach: ref =>
222222
if !ref.isReadOnly then
223223
val coreRef = ref.stripRestricted
224-
if refs2.exists(_.stripRestricted.stripReadOnly eq coreRef) then
224+
if refs2.exists(_.stripRestricted.stripReadOnly.coversFresh(coreRef)) then
225225
acc += coreRef
226226
acc
227227
assert(refs.forall(_.isTerminalCapability))

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

Lines changed: 86 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,86 @@
1+
-- Error: tests/neg-custom-args/captures/sep-pairs-unboxed.scala:11:27 -------------------------------------------------
2+
11 |def mkPair(x: Ref^) = Pair(x, x) // error: separation failure
3+
| ^
4+
|Separation failure: argument of type (x : Ref^)
5+
|to constructor Pair: (fst: Ref^, snd: Ref^): Pair
6+
|corresponds to capture-polymorphic formal parameter fst of type Ref^²
7+
|and hides capabilities {x}.
8+
|Some of these overlap with the captures of the second argument with type (x : Ref^).
9+
|
10+
| Hidden set of current argument : {x}
11+
| Hidden footprint of current argument : {x}
12+
| Capture set of second argument : {x}
13+
| Footprint set of second argument : {x}
14+
| The two sets overlap at : {x}
15+
|
16+
|where: ^ refers to a fresh root capability classified as Mutable in the type of parameter x
17+
| ^² refers to a fresh root capability classified as Mutable created in method mkPair when checking argument to parameter fst of constructor Pair
18+
-- Error: tests/neg-custom-args/captures/sep-pairs-unboxed.scala:35:25 -------------------------------------------------
19+
35 | val twoCopy = Pair(two.fst, two.fst) // error
20+
| ^^^^^^^
21+
|Separation failure: argument of type (two.fst : Ref^)
22+
|to constructor Pair: (fst: Ref^, snd: Ref^): Pair
23+
|corresponds to capture-polymorphic formal parameter fst of type Ref^²
24+
|and hides capabilities {two.fst}.
25+
|Some of these overlap with the captures of the second argument with type (two.fst : Ref^).
26+
|
27+
| Hidden set of current argument : {two.fst}
28+
| Hidden footprint of current argument : {two.fst}
29+
| Capture set of second argument : {two.fst}
30+
| Footprint set of second argument : {two.fst}
31+
| The two sets overlap at : {two.fst}
32+
|
33+
|where: ^ refers to a fresh root capability classified as Mutable in the type of value fst
34+
| ^² refers to a fresh root capability classified as Mutable created in value twoCopy when checking argument to parameter fst of constructor Pair
35+
-- Error: tests/neg-custom-args/captures/sep-pairs-unboxed.scala:41:29 -------------------------------------------------
36+
41 | val twisted = PairPair(two.fst, two) // error
37+
| ^^^^^^^
38+
|Separation failure: argument of type (two.fst : Ref^)
39+
|to constructor PairPair: (fst: Ref^, snd: Pair^): PairPair
40+
|corresponds to capture-polymorphic formal parameter fst of type Ref^²
41+
|and hides capabilities {two.fst}.
42+
|Some of these overlap with the captures of the second argument with type (two : Pair{val fst: Ref^; val snd: Ref^}^).
43+
|
44+
| Hidden set of current argument : {two.fst}
45+
| Hidden footprint of current argument : {two.fst}
46+
| Capture set of second argument : {two*}
47+
| Footprint set of second argument : {two*}
48+
| The two sets overlap at : {two.cap of class Pair}
49+
|
50+
|where: ^ refers to a fresh root capability classified as Mutable in the type of value fst
51+
| ^² refers to a fresh root capability classified as Mutable created in value twisted when checking argument to parameter fst of constructor PairPair
52+
-- Error: tests/neg-custom-args/captures/sep-pairs-unboxed.scala:47:24 -------------------------------------------------
53+
47 | val twisted = swapped(two, two.snd) // error
54+
| ^^^
55+
|Separation failure: argument of type (two : Pair{val fst: Ref^; val snd: Ref^²}^³)
56+
|to method swapped: (@consume x: Pair^, @consume y: Ref^): PairPair^
57+
|corresponds to capture-polymorphic formal parameter x of type Pair^⁴
58+
|and hides capabilities {two}.
59+
|Some of these overlap with the captures of the second argument with type (two.snd : Ref^).
60+
|
61+
| Hidden set of current argument : {two}
62+
| Hidden footprint of current argument : {two}
63+
| Capture set of second argument : {two.snd}
64+
| Footprint set of second argument : {two.snd}
65+
| The two sets overlap at : {two.snd}
66+
|
67+
|where: ^ refers to a fresh root capability classified as Mutable in the type of value fst
68+
| ^² refers to a fresh root capability classified as Mutable in the type of value snd
69+
| ^³ refers to a fresh root capability in the type of value two
70+
| ^⁴ 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 -------------------------------------------------
72+
58 | val twoOther = Pair(two.fst, two.snd) // error // error
73+
| ^^^
74+
| Separation failure: Illegal access to {two.fst} which is hidden by the previous definition
75+
| of value twoCopy with type Pair^.
76+
| This type hides capabilities {two.fst, two.snd}
77+
|
78+
| 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 -------------------------------------------------
80+
58 | val twoOther = Pair(two.fst, two.snd) // error // error
81+
| ^^^
82+
| Separation failure: Illegal access to {two.snd} which is hidden by the previous definition
83+
| of value twoCopy with type Pair^.
84+
| This type hides capabilities {two.fst, two.snd}
85+
|
86+
| where: ^ refers to a fresh root capability in the type of value twoCopy

‎tests/neg-custom-args/captures/sep-pairs-unboxed.scala‎

Lines changed: 60 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,60 @@
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 Pair(val fst: Ref^, val snd: Ref^)
10+
11+
def mkPair(x: Ref^) = Pair(x, x) // error: separation failure
12+
13+
def bad: Pair^ =
14+
val r0 = Ref()
15+
val r1 = mkPair(r0)
16+
r1
17+
18+
def twoRefs(): Pair^ =
19+
val r1 = Ref()
20+
val r2 = Ref()
21+
Pair(r1, r2)
22+
23+
def good1(): Unit =
24+
val two = twoRefs()
25+
val fst = two.fst
26+
val snd = two.snd
27+
val twoCopy = Pair(fst, snd) // ok
28+
29+
def good2(): Unit =
30+
val two = twoRefs()
31+
val twoCopy = Pair(two.fst, two.snd) // ok
32+
33+
def bad2(): Unit =
34+
val two = twoRefs()
35+
val twoCopy = Pair(two.fst, two.fst) // error
36+
37+
class PairPair(val fst: Ref^, val snd: Pair^)
38+
39+
def bad3(): Unit =
40+
val two = twoRefs()
41+
val twisted = PairPair(two.fst, two) // error
42+
43+
def swapped(consume x: Pair^, consume y: Ref^): PairPair^ = PairPair(y, x)
44+
45+
def bad4(): Unit =
46+
val two = twoRefs()
47+
val twisted = swapped(two, two.snd) // error
48+
49+
def good3(): Unit =
50+
val two = twoRefs()
51+
val twoCopy = Pair(two.fst, two.snd)
52+
val _: Pair^{two.fst, two.snd} = twoCopy
53+
val twoOther = Pair(two.fst, two.snd)
54+
55+
def bad5(): Unit =
56+
val two = twoRefs()
57+
val twoCopy: Pair^ = Pair(two.fst, two.snd)
58+
val twoOther = Pair(two.fst, two.snd) // error // error
59+
60+

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -26,7 +26,7 @@
2626
| Separation failure in value sameToPair's type Pair[Ref^, Ref^²].
2727
| One part, Ref^, hides capabilities {fstSame}.
2828
| Another part, Ref^², captures capabilities {sndSame, same.snd*}.
29-
| The two sets overlap at cap of value same.
29+
| 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
3232
| ^² refers to a fresh root capability classified as Mutable in the type of value sameToPair

0 commit comments

Comments
 (0)