# Multi-Language IR Patterns: CodeQL, Infer, and Kani

> Generated 2026-05-28. Research on multi-language IR approaches for fold.

## CodeQL — AST-Based with Shared Query Engine

CodeQL uses language-specific AST schemas (C++, Java, Python, etc.) but a shared:
- **DataFlow library**: source→sink taint tracking across all languages
- **TaintTracking library**: propagates taint through standard library calls
- **Query language**: same QL for all languages

**Key insight for fold**: The Z3 encoder is the shared back-end. Language-specific frontends (Clang, rustc) produce language-specific IR trees, but both feed into the same `encodeRustIr`/`encodeClangExpr` functions. CodeQL's lesson: don't unify the AST — unify the query engine (our Z3 solver + observer hooks).

## Infer — SIL (Smallfoot Intermediate Language)

Infer lowers C++, Java, and Objective-C to SIL, a simple imperative language:
- `Load` / `Store` — memory operations
- `Call` — function calls with argument lists
- `Prune` — conditional assume (path predicate)
- `Nullify` — set variable to null
- `ExitScope` — variable going out of scope

**Key insight for fold**: SIL has ~10 instructions total. fold's IR (`RustExprNode`) has ~25 node kinds. We could simplify by mapping both Clang and rustc expressions to a smaller set of core operations before the Z3 encoder.

## Kani — MIR-to-Goto-C

Kani translates rustc MIR to CBMC's Goto-C IR:
- MIR BasicBlocks → Goto-C basic blocks with labels
- MIR Statements → Goto-C statements (assign, call, assume, assert)
- MIR Rvalues → Goto-C expressions
- Goto-C then feeds into CBMC's SAT/SMT solver

**Key insight for fold**: Kani demonstrates that MIR→Z3 is feasible. fold's current approach (HIR→Z3) misses control flow. Adopting MIR→Z3 (task 120) mirrors Kani's architecture.

## What fold Should Adopt

1. **CodeQL pattern**: Language-specific frontends + shared symbolic back-end (we have this)
2. **Infer pattern**: Small set of core operations (simplify RustExprNode to ~10 core kinds)
3. **Kani pattern**: MIR→Z3 for Rust (task 120), SIL→Z3 for Swift (future)

## Recommended Architecture

```
Rust (rustc MIR) ──→ Simplified IR (~10 core ops) ──→ Z3 Encoder ──→ Observer Hooks
Clang (LibTooling) ──→ Simplified IR (~10 core ops) ──→ Z3 Encoder ──→ Observer Hooks
Swift (SWAN SIL)  ──→ Simplified IR (~10 core ops) ──→ Z3 Encoder ──→ Observer Hooks
```

The simplified IR would have: Load, Store, Call, BinaryOp, UnaryOp, Branch, Return, Alloc, Free, Nop — covering all operations the Z3 encoder needs.