Test Failure: Transforms/InstCombine/load-bitcast-select.ll

Test source: git

Log:

Source: <stdin>

----------------------------------------
@a = global 4000 bytes, align 16
@b = global 4000 bytes, align 16

define void @_Z3foov() {
%entry:
  br label %for.cond

%for.cond:
  %i.0 = phi i32 [ 0, %entry ], [ %inc, %for.body ]
  %cmp = icmp ult i32 %i.0, 1000
  br i1 %cmp, label %for.body, label %for.cond.cleanup

%for.body:
  %0 = zext i32 %i.0 to i64
  %arrayidx = gep inbounds * @a, 4000 x i64 0, 4 x i64 %0
  %arrayidx2 = gep inbounds * @b, 4000 x i64 0, 4 x i64 %0
  %1 = load float, * %arrayidx, align 4
  %2 = load float, * %arrayidx2, align 4
  %cmp.i = fcmp fast olt float %1, %2
  %__b.__a.i = select i1 %cmp.i, * %arrayidx2, * %arrayidx
  %3 = bitcast * %__b.__a.i to *
  %4 = load i32, * %3, align 4
  %5 = bitcast * %arrayidx to *
  store i32 %4, * %5, align 4
  %inc = add nsw nuw i32 %i.0, 1
  br label %for.cond

%for.cond.cleanup:
  ret void
}
=>
@a = global 4000 bytes, align 16
@b = global 4000 bytes, align 16

define void @_Z3foov() {
%entry:
  br label %for.cond

%for.cond:
  %i.0 = phi i32 [ 0, %entry ], [ %inc, %for.body ]
  %cmp = icmp ult i32 %i.0, 1000
  br i1 %cmp, label %for.body, label %for.cond.cleanup

%for.body:
  %0 = zext i32 %i.0 to i64
  %arrayidx = gep inbounds * @a, 4000 x i64 0, 4 x i64 %0
  %arrayidx2 = gep inbounds * @b, 4000 x i64 0, 4 x i64 %0
  %1 = load float, * %arrayidx, align 4
  %2 = load float, * %arrayidx2, align 4
  %cmp.i = fcmp fast olt float %1, %2
  %3 = select i1 %cmp.i, float %2, float %1
  store float %3, * %arrayidx, align 4
  %inc = add nsw nuw i32 %i.0, 1
  br label %for.cond

%for.cond.cleanup:
  ret void
}
Transformation doesn't verify!
ERROR: Precondition is always false

ERROR: Unsupported attribute: dereferenceable(4)
ERROR: Unsupported attribute: dereferenceable(4)

----------------------------------------
define void @bitcasted_store(i1 %cond, * %loadaddr1, * %loadaddr2, * %storeaddr) {
%0:
  %sel = select i1 %cond, * %loadaddr1, * %loadaddr2
  %int_load_addr = bitcast * %sel to *
  %ld = load i32, * %int_load_addr, align 4
  %int_store_addr = bitcast * %storeaddr to *
  store i32 %ld, * %int_store_addr, align 4
  ret void
}
=>
define void @bitcasted_store(i1 %cond, * %loadaddr1, * %loadaddr2, * %storeaddr) {
%0:
  %sel = select i1 %cond, * %loadaddr1, * %loadaddr2
  %int_load_addr = bitcast * %sel to *
  %ld = load i32, * %int_load_addr, align 4
  %int_store_addr = bitcast * %storeaddr to *
  store i32 %ld, * %int_store_addr, align 4
  ret void
}
Transformation doesn't verify!
ERROR: Timeout


----------------------------------------
define void @bitcasted_minmax_with_select_of_pointers(* %loadaddr1, * %loadaddr2, * %storeaddr) {
%0:
  %ld1 = load float, * %loadaddr1, align 4
  %ld2 = load float, * %loadaddr2, align 4
  %cond = fcmp ogt float %ld1, %ld2
  %sel = select i1 %cond, * %loadaddr1, * %loadaddr2
  %int_load_addr = bitcast * %sel to *
  %ld = load i32, * %int_load_addr, align 4
  %int_store_addr = bitcast * %storeaddr to *
  store i32 %ld, * %int_store_addr, align 4
  ret void
}
=>
define void @bitcasted_minmax_with_select_of_pointers(* %loadaddr1, * %loadaddr2, * %storeaddr) {
%0:
  %ld1 = load float, * %loadaddr1, align 4
  %ld2 = load float, * %loadaddr2, align 4
  %cond = fcmp ogt float %ld1, %ld2
  %ld3 = select i1 %cond, float %ld1, float %ld2
  store float %ld3, * %storeaddr, align 4
  ret void
}
Transformation doesn't verify!
ERROR: Mismatch in memory

Example:
* %loadaddr1 = pointer(non-local, block_id=3, offset=0)
* %loadaddr2 = pointer(non-local, block_id=1, offset=0)
* %storeaddr = pointer(non-local, block_id=1, offset=0)

Source:
float %ld1 = #x00002100 (0.000000000000?)
float %ld2 = NaN
i1 %cond = #x0 (0)
* %sel = pointer(non-local, block_id=1, offset=0)
* %int_load_addr = pointer(non-local, block_id=1, offset=0)
i32 %ld = #x7f800800 (2139097088)
* %int_store_addr = pointer(non-local, block_id=1, offset=0)

SOURCE MEMORY STATE
===================
NON-LOCAL BLOCKS:
Block 0 >	size: 0	align: 64	alloc type: 0
Block 1 >	size: 13	align: 0	alloc type: 0
Block 2 >	align: 0	alloc type: 0
Block 3 >	size: 6	align: 65536	alloc type: 0

Target:
float %ld1 = #x00002100 (0.000000000000?)
float %ld2 = NaN
i1 %cond = #x0 (0)
float %ld3 = NaN

Mismatch in pointer(non-local, block_id=1, offset=0)
Source value: #x7f800800
Target value: #x7f801000


------------------- SMT STATS -------------------
Num queries: 7
Num invalid: 0
Num skips:   0
Num trivial: 4 (36.4%)
Num timeout: 1 (14.3%)
Num errors:  0 (0.0%)
Num SAT:     3 (42.9%)
Num UNSAT:   3 (42.9%)

stderr:

+ : 'RUN: at line 2'
+ /home/nlopes/alive2/scripts/opt-alive.sh -instcombine -S -data-layout=e-m:e-i64:64-f80:128-n8:16:32:64-S128
+ /home/nlopes/llvm/build/bin/FileCheck /home/nlopes/llvm/llvm/test/Transforms/InstCombine/load-bitcast-select.ll

Alive2: Transform doesn't verify; aborting!
FileCheck error: '<stdin>' is empty.
FileCheck command line:  /home/nlopes/llvm/build/bin/FileCheck /home/nlopes/llvm/llvm/test/Transforms/InstCombine/load-bitcast-select.ll

<-- Back