Semantic Reification：如何生成无未定义行为的任意控制流代码？

背景

在编译器测试和验证领域，随机程序生成器（Random Program Generators）扮演着至关重要的角色。传统的生成器如 Csmith 虽然广泛使用，但往往难以保证生成的代码绝对“无未定义行为”（Undefined Behavior, UB）。未定义行为不仅会导致程序崩溃，更会让编译器优化产生不可预测的结果，从而掩盖潜在的编译器 Bug。

Reify 是一种基于**语义重ification（Semantic Reification）**技术的新型随机程序生成器。其核心理念是通过形式化方法，在生成代码的早期阶段就消除未定义行为，从而生成逻辑上健全、可执行的 C 函数和完整程序。这一特性使其成为测试 C 编译器（如 GCC 和 LLVM）以及潜在的其他语言虚拟机（如 Java JVM 和 eBPF 运行时）的理想工具。

目前，Reify 已在 GCC 和 LLVM 中发现了 59 个 Bug，并在实验性扩展至 Java 字节码和 eBPF 字节码生成时，分别发现了 OpenJ9 JIT 编译器的一个 Bug 和 Linux eBPF 运行时的两个 Bug。

核心内容

Reify 的技术实现、功能支持及使用方法如下：

1. 技术基础与依赖

Reify 依赖于复杂的约束求解技术。其核心组件包括：

• SymIR (Symbolic Intermediate Representation)：基于实验性的 symlang 全功能符号中间表示，支持指针、向量和内置函数（intrinsics）等更丰富的特性。
• Bitwuzla：一个高效的 SMT 求解器，用于处理生成过程中的约束满足问题。
• 编译环境：需要兼容 C++20 的编译器（GCC 10+ 或 Clang 10+）。
• 运行环境：Python 3 用于运行测试套件。

2. 当前支持类型与扩展

• C 语言支持：目前主要支持 i32（32位整数）、i32 数组和 i32 结构体。开发团队正在扩展以支持更多原始类型和聚合类型。
• 其他字节码支持：
  • Java 字节码：通过将叶子函数生成适配为 Java 字节码生成，已发现 OpenJ9 的一个 JIT 编译器 Bug。
  • eBPF 字节码：实验性支持，已发现 Linux eBPF 运行时的两个 Bug。

3. 生成模式

Reify 支持两种主要的生成模式：

A. 叶子函数生成 (Leaf Functions)

叶子函数是指不调用其他函数的独立函数。

• 生成命令：

  python scripts/rysmith.py --output generated --limit 512
  

  该脚本会自动轮换推荐的功能生成配置（如每个函数的基本块数量），以暴露各种控制流形状。
• 单次生成命令：

  timeout 3s ./build/bin/rysmith -A -U -m -S --output generated --Xbitwuzla-threads 4 --sno 0 $(uuidgen)
  

  注意：由于约束可能非常复杂，生成过程可能耗时较长或因约束不可满足而失败，因此建议使用 timeout 限制时间。
• 输出结构：每个函数生成在一个独立的目录 func_<uuid>_<sno> 中，包含：
  • func.c：生成的 C 代码（单独不可编译）。
  • inout.jsonl：确保无 UB 执行的输入-输出映射。
  • func.sexp：生成函数的 S-expression 表示。
  • main.c：用于测试该函数的驱动程序（可与 func.c 一起编译）。
  • func.log：生成日志。

B. 完整程序生成 (Whole Programs)

由多个函数组成的完整程序。

• 生成命令：

  python scripts/rylink.py --input generated --limit 512
  

  该脚本基于之前生成的叶子函数（通过 --input 指定），轮换程序生成配置（如每个程序的函数数量），以覆盖不同规模的程序。
• 单次生成命令：

  ./build/bin/rylink --input generated --limit 512 --Xfunction-depth 10 $(uuidgen)
  

• 输出结构：每个程序生成在 prog_<uuid>_<sno> 目录中，包含：
  • main.c：入口点。
  • chksum.c：校验和工具。
  • proto.h：所用叶子函数的原型声明。
  • func_*.c：各个函数文件。

4. 高级实验功能

• 基于现有 CFG 生成：可以从现有的控制流图（CFG）生成叶子函数。
  1. 安装 Clang。
  2. 从 Csmith 或 YARPGen 生成的程序中提取 CFG：

     python scripts/ggen.py -l /path/to/clang -L 512 -g csmith --csmith /path/to/csmith /path/to/csmith_db.jsonl
     

  3. 集成到生成过程中：

     python scripts/rysmith.py ... --extra '--unstable-graphdb /path/to/csmith_db.jsonl' ...
     

• Java 类生成：可通过 --unstable-javaclass 标志直接生成单个 Java 类，输出位于 javaclasses 子目录。

5. 模糊测试 (Fuzzing) 流程

• 测试 C 编译器：

  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：随机数生成器种子。
  • 引号内为编译器命令及参数。
• 测试 Java 虚拟机：

  ./scripts/fuzz_jvm.sh --nproc 8 --java-home /path/to/java/home
  

关键要点

• 无 UB 保证：Reify 的核心优势在于通过语义重ification 技术，从根源上生成不包含未定义行为（UB）的代码，极大提高了编译器测试的有效性。
• 已发现大量 Bug：在 GCC 和 LLVM 中已报告 59 个 Bug；在实验性支持 Java 和 eBPF 时，也分别发现了 OpenJ9 和 Linux eBPF 运行时的 Bug。
• 多语言/多平台扩展潜力：虽然目前主要支持 C 语言的 i32 类型，但团队正在扩展类型支持，并已成功实验性生成 Java 字节码和 eBPF 字节码。
• 灵活的生成策略：支持生成独立的叶子函数和由多个函数组成的完整程序，并能基于现有的控制流图（CFG）进行生成，增加了测试的多样性。
• 自动化模糊测试集成：提供了 fuzz.py 和 fuzz_jvm.sh 等脚本，简化了对 GCC、Clang/LLVM 和 JVM 的模糊测试流程。
• 技术栈要求：依赖 C++20 编译器、Bitwuzla SMT 求解器和 Python 3，体现了其对现代编译技术和形式化方法的依赖。

意义与影响

Reify 代表了随机程序生成领域的一个新范式。传统工具如 Csmith 虽然强大，但往往需要在生成后过滤掉包含未定义行为的代码，这不仅效率低下，而且可能遗漏某些特定于 UB 的编译器缺陷。Reify 通过语义重ification，将“无 UB”这一约束内