La préservation de propriétés établies sur le programme source jusqu'au code exécutable est un point important dans les méthodes formelles. Cette propriété de préservation est établie par la vérification formelle du proccessus de compilation. Un compilateur est formellement vérifié s'il est accompagné d'une preuve de préservation sémantique : "si la compilation réussit, le code compilé se comporte comme le code source le prédit." Le projet CompCert étudie la vérification formelle de compilateurs réalistes utilisable dans l'embarqué-critique. Il s'agit de développer et formellement vérifier de tels compilateur via l'assistant de preuve Coq. Un compilateur pour le langage C vers l'assembleur PowerPC a déjà ainsi été produit. Le code exécutable du compilateur a été obtenu en deux étapes non vérifiés : la génération automatique de code Ocaml par le mécanisme d'extration de Coq et la compilation du de ce code extrait par le système Objective Caml. En fait, cette lacune est commune à tous les développements spécifiés dans l'assistant de preuve Coq et destinés à produire un éxécutable. Cette thèse décrit l'étude, le développement et la vérification formelle, dans l'assistant de preuve Coq, d'un compilateur pour le fragment purement fonctionnel du langage ML : le langage cible du mécanisme d'extraction de Coq. Concrètement, il s'git d'une chaîne de compilation en amont pour mini-ML (lambda calcul, let, letrec et filtrage) vers le premier langage intermédiaire de la chaîne de compilation en aval du compilateur CompCert. Ce langage, Cminor, est un langage de bas niveau à la C. L'expressivité du langage source traité rend ce compilateur réaliste. Il comporte aussi des optimisations classiques propre à la compilation de langages fonctionnels : la décurryfication, comme celle implémentée dans le compilateur OCaml ; la représentation uniforme des données, explicitation des fermetures, numérotation des constructeurs et une mise en style par passage de continuation (CPS) optimisée. Le point fort de ce compilateur et que, comme les compilateurs modernes pour langage de haut niveau, il peut interagir avec un gestionnaire de mémoire automatique. Cette interaction a aussi été formellement vérifiée.
| Identifer | oai:union.ndltd.org:CCSD/oai:tel.archives-ouvertes.fr:tel-00452440 |
| Date | 06 July 2009 |
| Creators | Dargaye, Zaynah |
| Publisher | Université Paris-Diderot - Paris VII |
| Source Sets | CCSD theses-EN-ligne, France |
| Language | French |
| Detected Language | French |
| Type | PhD thesis |
Page generated in 0.0018 seconds