Greffons de génération automatique d'informations synthétiques sur le code analysé.
Début : M10
Fin : M16
Responsable : CEA
Participants : CEA, INRIA, IRISA
Ce sous-projet se propose de donner un cadre d'analyse par interprétation et de l'utiliser pour implanter des analyses classiques indispensables au reste de l'outil.
Le premier objectif de ces analyses est de fournir automatiquement une aide à la compréhension du programme analysé à l'utilisateur.
Le second objectif est de calculer des informations qui simplifient le travail des autres greffons. Parmi les informations que nous souhaitons calculer, on compte les valeurs des variables, la résolution des pointeurs, et des pointeurs de fonctions, l'accessibilité de certaines branches du code (code mort), les dépendances fonctionnelles entre les variables...
Ces informations sont absolument essentielles pour les autres sous-projets, mais ne seront pas calculées à l'aide de techniques innovantes. En particulier, on utilisera des treillis d'interprétation abstraite classiques en analyse de programmes.
Le projet LANDE de l’IRISA interviendra dans ce sous-projet pour la mise au point d’un modèle à contraintes de programmes C permettant l’extraction de propriétés de sécurité sur la manipulation des pointeurs. Ce modèle, dont une première version est d'ores et déjà disponible, ne traite qu’une classe extrêmement restreinte de pointeurs C et l’objectif de ce travail consistera à étendre le modèle ainsi que les propriétés abordées. La piste suivie consistera à bénéficier des résultats d’une analyse inter-procédurale de pointeurs ou d’une analyse de forme pour enrichir la modélisation à contraintes du programme et de son environnement d’exécution. Des propriétés telles que celles caractérisant l’absence de déréferencement de pointeurs nuls, seront extraites dans le langage de spécification défini par le CEA, de sorte à favoriser l’inter-opérabilité des outils dans le projet. De manière plus prospective, la combinaison d’analyses statique et dynamique concernant la manipulation des pointeurs en C pourrait permettre de lever certaines des difficultés inhérentes à ce type de construction et ouvrir ainsi la voie d’un nouveau type d’analyse qui pourrait se généraliser à d’autres domaines. Il est à noter que l’absence actuelle de formalismes permettant de décrire de manière précise les résultats d’analyses dynamiques complique l’étude d’une telle approche. Nous pensons que la modélisation originale des programmes sous forme de systèmes de contraintes offre un cadre générique idéal pour l’étude d’approches hybrides qui combineraient analyses statique et dynamique mais ceci reste à démontrer. De part la nature très prospective de ce sujet, nous envisageons le lancement d’une thèse sur ce thème dans le cadre du projet.
T3.0 Étude de besoin et identification d'exemples caractéristiques
En utilisant les résultats du sous-projet 1, nous identifierons la précision des interprétations abstraites qui est la plus pertinente en terme de rapport coût de calcul/information.
T3.1 Analyse de valeurs par des techniques d'interprétation abstraite, dans des domaines d'intervalles d'entiers et d'identificateur de case mémoire.
Les techniques utilisées seront de même nature que dans les outils traditionnels utilisant l'interprétation abstraite. L'expérience des acteurs majeurs dans ce domaine (Polyspace, Astrée) démontre la pertinence de cette approche.
T3.2 Analyse des variables modifiées et de leurs dépendances champs par champs pour les structures.
Les résultats de l'analyse de la tâche T3.1 seront utilisés pour la résolution des pointeurs.
Ce sujet a déjà fait l'objet d'une étude de faisabilité par le CEA dont les conclusions étaient positives.
T3.3 Extraction de propriété de sécurité des programmes
Cette sous-tâche se fera en parallèle avec le reste du projet étant donnée sa nature très prospective et débouchera sur une thèse.
T3.4 Si le besoin s'en fait sentir, utilisation de treillis relationnels pour pallier les limitations rencontrées dans T3.1 pendant les expérimentations sur les cas réels (selon les besoins, octogones, treillis de relations linéaires,...).
Nous fournirons un rapport sur l'exécution du prototype sur les exemples industriels et nous évaluerons le niveau de détail fourni par les analyses. Le risque d'échec est nul pour les tâches 0, 1 et 2 puisque nous nous appuierons sur des techniques classiques éprouvées qui ne demandent que des efforts de développement et des réglages. Les tâches 3 et 4 sont clairement plus exploratoires mais leur échec ne compromettrait pas le déroulement projet.
Tâche |
Resp. |
Début |
Fin |
Charge (homme/mois) |
Délivrables |
||||||
---|---|---|---|---|---|---|---|---|---|---|---|
CEA |
INRIA |
IRISA |
DA |
AF |
SVDO |
FT |
|||||
T3.0 |
CEA |
M10 |
M11 |
2 |
2 |
|
|
|
|
|
Rapport Exemples extraits de code industriels représentatifs |
T3.1 |
CEA |
M11 |
M13 |
6 |
6 |
|
|
|
|
|
Rapport de spécifications Prototype |
T3.2 |
CEA |
M13 |
M15 |
4 |
12 |
|
|
|
|
|
Rapport de spécification Documentation Prototype |
T3.3 |
IRISA |
M0 |
M36 |
|
|
48 |
|
|
|
|
Rapport Prototype Thèse |
T3.4 |
CEA |
M15 |
M16 |
2 |
|
|
|
|
|
|
Rapport de spécification |