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.
Type de document :
Communication dans un congrès
POPL'11 - 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Jan 2011, Austin, TX, United States. ACM Press, pp.67-79, 2011, <10.1145/1926385.1926395>
Liste complète des métadonnées

https://hal.inria.fr/hal-00674174
Contributeur : Xavier Leroy <>
Soumis le : samedi 25 février 2012 - 19:20:50
Dernière modification le : jeudi 22 mars 2012 - 15:27:10
Document(s) archivé(s) le : lundi 26 novembre 2012 - 10:16:19

Fichier

cpp-object-layout.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

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, Jan 2011, Austin, TX, United States. ACM Press, pp.67-79, 2011, <10.1145/1926385.1926395>. <hal-00674174>

Partager

Métriques

Consultations de
la notice

141

Téléchargements du document

122