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.