S-Space College of Engineering/Engineering Practice School (공과대학/대학원) Dept. of Computer Science and Engineering (컴퓨터공학부) Theses (Master's Degree_컴퓨터공학부)
Verified Credible Compilation Framework For Early CSE in LLVM
LLVM 내의 Early CSE 를 위한 검증되고 신뢰할 수 있는 컴파일러 프레임워크
- 공과대학 컴퓨터공학부
- Issue Date
- 서울대학교 대학원
- 학위논문 (석사)-- 서울대학교 대학원 : 공과대학 컴퓨터공학부, 2018. 8. 허충길.
- Compiler verification is important when obtaining a high level of reliability through software verification. Compiler bugs are crucial for software verification because code that running programs are not source code but execution code. However, many C/C++ mainstream compilers, including GCC and LLVM focus on efficiency rather than reliability. Although testing is an effective method to identify bugs, it does not guarantee a high level of reliability. Various approaches have been proposed to examine compiler internal logics, but as yet none have been very successful.
CRELLVM is a compiler framework that validates optimization passes in LLVM to ensure high reliability of LLVM optimizations. It is able to validate major optimizations of LLVM such as Register Promotion and Global Value Numbering.
This thesis shows validation of Early CSE optimization in LLVM, using CRELLVM. For the validation, proof generation code which corresponds to Early CSE in LLVM is implemented and the proof checker has been extended. Early CSE is one of the basic optimizations in LLVM that removes the repeated computations by erasing duplicated instructions.
Based on 5.40 million lines of C code benchmarks, the experiment result shows there is no mis-compilation for Early CSE, which guarantees a high level of reliability of Early CSE in the benchmarks.