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:

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 &&/`
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
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
13	null-deref	../src/daemon/components/EntityGraphService.cpp:498	Latent external precondition / interprocedural guard	Public helper populateKnowledgeGraph checks `if (!result
14	null-deref	../src/daemon/components/LifecycleComponent.cpp:98	CFG/path propagation gap	equalsIgnoreCase returns immediately when `a == nullptr
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
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.