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

Sift is an LLVM optimization pass and formal verification engine designed to eliminate pointer aliasing barriers in loops without source-level annotations (restrict).

It analyzes affine memory footprints, synthesizes overflow-safe dynamic disjointness guards, attaches scoped alias metadata (!alias.scope / !noalias) to enable AVX-512/AVX2 vectorization, and caches SMT proof certificates via E-Graph canonicalization.

Architecture

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

Key Technical Pillars

1. Affine Footprint & Convex-Hull Analysis: Evaluates SCEVAddRecExpr to compute accurate access bounds for arbitrary strides:
   • Positive stride ($+k$): $[\text{Base}, \text{Base} + (\text{Trip} - 1) \times k + \text{Size})$
   • Negative stride ($-k$): $[\text{Base} - (\text{Trip} - 1) \times k, \text{Base} + \text{Size})$
   • Guard multiplications are protected against 64-bit integer overflow via @llvm.umul.with.overflow.i64.
2. Type-Safe E-Graph Canonicalization: Normalizes loop bodies across commutative/associative permutations while preserving IEEE-754 semantics (floating-point reassociation is strictly gated by FastMathFlags).
3. Multi-Store Sequence Normalization: Loops with multiple store operations are sorted canonically by target base pointer and evaluated as unified (seq ...) expressions.
4. Concurrent Proof Ledger: Backed by LMDB with exponential backoff on write transactions, supporting contention-free parallel builds (ninja -j64).
5. Crash-Resilient Fallback: Loops with escaping scalar live-outs (reductions) or complex control flow bypass transformation and fall back safely to standard optimization.

Verification & Stress Testing

• Bit-Exact Numerical Correctness: $100%$ identical output (memcmp == 0) across $10^7$ elements comparing scalar baseline against Sift vectorization.
• Compiler Stability: Compiled the entire SQLite3 amalgamation (sqlite3.c, ~240,000 LOC) under -O3 with zero internal compiler errors (ICE) and verified in-memory SQL execution.
• Proof Latency:
  • Cold (In-process Z3 C-API): $< 1\text{ms}$
  • Warm (LMDB cache hit): $0.0\text{ms}$

Requirements

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

Build

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

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

Usage

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

Inspect optimization remarks:

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

License

MIT