Formal verification of Mem2Reg pass using Alive2

[yudongusa]

Background

The `mem2reg` pass (Cytron SSA construction) is the most semantically complex transformation in the project. A miscompilation in `mem2reg` will silently produce wrong results for any program that uses local variables — which is essentially every program. Alive2 is a formal verification tool that proves LLVM IR transformations are semantically equivalent.

Goals

• Alive2 integration: For each rewrite rule performed by `mem2reg`, generate a pair of `.ll` snippets (before/after) and verify them with Alive2 offline.
• Invariant documentation: Document the formal pre/post-conditions of `mem2reg` in code comments, derived from the Cytron et al. paper, so reviewers can audit the implementation.
• Test suite expansion: Add property-based tests (using proptest or quickcheck) that:
  1. Build random alloca/load/store patterns with the Builder API
  2. Run mem2reg
  3. Assert that the promoted SSA form is semantically equivalent (same outputs for all inputs) by running both versions through our x86 codegen and comparing execution results

Specific invariants to verify

1. Every load of a promoted alloca is replaced by the reaching SSA value
2. No phi node is inserted for a block that is not in the iterated dominance frontier
3. Every phi incoming edge has exactly one value per predecessor block
4. No alloca/load/store for a promoted slot remains after the pass

Acceptance criteria

• At least 20 Alive2-verified (before, after) .ll pairs committed to tests/alive2/
• Property-based test in llvm-transforms that generates 500+ random alloca patterns and checks semantic equivalence via round-trip execution
• Formal pre/post-conditions documented as /// # Correctness doc comments in mem2reg.rs

References

• Alive2
• Cytron et al., "Efficiently Computing Static Single Assignment Form and the Control Dependence Graph" (1991)