Skip to content

Commit 750c7f0

Browse files
oderskyodersky
committed
Generalize read-only adaptation
 - Also adapt in type arguments, refinements, and function results - Also adapt to readonly if target is a mutable, read-only type
1 parent 650874b commit 750c7f0

File tree

8 files changed

+195
-17
lines changed

8 files changed

+195
-17
lines changed

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

Lines changed: 6 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -136,6 +136,8 @@ sealed abstract class CaptureSet extends Showable:
136136
final def isReadOnly(using Context): Boolean =
137137
elems.forall(_.isReadOnly)
138138

139+
final def isAlwaysReadOnly(using Context): Boolean = isConst && isReadOnly
140+
139141
final def isExclusive(using Context): Boolean =
140142
elems.exists(_.isExclusive)
141143

@@ -1385,8 +1387,8 @@ object CaptureSet:
13851387
def apply(t: Type) = mapOver(t)
13861388

13871389
override def fuse(next: BiTypeMap)(using Context) = next match
1388-
case next: Inverse if next.inverse.getClass == getClass => assert(false); Some(IdentityTypeMap)
1389-
case next: NarrowingCapabilityMap if next.getClass == getClass => assert(false)
1390+
case next: Inverse if next.inverse.getClass == getClass => Some(IdentityTypeMap)
1391+
case next: NarrowingCapabilityMap if next.getClass == getClass => Some(this)
13901392
case _ => None
13911393

13921394
class Inverse extends BiTypeMap:
@@ -1395,8 +1397,8 @@ object CaptureSet:
13951397
def inverse = NarrowingCapabilityMap.this
13961398
override def toString = NarrowingCapabilityMap.this.toString ++ ".inverse"
13971399
override def fuse(next: BiTypeMap)(using Context) = next match
1398-
case next: NarrowingCapabilityMap if next.inverse.getClass == getClass => assert(false); Some(IdentityTypeMap)
1399-
case next: NarrowingCapabilityMap if next.getClass == getClass => assert(false)
1400+
case next: NarrowingCapabilityMap if next.inverse.getClass == getClass => Some(IdentityTypeMap)
1401+
case next: NarrowingCapabilityMap if next.getClass == getClass => Some(this)
14001402
case _ => None
14011403

14021404
lazy val inverse = Inverse()

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

Lines changed: 73 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -1568,17 +1568,81 @@ class CheckCaptures extends Recheck, SymTransformer:
15681568
* to narrow to the read-only set, since that set can be propagated
15691569
* by the type variable instantiation.
15701570
*/
1571-
private def improveReadOnly(actual: Type, expected: Type)(using Context): Type = actual match
1572-
case actual @ CapturingType(parent, refs)
1573-
if parent.derivesFrom(defn.Caps_Mutable)
1574-
&& expected.isValueType
1575-
&& !expected.derivesFromMutable
1576-
&& !expected.isSingleton
1577-
&& !expected.isBoxedCapturing =>
1578-
actual.derivedCapturingType(parent, refs.readOnly)
1579-
.showing(i"improv ro $actual vs $expected = $result", capt)
1571+
private def improveReadOnly(actual: Type, expected: Type)(using Context): Type = reporting.trace(i"improv ro $actual vs $expected"):
1572+
actual.dealiasKeepAnnots match
1573+
case actual @ CapturingType(parent, refs) =>
1574+
val parent1 = improveReadOnly(parent, expected)
1575+
val refs1 =
1576+
if parent1.derivesFrom(defn.Caps_Mutable)
1577+
&& expected.isValueType
1578+
&& (!expected.derivesFromMutable || expected.captureSet.isAlwaysReadOnly)
1579+
&& !expected.isSingleton
1580+
&& actual.isBoxedCapturing == expected.isBoxedCapturing
1581+
then refs.readOnly
1582+
else refs
1583+
actual.derivedCapturingType(parent1, refs1)
1584+
case actual @ FunctionOrMethod(aargs, ares) =>
1585+
expected.dealias.stripCapturing match
1586+
case FunctionOrMethod(eargs, eres) =>
1587+
actual.derivedFunctionOrMethod(aargs, improveReadOnly(ares, eres))
1588+
case _ =>
1589+
actual
1590+
case actual @ AppliedType(atycon, aargs) =>
1591+
def improveArgs(aargs: List[Type], eargs: List[Type], formals: List[ParamInfo]): List[Type] =
1592+
aargs match
1593+
case aargs @ (aarg :: aargs1) =>
1594+
val aarg1 =
1595+
if formals.head.paramVariance.is(Covariant)
1596+
then improveReadOnly(aarg, eargs.head)
1597+
else aarg
1598+
aargs.derivedCons(aarg1, improveArgs(aargs1, eargs.tail, formals.tail))
1599+
case Nil =>
1600+
aargs
1601+
val expected1 = expected.dealias.stripCapturing
1602+
val esym = expected1.typeSymbol
1603+
expected1 match
1604+
case AppliedType(etycon, eargs) =>
1605+
if atycon.typeSymbol == esym then
1606+
actual.derivedAppliedType(atycon,
1607+
improveArgs(aargs, eargs, etycon.typeParams))
1608+
else if esym.isClass then
1609+
// This case is tricky: Try to lift actual to the base type with class `esym`,
1610+
// improve the resulting arguments, and figure out if anything can be
1611+
// deduced from that for the original arguments.
1612+
actual.baseType(esym) match
1613+
case base @ AppliedType(_, bargs) =>
1614+
// If any of the base type arguments can be improved, check
1615+
// whether they are the same as an original argument, and in this
1616+
// case improve the original argument.
1617+
val iargs = improveArgs(bargs, eargs, etycon.typeParams)
1618+
if iargs ne bargs then
1619+
val updates =
1620+
for
1621+
(barg, iarg) <- bargs.lazyZip(iargs)
1622+
if barg ne iarg
1623+
aarg <- aargs.find(_ eq barg)
1624+
yield (aarg, iarg)
1625+
if updates.nonEmpty then AppliedType(atycon, aargs.map(updates.toMap))
1626+
else actual
1627+
else actual
1628+
case _ => actual
1629+
else actual
1630+
case _ =>
1631+
actual
1632+
case actual @ RefinedType(aparent, aname, ainfo) =>
1633+
expected.dealias.stripCapturing match
1634+
case RefinedType(eparent, ename, einfo) if aname == ename =>
1635+
actual.derivedRefinedType(
1636+
improveReadOnly(aparent, eparent),
1637+
aname,
1638+
improveReadOnly(ainfo, einfo))
1639+
case _ =>
1640+
actual
1641+
case actual @ AnnotatedType(parent, ann) =>
1642+
actual.derivedAnnotatedType(improveReadOnly(parent, expected), ann)
15801643
case _ =>
15811644
actual
1645+
end improveReadOnly
15821646

15831647
/* Currently not needed since it forms part of `adapt`
15841648
private def improve(actual: Type, prefix: Type)(using Context): Type =

‎tests/neg-custom-args/captures/matrix.check

Lines changed: 32 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,32 @@
1+
-- Error: tests/neg-custom-args/captures/matrix.scala:27:10 ------------------------------------------------------------
2+
27 | mul(m1, m2, m2) // error: will fail separation checking
3+
| ^^
4+
|Separation failure: argument of type Matrix^{m2.rd}
5+
|to method mul: (x: Matrix^{cap.rd}, y: Matrix^{cap.rd}, z: Matrix^): Unit
6+
|corresponds to capture-polymorphic formal parameter y of type Matrix^{cap.rd}
7+
|and hides capabilities {m2.rd}.
8+
|Some of these overlap with the captures of the third argument with type (m2 : Matrix^).
9+
|
10+
| Hidden set of current argument : {m2.rd}
11+
| Hidden footprint of current argument : {m2.rd}
12+
| Capture set of third argument : {m2}
13+
| Footprint set of third argument : {m2}
14+
| The two sets overlap at : {m2}
15+
|
16+
|where: cap is a fresh root capability created in method Test when checking argument to parameter y of method mul
17+
-- Error: tests/neg-custom-args/captures/matrix.scala:30:11 ------------------------------------------------------------
18+
30 | mul1(m1, m2, m2) // error: will fail separation checking
19+
| ^^
20+
|Separation failure: argument of type Matrix^{m2.rd}
21+
|to method mul1: (x: Matrix^{cap.rd}, y: Matrix^{cap.rd}, z: Matrix^): Unit
22+
|corresponds to capture-polymorphic formal parameter y of type Matrix^{cap.rd}
23+
|and hides capabilities {m2.rd}.
24+
|Some of these overlap with the captures of the third argument with type (m2 : Matrix^).
25+
|
26+
| Hidden set of current argument : {m2.rd}
27+
| Hidden footprint of current argument : {m2.rd}
28+
| Capture set of third argument : {m2}
29+
| Footprint set of third argument : {m2}
30+
| The two sets overlap at : {m2}
31+
|
32+
|where: cap is a fresh root capability created in method Test when checking argument to parameter y of method mul1

‎tests/neg-custom-args/captures/matrix.scala

Lines changed: 36 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,36 @@
1+
import caps.Mutable
2+
import caps.cap
3+
4+
trait Rdr[T]:
5+
def get: T
6+
7+
class Ref[T](init: T) extends Rdr[T], Mutable:
8+
private var current = init
9+
def get: T = current
10+
mut def put(x: T): Unit = current = x
11+
12+
abstract class IMatrix:
13+
def apply(i: Int, j: Int): Double
14+
15+
class Matrix(nrows: Int, ncols: Int) extends IMatrix, Mutable:
16+
val arr = Array.fill(nrows, ncols)(0.0)
17+
def apply(i: Int, j: Int): Double = arr(i)(j)
18+
mut def update(i: Int, j: Int, x: Double): Unit = arr(i)(j) = x
19+
20+
21+
def mul(x: Matrix, y: Matrix, z: Matrix^): Unit = ???
22+
def mul1(x: Matrix^{cap.rd}, y: Matrix^{cap.rd}, z: Matrix^): Unit = ???
23+
24+
def Test(c: Object^): Unit =
25+
val m1 = Matrix(10, 10)
26+
val m2 = Matrix(10, 10)
27+
mul(m1, m2, m2) // error: will fail separation checking
28+
mul(m1, m1, m2) // should be ok
29+
30+
mul1(m1, m2, m2) // error: will fail separation checking
31+
mul(m1, m1, m2) // should be ok
32+
33+
def f2(): Matrix^ = Matrix(10, 10)
34+
35+
val i1: IMatrix^{cap.rd} = m1
36+
val i2: IMatrix^{cap.rd} = f2()

‎tests/neg-custom-args/captures/ro-mut-conformance.check

Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
1+
-- Error: tests/neg-custom-args/captures/ro-mut-conformance.scala:8:4 --------------------------------------------------
2+
8 | a.set(42) // error
3+
| ^^^^^
4+
| cannot call update method set from (a : Ref),
5+
| since its capture set {a} is read-only
6+
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/ro-mut-conformance.scala:10:21 ---------------------------
7+
10 | val t: Ref^{cap} = a // error
8+
| ^
9+
| Found: (a : Ref)
10+
| Required: Ref^
11+
|
12+
| where: ^ refers to a fresh root capability in the type of value t
13+
|
14+
| longer explanation available when compiling with `-explain`

‎tests/neg-custom-args/captures/ro-mut-conformance.scala

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
import language.experimental.captureChecking
2+
import caps.*
3+
class Ref extends Mutable:
4+
private var _data: Int = 0
5+
def get: Int = _data
6+
mut def set(x: Int): Unit = _data = x
7+
def test1(a: Ref^{cap.rd}): Unit =
8+
a.set(42) // error
9+
def test2(a: Ref^{cap.rd}): Unit =
10+
val t: Ref^{cap} = a // error
11+
t.set(42)

‎tests/pos-custom-args/captures/deep-adapt.scala

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+
trait Rdr[T]:
5+
def get: T
6+
7+
class Ref[T](init: T) extends Rdr[T], Mutable:
8+
private var current = init
9+
def get: T = current
10+
mut def put(x: T): Unit = current = x
11+
12+
case class Pair[+A, +B](x: A, y: B)
13+
class Swap[+A, +B](x: A, y: B) extends Pair[B, A](y, x)
14+
15+
def Test(c: Object^): Unit =
16+
val refs = List(Ref(1), Ref(2))
17+
val rdrs: List[Ref[Int]^{cap.rd}] = refs
18+
val rdrs2: Seq[Ref[Int]^{cap.rd}] = refs
19+
20+
val swapped = Swap(Ref(1), Ref("hello"))
21+
val _: Swap[Ref[Int]^{cap.rd}, Ref[String]^{cap.rd}] = swapped
22+
val _: Pair[Ref[String]^{cap.rd}, Ref[Int]^{cap.rd}] @unchecked = swapped
23+

‎tests/pos-custom-args/captures/matrix.scala

Lines changed: 0 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,5 @@
11
import caps.Mutable
22
import caps.cap
3-
import language.`3.7` // fails separation checking right now
43

54
trait Rdr[T]:
65
def get: T
@@ -25,10 +24,7 @@ def mul1(x: Matrix^{cap.rd}, y: Matrix^{cap.rd}, z: Matrix^): Unit = ???
2524
def Test(c: Object^): Unit =
2625
val m1 = Matrix(10, 10)
2726
val m2 = Matrix(10, 10)
28-
mul(m1, m2, m2) // error: will fail separation checking
2927
mul(m1, m1, m2) // should be ok
30-
31-
mul1(m1, m2, m2) // error: will fail separation checking
3228
mul(m1, m1, m2) // should be ok
3329

3430
def f2(): Matrix^ = Matrix(10, 10)

0 commit comments

Comments
 (0)