[llvm] r185954 - ValueTracking: Fix bugs in isKnownToBeAPowerOfTwo

[Hal Finkel]

----- Original Message -----
> 
> 
> 
> 
> 
> 
> 
> On Wed, Jul 10, 2013 at 2:49 AM, Jay Foad < jay.foad at gmail.com >
> wrote:
> 
> 
> 
> On 9 July 2013 19:11, David Majnemer < david.majnemer at gmail.com >
> wrote:
> > Author: majnemer
> > Date: Tue Jul 9 13:11:10 2013
> > New Revision: 185954
> > 
> > URL: http://llvm.org/viewvc/llvm-project?rev=185954&view=rev
> > Log:
> > ValueTracking: Fix bugs in isKnownToBeAPowerOfTwo
> > 
> > (add nsw x, (and x, y)) isn't a power of two if x is zero, it's
> > zero
> > (add nsw x, (xor x, y)) isn't a power of two if y has bits set that
> > aren't set in x
> 
> Thanks! Please be very very careful not to introduce subtle
> mis-optimizations like this. If in doubt, get someone else to stare
> at
> the code before committing.
> 
> 
> 
> Another option is to use a theorem prover. I personally like <
> http://rise4fun.com/z3py >, which is super easy to use.

Unfortunately, z3 is for non-commercial use only: http://z3.codeplex.com/SourceControl/latest#LICENSE.txt
(Not a problem for everyone here, but certainly an issue for some people).

I generally use CVC4: http://cvc4.cs.nyu.edu/web/ (which is perhaps not as easy to use as z3 ;) -- but is BSD-licensed, and pretty convenient). The CLI input language is essentially the same as for CVC3 (http://www.cs.nyu.edu/acsys/cvc3/doc/user_doc.html)

For example, here's the transformation in question:

OrZero == true:

cvc4 1.2 assertions:off
CVC4> OPTION "produce-models";
CVC4> x, y : BITVECTOR(32);
CVC4> ISPOW2 : BITVECTOR(32) -> BOOLEAN = LAMBDA(x : BITVECTOR(32)): BVPLUS(32, x, 0hexffffffff) & x = 0hex00000000;
CVC4> ASSERT ISPOW2(x);
CVC4> QUERY(ISPOW2(BVPLUS(32, x, x & y)));
valid

OrZero == false:

cvc4 1.2 assertions:off
CVC4> OPTION "produce-models";
CVC4> x, y : BITVECTOR(32);
CVC4> ISPOW2 : BITVECTOR(32) -> BOOLEAN = LAMBDA(x : BITVECTOR(32)): BVPLUS(32, x, 0hexffffffff) & x = 0hex00000000 AND x /= 0hex00000000;
CVC4> ASSERT ISPOW2(x);
CVC4> % assert nuw or nsw
CVC4> ASSERT (BVZEROEXTEND(BVPLUS(32, x, x & y), 1) = BVPLUS(33, x, x & y)) OR (SX(BVPLUS(32, x, x & y), 33) = BVPLUS(33, x, x & y));
CVC4> QUERY(ISPOW2(BVPLUS(32, x, x & y)));
valid

If the query fails then you can type COUNTEREXAMPLE to get a counter-example. You can also type 'QUERY FALSE', and if it says 'valid' then you know that you've asserted some set of mutually-incompatible conditions.

[I'm not trying to engage in prover-wars... but I figured it would be good to provide a quick relevant example].

 -Hal

> 
> 
> -- Sean Silva
> _______________________________________________
> llvm-commits mailing list
> llvm-commits at cs.uiuc.edu
> http://lists.cs.uiuc.edu/mailman/listinfo/llvm-commits
> 

-- 
Hal Finkel
Assistant Computational Scientist
Leadership Computing Facility
Argonne National Laboratory