Re: [PATCH bpf-next v1 1/2] bpf: states with loop entry have incomplete read/precision marks

[Eduard Zingerman <eddyz87@gmail.com>]

On Fri, 2025-03-14 at 19:51 -0700, Alexei Starovoitov wrote:
> On Fri, Mar 14, 2025 at 10:41 AM Eduard Zingerman <eddyz87@gmail.com> 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.

Yes.
 
> > 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.

I think about it as follows:
- We can think about our path-tracing as if it is a path sensitive DFA;
- To make path sensitivity work we instantiate each "basic block"
  (span of instructions) for each path;
- Hence, instead of CFG there is a graph of states;
- So, use/def problem can be solved on this graph just like it is
  solved for CFG, but one needs to keep the complete graph to
  propagate the marks and reach fixed point;
- When "loop entry" is reached, assuming that all registers are read
  and all scalars are precise in that state is an over-approximation
  of an exact solution.
  
But I might miss something important.

> 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.

That's what I think as well.
I'll get back with analysis for cls_redirect and balancer_ingress from [1].

[1] https://lore.kernel.org/bpf/CAADnVQKcOLDqwhhQpy6YU13ZbY3edGgx1XpXF5VsmXt9Byxokg@mail.gmail.com/