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

See also:

Browse the Coq development

  
Main files related to C++ object construction and destruction
CplusconceptsBasic concepts of C++ multiple inheritance. Virtual base construction order.
CplusWfWell-formed hierarchies
DynamicDynamic (= polymorphic) classes
CppsemSyntax and operational semantics of a subset of C++ with object construction and destruction. The construction states of an object.
SubobjectOrderingRelations between subobjects: "direct subobject", "occurs before" and "subobject lifetime order" relations.
InvariantRun-time invariant. Stack objects.
ConstrSubobjectOrderingProperties of subobject relations on states verifying the run-time invariant. Relations between subobject relations and lifetime.
DyntypeThe generalized dynamic type of an object, if any, is unique.
PreservationProof 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
ConstrorderProperties 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.
ConstrorderOtherFurther properties about the lifetime of subobjects of different complete objects.
ProgressConstruction (resp. destruction) progress for classes with nearly trivial constructors, (resp. trivial destructors). This proof does not need the invariant.
ProgressInvMore complete theorems about progress (stating that objects are constructed when entering a block, and destructed after exiting the block). This proof needs the Invariant.
ScalarFieldsA scalar field has a value only if it is Constructed.
Library files that are part of Compcert
CoqlibAdditional libraries complement to the Coq standard library.
MapsApplicative finite maps
EventsTrace semantics
SmallstepSmall-step semantics
Other library files
ParamSettings 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.
TacticsTactics
LibListsLists
LibPosIntegers
LibMapsFinite 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.