Re: [PATCH v5 bpf-next 2/3] bpf: Relax precision marking in open coded iters and may_goto loop.

[Eduard Zingerman <eddyz87@gmail.com>]

On Thu, 2024-06-06 at 15:19 -0700, Eduard Zingerman wrote:

[...]

> For the following C code:
> 
>     long arr1[1024];
> 
>     SEC("socket")
>     __success
>     int test1(const void *ctx)
>     {
>         long i;
>     
>         for (i = 0; i < 1024 && can_loop; i++)
>                 arr1[i] = i;
>         return 0;
>     }
>     
> clang generates the following BPF code:
> 
> 0000000000000340 <test1>:
>      104:       r1 = 0x0
>      105:       r2 = 0x0 ll
> 
> 0000000000000358 <LBB28_1>:
>      107:       may_goto +0x4 <LBB28_3>
>      108:       *(u64 *)(r2 + 0x0) = r1
>      109:       r2 += 0x8
>      110:       r1 += 0x1
>      111:       if r1 != 0x400 goto -0x5 <LBB28_1>
> 
> 0000000000000380 <LBB28_3>:
>      112:       w0 = 0x0
>      113:       exit

[...]

I've also took a look why the same program could be verified w/o
can_loop, but fails with can_loop (with this series applied):

0000000000000358 <LBB28_1>:
     107:       may_goto +0x4 <LBB28_3>
     108:       *(u64 *)(r2 + 0x0) = r1
     109:       r2 += 0x8
     110:       r1 += 0x1
     111:       if r1 != 0x400 goto -0x5 <LBB28_1>
                   ^^
    r1 is no longer marked precise,
    thus maybe_widen_reg() forgets the range for it
    when widen_imprecise_scalars() is called from
    may_goto processing logic.
    
As a result, verifier enumerates states
{r2=0P,r1=scalar()}, {r2=8P,r1=scalar()}, {r2=16P,r1=scalar()}, ...
eventually hitting the value of r2 that does not fit in 'arr1' bounds.