Hello everyone,
We have developed a tool for inferring preconditions for LLVM peephole
optimizations expressed in Alive. Our prototype has found weaker
(more general) preconditions for several optimizations in the Alive suite.
We were able to trace several back to LLVM's InstCombine and
InstructionSimplify stages in the SVN head (r297512), and have identified
a good candidate for weakening in LLVM.
The details of our approach are available in the technical report at
http://export.arxiv.org/abs/1611.05980
Our prototype is available in the Alive-NJ github
at GitHub - rutgers-apl/alive-nj: Alive (Automated LLVM's InstCombine Verifier) with automated reasoning for both integer and floating point peephole optimizations in LLVM
The candidate we have found is in the function simplifySelectBitTest in
InstructionSimplify. The relevant code is:
// (X & Y) == 0 ? X & ~Y : X --> X
// (X & Y) != 0 ? X & ~Y : X --> X & ~Y
if (FalseVal == X && match(TrueVal, m_And(m_Specific(X), m_APInt(C))) &&
*Y == ~*C)
return TrueWhenUnset ? FalseVal : TrueVal;
// (X & Y) == 0 ? X : X & ~Y --> X & ~Y
// (X & Y) != 0 ? X : X & ~Y --> X
if (TrueVal == X && match(FalseVal, m_And(m_Specific(X), m_APInt(C))) &&
*Y == ~*C)
return TrueWhenUnset ? FalseVal : TrueVal;
simplifySelectBitTest is called in six different contexts, so this can be
expressed as 12 optimizations in Alive.
In all 12 cases, the precondition *Y == ~*C can be relaxed to
(*Y | *C).isAllOnesValue().
Alive verifies that the optimization is valid with the weaker
precondition in all 12 cases.
For reference, Alive version of the optimizations with the current
precondition:
Name: bittestand-1
Pre: C1 == ~C2
%l = and %X, C1
%c = icmp eq %l, 0
%t = and %X, C2
%r = select %c, %t, %X
=>
%r = %X
Name: bittestand-2
Pre: C1 == ~C2
%l = and %X, C1
%c = icmp eq %l, 0
%f = and %X, C2
%r = select %c, %X, %f
=>
%r = %f
Name: bittestand-3
Pre: C1 == ~C2
%l = and %X, C1
%c = icmp ne %l, 0
%t = and %X, C2
%r = select %c, %t, %X
=>
%r = %t
Name: bittestand-4
Pre: C1 == ~C2
%l = and %X, C1
%c = icmp ne %l, 0
%f = and %X, C2
%r = select %c, %X, %f
=>
%r = %X
Name: bittestand-5
Pre: C1 == ~C2
%l = trunc %X
%c = icmp slt %l, 0
%t = and %X, C2
%r = select %c, %t, %X
=>
C1 = 1 << (width(%l) - 1)
%r = %t
Name: bittestand-6
Pre: C1 == ~C2
%l = trunc %X
%c = icmp slt %l, 0
%f = and %X, C2
%r = select %c, %X, %f
=>
C1 = 1 << (width(%l) - 1)
%r = %X
Name: bittestand-7
Pre: C1 == ~C2
%c = icmp slt %X, 0
%t = and %X, C2
%r = select %c, %t, %X
=>
C1 = 1 << (width(%r) - 1)
%r = %t
Name: bittestand-8
Pre: C1 == ~C2
%c = icmp slt %X, 0
%f = and %X, C2
%r = select %c, %X, %f
=>
C1 = 1 << (width(%r) - 1)
%r = %X
Name: bittestand-9
Pre: C1 == ~C2
%l = trunc %X
%c = icmp sgt %l, -1
%t = and %X, C2
%r = select %c, %t, %X
=>
C1 = 1 << (width(%l)-1)
%r = %X
Name: bittestand-10
Pre: C1 == ~C2
%l = trunc %X
%c = icmp sgt %l, -1
%f = and %X, C2
%r = select %c, %X, %f
=>
C1 = 1 << (width(%l)-1)
%r = %f
Name: bittestand-11
Pre: C1 == ~C2
%c = icmp sgt %X, -1
%t = and %X, C2
%r = select %c, %t, %X
=>
C1 = 1 << (width(%r) - 1)
%r = %X
Name: bittestand-12
Pre: C1 == ~C2
%c = icmp sgt %X, -1
%f = and %X, C2
%r = select %c, %X, %f
=>
C1 = 1 << (width(%r) - 1)
%r = %f
And the optimizations with the weaker precondition:
Name: bittestand-1
Pre: C1 | C2 == -1
%l = and %X, C1
%c = icmp eq %l, 0
%t = and %X, C2
%r = select %c, %t, %X
=>
%r = %X
Name: bittestand-2
Pre: C1 | C2 == -1
%l = and %X, C1
%c = icmp eq %l, 0
%f = and %X, C2
%r = select %c, %X, %f
=>
%r = %f
Name: bittestand-3
Pre: C1 | C2 == -1
%l = and %X, C1
%c = icmp ne %l, 0
%t = and %X, C2
%r = select %c, %t, %X
=>
%r = %t
Name: bittestand-4
Pre: C1 | C2 == -1
%l = and %X, C1
%c = icmp ne %l, 0
%f = and %X, C2
%r = select %c, %X, %f
=>
%r = %X
Name: bittestand-5
Pre: C1 | C2 == -1
%l = trunc %X
%c = icmp slt %l, 0
%t = and %X, C2
%r = select %c, %t, %X
=>
C1 = 1 << (width(%l) - 1)
%r = %t
Name: bittestand-6
Pre: C1 | C2 == -1
%l = trunc %X
%c = icmp slt %l, 0
%f = and %X, C2
%r = select %c, %X, %f
=>
C1 = 1 << (width(%l) - 1)
%r = %X
Name: bittestand-7
Pre: C1 | C2 == -1
%c = icmp slt %X, 0
%t = and %X, C2
%r = select %c, %t, %X
=>
C1 = 1 << (width(%r) - 1)
%r = %t
Name: bittestand-8
Pre: C1 | C2 == -1
%c = icmp slt %X, 0
%f = and %X, C2
%r = select %c, %X, %f
=>
C1 = 1 << (width(%r) - 1)
%r = %X
Name: bittestand-9
Pre: C1 | C2 == -1
%l = trunc %X
%c = icmp sgt %l, -1
%t = and %X, C2
%r = select %c, %t, %X
=>
C1 = 1 << (width(%l)-1)
%r = %X
Name: bittestand-10
Pre: C1 | C2 == -1
%l = trunc %X
%c = icmp sgt %l, -1
%f = and %X, C2
%r = select %c, %X, %f
=>
C1 = 1 << (width(%l)-1)
%r = %f
Name: bittestand-11
Pre: C1 | C2 == -1
%c = icmp sgt %X, -1
%t = and %X, C2
%r = select %c, %t, %X
=>
C1 = 1 << (width(%r) - 1)
%r = %X
Name: bittestand-12
Pre: C1 | C2 == -1
%c = icmp sgt %X, -1
%f = and %X, C2
%r = select %c, %X, %f
=>
C1 = 1 << (width(%r) - 1)
%r = %f