Software analyzers and compilers have a lot in common: they both have to read and understand source code in order to prove facts about it and transform it into an equivalent code. While the goal of an analyzer is to prove facts (correctness, safety…) about the source, it often transforms the code through rewrites to make the analysis easier. In this talk, I will present how we integrate program transformations as part of an abstract interpretation analysis in the Codex analyzer for C and binary code. Specifically, I will show how we can obtain a new program as a result of abstract interpretation using a free-algebra domain; how we can encode program transformations as simple functors that operate on domains; as well as how and why we focus on compiling programs to an SSA representation for analysis. Finally, I will present a weakly relational domain based on a labeled union-find structure, which should enable us to include some relational information in an SSA non-relational analysis at a very low cost.
