[llvm] goldsteinn/icmp to fcmp (PR #82290)

[via llvm-commits]

goldsteinn wrote:

NB: Proofs of the transform: https://alive2.llvm.org/ce/z/AJDdQ8

They timeout online, so need to be run locally. here is the output:
```
; $> /home/noah/programs/opensource/llvm-dev/src/alive2/build/alive-tv (-smt-to=200000000)

----------------------------------------
define i1 @src_eq(i32 %x, i32 %C) {
#0:
  %C_abs = abs i32 %C, 0
  %X_abs = abs i32 %x, 0
  %C_lemma = icmp ult i32 %C_abs, 16777216
  %X_lemma = icmp ult i32 %X_abs, 16777216
  %lemma = or i1 %C_lemma, %X_lemma
  assume i1 %lemma
  %cmp = icmp eq i32 %x, %C
  ret i1 %cmp
}
=>
define i1 @tgt_eq(i32 %x, i32 %C) {
#0:
  %C_abs = abs i32 %C, 0
  %X_abs = abs i32 %x, 0
  %C_lemma = icmp ult i32 %C_abs, 16777216
  %X_lemma = icmp ult i32 %X_abs, 16777216
  %lemma = or i1 %C_lemma, %X_lemma
  assume i1 %lemma
  %CFp = sitofp i32 %C to float
  %conv = sitofp i32 %x to float
  %cmp = fcmp oeq float %conv, %CFp
  ret i1 %cmp
}
Transformation seems to be correct!


----------------------------------------
define i1 @src_ne(i32 %x, i32 %C) {
#0:
  %C_abs = abs i32 %C, 0
  %X_abs = abs i32 %x, 0
  %C_lemma = icmp ult i32 %C_abs, 16777216
  %X_lemma = icmp ult i32 %X_abs, 16777216
  %lemma = or i1 %C_lemma, %X_lemma
  assume i1 %lemma
  %cmp = icmp ne i32 %x, %C
  ret i1 %cmp
}
=>
define i1 @tgt_ne(i32 %x, i32 %C) {
#0:
  %C_abs = abs i32 %C, 0
  %X_abs = abs i32 %x, 0
  %C_lemma = icmp ult i32 %C_abs, 16777216
  %X_lemma = icmp ult i32 %X_abs, 16777216
  %lemma = or i1 %C_lemma, %X_lemma
  assume i1 %lemma
  %CFp = sitofp i32 %C to float
  %conv = sitofp i32 %x to float
  %cmp = fcmp one float %conv, %CFp
  ret i1 %cmp
}
Transformation seems to be correct!


----------------------------------------
define i1 @src_slt(i32 %x, i32 %C) {
#0:
  %C_abs = abs i32 %C, 0
  %X_abs = abs i32 %x, 0
  %C_lemma = icmp ult i32 %C_abs, 16777216
  %X_lemma = icmp ult i32 %X_abs, 16777216
  %lemma = or i1 %C_lemma, %X_lemma
  assume i1 %lemma
  %cmp = icmp slt i32 %x, %C
  ret i1 %cmp
}
=>
define i1 @tgt_slt(i32 %x, i32 %C) {
#0:
  %C_abs = abs i32 %C, 0
  %X_abs = abs i32 %x, 0
  %C_lemma = icmp ult i32 %C_abs, 16777216
  %X_lemma = icmp ult i32 %X_abs, 16777216
  %lemma = or i1 %C_lemma, %X_lemma
  assume i1 %lemma
  %CFp = sitofp i32 %C to float
  %conv = sitofp i32 %x to float
  %cmp = fcmp olt float %conv, %CFp
  ret i1 %cmp
}
Transformation seems to be correct!


----------------------------------------
define i1 @src_sgt(i32 %x, i32 %C) {
#0:
  %C_abs = abs i32 %C, 0
  %X_abs = abs i32 %x, 0
  %C_lemma = icmp ult i32 %C_abs, 16777216
  %X_lemma = icmp ult i32 %X_abs, 16777216
  %lemma = or i1 %C_lemma, %X_lemma
  assume i1 %lemma
  %cmp = icmp sgt i32 %x, %C
  ret i1 %cmp
}
=>
define i1 @tgt_sgt(i32 %x, i32 %C) {
#0:
  %C_abs = abs i32 %C, 0
  %X_abs = abs i32 %x, 0
  %C_lemma = icmp ult i32 %C_abs, 16777216
  %X_lemma = icmp ult i32 %X_abs, 16777216
  %lemma = or i1 %C_lemma, %X_lemma
  assume i1 %lemma
  %CFp = sitofp i32 %C to float
  %conv = sitofp i32 %x to float
  %cmp = fcmp ogt float %conv, %CFp
  ret i1 %cmp
}
Transformation seems to be correct!


----------------------------------------
define i1 @src_sle(i32 %x, i32 %C) {
#0:
  %C_abs = abs i32 %C, 0
  %X_abs = abs i32 %x, 0
  %C_lemma = icmp ult i32 %C_abs, 16777216
  %X_lemma = icmp ult i32 %X_abs, 16777216
  %lemma = or i1 %C_lemma, %X_lemma
  assume i1 %lemma
  %cmp = icmp sle i32 %x, %C
  ret i1 %cmp
}
=>
define i1 @tgt_sle(i32 %x, i32 %C) {
#0:
  %C_abs = abs i32 %C, 0
  %X_abs = abs i32 %x, 0
  %C_lemma = icmp ult i32 %C_abs, 16777216
  %X_lemma = icmp ult i32 %X_abs, 16777216
  %lemma = or i1 %C_lemma, %X_lemma
  assume i1 %lemma
  %CFp = sitofp i32 %C to float
  %conv = sitofp i32 %x to float
  %cmp = fcmp ole float %conv, %CFp
  ret i1 %cmp
}
Transformation seems to be correct!


----------------------------------------
define i1 @src_sge(i32 %x, i32 %C) {
#0:
  %C_abs = abs i32 %C, 0
  %X_abs = abs i32 %x, 0
  %C_lemma = icmp ult i32 %C_abs, 16777216
  %X_lemma = icmp ult i32 %X_abs, 16777216
  %lemma = or i1 %C_lemma, %X_lemma
  assume i1 %lemma
  %cmp = icmp sge i32 %x, %C
  ret i1 %cmp
}
=>
define i1 @tgt_sge(i32 %x, i32 %C) {
#0:
  %C_abs = abs i32 %C, 0
  %X_abs = abs i32 %x, 0
  %C_lemma = icmp ult i32 %C_abs, 16777216
  %X_lemma = icmp ult i32 %X_abs, 16777216
  %lemma = or i1 %C_lemma, %X_lemma
  assume i1 %lemma
  %CFp = sitofp i32 %C to float
  %conv = sitofp i32 %x to float
  %cmp = fcmp oge float %conv, %CFp
  ret i1 %cmp
}
Transformation seems to be correct!


----------------------------------------
define i1 @src_ult(i32 %x, i32 %C) {
#0:
  %C_lemma0 = icmp ult i32 %C, 16777216
  %X_lemma0 = icmp ult i32 %x, 16777216
  %lemma0 = or i1 %C_lemma0, %X_lemma0
  assume i1 %lemma0
  %C_lemma1 = icmp sge i32 %C, 0
  %X_lemma1 = icmp sge i32 %x, 0
  %lemma1 = and i1 %C_lemma1, %X_lemma1
  assume i1 %lemma1
  %cmp = icmp ult i32 %x, %C
  ret i1 %cmp
}
=>
define i1 @tgt_ult(i32 %x, i32 %C) {
#0:
  %C_lemma0 = icmp ult i32 %C, 16777216
  %X_lemma0 = icmp ult i32 %x, 16777216
  %lemma0 = or i1 %C_lemma0, %X_lemma0
  assume i1 %lemma0
  %C_lemma1 = icmp sge i32 %C, 0
  %X_lemma1 = icmp sge i32 %x, 0
  %lemma1 = and i1 %C_lemma1, %X_lemma1
  assume i1 %lemma1
  %CFp = sitofp i32 %C to float
  %conv = sitofp i32 %x to float
  %cmp = fcmp olt float %conv, %CFp
  ret i1 %cmp
}
Transformation seems to be correct!


----------------------------------------
define i1 @src_ule(i32 %x, i32 %C) {
#0:
  %C_lemma0 = icmp ult i32 %C, 16777216
  %X_lemma0 = icmp ult i32 %x, 16777216
  %lemma0 = or i1 %C_lemma0, %X_lemma0
  assume i1 %lemma0
  %C_lemma1 = icmp sge i32 %C, 0
  %X_lemma1 = icmp sge i32 %x, 0
  %lemma1 = and i1 %C_lemma1, %X_lemma1
  assume i1 %lemma1
  %cmp = icmp ule i32 %x, %C
  ret i1 %cmp
}
=>
define i1 @tgt_ule(i32 %x, i32 %C) {
#0:
  %C_lemma0 = icmp ult i32 %C, 16777216
  %X_lemma0 = icmp ult i32 %x, 16777216
  %lemma0 = or i1 %C_lemma0, %X_lemma0
  assume i1 %lemma0
  %C_lemma1 = icmp sge i32 %C, 0
  %X_lemma1 = icmp sge i32 %x, 0
  %lemma1 = and i1 %C_lemma1, %X_lemma1
  assume i1 %lemma1
  %CFp = sitofp i32 %C to float
  %conv = sitofp i32 %x to float
  %cmp = fcmp ole float %conv, %CFp
  ret i1 %cmp
}
Transformation seems to be correct!


----------------------------------------
define i1 @src_ugt(i32 %x, i32 %C) {
#0:
  %C_lemma0 = icmp ult i32 %C, 16777216
  %X_lemma0 = icmp ult i32 %x, 16777216
  %lemma0 = or i1 %C_lemma0, %X_lemma0
  assume i1 %lemma0
  %C_lemma1 = icmp sge i32 %C, 0
  %X_lemma1 = icmp sge i32 %x, 0
  %lemma1 = and i1 %C_lemma1, %X_lemma1
  assume i1 %lemma1
  %cmp = icmp ugt i32 %x, %C
  ret i1 %cmp
}
=>
define i1 @tgt_ugt(i32 %x, i32 %C) {
#0:
  %C_lemma0 = icmp ult i32 %C, 16777216
  %X_lemma0 = icmp ult i32 %x, 16777216
  %lemma0 = or i1 %C_lemma0, %X_lemma0
  assume i1 %lemma0
  %C_lemma1 = icmp sge i32 %C, 0
  %X_lemma1 = icmp sge i32 %x, 0
  %lemma1 = and i1 %C_lemma1, %X_lemma1
  assume i1 %lemma1
  %CFp = sitofp i32 %C to float
  %conv = sitofp i32 %x to float
  %cmp = fcmp ogt float %conv, %CFp
  ret i1 %cmp
}
Transformation seems to be correct!


----------------------------------------
define i1 @src_uge(i32 %x, i32 %C) {
#0:
  %C_lemma0 = icmp ult i32 %C, 16777216
  %X_lemma0 = icmp ult i32 %x, 16777216
  %lemma0 = or i1 %C_lemma0, %X_lemma0
  assume i1 %lemma0
  %C_lemma1 = icmp sge i32 %C, 0
  %X_lemma1 = icmp sge i32 %x, 0
  %lemma1 = and i1 %C_lemma1, %X_lemma1
  assume i1 %lemma1
  %cmp = icmp uge i32 %x, %C
  ret i1 %cmp
}
=>
define i1 @tgt_uge(i32 %x, i32 %C) {
#0:
  %C_lemma0 = icmp ult i32 %C, 16777216
  %X_lemma0 = icmp ult i32 %x, 16777216
  %lemma0 = or i1 %C_lemma0, %X_lemma0
  assume i1 %lemma0
  %C_lemma1 = icmp sge i32 %C, 0
  %X_lemma1 = icmp sge i32 %x, 0
  %lemma1 = and i1 %C_lemma1, %X_lemma1
  assume i1 %lemma1
  %CFp = sitofp i32 %C to float
  %conv = sitofp i32 %x to float
  %cmp = fcmp oge float %conv, %CFp
  ret i1 %cmp
}
Transformation seems to be correct!


----------------------------------------
define i1 @src_eq_bitcast(i32 %x, i32 %C) {
#0:
  %C_lemma = icmp ult i32 %C, 2139095041
  %X_lemma = icmp ult i32 %x, 2139095041
  %lemma = and i1 %C_lemma, %X_lemma
  assume i1 %lemma
  %cmp = icmp eq i32 %x, %C
  ret i1 %cmp
}
=>
define i1 @tgt_eq_bitcast(i32 %x, i32 %C) {
#0:
  %C_lemma = icmp ult i32 %C, 2139095041
  %X_lemma = icmp ult i32 %x, 2139095041
  %lemma = and i1 %C_lemma, %X_lemma
  assume i1 %lemma
  %CFp = bitcast i32 %C to float
  %conv = bitcast i32 %x to float
  %cmp = fcmp oeq float %conv, %CFp
  ret i1 %cmp
}
Transformation seems to be correct!


----------------------------------------
define i1 @src_ne_bitcast(i32 %x, i32 %C) {
#0:
  %C_lemma = icmp ult i32 %C, 2139095041
  %X_lemma = icmp ult i32 %x, 2139095041
  %lemma = and i1 %C_lemma, %X_lemma
  assume i1 %lemma
  %cmp = icmp ne i32 %x, %C
  ret i1 %cmp
}
=>
define i1 @tgt_ne_bitcast(i32 %x, i32 %C) {
#0:
  %C_lemma = icmp ult i32 %C, 2139095041
  %X_lemma = icmp ult i32 %x, 2139095041
  %lemma = and i1 %C_lemma, %X_lemma
  assume i1 %lemma
  %CFp = bitcast i32 %C to float
  %conv = bitcast i32 %x to float
  %cmp = fcmp one float %conv, %CFp
  ret i1 %cmp
}
Transformation seems to be correct!


----------------------------------------
define i1 @src_slt_bitcast(i32 %x, i32 %C) {
#0:
  %C_lemma = icmp ult i32 %C, 2139095041
  %X_lemma = icmp ult i32 %x, 2139095041
  %lemma = and i1 %C_lemma, %X_lemma
  assume i1 %lemma
  %cmp = icmp slt i32 %x, %C
  ret i1 %cmp
}
=>
define i1 @tgt_slt_bitcast(i32 %x, i32 %C) {
#0:
  %C_lemma = icmp ult i32 %C, 2139095041
  %X_lemma = icmp ult i32 %x, 2139095041
  %lemma = and i1 %C_lemma, %X_lemma
  assume i1 %lemma
  %CFp = bitcast i32 %C to float
  %conv = bitcast i32 %x to float
  %cmp = fcmp olt float %conv, %CFp
  ret i1 %cmp
}
Transformation seems to be correct!


----------------------------------------
define i1 @src_sgt_bitcast(i32 %x, i32 %C) {
#0:
  %C_lemma = icmp ult i32 %C, 2139095041
  %X_lemma = icmp ult i32 %x, 2139095041
  %lemma = and i1 %C_lemma, %X_lemma
  assume i1 %lemma
  %cmp = icmp sgt i32 %x, %C
  ret i1 %cmp
}
=>
define i1 @tgt_sgt_bitcast(i32 %x, i32 %C) {
#0:
  %C_lemma = icmp ult i32 %C, 2139095041
  %X_lemma = icmp ult i32 %x, 2139095041
  %lemma = and i1 %C_lemma, %X_lemma
  assume i1 %lemma
  %CFp = bitcast i32 %C to float
  %conv = bitcast i32 %x to float
  %cmp = fcmp ogt float %conv, %CFp
  ret i1 %cmp
}
Transformation seems to be correct!


----------------------------------------
define i1 @src_sle_bitcast(i32 %x, i32 %C) {
#0:
  %C_lemma = icmp ult i32 %C, 2139095041
  %X_lemma = icmp ult i32 %x, 2139095041
  %lemma = and i1 %C_lemma, %X_lemma
  assume i1 %lemma
  %cmp = icmp sle i32 %x, %C
  ret i1 %cmp
}
=>
define i1 @tgt_sle_bitcast(i32 %x, i32 %C) {
#0:
  %C_lemma = icmp ult i32 %C, 2139095041
  %X_lemma = icmp ult i32 %x, 2139095041
  %lemma = and i1 %C_lemma, %X_lemma
  assume i1 %lemma
  %CFp = bitcast i32 %C to float
  %conv = bitcast i32 %x to float
  %cmp = fcmp ole float %conv, %CFp
  ret i1 %cmp
}
Transformation seems to be correct!


----------------------------------------
define i1 @src_sge_bitcast(i32 %x, i32 %C) {
#0:
  %C_lemma = icmp ult i32 %C, 2139095041
  %X_lemma = icmp ult i32 %x, 2139095041
  %lemma = and i1 %C_lemma, %X_lemma
  assume i1 %lemma
  %cmp = icmp sge i32 %x, %C
  ret i1 %cmp
}
=>
define i1 @tgt_sge_bitcast(i32 %x, i32 %C) {
#0:
  %C_lemma = icmp ult i32 %C, 2139095041
  %X_lemma = icmp ult i32 %x, 2139095041
  %lemma = and i1 %C_lemma, %X_lemma
  assume i1 %lemma
  %CFp = bitcast i32 %C to float
  %conv = bitcast i32 %x to float
  %cmp = fcmp oge float %conv, %CFp
  ret i1 %cmp
}
Transformation seems to be correct!


----------------------------------------
define i1 @src_ult_bitcast(i32 %x, i32 %C) {
#0:
  %C_lemma = icmp ult i32 %C, 2139095041
  %X_lemma = icmp ult i32 %x, 2139095041
  %lemma = and i1 %C_lemma, %X_lemma
  assume i1 %lemma
  %cmp = icmp ult i32 %x, %C
  ret i1 %cmp
}
=>
define i1 @tgt_ult_bitcast(i32 %x, i32 %C) {
#0:
  %C_lemma = icmp ult i32 %C, 2139095041
  %X_lemma = icmp ult i32 %x, 2139095041
  %lemma = and i1 %C_lemma, %X_lemma
  assume i1 %lemma
  %CFp = bitcast i32 %C to float
  %conv = bitcast i32 %x to float
  %cmp = fcmp olt float %conv, %CFp
  ret i1 %cmp
}
Transformation seems to be correct!


----------------------------------------
define i1 @src_ule_bitcast(i32 %x, i32 %C) {
#0:
  %C_lemma = icmp ult i32 %C, 2139095041
  %X_lemma = icmp ult i32 %x, 2139095041
  %lemma = and i1 %C_lemma, %X_lemma
  assume i1 %lemma
  %cmp = icmp ule i32 %x, %C
  ret i1 %cmp
}
=>
define i1 @tgt_ule_bitcast(i32 %x, i32 %C) {
#0:
  %C_lemma = icmp ult i32 %C, 2139095041
  %X_lemma = icmp ult i32 %x, 2139095041
  %lemma = and i1 %C_lemma, %X_lemma
  assume i1 %lemma
  %CFp = bitcast i32 %C to float
  %conv = bitcast i32 %x to float
  %cmp = fcmp ole float %conv, %CFp
  ret i1 %cmp
}
Transformation seems to be correct!


----------------------------------------
define i1 @src_ugt_bitcast(i32 %x, i32 %C) {
#0:
  %C_lemma = icmp ult i32 %C, 2139095041
  %X_lemma = icmp ult i32 %x, 2139095041
  %lemma = and i1 %C_lemma, %X_lemma
  assume i1 %lemma
  %cmp = icmp ugt i32 %x, %C
  ret i1 %cmp
}
=>
define i1 @tgt_ugt_bitcast(i32 %x, i32 %C) {
#0:
  %C_lemma = icmp ult i32 %C, 2139095041
  %X_lemma = icmp ult i32 %x, 2139095041
  %lemma = and i1 %C_lemma, %X_lemma
  assume i1 %lemma
  %CFp = bitcast i32 %C to float
  %conv = bitcast i32 %x to float
  %cmp = fcmp ogt float %conv, %CFp
  ret i1 %cmp
}
Transformation seems to be correct!


----------------------------------------
define i1 @src_uge_bitcast(i32 %x, i32 %C) {
#0:
  %C_lemma = icmp ult i32 %C, 2139095041
  %X_lemma = icmp ult i32 %x, 2139095041
  %lemma = and i1 %C_lemma, %X_lemma
  assume i1 %lemma
  %cmp = icmp uge i32 %x, %C
  ret i1 %cmp
}
=>
define i1 @tgt_uge_bitcast(i32 %x, i32 %C) {
#0:
  %C_lemma = icmp ult i32 %C, 2139095041
  %X_lemma = icmp ult i32 %x, 2139095041
  %lemma = and i1 %C_lemma, %X_lemma
  assume i1 %lemma
  %CFp = bitcast i32 %C to float
  %conv = bitcast i32 %x to float
  %cmp = fcmp oge float %conv, %CFp
  ret i1 %cmp
}
Transformation seems to be correct!

Summary:
  20 correct transformations
  0 incorrect transformations
  0 failed-to-prove transformations
  0 Alive2 errors

```

https://github.com/llvm/llvm-project/pull/82290