Licence CC BY-NC-SA

Contrats de fonctions

Dernière mise à jour :

Il est plus que temps d’entamer les hostilités. Contrairement aux tutoriels sur divers langages, nous allons commencer par les fonctions. D’abord parce qu’il faut savoir en écrire avant d’entamer un tel tutoriel et surtout parce que cela permettra rapidement d’écrire quelques preuves jouables.

Au contraire, après le travail sur les fonctions, nous entamerons les notions les plus simples comme les affectations ou les structures conditionnelles pour comprendre comment fonctionne l’outil sous le capot.

Pour pouvoir prouver qu’un code est valide, il faut d’abord pouvoir spécifier ce que nous attendons de lui. La preuve de programme consistera donc à s’assurer que le code que nous avons écrit correspond bien à la spécification qui décrit le rôle qui lui a été attribué. Comme mentionné plus tôt dans le tutoriel, la spécification de code pour Frama-C est faite avec le langage ACSL, celui-ci nous permet (mais pas seulement, comme nous le verrons dans la suite) de poser un contrat pour chaque fonction.

Définition d'un contrat

Le principe d’un contrat de fonction est de poser les conditions selon lesquelles la fonction va s’exécuter. C’est-à-dire : ce que doit respecter le code appelant à propos des variables passées en paramètres et de l’état de la mémoire globale pour que la fonction s’exécute correctement, la pré-condition ; et ce que s’engage à respecter la fonction en retour à propos de l’état de la mémoire et de la valeur de retour : la post-condition.

Ces propriétés sont exprimées en langage ACSL, la syntaxe est relativement simple pour qui a déjà fait du C puisqu’elle reprend la syntaxe des expressions booléennes du C. Cependant, elle ajoute également :

  • certaines constructions et connecteurs logiques qui ne sont pas présents originellement en C pour faciliter l’écriture ;
  • des prédicats pré-implémentés pour exprimer des propriétés souvent utiles en C (par exemple : pointeur valide) ;
  • ainsi que des types plus généraux que les types primitifs du C, typiquement les types entiers ou réels.

Nous introduirons au fil du tutoriel les notations présentes dans le langage ACSL.

Les spécifications ACSL sont introduites dans nos codes source par l’intermédiaire d’annotations. Syntaxiquement, un contrat de fonction est intégré dans les sources de la manière suivante :

1
2
3
4
5
6
/*@
  //contrat
*/
void foo(int bar){

}

Notons bien le @ à la suite du début du bloc de commentaire, c’est lui qui fait que ce bloc devient un bloc d’annotations pour Frama-C et pas un simple bloc de commentaires à ignorer.

Maintenant, regardons comment sont exprimés les contrats, à commencer par la post-condition, puisque c’est ce que nous attendons en priorité de notre programme (nous nous intéresserons ensuite aux pré-conditions).

Post-condition

La post-condition d’une fonction est précisée avec la clause ensures. Nous allons travailler avec la fonction suivante qui donne la valeur absolue d’un entier reçu en entrée. Une de ses post-conditions est que le résultat (que nous notons avec le mot-clé \result) est supérieur ou égal à 0.

1
2
3
4
5
6
7
/*@
  ensures \result >= 0;
*/
int abs(int val){
  if(val < 0) return -val;
  return val;
}

(Notons le ; à la fin de la ligne de spécification comme en C).

Mais ce n’est pas tout, il faut également spécifier le comportement général attendu d’une fonction renvoyant la valeur absolue. À savoir : si la valeur est positive ou nulle, la fonction renvoie la même valeur, sinon elle renvoie l’opposée de la valeur.

Nous pouvons spécifier plusieurs post-conditions, soit en les composants avec un && comme en C, soit en introduisant une nouvelle clause ensures, comme illustré ci-dessous.

1
2
3
4
5
6
7
8
9
/*@
  ensures \result >= 0;
  ensures (val >= 0 ==> \result == val ) && 
          (val <  0 ==> \result == -val);
*/
int abs(int val){
  if(val < 0) return -val;
  return val;
}

Cette spécification est l’opportunité de présenter un connecteur logique très utile que propose ACSL mais qui n’est pas présent en C : l’implication $A \Rightarrow B$, que l’on écrit en ACSL A ==> B. La table de vérité de l’implication est la suivante :

$A$ $B$ $A \Rightarrow B$
$F$ $F$ $V$
$F$ $V$ $V$
$V$ $F$ $F$
$V$ $V$ $V$

Ce qui veut dire qu’une implication $A \Rightarrow B$ est vraie dans deux cas : soit $A$ est fausse (et dans ce cas, il ne faut pas se préoccuper de $B$), soit $A$ est vraie et alors $B$ doit être vraie aussi. L’idée étant finalement « je veux savoir si dans le cas où $A$ est vrai, $B$ l’est aussi. Si $A$ est faux, je considère que l’ensemble est vrai ».

Sa cousine l’équivalence $A \Leftrightarrow B$ (écrite A <==> B en ACSL) est plus forte. C’est la conjonction de l’implication dans les deux sens :$(A \Rightarrow B) \wedge (B \Rightarrow A)$. Cette formule n’est vraie que dans deux cas : $A$ et $B$ sont vraies toutes les deux, ou fausses toutes les deux (c’est donc la négation du ou-exclusif).

Profitons en pour rappeler l’ensemble des tables de vérités des opérateurs usuels en logique du premier ordre ($\neg$ = !, $\wedge$ = &&, $\vee$ = ||) :

$A$ $B$ $\neg A$ $A \wedge B$ $A \vee B$ $A \Rightarrow B$ $A \Leftrightarrow B$
$F$ $F$ $V$ $F$ $F$ $V$ $V$
$F$ $V$ $V$ $F$ $V$ $V$ $F$
$V$ $F$ $F$ $F$ $V$ $F$ $F$
$V$ $V$ $F$ $V$ $V$ $V$ $V$

Revenons à notre spécification. Quand nos fichiers commencent à être longs et contenir beaucoup de spécifications, il peut être commode de nommer les propriétés que nous souhaitons vérifier. Pour cela, nous indiquons un nom (les espaces ne sont pas autorisées) suivi de : avant de mettre effectivement la propriété, il est possible de mettre plusieurs « étages » de noms pour catégoriser nos propriétés. Par exemple nous pouvons écrire ceci :

1
2
3
4
5
6
7
8
9
/*@
  ensures positive_value: function_result: \result >= 0;
  ensures (val >= 0 ==> \result == val) && 
          (val < 0 ==> \result == -val);
*/
int abs(int val){
  if(val < 0) return -val;
  return val;
}

Dans une large part du tutoriel, nous ne nommerons pas les éléments que nous tenterons de prouver, les propriétés seront généralement relativement simples et peu nombreuses, les noms n’apporteraient pas beaucoup d’information.

Nous pouvons copier/coller la fonction abs et sa spécification dans un fichier abs.c et regarder avec Frama-C si l’implémentation est conforme à la spécification.

Pour cela, il faut lancer l’interface graphique de Frama-C (il est également possible de se passer de l’interface graphique, cela ne sera pas présenté dans ce tutoriel) soit par cette commande :

1
$ frama-c-gui

Soit en l’ouvrant depuis l’environnement graphique.

Il est ensuite possible de cliquer sur le bouton « Create a new session from existing C files », les fichiers à analyser peuvent être sélectionnés par double-clic, OK terminant la sélection. Par la suite, l’ajout d’autres fichiers à la session s’effectue en cliquant sur Files > Source Files.

À noter également qu’il est possible de directement ouvrir le(s) fichier(s) depuis la ligne de commande en le(s) passant en argument(s) de frama-c-gui.

1
$ frama-c-gui abs.c
Le volet latéral liste l’arbre des fichiers et des fonctions

La fenêtre de Frama-C s’ouvre, dans le volet correspondant aux fichiers et aux fonctions, nous pouvons sélectionner la fonction abs. Aux différentes lignes ensures, il y a un cercle bleu dans la marge, ils indiquent qu’aucune vérification n’a été tentée pour ces lignes.

Nous demandons la vérification que le code répond à la spécification en faisant un clic droit sur le nom de la fonction et « Prove function annotations by WP » :

Lancer la vérification de abs avec WP

Nous pouvons voir que les cercles bleus deviennent des pastilles vertes, indiquant que la spécification est bien assurée par le programme. Il est possible de prouver les propriétés une à une en cliquant droit sur celles-ci et pas sur le nom de la fonction.

Mais le code est-il vraiment sans erreur pour autant ? WP nous permet de nous assurer que le code répond à la spécification, mais il ne fait pas de contrôle d’erreur à l’exécution (RunTime Error : RTE). C’est le rôle d’un autre petit plugin que nous allons utiliser ici et qui s’appelle sobrement RTE. Son but est d’ajouter des contrôles dans le programme pour les erreurs d’exécutions possibles (débordements d’entiers, déréférencements de pointeurs invalides, division par 0, etc).

Pour activer ce contrôle, nous cochons la case montrée par cette capture (dans le volet de WP). Il est également possible de demander à Frama-C d’ajouter ces contrôles par un clic droit sur le nom de la fonction puis « Insert RTE guards ».

Activer la vérification des erreurs d’exécution

Enfin nous relançons la vérification (nous pouvons également cliquer sur le bouton « Reparse » de la barre d’outils, cela aura pour effet de supprimer les preuves déjà effectuées).

Nous pouvons alors voir alors que WP échoue à prouver l’impossibilité de débordement arithmétique sur le calcul de -val. Et c’est bien normal parce que -INT_MIN ($-2^{31}$) > INT_MAX ($2^{31}-1$).

Preuve incomplète de abs

Il est bon de noter que le risque de dépassement est pour nous réel car nos machines (dont Frama-C détecte la configuration) fonctionne en complément à deux pour lequel le dépassement n’est pas défini par la norme C.

Ici nous pouvons voir un autre type d’annotation ACSL. La ligne //@ assert propriete ; nous permet de demander la vérification d’une propriété à un point particulier du programme. Ici, l’outil l’a insérée pour nous car il faut vérifier que le -val ne provoque pas de débordement, mais il est également possible d’en ajouter manuellement dans un code.

Comme le montre cette capture d’écran, nous avons deux nouveaux codes couleur pour les pastilles : vert+marron et orange.

La couleur vert + marron nous indique que la preuve a été effectué mais qu’elle dépend potentiellement de propriétés qui, elle, ne l’ont pas été.

Si la preuve n’est pas recommencée intégralement par rapport à la preuve précédente, ces pastilles ont dû rester vertes car les preuves associées ont été réalisées avant l’introduction de la propriété nous assurant l’absence de runtime-error, et ne se sont donc pas reposées sur la connaissance de cette propriété puisqu’elle n’existait pas.

En effet, lorsque WP transmet une obligation de preuve à un prouveur automatique, il transmet (basiquement) deux types de propriétés : $G$, le but, la propriété que l’on cherche à prouver, et $S_1$$S_n$ les diverses suppositions que l’on peut faire à propos de l’état du programme au point où l’on cherche à vérifier $G$. Cependant, il ne reçoit pas, en retour, quelles propriétés ont été utilisées par le prouveur pour valider $G$. Donc si $S_3$ fait partie des suppositions, et si WP n’a pas réussi à obtenir une preuve de $S_3$, il indique que $G$ est vraie, mais à condition seulement que l’on arrive un jour à prouver $S_3$.

La couleur orange nous signale qu’aucun prouveur n’a pu déterminer si la propriété est vérifiable. Les deux raisons peuvent être :

  • qu’il n’a pas assez d’information pour le déterminer ;
  • que malgré toutes ses recherches, il n’a pas pu trouver un résultat à temps. Auquel cas, il rencontre un timeout dont la durée est configurable dans le volet de WP.

Dans le volet inférieur, nous pouvons sélectionner l’onglet « WP Goals », celui-ci nous affiche la liste des obligations de preuve et pour chaque prouveur indique un petit logo si la preuve a été tentée et si elle a été réussie, échouée ou a rencontré un timeout (ici nous pouvons voir un essai avec Z3 sur le contrôle de la RTE pour montrer le logo des ciseaux associé au timeout).

Tableau des obligations de preuve de WP pour abs

Le tableau est découpé comme suit, en première colonne nous avons le nom de la fonction où se trouve le but à prouver. En seconde colonne nous trouvons le nom du but. Ici par exemple notre post-condition nommée est estampillée "Post-condition ’positive_value,function_result’", nous pouvons d’ailleurs noter que lorsqu’une propriété est sélectionnée dans le tableau, elle est également sur-lignée dans le code source. Les propriétés non-nommées se voient assignées comme nom le type de propriété voulu. En troisième colonne, nous trouvons le modèle mémoire utilisé pour la preuve, (nous n’en parlerons pas dans ce tutoriel). Finalement, les dernières colonnes représentent les différents prouveurs accessibles à WP.

Dans ces prouveurs, le premier élément de la colonne est Qed. Ce n’est pas à proprement parler un prouveur. En fait, si nous double-cliquons sur la propriété "ne pas déborder" (surlignée en bleu dans la capture précédente), nous pouvons voir ceci :

Obligation de preuve associée à la vérification de débordement dans abs

C’est l’obligation de preuve que génère WP par rapport à notre propriété et notre programme, il n’est pas nécessaire de comprendre tout ce qui s’y passe, juste d’avoir une idée globale. Elle contient (dans la partie « Assume ») les suppositions que nous avons pu donner et celles que WP a pu déduire des instructions du programme. Elle contient également (dans la partie « Prove ») la propriété que nous souhaitons vérifier.

Que fait WP avec ces éléments ? En fait, il les transforme en une formule logique puis demande aux différents prouveurs s’il est possible de la satisfaire (de trouver pour chaque variable, une valeur qui rend la formule vraie), cela détermine si la propriété est prouvable. Mais avant d’envoyer cette formule aux prouveurs, WP utilise un module qui s’appelle Qed et qui est capable de faire différentes simplifications à son sujet. Parfois comme dans le cas des autres propriétés de abs, ces simplifications suffisent à déterminer que la propriété est forcément vraie, auquel cas, nous ne faisons pas appel aux prouveurs.

Lorsque les prouveurs automatiques ne parviennent pas à assurer que nos propriétés sont bien vérifiées, il est parfois difficile de comprendre pourquoi. En effet, les prouveurs ne sont généralement pas capables de nous répondre autre chose que « oui », « non » ou « inconnu », ils ne sont pas capables d’extraire le « pourquoi » d’un « non » ou d’un « inconnu ». Il existe des outils qui sont capables d’explorer les arbres de preuve pour en extraire ce type d’information, Frama-C n’en possède pas à l’heure actuelle. La lecture des obligations de preuve peut parfois nous aider, mais cela demande un peu d’habitude pour pouvoir les déchiffrer facilement. Finalement, le meilleur moyen de comprendre la raison d’un échec est d’effectuer la preuve de manière interactive avec Coq. En revanche, il faut déjà avoir une certaine habitude de ce langage pour ne pas être perdu devant les obligations de preuve générées par WP, étant donné que celles-ci encodent les éléments de la sémantique de C, ce qui rend le code souvent indigeste.

Si nous retournons dans notre tableau des obligations de preuve (bouton encadré dans la capture d’écran précédente), nous pouvons donc voir que les hypothèses n’ont pas suffi aux prouveurs pour déterminer que la propriété « absence de débordement » est vraie (et nous l’avons dit : c’est normal), il nous faut donc ajouter une hypothèse supplémentaire pour garantir le bon fonctionnement de la fonction : une pré-condition d’appel.

Pré-condition

Les pré-conditions de fonctions sont introduites par la clause requires, de la même manière qu’avec ensures, nous pouvons composer nos expressions logiques et mettre plusieurs pré-conditions :

1
2
3
4
5
6
7
/*@
  requires 0 <= a < 100;
  requires b < a;
*/
void foo(int a, int b){

}

Les pré-conditions sont des propriétés sur les entrées (et potentiellement sur des variables globales) qui seront supposées préalablement vraies lors de l’analyse de la fonction. La preuve que celles-ci sont effectivement validées n’interviendra qu’aux points où la fonction est appelée.

Dans ce petit exemple, nous pouvons également noter une petite différence avec C dans l’écriture des expressions booléennes. Si nous voulons spécifier que a se trouve entre 0 et 100, il n’y a pas besoin d’écrire 0 <= a && a < 100 (c’est-à-dire en composant les deux comparaisons avec un &&). Nous pouvons simplement écrire 0 <= a < 100 et l’outil se chargera de faire la traduction nécessaire.

Si nous revenons à notre exemple de la valeur absolue, pour éviter le débordement arithmétique, il suffit que la valeur de val soit strictement supérieure à INT_MIN pour garantir que le débordement n’arrivera pas. Nous l’ajoutons donc comme pré-condition (à noter : il faut également inclure le header où INT_MIN est défini) :

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
#include <limits.h>

/*@
  requires INT_MIN < val;

  ensures \result >= 0;
  ensures (val >= 0 ==> \result == val) && 
          (val < 0 ==> \result == -val);
*/
int abs(int val){
  if(val < 0) return -val;
  return val;
}

Rappel : la fenêtre de Frama-C ne permet pas l’édition du code source.

Avec les versions de Frama-C NEON et plus anciennes, le pré-processing des annotations n’était pas activé par défaut. Il faut donc lancer Frama-C avec l’option -pp-annot :

1
$ frama-c-gui -pp-annot file.c

Une fois le code source modifié de cette manière, un clic sur « Reparse » et nous lançons à nouveau l’analyse. Cette fois, tout est validé pour WP, notre implémentation est prouvée :

Preuve de abs effectuée

Nous pouvons également vérifier qu’une fonction qui appellerait abs respecte bien la pré-condition qu’elle impose :

1
2
3
4
5
6
void foo(int a){
   int b = abs(42);
   int c = abs(-42);
   int d = abs(a);       // Faux : "a", vaut peut être INT_MIN
   int e = abs(INT_MIN); // Faux : le paramètre doit être strictement supérieur à INT_MIN
}
Vérification du contrat à l’appel de abs

Pour modifier un peu l’exemple, nous pouvons essayer d’inverser les deux dernières lignes. Auquel cas, nous pouvons voir que l’appel abs(a) est validé par WP s’il se trouve après l’appel abs(INT_MIN) ! Pourquoi ?

Il faut bien garder en tête que le principe de la preuve déductive est de nous assurer que si les pré-conditions sont vérifiées et que le calcul termine alors la post-condition est vérifiée.

Si nous donnons à notre fonction une valeur qui viole ses pré-conditions, alors nous en déduisons que la post-condition est fausse. À partir de là, nous pouvons prouver tout ce que nous voulons car ce « false » devient une supposition pour tout appel qui viendrait ensuite. À partir de faux, nous prouvons tout ce que nous voulons, car si nous avons la preuve de « faux » alors « faux » est vrai, de même que « vrai » est vrai. Donc tout est vrai.

En prenant le programme modifié, nous pouvons d’ailleurs regarder les obligations de preuve générées par WP pour l’appel fautif et l’appel prouvé par conséquent :

Obligation générée pour l’appel fautif
Obligation générée pour l’appel qui suit

Nous pouvons remarquer que pour les appels de fonctions, l’interface graphique nous surligne le chemin d’exécution suivi avant l’appel dont nous cherchons à vérifier la pré-condition. Ensuite, si nous regardons l’appel abs(INT_MIN), nous pouvons remarquer qu’à force de simplifications, Qed a déduit que nous cherchons à prouver « False ». Conséquence logique, l’appel suivant abs(a) reçoit dans ses suppositions « False ». C’est pourquoi Qed est capable de déduire immédiatement « True ».

La deuxième partie de la question est alors : pourquoi lorsque nous mettons les appels dans l’autre sens (abs(a) puis abs(INT_MIN)), nous obtenons quand même une violation de la pré-condition sur le deuxième ? La réponse est simplement que abs(a) peut, ou ne peut pas, provoquer une erreur, alors que abs(INT_MIN) provoque forcément l’erreur. Donc si nous obtenons nécessairement une preuve de « faux » avec un appel abs(INT_MIN), ce n’est pas le cas de l’appel abs(a) qui peut aussi ne pas échouer.

Bien spécifier son programme est donc d’une importance cruciale. Typiquement, préciser une pré-condition fausse peut nous donner la possibilité de prouver FAUX :

1
2
3
4
5
6
7
/*@
  requires a < 0 && a > 0;
  ensures  \false;
*/
void foo(int a){

}

Si nous demandons à WP de prouver cette fonction. Il l’acceptera sans rechigner car la supposition que nous lui donnons en entrée est nécessairement fausse. Par contre, nous aurons bien du mal à lui donner une valeur en entrée qui respecte la pré-condition, nous pourrons donc nous en apercevoir. En regardant pourquoi nous n’arrivons pas à transmettre une valeur valide en entrée.

Certaines notions que nous verrons plus loin dans le tutoriel apporterons un risque encore plus grand de créer ce genre d’incohérence. Il faut donc toujours avoir une attention particulière pour ce que nous spécifions.

Trouver les bonnes pré-conditions

Trouver les bonnes pré-conditions à une fonction est parfois difficile. Le plus important est avant tout de déterminer ces pré-conditions sans prendre en compte le contenu de la fonction (au moins dans un premier temps) afin d’éviter de construire, par erreur, une spécification qui contiendrait le même bug qu’un code fautif, par exemple en prenant en compte une condition faussée. C’est pour cela que l’on souhaitera généralement que la personne qui développe le programme et la personne qui le spécifie formellement soient différentes (même si elles ont pu préalablement s’accorder sur une spécification textuelle par exemple).

Une fois ces pré-conditions posées, alors seulement, nous nous intéressons aux spécifications dues au fait que nous sommes soumis aux contraintes de notre langage et notre matériel. Par exemple, la fonction valeur absolue n’a, au fond, pas vraiment de pré-condition à respecter, c’est la machine cible qui détermine qu’une condition supplémentaire doit être respectée en raison du complément à deux.

Quelques éléments sur l’usage de WP et Frama-C

Dans les deux sous-sections précédentes, nous avons vu un certain nombre d’éléments à propos de l’usage de la GUI pour lancer les preuves. En fait, il est possible de demander immédiatement à WP d’effectuer les preuves pendant le lancement de Frama-C avec la commande :

1
$ frama-c-gui file.c -wp

Cela demande à WP d’immédiatement faire les calculs de plus faible pré-condition et de lancer les prouveurs sur les buts générés.

Concernant les contrôles des RTE, il est généralement conseillé de commencer par vérifier le programme sans mettre les contrôles de RTE. Et ensuite seulement de générer les assertions correspondantes pour terminer la vérification avec WP. Cela permet à WP de se « concentrer » dans un premier temps sur les propriétés fonctionnelles sans avoir la connaissance de propriétés purement techniques dues à C, qui chargent inutilement la base de connaissances. Une nouvelle fois, il est possible de produire ce comportement directement depuis la ligne de commande en écrivant :

1
$ frama-c-gui file.c -wp -then -rte -wp

« Lancer Frama-C avec WP, puis créer les assertions correspondant aux RTE, et lancer à nouveau WP ».

De l'importance d'une bonne spécification

Bien traduire ce qui est attendu

C’est certainement notre tâche la plus difficile. En soi, la programmation est déjà un effort consistant à écrire des algorithmes qui répondent à notre besoin. La spécification nous demande également de faire ce travail, la différence est que nous ne nous occupons plus de préciser la manière de répondre au besoin mais le besoin lui-même. Pour prouver que la réalisation implémente bien ce que nous attendons, il faut donc être capable de décrire précisément le besoin.

Changeons d’exemple et spécifions la fonction suivante :

1
2
3
int max(int a, int b){
  return (a > b) ? a : b;
}

Le lecteur pourra écrire et prouver sa spécification. Pour la suite, nous travaillerons avec celle-ci :

1
2
3
4
5
6
/*@
  ensures \result >= a && \result >= b;
*/
int max(int a, int b){
  return (a > b) ? a : b;
}

Si nous donnons ce code à WP, il accepte sans problème de prouver la fonction. Pour autant cette spécification est-elle juste ? Nous pouvons par exemple essayer de voir si ce code est validé :

1
2
3
4
5
6
7
void foo(){
  int a = 42;
  int b = 37;
  int c = max(a,b);

  //@assert c == 42;
}

La réponse est non. En fait, nous pouvons aller plus loin en modifiant le corps de la fonction max et remarquer que le code suivant est également valide quant à la spécification :

1
2
3
4
5
6
7
8
#include <limits.h>

/*@
  ensures \result >= a && \result >= b;
*/
int max(int a, int b){
  return INT_MAX;
}

Notre spécification est trop permissive. Il faut que nous soyons plus précis. Nous attendons du résultat non seulement qu’il soit supérieur ou égal à nos deux paramètres mais également qu’il soit exactement l’un des deux :

1
2
3
4
5
6
7
/*@
  ensures \result >= a && \result >= b;
  ensures \result == a || \result == b;
*/
int max(int a, int b){
  return (a > b) ? a : b;
}

Pointeurs

S’il y a une notion à laquelle nous sommes confrontés en permanence en langage C, c’est bien la notion de pointeur. C’est une notion complexe et l’une des principales cause de bugs critiques dans les programmes, ils ont donc droit à un traitement de faveur dans ACSL.

Prenons par exemple une fonction swap pour les entiers :

1
2
3
4
5
6
7
8
/*@
  ensures *a == \old(*b) && *b == \old(*a);
*/
void swap(int* a, int* b){
  int tmp = *a;
  *a = *b;
  *b = tmp;
}

Historique des valeurs

Ici, nous introduisons une première fonction logique fournie de base par ACSL : \old, qui permet de parler de l’ancienne valeur d’un élément. Ce que nous dit donc la spécification c’est « la fonction doit assurer que a soit égal à l’ancienne valeur (au sens : la valeur avant l’appel) de b et inversement ».

La fonction \old ne peut être utilisée que dans la post-condition d’une fonction. Si nous avons besoin de ce type d’information ailleurs, nous utilisons \at qui nous permet d’exprimer des propriétés à propos de la valeur d’une variable à un point donné. Elle reçoit deux paramètres. Le premier est la variable (ou position mémoire) dont nous voulons obtenir la valeur et le second la position (sous la forme d’un label C) à laquelle nous voulons contrôler la valeur en question.

Par exemple, nous pourrions écrire :

1
2
3
4
5
  int a = 42;
 Label_a:
  a = 45;

  //@assert a == 45 && \at(a, Label_a) == 42;

En plus des labels que nous pouvons nous-mêmes créer. Il existe 6 labels qu’ACSL nous propose par défaut, mais tous ne sont pas supportés par WP :

  • Pre/Old : valeur avant l’appel de la fonction,
  • Post : valeur après l’appel de la fonction,
  • LoopEntry : valeur en début de boucle (pas encore supporté),
  • LoopCurrent : valeur en début du pas actuel de la boucle (pas encore supporté),
  • Here : valeur au point d’appel.

Le comportement de Here est en fait le comportement par défaut lorsque nous parlons de la valeur d’une variable. Son utilisation avec \at nous servira généralement à s’assurer de l’absence d’ambiguïté lorsque nous parlons de divers points de programme dans la même expression.

À la différence de \old, qui ne peut être utilisée que dans les post-conditions de contrats de fonction, \at peut être utilisée partout. En revanche, tous les points de programme ne sont pas accessibles selon le type d’annotation que nous sommes en train d’écrire. Old et Post ne sont disponibles que dans les post-conditions d’un contrat, Pre et Here sont disponibles partout. LoopEntry et LoopCurrent ne sont disponibles que dans le contexte de boucles (dont nous parlerons plus loin dans le tutoriel).

Pour le moment, nous n’utiliserons pas \at, mais elle peut rapidement se montrer indispensable pour écrire des spécifications précises.

Validité de pointeurs

Si nous essayons de prouver le fonctionnement de swap (en activant la vérification des RTE), notre post-condition est bien vérifiée mais WP nous indique qu’il y a un certain nombre de possibilités de runtime-error. Ce qui est normal, car nous n’avons pas précisé à WP que les pointeurs que nous recevons en entrée de fonction sont valides.

Pour ajouter cette précision, nous allons utiliser le prédicat \valid qui reçoit un pointeur en entrée :

1
2
3
4
5
6
7
8
9
/*@
  requires \valid(a) && \valid(b);
  ensures  *a == \old(*b) && *b == \old(*a);
*/
void swap(int* a, int* b){
  int tmp = *a;
  *a = *b;
  *b = tmp;
}

À partir de là, les déréférencements qui sont effectués par la suite sont acceptés car la fonction demande à ce que les pointeurs d’entrée soient valides.

Comme nous le verrons plus tard, \valid peut recevoir plus qu’un pointeur en entrée. Par exemple, il est possible de lui transmettre une expression de cette forme : \valid(p + (s .. e)) qui voudra dire « pour tout i entre s et e (inclus), p+i est un pointeur valide », ce sera important notamment pour la gestion des tableaux dans les spécifications.

Si nous nous intéressons aux assertions ajoutées par WP dans la fonction swap avec la validation des RTEs, nous pouvons constater qu’il existe une variante de \valid sous le nom \valid_read. Contrairement au premier, celui-ci assure que le pointeur peut être déréférencé mais en lecture seulement. Cette subtilité est due au fait qu’en C, le downcast de pointeur vers un élément const est très facile à faire mais n’est pas forcément légal.

Typiquement, dans le code suivant :

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
/*@ requires \valid(p); */
int unref(int* p){
  return *p;
}

int const value = 42;

int main(){
  int i = unref(&value);
}

Le déréférencement de p est valide, pourtant la pré-condition de unref ne sera pas validée par WP car le déréférencement de l’adresse de value n’est légal qu’en lecture. Un accès en écriture sera un comportement indéterminé. Dans un tel cas, nous pouvons préciser que dans unref, le pointeur p doit être nécessairement \valid_read et pas \valid.

Effets de bord

Notre fonction swap est bien prouvable au regard de sa spécification et de ses potentielles erreurs à l’exécution, mais est-elle pour autant suffisamment spécifiée ? Pour voir cela, nous pouvons modifier légèrement le code de cette façon (nous utilisons assert pour analyser des propriétés ponctuelles) :

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
int h = 42; //nous ajoutons une variable globale

/*@
  requires \valid(a) && \valid(b);
  ensures  *a == \old(*b) && *b == \old(*a);
*/
void swap(int* a, int* b){
  int tmp = *a;
  *a = *b;
  *b = tmp;
}

int main(){
  int a = 37;
  int b = 91;

  //@ assert h == 42;
  swap(&a, &b);
  //@ assert h == 42;
}

Le résultat n’est pas vraiment celui escompté :

Échec de preuve sur une globale non concernée par l’appel à swap

En effet, nous n’avons pas spécifié les effets de bords autorisés pour notre fonction. Pour spécifier les effets de bords, nous utilisons la clause assigns qui fait partie des post-conditions de la fonction. Elle nous permet de spécifier quels éléments non locaux (on vérifie bien des effets de bord), sont susceptibles d’être modifiés par la fonction.

Par défaut, WP considère qu’une fonction a le droit de modifier n’importe quel élément en mémoire. Nous devons donc préciser ce qu’une fonction est en droit de modifier. Par exemple pour la fonction swap :

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
/*@
  requires \valid(a) && \valid(b);

  assigns *a, *b;

  ensures  *a == \old(*b) && *b == \old(*a);
*/
void swap(int* a, int* b){
  int tmp = *a;
  *a = *b;
  *b = tmp;
}

Si nous rejouons la preuve avec cette spécification, la fonction et les assertions que nous avions demandées dans le main seront validées par WP.

Finalement, il peut arriver que nous voulions spécifier qu’une fonction ne provoque pas d’effets de bords. Ce cas est précisé en donnant \nothing à assigns :

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
/*@
  requires \valid_read(a) && \valid_read(b);

  assigns  \nothing;

  ensures \result == *a || \result == *b;
  ensures \result >= *a && \result >= *b;
*/
int max_ptr(int* a, int* b){
  return (*a > *b) ? *a : *b ;
}

Le lecteur pourra maintenant reprendre les exemples précédents pour y intégrer la bonne clause assigns ;) .

Séparation des zones de la mémoire

Les pointeurs apportent le risque d’aliasing (plusieurs pointeurs ayant accès à la même zone de mémoire). Si dans certaines fonctions, cela ne pose pas de problème (par exemple si nous passons deux pointeurs égaux à notre fonction swap, la spécification est toujours vérifiée par le code source), dans d’autre cas, ce n’est pas si simple :

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
#include <limits.h>

/*@
  requires \valid(a) && \valid_read(b);
  assigns  *a;
  ensures  *a == \old(*a)+ *b;
  ensures  *b == \old(*b);
*/
void incr_a_by_b(int* a, int const* b){
  *a += *b;
}

Si nous demandons à WP de prouver cette fonction, nous obtenons le résultat suivant :

Échec de preuve : risque d’aliasing

La raison est simplement que rien ne garantit que le pointeur a est bien différent du pointeur b. Or, si les pointeurs sont égaux,

  • la propriété *a == \old(*a) + *b signifie en fait *a == \old(*a) + *a, ce qui ne peut être vrai que si l’ancienne valeur pointée par a était 0, ce qu’on ne sait pas,
  • la propriété *b == \old(*b) n’est pas validée car potentiellement, nous la modifions.

Pourquoi la clause assign est-elle validée ?

C’est simplement dû au fait, qu’il n’y a bien que la zone mémoire pointée para qui est modifiée étant donné que si a != b nous ne modifions bien que cette zone et que si a == b, il n’y a toujours que cette zone, et pas une autre.

Pour assurer que les pointeurs sont bien sur des zones séparées de mémoire, ACSL nous offre le prédicat \separated(p1, ..., pn) qui reçoit en entrée un certain nombre de pointeurs et qui va nous assurer qu’ils sont deux à deux disjoints. Ici, nous spécifierions :

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
#include <limits.h>

/*@
  requires \valid(a) && \valid_read(b);
  requires \separated(a, b);
  assigns  *a;
  ensures  *a == \old(*a)+ *b;
  ensures  *b == \old(*b);
*/
void incr_a_by_b(int* a, int const* b){
  *a += *b;
}

Et cette fois, la preuve est effectuée :

Résolution des problèmes d’aliasing

Nous pouvons noter que nous ne nous intéressons pas ici à la preuve de l’absence d’erreur à l’exécution car ce n’est pas l’objet de cette section. Cependant, si cette fonction faisait partie d’un programme complet à vérifier, il faudrait définir le contexte dans lequel on souhaite l’utiliser et définir les pré-conditions qui nous garantissent l’absence de débordement en conséquence.

Comportements

Il peut arriver qu’une fonction ait divers comportements potentiellement très différents en fonction de l’entrée. Un cas typique est la réception d’un pointeur vers une ressource optionnelle : si le pointeur est NULL, nous aurons un certain comportement et un comportement complètement différent s’il ne l’est pas.

Nous avons déjà vu une fonction qui avait des comportements différents, la fonction abs. Nous allons la reprendre comme exemple. Les deux comportements que nous pouvons isoler sont le cas où la valeur est positive et le cas où la valeur est négative.

Les comportements nous servent à spécifier les différents cas pour les post-conditions. Nous les introduisons avec le mot-clé behavior. Chaque comportement se voit attribué :

  • un nom ;
  • les suppositions du cas que nous traitons, introduites par le mot clé assumes ;
  • la post-condition associée à ce comportement.

Finalement, nous pouvons également demander à WP de vérifier le fait que les comportements sont disjoints (pour garantir le déterminisme) et complets.

Les comportements sont disjoints si pour toute entrée de la fonction, elle ne correspond aux suppositions (assumes) que d’un seul comportement. Les comportements sont complets si les suppositions recouvrent bien tout le domaine des entrées.

Par exemple pour abs :

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
/*@
  requires val > INT_MIN;
  assigns  \nothing;

  behavior pos:
    assumes 0 <= val;
    ensures \result == val;

  behavior neg:
    assumes val < 0;
    ensures \result == -val;

  complete behaviors;
  disjoint behaviors;
*/
int abs(int val){
  if(val < 0) return -val;
  return val;
}

Pour comprendre ce que font précisément complete et disjoint, il est utile d’expérimenter deux possibilités :

  • remplacer la supposition de « pos » par val > 0 auquel cas les comportements seront disjoints mais incomplets (il nous manquera le cas val == 0) ;
  • remplacer la supposition de « neg » par val <= 0 auquel cas les comportements seront complets mais non disjoints (le cas val == 0) sera présent dans les deux comportements.

Même si assigns est une post-condition, à ma connaissance, il n’est pas possible de mettre des assigns pour chaque behavior. Si nous avons besoin d’un tel cas, nous spécifions :

  • assigns avant les behavior (comme dans notre exemple) avec tout élément non-local susceptible d’être modifié,
  • en post-condition de chaque behavior les éléments qui ne sont finalement pas modifiés en les indiquant égaux à leur ancienne (\old) valeur.

Les comportements sont très utiles pour simplifier l’écriture de spécifications quand les fonctions ont des effets très différents en fonction de leurs entrées. Sans eux, les spécifications passent systématiquement par des implications traduisant la même idée mais dont l’écriture et la lecture sont plus difficiles (nous sommes susceptibles d’introduire des erreurs).

D’autre part, la traduction de la complétude et de la disjonction devraient être écrites manuellement, ce qui serait fastidieux et une nouvelle fois source d’erreurs.

Modularité du WP

Pour terminer cette partie nous allons parler de la composition des appels de fonctions et commencer à entrer dans les détails de fonctionnement de WP. Nous allons en profiter pour regarder comment se traduit le découpage de nos programmes en fichiers lorsque nous voulons les spécifier et les prouver avec WP.

Notre but sera de prouver la fonction max_abs qui renvoie les maximums entre les valeurs absolues de deux valeurs :

1
2
3
4
5
6
int max_abs(int a, int b){
  int abs_a = abs(a);
  int abs_b = abs(b);

  return max(abs_a, abs_b);
}

Commençons par (sur-)découper nos précédentes fonctions en couples headers/source pour abs et max. Cela donne pour abs :

Fichier abs.h :

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
#ifndef _ABS
#define _ABS

#include <limits.h>

/*@
  requires val > INT_MIN;
  assigns  \nothing;

  behavior pos:
    assumes 0 <= val;
    ensures \result == val;

  behavior neg:
    assumes val < 0;
    ensures \result == -val;

  complete behaviors;
  disjoint behaviors;
*/
int abs(int val);

#endif

Fichier abs.c

1
2
3
4
5
6
#include "abs.h"

int abs(int val){
  if(val < 0) return -val;
  return val;
}

Nous découpons en mettant le contrat de la fonction dans le header. Le but de ceci est de pouvoir, lorsque nous aurons besoin de la fonction dans un autre fichier, importer la spécification en même temps que la déclaration de celle-ci. En effet, WP en aura besoin pour montrer que les appels à cette fonction sont valides.

Nous pouvons créer un fichier sous le même formatage pour la fonction max. Dans les deux cas, nous pouvons ré-ouvrir le fichier source (pas besoin de spécifier les fichiers headers dans la ligne de commande) avec Frama-C et remarquer que la spécification est bien associée à la fonction et que nous pouvons la prouver.

Maintenant, nous pouvons préparer le terrain pour la fonction max_abs. Dans notre header :

1
2
3
4
5
6
#ifndef _MAX_ABS
#define _MAX_ABS

int max_abs(int a, int b);

#endif

Et dans le source :

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
#include "max_abs.h"
#include "max.h"
#include "abs.h"

int max_abs(int a, int b){
  int abs_a = abs(a);
  int abs_b = abs(b);

  return max(abs_a, abs_b);
}

Et ouvrir ce dernier fichier dans Frama-C. Si nous regardons le panneau latéral, nous pouvons voir que les fichiers header que nous avons inclus dans le fichier abs_max.c y apparaissent et que les contrats de fonction sont décorés avec des pastilles particulières (vertes et bleues) :

Le contrat de max est valide par hypothèse

Ces pastilles nous disent qu’en l’absence d’implémentation, les propriétés sont supposées vraies. Et c’est une des forces de la preuve déductive de programmes par rapport à certaines autres méthodes formelles, les fonctions sont vérifiées en isolation les unes des autres.

En dehors de la fonction, sa spécification est considérée comme étant vérifiée : nous ne cherchons pas à reprouver que la fonction fait bien son travail à chaque appel, nous nous contenterons de vérifier que les pré-conditions sont réunies au moment de l’appel. Cela donne donc des preuves très modulaires et donc des spécifications plus facilement réutilisables. Évidemment, si notre preuve repose sur la spécification d’une autre fonction, cette fonction doit-elle même être vérifiable pour que la preuve soit formellement complète. Mais nous pouvons également vouloir simplement faire confiance à une bibliothèque externe sans la prouver.

Finalement, le lecteur pourra essayer de spécifier la fonction max_abs.

La spécification peut ressembler à ceci (j’ai mis l’implémentation avec pour rappel) :

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
/*@
  requires a > INT_MIN;
  requires b > INT_MIN;

  assigns \nothing;

  ensures \result >= 0;
  ensures \result >= a && \result >= -a && \result >= b && \result >= -b;
  ensures \result == a || \result == -a || \result == b || \result == -b;
*/
int abs_max(int a, int b){
  int abs_a = abs(a);
  int abs_b = abs(b);

  return max(abs_a, abs_b);
}

Pendant cette partie, nous avons vu comment spécifier les fonctions par l’intermédiaire de leurs contrats, à savoir leurs pré et post-conditions, ainsi que quelques fonctionnalités offertes par ACSL pour exprimer ces propriétés. Nous avons également vu pourquoi il est important d’être précis dans la spécification et comment l’introduction des comportements nous permet de ne pas surcharger l’écriture pour autant.

En revanche, nous n’avons pas encore vu un point important : la spécification des boucles. Avant d’entamer cette partie, nous devrions regarder plus précisément comment fonctionne l’outil WP.