-
Notifications
You must be signed in to change notification settings - Fork 111
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
ptrmask(p, 0) -> null considered valid refinement #929
Comments
This is a complicated story, I'm afraid.. null is used a bit inconsistently across optimizations, and so I don't know the exact definition. Right now, Alive2 interprets null as a ptr whose address is 0. I need to re-test what's the blast radius if we change the definition of null. |
I'm back! So, if we change the definition of null to be a pointer to block with id=0 instead of any pointer whose address is 0x0, a few optimizations become wrong: ; just because it's not null, it could be an OOB pointer whose address is 0x0
define i1 @src(ptr nonnull %p) {
%a = ptrtoint ptr %p to i64
%c = icmp eq i64 %a, 0
ret i1 %c
}
define i1 @tgt(ptr nonnull %p) {
ret i1 false
} ; we've defined pointer comparison as comparison of addresses, so same reasoning here
; an OOB ptr can have addr 0x0
define i1 @src(ptr %p) {
%a = load ptr, ptr %p, align 1, !nonnull !{}
%c = icmp eq ptr %a, null
ret i1 %c
}
define i1 @tgt(ptr %p) {
ret i1 false
} ; same as before: p = q <=> (ptr2int p) = (ptr2int q)
define ptr @src(ptr %in) {
%c = icmp eq ptr %in, null
%r = select i1 %c, ptr null, ptr %in
ret ptr %r
}
define ptr @tgt(ptr %in) {
ret ptr %in
} |
I don't understand what this means. A null pointer should still have address |
Defining ptr comparison like that is useful for, e.g., optimizations that introduce run-time aliasing checks using geps that can go OOB (like the loop vectorizer). Our thoughts back in the day to try to make LLVM consistent were to define null = int2ptr 0. That would make Nikita's optimization correct, while still allowing a gep to move the pointer back to an inbounds ptr. It's a tough game to play. I would prefer if ptr comparison didn't compare addresses, but object id & offset. But then we would need some way for loop vectorization to check for aliasing of potentially OOB pointers. TL;DR: I don't know what to do here. Need help on the LLVM side. |
Right. A null pointer would just have provenance of block 0 (the "null block"). |
Okay, but then I don't get why your examples are no longer correct. I guess that depends on how you define |
True, I just checked it. define ptr @src(ptr %in) {
%c = icmp eq ptr %in, null
%r = select i1 %c, ptr null, ptr %in
ret ptr %r
}
define ptr @tgt(ptr %in) {
ret ptr %in
} |
This one is less straightforward. I would argue this transform is valid, because the provenance of This probably depends on details of how exactly this is represented in alive. Basically the statement would be that it's okay to refine the "null block" to any other block. |
Actually LLVM does transformations in both directions: (ptr)0 -> null define ptr @f() {
%p = inttoptr i64 0 to ptr
ret ptr %p
}
=>
define ptr @f() {
ret ptr null
} (https://llvm.godbolt.org/z/3KdWd1EvP) null -> (ptr)0 If we believe both transformations are correct, then null == (ptr)0. I think this reasoning shows a conflict in LLVM's behavior. |
I agree that this is the correct thing to do. The way this is currently handled is that we try to not produce Actually removing it will probably be fairly tricky though. |
One of the tricky bits: If you do a memset(0), do you get inttoptr(0) or null? I guess the correct answer is inttoptr(0), but that's not the answer we actually want to hear... |
True. Now I remember that was the reason why we defined But well, how often is that you load a null pointer from memory, and that load is store-forwarded from a memset? Also, it only matters for geps. For icmp, null is equivalent, and for memory-access functions it's UB to dereference (int)0. So it's really only for geps that we would need to keep inttoptr around. |
I would argue you get Or maybe this should be a frontend choice. In Rust, we are pretty certain that we want this to be |
https://alive2.llvm.org/ce/z/UhTwMb
I would have expected this to not verify, because provenance changes from
%p
tonull
.The text was updated successfully, but these errors were encountered: