fold/FOLLOWUP_FIXES_REPORT.md

Follow-up Fixes Report — PBI-012 symbolic modeling review items

Date: 2026-06-04

Completed items

#12 Fix P-Code branch block-order path semantics

Implemented bounded forward control-flow exploration in src/symbolic/pcode_encoder.cpp:

• CBRANCH now forks path state:
  • taken target gets path && cond
  • fallthrough gets path && !cond
• BRANCH now jumps to known forward targets and stops current fallthrough.
• RETURN / indirect branches stop the current path.
• Forward targets are resolved from operation addresses; backward/unknown targets are conservatively not followed to avoid unbounded loops.
• Path exploration is bounded by max(64, ops.size() * 16) executed ops.

Regression coverage:

• taken block ordered immediately after CBRANCH still reports a taken-path div-by-zero.
• unconditional branch no longer lets skipped fallthrough hazards fire.
• existing fallthrough guard/prune tests still pass.

#13 Extend unknown-call havoc to AccessPath facts

Added SymbolicEnv::clearAccessPathFacts() and call it from unknown-call reachable-memory havoc in src/symbolic/encoder.cpp.

Cleared AccessPath-backed state:

• cached member values
• ranges
• persistent/block non-null marks

Regression coverage verifies AccessPath range/non-null/member-cache invalidation at the env layer. Existing direct mutable/ref havoc regressions still pass.

#14 Produce latent/precondition evidence from detectors

Wired real detector producers for the previously serialization-only evidence fields:

• src/detect/div_by_zero.cpp
  • direct divisor parameters are marked precondition_required / latent
  • callsite/cross-TU divisor-precondition findings include required non-zero argument evidence
• src/detect/null_deref.cpp
  • direct pointer-parameter derefs are marked precondition_required / latent
  • callsite/cross-TU non-null precondition findings include required non-null argument evidence

Regression coverage:

• parameter divisor finding records required caller non-zero precondition.
• parameter pointer deref finding records required caller non-null precondition.

#15 Preserve hybrid profile timing counters

Exported and tested mergeScanProfilesForRouter(...) from include/fold/cli/scan_router.hpp / src/cli/scan_router.cpp.

Hybrid profile merge now preserves/sums:

• total_wall_ms, parse_ms, analyze_ms, report_ms
• compile_db_load_ms, fanout_orchestration_ms, serial_dispatch_ms
• TU/function counts
• incremental stale/fresh counts
• source prefilter skipped count
• detector profile rows

Regression coverage:

• new fold:scan_router_profile unit test validates merged lane timings and counters.

Validation

Passed focused gates:

ninja -C build/release
meson test -C build/release \
  fold:pcode_encoder fold:div_by_zero fold:null_deref \
  fold:scan_router_profile fold:scan_e2e fold:subprocess_fanout \
  --print-errorlogs
git diff --check

Result: 6/6 OK for focused Meson tests; LSP diagnostics reported 0 errors for touched C++ files.

Full suite is running under monitor #3 at report creation time.