On Fri, 2025-03-14 at 19:51 -0700, Alexei Starovoitov wrote:
[...]
> 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.
In [1] I tried conservatively marking cached state registers as both
read and precise when states_equal(cached, cur, RANGE_WITHIN) == true.
It works for the example at hand, but indeed falls apart because it
interferes with widening logic. So, anything like below can't be
verified anymore (what was I thinking?):
SEC("raw_tp")
__success
int iter_nested_deeply_iters(const void *ctx)
{
int sum = 0;
MY_PID_GUARD();
bpf_repeat(10) {
...
sum += 1;
...
}
return sum;
}
Looks like there are only two options left:
a. propagate read/precision marks in state graph until fixed point is
reached;
b. switch to CFG based DFA analysis (will need slot/register type
propagation to identify which scalars can be precise).
(a) is more in line with what we do currently and probably less code.
But I expect that it would be harder to think about in case if
something goes wrong (e.g. we don't print/draw states graph at the
moment, I have a debug patch for this that I just cherry-pick).
[1] https://github.com/eddyz87/bpf/tree/incomplete-read-marks-debug.1
