> <\body> |>>> L'analyse statique abstraite d'un programme consiste à exécuter ce programme non pas sur une entrée particulière mais sur un domaine abstrait qui représente toute un ensemble de données possibles. Cette façon de tester permet de découvrir des propriétés qui sont vraies quelle que soit l'entrée sur laquelle le programme est exécuté, et ce en une seule passe d'analyse statique (dont on est sûre qu'elle termine - contrairement au programme lui-même). L'analyse abstraite consiste à faire se propager le domaine abstrait à tous les points du programme. En plaçant des assertions à des endroits judicieux, on peut s'assurer que certaines conditions sont toujours vérifiées. Le domaine abstrait ne peut pas représenter avec la précision nécessaire (infinie) exactement tous les états du programme, c'est pourquoi nous sommes obligés d'en considérer une sur-approximation. Le but du jeu étant d'avoir la sur-approximation avec le moins de marge par rapport aux ensembles d'états concrets représentés, afin de pouvoir prouver un maximum de propriétés. Dans le cadre du cours \S sémantique et application à la vérification de programmes \T, nous avons eu à travailler sur un interpréteur abstrait pour un fragment du langage C. Le travail minimum demandé comportait les aspects suivants : <\itemize> Définition d'un interpréteur sur un domaine abstrait prenant en compte les déclarations de variables locales, les affectations, ainsi que les constructions , , , , ; Prise en charge du non-déterminisme (fonction ) ; Interprétation possible dans plusieurs domaines abstraits : deux domaines non-relationnels (treillis des constantes et treillis des intervalles) et un domaine relationnel (domaine des polyhèdres). Notre code s'appuie sur de nombreux éléments extérieurs : <\itemize> La bibliothèque , pour la manipulation d'entiers en précision arbitraire ; La bibliothèque , pour la manipulation du domaine des polyhèdres ; Un lexer et un parser pour notre fragment de C fourni par l'enseignant. Pour réaliser ce projet, nous avons tenté de factoriser notre code au maximum. Grâce à une interface de modules et de foncteurs astucieuse, nous avons écrit un code dont la partie \S interprétation abstraite \T fait moins de 1000 lignes. Nous présentons maintenant des extraits de cette interface, largement inspirée de celle proposée par l'enseignant dans les transparents de son cours \S Abstract Interpretation II \T. Dans tout le code, les entiers sont représentés par le type de la bibliothèque , qui permet de manipuler des entiers en précision arbitraire. > Cette signature de module définit les fonctions que doivent implémenter tout module pouvant être utilisé comme domaine abstrait (relationnel ou non relationnel). Il est utilisé pour paramétrer le module , qui contient le c÷ur de l'interpréteur abstrait. <\itemize> Le type abstrait représentant un environnement abstrait de notre interpréteur. Représentations respectives de > et >. Remarque : l'environnement représentant > est différent en fonction des variables que cet environnement contient. est l'environnement > ne contenant aucune variable. Il y a une fonction de test mais pas de test car celui-ci n'est pas nécessaire. id -\ t> Ajoute une variable à un environnement (elle est initialisée sans aucune contrainte, c'est-à-dire à > dans le cas des environnements non-relationnels) ; supprime une variable d'un environnement. id -\ expr ext -\ t> Réalise l'affectation d'une expression à une variable : |x\e|\>>. expr ext -\ expr ext -\ t> Restreint le domaine abstrait à une portion vérifiant une équation : |e\e?|\>> et |e=e?|\>>. t -\ t> Implémentation de l'union abstraite >, de l'intersection abstraite > et de l'opération de widening >. t -\ bool> Implémentation de la condition d'inclusion >. Une seule implication : a\b>. \ > Cette signature de module définit les fonctions requises pour tout module décrivant un domaine de valeurs pour une abstraction non relationnelle. Cette signature est le paramètre du module qui contient le code générique pour un non relationnel. <\itemize> Le type abstrait d'une valeur abstraite Les représentations de > et >. Il n'y a pas de fonctions de tests et , les représentations sont uniques. t> Obtenir la représentation d'une constante. Z.t -\ t> Obtenir la représentation d'un intervalle. t -\ bool> Implémentation de la relation d'inclusion > sur les valeurs. t -\ t> Implémentation de l'union >, de l'intersection > et du widening >. t> Négation unaire abstraite t -\ t> Opérateurs binaires abstraits t -\ t * t> Restreint deux valeurs > et aux meilleurs sur-approximations que l'on peut avoir en restreignant le domaine avec une condition de la forme b>. > Ce module implémente un correspondant au treillis des constantes. Le code est extrêmement simple et implémente directement la sémantique vue en cours. > Ce module implémente un correspondant au treillis des intervales. Le code est extrêmement simple et implémente directement la sémantique vue en cours. > Ce module implémente toutes les fonctions communes aux domaines non-relationnels (constantes, intervalles). Il est paramétré par un . <\itemize> Le type représentant un environnement abstrait est soit un map des identifieurs vers les éléments de , soit >. Dès qu'une valeur vaur >, on s'interdit de la mettre dans le map et on transforme tout l'environnement abstrait en >. La fonction permet de s'en assurer. Les expressions sont évaluées selont des modalités très simples : on récupère les valeurs abstraites correspondant aux constantes et aux variables et on applique les opérateurs de qui correspondent, ce qui donne une nouvelle valeur. L'évaluation d'une expression de cette manière est utiliée pour l'affectation ainsi que dans les operations et . Pour un opérateur \,=|}>>, les filtrages du type |e\e?|\>> sont implémentés comme suit (fonction ) : <\itemize> |x\y?|\>> : on applique l'opérateur ( pour > ou pour ) de sur les deux valeurs, ce qui donne deux nouvelles valeurs pour et (ou deux fois > si la conditin ne peut pas être remplie). On utilise ces deux valeurs pour mettre à jour l'environnement. |x\e?|\>> et |e\x?|\>> : on évalue l'expression et on applique l'opérateur de sur cette valeur et la valeur de , ce qui restreint éventuellement la valeur de , ou peut donner >. |e\e?|\>> : on évalue les expressions > et > et on applique l'opérateur de . Aucune valeur n'est restreinte dans l'environnement mais on peut détecter une condition impossible, auquel cas l'environnement est passé à >. Les opérateurs >, > et > sur les environnements appliquent l'opérateur correspondant sur les valeurs point-par-point pour chaque variable. Pour que ces opérateurs n'échouent pas, il faut que les mêmes variables soient déclarées dans les deux environnements. L'opérateur > sur les environnements fonctionne aussi point-par-point mais n'échoue pas dans le cas de deux environnements ne déclarant pas les mêmes variables. > Ce module implémente le domaine abstrait des polyhèdres (domaine relationnel) en faisant appel à la bibliothèque Apron. En pratique, ce module fait une simple traduction entre les appels et structures de notre programme et ceux de la bibliothèque Apron. > TODO <\initial> <\collection> <\references> <\collection> > > > > > > > > > > > <\auxiliary> <\collection> <\associate|toc> |math-font-series||1Introduction> |.>>>>|> |math-font-series||2Découpage des modules> |.>>>>|> |2.1La signature de module |language||ENVIRONMENT_DOMAIN> |.>>>>|> > |2.2La signature de module |language||VALUE_DOMAIN> |.>>>>|> > |2.3Le module |language||Constants> |.>>>>|> > |2.4Le module |language||Intervals> |.>>>>|> > |2.5Le module |language||NonRelationnal> |.>>>>|> > |2.6Le module |language||RelationnalDomain> |.>>>>|> > |2.7Le module |language||Interpret.Make> |.>>>>|> >