Compiling using abstract interpretation, and using the result to improve analysis

What is it about?

Program transformation and analysis can be mutually beneficial. One one hand, transformations can make analysis easier. For instance rewriting `x land 1` into `x mod 2` shows how the expression captures the parity of x. On the other hand, some transformation are enabled by prior analysis. For example, to perform dead-code elimination, one must prove that the branch to remove is never taken. With this in mind, a software analyzer or compiler will want to perform both transformations or analysis. Abstract interpretation offers many tools to combine different analysis, allowing them to run simultaneously and gain precision by collaboration. Our work allows performing transformation as part of an abstract interpretation analysis. This enables the analysis to benefit from precision increases of the transformation, and the transformations to use the most precise analysis information directly. Overall, the technique can improve the precision of the analysis being performed while only incurring a constant overhead time penalty.

Featured Image

Photo by James Harrison on Unsplash

Photo by James Harrison on Unsplash

Why is it important?

Our paper shows the following novel results: A standard abstract interpretation framework can be turned into a compiler: create a domain that is a free-algebra 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. Different abstract domain signatures correspond to different languages: the classical domain signature correspond to imperative programs expressed as a control-flow graph, and we provide a SSA domain signature corresponding to programs in SSA form. Functors can implement 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. 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 three-address code). The usual precision loss resulting from compiling large expressions into instruction sequences with multiple intermediate variables is recovered thanks to our SSA-based analysis.