Compiling with Abstract Interpretation
Context
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. As an example, rewriting e + e
into 2*e
makes it obvious that the value is even. Symmetrically, the goal of a compiler is code transformation, but compilers often run analyses on the code to perform optimizations. For instance, many compilers remove variables which are never read by the program: this is possible thanks to a liveness analysis.
With this in mind, it seems compilers and analyzers could be written using the same core library of analysis and program transformations. A problem that creeps up in both case is known as the phaseordering problem: in what order should we run transformations and analyses? Should we start by analyzing the code, and use that information to transform it? Or rather should first transform the code and then run the analysis on the simplified version? Should we alternate between transformation and analysis passes?
In practice, the best precision is obtained by running transformations and analyses simultaneously. Fortunately, abstract interpretation is wellsuited to fuse different analyses together. In abstract interpretation, each analysis is viewed as a domain, and all domains have a common signature/interface. This allows running multiple analyses in parallel (using a product of the relevant domains), and have them collaborate (domains can query other domains to see if they can prove a property).
Example
Below is an example of compiling a source program to SSA using our technique (you can see the labels in the nodes as just different names for each node). Our analyzer is capable of eliminating the dead else branch inside the loop. Doing so requires simultaneously performing numerical analysis (to learn that z is even), some syntactic transformations (to learn that F(j + z%2) is F(j)), optimistic global value numbering (to learn that i = j), and dead code elimination so that no analysis takes the else branch (which breaks all those properties).
Contributions
Our paper shows the following novel results:
 A standard abstract interpretation framework can be turned into a compiler: create a domain that is a freealgebra of the domain signature (i.e. a domain where each domain operation is a constructor creating an expression), then the analysis result can be used to construct a new program.

Functors can mimic compiler passes. A functor is just a function that builds a new abstract domain on top of abstract domains received as arguments. Functors are modular, they can be proved independently and then combined in a full compilation chain. Functor soundness and completeness imply forward and backward simulation between source and compiled program respectively.
Here is a small example of a sound and complete functor transformation: replacing a ternary operator with explicit control flow jumps.

Compiling to SSA recovers missing context and improves numerical analysis precision. We describe a functor for compiling a small imperative language to SSA. This allows performing a numerical analysis on the SSA form, which leverages variable immutability to store information on expressions. This is always more precise than direct numerical analysis, while just adding a constant overhead.
In particular, this domain car analyze compiled code with the same precision as source (when compilation corresponds, e.g., to transformation into threeaddress code). The usual precision loss resulting from compiling large expressions into instruction sequences with multiple intermediate variables is recovered thanks to our SSAbased analysis.
Here are a few examples of assertion this domain can prove:
 Propagate information across statements
c = (y >= 0); if (c) { assert(y >= 0); }
 Learn from related variables:
y = x + 1; z = x * x; if (2 <= y && y <= 5) { assert(1 <= x && x <= 4); assert(1 <= z && z <= 16); }
 Increase precision of the numeric abstraction: even though intervals can’t represent
x != 0
, using our domain with interval abstraction can prove thisif (x != 0) { assert(x != 0); }
 Propagate information across statements
Further information
 Read the paper: either published version or the version with appendices
 Download the software artifact from Zenodo to try out our example analyzer and explore the code.
 To appear at the Programming Language Design and Implementation (PLDI) 2024 conference