Soutenance mémoire
Autour de la structure d’ordre
En introduction, nous avons vu qu’une analyse par interpr´etation abstraite permet de g´en´erer une sur-approximation des ´etats accessibles du programme.
Cette comparaison ne peut se faire que si l’on a pr´ealablement d´efini un ordre.
Cette section explore les r´esultats de la th´eorie de l’ordre qui nous serviront par la suite. Nous commen¸cons par d´efinir la notion de treillis. Ce concept est particuli`erement important en interpr´etation abstraite car les domaines concrets et abstraits seront suppos´es munis d’une structure de treillis.
Les treillis
Un treillis est une structure ordonnee particuliere. Nous d´efinissons tout d’abord la notion d’ordre. Du point de vue des notations, nous utiliserons par la suite le symbole v pour d´efinir une relation binaire notee de maniere infixe.
Semantique concrete des programmes
Par s´emantique concr`ete, on entend s´emantique des ´etats accessibles. Plus precisement, on appellera s´emantique concrete d’un programme le processus qui permet d’obtenir l’ensemble des etats accessibles `a chaque point de programme.
Pour ce faire, il faut d´ej`a donner un interpr´etation en termes d’accessibilite de chaque commande (arc) du programme. Autrement dit, on d´efinit la s´emantique des commandes . Ensuite, afin d’obtenir les ´etats accessibles `a chaque point de programme, il faut aussi expliquer comment combiner les interpr´etations des commandes de sorte `a obtenir la s´emantique du programme dans son entier.
Analyse approch´ee des programmes
Le but d’une analyse par interpr´etation abstraite est d’inf´erer des propri´et´es particuli`eres de programmes. Ces propri´et´es, que l’on a appel´ees assertions, sont exprim´ees par la s´emantique concr`ete, qui est non calculable en g´en´eral. Nous avons vu, dans la section pr´ec´edente, que cette s´emantique pouvait se d´efinir comme point fixe d’une fonction dans un treillis. Nous avons aussi vu que ce point fixe pouvait se d´efinir de mani`ere it´erative comme limite d’une suite croissante.
Le d´efaut de calculabilit´e de la s´emantique concr`ete s’exprime alors par le fait que cette suite ne converge pas en temps fini. Ceci ne peut se produire dans les treillis v´erifiant la condition de chaˆıne ascendante, puisque cette propri´et´e exprime le fait que toute chaˆıne croissante est stationnaire. L’id´ee derri`ere une analyse par interpr´etation abstraite est de transporter cette proc´edure it´erative, d´efinissant la s´emantique concr`ete, dans un monde approch´e, plus grossier, appel´e ensemble des assertions abstraites A ] , o`u la calculabilit´e pourra ˆetre assur´ee. La question qui se pose alors est celle du choix du monde abstrait. Il faut r´eussir `a concilier au mieux deux exigences antagonistes : l’expressivit´e et l’efficacit´e. Plus pr´ecis´ement, plus le monde abstrait choisi est simple, moins il permet d’exprimer de propri´et´es int´eressantes mais plus les calculs it´eratifs sont rapides. `
A l’inverse, un monde abstrait plus complexe permet d’exprimer plus de propri´et´es mais augmente sensiblement le temps n´ecessaire au calcul de ces propri´et´es. Afin que les calculs dans le domaine des assertions abstraites A ] poss`edent du sens par rapport aux 38.L’interpr´etation abstraite : un cadre g´en´erique pour l’analyse statique assertions concr`etes que l’on souhaitait initialement calculer, il reste alors `a d´efinir comment les deux domaines A et A ] sont reli´es. Autrement dit, il s’agit de d´efinir formellement ce que l’on entend par le terme « approcher ». Le but de cette section est de d´etailler l’ensemble des aspects pr´esent´es dans ce paragraphe.
Structure du domaine abstrait et relation avec le domaine concret : un premier apercu
Nous commen¸cons par d´ecrire sommairement quelques propri´et´es que nous exigeons sur la structure des assertions abstraites A ] et la relation entre domaine concret A et abstrait A ].
Deroulement d’une analyse par interpretation abstraite dans un cadre ideal
En Section 2.3.2, nous avons pr´esent´e la structure de treillis de l’ensemble des assertions abstraites A ] et montr´e comment cet ensemble ´etait reli´e `a l’ensemble
A via une relation de correspondance σ. Cette pr´esentation initiale s’est faite dans un cadre assez large o`u nous avons fait peu d’hypoth`eses. Nous allons maintenant pr´esent´e le d´eroulement d’une analyse par interpr´etation abstraite dans un cadre id´eal : les ensembles A et A ] sont munis de la structure de treillis complet et la relation σ d´efinit une connexion de Galois sur ces ensembles.
Calculs corrects dans le domaine abstrait
Dans cette section, nous nous pla¸cons dans un cadre ideal de la theorie de l’interpretation abstraite. Plus pr´ecis´ement, le domaine concret A et le domaine abstrait A ] sont munis d’une structure de treillis complets et reli´es par une connexion de Galois <α, γ> telle que A ] = α(A).
La question qui se pose `a pr´esent est de savoir comment d´efinir les assertions abstraites verifees par le programme. Elles ne peuvent ˆetre obtenues comme image par α des assertions concr`etes v´erifi´ees par le programme. En effet, ce proc´ed´e requiertd’avoir calcul´e au pr´ealable les assertions concr`etes, ce qui, comme nous l’avons mentionn´e pr´ec´edemment n’est pas toujours possible ou requiert un temps de calcul jug´e trop important. D’autre part, nous avons justement introduit le domaine abstrait dans le but d’y effectuer des calculs de mani`ere plus simple et plus rapide en b´en´eficiant du caract`ere plus grossier de ce domaine. Ces calculs doivent refleter ceux que l’on aimerait effectuer dans le domaine concret. Ils sont censes approcher les calculs concrets par au-dessus. Nous commen¸cons par donner la definition d’approximation correcte.
Analyse par interpretation abstraite dans un cadre plus general
Afin de comprendre comment effectuer des analyses par interpr´etation abstraite dans un cadre autre que le cadre id´eal d´efini pr´ec´edemment, revenons sur l’exemple de l’analyse poly´edrique.
Etude d’un exemple : l’analyse poly´edrique [CH78]
Rappelons que le domaine concret est d´efini par le treillis complet P (R m )(⊆, ∅, R m , ∪, ∩). Le domaine abstrait, quant `a lui est d´efini par le treillis Pm(vP , ⊥P , >P , F P , d P ). Malheureusement, ce treillis n’est pas complet. En effet, la propri´et´e stipulant l’existence d’une borne inf´erieure pour toute partie de Pm n’est pas v´erifi´ee. Il suffit pour s’en convaincre d’´etudier la partie form´ee de tous les poly`edres incluant le disque unit´e. La borne inf´erieure de cette partie est le disque lui-mˆeme, qui n’est pas un ´el´ement de Pm. Nous ne pouvons donc pas utiliser les th´eor`emes pr´esent´es en Section 2.3.2. Cependant, tout n’est pas perdu. Par exemple, nous pouvons d´efinir la fonction de concr´etisation γ : Pm → P(R m )) comme ´etant la fonction qui `a tout poly`edre convexe associe l’ensemble des points qui le compose.A l’oppos´e, il semble difficile de d´efinir une fonction d’abstraction α pour la raison que nous avons d´ej`a mentionn´ee.
En effet, comment d´efinir l’abstraction de l’ensemble des points constituant le disque unit´e ? On peut approcher cet ensemble par une infinit´e de poly`edres mais il n’existe pas, dans le domaine Pm, de meilleure approximation de cet ensemble.
L’exemple de l’analyse poly`edrique soul`eve une question l´egitime : que faire dans le cas o`u l’hypoth`ese de meilleure approximation n’est pas v´erifi´ee ? En fait, on peut r´esoudre se probl`eme par l’utilisation de diverses strat´egies [CC92c]. Nous
Analyse approch´ee des programmes 47 pr´esentons ici deux possibilit´es permettant de se ramener au cas o`u l’hypoth`ese de meilleure approximation est v´erifi´ee par des manipulations sur le domaineabstrait.
Affaiblir les propri´et´es abstraites [CC92c]
On peut analyser la difficult´e rencontr´ee dans le cas de l’analyse poly´edrique par le fait que le domaine abstrait est trop pr´ecis. Ce point de vue consiste `a dire que l’on approche le disque unit´e de trop pr`es, si bien que la meilleure approximation de cet ensemble est le disque lui-mˆeme. L’id´ee est alors de choisir un domaine abstrait plus grossier. Ainsi, afin d’analyser le programme sqrt de la figure 2.3, nous aurions pu choisir le domaine abstrait des intervalles. Pour un programme `a m variables, un ´el´ement du domaine des intervalles est la donn´ee, pour chaque variable x i , d’un intervalle encadrant cette variable. Autrement dit, le domaine abstrait est constitu´e de l’ensemble des hyper rectangles de dimension au plus m. Dans ce domaine, le probl`eme de l’approximation du disque unit´e est trivial : la meilleure approximation du disque unit´e est l’hypercube unit´e. Ce domaine permet de se placer dans le cadre id´eal de l’existence de meilleure approximation. Cependant, le domaine des intervalles est trop grossier pour inf´erer les propri´et´es que l’on souhaite, `a savoir −2r + t − 1 = 0 et −n + s − 1 ≥ 0 (voir figure 2.3).
Analyse de programmes a couts
Un grand nombre des objets du quotidien embarquent des syst`emes ´electroniques. Cette tendance, comme nous l’avons d´ej`a mentionn´e, continue de se d´evelopper dans les domaines de l’automobile, de l’a´eronautique mais aussi dans le domaine m´edical. Dans ce chapitre, nous nous int´eressons particuli`erement aux syst`emes embarqu´es dont l’utilisation de ressources est limit´ee. Ceci peut se traduire par une limitation de l’espace m´emoire ou du temps durant lequel le programme peut s’ex´ecuter. Si l’on consid`ere l’exemple des technologies « portables » (tels que les t´el´ephones, ordinateurs, tablettes), on peut aussi citer une limitation des ressources ´energ´etiques disponibles (batteries limit´ees). L’analyse de tels syst`emes, pour lesquels la consommation de ressources est un probl`eme critique, doit permettre d’inf´erer des propri´et´es quantitatives assurant que les ressources disponibles seront suffisantes lors de l’ex´ecution.
Afin de r´epondre `a ce probl`eme, nous ´etudions, dans ce chapitre, la possibilit´e de quantifier par interpr´etation abstraite, l’utilisation des ressources d’un programme. La difficult´e de ce probl`eme est li´ee `a la nature de la th´eorie de l’interpr´etation abstraite. Nous avons vu dans le Chapitre 2, que cette th´eorie propose un cadre d’approximation bas´e sur la notion de treillis.`A l’aide de ces treillis, nous avons vu que nous pouvions comparer entre elles les abstractions. On peut ainsi d´efinir la qualit´e des approximations effectu´ees et notamment la notion de meilleure approximation. ` A l’oppos´e, les notions quantitatives n’apparaissent pas naturellement dans ce cadre. Nous cherchons, dans ce chapitre, `a r´econcilier ces deux aspects.
Plus pr´ecis´ement, nous pr´esentons une m´ethode permettant d’approcher, de mani`ere correcte, un mesure sur les programmes transportant des coˆuts.
La premi`ere ´etape de notre m´ethode consiste `a d´efinir ce genre de programmes.
Dans la suite, ces programmes seront repr´esent´es par une relation de transition ´etiquet´ee par des coˆuts. On notera σ → q σ 0 une transition entre l’´etat σ et l’´etat σ 0 poss´edant le coˆut q. Afin de pouvoir combiner les coˆuts des transitions, nous `a coˆuts supposerons que l’ensemble Q des coˆuts admet une structure particuli`ere. Plus pr´ecis´ement, nous supposerons l’existence d’un op´erateur not´e multiplicativement ⊗, permettant d’accumuler les coˆuts le long d’un chemin (s´equence de transitions) ainsi que l’existence d’un op´erateur not´e additivement ⊕, permettant de combiner les coˆuts de diff´erents chemins. Ces deux coˆuts munissent l’ensemble Q d’une structure appel´ee dio ¨ ıde. Nous verrons que cette structure permet de d´efinir une autre structure, appel´ee modulo ¨ ıde. Cette derni`ere structure est particuli`erement importante car elle permet de repr´esenter la s´emantique ´etiquet´ee de nos programmes sous forme matricielle. Cette matrice, index´ee par l’ensemble des ´etats du programme, transporte, en coefficients, les coˆuts du programme.
Notre analyse se concentre sur l’´etude de programmes dont le comportement est cyclique (tels que les syst`emes r´eactifs) dont la propri´et´e d’int´erˆet est le comportement asymptotique le long des cycles plutˆot que le coˆut global du programme en son entier. Ce comportement est d´ecrit par une mesure nomm´ee coˆut longrun. Cette ´enomination provient du cas classique o`u l’op´eration ⊗ du dio ¨ ıde correspond `a l’op´eration d’addition + arithm´etique. Dans ce cas, on montre que le coˆut long-run correspond `a la limite du coˆut moyen maximum sur des traces arbitrairement longues.
Le coˆut long-run ´etant g´en´eralement non calculable, nous d´efinissons un cadre d’approximation permettant d’inf´erer une sur-approximation de ce coˆut. Ce cadre tire parti de l’expression lin´eaire de la s´emantique de nos programmes. Plus pr´ecis´ement, nous verrons que toute abstraction α sur les ´etats d’un programme peut ˆetre relev´ee en un op´erateur matriciel α ↑ . Cette abstraction lin´eaire poss`ede alors l’avantage d’admettre une fonction r´esidu´ee γ ↑ , ce qui revient `a dire que le couple (α ↑ , γ ↑ ) forme une connexion de Galois. Ainsi, via ce rel`evement lin´eaire, nous d´efinissons une analyse par interpr´etation abstraite.
Notons au passage que nous ne supposons pas de propri´et´e particuli`ere sur les abstractions initiales α et que c’est le rel`evement lin´eaire qui permet de voir ces abstractions comme des ´el´ements d’une connexion de Galois. Ainsi, les abstractions initiales les plus ´el´ementaires consistent en un partitionnement des ´etats par fusion. Toutefois, nous nous sommes aussi interrog´es sur la possibilite d’utiliser des abstractions α plus complexes comme celles issues de connexions de Galois. Dans ce cas, nous verrons que le rel`evement lin´eaire n’est pas tr`es efficace et qu’il ne permet pas le transport des structures ordonn´ees. Nous nous attacherons alors `a proposer un rel`evement plus performant, qui respecte la notion d’ordre sur les ´etats tout en restant dans le cadre lin´eaire d´efini par notre methode.
Ce chapitre est structur´e comme suit. En Section 3.1, nous presentons la notion de programmes quantitatifs. En Section 3.2, nous d´ecrivons les propri´et´es qui munissent l’ensemble des couts Q d’une structure de dioıde particuliere nommee.
Les programmes quantitatifs 53 dio ¨ ıde de coˆuts. En Section 3.3 nous presenterons le cadre lineaire induit par les operations du dioıde de couts. Nous presenterons alors la notion de coˆut long-run.
Ce coˆut n’´etant pas directement calculable, nous proc´ederons `a des approximations. Nous ´etaillerons en Section 3.4, notre cadre d’approximation ainsi que le rel`evement lin´eaire sur lequel il se base. En Section 3.5, nous ´etudierons alors un rel`evement plus adapt´e lorsque l’abstraction initiale est issue d’une connexion de
Galois. Autrement dit, nous verrons comment l’on peut int´egrer les abstractions classiques de l’interpr´etation abstraite dans notre cadre lin´eaire. Enfin, nous illustrerons notre analyse en l’impl´ementant sur un exemple en Section 3.6 et finirons par un ´etat de l’art en Section 3.7.
Les programmes quantitatifs
L’analyse presentee dans ce chapitre a pour but d’inf´erer une surapproximation du coˆut asymptotique de programmes porteurs d’informations quantitatives. Dans cette section, nous presentons les programmes qui sont trait´es par notre analyse.
|
Table des matières
1 Introduction
1.1 Motivations
1.2 Structure de ce manuscrit
2 L’interpretation abstraite : un cadre generique pour l’analyse statique
2.1 Autour de la structure d’ordre
2.1.1 Les treillis
2.1.2 Calculer dans les treillis
2.1.2.1 Les morphismes d’ordre et d’union
2.1.2.2 Points fixes dans les treillis
2.2 Syntaxe et s´emantique des programmes
2.2.1 Syntaxe des programmes
2.2.2 S´emantique concr`ete des programmes
2.2.2.1 Le domaine concret
2.2.2.2 S´emantique concr`ete des commandes
2.2.2.3 S´emantique concr`ete : approche MOP et approche par plus petit point fixe
2.2.2.4 Une autre ( ?) d´efinition de la s´emantique
2.3 Analyse approch´ee des programmes
2.3.1 Structure du domaine abstrait et relation avec le domaine concret : un premier aper¸cu
2.3.1.1 Structure de l’ensemble des assertions abstraites
2.3.1.2 Relation entre assertions concr`etes et abstraites [CC92c]
2.3.2 D´eroulement d’une analyse par interpr´etation abstraite dans un cadre ideal
2.3.2.1 Connexions de Galois sur treillis complets
2.3.2.2 Calculs corrects dans le domaine abstrait
2.3.2.3 Notion de meilleure fonction abstraite
2 Table des matieres
2.3.3 Analyse par interpretation abstraite dans un cadre plus general
3 Analyse de programmes a couts
3.1 Les programmes quantitatifs
3.1.1 Syntaxe des programmes quantitatifs
3.1.2 S´emantique des programmes quantitatifs
3.2 Une structure mathematique adaptee : les dioıdes de couts
3.2.1 Les operateurs ⊕ et ⊗
3.2.2 Notion de dio ¨ ıde et ordre associe
3.2.3 Les dioıdes de couts
3.2.3.1 L’op´erateur racine n-i`eme
3.2.3.2 Les dio ¨ ıdes de coˆuts : d´efinition
3.2.4 Exemples de dio ¨ ıdes de coˆuts
3.3 S´emantique lin´eaire et coˆut long-run .
3.3.1 Matrice de transition et modulo ¨ ıde
3.3.2 Coˆut long-run
3.3.2.1 Quand les traces rejoignent les cycles
3.4 Abstraire un programme `a couts
3.4.1 Connexions de Galois dans les modulo ıdes
3.4.2 Rel`evement des abstractions
3.4.3 S´emantique abstraite induite
3.4.4 Analyse de coˆut long-run
3.5 Int´egration des abstractions classiques dans le modele lineaire
3.5.1 Critique du relevement lineaire
3.5.2 Rel`evement parfait des connexions de Galois
3.5.2.1 Rel`evement parfait dans le cas des parties d’ensemble
3.5.2.2 Rel`evement parfait dans le cas general
3.5.3 Rel`evement semi-parfait de connexions de Galois
3.6 Impl´ementation de la m´ethode sur un exemple
3.6.1 Syntaxe
3.6.2 S´emantique op´erationnelle quantitative
3.6.3 Abstraction
3.6.4 R´esultats exp´erimentaux
3.7 Comparaison avec les approches existantes
4 Generation rapide d’invariants inductifs sous forme d’´egalit´es polynomiales
4.1 Une structure math´ematique adapt´ee : les id´eaux
4.2 Les programmes polynomiaux
4.2.1 Syntaxe des programmes polynomiaux
4.2.2 S´emantique concr`ete des programmes polynomiaux
4.2.2.1 S´emantique op´erationnelle petit pas et accessibilit´e
4.2.2.2 S´emantique concr`ete arri`ere
4.2.2.3 Comparaison de la s´emantique concr`ete arri`ere avec la SOPP
4.3 Analyse approch´ee : g´en´eration d’invariants polynomiaux par proc´edure it´erative . . . . . . . . .
4.3.1 S´emantique abstraite
4.3.1.1 Abstraction des programmes polynomiaux
4.3.1.2 Correction de l’abstraction
4.3.2 G´en´eration d’invariants par proc´edure it´erative
4.3.3 Des preuves Coq
4.4 Le cas particulier des invariants inductifs
4.4.1 L’hypoth`ese d’inductivite
4.4.2 L’analyse fastind
4.4.2.1 Les contraintes d’id´eaux
4.4.2.2 S´emantique abstraite
4.4.2.3 Correction de l’analyse fastind
4.4.3Etude d’un exemple
4.5 R´esultats exp´erimentaux
4.5.1 Comparaison avec le travail de M¨ uller-Olm & Seidl
4.5.1.1 Description de la m´ethode
4.5.1.2 Comparaison s´emantique
4.5.1.3 Comparaison des impl´ementations
4.5.2 Comparaison avec le travail de Sankaranarayanan et al
4.5.2.1 Description de la methode
4.5.2.2 Comparaison semantique
4.5.2.3 Comparaison des impl´ementations
4.5.3 Comparaison avec le travail de Rodr´ıguez-Carbonell et Kapur sur les boucles simples . . . . . .
4.5.3.1 Description de la m´ethode
4.5.3.2 Comparaison s´emantique
4.5.3.3 Comparaison des impl´ementations
4.5.4 Comparaison avec la seconde approche Rodr´ıguez-Carbonell et Kapur
4.5.4.1 Description de la methode
4.5.4.2 Comparaison semantique
4.5.4.3 Comparaison des implementations
4.5.5 Integration de notre analyse dans l’analyseur statique sawja
4 Table des matieres
5 Conclusion
5.1 Bilan sur nos travaux
5.1.1 Dans le domaine des analyses quantitatives
5.1.2 Dans le domaine de la g´en´eration d’invariant
5.2 Perspectives
5.2.1 Dans le domaine des analyses quantitatives
5.2.2 Dans le domaine de la generation d’invariants
A Chapitre 3 : Analyse des programmes a couts
A.1 Section 3.4 : Abstraire un programme a couts
A.2 Section 3.6 : Implementation de la methode sur un exemple
B Chapitre 4 : G´en´eration rapide d’invariants inductifs sous forme d’egalites polynomiales
B.1 Section 4.2 : Les programmes polynomiaux
Bibliographie
