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

[Yonghong Song <yonghong.song@linux.dev>]

On 2/13/24 10:14 AM, Eduard Zingerman wrote:
> 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)

For the above line
    (c)  - (1) {7P,7P,7},depth=1            considered safe, pruned using checkpoint (b)
I would change to
    (c)  - (1) {7P,7P,7},depth=1
           - (0) {42P, 7P, 7},depth = 1     considered safe, pruned using checkpoint (11)

For
14   - (2) {7P,7,7},depth=1
15     - (0) {7P,42,7},depth=1          considered safe, pruned using checkpoint (a)
I suspect for line 15, the pruning uses checking point at line (8).

Other than the above, the diagram LGTM.

>
> 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 ---