[LLVMdev] poison and select

[Sanjoy Das]

Hi,

> Does this make any sense at all?  Have there been past attempts at
> formalizing poison along these lines?

Answering my own question, what I was considering is a slight variant
of the scheme mentioned in an earlier email by Dan:
http://lists.cs.uiuc.edu/pipermail/llvmdev/2011-November/045730.html

"
 - Instead of trying to define dependence in LangRef, just say that if
   changing the value returned from an overflowing add nsw would
   affect the observable behavior of the program, then the behavior of
   the program is undefined. This would reduce the amount of text in
   LangRef, but it would be a weaker definition, and it would require
   sign-extension optimizers and others to do significantly more work
   to establish that their transformations are safe.
"

That said, this scheme does not work as expected -- the bitness of the
result of an overflowing add prevents some optimizations:

 %a = add nsw i32 %v, 1
 %c = icmp slt i32 %v, %a
 store %c, < global variable >

In the case of signed overflow, %v is INT32_MAX.  For all values of
%a, the observable behavior of the program is the same (we store false
to < global variable > for all values of %a); and so we cannot exploit
undefined behavior and simplify '%c' to true.

Similar issues arise if you, for example, zero extend a poison value,
and then right shift out all the "poison bits" -- the resulting value
is all zeroes and do not capture overflowing semantics.

Thanks,
-- Sanjoy