语义具体化:如何生成任意控制流且无未定义行为的代码?
摘要
Reify 是一款基于语义具体化技术的开源随机 C 程序生成器,能够生成不含未定义行为的代码,专用于编译器测试。它已在 GCC 和 LLVM 中发现了 59 个 bug,并在 OpenJ9 和 Linux 的 eBPF 运行时中发现了额外的缺陷。
查看缓存全文
缓存时间: 2026/06/05 02:11
connglli/Reify 来源:https://github.com/connglli/Reify # Reify Reify 是一个基于*语义具象化(semantic reification)*的随机程序生成器。它能生成不含未定义行为(UB)的 C 函数和程序,适用于测试 C 编译器,以及潜在地测试其他语言的虚拟机。借助 Reify,已在 GCC 和 LLVM 中发现并报告了 59 个漏洞。 目前,Reify 仅支持 i32、i32 数组和 i32 结构体。我们正在扩展其对更多基本类型和聚合类型的支持。此外,我们也在尝试生成 Java 字节码和 eBPF 字节码。尽管这些实验性尝试尚处于早期阶段,已在 OpenJ9 中发现了一个 JIT 编译器漏洞,并在 Linux 的 eBPF 运行时中发现了两个漏洞。此外,我们还在实验一个功能完备的 SymIR,名为 symlang(https://github.com/connglli/symlang),并在此基础上对 Reify 进行了重新实现,支持指针、向量和内置函数等更丰富的特性。 ## 🚀 快速开始 前置条件:
- 兼容 C++20 的编译器(GCC 10+ 或 Clang 10+)
- Bitwuzla(安装方式:https://github.com/bitwuzla/bitwuzla)
- Python 3(用于运行测试套件)
开始对 C 编译器进行模糊测试:
bash make -j8 all python scripts/fuzz.py -j 8 'gcc -O3 -fno-tree-slsr -fno-tree-ch'
🎇 随机程序
Reify 能够生成不调用其他函数的叶函数(leaf functions),以及由多个函数组成的完整程序(whole programs)。
叶函数生成
使用以下脚本生成 512 个叶函数:
bash python scripts/rysmith.py --output generated --limit 512
该脚本会轮流使用推荐的函数生成配置(如每个函数的基本块数量等),使得生成的 512 个函数呈现出多样的形态。输出目录(由 --output 选项指定)包含多个子目录,每个子目录对应一个函数:
func__:包含单个叶函数的所有产物,具体如下:func.c:生成的 C 函数(不能单独编译)。inout.jsonl:确保无 UB 执行的输入输出映射。func.sexp:生成函数的 S 表达式。main.c:用于测试该函数的驱动程序(可与func.c一起编译)。func.log:生成日志。
或使用以下命令生成单个叶函数:
bash timeout 3s ./build/bin/rysmith -A -U -m -S --output generated --Xbitwuzla-threads 4 --sno 0 $(uuidgen)
注意,生成叶函数可能会(1)因约束条件复杂而耗时较长,或(2)因约束条件不可满足而失败。这正是上述命令以 timeout 3s 为前缀的原因。
实验性功能:叶函数可从现有控制流图(CFG)生成,该功能目前处于实验阶段。
首先安装 Clang:
bash apt install clang
然后从其他程序(如由 Csmith(https://github.com/csmith-project/csmith)或 YARPGen(https://github.com/intel/yarpgen/)生成的程序)中提取 512 个 CFG:
bash python scripts/ggen.py -l /path/to/clang -L 512 -g csmith --csmith /path/to/csmith /path/to/csmith_db.jsonl
最后将生成的 CFG 数据库集成到叶函数生成中:
bash python scripts/rysmith.py ... --extra '--unstable-graphdb /path/to/csmith_db.jsonl' ...
完整程序生成
使用以下脚本,从一组预先生成的叶函数(特别是其 S 表达式,由 --input 选项指定)生成 512 个完整程序:
bash python scripts/rylink.py --input generated --limit 512
该脚本会轮流使用推荐的程序生成配置(如每个程序的函数数量),使得 512 个程序涵盖各种规模。生成的程序与输入函数一同放置在 --input 目录中。每个程序有自己的目录:
prog__:包含完整程序的所有产物,具体如下:main.c:程序入口。chksum.c:校验和工具。proto.h:所用叶函数的原型声明。func_*.c:各个函数文件。
或使用以下命令一次性生成程序:
bash ./build/bin/rylink --input generated --limit 512 --Xfunction-depth 10 $(uuidgen)
🔎 编译器模糊测试
可以使用 scripts/fuzz.py 一键测试 GCC 和 Clang/LLVM。启动模糊测试:
bash python scripts/fuzz.py -o fuzzdir -j 10 -s 0 'gcc -O3 -fno-tree-slsr -fno-tree-ch'
-o fuzzdir:输出目录-j 10:并行运行 10 个任务-s 0:随机数生成器的种子
实验性功能:对 JVM 进行模糊测试
使用以下命令对 Java 虚拟机进行模糊测试:
bash ./scripts/fuzz_jvm.sh --nproc 8 --java-home /path/to/java/home
该过程将叶函数生成适配为生成 Java 字节码。也可以通过 build/bin/rysmith 中的 --unstable-javaclass 选项生成单个 Java 类:
bash timeout 3s ./build/bin/rysmith ... --unstable-javaclass ...
生成的 Java 类文件将放置在 javaclasses 子目录中。
🐞 漏洞展示
前往 bugs 查看。
✏️ 引用我们
如果您觉得本工作对您有所帮助,请考虑引用我们的论文:
bibtex @inproceedings{reify, title={Semantic Reification: A New Paradigm for Random Program Generation}, author={Kavya Chopra and Cong Li and Thodoris Sotiropoulos and Zhendong Su}, year={2026}, booktitle={Proceedings of the 2026 ACM SIGPLAN Conference on Programming Language Design and Implementation}, series={PLDI '26}, doi={10.1145/3808268}, }
🧾 许可证
`` MIT License
Copyright (c) 2025 Kavya Chopra ([email protected]) Cong Li ([email protected])
Permission is hereby granted, free of charge, to any person obtaining a copy of this software and associated documentation files (the “Software”), to deal in the Software without restriction, including without limitation the rights to use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is furnished to do so, subject to the following conditions:
The above copyright notice and this permission notice shall be included in all copies or substantial portions of the Software.
THE SOFTWARE IS PROVIDED “AS IS”, WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. ``
相似文章
Semantic Reification:随机程序生成的新范式
介绍了 Semantic Reification,一种随机程序生成的新范式,如本研究论文所述。
ReaComp:将LLM推理编译为符号求解器以实现高效程序合成
ReaComp将LLM推理轨迹编译为可重用的符号程序合成器,在程序合成基准测试中实现了强大的准确性,同时消除了测试时的LLM调用,显著降低了计算成本。
在 LLVM 中对抗 Hyrum 定律
本文概述了 LLVM 编译器基础设施中旨在防止依赖未指定行为(即 Hyrum 定律)以保障构建可重现性的机制。
字节码虚拟机在意外场景中的应用 (2024)
本文探讨了字节码虚拟机的出人意料的应用,特别是Linux内核中的eBPF以及编译后二进制文件中用于调试信息的DWARF表达式。
Révo编程语言
Revo 是一种编程语言,具有清晰的数据流、错误即值、编译时执行和基于纤程的并发特性。它使用Zig构建,并提供可选类型和强推断功能。