Incremental Abstract Interpretation

Abstract

Non-incremental static analysis by abstract interpretation has to be rerun every time the code to be analyzed changes. For large code bases, this incurs a significant overhead, in particular, if the individual changes to the code are small. In order to accelerate the analysis on changing code bases, incremental static analysis reuses analysis results computed for earlier versions of the source code where possible. We show that this behavior can seamlessly be achieved for the analysis of C programs if a local generic solver such as the top-down solver is used as the fixed-point engine. This solver maintains a set of stable unknowns for which fixpoint iteration has already stabilized and it recursively destabilizes dependent unknowns on change. We indicate how this machinery can be applied to selectively invalidate results for those unknowns that may be directly or indirectly affected by program changes. We also explain the technical difficulties faced when realizing this basic idea within an analysis infra-structure such as Goblint. We also report the results of a preliminary experimental evaluation concerning the impact of incrementalization on analysis performance.