Re: [PATCH bpf-next v2 1/2] bpf: Track aligned st store as imprecise spilled registers

[Eduard Zingerman <eddyz87@gmail.com>]

On Mon, 2024-01-08 at 11:51 -0800, Yonghong Song wrote:
[...]
> > In case if check_stack_read_var_off() would be modified to check not
> > only for STACK_ZERO, but also for zero spills, I think that all such
> > spills would have to be marked precise at the time of read,
> > as backtracking would not be able to find those later.
> 
> I don't understand the above. If the code pattern looks like
>    r1 = ...; /* r1 range [-32, -16);
>    *(u8 *)(r10 + r1) = r2;
>    ...
>    r3 = *(u8 *)(r10 + r1);
>    r3 needs to be marked as precise.
> 
> Conservatively marking r2 in '*(u8 *)(r10 + r1) = r2' as precise
> should be the correct way to do.
> 
> Or you are thinking even more complex code pattern like
>    *(u64 *)(r10 - 32) = r4;
>    *(u64 *)(r10 - 24) = r5;
>    ...
>    r1 = ...; /* r1 range [-32, -16) */
>    r3 = *(u8 *)(r10 + r1);
>    r3 needs to be marked as precise.
> 
> In this case, we should proactively mark r4 and r5 as precise.
> But currently we did not do it, right?

Yes, I'm thinking about the latter scenario.
There would be zero spills for fp-32 and fp-24.
If check_stack_read_var_off() is modified to handle zero spills,
then it would conclude that r3 is zero.
But if r3 is later marked precise, there would be no info for
backtracking to mark fp-32, fp-24, r4, r5 as precise:
- either backtracking info would have to be supplemented with a list
  of stack locations that were spilled zeros at time of
  check_stack_read_var_off();
- or check_stack_read_var_off() would need to conservatively mark
  all spilled zeros as precise.

Nothing like that is needed now, because check_stack_read_var_off()
would return unbound scalar for r3 upon seeing zero spill.

> I think this later case is a very unlikely case.

But it is possible and verifier has to be conservative.