Jeehoon Kang
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).
Supplemental Material
- Supplementary material for this paper, available at http://sf.snu.ac.kr/ crellvm/ .Google Scholar
- Andrew W. Appel. 2001. Foundational Proof-Carrying Code (LICS ’01). Google ScholarDigital Library
- The Coq Proof Assistant. https://coq.inria.fr/ .Google Scholar
- Gilles Barthe, Delphine Demange, and David Pichardie. 2014. Formal Verification of an SSA-Based Middle-End for CompCert. ACM Trans. Program. Lang. Syst. 36, 1 (March 2014). Google ScholarDigital Library
- The SPEC CINT2006 Benchmark. https://www.spec.org/cpu2006/ CINT2006/ .Google Scholar
- Nick Benton. 2004. Simple Relational Correctness Proofs for Static Analyses and Program Transformations (POPL ’04). Google ScholarDigital Library
- Yang Chen, Alex Groce, Chaoqiang Zhang, Weng-Keen Wong, Xiaoli Fern, Eric Eide, and John Regehr. 2013. Taming Compiler Fuzzers (PLDI ’13). Google ScholarDigital Library
- Ron Cytron, Jeanne Ferrante, Barry K. Rosen, Mark N. Wegman, and F. Kenneth Zadeck. 1991. Efficiently Computing Static Single Assignment Form and the Control Dependence Graph. ACM Trans. Program. Lang. Syst. 13, 4 (Oct. 1991). Google ScholarDigital Library
- Delphine Demange, David Pichardie, and Léo Stefanesco. 2016. Verifying Fast and Sparse SSA-Based Optimizations in Coq (CC ’16).Google Scholar
- Chris Hawblitzel, Shuvendu K. Lahiri, Kshama Pawar, Hammad Hashmi, Sedar Gokbulut, Lakshan Fernando, Dave Detlefs, and Scott Wadsworth. 2013. Will You Still Compile Me Tomorrow? Static Crossversion Compiler Validation (ESEC/FSE ’13). Google ScholarDigital Library
- Chung-Kil Hur, Derek Dreyer, Georg Neis, and Viktor Vafeiadis. 2012. The Marriage of Bisimulations and Kripke Logical Relations. In POPL. Google ScholarDigital Library
- Jeehoon Kang, Chung-Kil Hur, William Mansky, Dmitri Garbuzov, Steve Zdancewic, and Viktor Vafeiadis. 2015. A Formal C Memory Model Supporting Integer-pointer Casts (PLDI ’15). Google ScholarDigital Library
- Ramana Kumar, Magnus O. Myreen, Michael Norrish, and Scott Owens. 2014. CakeML: A Verified Implementation of ML (POPL ’14). Google ScholarDigital Library
- Vu Le, Mehrdad Afshari, and Zhendong Su. 2014. Compiler Validation via Equivalence Modulo Inputs (PLDI ’14). Google ScholarDigital Library
- Juneyoung Lee, Yoonseung Kim, Youngju Song, Chung-Kil Hur, Sanjoy Das, David Majnemer, John Regehr, and Nuno P. Lopes. 2017. Taming Undefined Behavior in LLVM (PLDI ’17). Google ScholarDigital Library
- Xavier Leroy. 2006. Formal Certification of a Compiler Back-end or: Programming a Compiler with a Proof Assistant (POPL ’06). Google ScholarDigital Library
- Xavier Leroy. 2009. Formal verification of a realistic compiler. Commun. ACM (2009). Google ScholarDigital Library
- Xavier Leroy, Andrew W. Appel, Sandrine Blazy, and Gordon Stewart. 2012. The CompCert Memory Model, Version 2. Research report RR-7987. INRIA.Google Scholar
- LLVM Linux. http://llvm.linuxfoundation.org .Google Scholar
- Nuno P. Lopes, David Menendez, Santosh Nagarakatte, and John Regehr. 2015. Provably Correct Peephole Optimizations with Alive (PLDI ’15). Google ScholarDigital Library
- David Menendez and Santosh Nagarakatte. 2017. Alive-Infer: Datadriven Precondition Inference for Peephole Optimizations in LLVM (PLDI ’17). Google ScholarDigital Library
- David Menendez, Santosh Nagarakatte, and Aarti Gupta. 2016. AliveFP: Automated Verification of Floating Point Based Peephole Optimizations in LLVM (SAS ’16).Google Scholar
- Kedar S. Namjoshi, Giacomo Tagliabue, and Lenore D. Zuck. 2013. A Witnessing Compiler: A Proof of Concept (RV ’13).Google Scholar
- Kedar S. Namjoshi and Lenore D. Zuck. 2013. Witnessing Program Transformations (SAS ’13).Google Scholar
- George C. Necula. 1997. Proof-carrying Code (POPL ’97). Google ScholarDigital Library
- George C. Necula. 2000. Translation Validation for an Optimizing Compiler (PLDI ’00). Google ScholarDigital Library
- Hakjoo Oh, Kihong Heo, Wonchan Lee, Woosuk Lee, Daejun Park, Jeehoon Kang, and Kwangkeun Yi. 2014. Global Sparse Analysis Framework. ACM Trans. Program. Lang. Syst. 36, 3 (Sept. 2014). Google ScholarDigital Library
- Amir Pnueli, Michael Siegel, and Eli Singerman. 1998. Translation Validation (TACAS ’98). Google ScholarDigital Library
- Amir Pnueli, Ofer Strichman, and Michael Siegel. 1998. The Code Validation Tool CVT: Automatic Verification of a Compilation Process (STTT ’98).Google Scholar
- HOL Interactive Theorem Prover. https://hol- theorem- prover.org/ .Google Scholar
- The Z3 Theorem Prover. https://github.com/Z3Prover/z3 .Google Scholar
- John Regehr, Yang Chen, Pascal Cuoq, Eric Eide, Chucky Ellison, and Xuejun Yang. 2012. Test-case reduction for C compiler bugs (PLDI ’12). Google ScholarDigital Library
- Silvain Rideau and Xavier Leroy. 2010. Validating Register Allocation and Spilling (CC ’10). Google ScholarDigital Library
- Martin C. Rinard and Darko Marinov. 1999. Credible Compilation with Pointers (RRV ’99).Google Scholar
- Hanan Samet. 1978. Proving the Correctness of Heuristically Optimized Code (ACM ’78).Google Scholar
- Michael Stepp, Ross Tate, and Sorin Lerner. 2011. Equality-based Translation Validator for LLVM (CAV ’11). Google ScholarDigital Library
- Ross Tate, Michael Stepp, Zachary Tatlock, and Sorin Lerner. 2009. Equality Saturation: A New Approach to Optimization (POPL ’09). Google ScholarDigital Library
- Zachary Tatlock and Sorin Lerner. 2010. Bringing Extensibility to Verified Compilers (PLDI ’10). Google ScholarDigital Library
- Jean-Baptiste Tristan, Paul Govereau, and Greg Morrisett. 2011. Evaluating Value-graph Translation Validation for LLVM (PLDI ’11). Google ScholarDigital Library
- Jean-Baptiste Tristan and Xavier Leroy. 2008. Formal Verification of Translation Validators: A Case Study on Instruction Scheduling Optimizations (POPL ’08). Google ScholarDigital Library
- Jean-Baptiste Tristan and Xavier Leroy. 2009. Verified Validation of Lazy Code Motion (PLDI ’09). Google ScholarDigital Library
- Jean-Baptiste Tristan and Xavier Leroy. 2010. A Simple, Verified Validator for Software Pipelining (POPL ’10). Google ScholarDigital Library
- Xuejun Yang, Yang Chen, Eric Eide, and John Regehr. 2011. Finding and Understanding Bugs in C Compilers (PLDI ’11). Google ScholarDigital Library
- Anna Zaks and Amir Pnueli. 2008. CoVaC: Compiler Validation by Program Analysis of the Cross-Product (FM ’08). Google ScholarDigital Library
- Jianzhou Zhao, Santosh Nagarakatte, Milo M.K. Martin, and Steve Zdancewic. 2012. Formalizing the LLVM Intermediate Representation for Verified Program Transformations (POPL ’12). Google ScholarDigital Library
- Jianzhou Zhao, Santosh Nagarakatte, Milo M.K. Martin, and Steve Zdancewic. 2013. Formal Verification of SSA-based Optimizations for LLVM (PLDI ’13). Google ScholarDigital Library
- Lenore Zuck, Amir Pnueli, Benjamin Goldberg, Clark Barrett, Yi Fang, and Ying Hu. 2002. Translation and Run-Time Validation of Loop Transformations (RV ’02).Google Scholar
- Lenore D. Zuck, Amir Pnueli, and Benjamin Goldberg. 2003. VOC: A Methodology for the Translation Validation of Optimizing Compilers (J. UCS ’03).Google Scholar
Index Terms
- Crellvm: verified credible compilation for LLVM
Recommendations
Formal verification of SSA-based optimizations for LLVM
PLDI '13: Proceedings of the 34th ACM SIGPLAN Conference on Programming Language Design and ImplementationModern compilers, such as LLVM and GCC, use a static single assignment(SSA) intermediate representation (IR) to simplify and enable many advanced optimizations. However, formally verifying the correctness of SSA-based optimizations is challenging ...
Crellvm: verified credible compilation for LLVM
PLDI '18Production 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 ...
Verified Compilation of Floating-Point Computations
Floating-point arithmetic is known to be tricky: roundings, formats, exceptional values. The IEEE-754 standard was a push towards straightening the field and made formal reasoning about floating-point computations easier and flourishing. Unfortunately, ...
Comments