< Retour au sommaire

Détection de chemins infaisables : un modèle formel et un algorithme.

Romain Aïssat le

Lieu: Salle 1073

Suivre en visio

Résumé

De nombreuses techniques d’analyse de programmes sont basées sur une représentation sous forme de graphe du programme appelée Graphe de Flot de Contrôle (CFG). Un CFG est une représentation compacte des comportements du programme : chaque exécution possible du programme est représentée par exactement un chemin dans le CFG. La propriété inverse est fausse : un chemin du CFG ne représente pas forcément une exécution du programme. De tels chemins sont dits infaisables. En général, le nombre de chemins infaisables dépasse largement celui des chemins faisables, même pour des programmes simples. Par conséquent, les techniques d’analyse basées sur le CFG sont généralement négativement impactées par l’existence des chemins infaisables.

Durant ce séminaire, nous présenterons un algorithme permettant de construire de meilleures approximations de l’ensemble des chemins faisables. Notre approche est basée sur un dépliage progressif du CFG par des techniques d’exécution symbolique et la résolution de contraintes pour détecter les chemins infaisables. En présence de boucles, le dépliage de tous les chemins du CFG résulterait en un arbre d’exécution symbolique infini : nous utilisons des techniques d’abstraction et de subsumption afin d’obtenir un graphe fini au lieu d’un arbre infini.

Nous présenterons les concepts théoriques de notre approche à l’aide d’une représentation sous forme de graphe spécifique et de cinq transformations sur ces graphes. Nous fournissons une formalisation complète sous Isabelle/HOL de cette représentation et de ces transformations afin de démontrer les propriétés de correction de notre approche. A partir de la formalisation, un prototype implémentant les cinq transformations ainsi que des heuristiques contrôlant l’application de ces transformations a été réalisé : nous prés nterons diverses expériences menées à l’aide de ce prototype ainsi que les résultats obtenus.