Incrementalizing Abstract Interpretation

A powerful approach to design static analysers is abstract interpretation, which reasons over an approximation of the program’s behaviour. The Abstracting Abstract Machines (AAM) technique, introduced by Van Horn & Might, presents a systematic approach to derive abstract interpreters. However, it is often not useable in the development and evolution of large- scale applications, as with the current state-of-the-art, an AAM analysis can not incrementally update its results upon changes in the program. That is, whenever minor modifications occur in the program’s source code, one needs to recompute the entire AAM analysis from scratch, which can easily get time-consuming.We therefore propose an incremental approach to abstract interpretation, more precisely the AAM technique. That is, we modify the technique so that the result of an AAM analysis, the abstract state graph, can incrementally be updated following a change in the program’s source code. Our algorithm tracks dependencies between the nodes in the abstract syntax tree (AST) of the program and the transitions in the abstract state graph to invalidate and recompute new transitions in the state graph upon a change in the AST. Our experiments using a set of Scheme micro-benchmarks reveal that in practice this approach is often limited, as only states that are identical in both state graphs are reusable. We therefore introduce an improvement to the original incremental algorithm, which we refer to as state adaptation. State adaptation also enables reusing states that are not identical, but similar. Both the original and improved algorithm are integrated and evaluated in the Scala-AM framework. Our current implementations already show good results in terms of incremental efficiency, although more optimization is required to achieve actual gains in run time performance with our approaches.