Skip to content

Commit

Permalink
Make reach refinement shallow (#19171)
Browse files Browse the repository at this point in the history
This is to address the following soundness issue:

```scala
trait File
val useFile: [R] -> (path: String) -> (op: File^ -> R) -> R = ???
def main(): Unit =
  val f: [R] -> (path: String) -> (op: File^ -> R) -> R = useFile
  val g: [R] -> (path: String) -> (op: File^{f*} -> R) -> R = f  // should be an error
  val leaked = g[File^{f*}]("test")(f => f)  // boom
```
  • Loading branch information
Linyxus committed Dec 6, 2023
2 parents 98184f1 + 64242f4 commit 86565a4
Show file tree
Hide file tree
Showing 3 changed files with 73 additions and 16 deletions.
63 changes: 47 additions & 16 deletions compiler/src/dotty/tools/dotc/cc/CaptureOps.scala
Original file line number Diff line number Diff line change
Expand Up @@ -236,35 +236,66 @@ extension (tp: Type)
* (2) all covariant occurrences of cap replaced by `x*`, provided there
* are no occurrences in `T` at other variances. (1) is standard, whereas
* (2) is new.
*
* For (2), multiple-flipped covariant occurrences of cap won't be replaced.
* In other words,
*
* - For xs: List[File^] ==> List[File^{xs*}], the cap is replaced;
* - while f: [R] -> (op: File^ => R) -> R remains unchanged.
*
* Without this restriction, the signature of functions like withFile:
*
* (path: String) -> [R] -> (op: File^ => R) -> R
*
* could be refined to
*
* (path: String) -> [R] -> (op: File^{withFile*} => R) -> R
*
* which is clearly unsound.
*
* Why is this sound? Covariant occurrences of cap must represent capabilities
* that are reachable from `x`, so they are included in the meaning of `{x*}`.
* At the same time, encapsulation is still maintained since no covariant
* occurrences of cap are allowed in instance types of type variables.
*/
def withReachCaptures(ref: Type)(using Context): Type =
object narrowCaps extends TypeMap:
class CheckContraCaps extends TypeTraverser:
var ok = true
def apply(t: Type) = t.dealias match
case t1 @ CapturingType(p, cs) if cs.isUniversal =>
if variance > 0 then
t1.derivedCapturingType(apply(p), ref.reach.singletonCaptureSet)
else
ok = false
t
case _ => t match
case t @ CapturingType(p, cs) =>
t.derivedCapturingType(apply(p), cs) // don't map capture set variables
case t =>
mapOver(t)
def traverse(t: Type): Unit =
if ok then
t match
case CapturingType(_, cs) if cs.isUniversal && variance <= 0 =>
ok = false
case _ =>
traverseChildren(t)

object narrowCaps extends TypeMap:
/** Has the variance been flipped at this point? */
private var isFlipped: Boolean = false

def apply(t: Type) =
val saved = isFlipped
try
if variance <= 0 then isFlipped = true
t.dealias match
case t1 @ CapturingType(p, cs) if cs.isUniversal && !isFlipped =>
t1.derivedCapturingType(apply(p), ref.reach.singletonCaptureSet)
case _ => t match
case t @ CapturingType(p, cs) =>
t.derivedCapturingType(apply(p), cs) // don't map capture set variables
case t =>
mapOver(t)
finally isFlipped = saved
ref match
case ref: CaptureRef if ref.isTrackableRef =>
val tp1 = narrowCaps(tp)
if narrowCaps.ok then
val checker = new CheckContraCaps
checker.traverse(tp)
if checker.ok then
val tp1 = narrowCaps(tp)
if tp1 ne tp then capt.println(i"narrow $tp of $ref to $tp1")
tp1
else
capt.println(i"cannot narrow $tp of $ref to $tp1")
capt.println(i"cannot narrow $tp of $ref")
tp
case _ =>
tp
Expand Down
18 changes: 18 additions & 0 deletions tests/neg-custom-args/captures/refine-reach-shallow.scala
Original file line number Diff line number Diff line change
@@ -0,0 +1,18 @@
import language.experimental.captureChecking
trait IO
def test1(): Unit =
val f: IO^ => IO^ = x => x
val g: IO^ => IO^{f*} = f // error
def test2(): Unit =
val f: [R] -> (IO^ => R) -> R = ???
val g: [R] -> (IO^{f*} => R) -> R = f // error
def test3(): Unit =
val f: [R] -> (IO^ -> R) -> R = ???
val g: [R] -> (IO^{f*} -> R) -> R = f // error
def test4(): Unit =
val xs: List[IO^] = ???
val ys: List[IO^{xs*}] = xs // ok
def test5(): Unit =
val f: [R] -> (IO^ -> R) -> IO^ = ???
val g: [R] -> (IO^ -> R) -> IO^{f*} = f // ok
val h: [R] -> (IO^{f*} -> R) -> IO^ = f // error
8 changes: 8 additions & 0 deletions tests/neg-custom-args/captures/refine-withFile.scala
Original file line number Diff line number Diff line change
@@ -0,0 +1,8 @@
import language.experimental.captureChecking

trait File
val useFile: [R] -> (path: String) -> (op: File^ -> R) -> R = ???
def main(): Unit =
val f: [R] -> (path: String) -> (op: File^ -> R) -> R = useFile
val g: [R] -> (path: String) -> (op: File^{f*} -> R) -> R = f // error
val leaked = g[File^{f*}]("test")(f => f) // boom

0 comments on commit 86565a4

Please sign in to comment.