You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
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.
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 😣
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 totrue
this is also verified as correct. Verification fails if the return value is replaced withundef
.https://alive2.llvm.org/ce/z/Rq3ECC
The text was updated successfully, but these errors were encountered: