Variable Dependent Relation Analysis in Program State Condition Merging

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.