Symbolic execution is a powerful program analysis and testing technique. Symbolic execution engines are usually implemented as interpreters, and the induced interpretation overhead 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 GenSym is 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.6x speedup for sequential execution and 9.4x speedup for parallel execution on 20 benchmark programs.

Artifact: https://github.com/Generative-Program-Analysis/icse23-artifact-evaluation