585ae4e4ab
- clang-analysis-api-research.md: AST nodes, CFG, type system, constant folding - multi-language-ir-patterns.md: CodeQL shared engine, Infer SIL, Kani MIR→Goto-C - rust-clang-scanning-parity.md: 9-component comparison table, 8 priority fixes
49 lines
2.6 KiB
Markdown
49 lines
2.6 KiB
Markdown
# 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.
|