Résumé
L’interprétation abstraite est un formalisme très général, introduit par Patrick Cousot et Radhia Cousot en 1977 pour décrire et implémenter des analyses statiques plus précises que celles réalisables par analyse de flot de données. Au-delà des optimisations dans les compilateurs, l’interprétation abstraite a permis la réalisation d’outils de vérification montrant automatiquement l’absence d’erreurs à l’exécution dans de grands programmes.
Une interprétation abstraite est traditionnellement formalisée par deux fonctions, une fonction d’abstraction α et une fonction de concrétisation γ, qui forment une correspondance de Galois entre un domaine abstrait correspondant aux résultats de l’analyse statique et les ensembles d’états concrets correspondant aux exécutions du programme. De manière élégante, ces deux fonctions permettent de « calculer » les opérateurs abstraits qui implémentent l’analyse statique, c’est-à-dire de dériver systématiquement des définitions de ces opérateurs qui sont correctes et relativement complètes par construction.
Cependant, cette présentation classique pose problème dans le cadre d’une mécanisation en Coq ou autre logique fondée sur une théorie des types : les fonctions d’abstraction α sont généralement non calculables, et parfois mal définies. Le cinquième cours a développé une autre présentation des domaines abstraits qui n’utilise pas de fonctions d’abstraction α, mais uniquement des prédicats de concrétisation γ reliant objets abstraits et états concrets de manière entièrement définissable en théorie des types. Les opérateurs abstraits ne sont plus « calculés » mais donnés a priori puis vérifiés a posteriori.
Nous avons suivi cette approche pour construire, en Coq, un analyseur statique générique (un « interprète abstrait ») pour IMP, et un domaine abstrait très simple pour l’analyse de constantes. Nous avons ensuite amélioré la précision de notre analyseur grâce à deux techniques typiques de l’interprétation abstraite : l’analyse « en arrière » des expressions booléennes dans les conditionnelles et les boucles, et le calcul de points fixes par itération avec élargissement. Cela nous a permis d’obtenir une analyse assez précise des intervalles de variation des variables d’un programme IMP.
