Test Failure: Transforms/Util/assume-builder.ll

Test source: git

Log:

Source: /bitbucket/nlopes/llvm/llvm/test/Transforms/Util/assume-builder.ll
-- 1. ModuleToFunctionPassAdaptor
ERROR: Unsupported instruction:   invoke void @may_throwv2(ptr nonnull %P)
          to label %Exit unwind label
-- 1. PassManager<Function> : Skipping NOP
-- 2. AssumeBuilderPass

----------------------------------------
declare void @func(ptr, ptr)
declare void @func_cold(ptr) willreturn
declare void @func_strbool(ptr)
declare void @func_many(ptr) willreturn
declare void @func_argattr(align(8) ptr, nonnull ptr)
declare void @func_argattr2(noundef align(8) ptr, nonnull noundef ptr)

define void @test(ptr %P, ptr %P1, ptr %P2, ptr %P3) {
bb:
  call void @func(nonnull dereferenceable(16) ptr %P, ptr null)
  call void @func(dereferenceable(12) ptr %P1, nonnull ptr %P)
  call void @func_cold(dereferenceable(12) ptr %P1) willreturn
  call void @func_cold(dereferenceable(12) ptr %P1) willreturn
  call void @func(ptr %P1, ptr %P)
  call void @func_strbool(ptr %P1)
  call void @func(dereferenceable(32) ptr %P, dereferenceable(8) ptr %P)
  call void @func_many(align(8) ptr %P1) willreturn
  call void @func_many(noundef align(8) ptr %P1) willreturn
  call void @func_argattr(align(8) ptr %P2, nonnull ptr %P3)
  call void @func_argattr2(noundef align(8) ptr %P2, nonnull noundef ptr %P3)
  call void @func(nonnull ptr %P1, nonnull ptr %P)
  call void @func(nonnull noundef ptr %P1, nonnull noundef ptr %P)
  ret void
}
Transformation seems to be correct! (syntactically equal)

-- 3. AssumeBuilderPass

----------------------------------------
declare void @func(ptr, ptr)
declare void @func_cold(ptr) willreturn
declare void @func_strbool(ptr)
declare void @func_many(ptr) willreturn
declare void @func_argattr(align(8) ptr, nonnull ptr)
declare void @func_argattr2(noundef align(8) ptr, nonnull noundef ptr)

define void @test(ptr %P, ptr %P1, ptr %P2, ptr %P3) {
bb:
  call void @func(nonnull dereferenceable(16) ptr %P, ptr null)
  call void @func(dereferenceable(12) ptr %P1, nonnull ptr %P)
  call void @func_cold(dereferenceable(12) ptr %P1) willreturn
  call void @func_cold(dereferenceable(12) ptr %P1) willreturn
  call void @func(ptr %P1, ptr %P)
  call void @func_strbool(ptr %P1)
  call void @func(dereferenceable(32) ptr %P, dereferenceable(8) ptr %P)
  call void @func_many(align(8) ptr %P1) willreturn
  call void @func_many(noundef align(8) ptr %P1) willreturn
  call void @func_argattr(align(8) ptr %P2, nonnull ptr %P3)
  call void @func_argattr2(noundef align(8) ptr %P2, nonnull noundef ptr %P3)
  call void @func(nonnull ptr %P1, nonnull ptr %P)
  call void @func(nonnull noundef ptr %P1, nonnull noundef ptr %P)
  ret void
}
=>
declare void @func(ptr, ptr)
declare void @func_cold(ptr) willreturn
declare void @func_strbool(ptr)
declare void @func_many(ptr) willreturn
declare void @func_argattr(align(8) ptr, nonnull ptr)
declare void @func_argattr2(noundef align(8) ptr, nonnull noundef ptr)

define void @test(ptr %P, ptr %P1, ptr %P2, ptr %P3) {
bb:
  assume_nonnull ptr %P
  assume_dereferenceable ptr %P, i64 16
  call void @func(nonnull dereferenceable(16) ptr %P, ptr null)
  assume_dereferenceable ptr %P1, i64 12
  call void @func(dereferenceable(12) ptr %P1, nonnull ptr %P)
  call void @func_cold(dereferenceable(12) ptr %P1) willreturn
  call void @func_cold(dereferenceable(12) ptr %P1) willreturn
  call void @func(ptr %P1, ptr %P)
  call void @func_strbool(ptr %P1)
  assume_dereferenceable ptr %P, i64 32
  call void @func(dereferenceable(32) ptr %P, dereferenceable(8) ptr %P)
  call void @func_many(align(8) ptr %P1) willreturn
  assume_welldefined ptr %P1
  assume_align ptr %P1, i64 8
  call void @func_many(noundef align(8) ptr %P1) willreturn
  call void @func_argattr(align(8) ptr %P2, nonnull ptr %P3)
  assume_welldefined ptr %P2
  assume_align ptr %P2, i64 8
  assume_welldefined ptr %P3
  assume_nonnull ptr %P3
  call void @func_argattr2(noundef align(8) ptr %P2, nonnull noundef ptr %P3)
  call void @func(nonnull ptr %P1, nonnull ptr %P)
  assume_nonnull ptr %P1
  assume_welldefined ptr %P
  call void @func(nonnull noundef ptr %P1, nonnull noundef ptr %P)
  ret void
}
Transformation seems to be correct!

-- 4. RequireAnalysisPass<DominatorTreeAnalysis, Function> : Skipping NOP
-- 5. RequireAnalysisPass<DominatorTreeAnalysis, Function> : Skipping NOP
-- 6. RequireAnalysisPass<AssumptionAnalysis, Function> : Skipping NOP
-- 7. RequireAnalysisPass<AssumptionAnalysis, Function> : Skipping NOP
-- 8. AssumeSimplifyPass

----------------------------------------
declare void @func(ptr, ptr)
declare void @func_cold(ptr) willreturn
declare void @func_strbool(ptr)
declare void @func_many(ptr) willreturn
declare void @func_argattr(align(8) ptr, nonnull ptr)
declare void @func_argattr2(noundef align(8) ptr, nonnull noundef ptr)

define void @test(ptr %P, ptr %P1, ptr %P2, ptr %P3) {
bb:
  assume_nonnull ptr %P
  assume_dereferenceable ptr %P, i64 16
  assume i1 1
  call void @func(nonnull dereferenceable(16) ptr %P, ptr null)
  assume_dereferenceable ptr %P1, i64 12
  assume i1 1
  call void @func(dereferenceable(12) ptr %P1, nonnull ptr %P)
  assume i1 1
  call void @func_cold(dereferenceable(12) ptr %P1) willreturn
  assume i1 1
  call void @func_cold(dereferenceable(12) ptr %P1) willreturn
  call void @func(ptr %P1, ptr %P)
  call void @func_strbool(ptr %P1)
  assume_dereferenceable ptr %P, i64 32
  assume i1 1
  call void @func(dereferenceable(32) ptr %P, dereferenceable(8) ptr %P)
  call void @func_many(align(8) ptr %P1) willreturn
  assume_welldefined ptr %P1
  assume_align ptr %P1, i64 8
  assume i1 1
  call void @func_many(noundef align(8) ptr %P1) willreturn
  call void @func_argattr(align(8) ptr %P2, nonnull ptr %P3)
  assume_welldefined ptr %P2
  assume_align ptr %P2, i64 8
  assume_welldefined ptr %P3
  assume_nonnull ptr %P3
  assume i1 1
  call void @func_argattr2(noundef align(8) ptr %P2, nonnull noundef ptr %P3)
  call void @func(nonnull ptr %P1, nonnull ptr %P)
  assume_nonnull ptr %P1
  assume_welldefined ptr %P
  assume i1 1
  call void @func(nonnull noundef ptr %P1, nonnull noundef ptr %P)
  ret void
}
Transformation seems to be correct! (syntactically equal)

-- 9. AssumeSimplifyPass

----------------------------------------
declare void @func(ptr, ptr)
declare void @func_cold(ptr) willreturn
declare void @func_strbool(ptr)
declare void @func_many(ptr) willreturn
declare void @func_argattr(align(8) ptr, nonnull ptr)
declare void @func_argattr2(noundef align(8) ptr, nonnull noundef ptr)

define void @test(ptr %P, ptr %P1, ptr %P2, ptr %P3) {
bb:
  assume_nonnull ptr %P
  assume_dereferenceable ptr %P, i64 16
  call void @func(nonnull dereferenceable(16) ptr %P, ptr null)
  assume_dereferenceable ptr %P1, i64 12
  call void @func(dereferenceable(12) ptr %P1, nonnull ptr %P)
  call void @func_cold(dereferenceable(12) ptr %P1) willreturn
  call void @func_cold(dereferenceable(12) ptr %P1) willreturn
  call void @func(ptr %P1, ptr %P)
  call void @func_strbool(ptr %P1)
  assume_dereferenceable ptr %P, i64 32
  call void @func(dereferenceable(32) ptr %P, dereferenceable(8) ptr %P)
  call void @func_many(align(8) ptr %P1) willreturn
  assume_welldefined ptr %P1
  assume_align ptr %P1, i64 8
  call void @func_many(noundef align(8) ptr %P1) willreturn
  call void @func_argattr(align(8) ptr %P2, nonnull ptr %P3)
  assume_welldefined ptr %P2
  assume_align ptr %P2, i64 8
  assume_welldefined ptr %P3
  assume_nonnull ptr %P3
  call void @func_argattr2(noundef align(8) ptr %P2, nonnull noundef ptr %P3)
  call void @func(nonnull ptr %P1, nonnull ptr %P)
  assume_nonnull ptr %P1
  assume_welldefined ptr %P
  call void @func(nonnull noundef ptr %P1, nonnull noundef ptr %P)
  ret void
}
=>
declare void @func(ptr, ptr)
declare void @func_cold(ptr) willreturn
declare void @func_strbool(ptr)
declare void @func_many(ptr) willreturn
declare void @func_argattr(align(8) ptr, nonnull ptr)
declare void @func_argattr2(noundef align(8) ptr, nonnull noundef ptr)

define void @test(ptr nonnull dereferenceable(16) %P, ptr %P1, ptr %P2, ptr %P3) {
bb:
  call void @func(nonnull dereferenceable(16) ptr nonnull dereferenceable(16) %P, ptr null)
  assume_dereferenceable ptr %P1, i64 12
  call void @func(dereferenceable(12) ptr %P1, nonnull ptr nonnull dereferenceable(16) %P)
  call void @func_cold(dereferenceable(12) ptr %P1) willreturn
  call void @func_cold(dereferenceable(12) ptr %P1) willreturn
  call void @func(ptr %P1, ptr nonnull dereferenceable(16) %P)
  call void @func_strbool(ptr %P1)
  assume_dereferenceable ptr nonnull dereferenceable(16) %P, i64 32
  call void @func(dereferenceable(32) ptr nonnull dereferenceable(16) %P, dereferenceable(8) ptr nonnull dereferenceable(16) %P)
  call void @func_many(align(8) ptr %P1) willreturn
  assume_welldefined ptr %P1
  assume_align ptr %P1, i64 8
  call void @func_many(noundef align(8) ptr %P1) willreturn
  call void @func_argattr(align(8) ptr %P2, nonnull ptr %P3)
  assume_welldefined ptr %P2
  assume_align ptr %P2, i64 8
  assume_welldefined ptr %P3
  assume_nonnull ptr %P3
  call void @func_argattr2(noundef align(8) ptr %P2, nonnull noundef ptr %P3)
  call void @func(nonnull ptr %P1, nonnull ptr nonnull dereferenceable(16) %P)
  assume_nonnull ptr %P1
  assume_welldefined ptr nonnull dereferenceable(16) %P
  call void @func(nonnull noundef ptr %P1, nonnull noundef ptr nonnull dereferenceable(16) %P)
  ret void
}
Transformation seems to be correct!

-- 10. VerifierPass : Skipping NOP
-- 11. VerifierPass : Skipping NOP
-- 12. PassManager<Function> : Skipping NOP
-- 13. PassManager<Function> : Skipping NOP
-- 14. AssumeBuilderPass

----------------------------------------
define i32 @test2(ptr %arg, ptr %arg1, ptr %arg2) {
bb:
  %i = alloca i64 8, align 8
  %i3 = alloca i64 8, align 8
  %i4 = alloca i64 8, align 8
  %i5 = alloca i64 16, align 8
  store ptr %arg, ptr %i, align 8
  store ptr %arg1, ptr %i3, align 8
  store ptr %arg2, ptr %i4, align 8
  %i6 = load ptr, ptr %i3, align 8
  %i7 = load i32, ptr %i6, align 4
  %i8 = trunc i32 %i7 to i8
  %i9 = load ptr, ptr %i4, align 8
  store i8 %i8, ptr %i9, align 1
  %i11 = load ptr, ptr %i, align 8
  %i14 = load ptr, ptr %i, align 8
  %i16 = load i32, ptr %i14, align 8
  %i17 = load ptr, ptr %i, align 8
  %i18 = gep inbounds ptr %i17, 16 x i32 0, 1 x i64 4
  %i19 = load i8, ptr %i18, align 4
  %i20 = sext i8 %i19 to i32
  %i21 = add nsw i32 %i16, %i20
  %i22 = load ptr, ptr %i, align 8
  %i23 = gep inbounds ptr %i22, 16 x i32 0, 1 x i64 8
  %i24 = load ptr, ptr %i23, align 8
  %i25 = load i32, ptr %i24, align 4
  %i26 = add nsw i32 %i21, %i25
  ret i32 %i26
}
Transformation seems to be correct! (syntactically equal)

-- 15. AssumeBuilderPass

----------------------------------------
define i32 @test2(ptr %arg, ptr %arg1, ptr %arg2) {
bb:
  %i = alloca i64 8, align 8
  %i3 = alloca i64 8, align 8
  %i4 = alloca i64 8, align 8
  %i5 = alloca i64 16, align 8
  store ptr %arg, ptr %i, align 8
  store ptr %arg1, ptr %i3, align 8
  store ptr %arg2, ptr %i4, align 8
  %i6 = load ptr, ptr %i3, align 8
  %i7 = load i32, ptr %i6, align 4
  %i8 = trunc i32 %i7 to i8
  %i9 = load ptr, ptr %i4, align 8
  store i8 %i8, ptr %i9, align 1
  %i11 = load ptr, ptr %i, align 8
  %i14 = load ptr, ptr %i, align 8
  %i16 = load i32, ptr %i14, align 8
  %i17 = load ptr, ptr %i, align 8
  %i18 = gep inbounds ptr %i17, 16 x i32 0, 1 x i64 4
  %i19 = load i8, ptr %i18, align 4
  %i20 = sext i8 %i19 to i32
  %i21 = add nsw i32 %i16, %i20
  %i22 = load ptr, ptr %i, align 8
  %i23 = gep inbounds ptr %i22, 16 x i32 0, 1 x i64 8
  %i24 = load ptr, ptr %i23, align 8
  %i25 = load i32, ptr %i24, align 4
  %i26 = add nsw i32 %i21, %i25
  ret i32 %i26
}
=>
define i32 @test2(ptr %arg, ptr %arg1, ptr %arg2) {
bb:
  %i = alloca i64 8, align 8
  %i3 = alloca i64 8, align 8
  %i4 = alloca i64 8, align 8
  %i5 = alloca i64 16, align 8
  store ptr %arg, ptr %i, align 8
  store ptr %arg1, ptr %i3, align 8
  store ptr %arg2, ptr %i4, align 8
  %i6 = load ptr, ptr %i3, align 8
  %i7 = load i32, ptr %i6, align 4
  %i8 = trunc i32 %i7 to i8
  %i9 = load ptr, ptr %i4, align 8
  store i8 %i8, ptr %i9, align 1
  %i11 = load ptr, ptr %i, align 8
  %i14 = load ptr, ptr %i, align 8
  %i16 = load i32, ptr %i14, align 8
  %i17 = load ptr, ptr %i, align 8
  %i18 = gep inbounds ptr %i17, 16 x i32 0, 1 x i64 4
  assume_dereferenceable ptr %i17, i64 5
  assume_nonnull ptr %i17
  assume_align ptr %i17, i64 4
  %i19 = load i8, ptr %i18, align 4
  %i20 = sext i8 %i19 to i32
  %i21 = add nsw i32 %i16, %i20
  %i22 = load ptr, ptr %i, align 8
  %i23 = gep inbounds ptr %i22, 16 x i32 0, 1 x i64 8
  assume_dereferenceable ptr %i22, i64 16
  assume_nonnull ptr %i22
  assume_align ptr %i22, i64 8
  %i24 = load ptr, ptr %i23, align 8
  %i25 = load i32, ptr %i24, align 4
  %i26 = add nsw i32 %i21, %i25
  ret i32 %i26
}
Transformation doesn't verify! (not unsound)
ERROR: Timeout
-- 16. RequireAnalysisPass<DominatorTreeAnalysis, Function> : Skipping NOP
-- 17. RequireAnalysisPass<DominatorTreeAnalysis, Function> : Skipping NOP
-- 18. RequireAnalysisPass<AssumptionAnalysis, Function> : Skipping NOP
-- 19. RequireAnalysisPass<AssumptionAnalysis, Function> : Skipping NOP
-- 20. AssumeSimplifyPass

----------------------------------------
define i32 @test2(ptr %arg, ptr %arg1, ptr %arg2) {
bb:
  %i = alloca i64 8, align 8
  %i3 = alloca i64 8, align 8
  %i4 = alloca i64 8, align 8
  %i5 = alloca i64 16, align 8
  store ptr %arg, ptr %i, align 8
  store ptr %arg1, ptr %i3, align 8
  store ptr %arg2, ptr %i4, align 8
  %i6 = load ptr, ptr %i3, align 8
  %i7 = load i32, ptr %i6, align 4
  %i8 = trunc i32 %i7 to i8
  %i9 = load ptr, ptr %i4, align 8
  store i8 %i8, ptr %i9, align 1
  %i11 = load ptr, ptr %i, align 8
  %i14 = load ptr, ptr %i, align 8
  %i16 = load i32, ptr %i14, align 8
  %i17 = load ptr, ptr %i, align 8
  %i18 = gep inbounds ptr %i17, 16 x i32 0, 1 x i64 4
  assume_dereferenceable ptr %i17, i64 5
  assume_nonnull ptr %i17
  assume_align ptr %i17, i64 4
  assume i1 1
  %i19 = load i8, ptr %i18, align 4
  %i20 = sext i8 %i19 to i32
  %i21 = add nsw i32 %i16, %i20
  %i22 = load ptr, ptr %i, align 8
  %i23 = gep inbounds ptr %i22, 16 x i32 0, 1 x i64 8
  assume_dereferenceable ptr %i22, i64 16
  assume_nonnull ptr %i22
  assume_align ptr %i22, i64 8
  assume i1 1
  %i24 = load ptr, ptr %i23, align 8
  %i25 = load i32, ptr %i24, align 4
  %i26 = add nsw i32 %i21, %i25
  ret i32 %i26
}
Transformation seems to be correct! (syntactically equal)

-- 21. AssumeSimplifyPass

----------------------------------------
define i32 @test2(ptr %arg, ptr %arg1, ptr %arg2) {
bb:
  %i = alloca i64 8, align 8
  %i3 = alloca i64 8, align 8
  %i4 = alloca i64 8, align 8
  %i5 = alloca i64 16, align 8
  store ptr %arg, ptr %i, align 8
  store ptr %arg1, ptr %i3, align 8
  store ptr %arg2, ptr %i4, align 8
  %i6 = load ptr, ptr %i3, align 8
  %i7 = load i32, ptr %i6, align 4
  %i8 = trunc i32 %i7 to i8
  %i9 = load ptr, ptr %i4, align 8
  store i8 %i8, ptr %i9, align 1
  %i11 = load ptr, ptr %i, align 8
  %i14 = load ptr, ptr %i, align 8
  %i16 = load i32, ptr %i14, align 8
  %i17 = load ptr, ptr %i, align 8
  %i18 = gep inbounds ptr %i17, 16 x i32 0, 1 x i64 4
  assume_dereferenceable ptr %i17, i64 5
  assume_nonnull ptr %i17
  assume_align ptr %i17, i64 4
  %i19 = load i8, ptr %i18, align 4
  %i20 = sext i8 %i19 to i32
  %i21 = add nsw i32 %i16, %i20
  %i22 = load ptr, ptr %i, align 8
  %i23 = gep inbounds ptr %i22, 16 x i32 0, 1 x i64 8
  assume_dereferenceable ptr %i22, i64 16
  assume_nonnull ptr %i22
  assume_align ptr %i22, i64 8
  %i24 = load ptr, ptr %i23, align 8
  %i25 = load i32, ptr %i24, align 4
  %i26 = add nsw i32 %i21, %i25
  ret i32 %i26
}
=>
define i32 @test2(ptr %arg, ptr %arg1, ptr %arg2) {
bb:
  %i = alloca i64 8, align 8
  %i3 = alloca i64 8, align 8
  %i4 = alloca i64 8, align 8
  %i5 = alloca i64 16, align 8
  store ptr %arg, ptr %i, align 8
  store ptr %arg1, ptr %i3, align 8
  store ptr %arg2, ptr %i4, align 8
  %i6 = load ptr, ptr %i3, align 8
  %i7 = load i32, ptr %i6, align 4
  %i8 = trunc i32 %i7 to i8
  %i9 = load ptr, ptr %i4, align 8
  store i8 %i8, ptr %i9, align 1
  %i11 = load ptr, ptr %i, align 8
  %i14 = load ptr, ptr %i, align 8
  %i16 = load i32, ptr %i14, align 8
  %i17 = load ptr, ptr %i, align 8
  %i18 = gep inbounds ptr %i17, 16 x i32 0, 1 x i64 4
  %i19 = load i8, ptr %i18, align 4
  %i20 = sext i8 %i19 to i32
  %i21 = add nsw i32 %i16, %i20
  %i22 = load ptr, ptr %i, align 8
  assume_dereferenceable ptr %i17, i64 5
  assume_nonnull ptr %i17
  assume_align ptr %i17, i64 4
  assume_dereferenceable ptr %i22, i64 16
  assume_nonnull ptr %i22
  assume_align ptr %i22, i64 8
  %i23 = gep inbounds ptr %i22, 16 x i32 0, 1 x i64 8
  %i24 = load ptr, ptr %i23, align 8
  %i25 = load i32, ptr %i24, align 4
  %i26 = add nsw i32 %i21, %i25
  ret i32 %i26
}
Transformation doesn't verify! (not unsound)
ERROR: Timeout
-- 22. VerifierPass : Skipping NOP
-- 23. VerifierPass : Skipping NOP
-- 24. PassManager<Function> : Skipping NOP
-- 25. PassManager<Function> : Skipping NOP
-- 26. AssumeBuilderPass

----------------------------------------
declare void @may_throw()

define i32 @test3(ptr %arg, ptr %arg1, ptr %arg2) null_pointer_is_valid {
bb:
  %i = alloca i64 8, align 8
  %i3 = alloca i64 8, align 8
  %i4 = alloca i64 8, align 8
  %i5 = alloca i64 16, align 8
  store ptr %arg, ptr %i, align 8
  store ptr %arg1, ptr %i3, align 8
  store ptr %arg2, ptr %i4, align 8
  %i6 = load ptr, ptr %i3, align 8
  %i7 = load i32, ptr %i6, align 4
  %i8 = trunc i32 %i7 to i8
  %i9 = load ptr, ptr %i4, align 8
  store i8 %i8, ptr %i9, align 1
  %i11 = load ptr, ptr %i, align 32
  call void @may_throw()
  %i14 = load ptr, ptr %i, align 8
  %i16 = load i32, ptr %i14, align 8
  %i17 = load ptr, ptr %i, align 8
  %i18 = gep inbounds ptr %i17, 16 x i32 0, 1 x i64 4
  %i19 = load i8, ptr %i18, align 8
  %i20 = sext i8 %i19 to i32
  %i21 = add nsw i32 %i16, %i20
  %i22 = load ptr, ptr %i, align 8
  %i23 = gep inbounds ptr %i22, 16 x i32 0, 1 x i64 8
  %i24 = load ptr, ptr %i23, align 8
  %i25 = load i32, ptr %i24, align 4
  %i26 = add nsw i32 %i21, %i25
  ret i32 %i26
}
Transformation seems to be correct! (syntactically equal)

-- 27. AssumeBuilderPass

----------------------------------------
declare void @may_throw()

define i32 @test3(ptr %arg, ptr %arg1, ptr %arg2) null_pointer_is_valid {
bb:
  %i = alloca i64 8, align 8
  %i3 = alloca i64 8, align 8
  %i4 = alloca i64 8, align 8
  %i5 = alloca i64 16, align 8
  store ptr %arg, ptr %i, align 8
  store ptr %arg1, ptr %i3, align 8
  store ptr %arg2, ptr %i4, align 8
  %i6 = load ptr, ptr %i3, align 8
  %i7 = load i32, ptr %i6, align 4
  %i8 = trunc i32 %i7 to i8
  %i9 = load ptr, ptr %i4, align 8
  store i8 %i8, ptr %i9, align 1
  %i11 = load ptr, ptr %i, align 32
  call void @may_throw()
  %i14 = load ptr, ptr %i, align 8
  %i16 = load i32, ptr %i14, align 8
  %i17 = load ptr, ptr %i, align 8
  %i18 = gep inbounds ptr %i17, 16 x i32 0, 1 x i64 4
  %i19 = load i8, ptr %i18, align 8
  %i20 = sext i8 %i19 to i32
  %i21 = add nsw i32 %i16, %i20
  %i22 = load ptr, ptr %i, align 8
  %i23 = gep inbounds ptr %i22, 16 x i32 0, 1 x i64 8
  %i24 = load ptr, ptr %i23, align 8
  %i25 = load i32, ptr %i24, align 4
  %i26 = add nsw i32 %i21, %i25
  ret i32 %i26
}
=>
declare void @may_throw()

define i32 @test3(ptr %arg, ptr %arg1, ptr %arg2) null_pointer_is_valid {
bb:
  %i = alloca i64 8, align 8
  %i3 = alloca i64 8, align 8
  %i4 = alloca i64 8, align 8
  %i5 = alloca i64 16, align 8
  store ptr %arg, ptr %i, align 8
  store ptr %arg1, ptr %i3, align 8
  store ptr %arg2, ptr %i4, align 8
  %i6 = load ptr, ptr %i3, align 8
  %i7 = load i32, ptr %i6, align 4
  %i8 = trunc i32 %i7 to i8
  %i9 = load ptr, ptr %i4, align 8
  store i8 %i8, ptr %i9, align 1
  %i11 = load ptr, ptr %i, align 32
  call void @may_throw()
  %i14 = load ptr, ptr %i, align 8
  %i16 = load i32, ptr %i14, align 8
  %i17 = load ptr, ptr %i, align 8
  %i18 = gep inbounds ptr %i17, 16 x i32 0, 1 x i64 4
  assume_dereferenceable ptr %i17, i64 5
  assume_align ptr %i17, i64 4
  %i19 = load i8, ptr %i18, align 8
  %i20 = sext i8 %i19 to i32
  %i21 = add nsw i32 %i16, %i20
  %i22 = load ptr, ptr %i, align 8
  %i23 = gep inbounds ptr %i22, 16 x i32 0, 1 x i64 8
  assume_dereferenceable ptr %i22, i64 16
  assume_align ptr %i22, i64 8
  %i24 = load ptr, ptr %i23, align 8
  %i25 = load i32, ptr %i24, align 4
  %i26 = add nsw i32 %i21, %i25
  ret i32 %i26
}

****************************************
WARNING: Source function is always UB.
It can be refined by any target function.
Please make sure this is what you wanted.
****************************************

Transformation seems to be correct!

-- 28. RequireAnalysisPass<DominatorTreeAnalysis, Function> : Skipping NOP
-- 29. RequireAnalysisPass<DominatorTreeAnalysis, Function> : Skipping NOP
-- 30. RequireAnalysisPass<AssumptionAnalysis, Function> : Skipping NOP
-- 31. RequireAnalysisPass<AssumptionAnalysis, Function> : Skipping NOP
-- 32. AssumeSimplifyPass

----------------------------------------
declare void @may_throw()

define i32 @test3(ptr %arg, ptr %arg1, ptr %arg2) null_pointer_is_valid {
bb:
  %i = alloca i64 8, align 8
  %i3 = alloca i64 8, align 8
  %i4 = alloca i64 8, align 8
  %i5 = alloca i64 16, align 8
  store ptr %arg, ptr %i, align 8
  store ptr %arg1, ptr %i3, align 8
  store ptr %arg2, ptr %i4, align 8
  %i6 = load ptr, ptr %i3, align 8
  %i7 = load i32, ptr %i6, align 4
  %i8 = trunc i32 %i7 to i8
  %i9 = load ptr, ptr %i4, align 8
  store i8 %i8, ptr %i9, align 1
  %i11 = load ptr, ptr %i, align 32
  call void @may_throw()
  %i14 = load ptr, ptr %i, align 8
  %i16 = load i32, ptr %i14, align 8
  %i17 = load ptr, ptr %i, align 8
  %i18 = gep inbounds ptr %i17, 16 x i32 0, 1 x i64 4
  assume_dereferenceable ptr %i17, i64 5
  assume_align ptr %i17, i64 4
  assume i1 1
  %i19 = load i8, ptr %i18, align 8
  %i20 = sext i8 %i19 to i32
  %i21 = add nsw i32 %i16, %i20
  %i22 = load ptr, ptr %i, align 8
  %i23 = gep inbounds ptr %i22, 16 x i32 0, 1 x i64 8
  assume_dereferenceable ptr %i22, i64 16
  assume_align ptr %i22, i64 8
  assume i1 1
  %i24 = load ptr, ptr %i23, align 8
  %i25 = load i32, ptr %i24, align 4
  %i26 = add nsw i32 %i21, %i25
  ret i32 %i26
}
Transformation seems to be correct! (syntactically equal)

-- 33. AssumeSimplifyPass

----------------------------------------
declare void @may_throw()

define i32 @test3(ptr %arg, ptr %arg1, ptr %arg2) null_pointer_is_valid {
bb:
  %i = alloca i64 8, align 8
  %i3 = alloca i64 8, align 8
  %i4 = alloca i64 8, align 8
  %i5 = alloca i64 16, align 8
  store ptr %arg, ptr %i, align 8
  store ptr %arg1, ptr %i3, align 8
  store ptr %arg2, ptr %i4, align 8
  %i6 = load ptr, ptr %i3, align 8
  %i7 = load i32, ptr %i6, align 4
  %i8 = trunc i32 %i7 to i8
  %i9 = load ptr, ptr %i4, align 8
  store i8 %i8, ptr %i9, align 1
  %i11 = load ptr, ptr %i, align 32
  call void @may_throw()
  %i14 = load ptr, ptr %i, align 8
  %i16 = load i32, ptr %i14, align 8
  %i17 = load ptr, ptr %i, align 8
  %i18 = gep inbounds ptr %i17, 16 x i32 0, 1 x i64 4
  assume_dereferenceable ptr %i17, i64 5
  assume_align ptr %i17, i64 4
  %i19 = load i8, ptr %i18, align 8
  %i20 = sext i8 %i19 to i32
  %i21 = add nsw i32 %i16, %i20
  %i22 = load ptr, ptr %i, align 8
  %i23 = gep inbounds ptr %i22, 16 x i32 0, 1 x i64 8
  assume_dereferenceable ptr %i22, i64 16
  assume_align ptr %i22, i64 8
  %i24 = load ptr, ptr %i23, align 8
  %i25 = load i32, ptr %i24, align 4
  %i26 = add nsw i32 %i21, %i25
  ret i32 %i26
}
=>
declare void @may_throw()

define i32 @test3(ptr %arg, ptr %arg1, ptr %arg2) null_pointer_is_valid {
bb:
  %i = alloca i64 8, align 8
  %i3 = alloca i64 8, align 8
  %i4 = alloca i64 8, align 8
  %i5 = alloca i64 16, align 8
  store ptr %arg, ptr %i, align 8
  store ptr %arg1, ptr %i3, align 8
  store ptr %arg2, ptr %i4, align 8
  %i6 = load ptr, ptr %i3, align 8
  %i7 = load i32, ptr %i6, align 4
  %i8 = trunc i32 %i7 to i8
  %i9 = load ptr, ptr %i4, align 8
  store i8 %i8, ptr %i9, align 1
  %i11 = load ptr, ptr %i, align 32
  call void @may_throw()
  %i14 = load ptr, ptr %i, align 8
  %i16 = load i32, ptr %i14, align 8
  %i17 = load ptr, ptr %i, align 8
  %i18 = gep inbounds ptr %i17, 16 x i32 0, 1 x i64 4
  %i19 = load i8, ptr %i18, align 8
  %i20 = sext i8 %i19 to i32
  %i21 = add nsw i32 %i16, %i20
  %i22 = load ptr, ptr %i, align 8
  assume_dereferenceable ptr %i17, i64 5
  assume_align ptr %i17, i64 4
  assume_dereferenceable ptr %i22, i64 16
  assume_align ptr %i22, i64 8
  %i23 = gep inbounds ptr %i22, 16 x i32 0, 1 x i64 8
  %i24 = load ptr, ptr %i23, align 8
  %i25 = load i32, ptr %i24, align 4
  %i26 = add nsw i32 %i21, %i25
  ret i32 %i26
}

****************************************
WARNING: Source function is always UB.
It can be refined by any target function.
Please make sure this is what you wanted.
****************************************

Transformation seems to be correct!

-- 34. VerifierPass : Skipping NOP
-- 35. VerifierPass : Skipping NOP
-- 36. PassManager<Function> : Skipping NOP
-- 37. PassManager<Function> : Skipping NOP
-- 38. AssumeBuilderPass

----------------------------------------
define i32 @_Z6squarePi(ptr %P, ptr %P1, i1 %cond) {
bb:
  store i32 0, ptr %P, align 4
  store i32 0, ptr %P1, align 8
  br i1 %cond, label %A, label %B

A:
  store i32 0, ptr %P, align 8
  store i32 0, ptr %P1, align 4
  br i1 %cond, label %C, label %B

B:
  store i32 0, ptr %P, align 8
  store i32 0, ptr %P1, align 8
  br label %C

C:
  store i32 0, ptr %P, align 32
  store i32 0, ptr %P1, align 4
  ret i32 0
}
Transformation seems to be correct! (syntactically equal)

-- 39. AssumeBuilderPass

----------------------------------------
define i32 @_Z6squarePi(ptr %P, ptr %P1, i1 %cond) {
bb:
  store i32 0, ptr %P, align 4
  store i32 0, ptr %P1, align 8
  br i1 %cond, label %A, label %B

A:
  store i32 0, ptr %P, align 8
  store i32 0, ptr %P1, align 4
  br i1 %cond, label %C, label %B

B:
  store i32 0, ptr %P, align 8
  store i32 0, ptr %P1, align 8
  br label %C

C:
  store i32 0, ptr %P, align 32
  store i32 0, ptr %P1, align 4
  ret i32 0
}
=>
define i32 @_Z6squarePi(ptr %P, ptr %P1, i1 %cond) {
bb:
  assume_dereferenceable ptr %P, i64 4
  assume_nonnull ptr %P
  assume_align ptr %P, i64 4
  store i32 0, ptr %P, align 4
  assume_dereferenceable ptr %P1, i64 4
  assume_nonnull ptr %P1
  assume_align ptr %P1, i64 8
  store i32 0, ptr %P1, align 8
  br i1 %cond, label %A, label %B

A:
  assume_align ptr %P, i64 8
  store i32 0, ptr %P, align 8
  store i32 0, ptr %P1, align 4
  br i1 %cond, label %C, label %B

B:
  assume_dereferenceable ptr %P, i64 4
  assume_nonnull ptr %P
  assume_align ptr %P, i64 8
  store i32 0, ptr %P, align 8
  assume_dereferenceable ptr %P1, i64 4
  assume_nonnull ptr %P1
  assume_align ptr %P1, i64 8
  store i32 0, ptr %P1, align 8
  br label %C

C:
  assume_dereferenceable ptr %P, i64 4
  assume_nonnull ptr %P
  assume_align ptr %P, i64 32
  store i32 0, ptr %P, align 32
  assume_dereferenceable ptr %P1, i64 4
  assume_nonnull ptr %P1
  assume_align ptr %P1, i64 4
  store i32 0, ptr %P1, align 4
  ret i32 0
}
Transformation seems to be correct!

-- 40. RequireAnalysisPass<DominatorTreeAnalysis, Function> : Skipping NOP
-- 41. RequireAnalysisPass<DominatorTreeAnalysis, Function> : Skipping NOP
-- 42. RequireAnalysisPass<AssumptionAnalysis, Function> : Skipping NOP
-- 43. RequireAnalysisPass<AssumptionAnalysis, Function> : Skipping NOP
-- 44. AssumeSimplifyPass

----------------------------------------
define i32 @_Z6squarePi(ptr %P, ptr %P1, i1 %cond) {
bb:
  assume_dereferenceable ptr %P, i64 4
  assume_nonnull ptr %P
  assume_align ptr %P, i64 4
  assume i1 1
  store i32 0, ptr %P, align 4
  assume_dereferenceable ptr %P1, i64 4
  assume_nonnull ptr %P1
  assume_align ptr %P1, i64 8
  assume i1 1
  store i32 0, ptr %P1, align 8
  br i1 %cond, label %A, label %B

A:
  assume_align ptr %P, i64 8
  assume i1 1
  store i32 0, ptr %P, align 8
  store i32 0, ptr %P1, align 4
  br i1 %cond, label %C, label %B

B:
  assume_dereferenceable ptr %P, i64 4
  assume_nonnull ptr %P
  assume_align ptr %P, i64 8
  assume i1 1
  store i32 0, ptr %P, align 8
  assume_dereferenceable ptr %P1, i64 4
  assume_nonnull ptr %P1
  assume_align ptr %P1, i64 8
  assume i1 1
  store i32 0, ptr %P1, align 8
  br label %C

C:
  assume_dereferenceable ptr %P, i64 4
  assume_nonnull ptr %P
  assume_align ptr %P, i64 32
  assume i1 1
  store i32 0, ptr %P, align 32
  assume_dereferenceable ptr %P1, i64 4
  assume_nonnull ptr %P1
  assume_align ptr %P1, i64 4
  assume i1 1
  store i32 0, ptr %P1, align 4
  ret i32 0
}
Transformation seems to be correct! (syntactically equal)

-- 45. AssumeSimplifyPass

----------------------------------------
define i32 @_Z6squarePi(ptr %P, ptr %P1, i1 %cond) {
bb:
  assume_dereferenceable ptr %P, i64 4
  assume_nonnull ptr %P
  assume_align ptr %P, i64 4
  store i32 0, ptr %P, align 4
  assume_dereferenceable ptr %P1, i64 4
  assume_nonnull ptr %P1
  assume_align ptr %P1, i64 8
  store i32 0, ptr %P1, align 8
  br i1 %cond, label %A, label %B

A:
  assume_align ptr %P, i64 8
  store i32 0, ptr %P, align 8
  store i32 0, ptr %P1, align 4
  br i1 %cond, label %C, label %B

B:
  assume_dereferenceable ptr %P, i64 4
  assume_nonnull ptr %P
  assume_align ptr %P, i64 8
  store i32 0, ptr %P, align 8
  assume_dereferenceable ptr %P1, i64 4
  assume_nonnull ptr %P1
  assume_align ptr %P1, i64 8
  store i32 0, ptr %P1, align 8
  br label %C

C:
  assume_dereferenceable ptr %P, i64 4
  assume_nonnull ptr %P
  assume_align ptr %P, i64 32
  store i32 0, ptr %P, align 32
  assume_dereferenceable ptr %P1, i64 4
  assume_nonnull ptr %P1
  assume_align ptr %P1, i64 4
  store i32 0, ptr %P1, align 4
  ret i32 0
}
=>
define i32 @_Z6squarePi(ptr nonnull dereferenceable(4) align(4) %P, ptr nonnull dereferenceable(4) align(8) %P1, i1 %cond) {
bb:
  store i32 0, ptr nonnull dereferenceable(4) align(4) %P, align 4
  store i32 0, ptr nonnull dereferenceable(4) align(8) %P1, align 8
  br i1 %cond, label %A, label %B

A:
  assume_align ptr nonnull dereferenceable(4) align(4) %P, i64 8
  store i32 0, ptr nonnull dereferenceable(4) align(4) %P, align 8
  store i32 0, ptr nonnull dereferenceable(4) align(8) %P1, align 8
  br i1 %cond, label %C, label %B

B:
  assume_align ptr nonnull dereferenceable(4) align(4) %P, i64 8
  store i32 0, ptr nonnull dereferenceable(4) align(4) %P, align 8
  store i32 0, ptr nonnull dereferenceable(4) align(8) %P1, align 8
  br label %C

C:
  assume_align ptr nonnull dereferenceable(4) align(4) %P, i64 32
  store i32 0, ptr nonnull dereferenceable(4) align(4) %P, align 32
  store i32 0, ptr nonnull dereferenceable(4) align(8) %P1, align 8
  ret i32 0
}
Transformation seems to be correct!

-- 46. VerifierPass : Skipping NOP
-- 47. VerifierPass : Skipping NOP
-- 48. PassManager<Function> : Skipping NOP
-- 49. PassManager<Function> : Skipping NOP
-- 50. AssumeBuilderPass

----------------------------------------
declare void @may_throw()

define i32 @test4A(ptr %arg, ptr %arg1, i32 %arg2, i32 %arg3) {
bb:
  %i = icmp ne ptr %arg1, null
  br i1 %i, label %bb4, label %bb10

bb4:
  %i5 = add nsw i32 %arg3, %arg2
  call void @may_throw()
  %i6 = load i32, ptr %arg, align 4
  %i7 = add nsw i32 %i5, %i6
  store i32 0, ptr %arg, align 4
  %i8 = load i32, ptr %arg1, align 4
  %i9 = add nsw i32 %i7, %i8
  call void @may_throw()
  store i32 %i9, ptr %arg1, align 4
  br label %bb10

bb10:
  ret i32 0
}
Transformation seems to be correct! (syntactically equal)

-- 51. AssumeBuilderPass

----------------------------------------
declare void @may_throw()

define i32 @test4A(ptr %arg, ptr %arg1, i32 %arg2, i32 %arg3) {
bb:
  %i = icmp ne ptr %arg1, null
  br i1 %i, label %bb4, label %bb10

bb4:
  %i5 = add nsw i32 %arg3, %arg2
  call void @may_throw()
  %i6 = load i32, ptr %arg, align 4
  %i7 = add nsw i32 %i5, %i6
  store i32 0, ptr %arg, align 4
  %i8 = load i32, ptr %arg1, align 4
  %i9 = add nsw i32 %i7, %i8
  call void @may_throw()
  store i32 %i9, ptr %arg1, align 4
  br label %bb10

bb10:
  ret i32 0
}
=>
declare void @may_throw()

define i32 @test4A(ptr %arg, ptr %arg1, i32 %arg2, i32 %arg3) {
bb:
  %i = icmp ne ptr %arg1, null
  br i1 %i, label %bb4, label %bb10

bb4:
  %i5 = add nsw i32 %arg3, %arg2
  call void @may_throw()
  assume_dereferenceable ptr %arg, i64 4
  assume_nonnull ptr %arg
  assume_align ptr %arg, i64 4
  %i6 = load i32, ptr %arg, align 4
  %i7 = add nsw i32 %i5, %i6
  store i32 0, ptr %arg, align 4
  assume_dereferenceable ptr %arg1, i64 4
  assume_nonnull ptr %arg1
  assume_align ptr %arg1, i64 4
  %i8 = load i32, ptr %arg1, align 4
  %i9 = add nsw i32 %i7, %i8
  call void @may_throw()
  store i32 %i9, ptr %arg1, align 4
  br label %bb10

bb10:
  ret i32 0
}
Transformation doesn't verify! (not unsound)
ERROR: Timeout
-- 52. RequireAnalysisPass<DominatorTreeAnalysis, Function> : Skipping NOP
-- 53. RequireAnalysisPass<DominatorTreeAnalysis, Function> : Skipping NOP
-- 54. RequireAnalysisPass<AssumptionAnalysis, Function> : Skipping NOP
-- 55. RequireAnalysisPass<AssumptionAnalysis, Function> : Skipping NOP
-- 56. AssumeSimplifyPass

----------------------------------------
declare void @may_throw()

define i32 @test4A(ptr %arg, ptr %arg1, i32 %arg2, i32 %arg3) {
bb:
  %i = icmp ne ptr %arg1, null
  br i1 %i, label %bb4, label %bb10

bb4:
  %i5 = add nsw i32 %arg3, %arg2
  call void @may_throw()
  assume_dereferenceable ptr %arg, i64 4
  assume_nonnull ptr %arg
  assume_align ptr %arg, i64 4
  assume i1 1
  %i6 = load i32, ptr %arg, align 4
  %i7 = add nsw i32 %i5, %i6
  store i32 0, ptr %arg, align 4
  assume_dereferenceable ptr %arg1, i64 4
  assume_nonnull ptr %arg1
  assume_align ptr %arg1, i64 4
  assume i1 1
  %i8 = load i32, ptr %arg1, align 4
  %i9 = add nsw i32 %i7, %i8
  call void @may_throw()
  store i32 %i9, ptr %arg1, align 4
  br label %bb10

bb10:
  ret i32 0
}
Transformation seems to be correct! (syntactically equal)

-- 57. AssumeSimplifyPass

----------------------------------------
declare void @may_throw()

define i32 @test4A(ptr %arg, ptr %arg1, i32 %arg2, i32 %arg3) {
bb:
  %i = icmp ne ptr %arg1, null
  br i1 %i, label %bb4, label %bb10

bb4:
  %i5 = add nsw i32 %arg3, %arg2
  call void @may_throw()
  assume_dereferenceable ptr %arg, i64 4
  assume_nonnull ptr %arg
  assume_align ptr %arg, i64 4
  %i6 = load i32, ptr %arg, align 4
  %i7 = add nsw i32 %i5, %i6
  store i32 0, ptr %arg, align 4
  assume_dereferenceable ptr %arg1, i64 4
  assume_nonnull ptr %arg1
  assume_align ptr %arg1, i64 4
  %i8 = load i32, ptr %arg1, align 4
  %i9 = add nsw i32 %i7, %i8
  call void @may_throw()
  store i32 %i9, ptr %arg1, align 4
  br label %bb10

bb10:
  ret i32 0
}
=>
declare void @may_throw()

define i32 @test4A(ptr %arg, ptr %arg1, i32 %arg2, i32 %arg3) {
bb:
  %i = icmp ne ptr %arg1, null
  br i1 %i, label %bb4, label %bb10

bb4:
  %i5 = add nsw i32 %arg3, %arg2
  call void @may_throw()
  assume_dereferenceable ptr %arg, i64 4
  assume_nonnull ptr %arg
  assume_align ptr %arg, i64 4
  assume_dereferenceable ptr %arg1, i64 4
  assume_nonnull ptr %arg1
  assume_align ptr %arg1, i64 4
  %i6 = load i32, ptr %arg, align 4
  %i7 = add nsw i32 %i5, %i6
  store i32 0, ptr %arg, align 4
  %i8 = load i32, ptr %arg1, align 4
  %i9 = add nsw i32 %i7, %i8
  call void @may_throw()
  store i32 %i9, ptr %arg1, align 4
  br label %bb10

bb10:
  ret i32 0
}
Transformation doesn't verify! (not unsound)
ERROR: Timeout
-- 58. VerifierPass : Skipping NOP
-- 59. VerifierPass : Skipping NOP
-- 60. PassManager<Function> : Skipping NOP
-- 61. PassManager<Function> : Skipping NOP
ERROR: Unsupported instruction:   invoke void @may_throwv2(ptr nonnull %P)
          to label %Exit unwind label
-- 62. AssumeBuilderPass
ERROR: Unsupported instruction:   invoke void @may_throwv2(ptr nonnull %P)
          to label %Exit unwind label
-- 63. AssumeBuilderPass
ERROR: Unsupported instruction:   invoke void @may_throwv2(ptr nonnull %P)
          to label %Exit unwind label
-- 64. RequireAnalysisPass<DominatorTreeAnalysis, Function> : Skipping NOP
ERROR: Unsupported instruction:   invoke void @may_throwv2(ptr nonnull %P)
          to label %Exit unwind label
-- 65. RequireAnalysisPass<DominatorTreeAnalysis, Function> : Skipping NOP
ERROR: Unsupported instruction:   invoke void @may_throwv2(ptr nonnull %P)
          to label %Exit unwind label
-- 66. RequireAnalysisPass<AssumptionAnalysis, Function> : Skipping NOP
ERROR: Unsupported instruction:   invoke void @may_throwv2(ptr nonnull %P)
          to label %Exit unwind label
-- 67. RequireAnalysisPass<AssumptionAnalysis, Function> : Skipping NOP
ERROR: Unsupported instruction:   invoke void @may_throwv2(ptr nonnull %P)
          to label %Exit unwind label
-- 68. AssumeSimplifyPass
ERROR: Unsupported instruction:   invoke void @may_throwv2(ptr nonnull %P)
          to label %Exit unwind label
-- 69. AssumeSimplifyPass
ERROR: Unsupported instruction:   invoke void @may_throwv2(ptr nonnull %P)
          to label %Exit unwind label
-- 70. VerifierPass : Skipping NOP
ERROR: Unsupported instruction:   invoke void @may_throwv2(ptr nonnull %P)
          to label %Exit unwind label
-- 71. VerifierPass : Skipping NOP
ERROR: Unsupported instruction:   invoke void @may_throwv2(ptr nonnull %P)
          to label %Exit unwind label
-- 72. PassManager<Function> : Skipping NOP
ERROR: Unsupported instruction:   invoke void @may_throwv2(ptr nonnull %P)
          to label %Exit unwind label
-- 73. PassManager<Function> : Skipping NOP
-- 74. AssumeBuilderPass

----------------------------------------
define i32 @test5(ptr %arg, i32 %arg1) {
bb:
  %i3 = sext i32 %arg1 to i64
  %i4 = gep inbounds ptr %arg, 2 x i64 %i3
  %i5 = load i16, ptr %i4, align 2
  %A = load i16, ptr %i4, align 4
  %i6 = sext i16 %i5 to i64
  %i7 = gep inbounds ptr %arg, 8 x i64 %i6
  %i8 = load i64, ptr %i7, align 16
  %B = load i64, ptr %i7, align 32
  %i9 = trunc i64 %i8 to i32
  ret i32 %i9
}
Transformation seems to be correct! (syntactically equal)

-- 75. AssumeBuilderPass

----------------------------------------
define i32 @test5(ptr %arg, i32 %arg1) {
bb:
  %i3 = sext i32 %arg1 to i64
  %i4 = gep inbounds ptr %arg, 2 x i64 %i3
  %i5 = load i16, ptr %i4, align 2
  %A = load i16, ptr %i4, align 4
  %i6 = sext i16 %i5 to i64
  %i7 = gep inbounds ptr %arg, 8 x i64 %i6
  %i8 = load i64, ptr %i7, align 16
  %B = load i64, ptr %i7, align 32
  %i9 = trunc i64 %i8 to i32
  ret i32 %i9
}
=>
define i32 @test5(ptr %arg, i32 %arg1) {
bb:
  %i3 = sext i32 %arg1 to i64
  %i4 = gep inbounds ptr %arg, 2 x i64 %i3
  assume_dereferenceable ptr %i4, i64 2
  assume_nonnull ptr %arg
  assume_align ptr %arg, i64 8
  %i5 = load i16, ptr %i4, align 2
  %A = load i16, ptr %i4, align 4
  %i6 = sext i16 %i5 to i64
  %i7 = gep inbounds ptr %arg, 8 x i64 %i6
  assume_dereferenceable ptr %i7, i64 8
  %i8 = load i64, ptr %i7, align 16
  %B = load i64, ptr %i7, align 32
  %i9 = trunc i64 %i8 to i32
  ret i32 %i9
}
Transformation doesn't verify! (not unsound)
ERROR: Timeout
-- 76. RequireAnalysisPass<DominatorTreeAnalysis, Function> : Skipping NOP
-- 77. RequireAnalysisPass<DominatorTreeAnalysis, Function> : Skipping NOP
-- 78. RequireAnalysisPass<AssumptionAnalysis, Function> : Skipping NOP
-- 79. RequireAnalysisPass<AssumptionAnalysis, Function> : Skipping NOP
-- 80. AssumeSimplifyPass

----------------------------------------
define i32 @test5(ptr %arg, i32 %arg1) {
bb:
  %i3 = sext i32 %arg1 to i64
  %i4 = gep inbounds ptr %arg, 2 x i64 %i3
  assume_dereferenceable ptr %i4, i64 2
  assume_nonnull ptr %arg
  assume_align ptr %arg, i64 8
  assume i1 1
  %i5 = load i16, ptr %i4, align 2
  %A = load i16, ptr %i4, align 4
  %i6 = sext i16 %i5 to i64
  %i7 = gep inbounds ptr %arg, 8 x i64 %i6
  assume_dereferenceable ptr %i7, i64 8
  assume i1 1
  %i8 = load i64, ptr %i7, align 16
  %B = load i64, ptr %i7, align 32
  %i9 = trunc i64 %i8 to i32
  ret i32 %i9
}
Transformation seems to be correct! (syntactically equal)

-- 81. AssumeSimplifyPass

----------------------------------------
define i32 @test5(ptr %arg, i32 %arg1) {
bb:
  %i3 = sext i32 %arg1 to i64
  %i4 = gep inbounds ptr %arg, 2 x i64 %i3
  assume_dereferenceable ptr %i4, i64 2
  assume_nonnull ptr %arg
  assume_align ptr %arg, i64 8
  %i5 = load i16, ptr %i4, align 2
  %A = load i16, ptr %i4, align 4
  %i6 = sext i16 %i5 to i64
  %i7 = gep inbounds ptr %arg, 8 x i64 %i6
  assume_dereferenceable ptr %i7, i64 8
  %i8 = load i64, ptr %i7, align 16
  %B = load i64, ptr %i7, align 32
  %i9 = trunc i64 %i8 to i32
  ret i32 %i9
}
=>
define i32 @test5(ptr nonnull align(8) %arg, i32 %arg1) {
bb:
  %i3 = sext i32 %arg1 to i64
  %i4 = gep inbounds ptr nonnull align(8) %arg, 2 x i64 %i3
  %i5 = load i16, ptr %i4, align 2
  %A = load i16, ptr %i4, align 4
  %i6 = sext i16 %i5 to i64
  %i7 = gep inbounds ptr nonnull align(8) %arg, 8 x i64 %i6
  assume_dereferenceable ptr %i4, i64 2
  assume_dereferenceable ptr %i7, i64 8
  %i8 = load i64, ptr %i7, align 16
  %B = load i64, ptr %i7, align 32
  %i9 = trunc i64 %i8 to i32
  ret i32 %i9
}
Transformation doesn't verify! (unsound)
ERROR: Source is more defined than target

Example:
ptr %arg = pointer(non-local, block_id=1, offset=94) / Address=#x000000060
i32 %arg1 = #x00000000 (0)

Source:
i64 %i3 = #x0000000000000000 (0)
ptr %i4 = pointer(non-local, block_id=1, offset=94) / Address=#x000000060
i16 %i5 = #xfff8 (65528, -8)
i16 %A = #xfff8 (65528, -8)
i64 %i6 = #xfffffffffffffff8 (18446744073709551608, -8)
ptr %i7 = pointer(non-local, block_id=1, offset=30) / Address=#x000000020
i64 %i8 = #xfff8fff8fff8fff8 (18444773718807347192, -1970354902204424)
i64 %B = #xfff8fff8fff8fff8 (18444773718807347192, -1970354902204424)
i32 %i9 = #xfff8fff8 (4294508536, -458760)

SOURCE MEMORY STATE
===================
NON-LOCAL BLOCKS:
Block 0 >	size: 0	align: 2	alloc type: 0	alive: false	address: 0
Block 1 >	size: 98	align: 2	alloc type: 0	alive: true	address: 2
Contents:
*: #xfff8


Target:
i64 %i3 = UB triggered!


Pass: AssumeSimplifyPass
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' '-passes=assume-builder,require<domtree>,require<assumptions>,assume-simplify,verify' '--enable-knowledge-retention' '-S' '/bitbucket/nlopes/llvm/llvm/test/Transforms/Util/assume-builder.ll' '-tv-smt-to=20000' '-tv-report-dir=/home/nlopes/alive2/build/logs' '-tv-smt-stats'
Wrote bitcode to: "/home/nlopes/alive2/build/logs/assume-builder_93SZQj1B_dxg9.bc"


------------------- SMT STATS -------------------
Num queries: 71
Num invalid: 0
Num skips:   0
Num trivial: 52 (42.3%)
Num timeout: 6 (8.5%)
Num errors:  0 (0.0%)
Num SAT:     38 (53.5%)
Num UNSAT:   27 (38.0%)
Alive2: Transform doesn't verify; aborting!

stderr:

RUN: at line 2: /home/nlopes/alive2/build/opt-alive.sh -passes='assume-builder,verify' --enable-knowledge-retention -S /bitbucket/nlopes/llvm/llvm/test/Transforms/Util/assume-builder.ll | /bitbucket/nlopes/llvm/build/bin/FileCheck /bitbucket/nlopes/llvm/llvm/test/Transforms/Util/assume-builder.ll --check-prefixes=BASIC
+ /home/nlopes/alive2/build/opt-alive.sh -passes=assume-builder,verify --enable-knowledge-retention -S /bitbucket/nlopes/llvm/llvm/test/Transforms/Util/assume-builder.ll
+ /bitbucket/nlopes/llvm/build/bin/FileCheck /bitbucket/nlopes/llvm/llvm/test/Transforms/Util/assume-builder.ll --check-prefixes=BASIC
RUN: at line 3: /home/nlopes/alive2/build/opt-alive.sh -passes='assume-builder,verify' --enable-knowledge-retention --assume-preserve-all -S /bitbucket/nlopes/llvm/llvm/test/Transforms/Util/assume-builder.ll | /bitbucket/nlopes/llvm/build/bin/FileCheck /bitbucket/nlopes/llvm/llvm/test/Transforms/Util/assume-builder.ll --check-prefixes=ALL
+ /bitbucket/nlopes/llvm/build/bin/FileCheck /bitbucket/nlopes/llvm/llvm/test/Transforms/Util/assume-builder.ll --check-prefixes=ALL
+ /home/nlopes/alive2/build/opt-alive.sh -passes=assume-builder,verify --enable-knowledge-retention --assume-preserve-all -S /bitbucket/nlopes/llvm/llvm/test/Transforms/Util/assume-builder.ll
RUN: at line 4: /home/nlopes/alive2/build/opt-alive.sh -passes='require<assumptions>,assume-builder,verify' --enable-knowledge-retention -S /bitbucket/nlopes/llvm/llvm/test/Transforms/Util/assume-builder.ll | /bitbucket/nlopes/llvm/build/bin/FileCheck /bitbucket/nlopes/llvm/llvm/test/Transforms/Util/assume-builder.ll --check-prefixes=WITH-AC
+ /bitbucket/nlopes/llvm/build/bin/FileCheck /bitbucket/nlopes/llvm/llvm/test/Transforms/Util/assume-builder.ll --check-prefixes=WITH-AC
+ /home/nlopes/alive2/build/opt-alive.sh '-passes=require<assumptions>,assume-builder,verify' --enable-knowledge-retention -S /bitbucket/nlopes/llvm/llvm/test/Transforms/Util/assume-builder.ll
RUN: at line 5: /home/nlopes/alive2/build/opt-alive.sh -passes='require<domtree>,require<assumptions>,assume-builder,verify' --enable-knowledge-retention -S /bitbucket/nlopes/llvm/llvm/test/Transforms/Util/assume-builder.ll | /bitbucket/nlopes/llvm/build/bin/FileCheck /bitbucket/nlopes/llvm/llvm/test/Transforms/Util/assume-builder.ll --check-prefixes=CROSS-BLOCK
+ /bitbucket/nlopes/llvm/build/bin/FileCheck /bitbucket/nlopes/llvm/llvm/test/Transforms/Util/assume-builder.ll --check-prefixes=CROSS-BLOCK
+ /home/nlopes/alive2/build/opt-alive.sh '-passes=require<domtree>,require<assumptions>,assume-builder,verify' --enable-knowledge-retention -S /bitbucket/nlopes/llvm/llvm/test/Transforms/Util/assume-builder.ll
RUN: at line 6: /home/nlopes/alive2/build/opt-alive.sh -passes='assume-builder,require<domtree>,require<assumptions>,assume-simplify,verify' --enable-knowledge-retention -S /bitbucket/nlopes/llvm/llvm/test/Transforms/Util/assume-builder.ll | /bitbucket/nlopes/llvm/build/bin/FileCheck /bitbucket/nlopes/llvm/llvm/test/Transforms/Util/assume-builder.ll --check-prefixes=FULL-SIMPLIFY
+ /bitbucket/nlopes/llvm/build/bin/FileCheck /bitbucket/nlopes/llvm/llvm/test/Transforms/Util/assume-builder.ll --check-prefixes=FULL-SIMPLIFY
+ /home/nlopes/alive2/build/opt-alive.sh '-passes=assume-builder,require<domtree>,require<assumptions>,assume-simplify,verify' --enable-knowledge-retention -S /bitbucket/nlopes/llvm/llvm/test/Transforms/Util/assume-builder.ll

FileCheck error: '<stdin>' is empty.
FileCheck command line:  /bitbucket/nlopes/llvm/build/bin/FileCheck /bitbucket/nlopes/llvm/llvm/test/Transforms/Util/assume-builder.ll --check-prefixes=FULL-SIMPLIFY

<-- Back