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
