Dorian Lesbre

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.

In this work-in-progress paper, we present labeled union-find, an extension of the union-find data structure where edges are annotated with labels that form a group algebraic structure. This structure allows to very efficiently represent the transitive closure of many useful binary relations, such as two-variables per equality (TVPE) constraints of the form y = ax+b. We characterize the properties of labeled union-find when used to represent binary relations between variables. More specifically, we study the use of this domain in a static analysis; either to represent binary relations, or as a reduced product with non-relational abstract domains with constraint propagation; as well as the design of efficient algorithms for the join of labeled union-find structures. We believe that this structure could be used as a low-cost relational domain or decision procedure, and that it could make other relational domains more efficient by removing the need to track some variables.