Test Failure: Transforms/ConstraintElimination/gep-arithmetic.ll

Test source: git

Log:

Source: /home/nlopes/llvm/llvm/test/Transforms/ConstraintElimination/gep-arithmetic.ll

----------------------------------------
define i1 @n_unknown(* %dst, i32 %n, i32 %i) {
%entry:
  %sub = add i32 %n, 4294967295
  %idxprom = zext i32 %sub to i64
  %ptr.n.sub.1 = gep * %dst, 4 x i64 %idxprom
  %cmp.ptr.dst = icmp uge * %ptr.n.sub.1, %dst
  br i1 %cmp.ptr.dst, label %pre.bb.2, label %exit

%pre.bb.2:
  %pre.2 = icmp uge i32 %i, 0
  br i1 %pre.2, label %tgt.bb, label %exit

%tgt.bb:
  %cmp1 = icmp ult i32 %i, %n
  ret i1 %cmp1

%exit:
  ret i1 0
}
=>
define i1 @n_unknown(* %dst, i32 %n, i32 %i) {
%entry:
  %sub = add i32 %n, 4294967295
  %idxprom = zext i32 %sub to i64
  %ptr.n.sub.1 = gep * %dst, 4 x i64 %idxprom
  %cmp.ptr.dst = icmp uge * %ptr.n.sub.1, %dst
  br i1 %cmp.ptr.dst, label %pre.bb.2, label %exit

%pre.bb.2:
  %pre.2 = icmp uge i32 %i, 0
  br i1 %pre.2, label %tgt.bb, label %exit

%tgt.bb:
  %cmp1 = icmp ult i32 %i, %n
  ret i1 %cmp1

%exit:
  ret i1 0
}
Transformation seems to be correct!


----------------------------------------
define i1 @n_known_zero_due_to_nuw(* %dst, i32 %n, i32 %i) {
%entry:
  %sub = add i32 %n, 4294967295
  %idxprom = zext i32 %sub to i64
  %ptr.n.sub.1 = gep * %dst, 4 x i64 %idxprom
  %cmp.ptr.dst = icmp uge * %ptr.n.sub.1, %dst
  br i1 %cmp.ptr.dst, label %pre.bb.2, label %exit

%pre.bb.2:
  %pre.2 = icmp uge i32 %i, 0
  br i1 %pre.2, label %tgt.bb, label %exit

%tgt.bb:
  %cmp1 = icmp ult i32 %i, %n
  ret i1 %cmp1

%exit:
  ret i1 0
}
=>
define i1 @n_known_zero_due_to_nuw(* %dst, i32 %n, i32 %i) {
%entry:
  %sub = add i32 %n, 4294967295
  %idxprom = zext i32 %sub to i64
  %ptr.n.sub.1 = gep * %dst, 4 x i64 %idxprom
  %cmp.ptr.dst = icmp uge * %ptr.n.sub.1, %dst
  br i1 %cmp.ptr.dst, label %pre.bb.2, label %exit

%pre.bb.2:
  %pre.2 = icmp uge i32 %i, 0
  br i1 %pre.2, label %tgt.bb, label %exit

%tgt.bb:
  %cmp1 = icmp ult i32 %i, %n
  ret i1 %cmp1

%exit:
  ret i1 0
}
Transformation seems to be correct!


----------------------------------------
define i4 @ptr_N_signed_positive_explicit_check_constant_step(* %src, * %lower, * %upper, i16 %N) {
%entry:
  %N.pos = icmp sge i16 %N, 0
  br i1 %N.pos, label %entry.1, label %trap.bb

%entry.1:
  %src.end = gep inbounds * %src, 1 x i16 %N
  %cmp.src.start = icmp ult * %src, %lower
  %cmp.src.end = icmp uge * %src.end, %upper
  %or.precond.0 = or i1 %cmp.src.start, %cmp.src.end
  br i1 %or.precond.0, label %trap.bb, label %step.check

%step.check:
  %step.ult.N = icmp ult i16 1, %N
  br i1 %step.ult.N, label %ptr.check, label %exit

%ptr.check:
  %src.step = gep inbounds * %src, 1 x i16 1
  %cmp.step.start = icmp ult * %src.step, %lower
  %cmp.step.end = icmp uge * %src.step, %upper
  %or.check = or i1 %cmp.step.start, %cmp.step.end
  br i1 %or.check, label %trap.bb, label %exit

%trap.bb:
  ret i4 2

%exit:
  ret i4 3
}
=>
define i4 @ptr_N_signed_positive_explicit_check_constant_step(* %src, * %lower, * %upper, i16 %N) {
%entry:
  %N.pos = icmp sge i16 %N, 0
  br i1 %N.pos, label %entry.1, label %trap.bb

%entry.1:
  %src.end = gep inbounds * %src, 1 x i16 %N
  %cmp.src.start = icmp ult * %src, %lower
  %cmp.src.end = icmp uge * %src.end, %upper
  %or.precond.0 = or i1 %cmp.src.start, %cmp.src.end
  br i1 %or.precond.0, label %trap.bb, label %step.check

%step.check:
  %step.ult.N = icmp ult i16 1, %N
  br i1 %step.ult.N, label %ptr.check, label %exit

%ptr.check:
  %src.step = gep inbounds * %src, 1 x i16 1
  %cmp.step.start = icmp ult * %src.step, %lower
  %cmp.step.end = icmp uge * %src.step, %upper
  %or.check = or i1 0, 0
  br i1 %or.check, label %trap.bb, label %exit

%trap.bb:
  ret i4 2

%exit:
  ret i4 3
}
Transformation seems to be correct!


----------------------------------------
define i4 @ptr_N_signed_positive_explicit_check_constant_step_no_inbonds(* %src, * %lower, * %upper, i16 %N) {
%entry:
  %N.pos = icmp sge i16 %N, 0
  br i1 %N.pos, label %entry.1, label %trap.bb

%entry.1:
  %src.end = gep * %src, 1 x i16 %N
  %cmp.src.start = icmp ult * %src, %lower
  %cmp.src.end = icmp uge * %src.end, %upper
  %or.precond.0 = or i1 %cmp.src.start, %cmp.src.end
  br i1 %or.precond.0, label %trap.bb, label %step.check

%step.check:
  %step.ult.N = icmp ult i16 1, %N
  br i1 %step.ult.N, label %ptr.check, label %exit

%ptr.check:
  %src.step = gep * %src, 1 x i16 1
  %cmp.step.start = icmp ult * %src.step, %lower
  %cmp.step.end = icmp uge * %src.step, %upper
  %or.check = or i1 %cmp.step.start, %cmp.step.end
  br i1 %or.check, label %trap.bb, label %exit

%trap.bb:
  ret i4 2

%exit:
  ret i4 3
}
=>
define i4 @ptr_N_signed_positive_explicit_check_constant_step_no_inbonds(* %src, * %lower, * %upper, i16 %N) {
%entry:
  %N.pos = icmp sge i16 %N, 0
  br i1 %N.pos, label %entry.1, label %trap.bb

%entry.1:
  %src.end = gep * %src, 1 x i16 %N
  %cmp.src.start = icmp ult * %src, %lower
  %cmp.src.end = icmp uge * %src.end, %upper
  %or.precond.0 = or i1 %cmp.src.start, %cmp.src.end
  br i1 %or.precond.0, label %trap.bb, label %step.check

%step.check:
  %step.ult.N = icmp ult i16 1, %N
  br i1 %step.ult.N, label %ptr.check, label %exit

%ptr.check:
  %src.step = gep * %src, 1 x i16 1
  %cmp.step.start = icmp ult * %src.step, %lower
  %cmp.step.end = icmp uge * %src.step, %upper
  %or.check = or i1 %cmp.step.start, %cmp.step.end
  br i1 %or.check, label %trap.bb, label %exit

%trap.bb:
  ret i4 2

%exit:
  ret i4 3
}
Transformation seems to be correct!


----------------------------------------
define i4 @ptr_N_and_step_signed_positive_explicit_check_constant_step(* %src, * %lower, * %upper, i16 %N, i16 %step) {
%entry:
  %N.pos = icmp sge i16 %N, 0
  %step.pos = icmp sge i16 %step, 0
  %and.1 = and i1 %N.pos, %step.pos
  br i1 %and.1, label %entry.1, label %trap.bb

%entry.1:
  %src.end = gep inbounds * %src, 1 x i16 %N
  %cmp.src.start = icmp ult * %src, %lower
  %cmp.src.end = icmp uge * %src.end, %upper
  %or.precond.0 = or i1 %cmp.src.start, %cmp.src.end
  br i1 %or.precond.0, label %trap.bb, label %step.check

%step.check:
  %step.uge.0 = icmp uge i16 %step, 0
  %step.ult.N = icmp ult i16 %step, %N
  %and.2 = and i1 %step.uge.0, %step.ult.N
  br i1 %and.2, label %ptr.check, label %exit

%ptr.check:
  %src.step = gep inbounds * %src, 1 x i16 1
  %cmp.step.start = icmp ult * %src.step, %lower
  %cmp.step.end = icmp uge * %src.step, %upper
  %or.check = or i1 %cmp.step.start, %cmp.step.end
  br i1 %or.check, label %trap.bb, label %exit

%trap.bb:
  ret i4 2

%exit:
  ret i4 3
}
=>
define i4 @ptr_N_and_step_signed_positive_explicit_check_constant_step(* %src, * %lower, * %upper, i16 %N, i16 %step) {
%entry:
  %N.pos = icmp sge i16 %N, 0
  %step.pos = icmp sge i16 %step, 0
  %and.1 = and i1 %N.pos, %step.pos
  br i1 %and.1, label %entry.1, label %trap.bb

%entry.1:
  %src.end = gep inbounds * %src, 1 x i16 %N
  %cmp.src.start = icmp ult * %src, %lower
  %cmp.src.end = icmp uge * %src.end, %upper
  %or.precond.0 = or i1 %cmp.src.start, %cmp.src.end
  br i1 %or.precond.0, label %trap.bb, label %step.check

%step.check:
  %step.uge.0 = icmp uge i16 %step, 0
  %step.ult.N = icmp ult i16 %step, %N
  %and.2 = and i1 %step.uge.0, %step.ult.N
  br i1 %and.2, label %ptr.check, label %exit

%ptr.check:
  %src.step = gep inbounds * %src, 1 x i16 1
  %cmp.step.start = icmp ult * %src.step, %lower
  %cmp.step.end = icmp uge * %src.step, %upper
  %or.check = or i1 0, 0
  br i1 %or.check, label %trap.bb, label %exit

%trap.bb:
  ret i4 2

%exit:
  ret i4 3
}
Transformation seems to be correct!


----------------------------------------
define i4 @ptr_N_and_step_signed_positive_unsigned_checks_only(* %src, * %lower, * %upper, i16 %N, i16 %step) {
%entry:
  %src.end = gep inbounds * %src, 1 x i16 %N
  %no.overflow = icmp ule * %src, %src.end
  br i1 %no.overflow, label %entry.1, label %trap.bb

%entry.1:
  %cmp.src.start = icmp ult * %src, %lower
  %cmp.src.end = icmp uge * %src.end, %upper
  %or.precond.0 = or i1 %cmp.src.start, %cmp.src.end
  br i1 %or.precond.0, label %trap.bb, label %step.check

%step.check:
  %step.uge.0 = icmp uge i16 %step, 0
  %step.ult.N = icmp ult i16 %step, %N
  %and.2 = and i1 %step.uge.0, %step.ult.N
  br i1 %and.2, label %ptr.check, label %exit

%ptr.check:
  %src.step = gep inbounds * %src, 1 x i16 1
  %cmp.step.start = icmp ult * %src.step, %lower
  %cmp.step.end = icmp uge * %src.step, %upper
  %or.check = or i1 %cmp.step.start, %cmp.step.end
  br i1 %or.check, label %trap.bb, label %exit

%trap.bb:
  ret i4 2

%exit:
  ret i4 3
}
=>
define i4 @ptr_N_and_step_signed_positive_unsigned_checks_only(* %src, * %lower, * %upper, i16 %N, i16 %step) {
%entry:
  %src.end = gep inbounds * %src, 1 x i16 %N
  %no.overflow = icmp ule * %src, %src.end
  br i1 %no.overflow, label %entry.1, label %trap.bb

%entry.1:
  %cmp.src.start = icmp ult * %src, %lower
  %cmp.src.end = icmp uge * %src.end, %upper
  %or.precond.0 = or i1 %cmp.src.start, %cmp.src.end
  br i1 %or.precond.0, label %trap.bb, label %step.check

%step.check:
  %step.uge.0 = icmp uge i16 %step, 0
  %step.ult.N = icmp ult i16 %step, %N
  %and.2 = and i1 %step.uge.0, %step.ult.N
  br i1 %and.2, label %ptr.check, label %exit

%ptr.check:
  %src.step = gep inbounds * %src, 1 x i16 1
  %cmp.step.start = icmp ult * %src.step, %lower
  %cmp.step.end = icmp uge * %src.step, %upper
  %or.check = or i1 0, 0
  br i1 %or.check, label %trap.bb, label %exit

%trap.bb:
  ret i4 2

%exit:
  ret i4 3
}
Transformation seems to be correct!


----------------------------------------
define i4 @ptr_N_signed_positive(* %src, * %lower, * %upper, i16 %N, i16 %step) {
%entry:
  %src.end = gep inbounds * %src, 1 x i16 %N
  %cmp.src.start = icmp ult * %src, %lower
  %cmp.src.end = icmp uge * %src.end, %upper
  %N.neg = icmp slt i16 %N, 0
  %or.precond.0 = or i1 %cmp.src.start, %cmp.src.end
  %or.precond.1 = or i1 %or.precond.0, %N.neg
  br i1 %or.precond.1, label %trap.bb, label %step.check

%step.check:
  %step.pos = icmp uge i16 %step, 0
  %step.ult.N = icmp ult i16 %step, %N
  %and.step = and i1 %step.pos, %step.ult.N
  br i1 %and.step, label %ptr.check, label %exit

%ptr.check:
  %src.step = gep inbounds * %src, 1 x i16 %step
  %cmp.step.start = icmp ult * %src.step, %lower
  %cmp.step.end = icmp uge * %src.step, %upper
  %or.check = or i1 %cmp.step.start, %cmp.step.end
  br i1 %or.check, label %trap.bb, label %exit

%exit:
  ret i4 3

%trap.bb:
  ret i4 2
}
=>
define i4 @ptr_N_signed_positive(* %src, * %lower, * %upper, i16 %N, i16 %step) {
%entry:
  %src.end = gep inbounds * %src, 1 x i16 %N
  %cmp.src.start = icmp ult * %src, %lower
  %cmp.src.end = icmp uge * %src.end, %upper
  %N.neg = icmp slt i16 %N, 0
  %or.precond.0 = or i1 %cmp.src.start, %cmp.src.end
  %or.precond.1 = or i1 %or.precond.0, %N.neg
  br i1 %or.precond.1, label %trap.bb, label %step.check

%step.check:
  %step.pos = icmp uge i16 %step, 0
  %step.ult.N = icmp ult i16 %step, %N
  %and.step = and i1 %step.pos, %step.ult.N
  br i1 %and.step, label %ptr.check, label %exit

%ptr.check:
  %src.step = gep inbounds * %src, 1 x i16 %step
  %cmp.step.start = icmp ult * %src.step, %lower
  %cmp.step.end = icmp uge * %src.step, %upper
  %or.check = or i1 %cmp.step.start, %cmp.step.end
  br i1 %or.check, label %trap.bb, label %exit

%exit:
  ret i4 3

%trap.bb:
  ret i4 2
}
Transformation seems to be correct!


----------------------------------------
define i4 @ptr_N_could_be_negative(* %src, * %lower, * %upper, i16 %N, i16 %step) {
%entry:
  %src.end = gep inbounds * %src, 1 x i16 %N
  %cmp.src.start = icmp ult * %src, %lower
  %cmp.src.end = icmp uge * %src.end, %upper
  %or.precond.0 = or i1 %cmp.src.start, %cmp.src.end
  br i1 %or.precond.0, label %trap.bb, label %step.check

%step.check:
  %step.pos = icmp uge i16 %step, 0
  %step.ult.N = icmp ult i16 %step, %N
  %and.step = and i1 %step.pos, %step.ult.N
  br i1 %and.step, label %ptr.check, label %exit

%ptr.check:
  %src.step = gep inbounds * %src, 1 x i16 %step
  %cmp.step.start = icmp ult * %src.step, %lower
  %cmp.step.end = icmp uge * %src.step, %upper
  %or.check = or i1 %cmp.step.start, %cmp.step.end
  br i1 %or.check, label %trap.bb, label %exit

%exit:
  ret i4 3

%trap.bb:
  ret i4 2
}
=>
define i4 @ptr_N_could_be_negative(* %src, * %lower, * %upper, i16 %N, i16 %step) {
%entry:
  %src.end = gep inbounds * %src, 1 x i16 %N
  %cmp.src.start = icmp ult * %src, %lower
  %cmp.src.end = icmp uge * %src.end, %upper
  %or.precond.0 = or i1 %cmp.src.start, %cmp.src.end
  br i1 %or.precond.0, label %trap.bb, label %step.check

%step.check:
  %step.pos = icmp uge i16 %step, 0
  %step.ult.N = icmp ult i16 %step, %N
  %and.step = and i1 %step.pos, %step.ult.N
  br i1 %and.step, label %ptr.check, label %exit

%ptr.check:
  %src.step = gep inbounds * %src, 1 x i16 %step
  %cmp.step.start = icmp ult * %src.step, %lower
  %cmp.step.end = icmp uge * %src.step, %upper
  %or.check = or i1 0, 0
  br i1 %or.check, label %trap.bb, label %exit

%exit:
  ret i4 3

%trap.bb:
  ret i4 2
}
Transformation doesn't verify!
ERROR: Value mismatch

Example:
* %src = pointer(non-local, block_id=1, offset=263192)
* %lower = undef
* %upper = pointer(non-local, block_id=1, offset=242861)
i16 %N = #xa011 (40977, -24559)
i16 %step = #x0c88 (3208)

Source:
* %src.end = pointer(non-local, block_id=1, offset=238633)
i1 %cmp.src.start = any
i1 %cmp.src.end = #x0 (0)
i1 %or.precond.0 = any
i1 %step.pos = #x1 (1)
i1 %step.ult.N = #x1 (1)
i1 %and.step = #x1 (1)
* %src.step = pointer(non-local, block_id=1, offset=266400)
i1 %cmp.step.start = any
i1 %cmp.step.end = #x1 (1)
i1 %or.check = #x1 (1)

SOURCE MEMORY STATE
===================
NON-LOCAL BLOCKS:
Block 0 >	size: 0	align: 1	alloc type: 0
Block 1 >	size: 524288	align: 4	alloc type: 0
Block 2 >	align: 2	alloc type: 0
Block 3 >	align: 4	alloc type: 0

Target:
* %src.end = pointer(non-local, block_id=1, offset=238633)
i1 %cmp.src.start = #x0 (0)
i1 %cmp.src.end = #x0 (0)
i1 %or.precond.0 = #x0 (0)
i1 %step.pos = #x1 (1)
i1 %step.ult.N = #x1 (1)
i1 %and.step = #x1 (1)
* %src.step = pointer(non-local, block_id=1, offset=266400)
i1 %cmp.step.start = any
i1 %cmp.step.end = #x1 (1)
i1 %or.check = #x0 (0)
Source value: #x2 (2)
Target value: #x3 (3)


------------------- SMT STATS -------------------
Num queries: 38
Num invalid: 0
Num skips:   0
Num trivial: 21 (35.6%)
Num timeout: 0 (0.0%)
Num errors:  0 (0.0%)
Num SAT:     9 (23.7%)
Num UNSAT:   29 (76.3%)

stderr:

+ : 'RUN: at line 2'
+ /home/nlopes/alive2/build/opt-alive.sh -constraint-elimination -S /home/nlopes/llvm/llvm/test/Transforms/ConstraintElimination/gep-arithmetic.ll
+ /home/nlopes/llvm/build/bin/FileCheck /home/nlopes/llvm/llvm/test/Transforms/ConstraintElimination/gep-arithmetic.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/ConstraintElimination/gep-arithmetic.ll

<-- Back