On Tue, Jul 22, 2025 at 03:32:03PM +0800, Shung-Hsi Yu wrote:
> On Sat, Jul 19, 2025 at 04:22:05PM +0200, Paul Chaignon wrote:
[...]
> > + /* If the s64 range crosses the sign boundary, then it's split
> > + * between the beginning and end of the U64 domain. In that
> > + * case, we can derive new bounds if the u64 range overlaps
> > + * with only one end of the s64 range.
> > + *
> > + * In the following example, the u64 range overlaps only with
> > + * positive portion of the s64 range.
> > + *
> > + * 0 U64_MAX
> > + * | [xxxxxxxxxxxxxx u64 range xxxxxxxxxxxxxx] |
> > + * |----------------------------|----------------------------|
> > + * |xxxxx s64 range xxxxxxxxx] [xxxxxxx|
> > + * 0 S64_MAX S64_MIN -1
> > + *
> > + * We can thus derive the following new s64 and u64 ranges.
> > + *
> > + * 0 U64_MAX
> > + * | [xxxxxx u64 range xxxxx] |
> > + * |----------------------------|----------------------------|
> > + * | [xxxxxx s64 range xxxxx] |
> > + * 0 S64_MAX S64_MIN -1
> > + *
> > + * If they overlap in two places, we can't derive anything
> > + * because reg_state can't represent two ranges per numeric
> > + * domain.
> > + *
> > + * 0 U64_MAX
> > + * | [xxxxxxxxxxxxxxxxx u64 range xxxxxxxxxxxxxxxxx] |
> > + * |----------------------------|----------------------------|
> > + * |xxxxx s64 range xxxxxxxxx] [xxxxxxxxxx|
> > + * 0 S64_MAX S64_MIN -1
> > + *
> > + * The first condition below corresponds to the diagram above.
> > + * The second condition considers the case where the u64 range
> > + * overlaps with the negative porition of the s64 range.
> > + */
> > + if (reg->umax_value < (u64)reg->smin_value) {
> > + reg->smin_value = (s64)reg->umin_value;
> > + reg->umax_value = min_t(u64, reg->umax_value, reg->smax_value);
>
> Acked-by: Shung-Hsi Yu <shung-hsi.yu@xxxxxxxx>
>
> Just one question/comment: could the u64 and s64 ranges be disjoint? Say
>
> 0 U64_MAX
> | [xxx u64 range xxx] |
> |----------------------------|----------------------------|
> |xxxxx s64 range xxxxxxxxx] [xxxxxxx|
> 0 S64_MAX S64_MIN -1
>
> If such case this code still works as the s64 range gets a bit wider at
> the smin end (thus still safe), and u64 range stays unchanged.
>
> That said if the u64 and s64 range always overlaps somewhere, it may be
> an invariant we want to check in reg_bounds_sanity_check(). I seems to
> have some vague memory that with conditionals jumps it may be possible
> to produce such disjoint signed & unsigned ranges, but I'm not sure if
> that is still true.
My assumption is that the u64 and s64 ranges can't be disjoint or that
would mean the register can't have any value. As you noted, even if that
were to happen, we would only lose some precision, i.e. the refinement
stays sound.
I considered returning an error from __reg64_deduce_bounds if that
invariant doesn't hold, but propagating it gets a bit messy. Adding it
to reg_bounds_sanity_check would likely be cleaner. Though to be
honest, I was hoping to see the impact of the present changes on the
syzbot reports before adding even more opportunities for invariant
violation reports :)
>
> > + } else if ((u64)reg->smax_value < reg->umin_value) {
> > + reg->smax_value = (s64)reg->umax_value;
> > + reg->umin_value = max_t(u64, reg->umin_value, reg->smin_value);
> > + }
> > }
> > }
> >
> > --
> > 2.43.0
> >
