SLR: Path-Sensitive Analysis through Infeasible-Path Detection and Syntactic Language Refinement
Gogul Balakrishnan and Sriram Sankaranarayanan and Franjo Ivancic and Ou Wei and Aarti Gupta
We present a technique for detecting semantically infeasible paths in programs using abstract interpretation. Our technique uses a sequence of path-insensitive forward and backward runs of an abstract interpreter to infer paths in the control flow graph that cannot be exercised in concrete executions of the program.
We then present a syntactic language refinement (SLR) technique that automatically excludes semantically infeasible paths from a program during static analysis. SLR allows us to iteratively prove more properties. Specifically, our technique simulates the effect of a path-sensitive analysis by performing syntactic language refinement over an underlying path-insensitive static analyzer. Finally, we present experimental results to quantify the impact of our technique on an abstract interpreter for C programs.
Paper available as: [PDF] [Official Version]