On Mon, Jul 22, 2024 at 12:13:20AM GMT, Eduard Zingerman wrote: > 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 I accidentally left the above paragraph unfinished, it should end with ... and using that information, it can be sure that that the result of [-1, 0] & -13 will be within that expected range of [-4095, 0]. > > 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 Thanks! > As a nitpick, I think that it would be good to have some shortened > version of the derivation in the comments alongside the code. Agree it would. Will try to add a 2-4 sentence explanation. > (Maybe with a link to the mailing list). Adding a link to the mailing list seems out of the usual for comment in verifier.c though, and it would be quite long. That said, it would be nice to hint that there exists a more verbose version of the explanation. Maybe an explicit "see commit for the full detail" at the end of the added comment? > Acked-by: Eduard Zingerman <eddyz87@xxxxxxxxx> > > [...] Will send an update for this tomorrow.
