InstCombine: Simplify (A ^ B) or/and (A ^ B ^ C)
authorDavid Majnemer <david.majnemer@gmail.com>
Wed, 30 Jul 2014 21:26:37 +0000 (21:26 +0000)
committerDavid Majnemer <david.majnemer@gmail.com>
Wed, 30 Jul 2014 21:26:37 +0000 (21:26 +0000)
commit5624046453adfd1e6807be4dd08f67f9e33a48ba
treef5d5e400de78ca68257ce0d45da65a48aaf2f98a
parentee6a05091a0d8cdb581856871f7fd02188d8823e
InstCombine: Simplify (A ^ B) or/and (A ^ B ^ C)

While we can already transform A | (A ^ B) into A | B, things get bad
once we have (A ^ B) | (A ^ B ^ Cst) because reassociation will morph
this into (A ^ B) | ((A ^ Cst) ^ B).  Our existing patterns fail once
this happens.

To fix this, we add a new pattern which looks through the tree of xor
binary operators to see that, in fact, there exists a redundant xor
operation.

What follows bellow is a correctness proof of the transform using CVC3.

$ cat t.cvc
A, B, C : BITVECTOR(64);

QUERY BVXOR(A, B) | BVXOR(BVXOR(B, C), A) = BVXOR(A, B) | C;
QUERY BVXOR(BVXOR(A, C), B) | BVXOR(A, B) = BVXOR(A, B) | C;

QUERY BVXOR(A, B) & BVXOR(BVXOR(B, C), A) = BVXOR(A, B) & ~C;
QUERY BVXOR(BVXOR(A, C), B) & BVXOR(A, B) = BVXOR(A, B) & ~C;

$ cvc3 < t.cvc
Valid.
Valid.
Valid.
Valid.

git-svn-id: https://llvm.org/svn/llvm-project/llvm/trunk@214342 91177308-0d34-0410-b5e6-96231b3b80d8
lib/Transforms/InstCombine/InstCombineAndOrXor.cpp
test/Transforms/InstCombine/or-xor.ll
test/Transforms/InstCombine/xor2.ll