On Thu, Jul 24, 2025 at 12:15:53PM -0700, Eduard Zingerman wrote:
> On Thu, 2025-07-24 at 15:43 +0200, Paul Chaignon wrote:
[...]
> > +SEC("socket")
> > +__description("bounds deduction cross sign boundary, negative overlap")
> > +__success __log_level(2) __flag(BPF_F_TEST_REG_INVARIANTS)
> > +__msg("7: (1f) r0 -= r6 {{.*}} R0=scalar(smin=-655,smax=smax32=-146,umin=0xfffffffffffffd71,umax=0xffffffffffffff6e,smin32=-783,umin32=0xfffffcf1,umax32=0xffffff6e,var_off=(0xfffffffffffffc00; 0x3ff))")
>
> Interesting, note the difference: smin=-655, smin32=-783.
> There is a code to infer s32 range from s46 range in this situation in
> __reg32_deduce_bounds(), but it looks like a third __reg_deduce_bounds
> call is needed to trigger it. E.g. the following patch removes the
> difference for me:
Hm, I can add the third __reg_deduce_bounds to the first patch in the
series. That said, we may want to rethink and optimize reg_bounds_sync
in a followup patchset. It's probably worth listing all the inferences
we have and their dependencies and see if we can reorganize the
subfunctions.
>
> diff --git a/kernel/bpf/verifier.c b/kernel/bpf/verifier.c
> index f0a41f1596b6..87050d17baf9 100644
> --- a/kernel/bpf/verifier.c
> +++ b/kernel/bpf/verifier.c
> @@ -2686,6 +2686,7 @@ static void reg_bounds_sync(struct bpf_reg_state *reg)
> /* We might have learned something about the sign bit. */
> __reg_deduce_bounds(reg);
> __reg_deduce_bounds(reg);
> + __reg_deduce_bounds(reg);
> /* We might have learned some bits from the bounds. */
> __reg_bound_offset(reg);
> /* Intersecting with the old var_off might have improved our bounds
>
> > +__retval(0)
> > +__naked void bounds_deduct_negative_overlap(void)
> > +{
> > + asm volatile(" \
> > + call %[bpf_get_prandom_u32]; \
> > + w3 = w0; \
> > + w6 = (s8)w0; \
> > + r0 = (s8)r0; \
> > + if w6 >= 0xf0000000 goto l0_%=; \
> > + r0 += r6; \
> > + r6 += 400; \
> > + r0 -= r6; \
> > + if r3 < r0 goto l0_%=; \
> > +l0_%=: r0 = 0; \
> > + exit; \
> > +" :
> > + : __imm(bpf_get_prandom_u32)
> > + : __clobber_all);
> > +}
>
> [...]
