Test Failure: Transforms/LoopVectorize/AArch64/armpl-calls.ll

Test source: git

Log:

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

----------------------------------------
define void @acos_f64(ptr nocapture %in.ptr, ptr %out.ptr) {
%entry:
  br label %for.body

%for.body:
  %iv = phi i64 [ 0, %entry ], [ %iv.next, %for.body ]
  %in.gep = gep inbounds ptr nocapture %in.ptr, 8 x i64 %iv
  %in = load double, ptr %in.gep, align 8
  %call = call double @acos(double %in)
  %out.gep = gep inbounds ptr %out.ptr, 8 x i64 %iv
  store double %call, ptr %out.gep, align 8
  %iv.next = add nsw nuw i64 %iv, 1
  %exitcond = icmp eq i64 %iv.next, 1000
  br i1 %exitcond, label %for.end, label %for.body

%for.end:
  ret void
}
Transformation seems to be correct! (syntactically equal)

-- 3. InjectTLIMappings

----------------------------------------
define void @acos_f64(ptr nocapture %in.ptr, ptr %out.ptr) {
%entry:
  br label %for.body

%for.body:
  %iv = phi i64 [ 0, %entry ], [ %iv.next, %for.body ]
  %in.gep = gep inbounds ptr nocapture %in.ptr, 8 x i64 %iv
  %in = load double, ptr %in.gep, align 8
  %call = call double @acos(double %in)
  %out.gep = gep inbounds ptr %out.ptr, 8 x i64 %iv
  store double %call, ptr %out.gep, align 8
  %iv.next = add nsw nuw i64 %iv, 1
  %exitcond = icmp eq i64 %iv.next, 1000
  br i1 %exitcond, label %for.end, label %for.body

%for.end:
  ret void
}
Transformation seems to be correct! (syntactically equal)

-- 4. LoopVectorizePass

----------------------------------------
define void @acos_f64(ptr nocapture %in.ptr, ptr %out.ptr) {
%entry:
  br label %for.body

%for.body:
  %iv = phi i64 [ 0, %entry ], [ %iv.next, %for.body ]
  %in.gep = gep inbounds ptr nocapture %in.ptr, 8 x i64 %iv
  %in = load double, ptr %in.gep, align 8
  %call = call double @acos(double %in)
  %out.gep = gep inbounds ptr %out.ptr, 8 x i64 %iv
  store double %call, ptr %out.gep, align 8
  %iv.next = add nsw nuw i64 %iv, 1
  %exitcond = icmp eq i64 %iv.next, 1000
  br i1 %exitcond, label %for.end, label %for.body

%for.end:
  ret void
}
Transformation seems to be correct! (syntactically equal)

-- 5. LoopVectorizePass

----------------------------------------
define void @acos_f64(ptr nocapture %in.ptr, ptr %out.ptr) {
%entry:
  br label %for.body

%for.body:
  %iv = phi i64 [ 0, %entry ], [ %iv.next, %for.body ]
  %in.gep = gep inbounds ptr nocapture %in.ptr, 8 x i64 %iv
  %in = load double, ptr %in.gep, align 8
  %call = call double @acos(double %in)
  %out.gep = gep inbounds ptr %out.ptr, 8 x i64 %iv
  store double %call, ptr %out.gep, align 8
  %iv.next = add nsw nuw i64 %iv, 1
  %exitcond = icmp eq i64 %iv.next, 1000
  br i1 %exitcond, label %for.end, label %for.body

%for.end:
  ret void
}
=>
define void @acos_f64(ptr nocapture %in.ptr, ptr %out.ptr) {
%entry:
  %in.ptr2 = ptrtoint ptr nocapture %in.ptr to i64
  %out.ptr1 = ptrtoint ptr %out.ptr to i64
  br i1 0, label %scalar.ph, label %vector.memcheck

%vector.memcheck:
  %0 = sub i64 %out.ptr1, %in.ptr2
  %diff.check = icmp ult i64 %0, 32
  br i1 %diff.check, label %scalar.ph, label %vector.ph

%vector.ph:
  br label %vector.body

%vector.body:
  %index = phi i64 [ 0, %vector.ph ], [ %index.next, %vector.body ]
  %1 = add i64 %index, 0
  %3 = gep inbounds ptr nocapture %in.ptr, 8 x i64 %1
  %5 = gep inbounds ptr %3, 8 x i32 0
  %wide.load = load <2 x double>, ptr %5, align 8
  %6 = gep inbounds ptr %3, 8 x i32 2
  %wide.load3 = load <2 x double>, ptr %6, align 8
  %7 = call <2 x double> @armpl_vacosq_f64(<2 x double> %wide.load)
  %8 = call <2 x double> @armpl_vacosq_f64(<2 x double> %wide.load3)
  %9 = gep inbounds ptr %out.ptr, 8 x i64 %1
  %11 = gep inbounds ptr %9, 8 x i32 0
  store <2 x double> %7, ptr %11, align 8
  %12 = gep inbounds ptr %9, 8 x i32 2
  store <2 x double> %8, ptr %12, align 8
  %index.next = add nuw i64 %index, 4
  %13 = icmp eq i64 %index.next, 1000
  br i1 %13, label %middle.block, label %vector.body

%middle.block:
  %cmp.n = icmp eq i64 1000, 1000, use_provenance
  br i1 %cmp.n, label %for.end, label %scalar.ph

%scalar.ph:
  %bc.resume.val = phi i64 [ 1000, %middle.block ], [ 0, %entry ], [ 0, %vector.memcheck ]
  br label %for.body

%for.body:
  %iv = phi i64 [ %bc.resume.val, %scalar.ph ], [ %iv.next, %for.body ]
  %in.gep = gep inbounds ptr nocapture %in.ptr, 8 x i64 %iv
  %in = load double, ptr %in.gep, align 8
  %call = call double @acos(double %in)
  %out.gep = gep inbounds ptr %out.ptr, 8 x i64 %iv
  store double %call, ptr %out.gep, align 8
  %iv.next = add nsw nuw i64 %iv, 1
  %exitcond = icmp eq i64 %iv.next, 1000
  br i1 %exitcond, label %for.end, label %for.body

%for.end:
  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: @acos

-- 6. PassManager<Function> : Skipping NOP
-- 7. PassManager<Function> : Skipping NOP
-- 8. InjectTLIMappings

----------------------------------------
define void @acos_f32(ptr nocapture %in.ptr, ptr %out.ptr) {
%entry:
  br label %for.body

%for.body:
  %iv = phi i64 [ 0, %entry ], [ %iv.next, %for.body ]
  %in.gep = gep inbounds ptr nocapture %in.ptr, 4 x i64 %iv
  %in = load float, ptr %in.gep, align 8
  %call = call float @acosf(float %in)
  %out.gep = gep inbounds ptr %out.ptr, 4 x i64 %iv
  store float %call, ptr %out.gep, align 4
  %iv.next = add nsw nuw i64 %iv, 1
  %exitcond = icmp eq i64 %iv.next, 1000
  br i1 %exitcond, label %for.end, label %for.body

%for.end:
  ret void
}
Transformation seems to be correct! (syntactically equal)

-- 9. InjectTLIMappings

----------------------------------------
define void @acos_f32(ptr nocapture %in.ptr, ptr %out.ptr) {
%entry:
  br label %for.body

%for.body:
  %iv = phi i64 [ 0, %entry ], [ %iv.next, %for.body ]
  %in.gep = gep inbounds ptr nocapture %in.ptr, 4 x i64 %iv
  %in = load float, ptr %in.gep, align 8
  %call = call float @acosf(float %in)
  %out.gep = gep inbounds ptr %out.ptr, 4 x i64 %iv
  store float %call, ptr %out.gep, align 4
  %iv.next = add nsw nuw i64 %iv, 1
  %exitcond = icmp eq i64 %iv.next, 1000
  br i1 %exitcond, label %for.end, label %for.body

%for.end:
  ret void
}
Transformation seems to be correct! (syntactically equal)

-- 10. LoopVectorizePass

----------------------------------------
define void @acos_f32(ptr nocapture %in.ptr, ptr %out.ptr) {
%entry:
  br label %for.body

%for.body:
  %iv = phi i64 [ 0, %entry ], [ %iv.next, %for.body ]
  %in.gep = gep inbounds ptr nocapture %in.ptr, 4 x i64 %iv
  %in = load float, ptr %in.gep, align 8
  %call = call float @acosf(float %in)
  %out.gep = gep inbounds ptr %out.ptr, 4 x i64 %iv
  store float %call, ptr %out.gep, align 4
  %iv.next = add nsw nuw i64 %iv, 1
  %exitcond = icmp eq i64 %iv.next, 1000
  br i1 %exitcond, label %for.end, label %for.body

%for.end:
  ret void
}
Transformation seems to be correct! (syntactically equal)

-- 11. LoopVectorizePass

----------------------------------------
define void @acos_f32(ptr nocapture %in.ptr, ptr %out.ptr) {
%entry:
  br label %for.body

%for.body:
  %iv = phi i64 [ 0, %entry ], [ %iv.next, %for.body ]
  %in.gep = gep inbounds ptr nocapture %in.ptr, 4 x i64 %iv
  %in = load float, ptr %in.gep, align 8
  %call = call float @acosf(float %in)
  %out.gep = gep inbounds ptr %out.ptr, 4 x i64 %iv
  store float %call, ptr %out.gep, align 4
  %iv.next = add nsw nuw i64 %iv, 1
  %exitcond = icmp eq i64 %iv.next, 1000
  br i1 %exitcond, label %for.end, label %for.body

%for.end:
  ret void
}
=>
define void @acos_f32(ptr nocapture %in.ptr, ptr %out.ptr) {
%entry:
  %in.ptr2 = ptrtoint ptr nocapture %in.ptr to i64
  %out.ptr1 = ptrtoint ptr %out.ptr to i64
  br i1 0, label %scalar.ph, label %vector.memcheck

%vector.memcheck:
  %0 = sub i64 %out.ptr1, %in.ptr2
  %diff.check = icmp ult i64 %0, 32
  br i1 %diff.check, label %scalar.ph, label %vector.ph

%vector.ph:
  br label %vector.body

%vector.body:
  %index = phi i64 [ 0, %vector.ph ], [ %index.next, %vector.body ]
  %1 = add i64 %index, 0
  %3 = gep inbounds ptr nocapture %in.ptr, 4 x i64 %1
  %5 = gep inbounds ptr %3, 4 x i32 0
  %wide.load = load <4 x float>, ptr %5, align 8
  %6 = gep inbounds ptr %3, 4 x i32 4
  %wide.load3 = load <4 x float>, ptr %6, align 8
  %7 = call <4 x float> @armpl_vacosq_f32(<4 x float> %wide.load)
  %8 = call <4 x float> @armpl_vacosq_f32(<4 x float> %wide.load3)
  %9 = gep inbounds ptr %out.ptr, 4 x i64 %1
  %11 = gep inbounds ptr %9, 4 x i32 0
  store <4 x float> %7, ptr %11, align 4
  %12 = gep inbounds ptr %9, 4 x i32 4
  store <4 x float> %8, ptr %12, align 4
  %index.next = add nuw i64 %index, 8
  %13 = icmp eq i64 %index.next, 1000
  br i1 %13, label %middle.block, label %vector.body

%middle.block:
  %cmp.n = icmp eq i64 1000, 1000, use_provenance
  br i1 %cmp.n, label %for.end, label %scalar.ph

%scalar.ph:
  %bc.resume.val = phi i64 [ 1000, %middle.block ], [ 0, %entry ], [ 0, %vector.memcheck ]
  br label %for.body

%for.body:
  %iv = phi i64 [ %bc.resume.val, %scalar.ph ], [ %iv.next, %for.body ]
  %in.gep = gep inbounds ptr nocapture %in.ptr, 4 x i64 %iv
  %in = load float, ptr %in.gep, align 8
  %call = call float @acosf(float %in)
  %out.gep = gep inbounds ptr %out.ptr, 4 x i64 %iv
  store float %call, ptr %out.gep, align 4
  %iv.next = add nsw nuw i64 %iv, 1
  %exitcond = icmp eq i64 %iv.next, 1000
  br i1 %exitcond, label %for.end, label %for.body

%for.end:
  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: @acosf

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

----------------------------------------
define void @acosh_f64(ptr nocapture %in.ptr, ptr %out.ptr) {
%entry:
  br label %for.body

%for.body:
  %iv = phi i64 [ 0, %entry ], [ %iv.next, %for.body ]
  %in.gep = gep inbounds ptr nocapture %in.ptr, 8 x i64 %iv
  %in = load double, ptr %in.gep, align 8
  %call = call double @acosh(double %in)
  %out.gep = gep inbounds ptr %out.ptr, 8 x i64 %iv
  store double %call, ptr %out.gep, align 8
  %iv.next = add nsw nuw i64 %iv, 1
  %exitcond = icmp eq i64 %iv.next, 1000
  br i1 %exitcond, label %for.end, label %for.body

%for.end:
  ret void
}
Transformation seems to be correct! (syntactically equal)

-- 15. InjectTLIMappings

----------------------------------------
define void @acosh_f64(ptr nocapture %in.ptr, ptr %out.ptr) {
%entry:
  br label %for.body

%for.body:
  %iv = phi i64 [ 0, %entry ], [ %iv.next, %for.body ]
  %in.gep = gep inbounds ptr nocapture %in.ptr, 8 x i64 %iv
  %in = load double, ptr %in.gep, align 8
  %call = call double @acosh(double %in)
  %out.gep = gep inbounds ptr %out.ptr, 8 x i64 %iv
  store double %call, ptr %out.gep, align 8
  %iv.next = add nsw nuw i64 %iv, 1
  %exitcond = icmp eq i64 %iv.next, 1000
  br i1 %exitcond, label %for.end, label %for.body

%for.end:
  ret void
}
Transformation seems to be correct! (syntactically equal)

-- 16. LoopVectorizePass

----------------------------------------
define void @acosh_f64(ptr nocapture %in.ptr, ptr %out.ptr) {
%entry:
  br label %for.body

%for.body:
  %iv = phi i64 [ 0, %entry ], [ %iv.next, %for.body ]
  %in.gep = gep inbounds ptr nocapture %in.ptr, 8 x i64 %iv
  %in = load double, ptr %in.gep, align 8
  %call = call double @acosh(double %in)
  %out.gep = gep inbounds ptr %out.ptr, 8 x i64 %iv
  store double %call, ptr %out.gep, align 8
  %iv.next = add nsw nuw i64 %iv, 1
  %exitcond = icmp eq i64 %iv.next, 1000
  br i1 %exitcond, label %for.end, label %for.body

%for.end:
  ret void
}
Transformation seems to be correct! (syntactically equal)

-- 17. LoopVectorizePass

----------------------------------------
define void @acosh_f64(ptr nocapture %in.ptr, ptr %out.ptr) {
%entry:
  br label %for.body

%for.body:
  %iv = phi i64 [ 0, %entry ], [ %iv.next, %for.body ]
  %in.gep = gep inbounds ptr nocapture %in.ptr, 8 x i64 %iv
  %in = load double, ptr %in.gep, align 8
  %call = call double @acosh(double %in)
  %out.gep = gep inbounds ptr %out.ptr, 8 x i64 %iv
  store double %call, ptr %out.gep, align 8
  %iv.next = add nsw nuw i64 %iv, 1
  %exitcond = icmp eq i64 %iv.next, 1000
  br i1 %exitcond, label %for.end, label %for.body

%for.end:
  ret void
}
=>
define void @acosh_f64(ptr nocapture %in.ptr, ptr %out.ptr) {
%entry:
  %in.ptr2 = ptrtoint ptr nocapture %in.ptr to i64
  %out.ptr1 = ptrtoint ptr %out.ptr to i64
  br i1 0, label %scalar.ph, label %vector.memcheck

%vector.memcheck:
  %0 = sub i64 %out.ptr1, %in.ptr2
  %diff.check = icmp ult i64 %0, 32
  br i1 %diff.check, label %scalar.ph, label %vector.ph

%vector.ph:
  br label %vector.body

%vector.body:
  %index = phi i64 [ 0, %vector.ph ], [ %index.next, %vector.body ]
  %1 = add i64 %index, 0
  %3 = gep inbounds ptr nocapture %in.ptr, 8 x i64 %1
  %5 = gep inbounds ptr %3, 8 x i32 0
  %wide.load = load <2 x double>, ptr %5, align 8
  %6 = gep inbounds ptr %3, 8 x i32 2
  %wide.load3 = load <2 x double>, ptr %6, align 8
  %7 = call <2 x double> @armpl_vacoshq_f64(<2 x double> %wide.load)
  %8 = call <2 x double> @armpl_vacoshq_f64(<2 x double> %wide.load3)
  %9 = gep inbounds ptr %out.ptr, 8 x i64 %1
  %11 = gep inbounds ptr %9, 8 x i32 0
  store <2 x double> %7, ptr %11, align 8
  %12 = gep inbounds ptr %9, 8 x i32 2
  store <2 x double> %8, ptr %12, align 8
  %index.next = add nuw i64 %index, 4
  %13 = icmp eq i64 %index.next, 1000
  br i1 %13, label %middle.block, label %vector.body

%middle.block:
  %cmp.n = icmp eq i64 1000, 1000, use_provenance
  br i1 %cmp.n, label %for.end, label %scalar.ph

%scalar.ph:
  %bc.resume.val = phi i64 [ 1000, %middle.block ], [ 0, %entry ], [ 0, %vector.memcheck ]
  br label %for.body

%for.body:
  %iv = phi i64 [ %bc.resume.val, %scalar.ph ], [ %iv.next, %for.body ]
  %in.gep = gep inbounds ptr nocapture %in.ptr, 8 x i64 %iv
  %in = load double, ptr %in.gep, align 8
  %call = call double @acosh(double %in)
  %out.gep = gep inbounds ptr %out.ptr, 8 x i64 %iv
  store double %call, ptr %out.gep, align 8
  %iv.next = add nsw nuw i64 %iv, 1
  %exitcond = icmp eq i64 %iv.next, 1000
  br i1 %exitcond, label %for.end, label %for.body

%for.end:
  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

-- 18. PassManager<Function> : Skipping NOP
-- 19. PassManager<Function> : Skipping NOP
-- 20. InjectTLIMappings

----------------------------------------
define void @acosh_f32(ptr nocapture %in.ptr, ptr %out.ptr) {
%entry:
  br label %for.body

%for.body:
  %iv = phi i64 [ 0, %entry ], [ %iv.next, %for.body ]
  %in.gep = gep inbounds ptr nocapture %in.ptr, 4 x i64 %iv
  %in = load float, ptr %in.gep, align 8
  %call = call float @acoshf(float %in)
  %out.gep = gep inbounds ptr %out.ptr, 4 x i64 %iv
  store float %call, ptr %out.gep, align 4
  %iv.next = add nsw nuw i64 %iv, 1
  %exitcond = icmp eq i64 %iv.next, 1000
  br i1 %exitcond, label %for.end, label %for.body

%for.end:
  ret void
}
Transformation seems to be correct! (syntactically equal)

-- 21. InjectTLIMappings

----------------------------------------
define void @acosh_f32(ptr nocapture %in.ptr, ptr %out.ptr) {
%entry:
  br label %for.body

%for.body:
  %iv = phi i64 [ 0, %entry ], [ %iv.next, %for.body ]
  %in.gep = gep inbounds ptr nocapture %in.ptr, 4 x i64 %iv
  %in = load float, ptr %in.gep, align 8
  %call = call float @acoshf(float %in)
  %out.gep = gep inbounds ptr %out.ptr, 4 x i64 %iv
  store float %call, ptr %out.gep, align 4
  %iv.next = add nsw nuw i64 %iv, 1
  %exitcond = icmp eq i64 %iv.next, 1000
  br i1 %exitcond, label %for.end, label %for.body

%for.end:
  ret void
}
Transformation seems to be correct! (syntactically equal)

-- 22. LoopVectorizePass

----------------------------------------
define void @acosh_f32(ptr nocapture %in.ptr, ptr %out.ptr) {
%entry:
  br label %for.body

%for.body:
  %iv = phi i64 [ 0, %entry ], [ %iv.next, %for.body ]
  %in.gep = gep inbounds ptr nocapture %in.ptr, 4 x i64 %iv
  %in = load float, ptr %in.gep, align 8
  %call = call float @acoshf(float %in)
  %out.gep = gep inbounds ptr %out.ptr, 4 x i64 %iv
  store float %call, ptr %out.gep, align 4
  %iv.next = add nsw nuw i64 %iv, 1
  %exitcond = icmp eq i64 %iv.next, 1000
  br i1 %exitcond, label %for.end, label %for.body

%for.end:
  ret void
}
Transformation seems to be correct! (syntactically equal)

-- 23. LoopVectorizePass

----------------------------------------
define void @acosh_f32(ptr nocapture %in.ptr, ptr %out.ptr) {
%entry:
  br label %for.body

%for.body:
  %iv = phi i64 [ 0, %entry ], [ %iv.next, %for.body ]
  %in.gep = gep inbounds ptr nocapture %in.ptr, 4 x i64 %iv
  %in = load float, ptr %in.gep, align 8
  %call = call float @acoshf(float %in)
  %out.gep = gep inbounds ptr %out.ptr, 4 x i64 %iv
  store float %call, ptr %out.gep, align 4
  %iv.next = add nsw nuw i64 %iv, 1
  %exitcond = icmp eq i64 %iv.next, 1000
  br i1 %exitcond, label %for.end, label %for.body

%for.end:
  ret void
}
=>
define void @acosh_f32(ptr nocapture %in.ptr, ptr %out.ptr) {
%entry:
  %in.ptr2 = ptrtoint ptr nocapture %in.ptr to i64
  %out.ptr1 = ptrtoint ptr %out.ptr to i64
  br i1 0, label %scalar.ph, label %vector.memcheck

%vector.memcheck:
  %0 = sub i64 %out.ptr1, %in.ptr2
  %diff.check = icmp ult i64 %0, 32
  br i1 %diff.check, label %scalar.ph, label %vector.ph

%vector.ph:
  br label %vector.body

%vector.body:
  %index = phi i64 [ 0, %vector.ph ], [ %index.next, %vector.body ]
  %1 = add i64 %index, 0
  %3 = gep inbounds ptr nocapture %in.ptr, 4 x i64 %1
  %5 = gep inbounds ptr %3, 4 x i32 0
  %wide.load = load <4 x float>, ptr %5, align 8
  %6 = gep inbounds ptr %3, 4 x i32 4
  %wide.load3 = load <4 x float>, ptr %6, align 8
  %7 = call <4 x float> @armpl_vacoshq_f32(<4 x float> %wide.load)
  %8 = call <4 x float> @armpl_vacoshq_f32(<4 x float> %wide.load3)
  %9 = gep inbounds ptr %out.ptr, 4 x i64 %1
  %11 = gep inbounds ptr %9, 4 x i32 0
  store <4 x float> %7, ptr %11, align 4
  %12 = gep inbounds ptr %9, 4 x i32 4
  store <4 x float> %8, ptr %12, align 4
  %index.next = add nuw i64 %index, 8
  %13 = icmp eq i64 %index.next, 1000
  br i1 %13, label %middle.block, label %vector.body

%middle.block:
  %cmp.n = icmp eq i64 1000, 1000, use_provenance
  br i1 %cmp.n, label %for.end, label %scalar.ph

%scalar.ph:
  %bc.resume.val = phi i64 [ 1000, %middle.block ], [ 0, %entry ], [ 0, %vector.memcheck ]
  br label %for.body

%for.body:
  %iv = phi i64 [ %bc.resume.val, %scalar.ph ], [ %iv.next, %for.body ]
  %in.gep = gep inbounds ptr nocapture %in.ptr, 4 x i64 %iv
  %in = load float, ptr %in.gep, align 8
  %call = call float @acoshf(float %in)
  %out.gep = gep inbounds ptr %out.ptr, 4 x i64 %iv
  store float %call, ptr %out.gep, align 4
  %iv.next = add nsw nuw i64 %iv, 1
  %exitcond = icmp eq i64 %iv.next, 1000
  br i1 %exitcond, label %for.end, label %for.body

%for.end:
  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: @acoshf

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

----------------------------------------
define void @asin_f64(ptr nocapture %in.ptr, ptr %out.ptr) {
%entry:
  br label %for.body

%for.body:
  %iv = phi i64 [ 0, %entry ], [ %iv.next, %for.body ]
  %in.gep = gep inbounds ptr nocapture %in.ptr, 8 x i64 %iv
  %in = load double, ptr %in.gep, align 8
  %call = call double @asin(double %in)
  %out.gep = gep inbounds ptr %out.ptr, 8 x i64 %iv
  store double %call, ptr %out.gep, align 8
  %iv.next = add nsw nuw i64 %iv, 1
  %exitcond = icmp eq i64 %iv.next, 1000
  br i1 %exitcond, label %for.end, label %for.body

%for.end:
  ret void
}
Transformation seems to be correct! (syntactically equal)

-- 27. InjectTLIMappings

----------------------------------------
define void @asin_f64(ptr nocapture %in.ptr, ptr %out.ptr) {
%entry:
  br label %for.body

%for.body:
  %iv = phi i64 [ 0, %entry ], [ %iv.next, %for.body ]
  %in.gep = gep inbounds ptr nocapture %in.ptr, 8 x i64 %iv
  %in = load double, ptr %in.gep, align 8
  %call = call double @asin(double %in)
  %out.gep = gep inbounds ptr %out.ptr, 8 x i64 %iv
  store double %call, ptr %out.gep, align 8
  %iv.next = add nsw nuw i64 %iv, 1
  %exitcond = icmp eq i64 %iv.next, 1000
  br i1 %exitcond, label %for.end, label %for.body

%for.end:
  ret void
}
Transformation seems to be correct! (syntactically equal)

-- 28. LoopVectorizePass

----------------------------------------
define void @asin_f64(ptr nocapture %in.ptr, ptr %out.ptr) {
%entry:
  br label %for.body

%for.body:
  %iv = phi i64 [ 0, %entry ], [ %iv.next, %for.body ]
  %in.gep = gep inbounds ptr nocapture %in.ptr, 8 x i64 %iv
  %in = load double, ptr %in.gep, align 8
  %call = call double @asin(double %in)
  %out.gep = gep inbounds ptr %out.ptr, 8 x i64 %iv
  store double %call, ptr %out.gep, align 8
  %iv.next = add nsw nuw i64 %iv, 1
  %exitcond = icmp eq i64 %iv.next, 1000
  br i1 %exitcond, label %for.end, label %for.body

%for.end:
  ret void
}
Transformation seems to be correct! (syntactically equal)

-- 29. LoopVectorizePass

----------------------------------------
define void @asin_f64(ptr nocapture %in.ptr, ptr %out.ptr) {
%entry:
  br label %for.body

%for.body:
  %iv = phi i64 [ 0, %entry ], [ %iv.next, %for.body ]
  %in.gep = gep inbounds ptr nocapture %in.ptr, 8 x i64 %iv
  %in = load double, ptr %in.gep, align 8
  %call = call double @asin(double %in)
  %out.gep = gep inbounds ptr %out.ptr, 8 x i64 %iv
  store double %call, ptr %out.gep, align 8
  %iv.next = add nsw nuw i64 %iv, 1
  %exitcond = icmp eq i64 %iv.next, 1000
  br i1 %exitcond, label %for.end, label %for.body

%for.end:
  ret void
}
=>
define void @asin_f64(ptr nocapture %in.ptr, ptr %out.ptr) {
%entry:
  %in.ptr2 = ptrtoint ptr nocapture %in.ptr to i64
  %out.ptr1 = ptrtoint ptr %out.ptr to i64
  br i1 0, label %scalar.ph, label %vector.memcheck

%vector.memcheck:
  %0 = sub i64 %out.ptr1, %in.ptr2
  %diff.check = icmp ult i64 %0, 32
  br i1 %diff.check, label %scalar.ph, label %vector.ph

%vector.ph:
  br label %vector.body

%vector.body:
  %index = phi i64 [ 0, %vector.ph ], [ %index.next, %vector.body ]
  %1 = add i64 %index, 0
  %3 = gep inbounds ptr nocapture %in.ptr, 8 x i64 %1
  %5 = gep inbounds ptr %3, 8 x i32 0
  %wide.load = load <2 x double>, ptr %5, align 8
  %6 = gep inbounds ptr %3, 8 x i32 2
  %wide.load3 = load <2 x double>, ptr %6, align 8
  %7 = call <2 x double> @armpl_vasinq_f64(<2 x double> %wide.load)
  %8 = call <2 x double> @armpl_vasinq_f64(<2 x double> %wide.load3)
  %9 = gep inbounds ptr %out.ptr, 8 x i64 %1
  %11 = gep inbounds ptr %9, 8 x i32 0
  store <2 x double> %7, ptr %11, align 8
  %12 = gep inbounds ptr %9, 8 x i32 2
  store <2 x double> %8, ptr %12, align 8
  %index.next = add nuw i64 %index, 4
  %13 = icmp eq i64 %index.next, 1000
  br i1 %13, label %middle.block, label %vector.body

%middle.block:
  %cmp.n = icmp eq i64 1000, 1000, use_provenance
  br i1 %cmp.n, label %for.end, label %scalar.ph

%scalar.ph:
  %bc.resume.val = phi i64 [ 1000, %middle.block ], [ 0, %entry ], [ 0, %vector.memcheck ]
  br label %for.body

%for.body:
  %iv = phi i64 [ %bc.resume.val, %scalar.ph ], [ %iv.next, %for.body ]
  %in.gep = gep inbounds ptr nocapture %in.ptr, 8 x i64 %iv
  %in = load double, ptr %in.gep, align 8
  %call = call double @asin(double %in)
  %out.gep = gep inbounds ptr %out.ptr, 8 x i64 %iv
  store double %call, ptr %out.gep, align 8
  %iv.next = add nsw nuw i64 %iv, 1
  %exitcond = icmp eq i64 %iv.next, 1000
  br i1 %exitcond, label %for.end, label %for.body

%for.end:
  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: @asin

-- 30. PassManager<Function> : Skipping NOP
-- 31. PassManager<Function> : Skipping NOP
-- 32. InjectTLIMappings

----------------------------------------
define void @asin_f32(ptr nocapture %in.ptr, ptr %out.ptr) {
%entry:
  br label %for.body

%for.body:
  %iv = phi i64 [ 0, %entry ], [ %iv.next, %for.body ]
  %in.gep = gep inbounds ptr nocapture %in.ptr, 4 x i64 %iv
  %in = load float, ptr %in.gep, align 8
  %call = call float @asinf(float %in)
  %out.gep = gep inbounds ptr %out.ptr, 4 x i64 %iv
  store float %call, ptr %out.gep, align 4
  %iv.next = add nsw nuw i64 %iv, 1
  %exitcond = icmp eq i64 %iv.next, 1000
  br i1 %exitcond, label %for.end, label %for.body

%for.end:
  ret void
}
Transformation seems to be correct! (syntactically equal)

-- 33. InjectTLIMappings

----------------------------------------
define void @asin_f32(ptr nocapture %in.ptr, ptr %out.ptr) {
%entry:
  br label %for.body

%for.body:
  %iv = phi i64 [ 0, %entry ], [ %iv.next, %for.body ]
  %in.gep = gep inbounds ptr nocapture %in.ptr, 4 x i64 %iv
  %in = load float, ptr %in.gep, align 8
  %call = call float @asinf(float %in)
  %out.gep = gep inbounds ptr %out.ptr, 4 x i64 %iv
  store float %call, ptr %out.gep, align 4
  %iv.next = add nsw nuw i64 %iv, 1
  %exitcond = icmp eq i64 %iv.next, 1000
  br i1 %exitcond, label %for.end, label %for.body

%for.end:
  ret void
}
Transformation seems to be correct! (syntactically equal)

-- 34. LoopVectorizePass

----------------------------------------
define void @asin_f32(ptr nocapture %in.ptr, ptr %out.ptr) {
%entry:
  br label %for.body

%for.body:
  %iv = phi i64 [ 0, %entry ], [ %iv.next, %for.body ]
  %in.gep = gep inbounds ptr nocapture %in.ptr, 4 x i64 %iv
  %in = load float, ptr %in.gep, align 8
  %call = call float @asinf(float %in)
  %out.gep = gep inbounds ptr %out.ptr, 4 x i64 %iv
  store float %call, ptr %out.gep, align 4
  %iv.next = add nsw nuw i64 %iv, 1
  %exitcond = icmp eq i64 %iv.next, 1000
  br i1 %exitcond, label %for.end, label %for.body

%for.end:
  ret void
}
Transformation seems to be correct! (syntactically equal)

-- 35. LoopVectorizePass

----------------------------------------
define void @asin_f32(ptr nocapture %in.ptr, ptr %out.ptr) {
%entry:
  br label %for.body

%for.body:
  %iv = phi i64 [ 0, %entry ], [ %iv.next, %for.body ]
  %in.gep = gep inbounds ptr nocapture %in.ptr, 4 x i64 %iv
  %in = load float, ptr %in.gep, align 8
  %call = call float @asinf(float %in)
  %out.gep = gep inbounds ptr %out.ptr, 4 x i64 %iv
  store float %call, ptr %out.gep, align 4
  %iv.next = add nsw nuw i64 %iv, 1
  %exitcond = icmp eq i64 %iv.next, 1000
  br i1 %exitcond, label %for.end, label %for.body

%for.end:
  ret void
}
=>
define void @asin_f32(ptr nocapture %in.ptr, ptr %out.ptr) {
%entry:
  %in.ptr2 = ptrtoint ptr nocapture %in.ptr to i64
  %out.ptr1 = ptrtoint ptr %out.ptr to i64
  br i1 0, label %scalar.ph, label %vector.memcheck

%vector.memcheck:
  %0 = sub i64 %out.ptr1, %in.ptr2
  %diff.check = icmp ult i64 %0, 32
  br i1 %diff.check, label %scalar.ph, label %vector.ph

%vector.ph:
  br label %vector.body

%vector.body:
  %index = phi i64 [ 0, %vector.ph ], [ %index.next, %vector.body ]
  %1 = add i64 %index, 0
  %3 = gep inbounds ptr nocapture %in.ptr, 4 x i64 %1
  %5 = gep inbounds ptr %3, 4 x i32 0
  %wide.load = load <4 x float>, ptr %5, align 8
  %6 = gep inbounds ptr %3, 4 x i32 4
  %wide.load3 = load <4 x float>, ptr %6, align 8
  %7 = call <4 x float> @armpl_vasinq_f32(<4 x float> %wide.load)
  %8 = call <4 x float> @armpl_vasinq_f32(<4 x float> %wide.load3)
  %9 = gep inbounds ptr %out.ptr, 4 x i64 %1
  %11 = gep inbounds ptr %9, 4 x i32 0
  store <4 x float> %7, ptr %11, align 4
  %12 = gep inbounds ptr %9, 4 x i32 4
  store <4 x float> %8, ptr %12, align 4
  %index.next = add nuw i64 %index, 8
  %13 = icmp eq i64 %index.next, 1000
  br i1 %13, label %middle.block, label %vector.body

%middle.block:
  %cmp.n = icmp eq i64 1000, 1000, use_provenance
  br i1 %cmp.n, label %for.end, label %scalar.ph

%scalar.ph:
  %bc.resume.val = phi i64 [ 1000, %middle.block ], [ 0, %entry ], [ 0, %vector.memcheck ]
  br label %for.body

%for.body:
  %iv = phi i64 [ %bc.resume.val, %scalar.ph ], [ %iv.next, %for.body ]
  %in.gep = gep inbounds ptr nocapture %in.ptr, 4 x i64 %iv
  %in = load float, ptr %in.gep, align 8
  %call = call float @asinf(float %in)
  %out.gep = gep inbounds ptr %out.ptr, 4 x i64 %iv
  store float %call, ptr %out.gep, align 4
  %iv.next = add nsw nuw i64 %iv, 1
  %exitcond = icmp eq i64 %iv.next, 1000
  br i1 %exitcond, label %for.end, label %for.body

%for.end:
  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: @asinf

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

----------------------------------------
define void @asinh_f64(ptr nocapture %in.ptr, ptr %out.ptr) {
%entry:
  br label %for.body

%for.body:
  %iv = phi i64 [ 0, %entry ], [ %iv.next, %for.body ]
  %in.gep = gep inbounds ptr nocapture %in.ptr, 8 x i64 %iv
  %in = load double, ptr %in.gep, align 8
  %call = call double @asinh(double %in)
  %out.gep = gep inbounds ptr %out.ptr, 8 x i64 %iv
  store double %call, ptr %out.gep, align 8
  %iv.next = add nsw nuw i64 %iv, 1
  %exitcond = icmp eq i64 %iv.next, 1000
  br i1 %exitcond, label %for.end, label %for.body

%for.end:
  ret void
}
Transformation seems to be correct! (syntactically equal)

-- 39. InjectTLIMappings

----------------------------------------
define void @asinh_f64(ptr nocapture %in.ptr, ptr %out.ptr) {
%entry:
  br label %for.body

%for.body:
  %iv = phi i64 [ 0, %entry ], [ %iv.next, %for.body ]
  %in.gep = gep inbounds ptr nocapture %in.ptr, 8 x i64 %iv
  %in = load double, ptr %in.gep, align 8
  %call = call double @asinh(double %in)
  %out.gep = gep inbounds ptr %out.ptr, 8 x i64 %iv
  store double %call, ptr %out.gep, align 8
  %iv.next = add nsw nuw i64 %iv, 1
  %exitcond = icmp eq i64 %iv.next, 1000
  br i1 %exitcond, label %for.end, label %for.body

%for.end:
  ret void
}
Transformation seems to be correct! (syntactically equal)

-- 40. LoopVectorizePass

----------------------------------------
define void @asinh_f64(ptr nocapture %in.ptr, ptr %out.ptr) {
%entry:
  br label %for.body

%for.body:
  %iv = phi i64 [ 0, %entry ], [ %iv.next, %for.body ]
  %in.gep = gep inbounds ptr nocapture %in.ptr, 8 x i64 %iv
  %in = load double, ptr %in.gep, align 8
  %call = call double @asinh(double %in)
  %out.gep = gep inbounds ptr %out.ptr, 8 x i64 %iv
  store double %call, ptr %out.gep, align 8
  %iv.next = add nsw nuw i64 %iv, 1
  %exitcond = icmp eq i64 %iv.next, 1000
  br i1 %exitcond, label %for.end, label %for.body

%for.end:
  ret void
}
Transformation seems to be correct! (syntactically equal)

-- 41. LoopVectorizePass

----------------------------------------
define void @asinh_f64(ptr nocapture %in.ptr, ptr %out.ptr) {
%entry:
  br label %for.body

%for.body:
  %iv = phi i64 [ 0, %entry ], [ %iv.next, %for.body ]
  %in.gep = gep inbounds ptr nocapture %in.ptr, 8 x i64 %iv
  %in = load double, ptr %in.gep, align 8
  %call = call double @asinh(double %in)
  %out.gep = gep inbounds ptr %out.ptr, 8 x i64 %iv
  store double %call, ptr %out.gep, align 8
  %iv.next = add nsw nuw i64 %iv, 1
  %exitcond = icmp eq i64 %iv.next, 1000
  br i1 %exitcond, label %for.end, label %for.body

%for.end:
  ret void
}
=>
define void @asinh_f64(ptr nocapture %in.ptr, ptr %out.ptr) {
%entry:
  %in.ptr2 = ptrtoint ptr nocapture %in.ptr to i64
  %out.ptr1 = ptrtoint ptr %out.ptr to i64
  br i1 0, label %scalar.ph, label %vector.memcheck

%vector.memcheck:
  %0 = sub i64 %out.ptr1, %in.ptr2
  %diff.check = icmp ult i64 %0, 32
  br i1 %diff.check, label %scalar.ph, label %vector.ph

%vector.ph:
  br label %vector.body

%vector.body:
  %index = phi i64 [ 0, %vector.ph ], [ %index.next, %vector.body ]
  %1 = add i64 %index, 0
  %3 = gep inbounds ptr nocapture %in.ptr, 8 x i64 %1
  %5 = gep inbounds ptr %3, 8 x i32 0
  %wide.load = load <2 x double>, ptr %5, align 8
  %6 = gep inbounds ptr %3, 8 x i32 2
  %wide.load3 = load <2 x double>, ptr %6, align 8
  %7 = call <2 x double> @armpl_vasinhq_f64(<2 x double> %wide.load)
  %8 = call <2 x double> @armpl_vasinhq_f64(<2 x double> %wide.load3)
  %9 = gep inbounds ptr %out.ptr, 8 x i64 %1
  %11 = gep inbounds ptr %9, 8 x i32 0
  store <2 x double> %7, ptr %11, align 8
  %12 = gep inbounds ptr %9, 8 x i32 2
  store <2 x double> %8, ptr %12, align 8
  %index.next = add nuw i64 %index, 4
  %13 = icmp eq i64 %index.next, 1000
  br i1 %13, label %middle.block, label %vector.body

%middle.block:
  %cmp.n = icmp eq i64 1000, 1000, use_provenance
  br i1 %cmp.n, label %for.end, label %scalar.ph

%scalar.ph:
  %bc.resume.val = phi i64 [ 1000, %middle.block ], [ 0, %entry ], [ 0, %vector.memcheck ]
  br label %for.body

%for.body:
  %iv = phi i64 [ %bc.resume.val, %scalar.ph ], [ %iv.next, %for.body ]
  %in.gep = gep inbounds ptr nocapture %in.ptr, 8 x i64 %iv
  %in = load double, ptr %in.gep, align 8
  %call = call double @asinh(double %in)
  %out.gep = gep inbounds ptr %out.ptr, 8 x i64 %iv
  store double %call, ptr %out.gep, align 8
  %iv.next = add nsw nuw i64 %iv, 1
  %exitcond = icmp eq i64 %iv.next, 1000
  br i1 %exitcond, label %for.end, label %for.body

%for.end:
  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

-- 42. PassManager<Function> : Skipping NOP
-- 43. PassManager<Function> : Skipping NOP
-- 44. InjectTLIMappings

----------------------------------------
define void @asinh_f32(ptr nocapture %in.ptr, ptr %out.ptr) {
%entry:
  br label %for.body

%for.body:
  %iv = phi i64 [ 0, %entry ], [ %iv.next, %for.body ]
  %in.gep = gep inbounds ptr nocapture %in.ptr, 4 x i64 %iv
  %in = load float, ptr %in.gep, align 8
  %call = call float @asinhf(float %in)
  %out.gep = gep inbounds ptr %out.ptr, 4 x i64 %iv
  store float %call, ptr %out.gep, align 4
  %iv.next = add nsw nuw i64 %iv, 1
  %exitcond = icmp eq i64 %iv.next, 1000
  br i1 %exitcond, label %for.end, label %for.body

%for.end:
  ret void
}
Transformation seems to be correct! (syntactically equal)

-- 45. InjectTLIMappings

----------------------------------------
define void @asinh_f32(ptr nocapture %in.ptr, ptr %out.ptr) {
%entry:
  br label %for.body

%for.body:
  %iv = phi i64 [ 0, %entry ], [ %iv.next, %for.body ]
  %in.gep = gep inbounds ptr nocapture %in.ptr, 4 x i64 %iv
  %in = load float, ptr %in.gep, align 8
  %call = call float @asinhf(float %in)
  %out.gep = gep inbounds ptr %out.ptr, 4 x i64 %iv
  store float %call, ptr %out.gep, align 4
  %iv.next = add nsw nuw i64 %iv, 1
  %exitcond = icmp eq i64 %iv.next, 1000
  br i1 %exitcond, label %for.end, label %for.body

%for.end:
  ret void
}
Transformation seems to be correct! (syntactically equal)

-- 46. LoopVectorizePass

----------------------------------------
define void @asinh_f32(ptr nocapture %in.ptr, ptr %out.ptr) {
%entry:
  br label %for.body

%for.body:
  %iv = phi i64 [ 0, %entry ], [ %iv.next, %for.body ]
  %in.gep = gep inbounds ptr nocapture %in.ptr, 4 x i64 %iv
  %in = load float, ptr %in.gep, align 8
  %call = call float @asinhf(float %in)
  %out.gep = gep inbounds ptr %out.ptr, 4 x i64 %iv
  store float %call, ptr %out.gep, align 4
  %iv.next = add nsw nuw i64 %iv, 1
  %exitcond = icmp eq i64 %iv.next, 1000
  br i1 %exitcond, label %for.end, label %for.body

%for.end:
  ret void
}
Transformation seems to be correct! (syntactically equal)

-- 47. LoopVectorizePass

----------------------------------------
define void @asinh_f32(ptr nocapture %in.ptr, ptr %out.ptr) {
%entry:
  br label %for.body

%for.body:
  %iv = phi i64 [ 0, %entry ], [ %iv.next, %for.body ]
  %in.gep = gep inbounds ptr nocapture %in.ptr, 4 x i64 %iv
  %in = load float, ptr %in.gep, align 8
  %call = call float @asinhf(float %in)
  %out.gep = gep inbounds ptr %out.ptr, 4 x i64 %iv
  store float %call, ptr %out.gep, align 4
  %iv.next = add nsw nuw i64 %iv, 1
  %exitcond = icmp eq i64 %iv.next, 1000
  br i1 %exitcond, label %for.end, label %for.body

%for.end:
  ret void
}
=>
define void @asinh_f32(ptr nocapture %in.ptr, ptr %out.ptr) {
%entry:
  %in.ptr2 = ptrtoint ptr nocapture %in.ptr to i64
  %out.ptr1 = ptrtoint ptr %out.ptr to i64
  br i1 0, label %scalar.ph, label %vector.memcheck

%vector.memcheck:
  %0 = sub i64 %out.ptr1, %in.ptr2
  %diff.check = icmp ult i64 %0, 32
  br i1 %diff.check, label %scalar.ph, label %vector.ph

%vector.ph:
  br label %vector.body

%vector.body:
  %index = phi i64 [ 0, %vector.ph ], [ %index.next, %vector.body ]
  %1 = add i64 %index, 0
  %3 = gep inbounds ptr nocapture %in.ptr, 4 x i64 %1
  %5 = gep inbounds ptr %3, 4 x i32 0
  %wide.load = load <4 x float>, ptr %5, align 8
  %6 = gep inbounds ptr %3, 4 x i32 4
  %wide.load3 = load <4 x float>, ptr %6, align 8
  %7 = call <4 x float> @armpl_vasinhq_f32(<4 x float> %wide.load)
  %8 = call <4 x float> @armpl_vasinhq_f32(<4 x float> %wide.load3)
  %9 = gep inbounds ptr %out.ptr, 4 x i64 %1
  %11 = gep inbounds ptr %9, 4 x i32 0
  store <4 x float> %7, ptr %11, align 4
  %12 = gep inbounds ptr %9, 4 x i32 4
  store <4 x float> %8, ptr %12, align 4
  %index.next = add nuw i64 %index, 8
  %13 = icmp eq i64 %index.next, 1000
  br i1 %13, label %middle.block, label %vector.body

%middle.block:
  %cmp.n = icmp eq i64 1000, 1000, use_provenance
  br i1 %cmp.n, label %for.end, label %scalar.ph

%scalar.ph:
  %bc.resume.val = phi i64 [ 1000, %middle.block ], [ 0, %entry ], [ 0, %vector.memcheck ]
  br label %for.body

%for.body:
  %iv = phi i64 [ %bc.resume.val, %scalar.ph ], [ %iv.next, %for.body ]
  %in.gep = gep inbounds ptr nocapture %in.ptr, 4 x i64 %iv
  %in = load float, ptr %in.gep, align 8
  %call = call float @asinhf(float %in)
  %out.gep = gep inbounds ptr %out.ptr, 4 x i64 %iv
  store float %call, ptr %out.gep, align 4
  %iv.next = add nsw nuw i64 %iv, 1
  %exitcond = icmp eq i64 %iv.next, 1000
  br i1 %exitcond, label %for.end, label %for.body

%for.end:
  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: @asinhf

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

----------------------------------------
define void @atan_f64(ptr nocapture %in.ptr, ptr %out.ptr) {
%entry:
  br label %for.body

%for.body:
  %iv = phi i64 [ 0, %entry ], [ %iv.next, %for.body ]
  %in.gep = gep inbounds ptr nocapture %in.ptr, 8 x i64 %iv
  %in = load double, ptr %in.gep, align 8
  %call = call double @atan(double %in)
  %out.gep = gep inbounds ptr %out.ptr, 8 x i64 %iv
  store double %call, ptr %out.gep, align 8
  %iv.next = add nsw nuw i64 %iv, 1
  %exitcond = icmp eq i64 %iv.next, 1000
  br i1 %exitcond, label %for.end, label %for.body

%for.end:
  ret void
}
Transformation seems to be correct! (syntactically equal)

-- 51. InjectTLIMappings

----------------------------------------
define void @atan_f64(ptr nocapture %in.ptr, ptr %out.ptr) {
%entry:
  br label %for.body

%for.body:
  %iv = phi i64 [ 0, %entry ], [ %iv.next, %for.body ]
  %in.gep = gep inbounds ptr nocapture %in.ptr, 8 x i64 %iv
  %in = load double, ptr %in.gep, align 8
  %call = call double @atan(double %in)
  %out.gep = gep inbounds ptr %out.ptr, 8 x i64 %iv
  store double %call, ptr %out.gep, align 8
  %iv.next = add nsw nuw i64 %iv, 1
  %exitcond = icmp eq i64 %iv.next, 1000
  br i1 %exitcond, label %for.end, label %for.body

%for.end:
  ret void
}
Transformation seems to be correct! (syntactically equal)

-- 52. LoopVectorizePass

----------------------------------------
define void @atan_f64(ptr nocapture %in.ptr, ptr %out.ptr) {
%entry:
  br label %for.body

%for.body:
  %iv = phi i64 [ 0, %entry ], [ %iv.next, %for.body ]
  %in.gep = gep inbounds ptr nocapture %in.ptr, 8 x i64 %iv
  %in = load double, ptr %in.gep, align 8
  %call = call double @atan(double %in)
  %out.gep = gep inbounds ptr %out.ptr, 8 x i64 %iv
  store double %call, ptr %out.gep, align 8
  %iv.next = add nsw nuw i64 %iv, 1
  %exitcond = icmp eq i64 %iv.next, 1000
  br i1 %exitcond, label %for.end, label %for.body

%for.end:
  ret void
}
Transformation seems to be correct! (syntactically equal)

-- 53. LoopVectorizePass

----------------------------------------
define void @atan_f64(ptr nocapture %in.ptr, ptr %out.ptr) {
%entry:
  br label %for.body

%for.body:
  %iv = phi i64 [ 0, %entry ], [ %iv.next, %for.body ]
  %in.gep = gep inbounds ptr nocapture %in.ptr, 8 x i64 %iv
  %in = load double, ptr %in.gep, align 8
  %call = call double @atan(double %in)
  %out.gep = gep inbounds ptr %out.ptr, 8 x i64 %iv
  store double %call, ptr %out.gep, align 8
  %iv.next = add nsw nuw i64 %iv, 1
  %exitcond = icmp eq i64 %iv.next, 1000
  br i1 %exitcond, label %for.end, label %for.body

%for.end:
  ret void
}
=>
define void @atan_f64(ptr nocapture %in.ptr, ptr %out.ptr) {
%entry:
  %in.ptr2 = ptrtoint ptr nocapture %in.ptr to i64
  %out.ptr1 = ptrtoint ptr %out.ptr to i64
  br i1 0, label %scalar.ph, label %vector.memcheck

%vector.memcheck:
  %0 = sub i64 %out.ptr1, %in.ptr2
  %diff.check = icmp ult i64 %0, 32
  br i1 %diff.check, label %scalar.ph, label %vector.ph

%vector.ph:
  br label %vector.body

%vector.body:
  %index = phi i64 [ 0, %vector.ph ], [ %index.next, %vector.body ]
  %1 = add i64 %index, 0
  %3 = gep inbounds ptr nocapture %in.ptr, 8 x i64 %1
  %5 = gep inbounds ptr %3, 8 x i32 0
  %wide.load = load <2 x double>, ptr %5, align 8
  %6 = gep inbounds ptr %3, 8 x i32 2
  %wide.load3 = load <2 x double>, ptr %6, align 8
  %7 = call <2 x double> @armpl_vatanq_f64(<2 x double> %wide.load)
  %8 = call <2 x double> @armpl_vatanq_f64(<2 x double> %wide.load3)
  %9 = gep inbounds ptr %out.ptr, 8 x i64 %1
  %11 = gep inbounds ptr %9, 8 x i32 0
  store <2 x double> %7, ptr %11, align 8
  %12 = gep inbounds ptr %9, 8 x i32 2
  store <2 x double> %8, ptr %12, align 8
  %index.next = add nuw i64 %index, 4
  %13 = icmp eq i64 %index.next, 1000
  br i1 %13, label %middle.block, label %vector.body

%middle.block:
  %cmp.n = icmp eq i64 1000, 1000, use_provenance
  br i1 %cmp.n, label %for.end, label %scalar.ph

%scalar.ph:
  %bc.resume.val = phi i64 [ 1000, %middle.block ], [ 0, %entry ], [ 0, %vector.memcheck ]
  br label %for.body

%for.body:
  %iv = phi i64 [ %bc.resume.val, %scalar.ph ], [ %iv.next, %for.body ]
  %in.gep = gep inbounds ptr nocapture %in.ptr, 8 x i64 %iv
  %in = load double, ptr %in.gep, align 8
  %call = call double @atan(double %in)
  %out.gep = gep inbounds ptr %out.ptr, 8 x i64 %iv
  store double %call, ptr %out.gep, align 8
  %iv.next = add nsw nuw i64 %iv, 1
  %exitcond = icmp eq i64 %iv.next, 1000
  br i1 %exitcond, label %for.end, label %for.body

%for.end:
  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: @atan

-- 54. PassManager<Function> : Skipping NOP
-- 55. PassManager<Function> : Skipping NOP
-- 56. InjectTLIMappings

----------------------------------------
define void @atan_f32(ptr nocapture %in.ptr, ptr %out.ptr) {
%entry:
  br label %for.body

%for.body:
  %iv = phi i64 [ 0, %entry ], [ %iv.next, %for.body ]
  %in.gep = gep inbounds ptr nocapture %in.ptr, 4 x i64 %iv
  %in = load float, ptr %in.gep, align 8
  %call = call float @atanf(float %in)
  %out.gep = gep inbounds ptr %out.ptr, 4 x i64 %iv
  store float %call, ptr %out.gep, align 4
  %iv.next = add nsw nuw i64 %iv, 1
  %exitcond = icmp eq i64 %iv.next, 1000
  br i1 %exitcond, label %for.end, label %for.body

%for.end:
  ret void
}
Transformation seems to be correct! (syntactically equal)

-- 57. InjectTLIMappings

----------------------------------------
define void @atan_f32(ptr nocapture %in.ptr, ptr %out.ptr) {
%entry:
  br label %for.body

%for.body:
  %iv = phi i64 [ 0, %entry ], [ %iv.next, %for.body ]
  %in.gep = gep inbounds ptr nocapture %in.ptr, 4 x i64 %iv
  %in = load float, ptr %in.gep, align 8
  %call = call float @atanf(float %in)
  %out.gep = gep inbounds ptr %out.ptr, 4 x i64 %iv
  store float %call, ptr %out.gep, align 4
  %iv.next = add nsw nuw i64 %iv, 1
  %exitcond = icmp eq i64 %iv.next, 1000
  br i1 %exitcond, label %for.end, label %for.body

%for.end:
  ret void
}
Transformation seems to be correct! (syntactically equal)

-- 58. LoopVectorizePass

----------------------------------------
define void @atan_f32(ptr nocapture %in.ptr, ptr %out.ptr) {
%entry:
  br label %for.body

%for.body:
  %iv = phi i64 [ 0, %entry ], [ %iv.next, %for.body ]
  %in.gep = gep inbounds ptr nocapture %in.ptr, 4 x i64 %iv
  %in = load float, ptr %in.gep, align 8
  %call = call float @atanf(float %in)
  %out.gep = gep inbounds ptr %out.ptr, 4 x i64 %iv
  store float %call, ptr %out.gep, align 4
  %iv.next = add nsw nuw i64 %iv, 1
  %exitcond = icmp eq i64 %iv.next, 1000
  br i1 %exitcond, label %for.end, label %for.body

%for.end:
  ret void
}
Transformation seems to be correct! (syntactically equal)

-- 59. LoopVectorizePass

----------------------------------------
define void @atan_f32(ptr nocapture %in.ptr, ptr %out.ptr) {
%entry:
  br label %for.body

%for.body:
  %iv = phi i64 [ 0, %entry ], [ %iv.next, %for.body ]
  %in.gep = gep inbounds ptr nocapture %in.ptr, 4 x i64 %iv
  %in = load float, ptr %in.gep, align 8
  %call = call float @atanf(float %in)
  %out.gep = gep inbounds ptr %out.ptr, 4 x i64 %iv
  store float %call, ptr %out.gep, align 4
  %iv.next = add nsw nuw i64 %iv, 1
  %exitcond = icmp eq i64 %iv.next, 1000
  br i1 %exitcond, label %for.end, label %for.body

%for.end:
  ret void
}
=>
define void @atan_f32(ptr nocapture %in.ptr, ptr %out.ptr) {
%entry:
  %in.ptr2 = ptrtoint ptr nocapture %in.ptr to i64
  %out.ptr1 = ptrtoint ptr %out.ptr to i64
  br i1 0, label %scalar.ph, label %vector.memcheck

%vector.memcheck:
  %0 = sub i64 %out.ptr1, %in.ptr2
  %diff.check = icmp ult i64 %0, 32
  br i1 %diff.check, label %scalar.ph, label %vector.ph

%vector.ph:
  br label %vector.body

%vector.body:
  %index = phi i64 [ 0, %vector.ph ], [ %index.next, %vector.body ]
  %1 = add i64 %index, 0
  %3 = gep inbounds ptr nocapture %in.ptr, 4 x i64 %1
  %5 = gep inbounds ptr %3, 4 x i32 0
  %wide.load = load <4 x float>, ptr %5, align 8
  %6 = gep inbounds ptr %3, 4 x i32 4
  %wide.load3 = load <4 x float>, ptr %6, align 8
  %7 = call <4 x float> @armpl_vatanq_f32(<4 x float> %wide.load)
  %8 = call <4 x float> @armpl_vatanq_f32(<4 x float> %wide.load3)
  %9 = gep inbounds ptr %out.ptr, 4 x i64 %1
  %11 = gep inbounds ptr %9, 4 x i32 0
  store <4 x float> %7, ptr %11, align 4
  %12 = gep inbounds ptr %9, 4 x i32 4
  store <4 x float> %8, ptr %12, align 4
  %index.next = add nuw i64 %index, 8
  %13 = icmp eq i64 %index.next, 1000
  br i1 %13, label %middle.block, label %vector.body

%middle.block:
  %cmp.n = icmp eq i64 1000, 1000, use_provenance
  br i1 %cmp.n, label %for.end, label %scalar.ph

%scalar.ph:
  %bc.resume.val = phi i64 [ 1000, %middle.block ], [ 0, %entry ], [ 0, %vector.memcheck ]
  br label %for.body

%for.body:
  %iv = phi i64 [ %bc.resume.val, %scalar.ph ], [ %iv.next, %for.body ]
  %in.gep = gep inbounds ptr nocapture %in.ptr, 4 x i64 %iv
  %in = load float, ptr %in.gep, align 8
  %call = call float @atanf(float %in)
  %out.gep = gep inbounds ptr %out.ptr, 4 x i64 %iv
  store float %call, ptr %out.gep, align 4
  %iv.next = add nsw nuw i64 %iv, 1
  %exitcond = icmp eq i64 %iv.next, 1000
  br i1 %exitcond, label %for.end, label %for.body

%for.end:
  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: @atanf

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

----------------------------------------
define void @atanh_f64(ptr nocapture %in.ptr, ptr %out.ptr) {
%entry:
  br label %for.body

%for.body:
  %iv = phi i64 [ 0, %entry ], [ %iv.next, %for.body ]
  %in.gep = gep inbounds ptr nocapture %in.ptr, 8 x i64 %iv
  %in = load double, ptr %in.gep, align 8
  %call = call double @atanh(double %in)
  %out.gep = gep inbounds ptr %out.ptr, 8 x i64 %iv
  store double %call, ptr %out.gep, align 8
  %iv.next = add nsw nuw i64 %iv, 1
  %exitcond = icmp eq i64 %iv.next, 1000
  br i1 %exitcond, label %for.end, label %for.body

%for.end:
  ret void
}
Transformation seems to be correct! (syntactically equal)

-- 63. InjectTLIMappings

----------------------------------------
define void @atanh_f64(ptr nocapture %in.ptr, ptr %out.ptr) {
%entry:
  br label %for.body

%for.body:
  %iv = phi i64 [ 0, %entry ], [ %iv.next, %for.body ]
  %in.gep = gep inbounds ptr nocapture %in.ptr, 8 x i64 %iv
  %in = load double, ptr %in.gep, align 8
  %call = call double @atanh(double %in)
  %out.gep = gep inbounds ptr %out.ptr, 8 x i64 %iv
  store double %call, ptr %out.gep, align 8
  %iv.next = add nsw nuw i64 %iv, 1
  %exitcond = icmp eq i64 %iv.next, 1000
  br i1 %exitcond, label %for.end, label %for.body

%for.end:
  ret void
}
Transformation seems to be correct! (syntactically equal)

-- 64. LoopVectorizePass

----------------------------------------
define void @atanh_f64(ptr nocapture %in.ptr, ptr %out.ptr) {
%entry:
  br label %for.body

%for.body:
  %iv = phi i64 [ 0, %entry ], [ %iv.next, %for.body ]
  %in.gep = gep inbounds ptr nocapture %in.ptr, 8 x i64 %iv
  %in = load double, ptr %in.gep, align 8
  %call = call double @atanh(double %in)
  %out.gep = gep inbounds ptr %out.ptr, 8 x i64 %iv
  store double %call, ptr %out.gep, align 8
  %iv.next = add nsw nuw i64 %iv, 1
  %exitcond = icmp eq i64 %iv.next, 1000
  br i1 %exitcond, label %for.end, label %for.body

%for.end:
  ret void
}
Transformation seems to be correct! (syntactically equal)

-- 65. LoopVectorizePass

----------------------------------------
define void @atanh_f64(ptr nocapture %in.ptr, ptr %out.ptr) {
%entry:
  br label %for.body

%for.body:
  %iv = phi i64 [ 0, %entry ], [ %iv.next, %for.body ]
  %in.gep = gep inbounds ptr nocapture %in.ptr, 8 x i64 %iv
  %in = load double, ptr %in.gep, align 8
  %call = call double @atanh(double %in)
  %out.gep = gep inbounds ptr %out.ptr, 8 x i64 %iv
  store double %call, ptr %out.gep, align 8
  %iv.next = add nsw nuw i64 %iv, 1
  %exitcond = icmp eq i64 %iv.next, 1000
  br i1 %exitcond, label %for.end, label %for.body

%for.end:
  ret void
}
=>
define void @atanh_f64(ptr nocapture %in.ptr, ptr %out.ptr) {
%entry:
  %in.ptr2 = ptrtoint ptr nocapture %in.ptr to i64
  %out.ptr1 = ptrtoint ptr %out.ptr to i64
  br i1 0, label %scalar.ph, label %vector.memcheck

%vector.memcheck:
  %0 = sub i64 %out.ptr1, %in.ptr2
  %diff.check = icmp ult i64 %0, 32
  br i1 %diff.check, label %scalar.ph, label %vector.ph

%vector.ph:
  br label %vector.body

%vector.body:
  %index = phi i64 [ 0, %vector.ph ], [ %index.next, %vector.body ]
  %1 = add i64 %index, 0
  %3 = gep inbounds ptr nocapture %in.ptr, 8 x i64 %1
  %5 = gep inbounds ptr %3, 8 x i32 0
  %wide.load = load <2 x double>, ptr %5, align 8
  %6 = gep inbounds ptr %3, 8 x i32 2
  %wide.load3 = load <2 x double>, ptr %6, align 8
  %7 = call <2 x double> @armpl_vatanhq_f64(<2 x double> %wide.load)
  %8 = call <2 x double> @armpl_vatanhq_f64(<2 x double> %wide.load3)
  %9 = gep inbounds ptr %out.ptr, 8 x i64 %1
  %11 = gep inbounds ptr %9, 8 x i32 0
  store <2 x double> %7, ptr %11, align 8
  %12 = gep inbounds ptr %9, 8 x i32 2
  store <2 x double> %8, ptr %12, align 8
  %index.next = add nuw i64 %index, 4
  %13 = icmp eq i64 %index.next, 1000
  br i1 %13, label %middle.block, label %vector.body

%middle.block:
  %cmp.n = icmp eq i64 1000, 1000, use_provenance
  br i1 %cmp.n, label %for.end, label %scalar.ph

%scalar.ph:
  %bc.resume.val = phi i64 [ 1000, %middle.block ], [ 0, %entry ], [ 0, %vector.memcheck ]
  br label %for.body

%for.body:
  %iv = phi i64 [ %bc.resume.val, %scalar.ph ], [ %iv.next, %for.body ]
  %in.gep = gep inbounds ptr nocapture %in.ptr, 8 x i64 %iv
  %in = load double, ptr %in.gep, align 8
  %call = call double @atanh(double %in)
  %out.gep = gep inbounds ptr %out.ptr, 8 x i64 %iv
  store double %call, ptr %out.gep, align 8
  %iv.next = add nsw nuw i64 %iv, 1
  %exitcond = icmp eq i64 %iv.next, 1000
  br i1 %exitcond, label %for.end, label %for.body

%for.end:
  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

-- 66. PassManager<Function> : Skipping NOP
-- 67. PassManager<Function> : Skipping NOP
-- 68. InjectTLIMappings

----------------------------------------
define void @atanh_f32(ptr nocapture %in.ptr, ptr %out.ptr) {
%entry:
  br label %for.body

%for.body:
  %iv = phi i64 [ 0, %entry ], [ %iv.next, %for.body ]
  %in.gep = gep inbounds ptr nocapture %in.ptr, 4 x i64 %iv
  %in = load float, ptr %in.gep, align 8
  %call = call float @atanhf(float %in)
  %out.gep = gep inbounds ptr %out.ptr, 4 x i64 %iv
  store float %call, ptr %out.gep, align 4
  %iv.next = add nsw nuw i64 %iv, 1
  %exitcond = icmp eq i64 %iv.next, 1000
  br i1 %exitcond, label %for.end, label %for.body

%for.end:
  ret void
}
Transformation seems to be correct! (syntactically equal)

-- 69. InjectTLIMappings

----------------------------------------
define void @atanh_f32(ptr nocapture %in.ptr, ptr %out.ptr) {
%entry:
  br label %for.body

%for.body:
  %iv = phi i64 [ 0, %entry ], [ %iv.next, %for.body ]
  %in.gep = gep inbounds ptr nocapture %in.ptr, 4 x i64 %iv
  %in = load float, ptr %in.gep, align 8
  %call = call float @atanhf(float %in)
  %out.gep = gep inbounds ptr %out.ptr, 4 x i64 %iv
  store float %call, ptr %out.gep, align 4
  %iv.next = add nsw nuw i64 %iv, 1
  %exitcond = icmp eq i64 %iv.next, 1000
  br i1 %exitcond, label %for.end, label %for.body

%for.end:
  ret void
}
Transformation seems to be correct! (syntactically equal)

-- 70. LoopVectorizePass

----------------------------------------
define void @atanh_f32(ptr nocapture %in.ptr, ptr %out.ptr) {
%entry:
  br label %for.body

%for.body:
  %iv = phi i64 [ 0, %entry ], [ %iv.next, %for.body ]
  %in.gep = gep inbounds ptr nocapture %in.ptr, 4 x i64 %iv
  %in = load float, ptr %in.gep, align 8
  %call = call float @atanhf(float %in)
  %out.gep = gep inbounds ptr %out.ptr, 4 x i64 %iv
  store float %call, ptr %out.gep, align 4
  %iv.next = add nsw nuw i64 %iv, 1
  %exitcond = icmp eq i64 %iv.next, 1000
  br i1 %exitcond, label %for.end, label %for.body

%for.end:
  ret void
}
Transformation seems to be correct! (syntactically equal)

-- 71. LoopVectorizePass

----------------------------------------
define void @atanh_f32(ptr nocapture %in.ptr, ptr %out.ptr) {
%entry:
  br label %for.body

%for.body:
  %iv = phi i64 [ 0, %entry ], [ %iv.next, %for.body ]
  %in.gep = gep inbounds ptr nocapture %in.ptr, 4 x i64 %iv
  %in = load float, ptr %in.gep, align 8
  %call = call float @atanhf(float %in)
  %out.gep = gep inbounds ptr %out.ptr, 4 x i64 %iv
  store float %call, ptr %out.gep, align 4
  %iv.next = add nsw nuw i64 %iv, 1
  %exitcond = icmp eq i64 %iv.next, 1000
  br i1 %exitcond, label %for.end, label %for.body

%for.end:
  ret void
}
=>
define void @atanh_f32(ptr nocapture %in.ptr, ptr %out.ptr) {
%entry:
  %in.ptr2 = ptrtoint ptr nocapture %in.ptr to i64
  %out.ptr1 = ptrtoint ptr %out.ptr to i64
  br i1 0, label %scalar.ph, label %vector.memcheck

%vector.memcheck:
  %0 = sub i64 %out.ptr1, %in.ptr2
  %diff.check = icmp ult i64 %0, 32
  br i1 %diff.check, label %scalar.ph, label %vector.ph

%vector.ph:
  br label %vector.body

%vector.body:
  %index = phi i64 [ 0, %vector.ph ], [ %index.next, %vector.body ]
  %1 = add i64 %index, 0
  %3 = gep inbounds ptr nocapture %in.ptr, 4 x i64 %1
  %5 = gep inbounds ptr %3, 4 x i32 0
  %wide.load = load <4 x float>, ptr %5, align 8
  %6 = gep inbounds ptr %3, 4 x i32 4
  %wide.load3 = load <4 x float>, ptr %6, align 8
  %7 = call <4 x float> @armpl_vatanhq_f32(<4 x float> %wide.load)
  %8 = call <4 x float> @armpl_vatanhq_f32(<4 x float> %wide.load3)
  %9 = gep inbounds ptr %out.ptr, 4 x i64 %1
  %11 = gep inbounds ptr %9, 4 x i32 0
  store <4 x float> %7, ptr %11, align 4
  %12 = gep inbounds ptr %9, 4 x i32 4
  store <4 x float> %8, ptr %12, align 4
  %index.next = add nuw i64 %index, 8
  %13 = icmp eq i64 %index.next, 1000
  br i1 %13, label %middle.block, label %vector.body

%middle.block:
  %cmp.n = icmp eq i64 1000, 1000, use_provenance
  br i1 %cmp.n, label %for.end, label %scalar.ph

%scalar.ph:
  %bc.resume.val = phi i64 [ 1000, %middle.block ], [ 0, %entry ], [ 0, %vector.memcheck ]
  br label %for.body

%for.body:
  %iv = phi i64 [ %bc.resume.val, %scalar.ph ], [ %iv.next, %for.body ]
  %in.gep = gep inbounds ptr nocapture %in.ptr, 4 x i64 %iv
  %in = load float, ptr %in.gep, align 8
  %call = call float @atanhf(float %in)
  %out.gep = gep inbounds ptr %out.ptr, 4 x i64 %iv
  store float %call, ptr %out.gep, align 4
  %iv.next = add nsw nuw i64 %iv, 1
  %exitcond = icmp eq i64 %iv.next, 1000
  br i1 %exitcond, label %for.end, label %for.body

%for.end:
  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: @atanhf

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

----------------------------------------
define void @cbrt_f64(ptr nocapture %in.ptr, ptr %out.ptr) {
%entry:
  br label %for.body

%for.body:
  %iv = phi i64 [ 0, %entry ], [ %iv.next, %for.body ]
  %in.gep = gep inbounds ptr nocapture %in.ptr, 8 x i64 %iv
  %in = load double, ptr %in.gep, align 8
  %call = call double @cbrt(double %in)
  %out.gep = gep inbounds ptr %out.ptr, 8 x i64 %iv
  store double %call, ptr %out.gep, align 8
  %iv.next = add nsw nuw i64 %iv, 1
  %exitcond = icmp eq i64 %iv.next, 1000
  br i1 %exitcond, label %for.end, label %for.body

%for.end:
  ret void
}
Transformation seems to be correct! (syntactically equal)

-- 75. InjectTLIMappings

----------------------------------------
define void @cbrt_f64(ptr nocapture %in.ptr, ptr %out.ptr) {
%entry:
  br label %for.body

%for.body:
  %iv = phi i64 [ 0, %entry ], [ %iv.next, %for.body ]
  %in.gep = gep inbounds ptr nocapture %in.ptr, 8 x i64 %iv
  %in = load double, ptr %in.gep, align 8
  %call = call double @cbrt(double %in)
  %out.gep = gep inbounds ptr %out.ptr, 8 x i64 %iv
  store double %call, ptr %out.gep, align 8
  %iv.next = add nsw nuw i64 %iv, 1
  %exitcond = icmp eq i64 %iv.next, 1000
  br i1 %exitcond, label %for.end, label %for.body

%for.end:
  ret void
}
Transformation seems to be correct! (syntactically equal)

-- 76. LoopVectorizePass

----------------------------------------
define void @cbrt_f64(ptr nocapture %in.ptr, ptr %out.ptr) {
%entry:
  br label %for.body

%for.body:
  %iv = phi i64 [ 0, %entry ], [ %iv.next, %for.body ]
  %in.gep = gep inbounds ptr nocapture %in.ptr, 8 x i64 %iv
  %in = load double, ptr %in.gep, align 8
  %call = call double @cbrt(double %in)
  %out.gep = gep inbounds ptr %out.ptr, 8 x i64 %iv
  store double %call, ptr %out.gep, align 8
  %iv.next = add nsw nuw i64 %iv, 1
  %exitcond = icmp eq i64 %iv.next, 1000
  br i1 %exitcond, label %for.end, label %for.body

%for.end:
  ret void
}
Transformation seems to be correct! (syntactically equal)

-- 77. LoopVectorizePass

----------------------------------------
define void @cbrt_f64(ptr nocapture %in.ptr, ptr %out.ptr) {
%entry:
  br label %for.body

%for.body:
  %iv = phi i64 [ 0, %entry ], [ %iv.next, %for.body ]
  %in.gep = gep inbounds ptr nocapture %in.ptr, 8 x i64 %iv
  %in = load double, ptr %in.gep, align 8
  %call = call double @cbrt(double %in)
  %out.gep = gep inbounds ptr %out.ptr, 8 x i64 %iv
  store double %call, ptr %out.gep, align 8
  %iv.next = add nsw nuw i64 %iv, 1
  %exitcond = icmp eq i64 %iv.next, 1000
  br i1 %exitcond, label %for.end, label %for.body

%for.end:
  ret void
}
=>
define void @cbrt_f64(ptr nocapture %in.ptr, ptr %out.ptr) {
%entry:
  %in.ptr2 = ptrtoint ptr nocapture %in.ptr to i64
  %out.ptr1 = ptrtoint ptr %out.ptr to i64
  br i1 0, label %scalar.ph, label %vector.memcheck

%vector.memcheck:
  %0 = sub i64 %out.ptr1, %in.ptr2
  %diff.check = icmp ult i64 %0, 32
  br i1 %diff.check, label %scalar.ph, label %vector.ph

%vector.ph:
  br label %vector.body

%vector.body:
  %index = phi i64 [ 0, %vector.ph ], [ %index.next, %vector.body ]
  %1 = add i64 %index, 0
  %3 = gep inbounds ptr nocapture %in.ptr, 8 x i64 %1
  %5 = gep inbounds ptr %3, 8 x i32 0
  %wide.load = load <2 x double>, ptr %5, align 8
  %6 = gep inbounds ptr %3, 8 x i32 2
  %wide.load3 = load <2 x double>, ptr %6, align 8
  %7 = call <2 x double> @armpl_vcbrtq_f64(<2 x double> %wide.load)
  %8 = call <2 x double> @armpl_vcbrtq_f64(<2 x double> %wide.load3)
  %9 = gep inbounds ptr %out.ptr, 8 x i64 %1
  %11 = gep inbounds ptr %9, 8 x i32 0
  store <2 x double> %7, ptr %11, align 8
  %12 = gep inbounds ptr %9, 8 x i32 2
  store <2 x double> %8, ptr %12, align 8
  %index.next = add nuw i64 %index, 4
  %13 = icmp eq i64 %index.next, 1000
  br i1 %13, label %middle.block, label %vector.body

%middle.block:
  %cmp.n = icmp eq i64 1000, 1000, use_provenance
  br i1 %cmp.n, label %for.end, label %scalar.ph

%scalar.ph:
  %bc.resume.val = phi i64 [ 1000, %middle.block ], [ 0, %entry ], [ 0, %vector.memcheck ]
  br label %for.body

%for.body:
  %iv = phi i64 [ %bc.resume.val, %scalar.ph ], [ %iv.next, %for.body ]
  %in.gep = gep inbounds ptr nocapture %in.ptr, 8 x i64 %iv
  %in = load double, ptr %in.gep, align 8
  %call = call double @cbrt(double %in)
  %out.gep = gep inbounds ptr %out.ptr, 8 x i64 %iv
  store double %call, ptr %out.gep, align 8
  %iv.next = add nsw nuw i64 %iv, 1
  %exitcond = icmp eq i64 %iv.next, 1000
  br i1 %exitcond, label %for.end, label %for.body

%for.end:
  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

-- 78. PassManager<Function> : Skipping NOP
-- 79. PassManager<Function> : Skipping NOP
-- 80. InjectTLIMappings

----------------------------------------
define void @cbrt_f32(ptr nocapture %in.ptr, ptr %out.ptr) {
%entry:
  br label %for.body

%for.body:
  %iv = phi i64 [ 0, %entry ], [ %iv.next, %for.body ]
  %in.gep = gep inbounds ptr nocapture %in.ptr, 4 x i64 %iv
  %in = load float, ptr %in.gep, align 8
  %call = call float @cbrtf(float %in)
  %out.gep = gep inbounds ptr %out.ptr, 4 x i64 %iv
  store float %call, ptr %out.gep, align 4
  %iv.next = add nsw nuw i64 %iv, 1
  %exitcond = icmp eq i64 %iv.next, 1000
  br i1 %exitcond, label %for.end, label %for.body

%for.end:
  ret void
}
Transformation seems to be correct! (syntactically equal)

-- 81. InjectTLIMappings

----------------------------------------
define void @cbrt_f32(ptr nocapture %in.ptr, ptr %out.ptr) {
%entry:
  br label %for.body

%for.body:
  %iv = phi i64 [ 0, %entry ], [ %iv.next, %for.body ]
  %in.gep = gep inbounds ptr nocapture %in.ptr, 4 x i64 %iv
  %in = load float, ptr %in.gep, align 8
  %call = call float @cbrtf(float %in)
  %out.gep = gep inbounds ptr %out.ptr, 4 x i64 %iv
  store float %call, ptr %out.gep, align 4
  %iv.next = add nsw nuw i64 %iv, 1
  %exitcond = icmp eq i64 %iv.next, 1000
  br i1 %exitcond, label %for.end, label %for.body

%for.end:
  ret void
}
Transformation seems to be correct! (syntactically equal)

-- 82. LoopVectorizePass

----------------------------------------
define void @cbrt_f32(ptr nocapture %in.ptr, ptr %out.ptr) {
%entry:
  br label %for.body

%for.body:
  %iv = phi i64 [ 0, %entry ], [ %iv.next, %for.body ]
  %in.gep = gep inbounds ptr nocapture %in.ptr, 4 x i64 %iv
  %in = load float, ptr %in.gep, align 8
  %call = call float @cbrtf(float %in)
  %out.gep = gep inbounds ptr %out.ptr, 4 x i64 %iv
  store float %call, ptr %out.gep, align 4
  %iv.next = add nsw nuw i64 %iv, 1
  %exitcond = icmp eq i64 %iv.next, 1000
  br i1 %exitcond, label %for.end, label %for.body

%for.end:
  ret void
}
Transformation seems to be correct! (syntactically equal)

-- 83. LoopVectorizePass

----------------------------------------
define void @cbrt_f32(ptr nocapture %in.ptr, ptr %out.ptr) {
%entry:
  br label %for.body

%for.body:
  %iv = phi i64 [ 0, %entry ], [ %iv.next, %for.body ]
  %in.gep = gep inbounds ptr nocapture %in.ptr, 4 x i64 %iv
  %in = load float, ptr %in.gep, align 8
  %call = call float @cbrtf(float %in)
  %out.gep = gep inbounds ptr %out.ptr, 4 x i64 %iv
  store float %call, ptr %out.gep, align 4
  %iv.next = add nsw nuw i64 %iv, 1
  %exitcond = icmp eq i64 %iv.next, 1000
  br i1 %exitcond, label %for.end, label %for.body

%for.end:
  ret void
}
=>
define void @cbrt_f32(ptr nocapture %in.ptr, ptr %out.ptr) {
%entry:
  %in.ptr2 = ptrtoint ptr nocapture %in.ptr to i64
  %out.ptr1 = ptrtoint ptr %out.ptr to i64
  br i1 0, label %scalar.ph, label %vector.memcheck

%vector.memcheck:
  %0 = sub i64 %out.ptr1, %in.ptr2
  %diff.check = icmp ult i64 %0, 32
  br i1 %diff.check, label %scalar.ph, label %vector.ph

%vector.ph:
  br label %vector.body

%vector.body:
  %index = phi i64 [ 0, %vector.ph ], [ %index.next, %vector.body ]
  %1 = add i64 %index, 0
  %3 = gep inbounds ptr nocapture %in.ptr, 4 x i64 %1
  %5 = gep inbounds ptr %3, 4 x i32 0
  %wide.load = load <4 x float>, ptr %5, align 8
  %6 = gep inbounds ptr %3, 4 x i32 4
  %wide.load3 = load <4 x float>, ptr %6, align 8
  %7 = call <4 x float> @armpl_vcbrtq_f32(<4 x float> %wide.load)
  %8 = call <4 x float> @armpl_vcbrtq_f32(<4 x float> %wide.load3)
  %9 = gep inbounds ptr %out.ptr, 4 x i64 %1
  %11 = gep inbounds ptr %9, 4 x i32 0
  store <4 x float> %7, ptr %11, align 4
  %12 = gep inbounds ptr %9, 4 x i32 4
  store <4 x float> %8, ptr %12, align 4
  %index.next = add nuw i64 %index, 8
  %13 = icmp eq i64 %index.next, 1000
  br i1 %13, label %middle.block, label %vector.body

%middle.block:
  %cmp.n = icmp eq i64 1000, 1000, use_provenance
  br i1 %cmp.n, label %for.end, label %scalar.ph

%scalar.ph:
  %bc.resume.val = phi i64 [ 1000, %middle.block ], [ 0, %entry ], [ 0, %vector.memcheck ]
  br label %for.body

%for.body:
  %iv = phi i64 [ %bc.resume.val, %scalar.ph ], [ %iv.next, %for.body ]
  %in.gep = gep inbounds ptr nocapture %in.ptr, 4 x i64 %iv
  %in = load float, ptr %in.gep, align 8
  %call = call float @cbrtf(float %in)
  %out.gep = gep inbounds ptr %out.ptr, 4 x i64 %iv
  store float %call, ptr %out.gep, align 4
  %iv.next = add nsw nuw i64 %iv, 1
  %exitcond = icmp eq i64 %iv.next, 1000
  br i1 %exitcond, label %for.end, label %for.body

%for.end:
  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: @cbrtf

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

----------------------------------------
define void @cos_f64(ptr nocapture %in.ptr, ptr %out.ptr) {
%entry:
  br label %for.body

%for.body:
  %iv = phi i64 [ 0, %entry ], [ %iv.next, %for.body ]
  %in.gep = gep inbounds ptr nocapture %in.ptr, 8 x i64 %iv
  %in = load double, ptr %in.gep, align 8
  %call = call double @cos(double %in)
  %out.gep = gep inbounds ptr %out.ptr, 8 x i64 %iv
  store double %call, ptr %out.gep, align 8
  %iv.next = add nsw nuw i64 %iv, 1
  %exitcond = icmp eq i64 %iv.next, 1000
  br i1 %exitcond, label %for.end, label %for.body

%for.end:
  ret void
}
Transformation seems to be correct! (syntactically equal)

-- 87. InjectTLIMappings

----------------------------------------
define void @cos_f64(ptr nocapture %in.ptr, ptr %out.ptr) {
%entry:
  br label %for.body

%for.body:
  %iv = phi i64 [ 0, %entry ], [ %iv.next, %for.body ]
  %in.gep = gep inbounds ptr nocapture %in.ptr, 8 x i64 %iv
  %in = load double, ptr %in.gep, align 8
  %call = call double @cos(double %in)
  %out.gep = gep inbounds ptr %out.ptr, 8 x i64 %iv
  store double %call, ptr %out.gep, align 8
  %iv.next = add nsw nuw i64 %iv, 1
  %exitcond = icmp eq i64 %iv.next, 1000
  br i1 %exitcond, label %for.end, label %for.body

%for.end:
  ret void
}
Transformation seems to be correct! (syntactically equal)

-- 88. LoopVectorizePass

----------------------------------------
define void @cos_f64(ptr nocapture %in.ptr, ptr %out.ptr) {
%entry:
  br label %for.body

%for.body:
  %iv = phi i64 [ 0, %entry ], [ %iv.next, %for.body ]
  %in.gep = gep inbounds ptr nocapture %in.ptr, 8 x i64 %iv
  %in = load double, ptr %in.gep, align 8
  %call = call double @cos(double %in)
  %out.gep = gep inbounds ptr %out.ptr, 8 x i64 %iv
  store double %call, ptr %out.gep, align 8
  %iv.next = add nsw nuw i64 %iv, 1
  %exitcond = icmp eq i64 %iv.next, 1000
  br i1 %exitcond, label %for.end, label %for.body

%for.end:
  ret void
}
Transformation seems to be correct! (syntactically equal)

-- 89. LoopVectorizePass

----------------------------------------
define void @cos_f64(ptr nocapture %in.ptr, ptr %out.ptr) {
%entry:
  br label %for.body

%for.body:
  %iv = phi i64 [ 0, %entry ], [ %iv.next, %for.body ]
  %in.gep = gep inbounds ptr nocapture %in.ptr, 8 x i64 %iv
  %in = load double, ptr %in.gep, align 8
  %call = call double @cos(double %in)
  %out.gep = gep inbounds ptr %out.ptr, 8 x i64 %iv
  store double %call, ptr %out.gep, align 8
  %iv.next = add nsw nuw i64 %iv, 1
  %exitcond = icmp eq i64 %iv.next, 1000
  br i1 %exitcond, label %for.end, label %for.body

%for.end:
  ret void
}
=>
define void @cos_f64(ptr nocapture %in.ptr, ptr %out.ptr) {
%entry:
  %in.ptr2 = ptrtoint ptr nocapture %in.ptr to i64
  %out.ptr1 = ptrtoint ptr %out.ptr to i64
  br i1 0, label %scalar.ph, label %vector.memcheck

%vector.memcheck:
  %0 = sub i64 %out.ptr1, %in.ptr2
  %diff.check = icmp ult i64 %0, 32
  br i1 %diff.check, label %scalar.ph, label %vector.ph

%vector.ph:
  br label %vector.body

%vector.body:
  %index = phi i64 [ 0, %vector.ph ], [ %index.next, %vector.body ]
  %1 = add i64 %index, 0
  %3 = gep inbounds ptr nocapture %in.ptr, 8 x i64 %1
  %5 = gep inbounds ptr %3, 8 x i32 0
  %wide.load = load <2 x double>, ptr %5, align 8
  %6 = gep inbounds ptr %3, 8 x i32 2
  %wide.load3 = load <2 x double>, ptr %6, align 8
  %7 = call <2 x double> @armpl_vcosq_f64(<2 x double> %wide.load)
  %8 = call <2 x double> @armpl_vcosq_f64(<2 x double> %wide.load3)
  %9 = gep inbounds ptr %out.ptr, 8 x i64 %1
  %11 = gep inbounds ptr %9, 8 x i32 0
  store <2 x double> %7, ptr %11, align 8
  %12 = gep inbounds ptr %9, 8 x i32 2
  store <2 x double> %8, ptr %12, align 8
  %index.next = add nuw i64 %index, 4
  %13 = icmp eq i64 %index.next, 1000
  br i1 %13, label %middle.block, label %vector.body

%middle.block:
  %cmp.n = icmp eq i64 1000, 1000, use_provenance
  br i1 %cmp.n, label %for.end, label %scalar.ph

%scalar.ph:
  %bc.resume.val = phi i64 [ 1000, %middle.block ], [ 0, %entry ], [ 0, %vector.memcheck ]
  br label %for.body

%for.body:
  %iv = phi i64 [ %bc.resume.val, %scalar.ph ], [ %iv.next, %for.body ]
  %in.gep = gep inbounds ptr nocapture %in.ptr, 8 x i64 %iv
  %in = load double, ptr %in.gep, align 8
  %call = call double @cos(double %in)
  %out.gep = gep inbounds ptr %out.ptr, 8 x i64 %iv
  store double %call, ptr %out.gep, align 8
  %iv.next = add nsw nuw i64 %iv, 1
  %exitcond = icmp eq i64 %iv.next, 1000
  br i1 %exitcond, label %for.end, label %for.body

%for.end:
  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: @cos

-- 90. PassManager<Function> : Skipping NOP
-- 91. PassManager<Function> : Skipping NOP
-- 92. InjectTLIMappings

----------------------------------------
define void @cos_f32(ptr nocapture %in.ptr, ptr %out.ptr) {
%entry:
  br label %for.body

%for.body:
  %iv = phi i64 [ 0, %entry ], [ %iv.next, %for.body ]
  %in.gep = gep inbounds ptr nocapture %in.ptr, 4 x i64 %iv
  %in = load float, ptr %in.gep, align 8
  %call = call float @cosf(float %in)
  %out.gep = gep inbounds ptr %out.ptr, 4 x i64 %iv
  store float %call, ptr %out.gep, align 4
  %iv.next = add nsw nuw i64 %iv, 1
  %exitcond = icmp eq i64 %iv.next, 1000
  br i1 %exitcond, label %for.end, label %for.body

%for.end:
  ret void
}
Transformation seems to be correct! (syntactically equal)

-- 93. InjectTLIMappings

----------------------------------------
define void @cos_f32(ptr nocapture %in.ptr, ptr %out.ptr) {
%entry:
  br label %for.body

%for.body:
  %iv = phi i64 [ 0, %entry ], [ %iv.next, %for.body ]
  %in.gep = gep inbounds ptr nocapture %in.ptr, 4 x i64 %iv
  %in = load float, ptr %in.gep, align 8
  %call = call float @cosf(float %in)
  %out.gep = gep inbounds ptr %out.ptr, 4 x i64 %iv
  store float %call, ptr %out.gep, align 4
  %iv.next = add nsw nuw i64 %iv, 1
  %exitcond = icmp eq i64 %iv.next, 1000
  br i1 %exitcond, label %for.end, label %for.body

%for.end:
  ret void
}
Transformation seems to be correct! (syntactically equal)

-- 94. LoopVectorizePass

----------------------------------------
define void @cos_f32(ptr nocapture %in.ptr, ptr %out.ptr) {
%entry:
  br label %for.body

%for.body:
  %iv = phi i64 [ 0, %entry ], [ %iv.next, %for.body ]
  %in.gep = gep inbounds ptr nocapture %in.ptr, 4 x i64 %iv
  %in = load float, ptr %in.gep, align 8
  %call = call float @cosf(float %in)
  %out.gep = gep inbounds ptr %out.ptr, 4 x i64 %iv
  store float %call, ptr %out.gep, align 4
  %iv.next = add nsw nuw i64 %iv, 1
  %exitcond = icmp eq i64 %iv.next, 1000
  br i1 %exitcond, label %for.end, label %for.body

%for.end:
  ret void
}
Transformation seems to be correct! (syntactically equal)

-- 95. LoopVectorizePass

----------------------------------------
define void @cos_f32(ptr nocapture %in.ptr, ptr %out.ptr) {
%entry:
  br label %for.body

%for.body:
  %iv = phi i64 [ 0, %entry ], [ %iv.next, %for.body ]
  %in.gep = gep inbounds ptr nocapture %in.ptr, 4 x i64 %iv
  %in = load float, ptr %in.gep, align 8
  %call = call float @cosf(float %in)
  %out.gep = gep inbounds ptr %out.ptr, 4 x i64 %iv
  store float %call, ptr %out.gep, align 4
  %iv.next = add nsw nuw i64 %iv, 1
  %exitcond = icmp eq i64 %iv.next, 1000
  br i1 %exitcond, label %for.end, label %for.body

%for.end:
  ret void
}
=>
define void @cos_f32(ptr nocapture %in.ptr, ptr %out.ptr) {
%entry:
  %in.ptr2 = ptrtoint ptr nocapture %in.ptr to i64
  %out.ptr1 = ptrtoint ptr %out.ptr to i64
  br i1 0, label %scalar.ph, label %vector.memcheck

%vector.memcheck:
  %0 = sub i64 %out.ptr1, %in.ptr2
  %diff.check = icmp ult i64 %0, 32
  br i1 %diff.check, label %scalar.ph, label %vector.ph

%vector.ph:
  br label %vector.body

%vector.body:
  %index = phi i64 [ 0, %vector.ph ], [ %index.next, %vector.body ]
  %1 = add i64 %index, 0
  %3 = gep inbounds ptr nocapture %in.ptr, 4 x i64 %1
  %5 = gep inbounds ptr %3, 4 x i32 0
  %wide.load = load <4 x float>, ptr %5, align 8
  %6 = gep inbounds ptr %3, 4 x i32 4
  %wide.load3 = load <4 x float>, ptr %6, align 8
  %7 = call <4 x float> @armpl_vcosq_f32(<4 x float> %wide.load)
  %8 = call <4 x float> @armpl_vcosq_f32(<4 x float> %wide.load3)
  %9 = gep inbounds ptr %out.ptr, 4 x i64 %1
  %11 = gep inbounds ptr %9, 4 x i32 0
  store <4 x float> %7, ptr %11, align 4
  %12 = gep inbounds ptr %9, 4 x i32 4
  store <4 x float> %8, ptr %12, align 4
  %index.next = add nuw i64 %index, 8
  %13 = icmp eq i64 %index.next, 1000
  br i1 %13, label %middle.block, label %vector.body

%middle.block:
  %cmp.n = icmp eq i64 1000, 1000, use_provenance
  br i1 %cmp.n, label %for.end, label %scalar.ph

%scalar.ph:
  %bc.resume.val = phi i64 [ 1000, %middle.block ], [ 0, %entry ], [ 0, %vector.memcheck ]
  br label %for.body

%for.body:
  %iv = phi i64 [ %bc.resume.val, %scalar.ph ], [ %iv.next, %for.body ]
  %in.gep = gep inbounds ptr nocapture %in.ptr, 4 x i64 %iv
  %in = load float, ptr %in.gep, align 8
  %call = call float @cosf(float %in)
  %out.gep = gep inbounds ptr %out.ptr, 4 x i64 %iv
  store float %call, ptr %out.gep, align 4
  %iv.next = add nsw nuw i64 %iv, 1
  %exitcond = icmp eq i64 %iv.next, 1000
  br i1 %exitcond, label %for.end, label %for.body

%for.end:
  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: @cosf

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

----------------------------------------
define void @cosh_f64(ptr nocapture %in.ptr, ptr %out.ptr) {
%entry:
  br label %for.body

%for.body:
  %iv = phi i64 [ 0, %entry ], [ %iv.next, %for.body ]
  %in.gep = gep inbounds ptr nocapture %in.ptr, 8 x i64 %iv
  %in = load double, ptr %in.gep, align 8
  %call = call double @cosh(double %in)
  %out.gep = gep inbounds ptr %out.ptr, 8 x i64 %iv
  store double %call, ptr %out.gep, align 8
  %iv.next = add nsw nuw i64 %iv, 1
  %exitcond = icmp eq i64 %iv.next, 1000
  br i1 %exitcond, label %for.end, label %for.body

%for.end:
  ret void
}
Transformation seems to be correct! (syntactically equal)

-- 99. InjectTLIMappings

----------------------------------------
define void @cosh_f64(ptr nocapture %in.ptr, ptr %out.ptr) {
%entry:
  br label %for.body

%for.body:
  %iv = phi i64 [ 0, %entry ], [ %iv.next, %for.body ]
  %in.gep = gep inbounds ptr nocapture %in.ptr, 8 x i64 %iv
  %in = load double, ptr %in.gep, align 8
  %call = call double @cosh(double %in)
  %out.gep = gep inbounds ptr %out.ptr, 8 x i64 %iv
  store double %call, ptr %out.gep, align 8
  %iv.next = add nsw nuw i64 %iv, 1
  %exitcond = icmp eq i64 %iv.next, 1000
  br i1 %exitcond, label %for.end, label %for.body

%for.end:
  ret void
}
Transformation seems to be correct! (syntactically equal)

-- 100. LoopVectorizePass

----------------------------------------
define void @cosh_f64(ptr nocapture %in.ptr, ptr %out.ptr) {
%entry:
  br label %for.body

%for.body:
  %iv = phi i64 [ 0, %entry ], [ %iv.next, %for.body ]
  %in.gep = gep inbounds ptr nocapture %in.ptr, 8 x i64 %iv
  %in = load double, ptr %in.gep, align 8
  %call = call double @cosh(double %in)
  %out.gep = gep inbounds ptr %out.ptr, 8 x i64 %iv
  store double %call, ptr %out.gep, align 8
  %iv.next = add nsw nuw i64 %iv, 1
  %exitcond = icmp eq i64 %iv.next, 1000
  br i1 %exitcond, label %for.end, label %for.body

%for.end:
  ret void
}
Transformation seems to be correct! (syntactically equal)

-- 101. LoopVectorizePass

----------------------------------------
define void @cosh_f64(ptr nocapture %in.ptr, ptr %out.ptr) {
%entry:
  br label %for.body

%for.body:
  %iv = phi i64 [ 0, %entry ], [ %iv.next, %for.body ]
  %in.gep = gep inbounds ptr nocapture %in.ptr, 8 x i64 %iv
  %in = load double, ptr %in.gep, align 8
  %call = call double @cosh(double %in)
  %out.gep = gep inbounds ptr %out.ptr, 8 x i64 %iv
  store double %call, ptr %out.gep, align 8
  %iv.next = add nsw nuw i64 %iv, 1
  %exitcond = icmp eq i64 %iv.next, 1000
  br i1 %exitcond, label %for.end, label %for.body

%for.end:
  ret void
}
=>
define void @cosh_f64(ptr nocapture %in.ptr, ptr %out.ptr) {
%entry:
  %in.ptr2 = ptrtoint ptr nocapture %in.ptr to i64
  %out.ptr1 = ptrtoint ptr %out.ptr to i64
  br i1 0, label %scalar.ph, label %vector.memcheck

%vector.memcheck:
  %0 = sub i64 %out.ptr1, %in.ptr2
  %diff.check = icmp ult i64 %0, 32
  br i1 %diff.check, label %scalar.ph, label %vector.ph

%vector.ph:
  br label %vector.body

%vector.body:
  %index = phi i64 [ 0, %vector.ph ], [ %index.next, %vector.body ]
  %1 = add i64 %index, 0
  %3 = gep inbounds ptr nocapture %in.ptr, 8 x i64 %1
  %5 = gep inbounds ptr %3, 8 x i32 0
  %wide.load = load <2 x double>, ptr %5, align 8
  %6 = gep inbounds ptr %3, 8 x i32 2
  %wide.load3 = load <2 x double>, ptr %6, align 8
  %7 = call <2 x double> @armpl_vcoshq_f64(<2 x double> %wide.load)
  %8 = call <2 x double> @armpl_vcoshq_f64(<2 x double> %wide.load3)
  %9 = gep inbounds ptr %out.ptr, 8 x i64 %1
  %11 = gep inbounds ptr %9, 8 x i32 0
  store <2 x double> %7, ptr %11, align 8
  %12 = gep inbounds ptr %9, 8 x i32 2
  store <2 x double> %8, ptr %12, align 8
  %index.next = add nuw i64 %index, 4
  %13 = icmp eq i64 %index.next, 1000
  br i1 %13, label %middle.block, label %vector.body

%middle.block:
  %cmp.n = icmp eq i64 1000, 1000, use_provenance
  br i1 %cmp.n, label %for.end, label %scalar.ph

%scalar.ph:
  %bc.resume.val = phi i64 [ 1000, %middle.block ], [ 0, %entry ], [ 0, %vector.memcheck ]
  br label %for.body

%for.body:
  %iv = phi i64 [ %bc.resume.val, %scalar.ph ], [ %iv.next, %for.body ]
  %in.gep = gep inbounds ptr nocapture %in.ptr, 8 x i64 %iv
  %in = load double, ptr %in.gep, align 8
  %call = call double @cosh(double %in)
  %out.gep = gep inbounds ptr %out.ptr, 8 x i64 %iv
  store double %call, ptr %out.gep, align 8
  %iv.next = add nsw nuw i64 %iv, 1
  %exitcond = icmp eq i64 %iv.next, 1000
  br i1 %exitcond, label %for.end, label %for.body

%for.end:
  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: @cosh

-- 102. PassManager<Function> : Skipping NOP
-- 103. PassManager<Function> : Skipping NOP
-- 104. InjectTLIMappings

----------------------------------------
define void @cosh_f32(ptr nocapture %in.ptr, ptr %out.ptr) {
%entry:
  br label %for.body

%for.body:
  %iv = phi i64 [ 0, %entry ], [ %iv.next, %for.body ]
  %in.gep = gep inbounds ptr nocapture %in.ptr, 4 x i64 %iv
  %in = load float, ptr %in.gep, align 8
  %call = call float @coshf(float %in)
  %out.gep = gep inbounds ptr %out.ptr, 4 x i64 %iv
  store float %call, ptr %out.gep, align 4
  %iv.next = add nsw nuw i64 %iv, 1
  %exitcond = icmp eq i64 %iv.next, 1000
  br i1 %exitcond, label %for.end, label %for.body

%for.end:
  ret void
}
Transformation seems to be correct! (syntactically equal)

-- 105. InjectTLIMappings

----------------------------------------
define void @cosh_f32(ptr nocapture %in.ptr, ptr %out.ptr) {
%entry:
  br label %for.body

%for.body:
  %iv = phi i64 [ 0, %entry ], [ %iv.next, %for.body ]
  %in.gep = gep inbounds ptr nocapture %in.ptr, 4 x i64 %iv
  %in = load float, ptr %in.gep, align 8
  %call = call float @coshf(float %in)
  %out.gep = gep inbounds ptr %out.ptr, 4 x i64 %iv
  store float %call, ptr %out.gep, align 4
  %iv.next = add nsw nuw i64 %iv, 1
  %exitcond = icmp eq i64 %iv.next, 1000
  br i1 %exitcond, label %for.end, label %for.body

%for.end:
  ret void
}
Transformation seems to be correct! (syntactically equal)

-- 106. LoopVectorizePass

----------------------------------------
define void @cosh_f32(ptr nocapture %in.ptr, ptr %out.ptr) {
%entry:
  br label %for.body

%for.body:
  %iv = phi i64 [ 0, %entry ], [ %iv.next, %for.body ]
  %in.gep = gep inbounds ptr nocapture %in.ptr, 4 x i64 %iv
  %in = load float, ptr %in.gep, align 8
  %call = call float @coshf(float %in)
  %out.gep = gep inbounds ptr %out.ptr, 4 x i64 %iv
  store float %call, ptr %out.gep, align 4
  %iv.next = add nsw nuw i64 %iv, 1
  %exitcond = icmp eq i64 %iv.next, 1000
  br i1 %exitcond, label %for.end, label %for.body

%for.end:
  ret void
}
Transformation seems to be correct! (syntactically equal)

-- 107. LoopVectorizePass

----------------------------------------
define void @cosh_f32(ptr nocapture %in.ptr, ptr %out.ptr) {
%entry:
  br label %for.body

%for.body:
  %iv = phi i64 [ 0, %entry ], [ %iv.next, %for.body ]
  %in.gep = gep inbounds ptr nocapture %in.ptr, 4 x i64 %iv
  %in = load float, ptr %in.gep, align 8
  %call = call float @coshf(float %in)
  %out.gep = gep inbounds ptr %out.ptr, 4 x i64 %iv
  store float %call, ptr %out.gep, align 4
  %iv.next = add nsw nuw i64 %iv, 1
  %exitcond = icmp eq i64 %iv.next, 1000
  br i1 %exitcond, label %for.end, label %for.body

%for.end:
  ret void
}
=>
define void @cosh_f32(ptr nocapture %in.ptr, ptr %out.ptr) {
%entry:
  %in.ptr2 = ptrtoint ptr nocapture %in.ptr to i64
  %out.ptr1 = ptrtoint ptr %out.ptr to i64
  br i1 0, label %scalar.ph, label %vector.memcheck

%vector.memcheck:
  %0 = sub i64 %out.ptr1, %in.ptr2
  %diff.check = icmp ult i64 %0, 32
  br i1 %diff.check, label %scalar.ph, label %vector.ph

%vector.ph:
  br label %vector.body

%vector.body:
  %index = phi i64 [ 0, %vector.ph ], [ %index.next, %vector.body ]
  %1 = add i64 %index, 0
  %3 = gep inbounds ptr nocapture %in.ptr, 4 x i64 %1
  %5 = gep inbounds ptr %3, 4 x i32 0
  %wide.load = load <4 x float>, ptr %5, align 8
  %6 = gep inbounds ptr %3, 4 x i32 4
  %wide.load3 = load <4 x float>, ptr %6, align 8
  %7 = call <4 x float> @armpl_vcoshq_f32(<4 x float> %wide.load)
  %8 = call <4 x float> @armpl_vcoshq_f32(<4 x float> %wide.load3)
  %9 = gep inbounds ptr %out.ptr, 4 x i64 %1
  %11 = gep inbounds ptr %9, 4 x i32 0
  store <4 x float> %7, ptr %11, align 4
  %12 = gep inbounds ptr %9, 4 x i32 4
  store <4 x float> %8, ptr %12, align 4
  %index.next = add nuw i64 %index, 8
  %13 = icmp eq i64 %index.next, 1000
  br i1 %13, label %middle.block, label %vector.body

%middle.block:
  %cmp.n = icmp eq i64 1000, 1000, use_provenance
  br i1 %cmp.n, label %for.end, label %scalar.ph

%scalar.ph:
  %bc.resume.val = phi i64 [ 1000, %middle.block ], [ 0, %entry ], [ 0, %vector.memcheck ]
  br label %for.body

%for.body:
  %iv = phi i64 [ %bc.resume.val, %scalar.ph ], [ %iv.next, %for.body ]
  %in.gep = gep inbounds ptr nocapture %in.ptr, 4 x i64 %iv
  %in = load float, ptr %in.gep, align 8
  %call = call float @coshf(float %in)
  %out.gep = gep inbounds ptr %out.ptr, 4 x i64 %iv
  store float %call, ptr %out.gep, align 4
  %iv.next = add nsw nuw i64 %iv, 1
  %exitcond = icmp eq i64 %iv.next, 1000
  br i1 %exitcond, label %for.end, label %for.body

%for.end:
  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: @coshf

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

----------------------------------------
define void @erf_f64(ptr nocapture %in.ptr, ptr %out.ptr) {
%entry:
  br label %for.body

%for.body:
  %iv = phi i64 [ 0, %entry ], [ %iv.next, %for.body ]
  %in.gep = gep inbounds ptr nocapture %in.ptr, 8 x i64 %iv
  %in = load double, ptr %in.gep, align 8
  %call = call double @erf(double %in)
  %out.gep = gep inbounds ptr %out.ptr, 8 x i64 %iv
  store double %call, ptr %out.gep, align 8
  %iv.next = add nsw nuw i64 %iv, 1
  %exitcond = icmp eq i64 %iv.next, 1000
  br i1 %exitcond, label %for.end, label %for.body

%for.end:
  ret void
}
Transformation seems to be correct! (syntactically equal)

-- 111. InjectTLIMappings

----------------------------------------
define void @erf_f64(ptr nocapture %in.ptr, ptr %out.ptr) {
%entry:
  br label %for.body

%for.body:
  %iv = phi i64 [ 0, %entry ], [ %iv.next, %for.body ]
  %in.gep = gep inbounds ptr nocapture %in.ptr, 8 x i64 %iv
  %in = load double, ptr %in.gep, align 8
  %call = call double @erf(double %in)
  %out.gep = gep inbounds ptr %out.ptr, 8 x i64 %iv
  store double %call, ptr %out.gep, align 8
  %iv.next = add nsw nuw i64 %iv, 1
  %exitcond = icmp eq i64 %iv.next, 1000
  br i1 %exitcond, label %for.end, label %for.body

%for.end:
  ret void
}
Transformation seems to be correct! (syntactically equal)

-- 112. LoopVectorizePass

----------------------------------------
define void @erf_f64(ptr nocapture %in.ptr, ptr %out.ptr) {
%entry:
  br label %for.body

%for.body:
  %iv = phi i64 [ 0, %entry ], [ %iv.next, %for.body ]
  %in.gep = gep inbounds ptr nocapture %in.ptr, 8 x i64 %iv
  %in = load double, ptr %in.gep, align 8
  %call = call double @erf(double %in)
  %out.gep = gep inbounds ptr %out.ptr, 8 x i64 %iv
  store double %call, ptr %out.gep, align 8
  %iv.next = add nsw nuw i64 %iv, 1
  %exitcond = icmp eq i64 %iv.next, 1000
  br i1 %exitcond, label %for.end, label %for.body

%for.end:
  ret void
}
Transformation seems to be correct! (syntactically equal)

-- 113. LoopVectorizePass

----------------------------------------
define void @erf_f64(ptr nocapture %in.ptr, ptr %out.ptr) {
%entry:
  br label %for.body

%for.body:
  %iv = phi i64 [ 0, %entry ], [ %iv.next, %for.body ]
  %in.gep = gep inbounds ptr nocapture %in.ptr, 8 x i64 %iv
  %in = load double, ptr %in.gep, align 8
  %call = call double @erf(double %in)
  %out.gep = gep inbounds ptr %out.ptr, 8 x i64 %iv
  store double %call, ptr %out.gep, align 8
  %iv.next = add nsw nuw i64 %iv, 1
  %exitcond = icmp eq i64 %iv.next, 1000
  br i1 %exitcond, label %for.end, label %for.body

%for.end:
  ret void
}
=>
define void @erf_f64(ptr nocapture %in.ptr, ptr %out.ptr) {
%entry:
  %in.ptr2 = ptrtoint ptr nocapture %in.ptr to i64
  %out.ptr1 = ptrtoint ptr %out.ptr to i64
  br i1 0, label %scalar.ph, label %vector.memcheck

%vector.memcheck:
  %0 = sub i64 %out.ptr1, %in.ptr2
  %diff.check = icmp ult i64 %0, 32
  br i1 %diff.check, label %scalar.ph, label %vector.ph

%vector.ph:
  br label %vector.body

%vector.body:
  %index = phi i64 [ 0, %vector.ph ], [ %index.next, %vector.body ]
  %1 = add i64 %index, 0
  %3 = gep inbounds ptr nocapture %in.ptr, 8 x i64 %1
  %5 = gep inbounds ptr %3, 8 x i32 0
  %wide.load = load <2 x double>, ptr %5, align 8
  %6 = gep inbounds ptr %3, 8 x i32 2
  %wide.load3 = load <2 x double>, ptr %6, align 8
  %7 = call <2 x double> @armpl_verfq_f64(<2 x double> %wide.load)
  %8 = call <2 x double> @armpl_verfq_f64(<2 x double> %wide.load3)
  %9 = gep inbounds ptr %out.ptr, 8 x i64 %1
  %11 = gep inbounds ptr %9, 8 x i32 0
  store <2 x double> %7, ptr %11, align 8
  %12 = gep inbounds ptr %9, 8 x i32 2
  store <2 x double> %8, ptr %12, align 8
  %index.next = add nuw i64 %index, 4
  %13 = icmp eq i64 %index.next, 1000
  br i1 %13, label %middle.block, label %vector.body

%middle.block:
  %cmp.n = icmp eq i64 1000, 1000, use_provenance
  br i1 %cmp.n, label %for.end, label %scalar.ph

%scalar.ph:
  %bc.resume.val = phi i64 [ 1000, %middle.block ], [ 0, %entry ], [ 0, %vector.memcheck ]
  br label %for.body

%for.body:
  %iv = phi i64 [ %bc.resume.val, %scalar.ph ], [ %iv.next, %for.body ]
  %in.gep = gep inbounds ptr nocapture %in.ptr, 8 x i64 %iv
  %in = load double, ptr %in.gep, align 8
  %call = call double @erf(double %in)
  %out.gep = gep inbounds ptr %out.ptr, 8 x i64 %iv
  store double %call, ptr %out.gep, align 8
  %iv.next = add nsw nuw i64 %iv, 1
  %exitcond = icmp eq i64 %iv.next, 1000
  br i1 %exitcond, label %for.end, label %for.body

%for.end:
  ret void
}
Transformation doesn't verify! (unsound)
ERROR: Source is more defined than target

Example:
ptr nocapture %in.ptr = pointer(non-local, block_id=1, offset=4611686018427387883, attrs=1)
ptr %out.ptr = poison

Source:
  >> Jump to %for.body
i64 %iv = #x0000000000000000 (0)
ptr %in.gep = pointer(non-local, block_id=1, offset=4611686018427387883, attrs=1)
double %in = poison
double %call = function did not return!

SOURCE MEMORY STATE
===================
NON-LOCAL BLOCKS:
Block 0 >	size: 0	align: 8	alloc type: 0	address: 0
Block 1 >	size: 4611686018427387904	align: 2	alloc type: 0	address: 5
Block 2 >	size: 0	align: 144115188075855872	alloc type: 0	address: 1
Block 3 >	align: 144115188075855872	alloc type: 0

Target:
i64 %in.ptr2 = UB triggered!


Pass: LoopVectorizePass
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' '-vector-library=ArmPL' '-passes=inject-tli-mappings,loop-vectorize' '-S' '-tv-smt-to=20000' '-tv-report-dir=/home/nlopes/alive2/build/logs' '-tv-smt-stats'
Wrote bitcode to: "/home/nlopes/alive2/build/logs/in_NT721prV_xfqk.bc"


------------------- SMT STATS -------------------
Num queries: 59
Num invalid: 0
Num skips:   0
Num trivial: 3 (4.8%)
Num timeout: 0 (0.0%)
Num errors:  0 (0.0%)
Num SAT:     59 (100.0%)
Num UNSAT:   0 (0.0%)
Alive2: Transform doesn't verify; aborting!

stderr:

+ : 'RUN: at line 1'
+ /bitbucket/nlopes/llvm/build/bin/FileCheck /bitbucket/nlopes/llvm/llvm/test/Transforms/LoopVectorize/AArch64/armpl-calls.ll --check-prefixes=CHECK,NEON
+ /home/nlopes/alive2/build/opt-alive.sh -vector-library=ArmPL -passes=inject-tli-mappings,loop-vectorize -S

FileCheck error: '<stdin>' is empty.
FileCheck command line:  /bitbucket/nlopes/llvm/build/bin/FileCheck /bitbucket/nlopes/llvm/llvm/test/Transforms/LoopVectorize/AArch64/armpl-calls.ll --check-prefixes=CHECK,NEON

<-- Back