Optimizing Constraint Solving to Better Support Symbolic Execution

Abstract

Constraint solving is an integral part of symbolic execution, as most symbolic execution techniques rely heavily on an underlying constraint solver. In fact, the performance of the constraint solver used by a symbolic execution technique can considerably affect its overall performance. Unfortunately, constraint solvers are mostly used in a black-box fashion within symbolic execution, without leveraging any of the contextual and domain information available. Because constraint solvers are optimized for specific kinds of constraints and heavily based on heuristics, this leaves on the table many opportunities for optimizing the solvers' performance. To address this problem, we propose a novel optimization strategy that uses domain and contextual information to optimize the performance of constraint solvers during symbolic execution. We also present a study in which we assess the effectiveness of our and other related strategies when used within dynamic symbolic execution performed on real software. Our results are encouraging, they show that optimizing constraints based on domain and contextual information can improve the efficiency and effectiveness of constraint solving and ultimately benefit symbolic execution.