Zones mémoire et pointeurs (projet no. 4)

Le langage C permet la manipulation de pointeurs, autrement dit d'adresses en mémoire. Au lieu d'abstraire les adresses, qui ne sont jamais que des entiers sur un certain nombre de bits, par un domaine abstrait numérique comme par exemple celui des intervalles d'entiers, on va utiliser un type specifique d'adresses abstraites, qui seront symboliques.

Les symboles utilisés dans cette représentation sont appelées les zones (le type zone de zones.mli). Les zones possibles sont:

Z_NULL, qui représente le pointeur NULL de C;
Z_GLOBAL (x, [m,n]), qui représente l'adresse de la variable globale x. L'intervalle entier [m,n] encadre la taille de la zone mémoire allouée à x. Par exemple, sur une machine 32 bits, la zone correspondant à int toto sera Z_GLOBAL ("toto", [4,4]), celle allouée à char titi[200] sera Z_GLOBAL ("titi", [200,200]), celle allouée à extern char sys_errlist[] sera Z_GLOBAL ("sys_errlist", [0,Arith.type_long.it_max]);
Z_STACK (x, [m,n], f, ctx), qui représente les adresses possibles de la variable locale x, déclarée dans la fonction f, lorsque f est appelée depuis le point de programme (optionnel) ctx. (ctx vaut None si f n'est appelée de nulle part dans le source du programme, ce qui arrive notamment si f=main.) L'intervalle [m,n] est un encadrement de la taille de x, comme dans le cas des variables globales;
Z_HEAP (pp) représente les adresses de blocs alloués en mémoire au point de programme pp. La taille du bloc n'y est pas stockée. Les points de programmes pp sont de type ppoint, définis dans control.ml. En d'autres mots, on trouvera typiquement au point de programme pp une instruction malloc (...), responsable de l'allocation de ce bloc.
Z_STRING (s) représente l'adresse de la constante chaîne s. On suppose que même si la chaîne s est écrite plusieurs fois dans le source, elle est toujours placée à la même adresse; autrement dit, que "abc"=="abc" retourne 1. Toute écriture dans une telle zone échoue, et déclenche le signal sig_segv (cf. const.ml).
Z_FUN (f) représente l'adresse du code machine de la fonction de nom f; la taille du code de f est inconnue. Toute écriture dans une telle zone échoue, et déclenche le signal sig_segv (cf. const.ml).

Dans tous les cas, on supposera que la lecture ou l'écriture en-dehors d'une zone est illégale, et déclenche le signal sig_segv (cf. const.ml).

Maintenant, une adresse abstraite, de type OCaml abs_addr, est soit None, qui est le top du treillis des adresses abstraites (on ne sait plus vers quoi ce pointeur pointe du tout), soit Some (zt), où zt est de type itv ZoneTable.t. Autrement dit, zt est une table qui à des zones associe des intervalles entiers (non vides), représentant toutes les zones possibles vers lesquelles peut pointer le pointeur, avec les décalages possibles de ces pointeurs par rapport au début de la zone. Par exemple, si on écrit:

int glob;

int f (int n) {
  int *p, *q;

  p = malloc (42);
  if (n>=2)
    q = p+3;
  else q = &glob;
}

alors à la sortie de f, la valeur de q sera l'adresse abstraite Some (Z_HEAP (pp) |® [12,12],

Z_GLOBAL

("glob", [4,4]) |® [0,0]) (en supposant que la taille des int et des pointeurs est de 4 octets). On appellera les décalages possibles des pointeurs par rapport aux débuts de zones les offsets, ils sont supposés être de type long (cf. Arith.type_long).

On demande maintenant d'écrire les définitions de z_bot, z_make, etc., comme décrits dans zones.mli. Consulter les commentaires dans ce fichier pour les détails.

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