Symbolic execution is a program analysis technique to automatically explore the execution space of programs by treating some inputs symbolically. To efficiently perform symbolic execution, one emerging way is to construct a compiler that translates input programs to symbolic programs without the interpretation overhead. Previous work has explored compiling nondeterministic symbolic execution by partially evaluating a symbolic interpreter.

In this paper, we follow a “semantics-first“ approach and investigate compiling concolic execution and backward symbolic execution by multi-stage programming. In particular, we construct variants of staged symbolic interpreters that can be partially evaluated using the Lightweight Modular Staging (LMS) framework. We demonstrate our approach using a simple low-level intermediate representation (IR) and evaluate the prototype implementations for the LLVM IR. Our concolic compiler shows comparable performance to SymCC, a state-of-the-art concolic compiler, and our backward symbolic compiler solves tasks that are difficult for forward execution engines. The demonstrated approach shows a unifying methodology that can be applied to compiling diverse flavors of symbolic execution.