Eurydice: Compiling Rust to Readable C for High-Assurance Software

A Rust to C translator for high-assurance code

Eurydice is a research project that converts Rust programs into C source code while keeping the original structure of the code intact. It targets high-assurance software projects, where existing verification and compliance tools expect C as their input. Until such tools learn to work with Rust directly, Eurydice offers a smoother transition path, and it can also serve as a stepping stone for environments that have a C compiler but no working Rust compiler. The project has already been used to compile some post-quantum-cryptography routines from Rust to C.

Eurydice was started in 2023 and is licensed under a mix of MIT and Apache-2.0 terms. It is part of the Aeneas project, which develops tools for applying formal verification to Rust code. The Aeneas projects are maintained by people employed by Inria, France's national computer science research institution, and Microsoft, and they accept outside contributions.

Structure preservation instead of optimization

Like most compilers, Eurydice takes a Rust program, converts it into an intermediate representation, applies a series of transformation passes, and emits code in a lower level language, in this case C. Its distinguishing goal, however, is to keep the output readable by preserving the overall structure of the source while removing constructs that exist in Rust but not in C. Where the evaluation order of the original must be defined, the tool introduces extra temporary variables. Compiling the same functions with rustc, by contrast, produces entangled loops filled with bit twiddling operations, which suits machine code output but is far less readable.

Where the translation gets hard

Not all Rust programs can be faithfully represented in C. For loops that use an iterator instead of a range must be compiled into while loops that call into Eurydice's support code to manage iterator state. Because C has no concept of generics, Rust code must be monomorphized during conversion, which can produce several implementations of a function that differ only by type. Dynamically sized types pose a particular challenge: Eurydice emits two representations, one with a flexible array member and one with a known length array member. Converting between them is a no-op at run time but technically violates C's strict aliasing rule, so the project recommends compiling generated code with the -fno-strict-aliasing flag.

Current limits and associated tooling

Eurydice is based on KaRaMeL, which applies the same approach of compiling a more abstract language to structured C, in that case for the F* programming language. Instead of implementing its own parser and type checker, Eurydice relies on Charon, another Aeneas tool, to extract the parsed and preprocessed program from rustc and dump its medium level intermediate representation as JSON. In practice, Charon is often foiled by newer Rust features such as const generics, so Eurydice currently works best for small, self-contained programs that avoid complex Rust features. The author of the original report suggests the tool is most worthwhile when the Rust code will keep changing and an automatic way to keep the C version in sync is needed. Eurydice is only the newest entry in a rapidly expanding collection of tools that adapt Rust code to fit more environments.

Sources: lwn.net