llvm dev - Sep 2015 - anyone want to help tune up computeKnownBits()?

While looking at optimizations where Souper exploits known bits, I 
realized that it would be easy to teach Souper to compute known bits. 
Comparing its results against computeKnownBits() from r246393, it looks 
like there are some easy (and some not-easy) opportunities for 
improvement, please see a few examples below.  The expressions come from 
compiling LLVM itself.

Happily, this exercise didn't identify any errors of unsoundness, only 
imprecisions.

If anyone starts to act on this info, please let me know-- this'll 
probably work best as an iterative process.

The full set of results can be found here:

   http://www.cs.utah.edu/~regehr/souper-known-bits-sep-2015.txt

Thanks,

John


--------------------------------------------------------------------

if the little end of a word contains some contiguous zeros, they'll 
still be there after a shl:

%0:i32 = var
%1:i32 = shl 8:i32, %0
infer %1

known from LLVM:   xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx
known from Souper: xxxxxxxxxxxxxxxxxxxxxxxxxxxxx000

--------------------------------------------------------------------

when the shift exponent is nonzero, shl nsw nuw must leave the MSB 
cleared (if not, the result would have been poison):

%0:i32 = var
%1:i32 = shlnw %0, 3:i32
infer %1

known from LLVM:   xxxxxxxxxxxxxxxxxxxxxxxxxxxxx000
known from Souper: 0xxxxxxxxxxxxxxxxxxxxxxxxxxxx000

--------------------------------------------------------------------

higher-order bits could only have been set in the poison case here:

%0:i64 = var
%1:i64 = subnuw 3:i64, %0
infer %1

known from LLVM: 
xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx
known from Souper: 
00000000000000000000000000000000000000000000000000000000000000xx

--------------------------------------------------------------------

mul nsw nuw 3, %0 is poison if the MSB is set, so:

%0:i32 = var
%1:i32 = mulnw 3:i32, %0
infer %1

known from LLVM:   xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx
known from Souper: 0xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx

--------------------------------------------------------------------

do we want to follow phis a bit more aggressively?

%0 = block 2
%1 = block 2
%2:i64 = phi %1, 0:i64, 1:i64
%3:i64 = phi %0, 1:i64, %2
infer %3

known from LLVM: 
xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx
known from Souper: 
000000000000000000000000000000000000000000000000000000000000000x

--------------------------------------------------------------------

if the big end of a word contains some zeros, lshr can't make them go away:

%0:i64 = var
%1:i64 = lshr 233:i64, %0
infer %1

known from LLVM: 
xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx
known from Souper: 
00000000000000000000000000000000000000000000000000000000xxxxxxxx

--------------------------------------------------------------------

impossible to get rid of all those 1s using a legal shl:

%0:i32 = var
%1:i32 = shl 4294967295:i32, %0
infer %1

known from LLVM:   xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx
known from Souper: 1xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx

--------------------------------------------------------------------

impossible to get rid of all those 1s using a legal lshr:

%0:i32 = var
%1:i32 = lshr 4294967295:i32, %0
infer %1

known from LLVM:   xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx
known from Souper: xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx1

--------------------------------------------------------------------

there are a lot of variants on this general theme where an icmp followed 
by a select don't need to lose all the bits:

%0:i64 = var
%1:i1 = ult 2:i64, %0
%2:i64 = select %1, 2:i64, %0
infer %2

known from LLVM: 
xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx
known from Souper: 
00000000000000000000000000000000000000000000000000000000000000xx

--------------------------------------------------------------------

no reason for bswap to lose known bits:

%0:i32 = var
%1:i32 = or 4277009102:i32, %0
%2:i32 = bswap %1
infer %2

known from LLVM:   xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx
known from Souper: 11xx111x11111x1x111x11x11111111x

--------------------------------------------------------------------

Nuno Lopes pointed out that I failed to make a distinction between known 
bits computations that do not involve reasoning about poison/undef/UB 
(such as the first one in my list) and ones that do (such as the second 
one).

There are some tricky issues here, maybe he'll explain them more.  In the 
future, if people want, I can categorize improvements based on whether or 
not they involve UB exploitation, or just leave out the UB ones if we 
don't want to go there.

John



On Tue, 1 Sep 2015, John Regehr via llvm-dev wrote:
> While looking at optimizations where Souper exploits known bits, I 
> realized that it would be easy to teach Souper to compute known bits. 
> Comparing its results against computeKnownBits() from r246393, it looks 
> like there are some easy (and some not-easy) opportunities for 
> improvement, please see a few examples below.  The expressions come from 
> compiling LLVM itself.
>
> Happily, this exercise didn't identify any errors of unsoundness, only 
> imprecisions.
>
> If anyone starts to act on this info, please let me know-- this'll 
> probably work best as an iterative process.
>
> The full set of results can be found here:
>
>   http://www.cs.utah.edu/~regehr/souper-known-bits-sep-2015.txt
>
> Thanks,
>
> John
>
>
> --------------------------------------------------------------------
>
> if the little end of a word contains some contiguous zeros, they'll 
> still be there after a shl:
>
> %0:i32 = var
> %1:i32 = shl 8:i32, %0
> infer %1
>
> known from LLVM:   xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx
> known from Souper: xxxxxxxxxxxxxxxxxxxxxxxxxxxxx000
>
> --------------------------------------------------------------------
>
> when the shift exponent is nonzero, shl nsw nuw must leave the MSB 
> cleared (if not, the result would have been poison):
>
> %0:i32 = var
> %1:i32 = shlnw %0, 3:i32
> infer %1
>
> known from LLVM:   xxxxxxxxxxxxxxxxxxxxxxxxxxxxx000
> known from Souper: 0xxxxxxxxxxxxxxxxxxxxxxxxxxxx000
>
> --------------------------------------------------------------------
>
> higher-order bits could only have been set in the poison case here:
>
> %0:i64 = var
> %1:i64 = subnuw 3:i64, %0
> infer %1
>
> known from LLVM: 
> xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx
> known from Souper: 
> 00000000000000000000000000000000000000000000000000000000000000xx
>
> --------------------------------------------------------------------
>
> mul nsw nuw 3, %0 is poison if the MSB is set, so:
>
> %0:i32 = var
> %1:i32 = mulnw 3:i32, %0
> infer %1
>
> known from LLVM:   xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx
> known from Souper: 0xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx
>
> --------------------------------------------------------------------
>
> do we want to follow phis a bit more aggressively?
>
> %0 = block 2
> %1 = block 2
> %2:i64 = phi %1, 0:i64, 1:i64
> %3:i64 = phi %0, 1:i64, %2
> infer %3
>
> known from LLVM: 
> xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx
> known from Souper: 
> 000000000000000000000000000000000000000000000000000000000000000x
>
> --------------------------------------------------------------------
>
> if the big end of a word contains some zeros, lshr can't make them go
away:
>
> %0:i64 = var
> %1:i64 = lshr 233:i64, %0
> infer %1
>
> known from LLVM: 
> xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx
> known from Souper: 
> 00000000000000000000000000000000000000000000000000000000xxxxxxxx
>
> --------------------------------------------------------------------
>
> impossible to get rid of all those 1s using a legal shl:
>
> %0:i32 = var
> %1:i32 = shl 4294967295:i32, %0
> infer %1
>
> known from LLVM:   xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx
> known from Souper: 1xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx
>
> --------------------------------------------------------------------
>
> impossible to get rid of all those 1s using a legal lshr:
>
> %0:i32 = var
> %1:i32 = lshr 4294967295:i32, %0
> infer %1
>
> known from LLVM:   xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx
> known from Souper: xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx1
>
> --------------------------------------------------------------------
>
> there are a lot of variants on this general theme where an icmp followed 
> by a select don't need to lose all the bits:
>
> %0:i64 = var
> %1:i1 = ult 2:i64, %0
> %2:i64 = select %1, 2:i64, %0
> infer %2
>
> known from LLVM: 
> xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx
> known from Souper: 
> 00000000000000000000000000000000000000000000000000000000000000xx
>
> --------------------------------------------------------------------
>
> no reason for bswap to lose known bits:
>
> %0:i32 = var
> %1:i32 = or 4277009102:i32, %0
> %2:i32 = bswap %1
> infer %2
>
> known from LLVM:   xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx
> known from Souper: 11xx111x11111x1x111x11x11111111x
>
> --------------------------------------------------------------------
> _______________________________________________
> LLVM Developers mailing list
> llvm-dev at lists.llvm.org
> http://lists.llvm.org/cgi-bin/mailman/listinfo/llvm-dev
>

Hi John, I'm amazed the following two were missed.  They seem like the first
to
implement.

 > if the little end of a word contains some contiguous zeros, they'll
still be
> there after a shl:
>
> %0:i32 = var
> %1:i32 = shl 8:i32, %0
> infer %1
>
> known from LLVM:   xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx
> known from Souper: xxxxxxxxxxxxxxxxxxxxxxxxxxxxx000
 > --------------------------------------------------------------------
 >
 > if the big end of a word contains some zeros, lshr can't make them go
away:
 >
 > %0:i64 = var
 > %1:i64 = lshr 233:i64, %0
 > infer %1
 >
 > known from LLVM:
xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx
 > known from Souper: 
00000000000000000000000000000000000000000000000000000000xxxxxxxx


As for looking through phis:
> do we want to follow phis a bit more aggressively?
>
> %0 = block 2
> %1 = block 2
> %2:i64 = phi %1, 0:i64, 1:i64
> %3:i64 = phi %0, 1:i64, %2
> infer %3
>
> known from LLVM:
xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx
> known from Souper:
000000000000000000000000000000000000000000000000000000000000000x
my guess is that this would be a win: optimizations on phis usually pay off.

Ciao, Duncan.

I've posted a new version of these results:

   http://www.cs.utah.edu/~regehr/souper-known-bits-sep-2015-2.txt

relative to the previous version this one:

- doesn't exploit undefined behaviors

- has known bit constraints on the expressions' inputs, when available

- uses r246940

This is one of my favorites:

%0:i32 = var (xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx0)
%1:i64 = zext %0
%2:i64 = shl 1:i64, %1
infer %2

known from Souper: 
0x0x0x0x0x0x0x0x0x0x0x0x0x0x0x0x0x0x0x0x0x0x0x0x0x0x0x0x0x0x0x0x
known from compiler: 
xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx

John