Reconciling High-Level Optimizations and Low-Level Code in LLVM

被引:0
作者
Lee, Juneyoung [1 ]
Hur, Chung-Kil [1 ]
Jung, Ralf [2 ]
Liu, Zhengyang [3 ]
Regehr, John [3 ]
Lopes, Nuno P. [4 ]
机构
[1] Seoul Natl Univ, Seoul, South Korea
[2] MPI SWS, Saarbrucken, Germany
[3] Univ Utah, Salt Lake City, UT 84112 USA
[4] Microsoft Res, Cambridge, England
来源
PROCEEDINGS OF THE ACM ON PROGRAMMING LANGUAGES-PACMPL | 2018年 / 2卷
基金
美国国家科学基金会; 新加坡国家研究基金会;
关键词
IR Memory Model; LLVM;
D O I
暂无
中图分类号
TP31 [计算机软件];
学科分类号
081202 ; 0835 ;
摘要
LLVM miscompiles certain programs in C, C++, and Rust that use low-level language features such as raw pointers in Rust or conversion between integers and pointers in C or C++. The problem is that it is difficult for the compiler to implement aggressive, high-level memory optimizations while also respecting the guarantees made by the programming languages to low-level programs. A deeper problem is that the memory model for LLVM's intermediate representation (IR) is informal and the semantics of corner cases are not always clear to all compiler developers. We developed a novel memory model for LLVM IR and formalized it. The new model requires a handful of problematic IR-level optimizations to be removed, but it also supports the addition of new optimizations that were not previously legal. We have implemented the new model and shown that it fixes known memorymodel-related miscompilations without impacting the quality of generated code.
引用
收藏
页数:28
相关论文
共 22 条
[1]  
Besson Frederic, 2014, Programming Languages and Systems. 12th Asian Symposium (APLAS 2014), Proceedings: LNCS 8858, P449, DOI 10.1007/978-3-319-12736-1_24
[2]   A Verified CompCert Front-End for a Memory Model Supporting Pointer Arithmetic and Uninitialised Data [J].
Besson, Frederic ;
Blazy, Sandrine ;
Wilke, Pierre .
JOURNAL OF AUTOMATED REASONING, 2019, 62 (04) :433-480
[3]   CompCertS: A Memory-Aware Verified C Compiler Using Pointer as Integer Semantics [J].
Besson, Frederic ;
Blazy, Sandrine ;
Wilke, Pierre .
INTERACTIVE THEOREM PROVING (ITP 2017), 2017, 10499 :81-97
[4]   A Concrete Memory Model for CompCert [J].
Besson, Frederic ;
Blazy, Sandrine ;
Wilke, Pierre .
INTERACTIVE THEOREM PROVING, 2015, 9236 :67-83
[5]  
Chisnall David, 2016, C MEMORY OBJECT VALU
[6]   A Context-Sensitive Memory Model for Verification of C/C plus plus Programs [J].
Gurfinkel, Arie ;
Navas, Jorge A. .
STATIC ANALYSIS (SAS 2017), 2017, 10422 :148-168
[7]  
Hathhorn C, 2015, ACM SIGPLAN NOTICES, V50, P336, DOI [10.1145/2737924.2737979, 10.1145/2813885.2737979]
[8]  
Kang J, 2015, ACM SIGPLAN NOTICES, V50, P326, DOI [10.1145/2813885.2738005, 10.1145/2737924.2738005]
[9]   A Typed C11 Semantics for Interactive Theorem Proving [J].
Krebbers, Robbert ;
Wiedijk, Freek .
CPP'15: PROCEEDINGS OF THE 2015 ACM CONFERENCE ON CERTIFIED PROGRAMS AND PROOFS, 2015, :15-27
[10]  
Krebbers Robbert, 2013, ALIASING RESTRICTION, DOI [10.1007/978-3-319-03545-1_4, DOI 10.1007/978-3-319-03545-1_4]