Skip to content

Commit

Permalink
Coarse restriction to disallow local roots in external types
Browse files Browse the repository at this point in the history
This needs to be refined further for class members, similar to how
we check that private types cannot escape from a class API.
  • Loading branch information
odersky committed Oct 30, 2023
1 parent 96928a2 commit 1065bd1
Show file tree
Hide file tree
Showing 8 changed files with 83 additions and 4 deletions.
16 changes: 16 additions & 0 deletions compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala
Original file line number Diff line number Diff line change
Expand Up @@ -1301,6 +1301,20 @@ class CheckCaptures extends Recheck, SymTransformer:
checker.traverse(tree.knownType)
end healTypeParam

def checkNoLocalRootIn(sym: Symbol, info: Type, pos: SrcPos)(using Context): Unit =
val check = new TypeTraverser:
def traverse(tp: Type) = tp match
case tp: TermRef if tp.isLocalRootCapability =>
if tp.localRootOwner == sym then
report.error(i"local root $tp cannot appear in type of $sym", pos)
case tp: ClassInfo =>
traverseChildren(tp)
for mbr <- tp.decls do
if !mbr.is(Private) then checkNoLocalRootIn(sym, mbr.info, mbr.srcPos)
case _ =>
traverseChildren(tp)
check.traverse(info)

/** Perform the following kinds of checks
* - Check all explicitly written capturing types for well-formedness using `checkWellFormedPost`.
* - Check that arguments of TypeApplys and AppliedTypes conform to their bounds.
Expand All @@ -1324,6 +1338,8 @@ class CheckCaptures extends Recheck, SymTransformer:
checkBounds(normArgs, tl)
args.lazyZip(tl.paramNames).foreach(healTypeParam(_, _, fun.symbol))
case _ =>
case _: ValOrDefDef | _: TypeDef =>
checkNoLocalRootIn(tree.symbol, tree.symbol.info, tree.symbol.srcPos)
case _ =>
end check
end checker
Expand Down
2 changes: 1 addition & 1 deletion tests/neg-custom-args/captures/filevar.scala
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,7 @@ class File:
def write(x: String): Unit = ???

class Service:
var file: File^{cap[Service]} = uninitialized
var file: File^{cap[Service]} = uninitialized // error
def log = file.write("log")

def withFile[T](op: (l: caps.Cap) ?-> (f: File^{l}) => T): T =
Expand Down
12 changes: 12 additions & 0 deletions tests/neg-custom-args/captures/localcaps.check
Original file line number Diff line number Diff line change
@@ -0,0 +1,12 @@
-- Error: tests/neg-custom-args/captures/localcaps.scala:4:12 ----------------------------------------------------------
4 | def x: C^{cap[d]} = ??? // error
| ^^^^^^
| `d` does not name an outer definition that represents a capture level
-- Error: tests/neg-custom-args/captures/localcaps.scala:9:47 ----------------------------------------------------------
9 | private val z2 = identity((x: Int) => (c: C^{cap[z2]}) => x) // error
| ^^^^^^^
| `z2` does not name an outer definition that represents a capture level
-- Error: tests/neg-custom-args/captures/localcaps.scala:6:6 -----------------------------------------------------------
6 | def y: C^{cap[C]} = ??? // error
| ^
| local root (cap[C] : caps.Cap) cannot appear in type of class C
2 changes: 1 addition & 1 deletion tests/neg-custom-args/captures/localcaps.scala
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,7 @@ class C:

def x: C^{cap[d]} = ??? // error

def y: C^{cap[C]} = ??? // ok
def y: C^{cap[C]} = ??? // error
private val z = (c0: caps.Cap) => (x: Int) => (c: C^{cap[C]}) => x // ok

private val z2 = identity((x: Int) => (c: C^{cap[z2]}) => x) // error
8 changes: 8 additions & 0 deletions tests/neg-custom-args/captures/pairs.check
Original file line number Diff line number Diff line change
Expand Up @@ -12,3 +12,11 @@
| Required: Cap^ ->{d} Unit
|
| longer explanation available when compiling with `-explain`
-- Error: tests/neg-custom-args/captures/pairs.scala:6:8 ---------------------------------------------------------------
6 | def fst: Cap^{cap[Pair]} ->{x} Unit = x // error
| ^
| local root (cap[Pair] : caps.Cap) cannot appear in type of class Pair
-- Error: tests/neg-custom-args/captures/pairs.scala:7:8 ---------------------------------------------------------------
7 | def snd: Cap^{cap[Pair]} ->{y} Unit = y // error
| ^
| local root (cap[Pair] : caps.Cap) cannot appear in type of class Pair
4 changes: 2 additions & 2 deletions tests/neg-custom-args/captures/pairs.scala
Original file line number Diff line number Diff line change
Expand Up @@ -3,8 +3,8 @@
object Monomorphic2:

class Pair(x: Cap => Unit, y: Cap => Unit):
def fst: Cap^{cap[Pair]} ->{x} Unit = x
def snd: Cap^{cap[Pair]} ->{y} Unit = y
def fst: Cap^{cap[Pair]} ->{x} Unit = x // error
def snd: Cap^{cap[Pair]} ->{y} Unit = y // error

def test(c: Cap, d: Cap) =
def f(x: Cap): Unit = if c == x then ()
Expand Down
22 changes: 22 additions & 0 deletions tests/neg-custom-args/captures/recursive-leaking-local-cap.scala
Original file line number Diff line number Diff line change
@@ -0,0 +1,22 @@
import language.experimental.captureChecking
trait Cap:
def use: Int = 42

def usingCap[sealed T](op: Cap^ => T): T = ???

def badTest(): Unit =
def bad(b: Boolean)(c: Cap^): Cap^{cap[bad]} = // error
if b then c
else
val leaked = usingCap[Cap^{cap[bad]}](bad(true))
leaked.use // boom
c

usingCap[Unit]: c0 =>
bad(false)(c0)

class Bad:
def foo: Cap^{cap[Bad]} = ??? // error
private def bar: Cap^{cap[Bad]} = ??? // ok


21 changes: 21 additions & 0 deletions tests/neg-custom-args/captures/sealed-classes.scala
Original file line number Diff line number Diff line change
@@ -0,0 +1,21 @@
abstract class C1[A1]:
def set(x: A1): Unit
def get: A1

trait Co[+A]:
def get: A

class C2[sealed A2] extends C1[A2], Co[A2]: // ok
private var x: A2 = ???
def set(x: A2): Unit =
this.x = x
def get: A2 = x

class C3[A3] extends C2[A3] // error

abstract class C4[sealed A4] extends Co[A4] // ok

abstract class C5[sealed +A5] extends Co[A5] // ok

abstract class C6[A6] extends C5[A6] // error

0 comments on commit 1065bd1

Please sign in to comment.