[all-commits] [llvm/llvm-project] 9cbedd: [LangRef] Relax semantics of writeonly / memory(wr...

[Nikita Popov via All-commits]

  Branch: refs/heads/main
  Home:   https://github.com/llvm/llvm-project
  Commit: 9cbedd925cba9e8ef76c50caa6d6ab4b0cc79c8f
      https://github.com/llvm/llvm-project/commit/9cbedd925cba9e8ef76c50caa6d6ab4b0cc79c8f
  Author: Nikita Popov <npopov at redhat.com>
  Date:   2024-06-19 (Wed, 19 Jun 2024)

  Changed paths:
    M llvm/docs/LangRef.rst

  Log Message:
  -----------
  [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.



To unsubscribe from these emails, change your notification settings at https://github.com/llvm/llvm-project/settings/notifications