-
Notifications
You must be signed in to change notification settings - Fork 16.8k
[Proposal] Extend KnownFPClass with unit-Interval refinement flags #190809
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 constants: x == ±1.0
bounded ranges: x ∈ (0,1) or x ∈ (-1,0)
Note: (0, 1 + machine_eps) -> (0, 1]
At the same time for example ConstantRange doesn't support floating-point types.
Proposal
Introduce the following refinement flags for KnownFPClass and FPClassTest:
fcPosOne // x == +1.0
fcNegOne // x == -1.0
fcPosSubOne // x ∈ (0, +1)
fcNegSubOne // x ∈ (-1, 0)Or Unit instead One suffix.
Possible additional flags:
fcPosEps
fcNegEps
fcPosSubEps
fcNegSubEps
fcPosMaximum
fcNegMaximumAnd composed flags:
fcOne = fcNegOne | fcPosOne, // -1.0 or 1.0
fcSubOne = fcNegSubOne | fcPosSubOne, // x ∈ (-1, 0) U (0 1)
fcSubOneFull = fcNegSubOne | fcPosSubOne | fcZero, // x ∈ (-1, 1)
fcSubOneClosed = fcSubOneFull | fcOne, // x ∈ [-1, 1]Use Cases
Fractional part patterns
x - trunc(x)
x - floor(x)
x - ceil(x)These are guaranteed to be in:
[0, 1) --> fcPosZero | fcPosSubOneAnd unlock enables better simplification of comparisons around ±1.0, clamps, min/max, math functions often has bound checks in such intervals etc.
Here is a real case:
%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)which could be simplified with this proposal to:
%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) -> x, when we know x ∈ [0, 1.0)WDYT? Does it make sense?