Imperative constraint solver prediction and analysis

Software failures remain costly and the need for more effective analysis techniques for finding faults in software systems continues to grow. A powerful form of analysis is based on constraint solving where logical constraints char- acterize desired properties of code and solutions to the constraints are desired program states. For example, a rogram’s precondition constraint characterizes the valid inputs to the program. While constraint solvers serve as backend engines that enable many analyses, often the cost of solving constraints for programs in modern languages is quite high, and constraint solvers form a bottle-neck for the performance of the overall analysis. Enhancing these backend engines is essential for developing more effective analyses. Our focus is a well-known constraint solver for imperative constraints called Korat, which has served as the backend for many analyses, including test input generation, program repair, and reliability analysis. We enhance Korat by (1) introducing techniques for analyzing and reporting the state of its search for solutions to the given constraint, (2) studying its search characteris- tics to gain an understanding of how the search progresses, and (3) predicting the future search behavior based on the current and past search status. Our key contributions are three-fold. One, we present the first progress counter that reports precisely on the progress of Korat in terms of the size of space of all candidate solutions covered, and the remaining space to be covered; the counter provides feedback to the user as he/she waits for the search to termi- nate. Two, we present the first study of the search characteristics of Korat; the study provides insights into the Korat search and form the foundation of a new class of techniques to predict the behavior of Korat. Three, we propose the first predictive technique for Korat, which provides a new approach to tackle the problem of model counting, i.e., counting the number of solutions of the given formula. While our focus is Korat, we believe our techniques can generalize to other forms of constraints and solving methods, and enhance other constraint solvers.