Re: [RFC] optimize x - y cmp 0 with undefined overflow

[Eric Botcazou <ebotcazou@adacore.com>]

[I'm at last back to this...]

> > With [1, -x + INF] as the resulting range?  But it can be bogus if x is
> > itself equal to +INF (unlike the input range [x + 1, +INF] which is
> > always correct)
>
> Hmm, indeed.
> 
> > so this doesn't look valid to me.  I don't see how we can get away
> > without a +INF(OVF) here, but I can compute it in
> > extract_range_from_binary_expr_1 if you prefer and try only [op0,op0]
> > and [op1,op1].
> 
> Yeah, I'd prefer that.

To recap, the range of y is [x + 1, +INF] and we're trying to evaluate the 
range of y - x, in particular we want to prove that y - x > 0.

We compute the range of y - x as [1, -x + INF] by combining [x + 1, +INF] with 
[x, x] and we want to massage it because compare_values will rightly choke.

If overflow is undefined, we can simply change it to [1, +INF (OVF)] and be 
done with that.  But if overflow is defined, we need to prove that -x + INF
cannot wrap around (which is true if the type is unsigned) and the simplest 
way to do that in the general case is to recursively invoke the machinery
of extract_range_from_binary_expr_1 on range_of(-x) + INF and analyze the 
result.  This looks much more complicated implementation-wise (and would very 
likely buy us nothing in practice) than my scheme, where we just approximate 
range_of(-x) by [-INF,+INF] and don't need to implement the recursion at all.

However I can change extract_range_from_binary_expr so that only one range 
among [-INF,x], [x,+INF] and [x,x] is tried instead of the 3 ranges in a row.
I initially didn't want to do that because this breaks the separation between 
extract_range_from_binary_expr_1 and extract_range_from_binary_expr but, given 
their names, this is very likely acceptable.  What do you think?

-- 
Eric Botcazou