SPLASH 2020
Sun 15 - Sat 21 November 2020 Online Conference
Wed 18 Nov 2020 18:00 - 18:20 at OOPSLA/ECOOP - W-6
Thu 19 Nov 2020 06:00 - 06:20 at OOPSLA/ECOOP - W-6

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 ELF object files that treats blocks of encoded definitions as unanalyzable and 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.

Wed 18 Nov
Times are displayed in time zone: Central Time (US & Canada) change

17:00 - 18:20: W-6OOPSLA at OOPSLA/ECOOP +12h
17:00 - 17:20
Talk
OOPSLA
Hila PelegUniversity of California, San Diego, Roi GabayTechnion, Shachar ItzhakyTechnion, Israel, Eran YahavTechnion
17:20 - 17:40
Talk
OOPSLA
Subarno BanerjeeUniversity of Michigan, David DevecseryGeorgia Institute of Technology, Peter M. ChenUniversity of Michigan, USA, Satish NarayanasamyUniversity of Michigan
17:40 - 18:00
Talk
OOPSLA
Guilherme LeobasUniversidade Federal de Minas Gerais, Fernando Magno Quintão PereiraUFMG
DOI Pre-print
18:00 - 18:20
Talk
OOPSLA
Yuting WangShanghai Jiao Tong University, Xiangzhe XuNanjing University, Pierre WILKECentraleSupelec Rennes, Zhong ShaoYale University

Thu 19 Nov
Times are displayed in time zone: Central Time (US & Canada) change

05:00 - 06:20: W-6OOPSLA at OOPSLA/ECOOP
05:00 - 05:20
Talk
OOPSLA
Hila PelegUniversity of California, San Diego, Roi GabayTechnion, Shachar ItzhakyTechnion, Israel, Eran YahavTechnion
05:20 - 05:40
Talk
OOPSLA
Subarno BanerjeeUniversity of Michigan, David DevecseryGeorgia Institute of Technology, Peter M. ChenUniversity of Michigan, USA, Satish NarayanasamyUniversity of Michigan
05:40 - 06:00
Talk
OOPSLA
Guilherme LeobasUniversidade Federal de Minas Gerais, Fernando Magno Quintão PereiraUFMG
DOI Pre-print
06:00 - 06:20
Talk
OOPSLA
Yuting WangShanghai Jiao Tong University, Xiangzhe XuNanjing University, Pierre WILKECentraleSupelec Rennes, Zhong ShaoYale University