Study On The Loop Guided And Recursion Guided Symbolic Execution Technology

Symbolic execution is a very popular method of program analysis and testing in recent years.It can automatically explore the path space of a program,analyze the constraints of each path and generate test cases according to the path constraints.Compared with other program analysis and testing methods,symbolic execution is highly automated and has higher path coverage rate.Now,it is widely used in program analysis,automated tests and many other fields.Path explosion is the largest challenge and bottleneck of symbolic execution.When the number of paths in the program is very large,it is difficult for symbolic execution to analyze and execute all the paths in the program with an accepatable execution time and storage space.Loop and recursion are two main triggers of path explosion.In the process of symbolic execution,each time the symbolic execution engine meets the loop condition,it will generate one path executing into the loop and another path leaving the loop,which results in the doubling of the number of paths.Each recursion contains at least one branch which will call recursion and one branch which will return from recursion.So,each recursion call generates at least two paths,one path goes deep into recursion and another path leaves the recrusion.This also results in the multiplication of the number of paths.In symbolic execution,iterations of loop and number of recursion calls are usually not fixed values,and the range of these values is very wide and the number of possible values is very large.Finally,loops and recursions will cause the rapid expansion of the number of paths during symbolic execution.By combining target guided and state merging technology,this thesis proposes loop guided method and recursion guided method to assist the process of loops and recursions in symbolic execution.On the one hand,we use target guided techonology to analyze the structure of loops and recursions in source codes of the program and generate guidance information to guide symbolic execution to go deep into loops and recursions and helps symbolic execution engine to discover errors hidden in loops and recursions.On the other hand,by merging paths generated in loops and recursions with state merging techonology,we reduce the size of path space to relieve the path explosion caused by loops and recursions.Also,by defining the method of describing the structure of loops and recursions,designing the graphical components to describe path in loops and recursions,this thesis proposes a visualization method to shows the execution path of symbolic execution in the loops and recursions.This thesis implements loop guided method and recursion guided method by extending the open source symbolic execution tool KLEE,and designs two experiments on Malardalen WCET,Debie,Scimark 2.0 and a set of recursion programs to evaluate the effectiveness of loop guided method and recursion guided method.By Comparing with the default method of KLEE,we find that in most of the cases,loop guided method and recursion guided method can improve the efficiency of symbolic execution in loops and recursions,and have a good effect on alleviating the path explosion caused by loops and recursions.