<div dir="ltr"><br><div class="gmail_extra"><br><div class="gmail_quote">On Wed, Feb 4, 2015 at 9:09 AM, John Regehr <span dir="ltr"><<a href="mailto:regehr@cs.utah.edu" target="_blank">regehr@cs.utah.edu</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Hi all, sorry to come late to the party. This is a great thread. I wanted to toss out an example I ran across the other day that seems somewhat interesting. We start with this C program that executes no UB:<br>
<br>
int foo(int x1, int x2) {<br>
  return<br>
    ((x2 > 0) && (x1 > <a href="tel:%282147483647%20-%20x2" value="+12147483647" target="_blank">(2147483647 - x2</a>))) ||<br>
    (x1 && (x2 < 0));<br>
}<br>
<br>
int main(void) {<br>
  printf("%x\n", foo(1, -770027279));<br>
  return 0;<br>
}<br>
<br>
Clang+LLVM turns foo() into this:<br>
<br>
define i32 @foo(i32 %x1, i32 %x2) #0 {<br>
  %1 = icmp sgt i32 %x2, 0<br>
  %2 = sub nsw i32 <a href="tel:2147483647" value="+12147483647" target="_blank">2147483647</a>, %x2<br>
  %3 = icmp slt i32 %2, %x1<br>
  %or.cond = and i1 %1, %3<br>
  br i1 %or.cond, label %6, label %4<br>
<br>
; <label>:4                                       ; preds = %0<br>
  %5 = icmp slt i32 %x2, 0<br>
  %not. = icmp ne i32 %x1, 0<br>
  %. = and i1 %5, %not.<br>
  br label %6<br>
<br>
; <label>:6                                       ; preds = %4, %0<br>
  %7 = phi i1 [ true, %0 ], [ %., %4 ]<br>
  %8 = zext i1 %7 to i32<br>
  ret i32 %8<br>
}<br>
<br>
In the semantics described by the LangRef, my interpretation of the<br>
execution is this:<br>
<br>
%1 = false<br>
%2 = poison<br>
%3 = poison<br>
%or.cond = poison<br>
... the br goes either way or both ways or something ...<br>
%5 = true<br>
%not. = true<br>
%. = true<br>
%7 = phi true, true<br>
<br>
So all is good despite the non-deterministic execution.<br>
<br>
In the proposed new model, we don't have to branch on poison since<br>
%or.cond is completely determined by its false argument and is therefore<br>
false. Does that all sound right?</blockquote><div><br></div><div>Under the semantics described by the RFC, yes.</div><div> </div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><span class="HOEnZb"><font color="#888888"><br>
<br>
John<br>
</font></span></blockquote></div><br></div></div>