| Attributes | Values |
|---|
| type
| |
| Thesis advisor
| |
| Author
| |
| alternative label
| - Mechanized Formal Semantics and Verified Compilation for C++ Objects
|
| dc:subject
| - Thèses et écrits académiques
- Langages de programmation fonctionnelle
- Compilateurs (logiciels)
- Logiciels -- Vérification
- Compilation (informatique)
|
| preferred label
| - Les objets en C + +, sémantique formelle mécanisée et compilation vérifiée
|
| Language
| |
| Subject
| |
| dc:title
| - Les objets en C + +, sémantique formelle mécanisée et compilation vérifiée
|
| Degree granting institution
| |
| note
| - 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.
- 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.
|
| dc:type
| |
| http://iflastandar...bd/elements/P1001
| |
| rdaw:P10219
| |
| has content type
| |
| is primary topic
of | |
| is rdam:P30135
of | |
![[RDF Data]](/fct/images/sw-rdf-blue.png)
