Je suis étudiant en doctorat à
l'équipe BINSEC,
au centre NanoINNOV du
CEA Paris-Saclay.
Je travaille sur l'interprétation abstraite par transformation SSA. Mon encadrant
de thèse est Matthieu Lemerre.
Je m'intéresse notamment à la vérification et l'informatique pratique bas niveau :
méthodes formelles, interprétation abstraite, système de types, Coq, systèmes d'exploitation, compilation,
circuits, programmation fonctionnelle et d'autres. En dehors de l'informatique, je m'intéresse
aussi aux mathématiques et à la physique.
Hors du domaine scolaire, j'aime bien faire des sports d'extérieur comme l'escalade, la voile, la randonnée
et le ski. J'aime bien lire, notamment de la SF et des romans policiers. Je m'occupe également en jouant à des jeux de société et des jeux vidéos.
Compiling with Abstract Interpretation
Dorian Lesbre et Matthieu Lemerre
Accepté à PLDI 2024, pas encore publié
Resumé
Rewriting and static analyses are mutually beneficial techniques: program transformations change the inten-
sional aspects of the program, and can thus improve analysis precision, while some efficient transformations
are enabled by specific knowledge of some program invariants. Despite the strong interaction between these
techniques, they are usually considered distinct. In this paper, we demonstrate that we can turn abstract
interpreters into compilers, using a simple free algebra over the standard signature of abstract domains.
Functor domains correspond to compiler passes, for which soundness is translated to a proof of forward
simulation, and completeness to backward simulation. We achieve translation to SSA using an abstract do-
main with a non-standard SSA signature. Incorporating such an SSA translation to an abstract interpreter
improves its precision; in particular we show that an SSA-based non-relational domain is always more precise
than a standard non-relational domain for similar time and memory complexity. Moreover, such a domain
allows recovering from precision losses that occur when analyzing low-level machine code instead of source
code. These results help implement analyses or compilation passes where symbolic and semantic methods
simultaneously refine each other, and improves precision when compared to doing the passes in sequence.
