<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
</head>
<body style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space;" class="">
Thanks. I missed that we could use alive to prove these kinds of transforms!
<div class=""><br class="">
</div>
<div class=""><br class="">
</div>
<div class="">Anna<br class="">
<div>
<blockquote type="cite" class="">
<div class="">On Nov 30, 2020, at 6:40 PM, Stefanos Baziotis <<a href="mailto:stefanos.baziotis@gmail.com" class="">stefanos.baziotis@gmail.com</a>> wrote:</div>
<br class="Apple-interchange-newline">
<div class="">
<div dir="ltr" class="">Hi,
<div class=""><br class="">
</div>
<div class="">Just wanted to point out the importance of _non-determinism_, it confused me when I first learned about it. AFAIU, if the branch was `if (*p for which we know nothing)` (consider no UB here),</div>
<div class="">the execution can take any of the two paths. However, in this case there's no non-determinism and this transformation would be incorrect because there could be an execution</div>
<div class="">of the program, for a fixed input, where the original program would not have UB (it took the return path) while the target program would (it took the return path as well but it executed</div>
<div class="">the load unconditionally).</div>
<div class=""><br class="">
</div>
<div class="">Best,<br class="">
Stefanos</div>
</div>
<br class="">
<div class="gmail_quote">
<div dir="ltr" class="gmail_attr">Στις Τρί, 1 Δεκ 2020 στις 1:34 π.μ., ο/η Nuno Lopes via llvm-dev <<a href="mailto:llvm-dev@lists.llvm.org" class="">llvm-dev@lists.llvm.org</a>> έγραψε:<br class="">
</div>
<blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">
Both transformations are correct, yes. See here:<br class="">
<a href="https://alive2.llvm.org/ce/z/EpqCUT" rel="noreferrer" target="_blank" class="">https://alive2.llvm.org/ce/z/EpqCUT</a><br class="">
<a href="https://alive2.llvm.org/ce/z/yyj9TQ" rel="noreferrer" target="_blank" class="">https://alive2.llvm.org/ce/z/yyj9TQ</a><br class="">
<br class="">
For a fixed input, if the source triggers UB for *at least one* set of <br class="">
chosen non-deterministic values (e.g., undef, freeze), then the source is <br class="">
declared UB for that input. So you can optimize it away to UB.<br class="">
<br class="">
Nuno<br class="">
<br class="">
-----Original Message----- <br class="">
From: Anna Thomas<br class="">
Sent: Monday, November 30, 2020 10:45 PM<br class="">
Subject: [llvm-dev] Hoisting instructions in presence of Undefined Behaviour<br class="">
<br class="">
We’d like to clarify whether the following transform is valid. Given the <br class="">
code:<br class="">
```<br class="">
if (freeze(undef))<br class="">
return<br class="">
UB<br class="">
```<br class="">
<br class="">
Can we hoist the UB above the `if` block:<br class="">
```<br class="">
UB<br class="">
if (freeze(undef))<br class="">
return<br class="">
```<br class="">
<br class="">
The reasoning is that:<br class="">
1. We were already having undefined behaviour in the code initially. `if <br class="">
freeze(undef)` evaluates to true or false. So, a valid execution of the <br class="">
program will fall through the `if` block and execute the UB.<br class="">
2. Given #1, hoisting a UB to above the `if` block is valid.<br class="">
<br class="">
<br class="">
Taking this one step further, if the program was:<br class="">
```<br class="">
if (freeze(undef))<br class="">
return<br class="">
load<br class="">
```<br class="">
Can we hoist the load over the if-block? I think we can.<br class="">
<br class="">
The `if freeze(undef)` being taken or not is independent of any other <br class="">
program variables and the compiler is free to refine the code into one where <br class="">
the if block is not taken.<br class="">
So, although the load is not guaranteedToExecute, we know that the execution <br class="">
of the load is not actually control dependent on the branch.<br class="">
<br class="">
Anything incorrect with the above transforms?<br class="">
<br class="">
<br class="">
Thanks,<br class="">
Anna <br class="">
<br class="">
_______________________________________________<br class="">
LLVM Developers mailing list<br class="">
<a href="mailto:llvm-dev@lists.llvm.org" target="_blank" class="">llvm-dev@lists.llvm.org</a><br class="">
<a href="https://lists.llvm.org/cgi-bin/mailman/listinfo/llvm-dev" rel="noreferrer" target="_blank" class="">https://lists.llvm.org/cgi-bin/mailman/listinfo/llvm-dev</a><br class="">
</blockquote>
</div>
</div>
</blockquote>
</div>
<br class="">
</div>
</body>
</html>