Update Heapster, Monadification, and MRSolver to handle high-order SpecM functions #2017
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 30 commits
August 24, 2023 07:38
…fact that it now generates a SpecDef type
…rsive shapes and permissions to use exprCtxPureTypeTerms for the arguments, to match their definitions
…tead of a translation term
… and pis when they are type-checked, in order to make the Coq translation work in cases where these argument types have identifiers that translate to alternate Coq definitions
… information is in a reader effect and not a state effect, making it clearer where in the translator code variables are bound; also fixed #1927
… directly translates an LLVM zero initializer to a Heapster permission + SAW core term, so that we use repeatBVVec in the SAW term rather than a giant vector literal
…ainst emptyBitSet with the new termIsClosed function
added 24 commits
February 2, 2024 17:05
…e unsafeAssert Coq tactic is currently defined *after* the translation to Coq of the Prelude
… in SpecM.v instead of automatically generated
…the other way around, so that it can use the generated Num operations like tcAdd and tcMul
…e_llvmshape to make sure the user-supplied type and type description match
…ow that Heapster checks that these agree
…debug level is at least 2
…use it currently has a panic
|
@RyanGlScott Could you please re-review this? Or are there still things you think I should address? |
RyanGlScott
approved these changes
Feb 9, 2024
There was a problem hiding this comment.
Thanks, @eddywestbrook. Two minor comments, but otherwise this LGTM.
| @@ -4,12 +4,14 @@ env <- heapster_init_env_from_file "clearbufs.sawcore" "clearbufs.bc"; | |||
| // Integer types | |||
| heapster_define_perm env "int64" " " "llvmptr 64" "exists x:bv 64.eq(llvmword(x))"; | |||
|
|
|||
| // FIXME: get reachability perms working again! | |||
There was a problem hiding this comment.
This sort of thing would also be worth mentioning in an issue about re-enabling Heapster tests (should you choose to file one), along with the other FIXMEs in the heapster-saw/examples subdirectory.
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.
This PR makes changes to Heapster, Cryptol Monadification, and MRSolver to support higher-order SpecM functions. In particular, this brings things into parity with the update to the Coq definition of the
SpecMmonad which allows such functions to be defined in a sound way (theuntyped-ho-callsbranch ofentree-specs, I believe - @eddywestbrook is that right?).Outside of the technical details of Heapster, Monadification, and MRSolver, this PR:
Prelude.sawcoreinto their own file,SpecM.sawcore, which is also included by default like the Preludeheaspter-saw/exampleswhich verifies that the top-level interface of the dilithium reference implementation satisfies a Cryptol spec using MRSolver