LLSC: a parallel symbolic execution compiler for LLVM IR
LLSC: a parallel symbolic execution compiler for LLVM IR
复制标题
DOI：
10.1145/3468264.3473108
复制
发表时间：
2021-08
期刊：
影响因子：
--
通讯作者：
Guannan Wei;Shangyin Tan;Oliver Bračevac;Tiark Rompf
中科院分区：
文献类型：
--
作者：
Guannan Wei;Shangyin Tan;Oliver Bračevac;Tiark Rompf
我们提出LLSC，一个原型编译器的LLVM中间表示（IR）的非确定性并行符号执行。给定LLVM IR程序，LLSC生成保留符号执行语义和编排求解器调用的代码。生成的代码运行效率很高，因为代码消除了解释开销并并行探索多个路径。据我们所知，LLSC是第一个基于fork的符号执行语义的编译器，可以生成并行执行代码。在这篇示范论文中，我们提出了目前的发展和初步评估的LLSC。LLSC背后的原理是通过第一个Futamura投影自动专门化符号解释器，这是解释器和编译器之间的基本联系。符号解释器是写在一个富有表现力的高级语言配备了多阶段的编程设施。我们通过一组基准测试程序展示了运行时性能，表明LLSC在显着方面优于基于解释的符号执行引擎。
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. 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.