Test source: git
Comments: Alive2 bug with fn calls memory comparison
Source: /bitbucket/nlopes/llvm/llvm/test/Transforms/DeadStoreElimination/captures-before-load.ll -- 1. ModuleToFunctionPassAdaptor ERROR: Unsupported attribute: noalias -- 1. PassManager<Function> : Skipping NOP -- 2. DSEPass ---------------------------------------- declare void @escape_and_clobber(ptr) define i32 @test_not_captured_before_load_same_bb(ptr %in.ptr) { #0: %a = alloca i64 4, align 4 store i32 55, ptr %a, align 4 %in.lv.1 = load ptr, ptr %in.ptr, align 2 %in.lv.2 = load i32, ptr %in.lv.1, align 2 store i32 99, ptr %a, align 4 call void @escape_and_clobber(ptr %a) ret i32 %in.lv.2 } Transformation seems to be correct! (syntactically equal) -- 3. DSEPass ---------------------------------------- declare void @escape_and_clobber(ptr) define i32 @test_not_captured_before_load_same_bb(ptr %in.ptr) { #0: %a = alloca i64 4, align 4 store i32 55, ptr %a, align 4 %in.lv.1 = load ptr, ptr %in.ptr, align 2 %in.lv.2 = load i32, ptr %in.lv.1, align 2 store i32 99, ptr %a, align 4 call void @escape_and_clobber(ptr %a) ret i32 %in.lv.2 } => declare void @escape_and_clobber(ptr) define i32 @test_not_captured_before_load_same_bb(ptr %in.ptr) { #0: %a = alloca i64 4, align 4 %in.lv.1 = load ptr, ptr %in.ptr, align 2 %in.lv.2 = load i32, ptr %in.lv.1, align 2 store i32 99, ptr %a, align 4 call void @escape_and_clobber(ptr %a) ret i32 %in.lv.2 } Transformation seems to be correct! -- 4. PassManager<Function> : Skipping NOP -- 5. PassManager<Function> : Skipping NOP -- 6. DSEPass ---------------------------------------- declare void @escape_and_clobber(ptr) define i32 @test_not_captured_before_load_same_bb_escape_unreachable_block(ptr %in.ptr) { #0: %a = alloca i64 4, align 4 store i32 55, ptr %a, align 4 %in.lv.1 = load ptr, ptr %in.ptr, align 2 %in.lv.2 = load i32, ptr %in.lv.1, align 2 store i32 99, ptr %a, align 4 call void @escape_and_clobber(ptr %a) ret i32 %in.lv.2 unreach: call void @escape_and_clobber(ptr %a) ret i32 0 } Transformation seems to be correct! (syntactically equal) -- 7. DSEPass ---------------------------------------- declare void @escape_and_clobber(ptr) define i32 @test_not_captured_before_load_same_bb_escape_unreachable_block(ptr %in.ptr) { #0: %a = alloca i64 4, align 4 store i32 55, ptr %a, align 4 %in.lv.1 = load ptr, ptr %in.ptr, align 2 %in.lv.2 = load i32, ptr %in.lv.1, align 2 store i32 99, ptr %a, align 4 call void @escape_and_clobber(ptr %a) ret i32 %in.lv.2 } => declare void @escape_and_clobber(ptr) define i32 @test_not_captured_before_load_same_bb_escape_unreachable_block(ptr %in.ptr) { #0: %a = alloca i64 4, align 4 %in.lv.1 = load ptr, ptr %in.ptr, align 2 %in.lv.2 = load i32, ptr %in.lv.1, align 2 store i32 99, ptr %a, align 4 call void @escape_and_clobber(ptr %a) ret i32 %in.lv.2 } Transformation seems to be correct! -- 8. PassManager<Function> : Skipping NOP -- 9. PassManager<Function> : Skipping NOP -- 10. DSEPass ---------------------------------------- declare void @escape_and_clobber(ptr) define i32 @test_not_captured_before_load_same_bb_escape_unreachable_block2(ptr %in.ptr) { #0: br label %bb unreach: call void @escape_and_clobber(ptr poison) ret i32 0 bb: %a = alloca i64 4, align 4 store i32 55, ptr %a, align 4 %in.lv.1 = load ptr, ptr %in.ptr, align 2 %in.lv.2 = load i32, ptr %in.lv.1, align 2 store i32 99, ptr %a, align 4 call void @escape_and_clobber(ptr %a) ret i32 %in.lv.2 } Transformation seems to be correct! (syntactically equal) -- 11. DSEPass ---------------------------------------- declare void @escape_and_clobber(ptr) define i32 @test_not_captured_before_load_same_bb_escape_unreachable_block2(ptr %in.ptr) { #0: br label %bb bb: %a = alloca i64 4, align 4 store i32 55, ptr %a, align 4 %in.lv.1 = load ptr, ptr %in.ptr, align 2 %in.lv.2 = load i32, ptr %in.lv.1, align 2 store i32 99, ptr %a, align 4 call void @escape_and_clobber(ptr %a) ret i32 %in.lv.2 } => declare void @escape_and_clobber(ptr) define i32 @test_not_captured_before_load_same_bb_escape_unreachable_block2(ptr %in.ptr) { #0: br label %bb bb: %a = alloca i64 4, align 4 %in.lv.1 = load ptr, ptr %in.ptr, align 2 %in.lv.2 = load i32, ptr %in.lv.1, align 2 store i32 99, ptr %a, align 4 call void @escape_and_clobber(ptr %a) ret i32 %in.lv.2 } Transformation seems to be correct! -- 12. PassManager<Function> : Skipping NOP -- 13. PassManager<Function> : Skipping NOP -- 14. DSEPass ---------------------------------------- declare void @escape_and_clobber(ptr) declare void @clobber() define i32 @test_captured_and_clobbered_after_load_same_bb_2(ptr %in.ptr) { #0: %a = alloca i64 4, align 4 store i32 55, ptr %a, align 4 %in.lv.1 = load ptr, ptr %in.ptr, align 2 %in.lv.2 = load i32, ptr %in.lv.1, align 2 call void @escape_and_clobber(ptr %a) store i32 99, ptr %a, align 4 call void @clobber() ret i32 %in.lv.2 } Transformation seems to be correct! (syntactically equal) -- 15. DSEPass ---------------------------------------- declare void @escape_and_clobber(ptr) declare void @clobber() define i32 @test_captured_and_clobbered_after_load_same_bb_2(ptr %in.ptr) { #0: %a = alloca i64 4, align 4 store i32 55, ptr %a, align 4 %in.lv.1 = load ptr, ptr %in.ptr, align 2 %in.lv.2 = load i32, ptr %in.lv.1, align 2 call void @escape_and_clobber(ptr %a) store i32 99, ptr %a, align 4 call void @clobber() ret i32 %in.lv.2 } Transformation seems to be correct! (syntactically equal) -- 16. PassManager<Function> : Skipping NOP -- 17. PassManager<Function> : Skipping NOP -- 18. DSEPass ---------------------------------------- declare void @escape_writeonly(ptr) declare void @clobber() define i32 @test_captured_after_load_same_bb_2_clobbered_later(ptr %in.ptr) { #0: %a = alloca i64 4, align 4 store i32 55, ptr %a, align 4 %in.lv.1 = load ptr, ptr %in.ptr, align 2 %in.lv.2 = load i32, ptr %in.lv.1, align 2 call void @escape_writeonly(ptr %a) memory(write) store i32 99, ptr %a, align 4 call void @clobber() ret i32 %in.lv.2 } Transformation seems to be correct! (syntactically equal) -- 19. DSEPass ---------------------------------------- declare void @escape_writeonly(ptr) declare void @clobber() define i32 @test_captured_after_load_same_bb_2_clobbered_later(ptr %in.ptr) { #0: %a = alloca i64 4, align 4 store i32 55, ptr %a, align 4 %in.lv.1 = load ptr, ptr %in.ptr, align 2 %in.lv.2 = load i32, ptr %in.lv.1, align 2 call void @escape_writeonly(ptr %a) memory(write) store i32 99, ptr %a, align 4 call void @clobber() ret i32 %in.lv.2 } => declare void @escape_writeonly(ptr) declare void @clobber() define i32 @test_captured_after_load_same_bb_2_clobbered_later(ptr %in.ptr) { #0: %a = alloca i64 4, align 4 %in.lv.1 = load ptr, ptr %in.ptr, align 2 %in.lv.2 = load i32, ptr %in.lv.1, align 2 call void @escape_writeonly(ptr %a) memory(write) store i32 99, ptr %a, align 4 call void @clobber() ret i32 %in.lv.2 } Transformation doesn't verify! (unsound) ERROR: Source is more defined than target Example: ptr %in.ptr = pointer(non-local, block_id=1, offset=0) Source: ptr %a = null ptr %in.lv.1 = pointer(non-local, block_id=1, offset=0) i32 %in.lv.2 = poison void = function did not return! SOURCE MEMORY STATE =================== NON-LOCAL BLOCKS: Block 0 > size: 0 align: 2 alloc type: 0 alive: false address: 0 Block 1 > size: 9 align: 1 alloc type: 0 alive: true address: 12 Contents: if (and (= idx #b0000010) (not (= idx #b0000011)) (not (= idx #b0000001))) pointer(non-local, block_id=1, offset=0), byte offset=2 else if (and (not (= idx #b0000010)) (not (= idx #b0000011)) (not (= idx #b0000001))) pointer(non-local, block_id=1, offset=0), byte offset=0 else if (= idx #b0000001) pointer(non-local, block_id=1, offset=0), byte offset=1 else if (and (= idx #b0000011) (not (= idx #b0000001))) pointer(non-local, block_id=1, offset=0), byte offset=3 else poison Block 2 > size: 0 align: 1 alloc type: 0 alive: true address: 5 Contents: if (and (= idx #b0000010) (not (= idx #b0000011)) (not (= idx #b0000001))) pointer(non-local, block_id=1, offset=0), byte offset=2 else if (and (not (= idx #b0000010)) (not (= idx #b0000011)) (not (= idx #b0000001))) pointer(non-local, block_id=1, offset=0), byte offset=0 else if (= idx #b0000001) pointer(non-local, block_id=1, offset=0), byte offset=1 else if (and (= idx #b0000011) (not (= idx #b0000001))) pointer(non-local, block_id=1, offset=0), byte offset=3 else poison Block 3 > align: 2 alloc type: 0 alive: true Contents: if (and (= idx #b0000010) (not (= idx #b0000011)) (not (= idx #b0000001))) pointer(non-local, block_id=1, offset=0), byte offset=2 else if (and (not (= idx #b0000010)) (not (= idx #b0000011)) (not (= idx #b0000001))) pointer(non-local, block_id=1, offset=0), byte offset=0 else if (= idx #b0000001) pointer(non-local, block_id=1, offset=0), byte offset=1 else if (and (= idx #b0000011) (not (= idx #b0000001))) pointer(non-local, block_id=1, offset=0), byte offset=3 else poison LOCAL BLOCKS: Block 4 > size: 4 align: 4 alloc type: 1 alive: true Target: ptr %a = null ptr %in.lv.1 = pointer(non-local, block_id=1, offset=0) i32 %in.lv.2 = poison Function @escape_writeonly triggered UB TARGET MEMORY STATE =================== LOCAL BLOCKS: Block 4 > size: 4 align: 4 alloc type: 1 alive: true address: 256 Pass: DSEPass 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=dse' '-S' '/bitbucket/nlopes/llvm/llvm/test/Transforms/DeadStoreElimination/captures-before-load.ll' '-tv-smt-to=20000' '-tv-report-dir=/home/nlopes/alive2/build/logs' '-tv-smt-stats' Wrote bitcode to: "/home/nlopes/alive2/build/logs/captures-before-load_UJQdV76b_tODX.bc" ------------------- SMT STATS ------------------- Num queries: 43 Num invalid: 0 Num skips: 0 Num trivial: 17 (28.3%) Num timeout: 0 (0.0%) Num errors: 0 (0.0%) Num SAT: 31 (72.1%) Num UNSAT: 12 (27.9%) Alive2: Transform doesn't verify; aborting!
RUN: at line 2: /home/nlopes/alive2/build/opt-alive.sh -passes='dse' -S /bitbucket/nlopes/llvm/llvm/test/Transforms/DeadStoreElimination/captures-before-load.ll | /bitbucket/nlopes/llvm/build/bin/FileCheck /bitbucket/nlopes/llvm/llvm/test/Transforms/DeadStoreElimination/captures-before-load.ll + /home/nlopes/alive2/build/opt-alive.sh -passes=dse -S /bitbucket/nlopes/llvm/llvm/test/Transforms/DeadStoreElimination/captures-before-load.ll + /bitbucket/nlopes/llvm/build/bin/FileCheck /bitbucket/nlopes/llvm/llvm/test/Transforms/DeadStoreElimination/captures-before-load.ll FileCheck error: '<stdin>' is empty. FileCheck command line: /bitbucket/nlopes/llvm/build/bin/FileCheck /bitbucket/nlopes/llvm/llvm/test/Transforms/DeadStoreElimination/captures-before-load.ll