-
Notifications
You must be signed in to change notification settings - Fork 2
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
Mutable references: mut cells everywhere #159
Closed
Closed
Conversation
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
yannbolliger
force-pushed
the
mut-refs
branch
3 times, most recently
from
May 28, 2021 06:58
1ed66d6
to
516a967
Compare
yannbolliger
changed the title
[WIP] Mutable references sketch
Mutable references: wrap borrowed variables from the start
Jun 1, 2021
yannbolliger
force-pushed
the
mut-refs
branch
2 times, most recently
from
June 1, 2021 07:57
da1251c
to
5b0e976
Compare
yannbolliger
force-pushed
the
mut-refs
branch
4 times, most recently
from
June 4, 2021 13:20
fc19eb1
to
9272b04
Compare
yannbolliger
changed the title
Mutable references: wrap borrowed variables from the start
Mutable references: mut cells everywhere
Jun 4, 2021
Merged
yannbolliger
force-pushed
the
mut-generics
branch
from
June 7, 2021 15:42
92d8c6e
to
72d0bd3
Compare
yannbolliger
force-pushed
the
mut-generics
branch
from
June 8, 2021 10:32
72d0bd3
to
3022425
Compare
yannbolliger
force-pushed
the
mut-refs
branch
8 times, most recently
from
June 11, 2021 10:32
7896a8c
to
8fb560d
Compare
yannbolliger
force-pushed
the
mut-generics
branch
from
June 24, 2021 10:36
3022425
to
3b126e1
Compare
Closing in favour of #164. Most of the changes here are contained there. |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Proposal for supporting mutable references. Closes #140
Original solution
The envisioned solution was to wrap mutably borrowed references in a
case class MutRef[@mutable T](t: T)
when the borrow happens. At the end of the loan's lifetime, we would reassign the changes made on theMutRef
object's field back to the original object. A little example:Would have been translated to the following in Scala:
In the above example, the reassignment of changes to the original
x
is necessary because of Scala semantics. In other cases where the original is an object, Scala semantics would be correct for our use-case but Stainless is not able to track the aliasing that is created by the wrap intoMutRef
. The following examples shows a weird case of this:This is translated to the following in Scala (only the
main
is shown):Stainless correctly tracks aliasing in the first block, where the borrow happens in the argument of the function. This is probably due to the fact that the last binding of that value is still
thing
. Then, the changes are correctly applied back tothing
in theAntiAliasing
phase.For the two later blocks, this is not the case. The newly created
MutRef(thing)
is bound to a name and Stainless correctly tracks changes to theMutRef
objectsthing2
andthing3
. But it does not track the fact that they are still aliasingthing
and therefore it doesn't propagate changes back tothing
.The example demonstrates, how the manual reassignment of changes to the original object at the end of the loan's lifetime is necessary to guarantee correctness. However, to implement this revealed itself to be very hard/impossible by only looking at the HIR (high-level intermediated representation in rustc) because the HIR does not know when the lifetime of a reference is over. Rustc performs borrow checking and lifetime resolution only later in the compilation and uses the MIR (mid-level IR), a sort of CFG that is much further apart from Stainless' AST, to do so.
Work-around
Thanks to @romac, I found a solution to that problem. Instead of propagating the changes back to the original, we can lift a variable that is later borrowed into a
MutRef
from the start. In that manner, borrowing simply becomes aliasing and Stainless can track the changes to the field of the object all the way through.Thanks to the fact that
y
is aval
, Stainless is able to track the aliasing that is introduced and hence correctly verifies the above example.