<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>
