fold/docs/internal/multi-language-ir-patterns.md

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.