AliveToolkit / alive2

Automatic verification of LLVM optimizations
MIT License
719 stars 93 forks source link

arm-tv issue with the null pointer #1066

Open regehr opened 2 days ago

regehr commented 2 days ago

I could use some help with this one. this is src:

define i1 @f(ptr %0) {
  %2 = getelementptr i8, ptr %0, i64 -1
  %3 = icmp ult ptr %2, %0
  ret i1 %3
}

this gets lowered very literally by the AArch64 backend:

_f:   
    sub x8, x0, #1
    cmp x8, x0
    cset    w0, lo
    ret

no problem so far! after optimization the lifted code is:

define i1 @f(ptr %0) {
arm_tv_entry:
  %a4_5.not.not = icmp ne ptr %0, null
  ret i1 %a4_5.not.not
}

this seems like it should be just fine in asm mode, but it doesn't verify, and I don't understand the reasoning. why shouldn't the pointer to offset -1 in block 1 be less than the pointer to offset 0 in the same block?

----------------------------------------
define i1 @f(ptr %#0) {
#1:
  %#2 = gep ptr %#0, 1 x i64 -1
  %#3 = icmp ult ptr %#2, %#0
  ret i1 %#3
}
=>
define i1 @f(ptr %#0) asm {
arm_tv_entry:
  %a4_5.not.not = icmp ne ptr %#0, null
  ret i1 %a4_5.not.not
}
Transformation doesn't verify!

ERROR: Value mismatch

Example:
ptr %#0 = pointer(non-local, block_id=1, offset=0)

Source:
ptr %#2 = pointer(non-local, block_id=1, offset=-1)
i1 %#3 = #x0 (0)

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

Target:
i1 %a4_5.not.not = #x1 (1)
Source value: #x0 (0)
Target value: #x1 (1)