论文标题
使用约束问题基准测试符号执行 - 初始结果
Benchmarking Symbolic Execution Using Constraint Problems -- Initial Results
论文作者
论文摘要
符号执行是用于寻找和程序测试的强大技术。它成功地在现实世界代码中查找错误。核心推理技术使用约束解决，路径探索和搜索，这也是解决组合问题（例如有限域约束满意度问题（CSP））中使用的相同技术。我们建议CSP实例作为更具挑战性的基准测试，以评估核心技术在符号执行中的有效性。我们将CSP基准测试转换为适合测试符号执行工具的推理功能的C程序。从单个CSP P中，我们根据转换选择转换为不同的C程序。使用KLEE，Tracer-X和LLBMC工具进行初步测试，显示了转换和求解器选择的实质性运行时差异。我们的C基准有效地显示了现有的符号执行工具的局限性。这项工作的动机是我们认为，这种形式的基准可以刺激符号执行引擎中核心推理的发展和工程。
Symbolic execution is a powerful technique for bug finding and program testing. It is successful in finding bugs in real-world code. The core reasoning techniques use constraint solving, path exploration, and search, which are also the same techniques used in solving combinatorial problems, e.g., finite-domain constraint satisfaction problems (CSPs). We propose CSP instances as more challenging benchmarks to evaluate the effectiveness of the core techniques in symbolic execution. We transform CSP benchmarks into C programs suitable for testing the reasoning capabilities of symbolic execution tools. From a single CSP P, we transform P depending on transformation choice into different C programs. Preliminary testing with the KLEE, Tracer-X, and LLBMC tools show substantial runtime differences from transformation and solver choice. Our C benchmarks are effective in showing the limitations of existing symbolic execution tools. The motivation for this work is we believe that benchmarks of this form can spur the development and engineering of improved core reasoning in symbolic execution engines.
