trevon/fold
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions
fold/ROADMAP_EXPANSION_TASKS_REPORT.md
trvon 50230c809b
 checkpoint
2026-06-04 20:20:29 -04:00

3.5 KiB
Raw Permalink Blame History

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

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:

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:

ninja -C build/release && meson test -C build/release --print-errorlogs && git diff --check