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