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

TL;DR

&inator is a novel tool that automatically translates C program interfaces into correct and precise Rust interfaces, facilitating safer and more modular system software migration.

Contribution

It introduces a constraint-based semantic and type correctness formulation for C-to-Rust interface translation, the first of its kind to ensure correctness and precision.

Findings

Produces correct Rust interfaces for real C programs

Ensures interfaces are semantics-preserving and use minimal types

Supports modular and incremental code translation

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.