Alive2: Bounded Translation Validation for LLVM

Resource history | v1 (current) | created by jjones on Apr 26, 2021

Details

see v1 | created by jjones on Apr 26, 2021 | Add topic "LLVM"

Title: Alive2: Bounded Translation Validation for LLVM
Type: Paper
Created: 2021
Description: 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.
Link: https://www.cs.utah.edu/~regehr/alive2-pldi21.pdf
Identifier: https://doi.org/10.1145/3453483.3454030

This resource has no history of related authors.

v1 | attached by jjones on Apr 26, 2021 | Add topic "LLVM"

This resource has no history of related resources.