Exploring Strategies for Guiding Symbolic Analysis with Machine Learning Prediction

To improve the scalability of symbolic analysis tools, one observation is that analysis resources are wasted on analyzing unsatisfiable paths, which are not possible in reality. While existing works attempt to predict the satisfiability of a program path without spending resources to analyze it, the performance of these predictor models are far from perfect. In this work, we attempt to understand how model predictions, even if imperfect, can be most effectively used to reduce the time required to analyze satisfiable paths. This work studies the sometimes complex interactions between model performance, analysis domain properties such as the distribution of path analysis costs and distribution of satisfiable paths, the design of symbolic analysis tools being used, and the algorithm used to prioritize and select paths for analysis. Using a novel simulation methodology, we study this problem and find that a number of factors can have as large an effect on symbolic analysis performance as improved predictors. Finally, we conclude with a couple of observations about how to best integrate machine learning prediction into symbolic analysis.