[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
