Problem: with --portfolio the OOB and UAF detectors took the portfolio's
SAT/UNSAT answer as final. The portfolio solves on its own contexts, so the
reporting solver was never checked: OOB read its counterexample from an
unchecked solver (i=0 under `i > 5`), and a SAT the reporting solver would
not reproduce was still emitted. Other detectors already fail closed through
reconcilePortfolioRecheck.
Fix: add symbolic::recheckPortfolioVerdict, which re-checks a decided verdict
on the reporting solver and reconciles the two (disagreement or timeout ->
unknown), and apply it at the four OOB and two UAF portfolio sites. The
now-redundant UNSAT-only artifact re-checks in OOB checkHazard are removed.
Test: test_proved_requires_exact_model "[portfolio]" requires the portfolio
counterexample to satisfy the path (was i=0, now i=6).
Problem: OOBObserver::emit marked every constant-index array OOB as Proved,
even when the path reaching the access was over-approximated (an opaque call
or a truncated loop). The heap and UAF paths already gated on exactEncoding.
Fix: pass exactEncoding(env) into emit and require it alongside a numeral
index before assigning Proved; otherwise the finding is Heuristic.
Test: test_proved_requires_exact_model "[oob]" adds an exact control (stays
Proved) and an opaque-call path (now Heuristic; was Proved).
Problem: docs/research/soundness.md defines `proved` as an exact bounded
model establishing the property, but several detectors assigned Proved
without one: double-free from a heap-model flag, static-ptr-asymmetry from
a cross-function pattern, unused-function and dead-statement from AST
facts, the stdlib copy-overflow check, and the heap use-after-free / OOB
checks from SAT results whose encoding precision was never consulted. A
SAT result over an over-approximated path (an opaque call, an unsupported
node) can be spurious.
Fix: double-free and static-ptr-asymmetry report Heuristic; unused-function
and dead-statement report Syntactic; the stdlib copy check reports
Heuristic. Heap OOB and use-after-free keep Proved only when the path's
SymbolicEnv carries no imprecision tag. So that `malloc(sizeof(T))` paths
stay exact, sizeof/alignof on complete non-VLA types are now encoded as
exact constants (symbolic::typeTraitConstant) instead of an unsupported
node.
Test: tests/unit/test_proved_requires_exact_model.cpp covers each
downgraded detector, a heap UAF on an exact path (stays Proved, control)
and under an opaque call (Heuristic), and typeTraitConstant including the
VLA negative case. Full suite: 138/138.
