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).
[...]
