paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Semantic Reification: A New Paradigm for Random Program Generation

语义具体化:随机程序生成的新范式
PLDI 10(PLDI)2026匹配度 2/10 · 论文属于编译器测试与随机程序生成方向,核心是 CFG/执行路径驱动的语义程序构造,不涉及 LLM/Agent,也不涉及机器学习系统或 Agentic 程序中的静态分析,与浮点程序分析、贝叶斯程序分析及 AI↔PL 交叉方向均无明显交集。其工程落地与工业 bug 发现值得肯定,但主题上与用户画像核心问题距离较远。引用 0 inbox
Kavya Chopra, Cong Li, Thodoris Sotiropoulos, Zhendong Su
crossref: 2026-09-10

AI 速览

一句话:提出以 CFG 与执行路径为核心的随机程序生成范式,可生成语义正确、可终止且支持任意控制流的程序,用于编译器测试。

随机程序生成是编译器测试的重要手段,但现有方法难以兼顾语义正确性与任意控制流。本文提出语义具体化范式,把生成目标从语法转向语义:以控制流图(CFG)刻画编译期语义,以 CFG 上的执行路径刻画运行时语义;对任意 CFG 与选中路径构造程序,使其在给定输入下确定性地沿该路径执行并产生预期输出,且支持无界循环与不可归约区域。实现上先用轻量符号执行生成满足约束的叶函数,再依任意调用图以语义保持的 peephole 重写组合成复杂程序。Reify 在 GCC 与 LLVM 上发现 59 个缺陷(57 确认、27 修复),含 24 个长期潜伏与 36 个 wrong-code。

问题
现有随机程序生成(如编译器模糊测试)难以同时保证生成程序的语义正确性、终止性,并支持无界循环、不可归约区域等任意控制流。
方法
提出语义具体化范式:以 CFG 表示编译期语义、以 CFG 上的执行路径表示运行时语义,对任意 CFG 与路径构造出在给定输入下必然沿该路径执行并产生预期输出的程序;实现上结合轻量符号执行的符号函数具体化与语义保持的 peephole 重写,按调用图将叶函数组合为复杂程序。
评估
实现面向 C 编译器的 Reify,在 GCC 与 LLVM 上开展为期五个月的测试,发现 59 个缺陷(57 个确认、27 个修复),其中 24 个长期潜伏、36 个为 wrong-code,多数为高优先级且涉及既有工具忽略的语义特性。
原文摘要(Abstract)

We introduce semantic reification, a novel paradigm for random program generation that centers on program semantics rather than syntax. Our key insight is to reformulate random program generation to capture two types of program semantics: (1) compile-time semantics (what a program can do), represented by the control flow graph (CFG), and (2) runtime semantics (what a program actually does), represented by execution paths within the CFG. For any CFG and any execution path on it, semantic reification constructs a program guaranteed to be well-behaved with respect to a specific input and output. This means that when executed with this input, the program deterministically follows the designated execution path to produce the expected output. This paradigm differs from existing work by supporting arbitrary control flow such as unbounded loops and irreducible regions, while still ensuring that the generated programs are semantically correct and terminating. We develop a practical realization of this paradigm. First, we introduce symbolic function reification that integrates a lightweight form of symbolic execution into the generation process to generate an individual, leaf function (i.e., a function that is free of function calls). Each leaf function satisfies the constraints of a given CFG and a selected execution path. Second, we compose multiple leaf functions into a larger, more complex program via semantics-preserving peephole rewriting, guided by an arbitrary call graph. Over five months, our implementation for C compilers, Reify, has uncovered 59 bugs in GCC and LLVM (57 confirmed, 27 fixed), 24 of which are long-latent. Among them, 36 are wrong-code bugs, many are high-priority issues, and most of them involve semantic characteristics overlooked by existing tools. We believe semantic reification opens new directions for research beyond compilers, such as validating debuggers, analyzers, and verifiers.

链接与引用

DOI 原文 · PDF(开放获取) · DBLP

BibTeX
@article{ChopraLSS26,
  title = {Semantic Reification: A New Paradigm for Random Program Generation},
  author = {Kavya Chopra and Cong Li and Thodoris Sotiropoulos and Zhendong Su},
  journal = {Proceedings of the ACM on Programming Languages},
  volume = {10},
  number = {PLDI},
  year = {2026},
  doi = {10.1145/3808268}
}