Analyse par intervalles

Eric Goubault

`Eric.Goubault@cea.fr`

1 Préambule

L'objet de ce projet est d'implémenter une méthode classique [2] permettant d'analyser ce qui peut se passer à l'exécution d'un programme impératif simple. Ce que l'on entend par là est d'être capable de déterminer automatiquement, à la lecture du code source du programme analysé, un sur-ensemble des valeurs que peuvent prendre les variables, et ceci à chaque ligne du programme. Cela permet ensuite de vérifier le programme, en particulier de voir si les valeurs attendues du programme sont bien celles trouvées par l'analyseur, ou cela peut faire partie d'un optimiseur de code (en particulier pour la parallélisation) lors de la compilation du programme. L'idée est d'utiliser une représentation approximée mais correcte [3, 1] des valeurs possibles des variables, et d'inférer automatiquement celles-ci par des moyens calculatoires simples dans tout un programme, sans l'exécuter: on a alors une certitude sur le programme dans tous les cas d'exécution possible. De telles techniques d'«interprétation abstraite» sont utilisées dans des compilateurs ainsi que dans des outils de vérification automatique de logiciels (Polyspace Verifier par exemple, utilisé en particulier pour la vérification de certains programmes d'Ariane V, après la catastrophe du vol 501).

Dans la suite de ces notes, on présente d'abord la syntaxe des programmes à analyser (section 2). On continue en donnant une approximation possible des valeurs des variables par des intervalles de valeurs (section 3), détaillant les opérations élémentaires que l'on peut effectuer avec cette approximation. Dans la section 4, on donne les algorithmes permettant d'approximer l'effet de chaque instruction du langage sur les variables, exprimé en termes d'intervalles entre les valeurs de celles-ci. C'est ce que l'on appelle une sémantique abstraite du langage. Enfin, on passe à l'explication de la façon pratique de réaliser le projet dans la section 5.

2 Syntaxe du Langage

On décrit ici un langage impératif simple dont les instructions agissent en modifiant les valeurs de variables entières d'un ensemble de variables Var.

Les expressions arithmétiques sur ces variables sont,

Expr	=	`cste`	expression constante entière
		X	variable X Î Var
		Expr`+`Expr	somme
		Expr``Expr*	produit
		Expr`-`Expr	différence
		Expr`/`Expr	division
		(Expr)	parenthésage

Les tests sur les expressions arithmétiques sont,

Test	=	Expr == 0	test de nullité
		Expr > 0	test de positivité stricte
		Expr ³ 0	test de positivité

Puis les instructions élémentaires du langage sont,

Instr	=	X`=`Expr	affectation pour X Î Var
		`if` Test `then` Bloc `else` Bloc	branchement conditionnel
		`while` (Test) Bloc	boucle while

où un bloc d'instruction est défini par,

Bloc	=	Ø	bloc vide
		Instr`;` Bloc	concaténation

Enfin un programme Prog est une suite de blocs Bloc; Bloc; ···; Bloc.

On suppose par la suite que des étiquettes sont associées par défaut aux instructions dans un programme comme suit,

une étiquette est un entier. Tout programme commence par l'étiquette (0).
chaque instruction Instr de Prog qui n'est pas un if a une étiquette gauche (l) et une étiquette droite (r) et l'on note (l) Instr (r). Par défaut on pose r=l+1.
dans le cas d'un bloc, Instr; Bloc, l'étiquette gauche de la première instruction de Bloc (appelée étiquette gauche de Bloc en bref) est égale à l'étiquette droite de Instr. L'étiquette droite de la dernière instruction de Bloc est appelée en bref l'étiquette droite de Bloc.
dans le cas de l'instruction composée Instr º if Test then Bloc₁ else Bloc₂ l'étiquette gauche de Bloc₁ est l'étiquette gauche de l'instruction Instr plus un. L'étiquette gauche de Bloc₂ est l'étiquette droite de Bloc₁ plus un. L'étiquette droite de Instr est égale à l'étiquette droite de Bloc₂ plus un.
dans le cas d'une boucle Instr º while (Test) Bloc: l'étiquette gauche de Bloc est l'étiquette gauche de Instr plus un. L'étiquette droite de Instr est l'étiquette droite de Bloc plus un.

On se reportera à la section 4.3 pour un exemple.

3 Domaine des intervalles

On suppose ici que Var={x₁,···,x_N}. On appelle domaine des intervalles

I = { [a₁,b₁]× ... × [a_N,b_N] | a_i, b_i Î Z È {-¥,+¥} }

Le domaine des intervalles abstrait les valeurs que peuvent prendre les variables de Var (considérées comme un élément de Z^N), de manière évidente: soit

a: Ã( Z^N) ® I

avec a(S)=[min p₁(S),max p₂(S)] × ... × [min p_N(S),max p_N(S)] où p_i: Z^N ® Z est la ième projection sur les entiers. Cette fonction est appelée fonction d'abstraction, elle décrit la perte d'information que l'on se permet, en représentant ici les ensembles de valeurs dans Z^N par des hypercubes de dimension N.

L'inclusion d'ensemble de n-uplets induit un ordre sur les éléments de I. Il se trouve que cet ordre, noté simplement £, fait de I un treillis complet, c'est à dire que,

étant donné deux élements X et Y de I, il existe un plus petit majorant x È Y et un plus grand minorant X Ç Y.
le treillis est complet c'est à dire qu'il existe un plus petit majorant de tout sous-ensemble (fini ou pas) de I.
cela implique également que l'on a un plus petit élément dans le treillis des intervalles qui correspond à un ensemble vide de valeurs (on le note ^) et que l'on a un plus grand élément (on le note T) qui correspond à tout R^N, c'est à dire que les variables peuvent prendre toutes les valeurs possibles.

4 Sémantique abstraite

4.1 Système d'équations sémantiques

On va écrire la sémantique d'un programme dans le domaine des intervalles, comme un système d'équations de point fixe (on indiquera comment le résoudre à la section 4.2) dans I, une équation par étiquette.

Commençons par l'affectation X=Expr. On a une valeur abstraite A Î I et on cherche à trouver la plus petite valeur abstraite B Î I vraie après cette affectation, dans un contexte validant A. On note B=[ [ X=Expr ] ] A: ce calcul peut se faire simplement par induction sur la syntaxe de Expr, en appliquant des règles de calcul simples sur les intervalles, à savoir, par exemple:

[a,b]+[c,d]=[a+b,c+d]
[a,b]*[c,d]=[min(a*c,a*d,b*c,b*d),max(a*c,a*d,b*c,b*d)]
(on peut trouver des formules légèrement plus économiques)

On passe maintenant aux tests. On veut pouvoir interpréter Test comme une approximation supérieure de l'élément de Ã( Rⁿ) tel que Test soit vrai sur ses points. On écrit cela [ [ Test ] ] A (où A l'environnement abstrait dans lequel on interprète le test). On interprète également Test de telle façon à avoir une approximation supérieure des valeurs pour lesquelles Test est faux dans l'environnement A. On représente cela par [ [ ¬ Test ] ] A. On peut calculer ces nouveaux intervalles (ou produits d'intervalles) par une «résolution de contraintes», s'effectuant également par induction sur la syntaxe de Test. Les étapes élémentaires sont:

supposons Testº Expr==0) (ou Expr>0, etc.), où l'arbre syntaxique représentant Expr commence par un noeud +, par exemple. On va résoudre récursivement des tests de la forme Expr Î [a,b]. Appelons les fils de Expr, X et Y respectivement. Alors résoudre X+Y Î [a,b] dans l'environnement A revient à essayer de raffiner [ [ X ] ] A (l'intervalle représentant la valeur de X dans l'environnement A) par la connaissance de la contrainte X+Y Î [a,b]. On pose donc X¹=[ [ X ] ] A Ç ([a,b]-[ [ Y ] ] A) et Y¹=[ [ Y ] ] A Ç ([a,b]-[ [ X ] ] A ) (on peut éventuellement itérer ce procédé et vérifier que l'on a atteint un point fixe), et le problème revient donc maintenant à résoudre les deux contraintes, dans l'environnement A: X Î X¹ et Y Î Y¹ (induction).
le cas terminal est celui où l'expression est une constante ou une variable:
- [ [ C Î [a,b] ] ] A vaut l'environnement abstrait ^ si C Ï[a,b] et A si C Î [a,b].
- [ [ x Î [a,b]] ] A vaut A où l'intervalle représentant la variable x dans A est remplacé par l'intervalle [a,b].
Pour [ [ ¬ Expr == 0 ] ] A, le principe est le même, si ce n'est que l'on résoud en même temps [ [ Expr Î [-¥,-1] ] ] A et [ [ Expr Î [1,¥] ] ] A, dont on fait l'union.

On considère maintenant l'instruction composée

(l) if Test then (l+1) Bloc₁ (l') else (l'+1) Bloc₂ (r) (r+1)

L'état abstrait en (l+1), que l'on écrit X_l+1 est X_l+1=[ [ Test ] ] X_l. Alors X_l'=[ [ Bloc₁ ] ] X_l+1, X_l'+1=[ [ ¬ Test ] ] A, X_r=[ [ Bloc₂ ] ] X_l'+1 and X_r+1=X_l' È X_r.

Les blocs d'instructions sont interprétés de façon itérative simple. Si Bloc=(l) Instr; (l+1) Bloc' (r) alors on pose X_l+1=[ [ Instr ] ] X_l et X_r=[ [ Bloc' ] ] X_l+1.

Enfin, pour les boucles while, du style (l) while (Test) (l+1) Bloc (r) (r+1), on a les équations suivantes:

X_l+1=[ [ Test ] ] (X_l È X_r),
X_r = [ [ Bloc ] ] X_l+1,
X_r+1=[ [ ¬ Test ] ] (X_l È X_r).

4.2 Résolution du système d'équations

Quand on a une fonction croissante f sur un treillis complet, on a au moins une solution à l'équation de point fixe x=f(x), en particulier on a une plus petite (lfp f) une plus grande (gfp f).

Si f est de plus continue lfp f=È_{i Î N} fⁱ(^), et c'est ce que l'on supposera ici. La fonction f ici est simplement la fonctionnelle de I^k vers I^k (k est le nombre d'étiquettes du programme) qui décrit le second membre du système d'équations construit à la section 4.1.

4.3 Exemple de calcul

Soit le programme,

(0) I=1;
 (1) while (I<=100)
  (2) I=I+1; (3)
(4)

La composante de fonctionelle associée à l'étiquette (2) est

f(X)=

(

[1,1] È (XÅ [1,1])

)

Ç [-¥,100]

Donc les itérés sont:

X⁰	=	^
X¹	=	[1,1]
X²	=	[1,2]
···
X¹⁰⁰	=	[1,100]
X¹⁰¹	= X¹⁰⁰

On a donc trouvé l'invariant de boucle I Î [1,100], puis on trouve le résultat du programme I=[101,101].

4.4 Elargissement/rétrécissement

Ce procédé de calcul de plus petit point fixe peut être extrèmement long; il peut même être infiniment long!

Il y a des moyens d'extrapoler les valeurs de l'union dans l'itération (ce que l'on fait généralement après un petit nombre d'itérations classiques, avec des unions), et ce de façon à ce que l'itération soit toujours finie. C'est ce que l'on appelle un élargissement. Par exemple, on a l'élargissement classique dans les intervalles:

[a₁,b₁] W [a₂,b₂] = [	si a₂ < a₁ alors -¥ sinon a₁,
	si b₂ > b₁ alors +¥ sinon b₁ ]

Donc les itérés pour f de la section 4.3 sont:

X⁰	=	^
X¹	=	[1,1]
X²	=	[1,+¥]
X³	=	X²

On a atteint une surapproximation du plus petit point fixe. Il y a en fait souvent moyen de «redescendre» en un temps fini vers un point fixe, éventuellement plus grand que le plus petit point fixe. Cela peut se faire en faisant des calculs itératifs de la fonctionnelle f, cette fois-ci en les combinant avec un opérateur de rétrécissement. Un rétrécissement classique dans les intervalles est:

[a₁,b₁] M [a₂,b₂] = [	si a₁=-¥ alors a₂ sinon min(a₁,a₂),
	si b₁=+¥ alors b₂ sinon max(b₁,b₂) ]

Les itérées successives sont donc maintenant:

Y⁰	=	X²
Y¹	=	[1,100]
Y²	=	Y¹

On a donc trouvé le même point fixe, cette fois-ci beaucoup plus rapidement.

5 Réalisation du projet

On commencera par écrire un petit parser des expressions du langage considéré. Ensuite, on écrira la représentation des éléments de I ainsi que les opérations élémentaires de treillis. Pour ce faire, on pourra compléter la liste des opérations comprises par l'analyseur, et donner les règles sémantiques adéquates.

Enfin, on fera un simple calcul de point fixe en parcourant (dans l'ordre d'exécution dans le cadre de ce projet) l'arbre généré par la phase d'analyse syntaxique.

On essaiera ensuite de programmer les phases d'élargissement et de rétrécissement; on pourra également proposer d'autres opérateurs d'élargissement et de rétrécissement.

Pour aller plus loin, il y a de nombreux aspects qui peuvent être creusés (on se reportera à la bibliographie pour avoir plus de détails et on pourra contacter E. Goubault pour tout renseignement supplémentaire), par exemple:

Comment améliorer la précision de l'analyse (avec ou sans assertions)? (par exemple en rajoutant une sémantique abstraite «arrière»)
Comment faire pour stocker plus efficacement les valeurs abstraites (moins de consommation mémoire)?
Comment analyser notre langage impératif, si on rajoute une notion de fonction, et d'appel de fonction?
etc.

References

[1]: P. Cousot and R. Cousot. Abstract interpretation: A unified lattice model for static analysis of programs by construction of approximations of fixed points. Principles of Programming Languages 4, pages 238--252, 1977.
[2]: P. Cousot and R. Cousot. Abstract interpretation frameworks. Journal of Logic and Computation, 2(4):511--547, August 1992.
[3]: D. A. Schmidt. Trace-based abstract interpretation of operational semantics, 1998.

This document was translated from L^AT_EX by H^EV^EA.