Don't treat struct padding as invalid memory with stable-symbolic
#998
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
robdockins
approved these changes
Jun 21, 2022
This will be required in a subsequent commit that changes the behavior of `writeMemWithAllocationCheck` to behave differently depending on whether `laxLoadsAndStores` is enabled or not. This requires adding implicit constraints in several functions that did not previously require them, so I have added mention of this in the affected libraries' changelogs.
When `laxLoadsAndStores` + `stable-symbolic` are enabled, all allocations are backed by fresh SMT arrays. When writing a struct to one of these arrays, we traverse through the array byte-by-byte, loading each byte in the struct and updating the array's value accordingly. Things went awry in the case where the struct has padding, however, as the code in `crucible-llvm` assumed that loading struct padding should always be an error. Not only is this possible with `stable-symbolic`, it has a sensible interpretation: whenever loading a byte of struct padding, just skip updating the array value corresponding to that byte. See GaloisInc/saw-script#1684 for the motivation behind this bugfix. I haven't found a way to trigger the same bug with `crux-llvm`, but I can trigger it programatically using the `crucible-llvm` API. I've added a test case to the `crucible-llvm` test suite to ensure that the bug remains fixed.
RyanGlScott
added a commit
to GaloisInc/semmc
that referenced
this pull request
Jun 28, 2022
This bumps the `crucible` submodule to bring in the changes from GaloisInc/crucible#998, which adds `?memOpts :: MemOptions` constraints to a handful of additional functions. This requires adding constraints to some functions in `semmc-synthesis` to accommodate. The `crucible-llvm` submodule now depends on a more recent `llvm-pretty` submodule commit to build, so this patch also bumps the `llvm-pretty` submodule.
RyanGlScott
added a commit
to GaloisInc/semmc
that referenced
this pull request
Jun 28, 2022
This bumps the `crucible` submodule to bring in the changes from GaloisInc/crucible#998, which adds `?memOpts :: MemOptions` constraints to a handful of additional functions. This requires adding constraints to some functions in `semmc-synthesis` to accommodate. The `crucible-llvm` submodule now depends on a more recent `llvm-pretty` submodule commit to build, so this patch also bumps the `llvm-pretty` submodule.
RyanGlScott
added a commit
to GaloisInc/semmc
that referenced
this pull request
Jun 28, 2022
This bumps the `crucible` submodule to bring in the changes from GaloisInc/crucible#998, which adds `?memOpts :: MemOptions` constraints to a handful of additional functions. This requires adding constraints to some functions in `semmc-synthesis` to accommodate. The `crucible-llvm` submodule now depends on a more recent `llvm-pretty` submodule commit to build, so this patch also bumps the `llvm-pretty` submodule.
RyanGlScott
added a commit
to GaloisInc/macaw
that referenced
this pull request
Jun 28, 2022
This bumps the `crucible` submodule to bring in the changes from GaloisInc/crucible#998, which adds `?memOpts :: MemOptions` constraints to a handful of additional functions. This requires adding constraints to some functions in `macaw-symbolic` to accommodate, as well as bumping the `semmc` submodule to bring in analogous changes from GaloisInc/semmc#76.
RyanGlScott
added a commit
to GaloisInc/macaw
that referenced
this pull request
Jun 28, 2022
This bumps the `crucible` submodule to bring in the changes from GaloisInc/crucible#998, which adds `?memOpts :: MemOptions` constraints to a handful of additional functions. This requires adding constraints to some functions in `macaw-symbolic` to accommodate, as well as bumping the `semmc` submodule to bring in analogous changes from GaloisInc/semmc#76.
RyanGlScott
added a commit
to GaloisInc/saw-script
that referenced
this pull request
Jun 28, 2022
Now that the `crucible-llvm` memory model can reason about struct padding with `lax-loads-and-stores` enabled, bumping the `crucible` submodule to bring in that change fixes #1684 as a consequence. I have also added a regression test.
RyanGlScott
added a commit
to GaloisInc/saw-script
that referenced
this pull request
Jun 28, 2022
Now that the `crucible-llvm` memory model can reason about struct padding with `lax-loads-and-stores` enabled, bumping the `crucible` submodule to bring in that change fixes #1684 as a consequence. I have also added a regression test.
mergify bot
added a commit
to GaloisInc/saw-script
that referenced
this pull request
Jun 28, 2022
Fix #1684 by bringing in GaloisInc/crucible#998
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.
When
laxLoadsAndStores+stable-symbolicare enabled, all allocations are backed by fresh SMT arrays. When writing a struct to one of these arrays, we traverse through the array byte-by-byte, loading each byte in the struct and updating the array's value accordingly.Things went awry in the case where the struct has padding, however, as the code in
crucible-llvmassumed that loading struct padding should always be an error. Not only is this possible withstable-symbolic, it has a sensible interpretation: whenever loading a byte of struct padding, just skip updating the array value corresponding to that byte.See GaloisInc/saw-script#1684 for the motivation behind this bugfix. I haven't found a way to trigger the same bug with
crux-llvm, but I can trigger it programatically using thecrucible-llvmAPI. I've added a test case to thecrucible-llvmtest suite to ensure that the bug remains fixed.