Partially Evaluating Symbolic Interpreters for All
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.
|Short paper (paper.pdf)||497KiB|
Mon 17 JanDisplayed time zone: Eastern Time (US & Canada) change
11:35 - 12:35
|Partially Evaluating Symbolic Interpreters for AllRemote|
|Parallel Algebraic Effect HandlersRemote|
Ningning Xie University of Cambridge, Daniel D. Johnson Google Research, Dougal Maclaurin Google Research, Adam Paszke Google ResearchFile Attached