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 (源链)。感谢您的支持!


PHP的未来: JIT 编译 作者:c9s 一直以来,我心中有一个疑问,就是 JIT compilation 为何一直难以在 Perl 或 PHP ...
是时候严肃对待利用未定义行为这件事了... 原文地址: 作者:John Regehr 当前的C与...
How Clang Compiles a Function I’ve been planning on writing a post about how LLVM optimizes a function, but...
llvm学习笔记(1) 1. 概述 指令选择(instruction selection,也称为代码选择,有时甚至称为代码生成)是编译器代码生成器后端所涉及的重要问题之一...
LLDB: Sanitizing the debugger’s runtime June 06, 2017 posted by Kamil Rytarowski This month I started to work ...