Hi,

I’m trying expand the Float2Int pass in order to make it able to optimize

expressions like f * x > y, where x and y are integers (we’ll assume unsigned for

simplicity) and f is a floating point constant. The optimization would convert

the expression to something like:

(a * x)/b > y

where a and b are integers guessed by the compiler (currently using continued

fractions, but some other method could also be used). The exact expression

would depend on the comparison type and on the type of input integers.

Note that dividing by an integer constant should be a cheap operation

compared to FP multiplication and comparison as this would get lowered to a

multiply+subtract+shift sequence (and should certainly be true on cores with no

FP unit)

The change will add some machinery to Float2Int in order to be able to

match certain known patterns. All patterns will have exactly representable

inputs and outputs. In this case, the FCMP will have two inputs, x and y and

one output (the result of the comparison). This allows us to use the existing

Float2Int infrastructure to track the integer length that would be required

for the conversion.

The main difficulty I can see with this is validating the transformation. Ideally

the property that we want to prove for the guessed integers a and b would be

that (a*x)/b == round_to_zero(f * to_float(x)), for every integer x in a given

range. The problem with this is that we would need to come up with a reasonably

quick method of proving this.

My best guess (still need to work out the exact details) would be that we only

need to check the first and last b numbers of the range. A hand-wavy argument

for this would be that since errors increase on the extremities of the range, so if

an error appears anywhere it must also appear at the edges of the range.

I still need to prove this. If there are any floating-point experts that can help

with this, I would greatly appreciate it.

Any other comments about the overall merits of the idea and the approach are

of course also welcome!

Thanks,

Silviu