GaloisInc / crucible

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

llvm: Refactor and document binding functions #1198

Closed langston-barrett closed 3 months ago

langston-barrett commented 3 months ago

Binding functions (whether they be translated CFGs or overrides) in the LLVM memory model is a bit more complex than in other frontends. We had organically grown a number of helpers that take care of various parts of this process, without actually documenting what needs to happen for everything to work as expected. This PR collects those helpers into a single module, with a top-level comment that outlines the whole process.

Along the way, it removes some superfluous helpers (bindLLVMFunPtr) and introduces some new ones (bindLLVMCFG).