PREACH: A Heuristic for Probabilistic Reachability to Identify Hard to Reach Statements
PREACH: A Heuristic for Probabilistic Reachability to Identify Hard to Reach Statements
复制标题
DOI：
10.1145/3510003.3510227
复制
发表时间：
2022-05
期刊：
影响因子：
--
通讯作者：
Seemanta Saha;M. Downing;Tegan Brennan;T. Bultan
中科院分区：
文献类型：
--
作者：
Seemanta Saha;M. Downing;Tegan Brennan;T. Bultan
我们提出了一个启发式近似的可能性达到一个给定的程序语句使用1）分支选择性（表示满足分支条件的值的百分比），我们使用模型计数来计算，2）依赖性分析，我们使用它来识别影响语句可达性的依赖于输入的分支条件，3）抽象解释，我们使用它来识别达到分支条件的值的集合，以及4）离散时间马尔可夫链模型，我们构建它来捕获程序的控制流结构以及每个分支的选择性。我们的实验表明，我们基于启发式的概率可达性分析工具PReach可以在软件验证和测试竞赛、Apache Commons Lang和DARPA STAC计划的基准测试中以高精度和准确度识别难以到达的语句。我们提供了一个详细的比较与概率符号执行和统计符号执行的目的，确定难以达到的语句。对于有界执行深度，PREACH实现了与概率和统计符号执行相当的精度和准确性，并且当执行深度无限并且程序路径的数量呈指数增长时实现了更好的精度和准确性。此外，PReach比概率和统计符号执行更具可扩展性。
We present a heuristic for approximating the likelihood of reaching a given program statement using 1) branch selectivity (representing the percentage of values that satisfy a branch condition), which we compute using model counting, 2) dependency analysis, which we use to identify input-dependent branch conditions that influence statement reachability, 3) abstract interpretation, which we use to identify the set of values that reach a branch condition, and 4) a discrete-time Markov chain model, which we construct to capture the control flow structure of the program together with the selectivity of each branch. Our experiments indicate that our heuristic-based probabilistic reachability analysis tool PReach can identify hard to reach statements with high precision and accuracy in benchmarks from software verification and testing competitions, Apache Commons Lang, and the DARPA STAC program. We provide a detailed comparison with probabilistic symbolic execution and statistical symbolic execution for the purpose of identifying hard to reach statements. PREACH achieves comparable precision and accuracy to both probabilistic and statistical symbolic execution for bounded execution depth and better precision and accuracy when execution depth is unbounded and the number of program paths grows exponentially. Moreover, PReach is more scalable than both probabilistic and statistical symbolic execution.