Aksjeeieropplysningsregister i privat regi

contrainte locale pour le maxcount et une globale pour le totalcount.

L’automate 5.14b permet d’isoler la derni`ere it´eration d’une boucle et devrait ˆetre construit lorsque la balise <iteration> d’une boucle comportera un attribut number="-1". Cependant il contient de l’ind´eterminisme qui n’est pas support´e par le formalisme actuel des HFAs, mais qui reste n´ecessaire puisque le r´esultat recherch´e est lui-mˆeme un CFG ind´eterministe, comme le montre le graphe 5.13b. Nous souhai- tons ici donner l’intuition qu’il est possible de construire un HFA ind´eterministe qui permettrait d’aboutir au r´esultat voulu.

Dans le sous-automate de L , l’entr´ee de la premi`ere it´eration pourra ˆetre captur´ee par la transition I Ie I' , mais ´egalement par l’entr´ee dans le contexte isol´e de la derni`ere it´eration via I Ie I , ce qui correspond au cas ou la premi`ere it´eration est aussi la derni`ere. Lorsqu’on se trouve dans l’´etat I' , les tours sont d´ecompt´es grˆace `a la variable n sur l’arc retour, mais la sortie de la boucle via Lx et interdite, pour forcer le passage dans le contexte I lors de la derni`ere it´eration. La sortie du contexte de la derni`ere it´eration aboutira pour finir dans l’´etat I'' o`u une nouvelle entr´ee dans une it´eration via Ie sera interdite.

5.5

Les contraintes num´eriques

Un des ´el´ements cl´e dans la pr´ecision de l’estimation du WCET d’un programme est le nombre de chemins infaisables tir´es des annotations qu’il a ´et´e possible d’int´egrer dans l’analyse. Les bornes de boucles par exemple sont n´ecessaire pour obtenir un pre- mier r´esultat mais il est possible de fournir des informations additionnelles susceptibles d’´eliminer de chemins infaisables suppl´ementaires, au moyen par exemple de contraintes num´eriques. Par exemple, un expert ou une analyse automatique sera parfois capable d’exprimer une exclusivit´e entre deux arcs du CFG, ou entre deux conditions du pro- gramme source, ce qui pourrait permettre, `a terme, de r´eduire le pessimisme de l’analyse de WCET.

Le format FFX supporte ce genre de contraintes num´eriques grˆace `a la balise <control-constraint> associ´ee `a des ´el´ements d´eclar´es comme des identifiants. La grammaire de cette balise est fournie en appendice A.

Habituellement, ces contraintes num´eriques sont directement int´egr´ees dans le syst`e- me ILP utilis´e dans la m´_{ethode IPET par Otawa. Les HFAs peuvent servir de support}

CHAPITRE 5. APPLICATION AU LANGAGE D’ANNOTATION FFX

dans le transfert des contraintes depuis le langage d’annotation vers ce syst`eme ILP, mais ils offrent ´egalement la possibilit´e de manipuler ces contraintes pour les repr´esenter sous forme d’automate d´epli´e, et les int´egrer ainsi non plus comme contraintes num´e- riques mais dans la structure mˆeme du CFG. Nous ne d´etaillerons pas ce point ici car il sera au cœur du chapitre 6. Nous y verrons notamment que l’int´egration sous forme de d´epliage du CFG permet d’am´eliorer la pr´ecision des analyses bas niveau. En effet, la duplication de certains blocs r´eduit parfois le nombre de chemins possibles dans le CFG et supprime par la mˆeme occasion certaines op´erations d’unions (sur les ´etats des caches abstraits principalement) qui ´etaient responsables de l’injection de pessimisme dans les analyses sur la mod´elisation du mat´eriel.

5.6

Conclusion

Nous avons montr´e dans ce chapitre comment il ´etait possible de construire des HFAs `a partir des annotations de flot exprim´ees dans le langage FFX et utilis´ees habituellement dans l’estimation de WCET par la m´ethode IPET. Les contextes des diff´erentes structures d’un programme, `a savoir les appels de fonction, les fonctions, les boucles et les it´erations de boucles ont ´et´e repr´esent´es sous forme de HFAs dans lesquels on a montr´e comment il ´etait possible d’exprimer des attributs comme les bornes de boucles locales et totales.

Par ailleurs, l’´etoile (∗) permettant de repr´esenter des ensembles de transitions a ´

et´e introduite ainsi que des r`egles de priorit´e destin´ees `a condenser et simplifier la repr´esentations des HFAs.

Enfin, des structures particuli`eres destin´ees `a d´eplier des contextes sp´ecifiques comme une it´eration pr´ecise d’une boucle ont ´et´e pr´esent´ees, et nous avons donn´e l’intuition du d´epliage de CFG qu’il ´etait possible de faire en repr´esentant des contraintes num´eriques sous forme d’automates, ainsi que les b´en´efices potentiels qui pouvaient en d´ecouler, mais ce point fera l’objet du chapitre suivant.

“Beneath this mask there is more than flesh. Beneath this mask there is an idea, Mr. Creedy, and ideas are bulletproof.”

— V

6

Compromis entre d´epliage du CFG et

int´egration par contraintes

Sommaire

6.1 Introduction . . . 93 6.2 Un premier exemple d’int´egration par d´epliage . . . 94 6.3 Exp´eriences . . . 98 6.4 Le d´epliage de contraintes num´eriques . . . 107 6.5 Conclusion . . . 112

6.1

Introduction

Dans la partie 2.5.2, nous mettons en avant la possibilit´e offerte par l’expressivit´e des automates pour int´egrer des annotations de flot dans la structure mˆeme du CFG plutˆot qu’au moyen d’une contrainte ILP suppl´ementaire. On d´etaille dans ce chapitre

CHAPITRE 6. COMPROMIS ENTRE D´EPLIAGE DU CFG ET INT´EGRATION PAR CONTRAINTES

ces deux m´ethodes d’int´egration et leurs impacts respectifs sur l’estimation de WCET par la m´ethode IPET. Ce chapitre reprend et ´etend l’article [46].

Dans un premier temps, nous illustrerons le d´epliage partiel de CFG sur un exemple, afin de mettre en ´evidence les diff´erences entre le r´esultat de l’int´egration d’annotation par ce d´epliage et l’int´egration par l’ajout de contraintes ILP.

On pr´esentera ensuite des exp´erimentations permettant de comparer les r´esultats issus de ces deux m´ethodes d’int´egration. On pr´esentera notamment les modules du plug-in int´egr´_{e dans l’outil Otawa et d´evelopp´e sp´ecifiquement pour g´erer la transfor-} mation de fichiers FFX en automates et pour int´egrer les annotations port´ees par ces automates dans une analyse de WCET par IPET.

Enfin, nous montrerons comment il est possible d’exprimer syst´ematiquement des contraintes num´eriques sous forme de restrictions structurelles des automates, et com- ment ce proc´ed´e peut aboutir `a un d´epliage partiel du CFG et `a des b´en´efices de pr´ecision de l’estimation de WCET. Pour cela, nous utiliserons des r´esultats exp´eri- mentaux issus d’un programme sp´ecifique destin´e `a faire la preuve de concept de cette approche.