On Tue, Jul 29, 2025 at 10:52 AM Shung-Hsi Yu <shung-hsi.yu@xxxxxxxx> wrote:
>
> I would say it is just not as precise, rather than inaccurate. But your
> point remain, the verifier was not able to come up with [0, 0] as the
> range after instruction 11, and we end up with [S16_MIN, S16_MAX]
> instead.
>
> Dimitar has a patchset[1] that make better use of tnum for sign
> extension, which should address this.
>
Hi and thanks for the nudge.
Agreed, to me this looks like the standard worst-case-scenario bail in
coerce_reg_to_size_sx() when the sign bit is unknown, and more
specifically the higher bits uniformity check here:
u64 top_smax = (reg->smax_value >> 16) << 16;
u64 top_smin = (reg->smin_value >> 16) << 16;
if (top_smax != top_smin)
goto out;
In this specific case, reg->smax_value >> 16 is
0x7fffffc000000000 >> 16 = 0x7fffffc0000 and shifting it back gives
top_smax = 0x7fffffc000000000. reg->smin_value >> 16 is
0 >> 16 = 0 and shifting back gives top_smin = 0 so we end up with the
large range defaults.
> Dimitar has a patchset[1] that make better use of tnum for sign
> extension, which should address this.
I have a simple out-of-tree checker which compares the resulting tnum
for different implementations of said scast. I haven't drafted any tests
to verify this exact scenario end-to-end, but the patch tries to deduce
the bounds from the tnum, so I ran it for this case with my proposal,
as well as Eduard's version of tnum_scast and they seem to agree here:
./tnum_scast_compare 0x0 0xffffffc000000000 2
Input: value=0x0000000000000000 mask=0xffffffc000000000 size=2
tnum_scast -> value=0x0000000000000000, mask=0x0000000000000000
tnum_scast_2 -> value=0x0000000000000000, mask=0x0000000000000000
Result: PASS (identical)
Sorry for the delay on this patch on my part. I'm still having a fair
amount of trouble on getting the whole changeset to work with the already
present __update_reg64_bounds, as well as writing some adequate tests.
I will follow up with these blockers on the original series.
