Analysis of code quality via a logical approach and application to robotics

La qualité d'un code informatique passe à la fois par sa correction fonctionnelle mais aussi par des critères de lisibilité, compréhension et maintenabilité. C'est une problématique actuellement importante en robotique où de nombreux frameworks open-source se diffusent mal dans l'industrie en raison d'incertitudes sur la qualité du code. Les outils d'analyse et de recherche de code sont efficaces pour améliorer ces aspects. Il est important qu'ils laissent l'utilisateur spécifier ce qu'il recherche afin pouvoir prendre en compte les spécificités de chaque projet et du domaine. Il existe deux principales représentations du code : son arbre de syntaxe abstraite (Abstract Syntax Tree en anglais, ou AST) et le graphe de flot de contrôle (Control Flow Graph en anglais, ou CFG) des fonctions qui sont définies dans le code. Les mécanismes de spécification existants utilisent exclusivement l'une ou l'autre de ces représentations, ce qui est dommage car elles offrent des informations complémentaires. L'objectif de ce travail est donc de développer une méthode de vérification de la conformité du code avec des règles utilisateurs qui puissent exploiter conjointement l'AST et le CFG. La méthode repose sur une nouvelle logique développée dans le cadre de ces travaux : FO++ , qui une extension temporelle de la logique du premier ordre. Cette logique a plusieurs avantages. Tout d'abord, elle est indépendante de tout langage de programmation et dotée d'une sémantique formelle. Ensuite, elle peut être utilisée comme moyen de formaliser les règles utilisateurs une fois instanciée pour un langage de programmation donné. Enfin, l'étude de son problème de model-checking offre un mécanisme de vérification automatique et correct de la conformité du code. Ces différents concepts ont été implémentés dans Pangolin, un outil pour le langage C++. Étant donné le code à vérifier et une spécification (qui correspond à une formule de FO++ , écrite dans le langage utilisateur de Pangolin), l'outil indique si oui ou non le code respecte la spécification. Il offre de plus un résumé synthétique de l'évaluation pour pouvoir retrouver le potentiel code fautif ainsi qu'un certificat de correction du résultat. Pangolin et FO++ ont trouvé une première application dans le domaine de la robotique via l'analyse de la qualité des paquets ROS et formalisation d'un design-pattern spécifique à ROS. Une seconde application plus générale concerne le développement de programme en C++ avec la formalisation de diverses règles de bonnes pratiques pour ce langage. Enfin, on montre comment il est possible de spécifier et vérifier des règles intimement liées à un projet en vérifiant des propriétés sur Pangolin lui-même.The quality of source code depends not only on its functional correctness but also on its readability, intelligibility and maintainability. This is currently an important problem in robotics where many open-source frameworks do not spread well in the industry because of uncertainty about the quality of the code. Code analysis and search tools are effective in improving these aspects. It is important that they let the user specify what she is looking for in order to be able to take into account the specific features of the project and of the domain. There exist two main representations of the source code : its Abstract Syntax Tree (AST) and the Control Flow Graph (CFG) of its functions. Existing specification mechanisms only use one of these representations, which is unfortunate because they offer complementaty information. The objective of this work is therefore to develop a method for verifying code compliance with user rules that can take benefit from both the AST and the CFG. The method is underpinned by a new logic we developed in this work : FO++ , which is a temporal extension of first-order logic. Relying on this logic has two advantages. First of all, it is independent of any programming language and has a formal semantics. Then, once instantiated for a given programming language, it can be used as a mean to formalize user provided properties. Finally, the study of its model-checking problem provides a mechanism for the automatic and correct verification of code compliance. These different concepts have been implemented in Pangolin, a tool for the C++ language. Given the code to be checked and a specification (which corresponds to an FO++ formula, written using Pangolin language), the tool indicates whether or not the code meets the specification. It also offers a summary of the evaluation in order to be able to find the code that violate the property as well as a certificate of the result correctness. Pangolin and FO++ have been applied to the field of robotics through the analysis of the quality of ROS packages and the formalization of a ROS-specific design-pattern. As a second and more general application to the development of programs in C++, we have formalized various good practice rules for this language. Finally, we have showed how it is possible to specify and verify rules that are closely related to a specific project by checking properties on the source code of Pangolin itself