Verified compilation of C++ Multiple Inheritance
Copyright 2009, 2010, 2011 Tahina Ramananandro, Gallium (INRIA)
The work presented here, described in detail in Chapter 11 of my PhD thesis, is a formalization of a verified compiler for the object-oriented subset of C++ described in the object construction and destruction part of my PhD thesis, using an extension of the target language described in the object layout part of my PhD thesis. It is a 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.
Browse the Coq development
The languages and their semantics
The compiler involves three languages k++, Ds++, CVcm:
- k++ is the source language including fundamental C++ object-oriented features (virtual function dispatch, static and dynamic cast, access to data members) as well as object construction and destruction.
- Ds++ is an intermediate language including fundamental C++ object-oriented features but generalizing the notion of dynamic type to any objects without referring to any construction or destruction context.
- CVcm is the target language including 3-address-style low-level memory accesses along with read-only accesses to virtual tables and virtual table tables (VTT) to model C++-flavoured polymorphism.
Summary of theories
| Language-independent infrastructure (part of Compcert) | |
| Coqlib | Additional libraries complement to the Coq standard library. |
| Maps | Applicative finite maps |
| Events | Trace semantics |
| Smallstep | Small-step semantics |
| Language-independent infrastructure (unrelated to Compcert) | |
| BuiltinTypes | Axiomatization of built-in types (booleans, numerical types...) |
| ForLoop | "For" loops with bounds known at compile time |
| Mangle | Language-independent tools for name mangling |
| Foundations of C++ object-oriented features | |
| Cplusconcepts | Basic concepts of C++ multiple inheritance. Virtual base construction order. |
| CplusWf | Well-formed hierarchies and decidability properties |
| Dynamic | Dynamic (= polymorphic) classes |
| DynamicWf | If the hierarchy is well-formed, then it is decidable whether a class is dynamic. |
| k++: C++ Object Construction and Destruction | |
| Cppsem | Syntax and operational semantics of a subset of C++ with object construction and destruction. The construction states of an object. |
| SubobjectOrdering | Relations between subobjects: "direct subobject", "occurs before" and "subobject lifetime order" relations. |
| Invariant | Run-time invariant. Stack objects. |
| ConstrSubobjectOrdering | Properties of subobject relations on states verifying the run-time invariant. Relations between subobject relations and lifetime. |
| Dyntype | The generalized dynamic type of an object, if any, is unique. |
| Preservation | Proof of preservation for the run-time invariant. This proof takes more than 2 hours to compile. It is split into several files, namely: IncludeHeader NotationHeader NotationLightHeader PreservationHeader PreservationStack2Header PreservationAux PreservationBreadthArrays PreservationBreadthDirectNonVirtual PreservationBreadthFields PreservationBreadthVirtualDirectNonVirtual PreservationBreadthVirtual PreservationConstructionStatesDirectNonVirtual PreservationConstructionStatesFields PreservationConstructionStatesStructureFields PreservationConstructionStatesVirtual PreservationKind PreservationStack2Kconstrarray PreservationStack2Kconstrothercells PreservationStack2Kconstrother PreservationStack2KConstr PreservationStack2Kdestr PreservationStack2 PreservationStackKconstrotherBase PreservationStackKconstrothercells PreservationStackKconstrotherField PreservationStackKdestrcell PreservationStackKdestrotherBase PreservationStackKdestrotherField PreservationStackStateWf PreservationStack PreservationStackWf |
| Constrorder | Properties about object lifetime during run-time executions (needing the proof of preservation of the invariant): construction state increase, intermediate values theorem, dynamic type evolution, subobjects destructed in the reverse order of their construction, RAII. |
| ScalarFields | A scalar field has a value only if it is Constructed. |
| The following further properties are irrelevant to compilation. | |
| ConstrorderOther | Further properties about the lifetime of subobjects of different complete objects. |
| Progress | Construction (resp. destruction) progress for classes with nearly trivial constructors, (resp. trivial destructors). This proof does not need the invariant. |
| ProgressInv | More complete theorems about progress (stating that objects are constructed when entering a block, and destructed after exiting the block). This proof needs the Invariant. |
| Ds++: C++ fundamental features with generalized dynamic type | |
| IntermSetDynType | Specification of the "set dynamic type" operator |
| Interm | Syntax and Semantics of the Ds++ intermediate language. |
| IntermSetDynTypeWf | If the class hierarchy is well-formed, then the "set dynamic type" operator is well-defined. |
| k++-to-Ds++ verified compiler | |
| Cppsem2IntermAux | Compilation of k++ statements, and proof of semantics preservation. This proof takes more than half an hour to compile. |
| Cppsem2Interm | Construction of an Ds++ program from k++ functions, constructors and destructors |
| CVcm: low-level 3-address-style target language | |
| Memory | Axiomatization of a Compcert-like low-level memory model |
| Target | Syntax and Semantics of the CVcm target language. |
| Ds++-to-CVcm verified compiler | |
| LayoutConstraints | Soundness conditions for low-level layout of C++ objects, and their proofs of correctness. Unchanged since object layout (POPL 2011). |
| CPP | A definition of dynamic classes, used only for layout algorithms |
| Vtables | Construction of virtual tables and virtual table tables. |
| CompileSetDynType | Compilation of the Ds++ "set dynamic type" operation |
| Interm2Target | Verified compilation of an Ds++ program to CVcm, expecting a layout algorithm compliant with the abovementioned soundness conditions |
| Layout algorithms | |
| CommonVendorABI | A layout algorithm derived from the Common Vendor ABI for Itanium |
| CCCPP | Our optimized version of this algorithm, to take empty member optimizations into account |
| 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 (and an estimated 3 hours) to process the files.