vbpf / prevail / 22081081213

push

github

Replace patricia tree with std::map (#1008)

Empirically, the median collection holds ~3 cells, overlap queries hit
<5% of the time, and the offset map is <1% of verifier runtime. At these
sizes, the patricia tree provided no benefit over std::map while adding
an external dependency.

- Remove radix_tree submodule dependency and offset_t bit-manipulation helpers
- Replace patricia tree with std::map<offset_t, std::set<Cell>>
- Simplify Cell to a plain struct with public (offset, size) fields
- Use defaulted == and <=> instead of manual comparison operators
- Replace Interval-based overlap check with direct integer arithmetic
- Move to_interval, symbolic_overlap, operator<< to free functions
- Inline get_scalar() as variable_registry->cell_var() at all call sites
- Document offset bound invariant in Cell::overlap
- Add assert(sz > 0) in Cell::overlap to document the invariant
- Simplify largest-cell lookup in get_overlap_cells_symbolic_offset:
  std::set is already sorted by (offset, size), so *rbegin() suffices
- Fix bug in backward scan of get_overlap_cells: remove early break
  that could skip overlapping cells at earlier offsets (a bucket with
  small cells may not overlap while an earlier bucket with larger
  cells does)
- Add assertion that offset <= EBPF_TOTAL_STACK_SIZE before the
gsl::narrow<int> conversion, documenting the precondition that
makes the narrowing safe.
- Add regression test for backward scan early-break bug

YAML test: writing to a sub-range of a cell must kill the cell so that a subsequent full-range
load returns unknown rather than the stale value.
The observation r0.svalue=0 (consistent mode) passes when the cell is correctly
havoced (0 is consistent with unknown) but fails when the stale
value r0.svalue=99 persists.

Verified: test fails when both the old remove_cell (no tombstone
cleanup) and the early break are reintroduced.
- Extract cell_var(kind, cell) helper to reduce repetition of
  variable_registry->cell_var(kind, c... (continued)

57 of 59 new or added lines in 1 file covered. (96.61%)

9319 of 10694 relevant lines covered (87.14%)

3049375.43 hits per line