Paper Info
Title
LLSC: a parallel symbolic execution compiler for LLVM IR
Abstract
ABSTRACTWe present LLSC, a prototype compiler for nondeterministic parallel symbolic execution of the LLVM intermediate representation (IR). Given an LLVM IR program, LLSC generates code preserving the symbolic execution semantics and orchestrating solver invocations. The generated code runs efficiently, since the code has eliminated the interpretation overhead and explores multiple paths in parallel. To the best of our knowledge, LLSC is the first compiler for fork-based symbolic execution semantics that can generate parallel execution code. In this demonstration paper, we present the current development and preliminary evaluation of LLSC. The principle behind LLSC is to automatically specialize a symbolic interpreter via the 1st Futamura projection, a fundamental connection between interpreters and compilers. The symbolic interpreter is written in an expressive high-level language equipped with a multi-stage programming facility. We demonstrate the run time performance through a set of benchmark programs, showing that LLSC outperforms interpretation-based symbolic execution engines in significant ways.
Year
DOI
Venue
2021
10.1145/3468264.3473108
Foundations of Software Engineering
Keywords
DocType
Citations 
symbolic execution, compilation, program testing, staging
Conference
0
PageRank 
References 
Authors
0.34
0
4
Name
Order
Citations
PageRank
Guannan Wei112.38
Shangyin Tan200.68
Oliver Bracevac300.68
Tiark Rompf474345.86