85 lines
3 KiB
Markdown
85 lines
3 KiB
Markdown
# 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.
|