paperbot · PL 论文追踪

全部论文 待读 收藏

P2 &inator: Correct, Precise C-to-Rust Interface Translation

&inator：正确、精确的 C 到 Rust 接口翻译
PLDI 10(PLDI)2026匹配度 3/10 · 该论文属于程序语言与形式化方法，核心是约束求解驱动的 C-to-Rust 接口翻译，涉及类型正确性和借用检查，但与用户画像中 LLM/Agent × 静态分析、浮点程序分析、贝叶斯程序分析等主线没有直接交集。它更偏向传统 PL/编译器与约束求解，而非 AI 与 PL 的交叉。引用 0 inbox
Victor Chen, Ayden Coughlin, Michael D. Bond
编译与代码生成逻辑与约束编程
crossref: 2026-09-10

AI 速览

一句话：提出首个基于约束求解的正确且精确的 C 到 Rust 接口翻译方法，生成满足借用检查的最简 Rust 声明。

将系统软件从 C 自动翻译到 Rust 颇具吸引力却十分困难，因为必须进行全程序推理以满足 Rust 的所有权与借用规则。接口翻译是其中的关键使能步骤：为 C 程序的顶层声明（结构体与函数签名）生成 Rust 声明，从而支持模块化和增量式的代码翻译。本文提出 &inator，首次实现正确、精确的 C 到 Rust 接口翻译。&inator 采用一种新颖的基于约束的表述来刻画语义等价与类型正确性（包括借用检查规则），并据此求解 Rust 接口。所得接口是正确的（即存在保持语义的 safe Rust 实现）且精确的（即使用最简单、代价最低的类型）。实验表明，&inator 能为真实 C 程序生成正确且精确的 Rust 接口；但对某些 C 特性的支持以及面向大型程序的可扩展性仍有待未来工作。

问题
C 到 Rust 的全程序翻译需要满足 Rust 的所有权与借用规则，而接口翻译——为 C 顶层结构体与函数签名生成 Rust 声明——是实现模块化、增量翻译的关键步骤。
方法
&inator 使用一种基于约束的表述来同时编码语义等价与类型正确性（含借用检查规则），并求解出正确且精确（使用最简、最低代价类型）的 Rust 接口。
评估
在真实 C 程序上评估，表明 &inator 能生成正确且精确的 Rust 接口；同时指出对某些 C 特性的支持和大型程序的可扩展性仍是未来工作。
原文摘要（Abstract）

Automatically translating system software from C to Rust is an appealing but challenging problem, as it requires whole-program reasoning to satisfy Rust’s ownership and borrowing discipline. A key enabling step in whole-program translation is interface translation , which produces Rust declarations for the C program’s top-level declarations (i.e., structs and function signatures), enabling modular and incremental code translation. This paper introduces correct, precise C-to-Rust interface translation, called &inator . &inator employs a novel constraint-based formulation of semantic equivalence and type correctness including borrow-checking rules to produce a Rust interface that is correct (i.e., the interface admits a semantics-preserving implementation in safe Rust) and precise (i.e., it uses the simplest, least costly types). Our results show &inator produces correct, precise Rust interfaces for real C programs, but support for certain C features and scaling to large programs are challenges left for future work. This work advances the state of the art by being the first correct, precise approach to C-to-Rust interface translation.

链接与引用

DOI 原文 · arXiv · PDF（开放获取） · DBLP

BibTeX 
@article{ChenCB26,
  title = {&inator: Correct, Precise C-to-Rust Interface Translation},
  author = {Victor Chen and Ayden Coughlin and Michael D. Bond},
  journal = {Proceedings of the ACM on Programming Languages},
  volume = {10},
  number = {PLDI},
  year = {2026},
  doi = {10.1145/3808270}
}