vbpf / ebpf-verifier / 11768558728

87%

Build Type

push

github

Committed by web-flow

Commit Message

Use GuardedInstruction for cfg_t node, instead of basic_block (#789)

cfg node is GuardedInstruction, not basic_block_t.

basic_block is destined to be a view of the CFG, not an essential part of it. The new node is called value_t since node_t is taken. We should find a better name though.

The checker still performs transfer after checking the assertions, but it's only needed in order to find out locations where the invariants becomes bottom, and there are better way to do it. avoiding this should improve performance significantly.

There are "Undefined" instructions instead of a NOP on entry and exit.

* simplify no longer affects the cfg itself. It should be relevant mainly for printing, and possibly as an optimization hint regarding where to keep the results of the fixpoint computation.
* Assume instructions get special nodes
* Loop counters get special nodes
* label_t is moved to a dedicated header. Added a special_label field, allowing distinguishing nodes for loop counters (and potentially jumps to fallthrough). Also, using the default "spaceship" comparison, and exit is not INT_MAX instead of -2.
* cfg_rev_t is removed.

Signed-off-by: Elazar Gershuni <elazarg@gmail.com>

Run Details

251 of 325 new or added lines in 15 files covered. (77.23%)

4 existing lines in 2 files now uncovered.

8520 of 9402 relevant lines covered (90.62%)

10837112.27 hits per line