Crellvm: Verified Credible Compilation for LLVM

Jeehoon Kang*, Yoonseung Kim*, Youngju Song*, Juneyoung Lee, Sanghoon Park,
Mark Dongyeon Shin, Yonghyun Kim, Sungkeun Cho, Joonwon Choi,
Chung-Kil Hur**, Kwangkeun Yi.
* The first three authors contributed equally to this work and are listed alphabetically.
** Hur is the corresponding author.

Production compilers such as GCC and LLVM are large complex software systems, for which achieving a high level of reliability is hard. Although testing is an effective method for finding bugs, it alone cannot guarantee a high level of reliability. To provide a higher level of reliability, many approaches that examine compilers’ internal logics have been proposed. However, none of them have been successfully applied to major optimizations of production compilers.

This paper presents Crellvm: a verified credible compilation (or equivalently, verified translation validation) framework for LLVM, which can be used as a systematic way of providing a high level of reliability for major optimizations in LLVM. Specifically, we augment an LLVM optimizer to generate translation results together with their correctness proofs, which can then be checked by a proof checker formally verified in Coq. As case studies, we applied our approach to two major optimizations of LLVM: register promotion (mem2reg) and global value numbering (gvn), having found four miscompilation bugs (two in each). This result is notable because, to the best of our knowledge, no previous systematic approaches including random testing have found any bugs in the mem2reg and gvn passes. Moreover, except for the two bugs we have reported, we found only one confirmed miscompilation bug for mem2reg in the LLVM bug tracker history.