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.

Publications

• Tahina Ramananandro (Gallium, INRIA), Gabriel Dos Reis (Parasol, Texas A&M University) and Xavier Leroy (Gallium, INRIA)
  Formal verification of object layout for C++ multiple inheritance
  POPL 2011
  Final version (at ACM Digital Library) | Paper preprint | Conference Talk
  
  
• Tahina Ramananandro
  Machine-checked object layout for C++ multiple inheritance with empty-base optimization
  Technical report, 2010

See also :

• Tahina Ramananandro
  A machine-checked formalization of object layout for C++ multiple inheritance
  Talk at Parasol team seminar, Texas A&M University, February 2010. (This talk is about a preliminary version of C++ object layout formalization, which included no empty base optimizations at that time.)

Browse the Coq development

  

Main files related to C++ multiple inheritance
Cplusconcepts	Basic concepts of C++ multiple inheritance (POPL 2011 Section 3)
CplusWf	Well-formed hierarchies
LayoutConstraints	Soundness conditions for object layout, and their proofs of correctness (Sections 4 and 5)
ConcreteOp	A 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.
CPP	A definition of dynamic classes, used only for layout algorithms
CommonVendorABI	An object layout algorithm based on the common vendor ABI, and its proof of correctness (Section 6.1)
CCCPP	An 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
Coqlib	Additional libraries complement to the Coq standard library.
Maps	Applicative finite maps
Other library files
Param	Settings 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.
Tactics	Tactics
LibLists	Lists
LibPos	Integers
LibMaps	Finite maps

Download

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

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