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! (syntactically equal)


----------------------------------------
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! (syntactically equal)


----------------------------------------
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! (syntactically equal)


----------------------------------------
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 doesn't verify!
ERROR: Timeout


----------------------------------------
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! (syntactically equal)


----------------------------------------
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: Timeout


----------------------------------------
define i4 @ptr_src_uge_end(* %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
  %cmp.overflow = icmp ugt * %src, %src.end
  %or.precond.0 = or i1 %cmp.src.start, %cmp.src.end
  %or.precond.1 = or i1 %or.precond.0, %cmp.overflow
  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_src_uge_end(* %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
  %cmp.overflow = icmp ugt * %src, %src.end
  %or.precond.0 = or i1 %cmp.src.start, %cmp.src.end
  %or.precond.1 = or i1 %or.precond.0, %cmp.overflow
  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! (syntactically equal)


----------------------------------------
define i4 @inc_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
  %next = add nsw nuw i16 %step, 2
  %step.ult.N = icmp ult i16 %next, %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 @inc_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
  %next = add nsw nuw i16 %step, 2
  %step.ult.N = icmp ult i16 %next, %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: Timeout


----------------------------------------
define i4 @inc_ptr_src_uge_end(* %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
  %cmp.overflow = icmp ugt * %src, %src.end
  %or.precond.0 = or i1 %cmp.src.start, %cmp.src.end
  %or.precond.1 = or i1 %or.precond.0, %cmp.overflow
  br i1 %or.precond.1, label %trap.bb, label %step.check

%step.check:
  %step.pos = icmp uge i16 %step, 0
  %next = add nsw nuw i16 %step, 2
  %step.ult.N = icmp ult i16 %next, %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 @inc_ptr_src_uge_end(* %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
  %cmp.overflow = icmp ugt * %src, %src.end
  %or.precond.0 = or i1 %cmp.src.start, %cmp.src.end
  %or.precond.1 = or i1 %or.precond.0, %cmp.overflow
  br i1 %or.precond.1, label %trap.bb, label %step.check

%step.check:
  %step.pos = icmp uge i16 %step, 0
  %next = add nsw nuw i16 %step, 2
  %step.ult.N = icmp ult i16 %next, %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! (syntactically equal)


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

%entry:
  %src.idx = gep inbounds * %src, 1 x i16 %idx
  %cmp.src.start = icmp ult * %src.idx, %lower
  br i1 %cmp.src.start, label %trap.bb, label %step.check

%step.check:
  %next = add i16 %idx, 2
  %src.step = gep inbounds * %src, 1 x i16 %next
  %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 @inc_ptr_src_uge_end_no_nsw_add(* %src, * %lower, * %upper, i16 %idx, i16 %N, i16 %step) {
%entry.1:
  %idx.pos = icmp sge i16 %idx, 0
  br i1 %idx.pos, label %entry, label %trap.bb

%entry:
  %src.idx = gep inbounds * %src, 1 x i16 %idx
  %cmp.src.start = icmp ult * %src.idx, %lower
  br i1 %cmp.src.start, label %trap.bb, label %step.check

%step.check:
  %next = add i16 %idx, 2
  %src.step = gep inbounds * %src, 1 x i16 %next
  %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! (syntactically equal)


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

%entry:
  %src.idx = gep inbounds * %src, 1 x i16 %idx
  %cmp.src.start = icmp ult * %src.idx, %lower
  br i1 %cmp.src.start, label %trap.bb, label %step.check

%step.check:
  %next = add i16 %idx, 2
  %src.step = gep inbounds * %src, 1 x i16 %next
  %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 @inc_ptr_src_uge_end_no_nsw_add_sge_0(* %src, * %lower, * %upper, i16 %idx, i16 %N, i16 %step) {
%entry.1:
  %idx.pos = icmp sge i16 %idx, 0
  br i1 %idx.pos, label %entry, label %trap.bb

%entry:
  %src.idx = gep inbounds * %src, 1 x i16 %idx
  %cmp.src.start = icmp ult * %src.idx, %lower
  br i1 %cmp.src.start, label %trap.bb, label %step.check

%step.check:
  %next = add i16 %idx, 2
  %src.step = gep inbounds * %src, 1 x i16 %next
  %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! (syntactically equal)


----------------------------------------
define i4 @ptr_N_unsigned_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 ult 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_unsigned_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 ult 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! (syntactically equal)


----------------------------------------
define i4 @ptr_N_signed_positive_assume(* %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
  assume i1 %N.neg
  %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_signed_positive_assume(* %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
  assume i1 %N.neg
  %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=65540)
* %lower = pointer(non-local, block_id=0, offset=186429)
* %upper = pointer(non-local, block_id=2, offset=173758)
i16 %N = #x804c (32844, -32692)
i16 %step = #x8000 (32768, -32768)

Source:
* %src.end = pointer(non-local, block_id=1, offset=32848)
i1 %cmp.src.start = #x0 (0)
i1 %cmp.src.end = #x0 (0)
i1 %N.neg = #x1 (1)
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=32772)
i1 %cmp.step.start = #x1 (1)
i1 %cmp.step.end = #x0 (0)
i1 %or.check = #x1 (1)

SOURCE MEMORY STATE
===================
NON-LOCAL BLOCKS:
Block 0 >	size: 0	align: 1	alloc type: 0	address: 0
Block 1 >	size: 524288	align: 4	alloc type: 0	address: 131072
Block 2 >	size: 165908	align: 4	alloc type: 0	address: 874816
Block 3 >	size: 19460	align: 4	alloc type: 0	address: 804868

Target:
* %src.end = pointer(non-local, block_id=1, offset=32848)
i1 %cmp.src.start = #x0 (0)
i1 %cmp.src.end = #x0 (0)
i1 %N.neg = #x1 (1)
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=32772)
i1 %cmp.step.start = #x1 (1)
i1 %cmp.step.end = #x0 (0)
i1 %or.check = #x0 (0)
Source value: #x2 (2)
Target value: #x3 (3)


------------------- SMT STATS -------------------
Num queries: 18
Num invalid: 0
Num skips:   0
Num trivial: 39 (68.4%)
Num timeout: 3 (16.7%)
Num errors:  0 (0.0%)
Num SAT:     7 (38.9%)
Num UNSAT:   8 (44.4%)
Alive2: Transform doesn't verify; aborting!

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

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