论文
翻译标签团队:形式规则和 LLM 一起翻译的宏多于分开翻译的宏
Translation Tag Team: Formal Rules and LLMs Translate More Macros Together than Apart
摘要
现代关键软件基础设施主要是用 C 语言编写的。由于 C 语言缺乏内存安全性,研究人员正在研究将 C 语言自动翻译为 Rust 等更安全的语言。但现实世界的 C 软件不仅仅包含 C 代码,还经常使用称为宏的命名代码片段,这些代码片段不属于 C 语言本身。最先进的技术通过在翻译 C 代码之前先对其进行预处理来避免翻译宏。但这种方法产生的翻译与原始 C 代码不同,因为预处理内联了所有宏定义。为了保留翻译代码中宏的使用,我们研究了宏和 C 共享的语言特性,并将它们提炼成第一个正式指定的翻译器 MerC。为了评估 MerC,我们引入了第一个宏翻译基准 MacroBench,其中的测试用例基于从实际 C 程序中随机采样的宏。我们发现 MerC 支持 MacroBench 50% 的宏测试用例。我们还使用 MacroBench 来评估 大语言模型 (LLM) 在执行先前未研究的宏翻译任务时的有效性。 LLM 比 MerC 多翻译了 22% 到 77% 的 MacroBench,但其中 8% 和 28% 的翻译是不正确的翻译,需要开发人员进行额外验证。相比之下,MerC 只产生正确的翻译。我们的主要见解是,首先运行 MerC,然后在其余部分上使用 LLM 比单独使用任一技术获得更大的好处。这种标签团队方法的平均失败率比 LLM 低 32%,同时翻译的测试用例比 MerC 平均多 51%。