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,

On se reportera à la section 4.3 pour un exemple.

3   Domaine des intervalles

On suppose ici que Var={x1,···,xN}. On appelle domaine des intervalles
I = { [a1,b1]× ... × [aN,bN] | ai, bi Î Z È {-¥,+¥} }

Le domaine des intervalles abstrait les valeurs que peuvent prendre les variables de Var (considérées comme un élément de ZN), de manière évidente: soit
a: Ã( ZN) ® I
avec a(S)=[min p1(S),max p2(S)] × ... × [min pN(S),max pN(S)] où pi: ZN ® 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 ZN 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,

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: On passe maintenant aux tests. On veut pouvoir interpréter Test comme une approximation supérieure de l'élément de Ã( Rn) 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: On considère maintenant l'instruction composée
(l) if Test then (l+1) Bloc1 (l') else (l'+1) Bloc2 (r) (r+1)
L'état abstrait en (l+1), que l'on écrit Xl+1 est Xl+1=[ [ Test ] ] Xl. Alors Xl'=[ [ Bloc1 ] ] Xl+1, Xl'+1=[ [ ¬ Test ] ] A, Xr=[ [ Bloc2 ] ] Xl'+1 and Xr+1=Xl' È Xr.

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 Xl+1=[ [ Instr ] ] Xl et Xr=[ [ Bloc' ] ] Xl+1.

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

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 fi(^), et c'est ce que l'on supposera ici. La fonction f ici est simplement la fonctionnelle de Ik vers Ik (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:
X0 = ^
X1 = [1,1]
X2 = [1,2]
···
X100 = [1,100]
X101 = X100

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:

[a1,b1] W [a2,b2] = [ si a2 < a1 alors -¥ sinon a1,
  si b2 > b1 alors +¥ sinon b1 ]

Donc les itérés pour f de la section 4.3 sont:
X0 = ^
X1 = [1,1]
X2 = [1,+¥]
X3 = X2

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:
[a1,b1] M [a2,b2] = [ si a1=-¥ alors a2 sinon min(a1,a2),
  si b1=+¥ alors b2 sinon max(b1,b2) ]

Les itérées successives sont donc maintenant:
Y0 = X2
Y1 = [1,100]
Y2 = Y1

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:

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 LATEX by HEVEA.