December 2, 2022
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. Instrumentation is another popular implementation choice with limited ability to transform programs. However, the use of compilation and code generation techniques beyond simple instrumentation for engine construction remains underexplored, and leaves potential performance gains untapped.
In this talk, I’m going to talk about improving the performance of symbolic execution via sophisticated compilation techniques. The key insight is to compile symbolic execution tasks into cooperative concurrency via continuation-passing style, which completely eliminates interpretation overhead and further enables efficient parallelism. I will also present GenSym, the symbolic-execution compiler we build for LLVM’s IR based on partial evaluation to continuation-passing code. We evaluate the performance of GenSym and compare with KLEE (the state-of-the-art symbolic interpreter for LLVM IR), which shows significant speedups on several Coreutils programs.
About Guannan Wei
Guannan is a PhD student in the department of Computer Science advised by Tiark Rompf. He works on building compilers for program analysis and designing expressive type/effect systems for higher-order imperative programs.