Sift：用 E-graph SMT 缓存实现推测性循环向量化的 LLVM pass

Sift 是一个 LLVM 优化 pass 和形式化验证引擎，旨在无需源码级注解即可消除循环中的指针别名障碍（restrict）。

它分析仿射内存足迹，合成防溢出的动态不相交守卫，附加作用域别名元数据（!alias.scope / !noalias）以启用 AVX-512/AVX2 向量化，并通过 E-Graph 规范化缓存 SMT 证明证书。

架构

C / C++ Source
      │
      ▼
[ LLVM Clang Frontend ]
      │
      ▼
[ SiftPass (LLVM Plugin) ] ──(FFI)──► [ Sift Core (Rust) ]
      │                                     │
      │                             E-Graph Normalization (egg)
      │                             (Integer vs IEEE-754 FastMath)
      │                                     │
      │                             Proof Ledger (LMDB)
      │                                     ├── HIT:  0.0ms load
      │                                     └── MISS: In-Process Z3 C-API
      │
      ▼
[ Loop Versioning ]
      ├── Path A (Fast): Scoped NoAlias Tagged ──► SIMD Vectorized
      └── Path B (Safe): Original Scalar Fallback

关键技术支柱

Affine Footprint & Convex-Hull Analysis: Evaluates SCEVAddRecExpr to compute accurate access bounds for arbitrary strides:
- 正向步长（$+k$）：$[\text{Base}, \text{Base} + (\text{Trip} - 1) \times k + \text{Size})$
- 负向步长（$-k$）：$[\text{Base} - (\text{Trip} - 1) \times k, \text{Base} + \text{Size})$
- 守卫乘法通过 @llvm.umul.with.overflow.i64 防止 64 位整数溢出。
类型安全的 E-Graph 规范化：在保持 IEEE-754 语义的同时，对循环体进行交换/结合排列的规范化（浮点重结合严格由 FastMathFlags 控制）。
多存储序列规范化：具有多个存储操作的循环按目标基指针规范排序，并作为统一的 (seq ...) 表达式进行评估。
并发证明账本：由 LMDB 支持，写入事务采用指数退避，支持无争用的并行构建（ninja -j64）。
崩溃恢复回退：具有逃逸标量活出（归约）或复杂控制流的循环绕过变换，安全回退到标准优化。

验证与压力测试

位精确数值正确性：在 $10^7$ 个元素上，标量基线对比 Sift 向量化，输出 $100%$ 完全相同（memcmp == 0）。
编译器稳定性：在 -O3 下编译整个 SQLite3 合并文件（sqlite3.c，约 240,000 行代码），零内部编译器错误（ICE），并验证了内存中 SQL 执行。
Proof Latency:
- 冷启动（进程内 Z3 C-API）：$< 1\text{ms}$
- 热启动（LMDB 缓存命中）：$0.0\text{ms}$

要求

LLVM / Clang 18+
Rust 1.75+
CMake 3.20+
libz3-dev

构建

# 1. Build Rust core library
cargo build --release

# 2. Build LLVM plugin
mkdir -p pass/build && cd pass/build
cmake ..
make -j$(nproc)

用法

clang-18 -O3 -fpass-plugin=./pass/build/SiftPass.so -march=native kernel.c -o kernel

查看优化备注：

clang-18 -O3 -fpass-plugin=./pass/build/SiftPass.so \
  -Rpass=loop-vectorize -march=native -S -emit-llvm kernel.c -o kernel.ll

许可证

MIT