[llvm] [LangRef] Relax semantics of writeonly / memory(write) (PR #95238)

[Nikita Popov via llvm-commits]

https://github.com/nikic updated https://github.com/llvm/llvm-project/pull/95238

>From 446e95bfce500660d82a21a985c7166376d79d62 Mon Sep 17 00:00:00 2001
From: Nikita Popov <npopov at redhat.com>
Date: Wed, 12 Jun 2024 14:33:52 +0200
Subject: [PATCH 1/3] [LangRef] Relax semantics of writeonly / memory(write)

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).

Fixes https://github.com/llvm/llvm-project/issues/95152.
---
 llvm/docs/LangRef.rst | 21 +++++++++++++++++++--
 1 file changed, 19 insertions(+), 2 deletions(-)

diff --git a/llvm/docs/LangRef.rst b/llvm/docs/LangRef.rst
index f39b8dc6c90d4..315baad5c6e81 100644
--- a/llvm/docs/LangRef.rst
+++ b/llvm/docs/LangRef.rst
@@ -1598,8 +1598,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)``
@@ -1973,6 +1975,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 the location is immediate
+      undefined behavior. This includes the case where the location is read 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 read and write allocas, and 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

>From d20b6a6d6defd9e71b3928284c6bab707bcd6951 Mon Sep 17 00:00:00 2001
From: Nikita Popov <npopov at redhat.com>
Date: Wed, 12 Jun 2024 15:07:55 +0200
Subject: [PATCH 2/3] [InstCombine] Use named values in comment (NFC)

Also use opaque pointers.
---
 .../InstCombine/InstCombineSelect.cpp         | 22 +++++++++----------
 1 file changed, 11 insertions(+), 11 deletions(-)

diff --git a/llvm/lib/Transforms/InstCombine/InstCombineSelect.cpp b/llvm/lib/Transforms/InstCombine/InstCombineSelect.cpp
index b04e0b300f95a..588607b3fea2f 100644
--- a/llvm/lib/Transforms/InstCombine/InstCombineSelect.cpp
+++ b/llvm/lib/Transforms/InstCombine/InstCombineSelect.cpp
@@ -2359,20 +2359,20 @@ static Instruction *foldSelectCmpBitcasts(SelectInst &Sel,
 /// operand, the result of the select will always be equal to its false value.
 /// For example:
 ///
-///   %0 = cmpxchg i64* %ptr, i64 %compare, i64 %new_value seq_cst seq_cst
-///   %1 = extractvalue { i64, i1 } %0, 1
-///   %2 = extractvalue { i64, i1 } %0, 0
-///   %3 = select i1 %1, i64 %compare, i64 %2
-///   ret i64 %3
+///   %cmpxchg = cmpxchg ptr %ptr, i64 %compare, i64 %new_value seq_cst seq_cst
+///   %val = extractvalue { i64, i1 } %cmpxchg, 0
+///   %success = extractvalue { i64, i1 } %cmpxchg, 1
+///   %sel = select i1 %success, i64 %compare, i64 %val
+///   ret i64 %sel
 ///
-/// The returned value of the cmpxchg instruction (%2) is the original value
-/// located at %ptr prior to any update. If the cmpxchg operation succeeds, %2
+/// The returned value of the cmpxchg instruction (%val) is the original value
+/// located at %ptr prior to any update. If the cmpxchg operation succeeds, %val
 /// must have been equal to %compare. Thus, the result of the select is always
-/// equal to %2, and the code can be simplified to:
+/// equal to %val, and the code can be simplified to:
 ///
-///   %0 = cmpxchg i64* %ptr, i64 %compare, i64 %new_value seq_cst seq_cst
-///   %1 = extractvalue { i64, i1 } %0, 0
-///   ret i64 %1
+///   %cmpxchg = cmpxchg ptr %ptr, i64 %compare, i64 %new_value seq_cst seq_cst
+///   %val = extractvalue { i64, i1 } %cmpxchg, 0
+///   ret i64 %val
 ///
 static Value *foldSelectCmpXchg(SelectInst &SI) {
   // A helper that determines if V is an extractvalue instruction whose

>From 10c7548b6d4f48a6e2983dc29c443c1748ae66a3 Mon Sep 17 00:00:00 2001
From: Nikita Popov <npopov at redhat.com>
Date: Mon, 17 Jun 2024 09:53:02 +0200
Subject: [PATCH 3/3] wording

---
 llvm/docs/LangRef.rst | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/llvm/docs/LangRef.rst b/llvm/docs/LangRef.rst
index 315baad5c6e81..78220b9350c24 100644
--- a/llvm/docs/LangRef.rst
+++ b/llvm/docs/LangRef.rst
@@ -1978,9 +1978,9 @@ example:
     The supported access kinds are:
 
     - ``readwrite``: Any kind of access to the location is allowed.
-    - ``read``: The location is only read. Writing the location is immediate
-      undefined behavior. This includes the case where the location is read and
-      then the same value is written back.
+    - ``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