1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
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>
|
