Sheng-Han Wen (National Taiwan University), Wei-Loon Mow (National Taiwan University), Wei-Ning Chen (National Taiwan University), Chien-Yuan Wang (National Taiwan University), Hsu-Chun Hsiao (National Taiwan University)
Constraint solving creates a serious performance bottleneck in symbolic execution. Examining a plethora of SMT solvers with diverse capabilities, we address the following research questions: How can the performance of symbolic execution improve if it can pick a priori the best solver for a given path constraint? How can such a prediction oracle be practically implemented? In this work, we first define the solver selection problem in symbolic execution and its evaluation metrics, and perform a preliminary study to gauge potential performance improvement through solver selection. We then present the design and implementation of Path Constraint Classifier (PCC), a machine learning based meta-solver that aims to reduce overall constraint solving latency by dynamically selecting a solver per query. Using machine learning seems straightforward, yet surprisingly underexplored; one main technical challenge is how to avoid excessive overhead introduced by feature extraction. We address this challenge by taking advantage of the structural characteristics of symbolic execution. Our experiments confirm that the overall solver time can be reduced by 10.3% in the KLEE dataset and 46% in the benchmark dataset, while the solver prediction procedure only accounts for 2% to 10% of overall solving time.