diff options
Diffstat (limited to 'rapport.tm')
| -rw-r--r-- | rapport.tm | 338 |
1 files changed, 338 insertions, 0 deletions
diff --git a/rapport.tm b/rapport.tm new file mode 100644 index 0000000..cb9a68b --- /dev/null +++ b/rapport.tm @@ -0,0 +1,338 @@ +<TeXmacs|1.0.7.21> + +<style|<tuple|article|french>> + +<\body> + <doc-data|<doc-title|Rapport de projet : interprétation + abstraite>|<doc-author|<author-data|<author-name|Alex AUVOLAT>>>> + + <section|Introduction> + + <subsection|Analyse statique abstraite> + + 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. + + <subsection|Notre tâche> + + 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> + <item>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 <verbatim|if>, <verbatim|while>, <verbatim|assert>, + <verbatim|print>, <verbatim|halt> ; + + <item>Prise en charge du non-déterminisme (fonction <verbatim|rand>) ; + + <item>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). + </itemize> + + Notre code s'appuie sur de nombreux éléments extérieurs : + + <\itemize> + <item>La bibliothèque <name|zarith>, pour la manipulation d'entiers en + précision arbitraire ; + + <item>La bibliothèque <name|apron>, pour la manipulation du domaine des + polyhèdres ; + + <item>Un lexer et un parser pour notre fragment de C fourni par + l'enseignant. + </itemize> + + <section|Découpage des modules> + + 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 <verbatim|Z.t> + de la bibliothèque <name|zarith>, qui permet de manipuler des entiers en + précision arbitraire. + + <subsection|La signature de module <verbatim|ENVIRONMENT_DOMAIN>> + + 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 + <verbatim|Interpret.Make>, qui contient le c÷ur de l'interpréteur abstrait. + + <verbatim|> + + <\itemize> + <item><verbatim|type t> + + Le type abstrait représentant un environnement abstrait de notre + interpréteur. + + <item><verbatim|val init, bottom : t> + + Représentations respectives de <math|\<top\>> et <math|\<bot\>>. Remarque + : l'environnement représentant <math|\<top\>> est différent en fonction + des variables que cet environnement contient. <verbatim|init> est + l'environnement <math|\<top\>> ne contenant aucune variable. Il y a une + fonction de test <verbatim|is_bot> mais pas de test <verbatim|is_top> car + celui-ci n'est pas nécessaire. + + <item><verbatim|val addvar, rmvar : t -\<gtr\> id -\<gtr\> t> + + Ajoute une variable à un environnement (elle est initialisée sans aucune + contrainte, c'est-à-dire à <math|\<top\>> dans le cas des environnements + non-relationnels) ; supprime une variable d'un environnement. + + <item><verbatim|val assign : t -\<gtr\> id -\<gtr\> expr ext -\<gtr\> t> + + Réalise l'affectation d'une expression à une variable : + <math|S<around*|\<llbracket\>|x\<leftarrow\>e|\<rrbracket\>>>. + + <item><verbatim|val compare_leq, compare_eq : t -\<gtr\> expr ext + -\<gtr\> expr ext -\<gtr\> t> + + Restreint le domaine abstrait à une portion vérifiant une équation : + <math|S<around*|\<llbracket\>|e<rsub|1>\<leqslant\>e<rsub|2>?|\<rrbracket\>>> + et <math|S<around*|\<llbracket\>|e<rsub|1>=e<rsub|2>?|\<rrbracket\>>>. + + <item><verbatim|val join, meet, widen : t -\<gtr\> t -\<gtr\> t> + + Implémentation de l'union abstraite <math|\<sqcup\>>, de l'intersection + abstraite <math|\<sqcap\>> et de l'opération de widening + <math|\<nabla\>>. + + <item><verbatim|val subset: t -\<gtr\> t -\<gtr\> bool> + + Implémentation de la condition d'inclusion <math|\<sqsubseteq\>>. Une + seule implication : <verbatim|subset a b> + <math|\<Rightarrow\>a\<sqsubseteq\>b>. + </itemize> + + \ + + <subsection|La signature de module <verbatim|VALUE_DOMAIN>> + + 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 <verbatim|NonRelationnal> qui + contient le code générique pour un <verbatim|ENVIRONMENT_DOMAIN> non + relationnel. + + <\itemize> + <item><verbatim|type t> + + Le type abstrait d'une valeur abstraite + + <item><verbatim|val top, bottom : t> + + Les représentations de <math|\<top\>> et <math|\<bot\>>. Il n'y a pas de + fonctions de tests <verbatim|is_bot> et <verbatim|is_top>, les + représentations sont uniques. + + <item><verbatim|val const : Z.t -\<gtr\> t> + + Obtenir la représentation d'une constante. + + <item><verbatim|val rand : Z.t -\<gtr\> Z.t -\<gtr\> t> + + Obtenir la représentation d'un intervalle. + + <item><verbatim|val subset : t -\<gtr\> t -\<gtr\> bool> + + Implémentation de la relation d'inclusion <math|\<sqsubset\>> sur les + valeurs. + + <item><verbatim|val join, meet, widen : t -\<gtr\> t -\<gtr\> t> + + Implémentation de l'union <math|\<sqcup\>>, de l'intersection + <math|\<sqcap\>> et du widening <math|\<nabla\>>. + + <item><verbatim|val neg : t -\<gtr\> t> + + Négation unaire abstraite + + <item><verbatim|val add, sub, mul, div, rem : t -\<gtr\> t -\<gtr\> t> + + Opérateurs binaires abstraits + + <item><verbatim|val leq : t -\<gtr\> t -\<gtr\> t * t> + + Restreint deux valeurs <math|a\<nocomma\>> et <math|b> aux meilleurs + sur-approximations que l'on peut avoir en restreignant le domaine avec + une condition de la forme <math|a\<leqslant\>b>. + </itemize> + + <subsection|Le module <verbatim|Constants>> + + Ce module implémente un <verbatim|VALUE_DOMAIN> correspondant au treillis + des constantes. Le code est extrêmement simple et implémente directement la + sémantique vue en cours. + + <subsection|Le module <verbatim|Intervals>> + + Ce module implémente un <verbatim|VALUE_DOMAIN> correspondant au treillis + des intervales. Le code est extrêmement simple et implémente directement la + sémantique vue en cours. + + <subsection|Le module <verbatim|NonRelationnal>> + + Ce module implémente toutes les fonctions communes aux domaines + non-relationnels (constantes, intervalles). Il est paramétré par un + <verbatim|VALUE_DOMAIN> <verbatim|V>. + + <\itemize> + <item>Le type <verbatim|t> représentant un environnement abstrait est + soit un map des identifieurs vers les éléments de <verbatim|V>, soit + <math|\<bot\>>. Dès qu'une valeur vaur <math|\<bot\>>, on s'interdit de + la mettre dans le map et on transforme tout l'environnement abstrait en + <math|\<bot\>>. La fonction <verbatim|strict> permet de s'en assurer. + + <item>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 <verbatim|V> 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 <verbatim|compare_leq> et <verbatim|compare_eq>. + + <item>Pour un opérateur <math|\<ltimes\>\<in\><around*|{|\<leqslant\>,=|}>>, + les filtrages du type <math|S<around*|\<llbracket\>|e<rsub|1>\<ltimes\>e<rsub|2>?|\<rrbracket\>>> + sont implémentés comme suit (fonction <verbatim|compare>) : + + <\itemize> + <item><math|S<around*|\<llbracket\>|x\<ltimes\>y?|\<rrbracket\>>> : on + applique l'opérateur (<verbatim|leq> pour <math|\<leqslant\>> ou + <verbatim|meet> pour <math|=>) de <verbatim|V> sur les deux valeurs, ce + qui donne deux nouvelles valeurs pour <math|x> et <math|y> (ou deux + fois <math|\<bot\>> si la conditin ne peut pas être remplie). On + utilise ces deux valeurs pour mettre à jour l'environnement. + + <item><math|S<around*|\<llbracket\>|x\<ltimes\>e?|\<rrbracket\>>> et + <math|S<around*|\<llbracket\>|e\<ltimes\>x?|\<rrbracket\>>> : on évalue + l'expression <math|e> et on applique l'opérateur de <verbatim|V> sur + cette valeur et la valeur de <math|x>, ce qui restreint éventuellement + la valeur de <math|x>, ou peut donner <math|\<bot\>>. + + <item><math|S<around*|\<llbracket\>|e<rsub|1>\<ltimes\>e<rsub|2>?|\<rrbracket\>>> + : on évalue les expressions <math|e<rsub|1>> et <math|e<rsub|2>> et on + applique l'opérateur de <verbatim|V>. Aucune valeur n'est restreinte + dans l'environnement mais on peut détecter une condition impossible, + auquel cas l'environnement est passé à <math|\<bot\>>. + </itemize> + + <item>Les opérateurs <math|\<sqcup\>>, <math|\<sqcap\>> et + <math|\<nabla\>> 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. + + <item>L'opérateur <math|\<sqsubset\>> 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. + </itemize> + + <subsection|Le module <verbatim|RelationnalDomain>> + + 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. + + <subsection|Le module <verbatim|Interpret.Make>> + + TODO +</body> + +<\initial> + <\collection> + <associate|page-medium|paper> + <associate|page-screen-margin|false> + </collection> +</initial> + +<\references> + <\collection> + <associate|auto-1|<tuple|1|1>> + <associate|auto-10|<tuple|2.6|?>> + <associate|auto-11|<tuple|2.7|?>> + <associate|auto-2|<tuple|1.1|1>> + <associate|auto-3|<tuple|1.2|1>> + <associate|auto-4|<tuple|2|2>> + <associate|auto-5|<tuple|2.1|2>> + <associate|auto-6|<tuple|2.2|2>> + <associate|auto-7|<tuple|2.3|2>> + <associate|auto-8|<tuple|2.4|2>> + <associate|auto-9|<tuple|2.5|2>> + </collection> +</references> + +<\auxiliary> + <\collection> + <\associate|toc> + <vspace*|1fn><with|font-series|<quote|bold>|math-font-series|<quote|bold>|1<space|2spc>Introduction> + <datoms|<macro|x|<repeat|<arg|x>|<with|font-series|medium|<with|font-size|1|<space|0.2fn>.<space|0.2fn>>>>>|<htab|5mm>> + <no-break><pageref|auto-1><vspace|0.5fn> + + <vspace*|1fn><with|font-series|<quote|bold>|math-font-series|<quote|bold>|2<space|2spc>Découpage + des modules> <datoms|<macro|x|<repeat|<arg|x>|<with|font-series|medium|<with|font-size|1|<space|0.2fn>.<space|0.2fn>>>>>|<htab|5mm>> + <no-break><pageref|auto-2><vspace|0.5fn> + + <with|par-left|<quote|1tab>|2.1<space|2spc>La signature de module + <with|font-family|<quote|tt>|language|<quote|verbatim>|ENVIRONMENT_DOMAIN> + <datoms|<macro|x|<repeat|<arg|x>|<with|font-series|medium|<with|font-size|1|<space|0.2fn>.<space|0.2fn>>>>>|<htab|5mm>> + <no-break><pageref|auto-3>> + + <with|par-left|<quote|1tab>|2.2<space|2spc>La signature de module + <with|font-family|<quote|tt>|language|<quote|verbatim>|VALUE_DOMAIN> + <datoms|<macro|x|<repeat|<arg|x>|<with|font-series|medium|<with|font-size|1|<space|0.2fn>.<space|0.2fn>>>>>|<htab|5mm>> + <no-break><pageref|auto-4>> + + <with|par-left|<quote|1tab>|2.3<space|2spc>Le module + <with|font-family|<quote|tt>|language|<quote|verbatim>|Constants> + <datoms|<macro|x|<repeat|<arg|x>|<with|font-series|medium|<with|font-size|1|<space|0.2fn>.<space|0.2fn>>>>>|<htab|5mm>> + <no-break><pageref|auto-5>> + + <with|par-left|<quote|1tab>|2.4<space|2spc>Le module + <with|font-family|<quote|tt>|language|<quote|verbatim>|Intervals> + <datoms|<macro|x|<repeat|<arg|x>|<with|font-series|medium|<with|font-size|1|<space|0.2fn>.<space|0.2fn>>>>>|<htab|5mm>> + <no-break><pageref|auto-6>> + + <with|par-left|<quote|1tab>|2.5<space|2spc>Le module + <with|font-family|<quote|tt>|language|<quote|verbatim>|NonRelationnal> + <datoms|<macro|x|<repeat|<arg|x>|<with|font-series|medium|<with|font-size|1|<space|0.2fn>.<space|0.2fn>>>>>|<htab|5mm>> + <no-break><pageref|auto-7>> + + <with|par-left|<quote|1tab>|2.6<space|2spc>Le module + <with|font-family|<quote|tt>|language|<quote|verbatim>|RelationnalDomain> + <datoms|<macro|x|<repeat|<arg|x>|<with|font-series|medium|<with|font-size|1|<space|0.2fn>.<space|0.2fn>>>>>|<htab|5mm>> + <no-break><pageref|auto-8>> + + <with|par-left|<quote|1tab>|2.7<space|2spc>Le module + <with|font-family|<quote|tt>|language|<quote|verbatim>|Interpret.Make> + <datoms|<macro|x|<repeat|<arg|x>|<with|font-series|medium|<with|font-size|1|<space|0.2fn>.<space|0.2fn>>>>>|<htab|5mm>> + <no-break><pageref|auto-9>> + </associate> + </collection> +</auxiliary>
\ No newline at end of file |