一句话：提出 NiceToMeetYou 框架，无需 sketch 地合成 MLIR 中实用、可证可靠的整数抽象转换器。
静态分析依赖抽象转换器为具体指令提供抽象语义，但编写既可靠又精确高效的转换器十分困难；LLVM 和 GCC 都曾因不可靠转换器导致错误编译，且 LLVM IR 中仍有数百条指令缺少转换器。本文提出 NiceToMeetYou，一个面向生产编译器常用的非关系型整数抽象域的抽象转换器程序合成框架。其核心是将合成问题分解：每个转换器由多个更简单且可靠的转换器通过 meet 组合而成，新合成的片段逐步填补最终转换器的精度缺口；设计目标是批量自动化，无需用户提供 sketch。合成结果通过降低到已有 MLIR 的 SMT dialect 进行验证。实验表明，合成转换器均可证明可靠，其中 17% 比 LLVM 提供的转换器更精确。
Static analyses play a fundamental role during compilation: they discover facts that are true in all executions of the code being compiled, and then these facts are used to justify optimizations and diagnostics. Each static analysis is based on a collection of abstract transformers that provide abstract semantics for the concrete instructions that make up a program. It can be challenging to implement abstract transformers that are sound, precise, and efficient—and in fact both LLVM and GCC have suffered from miscompilations caused by unsound abstract transformers. Moreover, even after more than 20 years of development, LLVM lacks abstract transformers for hundreds of instructions in its intermediate representation (IR). We developed NiceToMeetYou : a program synthesis framework for abstract transformers that are aimed at the kinds of non-relational integer abstract domains that are heavily used by today’s production compilers. It exploits a simple but novel technique for breaking the synthesis problem into parts: each of our transformers is the meet of a collection of simpler, sound transformers that are synthesized such that each new piece fills a gap in the precision of the final transformer. Our design point is bulk automation: no sketches are required. Transformers are verified by lowering to a previously-created SMT dialect of MLIR. Each of our synthesized transformers is provably sound and some (17 %) are more precise than those provided by LLVM.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{PengKFGRD26,
title = {Nice to Meet You: Synthesizing Practical MLIR Abstract Transformers},
author = {Xuanyu Peng and Dominic Kennedy and Yuyou Fan and Ben Greenman and John Regehr and Loris D'Antoni},
journal = {Proceedings of the ACM on Programming Languages},
volume = {10},
number = {POPL},
year = {2026},
doi = {10.1145/3776722}
}