Escaped pointers have non-deterministic address

[dzaima]

Escaped pointers have non-deterministic address

[nunoplopes]

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.

Hope this explanation makes sense.

[dzaima]

That makes sense.

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.

[nunoplopes]

You're right. That second example shouldn't verify for the exact reason you mention.