[llvm] 9cbedd9 - [LangRef] Relax semantics of writeonly / memory(write) (#95238)

[via llvm-commits]

Author: Nikita Popov
Date: 2024-06-19T09:45:04+02:00
New Revision: 9cbedd925cba9e8ef76c50caa6d6ab4b0cc79c8f

URL: https://github.com/llvm/llvm-project/commit/9cbedd925cba9e8ef76c50caa6d6ab4b0cc79c8f
DIFF: https://github.com/llvm/llvm-project/commit/9cbedd925cba9e8ef76c50caa6d6ab4b0cc79c8f.diff

LOG: [LangRef] Relax semantics of writeonly / memory(write) (#95238)

Instead of making writes immediate undefined behavior, consider these
attributes in terms of their externally observable effects. We don't
care if a location is read within the function, as long as it has no
impact on observed behavior. In particular, allow:

 * Reading a location after writing it.
 * Reading a location before writing it (within the function) returns a
poison value.

The latter could be further relaxed to also allow things like "reading
the value and then writing it back", but I'm not sure how one would
specify that operationally (so that proof checkers can verify it).

While here, also explicitly mention the fact that reads and writes to
allocas and read from constant globals are `memory(none)`.

Fixes https://github.com/llvm/llvm-project/issues/95152.

Added: 
    

Modified: 
    llvm/docs/LangRef.rst

Removed: 
    


################################################################################
diff  --git a/llvm/docs/LangRef.rst b/llvm/docs/LangRef.rst
index 5a1535cb782fb..7ecf876e027a9 100644
--- a/llvm/docs/LangRef.rst
+++ b/llvm/docs/LangRef.rst
@@ -1602,8 +1602,10 @@ Currently, only the following parameter attributes are defined:
     through this pointer argument (even though it may read from the memory that
     the pointer points to).
 
-    If a function reads from a writeonly pointer argument, the behavior is
-    undefined.
+    This attribute is understood in the same way as the ``memory(write)``
+    attribute. That is, the pointer may still be read as long as the read is
+    not observable outside the function. See the ``memory`` documentation for
+    precise semantics.
 
 ``writable``
     This attribute is only meaningful in conjunction with ``dereferenceable(N)``
@@ -1977,6 +1979,21 @@ example:
     - ``memory(readwrite, argmem: none)``: May access any memory apart from
       argument memory.
 
+    The supported access kinds are:
+
+    - ``readwrite``: Any kind of access to the location is allowed.
+    - ``read``: The location is only read. Writing to the location is immediate
+      undefined behavior. This includes the case where the location is read from
+      and then the same value is written back.
+    - ``write``: Only writes to the location are observable outside the function
+      call. However, the function may still internally read the location after
+      writing it, as this is not observable. Reading the location prior to
+      writing it results in a poison value.
+    - ``none``: No reads or writes to the location are observed outside the
+      function. It is always valid to read and write allocas, and to read global
+      constants, even if ``memory(none)`` is used, as these effects are not
+      externally observable.
+
     The supported memory location kinds are:
 
     - ``argmem``: This refers to accesses that are based on pointer arguments