Test Failure: Transforms/HipStdPar/math-fixup.ll

Test source: git

Log:

Source: /bitbucket/nlopes/llvm/llvm/test/Transforms/HipStdPar/math-fixup.ll
-- 1. HipStdParMathFixupPass
-- 2. HipStdParMathFixupPass

----------------------------------------
declare double @llvm.acos.f64(double) nofree willreturn memory(none)
declare float @llvm.acos.f32(float) nofree willreturn memory(none)

define void @test_acos(double %dbl, float %flt) {
entry:
  %#0 = call double @llvm.acos.f64(double %dbl) nofree willreturn memory(none)
  %#1 = call float @llvm.acos.f32(float %flt) nofree willreturn memory(none)
  ret void
}
=>
declare double @__hipstdpar_acos_f64(double)
declare float @__hipstdpar_acos_f32(float)

define void @test_acos(double %dbl, float %flt) {
entry:
  %#0 = call double @__hipstdpar_acos_f64(double %dbl)
  %#1 = call float @__hipstdpar_acos_f32(float %flt)
  ret void
}
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.acos.f32
 - Unknown libcall: @llvm.acos.f64


----------------------------------------
declare double @acosh(double)
declare float @acoshf(float)

define void @test_acosh(double %dbl, float %flt) {
entry:
  %#0 = call double @acosh(double %dbl)
  %#1 = call float @acoshf(float %flt)
  ret void
}
=>
declare double @__hipstdpar_acosh_f64(double)
declare float @__hipstdpar_acosh_f32(float)

define void @test_acosh(double %dbl, float %flt) {
entry:
  %#0 = call double @__hipstdpar_acosh_f64(double %dbl)
  %#1 = call float @__hipstdpar_acosh_f32(float %flt)
  ret void
}
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: @acosh
 - Unknown libcall: @acoshf


----------------------------------------
declare double @llvm.asin.f64(double) nofree willreturn memory(none)
declare float @llvm.asin.f32(float) nofree willreturn memory(none)

define void @test_asin(double %dbl, float %flt) {
entry:
  %#0 = call double @llvm.asin.f64(double %dbl) nofree willreturn memory(none)
  %#1 = call float @llvm.asin.f32(float %flt) nofree willreturn memory(none)
  ret void
}
=>
declare double @__hipstdpar_asin_f64(double)
declare float @__hipstdpar_asin_f32(float)

define void @test_asin(double %dbl, float %flt) {
entry:
  %#0 = call double @__hipstdpar_asin_f64(double %dbl)
  %#1 = call float @__hipstdpar_asin_f32(float %flt)
  ret void
}
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.asin.f32
 - Unknown libcall: @llvm.asin.f64


----------------------------------------
declare double @asinh(double)
declare float @asinhf(float)

define void @test_asinh(double %dbl, float %flt) {
entry:
  %#0 = call double @asinh(double %dbl)
  %#1 = call float @asinhf(float %flt)
  ret void
}
=>
declare double @__hipstdpar_asinh_f64(double)
declare float @__hipstdpar_asinh_f32(float)

define void @test_asinh(double %dbl, float %flt) {
entry:
  %#0 = call double @__hipstdpar_asinh_f64(double %dbl)
  %#1 = call float @__hipstdpar_asinh_f32(float %flt)
  ret void
}
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: @asinh
 - Unknown libcall: @asinhf


----------------------------------------
declare double @llvm.atan.f64(double) nofree willreturn memory(none)
declare float @llvm.atan.f32(float) nofree willreturn memory(none)

define void @test_atan(double %dbl, float %flt) {
entry:
  %#0 = call double @llvm.atan.f64(double %dbl) nofree willreturn memory(none)
  %#1 = call float @llvm.atan.f32(float %flt) nofree willreturn memory(none)
  ret void
}
=>
declare double @__hipstdpar_atan_f64(double)
declare float @__hipstdpar_atan_f32(float)

define void @test_atan(double %dbl, float %flt) {
entry:
  %#0 = call double @__hipstdpar_atan_f64(double %dbl)
  %#1 = call float @__hipstdpar_atan_f32(float %flt)
  ret void
}
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.atan.f32
 - Unknown libcall: @llvm.atan.f64


----------------------------------------
declare double @atanh(double)
declare float @atanhf(float)

define void @test_atanh(double %dbl, float %flt) {
entry:
  %#0 = call double @atanh(double %dbl)
  %#1 = call float @atanhf(float %flt)
  ret void
}
=>
declare double @__hipstdpar_atanh_f64(double)
declare float @__hipstdpar_atanh_f32(float)

define void @test_atanh(double %dbl, float %flt) {
entry:
  %#0 = call double @__hipstdpar_atanh_f64(double %dbl)
  %#1 = call float @__hipstdpar_atanh_f32(float %flt)
  ret void
}
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: @atanh
 - Unknown libcall: @atanhf


----------------------------------------
declare double @llvm.atan2.f64(double, double) nofree willreturn memory(none)
declare float @llvm.atan2.f32(float, float) nofree willreturn memory(none)

define void @test_atan2(double %dbl, float %flt) {
entry:
  %#0 = call double @llvm.atan2.f64(double %dbl, double %dbl) nofree willreturn memory(none)
  %#1 = call float @llvm.atan2.f32(float %flt, float %flt) nofree willreturn memory(none)
  ret void
}
=>
declare double @__hipstdpar_atan2_f64(double, double)
declare float @__hipstdpar_atan2_f32(float, float)

define void @test_atan2(double %dbl, float %flt) {
entry:
  %#0 = call double @__hipstdpar_atan2_f64(double %dbl, double %dbl)
  %#1 = call float @__hipstdpar_atan2_f32(float %flt, float %flt)
  ret void
}
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.atan2.f32
 - Unknown libcall: @llvm.atan2.f64


----------------------------------------
declare double @cbrt(double)
declare float @cbrtf(float)

define void @test_cbrt(double %dbl, float %flt) {
entry:
  %#0 = call double @cbrt(double %dbl)
  %#1 = call float @cbrtf(float %flt)
  ret void
}
=>
declare double @__hipstdpar_cbrt_f64(double)
declare float @__hipstdpar_cbrt_f32(float)

define void @test_cbrt(double %dbl, float %flt) {
entry:
  %#0 = call double @__hipstdpar_cbrt_f64(double %dbl)
  %#1 = call float @__hipstdpar_cbrt_f32(float %flt)
  ret void
}
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: @cbrt
 - Unknown libcall: @cbrtf


----------------------------------------
declare double @llvm.cos.f64(double) nofree willreturn memory(none)

define void @test_cos(double %dbl) {
entry:
  %#0 = call double @llvm.cos.f64(double %dbl) nofree willreturn memory(none)
  ret void
}
=>
declare double @__hipstdpar_cos_f64(double)

define void @test_cos(double %dbl) {
entry:
  %#0 = call double @__hipstdpar_cos_f64(double %dbl)
  ret void
}
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.cos.f64


----------------------------------------
declare double @llvm.cosh.f64(double) nofree willreturn memory(none)
declare float @llvm.cosh.f32(float) nofree willreturn memory(none)

define void @test_cosh(double %dbl, float %flt) {
entry:
  %#0 = call double @llvm.cosh.f64(double %dbl) nofree willreturn memory(none)
  %#1 = call float @llvm.cosh.f32(float %flt) nofree willreturn memory(none)
  ret void
}
=>
declare double @__hipstdpar_cosh_f64(double)
declare float @__hipstdpar_cosh_f32(float)

define void @test_cosh(double %dbl, float %flt) {
entry:
  %#0 = call double @__hipstdpar_cosh_f64(double %dbl)
  %#1 = call float @__hipstdpar_cosh_f32(float %flt)
  ret void
}
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.cosh.f32
 - Unknown libcall: @llvm.cosh.f64


----------------------------------------
declare double @erf(double)
declare float @erff(float)

define void @test_erf(double %dbl, float %flt) {
entry:
  %#0 = call double @erf(double %dbl)
  %#1 = call float @erff(float %flt)
  ret void
}
=>
declare double @__hipstdpar_erf_f64(double)
declare float @__hipstdpar_erf_f32(float)

define void @test_erf(double %dbl, float %flt) {
entry:
  %#0 = call double @__hipstdpar_erf_f64(double %dbl)
  %#1 = call float @__hipstdpar_erf_f32(float %flt)
  ret void
}
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: @erf
 - Unknown libcall: @erff


----------------------------------------
declare double @erfc(double)
declare float @erfcf(float)

define void @test_erfc(double %dbl, float %flt) {
entry:
  %#0 = call double @erfc(double %dbl)
  %#1 = call float @erfcf(float %flt)
  ret void
}
=>
declare double @__hipstdpar_erfc_f64(double)
declare float @__hipstdpar_erfc_f32(float)

define void @test_erfc(double %dbl, float %flt) {
entry:
  %#0 = call double @__hipstdpar_erfc_f64(double %dbl)
  %#1 = call float @__hipstdpar_erfc_f32(float %flt)
  ret void
}
Transformation doesn't verify! (unsound)
ERROR: Source is more defined than target

Example:
double %dbl = poison
float %flt = poison

Source:
double %#0 = function did not return!

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

Target:
Function @__hipstdpar_erfc_f64 triggered UB


Pass: HipStdParMathFixupPass
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=hipstdpar-math-fixup' '/bitbucket/nlopes/llvm/llvm/test/Transforms/HipStdPar/math-fixup.ll' '-tv-smt-to=20000' '-tv-report-dir=/home/nlopes/alive2/build/logs' '-tv-smt-stats'
Wrote bitcode to: "/home/nlopes/alive2/build/logs/math-fixup_TRDfYf8g_t7Dt.bc"


------------------- SMT STATS -------------------
Num queries: 55
Num invalid: 0
Num skips:   0
Num trivial: 0 (0.0%)
Num timeout: 0 (0.0%)
Num errors:  0 (0.0%)
Num SAT:     54 (98.2%)
Num UNSAT:   1 (1.8%)
Alive2: Transform doesn't verify; aborting!

stderr:

/home/nlopes/alive2/build/opt-alive.sh -S -passes=hipstdpar-math-fixup /bitbucket/nlopes/llvm/llvm/test/Transforms/HipStdPar/math-fixup.ll | /bitbucket/nlopes/llvm/build/bin/FileCheck /bitbucket/nlopes/llvm/llvm/test/Transforms/HipStdPar/math-fixup.ll # RUN: at line 2
+ /home/nlopes/alive2/build/opt-alive.sh -S -passes=hipstdpar-math-fixup /bitbucket/nlopes/llvm/llvm/test/Transforms/HipStdPar/math-fixup.ll
+ /bitbucket/nlopes/llvm/build/bin/FileCheck /bitbucket/nlopes/llvm/llvm/test/Transforms/HipStdPar/math-fixup.ll

FileCheck error: '<stdin>' is empty.
FileCheck command line:  /bitbucket/nlopes/llvm/build/bin/FileCheck /bitbucket/nlopes/llvm/llvm/test/Transforms/HipStdPar/math-fixup.ll

<-- Back