Constraint Normalization And Parameterized Caching For Quantitative Program Analysis

We present a constraint caching framework to expedite potentially expensive satisfiability and model-counting queries. Integral to this framework is our new constraint normalization procedure under which the cardinality of the solution set of a constraint, but not necessarily the solution set itself, is preserved. We extend these constraint normalization techniques to string constraints in order to support analysis of string-manipulating code. We use a group-theoretic framework, which generalizes earlier results, to express our normalization techniques. We also present a parameterized caching approach where, in addition to storing the result of a model-counting query, we store a model-counter object that allows us to efficiently recount the number of satisfying models for different bounds. We implement these techniques in our tool Cashew, which is built as an extension of the Green caching framework [55], and integrate it with the symbolic execution tool Symbolic PathFinder (SPF) and the model-counting constraint solver ABC. Our experiments show that constraint caching can significantly improve the performance of symbolic and quantitative program analyses. For instance, Cashew can normalize the 10,104 unique constraints in the SMC/Kaluza benchmark down to 394 normal forms, achieve a 10x speedup on the SMC/Kaluza-Big dataset, and an average 3x speedup in our SPF-based side-channel analysis experiments.