Skip to content

Commit 9cbedd9

Browse files
authored
[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 #95152.
1 parent 7fc975a commit 9cbedd9

File tree

1 file changed

+19
-2
lines changed

1 file changed

+19
-2
lines changed

llvm/docs/LangRef.rst

Lines changed: 19 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1602,8 +1602,10 @@ Currently, only the following parameter attributes are defined:
16021602
through this pointer argument (even though it may read from the memory that
16031603
the pointer points to).
16041604

1605-
If a function reads from a writeonly pointer argument, the behavior is
1606-
undefined.
1605+
This attribute is understood in the same way as the ``memory(write)``
1606+
attribute. That is, the pointer may still be read as long as the read is
1607+
not observable outside the function. See the ``memory`` documentation for
1608+
precise semantics.
16071609

16081610
``writable``
16091611
This attribute is only meaningful in conjunction with ``dereferenceable(N)``
@@ -1977,6 +1979,21 @@ example:
19771979
- ``memory(readwrite, argmem: none)``: May access any memory apart from
19781980
argument memory.
19791981

1982+
The supported access kinds are:
1983+
1984+
- ``readwrite``: Any kind of access to the location is allowed.
1985+
- ``read``: The location is only read. Writing to the location is immediate
1986+
undefined behavior. This includes the case where the location is read from
1987+
and then the same value is written back.
1988+
- ``write``: Only writes to the location are observable outside the function
1989+
call. However, the function may still internally read the location after
1990+
writing it, as this is not observable. Reading the location prior to
1991+
writing it results in a poison value.
1992+
- ``none``: No reads or writes to the location are observed outside the
1993+
function. It is always valid to read and write allocas, and to read global
1994+
constants, even if ``memory(none)`` is used, as these effects are not
1995+
externally observable.
1996+
19801997
The supported memory location kinds are:
19811998

19821999
- ``argmem``: This refers to accesses that are based on pointer arguments

0 commit comments

Comments
 (0)