Skip to content

Commit 65a1301

Browse files
oderskyodersky
committed
Check that @consumed prefix capabilities are not re-used
Also: Fixes to computations of overlapWith and -- on Refs that take account of pathss, where shorter paths cover deeper ones.
1 parent c1ad0c1 commit 65a1301

File tree

10 files changed

+280
-114
lines changed

10 files changed

+280
-114
lines changed

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

+26
Original file line numberDiff line numberDiff line change
@@ -259,6 +259,32 @@ trait CaptureRef extends TypeProxy, ValueType:
259259
case ReadOnlyCapability(y1) => this.stripReadOnly.maxSubsumes(y1, canAddHidden)
260260
case _ => false
261261

262+
/** `x covers y` if we should retain `y` when computing the overlap of
263+
* two footprints which have `x` respectively `y` as elements.
264+
* We assume that .rd have already been stripped on both sides.
265+
* We have:
266+
*
267+
* x covers x
268+
* x covers y ==> x covers y.f
269+
* x covers y ==> x* covers y*, x? covers y?
270+
* TODO what other clauses from subsumes do we need to port here?
271+
*/
272+
final def covers(y: CaptureRef)(using Context): Boolean =
273+
(this eq y)
274+
|| y.match
275+
case y @ TermRef(ypre: CaptureRef, _) if !y.isCap =>
276+
this.covers(ypre)
277+
case ReachCapability(y1) =>
278+
this match
279+
case ReachCapability(x1) => x1.covers(y1)
280+
case _ => false
281+
case MaybeCapability(y1) =>
282+
this match
283+
case MaybeCapability(x1) => x1.covers(y1)
284+
case _ => false
285+
case _ =>
286+
false
287+
262288
def assumedContainsOf(x: TypeRef)(using Context): SimpleIdentitySet[CaptureRef] =
263289
CaptureSet.assumedContains.getOrElse(x, SimpleIdentitySet.empty)
264290

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

+136-86
Large diffs are not rendered by default.

‎scala2-library-cc/src/scala/collection/View.scala

+3-1
Original file line numberDiff line numberDiff line change
@@ -16,6 +16,7 @@ import scala.annotation.{nowarn, tailrec}
1616
import scala.collection.mutable.{ArrayBuffer, Builder}
1717
import scala.collection.immutable.LazyList
1818
import language.experimental.captureChecking
19+
import caps.unsafe.unsafeAssumeSeparate
1920

2021
/** Views are collections whose transformation operations are non strict: the resulting elements
2122
* are evaluated only when the view is effectively traversed (e.g. using `foreach` or `foldLeft`),
@@ -151,7 +152,8 @@ object View extends IterableFactory[View] {
151152
def apply[A](underlying: Iterable[A]^, p: A => Boolean, isFlipped: Boolean): Filter[A]^{underlying, p} =
152153
underlying match {
153154
case filter: Filter[A]^{underlying} if filter.isFlipped == isFlipped =>
154-
new Filter(filter.underlying, a => filter.p(a) && p(a), isFlipped)
155+
unsafeAssumeSeparate:
156+
new Filter(filter.underlying, a => filter.p(a) && p(a), isFlipped)
155157
case _ => new Filter(underlying, p, isFlipped)
156158
}
157159
}

‎scala2-library-cc/src/scala/collection/mutable/CheckedIndexedSeqView.scala

+14-14
Original file line numberDiff line numberDiff line change
@@ -17,7 +17,7 @@ import language.experimental.captureChecking
1717

1818
private[mutable] trait CheckedIndexedSeqView[+A] extends IndexedSeqView[A] {
1919

20-
protected val mutationCount: () => Int
20+
protected val mutationCount: () -> Int
2121

2222
override def iterator: Iterator[A]^{this} = new CheckedIndexedSeqView.CheckedIterator(this, mutationCount())
2323
override def reverseIterator: Iterator[A]^{this} = new CheckedIndexedSeqView.CheckedReverseIterator(this, mutationCount())
@@ -42,7 +42,7 @@ private[mutable] object CheckedIndexedSeqView {
4242
import IndexedSeqView.SomeIndexedSeqOps
4343

4444
@SerialVersionUID(3L)
45-
private[mutable] class CheckedIterator[A](self: IndexedSeqView[A]^, mutationCount: => Int)
45+
private[mutable] class CheckedIterator[A](self: IndexedSeqView[A]^, mutationCount: -> Int)
4646
extends IndexedSeqView.IndexedSeqViewIterator[A](self) {
4747
private[this] val expectedCount = mutationCount
4848
override def hasNext: Boolean = {
@@ -52,7 +52,7 @@ private[mutable] object CheckedIndexedSeqView {
5252
}
5353

5454
@SerialVersionUID(3L)
55-
private[mutable] class CheckedReverseIterator[A](self: IndexedSeqView[A]^, mutationCount: => Int)
55+
private[mutable] class CheckedReverseIterator[A](self: IndexedSeqView[A]^, mutationCount: -> Int)
5656
extends IndexedSeqView.IndexedSeqViewReverseIterator[A](self) {
5757
private[this] val expectedCount = mutationCount
5858
override def hasNext: Boolean = {
@@ -62,43 +62,43 @@ private[mutable] object CheckedIndexedSeqView {
6262
}
6363

6464
@SerialVersionUID(3L)
65-
class Id[+A](underlying: SomeIndexedSeqOps[A]^)(protected val mutationCount: () => Int)
65+
class Id[+A](underlying: SomeIndexedSeqOps[A]^)(protected val mutationCount: () -> Int)
6666
extends IndexedSeqView.Id(underlying) with CheckedIndexedSeqView[A]
6767

6868
@SerialVersionUID(3L)
69-
class Appended[+A](underlying: SomeIndexedSeqOps[A]^, elem: A)(protected val mutationCount: () => Int)
69+
class Appended[+A](underlying: SomeIndexedSeqOps[A]^, elem: A)(protected val mutationCount: () -> Int)
7070
extends IndexedSeqView.Appended(underlying, elem) with CheckedIndexedSeqView[A]
7171

7272
@SerialVersionUID(3L)
73-
class Prepended[+A](elem: A, underlying: SomeIndexedSeqOps[A]^)(protected val mutationCount: () => Int)
73+
class Prepended[+A](elem: A, underlying: SomeIndexedSeqOps[A]^)(protected val mutationCount: () -> Int)
7474
extends IndexedSeqView.Prepended(elem, underlying) with CheckedIndexedSeqView[A]
7575

7676
@SerialVersionUID(3L)
77-
class Concat[A](prefix: SomeIndexedSeqOps[A]^, suffix: SomeIndexedSeqOps[A]^)(protected val mutationCount: () => Int)
77+
class Concat[A](prefix: SomeIndexedSeqOps[A]^, suffix: SomeIndexedSeqOps[A]^)(protected val mutationCount: () -> Int)
7878
extends IndexedSeqView.Concat[A](prefix, suffix) with CheckedIndexedSeqView[A]
7979

8080
@SerialVersionUID(3L)
81-
class Take[A](underlying: SomeIndexedSeqOps[A]^, n: Int)(protected val mutationCount: () => Int)
81+
class Take[A](underlying: SomeIndexedSeqOps[A]^, n: Int)(protected val mutationCount: () -> Int)
8282
extends IndexedSeqView.Take(underlying, n) with CheckedIndexedSeqView[A]
8383

8484
@SerialVersionUID(3L)
85-
class TakeRight[A](underlying: SomeIndexedSeqOps[A]^, n: Int)(protected val mutationCount: () => Int)
85+
class TakeRight[A](underlying: SomeIndexedSeqOps[A]^, n: Int)(protected val mutationCount: () -> Int)
8686
extends IndexedSeqView.TakeRight(underlying, n) with CheckedIndexedSeqView[A]
8787

8888
@SerialVersionUID(3L)
89-
class Drop[A](underlying: SomeIndexedSeqOps[A]^, n: Int)(protected val mutationCount: () => Int)
89+
class Drop[A](underlying: SomeIndexedSeqOps[A]^, n: Int)(protected val mutationCount: () -> Int)
9090
extends IndexedSeqView.Drop[A](underlying, n) with CheckedIndexedSeqView[A]
9191

9292
@SerialVersionUID(3L)
93-
class DropRight[A](underlying: SomeIndexedSeqOps[A]^, n: Int)(protected val mutationCount: () => Int)
93+
class DropRight[A](underlying: SomeIndexedSeqOps[A]^, n: Int)(protected val mutationCount: () -> Int)
9494
extends IndexedSeqView.DropRight[A](underlying, n) with CheckedIndexedSeqView[A]
9595

9696
@SerialVersionUID(3L)
97-
class Map[A, B](underlying: SomeIndexedSeqOps[A]^, f: A => B)(protected val mutationCount: () => Int)
97+
class Map[A, B](underlying: SomeIndexedSeqOps[A]^, f: A => B)(protected val mutationCount: () -> Int)
9898
extends IndexedSeqView.Map(underlying, f) with CheckedIndexedSeqView[B]
9999

100100
@SerialVersionUID(3L)
101-
class Reverse[A](underlying: SomeIndexedSeqOps[A]^)(protected val mutationCount: () => Int)
101+
class Reverse[A](underlying: SomeIndexedSeqOps[A]^)(protected val mutationCount: () -> Int)
102102
extends IndexedSeqView.Reverse[A](underlying) with CheckedIndexedSeqView[A] {
103103
override def reverse: IndexedSeqView[A] = underlying match {
104104
case x: IndexedSeqView[A] => x
@@ -107,7 +107,7 @@ private[mutable] object CheckedIndexedSeqView {
107107
}
108108

109109
@SerialVersionUID(3L)
110-
class Slice[A](underlying: SomeIndexedSeqOps[A]^, from: Int, until: Int)(protected val mutationCount: () => Int)
110+
class Slice[A](underlying: SomeIndexedSeqOps[A]^, from: Int, until: Int)(protected val mutationCount: () -> Int)
111111
extends AbstractIndexedSeqView[A] with CheckedIndexedSeqView[A] {
112112
protected val lo = from max 0
113113
protected val hi = (until max 0) min underlying.length

‎tests/neg-custom-args/captures/linear-buffer-2.check

+29
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,29 @@
1+
-- Error: tests/neg-custom-args/captures/linear-buffer-2.scala:13:13 ---------------------------------------------------
2+
13 | val buf3 = buf.append(3) // error
3+
| ^^^
4+
| Separation failure: Illegal access to {buf} which is hidden by the previous definition
5+
| of value buf1 with type Buffer[Int]^.
6+
| This type hides capabilities {buf}
7+
-- Error: tests/neg-custom-args/captures/linear-buffer-2.scala:20:13 ---------------------------------------------------
8+
20 | val buf3 = buf1.append(4) // error
9+
| ^^^^
10+
| Separation failure: Illegal access to (buf1 : Buffer[Int]^), which was passed to a
11+
| @consume parameter or was used as a prefix to a @consume method on line 18
12+
| and therefore is no longer available.
13+
-- Error: tests/neg-custom-args/captures/linear-buffer-2.scala:28:13 ---------------------------------------------------
14+
28 | val buf3 = buf1.append(4) // error
15+
| ^^^^
16+
| Separation failure: Illegal access to (buf1 : Buffer[Int]^), which was passed to a
17+
| @consume parameter or was used as a prefix to a @consume method on line 25
18+
| and therefore is no longer available.
19+
-- Error: tests/neg-custom-args/captures/linear-buffer-2.scala:38:13 ---------------------------------------------------
20+
38 | val buf3 = buf1.append(4) // error
21+
| ^^^^
22+
| Separation failure: Illegal access to (buf1 : Buffer[Int]^), which was passed to a
23+
| @consume parameter or was used as a prefix to a @consume method on line 33
24+
| and therefore is no longer available.
25+
-- Error: tests/neg-custom-args/captures/linear-buffer-2.scala:42:4 ----------------------------------------------------
26+
42 | buf.append(1) // error
27+
| ^^^
28+
| Separation failure: (buf : Buffer[Int]^) appears in a loop, therefore it cannot
29+
| be passed to a @consume parameter or be used as a prefix of a @consume method call.

‎tests/neg-custom-args/captures/linear-buffer-2.scala

+42
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,42 @@
1+
import caps.{cap, consume, Mutable}
2+
import language.experimental.captureChecking
3+
4+
class Buffer[T] extends Mutable:
5+
@consume mut def append(x: T): Buffer[T]^ = this // ok
6+
7+
def app[T](@consume buf: Buffer[T]^, elem: T): Buffer[T]^ =
8+
buf.append(elem)
9+
10+
def Test(@consume buf: Buffer[Int]^) =
11+
val buf1: Buffer[Int]^ = buf.append(1)
12+
val buf2 = buf1.append(2) // OK
13+
val buf3 = buf.append(3) // error
14+
15+
def Test2(@consume buf: Buffer[Int]^) =
16+
val buf1: Buffer[Int]^ = buf.append(1)
17+
val buf2 =
18+
if ??? then buf1.append(2) // OK
19+
else buf1.append(3) // OK
20+
val buf3 = buf1.append(4) // error
21+
22+
def Test3(@consume buf: Buffer[Int]^) =
23+
val buf1: Buffer[Int]^ = buf.append(1)
24+
val buf2 = (??? : Int) match
25+
case 1 => buf1.append(2) // OK
26+
case 2 => buf1.append(2)
27+
case _ => buf1.append(3)
28+
val buf3 = buf1.append(4) // error
29+
30+
def Test4(@consume buf: Buffer[Int]^) =
31+
val buf1: Buffer[Int]^ = buf.append(1)
32+
val buf2 = (??? : Int) match
33+
case 1 => buf1.append(2) // OK
34+
case 2 => buf1.append(2)
35+
case 3 => buf1.append(3)
36+
case 4 => buf1.append(4)
37+
case 5 => buf1.append(5)
38+
val buf3 = buf1.append(4) // error
39+
40+
def Test5(@consume buf: Buffer[Int]^) =
41+
while true do
42+
buf.append(1) // error

‎tests/neg-custom-args/captures/linear-buffer.check

+10-10
Original file line numberDiff line numberDiff line change
@@ -16,29 +16,29 @@
1616
-- Error: tests/neg-custom-args/captures/linear-buffer.scala:19:17 -----------------------------------------------------
1717
19 | val buf3 = app(buf, 3) // error
1818
| ^^^
19-
| Separation failure: Illegal access to (buf : Buffer[Int]^),
20-
| which was passed to a @consume parameter on line 17
19+
| Separation failure: Illegal access to (buf : Buffer[Int]^), which was passed to a
20+
| @consume parameter or was used as a prefix to a @consume method on line 17
2121
| and therefore is no longer available.
2222
-- Error: tests/neg-custom-args/captures/linear-buffer.scala:26:17 -----------------------------------------------------
2323
26 | val buf3 = app(buf1, 4) // error
2424
| ^^^^
25-
| Separation failure: Illegal access to (buf1 : Buffer[Int]^),
26-
| which was passed to a @consume parameter on line 24
25+
| Separation failure: Illegal access to (buf1 : Buffer[Int]^), which was passed to a
26+
| @consume parameter or was used as a prefix to a @consume method on line 24
2727
| and therefore is no longer available.
2828
-- Error: tests/neg-custom-args/captures/linear-buffer.scala:34:17 -----------------------------------------------------
2929
34 | val buf3 = app(buf1, 4) // error
3030
| ^^^^
31-
| Separation failure: Illegal access to (buf1 : Buffer[Int]^),
32-
| which was passed to a @consume parameter on line 31
31+
| Separation failure: Illegal access to (buf1 : Buffer[Int]^), which was passed to a
32+
| @consume parameter or was used as a prefix to a @consume method on line 31
3333
| and therefore is no longer available.
3434
-- Error: tests/neg-custom-args/captures/linear-buffer.scala:44:17 -----------------------------------------------------
3535
44 | val buf3 = app(buf1, 4) // error
3636
| ^^^^
37-
| Separation failure: Illegal access to (buf1 : Buffer[Int]^),
38-
| which was passed to a @consume parameter on line 39
37+
| Separation failure: Illegal access to (buf1 : Buffer[Int]^), which was passed to a
38+
| @consume parameter or was used as a prefix to a @consume method on line 39
3939
| and therefore is no longer available.
4040
-- Error: tests/neg-custom-args/captures/linear-buffer.scala:48:8 ------------------------------------------------------
4141
48 | app(buf, 1) // error
4242
| ^^^
43-
| Separation failure: (buf : Buffer[Int]^) appears in a loop,
44-
| therefore it cannot be passed to a @consume parameter.
43+
| Separation failure: (buf : Buffer[Int]^) appears in a loop, therefore it cannot
44+
| be passed to a @consume parameter or be used as a prefix of a @consume method call.

‎tests/neg-custom-args/captures/path-patmat-should-be-pos.scala

+3-1
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,8 @@
1+
import caps.cap
2+
13
class It[A]
24

3-
class Filter[A](val underlying: It[A]^, val p: A => Boolean) extends It[A]
5+
class Filter[A](val underlying: It[A]^, val p: A ->{cap, underlying} Boolean) extends It[A]
46
object Filter:
57
def apply[A](underlying: It[A]^, p: A => Boolean): Filter[A]^{underlying, p} =
68
underlying match

‎tests/pos-custom-args/captures/filter-iterable.scala

+11
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
import caps.cap
2+
3+
class It[A]
4+
5+
class Filter[A](val underlying: It[A]^, val p: A ->{cap, underlying} Boolean) extends It[A]
6+
object Filter:
7+
def apply[A](underlying: It[A]^, p: A => Boolean): Filter[A]^{cap, p, underlying} =
8+
underlying match
9+
case filter: Filter[A]^ =>
10+
val x = new Filter(filter.underlying, a => filter.p(a) && p(a))
11+
x: Filter[A]^{filter, p}

‎tests/run-custom-args/captures/colltest5/CollectionStrawManCC5_1.scala

+6-2
Original file line numberDiff line numberDiff line change
@@ -7,7 +7,7 @@ import annotation.unchecked.{uncheckedVariance, uncheckedCaptures}
77
import annotation.tailrec
88
import caps.cap
99
import caps.untrackedCaptures
10-
import language.`3.7` // sepchecks on
10+
import caps.unsafe.unsafeAssumeSeparate
1111

1212
/** A strawman architecture for new collections. It contains some
1313
* example collection classes and methods with the intent to expose
@@ -460,7 +460,11 @@ object CollectionStrawMan5 {
460460
def apply[A](underlying: Iterable[A]^, pp: A => Boolean, isFlipped: Boolean): Filter[A]^{underlying, pp} =
461461
underlying match
462462
case filter: Filter[A]^{underlying} =>
463-
new Filter(filter.underlying, a => filter.p(a) && pp(a))
463+
unsafeAssumeSeparate:
464+
// See filter-iterable.scala for a test where a variant of Filter
465+
// works without the unsafeAssumeSeparate. But it requires significant
466+
// changes compared to the version here.
467+
new Filter(filter.underlying, a => filter.p(a) && pp(a))
464468
case _ => new Filter(underlying, pp)
465469

466470
case class Partition[A](val underlying: Iterable[A]^, p: A => Boolean) {

0 commit comments

Comments
 (0)