Tighten bounds of abs()

[rootjalex]

This PR does four things:

• Drive-by update of error message regarding LLVM version.
• Tightens bounds of abs() on an expression that is strictly positive
• Tightens bounds of abs() on an int32/int64 expression that is strictly negative
• Fixes horrendous upper bound overflow on abs() of an int32/int64 that could be negative. (move cast outside of the max).

I am struggling to come up with the right lower bound that tightens the interval for abs() of a strictly negative thing that is a smaller integer type, because -a.max could overflow.

Update: figured out the right expression for tightening bounds without negating something that could overflow. (updated z3 example as well)

Also, new bounds are formally verified via z3:

import z3
abs = lambda x: z3.If(x > 0, x, 0 - x)
min = lambda x, y: z3.If(x > y, y, x)
max = lambda x, y: z3.If(x > y, x, y)
x, xl, xu = z3.Ints("x xl xu")

z3.solve(xl <= x, x <= xu, abs(x) < max(xl, 0 - min(0, xu)))
z3.solve(xl <= x, abs(x) < max(xl, 0))
z3.solve(x <= xu, abs(x) < 0 - min(0, xu))

[abadams]

It's abs, so t is unsigned, and a.min.type() is signed. Don't you want to do the max in the unsigned type?

[rootjalex]

If a = [2, 10] then originally you got interval.max = max(u32(-2), u32(10)) = 4294967294

[abadams]

Right, I was only considering the a.min < 0 case. Doing it in the unsigned type would be: max(abs(a.min), abs(a.max)), but I'm guessing elsewhere in bounds inference isn't going to like that.

[rootjalex]

Yeah, the original code works for a.min < 0, but I think the new code works for both negative and positive a.min. If you assume negation can't overflow, then the comparison should be done in the signed type.

[steven-johnson]

Ready to land?