Skip to content

Commit 66fc880

Browse files
oderskyodersky
committed
Check accesses to non-local this in hidden sets
Allow them only in @consume methods
1 parent 7b0b80b commit 66fc880

File tree

6 files changed

+80
-34
lines changed

6 files changed

+80
-34
lines changed

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

+2-1
Original file line numberDiff line numberDiff line change
@@ -281,7 +281,8 @@ extension (tp: Type)
281281

282282
/** The first element of this path type */
283283
final def pathRoot(using Context): Type = tp.dealias match
284-
case tp1: NamedType if tp1.symbol.maybeOwner.isClass => tp1.prefix.pathRoot
284+
case tp1: TermRef if tp1.symbol.maybeOwner.isClass => tp1.prefix.pathRoot
285+
case tp1: TypeRef if !tp1.symbol.is(Param) => tp1.prefix.pathRoot
285286
case tp1 => tp1
286287

287288
/** If this part starts with `C.this`, the class `C`.

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

+24-9
Original file line numberDiff line numberDiff line change
@@ -455,15 +455,30 @@ class SepChecker(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser:
455455
val badParams = mutable.ListBuffer[Symbol]()
456456
def currentOwner = kind.dclSym.orElse(ctx.owner)
457457
for hiddenRef <- prune(refsToCheck) do
458-
val refSym = hiddenRef.pathRoot.termSymbol // TODO also hangle ThisTypes as pathRoots
459-
if refSym.exists && !refSym.info.derivesFrom(defn.Caps_SharedCapability) then
460-
if currentOwner.enclosingMethodOrClass.isProperlyContainedIn(refSym.owner.enclosingMethodOrClass) then
461-
report.error(em"""Separation failure: $descr non-local $refSym""", pos)
462-
else if refSym.is(TermParam)
463-
&& !refSym.hasAnnotation(defn.ConsumeAnnot)
464-
&& currentOwner.isContainedIn(refSym.owner)
465-
then
466-
badParams += refSym
458+
val proot = hiddenRef.pathRoot
459+
if !proot.widen.derivesFrom(defn.Caps_SharedCapability) then
460+
proot match
461+
case ref: TermRef =>
462+
val refSym = ref.symbol
463+
if currentOwner.enclosingMethodOrClass.isProperlyContainedIn(refSym.maybeOwner.enclosingMethodOrClass) then
464+
report.error(em"""Separation failure: $descr non-local $refSym""", pos)
465+
else if refSym.is(TermParam)
466+
&& !refSym.hasAnnotation(defn.ConsumeAnnot)
467+
&& currentOwner.isContainedIn(refSym.owner)
468+
then
469+
badParams += refSym
470+
case ref: ThisType =>
471+
val encl = currentOwner.enclosingMethodOrClass
472+
if encl.isProperlyContainedIn(ref.cls)
473+
&& !encl.is(Synthetic)
474+
&& !encl.hasAnnotation(defn.ConsumeAnnot)
475+
then
476+
report.error(
477+
em"""Separation failure: $descr non-local this of class ${ref.cls}.
478+
|The access must be in a @consume method to allow this.""",
479+
pos)
480+
case _ =>
481+
467482
if badParams.nonEmpty then
468483
def paramsStr(params: List[Symbol]): String = (params: @unchecked) match
469484
case p :: Nil => i"${p.name}"

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

+17-8
Original file line numberDiff line numberDiff line change
@@ -698,15 +698,24 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI:
698698
*/
699699
def checkProperUseOrConsume(tree: Tree)(using Context): Unit = tree match
700700
case tree: MemberDef =>
701-
for ann <- tree.symbol.annotations do
702-
def isAllowedFor(sym: Symbol) =
703-
(sym.is(Param) || sym.is(ParamAccessor))
704-
&& (ann.symbol != defn.ConsumeAnnot || sym.isTerm)
701+
val sym = tree.symbol
702+
def isMethodParam = (sym.is(Param) || sym.is(ParamAccessor))
705703
&& !sym.owner.isAnonymousFunction
706-
def termStr =
707-
if ann.symbol == defn.ConsumeAnnot then " term" else ""
708-
if defn.ccParamOnlyAnnotations.contains(ann.symbol) && !isAllowedFor(tree.symbol) then
709-
report.error(i"Only$termStr parameters of methods can have @${ann.symbol.name} annotations", tree.srcPos)
704+
for ann <- tree.symbol.annotations do
705+
val annotCls = ann.symbol
706+
if annotCls == defn.ConsumeAnnot then
707+
if !(isMethodParam && sym.isTerm)
708+
&& !(sym.is(Method) && sym.owner.isClass)
709+
then
710+
report.error(
711+
em"""@consume cannot be used here. Only memeber methods and their term parameters
712+
|can have @consume annotations.""",
713+
tree.srcPos)
714+
else if annotCls == defn.UseAnnot then
715+
if !isMethodParam then
716+
report.error(
717+
em"@use cannot be used here. Only method parameters can have @use annotations.",
718+
tree.srcPos)
710719
case _ =>
711720
end checkProperUseOrConsume
712721
end setupTraverser

‎tests/neg-custom-args/captures/bad-uses-2.scala

+1-1
Original file line numberDiff line numberDiff line change
@@ -6,7 +6,7 @@ class TestUse:
66
def foo[@use T](@use c: T): Unit = ??? // OK
77

88
class TestConsume:
9-
@consume def F = ??? // error
9+
@consume def F = ??? // ok
1010
@consume val x = ??? // error
1111
@consume type T // error
1212
def foo[@consume T](@use c: T): Unit = ??? // error

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

+29-14
Original file line numberDiff line numberDiff line change
@@ -1,29 +1,44 @@
1-
-- Error: tests/neg-custom-args/captures/linear-buffer.scala:13:17 -----------------------------------------------------
2-
13 | val buf3 = app(buf, 3) // error
1+
-- Error: tests/neg-custom-args/captures/linear-buffer.scala:5:24 ------------------------------------------------------
2+
5 | mut def append(x: T): BadBuffer[T]^ = this // error
3+
| ^^^^^^^^^^^^^
4+
| Separation failure: method append's result type BadBuffer[T]^ hides non-local this of class class BadBuffer.
5+
| The access must be in a @consume method to allow this.
6+
-- Error: tests/neg-custom-args/captures/linear-buffer.scala:7:13 ------------------------------------------------------
7+
7 | def bar: BadBuffer[T]^ = this // error
8+
| ^^^^^^^^^^^^^
9+
| Separation failure: method bar's result type BadBuffer[T]^ hides non-local this of class class BadBuffer.
10+
| The access must be in a @consume method to allow this.
11+
-- Error: tests/neg-custom-args/captures/linear-buffer.scala:6:9 -------------------------------------------------------
12+
6 | def foo = // error
13+
| ^
14+
|Separation failure: method foo's inferred result type BadBuffer[box T^?]^ hides non-local this of class class BadBuffer.
15+
|The access must be in a @consume method to allow this.
16+
-- Error: tests/neg-custom-args/captures/linear-buffer.scala:19:17 -----------------------------------------------------
17+
19 | val buf3 = app(buf, 3) // error
318
| ^^^
419
| Separation failure: Illegal access to (buf : Buffer[Int]^),
5-
| which was passed to a @consume parameter on line 11
20+
| which was passed to a @consume parameter on line 17
621
| and therefore is no longer available.
7-
-- Error: tests/neg-custom-args/captures/linear-buffer.scala:20:17 -----------------------------------------------------
8-
20 | val buf3 = app(buf1, 4) // error
22+
-- Error: tests/neg-custom-args/captures/linear-buffer.scala:26:17 -----------------------------------------------------
23+
26 | val buf3 = app(buf1, 4) // error
924
| ^^^^
1025
| Separation failure: Illegal access to (buf1 : Buffer[Int]^),
11-
| which was passed to a @consume parameter on line 18
26+
| which was passed to a @consume parameter on line 24
1227
| and therefore is no longer available.
13-
-- Error: tests/neg-custom-args/captures/linear-buffer.scala:28:17 -----------------------------------------------------
14-
28 | val buf3 = app(buf1, 4) // error
28+
-- Error: tests/neg-custom-args/captures/linear-buffer.scala:34:17 -----------------------------------------------------
29+
34 | val buf3 = app(buf1, 4) // error
1530
| ^^^^
1631
| Separation failure: Illegal access to (buf1 : Buffer[Int]^),
17-
| which was passed to a @consume parameter on line 25
32+
| which was passed to a @consume parameter on line 31
1833
| and therefore is no longer available.
19-
-- Error: tests/neg-custom-args/captures/linear-buffer.scala:38:17 -----------------------------------------------------
20-
38 | val buf3 = app(buf1, 4) // error
34+
-- Error: tests/neg-custom-args/captures/linear-buffer.scala:44:17 -----------------------------------------------------
35+
44 | val buf3 = app(buf1, 4) // error
2136
| ^^^^
2237
| Separation failure: Illegal access to (buf1 : Buffer[Int]^),
23-
| which was passed to a @consume parameter on line 33
38+
| which was passed to a @consume parameter on line 39
2439
| and therefore is no longer available.
25-
-- Error: tests/neg-custom-args/captures/linear-buffer.scala:42:8 ------------------------------------------------------
26-
42 | app(buf, 1) // error
40+
-- Error: tests/neg-custom-args/captures/linear-buffer.scala:48:8 ------------------------------------------------------
41+
48 | app(buf, 1) // error
2742
| ^^^
2843
| Separation failure: (buf : Buffer[Int]^) appears in a loop,
2944
| therefore it cannot be passed to a @consume parameter.

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

+7-1
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,14 @@
11
import caps.{cap, consume, Mutable}
22
import language.experimental.captureChecking
33

4+
class BadBuffer[T] extends Mutable:
5+
mut def append(x: T): BadBuffer[T]^ = this // error
6+
def foo = // error
7+
def bar: BadBuffer[T]^ = this // error
8+
bar
9+
410
class Buffer[T] extends Mutable:
5-
mut def append(x: T): Buffer[T]^ = ???
11+
@consume mut def append(x: T): Buffer[T]^ = this // ok
612

713
def app[T](@consume buf: Buffer[T]^, elem: T): Buffer[T]^ =
814
buf.append(elem)

0 commit comments

Comments
 (0)