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.
