Let's be conservative here; it matches what we actually implement, and it should be rare in practice anyway.
Does this mean we can "construct" undef as:
x = alloca 0 y = alloca 0 undef = x == y // Non-deterministically 0 or 1
? If so, this is a problem since it means even if we spec un-initialized memory as poison we still have undef in the IR (with all the problems it brings).
x, y are still different objects. Comparing pointers of different objects yields false, except for the +n case, since p+n == q may be true at execution time if p,q are contiguous objects.
If x,y are zero-sized, then x == y is the +n case.
We either define p+n == q as undef or as non-deterministic value (freeze(poison) essentially). Both options have prons and cons (hard to hoist vs hard to copy), but we have to live with them, unfortunately. So alloc 0 doesn't bring any new difficulty.