Abstract:
In symbolic execution, constraint solving is mainly responsible for path reachability prediction and test input generation, but due to the path explosion problem and the limited power of the SMT solver, constraint solving occupy high overhead in symbolic execution, and this problem has become one of the bottlenecks in symbolic execution. This paper first introduces the basic concepts of symbolic execution, constraint solving, and analyzes the origin of the constraint solving problem. Second, this paper divides the optimization techniques in recent years into three stages:pre-solving, in-solving and post-solving. The related techniques include slicing, simplification, fast unsatisfiability check, multi-solver support, etc. Finally, the conclusions and prospects are made. It is proposed that the future work should focus on the improvements in respect of constraint reduction, constraint solutions reuse, parallel solving, solving configuration prediction, etc.