On Tue, Oct 3, 2023 at 8:33 AM Eduard Zingerman <eddyz87@xxxxxxxxx> wrote: > > > When I put states to the loop stack I do copy_verifier_state() and > increase .branches counter for each state parent, so this should not > trigger warnings with update_branch_counts(). No warn doesn't mean it's correct. I suspect what your reschedule_loop_states() will increase branches from 0 to 1. Which is equivalent to increasing refcnt from zero. Not good. > Logically, any state > that has a loop state as it's grandchild is not verified to be safe > until loops steady state is achieved, thus such states could not be > used for states pruning and it is correct to keep their branch > counters > 0. Correct. > > propagate_liveness() and propagate_precision() should not be called > for the delayed states (work-in-progress I'll update the patch). > Behavior for non-delayed states should not be altered by these changes. I disagree. Delayed states should not have different propagation rules. > Iterators (and callbacks) try to diverge from regular verification > logic of visiting all possible paths by making some general > assumptions about loop bodies. There is no way to verify safety of > such bodies w/o computing steady states. Iterators and callbacks should not be special. They are no different than bounded loops and their verification shouldn't be much different. Bounded loops have constant upper bound while iterators do not, so they have to converge based on state equivalence, but the verifier still has to do DFS and discover all possible paths, propagate precision and liveness before considering two states equivalent. It does this today for bounded loops and should do the same for iterators. The question is how to do it. Delaying states and breaking DFS assumptions is a non starter. I see now that my 2nd hack is still buggy. Differentiating state with branches vs looping_states counters doesn't seem to work in all cases. Your loop_state_deps1 demonstrates that. It's a great test.
