Skip to content

Commit c45bb88

Browse files
oderskyodersky
committed
Make sure fresh results of methods only hide local refs
1 parent ce339c1 commit c45bb88

File tree

12 files changed

+77
-35
lines changed

12 files changed

+77
-35
lines changed

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -281,7 +281,7 @@ 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.owner.isClass => tp1.prefix.pathRoot
284+
case tp1: NamedType if tp1.symbol.maybeOwner.isClass => tp1.prefix.pathRoot
285285
case tp1 => tp1
286286

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

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

Lines changed: 25 additions & 20 deletions
Original file line numberDiff line numberDiff line change
@@ -346,17 +346,19 @@ class SepChecker(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser:
346346
case t =>
347347
foldOver(c, t)
348348

349-
def checkParams(refsToCheck: Refs, descr: => String) =
349+
def checkRefs(refsToCheck: Refs, descr: => String) =
350350
val badParams = mutable.ListBuffer[Symbol]()
351351
def currentOwner = kind.dclSym.orElse(ctx.owner)
352-
for hiddenRef <- prune(refsToCheck.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
352+
for hiddenRef <- prune(refsToCheck) do
353+
val refSym = hiddenRef.pathRoot.termSymbol // TODO also hangle ThisTypes as pathRoots
354+
if refSym.exists && !refSym.info.derivesFrom(defn.Caps_SharedCapability) then
355+
if currentOwner.enclosingMethodOrClass.isProperlyContainedIn(refSym.owner.enclosingMethodOrClass) then
356+
report.error(em"""Separation failure: $descr non-local $refSym""", pos)
357+
else if refSym.is(TermParam)
358+
&& !refSym.hasAnnotation(defn.ConsumeAnnot)
359+
&& currentOwner.isContainedIn(refSym.owner)
360+
then
361+
badParams += refSym
360362
if badParams.nonEmpty then
361363
def paramsStr(params: List[Symbol]): String = (params: @unchecked) match
362364
case p :: Nil => i"${p.name}"
@@ -368,25 +370,28 @@ class SepChecker(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser:
368370
|The parameter$pluralS need$singleS to be annotated with @consume to allow this.""",
369371
pos)
370372

371-
def checkParameters() = kind match
373+
def checkLegalRefs() = kind match
372374
case TypeKind.Result(sym, _) =>
373375
if !sym.isAnonymousFunction // we don't check return types of anonymous functions
374376
&& !sym.is(Case) // We don't check so far binders in patterns since they
375377
// have inferred universal types. TODO come back to this;
376378
// either infer more precise types for such binders or
377379
// "see through them" when we look at hidden sets.
378-
then checkParams(tpe.deepCaptureSet.elems.hidden, i"$typeDescr type $tpe hides")
380+
then
381+
val refs = tpe.deepCaptureSet.elems
382+
val toCheck = refs.hidden.footprint -- refs.footprint
383+
checkRefs(toCheck, i"$typeDescr type $tpe hides")
379384
case TypeKind.Argument(arg) =>
380385
if tpe.hasAnnotation(defn.ConsumeAnnot) then
381386
val capts = captures(arg)
382387
def descr(verb: String) = i"argument to @consume parameter with type ${arg.nuType} $verb"
383-
checkParams(capts, descr("refers to"))
384-
checkParams(capts.hidden, descr("hides"))
388+
checkRefs(capts.footprint, descr("refers to"))
389+
checkRefs(capts.hidden.footprint, descr("hides"))
385390

386391
if !tpe.hasAnnotation(defn.UntrackedCapturesAnnot) then
387392
traverse(Captures.None, tpe)
388393
traverse.toCheck.foreach(checkParts)
389-
checkParameters()
394+
checkLegalRefs()
390395
end checkType
391396

392397
private def collectMethodTypes(tp: Type): List[TermLambda] = tp match
@@ -426,10 +431,12 @@ class SepChecker(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser:
426431
if argss.nestedExists(_.needsSepCheck) then
427432
checkApply(tree, argss.flatten, dependencies(tree, argss))
428433

434+
def isUnsafeAssumeSeparate(tree: Tree)(using Context): Boolean = tree match
435+
case tree: Apply => tree.symbol == defn.Caps_unsafeAssumeSeparate
436+
case _ => false
437+
429438
def traverse(tree: Tree)(using Context): Unit =
430-
tree match
431-
case tree: Apply if tree.symbol == defn.Caps_unsafeAssumeSeparate => return
432-
case _ =>
439+
if isUnsafeAssumeSeparate(tree) then return
433440
checkUse(tree)
434441
tree match
435442
case tree: GenericApply =>
@@ -446,7 +453,7 @@ class SepChecker(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser:
446453
defsShadow = saved
447454
case tree: ValOrDefDef =>
448455
traverseChildren(tree)
449-
if !tree.symbol.isOneOf(TermParamOrAccessor) then
456+
if !tree.symbol.isOneOf(TermParamOrAccessor) && !isUnsafeAssumeSeparate(tree.rhs) then
450457
checkType(tree.tpt, tree.symbol)
451458
if previousDefs.nonEmpty then
452459
capt.println(i"sep check def ${tree.symbol}: ${tree.tpt} with ${captures(tree.tpt).hidden.footprint}")
@@ -460,5 +467,3 @@ end SepChecker
460467

461468

462469

463-
464-

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

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -12,3 +12,7 @@
1212
| ^^^^
1313
| reference ops* is not included in the allowed capture set {}
1414
| of an enclosing function literal with expected type () -> Unit
15+
-- Error: tests/neg-custom-args/captures/delayedRunops.scala:22:16 -----------------------------------------------------
16+
22 | val ops1: List[() => Unit] = ops // error
17+
| ^^^^^^^^^^^^^^^^
18+
| Separation failure: value ops1's type List[box () => Unit] hides non-local parameter ops

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -19,7 +19,7 @@ import caps.{use, consume}
1919
// unsound: impure operation pretended pure
2020
def delayedRunOps2(@consume ops: List[() => Unit]): () ->{} Unit =
2121
() =>
22-
val ops1: List[() => Unit] = ops
22+
val ops1: List[() => Unit] = ops // error
2323
runOps(ops1) // error
2424

2525
// unsound: impure operation pretended pure

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

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -42,5 +42,4 @@
4242
-- Error: tests/neg-custom-args/captures/i15772.scala:34:10 ------------------------------------------------------------
4343
34 | def c : C^ = new C(x) // error separation
4444
| ^^
45-
| Separation failure: method c's result type C^ hides parameter x.
46-
| The parameter needs to be annotated with @consume to allow this.
45+
| Separation failure: method c's result type C^ hides non-local parameter x

‎tests/neg-custom-args/captures/non-local-consume.scala

Lines changed: 23 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,23 @@
1+
import caps.{cap, consume, Mutable}
2+
import language.experimental.captureChecking
3+
4+
class Buffer extends Mutable
5+
6+
def f1(@consume buf: Buffer^): Buffer^ =
7+
val buf1: Buffer^ = buf // OK
8+
buf1
9+
10+
def f2(@consume buf: Buffer^): Buffer^ =
11+
def g(): Buffer^ = buf // error
12+
g()
13+
14+
def f3(@consume buf: Buffer^): Buffer^ =
15+
val buf1 = buf
16+
def g(): Buffer^ = buf1 // error
17+
g()
18+
19+
def f4(@consume buf: Buffer^): Buffer^ =
20+
val buf1: Buffer^ = buf
21+
def g(): Buffer^ = buf1 // error
22+
g()
23+

‎tests/neg-custom-args/captures/sep-use.check

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -4,18 +4,30 @@
44
| Separation failure: Illegal access to {io} which is hidden by the previous definition
55
| of value x with type () => Unit.
66
| This type hides capabilities {io}
7+
-- Error: tests/neg-custom-args/captures/sep-use.scala:12:12 -----------------------------------------------------------
8+
12 | def x: () => Unit = () => println(io) // error
9+
| ^^^^^^^^^^
10+
| Separation failure: method x's result type () => Unit hides non-local parameter io
711
-- Error: tests/neg-custom-args/captures/sep-use.scala:13:10 -----------------------------------------------------------
812
13 | println(io) // error
913
| ^^
1014
| Separation failure: Illegal access to {io} which is hidden by the previous definition
1115
| of method x with result type () => Unit.
1216
| This type hides capabilities {io}
17+
-- Error: tests/neg-custom-args/captures/sep-use.scala:18:10 -----------------------------------------------------------
18+
18 | def xx: (y: Int) => Unit = _ => println(io) // error
19+
| ^^^^^^^^^^^^^^^^
20+
| Separation failure: method xx's result type (y: Int) => Unit hides non-local parameter io
1321
-- Error: tests/neg-custom-args/captures/sep-use.scala:19:10 -----------------------------------------------------------
1422
19 | println(io) // error
1523
| ^^
1624
| Separation failure: Illegal access to {io} which is hidden by the previous definition
1725
| of method xx with result type (y: Int) => Unit.
1826
| This type hides capabilities {io}
27+
-- Error: tests/neg-custom-args/captures/sep-use.scala:24:19 -----------------------------------------------------------
28+
24 | def xxx(y: Int): Object^ = io // error
29+
| ^^^^^^^
30+
| Separation failure: method xxx's result type Object^ hides non-local parameter io
1931
-- Error: tests/neg-custom-args/captures/sep-use.scala:25:10 -----------------------------------------------------------
2032
25 | println(io) // error
2133
| ^^

‎tests/neg-custom-args/captures/sep-use.scala

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -9,19 +9,19 @@ def test1(@consume io: Object^): Unit =
99

1010
def test2(@consume io: Object^): Unit =
1111

12-
def x: () => Unit = () => println(io)
12+
def x: () => Unit = () => println(io) // error
1313
println(io) // error
1414
println(x) // ok
1515

1616
def test3(@consume io: Object^): Unit =
1717

18-
def xx: (y: Int) => Unit = _ => println(io)
18+
def xx: (y: Int) => Unit = _ => println(io) // error
1919
println(io) // error
2020
println(xx(2)) // ok
2121

2222
def test4(@consume io: Object^): Unit =
2323

24-
def xxx(y: Int): Object^ = io
24+
def xxx(y: Int): Object^ = io // error
2525
println(io) // error
2626
println(xxx(2)) // ok
2727

‎tests/neg-custom-args/captures/sep-use2.scala

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -2,7 +2,7 @@
22
import caps.consume
33

44
def test1(@consume c: Object^, f: Object^ => Object^) =
5-
def cc: Object^ = c
5+
def cc: Object^ = c // error
66
val x1 =
77
{ f(cc) } // ok
88
val x2 =
@@ -13,7 +13,7 @@ def test1(@consume c: Object^, f: Object^ => Object^) =
1313
{ f(c) } // error
1414

1515
def test2(@consume c: Object^, f: Object^ ->{c} Object^) =
16-
def cc: Object^ = c
16+
def cc: Object^ = c // error
1717
val x1 =
1818
{ f(cc) } // error // error
1919
val x4: Object^ =

‎tests/neg-custom-args/captures/unsound-reach-6.check

Lines changed: 2 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -6,10 +6,8 @@
66
-- Error: tests/neg-custom-args/captures/unsound-reach-6.scala:11:14 ---------------------------------------------------
77
11 | val z = f(ys) // error @consume failure
88
| ^^
9-
|Separation failure: argument to @consume parameter with type (ys : List[box () ->{io} Unit]) refers to parameters ys and io.
10-
|The parameters need to be annotated with @consume to allow this.
9+
|Separation failure: argument to @consume parameter with type (ys : List[box () ->{io} Unit]) refers to non-local parameter ys
1110
-- Error: tests/neg-custom-args/captures/unsound-reach-6.scala:19:14 ---------------------------------------------------
1211
19 | val z = f(ys) // error @consume failure
1312
| ^^
14-
|Separation failure: argument to @consume parameter with type (ys : -> List[box () ->{io} Unit]) refers to parameter io.
15-
|The parameter needs to be annotated with @consume to allow this.
13+
|Separation failure: argument to @consume parameter with type (ys : -> List[box () ->{io} Unit]) refers to non-local parameter io

‎tests/pos-custom-args/captures/eta-expansions.scala

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ class Cap extends caps.Capability
33
def test(d: Cap) =
44
def map2(xs: List[Int])(f: Int => Int): List[Int] = xs.map(f)
55
val f1 = map2 // capture polymorphic implicit eta expansion
6-
def f2c: List[Int] => (Int => Int) => List[Int] = f1
6+
val f2c: List[Int] => (Int => Int) => List[Int] = f1
77
val a0 = identity[Cap ->{d} Unit] // capture monomorphic implicit eta expansion
88
val a0c: (Cap ->{d} Unit) ->{d} Cap ->{d} Unit = a0
99
val b0 = (x: Cap ->{d} Unit) => identity[Cap ->{d} Unit](x) // not an implicit eta expansion, hence capture polymorphic

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

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,9 @@
11

22
import caps.consume
3+
import caps.unsafe.unsafeAssumeSeparate
34

45
def Test(@consume c: Object^, f: Object^ => Object^) =
5-
def cc: Object^ = c
6+
def cc: Object^ = unsafeAssumeSeparate(c)
67
val x1 =
78
{ f(cc) }
89
val x2 =

0 commit comments

Comments
 (0)