[Proposal] Extend KnownFPClass with Interval refinement flags
- Dominant language
- LLVM
- Stars
- 40.5k
- Forks
- 18.7k
- PR merge metrics
- PR metrics pending
Description
**Motivation**
`KnownFPClass` provides a lightweight classification of floating-point values (NaN, Inf, normal, subnormal, zero), but it lacks the ability to express common, high-value numeric constraints such as:
exact values: `x == ±1.0`, `x ∈ Z` (integral)
bounded ranges: `x ∈ (0, 1)`, `x ∈ (-1, 0)`, `x ∈ (-inf, -1)`, `x ∈ (1, +inf)`
Note: `(0, 1)` + `machine_eps` -> `(0, 1]`
At the same time for example `ConstantRange` doesn't support floating-point types and this would require the actual implementation of interval arithmetic.
**Proposal**
Introduce the following refinement flags for `KnownFPClass` and [FPClassTest](https://github.com/llvm/llvm-project/blob/dfa1c56358830e6a79a76235b56833dab2ac0b02/llvm/include/llvm/ADT/FloatingPointMode.h#L338):
```cpp
PosOne // x == +1.0
NegOne // x == -1.0
PosSubOne // x ∈ (0, +1)
NegSubOne // x ∈ (-1, 0)
PosSubIntegral // x ∈ (1, 2/eps]
NegSubIntegral // x ∈ [-2/eps, -1)
Integral // x ∈ Z
```
Or `Unit` instead `One` suffix.
Possible additional flags:
```cpp
PosEps // x == +eps
NegEps // x == -eps
PosSubEps // x ∈ (0, eps)
NegSubEps // x ∈ (-eps, 0)
PosMaximum // x == +max_fp
NegMaximum // x == -max_fp
PosMinNormal // + subrange
NegMinNormal // + subrange
PowerOfTwo // x ∈ 2.0 ^ k
```
And composed flags:
```ts
One = NegOne | PosOne, // -1.0 or 1.0
SubOne = NegSubOne | PosSubOne, // x ∈ (-1, 0) U (0 1)
SubOneFull = NegSubOne | PosSubOne | Zero, // x ∈ (-1, 1)
SubOneClosed = SubOneFull | One, // x ∈ [-1, 1]
```
**Use Cases**
Fractional part patterns
```c
x - trunc(x) // (-1, 1)
x - floor(x) // [ 0, 1)
x - ceil(x) // (-1, 0)
trunc(x) // integral
floor(x) // integral
ceil(x) // integral
sin(x) // [-1, 1]
cos(x) // [-1, 1]
tanh(x) // [-1, 1]
erf(x) // (-1, 1)
cosh(x) // not in [0, 1)
...
```
How to make closed bounds:
```c
(0, 1) --> PosSubOne
[0, 1) --> PosSubOne | fcPosZero
[0, 1] --> PosSubOne | fcPosZero | PosOne
```
And unlock enables better simplification of comparisons around ±1.0, clamps, min/max, math functions (sin, cos, tanh and other hyperbolic functions) or have some bound checks in such intervals etc.
Here is a [real case](https://github.com/llvm/llvm-project/issues/188035):
```llvm
%i = tail call float @llvm.floor.f32(float %x)
%sub.i.i = fsub nsz float %x, %i ;; sub.i.i ∈ [0, 1.0)
%i1 = tail call nsz float @llvm.minnum.f32(float %sub.i.i, float 0x3FEFFFFFE0000000 ;~ 1.0 - eps/2;)
```
which could be simplified with this proposal to:
```llvm
%i = tail call float @llvm.floor.f32(float %x)
%i1 = fsub nsz float %x, %i
;; get rid of @llvm.minnum.f32 due to min(x, 1.0 - eps/2) -> x, when we know x ∈ [0, 1.0)
```
**UPDATE**
New possible monotonic property with 3 flags:
```
- Isotonic f(x) <= f(y) <-> x <= y
- Antitonic f(x) >= f(y) <-> x <= y
- Periodic f(x + k*P) <-> f(x)
where P: 1.0, π/2, π
```
It also covers https://github.com/llvm/llvm-project/issues/187088 and many more already existing specific peephole rewrites
WDYT? Does it make sense?
Contributor guide
Assessment
This issue has not been assessed yet.