# 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: IncludeHeaderNotationHeaderNotationLightHeaderPreservationHeaderPreservationStack2HeaderPreservationAuxPreservationBreadthArraysPreservationBreadthDirectNonVirtualPreservationBreadthFieldsPreservationBreadthVirtualDirectNonVirtualPreservationBreadthVirtualPreservationConstructionStatesDirectNonVirtualPreservationConstructionStatesFieldsPreservationConstructionStatesStructureFieldsPreservationConstructionStatesVirtualPreservationKindPreservationStack2KconstrarrayPreservationStack2KconstrothercellsPreservationStack2KconstrotherPreservationStack2KConstrPreservationStack2KdestrPreservationStack2PreservationStackKconstrotherBasePreservationStackKconstrothercellsPreservationStackKconstrotherFieldPreservationStackKdestrcellPreservationStackKdestrotherBasePreservationStackKdestrotherFieldPreservationStackStateWfPreservationStackPreservationStackWf |

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.