Refinement constraints are either over the BV or QF_BV
(quantified/quantifier-free bitvector) theories. The constraints in Section 3. 2 are negated before querying the SMT
solver, effectively removing one quantifier alternation.
Therefore, for transformations without undefined values
in the source template, we obtain quantifier-free formulas,
and formulas with a single quantifier otherwise.
We translated hundreds of peephole optimizations from
LLVM into Alive. We verified them, and we translated the
Alive optimizations into C++ that we linked into LLVM and
then used the resulting optimizer to build LLVM’s test suite
and the SPEC INT 2000 and 2006 benchmarks. The Alive-generated C++ code’s compilation time and the performance of the resultant code compiled with it is similar to
LLVM’s unverified InstCombine pass. 10
6. 1. Translating and verifying InstCombine
LLVM’s InstCombine pass rewrites expression trees to
reduce their cost, but does not change the control-flow
graph. During the initial testing of our prototype, we translated 334 InstCombine transformations to Alive. Of these,
8 could not be proved correct. We reported these erroneous
transformations to the LLVM developers, who confirmed
and fixed them. We re-translated the fixed optimizations to
Alive and proved them correct.
Subsequent efforts have used Alive to validate end-to-end
transformations and extended the Alive language. These
have lead to the discovery of at least fifteen additional bugs.
The buggiest InstCombine file that we found was
MulDivRem, which implements optimizations that have
multiply, divide, and remainder instructions as the root of
expression trees. Out of the 44 translated optimizations, we
found that 6 of them (14%) were incorrect.
The most common kind of bug in InstCombine was the
introduction of undefined behavior, where an optimization
replaces an expression with one that is defined for a smaller
range of inputs than was the original expression. There were 4
bugs in this category. We also found 2 bugs where the value of
an expression was incorrect for some inputs, and 2 bugs where
a transformation would generate a poison value for inputs that
the original expression did not. Figure 5 provides the Alive code
and the bug report numbers for a sample of the bugs that we
discovered during our translation of LLVM InstCombine optimizations into Alive.
Alive usually takes a few seconds to verify the correctness
of a transformation, during which time it may issue hundreds
or thousands of incremental solver calls. Unfortunately, for
some transformations involving multiplication and division
instructions, Alive can take several hours or longer to verify
the larger bitwidths. This indicates that further improvements are needed in SMT solvers to efficiently handle such
formulas. In the meantime, we work around slow verifications by limiting the bitwidths of operands.
6. 2. Preventing new bugs
Several LLVM developers use Alive to avoid introducing wrong-code bugs. Also, we have been monitoring proposed LLVM
pattern–matching library that InstCombine uses. The implementation checks whether a code fragment matches the pattern of the source template and whether the precondition
holds. If so, it creates the instructions in the target template,
replacing variables with their corresponding values from the
code fragment. Figure 4 shows an Alive transformation and its
corresponding C++ implementation.
4. 1. Translating a source template
The code generator uses LLVM’s pattern-matching library
to create a conditional which tests whether a code fragment
matches the source template. For example, match(I,
m_Add(m_Value(b), m_ConstantInt(C2))) returns true if
the LLVM instruction I adds a value to a constant, and sets the
variables b and C2 to point to its arguments. Matching begins
with the root instruction in the source template and recursively matches operands until all non-inputs have been bound.
4. 2. Translating a target template
A new instruction is created for each instruction that is in
the target template but not the source. The root instruction
from the source is replaced by its counterpart in the target.
4. 3. Type unification
The LLVM constructors for constant literal values and
conversion instructions require explicit types. In general,
this information will depend on types in the source. As Alive
transformations are parametric over types, and Alive provides support for explicit and named types, such information
is not readily available. The Alive code generator uses a unifi-cation-based type inference algorithm to identify appropriate types for the operands and introduces additional clauses
in the if condition to ensure the operands have the appropriate type before invoking the transformation. This type
system ensures that the generated code does not produce
ill-typed LLVM code.
The unification proceeds in 3 phases. First, the types of
the operands in the source are unified according to the constraints in the source (e.g., the operands of a binary operator must have the same type) based on the assumption that
source is a well-formed LLVM program. Second, the types
of the operands in the target are similarly unified according to constraints of the target. Third, when the operands
of a particular instruction in the target do not belong to the
same class, then an explicit check requiring that the types
are equal is added to the if condition in the C++ code generated. The explicit check is necessary as the target has type
constraints that cannot be determined by the source alone.
We implemented Alive in Python and used the Z3 SMT
solver4 to discharge both typing and refinement constraints.
Alive is about 5,200 lines of open-source code.
The number of possible type assignments for a transformation is usually infinite. To ensure termination, Alive considers integer types up to 64 bits.
b The version of Alive corresponding to this paper can be found at https://