## Z3 Symbolic Encoder Robustness Audit

**Scope:** Every file in `src/symbolic/*.cpp` and `include/fold/symbolic/*.hpp` (31 files)
**Date:** 2026-05-27

---

### 1. PATH PREDICATE PRECISION

#### 1.1 If/Else Forking — ADEQUATE with gaps

The walker (`src/detect/security_walker.cpp`, `walkIf()`) correctly forks the `SymbolicEnv` into `then_env` and `else_env` at every `IfStmt`, setting path predicates `path && cond` and `path && !cond` respectively. A `z3::solver::push()`/`pop()` pair wraps each arm so branch-local constraints don't leak.

**Phi-merge at join points** is conditionally applied: when both arms produce identical values for all live variables, the env is directly reused (cheap merge). Otherwise, phi variables are created with constraint `phi == ite(cond, then_v, else_v)`, and the path predicate is restored to pre-if.

**Gaps:**

| Gap | Location | Severity |
|-----|----------|----------|
| **Short-circuit `&&`/`||` not path-forked** | `encoder.cpp` `encodeBinary`, `BO_LAnd`/`BO_LOr` | HIGH |
| **WalkIf short-circuit handling incomplete** | `walkIf` uses `encodeConditionWithShortCircuit` for condition only | MEDIUM |

The `BO_LAnd` and `BO_LOr` arms fall through to simple `coerceToBool(lhs) && coerceToBool(rhs)` — treating them as eager boolean expressions. This is a **known FP class (Class D)** documented at `encoder.cpp` line ~1082: *"3 of 4 yams null-deref FPs are `(p != nullptr && p->m)` or `(p == nullptr || *p != ...)`"*.

#### 1.2 Ternaries — ADEQUATE

`encodeExpr` handles `ConditionalOperator` by forking two child envs with `path && cond` / `path && !cond`, encoding each arm, then combining via `z3::ite()`. Special handling for `assert(x)` macro patterns.

#### 1.3 Switch Statements — PARTIAL

`walkSwitch` encodes the condition but does NOT refine path predicates per case. Each case body runs against the same undifferentiated path.

#### 1.4 Loop Unrolling — ADEQUATE

Loop unrolling depth defaults to 5 (`SolverBudget::loop_unroll`). Canonical `for` loops are detected with tight interval ranges. Loop invariant inference is implemented but **unused** (`z3::fixedpoint` → `spdlog::debug` only).

---

### 2. TYPE THREADING

| Area | Status |
|------|--------|
| Source bit-widths | ADEQUATE — `sourceWidth()` returns bit-width, `coerceToExactBv` materializes |
| Signedness | ADEQUATE for Clang, **PARTIAL for Rust** — `int_signed` field exists but ignored |
| Struct fields | PARTIAL — field offset tracked, but field type info not threaded to observers |
| Union members | **NOT HANDLED** — no overlapping-storage constraints |
| Array elements | ADEQUATE — `z3::select` with known-length propagation |

**Rust signedness gap (HIGH):** `rust_ir_encoder.cpp` hard-codes `true` for signedness in all `onBinaryArith`/`onDivision` calls. The `RustExprNode` struct has `int_signed` but it is unused.

---

### 3. INTERPROCEDURAL HANDLING

**Direct calls (ADEQUATE):** Summary lookup, malloc/free tracking, stdlib sink recognition, string-length propagation, M20 non-null marking.

**Indirect calls / virtual dispatch (NOT HANDLED — HIGH):** `calleeName()` returns empty for indirect calls. Falls through to `OverApproximated` fresh-unknown return. Virtual dispatch through C++ vtables is completely opaque.

---

### 4. MEMORY MODEL

**HeapModel tracks:** regions (base, size, freed flag), derived pointers, OOB checking, use-after-free checking, concrete alias disambiguation via allocation IDs.

**Gaps:**
- No symbolic alias analysis — pointers tracked as BV-64 values only
- Stack arrays not in HeapModel — excluded from OOB/UAF queries
- Field access values are `freshUnknown` — no type/width preservation
- `mergeFrom` loses path-sensitivity for freed — crude boolean OR at phi-joins

---

### 5. RUST IR COMPLETENESS

| Kind | Handled? | Notes |
|------|----------|-------|
| IntegerLiteral, BoolLiteral, NullPtr, DeclRef | Yes | |
| BinaryOp, Deref, ArraySubscript, UnaryOp | Yes | |
| AddrOf, Cast, Call(transmute) | Yes | Pass-through or special-case |
| Call(other) | PARTIAL | Args only; no summaries |
| **Member** | **NO** | Absent from switch |
| **HeapNew/HeapDelete** | **NO** | Absent |
| **StringLiteral** | **NO** | Absent |
| **Conditional** | **NO** | No path forking |
| **ConstructorCall** | **NO** | No modeling |
| Default fallthrough | Returns BV-0 | |

Critical: No path predicate accumulation in Rust IR encoder — `path` starts as `true` and is never updated. All comparison operators use unsigned semantics despite `int_signed` being available.

---

### 6. Z3 QUERY CONSTRUCTION

- **Logic:** QF_BV ✓
- **Timeouts:** Per-query 2000ms (configurable) ✓
- **Caching:** LRU ExprCache per Z3 expression hash (4096 entries, thread-safe) ✓
- **Path predicates:** Can grow unbounded — no simplification or bounding applied

---

## PRECISION GAP SUMMARY

### HIGH severity — Directly causes false positives

| # | Gap | FP Class | Detectors | Estimated FP Impact |
|---|-----|----------|-----------|---------------------|
| H1 | `&&`/`||` short-circuit not forked | `if (p && p->field)` | null-deref | 30-40% of null-deref FPs |
| H2 | Indirect/virtual calls not resolved | Opaque callsites | All detectors | Misses findings |
| H3 | Rust IR incomplete (Member, Conditional, signedness, path) | All Rust ops | All Rust detectors | Near-total precision loss |

### MEDIUM severity

| # | Gap | Detectors |
|---|-----|-----------|
| M1 | Switch case path predicates not refined | null-deref, oob, dead-branch |
| M2 | Loop invariant inference unused | All post-loop detectors |
| M3 | Field type info not threaded to observers | int-overflow, sign-conversion |
| M4 | Union members not modeled | All memory-safety detectors |
| M5 | HeapModel mergeFrom loses freed path-sensitivity | UAF (future) |
| M6 | Rust comparisons always unsigned | All Rust detectors |

### LOW severity

| # | Gap |
|---|-----|
| L1 | Path predicate unbounded growth (perf) |
| L2 | ExprCache cleared per-function (perf) |
| L3 | Rust AdrOf/Cast pass-through (type info loss) |
| L4 | Stack arrays not in HeapModel |

---

## RECOMMENDED FIXES ORDERED BY ROI

### Fix 1: Fork path predicate for `&&`/`||` in encoder (H1)
**Effort:** S (~50 lines) | **ROI:** Highest
**Files:** `src/symbolic/encoder.cpp`, `encodeBinary`
**Approach:** In `BO_LAnd`/`BO_LOr` arms, fork env like `ConditionalOperator`: `lhs_env` with `path && lhs`, `rhs_env` with `path && !lhs && rhs`, encode RHS only in `rhs_env`.

### Fix 2: Wire Rust signedness through observer hooks (H3)
**Effort:** S (~10 lines) | **ROI:** Very high for Rust
**Files:** `src/symbolic/rust_ir_encoder.cpp`
**Approach:** Pass `node->int_signed` instead of hard-coded `true`.

### Fix 3: Add Rust `Member` + Conditional encoding (H3)
**Effort:** M (~80 lines) | **ROI:** Moderate
**Files:** `src/symbolic/rust_ir_encoder.cpp`
**Approach:** Add `Member` case (base encoding + `onPointerDerefIr`), add `Conditional` case with path-forking.

### Fix 4: Wire loop invariant results (M2)
**Effort:** S (~30 lines) | **ROI:** Moderate
**Files:** `src/symbolic/loop_invariant.cpp`, `src/detect/security_walker.cpp`
**Approach:** Use `invariant->invariant_expr` in `unrollLoop` to constrain widened range.

### Fix 5: Per-case path predicates in switch (M1)
**Effort:** M (~60 lines) | **ROI:** Moderate
**Files:** `src/detect/security_walker.cpp`
**Approach:** For each `CaseStmt`, add `switch_expr == case_val` to path predicate.

### Fix 6: Thread field type info through `onMemberAccess` (M3)
**Effort:** M (~40 lines) | **ROI:** Low-Moderate
**Files:** `include/fold/symbolic/safety_observer.hpp`, `src/symbolic/encoder.cpp`

### Fix 7: Indirect call / virtual dispatch resolution (H2)
**Effort:** L | **ROI:** High for C++ OO codebases
**Files:** `src/symbolic/encoder.cpp`
**Approach:** Enumerate possible targets via clang VTable analysis, model as `ite` over typeid choices.