< Retour au sommaire

Static Numeric Analysis based on SSA

Dorian Lesbre le

Lieu: Salle 1073

Suivre en visio

Abstract

Numerical program analysis by abstract interpretation depends on how the target program is written. To gain precision, and ensure analysis robustness, it can be interesting to transform program before analyzing them. My thesis focuses on transformations to a form that is easier to analyze: static single assignment (SSA), as well as on analyses that exploit SSA properties.

First, I’ve developed a technique to transform programs inside an abstract interpreter. This allows performing the analysis and the transformations simultaneously, which leads to mutual improvements. Applying it to SSA transformations yields more precise numerical analysis, as it enables reasoning on the program values rather than its variables and allows for more constraint propagations than a standard numeric domain.

Next, I introduced a fast relational domain based on union-find, which benefits from SSA immutability. It can represent binary injective relation between terms, such as y=ax+b, and factorize other domains, reducing the number of SSA terms they need to handle. Finally, I’ve extended this do ain to store flow-sensitive information by defining a fast join and inclusion check on union-find.