[llvm] r178409 - Implement XOR reassociation. It is based on following rules:

[Stephen Canon]

Many processors can do a & ~b with a single instruction (BIC on arm, ANDN in the BMI extension on x86, PANDN for sse, ANDC on ppc).  Hence my claim that it is a preferable form.

- Steve

On Mar 30, 2013, at 12:39 PM, Shuxin Yang <shuxin.llvm at gmail.com> wrote:

> This is truly wonderful tool. I need to spent some time today to digest this elegant approach. 
> 
> > We can do better for rule 3.  It simplifies to (~x & c3).
> I don't think (~x & c3) is better; it still need two instructions: one for ~x, the other one for & c3.
> On the other hand, the c3 is bound to & expression, instead of a xor operand, which means the 
> c3 is not able to directly contribute to the xor simplication.
> 
> In contrast, "(x & c3) ^ c3" may need only one instruction, in case c3 is "canceled" by XORing 
> with other constant. 
> 
> 
> On 3/30/13 7:56 AM, Stephen Canon wrote:
>> On Mar 30, 2013, at 10:11 AM, Stephen Canon <scanon at apple.com> wrote:
>> 
>>> On Mar 29, 2013, at 10:15 PM, Shuxin Yang <shuxin.llvm at gmail.com> wrote:
>>> 
>>>> Author: shuxin_yang
>>>> Date: Fri Mar 29 21:15:01 2013
>>>> New Revision: 178409
>>>> 
>>>> URL: http://llvm.org/viewvc/llvm-project?rev=178409&view=rev
>>>> Log:
>>>> Implement XOR reassociation. It is based on following rules:
>>>> 
>>>>  rule 1: (x | c1) ^ c2 => (x & ~c1) ^ (c1^c2),
>>>>     only useful when c1=c2
>>>>  rule 2: (x & c1) ^ (x & c2) = (x & (c1^c2))
>>>>  rule 3: (x | c1) ^ (x | c2) = (x & c3) ^ c3 where c3 = c1 ^ c2
>>>>  rule 4: (x | c1) ^ (x & c2) => (x & c3) ^ c1, where c3 = ~c1 ^ c2
>>> 
>>> We can do better for rule 3.  It simplifies to (~x & c3).
>> 
>> I should also point out that all of these have one-line proofs using only middle-school algebra (no theorem-prover required, though I encourage everyone to use one) if you re-cast them as statements about boolean rings.
>> 
>> A refresher:
>> 
>> Any expression in boolean algebra can be transformed into a statement in boolean rings as follows:
>> 
>>  (a XOR b) ==> a + b
>>  (a OR b) ==> a + ab + b
>>  (a AND b) ==> ab
>>  (NOT a) ==> a + 1
>> 
>> This may not seem like an improvement at first glance, but boolean rings are rings, meaning that your favorite properties of multiplication and addition hold, and you can now work with expressions in the same way that you have since you were 10.  Boolean rings also have two additional properties that let you do some simplifications:
>> 
>>  aa = a
>>  a + a = 0
>> 
>> As examples, I’ll give quick proofs of the rules in question:
>> 
>> Rule 1: (x | c) ^ d ==> x + xc + c + d ==> x(1 + c) + (c + d) ==> (x & ~c) ^ (c ^ d).
>> Rule 2: (x & c) ^ (x & d) ==> xc + xd ==> x(c + d) ==> x & (c ^ d).
>> Rule 3: (x | c) ^ (x | d) ==> x + xc + c + x + xd + d ==> xc + c + xd + d ==> (x + 1)(c + d) ==> ~x & (c ^ d).
>> Rule 4: (x | c) ^ (x & d) ==> x + xc + c + xd ==> x(c + d + 1) + c ==> (x & ~(c ^ d)) ^ c.
>> 
>> Much cleaner than the usual mess of truth tables or case analysis.
>> 
>> - Steve
> 
> 

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.llvm.org/pipermail/llvm-commits/attachments/20130330/05725e79/attachment.html>