A Search Strategy For The Symbolic Execution Of The Programs With Complex Computations

As software systems becoming more and more important in our daily life, the system reliability turns to be an essential aspect of software systems. As an accurate analysis technique, symbolic execution effectively improves the reliability of software systems, and it's widely used in academia and industry. However, 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, a spot of solving occupys most sovling time, which happens a lot when analyzing the programs with complex numerical calculations. This issue limits the ability of the solver for solving more constrains in a given period, which reduces the coverage of statements and paths.Considering the features above, this paper proposes a solving cost prediction based search strategy for symbolic execution. The complexity of constraints is related to the length of logical expression, operating and computing types included, and the number and types of contants and variables referred. 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. Based on the predicted values we designed a weighted random search strategy. So we can explore the paths with a lower solving cost with a higher priority by using our strategy. 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; our strategy can find more bugs. In addition, the time of using our strategy for finding same bugs decreases 44.43% in average.