On Wed, May 22, 2024 at 1:18 PM Eduard Zingerman <eddyz87@xxxxxxxxx> wrote:
>
> 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.
Agree with this conclusion.
As discussed offlist we can add a check that
Si->parent->parent...->parent == Sk.
to make the algorithm "by the book".
I'll play with that.
