Summary of the foo.ll Transformation

Original Transformation

The source in foo.ll checks whether:

fabs(float(x) - float(y)) < C

can be replaced with:

x == y

The concrete file uses:

• uitofp i16 -> float
• C = 1.0e-15

Alive2 validates the original example with:

alive-tv --disable-undef-input --smt-to=30000 foo.ll

and reports:

Transformation seems to be correct!

General Rule

For a binary floating-point format with precision p bits, the rewrite is sound for:

%a = uitofp_or_sitofp iN %x to FP
%b = uitofp_or_sitofp iN %y to FP
%d = fsub FP %a, %b
%u = call FP @llvm.fabs(FP %d)
%cmp = fcmp olt FP-or-wider %u, C

to:

%eq = icmp eq iN %x, %y

when both of these hold:

1. 0 < C <= 1
2. The integer-to-FP conversion is injective over the full input domain

That injectivity condition becomes:

• uitofp iN -> FP: require N <= p
• sitofp iN -> FP: require N <= p + 1

Why This Works

Under those conditions:

• Every input integer is represented exactly in FP.
• Distinct integers remain distinct after conversion.
• The difference between two unequal converted integers has magnitude at least 1.
• Therefore fabs(a - b) is:
  • 0 when x == y
  • at least 1 when x != y

So fabs(a - b) < C is equivalent to x == y exactly for 0 < C <= 1.

The fpext from float to double in the original file does not change the argument; it only compares the same nonnegative value in a wider format.

float Boundaries

For IEEE float, the precision is p = 24. Therefore:

• uitofp: safe up to i24
• sitofp: safe up to i25

Alive2 Boundary Checks

These checks were run with --disable-undef-input --smt-to=30000.

Verified

• uitofp i24 -> float, C = 1.0
• sitofp i25 -> float, C = 1.0

Rejected

• uitofp i24 -> float, C = 1.000001
  • Counterexample: x = 1, y = 0
  • Then fabs(float(x) - float(y)) = 1, so < 1.000001 is true but x == y is false.
• uitofp i25 -> float, C = 1.0
  • Counterexample from Alive2: two adjacent integers round to the same float.
  • Example: 16779285 and 16779284 both convert to 16779284.0f.

Signed Failure Past the Boundary

For sitofp i26 -> float, the transformation is not sound because conversion is no longer injective. A simple example is:

• 16777216 and 16777217 both convert to the same float
• so the source may return true for unequal inputs

Bottom Line

The rewrite

fabs(uitofp_or_sitofp(x) - uitofp_or_sitofp(y)) < C
    -> x == y

is sound when:

• 0 < C <= 1, and
• the source integer type is small enough to be represented injectively in the chosen FP type

For float, that means:

• unsigned: up to i24
• signed: up to i25