Alive2 consists of several libraries and tools for analysis and verification of LLVM code and transformations. Alive2 includes the following libraries:

  • Alive2 IR
  • Symbolic executor
  • LLVM → Alive2 IR converter
  • Refinement check (aka optimization verifier)
  • SMT abstraction layer
    Included tools:
  • Alive drop-in replacement
  • Translation validation plugins for clang and LLVM’s opt
  • Standalone translation validation tool: alive-tv (online)
  • Clang drop-in replacement with translation validation (alivecc and alive++)
  • An LLVM IR interpreter that is UB precise (alive-exec)
    For a technical introduction to Alive2, please see our paper from PLDI 2021.

笔记开始

安装流程：我用的 v19 版本。最新是 v20。

git clone --recursive https://github.com/AliveToolkit/alive2.git
cd alive2 && git checkout v19.0
mkdir build && cd build
cmake -G Ninja -DCMAKE_PREFIX_PATH=/home/yz/clean/llvm-project/build -DBUILD_TV=1 -DCMAKE_BUILD_TYPE=Release ..
ninja -j$(nproc)

注意事项：

  • 函数命名要求：
    • 默认必须叫 @src 和 @tgt，两个函数必须参数类型相同，返回类型也要一致。
  • 只支持函数级别验证：
    • 不支持完整 module 验证（多函数/全局变量）
    • 不支持跨函数调用（除非 inline 进来）
  • 对全局变量 / I/O / 调用外部函数的支持
    • 不支持引用 @global 等全局变量
    • 不支持 call 到未定义函数（除非有特殊建模）
    • 不支持 load / store 全功能建模（不推荐 memory-heavy 函数）
  • 其他
元信息类型支持情况
!dbg, !tbaa, !range✅ 忽略但接受，不会影响分析
nuw, nsw, exact✅ 有意义，影响语义等价性
align, nonnull（指针）✅ 有影响，注意使用
  • add undef, undef 可能 ≠ shl undef, 1
  • nsw, nuw, exact 一旦出错就可能生成 poison
  • freeze 可用于修正 undef 或 poison 引发的等价性问题 ✅