Re: [PATCH v2 bpf-next 1/2] bpf: Avoid one round of bounds deduction

[Eduard Zingerman <eddyz87@gmail.com>]

On Mon, 2026-03-09 at 18:30 -0700, Eduard Zingerman wrote:
> On Mon, 2026-03-09 at 18:07 -0700, Eduard Zingerman wrote:
> 
> [...]
> 
> > Of-course, I might have some bugs in the test definition, but in case
> > the definition is correct, I think I'm inclined to agree with Ihor
> > here. If we can't mathematically prove that the sequence converges in
> > a fixed number of steps, putting a loop on top of it seem to be a
> > reasonable thing to do.
> > 
> > [1] https://github.com/eddyz87/bpf/tree/deduce-bounds-reshuffle
> > [2] https://github.com/eddyz87/deduce-bounds-verif
> > 
> > [...]
> 
> Pushed an update to the test to check if new bounds are tighter than
> old bounds (instead of equivalent). Still get a failure log:
> 
> $ ./parse-log.sh out2.log
> Values extracted from log:
>   s32: [-1686110209,  1907957760]  v_s32=-1411416065
>   u32: [ 1746894847,  4030210048]  v_u32=2883551231
>   s64: [ -4350478693995380738,   2172132303447261182]  v_s64=-4350478693150261249
>   u64: [  2172132302103053322,  14096265381705949184]  v_u64=14096265380559290367
> 
> Running C code directly:
> input:
>   s32: [0x9b7fffff, 0x71b92000] [-1686110209, 1907957760]
>   u32: [0x681f7fff, 0xf0382000] [1746894847, 4030210048]
>   s64: [0xc39ffead797ffffe, 0x1e24f6d2501ffffe] [-4350478693995380738, 2172132303447261182]
>   u64: [0x1e24f6d20001040a, 0xc39ffeadf0382000] [2172132302103053322, 14096265381705949184]
> 
> old:
>   s32: [0x9b7fffff, 0xf0382000] [-1686110209, -264757248]
>   u32: [0x9b7fffff, 0xf0382000] [2608857087, 4030210048]
>   s64: [0xc39ffead9b7fffff, 0xc39ffeadf0382000] [-4350478693424955393, -4350478692003602432]
>   u64: [0xc39ffead9b7fffff, 0xc39ffeadf0382000] [14096265380284596223, 14096265381705949184]
> 
> new:
>   s32: [0x9b7fffff, 0x71b92000] [-1686110209, 1907957760]
>   u32: [0x797ffffe, 0xf0382000] [2038431742, 4030210048]
>   s64: [0xc39ffead797ffffe, 0xc39ffeadf0382000] [-4350478693995380738, -4350478692003602432]
>   u64: [0xc39ffead797ffffe, 0xc39ffeadf0382000] [14096265379714170878, 14096265381705949184]

I added back third round of __reg_deduce_bounds():

  diff --git a/deduce_bounds_new.c b/deduce_bounds_new.c
  index b0bd8c8..dc498b2 100644
  --- a/deduce_bounds_new.c
  +++ b/deduce_bounds_new.c
  @@ -326,4 +326,5 @@ void reg_bounds_sync_new(struct bpf_reg_state *reg)
   {
          __reg_deduce_bounds(reg);
          __reg_deduce_bounds(reg);
  +       __reg_deduce_bounds(reg);
   }

And run cbmc with the following assertions (see [1]):

	assert(a.smin_value == b.smin_value);
	assert(a.smax_value == b.smax_value);
	assert(a.umin_value == b.umin_value);
	assert(a.umax_value == b.umax_value);
	
	assert(a.s32_min_value == b.s32_min_value);
	assert(a.s32_max_value == b.s32_max_value);
	assert(a.u32_min_value == b.u32_min_value);
	assert(a.u32_max_value == b.u32_max_value);

This failed quickly with an example, showing different results for old
and new orderings, new being tighter.

And then with the following assertion:

	bool old_better = a.smin_value < b.smin_value ||
			  a.smax_value > b.smax_value ||
			  a.umin_value < b.umin_value ||
			  a.umax_value > b.umax_value ||
			  a.s32_min_value < b.s32_min_value ||
			  a.s32_max_value > b.s32_max_value ||
			  a.u32_min_value < b.u32_min_value ||
			  a.u32_max_value > b.u32_max_value;
	assert(!old_better);

This finished in 20 minutes claiming successful verification.
Hence, I conclude that new ordering is strictly better than the old
ordering if there are three rounds of deductions.

I suggest we should keep three rounds of deductions and adopt the new
ordering (or play with orderings some more to choose which one is
better under 3 rounds).

[1] https://github.com/eddyz87/deduce-bounds-verif/tree/experiment