Eurydice: Dự án biên dịch mã Rust thành C dễ đọc

Cách đây vài năm, cách duy nhất để biên dịch mã Rust là sử dụng trình biên dịch rustc với backend LLVM. Kể từ đó, nhiều dự án như mrustc, gccrs, rust_codegen_gcc và Cranelift đã đạt được những tiến bộ vượt bậc trong việc đa dạng hóa các trình biên dịch cho Rust.

Dự án mới nhất trong số đó, Eurydice, theo đuổi một mục tiêu tham vọng hơn: chuyển đổi mã Rust thành mã C sạch. Điều này đặc biệt hữu ích trong lĩnh vực phần mềm yêu cầu độ đảm bảo cao, nơi các công cụ xác minh và tuân thủ hiện có chỉ hỗ trợ C.

Eurydice là gì?

Eurydice được khởi động vào năm 2023, bao gồm một phần mã theo giấy phép MIT và một phần theo giấy phép Apache-2.0. Đây là một phần của dự án Aeneas — dự án phát triển nhiều công cụ liên quan đến việc áp dụng các công cụ xác minh hình thức cho mã Rust.

Các dự án thuộc Aeneas được duy trì bởi một nhóm nhân sự làm việc tại Inria (viện nghiên cứu khoa học máy tính quốc gia Pháp) và Microsoft, nhưng họ cũng chấp nhận đóng góp từ bên ngoài.

Eurydice tuân theo cấu trúc chung của nhiều trình biên dịch: nhận chương trình Rust, chuyển đổi thành biểu diễn trung gian (IR), tinh chỉnh IR qua một loạt các bước xử lý, rồi xuất ra mã nguồn ở ngôn ngữ bậc thấp hơn — trong trường hợp này là C.

Điểm khác biệt so với các trình biên dịch khác

Không giống các trình biên dịch khác, Eurydice tập trung vào việc bảo toàn cấu trúc tổng thể của mã trong khi loại bỏ những cấu trúc tồn tại trong Rust nhưng không có trong C.

Ví dụ, xét hàm Rust tính bội chung nhỏ nhất của hai số thông qua ước chung lớn nhất. Khi biên dịch bằng Eurydice sang C, mã kết quả vẫn giữ nguyên cấu trúc logic, thậm chí bảo toàn cả thứ tự đánh giá của bản gốc bằng cách thêm các biến tạm thời khi cần thiết.

Trong khi đó, nếu biên dịch cùng các hàm đó bằng rustc, kết quả là một cặp vòng lặp chằng chịt với các phép toán bit — phù hợp để xuất ra mã máy nhưng khó đọc hơn nhiều.

Những thách thức kỹ thuật

Tất nhiên, không phải mọi chương trình Rust đều có thể được biểu diễn trung thực trong C. Một số thách thức chính bao gồm:

• Vòng lặp với iterator: Các vòng lặp dùng iterator thay vì range cần được biên dịch thành vòng lặp while gọi vào mã hỗ trợ của Eurydice để quản lý trạng thái iterator.
• Kiểu generic: C không có khái niệm generic, nên mã Rust cần được đơn hình hóa (monomorphize) trong quá trình chuyển đổi. Điều này có thể tạo ra nhiều phiên bản hàm chỉ khác nhau về kiểu.
• Kiểu kích thước động: Rust cho phép định nghĩa cấu trúc với trường có kích thước không cố định. Eurydice phát ra hai loại biểu diễn khác nhau để bảo toàn chi tiết ngữ nghĩa quan trọng cho việc xác minh hình thức.

Do việc chuyển đổi giữa hai biểu diễn này vi phạm quy tắc strict-aliasing của C, tác giả Protzenko khuyến nghị biên dịch mã do Eurydice tạo ra với cờ -fno-strict-aliasing.

Công cụ liên quan và hạn chế hiện tại

Cách tiếp cận biên dịch ngôn ngữ trừu tượng hơn sang C mà vẫn bảo toàn cấu trúc mã không phải là mới. Dự án KaRaMeL — nền tảng mà Eurydice dựa trên — cũng làm điều tương tự cho ngôn ngữ F*, một ngôn ngữ lập trình hàm có kiểu phụ thuộc được dùng để phát triển các thư viện mật mã.

Hiện tại, Eurydice chưa thể mở rộng quy mô vượt xa các ví dụ nhỏ. Thay vì tự triển khai bộ phân tích cú pháp và kiểm tra kiểu cho Rust, Eurydice sử dụng công cụ Charon khác của Aeneas để trích xuất chương trình đã được phân tích từ rustc. Tuy nhiên, Charon thường bị vướng bởi các tính năng Rust mới như const generics.

Khi Charon hoạt động được, nó xuất biểu diễn trung gian bậc trung (MIR) của rustc dưới dạng JSON. Eurydice đọc JSON này và chuyển đổi sang biểu diễn trung gian của KaRaMeL, sau đó thực hiện một loạt bước xử lý nhỏ để loại bỏ các chi tiết đặc thù của Rust trước khi chuyển sang logic sinh mã mà KaRaMeL dùng cho F*.

Đánh giá và triển vọng

Ở dạng hiện tại, Eurydice hoạt động tốt nhất với các chương trình nhỏ, khép kín và tránh các tính năng Rust phức tạp. Trong phạm vi đó, nó hoạt động hiệu quả: mã tạo ra giữ nguyên cấu trúc như mã Rust gốc, ngoại trừ những chỗ Eurydice phát sinh thêm biến trung gian hoặc cần mã keo để triển khai tính năng phức tạp hơn.

Mặt khác, mã nhỏ khép kín cũng là loại dễ viết lại thủ công nhất. Do đó, việc đưa Eurydice vào chỉ thực sự đáng giá nếu mã Rust gốc sẽ được cập nhật thường xuyên và người dùng muốn có giải pháp tự động để giữ chúng đồng bộ.

Dù vậy, Eurydice chỉ là công cụ mới nhất trong bộ sưu tập đang mở rộng nhanh chóng các phương pháp để đưa mã Rust thích nghi với nhiều môi trường khác nhau. Đối với các dự án phần mềm yêu cầu độ đảm bảo cao tại Việt Nam — đặc biệt trong lĩnh vực tài chính, viễn thông hay quốc phòng — nơi các công cụ xác minh và tuân thủ vẫn dựa trên C, Eurydice có thể mở ra hướng tiếp cận mới để tận dụng lợi ích an toàn bộ nhớ của Rust mà không phải từ bỏ hoàn toàn hệ sinh thái công cụ hiện có.