Eurydice：将Rust代码编译为可读C代码

Eurydice 项目始于 2023 年，包含部分 MIT 许可证代码和部分 Apache-2.0 许可证代码。它是 Aeneas 项目的一部分，该项目致力于开发多种工具，将形式化验证工具应用于 Rust 代码。Aeneas 旗下的各个项目由 Inria（法国国家计算机科学研究机构）和 Microsoft 雇佣的一组人员维护，但也接受外部贡献。

Eurydice 遵循与许多编译器相同的总体结构：接收 Rust 程序，将其转换为中间表示（IR），通过一系列 pass 修改 IR，然后将其输出为较低级语言（在此场景下是 C）的代码。Jonathan Protzenko 是 Eurydice 最活跃的贡献者，他写了一篇博客文章解释该项目的方法。然而，与其他编译器不同，Eurydice 关注的是在移除 Rust 中存在但 C 中不存在的构造的同时，保留代码的整体结构。

例如，考虑这个 Rust 函数，它使用两个数的最大公约数来计算它们的最小公倍数：

fn gcd(a: u64, b: u64) -> u64 {
  if b == 0 {
    a
  } else {
    gcd(b, a%b)
  }
}

fn lcm(a: u64, b: u64) -> u64 {
  (a * b) / gcd(a, b)
}

以下是 Eurydice 将这些函数编译为 C 的结果：

uint64_t example_gcd(uint64_t a, uint64_t b)
{
  uint64_t uu____0;
  if (b == 0ULL)
    uu____0 = a;
  else
    uu____0 = example_gcd(b, a % b);
  return uu____0;
}

uint64_t example_lcm(uint64_t a, uint64_t b)
{
  uint64_t uu____0 = a * b;
  return uu____0 / example_gcd(a, b);
}

这段 C 代码是否算得上“可读”，大概因人而异。但它确实保留了代码的结构。甚至连原始代码的求值顺序也被保留了下来——在必要的地方添加了额外的临时变量（example_lcm() 中的 uu____0）来定义顺序。（Rust 保证如果乘法溢出并导致 panic，这会在调用 example_gcd() 产生的任何副作用之前发生，但 C 只保证在乘法在单独的语句中执行时才会如此。）用 rustc 编译同样的函数则会生成一对充满位运算的纠缠循环——这对机器码输出是合适的，但可读性差得多。

当然，并非所有 Rust 程序都能忠实地用 C 表示。例如，使用迭代器而非范围（range）的 for 循环需要编译为调用 Eurydice 支持代码来管理迭代器状态的 while 循环。更重要的是，C 没有泛型的概念，因此 Rust 代码在转换过程中需要单态化。这可能导致同一个函数产生多个仅在类型上不同的实现——而通常更符合 C 习惯的做法是使用宏或 void * 参数。

动态大小类型的实现也带来了某些挑战。在 Rust 中，可以定义一个结构体，其中一个字段没有固定大小——类似于 C 中的柔性数组成员：

struct DynamicallySized<U: ?Sized> {
  header: usize,
  my_data: U, // The compiler does not know the size of U, here
}

但如果该结构体是泛型的，并且该类型的某个泛型使用者给这个灵活大小的字段一个已知大小的类型，编译器就可以利用这个信息在适当的地方省略边界检查。

let foo: DynamicallySized<[u8; 4]> = ...;
// No bounds check emitted, since the array size is known to be 4:
let bar = foo.my_data[2];

这种分离——代码的某些部分可能知道类型的大小而另一些部分可能不知道——是一个重要的语义细节，需要在 C 中保留，因为它与形式化验证的可能性存在交互。如果 Eurydice 在编译 DynamicallySized 时到处都使用柔性数组成员，对 C 代码的分析可能会指出“缺失”的边界检查，而这些检查在 Rust 中并不需要。反过来，如果 Eurydice 添加了额外的边界检查，它就需要制造出 Rust 源码中不存在的额外错误路径，而这些路径本应完全不被使用。

因此，Eurydice 会生成两种不同的类型：一种带柔性数组成员的动态大小类型版本，以及一种带已知长度数组成员的版本。在二者之间转换在运行时是空操作，但技术上违反了 C 的严格别名规则。因此 Protzenko 建议使用 -fno-strict-aliasing 编译 Eurydice 生成的代码。

这种将更抽象的语言编译为 C 并保留代码结构的方法并不新鲜。Eurydice 所基于的 KaRaMeL 项目对 F* 编程语言做了同样的事情。F* 是一种依赖类型的函数式编程语言，用于开发密码学库。将可证明正确的 F* 程序编译为等价的 C，使得这些库可以用于对性能有要求的程序中。

遗憾的是，Eurydice 目前的可扩展性仅限于小型示例。Eurydice 没有为 Rust 代码实现自己的解析器和类型检查器，而是使用另一个 Aeneas 工具——Charon——从 rustc 中提取已解析和预处理过的程序。当我在各种 Rust 包上测试 Charon 时，它经常被较新的 Rust 特性（如 const 泛型）所难倒。

然而，当 Charon 能正常工作时，它会将 rustc 的中层中间表示（MIR）以 JSON 格式导出，同时附上理解编译所需的任何编译器标志。Eurydice 读取这个 JSON 表示并将其转换为 KaRaMeL 的中间表示。然后它对 KaRaMeL 代码执行一系列小型 pass 来消除一些 Rust 特有的细节，之后再交给 KaRaMeL 用于 F* 的同一套代码生成逻辑。

在当前形态下，Eurydice 最适合那些避免复杂 Rust 特性的小型、自包含程序。不过在这个细分领域内，它表现良好。生成的代码保持与原始 Rust 代码相同的结构，除了某些地方

（原文较长，此处译出前 6000 字，完整内容请点「打开原文」。）