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

Sat Mar 28 12:22:37 PDT 2020

nlopes added inline comments.

================
Comment at: llvm/docs/LangRef.rst:3457
+a not-frozen expression containing undef and it can be evaluted into different
+values.
+This explains optimizations that depend on branch conditions to construct
----------------
aqjune wrote:
> nikic wrote:
> > This definition seems unnecessary confusing, just saying "Branching on undef is undefined behavior" should be sufficient here. Undef is not frozen by definition. There's also no meaningful concept of "contains undef" in this context, as branch conditions are always scalar, so the value can only be undef or not be undef. Expressions reduce to undef or not undef in the usual ways.
> The tricky case is when a partially undef (e.g. `undef | 1`) is given to switch.
> I rephrased the text to make it clear that switching on a value is UB if it is not frozen. This needed defining the notion of a frozen value above.
Undef is a non-deterministic value that can evaluate to different values each time it is used, while "freeze undef" cannot.
That's the main difference. The way to detect this is to say that if the expression we branch on can evaluate to both true and false given the current state then it's UB.
Not sure we need to make this so explicit. Alive2 already has the details implemented.

BTW, @aqjune can you post the examples of optimizations that are incorrect if "br undef" is UB that I wrote the other day. Sorry, I don't have that email here at hand.

Repository:
  rG LLVM Github Monorepo

CHANGES SINCE LAST ACTION
  https://reviews.llvm.org/D76973/new/

https://reviews.llvm.org/D76973