-
Notifications
You must be signed in to change notification settings - Fork 42
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
stable-symbolic
: Properly initialize immutable malloc
'd memory
#1004
Conversation
-- Precondition: the pointer is valid and points to a mutable or immutable | ||
-- memory region. Therefore it can be used to initialize read-only memory | ||
-- regions. | ||
doConstStoreStableSymbolic :: |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
There is a code organization decision to make here: should we have separate doStoreStableSymbolic
and doConstStoreStableSymbolic
functions, or should we combine them into a single function that distinguishes between the two based on a Mutability
argument? We very well could do the latter, since the implementations of the two functions are very similar. On the other hand, the existing style in this module seems to be the former, since we already have separate doArrayStore
/doArrayConstStore
, storeRaw
/storeConstRaw
, and mallocRaw
/mallocConstRaw
functions. For this reason, I chose the former convention here, but do let me know if you'd prefer the latter instead.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I think having separate functions is deliberate. The Const
variants are only ever intended to be used in initialization, and the intention is to make it hard to accidentally chose the one that is abstraction-breaking (can write to immutable memory).
Adding a test case for this is surprisingly tricky, since the failure observed in GaloisInc/saw-script#1691 seemingly only arises during execution. The |
Previously, `stable-symbolic` would only initialize mutable memory with symbolic bytes when calling `malloc`. `malloc` can also be used to initialize immutable memory, however, so we must also account for this possibility when `stable-symbolic` is enabled. To this end, we create a new `doConstStoreStableSymbolic` function that is like `doStoreStableSymbolic`, but does not check if the memory being written to is mutable. (This is very much in the spirit of the existing `doArrayStore`/`doArrayConstStore`, `storeRaw`/`storeConstRaw`, and `mallocRaw`/`mallocConstRaw` split.) We now use `doConstStoreStableSymbolic` in the override for `malloc` to ensure that we do not generate a failing assertion when allocating immutable memory. (We also use it in `doAlloca` since this assertion doesn't buy us much when the memory being allocated is always known to be mutable.) See GaloisInc/saw-script#1691 for the motivation behind this bugfix.
Now that the `crucible-llvm` memory model has a fix for GaloisInc/crucible#1004, bumping the `crucible` submodule to bring in that change fixes #1691 as a consequence. I have also added a regression test.
Fix #1691 by bringing in GaloisInc/crucible#1004
Previously,
stable-symbolic
would only initialize mutable memory with symbolic bytes when callingmalloc
.malloc
can also be used to initialize immutable memory, however, so we must also account for this possibility whenstable-symbolic
is enabled.To this end, we create a new
doConstStoreStableSymbolic
function that is likedoStoreStableSymbolic
, but does not check if the memory being written to is mutable. (This is very much in the spirit of the existingdoArrayStore
/doArrayConstStore
,storeRaw
/storeConstRaw
, andmallocRaw
/mallocConstRaw
split.) We then pick betweendoStoreStableSymbolic
anddoConstStoreStableSymbolic
in the override formalloc
depending on whether the memory is mutable or immutable, respectively.See GaloisInc/saw-script#1691 for the motivation behind this bugfix.