ISSN 1000-1239 CN 11-1777/TP

• 软件技术 •

基于求解开销预测的符号执行搜索策略研究

1. 1(国防科学技术大学计算机学院 长沙 410073); 2(并行与分布处理国防科技重点实验室(国防科学技术大学计算机学院) 长沙 410073); 3(95835部队 新疆巴音郭楞 841700) (liujingde@nudt.edu.cn)
• 出版日期: 2016-05-01
• 基金资助:
国家“九七三”重点基础研究计划基金项目(2014CB340703);国家自然科学基金项目(61120106006,61472440,61272140)

Solving Cost Prediction Based Search in Symbolic Execution

Liu Jingde1,3, Chen Zhenbang1, Wang Ji1,2

1. 1(College of Computer, National University of Defense Technology, Changsha 410073); 2(Science and Technology on Parallel and Distributed Processing Laboratory (College of Computer, National University of Defense Technology), Changsha 410073); 3(95835 PLA Troops, Bayingolin, Xinjiang 841700)
• Online: 2016-05-01

Abstract: In symbolic execution, constraint solving needs a large proportion of execution time. The solving time of a constraint differs a lot with respect to the complexity, which happens a lot when analyzing the programs with complex numerical calculations. Solving more constraints within a specified time contributes to covering more statements and exploring more paths. Considering this feature, we propose a solving cost prediction based search strategy for symbolic execution. Based on the experimental data of constraint solving, we conclude an empirical formula to evaluate the complexity of constraints, and predict the solving cost of a constraint combined with historical solving cost data. The formula is used in our strategy to explore the paths with a lower solving cost with a higher priority. We have implemented our strategy in KLEE, a state-of-art symbolic executor for C, and carried out the experiments on the randomly selected 12 modules in GNU Scientific Library (GSL). The experimental results indicate that: in a same period, compared with the existing strategy, our strategy can explore averagely 24.34% more paths, without sacrificing the statement coverage; and our strategy can find more bugs. In addition, the time of using our strategy for finding same bugs decreases 44.43% in average.