Test Failure: Transforms/InstCombine/minmax-fp.ll

Test source: git

Comments: LLVM PR50281

Log:

Source: <stdin>

----------------------------------------
define double @t1(float %a) {
%0:
  %1 = fcmp ult float %a, 5.000000
  %2 = select i1 %1, float %a, float 5.000000
  %3 = fpext float %2 to double
  ret double %3
}
=>
define double @t1(float %a) {
%0:
  %.inv = fcmp oge float %a, 5.000000
  %1 = select i1 %.inv, float 5.000000, float %a
  %2 = fpext float %1 to double
  ret double %2
}
Transformation seems to be correct!


----------------------------------------
define double @t2(float %a) {
%0:
  %1 = fcmp ult float %a, 5.000000
  %2 = fpext float %a to double
  %3 = select i1 %1, double %2, double 5.000000
  ret double %3
}
=>
define double @t2(float %a) {
%0:
  %.inv = fcmp oge float %a, 5.000000
  %1 = select i1 %.inv, float 5.000000, float %a
  %2 = fpext float %1 to double
  ret double %2
}
Transformation seems to be correct!


----------------------------------------
define float @t4(double %a) {
%0:
  %1 = fcmp ult double %a, 5.000000
  %2 = fptrunc double %a to float
  %3 = select i1 %1, float %2, float 5.000000
  ret float %3
}
=>
define float @t4(double %a) {
%0:
  %.inv = fcmp oge double %a, 5.000000
  %1 = select i1 %.inv, double 5.000000, double %a
  %2 = fptrunc double %1 to float
  ret float %2
}
Transformation doesn't verify!
ERROR: Timeout


----------------------------------------
define double @t5(float %a) {
%0:
  %1 = fcmp ult float %a, 5.000000
  %2 = fpext float %a to double
  %3 = select i1 %1, double %2, double 5.001000
  ret double %3
}
=>
define double @t5(float %a) {
%0:
  %1 = fcmp ult float %a, 5.000000
  %2 = fpext float %a to double
  %3 = select i1 %1, double %2, double 5.001000
  ret double %3
}
Transformation seems to be correct! (syntactically equal)


----------------------------------------
define double @t6(float %a) {
%0:
  %1 = fcmp ult float %a, -0.000000
  %2 = fpext float %a to double
  %3 = select i1 %1, double %2, double 0.000000
  ret double %3
}
=>
define double @t6(float %a) {
%0:
  %.inv = fcmp oge float %a, 0.000000
  %1 = select i1 %.inv, float 0.000000, float %a
  %2 = fpext float %1 to double
  ret double %2
}
Transformation seems to be correct!


----------------------------------------
define double @t7(float %a) {
%0:
  %1 = fcmp ult float %a, 0.000000
  %2 = fpext float %a to double
  %3 = select i1 %1, double %2, double -0.000000
  ret double %3
}
=>
define double @t7(float %a) {
%0:
  %.inv = fcmp oge float %a, 0.000000
  %1 = select i1 %.inv, float -0.000000, float %a
  %2 = fpext float %1 to double
  ret double %2
}
Transformation seems to be correct!


----------------------------------------
define float @fmin_fmin_zero_mismatch(float %x) {
%0:
  %cmp1 = fcmp olt float %x, -0.000000
  %min1 = select i1 %cmp1, float %x, float 0.000000
  %cmp2 = fcmp olt float %min1, 0.000000
  %min2 = select i1 %cmp2, float %min1, float 0.000000
  ret float %min2
}
=>
define float @fmin_fmin_zero_mismatch(float %x) {
%0:
  %1 = fcmp olt float %x, 0.000000
  %min2 = select i1 %1, float %x, float 0.000000
  ret float %min2
}
Transformation seems to be correct!


----------------------------------------
define float @fmax_fmax_zero_mismatch(float %x) {
%0:
  %cmp1 = fcmp ogt float %x, 0.000000
  %max1 = select i1 %cmp1, float %x, float -0.000000
  %cmp2 = fcmp ogt float 0.000000, %max1
  %max2 = select i1 %cmp2, float -0.000000, float %max1
  ret float %max2
}
=>
define float @fmax_fmax_zero_mismatch(float %x) {
%0:
  %1 = fcmp ogt float %x, -0.000000
  %max11 = select i1 %1, float %x, float -0.000000
  ret float %max11
}
Transformation seems to be correct!


----------------------------------------
define i64 @t8(float %a) {
%0:
  %1 = fcmp ult float %a, 5.000000
  %2 = fptoui float %a to i64
  %3 = select i1 %1, i64 %2, i64 5
  ret i64 %3
}
=>
define i64 @t8(float %a) {
%0:
  %.inv = fcmp oge float %a, 5.000000
  %1 = select i1 %.inv, float 5.000000, float %a
  %2 = fptoui float %1 to i64
  ret i64 %2
}
Transformation seems to be correct!


----------------------------------------
define i8 @t9(float %a) {
%0:
  %1 = fcmp ult float %a, 0.000000
  %2 = fptosi float %a to i8
  %3 = select i1 %1, i8 %2, i8 0
  ret i8 %3
}
=>
define i8 @t9(float %a) {
%0:
  %.inv = fcmp oge float %a, 0.000000
  %1 = select i1 %.inv, float 0.000000, float %a
  %2 = fptosi float %1 to i8
  ret i8 %2
}
Transformation seems to be correct!


----------------------------------------
define i8 @t11(float %a, float %b) {
%0:
  %1 = fcmp fast ult float %b, %a
  %2 = fptosi float %a to i8
  %3 = fptosi float %b to i8
  %4 = select i1 %1, i8 %3, i8 %2
  ret i8 %4
}
=>
define i8 @t11(float %a, float %b) {
%0:
  %.inv = fcmp fast oge float %b, %a
  %1 = select fast i1 %.inv, float %a, float %b
  %2 = fptosi float %1 to i8
  ret i8 %2
}
Transformation doesn't verify!
ERROR: Couldn't prove the correctness of the transformation
Alive2 approximated the semantics of the programs and therefore we
cannot conclude whether the bug found is valid or not.

Approximations done:
 - afn
 - arcp
 - contract
 - reassoc



----------------------------------------
define i8 @t12(float %a, float %b) {
%0:
  %1 = fcmp nnan ult float %b, %a
  %2 = fptosi float %a to i8
  %3 = fptosi float %b to i8
  %4 = select i1 %1, i8 %3, i8 %2
  ret i8 %4
}
=>
define i8 @t12(float %a, float %b) {
%0:
  %.inv = fcmp nnan oge float %b, %a
  %1 = select nnan i1 %.inv, float %a, float %b
  %2 = fptosi float %1 to i8
  ret i8 %2
}
Transformation seems to be correct!


----------------------------------------
define i8 @t13(float %a) {
%0:
  %1 = fcmp ult float %a, 1.500000
  %2 = fptosi float %a to i8
  %3 = select i1 %1, i8 %2, i8 1
  ret i8 %3
}
=>
define i8 @t13(float %a) {
%0:
  %1 = fcmp ult float %a, 1.500000
  %2 = fptosi float %a to i8
  %3 = select i1 %1, i8 %2, i8 1
  ret i8 %3
}
Transformation seems to be correct! (syntactically equal)


----------------------------------------
define i8 @t14(float %a) {
%0:
  %1 = fcmp ule float %a, 0.000000
  %2 = fptosi float %a to i8
  %3 = select i1 %1, i8 %2, i8 0
  ret i8 %3
}
=>
define i8 @t14(float %a) {
%0:
  %.inv = fcmp oge float %a, 0.000000
  %1 = select i1 %.inv, float 0.000000, float %a
  %2 = fptosi float %1 to i8
  ret i8 %2
}
Transformation seems to be correct!


----------------------------------------
define i8 @t14_commute(float %a) {
%0:
  %1 = fcmp ule float %a, 0.000000
  %2 = fptosi float %a to i8
  %3 = select i1 %1, i8 0, i8 %2
  ret i8 %3
}
=>
define i8 @t14_commute(float %a) {
%0:
  %1 = fcmp ogt float %a, 0.000000
  %2 = select i1 %1, float %a, float 0.000000
  %3 = fptosi float %2 to i8
  ret i8 %3
}
Transformation seems to be correct!


----------------------------------------
define i8 @t15(float %a) {
%0:
  %1 = fcmp nsz ule float %a, 0.000000
  %2 = fptosi float %a to i8
  %3 = select i1 %1, i8 %2, i8 0
  ret i8 %3
}
=>
define i8 @t15(float %a) {
%0:
  %.inv = fcmp nsz oge float %a, 0.000000
  %1 = select nsz i1 %.inv, float 0.000000, float %a
  %2 = fptosi float %1 to i8
  ret i8 %2
}
Transformation seems to be correct!


----------------------------------------
define double @t16(i32 %x) {
%0:
  %cmp = icmp sgt i32 %x, 0
  %cst = sitofp i32 %x to double
  %sel = select i1 %cmp, double %cst, double 0.500000
  ret double %sel
}
=>
define double @t16(i32 %x) {
%0:
  %cmp = icmp sgt i32 %x, 0
  %cst = sitofp i32 %x to double
  %sel = select i1 %cmp, double %cst, double 0.500000
  ret double %sel
}
Transformation seems to be correct! (syntactically equal)


----------------------------------------
define double @t17(i32 %x) {
%0:
  %cmp = icmp sgt i32 %x, 2
  %cst = sitofp i32 %x to double
  %sel = select i1 %cmp, double %cst, double 2.000000
  ret double %sel
}
=>
define double @t17(i32 %x) {
%0:
  %1 = icmp sgt i32 %x, 2
  %sel1 = select i1 %1, i32 %x, i32 2
  %2 = sitofp i32 %sel1 to double
  ret double %2
}
Transformation seems to be correct!


----------------------------------------
define float @fneg_fmax(float %x, float %y) {
%0:
  %n1 = fneg float %x
  %n2 = fneg float %y
  %cond = fcmp nnan ogt float %n1, %n2
  %max = select i1 %cond, float %n1, float %n2
  ret float %max
}
=>
define float @fneg_fmax(float %x, float %y) {
%0:
  %cond = fcmp nnan olt float %x, %y
  %max.v = select i1 %cond, float %x, float %y
  %max = fneg float %max.v
  ret float %max
}
Transformation seems to be correct!


----------------------------------------
define <2 x float> @fsub_fmax(<2 x float> %x, <2 x float> %y) {
%0:
  %n1 = fsub <2 x float> { -0.000000, -0.000000 }, %x
  %n2 = fsub <2 x float> { -0.000000, -0.000000 }, %y
  %cond = fcmp nnan nsz uge <2 x float> %n1, %n2
  %max = select <2 x i1> %cond, <2 x float> %n1, <2 x float> %n2
  ret <2 x float> %max
}
=>
define <2 x float> @fsub_fmax(<2 x float> %x, <2 x float> %y) {
%0:
  %cond.inv = fcmp nnan nsz ogt <2 x float> %x, %y
  %1 = select nnan nsz <2 x i1> %cond.inv, <2 x float> %y, <2 x float> %x
  %max = fneg <2 x float> %1
  ret <2 x float> %max
}
Transformation doesn't verify!
ERROR: Timeout


----------------------------------------
define <2 x double> @fsub_fmin(<2 x double> %x, <2 x double> %y) {
%0:
  %n1 = fsub <2 x double> { -0.000000, -0.000000 }, %x
  %n2 = fsub <2 x double> { -0.000000, -0.000000 }, %y
  %cond = fcmp nnan olt <2 x double> %n1, %n2
  %max = select <2 x i1> %cond, <2 x double> %n1, <2 x double> %n2
  ret <2 x double> %max
}
=>
define <2 x double> @fsub_fmin(<2 x double> %x, <2 x double> %y) {
%0:
  %cond = fcmp nnan ogt <2 x double> %x, %y
  %max.v = select <2 x i1> %cond, <2 x double> %x, <2 x double> %y
  %max = fneg <2 x double> %max.v
  ret <2 x double> %max
}
Transformation doesn't verify!
ERROR: Timeout


----------------------------------------
define double @fneg_fmin(double %x, double %y) {
%0:
  %n1 = fneg double %x
  %n2 = fneg double %y
  %cond = fcmp nnan nsz ule double %n1, %n2
  %max = select i1 %cond, double %n1, double %n2
  ret double %max
}
=>
define double @fneg_fmin(double %x, double %y) {
%0:
  %cond.inv = fcmp nnan nsz olt double %x, %y
  %1 = select nnan nsz i1 %cond.inv, double %y, double %x
  %max = fneg double %1
  ret double %max
}
Transformation doesn't verify!
ERROR: Value mismatch

Example:
double %x = #x0000000000000000 (+0.0)
double %y = #x8010000471e0b245 (-0.000000000000?)

Source:
double %n1 = #x8000000000000000 (-0.0)
double %n2 = #x0010000471e0b245 (0.000000000000?)
i1 %cond = #x1 (1)
double %max = #x8000000000000000 (-0.0)

Target:
i1 %cond.inv = #x0 (0)
double %1 = #x8000000000000000 (-0.0)
double %max = #x0000000000000000 (+0.0)
Source value: #x8000000000000000 (-0.0)
Target value: #x0000000000000000 (+0.0)


------------------- SMT STATS -------------------
Num queries: 72
Num invalid: 0
Num skips:   0
Num trivial: 63 (46.7%)
Num timeout: 3 (4.2%)
Num errors:  0 (0.0%)
Num SAT:     22 (30.6%)
Num UNSAT:   47 (65.3%)
Alive2: Transform doesn't verify; aborting!

stderr:

+ : 'RUN: at line 2'
+ /home/nlopes/alive2/build/opt-alive.sh -S -instcombine
+ /home/nlopes/llvm/build/bin/FileCheck /home/nlopes/llvm/llvm/test/Transforms/InstCombine/minmax-fp.ll

FileCheck error: '<stdin>' is empty.
FileCheck command line:  /home/nlopes/llvm/build/bin/FileCheck /home/nlopes/llvm/llvm/test/Transforms/InstCombine/minmax-fp.ll

 

<-- Back