Authors
- Jeehoon Kang*, Seoul National University, Korea
- Yoonseung Kim*, Seoul National University, Korea
- Youngju Song*, Seoul National University, Korea
- Juneyoung Lee, Seoul National University, Korea
- Sanghoon Park, Seoul National University, Korea
- Mark Dongyeon Shin, Seoul National University, Korea
- Yonghyun Kim, Seoul National University, Korea
- Sungkeun Cho, Seoul National University, Korea
- Joonwon Choi, MIT CSAIL, USA
- Chung-Kil Hur**, Seoul National University, Korea
- Kwangkeun Yi, Seoul National University, Korea
* The first three authors contributed equally and are listed alphabetically.
** Hur is the corresponding author.
Abstract
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
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 new miscompilation bugs (two in each).