llvm dev - Sep 2014 - [LLVMdev] poison and select

> Poison is a flawed concept. I proved it was flawed back in 2011 [0]
Nice. My colleagues and I will dig through this material and possibly come 
back with some ideas. We're going to need some sort of semantics for UB in 
LLVM since otherwise these formal-methods-based tools like Souper and 
Alive risk not making sense.

Thanks,

John

Hi John,

On 12/09/14 04:17, John Regehr wrote:
>> Poison is a flawed concept. I proved it was flawed back in 2011 [0]
>
> Nice. My colleagues and I will dig through this material and possibly come
back
> with some ideas. We're going to need some sort of semantics for UB in
LLVM since
> otherwise these formal-methods-based tools like Souper and Alive risk not
making
> sense.
it's great to see this back and forth between the formal tools and the
language
reference.  The IR docs are primarily aimed at humans, but if ambiguities and 
problems spotted by the formal tools can be cleared up there without making the 
lang ref unreadable then that would be a win for everyone.

Ciao, Duncan.

Hi John,

More background is in this post (at which time "poison" was still
named
"trap") (and I apologize for the verbosity) [0]

[0] http://lists.cs.uiuc.edu/pipermail/llvmdev/2011-November/045730.html

The poison concept aimed to
  (a) enable the sign-extension elimination optimization
  (b) permit arbitrary speculation that doesn't destroy any optimization
opportunities

Undef does (b) but not (a). Immediate UB does (a) but not (b).
Additionally, here are some interesting debatable requirements:

  - Select(a, b, c) should be semantically equivalent to (sext(a) &
b)|(~sext(a) & c) (with appropriate bitcasting).
  - Select should be semantically equivalent to its intuitive translation
as a branch and a phi (the current poison concept violates this)
  - Branch should be semantically equivalent to its intuitive translation
as a switch, and as an indirect branch
  - Constant folding, mem2reg, and reg2mem should always be safe *and*
optimization-opportunity-preserving

I personally suggest a compromise on the optimization, and instead a focus
on helping programmers write better code. C++11 range-based for loops are
easier for humans to read, and in some cases avoid ol' "int" to
step
through arrays. Quoting the Zen of Python, "let's do more of
those!"


On Thu, Sep 11, 2014 at 7:17 PM, John Regehr <regehr at cs.utah.edu>
wrote:
> Poison is a flawed concept. I proved it was flawed back in 2011 [0]
>>
>
> Nice. My colleagues and I will dig through this material and possibly come
> back with some ideas. We're going to need some sort of semantics for UB
in
> LLVM since otherwise these formal-methods-based tools like Souper and Alive
> risk not making sense.
>
>
> Thanks,
>
> John
> _______________________________________________
> LLVM Developers mailing list
> LLVMdev at cs.uiuc.edu         http://llvm.cs.uiuc.edu
> http://lists.cs.uiuc.edu/mailman/listinfo/llvmdev
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL:
<http://lists.llvm.org/pipermail/llvm-dev/attachments/20140912/7c94d00f/attachment.html>

Today I ran into another aspect of the poison problem...

Basically, SimplifyCFG wants to take

   expr1 && expr2

and flatten it into

   x = expr1
   y = expr2
   x&y

This isn't safe when expr2 might execute UB.  The consequence is that no 
LLVM shift instruction is safe to speculatively execute, nor is any 
nsw/nuw/exact variant, unless the operands can be proven to be in bounds.

Real example here:

   http://llvm.org/bugs/show_bug.cgi?id=20997

John