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.

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

macaw-symbolic: Add more testing for SymbolicMutable option #325

Open
RyanGlScott opened this issue Feb 28, 2023 · 0 comments
Open

macaw-symbolic: Add more testing for SymbolicMutable option #325

RyanGlScott opened this issue Feb 28, 2023 · 0 comments
Labels
symbolic-execution Issues relating to macaw-symbolic and symbolic execution testing Issues related to the test suite

Comments

@RyanGlScott
Copy link
Contributor

The macaw-symbolic memory model has a somewhat obscure SymbolicMutable option:

data MemoryModelContents = SymbolicMutable
-- ^ All mutable global data is fully symbolic, but
-- read-only data is concrete (and taken from the
-- memory image of the binary)

Which is explained with:

-- If we are trying to prove properties about functions in isolation, though, we
-- have to assume that non-constant global data can have /any/ value, which
-- means that we have to represent each byte as symbolic. This will change when
-- we start pursuing compositional verification and want to have more elaborate
-- memory setups.

I'm unclear how many downstream projects are actually using SymbolicMutable, but the macaw repo itself certainly isn't. The only use of it that I can find is in this bitrotted example (see also #324), which is not run on CI. Moreover, all of the code run in the macaw-symbolic test suites uses ConcreteMutable instead of SymbolicMutable, so SymbolicMutable is effectively not being tested right now.

At the very least, we should add a basic unit test of some kind to make sure that SymbolicMutable is actually doing what it claims to do.

@RyanGlScott RyanGlScott added symbolic-execution Issues relating to macaw-symbolic and symbolic execution testing Issues related to the test suite labels Feb 28, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
symbolic-execution Issues relating to macaw-symbolic and symbolic execution testing Issues related to the test suite
Projects
None yet
Development

No branches or pull requests

1 participant