图例

算法概述

Algorithm 4 是 Minotaur 的核心合成过程，输入是一个函数切片 Cut（作为规范），以及指令数限制 InstLimit 和时间限制 TimeLimit。

输出是一组能精化（refine） Cut 的优化函数 Refinements

整个过程分为三个阶段：

1. Phase 1：构建指令池 InstPool，包含各种指令模板（操作数可以是具体输入、符号常量或占位符“洞”）。
2. Phase 2：通过广度优先搜索（BFS）填充“洞”，生成候选函数，并用成本模型剪枝。
3. Phase 3：使用 Alive2 验证候选函数的正确性，对含符号常量的候选求解具体常量值，在时间限制内返回所有有效优化。

代码逐段分析

Phase 1：填充指令池

Inputs ← all the SSA definitions in Cut
InstPool ← ∅
for all op in binary operations listed in Table 1
  InstPool ← InstPool ∪ {op hole, hole}, (op sym-const, hole), (op hole, sym-const)}
for all input1 in Inputs
  InstPool ← InstPool ∪ {op input1, sym-const}, (op sym-const, input1)}
  InstPool ← InstPool ∪ {op input1, hole}, (op hole, input1)}
for all input2 in Inputs
  InstPool ← InstPool ∪ {op input1, input2}}

作用：生成所有可能的指令“模板”。模板中的操作数可以是：

• hole：占位符，表示待填充的子表达式。
• sym-const：符号常量，具体数值由求解器决定。
• input1, input2：当前切片中已有的 SSA 定义（如函数参数、中间结果）。

关键点：区分了三种操作数来源，使后续枚举既能利用已有值，又能引入新常量，还能递归构造表达式。

Phase 2：枚举候选者

WorkList ← {{ret hole}, {ret sym-const}}
Candidates ← Inputs
while WorkList ≠ ∅
  I ← WorkList.pop()
  if I does not contain holes then
    Candidates ← Candidates ∪ {I}
    continue
  for all Hole in I
    if CountNewInsts(I) ≥ InstLimit then
      continue
    for all Inst in InstPool
      J ← I with Hole substituted by Inst
      if TargetTransformInfoCost(J) ≥ TargetTransformInfoCost(Cut) then
        continue
      WorkList ← WorkList ∪ {J}

作用：通过 BFS 逐步填充 hole，生成所有可能的函数体。

初始化：工作列表包含两个最简候选：ret hole 和 ret sym-const（即直接返回一个占位符或符号常量）

终止条件：

• 若 I 不含任何 hole，则它已成为完整候选，加入 Candidates。
• 若 I 中还有 hole，但当前已使用的指令数（CountNewInsts）已达到 InstLimit，则停止扩展该分支。

填充过程：对每个 hole，尝试用指令池中的每个模板 Inst 替换它，生成新候选 J。

成本剪枝：如果 J 的估算成本（通过 LLVM 的 TargetTransformInfo）不低于原始函数 Cut 的成本，则丢弃（continue）。这确保只保留可能更优的候选。

继续扩展：符合成本条件的 J 加入工作列表，继续填充剩余的 hole。

Phase 3：验证候选者

Sort Candidates by TargetTransformInfoCost
StartTime ← time()
Refinements ← ∅
for all C in Candidates
  if C does not contain symbolic constants then
    if Alive2 claims that C refines Cut then
      Refinements ← Refinements ∪ {C}
  else
    Build exists-forall query to get a model for symbolic constants
    if satisfiable then
      C' ← C with symbolic constants substituted by the constants in the model
      Refinements ← Refinements ∪ {C'}
  if time() - StartTime ≥ TimeLimit then
    break
return Refinements

作用：按成本升序验证候选，并用 Alive2 确保正确性。

排序：先验证成本低的候选，尽快找到优质优化。

处理无符号常量的候选：直接调用 Alive2 检查 C ⊑ Cut（精化关系）。若通过，加入结果集。

处理含符号常量的候选：

• 构造存在-全称查询：∃ constants. ∀ inputs. C ⊑ Cut。
• 若可满足，则求解器返回一组具体的常量值（模型），替换候选中的符号常量，得到具体候选 C'。
• 将 C' 加入结果集（Alive2 会确保此时 C' ⊑ Cut）。

时间限制：若验证时间超过 TimeLimit，则停止并返回已找到的优化。

详细示例：向量比较优化

原始函数 src（作为 Cut）

define <4 x i1> @src(<4 x i32> %x, <4 x i32> %y) {
entry:
    %0 = icmp eq <4 x i32> %x, %y      ; 向量相等比较，结果4个布尔值
    %1 = icmp ne <4 x i32> %x, %y      ; 向量不等比较
    %2 = shufflevector <4 x i1> %0, <4 x i1> %1, <4 x i32> <i32 0, i32 5, i32 2, i32 7>
    ret <4 x i1> %2
}

这段 LLVM IR 代码定义了一个函数 @src，它接受两个 <4 x i32> 类型的向量（即每个向量包含 4 个 32 位整数），并返回一个 <4 x i1> 类型的向量（4 个布尔值）。

相等比较

%0 = icmp eq <4 x i32> %x, %y

对%x和%y中对应的 4 个元素分别执行相等判断，得到一个长度为 4 的布尔向量 %0。

例如：若 %x = [a0, a1, a2, a3]，%y = [b0, b1, b2, b3]，则 %0 = [a0==b0, a1==b1, a2==b2, a3==b3]，记作 [eq0, eq1, eq2, eq3]。

不等比较

%1 = icmp ne <4 x i32> %x, %y

类似地，对每个元素执行不等判断，得到一个布尔向量 %1，其中每个元素是 %0 对应元素的逻辑非。

即 %1 = [ne0, ne1, ne2, ne3] = [not eq0, not eq1, not eq2, not eq3]。

混洗操作（shufflevector）

%2 = shufflevector <4 x i1> %0, <4 x i1> %1, <4 x i32> <i32 0, i32 5, i32 2, i32 7>

shufflevector 的作用是从两个输入向量中按指定掩码挑选元素，组合成一个新的向量。

• 输入向量一：%0，内部索引为 0, 1, 2, 3
• 输入向量二：%1，内部索引被映射为 4, 5, 6, 7（索引值减去 4 就是它在 %1 中的实际下标）

掩码 <0, 5, 2, 7> 的选取规则：

• 索引 0 → 取 %0[0]，即 eq0
• 索引 5 → 取 %1[1]（因为 5 - 4 = 1），即 ne1 = not eq1
• 索引 2 → 取 %0[2]，即 eq2
• 索引 7 → 取 %1[3]（7 - 4 = 3），即 ne3 = not eq3

最终 %2 的结果向量为：

[ eq0, ne1, eq2, ne3 ]  等价于  [ eq0, not eq1, eq2, not eq3 ]

Minotaur 的合成过程

Phase 1：构建指令池

Inputs = { %x, %y }（函数参数）

二元操作（如 icmp eq, icmp ne, xor, and, or, shufflevector 等）生成各种模板。
例如：

• icmp eq hole, hole、icmp eq sym-const, hole、icmp eq hole, sym-const
• xor hole, hole、xor sym-const, hole、xor hole, sym-const
• 用具体输入替换 hole：icmp eq %x, %y、icmp eq %x, sym-const 等。
• 混用输入和占位符：xor %x, hole、xor sym-const, %y 等。
• 也用具体输入做两个操作数：icmp eq %x, %y 等。

同时包含 shufflevector 等特殊指令的模板

Phase 2：枚举候选者（设 InstLimit=2，即最多2条新指令）

初始工作列表：{ ret hole }, { ret sym-const }。

以 ret hole 为例，尝试用指令池中的模板填充 hole：

• 用 icmp eq %x, %y 填充 → 得到 ret icmp eq %x, %y。该候选无 hole，加入 Candidates。成本可能比原函数低（原函数有两条比较+shuffle），但结果不同，后续验证会失败。
• 用 icmp ne %x, %y 填充 → 类似。
• 用 xor %0, sym-const 填充，但此时 %0 尚不存在，需先定义。因此会用 icmp eq %x, %y 先产生 %0，再用 xor。这需要两条指令，符合 InstLimit=2。

实际上，Minotaur 会探索到如下结构

• 先计算 %0 = icmp eq %x, %y（复用原切片中的指令，紫色节点）。
• 然后 %1 = xor %0, <i1 0, i1 1, i1 0, i1 1>（蓝色节点为 xor，橙色节点为常量掩码）。
• 最后 ret %1。

该候选 J 包含符号常量（掩码中的 0,1 是符号常量？实际上在合成时掩码是符号化的，表示为 sym-const 向量）。

其指令数 = 2（icmp 和 xor），成本估算（TargetTransformInfoCost）可能低于原函数（原函数有两条比较+shuffle，而新函数只有一条比较+一条按位异或，通常更便宜）.

因此通过剪枝，加入工作列表继续填充。

Phase 3：验证候选者

候选 C = ret xor (icmp eq %x, %y), sym-const-vec，其中 sym-const-vec 是符号常量向量 <c0, c1, c2, c3>。

由于含符号常量，Alive2 构造存在-全称查询：

∃ c0,c1,c2,c3 ∈ {0,1}. ∀ %x,%y.
  (xor (icmp eq %x,%y), <c0,c1,c2,c3>) ⊑ src(%x,%y)

求解器需要找到一组布尔常量，使得对任何输入，xor 后的结果等于原 shuffle 结果。

原结果：< eq0, not eq1, eq2, not eq3 >。

xor 的性质：xor(b, 0) = b，xor(b, 1) = not b

因此，取 c0=0, c1=1, c2=0, c3=1 即可满足：xor(eq0,0)=eq0，xor(eq1,1)=not eq1，等等

求解器找到模型 <0,1,0,1>，代入后得到具体候选:

define <4 x i1> @tgt(<4 x i32> %x, <4 x i32> %y) {
    %0 = icmp eq <4 x i32> %x, %y
    %1 = xor <4 x i1> %0, <i1 0, i1 1, i1 0, i1 1>
    ret <4 x i1> %1
}

Alive2 验证通过，加入 Refinements

最终结果

Minotaur 成功合成了更优的优化：用一条 xor 常量掩码代替了原来的 icmp ne 和 shufflevector，减少了指令数并可能提升性能

总结

Algorithm 4 通过指令池、BFS 填充洞、成本剪枝和SMT 求解符号常量，自动发现了将 icmp eq + icmp ne + shuffle 重写为 icmp eq + xor 常量的优化。

该算法平衡了搜索空间和求解器负担，能够合成出人类难以手工发现的底层优化。