Eurydice ist ein Compiler-Werkzeug aus dem Aeneas-Projekt (entwickelt von Inria und Microsoft), das Rust-Quellcode in strukturell ähnlichen C-Code übersetzt. Es richtet sich primär an sicherheitskritische Domänen, in denen formale Verifizierungswerkzeuge C voraussetzen, oder an Umgebungen ohne native Rust-Infrastruktur. Durch die Nutzung von Charon und KaRaMeL bewahrt das Tool die ursprüngliche Kontrollflussstruktur und Laufzeitsicherheit, stößt jedoch bei der Skalierung und komplexen Rust-Features wie Const-Generics an Grenzen.
Wichtigste Punkte
Ursprung und Lizenzen: Entwickelt ab 2023 als Teil des Aeneas-Projekts unter MIT- und Apache-2.0-Lizenzen durch Mitarbeiter von Inria (Frankreich) und Microsoft.
Architektur-Pipeline: Extrahiert über das Tool Charon die mittlere Zwischendarstellung (MIR) des rustc-Compilers als JSON, verarbeitet diese in der KaRaMeL-Zwischendarstellung und emittiert C-Code.
Erhaltung der Kontrollstruktur: Behält die ursprüngliche Auswertungsreihenfolge durch temporäre Variablen (z. B. uu____0) bei, um Seiteneffekte und Überlauf-Panics semantisch korrekt abzubilden.
Monomorphisierung von Generics: Da C keine generischen Typen unterstützt, dupliziert Eurydice Funktionen für jeden spezifischen Datentyp, den Code-Konsumenten anfordern.
Umgang mit dynamischen Typen: Emittiert für dynamisch dimensionierte Strukturen zwei Varianten (mit flexiblen und bekannten Array-Längen), was C's Strict-Aliasing-Regel verletzt und das Compiler-Flag -fno-strict-aliasing erfordert.
Aktuelle Einschränkungen: Funktioniert optimal für kleine, isolierte Programme; scheitert bei größeren Codebasen häufig an modernen Rust-Merkmalen wie Const-Generics in Charon.
Diskussions-Highlights
Laufzeitsicherheit und Semantik: Diskutanten bestätigen, dass in Rust definierte Laufzeitprüfungen (z. B. Array-Bounds-Checks) in die IR übernommen und somit im generierten C-Code erhalten bleiben, was für den Einsatz auf Plattformen ohne Rust-Compiler entscheidend ist.
Übertragbarkeit auf andere Sprachen: Es wird angeregt, dass ähnliche Übersetzungswerkzeuge auch für andere komplexe Sprachen wie D oder C++ von Vorteil wären.
Wortspiel zum Namen: Der Projektname „Eurydice“ wird in der Community humorvoll als Anspielung auf „You're da C“ oder „You're rid of C“ rezipiert.
Glossar
Eurydice: Ein Compiler-Werkzeug zur Übersetzung von Rust- Quellcode in strukturierten C-Code.
Aeneas: Ein akademisches und industrielles Projekt zur Anwendung formaler Verifizierungswerkzeuge auf Rust-Code.
Charon: Ein Werkzeug aus dem Aeneas-Ökosystem, das den AST und die MIR von Rust-Programmen analysiert und als JSON exportiert.
KaRaMeL: Ein Framework und Code-Generator zur Übersetzung von funktionalen Programmen (ursprünglich F*) in lesbares C.
MIR (Medium-Level Intermediate Representation): Eine Zwischenform des Rust-Compilers, die den Code auf einer CFG-basierten (Control Flow Graph) Abstraktionsebene darstellt.
Monomorphisierung: Der Prozess der Erzeugung konkreter Funktions- und Datenstrukturen für jeden spezifischen Datentyp, da C keine generischen Templates nativ unterstützt.
Strict-Aliasing: Eine Optimierungsregel des C-Standards, die untersagt, dass Zeiger unterschiedlicher Typen auf denselben Speicherbereich zugreifen; das Brechen dieser Regel erfordert das Flag -fno-strict-aliasing.
Const-Generics: Ein Rust-Sprachfeature, das Konstanten (wie Zahlenwerte) als generische Parameter in Typen und Traits erlaubt.
Bounds Checks: Automatische Laufzeitüberprüfungen, die garantieren, dass Speicher- oder Array-Zugriffe innerhalb der allozierten Grenzen erfolgen.