Greffon de spécialisation du code
Début : M9
Fin : M15
Responsable : CEA
Participants : CEA, DA, AF, SVDO
L'analyse de plusieurs logiciels industriels a fait apparaître l'utilisation croissante d'un caractère de généricité des codes et de spécialisation par le biais de fichiers de paramètres (valeurs de variables et fonctions pointées). Ainsi un logiciel de contrôle de moteur utilise une approche plate-forme indépendante du type de moteur, que ce soit essence ou diesel, avec prise en compte des différentes configurations possibles et des spécificités des constructeurs. Un logiciel de contrôle de réacteur nucléaire peut être instancié pour chaque réacteur, etc. Sans ces fichiers de paramètres, il est très difficile de dire quelque chose sur le logiciel. Les techniques de spécialisation de logiciel (slicing) sont donc nécessaires pour analyser ces applications. En effet la réduction du code permet de réduire mes efforts de preuves et de synthèse des propriétés. Elle peut mettre en évidence ce qui est réellement utile et essentiel pour une bonne compréhension du code.
L'objectif de ce sous-projet est de développer, dans l'infrastructure générique, un outil capable de transformer un code C initial, au regard de certains points de vue utilisateur, en un code C réduit sur lequel il est possible d'effectuer des analyses dont les résultats peuvent être transposés sur le code initial. Le code C transformé doit pouvoir de nouveau être analysé dans notre infrastructure. Les transformations réalisées visent la réduction de la complexité des analyses à effectuer afin de rendre leurs résultats plus pertinents. Pour chacune des transformations, une correspondance sémantique entre les deux codes doit être fournie afin de pouvoir transporter les propriétés obtenues sur un code vers l’autre code.
Ce greffon sera au centre de la méthodologie de vérification qui sera développée dans le sous-projet 8.
T5.0 Étude de besoin et identification d'exemples caractéristiques
L’objectif de cette tâche est pour le CEA de spécifier une interface du greffon répondant aux exigences révélées par les utilisateurs DA, AF et SVDO lors de l’étude des besoins et l’identification d'exemples caractéristiques issus de cas réels des utilisateurs. Ces exemples pourront servir de tests lors du développement du greffon.
T5.1 Propagation de constantes et élimination de code mort
Il s'agit d'exploiter les résultats fournis par l'analyse de valeurs de la tâche 3.1 afin de remplacer les expressions C constantes par leur valeur et d'éliminer le code inaccessible. L'utilisateur doit pouvoir choisir l'ensemble des constantes qu'il désire propager, ainsi que les zones où il autorise ces transformations. Le code C transformé se doit d'être comparable au code initial relativement à l'accessibilité en des points du code et de la valeur des variables en ces points. Par exemple, au sujet des zones non modifiables, la transformation assure qu'à chaque fois qu'un point de programme de ces zones est atteint avec le code initial, il l'est également avec le code transformé, et dans les mêmes conditions (les variables des deux codes ont les mêmes valeurs en ce point). De plus, la propagation des constantes doit se faire aussi dans les propriétés portant sur le code.
T5.2 Spécialisation de fonctions
La spécialisation d'une fonction consiste à remplacer un des appels donné à cette fonction par un appel à une nouvelle fonction ayant le même code afin de pouvoir y réaliser des transformations du type de celles réalisées par la tâche 5.1. La fonction obtenue correspond à une spécialisation de la fonction initiale, qui n'est valide que pour cet appel. Pour toute autre fonction du code initial, le code obtenu est comparable au code initial relativement à l'accessibilité des points de programmes, et de la valeur des variables. La spécialisation de fonctions permet d'avoir des résultats d'analyses plus précis en certains points du code, et conduit, par exemple, à propager des constantes dans les fonctions qui les appellent.
T5.3 Spécialisation en vue d'étudier un ensemble de variables particulier, une ligne de code particulière
Il s’agit d’éliminer les instructions du code C initial qui ne participent pas au calcul d’un ensemble donné de variables globales, à l'accessibilité en une ligne de code donnée, ou au calcul de la valeur d’un ensemble de variables en un point particulier du code. Le code obtenu assure par exemple, dans le cas de l’étude d’un ensemble de variables en un point du code donné, qu'à chaque fois que l’on atteint ce point avec le code initial, on l’atteint également avec le code réduit, avec pour ces variables, la même valeur. La réciproque est également vraie que pour les exécutions du code initial se terminant normalement.
T5.4 Évaluation sur des exemples réels
Des expérimentations du greffon seront effectuées par les utilisateurs DA, AF et SVDO sur des exemples réels afin de définir une méthodologie d’utilisation adaptée à leur processus de développement de leurs logiciels.
Ce projet sera un succès si les applications industrielles peuvent effectivement être spécialisées selon les critères définis par les partenaires industriels.
Tâche |
Resp |
Début |
Fin |
Charge (homme/mois) |
Délivrables |
||||||
---|---|---|---|---|---|---|---|---|---|---|---|
CEA |
PROV |
LANDE |
DA |
AF |
SVDO |
FT |
|||||
T5.0 |
CEA |
M9 |
M10 |
1 |
|
|
0,5 |
1 |
0,5 |
|
Rapport Exemples extraits de codes industriels |
T5.1 |
CEA |
M7 |
M10 |
4 |
|
|
|
|
|
|
Rapport de spécifications Documentation Prototype |
T5.2 |
CEA |
M10 |
M12 |
2 |
|
|
|
|
|
|
Rapport de spécifications Documentation Prototype |
T5.3 |
CEA |
M12 |
M15 |
6 |
|
|
|
|
|
|
Rapport de spécifications Documentation Prototype |
T5.4 |
CEA |
M12 |
M15 |
1 |
|
|
1,5 |
3 |
0,5 |
|
Rapports d'expérimentation Rapport de type didacticiel |