On Fri, Jun 20, 2014 at 11:33 AM, Eric Botcazou <ebotca...@adacore.com> wrote:
> [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.

Hmm, indeed.  Put the above into a comment so it's clear why we don't
do it that way.

> 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?

Yeah, that sounds good to me.

Thanks,
Richard.

> --
> Eric Botcazou

Reply via email to