Glu: environnements abstraits, opérations arithmétiques et logiques (projet no. 6)
L'analyseur va manipuler des valeurs abstraites, de type
abs_value (cf. glue.mli). Elles peuvent être
soit des intervalles d'entiers (cf. les projets 1 et
2), soit des intervalles flottants (cf. le projet
3), soit des adresses abstraites (cf. le projet
4).
À l'aide des valeurs abstraites, le fichier glue.mli
définit ensuite des environnements abstraits abs_env, qui sont
essentiellement des tables associant des valeurs abstraites à chaque
variable. La représentation réelle des abs_env est légèrement
différente pour des raisons pratiques: comme chaque variable est un couple
(x, glob) où x est une chaîne et glob est vrai s'il s'agit d'une
variable globale, faux sinon, on découpe les abs_env en un produit de
deux tables envoyant des chaînes x vers leurs valeurs abstraites; la
première table est la table des variables globales, la seconde celle des
variables locales.
Maintenant, la sémantique d'une instruction instr en C ne consiste pas
juste à passer d'un environnement abstrait avant l'instruction ae à un
environnement abstrait après ae'. L'analyseur (dans
analyseur.ml) a besoin de savoir, en plus de
l'environnement abstrait ae' après l'instruction instr:
-
l'ensemble des adresses sur lesquels instr a fait des effets de bord.
Par exemple, l'instruction
*to++ = *from++ effectue des effets de
bord sur l'adresse [a, a+3] (dans une architecture 32 bits, avec to,
from de type pointeur vers int), avec a l'adresse de to
avant l'instruction, mais aussi sur [&to, &to+3] et sur
[&from, &from+3] (incrémentations des variables to
et from). Cet ensemble d'adresses sera codé par une adresse
abstraite a, de type abs_addr;
- l'ensemble sigs des signaux possibles lancés par l'exécution de
l'instruction instr. Les structures servant à représenter les
ensembles de signaux sont en
sigs.ml; essentiellement,
les seuls signaux possibles sont sig_segv pour tout accès mémoire
illégal, et sig_fpe pour les erreurs arithmétiques (même, et en
fait uniquement, en arithmétique entière).
Les triplets (ae', a, sigs) forme un effet abstrait, de type
abs_effect. Le but des projets de glu (5 et 6) est de définir les
effets abstraits de chacune des instructions élémentaires que l'on peut
retrouver sur un graphe de contrôle; voir
control.mli et en particulier le type instr
pour savoir quelles sont les instructions possibles.
Le projet 6 (glue_log.ml) consiste à définir les sémantiques
abstraites en terme d'effets abstraits des instructions arithmétiques et
logiques x:=~y (ae_bnot), x:=-y (ae_minus),
x:=y*z (ae_mul), x:=y/z (ae_div), x:=y%z
(ae_mod), x:=y+z (ae_add), x:=y<<z
(ae_left), x:=y>>z (ae_right), x:=y&z
(ae_and), x:=y^z (ae_xor), x:=y|z (ae_or),
x:=(y==z) (ae_eq), x:=(y<=z) (ae_le),
x:=(y<z) (ae_lt). On demande aussi de coder ae_test_true,
ae_test_false qui testent si une valeur abstraite est possiblement
vraie (entière non nulle), resp. possiblement fausse (entière nulle).
N'oubliez pas d'aller chercher les fonctions dont vous avez besoin dans les
projets précédents.
La plupart de ces fonctions prennent en argument une chaîne func, le
nom de la fonction courante, et un loc_ppoint option ctx; ceci sert
à définir la zone mémoire où sont stockées les variables locales.
Elles prennent aussi en argument un abs_env ae qui est
l'environnement avant l'exécution de l'instruction considérée.
This document was translated from LATEX by
HEVEA.