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