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

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

On 1/5/24 3:37 PM, Eduard Zingerman wrote:
> On Thu, 2024-01-04 at 23:14 -0800, Yonghong Song wrote:
> [...]
>> There is an alternative implementation in check_stack_write_var_off().
>> For a spill of value/reg 0, we can convert it to STACK_ZERO instead
>> of trying to maintain STACK_SPILL. If we convert it to STACK_ZERO,
>> then we can reuse the rest of logic in check_stack_write_var_off()
>> and at the end we have
>>
>>           if (zero_used) {
>>                   /* backtracking doesn't work for STACK_ZERO yet. */
>>                   err = mark_chain_precision(env, value_regno);
>>                   if (err)
>>                           return err;
>>           }
>>
>> although I do not fully understand the above either. Need to go back to
>> git history to find why.
> Regarding this particular code (unrelated to this the patch-set).
>
> Both check_stack_read_fixed_off() and check_stack_read_var_off()
> set destination register to zero if all bytes at varying offset are STACK_ZERO.
> Backtracking can handle fixed offset writes, but does not know how to
> handle varying offset writes. E.g. if:
> - there is some code 'arr[i] = r0';
> - and r0 happens to be zero for some state;
> - later arr[i] is used in precise context;
> Verifier would have no means to propagate precision mark to r0.
> Hence apply precision mark conservatively.
>
> Does that makes sense?

Thanks for explanation. I guess I understand now, it does make sense.
let us say arr array's element type is long (8 byte) and the range of i could be
from -32 to -1. I guess one way could be doing backtracking with "... = arr[i]"
is to have four ranges, [-32, -24), [-24, -16), [-16, -8), [-8, 0).
Later, when we see arr[i] = r0 and i has range [-32, 0). Since it covers [-32, -24), etc.,
precision marking can proceed with 'r0'. But I guess this can potentially
increase verifier backtracking states a lot and is not scalable. Conservatively
doing precision marking with 'r0' (in arr[i] = r0) is a better idea.

Andrii has similar comments in
   https://lore.kernel.org/bpf/CAEf4Bzb0LdSPnFZ-kPRftofA6LsaOkxXLN4_fr9BLR3iG-te-g@mail.gmail.com/