Eurydice: Rust- լեզվի կազմը ընթեռնելի C-ում բարձր վստահելիության ծրագրերի համար

Rust-ից C-ում բարձր վստահելիության կոդի եղանակ

Eurydice-ը հետազոտական նախագիծ է, որը Rust-ի ծրագրերը վերածում է C-ի կոդի և անփոփոխ պահպանում կոդի սկզբնական կառուցվածքը։ Այն ուղղված է բարձր վստահելիության ծրագրային նախագծերին, որտեղ առկա վերիֆիկացիայի և համապատասխանության գործիքները պահանջում են C-ն որպես մուտքային տվյալ։ Մինչև այդպիսի գործիքները ուսումնասիրելու ուղղակի աշխատանքը Rust-ի հետ, Eurydice-ն առաջարկում է ավելի հեշտ անցումի ճանապարհ և կարող է ծառայել որպես սկզբնական փուլ այն միջավայրերի համար, որտեղ առկա է C-ի կոմպիլյատորը, բայց չկա աշխատող Rust-ի կոմպիլյատորը։ Նախագիծն արդեն օգտագործվել է պաստկանտուկ կրիպտոգրաֆիայի մի քանի ռուտինների Rust-ից C-ում վերակոմպիլյացնելու համար։

Eurydice-ն սկսել է 2023 թվականին և լցենզիավորված է MIT-ի և Apache-2.0-ի պայմանների խառնուրդով։ Այն Aeneas նախագծի մասն է, որը ստեղծում է գործիքներ Rust-ի կոդի վրա ձևական վերիֆիկացիայի կիրամելու համար։ Aeneas նախագծերը պահպանում են Inria-ն՝ Ֆրանսիայի ազգային համակարգչային գիտության հետազոտական ինստիտուտի և Microsoft-ի աշխատակիցները, և նրանք ընդունում են արտահայտի ներդրում։

Կառուցվածքի պահպանումը օպտիմիզացիայի փոխարեն

Ինչպես կոմպիլյատորների մեծամասնությունը, Eurydice-ն վերցնում է Rust-ի ծրագիրը, վերածում միջանկյալ ներկայացման, կատարում տրանսֆորմացիաների շարք և արտադրում կոդ ավելի ցածր մակարդակի լեզվով՝ այս դեպքում C-ով։ Նրա տարբերակի նպատակն է, որ արտադրված ընթեռնելի կոդը պահպանի կոդի ընդհանուր կառուցվածքը և միաժամանակ հեռացնի այդ կառուցումները, որոնք գոյություն ունեն Rust-ում, բայց չկան C-ում։ Այնտեղ, որտեղ սկզբնական գնահատման հաջորդականությունը պետք է որոշի, գործիքը լրացուցիչ ժամանակավոր փոփոխականներ է մուտքագրում։ Նույն ֆունկցիաների կոմպիլյացիան rustc-ով, ընդհակառակը, ստեղծում է բարդ ցիկլեր՝ լի բիթերի մանիպուլյացիայի գործողություններով, որոնք համապատասխան են մեքենայական կոդի արտադրության համար, բայց շատ ավելի քիչ ընթեռնելի են։

Որտեղ դժվարանում է թարգմանությունը

Հնարավոր չէ միասնական ձևով ներկայացնել բոլոր Rust-ի ծրագրերը C-ում։ Իտերատորի վրա հիմնված միջակայքների փոխարեն for ցիկլերը պետք է վերակոմպիլյացվեն 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