From f2b7c12e6941b472086debef420e4eb3578c178a Mon Sep 17 00:00:00 2001 From: odersky Date: Sun, 31 Mar 2024 11:21:32 +0200 Subject: [PATCH] Plug unsoundness for reach capabilities Enforce an analogous restriction to the one for creating reach capabilities for all values. The type of a value cannot both have a reach capability with variance >= 0 and at the same time a universal capability with variance <= 0. Plug soundness hole for reach capabilities --- .../dotty/tools/dotc/cc/CheckCaptures.scala | 44 ++++++++++++++++++- tests/neg/unsound-reach-2.scala | 25 +++++++++++ tests/neg/unsound-reach-3.scala | 21 +++++++++ tests/neg/unsound-reach.check | 5 +++ tests/neg/unsound-reach.scala | 20 +++++++++ 5 files changed, 113 insertions(+), 2 deletions(-) create mode 100644 tests/neg/unsound-reach-2.scala create mode 100644 tests/neg/unsound-reach-3.scala create mode 100644 tests/neg/unsound-reach.check create mode 100644 tests/neg/unsound-reach.scala diff --git a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala index de584797f154..675cd012e801 100644 --- a/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala +++ b/compiler/src/dotty/tools/dotc/cc/CheckCaptures.scala @@ -249,6 +249,44 @@ class CheckCaptures extends Recheck, SymTransformer: else i"references $cs1$cs1description are not all", pos, provenance) + def showRef(ref: CaptureRef)(using Context): String = + ctx.printer.toTextCaptureRef(ref).show + + // Uses 4-space indent as a trial + def checkReachCapsIsolated(tpe: Type, pos: SrcPos)(using Context): Unit = + + object checker extends TypeTraverser: + var refVariances: Map[Boolean, Int] = Map.empty + var seenReach: CaptureRef | Null = null + def traverse(tp: Type) = + tp match + case CapturingType(parent, refs) => + traverse(parent) + for ref <- refs.elems do + if ref.isReach && !ref.stripReach.isInstanceOf[TermParamRef] + || ref.isRootCapability + then + val isReach = ref.isReach + def register() = + refVariances = refVariances.updated(isReach, variance) + seenReach = ref + refVariances.get(isReach) match + case None => register() + case Some(v) => if v != 0 && variance == 0 then register() + case _ => + traverseChildren(tp) + + checker.traverse(tpe) + if checker.refVariances.size == 2 + && checker.refVariances(true) >= 0 + && checker.refVariances(false) <= 0 + then + report.error( + em"""Reach capability ${showRef(checker.seenReach.nn)} and universal capability cap cannot both + |appear in the type $tpe of this expression""", + pos) + end checkReachCapsIsolated + /** The current environment */ private val rootEnv: Env = inContext(ictx): Env(defn.RootClass, EnvKind.Regular, CaptureSet.empty, null) @@ -779,8 +817,10 @@ class CheckCaptures extends Recheck, SymTransformer: report.error(ex.getMessage.nn) tree.tpe finally curEnv = saved - if tree.isTerm && !pt.isBoxedCapturing then - markFree(res.boxedCaptureSet, tree.srcPos) + if tree.isTerm then + checkReachCapsIsolated(res.widen, tree.srcPos) + if !pt.isBoxedCapturing then + markFree(res.boxedCaptureSet, tree.srcPos) res override def recheckFinish(tpe: Type, tree: Tree, pt: Type)(using Context): Type = diff --git a/tests/neg/unsound-reach-2.scala b/tests/neg/unsound-reach-2.scala new file mode 100644 index 000000000000..27742d72557b --- /dev/null +++ b/tests/neg/unsound-reach-2.scala @@ -0,0 +1,25 @@ +import language.experimental.captureChecking +trait Consumer[-T]: + def apply(x: T): Unit + +trait File: + def close(): Unit + +def withFile[R](path: String)(op: Consumer[File]): R = ??? + +trait Foo[+X]: + def use(x: File^)(op: Consumer[X]): Unit +class Bar extends Foo[File^]: + def use(x: File^)(op: Consumer[File^]): Unit = op.apply(x) + +def bad(): Unit = + val backdoor: Foo[File^] = new Bar + val boom: Foo[File^{backdoor*}] = backdoor + + var escaped: File^{backdoor*} = null + withFile("hello.txt"): f => + boom.use(f): // error + new Consumer[File^{backdoor*}]: + def apply(f1: File^{backdoor*}) = + escaped = f1 + diff --git a/tests/neg/unsound-reach-3.scala b/tests/neg/unsound-reach-3.scala new file mode 100644 index 000000000000..71c27fe5007d --- /dev/null +++ b/tests/neg/unsound-reach-3.scala @@ -0,0 +1,21 @@ +import language.experimental.captureChecking +trait File: + def close(): Unit + +def withFile[R](path: String)(op: File^ => R): R = ??? + +trait Foo[+X]: + def use(x: File^): X +class Bar extends Foo[File^]: + def use(x: File^): File^ = x + +def bad(): Unit = + val backdoor: Foo[File^] = new Bar + val boom: Foo[File^{backdoor*}] = backdoor + + var escaped: File^{backdoor*} = null + withFile("hello.txt"): f => + escaped = boom.use(f) // error + // boom.use: (x: File^) -> File^{backdoor*}, it is a selection so reach capabilities are allowed + // f: File^, so there is no reach capabilities + diff --git a/tests/neg/unsound-reach.check b/tests/neg/unsound-reach.check new file mode 100644 index 000000000000..fd5c401416d1 --- /dev/null +++ b/tests/neg/unsound-reach.check @@ -0,0 +1,5 @@ +-- Error: tests/neg/unsound-reach.scala:18:9 --------------------------------------------------------------------------- +18 | boom.use(f): (f1: File^{backdoor*}) => // error + | ^^^^^^^^ + | Reach capability backdoor* and universal capability cap cannot both + | appear in the type (x: File^)(op: box File^{backdoor*} => Unit): Unit of this expression diff --git a/tests/neg/unsound-reach.scala b/tests/neg/unsound-reach.scala new file mode 100644 index 000000000000..468730168019 --- /dev/null +++ b/tests/neg/unsound-reach.scala @@ -0,0 +1,20 @@ +import language.experimental.captureChecking +trait File: + def close(): Unit + +def withFile[R](path: String)(op: File^ => R): R = ??? + +trait Foo[+X]: + def use(x: File^)(op: X => Unit): Unit +class Bar extends Foo[File^]: + def use(x: File^)(op: File^ => Unit): Unit = op(x) + +def bad(): Unit = + val backdoor: Foo[File^] = new Bar + val boom: Foo[File^{backdoor*}] = backdoor + + var escaped: File^{backdoor*} = null + withFile("hello.txt"): f => + boom.use(f): (f1: File^{backdoor*}) => // error + escaped = f1 +