Formal verification of object layout for C++ multiple inheritance

The work presented here, described in Chapters 3 to 6 of my Ph.D. thesis as well as the POPL 2011 paper mentioned below, is a formalization of object layout. It is a first step towards a formally verified, realistic compiler for a subset of the object-oriented part of C++, within the framework of the Compcert verified compiler.


See also :

Browse the Coq development

Main files related to C++ multiple inheritance
CplusconceptsBasic concepts of C++ multiple inheritance (POPL 2011 Section 3)
CplusWfWell-formed hierarchies
LayoutConstraintsSoundness conditions for object layout, and their proofs of correctness (Sections 4 and 5)
ConcreteOpA core language, small subset of C++ featuring field reads and writes, static casts, dynamic casts (to illustrate polymorphic behaviour), and array accesses. It comes with a compiler to a Cminor-style language performing low-level memory accesses, along with a proof of semantics preservation by forward simulation. This proof is an explicit example of how to use the soundness conditions and theorems.
CPPA definition of dynamic classes, used only for layout algorithms
CommonVendorABIAn object layout algorithm based on the common vendor ABI, and its proof of correctness (Section 6.1)
CCCPPAn object layout algorithm optimized for empty base tail padding, and its proof of correctness (Section 6.2). CCCPP stands for CompCert C Plus Plus
Library files that are part of Compcert
CoqlibAdditional libraries complement to the Coq standard library.
MapsApplicative finite maps
Other library files
ParamSettings for implicit arguments, etc. This file is used as a verbatim include for other files (using the Coq command Load), rather than as a library.
LibMapsFinite maps


You can also download a TAr.BZ2 archive of the whole Coq development.

Note: you will need Coq 8.2pl1 to process the files.