• # Coccinelle, userland

    Posté par . En réponse à la dépêche Sparse repasse à l'attaque. Évalué à 2.

    > Si Sparse n'est actuellement utilisé que par le noyau Linux,

    En fait il est déjà utilisé par quelques projets en espace utilisateur. A ma connaissance, qemu et xfsprogs intègrent des vérifications basées sur sparse. Le fait que ces deux projets soient fréquentés par des devs kernel n'est peut-être pas fortuit : pour avoir essayé sans succès d'utiliser sparse à partir de la "documentation" disponible, j'ai supposé qu'il fallait être soit super doué, soit déjà introduit par la connaissance de cas d'utilisations concrets (comme on en trouve dans le noyau). D'autre part les en-têtes de la glibc (et en pratique tout le /usr/include) produisent de copieux warnings, ce qui rends l'utilisation en espace utilisateur laborieuse. Bref, avec un peu plus de doc et d'exemples, et un solide système de filtres, sparse serait plus simple d'accès pour les "non kernel-hackers".

    Je profite de ce poste pour signaler Coccinelle, un analyseur statique mignon tout plein et oublié dans l'inventaire de la dépêche. Il est très facile à utiliser (il suffit généralement d'écrire des "patches sémantiques" de quelques lignes adaptés à ses besoins, cf. les exemples plus bas), et il ne nécessite pas d'annotations spécifiques dans le code cible.

    Coccinelle est un projet universitaire (franco-suédois), mais il a déjà donné des résultats très concrets, sous la forme idéale de nombreux patchs envoyés sur LKML corrigeant de vrais bugs (exemples : http://lkml.indiana.edu/hypermail/linux/kernel/0806.3/0094.h(...) , http://lkml.org/lkml/2009/9/22/198 , ...).

    Deux obstacles au succès de Coccinelle cependant : il est écrit en Objective Caml (sans jugement sur la pertinence technique de ce choix de langage, mais les utilisateurs de l'outil sont des développeurs C), et il incorpore son propre parseur C (ce qui l'expose à des problèmes de compatibilité en traitant des sources prévues pour gcc), à la différence de sparse, qui se branche facilement sur gcc ou llvm.

    # le site de Coccinelle
    http://coccinelle.lip6.fr

    # une introduction à Coccinelle par Val Aurora (anciennement Valerie Henson)
    http://lwn.net/Articles/315686/


    p.s.: en ce qui concerne la question de la licence de sparse :
    - Linus Torvalds donne une motivations spécifique sur le choix d'une licence incompatible avec la GPL, dans la FAQ de sparse. Il y explique qu'il souhaite (souhaitait) ainsi prendre le contrepied du parti prix monolithique de gcc (« I like the GPL, but as rms says, "Linus is just an engineer". I refuse to use a license if that license causes bad engineering decisions. I want the front-end to be considered a separate project ».
    cf.
    http://git.kernel.org/?p=linux/kernel/git/torvalds/sparse.gi(...)
    - Mais il reconnait que l'OSL n'est pas le meilleur choix :
    http://www.mail-archive.com/linux-sparse@vger.kernel.org/msg(...)
    - De toutes façons, Novafora (qui a hérité de la propriété intellectuelle de Transmeta) a accepté de re-licencer sous MIT il y a quelques mois :
    http://markmail.org/message/qijmu2cu4gbi74te