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

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

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