Skip to content
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.

Sign up for GitHub

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

Jump to bottom

Don't treat struct padding as invalid memory with stable-symbolic #998

Merged
merged 2 commits into from
Jun 28, 2022
Merged

Don't treat struct padding as invalid memory with stable-symbolic #998

merged 2 commits into from
Jun 28, 2022

Commits on Jun 28, 2022

  1. Thread ?memOpts through to writeMemWithAllocationCheck 

    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.
    @RyanGlScott
    RyanGlScott committed Jun 28, 2022
    Configuration menu
    Copy the full SHA
    955bfaf View commit details
    Browse the repository at this point in the history

  2. Don't treat struct padding as invalid memory with stable-symbolic 

    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
    RyanGlScott committed Jun 28, 2022
    Configuration menu
    Copy the full SHA
    7256ae4 View commit details
    Browse the repository at this point in the history