Ours & Hippy — le blog

Quand il est sorti sur Lambda the Ultimate, j’ai lu avec intérêt l’article Finding and Understanding Bugs in C Compilers (PDF, 12 pages), de Xuejun Yang, Yang Chen, Eric Eide, et John Regehr, 2011. Je compte en faire un petit résumé, mentionner quelques points de l’article qui m’ont intéressé, et surtout faire une longue digression sur un sujet très légèrement abordé par l’article mais qui m’intéresse beaucoup : les rapports entre tests de fonctionnement et preuves de correction dans le développement logiciel.

Le cœur de l’article

L’idée de base est de générer aléatoirement des programmes C, pour trouver des bugs dans les compilateurs. L’efficacité de la technique repose sur deux bonnes idées, une déjà connue et une nouvelle.

Concrètement, générer des programmes aléatoires permet de repérer les plantages (le compilateur lance une exception au lieu de produire un résultat), mais si le compilateur produit du code, comment savoir s’il est correct ? Alors déjà, il faut bien comprendre qu’on ne regarde pas directement le programme assembleur produit pour savoir s’il est correct ; cela demanderait de savoir raisonner sur du code assembleur quelconque, ce qui est bien trop compliqué. Non, on exécute le programme généré, et on regarde le résultat de l’exécution (donc le résultat du résultat du générateur de programmes…).

Que peut-on déduire du résultat de cette exécution ? D’habitude, on génère des tests dont on connaît le résultat (« l’exécution de ce programme va afficher 3 »), mais là on ne sait pas forcément prévoir le résultat correct à partir du programme C généré (pour cela, il faudrait dans le cas général avoir à disposition un compilateur C sans bugs…). C’est là qu’entre en jeu la première idée : on va comparer les sorties des différents compilateurs (GCC, Clang/LLVM, ICC, MSVC…), et supposer l’existence d’un bug quand ils se contredisent. Comme ça, on n’a pas besoin d’un « oracle » qui connaît la bonne réponse. C’est le principe des « tests différentiels » (differential testing).

Mais ce n’est pas aussi simple qu’il y paraît. Dans un grand nombre de cas, quand le programme en entrée n’est pas un « bon » programme, la norme ne définit pas uniquement le comportement que les compilateurs doivent adopter. Par exemple, si le programme commet une erreur grave comme une divison par 0 ou un accès hors d’un tableau, les compilateurs sont autorisés à produire un programme qui fait n’importe quoi (undefined behavior). Dans d’autres cas, il y a plusieurs choix possibles, comme par exemple pour l’ordre d’évaluation, et la norme ne tranche pas entre les différentes possibilités, elle laisse cet aspect non spécifié (unspecified behavior). Les auteurs de l’article ont recensé, dans la norme C99, 191 situations de undefined behavior et 52 cas de unspecified behavior. Si on prend un code C qui contient de tels comportements mal définis, deux compilateurs peuvent produire des résultats différents et être tout de même corrects, puisqu’ils respectent la norme.

La deuxième bonne idée de l’article est alors de vérifier que les programmes générés ne contiennent pas de comportement mal déterminé. Pour cela, ils utilisent une combinaison d’analyse statique du programme et des tests à l’exécution.

Les tests n’utilisent pas toutes les fonctionnalités du langage C, mais seulement un sous-ensemble raisonnable du langage pour lequel ils ont su mettre ces analyses au point. Ils ont sorti le grand jeu : data flow analysis pour déterminer le comportement des pointeurs, typage (qui prend en compte const et volatile), analyses d’effets… Il faut choisir des analyses qui rejettent tous les programmes mal définis ; mais elles rejettent alors nécessairement, on ne peut pas tout avoir dans la vie, certains programmes bien définis. Plus l’analyse est fine, moins elle rejette de programmes corrects, plus ils génèrent des tests compliqués et plus ils trouvent de bugs.

En pratique, ça marche bien : ils ont trouvé « des centaines de bugs » dans les compilateurs testés, dont 79 dans GCC et 202 dans LLVM ; certains des bugs trouvés sont détaillés dans l’article. Ces derniers correspondent en général à des optimisations trop aggressives des compilateurs, qui négligent certains cas et changent la sémantique, ou parfois à des erreurs d’implémentation dans le code de l’optimisation.

Quelques points de détail

Leur outil s’est révélé plus efficace quand il génère de gros programmes : « the largest number of bugs is found at a surprisingly large program size: about 81 KB ». Il n’y a pas de méthode complètement automatique pour réduire un programme-test en un programme plus petit qui préserve le bug sans introduire de comportement mal spécifié ; ils ont dû faire ça à la main. Ça pourrait s’automatiser, mais c’est sans doute un problème aussi difficile que la génération initiale de tests corrects.

Ils profitent de leur article pour critiquer gentiment certaines méthodologies de test, en particulier la métrique de couverture de code (code coverage). C’est une pratique très répandue dans l’industrie du test (et utilisée comme critère par exemple par les autorités de certification de code critique), qui consiste à utiliser un jeu de tests tel que chaque instruction du programme est exécutée au moins une fois (c’est le critère instruction coverage ; il y a d’autres critères de couverture, cf. Wikipédia) ; le terme « couverture » désigne ici la proportion du code du programme qui est exécuté au moins une fois par la batterie de tests. Ils montrent que leurs tests générés aléatoirement n’améliorent pas la couverture obtenue par les batteries de tests déjà existantes des compilateurs, c’est-à-dire qu’ils ont trouvé plein de bugs sans améliorer la couverture.

Enfin, ils ont même évalué le « retour sur investissement » de leur méthode : ils ont additionné les salaires de tous les chercheurs et étudiants qui ont travaillé sur cette méthode, le coût de l’équipement, de l’administration, etc., et obtenu un « coût » de $1000 par bug. Visiblement c’est considéré comme très rentable dans cette industrie (on imagine que les bugs dans les compilateurs peuvent être critiques et très difficiles à trouver) ; et maintenant que les outils sont développés, ils peuvent être utilisés à bien moindre coût.

Je suis quand même étonné de la quantité de bugs qui persistent dans ces compilateurs utilisés industriellement. Il ne s’agit pas de nouvelles fonctionnalités C99 qui viennent d’être implémentées (leur outil ne les prend pas en compte) mais de comportements bizarres sur un overflow dans une optimisation arithmétique, le genre de chose qu’on teste depuis des années. Pour la petite touche historique, ils mentionnent la longue histoire des tests par génération aléatoire de programme, qui a commencé en 1962 sur des compilateurs COBOL.

Le point le plus difficile de leur travail est la conception de ces analyses qui évitent les comportements mal définis et leur intégration dans le générateur de programmes. On peut se demander si cette difficulté est inhérente au langage C, et s’il faut prendre cet aspect en compte lors de la conception d’un langage de programmation : définir une sémantique déterministe rend le compilateur plus facile à tester. Sur la discussion de Lambda the Ultimate, un membre indique que les générateurs aléatoires de programme ont été très utiles pour les implémentations du langage Common Lisp ; est-ce lié à un plus petit nombre de comportement mal définis dans ce langage ?

Pour ma part, l’idée qu’un programme puisse se mettre à faire absolument n’importe quoi en cas d’erreur me semble désastreuse, mais je suis plutôt favorable à certains unspecified behavior, comme par exemple le fait de ne pas spécifier l’ordre d’évaluation des arguments d’une fonction, pour décourager les programmeurs d’écrire du mauvais code qui reposerait sur cet ordre. Mais des gens plus expérimentés que moi ne sont pas d’accord ; je crois que certains des concepteurs de Caml, par exemple, considèrent comme une erreur le fait de ne pas avoir fixé un ordre d’évaluation. La question n’est pas tranchée.

CompCert, tests et preuves de correction

L’article mentionne le compilateur CompCert, un compilateur prouvé correct écrit en Coq. Je ne suis pas tout à fait d’accord avec le traitement qui en est fait, et je voudrais développer un peu ce point.

The striking thing about our CompCert results is that the middle- end bugs we found in all other compilers are absent. As of early 2011, the under-development version of CompCert is the only compiler we have tested for which Csmith cannot find wrong-code errors. This is not for lack of trying: we have devoted about six CPU-years to the task. The apparent unbreakability of CompCert supports a strong argument that developing compiler optimizations within a proof framework, where safety checks are explicit and machine-checked, has tangible benefits for compiler users.

Aucun bug trouvé dans un compilateur certifié. C’est normal, mais vous étiez quand même un peu inquiets, non ? Il se trouve qu’ils ont en fait trouvé des bugs, avant « early 2011 », dans le front-end de Coq, qui utilise CIL, une bibliothèque externe codée en OCaml qui parse le code C et lui applique quelques transformations. Cette bibliothèque non vérifiée semble effectivement contenir quelques bugs. Depuis, Xavier Leroy a réécrit cette partie de CompCert pour rétrécir la partie non-prouvée ; mais il en reste un peu, car pour l’instant on ne sait même pas vraiment comment spécifier un parseur (décrire formellement son comportement).

Les auteurs du présent article concluent en substance : bon, la vérification c’est très sympa et ça enlève plein de bugs, mais ça reste complémentaire au test, parce qu’il y a toujours des petits détails qui coincent. On se souvient de la célèbre phrase de Knuth : « Beware of bugs in the above code ; I have only proved it correct, not tried it. » Mais fondamentalement, ils ne semblent pas vraiment convaincus ; ils font aussi remarquer, à juste titre, qu’on est encore loin d’avoir un compilateur certifié pour un langage aussi délirant que C++0X (la prochaine norme du langage C++, en cours de finalisation ces mois-ci).

Cette attitude sceptique par défaut se retrouve aussi chez les autorités de certification de logiciel critique. Les gens qui travaillent là-bas sont chargés d’expertiser du logiciel pour vérifier son respect de normes de qualité très strictes, permettant ensuite l’utilisation dans les avions, voitures, centrales nucléaires, etc. Les expertises consistent essentiellement à analyser le code et les tests qui l’accompagnent mais aussi le processus de conception, la documentation produite, etc. Il y a des critères de tests divers ; l’idée n’est même pas vraiment de vérifier que les tests passent correctement (c’est une évidence), mais que leur présence montre l’existence d’une démarche qualité appropriée chez les gens qui ont écrit le code.

Ces autorités de certification n’ont pas d’expérience en vérification formelle : les outils d’analyse de programme sont déjà utilisés dans l’industrie pour trouver des erreurs, mais jusqu’à présent aucun programme n’était entièrement certifié. Les outils formels prouvaient par exemple l’absence d’overflow, mais pas un lien entre le code et une spécification. L’idée commence à germer et des questions se posent : quel degré de confiance accorder à un programme prouvé en Coq ? Une preuve remplace-t-elle la construction des jeux de tests (processus qui a sa part de coûts et de lourdeurs) ? Il y a un début de débat, mais la question est loin d’être tranchée, et ce sont des milieux évidemment assez conservateurs.

À l’opposé, j’ai rencontré des utilisateurs de Coq pour qui la réponse était claire : quand un programme est « prouvé en Coq », il ne peut évidemment pas contenir d’erreur, et il est inutile de le tester. Pour eux, le test est une méthode peu coûteuse (il est facile d’écrire un test) mais peu fiable (un test qui passe ne garantit en rien l’absence de bugs) de prendre confiance en la correction d’un logiciel, et la preuve formelle est une méthode coûteuse (il est très difficile d’écrire une preuve complète) mais absolument fiable.

Ce point de vue est malheureusement un leurre ; ce n’est pas un idéal qu’on veut atteindre un jour et pour lequel on fait des progrès, c’est tout simplement un état qui ne pourra jamais exister. La preuve formelle permet de s’assurer que tel théorème (théorème qui mentionne le programme que l’on veut vérifier) est absolument, mathématiquement juste. Mais le théorème peut être une trivialité qui dit « le programme marche, ou bien le programme ne marche pas ». Quand on a une preuve d’un théorème vérifiée par ordinateur, on est sûr que la preuve est juste, mais il faut toujours vérifier que le théorème est bien celui que l’on croit. On aurait très bien pu se tromper dans sa formulation (et c’est déjà arrivé en pratique), même si le fait d’écrire une preuve permet la plupart du temps de détecter des incohérences dans l’énoncé.

Je pense donc que l’idée de tester un programme prouvé n’est pas la bonne approche, et que les six ans de CPU n’ont pas été très utiles. On devrait plutôt essayer de tester la spécification établie par la preuve, l’énoncé du théorème de correction. Qu’est-ce que ça veut dire, tester une formule mathématique ? Je ne sais pas exactement, mais j’ai quelques idées. Par exemple, on pourrait montrer à la main qu’un système simple et faux ne vérifie pas cette spécification. On a inversé la situation : au lieu de tester le programme en disant « telle entrée est acceptée par le programme comme prévu », on teste la spécification en disant « la spécification rejette tel programme comme prévu ».

Bref, je pense que oui, il faut continuer à « tester » un programme prouvé correct, mais qu’on ne le teste pas de la même façon. En substance, prouver un programme revient à réduire sa « surface de confiance » : au lieu de devoir mettre en doute l’ensemble du programme (lire le code et se convaincre qu’il fait bien ce qu’on pense), on doit ausculter sa spécification qui est, espère-t-on, plus abstraite, plus simple et plus concise. Mais la possibilité d’erreur est toujours là, et elle ne disparaîtra jamais : il y aura toujours un gouffre entre la description mécanique du programme donnée à l’ordinateur et l’idée informelle que s’en font ses concepteurs et utilisateurs ; ce sont deux mondes différents.

Une force de la preuve formelle que je n’ai pas mentionnée est son aspect progressif. On peut commencer par ne rien montrer du tout sur un programme, puis prouver qu’il vérifie telle propriété plus ou moins simple (par exemple qu’il termine sur toutes les entrées bien formées), puis une autre propriété un peu plus subtile. Par exemple, pour un programme qui renvoie les racines d’un polynôme, on peut commencer par montrer que tous les résultats renvoyés sont bien des racines, car c’est nettement plus facile que de montrer que toutes les racines sont bien renvoyées. Petit à petit, on peut progresser vers la preuve de correction « totale » où la spécification décrit exactement ce que le concepteur aimerait que son programme fasse. Une autre façon de s’assurer d’une spécification est alors de vérifier qu’elle implique les énoncés plus faibles précédents ; par opposition aux tests précédents, c’est une forme de preuve de spécification.

De nombreux articles d’opinions ont été écrits sur la question de la vérification formelle des logiciels. Je vous recommande chaudement la lecture de Social Process and Proofs of Theorems and Programs, Richard De Millo, Richard Lipton et Alan Perlis, 1979. Cet article explique avec fermeté que la vérification formelle est un rêve qui n’existe pas en réalité, même chez les mathématiciens, et que nous n’arriverons jamais à prouver formellement de « vrais programmes ». Je ne suis pas d’accord, mais ça le rend d’autant plus intéressant à lire. Plus neutre, et moins pessimiste, j’ai apprécié le court article de vulgarisation Formal Proof – Theory and Practice, de John Harrison, 2008.