Hotdry.
归档
compiler-design

构建自动化系统：从代码模式提取窥孔优化规则并在Lean中生成形式化证明

设计并实现从代码模式自动提取窥孔优化规则，在Lean定理证明器中生成形式化证明的完整系统架构与工程参数。

从验证已知到发现未知：窥孔优化规则的自动化证明生成

在编译器优化领域，窥孔优化（peephole optimization）作为最基础且高效的优化手段，长期以来依赖人工编写和验证。虽然已有 AliveInLean 等工具能够在 Lean 定理证明器中验证已知优化规则的正确性，但从代码模式自动发现新规则并生成形式化证明仍是一个未充分探索的工程挑战。本文提出一个完整的自动化系统架构，将代码模式提取、规则生成与 Lean 证明生成三个环节串联，实现窥孔优化规则的自动发现与验证。

现有框架的局限与机遇

当前窥孔优化的形式验证主要分为两个方向：一是如 AliveInLean 这样的验证框架，专注于验证已知规则的正确性；二是如 JOG（Java JIT Peephole Optimizations and Tests from Patterns）这样的模式提取框架，允许开发者用 Java 本身编写优化模式。然而，这两个方向之间存在明显的断层。

JOG 框架的核心洞察是 “许多窥孔优化可以在被优化的编程语言本身中表达”，这避免了操作低级代码表示的复杂模式。开发者可以编写包含优化前后代码的模式，JOG 自动将其转换为 C/C++ 优化通道并生成测试。但 JOG 缺少形式验证环节，无法保证提取的规则在数学意义上的正确性。

另一方面，l-m.dev 作者在 2025 年 12 月发布的 peephole-formal 项目展示了在 Lean 中建模 LLVM 整数指令和 C 风格未定义行为（UB）语义的可行性。关键建模包括iN类型（表示 LLVM 风格整数和 poison 值）和Rewrite命题，其中 poison 值可以重写为任何具体值，但具体值不能重写为 poison—— 这精确捕捉了 “程序可以变得更确定，但不能变得更不确定” 的编译器优化原则。

自动化系统架构设计

基于现有工作的分析，我们设计一个三阶段自动化系统：

第一阶段：代码模式提取与抽象

借鉴 JOG 框架的思路，系统首先从代码库中提取候选优化模式。关键工程参数包括：

  • 匹配窗口大小：建议 3-5 条指令，过小可能遗漏上下文，过大增加搜索复杂度
  • 模式抽象层级：支持从具体数值到符号变量的抽象，如x + 0 → x而非5 + 0 → 5
  • 语义等价性检查：使用符号执行或 SMT 求解器验证模式前后语义等价，过滤明显错误的候选

实现上，可以构建一个轻量级 AST 分析器，支持多种中间表示（LLVM IR、Java 字节码、自定义 IR）。对于每个候选模式，生成包含以下信息的描述：

structure PeepholePattern where
  before : Expr  -- 优化前表达式
  after : Expr   -- 优化后表达式
  preconditions : List Condition  -- 前提条件
  bitwidth : Nat  -- 位宽参数

第二阶段：规则形式化与 Lean 编码

将提取的模式转换为 Lean 中的形式化陈述。这是系统的核心创新点，需要处理几个关键问题：

  1. UB 语义的精确建模：基于 peephole-formal 项目的iN类型系统，确保规则正确处理 poison 值。例如，对于加法结合律优化，需要添加符号相同的约束条件：
theorem addNsw_assoc_same_sign {n} {x y z : iN n}
    (hxyz : x ∈ i[0,∞] ∧ y ∈ i[0,∞] ∧ z ∈ i[0,∞]   -- 全正
          ∨ x ∈ i[-∞,0] ∧ y ∈ i[-∞,0] ∧ z ∈ i[-∞,0]) -- 全负
    : (x +nsw y) +nsw z = x +nsw (y +nsw z) := ...

  1. 证明模板生成：为常见优化类别（常量折叠、代数恒等式、冗余消除）预定义证明模板。系统根据模式特征选择合适模板并实例化。

  2. 位宽参数化处理：窥孔优化通常需要证明对所有位宽都成立。系统生成带∀ n : Nat量化的定理，或为常用位宽（8、16、32、64）生成具体实例。

第三阶段：自动化证明生成与验证

利用 Lean 的自动化工具链生成证明。关键配置参数：

  • 证明超时设置：建议分层超时策略 —— 简单优化 30 秒，中等复杂度 2 分钟，复杂优化 5 分钟
  • 自动化策略组合：结合auto、simp、omega、linarith等策略，根据定理类型动态选择
  • 回退机制：当全自动证明失败时，生成带sorry的存根，供人工审查或后续改进

系统需要监控以下指标评估效果：

  • 规则发现率：从代码库中提取的有效规则比例
  • 证明成功率：自动生成证明的成功率
  • 证明时间分布：不同复杂度优化的证明耗时

工程实现细节与参数调优

代码模式匹配的精确性与召回率平衡

模式匹配面临精确性与召回率的经典权衡。过严格的匹配可能遗漏有效优化，过宽松的匹配产生大量误报。建议采用多级过滤策略：

  1. 语法级过滤：快速排除明显无效的模式（如类型不匹配）
  2. 轻量级语义检查：使用简单值传播分析验证基本等价性
  3. 形式化验证：对通过前两级的候选进行完整的 Lean 证明

实际参数建议：

  • 初始召回率目标：覆盖已知优化规则的 90% 以上
  • 精确率阈值：候选模式中至少 30% 可被自动证明
  • 处理吞吐量：每小时处理 1000-5000 个代码片段

Lean 证明生成的优化策略

Lean 证明生成的成功率高度依赖策略选择和参数调优。基于对 lean-auto 项目和 ImProver 的分析，建议以下配置：

-- 针对算术优化的策略组合
macro "peephole_arith" : tactic =>
  `(tactic|
    try (simp [*] at *)
    try (omega)
    try (linarith)
    try (nlinarith)
    try (ring)
  )

-- 针对位运算优化的策略组合  
macro "peephole_bitwise" : tactic =>
  `(tactic|
    try (bitblast)
    try (simp [BitVec.simps] at *)
    try (arith)
  )

对于无法自动证明的定理，系统可以：

  1. 生成带by native_decide的证明（适用于小位宽的具体计算）
  2. 生成交互式证明框架，提示用户需要证明的关键引理
  3. 记录失败模式，用于改进证明模板和策略选择

系统集成与工作流

完整的自动化系统应支持以下工作流：

  1. 批量处理模式：扫描整个代码库，提取所有候选优化
  2. 增量更新模式：监控代码变更，只处理新增或修改的代码片段
  3. 交互式探索模式：允许开发者手动提供模式，系统尝试证明

集成到现有编译器工具链时，系统输出标准化的优化规则描述，可直接被优化器使用。例如，对于 LLVM 优化器，生成llvm::PeepholePass兼容的规则描述。

实际应用场景与局限性

适用场景

  1. 编译器开发：为新编译器或中间表示快速构建优化规则库
  2. 遗留代码优化：从现有代码库中挖掘未被文档化的优化机会
  3. 教学与研究：作为编译器优化课程的教学工具，直观展示优化规则的形式化验证
  4. 安全关键系统：为航空、医疗等领域的编译器提供经过形式验证的优化规则

当前局限性

  1. 控制流处理有限：当前系统主要处理无副作用的表达式优化，对包含分支、循环的复杂模式支持有限
  2. 内存操作优化：对内存访问模式（如地址计算优化）的提取和验证需要更复杂的分析
  3. 浮点运算语义：浮点数的非结合性和舍入误差使形式化验证更加复杂
  4. 证明可读性：自动生成的证明可能缺乏良好的结构和注释，不利于人工审查

未来发展方向

基于当前系统的实现经验，以下几个方向值得进一步探索：

  1. 与超级优化器集成：将系统与 Souper 等超级优化器结合，形成 “发现 - 验证 - 应用” 的完整闭环。超级优化器发现潜在优化，本系统验证其正确性，验证通过的规则反馈给超级优化器指导搜索。

  2. 机器学习增强：使用机器学习模型预测证明策略的成功概率，动态调整策略选择和超时设置。可以基于历史证明数据训练模型，预测特定类型定理的最佳证明策略。

  3. 多证明器后端：除了 Lean，支持输出 Coq、Isabelle 等不同定理证明器的代码，提高系统的通用性。

  4. 在线优化验证：将系统集成到编译器的即时编译（JIT）环节，在运行时验证和应用优化规则，特别适用于动态语言和 JIT 编译器。

结语

从代码模式自动提取窥孔优化规则并在 Lean 中生成形式化证明，代表了编译器优化验证从 “验证已知” 到 “发现未知” 的重要转变。通过结合 JOG 的模式提取能力和 Lean 的形式验证能力，我们构建了一个完整的自动化系统架构。

系统的核心价值不仅在于提高优化规则开发的效率，更在于建立了一个可扩展、可验证的优化规则发现框架。随着定理证明和程序分析技术的进步，这样的自动化系统有望成为编译器开发的标准工具，推动整个领域向更高程度的自动化和形式化验证发展。

关键工程参数总结：

  • 匹配窗口：3-5 条指令
  • 证明超时：分层策略（30 秒 / 2 分钟 / 5 分钟）
  • 处理吞吐量：1000-5000 代码片段 / 小时
  • 精确率阈值：30% 以上候选可自动证明
  • 召回率目标：覆盖 90% 已知优化规则

资料来源：

  1. l-m.dev/cs/formally-verifying-peephole-optimisations-in-lean - peephole-formal 项目在 Lean 中建模 LLVM 整数指令和 UB 语义
  2. JOG: Java JIT Peephole Optimizations and Tests from Patterns (arXiv:2403.11283) - 用 Java 本身编写优化模式的框架
查看归档