On Wed, Jul 23, 2025 at 12:09:52AM +0200, Paul Chaignon wrote:
> 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 :)
Make sense, that is the better plan :)
...
