forked from OSchip/llvm-project
42af3601c2
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. llvm-svn: 214342 |
||
---|---|---|
.. | ||
Hello | ||
IPO | ||
InstCombine | ||
Instrumentation | ||
ObjCARC | ||
Scalar | ||
Utils | ||
Vectorize | ||
CMakeLists.txt | ||
LLVMBuild.txt | ||
Makefile |