18ce5a6050
- Swift ABI: tagged pointers, garbage-input abort path, ObjC bridging - C++ fuzz: libFuzzer dlopen coverage limits, AFL++ QEMU mode, vtable seeding - Cross-language IR: CodeQL/Infer/Joern patterns, Swift SIL gaps in fold IR - MIR verification: Kani/Prusti/Creusot approaches, BorrowTracker wiring
75 lines
3.4 KiB
Markdown
75 lines
3.4 KiB
Markdown
# MIR (Mid-level IR) Verification Research
|
|
|
|
> Generated 2026-05-28. Research on MIR-level analysis for Rust and Swift.
|
|
|
|
## Rust MIR vs HIR
|
|
|
|
| Aspect | HIR | MIR |
|
|
|--------|-----|-----|
|
|
| Abstraction level | High (desugared AST) | Mid (control-flow graph) |
|
|
| Control flow | Expressions, if-let, match | Basic blocks, terminators |
|
|
| Borrow checking | Not present | Full borrow-checked |
|
|
| Optimizations | None | Inlining, const-prop, GVN |
|
|
| Loops | Desugared to loop/match | Explicit backedges |
|
|
| Available in fold-rust | Yes (via rustc HIR visitor) | Partial (mir_analysis.rs) |
|
|
|
|
## MIR-Based Verification Tools
|
|
|
|
### Kani (AWS)
|
|
- **Approach**: MIR → Goto-C → CBMC (bounded model checker)
|
|
- **Output**: proof of correctness or counterexample
|
|
- **Key insight**: MIR is already in SSA form — easy to translate to SMT
|
|
- **Relevance to fold**: Kani demonstrates that MIR → Z3 is feasible and proven
|
|
|
|
### Prusti (ETH Zurich)
|
|
- **Approach**: MIR → Viper (verification intermediate language)
|
|
- **Uses**: Rust type system for permission-based reasoning
|
|
- **Key insight**: borrow-checker information carries through MIR
|
|
- **Relevance**: our MIR analysis can leverage borrow-checker facts
|
|
|
|
### Creusot
|
|
- **Approach**: MIR → Why3 (deductive verification platform)
|
|
- **Key insight**: MIR is designed for analysis — all Rust verifiers use it
|
|
|
|
### RustHorn
|
|
- **Approach**: MIR → CHC (Constrained Horn Clauses)
|
|
- **Key insight**: MIR BasicBlocks map naturally to CHC predicates
|
|
|
|
## fold's MIR Analysis (existing)
|
|
|
|
`tools/fold-rust/src/mir_analysis.rs`:
|
|
- `BorrowTracker`: two-pass fixed-point analysis tracking borrow-safe locals
|
|
- **Pass 0**: reference types (`&T`, `&mut T`) → inherently borrow-backed
|
|
- **Pass 1**: seeds from `Rvalue::Ref`, `Rvalue::RawPtr`, `Rvalue::CopyForDeref`
|
|
- **Pass 2**: propagates through casts, field access, tuple indexing
|
|
- Output: `is_borrow_safe()` predicate for each MIR local
|
|
|
|
**Gap**: MIR analysis exists but is NOT wired into the Z3 encoder. The encoder still walks HIR expression trees.
|
|
|
|
## What fold Needs from MIR
|
|
|
|
1. **Control flow**: MIR BasicBlock structure → Z3 path predicates (much richer than HIR if-let)
|
|
2. **Borrow safety**: `BorrowTracker` results → filter null-deref findings on safe borrows
|
|
3. **Discriminant switches**: MIR `switchInt` on enum discriminants → path refinement
|
|
4. **Call terminators**: MIR `TerminatorKind::Call` → interprocedural analysis
|
|
5. **SSA form**: MIR locals are immutable SSA values → direct Z3 variable mapping
|
|
|
|
## Swift SIL → MIR Equivalence
|
|
|
|
Swift SIL is structurally similar to Rust MIR:
|
|
- **Basic blocks** with terminators (br, cond_br, switch_enum, return)
|
|
- **SSA values** (SIL values are immutable)
|
|
- **Borrow scopes** (SIL borrows map to Rust borrows)
|
|
- **Witness tables** (SIL protocol witnesses map to Rust trait objects)
|
|
|
|
The SWAN parser already produces structured SIL. The gap is:
|
|
1. SIL → fold IR tree conversion (SIL is CFG-based, fold IR is expression-tree-based)
|
|
2. Lowering the CFG back to trees for the current encoder
|
|
|
|
## Recommended Approach
|
|
|
|
**Short-term**: Wire `BorrowTracker` into fold-rust's finding emission — skip null-deref on borrow-safe locals. ~30 lines, immediate FP reduction.
|
|
|
|
**Medium-term**: Add MIR control-flow to `encodeRustIr` — walk basic blocks instead of expression trees. Requires restructuring the encoder to understand basic blocks and terminators.
|
|
|
|
**Long-term**: Unify Rust MIR + Swift SIL into a common mid-level IR that the Z3 encoder operates on directly.
|