Conception d'un langage dédié à l'analyse et la transformation de programmes, Design of a programming language dedicated to program analysis and transformation

Emilie Balland

Description

Sous la direction de Claude Kirchner, Pierre-Etienne Moreau
Thèse soutenue le 11 mars 2009: Nancy 1
Développer des analyseurs statiques nécessite une manipulation intensive de structures d'arbres et de graphes représentant le programme. La finalité de cette thèse est de proposer des constructions de langage dédiées au prototypage d'outils d'analyse et de transformation de programmes et inspirées de la réécriture de termes et de termes-graphes. L'originalité de notre approche est d'embarquer ces nouvelles constructions dans les langages généralistes sous la forme d'un langage dédié embarqué. Les travaux de cette thèse se fondent sur le langage Tom qui propose d'embarquer des constructions de réécriture dans des langages généralistes comme Java. La première contribution de cette thèse a été de formaliser les langages embarqués sous le concept de langage îlot. Ce formalisme a ainsi permis de certifier la compilation du langage Tom. Nos travaux sur l'analyse de Bytecode nous ont ensuite conduit à réfléchir à la représentation et la manipulation de graphes de flot de programmes et nous avons alors proposé des constructions de langage inspirées de la réécriture de termes-graphes. Une autre contribution de cette thèse est la conception d'un langage de stratégies adapté à l'expression de propriétés sur un programme. Associé au filtrage, ce langage permet d'exprimer de manière déclarative des analyses et des transformations sur des arbres ou des graphes. Enfin, l'ensemble des propositions de cette thèse a été intégré au langage Tom sous la forme de nouvelles constructions syntaxiques ou d'améliorations de constructions existantes et a ainsi pu être appliqué à l'analyse du langage Java.
-termes-graphes
-analyse statique
-transformation de programmes
-langages embarqués
Developing static analyzers requires an intensive handling of tree and graph structures representing the program. Even if generalist languages such as Java or C++ have libraries dedicated to the manipulation of such structures, the absence of specialized statements makes the code complex and difficult to maintain. The purpose of this thesis is to provide dedicated language constructs to prototype tools for analysis and program transformation inspired by the term and term-graph rewriting. The originality of our approach is to embed these new statements in generalist languages. This is motivated by the development of the Tom language that offers rewriting constructs for generalist languages like Java. The first contribution of this thesis is to formalize embedded languages in the concept of island languages. This formalism enables the certification of the Tom compiler. Our work on Bytecode analysis leads us to propose a dedicated language for the representation and manipulation of program flow graphs. Thus we propose language constructs based on the term-graph rewriting. A further contribution of this thesis is to design a strategy language adapted to the expression of properties on a program. Associated with matching capabilities, this language allows to express in a declarative way analysis and transformations on trees or graphs. Finally, all the proposals of this thesis have been integrated into the Tom language in the form of new statements or improvements of existing ones. This language proposal has been applied to the analysis of Java programs.
Source: http://www.theses.fr/2009NAN10026/document

Informations

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

Extrait

AVERTISSEMENT

Ce document est le fruit d'un long travail approuvé par le
jury de soutenance et mis à disposition de l'ensemble de la
communauté universitaire élargie.

Il est soumis à la propriété intellectuelle de l'auteur. Ceci
implique une obligation de citation et de référencement lors
de l’utilisation de ce document.

D’autre part, toute contrefaçon, plagiat, reproduction
illicite encourt une poursuite pénale.


➢ Contact SCD Nancy 1 : [e-mail]




LIENS


Code de la Propriété Intellectuelle. articles L 122. 4
Code de la Propriété Intellectuelle. articles L 335.2- L 335.10
http://www.cfcopies.com/V2/leg/leg_droi.php
http://www.culture.gouv.fr/culture/infos-pratiques/droits/protection.htm Departement de formation doctorale en informatique
Ecole doctorale IAEM LorraineUniversite Henri Poincare
Conception d’un langage dedie a l’analyse
et la transformation de programmes
THESE
presentee et soutenue publiquement le 11 Mars 2009
pour l’obtention du
Doctorat de l’Universite Henri Poincare
(specialite informatique)
par
Emilie Balland
Composition du jury
President : Bernard Girau Professeur, Universite Henri Poincare, Nancy, France
Rapporteurs : Olivier Danvy Professeur associe, Aarhus, Danemark
Stephane Ducasse Directeur de recherche, INRIA, Lille, France
Examinateurs : Rachid Echahed Charge de recherche, CNRS, Grenoble, France
Claude Kirchner Directeur de INRIA, Nancy, France
Pierre-Etienne Moreau Charge de recherche, INRIA, Nancy, France
Joost Visser Directeur du service R&D de SIG, Amsterdam, Pays-Bas
Laboratoire Lorrain de Recherche en Informatique et ses Applications | UMR 7503AMis en page avec LT XEÀ Paul,
iiiRemerciements
Je tiens tout d’abord à remercier l’ensemble des enseignants de l’Université Henri
Poincaré qui m’ont fait découvrir l’informatique en tant que science et tout particulière-
ment Martine Gautier et Karol Proch qui m’ont communiqué le goût pour les langages
de programmation. Je souhaite aussi remercier Dominique Méry qui, en m’accueillant
en stage, m’a permis de découvrir le monde de la recherche et m’a donné envie de faire
un doctorat.
Je remercie mes directeurs de thèse Pierre-Etienne Moreau et Claude Kirchner, qui
m’ont accompagnée pendant ces trois années et ont toujours su trouver les mots pour
m’encourager. Par leur disponibilité et leur patience, ils m’ont offert des conditions de
travail exemplaires et je leur en suis profondément reconnaissante. Merci en particulier
à Pierre-Etienne pour son enthousiasme communicatif.
Je voudrais remercier les personnes qui ont accepté d’être membres de mon jury.
Stéphane Ducasse et Olivier Danvy ont accepté la tâche d’être rapporteurs. Je tiens
à les remercier pour leurs commentaires et pour l’intérêt qu’ils ont manifesté pour ce
travail. Je suis très touchée que Rachid Echahed ait accepté d’être président de ce jury
car durant cette thèse, nos échanges ont profondément contribué à améliorer mon travail
sur les termes-graphes. Je remercie enfin Joost Visser et Bernard Giraud qui ont accepté
de jouer le rôle d’examinateurs.
Merci à mes collègues et amis de l’équipe Protheo/Pareo pour tous les agréables mo-
ments que nous avons partagés. C’est avec beaucoup de nostalgie que j’ai vu chacun
terminer son doctorat et aujourd’hui, je veux profiter de ces quelques mots pour leur
souhaiter à chacun de réussir dans ce qui leur tient à cœur. Je tiens aussi à remercier
mes amis du projet Tom. En particulier, merci à Antoine Reilles avec qui j’ai beaucoup
travaillé et qui a toujours été de très bon conseil. Ses qualités scientifiques et ses compé-
tences en programmation m’ont toujours impressionnée et il a toujours su les partager
avec beaucoup de simplicité. Merci aussi à Radu Kopetz et Guillaume Burel avec qui
j’ai eu la chance de partager mon bureau et qui ont toujours été très attentionnés et
d’une bonne humeur constante. Je tiens à remercier aussi mes collègues du projet RA-
VAJ et notamment Yohan Boichut et Thomas Genet pour leurs qualités scientifiques et
humaines.
Un grand merci à Yannick Parmentier, Sébastien Hinderer, Eric Kow et Dmitry Sus-
tretov pour tous les bons moments passés ensemble en France et dans les quatre coins
de l’Europe. Enfin, je tiens à remercier ma famille et mes amis. Notamment merci à
Jacques sans qui je ne serais pas là et dont le soutien sans borne a toujours été d’un très
grand réconfort. Merci enfin à Paul pour son amour et la patience avec laquelle il a relu
chaque ligne de cette thèse.
iiiivTable des matières
Extended Abstract 1
Introduction 5
1 Notions préliminaires 11
1.1 Termes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11
1.2 Filtrage . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12
1.3 Théorie équationnelle . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13
1.4 Systèmes de réécriture . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 14
1.5 Confluence et terminaison . . . . . . . . . . . . . . . . . . . . . . . . . . . 14
1.6 Réécriture modulo une théorie équationnelle . . . . . . . . . . . . . . . . . 15
1.7 sous stratégies . . . . . . . . . . . . . . . . . . . . . . . . . . . 15
2 Contexte et motivations 17
2.1 Problématique de cette thèse . . . . . . . . . . . . . . . . . . . . . . . . . 17
2.1.1 Limites des langages dédiés existants . . . . . . . . . . . . . . . . . 17
2.1.2 Point de départ : le langage Tom . . . . . . . . . . . . . . . . . . . 18
2.1.3 Caractéristiques du langage dédié proposé . . . . . . . . . . . . . . 19
2.2 Présentation du langage Tom . . . . . . . . . . . . . . . . . . . . . . . . . 19
2.2.1 Filtrage dans Java . . . . . . . . . . . . . . . . . . . . . . . . . . . 20
2.2.2 Ancrages . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 21
2.2.3 Construction backquote . . . . . . . . . . . . . . . . . . . . . . . . 23
2.2.4 Filtrage associatif . . . . . . . . . . . . . . . . . . . . . . . . . . . 24
2.2.5 Contraintes de filtrage . . . . . . . . . . . . . . . . . . . . . . . . . 25
2.2.6 Notations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 26
2.2.7 Architecture du compilateur Tom . . . . . . . . . . . . . . . . . . . 27
2.3 Apports de cette thèse au langage Tom . . . . . . . . . . . . . . . . . . . . 30
2.3.1 Un langage de stratégies plus expressif . . . . . . . . . . . . . . . . 30
2.3.2 Réécriture de termes-graphes . . . . . . . . . . . . . . . . . . . . . 31
2.3.3 Manipulation de programmes Bytecode Java . . . . . . . . . . . . 31
3 Un cadre théorique pour les langages îlots 33
3.1 Les langages dédiés . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
3.1.1 Patrons de conception pour les langages dédiés . . . . . . . . . . . 34
3.1.2 Cas particulier des langages îlots . . . . . . . . . . . . . . . . . . . 35
3.2 Formalisation des langages îlots . . . . . . . . . . . . . . . . . . . . . . . . 36
3.2.1 Préliminaires . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
vTable des matières
3.2.2 Ancrage syntaxique . . . . . . . . . . . . . . . . . . . . . . . . . . 38
3.2.3 sémantique . . . . . . . . . . . . . . . . . . . . . . . . . . 39
3.2.4 Dissolution . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46
3.2.5 Exemples . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47
3.3 Caractérisation des îlots formels . . . . . . . . . . . . . . . . . . . . . . . . 51
3.4 Un îlot formel pour la réécriture : Tom . . . . . . . . . . . . . . . . . . . . 54
3.4.1 Ancrage syntaxique des îlots Tom dans Java . . . . . . . . . . . . . 55
3.4.2 sémantique des termes algébriques . . . . . . . . . . . . . 55
3.4.3 Dissolution par transformation source à source . . . . . . . . . . . 55
3.4.4 Propriétés d’îlots formels . . . . . . . . . . . . . . . . . . . . . . . 56
3.5 Synthèse . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 57
4 Un langage de stratégies pour l’analyse et la transformation de programmes 59
4.1 Tour d’horizon . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 60
4.1.1 Contrôle dans les langages à base de règles . . . . . . . . . . . . . 60
4.1.2 Traversée générique dans les langages typés . . . . . . . . . . . . . 65
4.2 Syntaxe et sémantique d