SYSTEM WARNING: 'session_name(): Cannot change session name when session is active' in '/home/gitlab-www/dokuwiki/inc/init.php' line 231

SYSTEM WARNING: 'session_set_cookie_params(): Cannot change session cookie parameters when session is active' in '/home/gitlab-www/dokuwiki/inc/init.php' line 232

mantis:frama-c:ensiie2016-2017-ias-tp [Frama-C]

User Tools

  • Logged in as: anonymous (anonymous)
  • Log Out

Site Tools


mantis:frama-c:ensiie2016-2017-ias-tp

Differences

This shows you the differences between two versions of the page.

Link to this comparison view

mantis:frama-c:ensiie2016-2017-ias-tp [2017/01/02 16:20] (current)
virgile énoncé TP
Line 1: Line 1:
 +====== Analyse Statique de Programmes -- TP Frama-C ======
 +
 +ENSIIE 3ème année -- année scolaire 2016/2017 Enseignants:​ Tristan Le Gall et Virgile Prevosto
 +
 +3 janvier 2017
 +
 +===== Exercice 1: =====
 +
 +On considère le programme suivant, également disponible dans le fichier {{mantis:​frama-c:​ensiie-2016-2017:​string.c|string.c}}
 +
 +<code c>
 +int f(char* dest, int len, const char* src) {
 +  int i = 0;
 +  while (src[i] != 0 && src[i] != ' ' && i < len) {
 +    dest[i] = src[i];
 +    i++;
 +  }
 +  dest[i] = 0;
 +  return i-1;
 +}
 +
 +int main() {
 +  const char* test[] = "​Example of character string";​
 +  char result1[10],​ result2[10];​
 +  int res = f(result1, 9, test);
 +  f(result2, 9, test + res + 1);
 +  return 0;
 +}
 +</​code>​
 +  - Lancer l'​analyse de valeur sur ce programme, à l'aide de la commande ''​%%frama-c -val string.c%%''​. Qu'​observe-t-on pour les valeurs possibles des éléments des tableaux ''​%%result1%%''​ et ''​%%result2%%''?​
 +  - Même question en utilisant l'​interface graphique (''​%%frama-c-gui -val string.c%%''​)
 +  - Insérer des appels à la famille de fonctions built-in ''​%%Frama_C_show_each_*%%''​ pour étudier l'​évolution des valeurs de ''​%%i%%'',​ ''​%%dest%%'',​ ''​%%src%%''​ et ''​%%dest[i]%%''​ lors du calcul du point fixe pour la boucle de la fonction ''​%%f%%''​. On rappelle qu'une fonction dont le nom commence par ''​%%Frama_C_show_each_%%''​ peut prendre un nombre arbitraire d'​arguments,​ dont l'​évaluation dans l'​état courant de l'​analyse de valeur sera affiché sur la sortie standard chaque fois que l'​analyse atteint ce point.
 +  - Une première possibilité d'​amélioration des résultats consiste à utiliser l'​option ''​%%-wlevel%%'',​ qui modifie le moment où le widening se déclenche. Observer ce qui se passe si on utilise ''​%%-wlevel 10%%''​
 +  - Une seconde possibilité consiste à dérouler syntaxiquement certaines boucles. Pour cela, on utilise l'​annotation ''​%%/​*@ loop pragma UNROLL n; */​%%''​ où ''​%%n%%''​ est un entier au-dessus de la boucle qu'on veut dérouler. Dérouler 10 fois la boucle de la fonction ''​%%f%%''​ interne. Qu'​observe-t-on?​
 +  - La méthode privilégiée d'​amélioration des résultats de l'​analyse de valeur est l'​option ''​%%-slevel%%''​ qui autorise l'​analyse à propager un certain nombre d'​états distincts par instruction avant de faire l'​union. Qu'​obtient-on comme résultat avec ''​%%-slevel 20%%''?​
 +  - Que calcule ce programme?
 +
 +===== Exercice 2: Contexte d'​exécution =====
 +
 +On reprend le programme de l'​exercice précédent. On va désormais s'​intéresser à ce qui se passe si la chaîne ''​%%test%%''​ initiale contient 99 caractères arbitraires (et le ''​%%0%%''​ terminal).
 +
 +  - En utilisant la fonction ''​%%Frama_C_interval%%''​ déclarée dans l'​en-tête ''​%%__fc_builtin.h%%''​ fourni avec Frama-C, définir une fonction ''​%%void init(char* s, int length)%%''​ qui remplit le bloc pointé par ''​%%s%%''​ avec des caractères non nuls arbitraires et un ''​%%0%%''​ terminal.
 +  - Modifier la fonction ''​%%main%%''​ pour que ''​%%test%%''​ ait un contenu arbitraire tel qu'​indiqué en début d'​énoncé.
 +  - Lancer Value Analysis (en jouant éventuellement avec les paramètres de précision) sur cette nouvelle fonction ''​%%main%%''​. Que constate-t-on?​
 +  - Après avoir corrigé le cas échéant la fonction ''​%%f%%'',​ relancer Value Analysis. D'où provient l'​alarme résiduelle?​ Modifier ''​%%init%%''​ pour que le contenu initial de ''​%%test%%''​ ne risque pas de provoquer d'​erreur à l'​exécution,​ et relancer Value Analysis pour le confirmer.
 +
 +===== Exercice 3: Fonction de Bessel =====
 +
 +On s'​intéresse au fichier {{mantis:​frama-c:​ensiie-2016-2017:​bessel.c|bessel.c}} de la ''​%%dietlibc%%'',​ une implantation minimaliste de bibliothèque système (https://​www.fefe.de/​dietlibc/​). Plus précisément,​ on cherche à déterminer la sensibilité de la fonction ''​%%j0%%''​ à une incertitude sur son argument.
 +
 +  - Écrire une fonction ''​%%main%%''​ qui calcule ''​%%j0(3)%%''​ et la différence entre ce résultat et ''​%%j0(x)%%''​ où ''​%%x%%''​ est dans l'​intervalle ''​%%[3-0.125,​3+0.125]%%''​
 +  - Utiliser Value Analysis pour vérifier que la variation du résultat de ''​%%j0%%''​ autour de ''​%%3%%''​ reste faible.
 +
 +===== Exercice 4: Fonction crypt =====
 +
 +On s'​intéresse désormais à la fonction ''​%%crypt%%''​ de la ''​%%dietlibc%%'',​ dont l'​implantation est fournie dans le fichier {{mantis:​frama-c:​ensiie-2016-2017:​crypt.c|crypt.c}}
 +
 +  - À l'aide de ''​%%man%%'',​ retrouver le comportement attendu de la fonction
 +  - En déduire une fonction ''​%%init%%''​ qui préparera un contexte d'​analyse de ''​%%crypt%%''​ pour un mot de passe de 29 caractères ASCII arbitraires.
 +  - À l'aide de l'​analyse de valeur, vérifier que le chiffrement d'un tel mot de passe ne peut pas conduire à une erreur à l'​exécution.
 +  - Observer le contenu du buffer contenant le mot de passe chiffré à la fin de l'​exécution de ''​%%crypt%%''​. Que peut-on en dire?
 +
 +===== Exercice 5: Chaînes dynamiques =====
 +
 +On s'​intéresse à la bibliothèque ''​%%sds%%''​ (http://​github.com/​antirez/​sds),​ qui se présente sous la forme d'un fichier en-tête sds.h et d'un fichier d'​implantation {{mantis:​frama-c:​ensiie-2016-2017:​sds.c|sds.c}}. On va chercher à vérifier que la concaténation de deux ''​%%sds%%''​ obtenues à partir de chaînes C standard de 50 caractères (quelconques) ne peut provoquer d'​erreur à l'​exécution.
 +
 +  - Écrire la fonction d'​initialisation du contexte et la fonction ''​%%main%%''​ correspondante.
 +  - Lancer Value Analysis. Que constate-t-on?​
 +  - Fournir une implantation naïve de ''​%%malloc%%''​ qui utilise deux tableaux ''​%%char __alloc[SIZE_MAX]%%''​ où seront faites les allocations et ''​%%size_t __alloc_size[SIZE_MAX]%%''​ qui stocke à chaque indice où une allocation a lieu la taille du bloc alloué. Relancer l'​analyse de valeur avec cette implantation. Obtient-on de meilleurs résultats?
 +  - Fournir les implantations des fonctions de la bibliothèque standard manquantes et vérifier qu'il n'y a effectivement pas d'​erreur à l'​exécution possible.
 +
 +===== Exercice 6: Compression de petites chaînes =====
 +
 +On s'​intéresse maintenant à la bibliothèque [[https://​github.com/​antirez/​smaz|smaz]],​ qui propose une fonction de compression optimisée pour les courtes chaînes ASCII. On partira de la fonction de test ''​%%main%%''​ du fichier ''​%%smaz_test.c%%''​. Le code est disponible dans cette {{mantis:​frama-c:​ensiie-2016-2017:​smaz.zip|archive}}.
 +
 +  - ''​%%smaz%%''​ utilise des fonctions de la bibliothèque standard C pour lesquelles il faut fournir une implantation que Value Analysis puisse analyser. Écrire une telle implantation pour ''​%%strlen%%''​.
 +  - Supprimer de ''​%%main%%''​ la partie qui teste la compression d'une chaîne aléatoire (on s'y intéressera dans un second temps), et utiliser Value Analysis pour vérifier qu'​aucune erreur à l'​exécution n'est possible pendant la compression et la décompression des chaînes données en exemple. Le cas échéant, fournir des implantations pour les fonctions de la bibliothèque standard utiles.
 +  - Modifier ''​%%main%%''​ pour vérifier que la compression et la décompression d'une chaîne aléatoire de longueur au plus 50 ne risque pas de provoquer d'​erreur à l'​exécution
 +
  
mantis/frama-c/ensiie2016-2017-ias-tp.txt · Last modified: 2017/01/02 16:20 by virgile