Alive2: Bounded Translation Validation for LLVM

Nuno P. Lopes, Juneyoung Lee, Chung-Kil Hur, Zhengyang Liu, John Regehr

Abstract:

We designed, implemented, and deployed Alive2: a 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.

Published:

N. P. Lopes, J. Lee, C. Hur, Z. Liu, J. Regehr. Alive2: Bounded Translation Validation for LLVM. In Proc. of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation (PLDI), June 2021 (Distinguished Paper Award).

Download:

Bibtex:

@inproceedings{alive2-pldi21,
  title =	{Alive2: Bounded Translation Validation for {LLVM}},
  author =	{Nuno P. Lopes and Juneyoung Lee and Chung-Kil Hur and Zhengyang Liu and John Regehr},
  booktitle =	{Proc. of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation (PLDI)},
  doi =		{10.1145/3453483.3454030},
  month =	jun,
  year =	2021
}

Copyright notice:

<-- Return