Laboratoire: Verimag (http://www-verimag.imag.fr/)
Équipe: SYNCHRONE (http://www-verimag.imag.fr/SYNCHRONE)
Encadrants: Nicolas Halbwachs <Nicolas.Halbwachs@imag.fr>, David Monniaux <David.Monniaux@imag.fr>, et Julien Henry <Julien.Henry@imag.fr>.
Contexte Scientifique
Nous voulons annoter automatiquement des fonctions (écrites en C, C++) avec des conditions suffisantes raisonnables pour que l’exécution de ces fonctions vérifie des propriétés intéressantes, par exemple l’absence de certaines erreurs à l’exécution (overflows arithmétiques, division par zéro) ou encore la possibilité d’utiliser une version optimisée de la fonction (vectorisation etc.).
Ceci permet par exemple de générer deux versions de la même fonction : l’une, moins efficace, qui va tester la possibilité des erreurs au moment de chaque opération et/ou utiliser une version non optimisée de certaines opérations (boucles), l’autre, qui va court-circuiter les tests et/ou utiliser des constructions optimisées.
Ceci a des applications à la fois en analyse de programmes (génération automatique de documentation à destination de l’utilisateur, du type « il faut appeler cette fonction avec 0<n<65534) et en compilation optimisante. Les applications à la compilation seront explorés en association avec l’entreprise STMicroelectronics.
Sujet
Modifier l’outil PAGAI de Julien Henry pour remonter des préconditions.
Compétences Attendues
- Notions de logique
- Notions de compilation
- C++
Contexte de Travail
Le stagiaire sera encadré par Nicolas Halbwachs et David Monniaux (permanents du laboratoire) et travaillera en collaboration avec Julien Henry (doctorant) sur la partie implémentation.
Des experts en compilation de STMicroelectronics viendront discuter des applications à ce domaine.
