False negative with compare of GEPs

[fhahn]

Alive2 verifies the example below as correct, but shouldn't this fail verification? Unless I am missing something, a counter example would be any pointer value for %arr so that %gep.2 doesn't overflow. Interestingly enough, if the return value of @tgt is changed to true this is also verified as correct. Verification fails if the return value is replaced with undef.

https://alive2.llvm.org/ce/z/Rq3ECC

define i1 @src() {
entry:
  %arr = alloca [3 x i8]
  %upper = getelementptr inbounds [3 x i8], [3 x i8]* %arr, i64 0, i64 3
  %gep.2 = getelementptr [3 x i8], [3 x i8]* %arr, i64 1, i64 1
  %c = icmp ugt i8* %gep.2, %upper
  ret i1 %c
}

define i1 @tgt() {
entry:
  ret i1 false
}

[nunoplopes]

This bug is annoying. %arr+4 may overflow, so the comparison may be true or false, depending on the memory layout. We can't model these multiple layouts as pure non-determinism, otherwise the refinement above would be correct.

Our refinement formulas looks like ∀ addr . addr ≤ 12 → addr + 4 ≤ addr + 3 The issue is when addr=12, addr+4 overflows. The precondition addr ≤ 12 is generated by the alloca, to ensure all inbounds pointers don't overflow. But about non-inbounds pointers? TL;DR The condition should hold for any "reasonable" memory layout (addr ≤ 12). In this case it does not. We need to tweak the refinement formula 😣

[regehr]

I didn't even realize it was possible for an i1 to refine to both true and false, but not to refine to undef

[fhahn]

Thanks for the explanation!