Incrementally Precise Program Analysis

Chu Duc Jiep, Joxan Jaffar and Vijayaraghavan Murali

Abstract

Program analysis has been dominated by Abstract Interpretation (AI), owing to its scalability. AI is typically not (or only partially) path-sensitive thus the obtained level of accuracy could be arbitrar- ily low. Recently, there have been works on path-sensitive program analysis, applied to domains where accuracy is critical. However, they suffer from the path explosion problem and are not scalable in general. In this paper, we present a general framework for program analysis that incrementally increases accuracy as it iterates.

We start with a formulation of analysis which is both a lower- bound as well as upper-bound analysis of the program’s behavior. This duality allows for a specification of precision in the overall analysis. We then define an abstract representation of the program which we can iteratively refine. The iterations allows for early ter- mination when a user-definable level of precision in the analysis has been extracted. The critical performance factors are (a) the in- crementality of the refinement step where results from previous it- erations are persistent for future iterations, (b) reuse of analysis from subproblems that have precise analysis, and most importantly, (c) a concept of domination which allows a lower-bound analysis to prune away subproblems. Finally, we demonstrate the frame- work with real programs on a backward counting analysis and a forward data flow analysis. We show that in many cases, our iter- ative method is in fact superior to both AI as well as algorithms designed to run continuously till an exact analysis is found.