GaloisInc / macaw

Open source binary analysis tools.
BSD 3-Clause "New" or "Revised" License
208 stars 21 forks source link

`symbolic`: Deduplicate `mkInitialRegVal` across projects #432

Open langston-barrett opened 2 months ago

langston-barrett commented 2 months ago

Apparently, it's common to make an initial struct of completely symbolic registers:

https://github.com/GaloisInc/macaw/blob/429df8edf13931da22561ed27b23f1fdbc77484c/symbolic/src/Data/Macaw/Symbolic/Testing.hs#L290

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 setting macaw-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.

langston-barrett commented 2 months ago

See also freshValue in macaw-x86-symbolic:

https://github.com/GaloisInc/macaw/blob/429df8edf13931da22561ed27b23f1fdbc77484c/x86_symbolic/src/Data/Macaw/X86/Symbolic.hs#L261

RyanGlScott commented 2 months ago

And for even more prior art, see freshCrucibleConstant in macaw-symbolic:

https://github.com/GaloisInc/macaw/blob/429df8edf13931da22561ed27b23f1fdbc77484c/symbolic/src/Data/Macaw/Symbolic.hs#L1281-L1288