Paper Info
Title
Path-sensitive sparse analysis without path conditions
Abstract
ABSTRACTSparse program analysis is fast as it propagates data flow facts via data dependence, skipping unnecessary control flows. However, when path-sensitively checking millions of lines of code, it is still prohibitively expensive because a huge number of path conditions have to be computed and solved via an SMT solver. This paper presents Fusion, a fused approach to inter-procedurally path-sensitive sparse analysis. In Fusion, the SMT solver does not work as a standalone tool on path conditions but directly on the program together with the sparse analysis. Such a fused design allows us to determine the path feasibility without explicitly computing path conditions, not only saving the cost of computing path conditions but also providing an opportunity to enhance the SMT solving algorithm. To the best of our knowledge, Fusion, for the first time, enables whole program bug detection on millions of lines of code in a common personal computer, with the precision of inter-procedural path-sensitivity. Compared to two state-of-the-art tools, Fusion is 10× faster but consumes only 10% of memory on average. Fusion has detected over a hundred bugs in mature open-source software, some of which have even been assigned CVE identifiers due to their security impact.
Year
DOI
Venue
2021
10.1145/3453483.3454086
PLDI
Keywords
DocType
Citations 
Sparse analysis, path sensitivity, program dependence graph, SMT solving
Conference
2
PageRank 
References 
Authors
0.36
0
4
Name
Order
Citations
PageRank
Qingkai Shi1447.50
Peisen Yao232.40
Rongxin Wu352819.69
Charles Zhang451228.97