LLSC: a parallel symbolic execution compiler for LLVM IR

Guannan Wei, Shangyin Tan, Oliver Bracevac, Tiark Rompf

Abstract

We 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.

BibTeX

@inproceedings{Wei-al:FSE21,
  author    = {Guannan Wei and
               Shangyin Tan and
               Oliver Bracevac and
               Tiark Rompf},
  title     = {{LLSC:} a parallel symbolic execution compiler for {LLVM} {IR}},
  booktitle = {{ESEC/SIGSOFT} {FSE}},
  pages     = {1495--1499},
  publisher = {{ACM}},
  year      = {2021},
}

LLSC: a parallel symbolic execution compiler for LLVM IR

Abstract

Related papers