Certification d'un simulateur de jeu d'instructions

Approaches based on axiomatic semantics (typically, Hoare logic) are the mostpopular for proving the correctness of imperative programs. However, we prefered totry a less usual but more direct approach, based on operational semantics : this wasmade possible in theory since the development of an operational semantics for theC language formalized in Coq in the CompCert project, and allowed us to use thecomfortable logic of Coq, of much help for managing the complexity of the specification.Up to our knowledge, this is the first development of formal correctness proofs basedon operational semantics, at least at this scale.We provide a formalized representation of the ARM instruction set and addressingmodes in Coq, using an automatic code generator from the instruction pseudo-code inthe ARM reference manual. We also generate a Coq representation of a correspondingsimulator in C, called Simlight, using the abstract syntax defined in CompCert.From these two Coq representations, we can then state and prove the correctnessof Simlight, using the operational semantics of C provided by CompCert. Currently,proofs are available for at least one instruction in each category of the ARM instructionset.During this work, we improved the technology available in Coq for performinginversions, a kind of proof steps which heavily occurs in our setting.Cette thèse expose nos travaux de certification d'une partie d'un programme C/C++ nommé SimSoC (Simulation of System on Chip), qui simule le comportement d'architectures basées sur des processeurs tels que ARM, PowerPC, MIPS ou SH4. Un simulateur de System on Chip peut être utilisé pour developper le logiciel d'un système embarqué spécifique, afin de raccourcir les phases des développement et de test, en particulier quand la vitesse de simulation est réaliste (environ 100 millions d'instructions par seconde par cœur dans le cas de SimSoC). Les réductions de temps et de coût de développement obtenues se traduisent par des cycles de conception interactifs et rapides, en évitant la lourdeur d'un système de développement matériel. SimSoC est un logiciel complexe, comprenant environ 60 000 de C++, intégrant des parties écrites en SystemC et des optimisations non triviales pour atteindre une grande vitesse de simulation. La partie de SimSoC dédiée au processeur ARM, l'un des plus répandus dans le domaine des SoC, transcrit les informations contenus dans un manuel épais de plus de 1000 pages. Les erreurs sont inévitables à ce niveau de complexité, et certaines sont passées au travers des tests intensifs effectués sur la version précédente de SimSoC pour l'ARMv5, qui réussissait tout de même à simuler l'amorçage complet de linux. Un problème critique se pose alors : le simulateur simule-t-il effectivement le matériel réel ? Pour apporter des éléments de réponse positifs à cette question, notre travail vise à prouver la correction d'une partie significative de SimSoC, de sorte à augmenter la confiance de l'utilisateur en ce similateur notamment pour des systèmes critiques. Nous avons concentré nos efforts sur un composant particulièrement sensible de SimSoC : le simulateur du jeu d'instructions de l'ARMv6, faisant partie de la version actuelle de SimSoC. Les approches basées sur une sémantique axiomatique (logique de Hoare par ex- emple) sont les plus répandues en preuve de programmes impératifs. Cependant, nous avons préféré essayer une approche moins classique mais plus directe, basée sur la sémantique opérationnelle de C : cela était rendu possible en théorie depuis la formalisation en Coq d'une telle sémantique au sein du projet CompCert et mettait à notre disposition toute la puissance de Coq pour gérer la complexitité de la spécification. À notre connaissance, au delà de la certification d'un simulateur, il s'agit de la première expérience de preuve de correction de programmes C à cette échelle basée sur la sémantique opérationnelle. Nous définissons une représentation du jeu d'instruction ARM et de ses modes d'adressage formalisée en Coq, grâce à un générateur automatique prenant en entrée le pseudo-code des instructions issu du manuel de référence ARM. Nous générons également l'arbre syntaxique abstrait CompCert du code C simulant les mêmes instructions au sein de Simlight, une version allégée de SimSoC. À partir de ces deux représentations Coq, nous pouvons énoncer et démontrer la correction de Simlight, en nous appuyant sur la sémantique opérationnelle définie dans CompCert. Cette méthodologie a été appliquée à au moins une instruction de chaque catégorie du jeu d'instruction de l'ARM. Au passage, nous avons amélioré la technologie disponible en Coq pour effectuer des inversions, une forme de raisonnement utilisée intensivement dans ce type de situation