Eurydice: yüksək etibarlı proqramlar üçün Rust-un oxunaqlı C-ə çevrilməsi

Rust-dan C-ə yüksək etibarlı kod üçün keçid

Eurydice Rust proqramlarını C mənbə koduna çevirən və kodun ilk strukturunu dəyişməz saxlayan tədqiqat layihəsidir. O, mövcud və yoxlama və uyğunluq alətləri giriş məlumatı kimi C tələb edən yüksək etibarlı proqram layihələrinə yönəlib. Bu cür alətlər birbaşa Rust ilə işləməyi öyrənməmişdən əvvəl, Eurydice daha səliqəli keçid təklif edir və həmçinin C kompilyatoru olan, lakin işləyən Rust kompilyatoru olmayan mühitlər üçün əsas ola bilər. Layihə artıq postkvant kriptografiyasının bir neçə rutininin Rust-dan C-ə kompilyasiya üçün istifadə olunub.

Eurydice 2023-cü ildə başladı və MIT ilə Apache-2.0 şərtlərinin qarışığı ilə lisenziyalanıb. O, Rust kodunda formal və yoxlamadan istifadə alətləri yaradan Aeneas layihəsinin hissəsidir. Aeneas layihələrini Inria, Fransa Milli Kompüter Elmləri İnstitutu və Microsoft əməkdaşları dəstəkləyir və onlar xarici töhfə qəbul edirlər.

Optimallaşdırma əvəzinə strukturun saxlanması

Kompilyatorların əksəriyyəti kimi Eurydice Rust proqramını alır, onu ara təsvirə çevirir, transformasiya seriyası icra edir və nəticəni daha aşağı səviyyəli dildə, bu halda C-də çıxarır. Onun fərqli məqsədi isə çıxışın oxunaqlı qalması üçün mənbənin ümumi strukturunu qorumaq və eyni zamanda Rust-da olan, C-də olmayan konstruksiyaları aradan qaldırmaqdır. Oriyinal qiymətlərmə ardıcıllığının müəyyən edilməsi lazım olan yerlərdə alət əlavə olaraq müvəqqəti dəyişənlər təqdim edir. Eyni funksiyaların rustc ilə kompilyasiyası, əksinə, tam bit manipulyasiyası əməliyyatları ilə mürəkkəb dövrər yaradır ki, bu da maşın kodu çıxışı üçün uyğundur, lakin oxunaqlılıq baxımından əhəmiyyətli dərəcədə azdır.

Tərcümə harada çətinləşir

Bütün Rust proqramlarının sadiqlə C-də təsviri mümkün deyil. İterator əsaslı, diapazon əvəzinə for dövrəri while dövrərinə kompilyasiya edilməlidir ki, Eurydice kömək kodu iterator vəziyyətini idarə edə biləsə. C-də generik anlayışı olmadığı üçün çevirmə zamanı Rust kodunun monomorfizmə gətirilməsi lazımdır, bu da yalnız tip ilə fərqlənən funksiyaların bir neçə implementasiyası yarada bilər. Dinamik ölçülü tiplər xüsusi böyük çətinlik yaradır: Eurydice iki təsvir çıxarır, birini elastik massiv üzvü, digərini isə məlum uzunluqlu massiv üzvü ilə. Aralarında keçid işə salınanda heç nə etmir, lakin texniki olaraq C-nin sərt aliasing qaydasını pozur, buna görə layihə yaradılmış kodu -fno-strict-aliasing bayrağı ilə kompilyasiya etməyi məsləhət görür.

Hazırki məhdudiyyətlər və müvafiq alətlər

Eurydice KaRaMeL-ə əsaslanır, o, eyni yanaşmanı daha abstrakt dildə, bu halda F* proqramlaşdırma dili üçün strukturallaşdırılmış C-ə kompilyasiya üçün istifadə edir. Öz parseri və tip yoxlayıcısı yeritmək əvəzinə Eurydice, rustc-dən emal edilmiş və əvvəlcədən işlənmiş proqramı çıxaran və onun orta səviyyəli ara təsvirini JSON kimi verən digər Aeneas aləti Charon-a güvənir. Praktikada Charon tez-tez const generics kimi Rust-un daha yeni xüsusiyyətlərini dəstəkləmir, buna görə Eurydice hal-hazırda mürəkkəb Rust xüsusiyyətlərini arxada qoyan kiçik, özünəkifayət proqramlarında ən yaxşı işləyir. Oriyinal təsvirin müəllifi alətin ən çox qiymətli olduğunu, Rust kodunun dəyişikliyini davam etdirdiyi və C versiyasını sinxron saxlamaq üçün avtomatik yol lazım olduğu vaxtda bildirir. Eurydice yalnız Rust kodunu daha çox mühitə uyğunlaşdıran sürətli artan alətlər koleksiyasında ən yeni qeyddir.

Mənbələr: lwn.net