[PATCH] D87994: [LangRef] State that pointers and/or sizes of memory access instructions are well-defined

[Juneyoung Lee via Phabricator via llvm-commits]

aqjune updated this revision to Diff 293347.
aqjune added a comment.

Update the contents to follow the conclusion of the discussion at llvm-dev.

I think the behavior of the sanitizer is still valid.
The logic couldn't be applied to IR because existing dereferenceability checking analyses accept pointers with undef bits.

Made the definition of a well-defined value clearer.
A definition of 'frozen value' is omitted because contexts of their current uses say the meaning straightforwardly.

Memset/memcpy/memmove's len are allowed to have undef bits as well.


Repository:
  rG LLVM Github Monorepo

CHANGES SINCE LAST ACTION
  https://reviews.llvm.org/D87994/new/

https://reviews.llvm.org/D87994

Files:
  llvm/docs/LangRef.rst


Index: llvm/docs/LangRef.rst
===================================================================
--- llvm/docs/LangRef.rst
+++ llvm/docs/LangRef.rst
@@ -3553,10 +3553,6 @@
 
 To ensure all uses of a given register observe the same value (even if
 '``undef``'), the :ref:`freeze instruction <i_freeze>` can be used.
-A value is frozen if its uses see the same value.
-An aggregate value or vector is frozen if its elements are frozen.
-The padding of an aggregate isn't considered, since it isn't visible
-without storing it into memory and loading it with a different type.
 
 .. code-block:: llvm
 
@@ -3729,6 +3725,22 @@
 
     end:
 
+.. _welldefinedvalues:
+
+Well-Defined Values
+-------------------
+
+A value is *well defined* if the value never has an undef bit and is never
+poison.
+An aggregate value or vector is well defined if its elements are well defined.
+The padding of an aggregate isn't considered, since it isn't visible
+without storing it into memory and loading it with a different type.
+
+A constant of a single value, non-vector type is well defined if it is a
+non-undef constant. Note that there is no poison constant in LLVM.
+The result of :ref:`freeze instruction <i_freeze>` is well defined regardless
+of its operand.
+
 .. _blockaddress:
 
 Addresses of Basic Blocks
@@ -9244,6 +9256,12 @@
 padding may be accessed but are ignored, because it is impossible to observe
 padding from the loaded aggregate value.
 
+If the pointer is not a well-defined value, all of its possible representations
+should be dereferenceable. For example, loading a byte from a pointer to an
+array of type ``[16 x i8]`` with offset ``undef & 31`` is undefined behavior.
+Loading a byte at offset ``undef & 15`` nondeterministically reads one of the
+bytes.
+
 Examples:
 """""""""
 
@@ -9335,6 +9353,12 @@
 If ``<value>`` is of aggregate type, padding is filled with
 :ref:`undef <undefvalues>`.
 
+If ``<pointer>`` is not a well-defined value, all of its possible
+representations should be dereferenceable. For example, storing a byte to a
+pointer to an array of type ``[16 x i8]`` with offset ``undef & 31`` is
+undefined behavior. Storing a byte to an offset ``undef & 15``
+nondeterministically stores to one of offsets from 0 to 15.
+
 Example:
 """"""""
 
@@ -12487,6 +12511,9 @@
 
 If "len" is 0, the pointers may be NULL, dangling, ``undef``, or ``poison``
 pointers. However, they must still be appropriately aligned.
+If "len" isn't a well-defined value, all of its possible representations should
+make the behavior of this ``llvm.memcpy`` defined, otherwise the behavior is
+undefined.
 
 .. _int_memcpy_inline:
 
@@ -12604,6 +12631,9 @@
 
 If "len" is 0, the pointers may be NULL, dangling, ``undef``, or ``poison``
 pointers. However, they must still be appropriately aligned.
+If "len" isn't a well-defined value, all of its possible representations should
+make the behavior of this ``llvm.memmove`` defined, otherwise the behavior is
+undefined.
 
 .. _int_memset:
 
@@ -12659,6 +12689,9 @@
 
 If "len" is 0, the pointer may be NULL, dangling, ``undef``, or ``poison``
 pointer. However, it must still be appropriately aligned.
+If "len" isn't a well-defined value, all of its possible representations should
+make the behavior of this ``llvm.memset`` defined, otherwise the behavior is
+undefined.
 
 '``llvm.sqrt.*``' Intrinsic
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^


-------------- next part --------------
A non-text attachment was scrubbed...
Name: D87994.293347.patch
Type: text/x-patch
Size: 3392 bytes
Desc: not available
URL: <http://lists.llvm.org/pipermail/llvm-commits/attachments/20200922/c369357f/attachment.bin>