[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