Re: [PATCH bpf-next 2/3] bpf: check bpf_func_state->callback_depth when pruning states

[Eduard Zingerman <eddyz87@gmail.com>]

Updated diagram with a few fixes, line numbers would be removed in the
final version.

--- 8< ---------------------------------

 .------------------------------------- Checkpoint / State name
 |    .-------------------------------- Code point number
 |    |   .---------------------------- Stack state {ctx.a,ctx.b,ctx.c}
 |    |   |        .------------------- Callback depth in frame #0
 v    v   v        v
1  - (0) {7P,7P,7},depth=0
2    - (3) {7P,7P,7},depth=1
3      - (0) {7P,7P,42},depth=1
(a)      - (3) {7P,7,42},depth=2
4          - (0) {7P,7,42},depth=2      loop terminates because of depth limit
5            - (4) {7P,7,42},depth=0    predicted false, ctx.a marked precise
6            - (6) exit
7        - (2) {7P,7,42},depth=2
8          - (0) {7P,42,42},depth=2     loop terminates because of depth limit
9            - (4) {7P,42,42},depth=0   predicted false, ctx.a marked precise
10           - (6) exit
(b)      - (1) {7P,7P,42},depth=2
11         - (0) {42P,7P,42},depth=2    loop terminates because of depth limit
12           - (4) {42P,7P,42},depth=0  predicted false, ctx.{a,b} marked precise
13           - (6) exit
14   - (2) {7P,7,7},depth=1
15     - (0) {7P,42,7},depth=1          considered safe, pruned using checkpoint (a)
(c)  - (1) {7P,7P,7},depth=1            considered safe, pruned using checkpoint (b)

Here checkpoint (b) has callback_depth of 2, meaning that it would
never reach state {42,42,7}.
While checkpoint (c) has callback_depth of 1, and thus
could yet explore the state {42,42,7} if not pruned prematurely.
This commit makes forbids such premature pruning,
allowing verifier to explore states sub-tree starting at (c):

(c)  - (1) {7,7,7P},depth=1
16     - (0) {42P,7,7P},depth=1
         ...
17       - (2) {42,7,7},depth=2
18         - (0) {42,42,7},depth=2      loop terminates because of depth limit
19           - (4) {42,42,7},depth=0    predicted true, ctx.{a,b,c} marked precise
20             - (5) division by zero

--------------------------------- >8 ---