alive2是llvm官方集成的翻译验证工具，通过refinement检查源ir与目标ir的语义包含关系，要求输入为签名一致的单函数ir，不支持全局变量或间接跳转；alive-tv可检测优化引入的新panic路径，如undef折叠导致未定义行为掩盖。
直接跑测试用例不能代替验证，尤其当优化涉及未定义行为、浮点精度、内存别名或控制流重排时。LLVM Pass 的正确性必须通过翻译验证（translation validation）工具链来确认，而不是靠“看起来输出一样”。
用 alive-tv 验证 InstCombine / GVN 等前端 Pass
Alive2 是目前最成熟、被 LLVM 官方集成的翻译验证工具，专为 IR-to-IR 变换设计。它不依赖运行时行为，而是对源 IR 和目标 IR 做形式化 refinement 检查：目标函数的所有行为是否都落在源函数行为的子集内。
-
alive-tv要求输入是两个合法的 LLVM IR 函数（@src和@tgt），且签名一致；不支持全局变量、外部调用、间接跳转等复杂结构 - 常见误用：把整个模块丢进去——必须提取出单个函数，且确保
@tgt是@src经某 Pass 单步变换后的结果（例如用opt -instcombine输出后手动截取） - 错误信息如
"refinement failed: src may trap, tgt does not"表示优化引入了新 panic 路径，典型原因是原 IR 有 undef 使用，而优化后把它折叠成确定值，掩盖了未定义行为 - 命令示例：
alive-tv src.ll tgt.ll --src-func=@foo --tgt-func=@foo
用 opt -passes=... -S + llvm-diff 快速比对 IR 差异
这不是语义验证，但能快速暴露优化是否做了“不该做的事”，比如意外删除了 volatile load、改写了 nonalias 内存、或把 icmp eq 错误地替换成 select。
-
llvm-diff默认忽略元数据（!dbg,!tbaa），但加上-no-metadata会更干净；加-no-types可跳过类型差异（如i32vsptr的 bitcast） - 重点关注 diff 中出现的
store指令增减、call消失、load地址变化——这些往往是别名分析失效或优化越界的表现 - 注意
llvm-diff不处理 PHI 节点重排序，同一逻辑的 PHI 可能因基本块顺序不同而显示为“完全不同”，需人工对照支配关系
用 llc + objdump 检查后端是否引入时序泄漏
对安全敏感代码（如密码学常量时间函数），IR 层验证只是起点。后端可能把 select lower 成 cmov 或 csel，也可能把循环向量化后导致访存地址依赖秘密值——这些在 IR 层完全不可见。
- 先用
llc -march=x86-64 -O2 -filetype=asm生成汇编，再用objdump -d查看是否出现cmov、je、jne等条件跳转指令 - 对 AArch64，检查是否用了
csel（安全）而非mov+b.eq（危险）；x86 上cmov在部分微架构（如 Intel Skylake）存在数据依赖延迟，不能视为真正常量时间 - 关键点：IR 层的
select是否被保留到最终指令？可通过llc -debug-only=isel查看 SelectionDAG lowering 日志
最容易被忽略的是：LLVM 的 refinement 模型默认不建模 cache line、分支预测器、TLB miss 这些硬件侧信道。即使 alive-tv 说“等价”，也不能保证时序安全——密码学代码必须额外加 llvm.sideeffect 元数据或用 __attribute__((optnone)) 封锁关键函数。
