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

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 Oxygen

Premier exemple

On s’intéresse au fichier exercice1.c

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;
}
  1. Lancer Frama-C de la manière suivante frama-c -val exercice1.c et observer les résultats fournis par l’analyse pour les différentes variables du programme.
  2. Faire de même en utilisant l’interface graphique avec la commande frama-c-gui -val exemple1.c
  3. 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.
  4. 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?
  5. Il est possible (quand le slevel est suffisant) de forcer l’analyse de valeur à séparer un état en utilisant une annotation logique ACSL sous forme de disjonction. Par exemple /*@ assert c<=0 || c > 0; */ 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.
  6. 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 exercice2.c)

  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;
  
  }
  1. 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?

  1. 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.
  2. À 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 exercice3.c):

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;
}
  1. Que vaut res à la fin de la fonction main?
  2. 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 frama-c -print-share-path 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
    1. On utilisera l’option -cpp-extra-args="-I$(frama-c -print-share-path)" pour indiquer au pré-processeur qu’il doit considérer le répertoire de frama-c lorsqu’il cherche des fichiers à inclure.
  3. Une autre possibilité consiste à lancer l’analyse directement depuis f, avec l’option -main f, en ajoutant un contrat ACSL à cette fonction qui va contraindre son argument. Par exemple /*@ requires x == 10; */ 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 problème des 1000 portes. On considère le programme suivant (fichier porte.c):

#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];
  }
}
  1. Vérifier qu’à la fin de la fonction, les seules cases pouvant contenir 1 ont un indice de la forme n²-1.
  2. 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 sqrt.c:

#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;
}

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

  1. Quelle est la valeur finale trouvée pour =d=?
  2. 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?
  3. On ajoute maintenant au programme un prototype sqrt double sqrt(double); 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?
  4. 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 devin.c):

#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;
}
  1. devine ne peut terminer que si secret est dans un intervalle particulier. Écrire le contrat correspondant.
  2. Écrire une fonction main qui appelle devine avec secret compris entre 0 et 100
  3. Quelles sont alors les valeurs que peut retourner devine?
  4. 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 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 euler1.c:

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;
}
  1. Utiliser Frama-C pour trouver la valeur de total à la fin de la fonction main
  2. 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.
  3. Reprendre la question précédente dans le cas où l’argument donné à sum est un entier quelconque entre 1 et 1000