Crellvm: Verified Credible Compilation for LLVM

综合技术 2018-03-08 阅读原文

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 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.


Hacker News

责编内容by:Hacker News阅读原文】。感谢您的支持!


Recompiling NES Games into Native Executables with... Statically Recompiling NES Games into Native Executables with LLVM and Go 2013 June 7 I have always wanted to write an emulator. I made a half-he...
LLVM 5.0.0 Release LLVM 5.0.0 Release Hans Wennborg via llvm-announce llvm-announce at Thu Sep 7 11:45:35 PDT 2017 Messages...
LLVM Weekly – #129, Jun 20th 2016 Welcome to the one hundred and twenty-ninth issue of LLVM Weekly, a weekly newsletter (published every Monday) covering developments in LLVM, Clang, ...
Rust 1.25升级到LLVM 6 看新闻很累?看技术新闻更累?试试 下载InfoQ手机客户端 ,每天上下班路上听新闻,有趣还有料! Rust 1.25 把LLVM升级到LLVM 6,新增 use 语句嵌套导入组支持、自定义结构对齐、库稳定化。不过,最新的Rust版本没有包含许多期待已久的特性,如 ...
Announcing the next LLVM Foundation Board of Direc... The LLVM Foundation is pleased to announce its new Board of Directors: Chandler Carruth Hal Finkel Arnau...