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.

翻译：将系统软件从C语言自动翻译为Rust是一个颇具吸引力但充满挑战的问题，因为需要全局程序推理才能满足Rust的所有权和借用规则。在全局程序翻译过程中，接口翻译是关键步骤，它为C程序的顶层声明（即结构体和函数签名）生成Rust声明，从而实现模块化、增量式的代码翻译。本文提出了一种名为&inator的正确、精确的C到Rust接口翻译方法。&inator采用了一种新颖的基于约束的方法，该方法结合了语义等价性、类型正确性（包括借用检查规则）来生成Rust接口，确保接口的正确性（即该接口允许在安全Rust中实现语义保持）和精确性（即使用最简单、成本最低的类型）。实验结果表明，&inator能为真实的C程序生成正确、精确的Rust接口，但对某些C语言特性的支持以及扩展到大型程序仍留待未来工作解决。本工作首次提出了正确且精确的C到Rust接口翻译方法，从而推进了该领域的研究前沿。