李 航，臧 洌，甘 露

(南京航空航天大学计算机科学与技术学院，江苏 南京 211106)

0 引 言

符号执行技术是一种重要的程序分析技术，由King等[1]于1976年提出。路径爆炸和约束求解是目前制约符号执行效率和可扩展性的2大因素。目前针对提高符号执行效率主要有以下4个方面的研究。

1)解决路径爆炸问题。Wang等[2]通过消除冗余路径缓解了路径爆炸；Liu等[3]提出了探索符号状态缓存的方法来解决路径爆炸；Adachi等[4]提出了基于分布式控制流图(Control Flow Graph)的符号执行来解决传统符号执行不能处理含有循环的程序和易产生路径爆炸的问题。

2)研究约束求解，提高约束求解效率。Zhang等[5]提出了猜测符号执行减少约束求解次数；Zou等[6]通过消除冗余约束条件来化简约束；Li等[7]使用机器学习的方法来化简复杂约束；汤恩义等[8]使用线性拟合来处理带非线性约束、逻辑复杂的程序。

3)限制程序的分析范围，避免不相关的路径探索，主要用于回归测试[9-11]。

4)研究程序的并行性来并行化符号执行。Siddiqui等[12]提出了一种并行化符号执行的新技术，使符号执行的状态可以用测试用例简洁的编码；孙盼盼等[13]设计了分布式符号执行平台；Rakadjiev等[14]对KLEE符号执行引擎进行了扩展，增加了Z3求解器，实现了并发执行和异步约束求解。

符号执行可以系统地探索程序的路径并生成相应的测试输入，进行详尽的路径探索目的是为了发现更多的程序错误[16]。理论上讲，覆盖更多的路径通常意味着覆盖更多的程序行为，是更严格的软件测试[17]。……