On Thu, 2023-09-21 at 21:16 +0300, Eduard Zingerman wrote:
> On Thu, 2023-09-21 at 09:35 -0700, Andrii Nakryiko wrote:
> > I've been thinking in a similar direction as Alexei, overnight. Here
> > are some raw thoughts.
> >
> > I think the overall approach with iter verification is sound. If we
> > loop and see an equivalent state at the entry to next loop iteration,
> > then it's safe to assume doing many iterations is safe. The problem is
> > that delayed precision and read marks make this state equivalence
> > wrong in some case. So we need to find a solution that will ensure
> > that all precision and read marks are propagated to parent state
> > before making a decision about convergence.
> >
> > The idea is to let verifier explore all code paths starting from
> > iteration #N, except the code paths that lead to looping into
> > iteration #N+1. I tried to do that with validating NULL case first and
> > exiting from loop on each iteration (first), but clearly that doesn't
> > capture all the cases, as Eduard have shown.
> >
> > So what if we delay convergence state checks (and then further
> > exploration at iteration #N+1) using BFS instead of DFS? That is, when
> > we are about to start new iteration and check state convergence, we
> > enqueue current state to be processed later after all the states that
> > "belong" to iteration #N are processed.
>
> This sounds correct if one iterator is involved.
>
> > We should work out exact details on how to do this hybrid BFS+DFS, but
> > let's think carefully if this will solve the problems?
> >
> > I think this is conceptually similar to what Alexei proposed above.
> > Basically, we "unroll" loop verification iteration by iteration, but
> > make sure that we explore all the branching within iteration #N before
> > going one iteration deeper.
> >
> > Let's think if there are any cases which wouldn't be handled. And then
> > think how to implement this elegantly (e.g., some sort of queue within
> > a parent state, which sounds similar to this separate "branches"
> > counter that Alexei is proposing above).
>
> To better understand the suggestion, suppose there is some iterator
> 'I' and two states:
> - state S1 where depth(I) == N and pending instruction is "next(I)"
> - state S2 where depth(I) == N and pending instruction is *not* "next(I)"
> In such situation state S2 should be verified first, right?
> And in general, any state that is not at "next(I)" should be explored
> before S1, right?
>
> Such interpretation seems to be prone to deadlocks, e.g. suppose there
> are two iterators: I1 and I2, and two states:
> - state S1 with depth(I1) == N, depth(I2) == M, at instruction "next(I1)";
> - state S2 with depth(I1) == N, depth(I2) == M, at instruction "next(I2)".
>
> E.g. like in the following loop:
>
> for (;;) {
> if (<random condition>)
> if (!next(it1)) break; // a
> else
> if (!next(it2)) break; // b
> ...
> }
>
> I think it is possible to get to two states here:
> - (a) it1(active, depth 0), it2(active, depth 0) at insn "next(it1)"
> - (b) it1(active, depth 0), it2(active, depth 0) at insn "next(it2)"
>
> And it is unclear which one should be processed next.
> Am I missing something?
Not sure if such ordering issues a real issues or any of the
candidates could be picked.
How about a more dumb solution which, imho, is easier to convince
oneself is correct (at-least from logical pov, not necessarily
implementation): substitute the goal of finding exact precision marks
with the goal of finding conservative precision marks. These marks
could be used instead of exact for states_equal() when .branches > 0.
A straightforward way to compute such marks is to run a flow-sensitive
context/path-insensitive backwards DFA before do_check(). The result
of this DFA is a bitmask encoding which registers / stack slots may be
precise at each instruction. Information for instructions other than
is_iter_next_insn() could be discarded.
Looking at the tests that are currently failing with my local fixes
(which force exact states comparions for .branches > 0) I think that
DFA based version would cover all of them.
This sure adds some code to the verifier, however changing current
states traversal logic from DFS to combination of DFS+BFS is a
significant change as well.
Wdyt?
