Generator Solving for Symbolic Execution

Automated test input generation based on symbolic execution has garnered significant research interest. However, the main drawback of symbolic execution is its poor scalability. Since the overhead associated with constraint modeling and solving is high, generating only one test input per SMT query is inefficient. In this paper, we introduce the concept of generator solving. Instead of solving for only one particular solution, we propose to find a generator that can be called multiple times to continuously yield new test inputs. This approach offers several benefits: (1) it allows efficient generation of as many test inputs as needed, thereby significantly improving the input generation efficiency of symbolic execution methods; (2) the continuously generated inputs facilitate a more comprehensive exploration of the solution set, potentially triggering new program behaviors; and (3) compared to hybrid approaches based on mutation, using a generator ensures the satisfiability of the target constraints. We present three key techniques for generator solving: (1) reusing invertible model converters in Z3 as generators; (2) constructing hierarchical range-based samplers to sample solutions of range constraints; and (3) employing optimistic simplification strategies to enhance the generality of the solving process. We have implemented GenSlv, a prototypical generator solver specifically designed for automated test case generation based on symbolic execution. Evaluation results demonstrate that (1) GenSlv is effective in finding generators for constraints collected from real-world programs (specifically, GenSlv can find a generator for 97% of the constraints that have at least two different solutions), and (2) GenSlv significantly and consistently improves the performance of commonly used symbolic executors (including KLEE, Angr, TritonDSE, and SymCC) in terms of program coverage and vulnerability detection across various settings in symbolic execution and hybrid fuzzing tasks, with a maximum of more than twofold increase in branch coverage.