Efficient Incremental Static Analysis Using Path Abstraction
Efficient Incremental Static Analysis Using Path Abstraction
复制标题
使用路径抽象进行高效增量静态分析
DOI：
--
复制
发表时间：
2014
期刊：
影响因子：
--
通讯作者：
M. Ramanathan
中科院分区：
文献类型：
--
作者：
Rashmi Mudduluru;M. Ramanathan
增量静态分析涉及分析对源代码的版本的改变沿着分析在语义上受改变影响的代码区域。现有的分析工具，试图执行增量分析可能会执行冗余的计算，由于穷人的抽象。在本文中，我们设计了一种新的和有效的增量分析算法，以减少整体分析时间。我们使用路径抽象，将程序中的不同路径编码为一组约束。将编码为布尔公式的约束输入到SAT求解器，并且公式的（不）可满足性进一步驱动分析。虽然大多数布尔公式在多个版本中是相似的，但找到它们的等价性的问题是图同构完全的。我们解决了一个轻松的版本的问题，通过设计高效的memoization技术，以确定等价的布尔公式，以提高性能的静态分析引擎。我们的实验结果在一些大的代码库（高达87 KLoC）显示了高达32%的性能增益时，使用增量分析。与识别布尔公式的等价性相关的开销小于（不超过8.4%）分析时间的总体减少。
Incremental static analysis involves analyzing changes to a version of a source code along with analyzing code regions that are semantically affected by the changes. Existing analysis tools that attempt to perform incremental analysis can perform redundant computations due to poor abstraction. In this paper, we design a novel and efficient incremental analysis algorithm for reducing the overall analysis time. We use a path abstraction that encodes different paths in the program as a set of constraints. The constraints encoded as boolean formulas are input to a SAT solver and the (un)satisfiability of the formulas drives the analysis further. While a majority of boolean formulas are similar across multiple versions, the problem of finding their equivalence is graph isomorphism complete. We address a relaxed version of the problem by designing efficient memoization techniques to identify equivalence of boolean formulas to improve the performance of the static analysis engine. Our experimental results on a number of large codebases (upto 87 KLoC) show a performance gain of upto 32% when incremental analysis is used. The overhead associated with identifying equivalence of boolean formulas is less (not more than 8.4%) than the overall reduction in analysis time.