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阅读原文】。感谢您的支持!


未定义行为 != 不安全的编程 原文地址: 作者:John Regehr 在C与C++里,未定义行为(UB)对开发者来说是一个清晰且现实的危险,特别是当他们编写将在一个信任...
LLVM学习笔记(44) 处理器特征数据 TD文件里通过SubTargetFeature定义来描述处理器所支持的指令集。反映到LLVM上,就体现为类型X86Subtarget(是下面输出X86GenSubtargetInfo类型的派生类)里...
LLVM Weekly – #123, May 9th 2016 Welcome to the one hundred and twenty-third issue of LLVM Weekly, a weekly newsletter (published every Monday) covering...
Phoronix SciMark benchmarking results Phoronix recently published an article “ Ryzen Compiler Performance: Clang 4/5 vs. GCC 6/7/8 Benchmarks ”, and there...
Review of the weeks 2018/47 & 48 Dear Tumbleweed users and hackers, The last two weeks were quite busy with snapshots: if you keep up at full pace, you...