You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
While working on #430, I realized that Data.Macaw.Symbolic.Testing has pretty hacky ABI-neutral code to set up the program stack. It would be nice to use the ABI-specific stack setup code that fixing #430 would require in the test suites, both to improve the variety of binaries that could successfully be run through the test harness, and to test the stack setup code itself.
In order to accomplish this, we will need to refactor the main driver functions simulate{AndVerify,Function} to take the initial register and memory state as arguments. They can export functions to initialize this state the way it is done now, but different test-suites may choose not to use these defaults (e.g., the x86-symbolic test suite would instead set up the stack with the functions in #433). This will likely result in a more parsimonious organization of the code anyway.
Also, while I'm in the neighborhood, I find the ResultExtractor setup pretty strange. It seems weird that we feed the whole register and memory state to a callback and expect the callback to return a bitvector that we assert to be nonzero. Why not just give the callback the register and memory state and allow it to make whatever assertions it wants to? We can provide a helper for this nonzeroness assertion if we want.
I plan to fix these faults as part of working on #430.
The text was updated successfully, but these errors were encountered:
While working on #430, I realized that
Data.Macaw.Symbolic.Testing
has pretty hacky ABI-neutral code to set up the program stack. It would be nice to use the ABI-specific stack setup code that fixing #430 would require in the test suites, both to improve the variety of binaries that could successfully be run through the test harness, and to test the stack setup code itself.In order to accomplish this, we will need to refactor the main driver functions
simulate{AndVerify,Function}
to take the initial register and memory state as arguments. They can export functions to initialize this state the way it is done now, but different test-suites may choose not to use these defaults (e.g., thex86-symbolic
test suite would instead set up the stack with the functions in #433). This will likely result in a more parsimonious organization of the code anyway.Also, while I'm in the neighborhood, I find the
ResultExtractor
setup pretty strange. It seems weird that we feed the whole register and memory state to a callback and expect the callback to return a bitvector that we assert to be nonzero. Why not just give the callback the register and memory state and allow it to make whatever assertions it wants to? We can provide a helper for this nonzeroness assertion if we want.I plan to fix these faults as part of working on #430.
The text was updated successfully, but these errors were encountered: