Hydra 可以泛化 LLVM 中错过的 75% 的窥孔优化，使得代码能够得到更好的优化，本文简单介绍一下。

1、问题

窥孔优化之前有写过，类似于滑动窗口，针对一小组编译器生成的指令序列进行优化，而不需要过多关注上下文、控制流等。比如乘 8 的操作指令，可以优化替换为左移 3 的操作指令，这样就提升了指令执行的性能。

现在的窥孔优化基本上只是模式匹配器的集合，匹配到可以对应的指令序列，就对其进行优化。

编译器通常由前端、优化 pass 和 transformer、后端构成，而这个编译器中端的优化数量多、开发耗时、正确性难以保证，编写成本很高。

如果要新增一个窥孔优化，大致流程是这样：

  1. 发现某种计算，可以被重写为性能更好的指令。
  2. 编译器开发者手工泛化这个重写逻辑，让它能匹配到更多的情况。
  3. 把这个泛化后的优化在编译器中实现。

其中步骤 2 费心费力，还特别容易出错，应该用自动化、正式的方式进行泛化。这就是 Hydra 要做的事情，同时它也能自动化步骤 3。

2、泛化

比如我们发现乘 2048 可以被左移 11 所代替，但这只是其中一种情况，我们还知道类似的，乘 32 可以被左移 5 所代替。

所以需要泛化以匹配更多的情况，转化成通用的正式的公式，再转化成 LLVM 中的代码实现。

但我们还需要担忧位宽(bitwidth) 的问题，随意左移是会有越界问题的。

3、Hydra

Hydra 的目标意在泛化优化，它采取贪心的策略从不同的角度去尝试泛化。

这里有几个操作步骤：

  • Pruning(剪枝)。移除无关紧要的部分，可以使得内容更加标准化。
  • Narrowing(限制范围)。尝试把位宽收窄，可以使得计算更快。(需要该优化是位宽无关的)
  • Symbolic Constants(符号化常量)。将常量用符号化表示，这样可以更好地得到通用的泛化。
  • Expression Synthesis(合成为表达式)。转换为常量表达式，让等式的两边建立起关系。
  • Precondition Synthesis(生成前提条件)。为优化生成可能的前提条件限制。很多优化是在某种前提条件下才能进行，这里会有几个步骤：生成前提条件、过滤和验证、整合。
  • Width Independence(位宽独立性)。尝试证明这个优化是具有位宽独立性的。越位操作会导致这个优化变成错误的优化。

虽然有 inductive synthesis engine(归纳合成引擎) 可以生成表达式，但论文中还是用的暴力枚举+剪枝，给出的原因是更快。

Hydra 使用 Souper 的内容作为输入(未泛化的、发现的窥孔优化的 IR)，然后输出泛化的优化，并生成库的方式让 LLVM 来进行加载其优化。

3.1、Souper

Souper 是一个 superoptimizer(超级优化器)，可以查看正在编译的代码并使用搜索、成本函数计算、等价验证器来自动化地发现更好的代码序列。Souper 使用 SMT 求解器来帮助识别 LLVM 中端优化器中缺失的窥孔优化。

它不是基于输入程序的语法和语义实现优化，而是遍历程序空间以找到有效的全局优化解决方案。

Souper 作为一个新的中端优化器有以下好处：

  • LLVM IR 的生态系统发展很好，在中端进行优化可以让不同的前端和后端都受益。
  • Souper 擅长生成常量，影响到其他优化，这对于常量传播、死代码消除和其他优化过程都有用。
  • SSA 的 IR 格式非常适合自动推理技术的实施。

一个简单 Souper 优化如下图，在最左侧，需要推断 r 的值，如果 a 等于 x 且不等于 y，则 r 为 true，但没法直接推断。如果假定了中间的状态，即 x 一定小于 y，则只要判断 a 等于 x 即可，就是 i 的值，可以优化成最右侧的指令。

4、总结

Souper 发现了更多可优化的窥孔优化，而 Hydra 将其泛化以推广到更多的场景应用。目前 Souper 是可以找得到仓库和应用的，Rust 也有操作 Souper IR 的库，但这个 Hydra 目前还找不到更多的信息。

关于自动化生成表达式、自动推理和验证正确性，这里面涉及的论文特别多，看不过来了，本文只简单介绍一下这个 Hydra 的思路。

参考