Skip to content

Commit 484137c

Browse files
oderskyodersky
committed
Fix unsoundness in APPLY and SELECT rules
We have to specially treat the case where the result contains a ResultCap. In that case no improvement is allowed, even if the alternative capture set is empty.
1 parent 0bddba1 commit 484137c

File tree

16 files changed

+122
-54
lines changed

16 files changed

+122
-54
lines changed

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

Lines changed: 12 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -732,19 +732,26 @@ class CheckCaptures extends Recheck, SymTransformer:
732732
|since its capture set ${qualType.captureSet} is read-only""",
733733
tree.srcPos)
734734

735-
val selType = mapResultRoots(recheckSelection(tree, qualType, name, disambiguate), tree.symbol)
735+
val origSelType = recheckSelection(tree, qualType, name, disambiguate)
736+
val selType = mapResultRoots(origSelType, tree.symbol)
736737
val selWiden = selType.widen
737738

739+
def capturesResult = origSelType.widenSingleton match
740+
case ExprType(resType) => resType.captureSet.containsResultCapability
741+
case _ => false
742+
738743
// Don't apply the rule
739744
// - on the LHS of assignments, or
740745
// - if the qualifier or selection type is boxed, or
741-
// - the selection is either a trackable capture reference or a pure type
746+
// - the selection is either a trackable capture reference or a pure type, or
747+
// - if the selection is of a parameterless method capturing a result cap
742748
if noWiden(selType, pt)
743749
|| qualType.isBoxedCapturing
744750
|| selType.isBoxedCapturing
745751
|| selWiden.isBoxedCapturing
746752
|| selType.isTrackableRef
747753
|| selWiden.captureSet.isAlwaysEmpty
754+
|| capturesResult
748755
then
749756
selType
750757
else
@@ -819,9 +826,8 @@ class CheckCaptures extends Recheck, SymTransformer:
819826
*/
820827
protected override
821828
def recheckApplication(tree: Apply, qualType: Type, funType: MethodType, argTypes: List[Type])(using Context): Type =
822-
val appType = resultToFresh(
823-
super.recheckApplication(tree, qualType, funType, argTypes),
824-
Origin.ResultInstance(funType, tree.symbol))
829+
val resultType = super.recheckApplication(tree, qualType, funType, argTypes)
830+
val appType = resultToFresh(resultType, Origin.ResultInstance(funType, tree.symbol))
825831
val qualCaptures = qualType.captureSet
826832
val argCaptures =
827833
for (argType, formal) <- argTypes.lazyZip(funType.paramInfos) yield
@@ -830,6 +836,7 @@ class CheckCaptures extends Recheck, SymTransformer:
830836
case appType @ CapturingType(appType1, refs)
831837
if qualType.exists
832838
&& !tree.fun.symbol.isConstructor
839+
&& !resultType.captureSet.containsResultCapability
833840
&& qualCaptures.mightSubcapture(refs)
834841
&& argCaptures.forall(_.mightSubcapture(refs)) =>
835842
val callCaptures = argCaptures.foldLeft(qualCaptures)(_ ++ _)

‎library/src/scala/collection/immutable/LazyListIterable.scala‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -321,7 +321,7 @@ final class LazyListIterable[+A] private (lazyState: LazyListIterable.EmptyMarke
321321
try fun().evaluated
322322
// restore `fun` in finally so we can try again later if an exception was thrown (similar to lazy val)
323323
finally _tail = fun
324-
_tail = l.rawTail
324+
_tail = caps.unsafe.unsafeAssumePure(l.rawTail)
325325
_head = l.rawHead
326326
}
327327
}

‎tests/neg-custom-args/captures/apply-fresh.check‎

Lines changed: 31 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,31 @@
1+
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/apply-fresh.scala:17:15 ----------------------------------
2+
17 | val _: Ref = x // error
3+
| ^
4+
| Found: (x : Ref^)
5+
| Required: Ref
6+
|
7+
| Note that capability cap is not included in capture set {}.
8+
|
9+
| where: ^ and cap refer to a fresh root capability in the type of value x
10+
|
11+
| longer explanation available when compiling with `-explain`
12+
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/apply-fresh.scala:21:15 ----------------------------------
13+
21 | val _: Ref = y // error
14+
| ^
15+
| Found: (y : Ref^)
16+
| Required: Ref
17+
|
18+
| Note that capability cap is not included in capture set {}.
19+
|
20+
| where: ^ and cap refer to a fresh root capability in the type of value y
21+
|
22+
| longer explanation available when compiling with `-explain`
23+
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/apply-fresh.scala:25:15 ----------------------------------
24+
25 | val _: Ref = z // error
25+
| ^
26+
| Found: (z : Ref^{bar.newRef})
27+
| Required: Ref
28+
|
29+
| Note that capability bar.newRef is not included in capture set {}.
30+
|
31+
| longer explanation available when compiling with `-explain`

‎tests/neg-custom-args/captures/apply-fresh.scala‎

Lines changed: 25 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,25 @@
1+
object Test
2+
3+
class Ref
4+
5+
class Foo:
6+
def newRef: Ref^ = Ref()
7+
8+
class Bar:
9+
val newRef: Ref^ = Ref()
10+
11+
def newRef: Ref^ = Ref()
12+
13+
def test =
14+
15+
val f = () => newRef
16+
val x = f()
17+
val _: Ref = x // error
18+
19+
val foo = Foo()
20+
val y = foo.newRef
21+
val _: Ref = y // error
22+
23+
val bar = Bar()
24+
val z = bar.newRef
25+
val _: Ref = z // error

‎tests/neg-custom-args/captures/capt-depfun.check‎

Lines changed: 5 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -1,11 +1,12 @@
11
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/capt-depfun.scala:11:43 ----------------------------------
22
11 | val dc: ((Str^{y, z}) => Str^{y, z}) = ac(g()) // error
33
| ^^^^^^^
4-
| Found: Str^{} ->{ac, y, z} Str^{y, z}
5-
| Required: Str^{y, z} => Str^{y, z}
4+
|Found: Str^{} => Str^{y, z}
5+
|Required: Str^{y, z} =>² Str^{y, z}
66
|
7-
| Note that capability y is not included in capture set {}.
7+
|Note that capability y is not included in capture set {}.
88
|
9-
| where: => refers to a fresh root capability in the type of value dc
9+
|where: => refers to a fresh root capability created in value dc when instantiating method apply's type (x: C^): Str^{x} =>³ Str^{x}
10+
| =>² refers to a fresh root capability in the type of value dc
1011
|
1112
| longer explanation available when compiling with `-explain`

‎tests/neg-custom-args/captures/caseclass/Test_2.scala‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -22,4 +22,4 @@ def test(c: C) =
2222

2323
val y4 = y3 match
2424
case Ref(xx) => xx
25-
val y4c: () ->{y3} Unit = y4
25+
val y4c: () ->{y3} Unit = y4 // error

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

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -1,11 +1,11 @@
11
-- Error: tests/neg-custom-args/captures/linear-buffer-2.scala:13:13 ---------------------------------------------------
22
13 | val buf3 = buf.append(3) // error
33
| ^^^
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}
4+
| Separation failure: Illegal access to (buf : Buffer[Int]^), which was passed to a
5+
| consume parameter or was used as a prefix to a consume method on line 11
6+
| and therefore is no longer available.
77
|
8-
| where: ^ refers to a fresh root capability classified as Mutable in the type of value buf1
8+
| where: ^ refers to a fresh root capability classified as Mutable in the type of parameter buf
99
-- Error: tests/neg-custom-args/captures/linear-buffer-2.scala:20:13 ---------------------------------------------------
1010
20 | val buf3 = buf1.append(4) // error
1111
| ^^^^

‎tests/neg-custom-args/captures/nested-classes-2.check‎

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/nested-classes-2.scala:9:36 ------------------------------
2+
9 | val cc3: cc1.C2^{cc1, x1, x2} = cc2 // error
3+
| ^^^
4+
| Found: cc1.C2{val y1: () ->{cc2*} Unit; val y2: (() => Unit) ->{cc2*} Unit}^{cc2}
5+
| Required: cc1.C2^{cc1, x1, x2}
6+
|
7+
| Note that capability cc2 is not included in capture set {cc1, x1, x2}.
8+
|
9+
| where: => refers to the universal root capability
10+
|
11+
| longer explanation available when compiling with `-explain`

‎tests/pos-custom-args/captures/nested-classes-2.scala‎ renamed to ‎tests/neg-custom-args/captures/nested-classes-2.scala‎

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -6,5 +6,7 @@ def test2(x1: (() => Unit), x2: (() => Unit) => Unit) =
66
def test3(y1: (() => Unit), y2: (() => Unit) => Unit) =
77
val cc1: C1^{y1, y2} = C1(y1, y2)
88
val cc2 = cc1.c2(x1, x2)
9-
val cc3: cc1.C2^{cc1, x1, x2} = cc2
9+
val cc3: cc1.C2^{cc1, x1, x2} = cc2 // error
10+
val cc4: cc1.C2^{cc2} = cc2 // ok
11+
1012

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

Lines changed: 10 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -81,26 +81,22 @@
8181
| ^³ and cap² refer to a fresh root capability in the type of value id
8282
|
8383
| longer explanation available when compiling with `-explain`
84-
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/reaches.scala:67:38 --------------------------------------
85-
67 | val leaked = usingFile[File^{id*}]: f => // error
86-
| ^
87-
|Found: (f: File^'s6) ->'s7 File^{id*}
88-
|Required: File^ => File^{id*}
84+
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/reaches.scala:68:27 --------------------------------------
85+
68 | val f1: File^{id*} = id(f) // error
86+
| ^^^^^
87+
|Found: File^
88+
|Required: File^{id*}
8989
|
9090
|Note that capability cap is not included in capture set {id*}.
9191
|
92-
|where: => refers to a fresh root capability created in value leaked when checking argument to parameter f of method usingFile
93-
| ^ refers to the universal root capability
94-
| cap is a fresh root capability created in anonymous function of type (f: File^'s6): File^{id*} of parameter parameter f² of method $anonfun
95-
68 | val f1: File^{id*} = id(f)
96-
69 | f1
92+
|where: ^ and cap refer to a fresh root capability created in value f1 when instantiating method apply's type (x: File^²): File^³
9793
|
9894
| longer explanation available when compiling with `-explain`
9995
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/reaches.scala:85:10 --------------------------------------
10096
85 | ps.map((x, y) => compose1(x, y)) // error
10197
| ^^^^^^^^^^^^^^^^^^^^^^^
102-
|Found: (x$1: (A^ ->'s8 A^'s9, A^ ->'s10 A^'s11)^'s12) ->'s13 A^'s14 ->'s15 A^'s16
103-
|Required: ((A ->{ps*} A, A ->{ps*} A)) => A^'s17 ->'s18 A^'s19
98+
|Found: (x$1: (A^ ->'s6 A^'s7, A^ ->'s8 A^'s9)^'s10) ->'s11 A^'s12 ->'s13 A^'s14
99+
|Required: ((A ->{ps*} A, A ->{ps*} A)) => A^'s15 ->'s16 A^'s17
104100
|
105101
|Note that capability ps* cannot be included in capture set {} of value x.
106102
|
@@ -111,8 +107,8 @@
111107
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/reaches.scala:88:10 --------------------------------------
112108
88 | ps.map((x, y) => compose1(x, y)) // error
113109
| ^^^^^^^^^^^^^^^^^^^^^^^
114-
|Found: (x$1: (A^ ->'s20 A^'s21, A^ ->'s22 A^'s23)^'s24) ->'s25 A^'s26 ->'s27 A^'s28
115-
|Required: ((A ->{C} A, A ->{C} A)) => A^'s29 ->'s30 A^'s31
110+
|Found: (x$1: (A^ ->'s18 A^'s19, A^ ->'s20 A^'s21)^'s22) ->'s23 A^'s24 ->'s25 A^'s26
111+
|Required: ((A ->{C} A, A ->{C} A)) => A^'s27 ->'s28 A^'s29
116112
|
117113
|Note that capability C cannot be included in capture set {} of value x.
118114
|

0 commit comments

Comments
 (0)