Présentation
Eurydice, lancé en 2023 au sein du projet Aeneas, propose de transformer du code Rust en C « lisible ». Le projet, maintenu par des chercheurs d’Inria et de Microsoft, combine des licences MIT et Apache‑2.0. Son objectif principal est de faciliter la migration de logiciels à haute assurance vers Rust, en offrant une étape intermédiaire exploitable par les outils de vérification et de conformité qui attendent du C.
Architecture et fonctionnement
Le compilateur suit la chaîne classique : il reçoit un programme Rust, le convertit en une représentation intermédiaire (IR), applique une série de passes d’optimisation et génère du C. La phase d’extraction de l’IR repose sur l’outil Aeneas Charon, qui interroge le compilateur officiel rustc pour obtenir le MIR (Medium‑level IR) sous forme JSON. Eurydice lit ce JSON, le transforme en une IR interne compatible avec le backend KaRaMeL, puis produit du C.
Un aspect clé est la préservation de la structure source. Par exemple, la fonction Rust suivante :
fn gcd(a: u64, b: u64) -> u64 {
if b == 0 { a } else { gcd(b, a % b) }
}
fn lcm(a: u64, b: u64) -> u64 {
(a * b) / gcd(a, b)
}est traduite en C avec des variables temporaires explicites afin de respecter l’ordre d’évaluation Rust :
uint64_t example_gcd(uint64_t a, uint64_t b) {
uint64_t uu____0;
if (b == 0ULL) {
uu____0 = a;
} else {
uu____0 = example_gcd(b, a % b);
}
return uu____0;
}
uint64_t example_lcm(uint64_t a, uint64_t b) {
uint64_t uu____0 = a * b;
return uu____0 / example_gcd(a, b);
}Cette approche contraste avec rustc, qui génère du code fortement optimisé mais difficile à lire.
Limitations et défis
La conversion n’est pas universelle. Les boucles basées sur des itérateurs Rust sont traduites en boucles while appelant du code de support, ce qui alourdit le résultat. Les génériques posent un problème majeur : le C ne possède pas de mécanisme de paramétrage de type, obligeant Eurydice à monomorphiser chaque instance. Le code produit peut donc contenir plusieurs fonctions identiques hormis le type, alors que l’équivalent idiomatique C recourrait à des macros ou à void *.
Les types à taille dynamique sont traités de deux façons : une version avec un tableau flexible et une version avec un tableau à taille connue. La conversion entre ces deux représentations est sans coût d’exécution, mais elle viole la règle du strict‑aliasing du C. Pour éviter des diagnostics erronés, les développeurs sont invités à compiler le code généré avec l’option -fno-strict-aliasing.
Enfin, Eurydice dépend de Charon pour le parsing Rust. Des fonctionnalités récentes comme les const generics bloquent souvent le processus, limitant l’usage du compilateur à de petits exemples.
Perspectives d’utilisation
Malgré ses contraintes, Eurydice a déjà servi à porter des routines de cryptographie post‑quantique de Rust vers C, démontrant son utilité dans des contextes où les outils de vérification formelle sont matures pour le C mais pas pour le Rust. En tant que pont, il permet d’exploiter les bibliothèques Rust dans des environnements dépourvus de chaîne d’outils Rust, tout en conservant une trace structurée du code source pour les analyses de sécurité.
