Conception et implantation d'un calcul générique de plus faibles préconditions pour le C.
Début : M12
Fin : M25
Responsable : INRIA
Participants : INRIA, CEA
La mise au point d'un calcul de plus faibles préconditions (WP) pour un langage tel que le C est une tâche laborieuse. De plus, un tel calcul dépend fortement du modèle mémoire utilisé, c'est-à-dire de la description abstraite de la mémoire du programme C utilisée pendant la preuve formelle. L'objectif de ce sous-projet est d'identifier la partie générique de ce calcul de WP et la partie spécifique au modèle mémoire. En effet, un certain nombre de règles du calcul de WP ne concerne que la structure de contrôle et sont peu dépendantes, si ce n'est pas du tout, du modèle mémoire. En revanche, d'autres règles telles que celle de l'affectation ou de l'appel de fonction, sont fortement dépendantes de ce modèle.
Plus précisément, il s'agit d'identifier d'une part le modèle mémoire comme un ensemble de types et d'opérations, incluant une notion d'effet, d'autre part de concevoir un calcul d'effets générique, et enfin de concevoir un calcul de WP générique.
T6.0 Identification d'une notion générique de modèle mémoire
Un modèle mémoire correspond à une description abstraite, mathématique, de l'état de la mémoire du programme C à un instant donné. C'est cette description qui est utilisée pendant la preuve formelle. Dans cette tâche, nous identifierons la notion générique de modèle mémoire, vu comme un ensemble de types et opérations. On identifiera notamment les primitives nécessaires au calcul d'effets (tâche T6.1), c'est-à-dire la possibilité de désigner des régions du modèle mémoire.
T6.1 Notion d'effet pour un modèle mémoire et calcul d'effets
La notion d'effet correspond aux portions du modèle mémoire qui sont susceptibles d'être accèdées en lecture et/ou en écriture par une partie du programme C. Dans cette tâche nous élaborerons un calcul d'effets pour le langage C, c'est-à-dire une analyse statique déterminant l'effet de chaque expression, instruction et fonction du programme C. Nous chercherons à écrire ce calcul d'effets de la manière la plus générique possible, en le paramétrant par un modèle mémoire.
T6.2 Calcul générique de plus faibles préconditions
Cette tâche consiste à élaborer un calcul de plus faibles préconditions générique pour les programmes C, paramétré par un modèle mémoire et un calcul d'effets associé. En effet, de nombreuses règles de calcul des plus faibles préconditions sont communes à tous les modèles mémoire car uniquement liées à la structure de contrôle, et il convient donc de les identifier afin de factoriser le code correspondant.
T6.3 Prototypage et application à un modèle mémoire particulier
Afin de valider l'approche générique explorée dans les trois tâches ci-dessous, nous développerons (au moins) un modèle mémoire particulier pour lui appliquer les calculs d'effets et de plus faibles préconditions génériques. Un tel exemple de modèle pourrait être celui d'un modèle très bas niveau où la mémoire du programme C est vue comme un unique tableau associant à des adresses entières des valeurs entières.
Ce sous-projet est critique pour l'ensemble du projet et comporte un part exploratoire importante. Au cas où la mise au poijt d'un calcul générique se révélerait hors de portée, il sera toujours possibles d'implanter un calcul de plus faible précondition particulier afin de pouvoir continuer les autres tâches.
Tâche |
Resp. |
Début |
Fin |
Charge (homme/mois) |
Délivrables |
||||||
---|---|---|---|---|---|---|---|---|---|---|---|
CEA |
INRIA |
IRISA |
DA |
AF |
SVDO |
FT |
|||||
T6.0 |
INRIA |
M12 |
M14 |
3 |
2 |
|
|
|
|
|
Rapport |
T6.1 |
INRIA |
M14 |
M16 |
3 |
2 |
|
|
|
|
|
Rapport |
T6.2 |
INRIA |
M16 |
M20 |
4 |
3 |
|
|
|
|
|
Rapport |
T6.3 |
INRIA |
M21 |
M25 |
4 |
3 |
|
|
|
|
|
Prototype |