Paper Info
Title
CompCertELF: verified separate compilation of C programs into ELF object files
Abstract
We present CompCertELF, the first extension to CompCert that supports verified compilation from C programs all the way to a standard binary file format, i.e., the ELF object format. Previous work on Stack-Aware CompCert provides a verified compilation chain from C programs to assembly programs with a realistic machine memory model. We build CompCertELF by modifying and extending this compilation chain with a verified assembler which further transforms assembly programs into ELF object files. CompCert supports large-scale verification via verified separate compilation: C modules can be written and compiled separately, and then linked together to get a target program that refines the semantics of the program linked from the source modules. However, verified separate compilation in CompCert only works for compilation to assembly programs, not to object files. For the latter, the main difficulty is to bridge the two different views of linking: one for CompCert's programs that allows arbitrary shuffling of global definitions by linking and the other for object files that treats blocks of encoded definitions as indivisible units. We propose a lightweight approach that solves the above problem without any modification to CompCert's framework for verified separate compilation: by introducing a notion of syntactical equivalence between programs and proving the commutativity between syntactical equivalence and the two different kinds of linking, we are able to transit from the more abstract linking operation in CompCert to the more concrete one for ELF object files. By applying this approach to CompCertELF, we obtain the first compiler that supports verified separate compilation of C programs into ELF object files.
Year
DOI
Venue
2020
10.1145/3428265
Proceedings of the ACM on Programming Languages
Keywords
DocType
Volume
Assembler Verification,Generation of Object Files,Verified Separate Compilation
Journal
4
Issue
ISSN
Citations 
OOPSLA
2475-1421
0
PageRank 
References 
Authors
0.34
0
4
Name
Order
Citations
PageRank
Yuting Wang1217.13
Xiangzhe Xu200.34
Pierre Wilke3102.61
Zhong Shao4322.85