-
Notifications
You must be signed in to change notification settings - Fork 130
Open
Description
https://alive2.llvm.org/ce/z/uYhgqi
target datalayout = "p:64:64:64:32"
define i1 @src_ptrtoint(ptr %p, i32 %offset) {
%p2 = getelementptr nuw i8, ptr %p, i32 %offset
%p.addr = ptrtoint ptr %p to i32
%p2.addr = ptrtoint ptr %p2 to i32
%cmp = icmp uge i32 %p2.addr, %p.addr
ret i1 %cmp
}
define i1 @tgt_ptrtoint(ptr %p, i32 %offset) {
ret i1 true
}
define i1 @src_ptrtoaddr(ptr %p, i32 %offset) {
%p2 = getelementptr nuw i8, ptr %p, i32 %offset
%p.addr = ptrtoaddr ptr %p to i32
%p2.addr = ptrtoaddr ptr %p2 to i32
%cmp = icmp uge i32 %p2.addr, %p.addr
ret i1 %cmp
}
define i1 @tgt_ptrtoaddr(ptr %p, i32 %offset) {
ret i1 true
}Output:
----------------------------------------
define i1 @src_ptrtoint(ptr %p, i32 %offset) {
#0:
%p2 = gep nuw ptr %p, 1 x i32 %offset
%p.addr = ptrtoint ptr %p to i32
%p2.addr = ptrtoint ptr %p2 to i32
%cmp = icmp uge i32 %p2.addr, %p.addr
ret i1 %cmp
}
=>
define i1 @tgt_ptrtoint(ptr %p, i32 %offset) {
#0:
ret i1 1
}
Transformation doesn't verify!
ERROR: Value mismatch
Example:
ptr %p = pointer(non-local, block_id=1, offset=0) / Address=#x80000000fffffff7
i32 %offset = #x00000009 (9)
Source:
ptr %p2 = pointer(non-local, block_id=1, offset=9) / Address=#x8000000100000000
i32 %p.addr = #xfffffff7 (4294967287, -9)
i32 %p2.addr = #x00000000 (0)
i1 %cmp = #x0 (0)
SOURCE MEMORY STATE
===================
NON-LOCAL BLOCKS:
Block 0 > size: 0 align: 1 alloc type: 0 alive: false address: #x0000000000000000
Block 1 > size: 0 align: 1 alloc type: 0 alive: true address: #x80000000fffffff7
Target:
TARGET MEMORY STATE
===================
NON-LOCAL BLOCKS:
Block 0 > size: 0 align: 1 alloc type: 0 alive: false address: #x0000000000000000
Block 1 > size: 0 align: 1 alloc type: 0 alive: true address: #x80000000fffffff7
Source value: #x0 (0)
Target value: #x1 (1)
----------------------------------------
define i1 @src_ptrtoaddr(ptr %p, i32 %offset) {
#0:
%p2 = gep nuw ptr %p, 1 x i32 %offset
%p.addr = ptrtoaddr ptr %p to i32
%p2.addr = ptrtoaddr ptr %p2 to i32
%cmp = icmp uge i32 %p2.addr, %p.addr
ret i1 %cmp
}
=>
define i1 @tgt_ptrtoaddr(ptr %p, i32 %offset) {
#0:
ret i1 1
}
Transformation seems to be correct!
I would expect both to verify. getelementptr only operates on the address/index bits and nuw refers to overflow in those bits only, so the case in the counter example should have GEP returning poison.
What causes me additional confusion here is that this does verify when using ptrtoaddr. ptrtoaddr and a truncating ptrtoint should be the same apart from the provenance exposure semantics, which shouldn't affect anything related to overflow behavior.
Metadata
Metadata
Assignees
Labels
No labels