Test source: git
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_align ptr %P, i64 8
store i32 0, ptr %P, align 8
store i32 0, ptr %P1, align 8
br label %C
C:
assume_align ptr %P, i64 32
store i32 0, ptr %P, align 32
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_align ptr %P, i64 8
assume i1 1
store i32 0, ptr %P, align 8
store i32 0, ptr %P1, align 8
br label %C
C:
assume_align ptr %P, i64 32
assume i1 1
store i32 0, ptr %P, align 32
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_align ptr %P, i64 8
store i32 0, ptr %P, align 8
store i32 0, ptr %P1, align 8
br label %C
C:
assume_align ptr %P, i64 32
store i32 0, ptr %P, align 32
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 seems to be correct!
-- 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=127) / Address=#x000000088
i32 %arg1 = #x00000000 (0)
Source:
i64 %i3 = #x0000000000000000 (0)
ptr %i4 = pointer(non-local, block_id=1, offset=127) / Address=#x000000088
i16 %i5 = #xfff3 (65523, -13)
i16 %A = #xfff3 (65523, -13)
i64 %i6 = #xfffffffffffffff3 (18446744073709551603, -13)
ptr %i7 = pointer(non-local, block_id=1, offset=23) / Address=#x000000020
i64 %i8 = #xfff3fff3fff3fff3 (18443366322448629747, -3377751260921869)
i64 %B = #xfff3fff3fff3fff3 (18443366322448629747, -3377751260921869)
i32 %i9 = #xfff3fff3 (4294180851, -786445)
SOURCE MEMORY STATE
===================
NON-LOCAL BLOCKS:
Block 0 > size: 0 align: 2 alloc type: 0 alive: false address: 0
Block 1 > size: 131 align: 1 alloc type: 0 alive: true address: 9
Contents:
*: #xfff3
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_mRQKYzOu_QC43.bc"
------------------- SMT STATS -------------------
Num queries: 73
Num invalid: 0
Num skips: 0
Num trivial: 51 (41.1%)
Num timeout: 4 (5.5%)
Num errors: 0 (0.0%)
Num SAT: 39 (53.4%)
Num UNSAT: 30 (41.1%)
Alive2: Transform doesn't verify; aborting!
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 + /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 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 + /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 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 + /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 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 + /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 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