A Mechanized Semantics for C++ Object Construction and Destruction, with Applications to Resource Management
The work presented here, described in Chapters 9 and 10 of my Ph.D. thesis as well as the POPL 2012 paper mentioned below, is a formalization of C++ object construction and destruction. 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.
Publications
- Tahina Ramananandro (Gallium, INRIA), Gabriel Dos Reis (Parasol, Texas A&M University) and Xavier Leroy (Gallium, INRIA)
A Mechanized Semantics for C++ Object Construction and Destruction, with Applications to Resource Management
POPL 2012
Final version (at ACM Digital Library) | Paper preprint | Conference Talk
- Tahina Ramananandro
A formal operational semantics for C++ object construction and destruction
Technical report, 2011
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++.
Browse the Coq development
| Main files related to C++ object construction and destruction | |
| Cplusconcepts | Basic concepts of C++ multiple inheritance. Virtual base construction order. |
| CplusWf | Well-formed hierarchies |
| Dynamic | Dynamic (= polymorphic) classes |
| 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 (out of an estimated 2 1/4 hours). 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. |
| 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. |
| ScalarFields | A scalar field has a value only if it is Constructed. |
| Library files that are part of Compcert | |
| Coqlib | Additional libraries complement to the Coq standard library. |
| Maps | Applicative finite maps |
| Events | Trace semantics |
| Smallstep | Small-step semantics |
| 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 2 1/4 hours) to process the files.