Incrementalizing Abstract Interpretation
Developers have come to rely on IDE's red squiggly lines that continuously point out bugs and vulnerabilities in their code. This feature relies on program analyses that predict the order in which the program's instructions might be executed at run-time (i.e., control flow) and the values they might operate upon (i.e., data flow). Predicting a program's run-time behavior while it is still being edited poses several challenges. For instance, how to predict the program's overall behavior when some of its code is not yet syntactically correct? But also, how to predict this behavior in a timely manner? Ideally, developers are warned about a potential mistake as soon as it is introduced Unfortunately, the analyses with the best predictions are computationally demanding to the extent that they take several minutes to run. As such, the most interesting analyses cannot be used to provide developers real-time feedback as they are editing source code.
Incremental variants have therefore been developed of the simpler program analyses. Incremental program analyses avoid re-considering the entire program upon a change. For instance, by attempting to re-use results that have been computed before and that have not been impacted directly or indirectly by the change. Unfortunately, such an incrementalization has not yet made it to powerful program analyses that support dynamic languages.
The Software Languages Lab has been developing such powerful analyses for both Scheme and JavaScript. Abstract interpretation using abstract machines is the
foundation for these analyses [1]. It produces a graph of states that a low-level interpreter would go through for a given program, but this in manner
that guarantees that the analysis even terminates on programs with infinite loops. To see abstract interpretation in action for JavaScript, go to http://jensnicolay.github.io/jipda/protopurity/protopurity.html and type in a simple program like
function sq(x){return x*x};sq(5)
and press eval.
The goal of this thesis is to investigate how abstract machines can be rendered incrementel such that Scheme or Javascript developers can be provided real-time feedback about their code. This will require a strategy for determining which parts of a previously computed state graph can be reused, and which parts need to be computed again.
This thesis will consist of:
- Surveying existing solutions for incremental computations and incrementalizing the simpler program analyses
- Designing and implementing your own solution, together with a formal description of your work.
[1]: Abstacting Abstract Machines, M. Might, D. Van Horn, 2010. http://matt.might.net/papers/vanhorn2010abstract.pdf
[2]: JIPDA, a Javascript abstract interpreter: http://jensnicolay.github.io/jipda/protopurity/protopurity.html
[3]: scala-am, a Scheme abstract interpreter: http://github.com/acieroid/scala-am
[4]: Incremental Computation with Names, M. Hammer, et al., http://arxiv.org/pdf/1503.07792