[llvm-commits] [PATCH] Simplify negated bit test

[Sean Silva]

> As an example, take a look to the output of the Z3 SMT solver (comment line
> 5 to get a counterexample):
> http://rise4fun.com/Z3/RuuZ

Awesome :) That's a great use for a theorem prover!

-- Sean Silva

On Sun, Dec 9, 2012 at 11:23 AM, Nuno Lopes <nunoplopes at sapo.pt> wrote:
> Please add a comment stating that this transformation is only correct
> because shifting by a number larger than the number of bits is undefined.
> Otherwise this transformation wouldn't be sound.
>
> As an example, take a look to the output of the Z3 SMT solver (comment line
> 5 to get a counterexample):
> http://rise4fun.com/Z3/RuuZ
>
> Nuno
>
>
>
> ----- Original Message -----
>>
>> The attached patched takes a sequence like:
>> %neg = xor i32 %A, -1
>> %shl = shl i32 1, %B
>> %and = and i32 %shl, %neg
>> %cmp = icmp ne i32 %and, 0
>>
>> and turns it into:
>> %shl = shl i32 1, %B
>> %and = and i32 %shl, %A
>> %cmp = icmp eq i32 %and, 0
>>
>> The patch includes a test case that exercises this transform.
>>
>> Examples of frontend code that could generate sequence 1 is:
>>
>> bool fun1(unsigned A, unsigned B) { return ~A & (1 << B); }
>>
>> An example of sequence 2 is:
>> bool fun2(unsigned A, unsigned B) { return !(A & (1 << B)); }
>>
>> With this patch, they would have the same IR.
>
>
> _______________________________________________
> llvm-commits mailing list
> llvm-commits at cs.uiuc.edu
> http://lists.cs.uiuc.edu/mailman/listinfo/llvm-commits