Compiling Rust to readable C with Eurydice

Since the inception of the Rust programming language, a handful of projects have emerged, striving to expand the compiler's versatility. Among these endeavors, the most recent, Eurydice, stands out with its unique objective: translating Rust code into clean C code. This conversion holds considerable value in the realm of high-assurance software development, where existing verification and compliance tools predominantly operate on C code.

Until such tools evolve to accommodate Rust, Eurydice presents a potential solution, facilitating a more seamless transition and serving as a precursor for environments equipped with C compilers but lacking a functional Rust compiler.

Eurydice, initiated in 2023, is an integral part of the Aeneas project, a collection of tools aimed at applying formal verification techniques to Rust code. The project, overseen by a team from Inria (France's national computer-science research institute) and Microsoft, welcomes contributions from external developers. Eurydice adheres to a typical compiler architecture, taking a Rust program, converting it into an intermediate representation (IR), refining the IR through a series of transformations, and ultimately producing code in a lower-level language, in this instance, C.

Jonathan Protzenko, the most active contributor to Eurydice, outlines the project's methodology in a detailed blog post. However, unlike traditional compilers, Eurydice places emphasis on maintaining the overall structure of the code while eliminating Rust-specific constructs. For instance, consider a Rust function calculating the least common multiple of two numbers using their greatest common denominator. Eurydice translates such functions into C as follows:

While the comprehensibility of the resulting C code is subjective, it invariably preserves the original code's structure. Moreover, the evaluation order is upheld by introducing auxiliary temporary variables (e.g., uu____0 in example_lcm()) where necessary to define an order (Rust guarantees that if the multiplication overflows and triggers an error, it occurs prior to any side effects from calling example_gcd(), whereas C only ensures that if the multiplication is conducted in a distinct statement).

Nonetheless, not all Rust programs can be accurately represented in C. For example, loops utilizing iterators instead of ranges necessitate conversion into while loops that call upon Eurydice's support code to manage the iterator's state. More critically, C lacks support for generics. To accommodate this, Rust code must undergo monomorphization during conversion, resulting in multiple distinct implementations of a function that differ solely by type.

Although the idiomatic C approach would involve macros or void* arguments, the preservation of this semantic detail in C, particularly concerning formal verification, is crucial.

Some structures in Rust, such as those featuring dynamically sized types, pose unique challenges during conversion. In Rust, a structure may have a field with a non-fixed size, akin to flexible array members in C. However, if the structure is generic, and one of the generic users assigns the flexibly sized field a type with a known size, the compiler can capitalize on this information to bypass bounds checks where appropriate.

This nuanced separation, where certain parts of the code may be aware of a type's size while others may not, must be maintained in C to account for the possibility of formal verification. Eurydice addresses this by emitting two distinct types: one with a flexible array member and another with a known-length array member. Converting between these representations is a runtime no-op, but it technically contravenes C's strict-aliasing rule.

Consequently, Protzenko advises compiling Eurydice-generated code with the -fno-strict-aliasing flag to mitigate potential issues.