ENSIIE 3ème année - année 2010/2011

Enseignants : Virgile Prevosto et Julien Signoles

14 janvier 2011

Le but de ce TP est d'utiliser l'outil Frama-C et en particulier son greffon d'analyse de valeur. La version installée à l'ENSIIE est Beryllium-20090902.

Frama-C est fondé sur un ensemble de greffons proposant chacun un type d'analyse particulier. La liste des greffons disponibles peut être obtenue par frama-c -help. De même, les options permettant de piloter le noyau s'obtiennent avec frama-c -kernel-help. Nous nous intéresserons en particulier aux options -main, -lib-entry et -pp-annot.

De plus, nous utiliserons avant tout le greffon value, fondé sur l'interprétation abstraite (cf. cours précédent). Ses options sont accessibles par frama-c -value-help. Les options les plus importantes pour ce TP sont -val, -slevel et -wlevel.

Enfin, il existe une interface graphique, frama-c-gui, qui accepte les mêmes options que frama-c.

On considère l'implantation de la factorielle telle que vue dans le cours 3: (fichier fact.c)

int fact(int x) {
  int y = 1;
  int z = 1L;
  while (y <= x) {
    z = z * y;
    y++;
  }
  return z;
}

On utilise l'option -main fact pour indiquer que le point d'entrée de notre analyse est la fonction fact, et l'option -val pour lancer l'analyse de valeur. Qu'indique Frama-C pour les valeurs possibles de x, y et z?

On va maintenant analyser fact dans un contexte particulier: on s'intéresse au cas où x est compris entre 0 et 100. Pour cela, on peut écrire une fonction qui va assigner à x une valeur présentant les bonnes propriétés puis appeler fact (fichier fact_context.c):

#include "fact.c"
 
volatile int entropy;
 
int interval(int min, int max) {
  int res = entropy;
  if (res < min) res = min;
  if (res > max) res = max;
  return res;
}
 
int main (void) {
  int x = interval(0,100);
  return fact(x);
}

La fonction interval renvoie un de ses deux arguments en fonction d'une valeur inconnue et qui change à chaque appel.

1. Lancer Frama-c sur la fonction main. Quelles sont les valeurs calculées pour x, y et z?
2. On peut utiliser l'option -wlevel pour retarder le moment où Frama-C fait un élargissement. Quelle est la valeur minimale pour laquelle on obtient la meilleure précision possible sur y?
3. Même question avec l'option -slevel qui propage des états séparés jusqu'à un certain point.
4. À quoi est due la valeur obtenue pour z? Donner la plus grande valeur possible pour x qui ne fait pas apparaître le problème.

On peut aussi guider l'analyse de valeur par des annotations ACSL: Avec un slevel approprié, une disjonction conduira à une analyse sur deux états séparés. On considère le programme suivant (fichier annot.c):

int x, y, z;
 
void f(int c) {
  int* p = 0;
 
  if (c == 1) p = &x;
  if (c == 2) p = &y;
  if (c == 3) p = &z; 
 
  if (0<c && c <4) *p=42;
}

1. Faire l'analyse à partir de f, considéré comme un appel de bibliothèque (option -lib-entry, qui a pour effet de ne pas considérer que dans l'état du début d'analyse les variables globales sont initialisées à 0 (ou NULL, ou 0.0 suivant le type de données).
2. Peut-on faire disparaître le warning en jouant avec -slevel? Pourquoi?
3. Donner une annotation qui permet de faire une analyse sans warning. Quel est alors le slevel minimal qui permet de faire une analyse sans warning?

Une implantation possible de la fonction memcpy de la bibliothèque standard du C est la suivante (fichier memcpy.c):

void *memcpy(void *src, void* dst, int size) {
  unsigned long dst_val = ((unsigned long) dst) % 4 ;
  int todo = size;
  char *dstc = (char *) dst;
  char *srcc = (char *) src;
  for (int i=0; i < dst_val && todo > 0; i++) {
    *dstc++ = *srcc++;
    todo--;
  }
  int *dsti = (int *) dstc;
  int *srci = (int *) srcc;
  while (todo>=4) {
    *dstc++=*srci++;
    todo-=4;
  }
  dstc=(char*)dsti;
  srcc=(char*)srci;
  for (int i=0; i < todo; i++) {
    *dstc++=*srci++;
  }
  return dst;
}

On effectue la copie par blocs de 4 caractères, excepté éventuellement au début (pour faire des écritures alignées en mémoire) ou à la fin (s'il reste moins de 4 caractères à copier).

1. Écrire une fonction de contexte permettant de vérifier que la copie d'un nombre n de caractères arbitraire entre 0 et 512 entre deux buffers distincts ne provoque pas d'accès hors-borne, et qu'après un appel à memcpy les n premières cases de dst ont été initialisées.
2. Utiliser l'analyse de valeur pour vérifier si c'est bien le cas. On pourra utiliser une annotation ACSL pour contraindre les valeurs possibles de dst_val, Frama-C ne gérant pas bien les modulo sur des valeurs issues de pointeurs.

On s'intéresse maintenant à des fonctions sur des chaînes de caractères C, c'est à dire des blocs d' unsigned char comportant un élément égal à 0.

1. Écrire une fonction strlen qui étant donné une chaîne retourne le premier index pointant sur 0.
2. Écrire une fonction de contexte permettant de vérifier que strlen ne fait pas d'accès hors-borne pour toute chaîne de longueur inférieure ou égale à 63 caractères (0 final exclu), et utiliser l'analyse de valeur pour vérifier qu'aucun warning n'apparaît.
3. Mêmes questions avec la fonction strcpy, qui copie le contenu de son premier argument dans le deuxième, pour des chaînes de taille au plus 63. Pour le contexte, on considérera deux cas: tout d'abord celui où la source et la destination sont deux buffers distincts, puis celui où source et destination sont deux parties du même bloc mémoire (avec un recouvrement potentiel).