User Tools

  • Logged in as: anonymous (anonymous)
  • Logout

Site Tools


mantis:frama-c:ensiie2013-2014-ias-tp

Differences

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

Link to this comparison view

mantis:frama-c:ensiie2013-2014-ias-tp [2014/01/10 00:38] (current)
virgile created
Line 1: Line 1:
 +====== Analyse Statique de programmes - TP Frama-C ======
 +
 +ENSIIE 3ème année - année 2013/2014
 +
 +Enseignants : Virgile Prevosto et Julien Signoles
 +
 +10 janvier 2014
 +
 +===== Prise en main de Frama-C =====
 +
 +[[http://​frama-c.com|Frama-C]] est un outil d'​analyse de programmes C. Nous nous intéresserons dans
 +cette séance à son greffon d'​analyse de valeur par interprétation abstraite,
 +lancé avec l'​option =-val=. La version installée à l'​ENSIIE est [[http://​frama-c.com/​download_oxygen.html|Oxygen]]
 +
 +==== Premier exemple ====
 +
 +On s'​intéresse au fichier {{:​mantis:​frama-c:​ENSIIE-2013-2014:​exercice1.c|exercice1.c}}
 +<​code>​
 +int x,y, *z, *idx, a[101], t;
 +float f;
 +
 +int main (int c) {
 +
 +  if(0<= c && c<=9) z = &x; else z = &y;
 +
 +  if(c==5) x = 1; else x = 2;
 +
 +  switch (c) {
 +    case 0: y = 3; break;
 +    case 1: y = 42; break;
 +    case 2: y = 36; break;
 +    case 3: y = 25; break;
 +    case 4: y = 10; break;
 +    case 5: y = 100; break;
 +    case 6: y = 18; break;
 +    case 7: y = 75; break;
 +    case 8: y = 83; break;
 +    case 9: y = 98; break;
 +    default: y = 2; break;
 +  }
 +
 +  idx = &a[y];
 +    ​
 +  if (c) f = 1.5; else f = 0x1p-2;
 +  ​
 +  return y + *z;
 +
 +</​code>​
 +  - Lancer Frama-C de la manière suivante <​code>​frama-c -val exercice1.c</​code>​ et observer les résultats fournis par l'​analyse pour les différentes variables du programme.
 +  - Faire de même en utilisant l'​interface graphique avec la commande <​code>​frama-c-gui -val exemple1.c</​code>​
 +  - Insérer l'​instruction ''​Frama_C_show_each_res(c,​y,​z);''​ après le switch, et relancer l'​analyse de valeur. Qu'​observe-t-on?​ Plus généralement,​ ''​Frama_C_show_each_xxx(args)''​ demande à l'​analyse de valeur d'​afficher les valeurs abstraites de ''​args''​ chaque fois qu'​elle arrive à cette instruction.
 +  - l'​option ''​-slevel <​n>''​ permet de demander à l'​analyse de valeur de propager jusqu'​à ''​n''​ états distincts avant de commencer à faire des unions. Essayer différentes valeur de ''​n''​. Obtient-on une amélioration de la précision des résultats sur la valeur de retour? S'​agit-il du résultat le plus précis que l'on puisse obtenir? Sinon, d'où provient l'​imprécision?​
 +  - Il est possible (quand le ''​slevel''​ est suffisant) de forcer l'​analyse de valeur à séparer un état en utilisant une annotation logique [[http://​frama-c.com/​acsl.html|ACSL]] sous forme de disjonction. Par exemple <​code>/​*@ assert c<=0 || c > 0; */</​code>​ permettra d'​analyser séparément les cas où ''​c''​ est négatif et ceux où ''​c''​ est positif. En utilisant une telle assertion, améliorer la précision du résultat obtenu.
 +  - Une autre façon d'​améliorer la précision est d'​augmenter le nombre d'​éléments que peut contenir un ensemble avant d'​être transformé en intervalle: c'est l'​option ''​-val-ilevel''​ Essayer différentes valeurs pour l'​option,​ en conjonction ou non avec ''​-slevel''​. Quelle est la précision des résultats obtenus?
 +
 +==== Alarmes ====
 +
 +On considère le programme suivant (fichier {{:​mantis:​frama-c:​ENSIIE-2013-2014:​exercice2.c|exercice2.c}})
 +
 +<​code>​
 +  int main(int c) {
 +    int x, y, z[5];
 +  ​
 +    if(c) { x = c; } else { y = 4; }
 +  ​
 +    if(c) { y = x; } else { x = y; }
 +  ​
 +    z[0] = x;
 +
 +    z[1] = y;
 +
 +    return x/y;
 +  ​
 +  }
 +</​code>​
 +
 +  - En plus des options indiquées dans l'​exercice précédent,​ on utilise maintenant l'​option <​tt>​-val-signed-overflow-alarms</​tt>​ qui demande à l'​analyse de valeur de traiter les débordement arithmétiques lors
 +d'​opérations entre entiers signés comme des problèmes. Que dit l'​analyse de valeur sur ce code?
 +  - Les ''​warning''​ sont des *alarmes*: l'​analyse signale qu'il y a potentiellement un problème. Pour chacun d'​entre eux, vérifier s'il s'agit d'une fausse alarme ou d'un vrai problème. Le cas échéant, corriger le code.
 +  - À l'aide de ''​-slevel''​ et d'​éventuelles assertions, faire disparaître les fausses alarmes. ​
 +
 +Dans toute la suite, si une alarme est levée, on cherchera à la faire disparaître,​ soit en corrigeant le code si c'est un vrai bug, soit en
 +améliorant la précision de l'​analyse.
 +
 +==== Définition d'un contexte initial ====
 +
 +Dans les exercices précédents,​ ''​c''​ est considéré par l'​analyse de valeur comme
 +pouvant être n'​importe quel entier (entre ''​INT_MIN''​ et ''​INT_MAX''​). Il est
 +fréquent qu'on veuille mener une analyse dans un contexte plus restreint. On
 +considère le programme suivant (fichier {{:​mantis:​frama-c:​ENSIIE-2013-2014:​exercice3.c|exercice3.c}}):​
 +
 +<​code>​
 +int f(int x) {
 +  int S = 0;
 +  for (int i=0; i<=x; i++) {
 +    if (S>=i) S-=i; else S+=i;
 +  }
 +  return S;
 +}
 +
 +int main() {
 +  int x = 10;
 +  int res = f(x);
 +  return res;
 +}
 +</​code>​
 +
 +  - Que vaut ''​res''​ à la fin de la fonction ''​main''?​
 +  - On veut maintenant savoir ce que peut valoir ''​res''​ quand ''​x''​ est compris entre 10 et 100. Pour cela, on va utiliser les fonctions déclarées dans le fichier ''​builtin.h''​ situé dans le répertoire de données de Frama-C, qu'on peut obtenir par la commande <​code>​frama-c -print-share-path</​code>​ Des implantations sont disponibles dans le fichier ''​builtin.c'',​ situé au même endroit. Modifier la fonction ''​main''​ pour qu'​elle appelle ''​f''​ avec un argument compris entre 10 et 100. On utilisera l'​option <​code>​-cpp-extra-args="​-I$(frama-c -print-share-path)"</​code>​ pour indiquer au pré-processeur qu'il doit considérer le répertoire de frama-c lorsqu'​il cherche des fichiers à inclure.
 +  - Une autre possibilité consiste à lancer l'​analyse directement depuis ''​f'',​ avec l'​option ''​-main f'',​ en ajoutant un contrat [[http://​frama-c.com|ACSL]] à cette fonction qui va contraindre son argument. Par exemple <​code>/​*@ requires x == 10; */</​code>​ signale que ''​f''​ ne peut être appelée qu'​avec un argument valant 10. Utiliser cette nouvelle méthode pour retrouver le résultat de la question précédente.
 +
 +===== Portes =====
 +Cet exercice est tiré du [[http://​ww2.ac-poitiers.fr/​math/​spip.php?​article235|problème des 1000 portes]]. On considère le programme suivant (fichier {{:​mantis:​frama-c:​ENSIIE-2013-2014:​porte.c|porte.c}}):​
 +
 +<​code>​
 +#include "​builtin.h"​
 +
 +int portes[100];​
 +
 +int main() {
 +  int N = Frama_C_interval(2,​100);​
 +  for(int i = 1; i<= N; i++) {
 +    for(int j=i; j<=N; j+=i) portes[j-1] = 1 - portes[j-1];​
 +  }
 +}
 +</​code>​
 +
 +  - Vérifier qu'à la fin de la fonction, les seules cases pouvant contenir 1 ont un indice de la forme n²-1.
 +  - Comment modifier ce programme pour s'​assurer que les cases d'​indice n²-1 pour ''​n <= N''​ contiennent bien 1?
 +
 +===== Racine carrée =====
 +On s'​intéresse au programme suivant, donné dans le fichier {{:​mantis:​frama-c:​ENSIIE-2013-2014:​sqrt.c|sqrt.c}}:​
 +<​code>​
 +#define MAX_IDX 256
 +
 +extern double exp(double);​
 +
 +double args[MAX_IDX];​
 +double res[MAX_IDX];​
 +
 +void init () {
 +for(int i = -MAX_IDX+2; i<​=MAX_IDX;​ i+=2) {
 +  args[(MAX_IDX+i)/​2-1] = exp(i);
 +  res[(MAX_IDX+i)/​2-1] = exp(i/2);
 + }
 +}
 +
 +int main () {
 +  init();
 +  double x = 3.
 +  int i;
 +  double d;
 +  for (i = 0; i<​MAX_IDX && args[i] < x; i++);
 +  if (i==MAX_IDX) d = res[MAX_IDX];​
 +  else if (x-args[i] < args[i+1] - x) d = res[i];
 +  else d = res[i+1];
 +  for(int j = 0; j < 4; j++) {
 +    d = (d + x/d) / 2.;
 +  }
 +  return 0;
 +}
 +</​code>​
 +
 +La fonction ''​exp''​ n'est pas définie, mais l'​analyse de valeur
 +dispose d'un built-in nommé ''​Frama_C_exp'',​ activable avec l'​option
 +''​-val-builtin exp:​Frama_C_exp''​
 +
 +  - Quelle est la valeur finale trouvée pour =d=?
 +  - On cherche maintenant à voir l'​intervalle calculé pour ''​d''​ quand ''​x''​ est un flottant compris entre ''​0x1p-256''​ et ''​0x1p256''​. Quel résultat donne l'​analyse de valeur?
 +  - On ajoute maintenant au programme un prototype ''​sqrt''​ <​code>​double sqrt(double);</​code>​ Là encore, l'​analyse de valeur dispose d'un built-in, nommé ''​Frama_C_sqrt''​ qui calcule le résultat attendu. Modifier ''​main''​ pour assigner dans une variable locale l'​erreur relative entre ''​d''​ et ''​sqrt(x)''​. Quelle est l'​intervalle calculé par l'​analyse de valeur pour cette variable?
 +  - Améliorer la précision de l'​analyse de valeur sur le calcul de l'​erreur relative en utilisant une assertion ACSL qui découpe l'​intervalle de valeurs de ''​x''​ en sous-intervalles
 +
 +===== Deviner un nombre =====
 +
 +On considère la fonction suivante (fichier {{:​mantis:​frama-c:​ENSIIE-2013-2014:​devin.c|devin.c}}):​
 +<​code>​
 +#include "​builtin.h"​
 +
 +int devine(int secret, int max) {
 +  int tentative = max / 2, inf = 0, sup = max, nb = 1;
 +  while(tentative != secret) {
 +    nb++;
 +    if (tentative < secret) inf = tentative+1;​
 +    if (tentative > secret) sup = tentative-1;​
 +    tentative = (inf+sup) / 2;
 +  }
 +  return nb;
 +}
 +</​code>​
 +
 +  - ''​devine''​ ne peut terminer que si ''​secret''​ est dans un intervalle particulier. Écrire le contrat correspondant.
 +  - Écrire une fonction ''​main''​ qui appelle ''​devine''​ avec ''​secret''​ compris entre 0 et 100
 +  - Quelles sont alors les valeurs que peut retourner ''​devine''?​
 +  - Mêmes questions (en utilisant l'​option ''​-val-signed-overflow-alarms''​),​ si ''​secret''​ est compris entre ''​INT_MAX-5000''​ et ''​INT_MAX''​. On rappelle que ''​INT_MAX''​ est défini dans le fichier ''​limits.h''​.
 +
 +===== Somme d'​entiers =====
 +
 +On s'​intéresse dans cet exercice au premier problème du [[https://​projecteuler.net/​problem%3D1|Projet Euler]]: trouver
 +la somme des entiers inférieurs à 1000 qui sont multiples de 3 ou multiples
 +de 5. Une implantation est proposée dans le fichier {{:​mantis:​frama-c:​ENSIIE-2013-2014:​euler1.c|euler1.c}}:​
 +
 +<​code>​
 +int total = 0;
 +
 +void add(int max, int x) { total += x; }
 +
 +void sum(int max) {
 +  int i=1;
 +  while ( i <= max / 3) {
 +    add(max,​3*i);​
 +    if (i%3 !=0) add(max, 5*i);
 +    i++;
 +  }
 +}
 +
 +int main() {
 +  sum(1000);
 +  return total;
 +}
 +</​code>​
 +
 +  - Utiliser Frama-C pour trouver la valeur de ''​total''​ à la fin de la fonction ''​main''​
 +  - On veut maintenant utiliser l'​analyse de valeur pour vérifier certaines propriétés du programme. Donner un contrat pour la fonction ''​add''​ qui vérifie que l'​argument ''​x''​ fait bien partie des entiers qu'il faut additionner. Utiliser l'​analyse de valeur pour voir si ''​sum''​ appelle ''​add''​ conformément à son contrat. Le cas échéant, corriger le code. On pourra utiliser des disjonction et ''​-slevel''​ pour séparer différents états.
 +  - Reprendre la question précédente dans le cas où l'​argument donné à ''​sum''​ est un entier quelconque entre 1 et 1000
  
mantis/frama-c/ensiie2013-2014-ias-tp.txt · Last modified: 2014/01/10 00:38 by virgile