Skip to Main content Skip to Navigation
Conference papers

Formal verification of object layout for C++ multiple inheritance

Abstract : Object layout - the concrete in-memory representation of objects - raises many delicate issues in the case of the C++ language, owing in particular to multiple inheritance, C compatibility and separate compilation. This paper formalizes a family of C++ object layout scheme and mechanically proves their correctness against the operational semantics for multiple inheritance of Wasserrab et al. This formalization is flexible enough to account for space-saving techniques such as empty base class optimization and tail-padding optimization. As an application, we obtain the first formal correctness proofs for realistic, optimized object layout algorithms, including one based on the popular GNU C++ application binary interface. This work provides semantic foundations to discover and justify new layout optimizations; it is also a first step towards the verification of a C++ compiler front-end.
Document type :
Conference papers
Complete list of metadata

Cited literature [17 references]  Display  Hide  Download
Contributor : Xavier Leroy Connect in order to contact the contributor
Submitted on : Saturday, February 25, 2012 - 7:20:50 PM
Last modification on : Friday, January 21, 2022 - 3:15:21 AM
Long-term archiving on: : Monday, November 26, 2012 - 10:16:19 AM


Files produced by the author(s)




Tahina Ramananandro, Gabriel dos Reis, Xavier Leroy. Formal verification of object layout for C++ multiple inheritance. POPL'11 - 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, ACM, Jan 2011, Austin, TX, United States. pp.67-79, ⟨10.1145/1926385.1926395⟩. ⟨hal-00674174⟩



Les métriques sont temporairement indisponibles