Les objets en C++ : sémantique formelle mécanisée et compilation vérifiée

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.C++ est un des langages de programmation les plus utilisés en pratique, y compris pour le logiciel embarqué critique. C'est pourquoi la vérication de programmes écrits en C++ devient intéressante, en particulier via l'utilisation de méthodes formelles. Pour cela, il est nécessaire de se fonder sur une sémantique formelle de C++. De plus, une telle sémantique formelle peut être validée en la prenant comme base pour la spécication et la preuve d'un compilateur C++ réaliste, afin d'établir la confiance dans les techniques usuelles des compilateurs C++. Dans cette thèse, nous nous focalisons sur le modèle objet de C++. Nous proposons une sémantique formelle de l'héritage multiple en C++ comprenant les structures imbriquées à la C, sur laquelle s'appuie notre étude de la représentation concrète des objets avec optimisations des bases vides, à travers des conditions suffisantes que nous prouvons correctes vis-à-vis des accès aux champs et des opérations polymorphes. Puis nous spécifions un algorithme de représentation en mémoire fondé sur l'ABI pour Itanium, et une extension de cet algorithme avec optimisations des champs vides, et nous prouvons qu'ils satisfont nos conditions. Nous obtenons alors un compilateur vérifié et réaliste d'un sous-ensemble de C++ vers un langage à trois adresses et accès mémoire de bas niveau. Rajoutant à notre sémantique la construction et la destruction d'objets, nous étudions leurs interactions avec l'héritage multiple. Cela nous permet de formaliser la gestion de ressources, notamment le principe RAII (resource acquisition is initialization) via l'ordre de construction et destruction des sous-objets. Nous étudions aussi les effets sur les opérations polymorphes telles que la sélection de fonction virtuelle pendant la construction et la destruction, en généralisant la notion de type dynamique. Nous obtenons alors un compilateur vérifié pour notre sémantique étendue, notamment en prouvant la correction de l'implémentation des changements de types dynamiques. Toutes nos spécifications et preuves sont formalisées en Coq