Linux Embedded

Le blog des technologies libres et embarquées

HowTo

Analyse statique de code avec Frama-C

Par le  •  pas de commentaire

Introduction

Frama-C est un framework open source d’analyse statique de code C. Contrairement à ce que l’on pourrait penser, il n’a pas pour objectif de mesurer des données telles que le nombre de commentaires par lignes de code. Il ressemble plus à un outil de bug-finding, mais avec deux avantages majeurs.

Premièrement le fait qu’il tend à être correct, c’est à dire que si une erreur susceptible de faire planter le programme durant l’exécution est présente dans le code, il doit la détecter.

Deuxièmement, il permet à l’utilisateur de manipuler des spécifications, et de prouver que le code est bien conforme à celles-ci.

Ces deux fonctionnalités sont garanties, cependant l’utilisation de Frama-C en devient plus complexe que celle des autres programmes d’analyse statique.

Il fonctionne sur le modèle d’un noyau auquel on peut ajouter des modules ou plug-in, comme Gimp ou Eclipse. Ces plug-in peuvent interagir les uns avec les autres. Par exemple, Slicing utilise les résultats de Eva (Evolved Value Analysis plug-in) et From pour découper le code. Nous verrons plus en détail l'utilisation d'Eva dans cet article.

Il est aussi possible de réaliser des analyses pour différentes plateformes, ce qui peut être utile pour l’embarqué par exemple.

Installation

Il existe plusieurs moyens d’installer Frama-C : télécharger le binaire, compiler depuis les sources, ou bien utiliser le Opam packet manager (recommandé).

Nous allons suivre la méthode recommandée, comme indiqué dans le manuel utilisateur. Il s’agit de la méthode la plus rapide car opam devrait installer les dépendances suivantes automatiquement.

Note : Frama-c est aussi disponible dans Fedora 29. Il suffit alors d'utiliser la commande suivante :
$ sudo dnf install frama-c

  • Un préprocesseur C (par défaut, Frama-C utilise gcc, mais il est possible d’en utiliser un autre. Il est aussi possible d’utiliser Frama-C sur des fichiers pré-compilés. )

  • Un compilateur C

  • Un environnement de compilation Unix (GNU make)

  • Le compilateur OCaml

  • Gtk (pour utiliser l’interface graphique)

  • OcamlGraph

  • Zarith

Nous allons dans un premier temps installer opam. Suivez les instructions correspondant à votre distribution sur cette page : http://opam.ocaml.org/doc/Install.html.

Lancez ensuite la commande suivante :

opam install frama-c

Différents exécutables sont installés :

  • frama-c: Version compilée, ligne de commande

  • frama-c.byte: Bytecode version, ligne de commande

  • frama-c-gui: Version compilée, interface graphique

  • frama-c-gui.byte: Version Bytecode, interface graphique

Les versions Bytecode permettent d’être exécutées dans différents environnements, mais sont bien plus lentes que les versions compilées. En temps normal, il vaut donc mieux utiliser les versions compilées.

Frama-c dispose d’une interface graphique : pour la lancer, il suffit d’utiliser la commande frama-c-gui à la place de frama-c. Le reste de la commande reste inchangé.

Note : Il faut lancer la commande sudo opam init afin de mettre à jour les variables d’environnement qui vont permettre d’utiliser les packets opam et les compilateurs. Afin de ne pas avoir à relancer cette commande à chaque session, laissez-le mettre à jour fichier de configuration (~/.bashrc , ~/.profile, etc)

Les Plug-ins

Il suffit de lancer la commande dans un terminal afin de démarrer l’analyse. Comme on l’a vu précédemment, Frama-c fonctionne sur le modèle de plug-in. Certains plug-ins sont installés par défaut, c’est le cas du Evolved Value Analysis plug-in (Eva). Chaque plug-in fonctionne différemment. Il existe une documentation pour la plupart d’entre-eux, ainsi qu’un utilitaire d’aide en rajoutant le suffixe -h au nom du plugin appelé, par exemple : frama-c -eva-h code.c. Une petite aide est aussi disponible en tapant frama-c -h. La commande frama-c -plugin permet d’afficher une brève description des plug-ins installés, ainsi que la commande d’aide correspondante.

Au lancement, Frama-c va charger les plug-in disponibles dans le répertoire indiqué par la commande frama-c -print-plugin-path. Voici une liste non exhaustive des différents plug-in installés par défaut :

  • Aoraï : Permet de vérifier les spécifications exprimées au format LTL

  • Callgraph: Permet de générer le callgraph d’un programme, au format dot. Il sera alors possible d’en dessiner un diagramme à l’aide de GraphViz.

  • E-ACSL : Permet de traduire les annotations ACSL (ANSI/ISO C Specification Language) en C afin d’effectuer des vérifications d’assertion lors de l’exécution.

  • Eva : The Evolved Value Analysis plug-in : Permet de calculer le domaine de variation des variables d’un programme en C. Il est souvent utilisé en complément par d’autres plug-ins. C’est ce plug-in qui permet d’assurer l’absence de run-time error d’un programme.

  • Impact : Ce plug-in permet de mettre en évidence les lignes de codes qui sont impactées par une modification.

  • Metrics : Permet de calculer différentes « metrics » dans le code. Les Metrics sont en réalité les différentes statistiques d’un programme, comme par exemple le nombre de if, de goto, de loop, le total d’opérateurs, etc.

  • Nonterm : Alerte s’il existe des fonctions qui ne peuvent atteindre de valeur de retour ou des boucles infinies.

  • Pdg : Affiche les dépendances d’un programme.

  • Slicing : Permet de découper le code en plusieurs fonctions, selon un critère défini par l’utilisateur.

  • Wp : Plug-in de vérification. Il permet de prouver qu’un code est conforme à une spécification exprimée en ACSL.

Utilisation

Frama-c s’utilise exclusivement à l’aide de plugins. La commande principale pour lancer une analyse est :

frama-c -plugin mon_code.c

Cette commande diffère pour chaque plug-in, mais la structure reste globalement la même.

A chaque utilisation, frama-c va utiliser le pré-processeur avant d’analyser chaque fichier. La commande utilisée par défaut est gcc -C -E -I . Il est cependant possible d’utiliser des fichiers .i qui sont déjà pré-processés.

Note: En effet lorsque frama-c lance une analyse, il commence par pré-processer les fichiers. Si un fichier sur lequel on veut lancer l'analyse a l'extension .i, alors frama-c ne lancera pas le pré-processeur sur celui-ci. Il est possible d'utiliser gcc -E afin de réaliser uniquement le pré-process, et ainsi produire les fichiers .i.

Interface graphique

Nous allons maintenant passer à la pratique. L’interface graphique de frama-c se lance avec la commande frama-c-gui example.c. Elle se présente de la manière suivante :

On distingue 5 zones importantes : l’arborescence, les plug-in, la fenêtre des messages, le code source d’origine et le code source normalisé.

La fenêtre de message contient 6 pages différentes :

  • Information : fournit des détails sur les objets sélectionnés, ou bien des messages d’information des plugins.

  • Messages : les messages importants générés par l’analyse de Frama-c se trouvent dans cet onglet. On y trouve notamment les messages de type Alarm, qui indiquent les potentielles erreurs.

  • Console : c’est la sortie standard. On retrouve exactement les mêmes informations qu’avec frama-c en mode console.

  • Properties : affiche le statut des propriétés et problèmes découverts lors de l’analyse.

  • Values : affiche des informations du plugin Value Analysis.

  • WP Goals : affiche des informations du plugin WP.

Frama-c effectue quelques transformations du code. Ces transformations ont pour but de rendre le travail d’analyse plus aisé. Le code ainsi obtenu est sémantiquement le même.

Afin de démarrer une analyse immédiatement au démarrage de l’interface graphique, lancez la commande :

frama-c-gui -eva example.c

Eva

L’un des plug-ins les plus important est Eva. Comme nous l’avons vu précédemment, il permet de prouver qu’un code ne peut planter à l’exécution. C’est aussi l’un des plug-ins les plus lourds, avec un grand nombre d’options. Enfin, beaucoup d’autres plug-ins se basent sur les résultats d’Eva pour fonctionner. Par ailleurs, il dispose de sa propre documentation, disponible sur le site de Frama-c.

Note : La garantie d’absence de bug peut ne pas être réalisée en utilisant des tests. En effet, beaucoup de formes de bugs qui peuvent arriver dans un programme en C peuvent donner un comportement non déterministe. De ce fait, un code peut fonctionner durant les tests et planter après déploiement. De plus, il est impossible de tester toutes les valeurs possibles d’un programme en un temps raisonnable, d’où l’existence de couverture de tests.

 

Essayez de lancer l’analyse sur l’exemple de code suivant : (rappel de la commande : frama-c-gui -eva example.c.)

#include <stdio.h>

int S=0;
int T[5];
int main(void)
{
	int i;
	int *p = &T[0] ;
	for (i=0; i<5; i++)
	{ S = S+i; 
		*p++ = S; 
	}
	printf("%d", S);
	return S;
}

On obtient le code normalisé suivant :

int main(void)
{
  int i;
  int *p = T;
  i = 0;
  while (i < 5) {
    {
      int *tmp;
      /*@ assert Eva: signed_overflow: S + i ≤ 2147483647; */
      S += i;
      { /* sequence */
        tmp = p;
        p ++;
        /*@ assert Eva: mem_access: \valid(tmp); */
        *tmp = S;
      }
    }
    i ++;
  }
  printf_va_1("%d",S);
  return S;
}

On remarque que l’analyse met en évidence deux alarmes :

/*@ assert Eva: signed_overflow: S + i ≤ 2147483647; */
et 
/*@ assert Eva: mem_access: \valid(tmp); */

Ceci signifie que le plugin a détecté deux problèmes potentiels. Cependant, en lisant le code, on comprend facilement que S ne dépassera jamais la valeur maximale d’un entier, et que tmp (l’adresse de p avant incrément) est parfaitement accessible. En réalité, on peut voir en cliquant sur l’une de ces deux lignes, que le statut de l’alarme est « Unknown ». Ceci signifie que l’analyse n’a pas été assez poussée pour vérifier toutes les conditions.

Pour pallier à ce problème, rendez-vous dans la fenêtre des plugins, en bas à gauche. Dans la partie « Eva », on peut apercevoir la case : slevel. Cette option permet d’indiquer au plugin le nombre de fois qu’il doit dérouler les boucles d’un programme. Dans notre cas, T contient 5 cases, et la boucle incrémente les valeurs de i de 0 à 4. On peut donc mettre une valeur de 5 dans le slevel, puis cliquer sur Run pour recommencer l’analyse.

On remarque ainsi que les potentielles erreurs détectées précédemment sont passées du statut de Unknown à Valid, avec une colorisation verte.

Lorsque vous analysez un programme de cette manière, et que Eva ne signale pas d’erreur ou d’erreur potentielle, cela signifie Frama-c garantie que votre code ne plantera jamais durant l’exécution.

Essayons maintenant de tester un code qui plante, cette fois-ci en mode console :

#include <stdio.h>
#include <stdlib.h>

int main(void)
{

float f = 4294967296;
unsigned int i;

i = f;
	printf("%d",i);	
	return i;
}

Ce code a l’air parfaitement fonctionnel, il compile sans warnings et on peut lancer l’exécutable normalement. Cependant, il contient une erreur qui ferait exploser une fusée en plein vol. Essayons d’analyser ce programme à l’aide d’Eva :

frama-c -eva example2.c

On obtient le résultat suivant sur la sortie standard :

Frama-c a détecté un overflow lors de la conversion flottant vers entier. Il indique donc un message NON TERMINATING FUNCTION, qui signifie qu’il subsiste une erreur dans le code. Il faudra donc la corriger avant de lancer Ariane 6.

Astuce : Comme précédemment, vous pouvez indiquer à Eva le nombre d’itération de boucle à l’aide de la commande : frama-c -eva -slevel n example.c, avec n le nombre d’itérations. Vous pouvez également afficher la version du code normalisé : frama-c -eva -print example.c.

Callgraph

Ce plugin permet de générer automatiquement un graphe d’appels de fonctions d’un programme. Cela permet de découvrir un nouveau programme plus facilement, afin de le comprendre et d’y apporter des modifications plus rapidement (par exemple pour un programme open source).

Vous trouverez en pièce jointe un exemple de programme : exemple_cuisine

Afin de lancer callgraph, tapez la commande suivante dans un terminal :

frama-c *.c -cg diagram.dot

Un fichier .dot est ainsi généré. Il va nous permettre d’afficher un graphe à l’aide de la commande suivante :

dot -Tsvg diagram.dot -o diagram.svg

Ici la commande dot permet de convertir un fichier .dot en image. On peut choisir le format de sortie avec l’option -T. Ici, on a choisit le format svg car c’est un format vectoriel, très pratique pour pouvoir redimensionner un graphe sans pixeliser l’image. On obtient ainsi :

Dans cet exemple, on comprend en quelques secondes le fonctionnement de ce programme.

Note : Malheureusement, je n’ai trouvé aucune documentation concernant ce plugin. Impossible donc de connaître la signification des couleurs, des losanges/cercles, des blocs et des S<numéro>. On peut néanmoins supposer que les cercles en pointillés sont les appels à la bibliothèque standard.

Difficultés rencontrées

Frama-c est un programme qui offre beaucoup de possibilités. Cependant, il est assez difficile à prendre en main. Réaliser une première analyse peut paraître rapide et simple, car il suffit d’une seule commande dans le terminal. En réunissant toutes les sources au même endroit, frama-c *.c permet de lancer une analyse sur tous les fichiers en même temps, ce qui est indispensable pour réaliser un Callgraph par exemple.

Malheureusement, chaque projet open-source dispose d’une arborescence différente, les fichiers étant regroupés dans des dossiers et des sous-dossiers. De plus, la plupart des projets sont compilés dans un environnement configuré par un utilitaire comme Autoconf. Dans ce genre de projets, il est difficile de lancer une analyse avec Frama-c.

Premièrement, afin de parcourir les dossiers et les sous-dossiers, la commande s’alourdit sensiblement :

find . -name \*.c -exec frama-c -cg diagram_busy {} \;

Il faut ensuite lui préciser l’emplacement de librairies manquantes :

find . -name \*.c -exec frama-c -cpp-extra-args="-I /usr/include" -cg diagram_busy {} \;

Puis rajouter des librairies jusqu’à ce qu’il n’y ait plus d’erreur de précompilation.

La documentation évoque un moyen de récupérer des fichiers précompilés afin de lancer une analyse sur ceux-ci. Cette méthode pourrait permettre de résoudre le problème précédent, car il suffirait de modifier le makefile produit par autoconf pour dire au compilateur de s’arrêter après la compilation, ou bien de modifier le fichier configure.ac afin de lui indiquer de produire un makefile qui lance le précompilateur uniquement. La commande AC_PREPROC_IFELSE permet de réaliser cela.

Malheureusement, aucune des deux méthodes précédentes n’a été fructueuse lors de mes tests.

J’ai néanmoins réussi à produire des .i sur mes fichiers de tests, avec la commande gcc suivante :

gcc -E *.c > test.i

Cependant, l’analyse frama-c sur ce fichier n’a rien donné, si ce n’est des erreurs.

Note : Si vous lisez ces lignes et que vous parvenez à faire fonctionner frama-c à partir de fichiers .i, ou bien dans sur un gros projet open-source tel que busybox, merci de laisser votre solution en commentaire de cet article.

Conclusion

Au cours de cet article, nous avons vu comment installer et utiliser Frama-c en ligne de commande et dans la console. Nous avons mis en pratique l’utilisation du plug-in Eva, qui permet de prouver qu’un code ne peut planter lors de son exécution. Enfin, nous avons utilisé le plug-in Callgraph afin de générer automatiquement un diagramme d’appels de fonctions permettant de comprendre facilement un code non familier.

Pour aller plus loin

Comme nous l’avons vu, Frama-c fonctionne sur le principe de plug-ins. Nous en avons vu deux, mais il en reste encore beaucoup à découvrir. De plus, il est possible de créer son propre plug-in à l’aide de l’API de Frama-c. Un guide disponible sur le site de frama-c décrit les étapes permettant de réaliser son propre plug-in pas à pas. On peut aussi penser à une utilisation dans un contexte d’intégration continue avec Jenkins et SonarQube. Il serait possible par exemple de lancer automatiquement une analyse avec Eva, qui pourrait indiquer si le code comporte des risques de plantage durant l’exécution ou non.

 

 

Laisser un commentaire

Votre adresse de messagerie ne sera pas publiée.