big query indicated a nop, but none was found

[regehr]

When Souper look for nops, it batches up the possibilities and issues a single solver query looking for the existence of a nop. If none of them work (the expected case by far) then we're done. If a nop is detected, with an unsat result, we don't know which nop is the one that worked, so we have to go and look at each one individually. If none is found, then there must be a bug in the way we aggregated the nops into a single query. That seems to be the case here. This is the smallest LHS that I can find that triggers this bug.

/home/regehr/souper-regehr/build/souper-check -solver-timeout=15 -z3-path=/usr/bin/z3 -infer-rhs -souper-infer-nop
*** oops ***
%0:i32 = var
%1:i1 = eq 0:i32, %0
%2:i32 = sub 32:i32, %0
%3:i32 = lshr 71:i32, %2
%4:i32 = select %1, 0:i32, %3
infer %4

LLVM ERROR: big query indicated a nop, but none was found 

[rsas]

Here is the failing optimization that must be LGTM:

%0:i32 = var
%1:i1 = eq 0:i32, %0
%2:i32 = sub 32:i32, %0
%3:i32 = lshr 71:i32, %2
%4:i32 = select %1, 0:i32, %3
infer %4
result %3

[rsas]

Alive says this optimization is wrong:

----------------------------------------
Optimization: 1
Precondition: true
  %1 = icmp eq 0, %0
  %2 = sub i32 32, %0
  %3 = lshr 71, %2
  %4 = select i1 %1, 0, %3
=>
  %4 = %3


ERROR: Target is more poisonous than Source for i32 %4

Example:
%0 i32 = 0x00000000 (0)
%1 i1 = 0x1 (1, -1)
%2 i32 = 0x00000020 (32)
%3 i32 = poison
Source value: 0x00000000 (0)
Target value: poison 

The "big nop" query is not correct in this case.

[mateon1]

This issue bit me when using sclang to compile a program.

Original oops:

*** oops ***
%0:i64 = var
%1:i64 = var
%2:i64 = and 3:i64, %1
%3:i1 = eq %0, %2
pc %3 1:i1
%4:i64 = var
%5:i1 = ult %4, 2:i64
%6:i64 = shl %1, %4
%7:i64 = and 3:i64, %6
%8:i64 = select %5, %7, 0:i64
infer %8

LLVM ERROR: big query indicated a nop, but none was found

Reduced:

*** oops ***
%0:i64 = var
%1:i1 = ult %0, 2:i64
%2:i64 = var
%3:i64 = shl %2, %0
%4:i64 = and 3:i64, %3
%5:i64 = select %1, %4, 0:i64
infer %5

LLVM ERROR: big query indicated a nop, but none was found

I think this example is clearer.