Fonctions de bibliothèque (projet no. 7)
L'analyseur, décrit dans analyseur.ml, ne
connaît pas le source des fonctions de la bibliothèque standard, comme
malloc, free, exit, etc. Il arrive donc que l'analyseur
cherche à analyser l'appel d'une fonction comme malloc dont il ne
connaît pas le source. Dans ce cas, l'analyseur cherche dans la table
external_functions un morceau de code OCaml qui saura l'informer de ce
que calcule la fonction inconnue appelée.
Le but de ce projet est d'écrire quelques-unes des descriptions des
fonctions de la bibliothèque C, à commencer par les fonctions d'allocation
mémoire. Un exemple de code est fourni pour malloc dans
api.ml. On notera qu'il s'agit essentiellement d'ecrire
une fonction (fun vt ft ...) que l'on rajoute a la table
external_functions en utilisant Hashtbl.add, une fonction de la
bibliothèque standard OCaml.
Avant de commencer, on attire l'attention sur le fait que les treillis
abstraits utilisés dans Csur sont décrits dans les projets
2, 3, et 4.
Il est aussi recommandé de comprendre comment sont représentés les
environnements abstraits, cf. le projet 5.
Une fonction externe abstraite prend un nombre relativement grand de
paramètres en entrée, dont voici une description (cf.
analyseur.mli):
-
vt, de type var_table, est une table qui à chaque
variable globale (une chaîne de caractères) associe des informations
sur cette variable: essentiellement l'endroit où cette variable est
déclarée et son type, cf. control.ml; ceci sera
normalement d'une utilité limitée;
-
ft, de type fun_table, est une table qui à chaque nom de
fonction (une chaîne de caractères) associe tout ce qu'on a à
savoir sur cette fonction, et notamment son graphe de contrôle complet,
cf. control.ml; ce sera cependant d'une utilité
limitée dans ce projet;
-
info, de type abs_info, est la structure associant à
chaque point de programme l'environnement abstrait calculé par
l'analyseur. C'est donc le résultat essentiel retourné par l'analyseur.
Au lieu d'être codé comme une (ppoint, abs_env) Hashtbl.t, il est
défini comme une (loc_ppoint option, (loc_ppoint, abs_env)
Hashtbl.t) Hashtbl.t, en utilisant le fait que
ppoint=loc_ppoint option * loc_ppoint (cf.
control.ml); ceci permet une meilleure efficacité
à certains endroits de l'analyseur; il est peu probable que vous ayez à
mettre info à jour;
-
finfo, de type function_info, sert à l'analyseur à
conserver des informations sur les fonctions appelées, d'un appel à
l'autre; cf. analyseur.mli; il est peu probable
que vous ayez à mettre à jour cette structure;
-
sinfo, de type sig_info, est utilisé par l'analyseur
pour retourner les ensembles de signaux possiblement lancés par le
programme à chaque point de programme; ceci ressemble en un sens à
info, et encore une fois il est peu probable que vous ayez à mettre
cette table à jour;
-
notfound, de type functions_not_found, est utilisé par
l'analyseur pour retourner l'ensemble des fonctions dont il n'a pas trouvé
de définition (toutes les fonctions dont on n'a pas le source et pour
lesquelles le projet courant n'a pas fourni de définition); vous n'aurez
pas à mettre cette table à jour;
-
heapsizes, de type heap_size_info, enregistre pour chaque
point de programme où malloc est appelé un intervalle entier de
toutes les tailles possibles de blocs alloués à ce point de programme.
Ceci sert notamment à détecter ultérieurement les erreurs d'accès
par pointeurs à des adresses débordant de ces blocs; noter que,
naturellement, le code pour malloc dans api.ml
renseigne cette table;
-
cctx, de type CallContext.t, est l'ensemble des noms de
fonctions dans la pile au-dessus du point de programme courant; ceci sert
à l'analyseur à décider quand opérer des élargissements au niveau
interprocédural (détection des appels récursifs); vous n'aurez pas a
priori à vous occuper de cctx;
-
pp, de type ppoint (cf.
control.ml), est le point de programme courant,
celui où l'on trouve l'appel à la fonction de bibliothèque que l'on
cherche à analyser; il s'agit d'une donnée importante pour certaines
fonctions de bibliothèque, comme malloc;
-
globs, de type abs_value AbsEnv.t, est un(e moitié d')
environnement abstrait, correspondant aux valeurs des variables globales
(les fonctions appelées ne voyant pas les variables locales de leur
fonction appelante); cf. le projet 5 pour une description
des environnements abstraits;
-
args, de type abs_value list, est la liste des valeurs
abstraites des arguments passés à la fonction appelée. Consulter le
code pour malloc pour voir comment on récupère les valeurs des
arguments dans api.ml;
-
restype, de type Cparse.q_ctype, est le type de retour de
la fonction appelée.
À partir de ces informations, et notamment de heapsizes, pp,
args, les fonctions abstraites de ce projet doivent retourner un
abs_call_effect (cf. analyseur.mli).
Consulter aussi l'exemple du code pour malloc dans
api.ml.
La fonction free
Tout d'abord, l'argument de free est censé être un pointeur p.
On considérera que si p pointe vers autre chose que le début (offset
nul) d'un bloc Z_HEAP, alors free peut faire n'importe quel
effet de bord (None). La troisième composante de
l'abs_call_effect à retourner doit en tenir compte. Si p est
nécessairement l'adresse de début d'un bloc Z_HEAP, cette
troisième composante doit contenir toutes les adresses allant de p à
p+N-1, où N est la taille du bloc (utiliser heapsizes).
D'autre part, free peut toujours lancer le signal sig_segv
(segmentation violation), même lorsque free est appelé sur un
pointeur vers le début d'un bloc Z_HEAP: la raison est que ce bloc a
pu être déjà libéré précédemment. (Note: comment pourrait-on
raffiner l'approche pour détecter ce cas?)
La fonction calloc
Cette fonction ressemble beaucoup à malloc. Les deux différences
sont que, d'une part, calloc(n, size) alloue une zone mémoire de
taille n × size, d'autre part calloc met à zéro la zone
ainsi allouée. Les arguments n et size sont de type size_t, que
l'on estimera à être unsigned long.
Si vous le pouvez, codez aussi de la même façon la fonction
realloc.
La fonction strlen
Elle prend un pointeur vers char, censé dénoter une chaîne C,
et retourne sa longueur sous forme d'un unsigned long. La longueur
d'une chaîne C est le nombre de caractères avant le premier caractère
nul. Noter qu'en général on ne peut pas même pas garantir qu'on finira
par trouver un caractère nul dans le bloc pointé. Comment peut-on faire
pour améliorer l'analyse?
Si vous le pouvez, codez aussi les fonctions strcpy et strncpy.
La fonction log
La fonction log calcule le logarithme népérien du flottant en argument.
Si l'argument est nul, log retourne moins infini et met la variable
globale errno de type int à Const.erange. Si
l'argument est négatif, log retourne un NaN (cf. le projet
3) et met errno à Const.edom. Sinon,
errno reste inchangé. En particulier, log ne met pas
errno à 0.
Si vous le pouvez, codez aussi les fonctions exp, pow,
sqrt, sin, cos, tan, asin, acos,
atan, atan2.
This document was translated from LATEX by
HEVEA.