On Thu, Dec 14, 2023 at 6:21 AM Maxim Mikityanskiy <maxtram95@xxxxxxxxx> wrote:
>
> Hi Andrii,
>
> I'm preparing a series for submission [1], and it started failing on
> this selftest on big endian after I rebased over your series. Can we
> discuss (see below) to figure out whether it's a bug in your patch or
> whether I'm missing something?
>
> On Tue, 05 Dec 2023 at 10:42:47 -0800, Andrii Nakryiko wrote:
> > Enhance partial_stack_load_preserves_zeros subtest with detailed
> > precision propagation log checks. We know expect fp-16 to be spilled,
> > initially imprecise, zero const register, which is later marked as
> > precise even when partial stack slot load is performed, even if it's not
> > a register fill (!).
> >
> > Acked-by: Eduard Zingerman <eddyz87@xxxxxxxxx>
> > Signed-off-by: Andrii Nakryiko <andrii@xxxxxxxxxx>
> > ---
> > .../selftests/bpf/progs/verifier_spill_fill.c | 16 ++++++++++++++++
> > 1 file changed, 16 insertions(+)
> >
> > diff --git a/tools/testing/selftests/bpf/progs/verifier_spill_fill.c b/tools/testing/selftests/bpf/progs/verifier_spill_fill.c
> > index 41fd61299eab..df4920da3472 100644
> > --- a/tools/testing/selftests/bpf/progs/verifier_spill_fill.c
> > +++ b/tools/testing/selftests/bpf/progs/verifier_spill_fill.c
> > @@ -495,6 +495,22 @@ char single_byte_buf[1] SEC(".data.single_byte_buf");
> > SEC("raw_tp")
> > __log_level(2)
> > __success
> > +/* make sure fp-8 is all STACK_ZERO */
> > +__msg("2: (7a) *(u64 *)(r10 -8) = 0 ; R10=fp0 fp-8_w=00000000")
> > +/* but fp-16 is spilled IMPRECISE zero const reg */
> > +__msg("4: (7b) *(u64 *)(r10 -16) = r0 ; R0_w=0 R10=fp0 fp-16_w=0")
> > +/* and now check that precision propagation works even for such tricky case */
> > +__msg("10: (71) r2 = *(u8 *)(r10 -9) ; R2_w=P0 R10=fp0 fp-16_w=0")
>
> Why do we require R2 to be precise at this point? It seems the only
> reason it's marked as precise here is because it was marked at line 6,
> and the mark was never cleared: when R2 was overwritten at line 10, only
> __mark_reg_const_zero was called, and no-one cleared the flag, although
> R2 was overwritten.
>
> Moreover, if I replace r2 with r3 in this block, it doesn't get the
> precise mark, as I expect.
>
> Preserving the flag looks like a bug to me, but I wanted to double-check
> with you.
>
So let's look at the relevant pieces of the code and the log.
First, note that we set fp-16 slot to all zeroes by spilling register
with known value zero (but not yet marked precise)
3: (b7) r0 = 0 ; R0_w=0
4: (7b) *(u64 *)(r10 -16) = r0 ; R0_w=0 R10=fp0 fp-16_w=0
then eventually we get to insns #11, which is using r2 as an offset
into map_value pointer, so r2's value is important to know precisely,
so we start precision back propagation:
8: (73) *(u8 *)(r1 +0) = r2 ;
R1_w=map_value(map=.data.single_by,ks=4,vs=1) R2_w=P0
9: (bf) r1 = r6 ;
R1_w=map_value(map=.data.single_by,ks=4,vs=1)
R6_w=map_value(map=.data.single_by,ks=4,vs=1)
10: (71) r2 = *(u8 *)(r10 -9) ; R2_w=P0 R10=fp0 fp-16_w=0
11: (0f) r1 += r2
mark_precise: frame0: last_idx 11 first_idx 0 subseq_idx -1
mark_precise: frame0: regs=r2 stack= before 10: (71) r2 = *(u8 *)(r10 -9)
^^ here r2 is assigned from fp-16 slot, so now we drop r2, but start
tracking fp-16 to mark it as precise
mark_precise: frame0: regs= stack=-16 before 9: (bf) r1 = r6
mark_precise: frame0: regs= stack=-16 before 8: (73) *(u8 *)(r1 +0) = r2
mark_precise: frame0: regs= stack=-16 before 7: (0f) r1 += r2
mark_precise: frame0: regs= stack=-16 before 6: (71) r2 = *(u8 *)(r10 -1)
mark_precise: frame0: regs= stack=-16 before 5: (bf) r1 = r6
^^ irrelevant instructions which we just skip
mark_precise: frame0: regs= stack=-16 before 4: (7b) *(u64 *)(r10 -16) = r0
^^ here we notice that fp-16 was set by spilling r0 state, so we drop
fp-16, start tracking r0
mark_precise: frame0: regs=r0 stack= before 3: (b7) r0 = 0
^^ and finally we arrive at r0 which was assigned 0 directly. We are done.
All seems correct. Did you spot any problem in the logic?
> The context why it's relevant to my series: after patch [3], this fill
> goes to the then-branch on big endian (not to the else-branch, as
> before), and I copy the register with copy_register_state, which
> preserves the precise flag from the stack, not from the old value of r2.
>
I haven't looked at your patches, sorry, let's try figuring out if the
test's logic is broken, first.
> > +__msg("11: (0f) r1 += r2")
> > +__msg("mark_precise: frame0: last_idx 11 first_idx 0 subseq_idx -1")
> > +__msg("mark_precise: frame0: regs=r2 stack= before 10: (71) r2 = *(u8 *)(r10 -9)")
> > +__msg("mark_precise: frame0: regs= stack=-16 before 9: (bf) r1 = r6")
> > +__msg("mark_precise: frame0: regs= stack=-16 before 8: (73) *(u8 *)(r1 +0) = r2")
> > +__msg("mark_precise: frame0: regs= stack=-16 before 7: (0f) r1 += r2")
> > +__msg("mark_precise: frame0: regs= stack=-16 before 6: (71) r2 = *(u8 *)(r10 -1)")
> > +__msg("mark_precise: frame0: regs= stack=-16 before 5: (bf) r1 = r6")
> > +__msg("mark_precise: frame0: regs= stack=-16 before 4: (7b) *(u64 *)(r10 -16) = r0")
> > +__msg("mark_precise: frame0: regs=r0 stack= before 3: (b7) r0 = 0")
> > __naked void partial_stack_load_preserves_zeros(void)
> > {
> > asm volatile (
> > --
> > 2.34.1
> >
> >
>
> [1]: https://github.com/kernel-patches/bpf/pull/6132
> [2]: https://git.kernel.org/pub/scm/linux/kernel/git/bpf/bpf-next.git/tree/kernel/bpf/verifier.c?id=c838fe1282df540ebf6e24e386ac34acb3ef3115#n4806
> [3]: https://github.com/kernel-patches/bpf/pull/6132/commits/0e72ee541180812e515b2bf3ebd127b6e670fd59
