Optimal Refinement-based Array Constraint Solving for Symbolic Execution

Array constraint solving is widely adopted by the existing symbolic execution engines for encoding programs precisely. The counterexample-guided abstraction refinement (CEGAR) based method is state-of-the-art for array constraint solving. However, we observed that the CEGAR-based method may need many refinements to solve the array constraints produced by the symbolic executor, which decreases the performance of constraint solving. Based on the observation, we propose a machine learning-based method to improve the efficiency of the CEGAR-based array constraint solving. Our method adaptively turns on or off the CEGAR loop according to different solving problems. We have implemented our method on the symbolic executor KLEE and its underlying CEGAR-based constraint solver STP. We have conducted an extensive experiment on 55 real-world programs. On average, our method increases the number of explored paths by 21%. The results of the extensive experiments on real-world C programs show the effectiveness of our method.