On Tue, Sep 19, 2023 at 5:19 PM Eduard Zingerman <eddyz87@xxxxxxxxx> wrote:
>
> > >
> > > Note that R7=fp-16 in old state vs R7_w=57005 in cur state.
> > > The registers are considered equal because R7 does not have a read mark.
> > > However read marks are not yet finalized for old state because
> > > sl->state.branches != 0.
By "liveness marks are not finalized" you mean that
regs don't have LIVE_DONE?
That shouldn't matter to state comparison.
It only needs to see LIVE_READ.
LIVE_DONE is a sanity check for liveness algorithm only.
It doesn't affect correctness.
> > > (Note: precision marks are not finalized as
> > > well, which should be a problem, but this requires another example).
> >
> > I originally convinced myself that non-finalized precision marking is
> > fine, see the comment next to process_iter_next_call() for reasoning.
> > If you can have a dedicated example for precision that would be great.
> >
> > As for read marks... Yep, that's a bummer. That r7 is not used after
> > the loop, so is not marked as read, and it's basically ignored for
> > loop invariant checking, which is definitely not what was intended.
>
> Liveness is a precondition for all subsequent checks, so example
> involving precision would also involve liveness. Here is a combined
> example:
>
> r8 = 0
> fp[-16] = 0
> r7 = -16
> r6 = bpf_get_current_pid_tgid()
> bpf_iter_num_new(&fp[-8], 0, 10)
> while (bpf_iter_num_next(&fp[-8])) {
> r6++
> if (r6 != 42) {
> r7 = -32
> continue;
> }
> r0 = r10
> r0 += r7
> r8 = *(u64 *)(r0 + 0)
> }
> bpf_iter_num_destroy(&fp[-8])
> return r8
>
> (Complete source code is at the end of the email).
>
> The call to bpf_iter_num_next() is reachable with r7 values -16 and -32.
> State with r7=-16 is visited first, at which point r7 has no read mark
> and is not marked precise.
> State with r7=-32 is visited second:
> - states_equal() for is_iter_next_insn() should ignore absence of
> REG_LIVE_READ mark on r7, otherwise both states would be considered
> identical;
I think assuming live_read on all regs in regsafe() when
cb or iter body is being processed will have big impact
on processed insns.
I suspect the underlying issue is different.
In the first pass of the body with r7=-16 the 'r0 += r7'
insn should have added the read mark to r7,
so is_iter_next_insn after 2nd pass with r7=-32 should reach
case SCALAR_VALUE in regsafe().
There we need to do something with lack of precision in r7=-16,
but assume that is fixed, the 3rd iter of the loop should continue
and 'r0 += r7' in the _3rd_ iter of the loop should propagate
read mark all the way to r7=-32 reg.
I mean the parentage chain between regs should link
regs of iterations.
I believe the process_iter_next_call() logic maintains
correct parentage chain, since it's just a push_stack()
and is_state_visited() should be connecting parents.
So in case of iter body the issue with above loop is only
in missing precision,
but for your cb verification code I suspect the issue is due
to lack of parentage chain and liveness is not propagated ?
I could be completely off the mark.
The discussion is hard to follow.
It's probably time to post raw patch and continue with code.
