Test source: git
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!
+ : '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