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?
