Eurydice: компіляція Rust у читабельний C для високонадійного ПЗ

Код високої надійності з Rust у C

Eurydice — дослідницький проєкт, який перетворює програми Rust на вихідний код C, зберігаючи початкову структуру. Він орієнтований на високонадійні проєкти, де наявні інструменти верифікації та відповідності вимагають C як вхідних даних. Поки такі інструменти не навчаться працювати безпосередньо з Rust, Eurydice пропонує плавніший перехід і може стати першим кроком там, де є компілятор C, але немає компілятора Rust. Проєкт уже використовувався для компіляції кількох рутин постквантової криптографії з Rust у C.

Збереження структури замість оптимізації

Як і більшість компіляторів, Eurydice бере програму Rust, перетворює її на проміжне представлення, виконує серію перетворень і видає код мовою нижчого рівня — тут C. Його відмінна мета: результат має лишатися читабельним, зберігаючи загальну структуру джерела, і водночас прибирати конструкції, які існують у Rust, але не в C. Де порядок обчислень оригіналу має значення, інструмент додає тимчасові змінні. Компіляція тих самих функцій через rustc, навпаки, створює складні цикли й операції з бітами, придатні для машинного коду, але набагато гірше читабельні.

Де переклад ускладнюється

Вірне представлення кожної програми Rust у C неможливе. Цикли на основі ітераторів замість діапазонів потрібно компілювати в цикли while, якими Eurydice керує станом ітератора. Оскільки в C немає дженериків, код Rust під час перетворення мономорфізується, тому функції, які відрізняються лише типом, можуть породжувати кілька реалізацій. Динамічні типи — особлива складність: Eurydice видає два представлення, одне з гнучким членом масиву, інше з фіксованою довжиною. Перемикання між ними відбувається під час виконання, але технічно порушує суворе правило аліасингу C, тому проєкт радить компілювати згенерований код із -fno-strict-aliasing.

Поточні обмеження та супутні інструменти

Eurydice спирається на KaRaMeL, який використовує схожий підхід для компіляції структурного C із більш абстрактної мови — тут F*. Замість власних парсера й перевірки типів Eurydice покладається на Charon, ще один інструмент Aeneas, щоб взяти з rustc оброблену й попередньо проаналізовану програму і вивести її проміжне представлення у JSON. На практиці Charon часто відстає від нових властивостей Rust, таких як const generics, тому Eurydice найкраще працює з малими самодостатніми програмами, які не використовує складні властивості Rust. Автор пояснює, що інструмент найдоречніший, коли код Rust постійно змінюється і потрібен автоматичний спосіб утримувати версію C синхронно. Eurydice — лише один із швидко зростаючого набору інструментів, які адаптують код Rust до більшого середовища.

Джерела: lwn.net