# 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`