paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Ratte: Fuzzing for Miscompilations in Multi-Level Compilers Using Composable Semantics

Ratte:使用可组合语义对多级编译器中的错误编译进行模糊测试
ASPLOS Proceedings of the 30th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, Volume 22025匹配度 3/10 · 论文聚焦 MLIR 多级编译器的模糊测试、方言语义与错误编译发现,属于编译器测试与形式语义方向,但未涉及用户核心关注的静态分析、LLM/Agent、浮点程序分析或贝叶斯程序分析。仅在 PL/编译器工程与工业界落地偏好上有一定边缘相关性,因此匹配度较低。引用 7 inbox
Pingshi Yu, Nicolas Wu, Alastair F. Donaldson
crossref: 2026-09-12dblp: 2026-09-12

AI 速览

一句话:提出 Ratte,用可组合的方言语义与模块化模糊测试器,在生产 MLIR 中发现 6 个未知的错误编译缺陷。

多级中间表示 MLIR 以「方言」形式组织模块化的语言片段,其语义规约与实现验证面临现有技术难以应对的模块性与可组合性挑战。论文提出 Ratte 框架,用于书写可组合的方言语义并据此自动派生模块化的方言模糊测试器。其核心思想是让语义与测试器形成良性循环:模糊测试器通过生成测试用例来验证语义,而语义又约束生成器,使其产出不含未定义行为的高质量测试用例;语义与测试器的可组合性还允许以很低成本构造方言组合的生成器,这一能力在以往工作中并不存在。作者用 Ratte 在生产级 MLIR 实现中发现了 6 个此前未知的错误编译缺陷,据称是首个能发现此类缺陷的 MLIR 模糊测试器;工作还揭示出 MLIR 规范中若干表述不清之处,所提修复已被采纳,并提供了经生产实现验证的重要方言的可组合参考解释器。

问题
MLIR 的方言生态高度模块化、可组合,现有语义规约与实现验证技术未针对这种特性设计,难以系统性地暴露编译器中的错误编译(miscompilation)。
方法
提出 Ratte,为 MLIR 方言编写可组合的语义,并从语义派生模块化模糊测试器:测试器生成用例验证语义,语义反过来保证生成用例无未定义行为,且二者可组合以低成本覆盖方言组合。
评估
在生产级 MLIR 实现中运行,发现 6 个此前未知的错误编译缺陷;同时指出规范中不清晰之处并提出被采纳的修复,还给出经生产实现验证的可组合参考解释器。
原文摘要(Abstract)

Multi-level intermediate representation (MLIR) is a rapidly growing compiler framework, with its defining feature being an ecosystem of modular language fragments called dialects. Specifying dialect semantics and validating dialect implementations presents novel challenges, as existing techniques do not cater for the modularity and composability required by MLIR. We present Ratte, a framework for specifying composable dialect semantics and modular dialect fuzzers. We introduce a novel technique for the development of semantics and fuzzers for MLIR dialects, enabling a harmonious cycle where the fuzzer validates the semantics via test-case generation, whilst at the same time the semantics allow the generation of high-quality test cases that are free from undefined behaviour. The composability of semantics and fuzzers allows generators to be cheaply derived to test combinations of dialects. We have used Ratte to find 6 previously-unknown miscompilation bugs in the production MLIR implementation. To our knowledge, Ratte is the first MLIR fuzzer capable of finding such bugs. Our work identified several aspects of the MLIR specification that were unclear, for which we proposed fixes that were adopted. Our technique provides composable reference interpreters for important MLIR dialects, validated against the production implementation, which can be used in future compiler development and testing research.

链接与引用

DOI 原文 · PDF(开放获取) · DBLP

BibTeX
@inproceedings{YuWD25,
  title = {Ratte: Fuzzing for Miscompilations in Multi-Level Compilers Using Composable Semantics},
  author = {Pingshi Yu and Nicolas Wu and Alastair F. Donaldson},
  booktitle = {ASPLOS},
  year = {2025},
  doi = {10.1145/3676641.3716270}
}