一句话：提出「生成器求解」：不求解单个解，而是求解可反复调用、持续产出新测试输入的生成器，以提升符号执行效率。
基于符号执行的自动化测试输入生成广受关注，但其可扩展性差：约束建模与求解开销大，而每次 SMT 查询只产出一个测试输入，效率低下。本文提出「生成器求解」（generator solving）概念，不再针对单个特解求解，而是寻找一个可反复调用、持续产生新测试输入的生成器。其好处有三：可按需高效生成任意数量的测试输入，显著提升符号执行方法的输入生成效率；持续生成的输入能更充分地探索解空间，从而可能触发新的程序行为；相比基于变异（mutation）的混合方法，使用生成器可保证目标约束的可满足性。作者给出三项关键技术：复用 Z3 中可逆的模型转换器作为生成器；构造分层的基于区间的采样器以采样范围约束的解；采用乐观化简策略提升求解的通用性。并实现了原型生成器求解器 GenSlv。评估显示：对真实程序收集的约束中，凡至少有两个不同解者，GenSlv 能为其找到生成器的比例达 97%；在符号执行与混合 fuzzing 任务中，GenSlv 持续显著提升 KLEE、Angr、TritonDSE、SymCC 等常用符号执行器的程序覆盖率与漏洞检测能力，分支覆盖率最高提升两倍以上。
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.