Speculative Symbolic Execution
Speculative Symbolic Execution
复制标题
DOI：
10.1109/issre.2012.8
复制
发表时间：
2012-05
期刊：
影响因子：
--
通讯作者：
Yufeng Zhang;Zhenbang Chen;Ji Wang
中科院分区：
文献类型：
--
作者：
Yufeng Zhang;Zhenbang Chen;Ji Wang
符号执行是一种有效的面向路径和基于约束的程序分析技术。近年来，符号执行的研究和应用有了长足的发展。然而，符号执行在实际应用中仍然存在可伸缩性问题，特别是在应用于大规模或非常复杂的程序时。本文提出了一种新的符号执行方式，称为推测符号执行(SSE)，通过减少约束求解器的调用次数来提高符号执行的速度。在SSE中，当遇到分支语句时，搜索过程可能会推测性地探索分支，而不考虑可行性。仅当推测的分支累积到指定数量时才调用约束求解器。此外，我们还提出了一种关键的优化技术，极大地提高了SSE。我们已经在符号探路器(SPF)上实现了SSE和优化技术。在6个程序上的实验结果表明，我们的方法可以将约束求解器的调用次数减少20.7%到48.7%(平均29.9%)，搜索时间从23.6%减少到43.6%(平均30%)。
Symbolic execution is an effective path oriented and constraint based program analysis technique. Recently, there is a significant development in the research and application of symbolic execution. However, symbolic execution still suffers from the scalability problem in practice, especially when applied to large-scale or very complex programs. In this paper, we propose a new fashion of symbolic execution, named Speculative Symbolic Execution (SSE), to speed up symbolic execution by reducing the invocation times of constraint solver. In SSE, when encountering a branch statement, the search procedure may speculatively explore the branch without regard to the feasibility. Constraint solver is invoked only when the speculated branches are accumulated to a specified number. In addition, we present a key optimization technique that enhances SSE greatly. We have implemented SSE and the optimization technique on Symbolic Pathfinder (SPF). Experimental results on six programs show that, our method can reduce the invocation times of constraint solver by 20.7% to 48.7% (with an average of 29.9%), and save the search time from 23.6% to 43.6% (with an average of 30%).