-
Notifications
You must be signed in to change notification settings - Fork 256
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
Make the Boogie representation of the Dafny heap use only Box #4020
Conversation
614ab31
to
9ffc2f9
Compare
9ffc2f9
to
5f1b0f5
Compare
19f21ae
to
364e19c
Compare
0e0f8ff
to
c84f471
Compare
c84f471
to
ec9ee4f
Compare
Also reduce a little redundancy.
Fields still have type parameters, but not for long.
This reverts commit ddac03c66aa82c91696299b7fae931743c5969db.
ec9ee4f
to
b4a9248
Compare
It is simply too brittle and stops verifying whenever we change anything.
Change parsing of boxed values in counterexamples
This doesn't cover all uses, but fills in the obvious cases.
Box
Box
@@ -1,3 +1,4 @@ | |||
// UNSUPPORTED: windows,posix |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This test repeatedly fails essentially whenever we make any change to the Boogie encoding. So I'm disabling it for now. I think it could be refactored to be less difficult, but that would be a somewhat involved job.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
At least it's still tested on other OS, right?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
No, it's not tested anywhere. One of the other tests in that directory is disabled, too, because it doesn't reliably verify. Ultimately, it's interesting code but I'm not sure it's testing something particularly valuable. And it's so brittle that changing essentially anything in the encoding causes it to fail, even if it makes other things better.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Looks good! If it helps performance, I think monomorphization is a good process, especially as it will make the code more maintainable (I have some other ideas)
@@ -649,7 +649,7 @@ procedure $IterHavoc1(this: ref, modi: Set Box, nw: Set Box); | |||
procedure $IterCollectNewObjects(prevHeap: Heap, newHeap: Heap, this: ref, NW: Field (Set Box)) | |||
returns (s: Set Box); | |||
ensures (forall bx: Box :: { s[bx] } s[bx] <==> | |||
read(newHeap, this, NW)[bx] || | |||
(read(newHeap, this, NW) : Set Box)[bx] || |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This is not needed, but because you will eventually remove the alpha from read, you add it preventively, right?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Exactly. And the code in Dafny that generates Boogie code does this for some but not all instances of read
, as well. Once it does it everywhere, we can remove the type parameter to Field
.
@@ -1,3 +1,4 @@ | |||
// UNSUPPORTED: windows,posix |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
At least it's still tested on other OS, right?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Thanks for doing this work. I look forward to the polymorphic map types being removed, since they add a Boogie-level of boxing on top of the boxing that Dafny already does.
This PR makes a simple but significant change to the Boogie representation of the Dafny heap, ensuring that all values stored in it are of type
Box
. This makes the polymorphism in the Boogie$Heap
variable irrelevant, but does not remove it. Removing it will, unfortunately, require slightly more significant changes to Dafny itself, more than the prelude. I plan that in a separate PR, but this one already seems to reduce resource use and resource use variation a little bit, so I thought it'd be good to merge it now. These changes seem to work best if done in very small steps.The
ReadHeap
method now takes an optional type, which will ultimately be provided at all call sites. Once it is, theField
type in the prelude will no longer need a parameter and the heap can become truly monomorphic. The correct value to pass in isn't obvious at all call sites, however, so I'm filling each one in incrementally as I conclude what the right parameter should be.(Note: there are a few tests that currently fail, but I'm working on fixing them. They're independent of the main content of this PR, just perturbed by essentially any verification change.)
By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.