Réécriture et compilation de confiance, Rewriting and trustworthy compilation

Antoine Reilles

Description

Sous la direction de Claude Kirchner, Pierre-Etienne Moreau
Thèse soutenue le 27 novembre 2006: INPL
La plupart des processus informatiques mettent en jeu la notion de transformation, en particulier la compilation. Nous nous intéressons dans cette thèse à fournir des outils et des méthodes, utilisant la réécriture, permettant d'accroître la confiance que l'on peut placer dans ces processus. Nous développons dans un premier temps un cadre permettant de valider la compilation de constructions de filtrage, produisant une preuve formelle de la validité de la compilation, ainsi qu'un témoin de cette preuve, à chaque exécution du compilateur. Afin de permettre l'écriture sûre de transformations complexes, nous proposons un générateur de structures de données efficaces intégrant des invariants algébriques, et un langage de stratégies permettant de contrôler l'application des transformations. Ces résultats constituent donc une avancée vers la constitution de methodes génériques sûres pour le développement de transformations de confiance.
-Compilation
-Certification
-Confiance
-Filtrage algébrique
-Termes
-Structures de données
-Stratégies de réécriture
-Langages de programmation
Most computer processes involve the notion of transformation, in particular the compilation processes. We interest in this thesis in providing tools and methods, based on rewriting, giving the opportunity to increase the confidence we can place into those processes. We develop first a framework used to validate the compilation of matching constructs, building a formal proof of the validity of the compilation process along with a witness of this proof, for each run of the compiler. Then, in order to allow one to write safely complex transformations, we propose a tool that generates an efficient data structure integrating algebraic invariants, as well as a strategy language that enables to control the application of transformations. Those results can be seen as a first step towards the constitution of generic and safe methods for the development of trustworthy transformations.
-Compilation
-Certification
-Confidence
-Algebraic matching
-Terms
-Data structures
-Rewriting strategies
-Programming language
Source: http://www.theses.fr/2006INPL084N/document

Sujets

• Certification
• Confiance
• Termes
• Structure de données
• Langage de programmation

Informations

• Publié par: Thesee
• Nombre de lectures: 83
• Langue: Français
• Poids de l'ouvrage: 1 Mo

Extrait

D´epartement de formation doctorale en informatique
Institut National ´Ecole doctorale IAEM Lorraine
Polytechnique de Lorraine
R´e´ecriture et compilation de confiance
`THESE
pr´esent´ee et soutenue publiquement le 27 novembre 2006
pour l’obtention du
Doctorat de l’Institut National Polytechnique de Lorraine
(sp´ecialit´e informatique)
par
Antoine Reilles
Composition du jury
´Rapporteurs : Pierre Cointe Professeur, Ecole des Mines de Nantes, France
Paul Klint Professeur, Universiteit van Amsterdam, Pays-Bas
Examinateurs : Claude Kirchner Directeur de recherche, INRIA, Nancy, France
´Pierre-Etienne Moreau Charg´e de recherche, INRIA, Nancy, France
´Karl Tombre Professeur, Ecole des Mines de Nancy, INPL, France
Reinhard Wilhelm Professeur, Universit¨at des Saarlandes, Allemagne
Laboratoire Lorrain de Recherche en Informatique et ses Applications — UMR 7503AMis en page avec LT XETable des matières
Remerciements v
Extended Abstract vii
Introduction 1
1. Notions préliminaires 7
1.1. Réécriture . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7
1.1.1. Termes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7
1.1.2. Filtrage . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 8
1.1.3. Systèmes de réécriture . . . . . . . . . . . . . . . . . . . . . . . . . 9
1.1.4. Confluence et terminaison . . . . . . . . . . . . . . . . . . . . . . . 10
1.2. Pouvoir expressif de la réécriture . . . . . . . . . . . . . . . . . . . . . . . 11
1.2.1. Réécriture conditionnelle . . . . . . . . . . . . . . . . . . . . . . . 11
1.2.2. Réécriture sous stratégies . . . . . . . . . . . . . . . . . . . . . . . 12
1.2.3. Réécriture modulo une théorie . . . . . . . . . . . . . . . . . . . . 13
1.3. Langages basés sur la réécriture . . . . . . . . . . . . . . . . . . . . . . . . 13
1.3.1. La réécriture comme paradigme de calcul . . . . . . . . . . . . . . 14
1.3.2. Des langages basés sur la réécriture . . . . . . . . . . . . . . . . . . 14
2. Le langage Tom 17
2.1. Motivations et historique . . . . . . . . . . . . . . . . . . . . . . . . . . . 17
2.2. Le cœur du langage. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 17
2.2.1. Filtrage dans Java . . . . . . . . . . . . . . . . . . . . . . . . . . . 18
2.2.2. Mappings : notion d’ancrage . . . . . . . . . . . . . . . . . . . . . . 19
2.2.3. Filtrage associatif . . . . . . . . . . . . . . . . . . . . . . . . . . . 21
2.2.4. Notations utiles . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 24
2.3. Structures de données . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 26
2.3.1. Définition des mappings . . . . . . . . . . . . . . . . . . . . . . . . 26
2.3.2. Contraintes sur les structures de données pour Tom . . . . . . . . 28
2.3.3. Générateurs de structures de données . . . . . . . . . . . . . . . . 29
2.4. Des problèmes à résoudre . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
2.4.1. Correction du code généré . . . . . . . . . . . . . . . . . . . . . . . 30
2.4.2. Les invariants des structures de données . . . . . . . . . . . . . . . 31
2.4.3. Traversées génériques des arbres . . . . . . . . . . . . . . . . . . . 31
iTable des matières
3. Certification du filtrage 33
3.1. Certifier la compilation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
3.1.1. Compilateur certifié . . . . . . . . . . . . . . . . . . . . . . . . . . 33
3.1.2. Validation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
3.2. Particularités de l’environnement : îlot formel . . . . . . . . . . . . . . . . 35
3.2.1. Un cadre plus large. . . . . . . . . . . . . . . . . . . . . . . . . . . 35
3.3. Certifier le filtrage . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
3.3.1. Ancrage formel . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
3.3.2. Fonction de représentation. . . . . . . . . . . . . . . . . . . . . . . 37
3.3.3. Le langage intermédiaire PIL . . . . . . . . . . . . . . . . . . . . . 39
3.3.4. Processus de validation . . . . . . . . . . . . . . . . . . . . . . . . 45
3.4. Une extension pour Tom et Caml : multi-match . . . . . . . . . . . . . . 53
3.4.1. Sémantique de la séquence. . . . . . . . . . . . . . . . . . . . . . . 54
3.4.2. Correction de la compilation . . . . . . . . . . . . . . . . . . . . . 55
3.5. Génération des contraintes et des obligations de preuve . . . . . . . . . . 57
3.5.1. Algorithme de collecte de contraintes . . . . . . . . . . . . . . . . . 57
3.5.2. Simplification des contraintes . . . . . . . . . . . . . . . . . . . . . 59
3.6. Autres extensions : notation crochet, alias . . . . . . . . . . . . . . . . . . 61
3.6.1. Notations crochet et souligné . . . . . . . . . . . . . . . . . . . . . 61
3.6.2. Alias . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 62
3.6.3. Filtrage de liste . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 62
3.7. Implémentation et intégration . . . . . . . . . . . . . . . . . . . . . . . . . 63
4. Structure de données sûre 65
4.1. Des arbres de syntaxe abstraits en Java . . . . . . . . . . . . . . . . . . . 65
4.1.1. Une bibliothèque générique pour représenter des arbres : ATerm . 66
4.1.2. Un générateur d’implantation typée : ApiGen . . . . . . . . . . . 68
4.2. Discussion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 69
4.2.1. Caractéristiques d’ApiGen pour Java . . . . . . . . . . . . . . . . 69
4.2.2. Améliorations possibles . . . . . . . . . . . . . . . . . . . . . . . . 70
4.2.3. Travaux en rapport. . . . . . . . . . . . . . . . . . . . . . . . . . . 72
4.3. Le langage Gom . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 73
4.3.1. Définir des signatures . . . . . . . . . . . . . . . . . . . . . . . . . 73
4.3.2. Le code généré . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 75
4.3.3. Filtrage pour Tom . . . . . . . . . . . . . . . . . . . . . . . . . . . 84
4.4. Représentants canoniques . . . . . . . . . . . . . . . . . . . . . . . . . . . 84
4.4.1. Hooks . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 85
4.5. Interactions avec Tom . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 87
4.5.1. Un exemple plus élaboré : le calcul des structures . . . . . . . . . . 88
4.5.2. L’approche . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 88
4.5.3. Structure de données . . . . . . . . . . . . . . . . . . . . . . . . . . 90
4.5.4. Les invariants . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 91
4.5.5. Les règles du calcul . . . . . . . . . . . . . . . . . . . . . . . . . . . 94
4.5.6. Stratégie d’application et recherche de preuve . . . . . . . . . . . . 97
iiTable des matières
4.6. Synthèse . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 99
4.6.1. Modules dans Gom . . . . . . . . . . . . . . . . . . . . . . . . . . . 99
4.6.2. Le problème des phases . . . . . . . . . . . . . . . . . . . . . . . . 100
5. Les opérateurs associatifs et leur représentation 101
5.1. Opérateurs associatifs et opérateurs variadiques . . . . . . . . . . . . . . . 101
5.1.1. Signature associative . . . . . . . . . . . . . . . . . . . . . . . . . . 101
5.1.2. Signature variadique . . . . . . . . . . . . . . . . . . . . . . . . . . 102
5.2. Représentants canoniques . . . . . . . . . . . . . . . . . . . . . . . . . . . 103
5.2.1. Représentants canoniques pour les termes associatifs . . . . . . . . 103
5.2.2. Représentants canoniques pour les termes variadiques . . . . . . . 104
5.3. Passer de terme associatif à terme variadique . . . . . . . . . . . . . . . . 104
5.4. Liens entre termes variadiques et termes associatifs . . . . . . . . . . . . . 105
5.5. Preuves, utilisant Coq . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 107
5.5.1. Les fonctions de normalisation et transformation . . . . . . . . . . 108
5.5.2. Les théorèmes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 111
5.6. Synthèse . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 112
6. Stratégies de réécriture réflexives en Java 113
6.1. Langages de stratégies . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 113
6.1.1. Ce qu’on veut pouvoir exprimer. . . . . . . . . . . . . . . . . . . . 113
6.1.2. Tour d’horizon . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 115
6.2. Rendre l’opérateur de récursion μ explicite. . . . . . . . . . . . . . . . . . 123
6.2.1. La μ-expansion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 123
6.2.2. Stratégies visitables . . . . . . . . . . . . . . . . . . . . . . . . . . 125
6.3. Filtrage et transformation de stratégies . . . . . . . . . . . . . . . . . . . 125
6.3.1. Les stratégies sont des termes : un mapping pour Tom . . . . . . . 126
6.3.2. Opérateur μ encore plus explicite . . . . . . . . .