We designed, implemented, and deployed Alive2: a \emph{bounded}
translation validation tool for the LLVM compiler's intermediate
representation (IR).
It limits resource consumption by, for example, unrolling loops up to
some bound, which means there are circumstances in which it misses
bugs.
Alive2 is designed to avoid false alarms, is fully automatic
through the use of an SMT solver, and requires no changes to LLVM.
By running Alive2 over LLVM's unit test suite, we discovered and reported
47 new bugs, 28 of which have been fixed already.
Moreover, our work has led to eight patches to the LLVM Language
Reference—the definitive description of the semantics of its
IR—and we have participated in numerous discussions with
the goal of clarifying ambiguities and fixing errors in these
semantics.
Alive2 is open source and we also made it available on the web,
where it has active users from the LLVM community.