paperbot · PL 论文追踪

全部论文 待读 收藏

P2 LLSC: a parallel symbolic execution compiler for LLVM IR

LLSC：面向 LLVM IR 的并行符号执行编译器
FSE Proceedings of the 29th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering2021匹配度 4/10 · 该论文属于符号执行与编译器方向的程序分析工作，与用户的 PL/形式化验证背景有交集；但它不涉及 LLM/Agent、浮点程序分析或贝叶斯程序分析等用户当前核心追踪的交叉方向。引用 2 inbox
Guannan Wei, Shangyin Tan, Oliver Bračevac, Tiark Rompf
程序分析与抽象解释编译与代码生成
crossref: 2026-09-12

AI 速览

一句话：提出 LLSC，首个能为基于 fork 的符号执行语义生成并行执行代码的 LLVM IR 编译器。

符号执行是程序分析的重要技术，但传统实现常依赖解释器，带来解释开销，且难以并行探索多条路径。LLSC 是一个面向 LLVM 中间表示（IR）的原型编译器：给定 LLVM IR 程序，它生成保持符号执行语义并编排求解器调用的代码，从而实现非确定性的并行符号执行。生成代码因消除了逐指令解释开销，并且能够并行探索多条路径，因而运行高效。作者称，据其所知，LLSC 是首个能为基于 fork 的符号执行语义生成并行执行代码的编译器。

问题
如何避免符号执行中的解释开销，并让多条符号执行路径并行运行。
方法
将 LLVM IR 程序编译为保持符号执行语义、并负责编排求解器调用的并行执行代码。
评估
以原型编译器实现并展示生成代码的高效性；作者称其为首个支持 fork 式符号执行语义并生成并行执行代码的编译器。
原文摘要（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.

链接与引用

DOI 原文 · PDF（开放获取） ·

BibTeX 
@inproceedings{paperbot6455,
  title = {LLSC: a parallel symbolic execution compiler for LLVM IR},
  author = {Guannan Wei and Shangyin Tan and Oliver Bračevac and Tiark Rompf},
  booktitle = {FSE},
  year = {2021},
  doi = {10.1145/3468264.3473108}
}