GaloisInc / crucible

Crucible is a library for symbolic simulation of imperative programs
617 stars 42 forks source link

crucible-llvm: Refactor and export override pipe-fitting code #1193

Closed langston-barrett closed 4 months ago

langston-barrett commented 4 months ago

The code in question converts between bitvectors and pointers so that it is easy and natural to specify overrides using bitvectors, while at runtime only LLVM pointers are used. The built-in overrides (e.g., for libc) all expect to be wrapped in this casting code. They're all exported, so to make them usable by downstream clients, we also need to export the code that does the pipe-fitting.

langston-barrett commented 4 months ago

I have tested this using a non-Crucible-LLVM frontend, and it appears to work as intended.