Question about pointer compare mode and refinement

[dtcxzyw]

See the case from llvm/llvm-project#115574: https://alive2.llvm.org/ce/z/VbP3na

----------------------------------------
define ptr @src(ptr %a, ptr %b) {
#0:
  %cmp1 = icmp eq ptr %a, %b
  %sel = select i1 %cmp1, ptr %a, ptr %b
  ret ptr %sel
}
=>
define ptr @tgt(ptr %a, ptr %b) {
#0:
  ret ptr %b
}
Transformation doesn't verify!

ERROR: Value mismatch

Example:
ptr %a = pointer(non-local, block_id=0, offset=1) / Address=#x1
ptr %b = pointer(non-local, block_id=1, offset=0) / Address=#x1

Source:
i1 %cmp1 = #x1 (1)
ptr %sel = pointer(non-local, block_id=0, offset=1) / Address=#x1

SOURCE MEMORY STATE
===================
NON-LOCAL BLOCKS:
Block 0 >	size: 0	align: 1	alloc type: 0	alive: false	address: 0
Block 1 >	size: 2	align: 281474976710656	alloc type: 0	alive: true	address: 1
Block 2 >	size: 1	align: 2251799813685248	alloc type: 0	alive: true	address: 8

Target:
Source value: pointer(non-local, block_id=0, offset=1) / Address=#x1
Target value: pointer(non-local, block_id=1, offset=0) / Address=#x1

In ICmp::toSMT, we use pointer compare mode INTEGRAL for icmp eq. However, in Pointer::refined we use PROVENANCE mode to check refinement:

alive2/ir/pointer.cpp

Line 736 in 0281f6a

expr nonlocal = is_asm ? getAddress() == other.getAddress() : *this == other;

Is it possible to allow this transformation under non-asm mode?

[nunoplopes]

Alive2 is correct in rejecting this.
There was a decision some time ago that pointer comparison compares addresses. I forget if it was needed for C/C++, but at least it was needed for optimizations that do alias checks at run time (i.e., the loop vectorizer).

This means that ptr1 == ptr2 does not imply that the pointers are equivalent. It just states that their addresses are equal, ignoring provenance. Establishing pointer equivalent in this scheme is quite tricky (seeing a gep inbounds or a dereference is not sufficient due to integer to pointer casts, for example).