Mechanized Formal Semantics and Verified Compilation for C++ Objects

Copyright 2009, 2010, 2011 Tahina Ramananandro

I successfully defended my Ph.D. thesis on Tuesday, January 10th, 2012 at École normale supérieure.

• Ph. D. dissertation (PDF, < 2.9 Mb). Final version.
• Slides for the defense
• Coq development

C++ is one of the most widely used programming languages in practice, including for embedded critical software. Thus, it becomes interesting to apply formal methods to programs written in C++. To this end, it is necessary to rely on a formal semantics of C++. Moreover, such a formal semantics can be validated as a basis to the specification and proof of a verified realistic compiler for C++ to gain confidence in the implementation techniques of mainstream C++ compilers. In this thesis, we focus on the C++ object model.

We formally specify C++ multiple inheritance with C-style embedded structures, leading us to study the concrete representation of objects with empty base optimizations. We propose a set of sufficient layout conditions, and we show that they are sound with respect to field accesses and polymorphic operations. We then specify a realistic layout algorithm based on the Common Vendor ABI for Itanium, and an extension performing empty member optimizations, and we prove that they satisfy our conditions. We obtain a verified realistic compiler from a subset of C++ to a 3-address language with low-level memory accesses.

Extending our semantics with object construction and destruction, we study their intrications with multiple inheritance. This leads us to formalize resource management, namely resource acquisition is initialization through the subobject construction and destruction order. We also study the impact on polymorphic operations such as virtual function dispatch during construction and destruction, by generalizing the notion of dynamic type. We obtain a verified compiler for our extended semantics, in particular by verifying the implementation of dynamic type changes.

All our specifications and proofs are carried out with Coq.

Ph. D. advisor	Xavier Leroy	Gallium	INRIA Paris-Rocquencourt
Reviewers	Thomas Jensen	Celtique	INRIA Rennes Bretagne Atlantique
	Michael Norrish	ERTOS	NICTA (Australia)
Examiners	Patrick Cousot	Sémantique et Interprétation abstraite	École normale supérieure
	Gabriel Dos Reis	Parasol	Texas A&M University (Texas, USA)
	Claude Marché	ProVal	INRIA Saclay Île-de-France
President	Roberto Di Cosmo	Preuves Programmes, Systèmes	Université Paris. Diderot (Paris 7)

My Ph. D work has given birth to the following publications:

A Mechanized Semantics for C++ Object Construction and Destruction, with Applications to Resource Management

By Tahina Ramananandro (Gallium, INRIA), Gabriel Dos Reis (Parasol, Texas A&M University) and Xavier Leroy (Gallium, INRIA)

POPL 2012

• Final version (at ACM Digital Library)
• Paper preprint
• Slides for the talk
• Technical report
• Coq development (requires Coq 8.2pl1)

See also :

• Tahina Ramananandro
  Formal verification of C++ object construction and destruction
  Talk at FLINT team seminar, Yale University, November 2011. This talk also includes a reminder of formalized object layout, and an overview of verified compilation of C++.

Formal verification of object layout for C++ multiple inheritance

By Tahina Ramananandro (Gallium, INRIA), Gabriel Dos Reis (Parasol, Texas A&M University) and Xavier Leroy (Gallium, INRIA)

POPL 2011

• Final version (at ACM Digital Library)
• Paper preprint
• Slides for the talk
• Technical report
• Coq development (requires Coq 8.2pl1)

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.)

---

This website is kindly hosted by the INRIA Gallium project-team.