一句话：将形式语义作为一等公民引入 MLIR，设计验证方言以支持编译器 IR 的语义编码与通用验证工具。
MLIR 是支持可扩展中间表示（dialect）的工具包，但以语法为中心，无法直接编码操作语义，依赖语义的工具必须手工构建。作者将形式语义作为一等公民，设计一组验证方言，实现关注点分离：编译器开发者以 lowering 定义语义，SMT 专家提供 SMT 编码，工具构建者创建方言无关验证工具。为五个方言定义语义，构建三个无关工具，发现五个误编译错误，验证一个规范化 pass 及 known/demanded bits 传递函数；改进后的传递函数平均多检测出 36.6% 的 known bits。
MLIR is a toolkit supporting the development of extensible and composable intermediate representations (IRs) called dialects ; it was created in response to rapid changes in hardware platforms, programming languages, and application domains such as machine learning. MLIR supports development teams creating compilers and compiler-adjacent tools by factoring out common infrastructure such as parsers and printers. A major limitation of MLIR is that it is syntax-focused: it has no support for directly encoding the semantics of operations in its dialects. Thus, at present, the parts of MLIR tools that depend on semantics—optimizers, analyzers, verifiers, transformers—must all be engineered by hand. Our work makes formal semantics a first-class citizen in the MLIR ecosystem. We designed and implemented a collection of semantics-supporting MLIR dialects for encoding the semantics of compiler IRs. These dialects support a separation of concerns between three domains of expertise when building formal-methods-based tooling for compilers. First, compiler developers define their dialect’s semantics as a lowering (compilation transformation) from their dialect to one or more of ours. Second, SMT solver experts provide tools to optimize domain-specific high-level semantics and lower them to SMT queries. Third, tool builders create dialect-independent verification tools. We validate our work by defining semantics for five key MLIR dialects, defining a state-of-the-art SMT encoding for memory-based semantics, and building three dialect-agnostic tools, which we used to find five miscompilation bugs in upstream MLIR, verify a canonicalization pass, and also formally verify transfer functions for two dataflow analyses: “known bits” (that finds individual bits that are always zero or one in all executions) and “demanded bits” (that finds don't-care bits). The transfer functions that we verify are improved versions of those in upstream MLIR; they detect on average 36.6% more known bits in real-world MLIR programs compared to the upstream implementation.
@article{paperbot3092,
title = {First-Class Verification Dialects for MLIR},
author = {Mathieu Fehr and Yuyou Fan and Hugo Pompougnac and John Regehr and Tobias Grosser},
journal = {Proceedings of the ACM on Programming Languages},
volume = {9},
number = {PLDI},
year = {2025},
doi = {10.1145/3729309}
}