On Fri, 2024-07-19 at 19:00 +0800, Xu Kuohai wrote: > From: Shung-Hsi Yu <shung-hsi.yu@xxxxxxxx> [...] > > | src_reg > smin' = ? +----------------------------+--------------------------- > smin'(r) <= smin(r) | negative | non-negative > ---------+--------------+----------------------------+--------------------------- > | negative |negative_bit_floor( |negative_bit_floor( > | | min(dst->smin, src->smin))| min(dst->smin, src->smin)) > dst_reg +--------------+----------------------------+--------------------------- > | non-negative |negative_bit_floor( |negative_bit_floor( > | | min(dst->smin, src->smin))| min(dst->smin, src->smin)) > > Meaning that simply using > > negative_bit_floor(min(dst_reg->smin_value, src_reg->smin_value)) > > to calculate the resulting smin_value would work across all sign combinations. > > Together these allows the BPF verifier to infer the signed range of the > result of BPF_AND operation using the signed range from its operands, > and use that information > > r0 s>>= 63; R0_w=scalar(smin=smin32=-1,smax=smax32=0) > r0 &= -13 ; R0_w=scalar(smin=smin32=-16,smax=smax32=0,umax=0xfffffffffffffff3,umax32=0xfffffff3,var_off=(0x0; 0xfffffffffffffff3)) > > [0] https://lore.kernel.org/bpf/e62e2971301ca7f2e9eb74fc500c520285cad8f5.camel@xxxxxxxxx/ > > Link: https://lore.kernel.org/bpf/phcqmyzeqrsfzy7sb4rwpluc37hxyz7rcajk2bqw6cjk2x7rt5@m2hl6enudv7d/ > Cc: Eduard Zingerman <eddyz87@xxxxxxxxx> > Signed-off-by: Shung-Hsi Yu <shung-hsi.yu@xxxxxxxx> > Acked-by: Xu Kuohai <xukuohai@xxxxxxxxxx> > --- I find derivation of these new rules logical. Also tried a simple brute force testing of this algorithm for 6-bit signed integers, and have not found any constraint violations: https://github.com/eddyz87/bpf-and-brute-force-check As a nitpick, I think that it would be good to have some shortened version of the derivation in the comments alongside the code. (Maybe with a link to the mailing list). Acked-by: Eduard Zingerman <eddyz87@xxxxxxxxx> [...]
