Algorithme de complétion pour automates d’arbres à treillis

Algorithme de complétion pour automates d’arbres à treillis

Nous allons voir dans ce chapitre que les techniques actuelles liées au Model-Checking régulier sur arbres ne permettent pas de capturer efficacement à la fois la structure complexe d’un système et certaines de ses caractéristiques. Si on prend par exemple les programmes J ava, la structure d’un terme est efficacement exploitée pour modéliserla structure d’un état du système. En contrepartie, les entiers présents dans les pro- grammes J ava doivent être encodés par des entiers de Peano, et dans ce cas chaque opération arithmétique est potentiellement modélisée par une centaine d’applications de règles de réécriture. Dans ce chapitre, nous proposons les automates d’arbres à treillis (LTA), une version étendue des automates d’arbres dont les feuilles sont équipées avec des éléments d’un treillis.Les LTA nous permettent de représenter des ensembles possiblement infinis de termes pouvant être interprétés. Ces termes interprétables permettent de représenter efficace- ment des domaines complexes et leurs opérations associées. Nous étendons également les opérations booléennes des automates d’arbres classiques aux LTA. Enfin, en tant que contribution principale, nous définissons un nouvel algorithme de complétion, équipé d’une fonction d’abstraction, permettant de calculer l’ensemble possiblement infini des termes interprétables accessibles en un temps fini.

Nous avons vu, dans les chapitres précédents de ce mémoire, que la modélisation grâce à un espace infini d’états était utilisée pour éviter les hypothèses artificielles sur les structures de données, comme par exemple décider d’une borne maximum arbitraire sur la taille des piles ou la valeur des entiers. Nous utilisons alors dans cette thèse une représentation symbolique pour modéliser des espaces infinis d’états : les automates d’arbres (voir définition 2.2.3).Rappelons brièvement que cette représentation est utilisée dans le but de vérifier des propriétés de sûreté sur les systèmes représentés, et que la technique de vérification utilisée est le Model-Checking régulier d’arbres (Regular Tree Model-Checking : RTMC). Dans cette technique, les états du système sont représentés par des automates d’arbres, et son comportement par un système de réécriture. Des techniques d’abstraction et d’ac- célération du calcul des états accessibles sont très souvent utilisées. Parmi ces techniques d’abstraction se trouve la fusion d’états équivalents par équations (l’abstraction équa- tionnelle : section 2.4.2), dont il sera question dans ce chapitre.Dans [Boichut et al., 2007], les auteurs proposent une traduction exacte de la séman- tique de la machine J ava virtuelle en utilisant des automate d’arbres et des règles de réécriture. Cette traduction permet d’analyser des programmes J ava grâce aux model- checkers RTMC classiques. Une des principales difficultés de ce codage est de capturer et gérer les deux dimensions infinies qui peuvent apparaitre dans un programme J ava. En effet, le comportement infini de ces programmes peut être dû à un nombre non- borné d’appels de méthodes ou de création d’objets, ou simplement parce que le pro- gramme manipule des données dont le domaine n’est pas borné, comme par exemple les variables entières. Or, dans le cadre du RTMC, la représentation actuelle de ces données définies sur un domaine infini alourdit significativement le temps de calcul, alors que de multiples comportements infinis sur la structure du programme peuvent être sur-approchés de manière très efficace par la complétion d’automates d’arbres et représenter la structure d’une configuration d’une manière très concise. En effet, les piles peuvent se modéliser facilement par des termes (on peut par exemple avoir la pile stack(1,stack(2,stack(3,nil)))), ou encore, une méthode se représente facilement par le terme frame(m,pc,s,l) où m est le nom de la méthode, pc le point de programme courant, s la pile des instructions, et t le tableau des variables locales.

Mais d’un autre côté, la représentation des entiers relatifs et leurs différentes opé- rations arithmétiques n’est pas optimale et nécessite d’être simplifiée. En effet, pour pouvoir modéliser un entier par un terme, et une opération arithmétique par un en- semble de règles de réécriture, on peut par exemple utiliser l’arithmétique de Peano, où les entiers sont représentés grâce à trois fonctions :Mais cette représentation a un impact exponentiel sur la taille des automates repré- sentant les ensembles d’états du programme aussi bien que sur le temps de calcul des états accessibles. Par exemple, le temps de calcul de « 300 + 400 », représenté par le terme xadd(succ300(zero); succ400(zero)), nécessite d’appliquer 300 fois les règles de réécritures de la figure 5.1 (x + y requiert l’application de x règles de réécriture), et donc d’autant d’étapes de complétion. De la même manière, x y requiert l’application de x (y + 2)bits, et dans ce cas, les opérations arithmétiques sont modélisées par des règles de réécriture codant les opérations binaires. Par exemple, l’entier 5 est représenté par le terme stack(un; stack(un; stack(zero; nil))) (représentant le nombre binaire 110). Cette représentation, bien que plus concise que la précédente, surcharge également la taille des automates et du système de réécriture, ainsi que le calcul des accessibles. Ainsi, une addition x + y implique l’application de log(x) règles de réécriture, ce qui est plus efficace, mais grandement perfectible.