Paper Info
Title
Compiling symbolic execution with staging and algebraic effects
Abstract
Building effective symbolic execution engines poses challenges in multiple dimensions: an engine must correctly model the program semantics, provide flexibility in symbolic execution strategies, and execute them efficiently. This paper proposes a principled approach to building correct, flexible, and efficient symbolic execution engines, directly rooted in the semantics of the underlying language in terms of a high-level definitional interpreter. The definitional interpreter induces algebraic effects to abstract over semantic variants of symbolic execution, e.g., collecting path conditions as a state effect and path exploration as a nondeterminism effect. Different handlers of these effects give rise to different symbolic execution strategies, making execution strategies orthogonal to the symbolic execution semantics, thus improving flexibility. Furthermore, by annotating the symbolic definitional interpreter with binding-times and specializing it to the input program via the first Futamura projection, we obtain a "symbolic compiler", generating efficient instrumented code having the symbolic execution semantics. Our work reconciles the interpretation- and instrumentation-based approaches to building symbolic execution engines in a uniform framework. We illustrate our approach on a simple imperative language step-by-step and then scale up to a significant subset of LLVM IR. We also show effect handlers for common path selection strategies. Evaluating our prototype's performance shows speedups of 10~30x over the unstaged counterpart, and ~2x over KLEE, a state-of-the-art symbolic interpreter for LLVM IR.
Year
DOI
Venue
2020
10.1145/3428232
Proceedings of the ACM on Programming Languages
Keywords
DocType
Volume
algebraic effects,definitional interpreters,multi-stage programming,symbolic execution
Journal
4
Issue
ISSN
Citations 
OOPSLA
2475-1421
0
PageRank 
References 
Authors
0.34
0
4
Name
Order
Citations
PageRank
Guannan Wei112.38
Oliver Bračevac200.34
Shangyin Tan300.68
Tiark Rompf474345.86