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.llvm.org) is reported as correct, but uncommenting the commented-out assume results in it finding a case of %cmp == 1 even though before it reported %cmp → 0 as a valid transformation.
The text was updated successfully, but these errors were encountered:
This is a tricky case.
The address of malloc'ed objects is a non-deterministic value. The compiler is assume whatever it wants, as long as it makes consistent choices. So it may either assume that the allocations are contiguous or not.
So both ret false and ret true are valid return values. That's because the addresses are not observable by the program, so anything goes. LLVM will just remove the allocations altogether.
The assume is wrong because you cannot force the comparison to go to one way in the target. You would have to place it in the src program.
Though, at first I had a call void @use(ptr %x, ptr %y) after the malloc calls (https://alive2.llvm.org/ce/z/ERH5Fj), which should allow the program to observe the pointers, e.g. @use could have if ((intptr_t)x != (intptr_t)y+8) abort(); at which point @src/@tgt would be required to return be able to return 1 if use doesn't choose to guarantee always taking the abort path. I don't think it's possible to guarantee the consistent choice across functions?
But yes, very tricky; wouldn't be surprised if I've missed something here too; it's also hitting inter-procedural stuff.
Potentially I'm not understanding alive2's intended behavior, but this:
(alive2.llvm.org) is reported as correct, but uncommenting the commented-out assume results in it finding a case of
%cmp == 1
even though before it reported%cmp
→0
as a valid transformation.The text was updated successfully, but these errors were encountered: