Test Failure: Transforms/InstSimplify/known-never-nan.ll

Test source: git

Log:

Source: <stdin>
-- 1. ModuleToFunctionPassAdaptor
ERROR: Unsupported attribute: nofpclass(nan)
ERROR: Unsupported attribute: nofpclass(qnan)
ERROR: Unsupported attribute: nofpclass(snan)
ERROR: Unsupported attribute: nofpclass(zero)
ERROR: Unsupported instruction:   %call = call nofpclass(nan) double %fptr()
ERROR: Unsupported instruction:   %invoke = invoke nofpclass(nan) float %ptr()
          to label %normal unwind
-- 1. PassManager<Function> : Skipping NOP
-- 2. InstSimplifyPass

----------------------------------------
define i1 @nnan_call() {
%0:
  %op = call double @func() NNaN
  %tmp = fcmp ord double %op, %op
  ret i1 %tmp
}
Transformation seems to be correct! (syntactically equal)

-- 3. InstSimplifyPass

----------------------------------------
define i1 @nnan_call() {
%0:
  %op = call double @func() NNaN
  %tmp = fcmp ord double %op, %op
  ret i1 %tmp
}
=>
define i1 @nnan_call() {
%0:
  %op = call double @func() NNaN
  ret i1 1
}
Transformation seems to be correct!

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

----------------------------------------
define i1 @nnan_fabs_src(double %arg) {
%0:
  %nnan = fadd nnan double %arg, 1.000000
  %op = fabs double %nnan
  %tmp = fcmp uno double %op, %op
  ret i1 %tmp
}
Transformation seems to be correct! (syntactically equal)

-- 7. InstSimplifyPass

----------------------------------------
define i1 @nnan_fabs_src(double %arg) {
%0:
  %nnan = fadd nnan double %arg, 1.000000
  %op = fabs double %nnan
  %tmp = fcmp uno double %op, %op
  ret i1 %tmp
}
=>
define i1 @nnan_fabs_src(double %arg) {
%0:
  ret i1 0
}
Transformation seems to be correct!

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

----------------------------------------
define i1 @nnan_canonicalize_src(double %arg) {
%0:
  %nnan = fadd nnan double %arg, 1.000000
  %op = canonicalize double %nnan
  %tmp = fcmp ord double %op, %op
  ret i1 %tmp
}
Transformation seems to be correct! (syntactically equal)

-- 11. InstSimplifyPass

----------------------------------------
define i1 @nnan_canonicalize_src(double %arg) {
%0:
  %nnan = fadd nnan double %arg, 1.000000
  %op = canonicalize double %nnan
  %tmp = fcmp ord double %op, %op
  ret i1 %tmp
}
=>
define i1 @nnan_canonicalize_src(double %arg) {
%0:
  ret i1 1
}
Transformation seems to be correct!

-- 12. PassManager<Function> : Skipping NOP
-- 13. PassManager<Function> : Skipping NOP
-- 14. InstSimplifyPass

----------------------------------------
define i1 @nnan_copysign_src(double %arg0, double %arg1) {
%0:
  %nnan = fadd nnan double %arg0, 1.000000
  %op = copysign double %nnan, %arg1
  %tmp = fcmp uno double %op, %op
  ret i1 %tmp
}
Transformation seems to be correct! (syntactically equal)

-- 15. InstSimplifyPass

----------------------------------------
define i1 @nnan_copysign_src(double %arg0, double %arg1) {
%0:
  %nnan = fadd nnan double %arg0, 1.000000
  %op = copysign double %nnan, %arg1
  %tmp = fcmp uno double %op, %op
  ret i1 %tmp
}
=>
define i1 @nnan_copysign_src(double %arg0, double %arg1) {
%0:
  ret i1 0
}
Transformation seems to be correct!

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

----------------------------------------
define i1 @fabs_sqrt_src(double %arg0, double %arg1) {
%0:
  %nnan = fadd nnan double %arg0, 1.000000
  %fabs = fabs double %nnan
  %op = sqrt double %fabs
  %tmp = fcmp ord double %op, %op
  ret i1 %tmp
}
Transformation seems to be correct! (syntactically equal)

-- 19. InstSimplifyPass

----------------------------------------
define i1 @fabs_sqrt_src(double %arg0, double %arg1) {
%0:
  %nnan = fadd nnan double %arg0, 1.000000
  %fabs = fabs double %nnan
  %op = sqrt double %fabs
  %tmp = fcmp ord double %op, %op
  ret i1 %tmp
}
=>
define i1 @fabs_sqrt_src(double %arg0, double %arg1) {
%0:
  ret i1 1
}
Transformation doesn't verify! (not unsound)
ERROR: Timeout
-- 20. PassManager<Function> : Skipping NOP
-- 21. PassManager<Function> : Skipping NOP
-- 22. InstSimplifyPass

----------------------------------------
define i1 @fabs_sqrt_src_maybe_nan(double %arg0, double %arg1) {
%0:
  %fabs = fabs double %arg0
  %op = sqrt double %fabs
  %tmp = fcmp uno double %op, %op
  ret i1 %tmp
}
Transformation seems to be correct! (syntactically equal)

-- 23. InstSimplifyPass

----------------------------------------
define i1 @fabs_sqrt_src_maybe_nan(double %arg0, double %arg1) {
%0:
  %fabs = fabs double %arg0
  %op = sqrt double %fabs
  %tmp = fcmp uno double %op, %op
  ret i1 %tmp
}
Transformation seems to be correct! (syntactically equal)

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

----------------------------------------
define i1 @exp_nnan_src(double %arg) {
%0:
  %nnan = fadd nnan double %arg, 1.000000
  %op = call double @llvm.exp.f64(double %nnan) nofree willreturn memory(none)
  %tmp = fcmp ord double %op, %op
  ret i1 %tmp
}
Transformation seems to be correct! (syntactically equal)

-- 27. InstSimplifyPass

----------------------------------------
define i1 @exp_nnan_src(double %arg) {
%0:
  %nnan = fadd nnan double %arg, 1.000000
  %op = call double @llvm.exp.f64(double %nnan) nofree willreturn memory(none)
  %tmp = fcmp ord double %op, %op
  ret i1 %tmp
}
=>
define i1 @exp_nnan_src(double %arg) {
%0:
  ret i1 1
}
Transformation doesn't verify! (not unsound)
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:
 - Unknown libcall: @llvm.exp.f64

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

----------------------------------------
define i1 @exp2_nnan_src(double %arg) {
%0:
  %nnan = fadd nnan double %arg, 1.000000
  %op = call double @llvm.exp2.f64(double %nnan) nofree willreturn memory(none)
  %tmp = fcmp uno double %op, %op
  ret i1 %tmp
}
Transformation seems to be correct! (syntactically equal)

-- 31. InstSimplifyPass

----------------------------------------
define i1 @exp2_nnan_src(double %arg) {
%0:
  %nnan = fadd nnan double %arg, 1.000000
  %op = call double @llvm.exp2.f64(double %nnan) nofree willreturn memory(none)
  %tmp = fcmp uno double %op, %op
  ret i1 %tmp
}
=>
define i1 @exp2_nnan_src(double %arg) {
%0:
  ret i1 0
}
Transformation doesn't verify! (not unsound)
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:
 - Unknown libcall: @llvm.exp2.f64

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

----------------------------------------
define i1 @floor_nnan_src(double %arg) {
%0:
  %nnan = fadd nnan double %arg, 1.000000
  %op = floor double %nnan
  %tmp = fcmp ord double %op, %op
  ret i1 %tmp
}
Transformation seems to be correct! (syntactically equal)

-- 35. InstSimplifyPass

----------------------------------------
define i1 @floor_nnan_src(double %arg) {
%0:
  %nnan = fadd nnan double %arg, 1.000000
  %op = floor double %nnan
  %tmp = fcmp ord double %op, %op
  ret i1 %tmp
}
=>
define i1 @floor_nnan_src(double %arg) {
%0:
  ret i1 1
}
Transformation seems to be correct!

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

----------------------------------------
define i1 @ceil_nnan_src(double %arg) {
%0:
  %nnan = fadd nnan double %arg, 1.000000
  %op = ceil double %nnan
  %tmp = fcmp uno double %op, %op
  ret i1 %tmp
}
Transformation seems to be correct! (syntactically equal)

-- 39. InstSimplifyPass

----------------------------------------
define i1 @ceil_nnan_src(double %arg) {
%0:
  %nnan = fadd nnan double %arg, 1.000000
  %op = ceil double %nnan
  %tmp = fcmp uno double %op, %op
  ret i1 %tmp
}
=>
define i1 @ceil_nnan_src(double %arg) {
%0:
  ret i1 0
}
Transformation seems to be correct!

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

----------------------------------------
define i1 @trunc_nnan_src(double %arg) {
%0:
  %nnan = fadd nnan double %arg, 1.000000
  %op = trunc double %nnan
  %tmp = fcmp ord double %op, %op
  ret i1 %tmp
}
Transformation seems to be correct! (syntactically equal)

-- 43. InstSimplifyPass

----------------------------------------
define i1 @trunc_nnan_src(double %arg) {
%0:
  %nnan = fadd nnan double %arg, 1.000000
  %op = trunc double %nnan
  %tmp = fcmp ord double %op, %op
  ret i1 %tmp
}
=>
define i1 @trunc_nnan_src(double %arg) {
%0:
  ret i1 1
}
Transformation seems to be correct!

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

----------------------------------------
define i1 @rint_nnan_src(double %arg) {
%0:
  %nnan = fadd nnan double %arg, 1.000000
  %op = rint double %nnan
  %tmp = fcmp uno double %op, %op
  ret i1 %tmp
}
Transformation seems to be correct! (syntactically equal)

-- 47. InstSimplifyPass

----------------------------------------
define i1 @rint_nnan_src(double %arg) {
%0:
  %nnan = fadd nnan double %arg, 1.000000
  %op = rint double %nnan
  %tmp = fcmp uno double %op, %op
  ret i1 %tmp
}
=>
define i1 @rint_nnan_src(double %arg) {
%0:
  ret i1 0
}
Transformation seems to be correct!

-- 48. PassManager<Function> : Skipping NOP
-- 49. PassManager<Function> : Skipping NOP
-- 50. InstSimplifyPass

----------------------------------------
define i1 @nearbyint_nnan_src(double %arg) {
%0:
  %nnan = fadd nnan double %arg, 1.000000
  %op = nearbyint double %nnan
  %tmp = fcmp ord double %op, %op
  ret i1 %tmp
}
Transformation seems to be correct! (syntactically equal)

-- 51. InstSimplifyPass

----------------------------------------
define i1 @nearbyint_nnan_src(double %arg) {
%0:
  %nnan = fadd nnan double %arg, 1.000000
  %op = nearbyint double %nnan
  %tmp = fcmp ord double %op, %op
  ret i1 %tmp
}
=>
define i1 @nearbyint_nnan_src(double %arg) {
%0:
  ret i1 1
}
Transformation seems to be correct!

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

----------------------------------------
define i1 @round_nnan_src(double %arg) {
%0:
  %nnan = fadd nnan double %arg, 1.000000
  %op = round double %nnan
  %tmp = fcmp uno double %op, %op
  ret i1 %tmp
}
Transformation seems to be correct! (syntactically equal)

-- 55. InstSimplifyPass

----------------------------------------
define i1 @round_nnan_src(double %arg) {
%0:
  %nnan = fadd nnan double %arg, 1.000000
  %op = round double %nnan
  %tmp = fcmp uno double %op, %op
  ret i1 %tmp
}
=>
define i1 @round_nnan_src(double %arg) {
%0:
  ret i1 0
}
Transformation seems to be correct!

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

----------------------------------------
define i1 @roundeven_nnan_src(double %arg) {
%0:
  %nnan = fadd nnan double %arg, 1.000000
  %op = roundeven double %nnan
  %tmp = fcmp uno double %op, %op
  ret i1 %tmp
}
Transformation seems to be correct! (syntactically equal)

-- 59. InstSimplifyPass

----------------------------------------
define i1 @roundeven_nnan_src(double %arg) {
%0:
  %nnan = fadd nnan double %arg, 1.000000
  %op = roundeven double %nnan
  %tmp = fcmp uno double %op, %op
  ret i1 %tmp
}
=>
define i1 @roundeven_nnan_src(double %arg) {
%0:
  ret i1 0
}
Transformation seems to be correct!

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

----------------------------------------
define i1 @known_nan_select(i1 %cond, double %arg0, double %arg1) {
%0:
  %lhs = fadd nnan double %arg0, 1.000000
  %rhs = fadd nnan double %arg1, 2.000000
  %op = select i1 %cond, double %lhs, double %rhs
  %tmp = fcmp ord double %op, %op
  ret i1 %tmp
}
Transformation seems to be correct! (syntactically equal)

-- 63. InstSimplifyPass

----------------------------------------
define i1 @known_nan_select(i1 %cond, double %arg0, double %arg1) {
%0:
  %lhs = fadd nnan double %arg0, 1.000000
  %rhs = fadd nnan double %arg1, 2.000000
  %op = select i1 %cond, double %lhs, double %rhs
  %tmp = fcmp ord double %op, %op
  ret i1 %tmp
}
=>
define i1 @known_nan_select(i1 %cond, double %arg0, double %arg1) {
%0:
  ret i1 1
}
Transformation seems to be correct!

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

----------------------------------------
define i1 @nnan_ninf_known_nan_select(i1 %cond, double %arg0, double %arg1) {
%0:
  %lhs = fadd nnan ninf double %arg0, 1.000000
  %rhs = fadd nnan ninf double %arg1, 2.000000
  %op = select i1 %cond, double %lhs, double %rhs
  %mul = fmul double %op, 2.000000
  %tmp = fcmp ord double %mul, %mul
  ret i1 %tmp
}
Transformation seems to be correct! (syntactically equal)

-- 67. InstSimplifyPass

----------------------------------------
define i1 @nnan_ninf_known_nan_select(i1 %cond, double %arg0, double %arg1) {
%0:
  %lhs = fadd nnan ninf double %arg0, 1.000000
  %rhs = fadd nnan ninf double %arg1, 2.000000
  %op = select i1 %cond, double %lhs, double %rhs
  %mul = fmul double %op, 2.000000
  %tmp = fcmp ord double %mul, %mul
  ret i1 %tmp
}
=>
define i1 @nnan_ninf_known_nan_select(i1 %cond, double %arg0, double %arg1) {
%0:
  ret i1 1
}
Transformation doesn't verify! (not unsound)
ERROR: Timeout
-- 68. PassManager<Function> : Skipping NOP
-- 69. PassManager<Function> : Skipping NOP
-- 70. InstSimplifyPass

----------------------------------------
define i1 @select_maybe_nan_lhs(i1 %cond, double %lhs, double %arg1) {
%0:
  %rhs = fadd nnan double %arg1, 1.000000
  %op = select i1 %cond, double %lhs, double %rhs
  %tmp = fcmp uno double %op, %op
  ret i1 %tmp
}
Transformation seems to be correct! (syntactically equal)

-- 71. InstSimplifyPass

----------------------------------------
define i1 @select_maybe_nan_lhs(i1 %cond, double %lhs, double %arg1) {
%0:
  %rhs = fadd nnan double %arg1, 1.000000
  %op = select i1 %cond, double %lhs, double %rhs
  %tmp = fcmp uno double %op, %op
  ret i1 %tmp
}
Transformation seems to be correct! (syntactically equal)

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

----------------------------------------
define i1 @select_maybe_nan_rhs(i1 %cond, double %arg0, double %rhs) {
%0:
  %lhs = fadd nnan double %arg0, 1.000000
  %op = select i1 %cond, double %lhs, double %rhs
  %tmp = fcmp ord double %op, %op
  ret i1 %tmp
}
Transformation seems to be correct! (syntactically equal)

-- 75. InstSimplifyPass

----------------------------------------
define i1 @select_maybe_nan_rhs(i1 %cond, double %arg0, double %rhs) {
%0:
  %lhs = fadd nnan double %arg0, 1.000000
  %op = select i1 %cond, double %lhs, double %rhs
  %tmp = fcmp ord double %op, %op
  ret i1 %tmp
}
Transformation seems to be correct! (syntactically equal)

-- 76. PassManager<Function> : Skipping NOP
-- 77. PassManager<Function> : Skipping NOP
-- 78. InstSimplifyPass

----------------------------------------
define i1 @nnan_fadd(double %arg0, double %arg1) {
%0:
  %nnan.arg0 = fadd nnan double %arg0, 1.000000
  %nnan.arg1 = fadd nnan double %arg0, 2.000000
  %op = fadd double %nnan.arg0, %nnan.arg1
  %tmp = fcmp uno double %op, %op
  ret i1 %tmp
}
Transformation seems to be correct! (syntactically equal)

-- 79. InstSimplifyPass

----------------------------------------
define i1 @nnan_fadd(double %arg0, double %arg1) {
%0:
  %nnan.arg0 = fadd nnan double %arg0, 1.000000
  %nnan.arg1 = fadd nnan double %arg0, 2.000000
  %op = fadd double %nnan.arg0, %nnan.arg1
  %tmp = fcmp uno double %op, %op
  ret i1 %tmp
}
Transformation seems to be correct! (syntactically equal)

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

----------------------------------------
define i1 @nnan_fadd_maybe_nan_lhs(double %arg0, double %arg1) {
%0:
  %nnan.arg1 = fadd nnan double %arg1, 1.000000
  %op = fadd double %arg0, %nnan.arg1
  %tmp = fcmp ord double %op, %op
  ret i1 %tmp
}
Transformation seems to be correct! (syntactically equal)

-- 83. InstSimplifyPass

----------------------------------------
define i1 @nnan_fadd_maybe_nan_lhs(double %arg0, double %arg1) {
%0:
  %nnan.arg1 = fadd nnan double %arg1, 1.000000
  %op = fadd double %arg0, %nnan.arg1
  %tmp = fcmp ord double %op, %op
  ret i1 %tmp
}
Transformation seems to be correct! (syntactically equal)

-- 84. PassManager<Function> : Skipping NOP
-- 85. PassManager<Function> : Skipping NOP
-- 86. InstSimplifyPass

----------------------------------------
define i1 @nnan_fadd_maybe_nan_rhs(double %arg0, double %arg1) {
%0:
  %nnan.arg0 = fadd nnan double %arg0, 1.000000
  %op = fadd double %nnan.arg0, %arg1
  %tmp = fcmp uno double %op, %op
  ret i1 %tmp
}
Transformation seems to be correct! (syntactically equal)

-- 87. InstSimplifyPass

----------------------------------------
define i1 @nnan_fadd_maybe_nan_rhs(double %arg0, double %arg1) {
%0:
  %nnan.arg0 = fadd nnan double %arg0, 1.000000
  %op = fadd double %nnan.arg0, %arg1
  %tmp = fcmp uno double %op, %op
  ret i1 %tmp
}
Transformation seems to be correct! (syntactically equal)

-- 88. PassManager<Function> : Skipping NOP
-- 89. PassManager<Function> : Skipping NOP
-- 90. InstSimplifyPass

----------------------------------------
define i1 @nnan_fmul(double %arg0, double %arg1) {
%0:
  %nnan.arg0 = fadd nnan double %arg0, 1.000000
  %nnan.arg1 = fadd nnan double %arg0, 2.000000
  %op = fmul double %nnan.arg0, %nnan.arg1
  %tmp = fcmp ord double %op, %op
  ret i1 %tmp
}
Transformation seems to be correct! (syntactically equal)

-- 91. InstSimplifyPass

----------------------------------------
define i1 @nnan_fmul(double %arg0, double %arg1) {
%0:
  %nnan.arg0 = fadd nnan double %arg0, 1.000000
  %nnan.arg1 = fadd nnan double %arg0, 2.000000
  %op = fmul double %nnan.arg0, %nnan.arg1
  %tmp = fcmp ord double %op, %op
  ret i1 %tmp
}
Transformation seems to be correct! (syntactically equal)

-- 92. PassManager<Function> : Skipping NOP
-- 93. PassManager<Function> : Skipping NOP
-- 94. InstSimplifyPass

----------------------------------------
define i1 @nnan_fsub(double %arg0, double %arg1) {
%0:
  %nnan.arg0 = fadd nnan double %arg0, 1.000000
  %nnan.arg1 = fadd nnan double %arg0, 2.000000
  %op = fsub double %nnan.arg0, %nnan.arg1
  %tmp = fcmp uno double %op, %op
  ret i1 %tmp
}
Transformation seems to be correct! (syntactically equal)

-- 95. InstSimplifyPass

----------------------------------------
define i1 @nnan_fsub(double %arg0, double %arg1) {
%0:
  %nnan.arg0 = fadd nnan double %arg0, 1.000000
  %nnan.arg1 = fadd nnan double %arg0, 2.000000
  %op = fsub double %nnan.arg0, %nnan.arg1
  %tmp = fcmp uno double %op, %op
  ret i1 %tmp
}
Transformation seems to be correct! (syntactically equal)

-- 96. PassManager<Function> : Skipping NOP
-- 97. PassManager<Function> : Skipping NOP
-- 98. InstSimplifyPass

----------------------------------------
define i1 @nnan_binary_fneg() {
%0:
  %nnan = call double @func() NNaN
  %op = fsub double -0.000000, %nnan
  %tmp = fcmp ord double %op, %op
  ret i1 %tmp
}
Transformation seems to be correct! (syntactically equal)

-- 99. InstSimplifyPass

----------------------------------------
define i1 @nnan_binary_fneg() {
%0:
  %nnan = call double @func() NNaN
  %op = fsub double -0.000000, %nnan
  %tmp = fcmp ord double %op, %op
  ret i1 %tmp
}
=>
define i1 @nnan_binary_fneg() {
%0:
  %nnan = call double @func() NNaN
  ret i1 1
}
Transformation seems to be correct!

-- 100. PassManager<Function> : Skipping NOP
-- 101. PassManager<Function> : Skipping NOP
-- 102. InstSimplifyPass

----------------------------------------
define i1 @nnan_unary_fneg() {
%0:
  %nnan = call double @func() NNaN
  %op = fneg double %nnan
  %tmp = fcmp ord double %op, %op
  ret i1 %tmp
}
Transformation seems to be correct! (syntactically equal)

-- 103. InstSimplifyPass

----------------------------------------
define i1 @nnan_unary_fneg() {
%0:
  %nnan = call double @func() NNaN
  %op = fneg double %nnan
  %tmp = fcmp ord double %op, %op
  ret i1 %tmp
}
=>
define i1 @nnan_unary_fneg() {
%0:
  %nnan = call double @func() NNaN
  ret i1 1
}
Transformation seems to be correct!

-- 104. PassManager<Function> : Skipping NOP
-- 105. PassManager<Function> : Skipping NOP
-- 106. InstSimplifyPass

----------------------------------------
define i1 @isNotKnownNeverNaN_fneg(double %x) {
%0:
  %neg = fneg double %x
  %cmp = fcmp ord double %neg, %neg
  ret i1 %cmp
}
Transformation seems to be correct! (syntactically equal)

-- 107. InstSimplifyPass

----------------------------------------
define i1 @isNotKnownNeverNaN_fneg(double %x) {
%0:
  %neg = fneg double %x
  %cmp = fcmp ord double %neg, %neg
  ret i1 %cmp
}
Transformation seems to be correct! (syntactically equal)

-- 108. PassManager<Function> : Skipping NOP
-- 109. PassManager<Function> : Skipping NOP
-- 110. InstSimplifyPass

----------------------------------------
define i1 @sitofp(i32 %arg0) {
%0:
  %op = sitofp i32 %arg0 to double
  %tmp = fcmp uno double %op, %op
  ret i1 %tmp
}
Transformation seems to be correct! (syntactically equal)

-- 111. InstSimplifyPass

----------------------------------------
define i1 @sitofp(i32 %arg0) {
%0:
  %op = sitofp i32 %arg0 to double
  %tmp = fcmp uno double %op, %op
  ret i1 %tmp
}
=>
define i1 @sitofp(i32 %arg0) {
%0:
  ret i1 0
}
Transformation seems to be correct!

-- 112. PassManager<Function> : Skipping NOP
-- 113. PassManager<Function> : Skipping NOP
-- 114. InstSimplifyPass

----------------------------------------
define i1 @uitofp(i32 %arg0) {
%0:
  %op = uitofp i32 %arg0 to double
  %tmp = fcmp ord double %op, %op
  ret i1 %tmp
}
Transformation seems to be correct! (syntactically equal)

-- 115. InstSimplifyPass

----------------------------------------
define i1 @uitofp(i32 %arg0) {
%0:
  %op = uitofp i32 %arg0 to double
  %tmp = fcmp ord double %op, %op
  ret i1 %tmp
}
=>
define i1 @uitofp(i32 %arg0) {
%0:
  ret i1 1
}
Transformation seems to be correct!

-- 116. PassManager<Function> : Skipping NOP
-- 117. PassManager<Function> : Skipping NOP
-- 118. InstSimplifyPass

----------------------------------------
define i1 @uitofp_add(i32 %arg0) {
%0:
  %op = uitofp i32 %arg0 to double
  %add = fadd double %op, %op
  %tmp = fcmp ord double %add, %add
  ret i1 %tmp
}
Transformation seems to be correct! (syntactically equal)

-- 119. InstSimplifyPass

----------------------------------------
define i1 @uitofp_add(i32 %arg0) {
%0:
  %op = uitofp i32 %arg0 to double
  %add = fadd double %op, %op
  %tmp = fcmp ord double %add, %add
  ret i1 %tmp
}
=>
define i1 @uitofp_add(i32 %arg0) {
%0:
  ret i1 1
}
Transformation seems to be correct!

-- 120. PassManager<Function> : Skipping NOP
-- 121. PassManager<Function> : Skipping NOP
-- 122. InstSimplifyPass

----------------------------------------
define i1 @uitofp_add_big(i1024 %arg0) {
%0:
  %op = uitofp i1024 %arg0 to double
  %add = fadd double %op, %op
  %tmp = fcmp ord double %add, %add
  ret i1 %tmp
}
Transformation seems to be correct! (syntactically equal)

-- 123. InstSimplifyPass

----------------------------------------
define i1 @uitofp_add_big(i1024 %arg0) {
%0:
  %op = uitofp i1024 %arg0 to double
  %add = fadd double %op, %op
  %tmp = fcmp ord double %add, %add
  ret i1 %tmp
}
Transformation seems to be correct! (syntactically equal)

-- 124. PassManager<Function> : Skipping NOP
-- 125. PassManager<Function> : Skipping NOP
-- 126. InstSimplifyPass

----------------------------------------
define i1 @fpext(float %arg0) {
%0:
  %arg0.nnan = fadd nnan float %arg0, 1.000000
  %op = fpext float %arg0.nnan to double
  %tmp = fcmp uno double %op, %op
  ret i1 %tmp
}
Transformation seems to be correct! (syntactically equal)

-- 127. InstSimplifyPass

----------------------------------------
define i1 @fpext(float %arg0) {
%0:
  %arg0.nnan = fadd nnan float %arg0, 1.000000
  %op = fpext float %arg0.nnan to double
  %tmp = fcmp uno double %op, %op
  ret i1 %tmp
}
=>
define i1 @fpext(float %arg0) {
%0:
  ret i1 0
}
Transformation seems to be correct!

-- 128. PassManager<Function> : Skipping NOP
-- 129. PassManager<Function> : Skipping NOP
-- 130. InstSimplifyPass

----------------------------------------
define i1 @fpext_maybe_nan(float %arg0) {
%0:
  %op = fpext float %arg0 to double
  %tmp = fcmp ord double %op, %op
  ret i1 %tmp
}
Transformation seems to be correct! (syntactically equal)

-- 131. InstSimplifyPass

----------------------------------------
define i1 @fpext_maybe_nan(float %arg0) {
%0:
  %op = fpext float %arg0 to double
  %tmp = fcmp ord double %op, %op
  ret i1 %tmp
}
Transformation seems to be correct! (syntactically equal)

-- 132. PassManager<Function> : Skipping NOP
-- 133. PassManager<Function> : Skipping NOP
-- 134. InstSimplifyPass

----------------------------------------
define i1 @fptrunc(double %arg0) {
%0:
  %arg0.nnan = fadd nnan double %arg0, 1.000000
  %op = fptrunc double %arg0.nnan to float
  %tmp = fcmp uno float %op, %op
  ret i1 %tmp
}
Transformation seems to be correct! (syntactically equal)

-- 135. InstSimplifyPass

----------------------------------------
define i1 @fptrunc(double %arg0) {
%0:
  %arg0.nnan = fadd nnan double %arg0, 1.000000
  %op = fptrunc double %arg0.nnan to float
  %tmp = fcmp uno float %op, %op
  ret i1 %tmp
}
=>
define i1 @fptrunc(double %arg0) {
%0:
  ret i1 0
}
Transformation seems to be correct!

-- 136. PassManager<Function> : Skipping NOP
-- 137. PassManager<Function> : Skipping NOP
-- 138. InstSimplifyPass

----------------------------------------
define i1 @fptrunc_maybe_nan(double %arg0) {
%0:
  %op = fptrunc double %arg0 to float
  %tmp = fcmp ord float %op, %op
  ret i1 %tmp
}
Transformation seems to be correct! (syntactically equal)

-- 139. InstSimplifyPass

----------------------------------------
define i1 @fptrunc_maybe_nan(double %arg0) {
%0:
  %op = fptrunc double %arg0 to float
  %tmp = fcmp ord float %op, %op
  ret i1 %tmp
}
Transformation seems to be correct! (syntactically equal)

-- 140. PassManager<Function> : Skipping NOP
-- 141. PassManager<Function> : Skipping NOP
-- 142. InstSimplifyPass

----------------------------------------
define i1 @nnan_fdiv(double %arg0, double %arg1) {
%0:
  %nnan.arg0 = fadd nnan double %arg0, 1.000000
  %nnan.arg1 = fadd nnan double %arg0, 2.000000
  %op = fdiv double %nnan.arg0, %nnan.arg1
  %tmp = fcmp uno double %op, %op
  ret i1 %tmp
}
Transformation seems to be correct! (syntactically equal)

-- 143. InstSimplifyPass

----------------------------------------
define i1 @nnan_fdiv(double %arg0, double %arg1) {
%0:
  %nnan.arg0 = fadd nnan double %arg0, 1.000000
  %nnan.arg1 = fadd nnan double %arg0, 2.000000
  %op = fdiv double %nnan.arg0, %nnan.arg1
  %tmp = fcmp uno double %op, %op
  ret i1 %tmp
}
Transformation seems to be correct! (syntactically equal)

-- 144. PassManager<Function> : Skipping NOP
-- 145. PassManager<Function> : Skipping NOP
-- 146. InstSimplifyPass

----------------------------------------
define i1 @nnan_frem(double %arg0, double %arg1) {
%0:
  %nnan.arg0 = fadd nnan double %arg0, 1.000000
  %nnan.arg1 = fadd nnan double %arg0, 2.000000
  %op = frem double %nnan.arg0, %nnan.arg1
  %tmp = fcmp ord double %op, %op
  ret i1 %tmp
}
Transformation seems to be correct! (syntactically equal)

-- 147. InstSimplifyPass

----------------------------------------
define i1 @nnan_frem(double %arg0, double %arg1) {
%0:
  %nnan.arg0 = fadd nnan double %arg0, 1.000000
  %nnan.arg1 = fadd nnan double %arg0, 2.000000
  %op = frem double %nnan.arg0, %nnan.arg1
  %tmp = fcmp ord double %op, %op
  ret i1 %tmp
}
Transformation seems to be correct! (syntactically equal)

-- 148. PassManager<Function> : Skipping NOP
-- 149. PassManager<Function> : Skipping NOP
-- 150. InstSimplifyPass

----------------------------------------
define i1 @nnan_arithemtic_fence_src(double %arg) {
%0:
  %nnan = fadd nnan double %arg, 1.000000
  %op = double %nnan
  %tmp = fcmp ord double %op, %op
  ret i1 %tmp
}
Transformation seems to be correct! (syntactically equal)

-- 151. InstSimplifyPass

----------------------------------------
define i1 @nnan_arithemtic_fence_src(double %arg) {
%0:
  %nnan = fadd nnan double %arg, 1.000000
  %op = double %nnan
  %tmp = fcmp ord double %op, %op
  ret i1 %tmp
}
=>
define i1 @nnan_arithemtic_fence_src(double %arg) {
%0:
  ret i1 1
}
Transformation seems to be correct!

-- 152. PassManager<Function> : Skipping NOP
-- 153. PassManager<Function> : Skipping NOP
ERROR: Unsupported attribute: nofpclass(nan)
-- 154. InstSimplifyPass
ERROR: Unsupported attribute: nofpclass(nan)
-- 155. InstSimplifyPass
ERROR: Unsupported attribute: nofpclass(nan)
-- 156. PassManager<Function> : Skipping NOP
ERROR: Unsupported attribute: nofpclass(nan)
-- 157. PassManager<Function> : Skipping NOP
ERROR: Unsupported attribute: nofpclass(qnan)
-- 158. InstSimplifyPass
ERROR: Unsupported attribute: nofpclass(qnan)
-- 159. InstSimplifyPass
ERROR: Unsupported attribute: nofpclass(qnan)
-- 160. PassManager<Function> : Skipping NOP
ERROR: Unsupported attribute: nofpclass(qnan)
-- 161. PassManager<Function> : Skipping NOP
ERROR: Unsupported attribute: nofpclass(snan)
-- 162. InstSimplifyPass
ERROR: Unsupported attribute: nofpclass(snan)
-- 163. InstSimplifyPass
ERROR: Unsupported attribute: nofpclass(snan)
-- 164. PassManager<Function> : Skipping NOP
ERROR: Unsupported attribute: nofpclass(snan)
-- 165. PassManager<Function> : Skipping NOP
ERROR: Unsupported attribute: nofpclass(zero)
-- 166. InstSimplifyPass
ERROR: Unsupported attribute: nofpclass(zero)
-- 167. InstSimplifyPass
ERROR: Unsupported attribute: nofpclass(zero)
-- 168. PassManager<Function> : Skipping NOP
ERROR: Unsupported attribute: nofpclass(zero)
-- 169. PassManager<Function> : Skipping NOP
-- 170. InstSimplifyPass

----------------------------------------
define i1 @isKnownNeverNaN_nofpclass_call_decl() {
%0:
  %call = call double @declare_no_nan_return()
  %tmp = fcmp ord double %call, %call
  ret i1 %tmp
}
Transformation seems to be correct! (syntactically equal)

-- 171. InstSimplifyPass

----------------------------------------
define i1 @isKnownNeverNaN_nofpclass_call_decl() {
%0:
  %call = call double @declare_no_nan_return()
  %tmp = fcmp ord double %call, %call
  ret i1 %tmp
}
=>
define i1 @isKnownNeverNaN_nofpclass_call_decl() {
%0:
  %call = call double @declare_no_nan_return()
  ret i1 1
}
Transformation doesn't verify! (unsound)
ERROR: Value mismatch

Example:

Source:
double %call = #x7ff0000040000000 (SNaN)
i1 %tmp = #x0 (0)

SOURCE MEMORY STATE
===================
NON-LOCAL BLOCKS:
Block 0 >	size: 0	align: 1	alloc type: 0	address: 0
Block 1 >	size: 0	align: 1	alloc type: 0	address: 0

Target:
double %call = #x7ff0000040000000 (SNaN)
Source value: #x0 (0)
Target value: #x1 (1)

Pass: InstSimplifyPass
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=instsimplify' '-tv-smt-to=20000' '-tv-report-dir=/home/nlopes/alive2/build/logs' '-tv-smt-stats'
Wrote bitcode to: "/home/nlopes/alive2/build/logs/in_gE5grXtP_X9GK.bc"


------------------- SMT STATS -------------------
Num queries: 99
Num invalid: 0
Num skips:   0
Num trivial: 126 (56.0%)
Num timeout: 2 (2.0%)
Num errors:  0 (0.0%)
Num SAT:     78 (78.8%)
Num UNSAT:   19 (19.2%)
Alive2: Transform doesn't verify; aborting!

stderr:

+ : 'RUN: at line 2'
+ /home/nlopes/alive2/build/opt-alive.sh -S -passes=instsimplify
+ /bitbucket/nlopes/llvm/build/bin/FileCheck /bitbucket/nlopes/llvm/llvm/test/Transforms/InstSimplify/known-never-nan.ll

FileCheck error: '<stdin>' is empty.
FileCheck command line:  /bitbucket/nlopes/llvm/build/bin/FileCheck /bitbucket/nlopes/llvm/llvm/test/Transforms/InstSimplify/known-never-nan.ll

<-- Back