Test Failure: Transforms/ConstraintElimination/loops-header-tested-pointer-cmps.ll

Test source: git

Log:

Source: /home/nlopes/llvm/llvm/test/Transforms/ConstraintElimination/loops-header-tested-pointer-cmps.ll

----------------------------------------
define void @test1(* %src, * noundef %lower, * noundef %upper, i8 %N) {
%entry:
  %src.end = gep inbounds * %src, 1 x i8 %N
  %cmp.src.start = icmp ult * %src, noundef %lower
  %cmp.src.end = icmp uge * %src.end, noundef %upper
  %or.0 = or i1 %cmp.src.start, %cmp.src.end
  br i1 %or.0, label %trap.bb, label %loop.header

%loop.header:
  %iv = phi i8 [ 0, %entry ], [ %iv.next, %loop.latch ]
  %ec = icmp uge i8 %iv, %N
  br i1 %ec, label %exit, label %loop.body

%exit:
  ret void

%loop.body:
  %src.iv = gep inbounds * %src, 1 x i8 %iv
  %cmp.iv.start = icmp ult * %src.iv, noundef %lower
  %cmp.iv.end = icmp uge * %src.iv, noundef %upper
  %or.1 = or i1 %cmp.iv.start, %cmp.iv.end
  br i1 %or.1, label %trap.bb, label %loop.body.1

%loop.body.1:
  %ptr.src.iv = bitcast * %src.iv to *
  store i32 0, * %ptr.src.iv, align 4
  %add.1 = add nsw nuw i8 %iv, 1
  %src.iv.1 = gep inbounds * %src, 1 x i8 %add.1
  %cmp.iv.1.start = icmp ult * %src.iv.1, noundef %lower
  %cmp.iv.1.end = icmp uge * %src.iv.1, noundef %upper
  %or.2 = or i1 %cmp.iv.1.start, %cmp.iv.1.end
  br i1 %or.2, label %trap.bb, label %loop.body.2

%loop.body.2:
  %ptr.src.iv.1 = bitcast * %src.iv.1 to *
  store i32 0, * %ptr.src.iv.1, align 4
  %add.2 = add nsw nuw i8 %iv, 2
  %src.iv.2 = gep inbounds * %src, 1 x i8 %add.2
  %cmp.iv.2.start = icmp ult * %src.iv.2, noundef %lower
  %cmp.iv.2.end = icmp uge * %src.iv.2, noundef %upper
  %or.3 = or i1 %cmp.iv.2.start, %cmp.iv.2.end
  br i1 %or.3, label %trap.bb, label %loop.latch

%loop.latch:
  %ptr.src.iv.2 = bitcast * %src.iv.2 to *
  store i32 0, * %ptr.src.iv.2, align 4
  %iv.next = add nsw nuw i8 %iv, 1
  br label %loop.header

%trap.bb:
  ret void
}
=>
define void @test1(* %src, * noundef %lower, * noundef %upper, i8 %N) {
%entry:
  %src.end = gep inbounds * %src, 1 x i8 %N
  %cmp.src.start = icmp ult * %src, noundef %lower
  %cmp.src.end = icmp uge * %src.end, noundef %upper
  %or.0 = or i1 %cmp.src.start, %cmp.src.end
  br i1 %or.0, label %trap.bb, label %loop.header

%loop.header:
  %iv = phi i8 [ 0, %entry ], [ %iv.next, %loop.latch ]
  %ec = icmp uge i8 %iv, %N
  br i1 %ec, label %exit, label %loop.body

%exit:
  ret void

%loop.body:
  %src.iv = gep inbounds * %src, 1 x i8 %iv
  %cmp.iv.start = icmp ult * %src.iv, noundef %lower
  %cmp.iv.end = icmp uge * %src.iv, noundef %upper
  %or.1 = or i1 %cmp.iv.start, 0
  br i1 %or.1, label %trap.bb, label %loop.body.1

%loop.body.1:
  %ptr.src.iv = bitcast * %src.iv to *
  store i32 0, * %ptr.src.iv, align 4
  %add.1 = add nsw nuw i8 %iv, 1
  %src.iv.1 = gep inbounds * %src, 1 x i8 %add.1
  %cmp.iv.1.start = icmp ult * %src.iv.1, noundef %lower
  %cmp.iv.1.end = icmp uge * %src.iv.1, noundef %upper
  %or.2 = or i1 0, 0
  br i1 %or.2, label %trap.bb, label %loop.body.2

%loop.body.2:
  %ptr.src.iv.1 = bitcast * %src.iv.1 to *
  store i32 0, * %ptr.src.iv.1, align 4
  %add.2 = add nsw nuw i8 %iv, 2
  %src.iv.2 = gep inbounds * %src, 1 x i8 %add.2
  %cmp.iv.2.start = icmp ult * %src.iv.2, noundef %lower
  %cmp.iv.2.end = icmp uge * %src.iv.2, noundef %upper
  %or.3 = or i1 0, %cmp.iv.2.end
  br i1 %or.3, label %trap.bb, label %loop.latch

%loop.latch:
  %ptr.src.iv.2 = bitcast * %src.iv.2 to *
  store i32 0, * %ptr.src.iv.2, align 4
  %iv.next = add nsw nuw i8 %iv, 1
  br label %loop.header

%trap.bb:
  ret void
}
Transformation doesn't verify!
ERROR: Source is more defined than target

Example:
* %src = pointer(non-local, block_id=1, offset=32)
* noundef %lower = pointer(non-local, block_id=0, offset=931)
* noundef %upper = pointer(non-local, block_id=0, offset=1057)
i8 %N = #xe0 (224, -32)

Source:
* %src.end = pointer(non-local, block_id=1, offset=0)
i1 %cmp.src.start = #x0 (0)
i1 %cmp.src.end = #x0 (0)
i1 %or.0 = #x0 (0)
  >> Jump to %loop.header
i8 %iv = #x00 (0)
i1 %ec = #x0 (0)
  >> Jump to %loop.body
* %src.iv = pointer(non-local, block_id=1, offset=32)
i1 %cmp.iv.start = #x0 (0)
i1 %cmp.iv.end = #x0 (0)
i1 %or.1 = #x0 (0)
  >> Jump to %loop.body.1
* %ptr.src.iv = pointer(non-local, block_id=1, offset=32)
i8 %add.1 = #x01 (1)
* %src.iv.1 = pointer(non-local, block_id=1, offset=33)
i1 %cmp.iv.1.start = #x0 (0)
i1 %cmp.iv.1.end = #x1 (1)
i1 %or.2 = #x1 (1)
  >> Jump to %trap.bb

SOURCE MEMORY STATE
===================
NON-LOCAL BLOCKS:
Block 0 >	size: 0	align: 4	alloc type: 0	address: 0
Block 1 >	size: 512	align: 2	alloc type: 0	address: 1024
Block 2 >	size: 642	align: 2	alloc type: 0	address: 209
Block 3 >	size: 12	align: 4	alloc type: 0	address: 2833

Target:
* %src.end = pointer(non-local, block_id=1, offset=0)
i1 %cmp.src.start = #x0 (0)
i1 %cmp.src.end = #x0 (0)
i1 %or.0 = #x0 (0)
  >> Jump to %loop.header
i8 %iv = #x00 (0)
i1 %ec = #x0 (0)
  >> Jump to %loop.body
* %src.iv = pointer(non-local, block_id=1, offset=32)
i1 %cmp.iv.start = #x0 (0)
i1 %cmp.iv.end = #x0 (0)
i1 %or.1 = #x0 (0)
  >> Jump to %loop.body.1
* %ptr.src.iv = pointer(non-local, block_id=1, offset=32)
i8 %add.1 = #x01 (1)
* %src.iv.1 = pointer(non-local, block_id=1, offset=33)
i1 %cmp.iv.1.start = #x0 (0)
i1 %cmp.iv.1.end = #x1 (1)
i1 %or.2 = #x0 (0)
  >> Jump to %loop.body.2
* %ptr.src.iv.1 = pointer(non-local, block_id=1, offset=33)
void = UB triggered!



------------------- SMT STATS -------------------
Num queries: 4
Num invalid: 0
Num skips:   0
Num trivial: 37 (90.2%)
Num timeout: 0 (0.0%)
Num errors:  0 (0.0%)
Num SAT:     4 (100.0%)
Num UNSAT:   0 (0.0%)
Alive2: Transform doesn't verify; aborting!

stderr:

+ : 'RUN: at line 2'
+ /home/nlopes/llvm/build/bin/FileCheck /home/nlopes/llvm/llvm/test/Transforms/ConstraintElimination/loops-header-tested-pointer-cmps.ll
+ /home/nlopes/alive2/build/opt-alive.sh -constraint-elimination -S /home/nlopes/llvm/llvm/test/Transforms/ConstraintElimination/loops-header-tested-pointer-cmps.ll

FileCheck error: '<stdin>' is empty.
FileCheck command line:  /home/nlopes/llvm/build/bin/FileCheck /home/nlopes/llvm/llvm/test/Transforms/ConstraintElimination/loops-header-tested-pointer-cmps.ll

<-- Back