81 lines
3.5 KiB
Markdown
81 lines
3.5 KiB
Markdown
# Roadmap Expansion Tasks Report — PBI-012
|
|
|
|
Date: 2026-06-04
|
|
|
|
## Completed tasks
|
|
|
|
1. **Docs checkpoint update**
|
|
- Updated symbolic modeling, SAST/DAST roadmap, and maturity docs to reflect completed branch-order P-Code exploration, AccessPath havoc, latent/precondition detector evidence, hybrid profile merge, assertion behavior, and full-suite status.
|
|
|
|
2. **Production guarded-fact read API**
|
|
- Added `SymbolicEnv` facade methods over `GuardedFactStore`:
|
|
- `guardedFacts()`
|
|
- `addFact`, `clearFacts`
|
|
- `markFactNonNull`, `markFactNonZero`
|
|
- `setFactRange`, `setFactMemberValue`
|
|
- `isFactNonNull`, `isFactNonZero`, `factRange`, `factMemberValue`
|
|
- Added env-level tests using current-path implications.
|
|
|
|
3. **Div-by-zero guarded-fact migration**
|
|
- Mirrored AccessPath range/nonzero assignments into guarded facts.
|
|
- Div/rem encoder call sites now suppress observer emission when live env guarded facts prove the denominator non-zero.
|
|
- Avoided stale deferred-observer `SymbolicEnv*` access by checking facts at the live encoder point.
|
|
|
|
4. **Null-deref/OOB guarded-query migration**
|
|
- Mirrored non-null marks into guarded facts.
|
|
- Pointer deref encoder call sites skip null-deref observer emission when guarded facts prove non-null.
|
|
- OOB focused tests remain green after range fact mirroring.
|
|
|
|
5. **Precise AccessPath havoc dependencies**
|
|
- Added `ir::isSameOrDescendantAccessPath(candidate, root)`.
|
|
- Added `GuardedFactStore::clearDescendantsOf(root)`.
|
|
- Added `SymbolicEnv::clearAccessPathFacts(root)` for root-scoped invalidation.
|
|
- Unknown-call havoc now clears only roots for mutable refs, `&aggregate`, and pointer-reachable args when roots are known; falls back to coarse clear on unknown roots.
|
|
|
|
6. **Generic assertion/contract macro modeling**
|
|
- Added `isContractAssumeCall` for `assert`, `Expects`, `Ensures`, `FOLD_ASSERT`, `FOLD_PRECONDITION`, `FOLD_POSTCONDITION`, `FOLD_DCHECK`, `fold_assume`, and `FOLD_ASSUME`.
|
|
- Function-style contract calls now conjoin their first boolean argument into the symbolic path.
|
|
- Existing null-check extractor marks pointer args non-null for contract predicates such as `p != nullptr`.
|
|
|
|
7. **Benchmark baseline maturity gate**
|
|
- Added `--baseline-dir` and `--require-baselines` to `scripts/benchmarks/summarize_maturity.py`.
|
|
- Required-baseline mode fails closed on missing, malformed, or non-object baseline JSON.
|
|
- Documented required-baseline usage in `tests/benchmarks/README.md`.
|
|
|
|
## Focused validation passed
|
|
|
|
```sh
|
|
ninja -C build/release \
|
|
tests/unit/test_access_path tests/unit/test_guarded_facts \
|
|
tests/unit/test_div_by_zero tests/unit/test_null_deref \
|
|
tests/unit/test_oob_access tests/unit/test_encoder_callee_predicates
|
|
|
|
meson test -C build/release \
|
|
fold:access_path fold:guarded_facts fold:div_by_zero \
|
|
fold:null_deref fold:oob_access fold:encoder_callee_predicates \
|
|
--print-errorlogs
|
|
|
|
python3 -m py_compile scripts/benchmarks/summarize_maturity.py
|
|
git diff --check
|
|
```
|
|
|
|
Result: `6/6 OK`, LSP diagnostics reported 0 errors for touched C++ files.
|
|
|
|
Additional benchmark smoke:
|
|
|
|
```sh
|
|
scripts/benchmarks/summarize_maturity.py --build build/release --source \
|
|
--output-dir /tmp/fold-maturity-source-check
|
|
```
|
|
|
|
Result: `status=ok`, `source_goldens=ok`.
|
|
|
|
Required-baseline negative checks passed for missing and malformed baseline JSON.
|
|
|
|
## Full suite
|
|
|
|
Full validation is running under monitor `#4`:
|
|
|
|
```sh
|
|
ninja -C build/release && meson test -C build/release --print-errorlogs && git diff --check
|
|
```
|