Crellvm: verified credible compilation for LLVM
| Autor: | Yonghyun Kim, Sang-Hoon Park, Joonwon Choi, June-Young Lee, Chung-Kil Hur, Mark Dongyeon Shin, Sungkeun Cho, Kwangkeun Yi, Jeehoon Kang, Youngju Song, Yoonseung Kim |
|---|---|
| Rok vydání: | 2018 |
| Předmět: |
Global value numbering
Computer science Programming language 020207 software engineering 02 engineering and technology computer.software_genre Computer Graphics and Computer-Aided Design Automated proof checking 020204 information systems 0202 electrical engineering electronic engineering information engineering Software system Compiler Software_PROGRAMMINGLANGUAGES computer Reliability (statistics) Software |
| Zdroj: | PLDI |
| ISSN: | 1558-1160 0362-1340 |
| DOI: | 10.1145/3296979.3192377 |
| Popis: | 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). |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|