[PATCH] D90708: [LangRef] Clarify GEP inbounds wrapping semantics

[Nikita Popov via Phabricator via llvm-commits]

nikic created this revision.
nikic added reviewers: jdoerfert, aqjune, nlopes, efriedma, lebedev.ri.
Herald added subscribers: llvm-commits, pengfei, javed.absar.
Herald added a project: LLVM.
nikic requested review of this revision.

The current LangRef wording for GEP inbounds is not very clear in what it implies in terms of wrapping restrictions for the underlying additions and multiplications. This updates LangRef with my understanding of how this is currently being interpreted in practice.

For example, there's this SCEV comment: https://github.com/llvm/llvm-project/blob/7f34aca083b528db1d880b406f1a1953eeb6aa95/llvm/lib/Analysis/ScalarEvolution.cpp#L5061-L5066

Another indication is the fact that clang emits pointer comparisons using unsigned predicates, so we must be assuming that allocated objects cannot wrap the unsigned address space. (For address space 0 this is automatically given because there may be no allocated object containing the null pointer.)

However, I do wonder if we could get away with saying that no allocated object may wrap the signed address space, in which case inbounds would just map cleanly to nsw, which would both allow more optimization and be easier to reason about. We have at least one important target (x86-64) where this is a given by hardware constraints. But I don't know if we can get away with making that a general limitation. (I don't think it's a good idea to make core GEP semantics target-dependent.)


Repository:
  rG LLVM Github Monorepo

https://reviews.llvm.org/D90708

Files:
  llvm/docs/LangRef.rst


Index: llvm/docs/LangRef.rst
===================================================================
--- llvm/docs/LangRef.rst
+++ llvm/docs/LangRef.rst
@@ -9765,17 +9765,27 @@
     }
 
 If the ``inbounds`` keyword is present, the result value of the
-``getelementptr`` is a :ref:`poison value <poisonvalues>` if the base
-pointer is not an *in bounds* address of an allocated object, or if any
-of the addresses that would be formed by successive addition of the
-offsets implied by the indices to the base address with infinitely
-precise signed arithmetic are not an *in bounds* address of that
-allocated object. The *in bounds* addresses for an allocated object are
-all the addresses that point into the object, plus the address one byte
-past the end. The only *in bounds* address for a null pointer in the
-default address-space is the null pointer itself. In cases where the
-base is a vector of pointers the ``inbounds`` keyword applies to each
-of the computations element-wise.
+``getelementptr`` is a :ref:`poison value <poisonvalues>` if one of the
+following rules is violated:
+
+*  The base pointer is an *in bounds* address of an allocated object, which
+   means that it points into or one byte past the end of an allocated object.
+   The only *in bounds* address for a null pointer in the default
+   address-space is the null pointer itself.
+*  The multiplication of an index by the type size does not wrap in a signed
+   sense (``nsw``).
+*  The successive addition of the current address, interpreted as an unsigned
+   number, and an offset, interpreted as a signed number, does not wrap the
+   unsigned address space and remains *in bounds* of the allocated object.
+*  In cases where the base is a vector of pointers, the ``inbounds`` keyword
+   applies to each of the computations element-wise.
+
+As a corollary, the following two properties follow:
+
+*  The successive addition of offsets (without adding the base address) does
+   not wrap in a signed sense (``nsw``).
+*  The addition of the base address and a *non-negative* offset does not wrap
+   in an unsigned sense (``nuw``).
 
 If the ``inbounds`` keyword is not present, the offsets are added to the
 base address with silently-wrapping two's complement arithmetic. If the


-------------- next part --------------
A non-text attachment was scrubbed...
Name: D90708.302646.patch
Type: text/x-patch
Size: 2265 bytes
Desc: not available
URL: <http://lists.llvm.org/pipermail/llvm-commits/attachments/20201103/fe618e22/attachment.bin>