Fix Heapster reachability permissions examples #2030
Merged
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
added 4 commits
February 9, 2024 18:29
…n eliminating sigmas, just like is used when building them
eddywestbrook
added
the
subsystem: heapster
RyanGlScott
approved these changes
Feb 16, 2024
| @@ -3,6 +3,22 @@ module iter_linked_list where | |||
|
|
|||
| import SpecM; | |||
|
|
|||
| -- Type description for the Mbox type, which is equivalent to Mbox_Ind | |||
There was a problem hiding this comment.
Should this say List/List_Ind instead of Mbox/Mbox_Ind?
There was a problem hiding this comment.
Actually, the comment needed to be slightly different, but I fixed it, thanks!
| Mbox_nil : Mbox; | ||
| Mbox_cons : Vec 64 Bool -> Vec 64 Bool -> Mbox -> BVVec 64 bv64_128 (Vec 8 Bool) -> Mbox; | ||
| -- An inductive type formulation of the Mbox type; this is just for | ||
| -- documentation purposes, and isn't used in the below |
There was a problem hiding this comment.
I think this accidentally a word:
Suggested change
| -- documentation purposes, and isn't used in the below | |
| -- documentation purposes, and isn't used in the code below |
There was a problem hiding this comment.
"In the below" is a phase often used in papers as a synonym for "in the following"
|
|
||
| primitive appendList : (T:TpDesc) -> ListTpF T -> ListTpF T -> ListTpF T; | ||
|
|
||
| {- |
There was a problem hiding this comment.
Should this chunk of commented-out code include a FIXME similar to the one in the commented-out data Mbox code in mbox.sawcore?
There was a problem hiding this comment.
Yep, I'll add that
eddywestbrook
added
the
PR: ready to merge
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.
As noted in #2027, the Heapster examples that were using reachability permissions were creating SAW core type errors in the translation to SAW core. Turns out there were not actually anything wrong with reachability permissions, just a bug in the
sigmaElimTransMfunction used by the Heapster-to-SAW translation to translate the elimination of existential permissions. This PR fixes that bug and re-enables the Heapster examples that use reachability permissions.