PARTI: a multi-interval theory solver for symbolic execution
PARTI: a multi-interval theory solver for symbolic execution
复制标题
PARTI：用于符号执行的多区间理论求解器
DOI：
10.1145/3238147.3238179
复制
发表时间：
2018
期刊：
影响因子：
--
通讯作者：
Dustmann O
中科院分区：
文献类型：
--
作者：
Dustmann O
符号执行是一种有效的程序分析技术，其可扩展性在很大程度上取决于快速解决大量一阶逻辑查询的能力。针对特定结构的数组和位向量理论，提出了一种快速求解查询的通用技术，该技术分为两个阶段：确定每个符号变量的解集的学习阶段和利用这些信息快速确定特定类型查询的可满足性的决策阶段。主要的挑战包括决定支持哪些运算符，以及精确地处理整数类型强制转换和算术下溢和溢出。我们在一个名为PARTI(区间的部分理论解算器)的不完整求解器中实现了这一技术，直接将其集成到流行的Klee符号执行引擎中。我们将Klee与PARTI和最先进的SMT解算器应用于合成基准和真实基准。我们发现，在多次实现数量级加速的同时，PARTI几乎不会影响性能。
Symbolic execution is an effective program analysis technique whose scalability largely depends on the ability to quickly solve large numbers of first-order logic queries. We propose an effective general technique for speeding up the solving of queries in the theory of arrays and bit-vectors with a specific structure, while otherwise falling back to a complete solver.The technique has two stages: a learning stage that determines the solution sets of each symbolic variable, and a decision stage that uses this information to quickly determine the satisfiability of certain types of queries. The main challenges involve deciding which operators to support and precisely dealing with integer type casts and arithmetic underflow and overflow.We implemented this technique in an incomplete solver called PARTI (``PARtial Theory solver for Intervals''), directly integrating it into the popular KLEE symbolic execution engine. We applied KLEE with PARTI and a state-of-the-art SMT solver to synthetic and real-world benchmarks. We found that PARTI practically does not hurt performance while many times achieving order-of-magnitude speedups.