On Fri, Mar 14, 2025 at 10:41 AM Eduard Zingerman <eddyz87@xxxxxxxxx> wrote: > > On Thu, 2025-03-13 at 12:28 -0700, Eduard Zingerman wrote: > > [...] > > > Which makes me wonder. > > If read/precision marks for B are not final and some state D outside > > of the loop becomes equal to B, the read/precision marks for that > > state would be incomplete as well: > > > > D------. // as some read/precision marks are missing from C > > | // propagate_liveness() won't copy all necessary > > .-> A --. | // marks to D. > > | | | | > > | v v | > > '-- B C | > > ^ | > > '------' > > > > This makes comparison with 'loop_entry' states contagious, > > propagating incomplete read/precision mark flag up to the root state. > > This will have verification performance implications. > > > > Alternatively read/precision marks need to be propagated in the state > > graph until fixed point is reached. Like with DFA analysis. > > > > Решето. > > And below is an example that verifier does not catch. Looks like the whole concept of old-style liveness and precision is broken with loops. propagate_liveness() will take marks from old state, but old is incomplete, so propagating them into cur doesn't make cur complete either. > Another possibility is to forgo loop entries altogether and upon > states_equal(cached, cur, RANGE_WITHIN) mark all registers in the > `cached` state as read and precise, propagating this info in `cur`. > I'll try this as well. Have a gut feel that it won't work. Currently we have loop_entry->branches is a flag of "completeness". which doesn't work for loops, so maybe we need a bool flag for looping states and instead of: force_exact = loop_entry && complete use force_exact = loop_entry || incomplete looping state will have "incomplete" flag cleared only when branches == 0 ? or maybe never. The further we get into this the more I think we need to get rid of existing liveness, precision, and everything path sensitive and convert it all to data flow analysis.
