Efficient Path-Sensitive Data-Dependence Analysis
This addresses the scalability bottleneck in program analysis for software verification and optimization, though it is an incremental improvement over existing methods.
The paper tackles the aliasing-path-explosion problem in data-dependence analysis by introducing a scalable path- and context-sensitive method that decomposes disjunctive reasoning into a summary phase and a demand-driven phase, achieving significant precision and scalability advantages over state-of-the-art analyses on programs up to 8 MLoC.
This paper presents a scalable path- and context-sensitive data-dependence analysis. The key is to address the aliasing-path-explosion problem via a sparse, demand-driven, and fused approach that piggybacks the computation of pointer information with the resolution of data dependence. Specifically, our approach decomposes the computational efforts of disjunctive reasoning into 1) a context- and semi-path-sensitive analysis that concisely summarizes data dependence as the symbolic and storeless value-flow graphs, and 2) a demand-driven phase that resolves transitive data dependence over the graphs. We have applied the approach to two clients, namely thin slicing and value flow analysis. Using a suite of 16 programs ranging from 13 KLoC to 8 MLoC, we compare our techniques against a diverse group of state-of-the-art analyses, illustrating significant precision and scalability advantages of our approach.