fold/docs/internal/z3-encoder-robustness-audit.md

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**
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)
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.