论文标题
tracerx：插值的动态符号执行
TracerX: Dynamic Symbolic Execution with Interpolation
论文作者
论文摘要
动态符号执行（DSE）是测试程序的重要方法。 DSE上的一个重要系统是KLEE，它输入了用符号变量注释的C/C ++程序，将其编译为LLVM，然后使用指定的回溯策略模拟LLVM的执行路径。符号执行的主要挑战是路径爆炸。抽象学习的方法已用于解决此问题。这里的关键步骤是计算interpolant来表示学习的抽象。在本文中，我们提出了一种新的插值算法，并将其在KLEE系统的基础上实现。主要目的是解决追求代码渗透的路径爆炸问题：证明目标程序点可以达到或无法到达。也就是说，我们的重点是验证。我们表明，尽管计算插值剂的开销，但插值剂提供的符号执行树的修剪通常会带来显着的总体好处。然后，我们对KLEE进行了全面的实验评估，以及基于静态符号执行CBMC的一个知名系统。我们的主要实验显示了新级别的代码渗透成功，尤其是当目标难以确定时。次要实验表明，我们的实施具有测试竞争力。
Dynamic Symbolic Execution (DSE) is an important method for the testing of programs. An important system on DSE is KLEE which inputs a C/C++ program annotated with symbolic variables, compiles it into LLVM, and then emulates the execution paths of LLVM using a specified backtracking strategy. The major challenge in symbolic execution is path explosion. The method of abstraction learning has been used to address this. The key step here is the computation of an interpolant to represent the learnt abstraction. In this paper, we present a new interpolation algorithm and implement it on top of the KLEE system. The main objective is to address the path explosion problem in pursuit of code penetration: to prove that a target program point is either reachable or unreachable. That is, our focus is verification. We show that despite the overhead of computing interpolants, the pruning of the symbolic execution tree that interpolants provide often brings significant overall benefits. We then performed a comprehensive experimental evaluation against KLEE, as well as against one well-known system that is based on Static Symbolic Execution, CBMC. Our primary experiment shows code penetration success at a new level, particularly so when the target is hard to determine. A secondary experiment shows that our implementation is competitive for testing.
