Mon 17 Jan 2022 11:35 - 12:05 at PEPM - Contributed Talks 1 Chair(s): Antonina Nepeivoda

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 Jan

Displayed time zone: Eastern Time (US & Canada) change

11:35 - 12:35
Contributed Talks 1PEPM at PEPM
Chair(s): Antonina Nepeivoda Program Systems Institute of RAS, Russia
11:35
30m
Talk
Partially Evaluating Symbolic Interpreters for AllRemote
PEPM
Shangyin Tan Purdue University, Guannan Wei Purdue University, Tiark Rompf Purdue University
File Attached
12:05
30m
Talk
Parallel Algebraic Effect HandlersRemote
PEPM
Ningning Xie University of Toronto, Daniel D. Johnson Google Research, Dougal Maclaurin Google Research, Adam Paszke Google Research
File Attached