Glu: environnements abstraits, généralités et pointeurs (projet no. 5)

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.

Il est demandé en premier d'écrire les unions, élargissements, top et tests d'égalité entre valeurs abstraites, puis entre environnements abstraits.

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 5 (glue.ml) consiste à définir les sémantiques abstraites en terme d'effets abstraits des instructions x:=y (ae_assign), x:=a où a est déclaré comme tableau (ae_set_array; on pourra utiliser Zones.z_array), x:=f où f est un nom de fonction (ae_set_fun; on pourra utiliser Zones.z_fun), x:=constante (ae_set_cst), *x:=*y (ae_copy), x:=*y (ae_ptr), *x=y (ae_set_ptr), x=&y (ae_addr_var; on pourra utiliser Zones.z_addr_var), x=&a[i] (ae_addr_index), x=y-z où y et z sont deux pointeurs du même type (ae_anti_addr_index), x=&y->f (ae_addr_sel), x=(type)y (ae_convert; il s'agit de conversion de type; cf. control.ml et le commentaire sur I_CONVERT en particulier), x=(type)y (ae_cast; il s'agit d'un cast, sans conversion; cf. control.ml et le commentaire sur I_CONVERT en particulier). N'oubliez pas d'aller chercher les fonctions dont vous avez besoin dans les projets précédents.

On demande aussi de coder deux fonctions supplémentaires:

ae_value récupère la valeur abstraite d'une variable passée en argument;
ae_wipe, appliqué à un environnement abstrait ae et à une adresse abstraite a, calcule l'environnement abstrait obtenu à partir de ae lorsqu'on passe à top toutes les variables dont les adresses rencontrent a. ae_wipe est utilisé par Analyseur.analyseur pour prendre en compte les effets de bords sur des alias des variables dans ae.

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.

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