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

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

On 2/16/24 6:27 AM, Eduard Zingerman wrote:
> On Wed, 2024-02-14 at 09:42 -0800, Yonghong Song wrote:
>
>>>    .------------------------------------- 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)
> At that point:
> - there is a checkpoint at (1) with state {7P,7P,42}
> - verifier is at (1) in state {7,7,7}
> Thus, verifier won't proceed to (0) because {7,7,7} is states_equal to {7P,7P,42}.

Okay, I think the above example has BPF_F_TEST_STATE_FREQ set as in Patch 3. It will
be great if you can explicitly mention this (BPF_F_TEST_STATE_FREQ) in the commit message.
With this flag,
   (c)  - (1) {7P,7P,7},depth=1            considered safe, pruned using checkpoint (b)
is correct.

But then for
   14   - (2) {7P,7,7},depth=1
   15     - (0) {7P,42,7},depth=1          considered safe, pruned using checkpoint (a)
The state
   14   - (2) {7P,7,7},depth=1
will have state equal to
    7        - (2) {7P,7,42},depth=2
right?
   

>
>> 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).
> Right, because checkpoints for a particular insn form a stack. My bad.
>
>> Other than the above, the diagram LGTM.
> Thank you for the feedback, I'll post v2 shortly.