Eurydice is een project dat Rust-code compileert naar schone, leesbare C-code. Dit is met name waardevol voor high-assurance software, waarbij bestaande verificatietools vaak C vereisen. Het project maakt deel uit van het bredere Aeneas-project, beheerd door experts van Inria en Microsoft.
Technische aanpak en uitdagingen:
- Structuurbehoud: In tegenstelling tot standaard compilers probeert Eurydice de oorspronkelijke codestructuur te behouden, waarbij Rust-constructen worden vertaald naar C-equivalenten via een tussenrepresentatie (IR).
- Complexiteit: Omdat C geen generics ondersteunt, moet code worden gemonomorfiseerd. Daarnaast vormen dynamically sized types (DST's) een uitdaging, wat resulteert in het genereren van specifieke typen en het advies om de vlag
-fno-strict-aliasing te gebruiken.
- Tooling: Eurydice bouwt voort op het KaRaMeL-project en maakt gebruik van de tool Charon om de medium-level intermediate representation (MIR) uit
rustc te extraheren.
Hiertoe is het project momenteel het meest geschikt voor kleine, zelfstandige programma's die complexe Rust-functies vermijden.
Rust compileren naar leesbare C met Eurydice
Een paar jaar geleden was de enige manier om Rust-code te compileren het gebruik van de rustc-compiler met LLVM als backend. Sindsdien hebben verschillende projecten, waaronder Mutabah's Rust Compiler (mrustc), de Rust-ondersteuning van GCC (gccrs), rustcodegengcc en Cranelift, enorme stappen gezet in het diversifiëren van compiler-implementaties voor Rust. Het meest recente project, Eurydice, heeft een ambitieuzer doel: het omzetten van Rust-code naar schone C-code.
Dit is vooral nuttig voor software met een hoge betrouwbaarheid (high-assurance software), waar bestaande verificatie- en nalevingstools C verwachten. Totdat dergelijke tools worden bijgewerkt om met Rust te werken, kan Eurydice zorgen voor een soepelere overgang voor deze projecten, en dienen als springplank voor omgevingen die wel een C-compiler maar geen werkende Rust-compiler hebben. Zo is Eurydice al gebruikt om enkele routines voor post-quantumcryptografie van Rust naar C te compileren.
Eurydice is gestart in 2023 en bevat code onder de MIT- en Apache-2.0-licenties. Het maakt deel uit van het Aeneas-project, dat zich richt op de ontwikkeling van diverse tools voor het toepassen van formele verificatiemethoden op Rust-code. De verschillende Aeneas-projecten worden beheerd door een groep mensen in dienst van Inria (het nationale Franse onderzoeksinstituut voor informatica) en Microsoft, maar ze staan open voor externe bijdragen.
De aanpak van Eurydice
Eurydice volgt dezelfde algemene structuur als veel compilers: een Rust-programma wordt genomen, omgezet in een tussenrepresentatie (IR), aangepast via een reeks passes, en vervolgens uitgevoerd als code in een lagere taal (in dit geval C).
Jonathan Protzenko, de meest productieve bijdrager aan Eurydice, legt de aanpak van het project uit in een blogpost. In tegenstelling tot andere compilers is Eurydice gericht op het behouden van de algemene structuur van de code, terwijl constructen die wel in Rust maar niet in C bestaan, worden verwijderd.
Overweeg bijvoorbeeld deze Rust-functie die het kleinste gemene veelvoud (LCM) van twee getallen berekent met behulp van hun grootste gemene deler (GCD):
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)
}
Dit is hoe Eurydice deze functies compileert naar C:
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);
}
Of deze C-code als "leesbaar" wordt beschouwd, is waarschijnlijk een kwestie van smaak. Het behoudt echter wel de structuur van de code. Zelfs de evaluatievolgorde van het origineel wordt bewaard door waar nodig extra tijdelijke variabelen toe te voegen (zoals uu____0 in example_lcm()) om een volgorde te definiëren.
Rust garandeert namelijk dat als de vermenigvuldiging overloopt en een panic veroorzaakt, dit gebeurt vóór eventuele neveneffecten die worden veroorzaakt door het aanroepen van example_gcd(). C garandeert dit alleen als de vermenigvuldiging in een aparte statement wordt uitgevoerd. Het compileren van dezelfde functies met rustc resulteert daarentegen in een paar verstrengelde loops gevuld met bit-twiddling operaties; dit is passend voor machinecode, maar veel minder leesbaar.
Technische uitdagingen
Niet alle Rust-programma's kunnen getrouw worden weergegeven in C. Zo moeten for-loops die een iterator gebruiken in plaats van een bereik (range), worden gecompileerd naar while-loops die gebruikmaken van ondersteuningscode van Eurydice om de status van de iterator te beheren.
Belangrijker is dat C geen concept van generics heeft, waardoor Rust-code tijdens de conversie moet worden gemonomorfiseerd (monomorphized). Dit kan resulteren in verschillende implementaties van een functie die alleen in type verschillen. In idiomatisch C zou men vaker macro's of void *-argumenten gebruiken.
Ook de implementatie van dynamisch gedimensioneerde typen (dynamically sized types of DST's) vormt een uitdaging. In Rust kan een structuur worden gedefinieerd waarbij een van de velden geen vaste grootte heeft, vergelijkbaar met flexible array members in C:
struct DynamicallySized<U: ?Sized> {
header: usize,
my_data: U, // De compiler kent de grootte van U hier niet
}
Wanneer die structuur echter generiek is en een gebruiker van het type een veld met een bekende grootte opgeeft, kan de compiler deze kennis gebruiken om bounds checks weg te laten waar dat gepast is:
let foo: DynamicallySized<[u8; 4]> = ...;
// Geen bounds check gegenereerd, aangezien de array-grootte bekend is als 4:
let bar = foo.my_data[2];
Dit onderscheid — waarbij sommige delen van de code de grootte van een type kennen en andere niet — is een belangrijk semantisch detail dat in C bewaard moet blijven vanwege de interactie met formele verificatie. Als Eurydice DynamicallySized overal zou compileren met een flexible array member, zou analyse van de C-code kunnen wijzen op "ontbrekende" bounds checks die in Rust niet nodig waren. Omgekeerd, als Eurydice extra bounds checks zou toevoegen, zou het extra foutpaden moeten creëren die niet in de Rust-broncode voorkomen en volledig ongebruikt zouden blijven.
Daarom genereert Eurydice twee verschillende typen: een versie van het dynamisch gedimensioneerde type met een flexible array member, en één met een array-lid van bekende lengte. De conversie tussen deze twee representaties is tijdens runtime een no-op, maar het overtreedt technisch gezien de strict-aliasing regel van C. Daarom adviseert Protzenko om door Eurydice gegenereerde code te compileren met de vlag -fno-strict-aliasing.
Gerelateerde tooling
De aanpak om een abstracte taal naar C te compileren op een manier die de structuur bewaart, is niet nieuw. Het KaRaMeL-project, waarop Eurydice is gebaseerd, doet hetzelfde voor de programmeertaal F. F is een functionele taal met afhankelijke typen (dependently typed) die wordt gebruikt voor de ontwikkeling van cryptografische bibliotheken. Door bewijsbaar correcte F*-programma's naar equivalente C-code te compileren, kunnen deze bibliotheken worden gebruikt in programma's waar prestaties cruciaal zijn.
Momenteel schaalt Eurydice echter nog niet goed voorbij kleine voorbeelden. In plaats van een eigen parser en typechecker voor Rust-code te implementeren, gebruikt Eurydice een andere Aeneas-tool — Charon — om het geparseerde en gepreprocessede programma uit rustc te extraheren. Bij tests met diverse Rust-pakketten bleek Charon echter regelmatig te worden gedwarsboomd door recentere Rust-functies, zoals const generics.
Wanneer Charon wel werkt, dumpt het de medium-level intermediate representation (MIR) van rustc als JSON, samen met de nodige compiler-vlaggen. Eurydice leest deze JSON-representatie en converteert deze naar de IR van KaRaMeL. Daarna volgt een reeks kleine passes over de KaRaMeL-code om Rust-specifieke details te elimineren, waarna de code-generatielogica van KaRaMeL wordt gebruikt voor de uiteindelijke output.
In zijn huidige vorm werkt Eurydice het beste voor kleine, zelfstandige programma's die complexe Rust-functies vermijden. Binnen die niche werkt het goed; de gegenereerde code behoudt dezelfde structuur als de originele Rust-code, op de plekken waar Eurydice extra tussenvariabelen of glue code moet toevoegen. Omdat kleine, zelfstandige code echter ook het makkelijkst handmatig te herschrijven is, is het gebruik van Eurydice waarschijnlijk alleen zinvol als de originele Rust-code regelmatig wordt bijgewerkt en men een automatische oplossing wil om beide versies synchroon te houden. In ieder geval is Eurydice het nieuwste instrument in een snel groeiende verzameling methoden om Rust-code aan te passen aan diverse omgevingen.
Rust compileren naar leesbare C met Eurydice
Een paar jaar geleden was de enige manier om Rust-code te compileren het gebruik van de rustc-compiler met LLVM als backend. Sindsdien hebben verschillende projecten, waaronder Mutabah's Rust Compiler (mrustc), de Rust-ondersteuning van GCC (gccrs), rustcodegengcc en Cranelift, enorme stappen gezet in het diversifiëren van compiler-implementaties voor Rust. Het meest recente project, Eurydice, heeft een ambitieuzer doel: het omzetten van Rust-code naar schone C-code.
Dit is vooral nuttig voor software met een hoge betrouwbaarheid (high-assurance software), waar bestaande verificatie- en nalevingstools C verwachten. Totdat dergelijke tools worden bijgewerkt om met Rust te werken, kan Eurydice zorgen voor een soepelere overgang voor deze projecten, en dienen als springplank voor omgevingen die wel een C-compiler maar geen werkende Rust-compiler hebben. Zo is Eurydice al gebruikt om enkele routines voor post-quantumcryptografie van Rust naar C te compileren.
Eurydice is gestart in 2023 en bevat code onder de MIT- en Apache-2.0-licenties. Het maakt deel uit van het Aeneas-project, dat zich richt op de ontwikkeling van diverse tools voor het toepassen van formele verificatiemethoden op Rust-code. De verschillende Aeneas-projecten worden beheerd door een groep mensen in dienst van Inria (het nationale Franse onderzoeksinstituut voor informatica) en Microsoft, maar ze staan open voor externe bijdragen.
De aanpak van Eurydice
Eurydice volgt dezelfde algemene structuur als veel compilers: een Rust-programma wordt genomen, omgezet in een tussenrepresentatie (IR), aangepast via een reeks passes, en vervolgens uitgevoerd als code in een lagere taal (in dit geval C).
Jonathan Protzenko, de meest productieve bijdrager aan Eurydice, legt de aanpak van het project uit in een blogpost. In tegenstelling tot andere compilers is Eurydice gericht op het behouden van de algemene structuur van de code, terwijl constructen die wel in Rust maar niet in C bestaan, worden verwijderd.
Overweeg bijvoorbeeld deze Rust-functie die het kleinste gemene veelvoud (LCM) van twee getallen berekent met behulp van hun grootste gemene deler (GCD):
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)
}
Dit is hoe Eurydice deze functies compileert naar C:
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);
}
Of deze C-code als "leesbaar" wordt beschouwd, is waarschijnlijk een kwestie van smaak. Het behoudt echter wel de structuur van de code. Zelfs de evaluatievolgorde van het origineel wordt bewaard door waar nodig extra tijdelijke variabelen toe te voegen (zoals uu____0 in example_lcm()) om een volgorde te definiëren.
Rust garandeert namelijk dat als de vermenigvuldiging overloopt en een panic veroorzaakt, dit gebeurt vóór eventuele neveneffecten die worden veroorzaakt door het aanroepen van example_gcd(). C garandeert dit alleen als de vermenigvuldiging in een aparte statement wordt uitgevoerd. Het compileren van dezelfde functies met rustc resulteert daarentegen in een paar verstrengelde loops gevuld met bit-twiddling operaties; dit is passend voor machinecode, maar veel minder leesbaar.
Technische uitdagingen
Niet alle Rust-programma's kunnen getrouw worden weergegeven in C. Zo moeten for-loops die een iterator gebruiken in plaats van een bereik (range), worden gecompileerd naar while-loops die gebruikmaken van ondersteuningscode van Eurydice om de status van de iterator te beheren.
Belangrijker is dat C geen concept van generics heeft, waardoor Rust-code tijdens de conversie moet worden gemonomorfiseerd (monomorphized). Dit kan resulteren in verschillende implementaties van een functie die alleen in type verschillen. In idiomatisch C zou men vaker macro's of void *-argumenten gebruiken.
Ook de implementatie van dynamisch gedimensioneerde typen (dynamically sized types of DST's) vormt een uitdaging. In Rust kan een structuur worden gedefinieerd waarbij een van de velden geen vaste grootte heeft, vergelijkbaar met flexible array members in C:
struct DynamicallySized<U: ?Sized> {
header: usize,
my_data: U, // De compiler kent de grootte van U hier niet
}
Wanneer die structuur echter generiek is en een gebruiker van het type een veld met een bekende grootte opgeeft, kan de compiler deze kennis gebruiken om bounds checks weg te laten waar dat gepast is:
let foo: DynamicallySized<[u8; 4]> = ...;
// Geen bounds check gegenereerd, aangezien de array-grootte bekend is als 4:
let bar = foo.my_data[2];
Dit onderscheid — waarbij sommige delen van de code de grootte van een type kennen en andere niet — is een belangrijk semantisch detail dat in C bewaard moet blijven vanwege de interactie met formele verificatie. Als Eurydice DynamicallySized overal zou compileren met een flexible array member, zou analyse van de C-code kunnen wijzen op "ontbrekende" bounds checks die in Rust niet nodig waren. Omgekeerd, als Eurydice extra bounds checks zou toevoegen, zou het extra foutpaden moeten creëren die niet in de Rust-broncode voorkomen en volledig ongebruikt zouden blijven.
Daarom genereert Eurydice twee verschillende typen: een versie van het dynamisch gedimensioneerde type met een flexible array member, en één met een array-lid van bekende lengte. De conversie tussen deze twee representaties is tijdens runtime een no-op, maar het overtreedt technisch gezien de strict-aliasing regel van C. Daarom adviseert Protzenko om door Eurydice gegenereerde code te compileren met de vlag -fno-strict-aliasing.
Gerelateerde tooling
De aanpak om een abstracte taal naar C te compileren op een manier die de structuur bewaart, is niet nieuw. Het KaRaMeL-project, waarop Eurydice is gebaseerd, doet hetzelfde voor de programmeertaal F. F is een functionele taal met afhankelijke typen (dependently typed) die wordt gebruikt voor de ontwikkeling van cryptografische bibliotheken. Door bewijsbaar correcte F*-programma's naar equivalente C-code te compileren, kunnen deze bibliotheken worden gebruikt in programma's waar prestaties cruciaal zijn.
Momenteel schaalt Eurydice echter nog niet goed voorbij kleine voorbeelden. In plaats van een eigen parser en typechecker voor Rust-code te implementeren, gebruikt Eurydice een andere Aeneas-tool — Charon — om het geparseerde en gepreprocessede programma uit rustc te extraheren. Bij tests met diverse Rust-pakketten bleek Charon echter regelmatig te worden gedwarsboomd door recentere Rust-functies, zoals const generics.
Wanneer Charon wel werkt, dumpt het de medium-level intermediate representation (MIR) van rustc als JSON, samen met de nodige compiler-vlaggen. Eurydice leest deze JSON-representatie en converteert deze naar de IR van KaRaMeL. Daarna volgt een reeks kleine passes over de KaRaMeL-code om Rust-specifieke details te elimineren, waarna de code-generatielogica van KaRaMeL wordt gebruikt voor de uiteindelijke output.
In zijn huidige vorm werkt Eurydice het beste voor kleine, zelfstandige programma's die complexe Rust-functies vermijden. Binnen die niche werkt het goed; de gegenereerde code behoudt dezelfde structuur als de originele Rust-code, op de plekken waar Eurydice extra tussenvariabelen of glue code moet toevoegen. Omdat kleine, zelfstandige code echter ook het makkelijkst handmatig te herschrijven is, is het gebruik van Eurydice waarschijnlijk alleen zinvol als de originele Rust-code regelmatig wordt bijgewerkt en men een automatische oplossing wil om beide versies synchroon te houden. In ieder geval is Eurydice het nieuwste instrument in een snel groeiende verzameling methoden om Rust-code aan te passen aan diverse omgevingen.
Groetjes,