symbolic
: Deduplicate mkInitialRegVal
across projects
#432
Labels
symbolic-execution
Issues relating to macaw-symbolic and symbolic execution
Apparently, it's common to make an initial struct of completely symbolic registers:
macaw/symbolic/src/Data/Macaw/Symbolic/Testing.hs
Line 290 in 429df8e
https://github.com/GaloisInc/pate/blob/c43542818be7780264d8a2552bfeba1cffba2902/src/Pate/Verification/InlineCallee.hs#L88
https://github.com/GaloisInc/ambient-verifier/blob/eab04abb9750825a25ec0cbe0379add63f05f6c6/src/Ambient/Verifier/SymbolicExecution.hs#L172
https://github.com/GaloisInc/saw-script/blob/47a7632c973df3fdb2d32268edc92948fc150f2d/src/SAWScript/X86Spec.hs#L453
We should probably export this kind of functionality from
macaw-symbolic
, to prevent reinventing the wheel. Ideally, this could have some sort of tie-in with the solution to #430, such that the initial register state is reasonably suitable for executing actual machine code.This does kind of toe the line of what should be included in
macaw-symbolic
. Certainly, one can imagine clients that would not want to set all registers to fully symbolic values. However, it appears to be relatively common in practice. I think it's not unreasonable to include helpers for settingmacaw-symbolic
up "in the normal way", and allow clients with more specific needs to use lower-level APIs to achieve what they want. We could also consider collecting this sort of functionality in a separate library, so that not every dependency would have to pay the price of additional compile time.The text was updated successfully, but these errors were encountered: