Test source: git
Source: <stdin> ERROR: Unsupported instruction: %addrspcast = addrspacecast i8* %p to i8 addrspace(1)* ---------------------------------------- define void @nonnullAfterBitCast() { %entry: %i = alloca i64 4, align 4 %tmp1 = bitcast * %i to * call void @foo(* %tmp1) ret void } => define void @nonnullAfterBitCast() { %entry: %i = alloca i64 4, align 4 %tmp1 = bitcast * %i to * call void @foo(nonnull * %tmp1) ret void } Transformation seems to be correct! ---------------------------------------- define void @nonnullAfterSExt(i8 %a) { %entry: %b = zext i8 %a to i32 %c = add nsw nuw i32 %b, 2 %sext = sext i32 %c to i64 %i2p = int2ptr i64 %sext to * call void @foo(* %i2p) ret void } => define void @nonnullAfterSExt(i8 %a) { %entry: %b = zext i8 %a to i64 %c = add nsw nuw i64 %b, 2 %i2p = int2ptr i64 %c to * call void @foo(nonnull * %i2p) ret void } Transformation doesn't verify! ERROR: Couldn't prove the correctness of the transformation Alive2 approximated the semantics of the programs and therefore we cannot conclude whether the bug found is valid or not. Approximations done: - inttoptr ---------------------------------------- define void @nonnullAfterZExt(i8 %a) { %entry: %b = zext i8 %a to i32 %c = add nsw nuw i32 %b, 2 %zext = zext i32 %c to i64 %i2p = int2ptr i64 %zext to * call void @foo(* %i2p) ret void } => define void @nonnullAfterZExt(i8 %a) { %entry: %b = zext i8 %a to i64 %c = add nsw nuw i64 %b, 2 %i2p = int2ptr i64 %c to * call void @foo(nonnull * %i2p) ret void } Transformation doesn't verify! ERROR: Couldn't prove the correctness of the transformation Alive2 approximated the semantics of the programs and therefore we cannot conclude whether the bug found is valid or not. Approximations done: - inttoptr - inttoptr ---------------------------------------- define void @nonnullAfterInt2Ptr(i32 %u, i64 %lu) { %entry: %nz = sdiv exact i32 100, %u %i2p = int2ptr i32 %nz to * call void @foo(* %i2p) %nz.2 = sdiv exact i64 100, %lu %i2p.2 = int2ptr i64 %nz.2 to * call void @foo(* %i2p.2) ret void } => define void @nonnullAfterInt2Ptr(i32 %u, i64 %lu) { %entry: %nz = sdiv exact i32 100, %u %0 = zext i32 %nz to i64 %i2p = int2ptr i64 %0 to * call void @foo(nonnull * %i2p) %nz.2 = sdiv exact i64 100, %lu %i2p.2 = int2ptr i64 %nz.2 to * call void @foo(nonnull * %i2p.2) ret void } Transformation doesn't verify! ERROR: Couldn't prove the correctness of the transformation Alive2 approximated the semantics of the programs and therefore we cannot conclude whether the bug found is valid or not. Approximations done: - inttoptr - inttoptr ---------------------------------------- define void @nonnullAfterPtr2Int() { %entry: %a = alloca i64 4, align 4 %p2i = ptrtoint * %a to i64 %i2p = int2ptr i64 %p2i to * call void @foo(* %i2p) ret void } => define void @nonnullAfterPtr2Int() { %entry: %a = alloca i64 4, align 4 %i2p = bitcast * %a to * call void @foo(nonnull * %i2p) ret void } Transformation doesn't verify! ERROR: Source is more defined than target Example: Source: * %a = pointer(local, block_id=4, offset=0) i64 %p2i = #x8000000000000000 (9223372036854775808, -9223372036854775808) * %i2p = pointer(non-local, block_id=0, offset=-2346676772369940628) SOURCE MEMORY STATE =================== NON-LOCAL BLOCKS: Block 0 > size: 0 align: 1 alloc type: 0 address: 0 Block 1 > size: 63122977054597352 align: 1 alloc type: 0 address: 360296788411942688 Block 2 > size: 4611690417016802304 align: 1 alloc type: 1 address: 0 LOCAL BLOCKS: Block 4 > size: 4 align: 4 alloc type: 1 address: 9223372036854775808 Target: * %a = pointer(local, block_id=4, offset=0) * %i2p = pointer(local, block_id=4, offset=0) TARGET MEMORY STATE =================== LOCAL BLOCKS: Block 4 > size: 4 align: 4 alloc type: 1 address: 9223372036854775808 ------------------- SMT STATS ------------------- Num queries: 10 Num invalid: 0 Num skips: 0 Num trivial: 6 (37.5%) Num timeout: 0 (0.0%) Num errors: 0 (0.0%) Num SAT: 10 (100.0%) Num UNSAT: 0 (0.0%)
+ : 'RUN: at line 1' + /home/nlopes/alive2/build/opt-alive.sh -instcombine -S + /home/nlopes/llvm/build/bin/FileCheck --allow-unused-prefixes=false /home/nlopes/llvm/llvm/test/Transforms/InstCombine/callsite_nonnull_args_through_casts.ll Alive2: Transform doesn't verify; aborting! FileCheck error: '<stdin>' is empty. FileCheck command line: /home/nlopes/llvm/build/bin/FileCheck --allow-unused-prefixes=false /home/nlopes/llvm/llvm/test/Transforms/InstCombine/callsite_nonnull_args_through_casts.ll