Eurydice превращает код Rust в чистый C, но пока только для небольших программ

Обозреватель LWN разбирает Eurydice, инструмент, который преобразует код на Rust в «чистый» код на C. Раньше Rust компилировался в основном через rustc с бэкендом LLVM; затем появились альтернативные реализации, mrustc, gccrs, rust_codegen_gcc и Cranelift. Цель Eurydice, по словам автора статьи, амбициознее: получить на выходе не машинный код, а C, который можно читать и подавать в существующие средства проверки. Это особенно полезно в системах с высокими требованиями к надёжности, где инструменты верификации и проверки соответствия стандартам рассчитаны на C. Пока их не научили работать с Rust, Eurydice может сделать переход мягче, а также стать ступенькой для сред, где есть компилятор C, но нет работающего компилятора Rust. Для примера: с помощью Eurydice уже компилировали некоторые процедуры постквантовой криптографии из Rust в C.

Проект начат в 2023 году, часть кода лицензирована под MIT, часть, под Apache-2.0. Он входит в проект Aeneas, который разрабатывает инструменты для применения средств формальной верификации к коду на Rust. Aeneas поддерживает группа сотрудников Inria (национального института исследований в области информатики Франции) и Microsoft, при этом внешние вклады принимаются. Самый активный участник Eurydice, Jonathan Protzenko, у него есть блог-запись с объяснением подхода.

Устройство обычное для компилятора: программа на Rust превращается в промежуточное представление, оно изменяется серией проходов, затем выводится код на C. Отличие в том, что Eurydice старается сохранить общую структуру кода, убирая лишь конструкции, существующие в Rust, но отсутствующие в C. В примере с функциями gcd и lcm (наименьшее общее кратное через наибольший общий делитель) получается C-код с рекурсивным вызовом и временной переменной uu____0. Порядок вычислений сохраняется за счёт дополнительных временных переменных: Rust гарантирует, что при переполнении умножения паника случится до побочных эффектов вызова gcd, а C гарантирует это, только если умножение выполнено отдельным оператором. Тот же код, скомпилированный через rustc, превращается в пару запутанных циклов с битовыми трюками, для машинного кода это уместно, но читать такое куда труднее. Является ли результат Eurydice «читаемым», вопрос вкуса, подчёркивает автор, но структуру он сохраняет.

Не всё в Rust можно точно выразить в C. Циклы for по итератору приходится превращать в циклы while с вызовами вспомогательного кода Eurydice, который хранит состояние итератора. В C нет обобщённых типов (generics), поэтому код при конвертации мономорфизируется: появляется несколько реализаций функции, отличающихся только типом, тогда как в идиоматичном C обычно применяют макросы или аргументы void *. Отдельная трудность, типы динамического размера. В Rust структура может содержать поле неизвестного размера (как гибкий член массива в C), но если обобщённая структура используется с полем известного размера, компилятор вправе опустить проверки границ. Чтобы не получить в C «лишних» предупреждений о пропущенных проверках и не выдумывать несуществующих путей ошибки, Eurydice порождает два разных типа: с гибким членом массива и с массивом известной длины. Преобразование между ними ничего не стоит во время выполнения, но формально нарушает правило строгого алиасинга C, поэтому Protzenko рекомендует компилировать код, сгенерированный Eurydice, с флагом -fno-strict-aliasing.

Подход не нов: проект KaRaMeL, на котором основан Eurydice, делает то же самое для языка F*, функционального языка с зависимыми типами, на котором пишут криптографические библиотеки. Доказуемо корректные программы на F* компилируются в эквивалентный C, и библиотеки можно использовать там, где важна производительность. Eurydice не пишет собственный парсер и систему типов для Rust: он берёт разобранную и предобработанную программу из rustc через ещё один инструмент Aeneas, Charon. Тот выгружает среднеуровневое промежуточное представление rustc (MIR) в виде JSON вместе с нужными флагами компиляции; Eurydice читает JSON, переводит в промежуточное представление KaRaMeL, прогоняет через небольшие проходы, убирающие детали Rust, и отдаёт общему с F* генератору кода.

Главная оговорка: пока Eurydice почти не масштабируется дальше небольших примеров. Когда автор статьи проверял Charon на разных пакетах Rust, тот регулярно отказывал на более новых возможностях языка, например на константных обобщениях (const generics). Итог: инструмент лучше всего подходит для небольших самодостаточных программ без сложных возможностей Rust, и в этой нише работает хорошо. Но такой код проще всего переписать вручную, поэтому подключать Eurydice стоит, вероятно, только если исходный Rust-код будет развиваться и нужен автоматический способ держать C-версию в синхронизации.

Ключевые факты

Eurydice, инструмент проекта Aeneas, который преобразует код на Rust в чистый C, сохраняя структуру исходной программы и порядок вычислений (через дополнительные временные переменные).
Цель, высоконадёжное ПО, где инструменты верификации и проверки соответствия рассчитаны на C; уже компилировали некоторые процедуры постквантовой криптографии.
Конвейер: Charon выгружает MIR из rustc в JSON, Eurydice переводит его в представление KaRaMeL и генерирует C тем же кодом, что используется для F*.
Для типов динамического размера Eurydice порождает два разных типа; это формально нарушает строгий алиасинг, поэтому рекомендован флаг -fno-strict-aliasing.
Главное ограничение: пока работает хорошо лишь для небольших самодостаточных программ; Charon регулярно отказывает на новых возможностях Rust вроде const generics.

Почему это важно

Rust всё чаще приходит в области, где используются проверенные годами средства верификации и сертификации, заточенные под C. Eurydice, попытка сократить этот разрыв: получить из Rust код на C, по которому можно вести анализ и который ещё можно читать. Для сред без рабочего компилятора Rust это также способ доставить туда код на Rust. В отличие от других проектов, расширяющих число реализаций компилятора Rust, цель здесь иная, читаемый C на выходе.

Кому это важно

Разработчикам высоконадёжного ПО и криптографических библиотек, у которых процесс проверки и сертификации привязан к C; командам, чьи целевые среды имеют компилятор C, но не имеют Rust; тем, кто следит за проектом Aeneas и формальной верификацией Rust. Для остальных это скорее любопытный инструмент в «быстро растущей коллекции способов приспособить Rust к новым средам», как пишет автор статьи.

Как это применить

Eurydice подходит для небольших самодостаточных программ без сложных возможностей Rust. Практически: Charon выгружает MIR в JSON, Eurydice конвертирует его в C, а сгенерированный код нужно компилировать с -fno-strict-aliasing. Часть кода проекта распространяется под MIT, часть, под Apache-2.0. Автор статьи оговаривает, что если Rust-код не будет меняться, небольшую программу проще переписать на C вручную; смысл Eurydice, в автоматической синхронизации при дальнейших правках Rust-версии.

Можно ли доверять

Источник, обзор на LWN, где автор делится и собственным опытом: вывод о плохой масштабируемости основан на его проверке Charon на разных пакетах Rust. Конкретные пакеты, номера версий и количественные замеры в тексте не приводятся, так что оценки качественные. Оценка читаемости сгенерированного C прямо названа делом вкуса.

Риски и подводные камни

Масштабирование: инструмент плохо справляется за пределами небольших примеров, а Charon регулярно отказывает на более новых возможностях Rust, таких как const generics. Мономорфизация даёт несколько реализаций одной функции, отличающихся только типом, не так, как написал бы C-программист. Появляются дополнительные временные переменные и вспомогательный код (например, для итераторов). Преобразование между двумя представлениями типа динамического размера формально нарушает строгий алиасинг, что требует специального флага компиляции.

«К сожалению, Eurydice пока почти не масштабируется дальше небольших примеров.»

— из обзора на LWN