Accelerating array constraints in symbolic execution
Accelerating array constraints in symbolic execution
复制标题
DOI：
10.1145/3092703.3092728
复制
发表时间：
2017-07
期刊：
影响因子：
--
通讯作者：
D. Perry;Andrea Mattavelli;X. Zhang;Cristian Cadar
中科院分区：
文献类型：
--
作者：
D. Perry;Andrea Mattavelli;X. Zhang;Cristian Cadar
尽管最近取得了重大进展，但在用于测试复杂的真实软件时，符号执行的有效性是有限的。可伸缩性的主要挑战之一与约束求解有关：大型应用程序和较长的探索路径导致复杂的约束，通常涉及由符号表达式索引的大型数组。在本文中，我们提出了一组保持语义的数组操作转换，这些转换利用了符号执行过程中收集的上下文信息。我们的转换导致了更简单的编码，因此在约束求解中具有更好的性能。我们得到的结果是令人鼓舞的：我们通过广泛的实验分析表明，我们的转换有助于显著提高在存在数组的情况下的符号执行性能。我们还展示了我们的转换支持对新代码的分析，否则这将是符号执行无法实现的。
Despite significant recent advances, the effectiveness of symbolic execution is limited when used to test complex, real-world software. One of the main scalability challenges is related to constraint solving: large applications and long exploration paths lead to complex constraints, often involving big arrays indexed by symbolic expressions. In this paper, we propose a set of semantics-preserving transformations for array operations that take advantage of contextual information collected during symbolic execution. Our transformations lead to simpler encodings and hence better performance in constraint solving. The results we obtain are encouraging: we show, through an extensive experimental analysis, that our transformations help to significantly improve the performance of symbolic execution in the presence of arrays. We also show that our transformations enable the analysis of new code, which would be otherwise out of reach for symbolic execution.