# 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:

```sh
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.