[llvm-dev] undef * 0

[Sanjoy Das via llvm-dev]

Hi Soham,

Soham Chakraborty wrote:
 > As a result,  the transformation ' ((a&  (~b)) |((~a)&  b)) ~>  xor a b '
 > is unsound. LLVM presently performs this transformation.

This transform looks fine to me.

For simplicity let's look at an `i1` expression.  Since these are
bitwise ops we can extend the reasoning below to iN.

Transform: ((A & (~B)) | ((~A) & B))  ~> A ^ B

Neither A nor B are undef:
   Transform is correct by normal boolean algebra

Both A and B are undef:
   LHS = (undef & undef) | (undef & undef) = undef  // Since ~undef = undef
   RHS = undef
   Thus transform is correct.

A is undef but B is not undef:
   LHS = ((undef & (~B)) | (undef & B)) // Since ~undef = undef

   Now, by choosing 0 for undef in LHS, we can make LHS be equal to 0,
   and by choosing 1 for undef in LHS, we can make LHS be equal to 1.
   Therefore

   LHS = undef
   RHS = undef ^ B = undef

   Thus the transform is correct.

A is not undef but B is undef:
   Similar reasoning follows.

-- Sanjoy