综合技术

Crellvm: Verified Credible Compilation for LLVM

微信扫一扫,分享到朋友圈

Crellvm: Verified Credible Compilation for LLVM
0

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.

Downloads

阅读原文...

Hacker News

Go基础之--操作Mysql(三)

上一篇

Getting an Error: access denied for Node.js with mysql

下一篇

您也可能喜欢

评论已经被关闭。

插入图片
Crellvm: Verified Credible Compilation for LLVM

长按储存图像,分享给朋友