forked from scala/scala3
-
Notifications
You must be signed in to change notification settings - Fork 17
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Handle reach capabilities correctly in markFree
The correct point to address charging reach capabilities is in markFree itself: When a reach capability goes out of scope, and that capability is not a parameter, we need to continue with the underlying capture set.
- Loading branch information
Showing
25 changed files
with
323 additions
and
114 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,14 @@ | ||
-- Error: tests/neg-custom-args/captures/delayedRunops.scala:16:13 ----------------------------------------------------- | ||
16 | runOps(ops1) // error | ||
| ^^^^ | ||
| reference ops* is not included in the allowed capture set {} | ||
| of an enclosing function literal with expected type () -> Unit | ||
-- Error: tests/neg-custom-args/captures/delayedRunops.scala:22:13 ----------------------------------------------------- | ||
22 | runOps(ops1) // error | ||
| ^^^^ | ||
| Local reach capability ops1* leaks into capture scope of enclosing function | ||
-- Error: tests/neg-custom-args/captures/delayedRunops.scala:28:13 ----------------------------------------------------- | ||
28 | runOps(ops1) // error | ||
| ^^^^ | ||
| reference ops* is not included in the allowed capture set {} | ||
| of an enclosing function literal with expected type () -> Unit |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,28 @@ | ||
import language.experimental.captureChecking | ||
import caps.unbox | ||
|
||
// ok | ||
def runOps(@unbox ops: List[() => Unit]): Unit = | ||
ops.foreach(op => op()) | ||
|
||
// ok | ||
def delayedRunOps(@unbox ops: List[() => Unit]): () ->{ops*} Unit = // @unbox should not be necessary in the future | ||
() => runOps(ops) | ||
|
||
// unsound: impure operation pretended pure | ||
def delayedRunOps1(ops: List[() => Unit]): () ->{} Unit = | ||
() => | ||
val ops1 = ops | ||
runOps(ops1) // error | ||
|
||
// unsound: impure operation pretended pure | ||
def delayedRunOps2(ops: List[() => Unit]): () ->{} Unit = | ||
() => | ||
val ops1: List[() => Unit] = ops | ||
runOps(ops1) // error | ||
|
||
// unsound: impure operation pretended pure | ||
def delayedRunOps3(ops: List[() => Unit]): () ->{} Unit = | ||
() => | ||
val ops1: List[() ->{ops*} Unit] = ops | ||
runOps(ops1) // error |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,55 @@ | ||
-- Error: tests/neg-custom-args/captures/i16114.scala:18:12 ------------------------------------------------------------ | ||
18 | expect[Cap^] { // error | ||
| ^^^^^^^^^^^^ | ||
| Sealed type variable T cannot be instantiated to box Cap^ since | ||
| that type captures the root capability `cap`. | ||
| This is often caused by a local capability in an argument of method expect | ||
| leaking as part of its result. | ||
-- Error: tests/neg-custom-args/captures/i16114.scala:20:8 ------------------------------------------------------------- | ||
20 | fs // error (limitation) | ||
| ^^ | ||
| (fs : Cap^) cannot be referenced here; it is not included in the allowed capture set {io} | ||
| of an enclosing function literal with expected type Unit ->{io} Unit | ||
-- Error: tests/neg-custom-args/captures/i16114.scala:24:12 ------------------------------------------------------------ | ||
24 | expect[Cap^] { // error | ||
| ^^^^^^^^^^^^ | ||
| Sealed type variable T cannot be instantiated to box Cap^ since | ||
| that type captures the root capability `cap`. | ||
| This is often caused by a local capability in an argument of method expect | ||
| leaking as part of its result. | ||
-- Error: tests/neg-custom-args/captures/i16114.scala:26:8 ------------------------------------------------------------- | ||
26 | io // error (limitation) | ||
| ^^ | ||
| (io : Cap^) cannot be referenced here; it is not included in the allowed capture set {fs} | ||
| of an enclosing function literal with expected type Unit ->{fs} Unit | ||
-- Error: tests/neg-custom-args/captures/i16114.scala:30:12 ------------------------------------------------------------ | ||
30 | expect[Cap^] { // error | ||
| ^^^^^^^^^^^^ | ||
| Sealed type variable T cannot be instantiated to box Cap^ since | ||
| that type captures the root capability `cap`. | ||
| This is often caused by a local capability in an argument of method expect | ||
| leaking as part of its result. | ||
-- Error: tests/neg-custom-args/captures/i16114.scala:36:12 ------------------------------------------------------------ | ||
36 | expect[Cap^](io) // error | ||
| ^^^^^^^^^^^^ | ||
| Sealed type variable T cannot be instantiated to box Cap^ since | ||
| that type captures the root capability `cap`. | ||
| This is often caused by a local capability in an argument of method expect | ||
| leaking as part of its result. | ||
-- Error: tests/neg-custom-args/captures/i16114.scala:39:12 ------------------------------------------------------------ | ||
39 | expect[Cap^] { // error | ||
| ^^^^^^^^^^^^ | ||
| Sealed type variable T cannot be instantiated to box Cap^ since | ||
| that type captures the root capability `cap`. | ||
| This is often caused by a local capability in an argument of method expect | ||
| leaking as part of its result. | ||
-- Error: tests/neg-custom-args/captures/i16114.scala:40:8 ------------------------------------------------------------- | ||
40 | io.use() // error | ||
| ^^ | ||
| (io : Cap^) cannot be referenced here; it is not included in the allowed capture set {} | ||
| of an enclosing function literal with expected type Unit -> Unit | ||
-- Error: tests/neg-custom-args/captures/i16114.scala:41:8 ------------------------------------------------------------- | ||
41 | io // error | ||
| ^^ | ||
| (io : Cap^) cannot be referenced here; it is not included in the allowed capture set {} | ||
| of an enclosing function literal with expected type Unit -> Unit |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,15 +1,12 @@ | ||
-- Error: tests/neg-custom-args/captures/i21347.scala:4:15 ------------------------------------------------------------- | ||
4 | ops.foreach: op => // error | ||
| ^ | ||
| Local reach capability C leaks into capture scope of method runOps | ||
| Capture set parameter C leaks into capture scope of method runOps. | ||
| To allow this, the type C should be declared with a @use annotation | ||
5 | op() | ||
-- Error: tests/neg-custom-args/captures/i21347.scala:8:14 ------------------------------------------------------------- | ||
8 | () => runOps(f :: Nil) // error | ||
| ^^^^^^^^^^^^^^^^ | ||
| reference (caps.cap : caps.Capability) is not included in the allowed capture set {} | ||
| of an enclosing function literal with expected type () -> Unit | ||
-- Error: tests/neg-custom-args/captures/i21347.scala:11:15 ------------------------------------------------------------ | ||
11 | ops.foreach: op => // error | ||
| ^ | ||
| Local reach capability ops* leaks into capture scope of method runOpsAlt | ||
| Local reach capability ops* leaks into capture scope of method runOpsAlt. | ||
| To allow this, the parameter ops should be declared with a @use annotation | ||
12 | op() |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Oops, something went wrong.