ISSN 1000-1239 CN 11-1777/TP

计算机研究与发展 ›› 2018, Vol. 55 ›› Issue (10): 2331-2342.doi: 10.7544/issn1000-1239.2018.20170545

• 软件技术 • 上一篇    

程序状态条件合并中变量隐式关联分析方法

郭曦1,王盼2   

  1. 1(华中农业大学信息学院计算机科学系 武汉 430070);2(武汉电力职业技术学院电力工程系 武汉 430079) (xguo@mail.hzau.edu.cn)
  • 出版日期: 2018-10-01
  • 基金资助: 
    国家自然科学基金项目(61502194);中央高校基本科研业务费专项资金(2662018JC028)

Variable Dependent Relation Analysis in Program State Condition Merging

Guo Xi1, Wang Pan2   

  1. 1(Department of Computer Science, College of Informatics, Huazhong Agriculture University, Wuhan 430070);2(Department of Power Engineering, Wuhan Electric Power Technical College, Wuhan 430079)
  • Online: 2018-10-01

摘要: 程序分析的主要目标是对程序的性质进行研究,符号执行作为目前主流的分析方法在生成高效的测试用例集或提高路径覆盖率等方面发挥着重要的作用,其中路径条件表达式的提取以及约束求解是路径分析过程中的关键步骤.现有的路径分析方法普遍存在约束求解效率不高而导致的路径覆盖率较低的问题.由于符号执行引擎所采用的搜索策略不尽相同,在符号执行分析过程中存在状态合并的过程,该抽象过程可能导致产生不正确的测试用例.以提高路径分析效率为目标,提出一种高效的程序分析方法:首先对传统的符号执行树的表示方法进行改进,提取不同路径共享的符号表达式和路径约束条件以提高符号执行过程中状态合并的效率,然后采用隐式关联分析方法,产生逆向分析中的依赖条件集合,并给出基于依赖条件重构的算法以提高路径覆盖率.实验结果表明:相对于传统的状态合并以及符号执行方法,该方法有更为高效的状态合并效率以及更高的路径约束条件分析精度.

关键词: 路径分析, 状态合并, 依赖条件, 符号执行, 约束求解

Abstract: The main purpose of program analysis is researching the properties of programs. Symbolic execution, which is the current popular analysis method, plays an important role in the aspects of generating efficient test cases, improving the path coverage ratio and so on. The key processes are extracting the path constraint and constraint solving. The current analysis methods have the shortcomings with low efficient of constraint solving, which results to low path coverage ratio. Due to different search strategies used by symbolic execution engine, the process of state merging may exist during symbolic execution, which may result to incorrect path information. This paper aims at improving the efficiency of path analysis, and a high efficient program analysis method is proposed. The shape of conventional symbolic execution tree is improved, and extracting the symbolic expression and path constraints in different paths to improve the efficiency of state merging; and then we use the potential relation analysis to generate the dependent relation set in backward analysis. The algorithm of dependent relation reorder is proposed to improve the path coverage ratio. Experimental results demonstrate that our method can improve the efficiency of state merging and improve the accuracy of path constraint analysis compared with conventional methods of state merging and symbolic execution.

Key words: path analysis, state merging, dependency condition, symbolic execution, constrain solving

中图分类号: