Adaptive solving strategy synthesis for symbolic execution

Constraint solving is the enabling technique for symbolic execution. The advancement of constraint solving boosts the development and application of symbolic execution. Modern Satisfiability Modulo Theories (SMT) solvers provide the mechanism of solving strategy, allowing users to control the solving procedure. This mechanism significantly improves the solver's generalization ability. We observe that the symbolic executions of different programs are different constraint solving problems. Therefore, we propose synthesizing solving strategies for a program to fit the program's symbolic execution best. To achieve this, we propose an adaptive framework for synthesizing solving strategies, in which the constraints are classified into different categories, and the solving strategies are synthesized for different categories on demand. We propose novel synthesis algorithms that combine the offline trained deep learning models and online tuning to synthesize the solving strategy. The algorithms balance the synthesis overhead and the improvement achieved by the synthesized solving strategy. We have implemented our method on the state-of-the-art symbolic execution engine KLEE for C programs and Symbolic Pathfinder (SPF) for Java programs. The results of the extensive experiments indicate that our method effectively improves the efficiency of symbolic execution. For the Coreutils benchmark, our method, on average, increases the numbers of paths and queries by 74.37% and 73.94% under Breadth First Search (BFS), respectively. Besides, we applied our method to a different benchmark of C programs and a benchmark of Java programs to validate the generalization ability. The results demonstrate that for the C benchmark, our method increases the numbers of paths and queries by 71.09% and 70.60% under BFS, respectively; For the Java benchmark, our method increases the numbers of paths and queries by 50.31% and 49.93% under BFS, respectively. These results show that our method has a good generalization ability.