Submodules: Adapt to GaloisInc/crucible#914, GaloisInc/crucible#906, and GaloisInc/crucible#928 #1521
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
There was a problem hiding this comment.
All the Hepaster-related changes look good to me, and it appears that all the Heapster tests work. I'm not going to "approve" because I think it makes more sense for @brianhuffman to look at all the other changes. Thanks for removing all that annoying extra whitespace, btw!
This bumps the `crucible` submodule to include GaloisInc/crucible#914. This also bumps the `macaw` submodule to include GaloisInc/macaw#244, which adapts `macaw-symbolic` to the `crucible` changes. These `crucible` changes require some tweaks in the following libraries: * In `heapster-saw`, we need to add a `NuMatching1` instance for `GlobalVar` now that `LLVM_SideConditions` has a field of type `GlobalVar Mem`. This also requires defining an opaque `NuMatching` instance for `Nonce` to support the `NuMatching1` instance for `GlobalVar`. Elsewhere in `heapster-saw`, we need to adapt a pattern match on `LLVM_SideConditions` to accommodate its new field. * In `saw-script`, we need to make sure that `?recordLLVMAnnotation` is given three arguments, not two, so that its type matches what `HasLLVMAnn` expects.
This bumps the `crucible` submodule to include GaloisInc/crucible#906. This also bumps the `macaw` submodule to include GaloisInc/macaw#245, which adapts `macaw-symbolic` to the `crucible` changes. The `crucible` changes require adding some additional `?memOpts :: MemOptions` and `HasLLVMAnn Sym` constraints to various functions in `saw-script`.
This bumps the `crucible` submodule to include GaloisInc/crucible#928. The `crucible` changes require adding some additional `?memOpts :: MemOptions` constraints to various functions.
RyanGlScott
force-pushed
the
crucible-submod-bump
branch
from
0c4c622
to
acb7894
Compare
RyanGlScott
changed the title
|
I also pushed an additional commits which adapts |
robdockins
approved these changes
Dec 6, 2021
RyanGlScott
added
the
PR: ready to merge
|
Mergify isn't automatically landing this, apparently due to our use of the |
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 contains three submodule-updating commits to bring
saw-script'scruciblesubmodule up to date. The commit messages for each commits are included below for reference:Adapt to GaloisInc/crucible#914
This bumps the
cruciblesubmodule to include GaloisInc/crucible#914. This also bumps themacawsubmodule to include GaloisInc/macaw#244, which adaptsmacaw-symbolicto thecruciblechanges. Thesecruciblechanges require some tweaks in the following libraries:In
heapster-saw, we need to add aNuMatching1instance forGlobalVarnow thatLLVM_SideConditionshas a field of typeGlobalVar Mem. This also requires defining an opaqueNuMatchinginstance forNonceto support theNuMatching1instance forGlobalVar.Elsewhere in
heapster-saw, we need to adapt a pattern match onLLVM_SideConditionsto accommodate its new field.In
saw-script, we need to make sure that?recordLLVMAnnotationis given three arguments, not two, so that its type matches whatHasLLVMAnnexpects.Adapt to GaloisInc/crucible#906
This bumps the
cruciblesubmodule to include GaloisInc/crucible#906. This also bumps themacawsubmodule to include GaloisInc/macaw#245, which adaptsmacaw-symbolicto thecruciblechanges. Thecruciblechanges require adding some additional?memOpts :: MemOptionsandHasLLVMAnn Symconstraints to various functions insaw-script.Adapt to GaloisInc/crucible#928
This bumps the
cruciblesubmodule to include GaloisInc/crucible#928. Thecruciblechanges require adding some additional?memOpts :: MemOptionsconstraints to various functions.