Changes to Fresh and Separation Checking #24112
Conversation
Also: Factor out Vars that are part of inferred types of vals and defs as ProperVars.
New definition does not go upwards from hidden to hiding, but does go into hidden sets. Except for a variant `exposedPeaks` which does not do that. This is currently very rough. There's a switch to go from old to new behavior based on source version. Todo: Polish and then drop the switch if we are convinced verything works as expected.
Ensure that capset variables in types of vals and result types of non-anonymous functions contain only a single FreshCap, and furthermore that that FreshCap has as origin InDecl(owner), where owner is the val or def for which the type is defined.
That was needed only to order fresh caps to find the peak of peaks but we don't do that anymore.
Classifiers are ignored in covers.
odersky
requested review from
Linyxus and
bracevac
and removed request for
Linyxus
| * x covers x | ||
| * x covers y ==> x covers y.f | ||
| * x covers y ==> x* covers y*, x? covers y? | ||
| * x covers y ==> x.only[C] covers y, x covers y.only[C] |
There was a problem hiding this comment.
This seems dubious. We can derive that x.only[C] covers x. Couldn't we pick a C that would exclude x? Maybe it's fine in the usage contexts of covers? What's the expected interaction of covers and substitution of capture sets?
There was a problem hiding this comment.
This clause is a conservative over-approximation: basically, we can't achieve
separation by having different classifiers for now. I would be good to
have a test that would expect such separation, then we can try to refine
the clause to make the test pass.
| arg.formalType.orElse(arg.nuType).deepCaptureSet.elems | ||
| arg.formalType.orElse(arg.nuType).spanCaptureSet.elems | ||
|
|
||
| /** The span capture set if the type of `tree` */ |
There was a problem hiding this comment.
| /** The span capture set if the type of `tree` */ | |
| /** The span capture set of the type of `tree` */ |
| private def spanCaptures(tree: Tree)(using Context): Refs = | ||
| tree.nuType.spanCaptureSet.elems | ||
|
|
||
| /** The deep capture set if the type of `tree` */ |
There was a problem hiding this comment.
| /** The deep capture set if the type of `tree` */ | |
| /** The deep capture set of the type of `tree` */ |
| private def spanCaptures(tree: Tree)(using Context): Refs = | ||
| tree.nuType.spanCaptureSet.elems | ||
|
|
||
| /** The deep capture set if the type of `tree` */ |
There was a problem hiding this comment.
| /** The deep capture set if the type of `tree` */ | |
| /** The deep capture set of the type of `tree` */ |
| * - one of the sets contains `r.rd` | ||
| * - the other contains a capability `s` where `s` _covers_ `r` | ||
| * | ||
| * A capability `s` covers `r` if `r` can be seen as a path extension of `s`. E.g. |
There was a problem hiding this comment.
Should be in sync with the comment describing def covers in Capability.scala.
| val left = src1.transformValuesWith(Left(_)) | ||
| val right = src2.transformValuesWith(Right(_)) | ||
| val left = src1.transformValuesWith(Left(_)) // error | ||
| val right = src2.transformValuesWith(Right(_)) // error |
There was a problem hiding this comment.
It's not clear why these should be errors.
There was a problem hiding this comment.
I now added the .check file. It reads:
-- Error: tests/neg-custom-args/captures/cc-poly-varargs.scala:11:13 ---------------------------------------------------
11 | val left = src1.transformValuesWith(Left()) // error
| ^^^^
|Separation failure: argument of type (src1 : Source[T1, scala.caps.CapSet^{Cap}]^{Cap})
|to method transformValuesWith: [T, Cap >: scala.caps.CapSet <: scala.caps.CapSet^]
| (src: Source[T, scala.caps.CapSet^{Cap}]^)[U](f: T ->{Cap} U): Source[U, scala.caps.CapSet^{Cap}]^{src, f}
|corresponds to capture-polymorphic formal parameter src of type Source[T1^'s3, scala.caps.CapSet^{Cap}]^
|and hides capabilities {src1}.
|Some of these overlap with the captures of the function result with type Source[Left[T1^'s1, Nothing]^'s2, scala.caps.CapSet^{Cap}]^{src1}.
|
| Hidden set of current argument : {src1}
| Hidden footprint of current argument : {src1, Cap}
| Capture set of function result : {src1, Cap}
| Footprint set of function result : {src1, Cap}
| The two sets overlap at : {src1, Cap}
|
|where: ^ refers to a fresh root capability created in value left when checking argument to parameter src of method transformValuesWith
-- Error: tests/neg-custom-args/captures/cc-poly-varargs.scala:12:14 ---------------------------------------------------
12 | val right = src2.transformValuesWith(Right()) // error
| ^^^^
|Separation failure: argument of type (src2 : Source[T2, scala.caps.CapSet^{Cap}]^{Cap})
|to method transformValuesWith: [T, Cap >: scala.caps.CapSet <: scala.caps.CapSet^]
| (src: Source[T, scala.caps.CapSet^{Cap}]^)[U](f: T ->{Cap} U): Source[U, scala.caps.CapSet^{Cap}]^{src, f}
|corresponds to capture-polymorphic formal parameter src of type Source[T2^'s6, scala.caps.CapSet^{Cap}]^
|and hides capabilities {src2}.
|Some of these overlap with the captures of the function result with type Source[Right[Nothing, T2^'s4]^'s5, scala.caps.CapSet^{Cap}]^{src2}.
|
| Hidden set of current argument : {src2}
| Hidden footprint of current argument : {src2, Cap}
| Capture set of function result : {src2, Cap}
| Footprint set of function result : {src2, Cap}
| The two sets overlap at : {src2, Cap}
|
|where: ^ refers to a fresh root capability created in value right when checking argument to parameter src of method transformValuesWith
So the problem seems to be that src also appears in the function result. @Linyxus can you comment whether the errors are correct?
There was a problem hiding this comment.
After discussion & investigation we agree that this is supposed to fail.
Without the extension method acrobatics the function is essentially:
def f[T, Cap^](src: Source[T, {Cap}]^)[U](f: (T -> U)^{Cap}): Source[U, {Cap}]^{src, f} = ...
In the application
f(src1)(Left(_))
The intermediate result type of f[T1, {Cap}](src1) is
[U] -> (f: (T -> U)^{Cap}) -> Source[U, {Cap}]^{src1, f}
which indeed interferes with the argument src1 (overlapping at Cap).
The example itself is quite bizzard: it re-uses the same Cap parameter for multiple captures, which results in quite a lot of overlaps. Previously, it passes because the implementation was unsound.
Writing the function this way
def either[T1, T2, Cap^](
src1: Source[T1, {Cap}]^,
src2: Source[T2, {Cap}]^): Source[Either[T1, T2], {Cap}]^{Cap} = ...
will fix the error.
There was a problem hiding this comment.
IIRC, this example was conceived without separation checking in mind,
and the capture parameter expresses that the arguments indeed share the same capture set (resp. we expect inference to assign the least upper bound if they are different).
I'm somewhat surprised by your suggestion for either's signature, because it makes less sense to me. The capture parameter appears in the qualifier of the result type, but seems to have no connection to the parameters.
There was a problem hiding this comment.
I believe this should be the intended version:
import language.experimental.captureChecking
import language.experimental.separationChecking
abstract class Source[+T, Cap^]
extension[T, Cap^](src: Source[T, {Cap}]^)
def transformValuesWith[U](f: (T -> U)^{src, caps.cap}): Source[U, {Cap}]^{src, f} = ???
def race[T, Cap^, D^](sources: Source[T, {Cap}]^{D}*): Source[T, {Cap}]^{D} = ???
def either[T1, T2, Cap^](
src1: Source[T1, {Cap}]^,
src2: Source[T2, {Cap}]^): Source[Either[T1, T2], {Cap}]^{src1, src2} =
val left = src1.transformValuesWith(Left(_)) // ok
val right = src2.transformValuesWith(Right(_)) // ok
race(left, right)
It compiles on this branch. We could probably do away with the Cap^ parameter entirely. @odersky
There was a problem hiding this comment.
import language.experimental.captureChecking
import language.experimental.separationChecking
abstract class Source[+T]
extension[T](src: Source[T]^)
def transformValuesWith[U](f: (T -> U)^{src, caps.cap}): Source[U]^{src, f} = ???
def race[T, D^](sources: Source[T]^{D}*): Source[T]^{D} = ???
def either[T1, T2](
src1: Source[T1]^,
src2: Source[T2]^): Source[Either[T1, T2]]^{src1, src2} =
val left = src1.transformValuesWith(Left(_)) // ok
val right = src2.transformValuesWith(Right(_)) // ok
race(left, right)Further cleaned up.
There was a problem hiding this comment.
Great! They look much better. Let's add these versions to tests too.
There was a problem hiding this comment.
Agreed. Let's put that as a pos test. I am still unsure whether the original neg test should fail or whether we are too conservative here. In any case it would be good to point out the actual problem is Cap, not src1.
There was a problem hiding this comment.
I'll add the pos test to the next PR on fresh prefixes on which I am currently working.
In this PR, I originally only wanted to change the scheme handling fresh caps: Capture sets in the type of a val or the result type of a def should only have a single fresh that had the val or def as its origin. Any other fresh caps that were inferred before in those sets should instead be hidden by the unique fresh.
But doing this disturbed the system sufficiently to cause new problems in separation checking. These problems were caused by incorrect algorithms that had to be fixed first. The current status of the separation checker is "improved relative to the state before, but still a way to go".