GaloisInc / crucible

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

crucible-llvm: Make a list of libc overrides #1186

Closed langston-barrett closed 6 months ago

langston-barrett commented 6 months ago

Before this change, lists of LLVM overrides (e.g., declare_overrides) consisted of libc and LLVM-specific overrides grouped together. Because of the difficulties surrounding "polymorphic" LLVM overrides, they were also only available as OverrideTemplates, which are necessarily dynamic (i.e., are essentially monadic actions in OverrideSim that register the override in question, rather than a data structure describing the override).

Macaw-based Crucible frontends might want to reuse the libc overrides in the context of binaries. This commit separates them out and lists them purely as SomeLLVMOverrides, facilitating this reuse.

langston-barrett commented 6 months ago

At the very least, could we make a separate list for the simple ones that can be registered with basic_llvm_override?

Will do!