ffc7917957
- Rust IR encoder (encodeRustIr): walks HIR expr trees, fires SafetyObserver hooks - Swift SIL frontend (fold-swift): swiftc -emit-sil parser, demangling, NDJSON output - SwiftBackend: --mode swift CLI routing, shells out to fold-swift - Binary-to-fuzz: Mach-O export discovery, ARM64 ABI param-count inference, dlopen harness generation - Language-agnostic IR: json_keys canonical constants, Call/Member/ArraySubscript/Cast/HeapNew nodes - Dogfood fixes: SARIF kind field, cross-detector dedup, harness_file in predictions, Swift stoi safety - Corpuses: swift-sil-z3-corpus.md, binary-fuzz-corpus.md - AGENTS.md: cross-language wire format rule
123 lines
5.1 KiB
Markdown
123 lines
5.1 KiB
Markdown
# Swift SIL + Z3 Corpus for fold Symbolic Engine
|
|
|
|
> Generated 2026-05-27 from canonical sources. Reference for Rust/Swift IR→Z3 lowering.
|
|
|
|
## Swift SIL Operations (canonical sources)
|
|
|
|
Source: `github.com/swiftlang/swift/blob/main/docs/SIL/SIL.md`
|
|
|
|
### Compiler Pipeline
|
|
|
|
```
|
|
Swift source → Parser → AST → Type Checker → SILGen (raw SIL) →
|
|
Mandatory opts → Canonical SIL → IRGen → LLVM IR → Binary
|
|
```
|
|
|
|
- **Raw SIL**: produced by SILGen, may have dataflow errors, `assign` instructions
|
|
- **Canonical SIL**: after mandatory optimizations, dataflow-clean, used for codegen
|
|
- **Ownership SSA (OSSA)**: enforces memory ownership, detects use-after-free at compile time
|
|
|
|
### Key SIL Operations (fold-swift detection targets)
|
|
|
|
| SIL Op | Category | fold FindingKind | Hazard |
|
|
|--------|----------|-----------------|--------|
|
|
| `unchecked_ref_cast` | unsafe cast | rust-unsafe-api | swift-unchecked-ref-cast |
|
|
| `unchecked_addr_cast` | unsafe cast | rust-unsafe-api | swift-unchecked-addr-cast |
|
|
| `unchecked_trivial_bit_cast` | type punning | rust-unsafe-api | swift-unchecked-bit-cast |
|
|
| `load [trivial]` through raw ptr | null deref | null-deref | swift-unsafe-load |
|
|
| `store [trivial]` through raw ptr | null deref | null-deref | swift-unsafe-store |
|
|
| `struct_element_addr` | field access | — | (benign, used in member access) |
|
|
| `apply` | function call | — | callee target for taint |
|
|
| `integer_literal` | constant | — | leaf value in IR |
|
|
| `builtin "assumeNonEmpty"` | force unwrap | rust-unchecked-index | swift-force-unwrap |
|
|
| `cond_fail` | assertion failure | — | crash oracle for fuzz |
|
|
|
|
### Swift Types in SIL
|
|
|
|
- `$*T` — address type (pointer to T)
|
|
- `$Builtin.Int32`, `$Builtin.Int64` — builtin integers
|
|
- `$Int`, `$Bool`, `$String` — standard library types
|
|
- `$@convention(thin)` — thin function (no context)
|
|
- `$@convention(method)` — method with self
|
|
- `$Optional<T>` — lowered to two-case enum
|
|
|
|
## Z3 C++ API (fold usage)
|
|
|
|
Source: `z3prover.github.io/api/html/classz3_1_1expr.html`, `z3++.h`
|
|
|
|
### Core Pattern (from fold's encoder)
|
|
|
|
```cpp
|
|
z3::context ctx;
|
|
z3::solver s(ctx);
|
|
|
|
// Create BV-64 variable (fold's bounded model)
|
|
z3::expr x = ctx.bv_const("x", 64);
|
|
z3::expr y = ctx.bv_const("y", 64);
|
|
|
|
// Path predicate accumulation
|
|
z3::expr path = ctx.bool_val(true);
|
|
z3::expr cond = (x == ctx.bv_val(0, 64)); // x == 0
|
|
path = path && cond; // accumulate
|
|
|
|
// Null-deref check: path && (ptr == 0) SAT?
|
|
z3::expr hazard = (ptr == ctx.bv_val(0, 64));
|
|
s.add(path && hazard);
|
|
z3::check_result r = s.check();
|
|
if (r == z3::sat) {
|
|
// Proved: path can lead to null deref
|
|
z3::model m = s.get_model();
|
|
// Extract counterexample values...
|
|
}
|
|
```
|
|
|
|
### Key API calls used by fold
|
|
|
|
| API | fold usage |
|
|
|-----|-----------|
|
|
| `ctx.bv_const(name, width)` | Create symbolic variable |
|
|
| `ctx.bv_val(int, width)` | Create constant BV |
|
|
| `ctx.bool_val(bool)` | Create boolean constant |
|
|
| `s.add(expr)` / `s.reset()` | Accumulate path predicate |
|
|
| `s.check()` | SAT/UNSAT query |
|
|
| `s.get_model()` | Extract counterexample |
|
|
| `expr.is_bv()` / `expr.is_bool()` | Type dispatch |
|
|
| `z3::expr_vector` | For assumptions |
|
|
|
|
## Swift Security Sharp Edges → fold Detector Map
|
|
|
|
| Swift Footgun | SIL Operation | fold Family | CWE |
|
|
|--------------|---------------|-------------|-----|
|
|
| Force unwrap (`!`) | `builtin "assumeNonEmpty"` | rust-unchecked-index | — |
|
|
| `try!` | `builtin "unexpectedError"` | rust-unsafe-api | 248 |
|
|
| `unsafeBitCast` | `unchecked_trivial_bit_cast` | rust-unsafe-api | 704 |
|
|
| `unsafeDowncast` | `unchecked_ref_cast` | rust-unsafe-api | 704 |
|
|
| `withUnsafePointer` | `pointer_to_address` + `load`/`store` | null-deref | 476 |
|
|
| `unowned(unsafe)` | `unowned_retain`/`release` | rust-unsafe-api | 416 |
|
|
| `@unchecked Sendable` | (compile-time attribute) | — | — |
|
|
| `UnsafeMutablePointer.advanced(by:)` | `index_addr` | oob-access | 823 |
|
|
| `String(validatingUTF8:)` bypass | — | — | — |
|
|
|
|
## Integration Architecture
|
|
|
|
```
|
|
Swift .swift → swiftc -emit-sil → fold-swift → NDJSON (findings + IR)
|
|
↓
|
|
RustBackend::extractFunctions
|
|
↓
|
|
fromJson → RustExprNode trees
|
|
↓
|
|
Z3 encoder (future: task 41)
|
|
↓
|
|
Proved | Heuristic findings
|
|
```
|
|
|
|
## References
|
|
|
|
- SIL spec: `https://github.com/swiftlang/swift/blob/main/docs/SIL/SIL.md`
|
|
- SIL docs: `https://apple-swift.readthedocs.io/en/latest/SIL.html`
|
|
- Swift compiler: `https://www.swift.org/documentation/swift-compiler/`
|
|
- Z3 C++ API: `https://z3prover.github.io/api/html/classz3_1_1expr.html`
|
|
- Z3 C++ header: `https://github.com/Z3Prover/z3/blob/master/src/api/c++/z3++.h`
|
|
- Swift memory safety: `https://github.com/swiftlang/swift-evolution/blob/main/visions/memory-safety.md`
|
|
- Strict memory safety: `https://github.com/swiftlang/swift-evolution/blob/main/proposals/0458-strict-memory-safety.md`
|