Skip to content

Commit 3adf4b0

Browse files
oderskyodersky
committed
Check that hidden parameters are annotated @consume
TODO: - check that only @consume parameters flow to @consume parameters
1 parent 131f070 commit 3adf4b0

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

42 files changed

+332
-123
lines changed

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

+3-1
Original file line numberDiff line numberDiff line change
@@ -1559,7 +1559,7 @@ class CheckCaptures extends Recheck, SymTransformer:
15591559

15601560
override def checkInheritedTraitParameters: Boolean = false
15611561

1562-
/** Check that overrides don't change the @use status of their parameters */
1562+
/** Check that overrides don't change the @use or @consume status of their parameters */
15631563
override def additionalChecks(member: Symbol, other: Symbol)(using Context): Unit =
15641564
def fail(msg: String) =
15651565
report.error(
@@ -1571,6 +1571,8 @@ class CheckCaptures extends Recheck, SymTransformer:
15711571
do
15721572
if param1.hasAnnotation(defn.UseAnnot) != param2.hasAnnotation(defn.UseAnnot) then
15731573
fail(i"has a parameter ${param1.name} with different @use status than the corresponding parameter in the overridden definition")
1574+
if param1.hasAnnotation(defn.ConsumeAnnot) != param2.hasAnnotation(defn.ConsumeAnnot) then
1575+
fail(i"has a parameter ${param1.name} with different @consume status than the corresponding parameter in the overridden definition")
15741576
end OverridingPairsCheckerCC
15751577

15761578
def traverse(t: Tree)(using Context) =

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

+72-17
Original file line numberDiff line numberDiff line change
@@ -28,6 +28,16 @@ object SepChecker:
2828
else NeedsCheck
2929
end Captures
3030

31+
/** The kind of checked type, used for composing error messages */
32+
enum TypeKind:
33+
case Result(sym: Symbol, inferred: Boolean)
34+
case Argument
35+
36+
def dclSym = this match
37+
case Result(sym, _) => sym
38+
case _ => NoSymbol
39+
end TypeKind
40+
3141
class SepChecker(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser:
3242
import tpd.*
3343
import checker.*
@@ -204,7 +214,7 @@ class SepChecker(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser:
204214
for (arg, idx) <- indexedArgs do
205215
if arg.needsSepCheck then
206216
val ac = formalCaptures(arg)
207-
checkType(arg.formalType, arg.srcPos, NoSymbol, " the argument's adapted type")
217+
checkType(arg.formalType, arg.srcPos, TypeKind.Argument)
208218
val hiddenInArg = ac.hidden.footprint
209219
//println(i"check sep $arg: $ac, footprint so far = $footprint, hidden = $hiddenInArg")
210220
val overlap = hiddenInArg.overlapWith(footprint).deductCapturesOf(deps(arg))
@@ -232,18 +242,29 @@ class SepChecker(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser:
232242
sepUseError(tree, usedFootprint, overlap)
233243

234244
def checkType(tpt: Tree, sym: Symbol)(using Context): Unit =
235-
checkType(tpt.nuType, tpt.srcPos, sym, "")
236-
237-
/** Check that all parts of type `tpe` are separated.
238-
* @param tpe the type to check
239-
* @param pos position for error reporting
240-
* @param sym if `tpe` is the (result-) type of a val or def, the symbol of
241-
* this definition, otherwise NoSymbol. If `sym` exists we
242-
* deduct its associated direct and reach capabilities everywhere
243-
* from the capture sets we check.
244-
* @param what a string describing what kind of type it is
245-
*/
246-
def checkType(tpe: Type, pos: SrcPos, sym: Symbol, what: String)(using Context): Unit =
245+
checkType(tpt.nuType, tpt.srcPos,
246+
TypeKind.Result(sym, inferred = tpt.isInstanceOf[InferredTypeTree]))
247+
248+
/** Check that all parts of type `tpe` are separated. */
249+
def checkType(tpe: Type, pos: SrcPos, kind: TypeKind)(using Context): Unit =
250+
251+
def typeDescr = kind match
252+
case TypeKind.Result(sym, inferred) =>
253+
def inferredStr = if inferred then " inferred" else ""
254+
def resultStr = if sym.info.isInstanceOf[MethodicType] then " result" else ""
255+
i" $sym's$inferredStr$resultStr"
256+
case TypeKind.Argument =>
257+
" the argument's adapted type"
258+
259+
def explicitRefs(tp: Type): Refs = tp match
260+
case tp: (TermRef | ThisType) => SimpleIdentitySet(tp)
261+
case AnnotatedType(parent, _) => explicitRefs(parent)
262+
case AndType(tp1, tp2) => explicitRefs(tp1) ++ explicitRefs(tp2)
263+
case OrType(tp1, tp2) => explicitRefs(tp1) ** explicitRefs(tp2)
264+
case _ => emptySet
265+
266+
def prune(refs: Refs): Refs =
267+
refs.deductSym(kind.dclSym) -- explicitRefs(tpe)
247268

248269
def checkParts(parts: List[Type]): Unit =
249270
var footprint: Refs = emptySet
@@ -265,21 +286,21 @@ class SepChecker(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser:
265286
if !globalOverlap.isEmpty then
266287
val (prevStr, prevRefs, overlap) = parts.iterator.take(checked)
267288
.map: prev =>
268-
val prevRefs = mapRefs(prev.deepCaptureSet.elems).footprint.deductSym(sym)
289+
val prevRefs = prune(mapRefs(prev.deepCaptureSet.elems).footprint)
269290
(i", $prev , ", prevRefs, prevRefs.overlapWith(next))
270291
.dropWhile(_._3.isEmpty)
271292
.nextOption
272293
.getOrElse(("", current, globalOverlap))
273294
report.error(
274-
em"""Separation failure in$what type $tpe.
295+
em"""Separation failure in$typeDescr type $tpe.
275296
|One part, $part , $nextRel ${CaptureSet(next)}.
276297
|A previous part$prevStr $prevRel ${CaptureSet(prevRefs)}.
277298
|The two sets overlap at ${CaptureSet(overlap)}.""",
278299
pos)
279300

280301
val partRefs = part.deepCaptureSet.elems
281-
val partFootprint = partRefs.footprint.deductSym(sym)
282-
val partHidden = partRefs.hidden.footprint.deductSym(sym) -- partFootprint
302+
val partFootprint = prune(partRefs.footprint)
303+
val partHidden = prune(partRefs.hidden.footprint) -- partFootprint
283304

284305
checkSep(footprint, partHidden, identity, "references", "hides")
285306
checkSep(hiddenSet, partHidden, _.hidden, "also hides", "hides")
@@ -325,9 +346,43 @@ class SepChecker(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser:
325346
case t =>
326347
foldOver(c, t)
327348

349+
def checkParameters() =
350+
val badParams = mutable.ListBuffer[Symbol]()
351+
def currentOwner = kind.dclSym.orElse(ctx.owner)
352+
for hiddenRef <- prune(tpe.deepCaptureSet.elems.hidden.footprint) do
353+
val refSym = hiddenRef.termSymbol
354+
if refSym.is(TermParam)
355+
&& !refSym.hasAnnotation(defn.ConsumeAnnot)
356+
&& !refSym.info.derivesFrom(defn.Caps_SharedCapability)
357+
&& currentOwner.isContainedIn(refSym.owner)
358+
then
359+
badParams += refSym
360+
if badParams.nonEmpty then
361+
def paramsStr(params: List[Symbol]): String = (params: @unchecked) match
362+
case p :: Nil => i"${p.name}"
363+
case p :: p2 :: Nil => i"${p.name} and ${p2.name}"
364+
case p :: ps => i"${p.name}, ${paramsStr(ps)}"
365+
val (pluralS, singleS) = if badParams.tail.isEmpty then ("", "s") else ("s", "")
366+
report.error(
367+
em"""Separation failure:$typeDescr type $tpe hides parameter$pluralS ${paramsStr(badParams.toList)}
368+
|The parameter$pluralS need$singleS to be annotated with @consume to allow this.""",
369+
pos)
370+
371+
def flagHiddenParams =
372+
kind match
373+
case TypeKind.Result(sym, _) =>
374+
!sym.isAnonymousFunction // we don't check return types of anonymous functions
375+
&& !sym.is(Case) // We don't check so far binders in patterns since they
376+
// have inferred universal types. TODO come back to this;
377+
// either infer more precise types for such binders or
378+
// "see through them" when we look at hidden sets.
379+
case TypeKind.Argument =>
380+
false
381+
328382
if !tpe.hasAnnotation(defn.UntrackedCapturesAnnot) then
329383
traverse(Captures.None, tpe)
330384
traverse.toCheck.foreach(checkParts)
385+
if flagHiddenParams then checkParameters()
331386
end checkType
332387

333388
private def collectMethodTypes(tp: Type): List[TermLambda] = tp match

‎compiler/src/dotty/tools/dotc/core/Definitions.scala

+2
Original file line numberDiff line numberDiff line change
@@ -1010,6 +1010,7 @@ class Definitions {
10101010
@tu lazy val Caps_ContainsTrait: TypeSymbol = CapsModule.requiredType("Contains")
10111011
@tu lazy val Caps_containsImpl: TermSymbol = CapsModule.requiredMethod("containsImpl")
10121012
@tu lazy val Caps_Mutable: ClassSymbol = requiredClass("scala.caps.Mutable")
1013+
@tu lazy val Caps_SharedCapability: ClassSymbol = requiredClass("scala.caps.SharedCapability")
10131014

10141015
/** The same as CaptureSet.universal but generated implicitly for references of Capability subtypes */
10151016
@tu lazy val universalCSImpliedByCapability = CaptureSet(captureRoot.termRef.readOnly)
@@ -1071,6 +1072,7 @@ class Definitions {
10711072
@tu lazy val UncheckedCapturesAnnot: ClassSymbol = requiredClass("scala.annotation.unchecked.uncheckedCaptures")
10721073
@tu lazy val UntrackedCapturesAnnot: ClassSymbol = requiredClass("scala.caps.untrackedCaptures")
10731074
@tu lazy val UseAnnot: ClassSymbol = requiredClass("scala.caps.use")
1075+
@tu lazy val ConsumeAnnot: ClassSymbol = requiredClass("scala.caps.consume")
10741076
@tu lazy val RefineOverrideAnnot: ClassSymbol = requiredClass("scala.caps.refineOverride")
10751077
@tu lazy val VolatileAnnot: ClassSymbol = requiredClass("scala.volatile")
10761078
@tu lazy val LanguageFeatureMetaAnnot: ClassSymbol = requiredClass("scala.annotation.meta.languageFeature")

‎compiler/src/dotty/tools/dotc/util/SimpleIdentitySet.scala

+5
Original file line numberDiff line numberDiff line change
@@ -42,6 +42,11 @@ abstract class SimpleIdentitySet[+Elem <: AnyRef] {
4242
if (that.contains(x)) s else s + x
4343
}
4444

45+
def ** [E >: Elem <: AnyRef](that: SimpleIdentitySet[E]): SimpleIdentitySet[E] =
46+
if this.size == 0 then this
47+
else if that.size == 0 then that
48+
else this.filter(that.contains)
49+
4550
def == [E >: Elem <: AnyRef](that: SimpleIdentitySet[E]): Boolean =
4651
this.size == that.size && forall(that.contains)
4752

‎library/src/scala/caps.scala

+4
Original file line numberDiff line numberDiff line change
@@ -18,6 +18,8 @@ import annotation.{experimental, compileTimeOnly, retainsCap}
1818

1919
trait Mutable extends Capability
2020

21+
trait SharedCapability extends Capability
22+
2123
/** Carrier trait for capture set type parameters */
2224
trait CapSet extends Any
2325

@@ -77,6 +79,8 @@ import annotation.{experimental, compileTimeOnly, retainsCap}
7779
*/
7880
final class refineOverride extends annotation.StaticAnnotation
7981

82+
final class consume extends annotation.StaticAnnotation
83+
8084
object unsafe:
8185

8286
extension [T](x: T)

‎tests/neg-custom-args/captures/box-adapt-contra.scala

+3-2
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,5 @@
1-
import language.experimental.captureChecking
1+
import language.future // sepchecks on
2+
import caps.consume
23

34
trait Cap
45

@@ -7,7 +8,7 @@ def useCap[X](x: X): (X -> Unit) -> Unit = ???
78
def test1(c: Cap^): Unit =
89
val f: (Cap^{c} -> Unit) -> Unit = useCap[Cap^{c}](c) // error
910

10-
def test2(c: Cap^, d: Cap^): Unit =
11+
def test2(@consume c: Cap^, d: Cap^): Unit =
1112
def useCap1[X](x: X): (X => Unit) -> Unit = ???
1213
val f1: (Cap^{c} => Unit) ->{c} Unit = useCap1[Cap^{c}](c) // ok
1314

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

+7-2
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,12 @@
1-
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/capt-depfun.scala:10:43 ----------------------------------
2-
10 | val dc: ((Str^{y, z}) => Str^{y, z}) = ac(g()) // error
1+
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/capt-depfun.scala:11:43 ----------------------------------
2+
11 | val dc: ((Str^{y, z}) => Str^{y, z}) = ac(g()) // error // error: separatioon
33
| ^^^^^^^
44
| Found: Str^{} ->{ac, y, z} Str^{y, z}
55
| Required: Str^{y, z} ->{fresh} Str^{y, z}
66
|
77
| longer explanation available when compiling with `-explain`
8+
-- Error: tests/neg-custom-args/captures/capt-depfun.scala:11:24 -------------------------------------------------------
9+
11 | val dc: ((Str^{y, z}) => Str^{y, z}) = ac(g()) // error // error: separatioon
10+
| ^^^^^^^^^^^^^^^^^^^^^^^^^^
11+
| Separation failure: value dc's type Str^{y, z} => Str^{y, z} hides parameters y and z
12+
| The parameters need to be annotated with @consume to allow this.

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

+2-1
Original file line numberDiff line numberDiff line change
@@ -1,10 +1,11 @@
11
import annotation.retains
22
import language.future // sepchecks on
3+
34
class C
45
type Cap = C @retains(caps.cap)
56
class Str
67

78
def f(y: Cap, z: Cap) =
89
def g(): C @retains(y, z) = ???
910
val ac: ((x: Cap) => Str @retains(x) => Str @retains(x)) = ???
10-
val dc: ((Str^{y, z}) => Str^{y, z}) = ac(g()) // error
11+
val dc: ((Str^{y, z}) => Str^{y, z}) = ac(g()) // error // error: separatioon

‎tests/neg-custom-args/captures/consume-overrides.scala

+15
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,15 @@
1+
import caps.consume
2+
3+
trait A[X]:
4+
def foo(@consume x: X): X
5+
def bar(x: X): X
6+
7+
trait B extends A[C]:
8+
def foo(x: C): C // error
9+
def bar(@consume x: C): C // error
10+
11+
trait B2:
12+
def foo(x: C): C
13+
def bar(@consume x: C): C
14+
15+
abstract class C extends A[C], B2 // error

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

+6-6
Original file line numberDiff line numberDiff line change
@@ -1,14 +1,14 @@
1-
-- Error: tests/neg-custom-args/captures/delayedRunops.scala:16:13 -----------------------------------------------------
2-
16 | runOps(ops1) // error
1+
-- Error: tests/neg-custom-args/captures/delayedRunops.scala:17:13 -----------------------------------------------------
2+
17 | runOps(ops1) // error
33
| ^^^^
44
| reference ops* is not included in the allowed capture set {}
55
| of an enclosing function literal with expected type () -> Unit
6-
-- Error: tests/neg-custom-args/captures/delayedRunops.scala:22:13 -----------------------------------------------------
7-
22 | runOps(ops1) // error
6+
-- Error: tests/neg-custom-args/captures/delayedRunops.scala:23:13 -----------------------------------------------------
7+
23 | runOps(ops1) // error
88
| ^^^^
99
| Local reach capability ops1* leaks into capture scope of enclosing function
10-
-- Error: tests/neg-custom-args/captures/delayedRunops.scala:28:13 -----------------------------------------------------
11-
28 | runOps(ops1) // error
10+
-- Error: tests/neg-custom-args/captures/delayedRunops.scala:29:13 -----------------------------------------------------
11+
29 | runOps(ops1) // error
1212
| ^^^^
1313
| reference ops* is not included in the allowed capture set {}
1414
| of an enclosing function literal with expected type () -> Unit

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

+3-2
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,6 @@
11
import language.experimental.captureChecking
2-
import caps.use
2+
import language.future // sepchecks on
3+
import caps.{use, consume}
34

45
// ok
56
def runOps(@use ops: List[() => Unit]): Unit =
@@ -16,7 +17,7 @@ import caps.use
1617
runOps(ops1) // error
1718

1819
// unsound: impure operation pretended pure
19-
def delayedRunOps2(ops: List[() => Unit]): () ->{} Unit =
20+
def delayedRunOps2(@consume ops: List[() => Unit]): () ->{} Unit =
2021
() =>
2122
val ops1: List[() => Unit] = ops
2223
runOps(ops1) // error

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

+5
Original file line numberDiff line numberDiff line change
@@ -12,3 +12,8 @@
1212
| Required: (xs: List[box () ->{io} Unit]) ->{fresh} List[() -> Unit]
1313
|
1414
| longer explanation available when compiling with `-explain`
15+
-- Error: tests/neg-custom-args/captures/depfun-reach.scala:12:17 ------------------------------------------------------
16+
12 | : (xs: List[(X, () ->{io} Unit)]) => List[() ->{} Unit] = // error
17+
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
18+
|Separation failure: method foo's result type (xs: List[(X, box () ->{io} Unit)]) => List[() -> Unit] hides parameter op
19+
|The parameter needs to be annotated with @consume to allow this.

‎tests/neg-custom-args/captures/depfun-reach.scala

+1-1
Original file line numberDiff line numberDiff line change
@@ -9,7 +9,7 @@ def test(io: Object^, async: Object^) =
99
compose(op)
1010

1111
def foo[X](op: (xs: List[(X, () ->{io} Unit)]) => List[() ->{xs*} Unit])
12-
: (xs: List[(X, () ->{io} Unit)]) => List[() ->{} Unit] =
12+
: (xs: List[(X, () ->{io} Unit)]) => List[() ->{} Unit] = // error
1313
op // error
1414

1515
def boom(op: List[(() ->{async} Unit, () ->{io} Unit)]): List[() ->{} Unit] =

‎tests/neg-custom-args/captures/effect-swaps-explicit.scala

+2-2
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
1+
import language.future // sepchecks on
22

33
object boundary:
44

@@ -14,7 +14,7 @@ end boundary
1414

1515
import boundary.{Label, break}
1616

17-
trait Async extends caps.Capability
17+
trait Async extends caps.SharedCapability
1818
object Async:
1919
def blocking[T](body: Async ?=> T): T = ???
2020

‎tests/neg-custom-args/captures/effect-swaps.check

+11-11
Original file line numberDiff line numberDiff line change
@@ -1,29 +1,29 @@
1-
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/effect-swaps.scala:62:8 ----------------------------------
2-
61 | Result:
3-
62 | Future: // error, type mismatch
1+
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/effect-swaps.scala:64:8 ----------------------------------
2+
63 | Result:
3+
64 | Future: // error, type mismatch
44
| ^
55
| Found: Result.Ok[box Future[box T^?]^{fr, contextual$1}]
66
| Required: Result[Future[T], Nothing]
7-
63 | fr.await.ok
7+
65 | fr.await.ok
88
|--------------------------------------------------------------------------------------------------------------------
99
|Inline stack trace
1010
|- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
11-
|This location contains code that was inlined from effect-swaps.scala:39
12-
39 | boundary(Ok(body))
11+
|This location contains code that was inlined from effect-swaps.scala:41
12+
41 | boundary(Ok(body))
1313
| ^^^^^^^^
1414
--------------------------------------------------------------------------------------------------------------------
1515
|
1616
| longer explanation available when compiling with `-explain`
17-
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/effect-swaps.scala:72:10 ---------------------------------
18-
72 | Future: fut ?=> // error: type mismatch
17+
-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/effect-swaps.scala:74:10 ---------------------------------
18+
74 | Future: fut ?=> // error: type mismatch
1919
| ^
2020
| Found: Future[box T^?]^{fr, lbl}
2121
| Required: Future[box T^?]^?
22-
73 | fr.await.ok
22+
75 | fr.await.ok
2323
|
2424
| longer explanation available when compiling with `-explain`
25-
-- Error: tests/neg-custom-args/captures/effect-swaps.scala:66:15 ------------------------------------------------------
26-
66 | Result.make: // error: local reference leaks
25+
-- Error: tests/neg-custom-args/captures/effect-swaps.scala:68:15 ------------------------------------------------------
26+
68 | Result.make: // error: local reference leaks
2727
| ^^^^^^^^^^^
2828
|local reference contextual$9 from (using contextual$9: boundary.Label[Result[box Future[box T^?]^{fr, contextual$9}, box E^?]]):
2929
| box Future[box T^?]^{fr, contextual$9} leaks into outer capture set of type parameter T of method make in object Result

‎tests/neg-custom-args/captures/effect-swaps.scala

+3-1
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,5 @@
1+
import language.future // sepchecks on
2+
13
object boundary:
24

35
final class Label[-T] extends caps.Capability
@@ -12,7 +14,7 @@ end boundary
1214

1315
import boundary.{Label, break}
1416

15-
trait Async extends caps.Capability
17+
trait Async extends caps.SharedCapability
1618
object Async:
1719
def blocking[T](body: Async ?=> T): T = ???
1820

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

+5
Original file line numberDiff line numberDiff line change
@@ -39,3 +39,8 @@
3939
| Required: () -> Unit
4040
|
4141
| longer explanation available when compiling with `-explain`
42+
-- Error: tests/neg-custom-args/captures/i15772.scala:34:10 ------------------------------------------------------------
43+
34 | def c : C^ = new C(x) // error separation
44+
| ^^
45+
| Separation failure: method c's result type C^ hides parameter x
46+
| The parameter needs to be annotated with @consume to allow this.

0 commit comments

Comments
 (0)