[llvm] LangRef: getelementptr: inbounds is about the object the pointer is 'based on' (PR #95650)
Nikita Popov via llvm-commits
llvm-commits at lists.llvm.org
Sat Jun 15 02:49:06 PDT 2024
https://github.com/nikic commented:
This looks reasonable to me. I think this requirement is necessary to ensure that `gep inbounds (gep inbounds p, a), b` refines to `gep inbounds (p, a+b)`. Otherwise, `p+a` could point both to the end of one and start of another allocated object, such that `a+b` overflows.
One thing to note here is that this says "the allocated object", while the current inttoptr phrasing implies that a pointer may be based on multiple allocated objects. But I think that's a possibility we should exclude from the pointer aliasing semantics.
@nunoplopes How does alive2 currently model inbounds?
https://github.com/llvm/llvm-project/pull/95650
More information about the llvm-commits
mailing list