[PATCH] D76973: [LangRef] Clarify the semantics of branch on undef

[Juneyoung Lee via Phabricator via llvm-commits]

aqjune created this revision.
aqjune added reviewers: efriedma, fhahn, nikic, spatel, jdoerfert.
Herald added a project: LLVM.
Herald added a subscriber: llvm-commits.
aqjune added a reviewer: nlopes.
aqjune added a subscriber: regehr.
jdoerfert added a comment.

I don't like the way you say "non-frozen undef" but maybe it is just me. For me, a frozen value is neither undef nor poison, full stop.
I also don't like "expression containing undef" which could be interpreted as `and i1 false, undef`, though that one is an OK branch condition.



================
Comment at: llvm/docs/LangRef.rst:7068
+If '``cond``' is ``poison`` or ``undef``, this instruction has undefined
+behavior.
 
----------------
Do we have this for switch also?


This patch clarifies the semantics of branching on undef value.

Defining `br undef` as undefined behavior explains optimizations that use branch conditions, such as CVP (D76931 <https://reviews.llvm.org/D76931>) and GVN (propagateEquality).

For `switch cond`, it is defined to raise UB if cond is an expression containing undef && cond is not frozen &&
it may yield different values.
This allows that at the destination block the branch condition can be assumed to be frozen already (otherwise UB was already triggered).
This condition is slightly stricter than MemorySanitizer, which allows undef-y condition if it always leads to the same destination,
but it does not break MemorySanitizer because we are giving stricter constraint.


Repository:
  rG LLVM Github Monorepo

https://reviews.llvm.org/D76973

Files:
  llvm/docs/LangRef.rst


Index: llvm/docs/LangRef.rst
===================================================================
--- llvm/docs/LangRef.rst
+++ llvm/docs/LangRef.rst
@@ -3452,7 +3452,36 @@
 location could clobber arbitrary memory, therefore, it has undefined
 behavior.
 
-**MemorySanitizer**, a detector of uses of uninitialized memory,
+Execution of a conditional branch is undefined behavior if its condition is
+a not-frozen expression containing undef and it can be evaluted into different
+values.
+This explains optimizations that depend on branch conditions to construct
+predicates, such as Correlated Value Propagation and Global Value Numbering.
+As it raises undefined behavior otherwise, we can assume that the branch
+condition is frozen at destination blocks.
+
+.. code-block:: text
+
+    Unsafe:
+      br undef, BB1, BB2 ; UB
+
+      %X = and i32 undef, 255
+      switch %X, label %ret [ .. ] ; UB
+
+      store undef, i8* %ptr
+      %X = load i8* %ptr ; %X is undef
+      switch i8 %X, label %ret [ .. ] ; UB
+
+    Safe:
+      %X = or i8 undef, 255 ; always 255
+      switch i8 %X, label %ret [ .. ] ; Well-defined
+
+      %X = freeze i1 undef
+      br %X, BB1, BB2 ; Well-defined (non-deterministic jump)
+
+
+This is also consistent with the behavior of MemorySanitizer.
+MemorySanitizer, detector of uses of uninitialized memory,
 defines a branch with condition that depends on an undef value (or
 certain other values, like e.g. a result of a load from heap-allocated
 memory that has never been stored to) to have an externally visible
@@ -7035,7 +7064,8 @@
 argument is evaluated. If the value is ``true``, control flows to the
 '``iftrue``' ``label`` argument. If "cond" is ``false``, control flows
 to the '``iffalse``' ``label`` argument.
-If '``cond``' is ``poison``, this instruction has undefined behavior.
+If '``cond``' is ``poison`` or ``undef``, this instruction has undefined
+behavior.
 
 Example:
 """"""""


-------------- next part --------------
A non-text attachment was scrubbed...
Name: D76973.253302.patch
Type: text/x-patch
Size: 1940 bytes
Desc: not available
URL: <http://lists.llvm.org/pipermail/llvm-commits/attachments/20200328/e35dc8f1/attachment.bin>