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

Test source: git

Log:

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

----------------------------------------
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_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_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=32768)
* %lower = undef
* %upper = pointer(non-local, block_id=1, offset=32769)
i16 %N = #x8000 (32768, -32768)
i16 %step = #x2000 (8192)

Source:
* %src.end = pointer(non-local, block_id=1, offset=0)
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=40960)
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: 131072	align: 4	alloc type: 0
Block 2 >	align: 256	alloc type: 0
Block 3 >	align: 8589934592	alloc type: 0

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.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=40960)
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: 20
Num invalid: 0
Num skips:   0
Num trivial: 40 (66.7%)
Num timeout: 0 (0.0%)
Num errors:  0 (0.0%)
Num SAT:     5 (25.0%)
Num UNSAT:   15 (75.0%)
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