GaloisInc / crucible

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

Work around LLVM's reltable lookup optimization #1214

Closed RyanGlScott closed 1 month ago

RyanGlScott commented 1 month ago

Clang 14.0.0+ introduce a relative lookup table optimization that produces code that subtracts two pointers from different allocation regions, which is something that crucible-llvm is ill equipped to reason about. For lack of a viable alternative, we work around this issue by "undoing" this optimization before translating the code to Crucible. For the full details, see the new Note [Undoing LLVM's relative table lookup conversion pass] in Lang.Crucible.LLVM.Globals.

Fixes #1174.