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

Test source: git

Comments: LLVM PR50281

Log:

Source: <stdin>
-- 1. ModuleToFunctionPassAdaptor
-- 1. PassManager<llvm::Function> : Skipping NOP
-- 2. InstCombinePass

----------------------------------------
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
}
Transformation seems to be correct! (syntactically equal)

-- 3. InstCombinePass

----------------------------------------
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!

-- 4. PassManager<llvm::Function> : Skipping NOP
-- 5. PassManager<llvm::Function> : Skipping NOP
-- 6. InstCombinePass

----------------------------------------
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
}
Transformation seems to be correct! (syntactically equal)

-- 7. InstCombinePass

----------------------------------------
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!

-- 8. PassManager<llvm::Function> : Skipping NOP
-- 9. PassManager<llvm::Function> : Skipping NOP
-- 10. InstCombinePass

----------------------------------------
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
}
Transformation seems to be correct! (syntactically equal)

-- 11. InstCombinePass

----------------------------------------
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! (not unsound)
ERROR: Timeout
-- 12. PassManager<llvm::Function> : Skipping NOP
-- 13. PassManager<llvm::Function> : Skipping NOP
-- 14. InstCombinePass

----------------------------------------
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)

-- 15. InstCombinePass

----------------------------------------
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)

-- 16. PassManager<llvm::Function> : Skipping NOP
-- 17. PassManager<llvm::Function> : Skipping NOP
-- 18. InstCombinePass

----------------------------------------
define float @not_maxnum(float %x) {
#0:
  %cmp = fcmp olt float %x, 0.000000
  %sel = select i1 %cmp, float -0.000000, float %x
  ret float %sel
}
Transformation seems to be correct! (syntactically equal)

-- 19. InstCombinePass

----------------------------------------
define float @not_maxnum(float %x) {
#0:
  %cmp = fcmp olt float %x, 0.000000
  %sel = select i1 %cmp, float -0.000000, float %x
  ret float %sel
}
Transformation seems to be correct! (syntactically equal)

-- 20. PassManager<llvm::Function> : Skipping NOP
-- 21. PassManager<llvm::Function> : Skipping NOP
-- 22. InstCombinePass

----------------------------------------
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
}
Transformation seems to be correct! (syntactically equal)

-- 23. InstCombinePass

----------------------------------------
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!

-- 24. PassManager<llvm::Function> : Skipping NOP
-- 25. PassManager<llvm::Function> : Skipping NOP
-- 26. InstCombinePass

----------------------------------------
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
}
Transformation seems to be correct! (syntactically equal)

-- 27. InstCombinePass

----------------------------------------
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
}
Transformation seems to be correct! (syntactically equal)

-- 28. PassManager<llvm::Function> : Skipping NOP
-- 29. PassManager<llvm::Function> : Skipping NOP
-- 30. InstCombinePass

----------------------------------------
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
}
Transformation seems to be correct! (syntactically equal)

-- 31. InstCombinePass

----------------------------------------
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:
  %cmp1 = fcmp olt float %x, 0.000000
  %min2 = select i1 %cmp1, float %x, float 0.000000
  ret float %min2
}
Transformation seems to be correct!

-- 32. PassManager<llvm::Function> : Skipping NOP
-- 33. PassManager<llvm::Function> : Skipping NOP
-- 34. InstCombinePass

----------------------------------------
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
}
Transformation seems to be correct! (syntactically equal)

-- 35. InstCombinePass

----------------------------------------
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:
  %cmp1 = fcmp ogt float %x, 0.000000
  %max1 = select i1 %cmp1, float %x, float -0.000000
  ret float %max1
}
Transformation seems to be correct!

-- 36. PassManager<llvm::Function> : Skipping NOP
-- 37. PassManager<llvm::Function> : Skipping NOP
-- 38. InstCombinePass

----------------------------------------
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
}
Transformation seems to be correct! (syntactically equal)

-- 39. InstCombinePass

----------------------------------------
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!

-- 40. PassManager<llvm::Function> : Skipping NOP
-- 41. PassManager<llvm::Function> : Skipping NOP
-- 42. InstCombinePass

----------------------------------------
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
}
Transformation seems to be correct! (syntactically equal)

-- 43. InstCombinePass

----------------------------------------
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!

-- 44. PassManager<llvm::Function> : Skipping NOP
-- 45. PassManager<llvm::Function> : Skipping NOP
-- 46. InstCombinePass

----------------------------------------
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
}
Transformation seems to be correct! (syntactically equal)

-- 47. InstCombinePass

----------------------------------------
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:
  %.v = fmin fast float %b, %a
  %#1 = fptosi float %.v to i8
  ret i8 %#1
}
Transformation doesn't verify! (not unsound)
ERROR: SMT Error: smt tactic failed to show goal to be sat/unsat (incomplete quantifiers)
-- 48. PassManager<llvm::Function> : Skipping NOP
-- 49. PassManager<llvm::Function> : Skipping NOP
-- 50. InstCombinePass

----------------------------------------
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
}
Transformation seems to be correct! (syntactically equal)

-- 51. InstCombinePass

----------------------------------------
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
  %.v = select nnan i1 %.inv, float %a, float %b
  %#1 = fptosi float %.v to i8
  ret i8 %#1
}
Transformation seems to be correct!

-- 52. PassManager<llvm::Function> : Skipping NOP
-- 53. PassManager<llvm::Function> : Skipping NOP
-- 54. InstCombinePass

----------------------------------------
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)

-- 55. InstCombinePass

----------------------------------------
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)

-- 56. PassManager<llvm::Function> : Skipping NOP
-- 57. PassManager<llvm::Function> : Skipping NOP
-- 58. InstCombinePass

----------------------------------------
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
}
Transformation seems to be correct! (syntactically equal)

-- 59. InstCombinePass

----------------------------------------
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!

-- 60. PassManager<llvm::Function> : Skipping NOP
-- 61. PassManager<llvm::Function> : Skipping NOP
-- 62. InstCombinePass

----------------------------------------
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
}
Transformation seems to be correct! (syntactically equal)

-- 63. InstCombinePass

----------------------------------------
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!

-- 64. PassManager<llvm::Function> : Skipping NOP
-- 65. PassManager<llvm::Function> : Skipping NOP
-- 66. InstCombinePass

----------------------------------------
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
}
Transformation seems to be correct! (syntactically equal)

-- 67. InstCombinePass

----------------------------------------
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!

-- 68. PassManager<llvm::Function> : Skipping NOP
-- 69. PassManager<llvm::Function> : Skipping NOP
-- 70. InstCombinePass

----------------------------------------
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)

-- 71. InstCombinePass

----------------------------------------
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)

-- 72. PassManager<llvm::Function> : Skipping NOP
-- 73. PassManager<llvm::Function> : Skipping NOP
-- 74. InstCombinePass

----------------------------------------
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
}
Transformation seems to be correct! (syntactically equal)

-- 75. InstCombinePass

----------------------------------------
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:
  %sel1 = smax i32 %x, 2
  %sel = uitofp nneg i32 %sel1 to double
  ret double %sel
}
Transformation doesn't verify! (not unsound)
ERROR: Timeout
-- 76. PassManager<llvm::Function> : Skipping NOP
-- 77. PassManager<llvm::Function> : Skipping NOP
-- 78. InstCombinePass

----------------------------------------
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
}
Transformation seems to be correct! (syntactically equal)

-- 79. InstCombinePass

----------------------------------------
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!

-- 80. PassManager<llvm::Function> : Skipping NOP
-- 81. PassManager<llvm::Function> : Skipping NOP
-- 82. InstCombinePass

----------------------------------------
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
}
Transformation seems to be correct! (syntactically equal)

-- 83. InstCombinePass

----------------------------------------
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:
  %max.v = fmin nnan nsz <2 x float> %x, %y
  %max = fneg <2 x float> %max.v
  ret <2 x float> %max
}
Transformation doesn't verify! (unsound)
ERROR: Target's return value is more undefined

Example:
<2 x float> %x = < #x80000000 (-0.0), #x7f880000 (SNaN) >
<2 x float> %y = < #x00000000 (+0.0), #x7f808000 (SNaN) >

Source:
<2 x float> %n1 = < #x00000000 (+0.0), #xffc80000 (QNaN) >
<2 x float> %n2 = < #x80000000 (-0.0), #xffc08000 (QNaN) >
<2 x i1> %cond = < #x1 (1), poison >
<2 x float> %max = < #x00000000 (+0.0), poison >

Target:
<2 x float> %max.v = < #x80000000 (-0.0), poison >
<2 x float> %max = < #x00000000 (+0.0), poison >
Source value: < #x00000000 (+0.0), poison >
Target value: < #x00000000 (+0.0), poison >

Pass: InstCombinePass
Command line: '/home/nlopes/llvm/build/bin/opt' '-load=/home/nlopes/alive2/build/tv/tv.so' '-load-pass-plugin=/home/nlopes/alive2/build/tv/tv.so' '-tv-exit-on-error' '-S' '-passes=instcombine' '-tv-smt-to=20000' '-tv-report-dir=/home/nlopes/alive2/build/logs' '-tv-smt-stats'
Wrote bitcode to: "/home/nlopes/alive2/build/logs/in_gOdtP4zt_W8F6.bc"


------------------- SMT STATS -------------------
Num queries: 132
Num invalid: 0
Num skips:   0
Num trivial: 55 (29.4%)
Num timeout: 2 (1.5%)
Num errors:  1 (0.8%)
Num SAT:     71 (53.8%)
Num UNSAT:   58 (43.9%)
Alive2: Transform doesn't verify; aborting!

stderr:

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

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

<-- Back