一句话：提出 Gensym，将符号执行任务编译为 CPS 风格的协作式并发，实现并行符号执行的优化编译器。
符号执行是强大的程序分析与测试技术，但引擎多以解释器实现，解释开销严重抑制性能；基于插桩的实现又难以进行更复杂的程序变换，编译与代码生成技术在引擎构建中尚未被充分探索。本文提出 Gensym，一个优化符号执行编译器，其核心洞见是将符号执行任务通过续延传递风格（CPS）编译为协作式并发，进而高效并行化。Gensym 基于部分求值与生成式编程技术实现，兼顾高层抽象与高性能，生成可并行探索路径并生成测试的符号代码。在 20 个基准程序上，与先前的符号执行编译器 LLSC 和当前最优符号解释器 KLEE 相比，顺序执行平均加速 4.6 倍，并行执行平均加速 9.4 倍。
Symbolic execution is a powerful program analysis and testing technique. Symbolic execution engines are usually implemented as interpreters, and the induced interpretation over-head can dramatically inhibit performance. Alternatively, implementation choices based on instrumentation provide a limited ability to transform programs. However, the use of compilation and code generation techniques beyond simple instrumentation remains underexplored for engine construction, leaving potential performance gains untapped. In this paper, we show how to tap some of these gains using sophisticated compilation techniques: We present Gensym, an optimizing symbolic-execution compiler that generates symbolic code which explores paths and generates tests in parallel. The key insight of GensYmis to compile symbolic execution tasks into cooperative concurrency via continuation-passing style, which further enables efficient parallelism. The design and implementation of Gensym is based on partial evaluation and generative programming techniques, which make it high-level and performant at the same time. We compare the performance of Gensym against the prior symbolic-execution compiler LLSC and the state-of-the-art symbolic interpreter KLEE. The results show an average 4.6× speedup for sequential execution and 9.4× speedup for parallel execution on 20 benchmark programs.
@inproceedings{WeiJGDTBR23,
title = {Compiling Parallel Symbolic Execution with Continuations},
author = {Guannan Wei and Songlin Jia and Ruiqi Gao and Haotian Deng and Shangyin Tan and Oliver Bračevac and Tiark Rompf},
booktitle = {ICSE},
year = {2023},
doi = {10.1109/icse48619.2023.00116}
}