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

[Eduard Zingerman <eddyz87@gmail.com>]

On Tue, 2024-05-21 at 19:47 -0700, Alexei Starovoitov wrote:

[...]

Regarding this part, since we discussed it off-list
(I'll continue with the rest of the patch a bit later).

> First of all:
>    if (is_may_goto_insn_at(env, insn_idx)) {
> +          update_loop_entry(cur, &sl->state);
>            if (states_equal(env, &sl->state, cur, RANGE_WITHIN)) {
> -                  update_loop_entry(cur, &sl->state);
> 
> This should be correct, since reaching the same insn should
> satisfy "if h1 in path" requirement of update_loop_entry() algorithm.
> It's too conservative to update loop_entry only on a state match.

So, this basically changes the definition of the verifier states loop.
Previously, we considered a state loop to be such a sequence of states
Si -> ... -> Sj -> ... -> Sk that states_equal(Si, Sk, RANGE_WITHIN)
is true.

With this change Si -> ... -> Sj -> ... Sk is a loop if call sites and
instruction pointers for Si and Sk match.

Whether or not Si and Sk are in the loop influences two things:
(a) if exact comparison is needed for states cache;
(b) if widening transformation could be applied to some scalars.

As far as I understand, all pairs (Si, Sk) marked as a loop using old
definition would be marked as such using new definition
(in a addition to some new pairs).

I think that it is safe to apply (a) and (b) in strictly more cases.
(Although it is probably possible to conjure a program where such
 change would hinder verification convergence).

[...]