NiceToMeetYou：MLIR抽象变换器自动合成框架，精度超越手工版17%，革新编译器静态分析

关键词： Abstract Transformers 、Program Synthesis 、MLIR、Static Analysis 、 Compiler Optimization 、Formal Verification

不再依赖人工编写，一个框架让编译器拥有更精确的静态分析能力。

编译器是现代软件基础设施的基石之一，它们不仅将高级语言代码翻译成机器指令，还通过各种优化手段大幅提升程序性能。在这些优化背后，静态分析 技术扮演着至关重要的角色——它能够在程序运行之前推断出代码的某些属性，为优化提供依据。

然而，静态分析的核心组件 抽象变换器 的编写一直是一项高难度、易出错的任务，它既需要保证正确性 ，又要兼顾精确性 和效率 。

现有 LLVM 和 GCC 等编译器仍存在大量指令缺乏抽象变换器，或因其不正确而引发编译错误。

• Nice to Meet You: Synthesizing Practical MLIR Abstract Transformers
• https://arxiv.org/pdf/2512.06442
• 4700 字，阅读 16 分钟，播客 19 分钟

最近，来自加州大学圣地亚哥分校和犹他大学的研究团队提出了一种名为 NiceToMeetYou 的创新框架，能够自动合成形式化验证的抽象变换器，为编译器开发带来全新的可能性。

图2：NiceToMeetYou系统架构概览

NiceToMeetYou 针对整数抽象域（如 KnownBits 和 ConstantRange），提出一种分解合成策略： 将目标变换器表示为多个简单且正确的子变换器的“交”运算，并通过动态调整的适应度函数引导合成过程逐步填补输入空间中的精度缺口。 该框架基于 MLIR 生态，利用其 SMT 方言进行形式化验证，无需用户提供程序模板或草图，支持批量自动化合成。

实验表明，NiceToMeetYou 成功合成了 40 种 LLVM 指令的抽象变换器（覆盖了 47 种目标无关指令中的 40 种），其中 在 KnownBits 域有 3 个、在 ConstantRange 域有 9 个变换器的精度优于 LLVM 手工实现，部分还可与现有变换器互补，进一步提升分析精度 。该工作为编译器开发提供了高效、可靠且可扩展的抽象变换器自动生成方法。

一、编译器优化的“大脑”：抽象变换器

要理解“抽象变换器”（abstract transformer），咱们得先从编译器的核心需求 说起，再一步步拆解它的作用。

第一步：先搞懂编译器的“痛点”——它需要“未卜先知”

编译器的 job 是把咱们写的代码（比如C、C++）变成电脑能跑的机器码，而且要尽量优化（比如让代码跑得更快、占内存更小）。要优化，编译器得“未卜先知”一个关键信息：

代码里的变量在所有可能的运行场景下，都会是哪些值？

比如：

• 知道变量x的取值一定是0~10，编译器就能把“如果x>10就报错”的代码删掉（因为永远不会触发）；
• 知道变量y的第3个比特位一定是0，编译器就能简化涉及y的位运算（比如y & 8直接等于0，不用算了）。

但编译器没法真的“跑一遍代码”来知道这些（静态分析阶段还没生成可执行文件），所以它得用一种“简化的描述”来代替真实值——这就是“抽象值”，比如用[0,10]描述x的可能范围，用“第3位是0”描述y的比特特征。

第二步：抽象变换器的核心作用——“翻译”具体操作到抽象世界

代码里全是具体操作：加、减、乘、取余、位运算（比如x + 3、y % 5）。这些操作能把“具体值”变成新的“具体值”，但编译器手里只有“抽象值”（比如x的抽象值是[2,5]），它需要一个工具来回答：

“如果输入是这个抽象值，经过这个具体操作后，输出的抽象值应该是什么？”

这个工具就是抽象变换器 。它的本质是“翻译器”—— 把代码里的“具体操作”（比如+、%），翻译成“抽象世界的操作”，让编译器能从输入抽象值算出输出抽象值。

举个通俗例子：

• 具体操作是y = x + 3；
• 编译器知道x的抽象值是[2,5]（也就是实际运行时x只能是2、3、4、5）；
• 对应的抽象变换器就要算出y的抽象值是[5,8]（2+3=5，5+3=8，所有可能的y都在这个范围里）；
• 这样编译器就知道y的范围，后续可以基于这个信息优化。

第三步：为什么这个“翻译器”这么难搞？

手动写抽象变换器是个“苦差事”，主要有两个坑：

手动编写抽象变换器的两大痛点

1. 指令繁多，难以覆盖：以 LLVM 编译器为例，其拥有超过 400 条核心指令以及上千条硬件相关的特殊指令（如 x86 的 intrinsics）。为每一条指令手动编写对应的抽象变换器是一项浩大工程，历经二十年仍未完成。大量指令至今缺乏变换器，导致编译器在分析这些指令时只能保守地返回“未知”（术语称为 top），严重限制了优化效果。
2. 易于出错，难以保证正确性：抽象变换器必须满足“可靠性”（术语 sound）要求，即其计算出的抽象值必须包含所有可能的实际值（例如，若 x 的抽象值为 [2,5]，则 y=x+3 的抽象值不能是 [6,8]，因为遗漏了 x=5 的情况）。历史上，LLVM 和 GCC 都曾因手动编写的变换器“不可靠”而导致编译出的代码产生运行时错误。

解决方案：自动合成变换器框架

鉴于手动编写方式效率低下且易错，本文提出了名为 NiceToMeetYou 的框架，旨在自动生成抽象变换器，并解决两个核心问题：

1. 保证可靠性：生成的变换器会使用数学工具（SMT 求解器 Z3）进行形式化验证，确保在所有情况下其输出的抽象值都包含实际值，从而避免因变换器错误引发的编译 Bug。
2. 追求高精度：自动合成能够发现手动编写可能遗漏的精确规则。例如，对于无符号取余运算（urem），手动变换器可能遗漏一个场景：当被除数的最大值小于除数的最小值时（例如 x 为 [2,3]，y 为 [4,5]），x % y 的结果就等于 x。自动合成的变换器能够识别此规则，从而计算出更精确的抽象值，为编译器优化提供更有效的信息。

核心思想与关键技术

NiceToMeetYou 的核心创新在于将复杂的变换器合成问题分解为多个简单部分，然后通过交集操作组合成完整的、高精度的变换器。

2.1 关键技术突破

分而治之的合成策略
传统方法试图一次性合成完整的变换器，对于复杂操作而言非常困难。NiceToMeetYou 采用分解策略：将目标变换器表示为多个简单变换器的交集。例如，对于区间域上的 max(x, y) 函数，框架可以合成四个简单变换器，其交集等价于最优变换器。

图1：变换器合成问题的输入输出示例

自适应精度引导
为避免合成的多个变换器重复覆盖相同的“简单”输入空间，框架引入了动态适应的适应度函数。每个新变换器的评分基于它对当前变换器集合尚未精确处理的输入区域的改进程度，从而引导搜索聚焦于需要新规则的输入部分。

随机搜索与归纳合成
框架采用马尔可夫链蒙特卡洛（MCMC） 随机搜索技术在程序空间中探索候选变换器。搜索过程由一个结合了正确性和精度的成本函数引导：

cost(f) = λ × (1 - Soundness(f)) + (1 - λ) × (1 - Improvement(f, F))

其中 Soundness(f) 度量变换器的可靠性，Improvement(f, F) 度量其相对于当前变换器集合 F 的精度改进。

条件归纳机制
当搜索过程中发现精度很高但不可靠的变换器时，框架不会直接丢弃，而是尝试为其合成一个条件守卫，将其应用范围限制在正确的输入子集上。这种“条件归纳”策略能够挽救潜在的宝贵启发式规则。

2.2 实际效果展示

以无符号取模运算 urem 为例，NiceToMeetYou 合成了一个由 9 个独立变换器取交集组成的解决方案。其中，8 个组件共同实现了 LLVM 现有实现中的关键启发式规则，另有 1 个是全新的启发式规则。

表 1 展示了 NiceToMeetYou 合成的 KnownBits 变换器与 LLVM 手工编写变换器的对比结果：

表1. 8位和64位整数的已知比特结果。8位结果报告了转换器与最佳转换器𝑓#匹配的测试百分比。64位结果报告了转换器的范数（按测试数量归一化），该范数反映了其不精确性。对于精确性而言，数值越高（↑）越好；对于范数而言，数值越低（↓）越好。#𝑓#是F𝑠中的转换器数量。#𝑐统计那些带有条件的转换器。#inst是这些转换器使用的MLIR指令总数。Tests是采样的测试输入数量。⊤、synth和LLVM分别呈现了三种转换器的结果：一种始终返回顶部的简单转换器、我们合成的转换器以及LLVM的手动实现转换器。meet列对应转换器synth⊓LLVM。粗体数字表示合成转换器与LLVM转换器的交在精确性上高于LLVM转换器的情况。如果没有可用的LLVM实现（N/A），我们会将合成转换器优于⊤的情况加粗。一些64位行包含短横线（-），因为随机采样未能产生任何有效的输入对。这些运算符对其输入有严格的约束

系统架构与实现

NiceToMeetYou 构建于 MLIR 生态系统之上，充分利用现有形式化语义描述。其整体架构采用外层验证循环与内层合成循环的双循环结构。

图2：NiceToMeetYou系统架构概览

3.1 关键工程优化

• 并行 MCMC 搜索：内层循环并行运行多个 MCMC 搜索实例，加速收敛过程。
• LLVM 即时编译：使用 LLVM JIT 快速编译和测试候选变换器，性能提升两个数量级。
• 智能测试生成：根据操作数位宽采用不同的测试策略，平衡覆盖率和效率。

3.2 支持的抽象域

目前，NiceToMeetYou 专注于编译器友好的有限、非关系型整数抽象域：
1. KnownBits：跟踪值的特定位是 0 还是 1。
2. ConstantRange：追踪可能的数值范围（支持有符号和无符号变体）。

实验评估与结果

研究团队对 NiceToMeetYou 进行了全面评估，涵盖精度比较和扩展性分析。评估覆盖了 LLVM 47 个整数操作符中的 40 个（排除了 7 个需要复杂溢出检查语义的操作符）。

4.1 精度对比

在 40 个 LLVM 操作符的评估中，NiceToMeetYou 表现出了强大的能力。

4.2 端到端性能

研究团队将合成的变换器集成到 LLVM 中，并在 SPEC CPU 2017 基准测试上评估了实际编译效果。如表 2 所示，虽然集成后性能略有下降（平均约 3.4%），但考虑到这是首次尝试且尚未进行性能优化，该结果已相当可观。

表 2：SPEC CPU 2017 整数基准测试的编译时间和精度对比

4.3 合成带来的新机会

NiceToMeetYou 不仅能复制现有的启发式规则，还能发现被人工实现所忽略的新规则。例如，对于无符号取模运算，框架发现了一个新的启发式规则：“如果被除数被证明小于除数，那么 urem(L, R) 的结果就等于 L”——这条规则在 LLVM 的现有实现中并不存在。

五、相关技术对比

与现有方法相比，NiceToMeetYou 的主要优势在于完全自动化和无需模板。

5.1 与 Amurth 对比

Amurth 是先前最相关的抽象变换器合成工作，但它需要人工提供的程序草图和特定于操作的辅助函数。如表 3 所示，当两者在相同设置下（无草图、无辅助函数）进行对比时，Amurth 无法合成任何变换器，而 NiceToMeetYou 仍能合成有效的变换器。

表3：NiceToMeetYou与Amurth对比

5.2 与符号抽象方法对比

传统的符号抽象方法（如 Reps、Sagiv 和 Yorsh 的工作）侧重于计算最佳抽象变换器，但通常不产生可执行的程序代码。NiceToMeetYou 则明确生成可直接集成到编译器中的 MLIR 代码。

5.3 与随机合成方法对比

受 Stoke 启发的随机合成方法通常针对具体程序优化，而 NiceToMeetYou 专门针对抽象变换器合成，并引入了条件归纳等创新机制。

六、局限性与未来方向

尽管 NiceToMeetYou 取得了显著成果，但仍存在一些局限性：

1. 当前支持的抽象域有限：主要针对非关系整数域。
2. 性能开销：合成的变换器在运行时性能上略逊于手工优化版本。
3. 可扩展性：对关系型抽象域（如八边形、多面体）的支持仍需探索。

未来工作可能包括：

• 扩展到更多抽象域：支持字符串、浮点数等更丰富的类型。
• 集成性能优化：在合成过程中考虑运行时性能。
• 与编译器深度集成：建立更紧密的反馈循环，根据实际优化效果调整合成策略。

七、总结

NiceToMeetYou 代表了抽象变换器合成领域的重要进展。通过将复杂变换器分解为简单部分的交集、利用 MCMC 随机搜索和条件归纳等技术，它首次实现了无需人工干预的大规模抽象变换器自动合成。

这项工作不仅能帮助编译器开发者快速获得合理的初始实现，还能发现被人类专家忽视的新启发式规则，从而提升静态分析的精度。随着编译器中间表示和形式化语义的不断发展，自动合成技术有望在未来编译器基础设施中扮演更加重要的角色。

• 对于编译器研究者而言，NiceToMeetYou 提供了探索新抽象域和操作符的快速原型工具；
• 对于编译器开发者，它能够减轻实现和维护抽象变换器的负担；
• 对于整个编译技术社区，它展示了自动化和形式化方法结合的巨大潜力。

关注“鲸栖”小程序，掌握最新AI资讯