fold/docs/research/yams-null-div-classification-2026-06-03.md

# YAMS null/div focused findings classification

Date: 2026-06-03
PBI: PBI-012
Task: classify-yams-null-div-findings
Owner: codex

## Research question

How should Fold classify the 23 source-lane `null-deref` / `div-by-zero` findings from the YAMS focused shard so the symbolic-modeling implementation tasks target general model gaps rather than YAMS-specific suppressions?

## Inputs and validation

- Primary classification report: `/tmp/fold-yams-reported-v7.json`.
- Latest rerun report: `/tmp/fold-yams-reported-v8.json`.
- Compile DB shard: `/tmp/yams-reported-compile_commands.json`.
- Re-validation command run from Fold:

```sh
build/release/src/cli/fold scan \
  --mode source \
  --compile-db /tmp/yams-reported-compile_commands.json \
  --detectors div-by-zero,null-deref \
  -f json \
  -o /tmp/fold-yams-current-classify.json \
  -j 4 \
  --budget-seconds 120 \
  --per-query-ms 2000
```

Initial v7 result: scan reproduced all 23 findings (`13 fold.null-deref`, `10 fold.div-by-zero`).

V8 rerun after first-class path-state, AccessPath, guarded-fact substrate, unknown-call havoc, and P-Code pruning work emitted 20 SARIF results (`13 fold.null-deref`, `7 fold.div-by-zero`). The removed findings are:

- `../src/daemon/components/post_ingest_enrichment.cpp:91`
- `../src/daemon/components/post_ingest_enrichment.cpp:92`
- `../src/vector/sqlite_vec_backend.cpp:3140`

No new findings were added relative to v7. The remaining 20 findings continue to represent the same unresolved modeling classes below.

## Category summary (v7 baseline)

| Category | Count | Meaning for Fold |
|---|---:|---|
| True positive / likely real bug | 1 | Keep as actionable unless YAMS adds a contract/check. |
| Latent external precondition | 4 | Should not be emitted as `Proved` unless caller/contract discharges the precondition. |
| CFG/path propagation gap | 11 | Dominating guards, early returns, logical `&&`/`||`, and loop/switch state should flow through a shared `assume` API. |
| Access-path / alias / postcondition gap | 6 | Need canonical `AccessPath` subjects and modeled call/cast/container postconditions. |
| Intentional unsupported / constexpr-template fact | 1 | Track separately from actionable runtime bugs; optional future constexpr/static-assert modeling. |

## Finding classification table

| # | Rule | Location | Classification | Evidence | Fold modeling implication |
|---:|---|---|---|---|---|
| 1 | div-by-zero | `../src/cli/progress_indicator.cpp:119` | CFG/path propagation gap | Division is dominated by `if (total_ > 0)` at line 112. | `assume(total_ > 0)` must constrain all statements in the then branch. |
| 2 | div-by-zero | `../src/daemon/components/GradientLimiter.cpp:99` | CFG/path propagation gap | RHS division is guarded by short-circuit `newSmoothed > 0.0 && ...`. | Logical `&&` RHS must inherit LHS truth. |
| 3 | div-by-zero | `../src/daemon/components/post_ingest_enrichment.cpp:91` | Access-path/range gap — resolved in v8 | `totalSecs = docSections.sections.size()` inside branch requiring `!empty()` and `size() >= 2`. | Stable `.size()` access-path identity plus range propagation. |
| 4 | div-by-zero | `../src/daemon/components/post_ingest_enrichment.cpp:92` | Access-path/range gap — resolved in v8 | Same `totalSecs >= 2` fact as line 91. | Same as #3. |
| 5 | div-by-zero | `../src/daemon/ipc/connection_fsm.cpp:247` | Intentional unsupported / constexpr-template fact | `SnapshotRing<N>` has `static_assert(N > 0)` and current instantiation is `SnapshotRing<256>`. | Optional template constant/static-assert modeling; not a runtime bug. |
| 6 | div-by-zero | `../src/vector/sqlite_vec_backend.cpp:3019` | CFG/path + assertion contract gap | `YAMS_ASSERT(m > 0 && dim % m == 0)` reports the RHS `% m`; RHS is short-circuit guarded by `m > 0`. | Logical `&&` RHS path plus assertion macro treatment. |
| 7 | div-by-zero | `../src/vector/sqlite_vec_backend.cpp:3140` | CFG/path propagation gap — resolved in v8 | `if (m == 0 || dim % m != 0)` means RHS `% m` is evaluated only when `m != 0`. | Logical `||` RHS must inherit `!lhs`. |
| 8 | div-by-zero | `../src/vector/turboquant.cpp:1019` | Latent external precondition | `config_.dimension == 0` causes float division by `sqrt(0)`; constructor has no local guard. | Treat as precondition `dimension > 0`, not automatically `Proved`. |
| 9 | div-by-zero | `../src/vector/turboquant.cpp:1189` | Latent external precondition / library semantics | `sampleBeta` divides by `x1 + x2`; safety depends on valid positive gamma parameters and nonzero samples. | Need numeric/library contracts or latent classification. |
| 10 | div-by-zero | `../src/vector/turboquant.cpp:501` | True positive / likely real bug | `computeMSE` only checks equal sizes; two empty vectors satisfy the precondition and divide by `original.size() == 0`. | Keep actionable; regression should ensure empty-container divisor remains reported. |
| 11 | null-deref | `../src/daemon/components/ConfigResolver.cpp:103` | Access-path/postcondition gap | `std::strtod(value.c_str(), &end)` with non-null `endptr` should write `end` to a non-null position in the input buffer. | Add libc postcondition model for `strtod`/endptr or demote to latent when unmodeled. |
| 12 | null-deref | `../src/daemon/components/DatabaseManager.cpp:41` | CFG/path propagation gap | `if (!raw || !*raw || *raw == '-')` dereferences `raw` only after `!raw` is false. | Logical `||` RHS path should carry `raw != nullptr`. |
| 13 | null-deref | `../src/daemon/components/EntityGraphService.cpp:498` | Latent external precondition / interprocedural guard | Public helper `populateKnowledgeGraph` checks `if (!result || result->symbol_count == 0) return true` before calling deferred helper; deferred helper itself lacks local guard. | Intra-proc reports should be latent unless caller summary/contract proves non-null. |
| 14 | null-deref | `../src/daemon/components/LifecycleComponent.cpp:98` | CFG/path propagation gap | `equalsIgnoreCase` returns immediately when `a == nullptr || b == nullptr`; loop derefs are post-guard. | Early-return non-null fact should survive into following loop. |
| 15 | null-deref | `../src/daemon/components/LifecycleComponent.cpp:100` | CFG/path propagation gap | Same early-return guard; deref of `b` occurs after both inputs proved non-null. | Same as #14. |
| 16 | null-deref | `../src/daemon/components/LifecycleComponent.cpp:106` | CFG/path propagation gap | Return derefs both pointers after early-return guard and loop increments. | Non-null fact should survive loop; pointer increment identity should preserve non-null. |
| 17 | null-deref | `../src/daemon/components/LifecycleComponent.cpp:106` | CFG/path propagation gap | Same as #16. | Same as #16. |
| 18 | null-deref | `../src/daemon/components/LifecycleComponent.cpp:98` | CFG/path propagation gap | Duplicate location/variable class from same function. | Dedup/class-level regression can cover all `equalsIgnoreCase` reports. |
| 19 | null-deref | `../src/daemon/components/RepairService.cpp:456` | Latent external precondition | Coroutine receives `shutdownState.get()` from `shutdownState_`; function-local signature is raw pointer and lacks local guard. | Raw pointer parameter derefs should be latent unless contract/caller summary proves non-null. |
| 20 | null-deref | `../src/downloader/http_adapter_curl.cpp:241` | Access-path/alias gap | `userdata == nullptr` returns before `auto* ctx = static_cast<WriteContext*>(userdata)`; `ctx` aliases non-null userdata. | Cast alias should inherit non-null from source pointer. |
| 21 | null-deref | `../src/downloader/http_adapter_curl.cpp:243` | Access-path/alias gap | Same `ctx` alias as #20; optional `ctx->total` guard is separate and valid. | Same as #20 plus optional/deref access-path modeling. |
| 22 | null-deref | `../src/metadata/connection_pool.cpp:775` | Access-path / CFG guard gap | `if (!conn || !conn->db_) return;` dominates later `**conn`. | Guard on object and member/subobject path must prove later deref safe. |
| 23 | null-deref | `../src/search/simeon_lexical_backend.cpp:76` | Access-path / array-base guard gap | `zoneAddrs != nullptr` dominates loop and `zoneAddrs[i]`. | Array base access path should inherit non-null guard. |

## Minimal regression proposals by class

1. **True positive**
   - `double mse(std::vector<float> a, std::vector<float> b) { if (a.size() != b.size()) return 0; return sum / a.size(); }`
   - Empty/equal vectors should remain reported.

2. **Latent external precondition**
   - Raw pointer parameter helper: `void f(State* s) { use(s->x); }` called from one guarded caller and one unknown context.
   - Expected Fold behavior after Phase 4: latent/precondition evidence, not `Proved`, unless a caller summary proves `s != nullptr`.

3. **CFG/path propagation**
   - Short-circuit OR: `if (m == 0 || n % m != 0) return false;`
   - Short-circuit AND: `if (d > 0 && n / d > 1) return true;`
   - Early return: `if (p == nullptr || q == nullptr) return false; return *p == *q;`

4. **Access-path / alias / postcondition**
   - Cast alias: `if (!userdata) return; auto* ctx = static_cast<C*>(userdata); return ctx->x;`
   - Size alias: `if (v.size() >= 2) { auto n = v.size(); return x / n; }`
   - Endptr postcondition: `char* end=nullptr; std::strtod(s, &end); if (end && *end == '\0') ...` plus modeled non-null when appropriate.

5. **Intentional unsupported / constexpr-template fact**
   - `template <std::size_t N> void push() { static_assert(N > 0); i = (i + 1) % N; }` instantiated with `N=256`.
   - Keep as non-blocking until Fold models template non-type parameters/static assertions.

## Recommended action plan

1. Implement `SourcePathState`/`assume` before detector-specific fixes; most CFG reports share the same root cause.
2. Add `AccessPath` subjects for local/member/cast/array-base/zero-arg call identities before adding YAMS-specific contracts.
3. Add guarded facts and join semantics so early returns and short-circuit facts are retained naturally.
4. Add latent/precondition evidence classification for raw pointer params and config-derived divisors.
5. Add targeted standard/library contracts only after the generic state model is in place: `strtod` endptr, assertions/preconditions, optional-like guards.

## Open unknowns

- Whether YAMS intends `TurboQuantMSE::computeMSE({}, {})` to be valid input; until YAMS adds a precondition or explicit empty handling, classify as likely true positive.
- Whether `sampleBeta` should accept non-positive alpha/beta; this needs a YAMS-side API contract to decide TP vs latent.
- Whether Fold should model `YAMS_PRECONDITION`/`YAMS_ASSERT` generically through macro names or through a user-configurable contract registry.