Eurydice是一款开源工具，能够将Rust代码编译转换为可读的C代码1。该项目由法国国家计算机科学研究机构Inria和微软员工共同维护，并接受外部贡献1，是Aeneas形式化验证项目的一部分1。Jonathan Protzenko是该项目最多产的贡献者1。
该工具采用MIT和Apache-2.0双重许可，项目始于2023年1。Eurydice基于KaRaMeL项目进行开发，后者原本用于F*编程语言的C代码生成1。在技术实现上，工具利用rustc的中级中间表示（MIR）进行转换，通过Charon工具以JSON格式提取相关代码信息1。生成的C代码采用-fno-strict-aliasing编译标志以处理严格别名规则问题1。
Eurydice通过保留原始代码结构并消除Rust特有构造来实现跨语言转换，特别适用于需要C编译器支持的高保证软件领域1。目前该工具在小型自包含程序上表现良好，但在处理const generics等较新Rust特性时存在限制1。
Eurydice is an open-source tool that translates Rust code into readable C code, maintained by developers from Inria and Microsoft as part of the Aeneas formal verification project 1. The tool preserves the structure of the original code while eliminating Rust-specific constructs, enabling cross-language conversion particularly suited for high-assurance software domains requiring C compiler support 1.
The project, which began in 2023 under MIT and Apache-2.0 dual licensing, leverages Rust's mid-level intermediate representation (MIR) for code transformation, extracting the representation through the Charon tool in JSON format 1. The generated C code is compiled using the -fno-strict-aliasing flag to address strict aliasing rule complications 1. Jonathan Protzenko serves as the project's most prolific contributor 1, while the initiative welcomes external contributions alongside its core maintenance by Inria and Microsoft personnel 1.
Currently, Eurydice demonstrates effective performance on small, self-contained programs, though it faces limitations when handling complex Rust features such as const generics 1. The tool builds upon the KaRaMeL project, which originally provided C code generation capabilities for the F* programming language 1.
评论
还没有评论，欢迎留下第一条。