Université de Rennes 1 Vers la compilation vérifiée de Sea of Nodes : propriétés et raisonnement sémantiques Toward verified compilation of Sea of Nodes : semantic properties and reasoning vérificationcompilation verificationcompilation Logiciels -- Vérification Thèses et écrits académiques Compilation (informatique) Thèses et écrits académiques Les compilateurs optimisants pour les langages de programmation sont devenus des logiciels complexes et donc une source de bugs. Ceci peut être dangereux dans le contexte de systèmes critiques comme l'avionique ou la médecine. Cette thèse s'inscrit dans le cadre de la compilation vérifiée optimisante dont l'objectif est d'assurer l'absence de tels bugs. Plus précisément, nous étudions sémantiquement une représentation intermédiaire SSA (Single Static Assignment) particulière, Sea of Nodes, utilisée notamment dans le compilateur optimisant HotSpot pour Java. La propriété SSA a déjà été étudiée d'un point de vue sémantique sur des représentations simples sous forme de graphe de flot de contrôle, mais le sujet des dépendances entre instructions a seulement été effleuré depuis une perspective formelle. Cette thèse apporte une étude sémantique de transformations de programmes sous forme Sea of Nodes, intégrant la flexibilité en termes de dépendances de données entre instructions. En particulier, élimination de zero-checks redondants, propagation de constantes, retour au bloc de base séquentiel et destruction de SSA sont étudiés. Certains des sujets abordés, dont la formalisation d'une sémantique pour Sea of Nodes, sont accompagnés d'une vérification à l'aide de l'assistant de preuve Coq. Optimizing compilers for programming languages have become complex software, and they are hence subject to bugs. This can be dangerous in the context of critical systems such as avionics or health care. This thesis is part of research work on verified optimizing compilers, whose objective is to ensure the absence of such bugs. More precisely, we semantically study a particular SSA intermediate representation, Sea of Nodes, which is notably used in the optimizing compiler HotSpot for Java. The SSA property has already been studied from a semantic point of view on simple intermediate representations in control flow graph form, but the subject of dependencies between instructions has just been skimmed from a formal perspective. This thesis brings a semantic study of transformations of programs in Sea of Nodes form, integrating the flexibility regarding data dependencies between instructions. In particular, redundant zero-check elimination, constant propagation, transformation back to sequential basic block, and SSA destruction are studied. Some of the approached topics, including the formalization of a semantics for Sea of Nodes, are accompanied by a verification using the Coq proof assistant. Electronic Thesis or DissertationText fr application/pdf1 : 1491 Kohttps://ecm.univ-rennes1.fr/nuxeo/site/esupversions/aac323f2-e552-42e8-8fac-4e3c5a55ae6e Fernández de Retana Yon 1990-02-22 ES 229847463 yon.fernandez.de.retana@bardinflor.perso.aquilenet.fr 2018REN1S020 http://www.theses.fr/2018REN1S020 2018-07-05 Informatique Universite de Rennes 1thesis.degree.grantor_1 02778715X Doctorat non ouiPichardieDavidintervenant_1093668392DemangeDelphineintervenant_2174231989 MATHSTICecoleDoctorale_1 204770424 Universite Bretagne LoirepartenaireRecherche_1 191639044 IRISA partenaireRecherche_2 026386909 ddc:004 PichardieDavidDemangeDelphineUniversite de Rennes 1Sciences et technologie, medecine, pharmacie, odontologie, droit, economie, gestion, philosophieMATHSTICÉcole doctorale Mathématiques et sciences et technologies de l'information et de la communication (Rennes)Universite Bretagne Loire Communaute des etablissements d enseignement superieur et de recherche (ComuE) IRISA ASCII PDF 1527127