语义具体化:如何生成任意控制流且无未定义行为的代码?

Hacker News Top 工具

摘要

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. ``

相似文章

在 LLVM 中对抗 Hyrum 定律

Lobsters Hottest

本文概述了 LLVM 编译器基础设施中旨在防止依赖未指定行为(即 Hyrum 定律)以保障构建可重现性的机制。

Révo编程语言

Lobsters Hottest

Revo 是一种编程语言,具有清晰的数据流、错误即值、编译时执行和基于纤程的并发特性。它使用Zig构建,并提供可选类型和强推断功能。