vbpf / prevail / 29851398100

87%

push

github

Reconstruct inlined callee's internal edges in a second pass (fixes #1203) (#1209)

* Reconstruct inlined callee's internal edges in a second pass (fixes #1203)

When a bpf-to-bpf local function is inlined, `add_cfg_nodes` reconstructed the
clone's internal edges incrementally, pulling only from already-cloned
predecessors. Nodes are processed in ascending instruction index, so a loop
head is cloned before its latch. When the head is cloned the latch clone does
not exist yet, so the back-edge (latch->head) is skipped; when the latch is
later cloned only its own predecessors are consulted, so the back-edge is never
re-added.

The cloned subprogram was therefore analyzed straight-line: `Wto` found no
cycle, the ascending sequence never widened the loop, and `check_for_termination`
inserted no loop counter. A pointer in bounds on iteration 1 but out of bounds
by iteration k was never checked -- an accept-unsafe soundness hole.

Reconstruct all internal edges (and exit transitions) in a second pass, after
every macro block has been cloned, adding edges from the successor side. `Cfg`
adjacency is a std::set, so this is idempotent. The first (cloning) pass now
only clones blocks and walks successors to enqueue them.

Regression test in test-data/calllocal.yaml: a counted loop wholly inside a
callee. With the fix the loop counter `pc[0/3]` appears in the post-invariant;
without it the loop is analyzed for a single iteration and no counter is
produced.

* Add accept-unsafe regression; simplify successor loop (review #1209)

- Add a companion test that demonstrates the *unsound* outcome the fix removes,
  not just the sound one. A callee walks a packet pointer one byte further each
  iteration and reads through it without re-checking the index against
  packet_size; `assume r2 != r1` keeps the first read (packet[0]) in bounds.
  Before the fix the callee loop lost its back-edge and was analyzed for that
  single iteration, so the read was accepted (accept-unsa... (continued)

10 of 10 new or added lines in 1 file covered. (100.0%)

9326 of 10749 relevant lines covered (86.76%)

6318729.09 hits per line