On Mon, 2023-10-02 at 09:29 -0700, Alexei Starovoitov wrote: [...] > > I'd like to argue about B "widening" for a bit, as I think it might be > > interesting in general, and put A aside for now. The algorithm for > > widening looks as follows: > > - In is_states_equal() for (sl->state.branches > 0 && is_iter_next_insn()) case: > > - Check if states are equal exactly: > > - ignore liveness marks on old state; > > - demand same type for registers and stack slots; > > - ignore precision marks, instead compare scalars using > > regs_exact() [this differs from my previous emails, I'm now sure > > that for this scheme to be correct regs_exact() is needed]. > > - If there is an exact match then follow "hit" branch. The idea > > being that visiting exactly the same state can't produce new > > execution paths (like with graph traversal). > > Right. Exactly the same C state won't produce new paths > as seen in visited state V, but > if C==V at the same insn indx it means we're in the infinite loop. This is true in general, but for bpf_iter_next() we have a guarantee that iteration would end eventually. > > More formally, before pruning potential looping states we need to > > make sure that all precision and read marks are in place. > > To achieve this: > > - Process states from env->head while those are available, in case if > > potential looping state (is_states_equal()) is reached put it to a > > separate queue. > > - Once all env->head states are processed the only source for new read > > and precision marks is in postponed looping states, some of which > > might not be is_states_equal() anymore. Submit each such state for > > verification until fixed point is reached (repeating steps for > > env->head processing). > > Comparing if (sl->state.branches) makes sense to find infinite loop. > It's waste for the verifier to consider visited state V with branches > 0 > for pruning. > The safety of V is unknown. The lack of liveness and precision > is just one part. The verifier didn't conclude that V is safe yet. > The current state C being equivalent to V doesn't tell us anything. > > If infinite loop detection logic trips us, let's disable it. > I feel the fix should be in process_iter_next_call() to somehow > make it stop doing push_stack() when states_equal(N-1, N-2). Consider that we get to the environment state where: - all env->head states are exhausted; - all potentially looping states (stored in as a separate set of states instead of env->head) are states_equal() to some already explored state. I argue that if such environment state is reached the program should be safe, because: - Each looping state L is a sub-state of some explored state V and every path from V leads to either safe exit or another loop. - Iterator loops are guaranteed to exit eventually. Achieving this steady state is the mechanism that tells verifier that there is no need to schedule exploration of the N+1 iteration level for any iterator in the program.
