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.
While working on #430, I realized that
Data.Macaw.Symbolic.Testinghas 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-symbolictest 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
ResultExtractorsetup 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.