Test Failure: Transforms/SLPVectorizer/X86/horizontal-list.ll

Test source: git

Log:

Source: <stdin>

----------------------------------------
@n = global 4 bytes, align 4
@arr = global 80 bytes, align 16
@arr1 = global 80 bytes, align 16
@res = global 4 bytes, align 4

define float @baz() {
%entry:
  %0 = load i32, ptr @n, align 4
  %mul = mul nsw i32 %0, 3
  %conv = sitofp i32 %mul to float, exceptions=ignore
  %__constexpr_0 = gep inbounds ptr @arr, 80 x i64 0, 4 x i64 0
  %1 = load float, ptr %__constexpr_0, align 16
  %__constexpr_1 = gep inbounds ptr @arr1, 80 x i64 0, 4 x i64 0
  %2 = load float, ptr %__constexpr_1, align 16
  %mul4 = fmul fast float %2, %1, exceptions=ignore
  %add = fadd fast float %mul4, %conv, exceptions=ignore
  %__constexpr_2 = gep inbounds ptr @arr, 80 x i64 0, 4 x i64 1
  %3 = load float, ptr %__constexpr_2, align 4
  %__constexpr_3 = gep inbounds ptr @arr1, 80 x i64 0, 4 x i64 1
  %4 = load float, ptr %__constexpr_3, align 4
  %mul4.1 = fmul fast float %4, %3, exceptions=ignore
  %add.1 = fadd fast float %mul4.1, %add, exceptions=ignore
  %__constexpr_4 = gep inbounds ptr @arr, 80 x i64 0, 4 x i64 2
  %5 = load float, ptr %__constexpr_4, align 8
  %__constexpr_5 = gep inbounds ptr @arr1, 80 x i64 0, 4 x i64 2
  %6 = load float, ptr %__constexpr_5, align 8
  %mul4.2 = fmul fast float %6, %5, exceptions=ignore
  %add.2 = fadd fast float %mul4.2, %add.1, exceptions=ignore
  %__constexpr_6 = gep inbounds ptr @arr, 80 x i64 0, 4 x i64 3
  %7 = load float, ptr %__constexpr_6, align 4
  %__constexpr_7 = gep inbounds ptr @arr1, 80 x i64 0, 4 x i64 3
  %8 = load float, ptr %__constexpr_7, align 4
  %mul4.3 = fmul fast float %8, %7, exceptions=ignore
  %add.3 = fadd fast float %mul4.3, %add.2, exceptions=ignore
  %add7 = fadd fast float %add.3, %conv, exceptions=ignore
  %add19 = fadd fast float %mul4, %add7, exceptions=ignore
  %add19.1 = fadd fast float %mul4.1, %add19, exceptions=ignore
  %add19.2 = fadd fast float %mul4.2, %add19.1, exceptions=ignore
  %add19.3 = fadd fast float %mul4.3, %add19.2, exceptions=ignore
  store float %add19.3, ptr @res, align 4
  ret float %add19.3
}
=>
@n = global 4 bytes, align 4
@arr = global 80 bytes, align 16
@arr1 = global 80 bytes, align 16
@res = global 4 bytes, align 4

define float @baz() {
%entry:
  %0 = load i32, ptr @n, align 4
  %mul = mul nsw i32 %0, 3
  %conv = sitofp i32 %mul to float, exceptions=ignore
  %__constexpr_0 = bitcast ptr @arr to ptr
  %1 = load <4 x float>, ptr %__constexpr_0, align 16
  %__constexpr_1 = bitcast ptr @arr1 to ptr
  %2 = load <4 x float>, ptr %__constexpr_1, align 16
  %3 = fmul fast <4 x float> %2, %1, exceptions=ignore
  %shuffle = shufflevector <4 x float> %3, <4 x float> poison, 0, 0, 1, 1, 2, 2, 3, 3
  %4 = call float @llvm.vector.reduce.fadd.v8f32(float -0.000000, <8 x float> %shuffle) noread nowrite NNaN nofree willreturn
  %op.rdx = fadd fast float %4, %conv, exceptions=ignore
  %op.rdx1 = fadd fast float %op.rdx, %conv, exceptions=ignore
  store float %op.rdx1, ptr @res, align 4
  ret float %op.rdx1
}
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:
 - Unknown libcall: @llvm.vector.reduce.fadd.v8f32



----------------------------------------
@n = global 4 bytes, align 4
@arr = global 80 bytes, align 16
@arr1 = global 80 bytes, align 16
@res = global 4 bytes, align 4

define float @bazz() {
%entry:
  %0 = load i32, ptr @n, align 4
  %mul = mul nsw i32 %0, 3
  %conv = sitofp i32 %mul to float, exceptions=ignore
  %__constexpr_0 = gep inbounds ptr @arr, 80 x i64 0, 4 x i64 0
  %1 = load float, ptr %__constexpr_0, align 16
  %__constexpr_1 = gep inbounds ptr @arr1, 80 x i64 0, 4 x i64 0
  %2 = load float, ptr %__constexpr_1, align 16
  %mul4 = fmul fast float %2, %1, exceptions=ignore
  %add = fadd fast float %mul4, %conv, exceptions=ignore
  %__constexpr_2 = gep inbounds ptr @arr, 80 x i64 0, 4 x i64 1
  %3 = load float, ptr %__constexpr_2, align 4
  %__constexpr_3 = gep inbounds ptr @arr1, 80 x i64 0, 4 x i64 1
  %4 = load float, ptr %__constexpr_3, align 4
  %mul4.1 = fmul fast float %4, %3, exceptions=ignore
  %add.1 = fadd fast float %mul4.1, %add, exceptions=ignore
  %__constexpr_4 = gep inbounds ptr @arr, 80 x i64 0, 4 x i64 2
  %5 = load float, ptr %__constexpr_4, align 8
  %__constexpr_5 = gep inbounds ptr @arr1, 80 x i64 0, 4 x i64 2
  %6 = load float, ptr %__constexpr_5, align 8
  %mul4.2 = fmul fast float %6, %5, exceptions=ignore
  %add.2 = fadd fast float %mul4.2, %add.1, exceptions=ignore
  %__constexpr_6 = gep inbounds ptr @arr, 80 x i64 0, 4 x i64 3
  %7 = load float, ptr %__constexpr_6, align 4
  %__constexpr_7 = gep inbounds ptr @arr1, 80 x i64 0, 4 x i64 3
  %8 = load float, ptr %__constexpr_7, align 4
  %mul4.3 = fmul fast float %8, %7, exceptions=ignore
  %add.3 = fadd fast float %mul4.3, %add.2, exceptions=ignore
  %mul5 = shl nsw i32 %0, 2
  %conv6 = sitofp i32 %mul5 to float, exceptions=ignore
  %add7 = fadd fast float %add.3, %conv6, exceptions=ignore
  %__constexpr_8 = gep inbounds ptr @arr, 80 x i64 0, 4 x i64 4
  %9 = load float, ptr %__constexpr_8, align 16
  %__constexpr_9 = gep inbounds ptr @arr1, 80 x i64 0, 4 x i64 4
  %10 = load float, ptr %__constexpr_9, align 16
  %mul18 = fmul fast float %10, %9, exceptions=ignore
  %add19 = fadd fast float %mul18, %add7, exceptions=ignore
  %__constexpr_10 = gep inbounds ptr @arr, 80 x i64 0, 4 x i64 5
  %11 = load float, ptr %__constexpr_10, align 4
  %__constexpr_11 = gep inbounds ptr @arr1, 80 x i64 0, 4 x i64 5
  %12 = load float, ptr %__constexpr_11, align 4
  %mul18.1 = fmul fast float %12, %11, exceptions=ignore
  %add19.1 = fadd fast float %mul18.1, %add19, exceptions=ignore
  %__constexpr_12 = gep inbounds ptr @arr, 80 x i64 0, 4 x i64 6
  %13 = load float, ptr %__constexpr_12, align 8
  %__constexpr_13 = gep inbounds ptr @arr1, 80 x i64 0, 4 x i64 6
  %14 = load float, ptr %__constexpr_13, align 8
  %mul18.2 = fmul fast float %14, %13, exceptions=ignore
  %add19.2 = fadd fast float %mul18.2, %add19.1, exceptions=ignore
  %__constexpr_14 = gep inbounds ptr @arr, 80 x i64 0, 4 x i64 7
  %15 = load float, ptr %__constexpr_14, align 4
  %__constexpr_15 = gep inbounds ptr @arr1, 80 x i64 0, 4 x i64 7
  %16 = load float, ptr %__constexpr_15, align 4
  %mul18.3 = fmul fast float %16, %15, exceptions=ignore
  %add19.3 = fadd fast float %mul18.3, %add19.2, exceptions=ignore
  store float %add19.3, ptr @res, align 4
  ret float %add19.3
}
=>
@n = global 4 bytes, align 4
@arr = global 80 bytes, align 16
@arr1 = global 80 bytes, align 16
@res = global 4 bytes, align 4

define float @bazz() {
%entry:
  %0 = load i32, ptr @n, align 4
  %mul = mul nsw i32 %0, 3
  %conv = sitofp i32 %mul to float, exceptions=ignore
  %mul5 = shl nsw i32 %0, 2
  %conv6 = sitofp i32 %mul5 to float, exceptions=ignore
  %__constexpr_0 = bitcast ptr @arr to ptr
  %1 = load <8 x float>, ptr %__constexpr_0, align 16
  %__constexpr_1 = bitcast ptr @arr1 to ptr
  %2 = load <8 x float>, ptr %__constexpr_1, align 16
  %3 = fmul fast <8 x float> %2, %1, exceptions=ignore
  %4 = call float @llvm.vector.reduce.fadd.v8f32(float -0.000000, <8 x float> %3) noread nowrite NNaN nofree willreturn
  %op.rdx = fadd fast float %4, %conv, exceptions=ignore
  %op.rdx1 = fadd fast float %op.rdx, %conv6, exceptions=ignore
  store float %op.rdx1, ptr @res, align 4
  ret float %op.rdx1
}
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:
 - Unknown libcall: @llvm.vector.reduce.fadd.v8f32



----------------------------------------
@n = global 4 bytes, align 4
@arr = global 80 bytes, align 16
@arr1 = global 80 bytes, align 16
@res = global 4 bytes, align 4

define float @bazzz() {
%entry:
  %0 = load i32, ptr @n, align 4
  %conv = sitofp i32 %0 to float, exceptions=ignore
  %__constexpr_0 = gep inbounds ptr @arr, 80 x i64 0, 4 x i64 0
  %1 = load float, ptr %__constexpr_0, align 16
  %__constexpr_1 = gep inbounds ptr @arr1, 80 x i64 0, 4 x i64 0
  %2 = load float, ptr %__constexpr_1, align 16
  %mul = fmul fast float %2, %1, exceptions=ignore
  %__constexpr_2 = gep inbounds ptr @arr, 80 x i64 0, 4 x i64 1
  %3 = load float, ptr %__constexpr_2, align 4
  %__constexpr_3 = gep inbounds ptr @arr1, 80 x i64 0, 4 x i64 1
  %4 = load float, ptr %__constexpr_3, align 4
  %mul.1 = fmul fast float %4, %3, exceptions=ignore
  %5 = fadd fast float %mul.1, %mul, exceptions=ignore
  %__constexpr_4 = gep inbounds ptr @arr, 80 x i64 0, 4 x i64 2
  %6 = load float, ptr %__constexpr_4, align 8
  %__constexpr_5 = gep inbounds ptr @arr1, 80 x i64 0, 4 x i64 2
  %7 = load float, ptr %__constexpr_5, align 8
  %mul.2 = fmul fast float %7, %6, exceptions=ignore
  %8 = fadd fast float %mul.2, %5, exceptions=ignore
  %__constexpr_6 = gep inbounds ptr @arr, 80 x i64 0, 4 x i64 3
  %9 = load float, ptr %__constexpr_6, align 4
  %__constexpr_7 = gep inbounds ptr @arr1, 80 x i64 0, 4 x i64 3
  %10 = load float, ptr %__constexpr_7, align 4
  %mul.3 = fmul fast float %10, %9, exceptions=ignore
  %11 = fadd fast float %mul.3, %8, exceptions=ignore
  %12 = fmul fast float %conv, %11, exceptions=ignore
  store float %12, ptr @res, align 4
  ret float %12
}
=>
@n = global 4 bytes, align 4
@arr = global 80 bytes, align 16
@arr1 = global 80 bytes, align 16
@res = global 4 bytes, align 4

define float @bazzz() {
%entry:
  %0 = load i32, ptr @n, align 4
  %conv = sitofp i32 %0 to float, exceptions=ignore
  %__constexpr_0 = bitcast ptr @arr to ptr
  %1 = load <4 x float>, ptr %__constexpr_0, align 16
  %__constexpr_1 = bitcast ptr @arr1 to ptr
  %2 = load <4 x float>, ptr %__constexpr_1, align 16
  %3 = fmul fast <4 x float> %2, %1, exceptions=ignore
  %4 = call float @llvm.vector.reduce.fadd.v4f32(float -0.000000, <4 x float> %3) noread nowrite NNaN nofree willreturn
  %5 = fmul fast float %conv, %4, exceptions=ignore
  store float %5, ptr @res, align 4
  ret float %5
}
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:
 - Unknown libcall: @llvm.vector.reduce.fadd.v4f32



----------------------------------------
@n = global 4 bytes, align 4
@arr = global 80 bytes, align 16
@arr1 = global 80 bytes, align 16

define i32 @foo() {
%entry:
  %0 = load i32, ptr @n, align 4
  %conv = sitofp i32 %0 to float, exceptions=ignore
  %__constexpr_0 = gep inbounds ptr @arr, 80 x i64 0, 4 x i64 0
  %1 = load float, ptr %__constexpr_0, align 16
  %__constexpr_1 = gep inbounds ptr @arr1, 80 x i64 0, 4 x i64 0
  %2 = load float, ptr %__constexpr_1, align 16
  %mul = fmul fast float %2, %1, exceptions=ignore
  %__constexpr_2 = gep inbounds ptr @arr, 80 x i64 0, 4 x i64 1
  %3 = load float, ptr %__constexpr_2, align 4
  %__constexpr_3 = gep inbounds ptr @arr1, 80 x i64 0, 4 x i64 1
  %4 = load float, ptr %__constexpr_3, align 4
  %mul.1 = fmul fast float %4, %3, exceptions=ignore
  %5 = fadd fast float %mul.1, %mul, exceptions=ignore
  %__constexpr_4 = gep inbounds ptr @arr, 80 x i64 0, 4 x i64 2
  %6 = load float, ptr %__constexpr_4, align 8
  %__constexpr_5 = gep inbounds ptr @arr1, 80 x i64 0, 4 x i64 2
  %7 = load float, ptr %__constexpr_5, align 8
  %mul.2 = fmul fast float %7, %6, exceptions=ignore
  %8 = fadd fast float %mul.2, %5, exceptions=ignore
  %__constexpr_6 = gep inbounds ptr @arr, 80 x i64 0, 4 x i64 3
  %9 = load float, ptr %__constexpr_6, align 4
  %__constexpr_7 = gep inbounds ptr @arr1, 80 x i64 0, 4 x i64 3
  %10 = load float, ptr %__constexpr_7, align 4
  %mul.3 = fmul fast float %10, %9, exceptions=ignore
  %11 = fadd fast float %mul.3, %8, exceptions=ignore
  %12 = fmul fast float %conv, %11, exceptions=ignore
  %conv4 = fptosi float %12 to i32, exceptions=ignore
  store i32 %conv4, ptr @n, align 4
  ret i32 %conv4
}
=>
@n = global 4 bytes, align 4
@arr = global 80 bytes, align 16
@arr1 = global 80 bytes, align 16

define i32 @foo() {
%entry:
  %0 = load i32, ptr @n, align 4
  %conv = sitofp i32 %0 to float, exceptions=ignore
  %__constexpr_0 = bitcast ptr @arr to ptr
  %1 = load <4 x float>, ptr %__constexpr_0, align 16
  %__constexpr_1 = bitcast ptr @arr1 to ptr
  %2 = load <4 x float>, ptr %__constexpr_1, align 16
  %3 = fmul fast <4 x float> %2, %1, exceptions=ignore
  %4 = call float @llvm.vector.reduce.fadd.v4f32(float -0.000000, <4 x float> %3) noread nowrite NNaN nofree willreturn
  %5 = fmul fast float %conv, %4, exceptions=ignore
  %conv4 = fptosi float %5 to i32, exceptions=ignore
  store i32 %conv4, ptr @n, align 4
  ret i32 %conv4
}
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:
 - Unknown libcall: @llvm.vector.reduce.fadd.v4f32



----------------------------------------
@arr = global 80 bytes, align 16
@arr1 = global 80 bytes, align 16
@res = global 4 bytes, align 4

define float @bar() {
%entry:
  %__constexpr_0 = gep inbounds ptr @arr, 80 x i64 0, 4 x i64 0
  %0 = load float, ptr %__constexpr_0, align 16
  %__constexpr_1 = gep inbounds ptr @arr1, 80 x i64 0, 4 x i64 0
  %1 = load float, ptr %__constexpr_1, align 16
  %mul = fmul fast float %1, %0, exceptions=ignore
  %__constexpr_2 = gep inbounds ptr @arr, 80 x i64 0, 4 x i64 1
  %2 = load float, ptr %__constexpr_2, align 4
  %__constexpr_3 = gep inbounds ptr @arr1, 80 x i64 0, 4 x i64 1
  %3 = load float, ptr %__constexpr_3, align 4
  %mul3 = fmul fast float %3, %2, exceptions=ignore
  %cmp4 = fcmp fast ogt float %mul, %mul3
  %max.0.mul3 = select i1 %cmp4, float %mul, float %mul3
  %__constexpr_4 = gep inbounds ptr @arr, 80 x i64 0, 4 x i64 2
  %4 = load float, ptr %__constexpr_4, align 8
  %__constexpr_5 = gep inbounds ptr @arr1, 80 x i64 0, 4 x i64 2
  %5 = load float, ptr %__constexpr_5, align 8
  %mul3.1 = fmul fast float %5, %4, exceptions=ignore
  %cmp4.1 = fcmp fast ogt float %max.0.mul3, %mul3.1
  %max.0.mul3.1 = select i1 %cmp4.1, float %max.0.mul3, float %mul3.1
  %__constexpr_6 = gep inbounds ptr @arr, 80 x i64 0, 4 x i64 3
  %6 = load float, ptr %__constexpr_6, align 4
  %__constexpr_7 = gep inbounds ptr @arr1, 80 x i64 0, 4 x i64 3
  %7 = load float, ptr %__constexpr_7, align 4
  %mul3.2 = fmul fast float %7, %6, exceptions=ignore
  %cmp4.2 = fcmp fast ogt float %max.0.mul3.1, %mul3.2
  %max.0.mul3.2 = select i1 %cmp4.2, float %max.0.mul3.1, float %mul3.2
  store float %max.0.mul3.2, ptr @res, align 4
  ret float %max.0.mul3.2
}
=>
@arr = global 80 bytes, align 16
@arr1 = global 80 bytes, align 16
@res = global 4 bytes, align 4

define float @bar() {
%entry:
  %__constexpr_0 = bitcast ptr @arr to ptr
  %0 = load <2 x float>, ptr %__constexpr_0, align 16
  %__constexpr_1 = bitcast ptr @arr1 to ptr
  %1 = load <2 x float>, ptr %__constexpr_1, align 16
  %2 = fmul fast <2 x float> %1, %0, exceptions=ignore
  %3 = extractelement <2 x float> %2, i32 0
  %4 = extractelement <2 x float> %2, i32 1
  %cmp4 = fcmp fast ogt float %3, %4
  %max.0.mul3 = select i1 %cmp4, float %3, float %4
  %__constexpr_2 = gep inbounds ptr @arr, 80 x i64 0, 4 x i64 2
  %5 = load float, ptr %__constexpr_2, align 8
  %__constexpr_3 = gep inbounds ptr @arr1, 80 x i64 0, 4 x i64 2
  %6 = load float, ptr %__constexpr_3, align 8
  %mul3.1 = fmul fast float %6, %5, exceptions=ignore
  %cmp4.1 = fcmp fast ogt float %max.0.mul3, %mul3.1
  %max.0.mul3.1 = select i1 %cmp4.1, float %max.0.mul3, float %mul3.1
  %__constexpr_4 = gep inbounds ptr @arr, 80 x i64 0, 4 x i64 3
  %7 = load float, ptr %__constexpr_4, align 4
  %__constexpr_5 = gep inbounds ptr @arr1, 80 x i64 0, 4 x i64 3
  %8 = load float, ptr %__constexpr_5, align 4
  %mul3.2 = fmul fast float %8, %7, exceptions=ignore
  %cmp4.2 = fcmp fast ogt float %max.0.mul3.1, %mul3.2
  %max.0.mul3.2 = select i1 %cmp4.2, float %max.0.mul3.1, float %mul3.2
  store float %max.0.mul3.2, ptr @res, align 4
  ret float %max.0.mul3.2
}
Transformation doesn't verify!
ERROR: Timeout


----------------------------------------
define float @f(ptr nocapture nowrite %x) {
%entry:
  %0 = load float, ptr nocapture nowrite %x, align 4
  %arrayidx.1 = gep inbounds ptr nocapture nowrite %x, 4 x i64 1
  %1 = load float, ptr %arrayidx.1, align 4
  %add.1 = fadd fast float %1, %0, exceptions=ignore
  %arrayidx.2 = gep inbounds ptr nocapture nowrite %x, 4 x i64 2
  %2 = load float, ptr %arrayidx.2, align 4
  %add.2 = fadd fast float %2, %add.1, exceptions=ignore
  %arrayidx.3 = gep inbounds ptr nocapture nowrite %x, 4 x i64 3
  %3 = load float, ptr %arrayidx.3, align 4
  %add.3 = fadd fast float %3, %add.2, exceptions=ignore
  %arrayidx.4 = gep inbounds ptr nocapture nowrite %x, 4 x i64 4
  %4 = load float, ptr %arrayidx.4, align 4
  %add.4 = fadd fast float %4, %add.3, exceptions=ignore
  %arrayidx.5 = gep inbounds ptr nocapture nowrite %x, 4 x i64 5
  %5 = load float, ptr %arrayidx.5, align 4
  %add.5 = fadd fast float %5, %add.4, exceptions=ignore
  %arrayidx.6 = gep inbounds ptr nocapture nowrite %x, 4 x i64 6
  %6 = load float, ptr %arrayidx.6, align 4
  %add.6 = fadd fast float %6, %add.5, exceptions=ignore
  %arrayidx.7 = gep inbounds ptr nocapture nowrite %x, 4 x i64 7
  %7 = load float, ptr %arrayidx.7, align 4
  %add.7 = fadd fast float %7, %add.6, exceptions=ignore
  %arrayidx.8 = gep inbounds ptr nocapture nowrite %x, 4 x i64 8
  %8 = load float, ptr %arrayidx.8, align 4
  %add.8 = fadd fast float %8, %add.7, exceptions=ignore
  %arrayidx.9 = gep inbounds ptr nocapture nowrite %x, 4 x i64 9
  %9 = load float, ptr %arrayidx.9, align 4
  %add.9 = fadd fast float %9, %add.8, exceptions=ignore
  %arrayidx.10 = gep inbounds ptr nocapture nowrite %x, 4 x i64 10
  %10 = load float, ptr %arrayidx.10, align 4
  %add.10 = fadd fast float %10, %add.9, exceptions=ignore
  %arrayidx.11 = gep inbounds ptr nocapture nowrite %x, 4 x i64 11
  %11 = load float, ptr %arrayidx.11, align 4
  %add.11 = fadd fast float %11, %add.10, exceptions=ignore
  %arrayidx.12 = gep inbounds ptr nocapture nowrite %x, 4 x i64 12
  %12 = load float, ptr %arrayidx.12, align 4
  %add.12 = fadd fast float %12, %add.11, exceptions=ignore
  %arrayidx.13 = gep inbounds ptr nocapture nowrite %x, 4 x i64 13
  %13 = load float, ptr %arrayidx.13, align 4
  %add.13 = fadd fast float %13, %add.12, exceptions=ignore
  %arrayidx.14 = gep inbounds ptr nocapture nowrite %x, 4 x i64 14
  %14 = load float, ptr %arrayidx.14, align 4
  %add.14 = fadd fast float %14, %add.13, exceptions=ignore
  %arrayidx.15 = gep inbounds ptr nocapture nowrite %x, 4 x i64 15
  %15 = load float, ptr %arrayidx.15, align 4
  %add.15 = fadd fast float %15, %add.14, exceptions=ignore
  %arrayidx.16 = gep inbounds ptr nocapture nowrite %x, 4 x i64 16
  %16 = load float, ptr %arrayidx.16, align 4
  %add.16 = fadd fast float %16, %add.15, exceptions=ignore
  %arrayidx.17 = gep inbounds ptr nocapture nowrite %x, 4 x i64 17
  %17 = load float, ptr %arrayidx.17, align 4
  %add.17 = fadd fast float %17, %add.16, exceptions=ignore
  %arrayidx.18 = gep inbounds ptr nocapture nowrite %x, 4 x i64 18
  %18 = load float, ptr %arrayidx.18, align 4
  %add.18 = fadd fast float %18, %add.17, exceptions=ignore
  %arrayidx.19 = gep inbounds ptr nocapture nowrite %x, 4 x i64 19
  %19 = load float, ptr %arrayidx.19, align 4
  %add.19 = fadd fast float %19, %add.18, exceptions=ignore
  %arrayidx.20 = gep inbounds ptr nocapture nowrite %x, 4 x i64 20
  %20 = load float, ptr %arrayidx.20, align 4
  %add.20 = fadd fast float %20, %add.19, exceptions=ignore
  %arrayidx.21 = gep inbounds ptr nocapture nowrite %x, 4 x i64 21
  %21 = load float, ptr %arrayidx.21, align 4
  %add.21 = fadd fast float %21, %add.20, exceptions=ignore
  %arrayidx.22 = gep inbounds ptr nocapture nowrite %x, 4 x i64 22
  %22 = load float, ptr %arrayidx.22, align 4
  %add.22 = fadd fast float %22, %add.21, exceptions=ignore
  %arrayidx.23 = gep inbounds ptr nocapture nowrite %x, 4 x i64 23
  %23 = load float, ptr %arrayidx.23, align 4
  %add.23 = fadd fast float %23, %add.22, exceptions=ignore
  %arrayidx.24 = gep inbounds ptr nocapture nowrite %x, 4 x i64 24
  %24 = load float, ptr %arrayidx.24, align 4
  %add.24 = fadd fast float %24, %add.23, exceptions=ignore
  %arrayidx.25 = gep inbounds ptr nocapture nowrite %x, 4 x i64 25
  %25 = load float, ptr %arrayidx.25, align 4
  %add.25 = fadd fast float %25, %add.24, exceptions=ignore
  %arrayidx.26 = gep inbounds ptr nocapture nowrite %x, 4 x i64 26
  %26 = load float, ptr %arrayidx.26, align 4
  %add.26 = fadd fast float %26, %add.25, exceptions=ignore
  %arrayidx.27 = gep inbounds ptr nocapture nowrite %x, 4 x i64 27
  %27 = load float, ptr %arrayidx.27, align 4
  %add.27 = fadd fast float %27, %add.26, exceptions=ignore
  %arrayidx.28 = gep inbounds ptr nocapture nowrite %x, 4 x i64 28
  %28 = load float, ptr %arrayidx.28, align 4
  %add.28 = fadd fast float %28, %add.27, exceptions=ignore
  %arrayidx.29 = gep inbounds ptr nocapture nowrite %x, 4 x i64 29
  %29 = load float, ptr %arrayidx.29, align 4
  %add.29 = fadd fast float %29, %add.28, exceptions=ignore
  %arrayidx.30 = gep inbounds ptr nocapture nowrite %x, 4 x i64 30
  %30 = load float, ptr %arrayidx.30, align 4
  %add.30 = fadd fast float %30, %add.29, exceptions=ignore
  %arrayidx.31 = gep inbounds ptr nocapture nowrite %x, 4 x i64 31
  %31 = load float, ptr %arrayidx.31, align 4
  %add.31 = fadd fast float %31, %add.30, exceptions=ignore
  %arrayidx.32 = gep inbounds ptr nocapture nowrite %x, 4 x i64 32
  %32 = load float, ptr %arrayidx.32, align 4
  %add.32 = fadd fast float %32, %add.31, exceptions=ignore
  %arrayidx.33 = gep inbounds ptr nocapture nowrite %x, 4 x i64 33
  %33 = load float, ptr %arrayidx.33, align 4
  %add.33 = fadd fast float %33, %add.32, exceptions=ignore
  %arrayidx.34 = gep inbounds ptr nocapture nowrite %x, 4 x i64 34
  %34 = load float, ptr %arrayidx.34, align 4
  %add.34 = fadd fast float %34, %add.33, exceptions=ignore
  %arrayidx.35 = gep inbounds ptr nocapture nowrite %x, 4 x i64 35
  %35 = load float, ptr %arrayidx.35, align 4
  %add.35 = fadd fast float %35, %add.34, exceptions=ignore
  %arrayidx.36 = gep inbounds ptr nocapture nowrite %x, 4 x i64 36
  %36 = load float, ptr %arrayidx.36, align 4
  %add.36 = fadd fast float %36, %add.35, exceptions=ignore
  %arrayidx.37 = gep inbounds ptr nocapture nowrite %x, 4 x i64 37
  %37 = load float, ptr %arrayidx.37, align 4
  %add.37 = fadd fast float %37, %add.36, exceptions=ignore
  %arrayidx.38 = gep inbounds ptr nocapture nowrite %x, 4 x i64 38
  %38 = load float, ptr %arrayidx.38, align 4
  %add.38 = fadd fast float %38, %add.37, exceptions=ignore
  %arrayidx.39 = gep inbounds ptr nocapture nowrite %x, 4 x i64 39
  %39 = load float, ptr %arrayidx.39, align 4
  %add.39 = fadd fast float %39, %add.38, exceptions=ignore
  %arrayidx.40 = gep inbounds ptr nocapture nowrite %x, 4 x i64 40
  %40 = load float, ptr %arrayidx.40, align 4
  %add.40 = fadd fast float %40, %add.39, exceptions=ignore
  %arrayidx.41 = gep inbounds ptr nocapture nowrite %x, 4 x i64 41
  %41 = load float, ptr %arrayidx.41, align 4
  %add.41 = fadd fast float %41, %add.40, exceptions=ignore
  %arrayidx.42 = gep inbounds ptr nocapture nowrite %x, 4 x i64 42
  %42 = load float, ptr %arrayidx.42, align 4
  %add.42 = fadd fast float %42, %add.41, exceptions=ignore
  %arrayidx.43 = gep inbounds ptr nocapture nowrite %x, 4 x i64 43
  %43 = load float, ptr %arrayidx.43, align 4
  %add.43 = fadd fast float %43, %add.42, exceptions=ignore
  %arrayidx.44 = gep inbounds ptr nocapture nowrite %x, 4 x i64 44
  %44 = load float, ptr %arrayidx.44, align 4
  %add.44 = fadd fast float %44, %add.43, exceptions=ignore
  %arrayidx.45 = gep inbounds ptr nocapture nowrite %x, 4 x i64 45
  %45 = load float, ptr %arrayidx.45, align 4
  %add.45 = fadd fast float %45, %add.44, exceptions=ignore
  %arrayidx.46 = gep inbounds ptr nocapture nowrite %x, 4 x i64 46
  %46 = load float, ptr %arrayidx.46, align 4
  %add.46 = fadd fast float %46, %add.45, exceptions=ignore
  %arrayidx.47 = gep inbounds ptr nocapture nowrite %x, 4 x i64 47
  %47 = load float, ptr %arrayidx.47, align 4
  %add.47 = fadd fast float %47, %add.46, exceptions=ignore
  ret float %add.47
}
=>
define float @f(ptr nocapture nowrite %x) {
%entry:
  %0 = bitcast ptr nocapture nowrite %x to ptr
  %1 = load <32 x float>, ptr %0, align 4
  %arrayidx.32 = gep inbounds ptr nocapture nowrite %x, 4 x i64 32
  %2 = bitcast ptr %arrayidx.32 to ptr
  %3 = load <16 x float>, ptr %2, align 4
  %4 = call float @llvm.vector.reduce.fadd.v32f32(float -0.000000, <32 x float> %1) noread nowrite NNaN nofree willreturn
  %5 = call float @llvm.vector.reduce.fadd.v16f32(float -0.000000, <16 x float> %3) noread nowrite NNaN nofree willreturn
  %op.rdx = fadd fast float %4, %5, exceptions=ignore
  ret float %op.rdx
}
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:
 - Unknown libcall: @llvm.vector.reduce.fadd.v16f32
 - Unknown libcall: @llvm.vector.reduce.fadd.v32f32



----------------------------------------
define float @f1(ptr nocapture nowrite %x, i32 %a, i32 %b) {
%entry:
  %rem = srem i32 %a, %b
  %conv = sitofp i32 %rem to float, exceptions=ignore
  %0 = load float, ptr nocapture nowrite %x, align 4
  %add = fadd fast float %0, %conv, exceptions=ignore
  %arrayidx.1 = gep inbounds ptr nocapture nowrite %x, 4 x i64 1
  %1 = load float, ptr %arrayidx.1, align 4
  %add.1 = fadd fast float %1, %add, exceptions=ignore
  %arrayidx.2 = gep inbounds ptr nocapture nowrite %x, 4 x i64 2
  %2 = load float, ptr %arrayidx.2, align 4
  %add.2 = fadd fast float %2, %add.1, exceptions=ignore
  %arrayidx.3 = gep inbounds ptr nocapture nowrite %x, 4 x i64 3
  %3 = load float, ptr %arrayidx.3, align 4
  %add.3 = fadd fast float %3, %add.2, exceptions=ignore
  %arrayidx.4 = gep inbounds ptr nocapture nowrite %x, 4 x i64 4
  %4 = load float, ptr %arrayidx.4, align 4
  %add.4 = fadd fast float %4, %add.3, exceptions=ignore
  %arrayidx.5 = gep inbounds ptr nocapture nowrite %x, 4 x i64 5
  %5 = load float, ptr %arrayidx.5, align 4
  %add.5 = fadd fast float %5, %add.4, exceptions=ignore
  %arrayidx.6 = gep inbounds ptr nocapture nowrite %x, 4 x i64 6
  %6 = load float, ptr %arrayidx.6, align 4
  %add.6 = fadd fast float %6, %add.5, exceptions=ignore
  %arrayidx.7 = gep inbounds ptr nocapture nowrite %x, 4 x i64 7
  %7 = load float, ptr %arrayidx.7, align 4
  %add.7 = fadd fast float %7, %add.6, exceptions=ignore
  %arrayidx.8 = gep inbounds ptr nocapture nowrite %x, 4 x i64 8
  %8 = load float, ptr %arrayidx.8, align 4
  %add.8 = fadd fast float %8, %add.7, exceptions=ignore
  %arrayidx.9 = gep inbounds ptr nocapture nowrite %x, 4 x i64 9
  %9 = load float, ptr %arrayidx.9, align 4
  %add.9 = fadd fast float %9, %add.8, exceptions=ignore
  %arrayidx.10 = gep inbounds ptr nocapture nowrite %x, 4 x i64 10
  %10 = load float, ptr %arrayidx.10, align 4
  %add.10 = fadd fast float %10, %add.9, exceptions=ignore
  %arrayidx.11 = gep inbounds ptr nocapture nowrite %x, 4 x i64 11
  %11 = load float, ptr %arrayidx.11, align 4
  %add.11 = fadd fast float %11, %add.10, exceptions=ignore
  %arrayidx.12 = gep inbounds ptr nocapture nowrite %x, 4 x i64 12
  %12 = load float, ptr %arrayidx.12, align 4
  %add.12 = fadd fast float %12, %add.11, exceptions=ignore
  %arrayidx.13 = gep inbounds ptr nocapture nowrite %x, 4 x i64 13
  %13 = load float, ptr %arrayidx.13, align 4
  %add.13 = fadd fast float %13, %add.12, exceptions=ignore
  %arrayidx.14 = gep inbounds ptr nocapture nowrite %x, 4 x i64 14
  %14 = load float, ptr %arrayidx.14, align 4
  %add.14 = fadd fast float %14, %add.13, exceptions=ignore
  %arrayidx.15 = gep inbounds ptr nocapture nowrite %x, 4 x i64 15
  %15 = load float, ptr %arrayidx.15, align 4
  %add.15 = fadd fast float %15, %add.14, exceptions=ignore
  %arrayidx.16 = gep inbounds ptr nocapture nowrite %x, 4 x i64 16
  %16 = load float, ptr %arrayidx.16, align 4
  %add.16 = fadd fast float %16, %add.15, exceptions=ignore
  %arrayidx.17 = gep inbounds ptr nocapture nowrite %x, 4 x i64 17
  %17 = load float, ptr %arrayidx.17, align 4
  %add.17 = fadd fast float %17, %add.16, exceptions=ignore
  %arrayidx.18 = gep inbounds ptr nocapture nowrite %x, 4 x i64 18
  %18 = load float, ptr %arrayidx.18, align 4
  %add.18 = fadd fast float %18, %add.17, exceptions=ignore
  %arrayidx.19 = gep inbounds ptr nocapture nowrite %x, 4 x i64 19
  %19 = load float, ptr %arrayidx.19, align 4
  %add.19 = fadd fast float %19, %add.18, exceptions=ignore
  %arrayidx.20 = gep inbounds ptr nocapture nowrite %x, 4 x i64 20
  %20 = load float, ptr %arrayidx.20, align 4
  %add.20 = fadd fast float %20, %add.19, exceptions=ignore
  %arrayidx.21 = gep inbounds ptr nocapture nowrite %x, 4 x i64 21
  %21 = load float, ptr %arrayidx.21, align 4
  %add.21 = fadd fast float %21, %add.20, exceptions=ignore
  %arrayidx.22 = gep inbounds ptr nocapture nowrite %x, 4 x i64 22
  %22 = load float, ptr %arrayidx.22, align 4
  %add.22 = fadd fast float %22, %add.21, exceptions=ignore
  %arrayidx.23 = gep inbounds ptr nocapture nowrite %x, 4 x i64 23
  %23 = load float, ptr %arrayidx.23, align 4
  %add.23 = fadd fast float %23, %add.22, exceptions=ignore
  %arrayidx.24 = gep inbounds ptr nocapture nowrite %x, 4 x i64 24
  %24 = load float, ptr %arrayidx.24, align 4
  %add.24 = fadd fast float %24, %add.23, exceptions=ignore
  %arrayidx.25 = gep inbounds ptr nocapture nowrite %x, 4 x i64 25
  %25 = load float, ptr %arrayidx.25, align 4
  %add.25 = fadd fast float %25, %add.24, exceptions=ignore
  %arrayidx.26 = gep inbounds ptr nocapture nowrite %x, 4 x i64 26
  %26 = load float, ptr %arrayidx.26, align 4
  %add.26 = fadd fast float %26, %add.25, exceptions=ignore
  %arrayidx.27 = gep inbounds ptr nocapture nowrite %x, 4 x i64 27
  %27 = load float, ptr %arrayidx.27, align 4
  %add.27 = fadd fast float %27, %add.26, exceptions=ignore
  %arrayidx.28 = gep inbounds ptr nocapture nowrite %x, 4 x i64 28
  %28 = load float, ptr %arrayidx.28, align 4
  %add.28 = fadd fast float %28, %add.27, exceptions=ignore
  %arrayidx.29 = gep inbounds ptr nocapture nowrite %x, 4 x i64 29
  %29 = load float, ptr %arrayidx.29, align 4
  %add.29 = fadd fast float %29, %add.28, exceptions=ignore
  %arrayidx.30 = gep inbounds ptr nocapture nowrite %x, 4 x i64 30
  %30 = load float, ptr %arrayidx.30, align 4
  %add.30 = fadd fast float %30, %add.29, exceptions=ignore
  %arrayidx.31 = gep inbounds ptr nocapture nowrite %x, 4 x i64 31
  %31 = load float, ptr %arrayidx.31, align 4
  %add.31 = fadd fast float %31, %add.30, exceptions=ignore
  ret float %add.31
}
=>
define float @f1(ptr nocapture nowrite %x, i32 %a, i32 %b) {
%entry:
  %rem = srem i32 %a, %b
  %conv = sitofp i32 %rem to float, exceptions=ignore
  %0 = bitcast ptr nocapture nowrite %x to ptr
  %1 = load <32 x float>, ptr %0, align 4
  %2 = call float @llvm.vector.reduce.fadd.v32f32(float -0.000000, <32 x float> %1) noread nowrite NNaN nofree willreturn
  %op.rdx = fadd fast float %2, %conv, exceptions=ignore
  ret float %op.rdx
}
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:
 - Unknown libcall: @llvm.vector.reduce.fadd.v32f32



----------------------------------------
define float @loadadd31(ptr nocapture nowrite %x) {
%entry:
  %arrayidx = gep inbounds ptr nocapture nowrite %x, 4 x i64 1
  %0 = load float, ptr %arrayidx, align 4
  %arrayidx.1 = gep inbounds ptr nocapture nowrite %x, 4 x i64 2
  %1 = load float, ptr %arrayidx.1, align 4
  %add.1 = fadd fast float %1, %0, exceptions=ignore
  %arrayidx.2 = gep inbounds ptr nocapture nowrite %x, 4 x i64 3
  %2 = load float, ptr %arrayidx.2, align 4
  %add.2 = fadd fast float %2, %add.1, exceptions=ignore
  %arrayidx.3 = gep inbounds ptr nocapture nowrite %x, 4 x i64 4
  %3 = load float, ptr %arrayidx.3, align 4
  %add.3 = fadd fast float %3, %add.2, exceptions=ignore
  %arrayidx.4 = gep inbounds ptr nocapture nowrite %x, 4 x i64 5
  %4 = load float, ptr %arrayidx.4, align 4
  %add.4 = fadd fast float %4, %add.3, exceptions=ignore
  %arrayidx.5 = gep inbounds ptr nocapture nowrite %x, 4 x i64 6
  %5 = load float, ptr %arrayidx.5, align 4
  %add.5 = fadd fast float %5, %add.4, exceptions=ignore
  %arrayidx.6 = gep inbounds ptr nocapture nowrite %x, 4 x i64 7
  %6 = load float, ptr %arrayidx.6, align 4
  %add.6 = fadd fast float %6, %add.5, exceptions=ignore
  %arrayidx.7 = gep inbounds ptr nocapture nowrite %x, 4 x i64 8
  %7 = load float, ptr %arrayidx.7, align 4
  %add.7 = fadd fast float %7, %add.6, exceptions=ignore
  %arrayidx.8 = gep inbounds ptr nocapture nowrite %x, 4 x i64 9
  %8 = load float, ptr %arrayidx.8, align 4
  %add.8 = fadd fast float %8, %add.7, exceptions=ignore
  %arrayidx.9 = gep inbounds ptr nocapture nowrite %x, 4 x i64 10
  %9 = load float, ptr %arrayidx.9, align 4
  %add.9 = fadd fast float %9, %add.8, exceptions=ignore
  %arrayidx.10 = gep inbounds ptr nocapture nowrite %x, 4 x i64 11
  %10 = load float, ptr %arrayidx.10, align 4
  %add.10 = fadd fast float %10, %add.9, exceptions=ignore
  %arrayidx.11 = gep inbounds ptr nocapture nowrite %x, 4 x i64 12
  %11 = load float, ptr %arrayidx.11, align 4
  %add.11 = fadd fast float %11, %add.10, exceptions=ignore
  %arrayidx.12 = gep inbounds ptr nocapture nowrite %x, 4 x i64 13
  %12 = load float, ptr %arrayidx.12, align 4
  %add.12 = fadd fast float %12, %add.11, exceptions=ignore
  %arrayidx.13 = gep inbounds ptr nocapture nowrite %x, 4 x i64 14
  %13 = load float, ptr %arrayidx.13, align 4
  %add.13 = fadd fast float %13, %add.12, exceptions=ignore
  %arrayidx.14 = gep inbounds ptr nocapture nowrite %x, 4 x i64 15
  %14 = load float, ptr %arrayidx.14, align 4
  %add.14 = fadd fast float %14, %add.13, exceptions=ignore
  %arrayidx.15 = gep inbounds ptr nocapture nowrite %x, 4 x i64 16
  %15 = load float, ptr %arrayidx.15, align 4
  %add.15 = fadd fast float %15, %add.14, exceptions=ignore
  %arrayidx.16 = gep inbounds ptr nocapture nowrite %x, 4 x i64 17
  %16 = load float, ptr %arrayidx.16, align 4
  %add.16 = fadd fast float %16, %add.15, exceptions=ignore
  %arrayidx.17 = gep inbounds ptr nocapture nowrite %x, 4 x i64 18
  %17 = load float, ptr %arrayidx.17, align 4
  %add.17 = fadd fast float %17, %add.16, exceptions=ignore
  %arrayidx.18 = gep inbounds ptr nocapture nowrite %x, 4 x i64 19
  %18 = load float, ptr %arrayidx.18, align 4
  %add.18 = fadd fast float %18, %add.17, exceptions=ignore
  %arrayidx.19 = gep inbounds ptr nocapture nowrite %x, 4 x i64 20
  %19 = load float, ptr %arrayidx.19, align 4
  %add.19 = fadd fast float %19, %add.18, exceptions=ignore
  %arrayidx.20 = gep inbounds ptr nocapture nowrite %x, 4 x i64 21
  %20 = load float, ptr %arrayidx.20, align 4
  %add.20 = fadd fast float %20, %add.19, exceptions=ignore
  %arrayidx.21 = gep inbounds ptr nocapture nowrite %x, 4 x i64 22
  %21 = load float, ptr %arrayidx.21, align 4
  %add.21 = fadd fast float %21, %add.20, exceptions=ignore
  %arrayidx.22 = gep inbounds ptr nocapture nowrite %x, 4 x i64 23
  %22 = load float, ptr %arrayidx.22, align 4
  %add.22 = fadd fast float %22, %add.21, exceptions=ignore
  %arrayidx.23 = gep inbounds ptr nocapture nowrite %x, 4 x i64 24
  %23 = load float, ptr %arrayidx.23, align 4
  %add.23 = fadd fast float %23, %add.22, exceptions=ignore
  %arrayidx.24 = gep inbounds ptr nocapture nowrite %x, 4 x i64 25
  %24 = load float, ptr %arrayidx.24, align 4
  %add.24 = fadd fast float %24, %add.23, exceptions=ignore
  %arrayidx.25 = gep inbounds ptr nocapture nowrite %x, 4 x i64 26
  %25 = load float, ptr %arrayidx.25, align 4
  %add.25 = fadd fast float %25, %add.24, exceptions=ignore
  %arrayidx.26 = gep inbounds ptr nocapture nowrite %x, 4 x i64 27
  %26 = load float, ptr %arrayidx.26, align 4
  %add.26 = fadd fast float %26, %add.25, exceptions=ignore
  %arrayidx.27 = gep inbounds ptr nocapture nowrite %x, 4 x i64 28
  %27 = load float, ptr %arrayidx.27, align 4
  %add.27 = fadd fast float %27, %add.26, exceptions=ignore
  %arrayidx.28 = gep inbounds ptr nocapture nowrite %x, 4 x i64 29
  %28 = load float, ptr %arrayidx.28, align 4
  %add.28 = fadd fast float %28, %add.27, exceptions=ignore
  %arrayidx.29 = gep inbounds ptr nocapture nowrite %x, 4 x i64 30
  %29 = load float, ptr %arrayidx.29, align 4
  %add.29 = fadd fast float %29, %add.28, exceptions=ignore
  ret float %add.29
}
=>
define float @loadadd31(ptr nocapture nowrite %x) {
%entry:
  %arrayidx = gep inbounds ptr nocapture nowrite %x, 4 x i64 1
  %0 = bitcast ptr %arrayidx to ptr
  %1 = load <16 x float>, ptr %0, align 4
  %arrayidx.16 = gep inbounds ptr nocapture nowrite %x, 4 x i64 17
  %2 = bitcast ptr %arrayidx.16 to ptr
  %3 = load <8 x float>, ptr %2, align 4
  %arrayidx.24 = gep inbounds ptr nocapture nowrite %x, 4 x i64 25
  %4 = bitcast ptr %arrayidx.24 to ptr
  %5 = load <4 x float>, ptr %4, align 4
  %arrayidx.28 = gep inbounds ptr nocapture nowrite %x, 4 x i64 29
  %6 = load float, ptr %arrayidx.28, align 4
  %arrayidx.29 = gep inbounds ptr nocapture nowrite %x, 4 x i64 30
  %7 = load float, ptr %arrayidx.29, align 4
  %8 = call float @llvm.vector.reduce.fadd.v16f32(float -0.000000, <16 x float> %1) noread nowrite NNaN nofree willreturn
  %9 = call float @llvm.vector.reduce.fadd.v8f32(float -0.000000, <8 x float> %3) noread nowrite NNaN nofree willreturn
  %op.rdx = fadd fast float %8, %9, exceptions=ignore
  %10 = call float @llvm.vector.reduce.fadd.v4f32(float -0.000000, <4 x float> %5) noread nowrite NNaN nofree willreturn
  %op.rdx1 = fadd fast float %op.rdx, %10, exceptions=ignore
  %op.rdx2 = fadd fast float %op.rdx1, %6, exceptions=ignore
  %op.rdx3 = fadd fast float %op.rdx2, %7, exceptions=ignore
  ret float %op.rdx3
}
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:
 - Unknown libcall: @llvm.vector.reduce.fadd.v16f32
 - Unknown libcall: @llvm.vector.reduce.fadd.v4f32
 - Unknown libcall: @llvm.vector.reduce.fadd.v8f32



----------------------------------------
define float @extra_args(ptr nocapture nowrite %x, i32 %a, i32 %b) {
%entry:
  %mul = mul nsw i32 %b, %a
  %conv = sitofp i32 %mul to float, exceptions=ignore
  %0 = load float, ptr nocapture nowrite %x, align 4
  %add = fadd fast float %conv, 3.000000, exceptions=ignore
  %add1 = fadd fast float %0, %add, exceptions=ignore
  %arrayidx3 = gep inbounds ptr nocapture nowrite %x, 4 x i64 1
  %1 = load float, ptr %arrayidx3, align 4
  %add4 = fadd fast float %1, %add1, exceptions=ignore
  %add5 = fadd fast float %add4, %conv, exceptions=ignore
  %arrayidx3.1 = gep inbounds ptr nocapture nowrite %x, 4 x i64 2
  %2 = load float, ptr %arrayidx3.1, align 4
  %add4.1 = fadd fast float %2, %add5, exceptions=ignore
  %arrayidx3.2 = gep inbounds ptr nocapture nowrite %x, 4 x i64 3
  %3 = load float, ptr %arrayidx3.2, align 4
  %add4.2 = fadd fast float %3, %add4.1, exceptions=ignore
  %arrayidx3.3 = gep inbounds ptr nocapture nowrite %x, 4 x i64 4
  %4 = load float, ptr %arrayidx3.3, align 4
  %add4.3 = fadd fast float %4, %add4.2, exceptions=ignore
  %arrayidx3.4 = gep inbounds ptr nocapture nowrite %x, 4 x i64 5
  %5 = load float, ptr %arrayidx3.4, align 4
  %add4.4 = fadd fast float %5, %add4.3, exceptions=ignore
  %arrayidx3.5 = gep inbounds ptr nocapture nowrite %x, 4 x i64 6
  %6 = load float, ptr %arrayidx3.5, align 4
  %add4.5 = fadd fast float %6, %add4.4, exceptions=ignore
  %arrayidx3.6 = gep inbounds ptr nocapture nowrite %x, 4 x i64 7
  %7 = load float, ptr %arrayidx3.6, align 4
  %add4.6 = fadd fast float %7, %add4.5, exceptions=ignore
  ret float %add4.6
}
=>
define float @extra_args(ptr nocapture nowrite %x, i32 %a, i32 %b) {
%entry:
  %mul = mul nsw i32 %b, %a
  %conv = sitofp i32 %mul to float, exceptions=ignore
  %0 = bitcast ptr nocapture nowrite %x to ptr
  %1 = load <8 x float>, ptr %0, align 4
  %2 = call float @llvm.vector.reduce.fadd.v8f32(float -0.000000, <8 x float> %1) noread nowrite NNaN nofree willreturn
  %op.rdx = fadd fast float %2, %conv, exceptions=ignore
  %op.rdx1 = fadd fast float %op.rdx, %conv, exceptions=ignore
  %op.rdx2 = fadd fast float %op.rdx1, 3.000000, exceptions=ignore
  ret float %op.rdx2
}
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:
 - Unknown libcall: @llvm.vector.reduce.fadd.v8f32



----------------------------------------
define float @extra_args_same_several_times(ptr nocapture nowrite %x, i32 %a, i32 %b) {
%entry:
  %mul = mul nsw i32 %b, %a
  %conv = sitofp i32 %mul to float, exceptions=ignore
  %0 = load float, ptr nocapture nowrite %x, align 4
  %add = fadd fast float %conv, 3.000000, exceptions=ignore
  %add1 = fadd fast float %0, %add, exceptions=ignore
  %arrayidx3 = gep inbounds ptr nocapture nowrite %x, 4 x i64 1
  %1 = load float, ptr %arrayidx3, align 4
  %add4 = fadd fast float %1, %add1, exceptions=ignore
  %add41 = fadd fast float %add4, 5.000000, exceptions=ignore
  %add5 = fadd fast float %add41, %conv, exceptions=ignore
  %arrayidx3.1 = gep inbounds ptr nocapture nowrite %x, 4 x i64 2
  %2 = load float, ptr %arrayidx3.1, align 4
  %add4.1 = fadd fast float %2, %add5, exceptions=ignore
  %add4.11 = fadd fast float %add4.1, 5.000000, exceptions=ignore
  %arrayidx3.2 = gep inbounds ptr nocapture nowrite %x, 4 x i64 3
  %3 = load float, ptr %arrayidx3.2, align 4
  %add4.2 = fadd fast float %3, %add4.11, exceptions=ignore
  %arrayidx3.3 = gep inbounds ptr nocapture nowrite %x, 4 x i64 4
  %4 = load float, ptr %arrayidx3.3, align 4
  %add4.3 = fadd fast float %4, %add4.2, exceptions=ignore
  %arrayidx3.4 = gep inbounds ptr nocapture nowrite %x, 4 x i64 5
  %5 = load float, ptr %arrayidx3.4, align 4
  %add4.4 = fadd fast float %5, %add4.3, exceptions=ignore
  %arrayidx3.5 = gep inbounds ptr nocapture nowrite %x, 4 x i64 6
  %6 = load float, ptr %arrayidx3.5, align 4
  %add4.5 = fadd fast float %6, %add4.4, exceptions=ignore
  %arrayidx3.6 = gep inbounds ptr nocapture nowrite %x, 4 x i64 7
  %7 = load float, ptr %arrayidx3.6, align 4
  %add4.6 = fadd fast float %7, %add4.5, exceptions=ignore
  ret float %add4.6
}
=>
define float @extra_args_same_several_times(ptr nocapture nowrite %x, i32 %a, i32 %b) {
%entry:
  %mul = mul nsw i32 %b, %a
  %conv = sitofp i32 %mul to float, exceptions=ignore
  %0 = bitcast ptr nocapture nowrite %x to ptr
  %1 = load <8 x float>, ptr %0, align 4
  %2 = call float @llvm.vector.reduce.fadd.v8f32(float -0.000000, <8 x float> %1) noread nowrite NNaN nofree willreturn
  %op.rdx = fadd fast float %2, 5.000000, exceptions=ignore
  %op.rdx1 = fadd fast float %op.rdx, 5.000000, exceptions=ignore
  %op.rdx2 = fadd fast float %op.rdx1, 3.000000, exceptions=ignore
  %op.rdx3 = fadd fast float %op.rdx2, %conv, exceptions=ignore
  %op.rdx4 = fadd fast float %op.rdx3, %conv, exceptions=ignore
  ret float %op.rdx4
}
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:
 - Unknown libcall: @llvm.vector.reduce.fadd.v8f32



----------------------------------------
define float @extra_args_no_replace(ptr nocapture nowrite %x, i32 %a, i32 %b, i32 %c) {
%entry:
  %mul = mul nsw i32 %b, %a
  %conv = sitofp i32 %mul to float, exceptions=ignore
  %0 = load float, ptr nocapture nowrite %x, align 4
  %convc = sitofp i32 %c to float, exceptions=ignore
  %addc = fadd fast float %convc, 3.000000, exceptions=ignore
  %add = fadd fast float %conv, %addc, exceptions=ignore
  %add1 = fadd fast float %0, %add, exceptions=ignore
  %arrayidx3 = gep inbounds ptr nocapture nowrite %x, 4 x i64 1
  %1 = load float, ptr %arrayidx3, align 4
  %add4 = fadd fast float %1, %add1, exceptions=ignore
  %arrayidx3.1 = gep inbounds ptr nocapture nowrite %x, 4 x i64 2
  %2 = load float, ptr %arrayidx3.1, align 4
  %add4.1 = fadd fast float %2, %add4, exceptions=ignore
  %arrayidx3.2 = gep inbounds ptr nocapture nowrite %x, 4 x i64 3
  %3 = load float, ptr %arrayidx3.2, align 4
  %add4.2 = fadd fast float %3, %add4.1, exceptions=ignore
  %arrayidx3.3 = gep inbounds ptr nocapture nowrite %x, 4 x i64 4
  %4 = load float, ptr %arrayidx3.3, align 4
  %add4.3 = fadd fast float %4, %add4.2, exceptions=ignore
  %add5 = fadd fast float %add4.3, %conv, exceptions=ignore
  %arrayidx3.4 = gep inbounds ptr nocapture nowrite %x, 4 x i64 5
  %5 = load float, ptr %arrayidx3.4, align 4
  %add4.4 = fadd fast float %5, %add5, exceptions=ignore
  %arrayidx3.5 = gep inbounds ptr nocapture nowrite %x, 4 x i64 6
  %6 = load float, ptr %arrayidx3.5, align 4
  %add4.5 = fadd fast float %6, %add4.4, exceptions=ignore
  %arrayidx3.6 = gep inbounds ptr nocapture nowrite %x, 4 x i64 7
  %7 = load float, ptr %arrayidx3.6, align 4
  %add4.6 = fadd fast float %7, %add4.5, exceptions=ignore
  ret float %add4.6
}
=>
define float @extra_args_no_replace(ptr nocapture nowrite %x, i32 %a, i32 %b, i32 %c) {
%entry:
  %mul = mul nsw i32 %b, %a
  %conv = sitofp i32 %mul to float, exceptions=ignore
  %convc = sitofp i32 %c to float, exceptions=ignore
  %0 = bitcast ptr nocapture nowrite %x to ptr
  %1 = load <8 x float>, ptr %0, align 4
  %2 = call float @llvm.vector.reduce.fadd.v8f32(float -0.000000, <8 x float> %1) noread nowrite NNaN nofree willreturn
  %op.rdx = fadd fast float %2, %conv, exceptions=ignore
  %op.rdx1 = fadd fast float %op.rdx, %conv, exceptions=ignore
  %op.rdx2 = fadd fast float %op.rdx1, %convc, exceptions=ignore
  %op.rdx3 = fadd fast float %op.rdx2, 3.000000, exceptions=ignore
  ret float %op.rdx3
}
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:
 - Unknown libcall: @llvm.vector.reduce.fadd.v8f32



----------------------------------------
define float @extra_args_no_fast(ptr %x, float %a, float %b) {
%0:
  %addc = fadd fast float %b, 3.000000, exceptions=ignore
  %add = fadd fast float %a, %addc, exceptions=ignore
  %arrayidx3 = gep inbounds ptr %x, 4 x i64 1
  %arrayidx3.1 = gep inbounds ptr %x, 4 x i64 2
  %arrayidx3.2 = gep inbounds ptr %x, 4 x i64 3
  %t0 = load float, ptr %x, align 4
  %t1 = load float, ptr %arrayidx3, align 4
  %t2 = load float, ptr %arrayidx3.1, align 4
  %t3 = load float, ptr %arrayidx3.2, align 4
  %add1 = fadd fast float %t0, %add, exceptions=ignore
  %add4 = fadd fast float %t1, %add1, exceptions=ignore
  %add4.1 = fadd float %t2, %add4, exceptions=ignore
  %add4.2 = fadd fast float %t3, %add4.1, exceptions=ignore
  %add5 = fadd fast float %add4.2, %a, exceptions=ignore
  ret float %add5
}
=>
define float @extra_args_no_fast(ptr %x, float %a, float %b) {
%0:
  %addc = fadd fast float %b, 3.000000, exceptions=ignore
  %add = fadd fast float %a, %addc, exceptions=ignore
  %arrayidx3 = gep inbounds ptr %x, 4 x i64 1
  %arrayidx3.1 = gep inbounds ptr %x, 4 x i64 2
  %arrayidx3.2 = gep inbounds ptr %x, 4 x i64 3
  %t0 = load float, ptr %x, align 4
  %t1 = load float, ptr %arrayidx3, align 4
  %t2 = load float, ptr %arrayidx3.1, align 4
  %t3 = load float, ptr %arrayidx3.2, align 4
  %add1 = fadd fast float %t0, %add, exceptions=ignore
  %add4 = fadd fast float %t1, %add1, exceptions=ignore
  %add4.1 = fadd float %t2, %add4, exceptions=ignore
  %add4.2 = fadd fast float %t3, %add4.1, exceptions=ignore
  %add5 = fadd fast float %add4.2, %a, exceptions=ignore
  ret float %add5
}
Transformation seems to be correct! (syntactically equal)


----------------------------------------
define i32 @wobble(i32 %arg, i32 %bar) {
%bb:
  %x1 = xor i32 %arg, %bar
  %i1 = icmp eq i32 %x1, 0
  %s1 = sext i1 %i1 to i32
  %x2 = xor i32 %arg, %bar
  %i2 = icmp eq i32 %x2, 0
  %s2 = sext i1 %i2 to i32
  %x3 = xor i32 %arg, %bar
  %i3 = icmp eq i32 %x3, 0
  %s3 = sext i1 %i3 to i32
  %x4 = xor i32 %arg, %bar
  %i4 = icmp eq i32 %x4, 0
  %s4 = sext i1 %i4 to i32
  %r1 = add nuw i32 %arg, %s1
  %r2 = add nsw i32 %r1, %s2
  %r3 = add nsw i32 %r2, %s3
  %r4 = add nsw i32 %r3, %s4
  %r5 = add nsw i32 %r4, %x4
  ret i32 %r5
}
=>
define i32 @wobble(i32 %arg, i32 %bar) {
%bb:
  %0 = insertelement <4 x i32> poison, i32 %arg, i32 0
  %shuffle = shufflevector <4 x i32> %0, <4 x i32> poison, 0, 0, 0, 0
  %1 = insertelement <4 x i32> poison, i32 %bar, i32 0
  %shuffle1 = shufflevector <4 x i32> %1, <4 x i32> poison, 0, 0, 0, 0
  %2 = xor <4 x i32> %shuffle, %shuffle1
  %3 = extractelement <4 x i32> %2, i32 3
  %4 = icmp eq <4 x i32> %2, { 0, 0, 0, 0 }
  %5 = sext <4 x i1> %4 to <4 x i32>
  %6 = reduce_add <4 x i32> %5
  %op.rdx = add nsw i32 %6, %3
  %op.rdx2 = add nuw i32 %op.rdx, %arg
  ret i32 %op.rdx2
}
Transformation doesn't verify!
ERROR: Target is more poisonous than source

Example:
i32 %arg = #x41009990 (1090558352)
i32 %bar = #x98120008 (2551316488, -1743650808)

Source:
i32 %x1 = #xd9129998 (3641874840, -653092456)
i1 %i1 = #x0 (0)
i32 %s1 = #x00000000 (0)
i32 %x2 = #xd9129998 (3641874840, -653092456)
i1 %i2 = #x0 (0)
i32 %s2 = #x00000000 (0)
i32 %x3 = #xd9129998 (3641874840, -653092456)
i1 %i3 = #x0 (0)
i32 %s3 = #x00000000 (0)
i32 %x4 = #xd9129998 (3641874840, -653092456)
i1 %i4 = #x0 (0)
i32 %s4 = #x00000000 (0)
i32 %r1 = #x41009990 (1090558352)
i32 %r2 = #x41009990 (1090558352)
i32 %r3 = #x41009990 (1090558352)
i32 %r4 = #x41009990 (1090558352)
i32 %r5 = #x1a133328 (437465896)

Target:
<4 x i32> %0 = < #x41009990 (1090558352), poison, poison, poison >
<4 x i32> %shuffle = < #x41009990 (1090558352), #x41009990 (1090558352), #x41009990 (1090558352), #x41009990 (1090558352) >
<4 x i32> %1 = < #x98120008 (2551316488, -1743650808), poison, poison, poison >
<4 x i32> %shuffle1 = < #x98120008 (2551316488, -1743650808), #x98120008 (2551316488, -1743650808), #x98120008 (2551316488, -1743650808), #x98120008 (2551316488, -1743650808) >
<4 x i32> %2 = < #xd9129998 (3641874840, -653092456), #xd9129998 (3641874840, -653092456), #xd9129998 (3641874840, -653092456), #xd9129998 (3641874840, -653092456) >
i32 %3 = #xd9129998 (3641874840, -653092456)
<4 x i1> %4 = < #x0 (0), #x0 (0), #x0 (0), #x0 (0) >
<4 x i32> %5 = < #x00000000 (0), #x00000000 (0), #x00000000 (0), #x00000000 (0) >
i32 %6 = #x00000000 (0)
i32 %op.rdx = #xd9129998 (3641874840, -653092456)
i32 %op.rdx2 = poison
Source value: #x1a133328 (437465896)
Target value: poison


------------------- SMT STATS -------------------
Num queries: 48
Num invalid: 0
Num skips:   0
Num trivial: 49 (50.5%)
Num timeout: 1 (2.1%)
Num errors:  0 (0.0%)
Num SAT:     47 (97.9%)
Num UNSAT:   0 (0.0%)
Alive2: Transform doesn't verify; aborting!

stderr:

+ : 'RUN: at line 2'
+ /home/nlopes/llvm/build/bin/FileCheck /home/nlopes/llvm/llvm/test/Transforms/SLPVectorizer/X86/horizontal-list.ll
+ /home/nlopes/alive2/build/opt-alive.sh -slp-vectorizer -slp-vectorize-hor -slp-vectorize-hor-store -S -mtriple=x86_64-unknown-linux-gnu -mcpu=bdver2

FileCheck error: '<stdin>' is empty.
FileCheck command line:  /home/nlopes/llvm/build/bin/FileCheck /home/nlopes/llvm/llvm/test/Transforms/SLPVectorizer/X86/horizontal-list.ll

 

<-- Back