[llvm] [InstCombine] Add folds for `(fp_binop ({s|u}itofp x), ({s|u}itofp y))` (PR #82555)

[via llvm-commits]

goldsteinn wrote:

Result of all the proofs run locally:
```
; $> /home/noah/programs/opensource/llvm-dev/src/alive2/build/alive-tv (-smt-to=200000000)

----------------------------------------
define half @src_sisi_add_i8(i8 noundef %x, i8 noundef %y) {
#0:
  %overflow_info = sadd_overflow i8 noundef %x, noundef %y
  %does_overflow = extractvalue {i8, i1} %overflow_info, 1
  %doesnot_overflow = xor i1 %does_overflow, 1
  assume i1 %doesnot_overflow
  %xf = sitofp i8 noundef %x to half
  %yf = sitofp i8 noundef %y to half
  %r = fadd half %xf, %yf
  ret half %r
}
=>
define half @tgt_sisi_add_i8(i8 noundef %x, i8 noundef %y) {
#0:
  %overflow_info = sadd_overflow i8 noundef %x, noundef %y
  %does_overflow = extractvalue {i8, i1} %overflow_info, 1
  %doesnot_overflow = xor i1 %does_overflow, 1
  assume i1 %doesnot_overflow
  %xy = add i8 noundef %x, noundef %y
  %r = sitofp i8 %xy to half
  ret half %r
}
Transformation seems to be correct!


----------------------------------------
define half @src_uiui_add_i8(i8 noundef %x, i8 noundef %y) {
#0:
  %overflow_info = uadd_overflow i8 noundef %x, noundef %y
  %does_overflow = extractvalue {i8, i1} %overflow_info, 1
  %doesnot_overflow = xor i1 %does_overflow, 1
  assume i1 %doesnot_overflow
  %xf = uitofp i8 noundef %x to half
  %yf = uitofp i8 noundef %y to half
  %r = fadd half %xf, %yf
  ret half %r
}
=>
define half @tgt_uiui_add_i8(i8 noundef %x, i8 noundef %y) {
#0:
  %overflow_info = uadd_overflow i8 noundef %x, noundef %y
  %does_overflow = extractvalue {i8, i1} %overflow_info, 1
  %doesnot_overflow = xor i1 %does_overflow, 1
  assume i1 %doesnot_overflow
  %xy = add i8 noundef %x, noundef %y
  %r = uitofp i8 %xy to half
  ret half %r
}
Transformation seems to be correct!


----------------------------------------
define half @src_sisi_sub_i8(i8 noundef %x, i8 noundef %y) {
#0:
  %overflow_info = ssub_overflow i8 noundef %x, noundef %y
  %does_overflow = extractvalue {i8, i1} %overflow_info, 1
  %doesnot_overflow = xor i1 %does_overflow, 1
  assume i1 %doesnot_overflow
  %xf = sitofp i8 noundef %x to half
  %yf = sitofp i8 noundef %y to half
  %r = fsub half %xf, %yf
  ret half %r
}
=>
define half @tgt_sisi_sub_i8(i8 noundef %x, i8 noundef %y) {
#0:
  %overflow_info = ssub_overflow i8 noundef %x, noundef %y
  %does_overflow = extractvalue {i8, i1} %overflow_info, 1
  %doesnot_overflow = xor i1 %does_overflow, 1
  assume i1 %doesnot_overflow
  %xy = sub i8 noundef %x, noundef %y
  %r = sitofp i8 %xy to half
  ret half %r
}
Transformation seems to be correct!


----------------------------------------
define half @src_uiui_sub_i8(i8 noundef %x, i8 noundef %y) {
#0:
  %overflow_info = usub_overflow i8 noundef %x, noundef %y
  %does_overflow = extractvalue {i8, i1} %overflow_info, 1
  %doesnot_overflow = xor i1 %does_overflow, 1
  assume i1 %doesnot_overflow
  %xf = uitofp i8 noundef %x to half
  %yf = uitofp i8 noundef %y to half
  %r = fsub half %xf, %yf
  ret half %r
}
=>
define half @tgt_uiui_sub_i8(i8 noundef %x, i8 noundef %y) {
#0:
  %overflow_info = usub_overflow i8 noundef %x, noundef %y
  %does_overflow = extractvalue {i8, i1} %overflow_info, 1
  %doesnot_overflow = xor i1 %does_overflow, 1
  assume i1 %doesnot_overflow
  %xy = sub i8 noundef %x, noundef %y
  %r = uitofp i8 %xy to half
  ret half %r
}
Transformation seems to be correct!


----------------------------------------
define half @src_sisi_mul_i8(i8 noundef %x, i8 noundef %y) {
#0:
  %x_okay = icmp ne i8 noundef %x, 0
  assume i1 %x_okay
  %y_okay = icmp ne i8 noundef %y, 0
  assume i1 %y_okay
  %overflow_info = smul_overflow i8 noundef %x, noundef %y
  %does_overflow = extractvalue {i8, i1} %overflow_info, 1
  %doesnot_overflow = xor i1 %does_overflow, 1
  assume i1 %doesnot_overflow
  %xf = sitofp i8 noundef %x to half
  %yf = sitofp i8 noundef %y to half
  %r = fmul half %xf, %yf
  ret half %r
}
=>
define half @tgt_sisi_mul_i8(i8 noundef %x, i8 noundef %y) {
#0:
  %x_okay = icmp ne i8 noundef %x, 0
  assume i1 %x_okay
  %y_okay = icmp ne i8 noundef %y, 0
  assume i1 %y_okay
  %overflow_info = smul_overflow i8 noundef %x, noundef %y
  %does_overflow = extractvalue {i8, i1} %overflow_info, 1
  %doesnot_overflow = xor i1 %does_overflow, 1
  assume i1 %doesnot_overflow
  %xy = mul i8 noundef %x, noundef %y
  %r = sitofp i8 %xy to half
  ret half %r
}
Transformation seems to be correct!


----------------------------------------
define half @src_uiui_mul_i8(i8 noundef %x, i8 noundef %y) {
#0:
  %overflow_info = umul_overflow i8 noundef %x, noundef %y
  %does_overflow = extractvalue {i8, i1} %overflow_info, 1
  %doesnot_overflow = xor i1 %does_overflow, 1
  assume i1 %doesnot_overflow
  %xf = uitofp i8 noundef %x to half
  %yf = uitofp i8 noundef %y to half
  %r = fmul half %xf, %yf
  ret half %r
}
=>
define half @tgt_uiui_mul_i8(i8 noundef %x, i8 noundef %y) {
#0:
  %overflow_info = umul_overflow i8 noundef %x, noundef %y
  %does_overflow = extractvalue {i8, i1} %overflow_info, 1
  %doesnot_overflow = xor i1 %does_overflow, 1
  assume i1 %doesnot_overflow
  %xy = mul i8 noundef %x, noundef %y
  %r = uitofp i8 %xy to half
  ret half %r
}
Transformation seems to be correct!


----------------------------------------
define half @src_sisi_add_i16(i16 noundef %x, i16 noundef %y) {
#0:
  %x_high_zeros = icmp ule i16 noundef %x, 2048
  %x_high_ones = icmp uge i16 noundef %x, 63488
  %x_okay = or i1 %x_high_zeros, %x_high_ones
  assume i1 %x_okay
  %y_high_zeros = icmp ule i16 noundef %y, 2048
  %y_high_ones = icmp uge i16 noundef %y, 63488
  %y_okay = or i1 %y_high_zeros, %y_high_ones
  assume i1 %y_okay
  %xf = sitofp i16 noundef %x to half
  %yf = sitofp i16 noundef %y to half
  %r = fadd half %xf, %yf
  ret half %r
}
=>
define half @tgt_sisi_add_i16(i16 noundef %x, i16 noundef %y) {
#0:
  %x_high_zeros = icmp ule i16 noundef %x, 2048
  %x_high_ones = icmp uge i16 noundef %x, 63488
  %x_okay = or i1 %x_high_zeros, %x_high_ones
  assume i1 %x_okay
  %y_high_zeros = icmp ule i16 noundef %y, 2048
  %y_high_ones = icmp uge i16 noundef %y, 63488
  %y_okay = or i1 %y_high_zeros, %y_high_ones
  assume i1 %y_okay
  %xy = add i16 noundef %x, noundef %y
  %r = sitofp i16 %xy to half
  ret half %r
}
Transformation seems to be correct!


----------------------------------------
define half @src_uiui_add_i16(i16 noundef %x, i16 noundef %y) {
#0:
  %x_okay = icmp ule i16 noundef %x, 2048
  assume i1 %x_okay
  %y_okay = icmp ule i16 noundef %y, 2048
  assume i1 %y_okay
  %xf = uitofp i16 noundef %x to half
  %yf = uitofp i16 noundef %y to half
  %r = fadd half %xf, %yf
  ret half %r
}
=>
define half @tgt_uiui_add_i16(i16 noundef %x, i16 noundef %y) {
#0:
  %x_okay = icmp ule i16 noundef %x, 2048
  assume i1 %x_okay
  %y_okay = icmp ule i16 noundef %y, 2048
  assume i1 %y_okay
  %xy = add i16 noundef %x, noundef %y
  %r = uitofp i16 %xy to half
  ret half %r
}
Transformation seems to be correct!


----------------------------------------
define half @src_sisi_sub_i16(i16 noundef %x, i16 noundef %y) {
#0:
  %x_high_zeros = icmp ule i16 noundef %x, 2048
  %x_high_ones = icmp uge i16 noundef %x, 63488
  %x_okay = or i1 %x_high_zeros, %x_high_ones
  assume i1 %x_okay
  %y_high_zeros = icmp ule i16 noundef %y, 2048
  %y_high_ones = icmp uge i16 noundef %y, 63488
  %y_okay = or i1 %y_high_zeros, %y_high_ones
  assume i1 %y_okay
  %xf = sitofp i16 noundef %x to half
  %yf = sitofp i16 noundef %y to half
  %r = fsub half %xf, %yf
  ret half %r
}
=>
define half @tgt_sisi_sub_i16(i16 noundef %x, i16 noundef %y) {
#0:
  %x_high_zeros = icmp ule i16 noundef %x, 2048
  %x_high_ones = icmp uge i16 noundef %x, 63488
  %x_okay = or i1 %x_high_zeros, %x_high_ones
  assume i1 %x_okay
  %y_high_zeros = icmp ule i16 noundef %y, 2048
  %y_high_ones = icmp uge i16 noundef %y, 63488
  %y_okay = or i1 %y_high_zeros, %y_high_ones
  assume i1 %y_okay
  %xy = sub i16 noundef %x, noundef %y
  %r = sitofp i16 %xy to half
  ret half %r
}
Transformation seems to be correct!


----------------------------------------
define half @src_uiui_sub_i16(i16 noundef %x, i16 noundef %y) {
#0:
  %x_okay = icmp ule i16 noundef %x, 2048
  assume i1 %x_okay
  %y_okay = icmp ule i16 noundef %y, 2048
  assume i1 %y_okay
  %xf = uitofp i16 noundef %x to half
  %yf = uitofp i16 noundef %y to half
  %r = fsub half %xf, %yf
  ret half %r
}
=>
define half @tgt_uiui_sub_i16(i16 noundef %x, i16 noundef %y) {
#0:
  %x_okay = icmp ule i16 noundef %x, 2048
  assume i1 %x_okay
  %y_okay = icmp ule i16 noundef %y, 2048
  assume i1 %y_okay
  %xy = sub i16 noundef %x, noundef %y
  %r = sitofp i16 %xy to half
  ret half %r
}
Transformation seems to be correct!


----------------------------------------
define half @src_sisi_mul_i16(i16 noundef %x, i16 noundef %y) {
#0:
  %x_high_zeros = icmp ule i16 noundef %x, 2048
  %x_high_ones = icmp uge i16 noundef %x, 63488
  %x_non_zero = icmp ne i16 noundef %x, 0
  %x_okay0 = or i1 %x_high_zeros, %x_high_ones
  %x_okay = and i1 %x_okay0, %x_non_zero
  assume i1 %x_okay
  %y_high_zeros = icmp ule i16 noundef %y, 2048
  %y_high_ones = icmp uge i16 noundef %y, 63488
  %y_non_zero = icmp ne i16 noundef %y, 0
  %y_okay0 = or i1 %y_high_zeros, %y_high_ones
  %y_okay = and i1 %y_okay0, %y_non_zero
  assume i1 %y_okay
  %overflow_info = smul_overflow i16 noundef %x, noundef %y
  %does_overflow = extractvalue {i16, i1, i8} %overflow_info, 1
  %doesnot_overflow = xor i1 %does_overflow, 1
  assume i1 %doesnot_overflow
  %xf = sitofp i16 noundef %x to half
  %yf = sitofp i16 noundef %y to half
  %r = fmul half %xf, %yf
  ret half %r
}
=>
define half @tgt_sisi_mul_i16(i16 noundef %x, i16 noundef %y) {
#0:
  %x_high_zeros = icmp ule i16 noundef %x, 2048
  %x_high_ones = icmp uge i16 noundef %x, 63488
  %x_non_zero = icmp ne i16 noundef %x, 0
  %x_okay0 = or i1 %x_high_zeros, %x_high_ones
  %x_okay = and i1 %x_okay0, %x_non_zero
  assume i1 %x_okay
  %y_high_zeros = icmp ule i16 noundef %y, 2048
  %y_high_ones = icmp uge i16 noundef %y, 63488
  %y_non_zero = icmp ne i16 noundef %y, 0
  %y_okay0 = or i1 %y_high_zeros, %y_high_ones
  %y_okay = and i1 %y_okay0, %y_non_zero
  assume i1 %y_okay
  %overflow_info = smul_overflow i16 noundef %x, noundef %y
  %does_overflow = extractvalue {i16, i1, i8} %overflow_info, 1
  %doesnot_overflow = xor i1 %does_overflow, 1
  assume i1 %doesnot_overflow
  %xy = mul i16 noundef %x, noundef %y
  %r = sitofp i16 %xy to half
  ret half %r
}
Transformation seems to be correct!


----------------------------------------
define half @src_uiui_mul_i16(i16 noundef %x, i16 noundef %y) {
#0:
  %x_okay = icmp ule i16 noundef %x, 2048
  assume i1 %x_okay
  %y_okay = icmp ule i16 noundef %y, 2048
  assume i1 %y_okay
  %overflow_info = umul_overflow i16 noundef %x, noundef %y
  %does_overflow = extractvalue {i16, i1, i8} %overflow_info, 1
  %doesnot_overflow = xor i1 %does_overflow, 1
  assume i1 %doesnot_overflow
  %xf = uitofp i16 noundef %x to half
  %yf = uitofp i16 noundef %y to half
  %r = fmul half %xf, %yf
  ret half %r
}
=>
define half @tgt_uiui_mul_i16(i16 noundef %x, i16 noundef %y) {
#0:
  %x_okay = icmp ule i16 noundef %x, 2048
  assume i1 %x_okay
  %y_okay = icmp ule i16 noundef %y, 2048
  assume i1 %y_okay
  %overflow_info = umul_overflow i16 noundef %x, noundef %y
  %does_overflow = extractvalue {i16, i1, i8} %overflow_info, 1
  %doesnot_overflow = xor i1 %does_overflow, 1
  assume i1 %doesnot_overflow
  %xy = mul i16 noundef %x, noundef %y
  %r = uitofp i16 %xy to half
  ret half %r
}
Transformation seems to be correct!

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

```

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