Make the Boogie representation of the Dafny heap use only Box #4020
Conversation
atomb
force-pushed
the
simplify-boogie-prelude
branch
from
614ab31
to
9ffc2f9
Compare
atomb
force-pushed
the
simplify-boogie-prelude
branch
from
9ffc2f9
to
5f1b0f5
Compare
atomb
force-pushed
the
simplify-boogie-prelude
branch
2 times, most recently
from
19f21ae
to
364e19c
Compare
atomb
force-pushed
the
simplify-boogie-prelude
branch
4 times, most recently
from
0e0f8ff
to
c84f471
Compare
atomb
force-pushed
the
simplify-boogie-prelude
branch
from
c84f471
to
ec9ee4f
Compare
Also reduce a little redundancy.
Fields still have type parameters, but not for long.
This reverts commit ddac03c66aa82c91696299b7fae931743c5969db.
atomb
force-pushed
the
simplify-boogie-prelude
branch
from
ec9ee4f
to
b4a9248
Compare
atomb
changed the title
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.
atomb
changed the title
atomb
changed the title
Box
atomb
changed the title
Box
| @@ -1,3 +1,4 @@ | |||
| // UNSUPPORTED: windows,posix | |||
There was a problem hiding this comment.
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.
At least it's still tested on other OS, right?
There was a problem hiding this comment.
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.
| @@ -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.
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.
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.
At least it's still tested on other OS, right?
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$Heapvariable 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
ReadHeapmethod now takes an optional type, which will ultimately be provided at all call sites. Once it is, theFieldtype 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.