fold/docs/internal/swift-sil-z3-corpus.md

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)

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