Le logiciel Coccinelle, un outil de correspondance et transformation en langage C, a été réalisé en 2008 par l’actuelle équipe de recherche Whisper (Équipe de projet commune entre l’Inria et la Sorbonne Université) pour faciliter les spécifications et automatisations de l'évolution du noyau Linux. La nouvelle contribution de Coccinelle fut d'autoriser les développeurs à écrire des règles de manipulation de code directement dans la structure syntaxique du code, via la généralisation de de patch. Au fil des années, l’outil Coccinelle a été largement utilisé dans le développement du noyau Linux, aboutissant à plus de 6000 commits, et a trouvé sa place dans le processus de développement de Linux.
Caractéristiques de l'outil Coccinelle thumb|alt=Coccinelle| Fig. 1 Moteur de transformation Coccinelle|upright=1 Coccinelle est un programme de correspondance et un outil de transformation pour le code en C. Il est utilisé pour la découverte de bugs dans les évolutions du noyau Linux et développé par Lawall, Muller et coll. depuis 2008. Coccinelle a été à l'origine conçu pour cibler les évolutions collatérales des pilotes de périphériques Linux, où le but était de mettre à jour le code client en réponse à un changement de l'interface d'une bibliothèque. Coccinelle a aussi été largement utilisé pour trouver et corriger des bugs. L'outil Coccinelle est conçu pour être facile à utiliser par les développeurs de logiciels, sans exiger d’expertise dans l'analyse de programme, la transformation de programme, ou la conception interne de l'outil lui-même. À cette fin, l’outil de transformation Coccinelle et les règles de découverte de bug sont exprimées en utilisant une syntaxe qui est proche de celle d’un patch. Étant donné que Coccinelle tient compte de la sémantique du langage C, notamment sa structure de contrôle, Lawall et coll. font référence à l’outil de transformation Coccinelle ou à la spécification de recherche de bug comme un patch sémantique (semantic patch). En 2014, presque 2000 patchs acceptés dans le noyau Linux ont été créées en utilisant Coccinelle, y compris environ 700 patchs créés par 90 développeurs n’appartenant pas au groupe de recherche de Coccinelle.
Coccinelle est conçu autour d'un langage dédié (en anglais, domain-specific language ou DSL), SmPL (Semantic Patch Language), pour exprimer des changements en termes d'une forme abstraite de patch, mentionné comme un patch sémantique. À la différence d’un patch classique, qui est lié aux lignes et fichiers spécifiques dans le code source, un patch sémantique simple peut mettre à jour tous les emplacements appropriés dans la base de code entière.
La figure 1 montre les étapes principales exécutées par le moteur de Coccinelle. Les points clefs dans sa conception sont les stratégies pour (i) faire face au préprocesseur C (cpp), être capables de préserver le style de code original, (ii) faire l’ abstraction de la syntaxe et des variations de structure de contrôle et (iii) appliquer le code de transformation efficacement. Le résultat de correspondance de la formule CTL avec le CFG est une collection de nœuds où une transformation est requise, le fragment du patch sémantique qui correspond à ces nœuds et les liens de métavariable. Le moteur propage alors les - et + des annotations sur le patch sémantique aux correspondants aux nœuds correspondants du CFG, et ensuite à l’arbre de syntaxe abstraite. Le moteur l’arbre de syntaxe abstraite en supprimant n'importe quel token annoté avec - et en ajoutant les + du patch sémantique, comme approprié. N'importe quel métavariables dans l’ajout supplémentaire des + dans le code sont instanciés selon les liens établis par le processus de correspondance CTL.
Les méthodes utilisées par l'outil Coccinelle: Isomorphisme Les isomorphismes assimilent sémantiquement des fragments de code équivalents, pour extraire des variations dans le style de code, et l'utilisation de logique temporelle pour extraire des variations dans les chemins d'exécution spécifiques des périphériques. Le résultat de généricité implique qu’un simple patch sémantique de moins de 50 lignes peut suffire pour mettre à jour plus de 500 fichiers.
CTL () Le patch sémantique SmPL est compilé dans une formule de logique temporelle (CTL). La correspondance de la formule avec le modèle est alors mise en œuvre utilisant une variante d'un modèle standard vérifiant l'algorithme. Tandis que CTL est probablement peu familier à la plupart des mainteneurs de pilote, il sert seulement comme un langage d’ assembleur, que le mainteneur de pilote ne doit pas lire ou comprendre.
CFG (Graphe de flot de contrôle) Padioleau et coll. utilisent des chemins dans le graphe de flux de contrôle (CFG), comme une approximation du patron d'opérations exécutées au temps d(exécution par un pilote. Ainsi, une séquence de termes dans un patch sémantique SmPL correspond à une séquence de termes du langage C le long d'un chemin dans le CFG.
Vérification de modèles Pour raisonner en graphes de flux de contrôle, Padioleau et coll. ont basé le moteur Coccinelle sur la technologie vérification de modèles, qui est orienté graphe. Dans cette approche, chaque au plus haut niveau de code source C (par exemple, une ou une macro-définition) est traduit dans un graphique de flux de contrôle.
Stratégie d'adaptation au préprocesseur C (cpp) Un analyseur syntaxique qui est capable d’adapter beaucoup d'utilisations des directives du préprocesseur C. Les commentaires et les sont maintenus où c’est possible dans le code transformé pour préserver la capacité de comprendre et maintenir le pilote. Parce que les évolutions collatérales sont justes un pas dans la maintenance en cours d'un pilote de périphérique Linux, le moteur Coccinelle doit générer un code qui est lisible et dans le style du code source original, y compris l'utilisation de constructions cpp. En outre, une évolution collatérale peut impliquer des constructions cpp. Donc, Coccinelle fait l'analyse syntaxique du code C, sans étendre des directives du préprocesseur cpp, pour qu'elles soient préservés tant dans le processus de transformation que dans le code généré.
Origines du projet Coccinelle Dans les systèmes d’exploitation (OS) modernes, les pilotes des périphériques peuvent constituer 70% du code source. Le code du pilote est lui aussi fortement dépendant du reste du code source de l’OS, pour ses fonctions ainsi que la structure de données définie dans le noyau et les bibliothèques de support des pilotes. En conséquence, n’importe quels changements des interfaces du noyau ou des bibliothèques de support des pilotes vont probablement déclencher des modifications dans le code du périphérique pour rétablir son bon fonctionnement. Yoann Padioleau, Julia Lawall et Gilles Muller font référence, en , à ces modifications comme des évolutions collatérales. Elles peuvent entraîner des réorganisations de code substantielles, qui prennent du temps et sont sujettes aux erreurs. Le besoin d'évolutions collatérales peut donc gêner l'évolution de l'OS en pratique. C’est ainsi que Padioleau, Lawall et Muller ont commencé à examiner les problèmes révélés par ces évolutions collatérales dans le contexte de Linux.
En , ils ont proposé un langage de transformation déclaratif, SmPL (Semantic Patch Language), pour exprimer précisément les évolutions collatérales des pilotes de périphériques Linux. La communauté des programmeurs Linux est habitués à l'échange, la lecture et la manipulation de patchs qui fournissent un rapport des changements précédemment exécutés. Padioleau et coll. ont ainsi axé la syntaxe de SmPL sur la notation de fichier de patch. À la différence des patchs habituels, qui enregistrent les changements dans des fichiers spécifiques, SmPL peut décrire les transformations génériques qui s'appliquent aux évolutions collatérales multiples. Ce fut une première étape dans le projet de développer l’outil de transformation Coccinelle, fournissant une assistance automatisée pour exécuter des évolutions collatérales. Cette assistance comprend le langage SmPL pour spécifier les évolutions collatérales et un moteur de transformation pour les appliquer au code des pilotes de périphériques. Le projet de développement de Coccinelle est soutenu par le Conseil de Recherche danois (Danish Research Council for Technology and Production) des universités de Copenhague et Aalborg et l’institut national de recherche en sciences et technologies du numérique (Inria) en France.
Les évolutions collatérales Le problème des évolutions collatérales L’équipe Whisper a évalué les divers aspects du besoin d'évolutions collatérales dans les pilotes de périphériques Linux, utilisant des outils d'extraction de données ad hoc qu’ils ont développé. Ces résultats montrent que les bibliothèques de support des pilotes et les fichiers spécifiques des périphériques qui en dépendent sont nombreux et leurs relations complexes. Yoann Padioleau, René R. Hansen, Julia Lawall et Gilles Muller ont ainsi identifié en 2006, dans la version 2.6.13 du noyau Linux, 150 bibliothèques de support de pilotes et presque 2000 fichiers spécifiques des périphériques. Un fichier spécifique de périphérique peut utiliser jusqu'à 59 fonctions de bibliothèque différentes. Plutôt que de devenir plus stable, cette base de code se développe de plus en plus rapidement. Ils ont constaté que le nombre d'évolutions dans les éléments d'interface croient fortement, avec 300 évolutions probables dans le code de Linux 2.2 et plus de 1200 dans Linux 2.6 jusqu'à Linux 2.6.13. Certaines de ces évolutions déclenchent des évolutions collatérales dans presque 400 fichiers. Entre Linux 2.6.9 et Linux 2.6.10, plus de de code périphériques spécifique, affectées par des évolutions collatérales, ont été trouvées.
Les divers aspects du processus des évolutions collatérales Avant l’arrivée de l’outil Coccinelle, ces évolutions suivaient ce procédé typique : Quand un développeur fait un changement dans une bibliothèque Linux interne qui a un impact sur une API, il met manuellement à jour tout le code spécifique du périphérique dans l'arborescence source Linux, basé sur sa compréhension de l'évolution et son approche des pilotes concernés. Ensuite, les mainteneurs des nombreux pilotes extérieurs à l'arborescence source de Linux exécutent l'évolution collatérale dans leurs propres codes. Ces mainteneurs de pilotes n'ont pas la connaissance immédiate de cette évolution et doivent ainsi déduire comment elle s'applique à leurs codes depuis n'importe quels commentaires de code disponibles, de mails informels et de patchs souvent volumineuses. Finalement, des utilisateurs motivés appliquent les évolutions collatérales pour coder ce qui a été omis par le développeur de bibliothèque ou le mainteneur de pilotes. Et ce cas pose problème au mainteneur de pilotes car ces utilisateurs ne peuvent avoir aucune expérience avec l'évolution collatérale ou le code des pilotes.
Comme Linux est un OS open source, beaucoup de programmeurs différents contribuent à son développement. En effet, les mainteneurs de pilote ne sont souvent pas des experts du noyau, mais plutôt des experts d’un périphérique donné ou même des utilisateurs ordinaires qui constatent que leur matériel n'est pas correctement supporté. Parce que les développeurs qui mettent à jour le noyau et les bibliothèques de support des pilotes ne partagent pas souvent de langage commun et une expertise avec le mainteneur de périphérique, la documentation d'évolutions collatérales complexes est souvent incomplète.
Les précédentes tentatives de résolution La réutilisation de pilotes de périphériques a été tentée par la restructuration des systèmes d'exploitation utilisant une approche de micro-noyau. Goel et Duchamp ont émulé des pilotes de périphériques de Linux sur un micro-noyau Mach 4.0, avec des résultats de performance décevants .