Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Dependent function can leak scoped capability #15921

Closed
Linyxus opened this issue Aug 26, 2022 · 0 comments · Fixed by #16264
Closed

Dependent function can leak scoped capability #15921

Linyxus opened this issue Aug 26, 2022 · 0 comments · Fixed by #16264
Assignees
Labels
cc-experiment Intended to be merged with cc-experiment branch on origin itype:bug
Milestone

Comments

@Linyxus
Copy link
Contributor

Linyxus commented Aug 26, 2022

Compiler version

cc-experiment branch

Minimized code

trait Stream { def close(): Unit = (); def write(x: Any): Unit = () }

object Test {
  def usingLogFile[T](op: (c: {*} Stream) => T): T =
    val logFile = new Stream { }
    val result = op(logFile)
    logFile.close()
    result

  val later = usingLogFile { f => () => f.write(0) }
  later();  // writing to closed file!
}

Output

It compiles.

Expectation

It should not compile, since later leaks a scoped capability.

Note: the following code is rejected as expected, the only difference is the argument type of op.

trait Stream { def close(): Unit = (); def write(x: Any): Unit = () }

object Test {
  def usingLogFile[T](op: ({*} Stream) => T): T =
    val logFile = new Stream { }
    val result = op(logFile)
    logFile.close()
    result

  val later = usingLogFile { f => () => f.write(0) }
  later();  // writing to closed file!
}
@Linyxus Linyxus added itype:bug stat:needs triage Every issue needs to have an "area" and "itype" label cc-experiment Intended to be merged with cc-experiment branch on origin and removed stat:needs triage Every issue needs to have an "area" and "itype" label labels Aug 26, 2022
@Linyxus Linyxus self-assigned this Oct 19, 2022
Linyxus added a commit to dotty-staging/dotty that referenced this issue Oct 31, 2022
Linyxus added a commit to dotty-staging/dotty that referenced this issue Nov 10, 2022
odersky added a commit that referenced this issue Nov 22, 2022
Fixes #15921.

Capture checking can be unsound for dependent functions. Minimized
example:

```scala
trait Cap { def use(): Unit }

def main() = {
  val f: (io: {*} Cap) -> {} () -> Unit =
    io => () => io.use()  // should be an error

  val g: ({*} Cap) -> {} () -> Unit =
    io => () => io.use()  // error, as expected
}
```
In the above example, we issue an error for `g`, but not for `f`, which
is unsound.

The root cause of this issue is that in the `Typer` phase, we only
create `InferredTypeTree` for the result type of function values when
the expected type of the function literal is non-dependent; and later
during `Setup` of the capture checking phase, we only create capture set
variables and update the information of function symbols when its result
type tree is an `InferredTypeTree`.

To be more specific, the function literal `io => () => io.use()` in both
`f` and `g` would be expaneded into the following tree in `Typer`:
```scala
def $anonfun(io: {*} Cap): {} () -> Unit = 
  {
    {
      def $anonfun(): Unit = 
        {
          io.use()
        }
      closure($anonfun)
    }
  }
closure($anonfun)
```
For `g`, where the expected type of the function literal is
non-dependent, we would create capture set variables in `Setup` for the
return type `{} () -> Unit` and update the symbol info of the outer
`$anonfun`. For `f`, we would not do these things because `{} () ->
Unit` is not an `InferredTypeTree`.

This PR fixes this issue by typing the `DependentTypeTree` as an
`InferredTypeTree` in the typer.

~Currently, although this PR fixes the soundness problem, it brings
completeness issues, where sometimes we propagate the universal
capability to some capture sets incorrectly, which prevents some
positive test cases from being accepted. I am still investigating this
issue and thus mark this PR as a draft for now.~

The completeness problem is fixed by two additional refinements:
- preciser propagation of captured references through mapped instance
(see
[dd88672](dd88672)),
- healing ill-formed type parameter capture sets (see
[0e7d33a](0e7d33a)).
little-inferno pushed a commit to little-inferno/dotty that referenced this issue Jan 25, 2023
@Kordyjan Kordyjan added this to the 3.3.0 milestone Aug 1, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
cc-experiment Intended to be merged with cc-experiment branch on origin itype:bug
Projects
None yet
Development

Successfully merging a pull request may close this issue.

2 participants