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接口翻译方法，推动了该领域的技术发展。