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): À 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.