Communications of the ACM
Home/Magazine Archive/February 2018 (Vol. 61, No. 2)/Practical Verification of Peephole Optimizations with.../Full Text
Research highlights
Practical Verification of Peephole Optimizations with Alive
Compilers should not miscompile. Peephole optimizations, which perform local rewriting of the input program to improve the efficiency of generated code, are a persistent source of compiler bugs. We created Alive, a domain-specific language for writing optimizations and for automatically either proving them correct or else generating counterexamples. Furthermore, Alive can be automatically translated into C++ code that is suitable for inclusion in an LLVM optimization pass. Alive is based on an attempt to balance usability and formal methods; for example, it captures—but largely hides—the detailed semantics of the various kinds of undefined behavior. Alive has found numerous bugs in the LLVM compiler and is being used by LLVM developers.
1. Introduction
Compiler optimizations should be efficient, effective, and correct—but meeting all of these goals is difficult. In practice, whereas efficiency and effectiveness are relatively easy to quantify, correctness is not. Incorrect compiler optimizations can remain latent for long periods of time; the resulting problems are subtle and difficult to diagnose since the incorrectness is introduced at a level of abstraction lower than the one where software developers typically work.
Random testing7, 20 is one approach to improving the correctness of compilers; it has been shown to be effective, but of course testing misses bugs. A stronger form of insurance against compiler bugs can be provided by a proof that the compiler is correct (compiler verification) or a proof that a particular compilation was correct (translation validation). The state of the art in compiler verification requires a fresh compiler implementation and many person-years of proof engineering (e.g., CompCert9), making this appoach impractical in most production environments.
We developed Alive: a new language and tool for developing correct peephole optimizations as shown in Figure 1. Peephole optimizations in LLVM are performed by the instruction combiner (InstCombine) pass. Alive aims for a design point that is both practical and formal; it allows compiler writers to specify peephole optimizations for LLVM's Intermediate Representation (IR), it automatically proves them correct with the help of a Satisfiability Modulo Theory (SMT) solver (or provides a counterexample), and it automatically generates C++ code that is similar to handwritten peephole optimizations such as those found in the instruction combiner. Alive's main contributions are in identifying a subset of peephole optimizations that can be automatically verified and in providing a usable formal methods tool based on the semantics of LLVM IR, with support for automated correctness proofs in the presence of LLVM's undefined behavior, and with support for code generation.
Figure 1. Overview of Alive. Optimizations expressed in Alive are automatically verified using the Z3 SMT solver. Verified optimizations are converted to C++ implementations for use in LLVM.
InstCombine transformations perform numerous algebraic simplifications that improve efficiency, enable other optimizations, and canonicalize LLVM code. InstCombine optimizations have been a persistent source of LLVM bugs.7, 20
An example InstCombine transformation takes (x ⊕ − 1) + C and turns it into (C – 1) – x where x is a variable, ⊕ is exclusive or, and C is an arbitrary constant as wide as x. If C is 3333, the LLVM input to this InstCombine transformation would look like this:
%1 = xor i32 %x, −1
%2 = add i32 %1, 3333
and the optimized code:
%2 = sub i32 3332, %x
In Alive the same optimization is:
%1 = xor %x, −1
%2 = add %1, C
= >
%2 = sub C-1, %x
The Alive specification is designed to resemble—both syntactically and semantically—the LLVM transformation that it describes. It is much more succinct than its equivalent C++ implementation, is not expressed in terms of LLVM's internal data structures and control flow, and can be automatically verified by the Alive tool kit. This transformation illustrates 2 forms of abstraction supported by Alive: abstraction over choice of a compile-time constant and abstraction over bitwidth.
So far Alive has helped us discover twenty-three previously unknown bugs in the LLVM InstCombine transformations. Furthermore, we have prevented dozens of bugs from getting into LLVM by monitoring the various InstCombine patches as they were committed to the LLVM subversion repository. Several LLVM developers are currently using the Alive prototype to check their InstCombine transformations. Alive is open source and it is also available on-line at http://rise4fun.com/Alive.
2. The Alive Languagea
We designed Alive to resemble the LLVM IR because our users—the LLVM developers—are already experts with it. Alive's most important features include its abstraction over choice of constants, over the bitwidths of operands (Section 2.2), and over LLVM's instruction attributes that control undefined behavior (Section 2.4).
2.1. Syntax
An Alive transformation has the form A ⇒ B, where A is the source template (unoptimized code) and B is the target template (optimized code). Additionally, a transformation may include a precondition. Since Alive's representation, like LLVM's, is based on directed graphs of instructions in Static Single Assignment (SSA) form, the ordering of non-dependent instructions is irrelevant.
Alive implements a subset of LLVM's integer and pointer instructions. It also has limited support for branches: to avoid loops, they are not allowed to jump backwards. Alive supports LLVM's nsw, nuw, and exact instruction attributes that weaken the behavior of integer instructions by adding undefined behaviors.
Scoping. The source and target templates must have a common root variable that is the root of the respective graphs. The remaining variables are either inputs to the transformation or else temporary variables produced by instructions in the source or target template. Inputs are visible throughout the source and target templates. Temporaries defined in the source template are in scope for the precondition, the target, and the remaining part of the source from the point of definition. Temporaries declared in the target are in scope for the remainder of the target. To help catch errors, every temporary in the source template must be used in a later source instruction or be overwritten in the target, and all target instructions must be used in a later target instruction or overwrite a source instruction.
Constant expressions. To allow algebraic simplifications and constant folding, Alive includes a language for constant expressions. A constant expression may be a literal, an abstract constant (e.g., C in the example on the previous page), or a unary or binary operator applied to 1 or 2 constant expressions. The operators include signed and unsigned arithmetic operators and bitwise logical operators. Alive also supports functions on constant expressions. Built-in functions include type conversions and mathematical and bitvector utilities (e.g., abs(), umax(), width() ).
2.2. Type system
Alive supports a subset of LLVM's types, such as integers and pointers. LLVM uses arbitrarily-sized integers, with a separate type for each width (e.g., i8 or i57). Alive has limited support for LLVM's pointer and array types, and does not supports structures or vectors. Recent efforts have subsequently extended Alive with support for floating-point types.14, 16
Unlike LLVM, Alive permits type annotations to be omitted and does not require values to have a unique type. This enables succinct specifications of optimizations in Alive, as many peephole optimizations are not type-specific. A set of possible types is inferred for each implicitly-typed value, and the correctness of an optimization is checked for each type assignment. Because LLVM has infinitely many integer types, we set an upper bound of 64 bits for implicitly typed integer values.
2.3. Built-In predicates
Some peephole optimizations use the results of dataflow analyses. Alive makes these results available using a collection of built-in predicates such as isPowerOf2(), MaskedValueIsZero(), and WillNotOverflowSignedAdd(). The analyses producing these results are trusted by Alive: verifying their correctness is not within Alive's scope. Predicates can be combined with the usual logical connectives. Figure 2 shows an example transformation that includes a built-in predicate in its precondition.
Figure 2. An example illustrating many of Alive's features. ( (B ∨ V) ∧ C1) ∨ (B ∧ C2) can be transformed to (B ∨ V) ∧ (C1 ∨ C2) when C1 ∧ C2 = 0 and when the predicate MaskedValueIsZero(V, ¬C1) is true, indicating that an LLVM dataflow analysis has concluded that V ∧ ¬C1 = 0. %B and %V are input variables. C1 and C2 are constants. %t0, %t1, and %t2 are temporaries. This transformation is rooted at %R.
2.4. Undefined behaviors in LLVM
To aggressively optimize well-defined programs, LLVM has 3 distinct kinds of undefined behavior. Together, they enable many desirable optimizations, and LLVM aggressively exploits these opportunities.
Undefined behavior in LLVM resembles undefined behavior in C and C++: anything may happen to a program that executes it. The compiler may simply assume that undefined behavior does not occur; this assumption places a corresponding obligation on the program developer (or on the compiler and language runtime, when a safe language is compiled to LLVM) to ensure that undefined operations are never executed. An instruction that executes undefined behavior can be replaced with an arbitrary sequence of instructions. When an instruction executes undefined behavior, all subsequent instructions can be considered undefined as well.
Table 1 shows when Alive's arithmetic instructions have defined behavior, following the LLVM IR specification. For example, the udiv instruction is defined only when the dividend is non-zero. With the exception of memory access instructions (discussed in the original paper10), instructions not listed in Table 1 are always defined.
Table 1. The constraints for arithmetic instructions to be defined. <u is unsigned less-than. INT_MIN is the smallest signed integer value for a given bitwidth.
The undefined value (undef in the IR) is a limited form of undefined behavior that mimics a free-floating hardware register than can return any value each time it is read. Semantically, undef stands for the set of all possible bit patterns for a particular type; the compiler is free to pick a convenient value for each use of undef to enable aggressive optimizations. For example, a 1-bit undefined value, sign-extended to 32 bits, produces a variable containing either all 0s or all 1s.
Poison values, which are distinct from undefined values, are used to indicate that a side-effect-free instruction has a condition that produces undefined behavior. When the poison value gets used by an instruction with side effects, the program exhibits true undefined behavior. Hence, poison values are deferred undefined behaviors: they are intended to support speculative execution of possibly-undefined operations. Poison values taint subsequent dependent instructions; unlike undef, poison values cannot be untainted by subsequent operations. The subtleties in the semantics of undef and poison values and its impact on either enabling or disabling optimizations are currently being explored.8
Shift instructions, shl, ashr, and lshr, produce a poison value when their second argument, the shift amount, is larger than or equal to the bit width of the operation.
Instruction attributes modify the behavior of some LLVM instructions. The nsw attribute ("no signed wrap") makes signed overflow undefined. For example, this Alive transformation, which is equivalent to the optimization of (x+1) >x to 1 in C and C ++ where x is a signed integer, is valid:
%1 = add nsw %x, 1
%2 = icmp sgt %1, %x
=>
%2 = true
An analogous nuw attribute exists to rule out unsigned wrap. If an add, subtract, multiply, or left shift operation with an nsw or nuw attribute overflows, the result is poison. Additionally, LLVM's right shift and divide instructions have an exact attribute that requires an operation to not be lossy. Table 2 provides the constraints for the instructions to be poison-free. Developers writing Alive patterns can omit instruction attributes, in which case Alive infers where they can be safely placed.
Table 2. The constraints for arithmetic instructions to be poison-free. >>u and ÷u are the unsigned shift and division operations. B is the bitwidth of the operands. SExt(a, n) sign-extends a by n bits; ZExt(a, n) zero-extends a by n bits.
3. Verifying Optimizations in Alive
The Alive interpreter verifies a transformation by automatically encoding the source and target, their definedness conditions, and the overall correctness criteria into SMT queries. An Alive transformation is parametric over the set of all feasible types: the concrete types satisfying the constraints of LLVM's type system and not exceeding the default limit of 64 bits.
In the absence of undefined behavior in the source or target of an Alive transformation, we can check correctness using a straightforward equivalence check: for each valuation of the input variables, the value of any variable that is present in both the source and target must be identical. However, an equivalence check is not sufficient to prove correctness in the presence of any of the 3 kinds of undefined behavior described in Section 2.4. We use refinement to reason about optimizations in the presence of undefined behavior. The target of an Alive transformation refines the source template if all the behaviors of the target are included in the set of behaviors of the source. That is, a transformation may remove undefined behaviors but not add them.
When an optimization contains or may produce undef values, we need to ensure that the target never produces a value that the source does not produce. In other words, an undef in the source represents a set of values and the target can refine it to any particular value, but an undef in the target represents a set of values which must all be refinements of the source. Poison values are handled by ensuring that an instruction in the target template will not yield a poison value when the source instruction did not, for any specific choice of input values. In summary, we check correctness by checking (1) the target is defined when the source is defined, (2) the target is poison-free when the source is poison-free, and (3) the target produces a subset of the values produced by the source when the source is defined and poison-free.
To determine whether these conditions hold, we ask an SMT solver to find cases where they are violated. When found, these counter-examples are reported to the user, as shown in Figure 3. Conversely, if the SMT solver can show that no counter-example exists, then the conditions must hold and the optimization is valid.
Figure 3. Alive's counterexample for the incorrect transformation reported as LLVM PR21245.
3.1. Verification condition generation
Alive's Verification Condition Generator (VC Gen) encodes the values, instructions, and expressions in a transformation into SMT expressions using the theory of bitvectors. The correspondence between LLVM operations and bitvector logic is very close, which makes the encoding straightforward. For each instruction, the interpreter computes 3 SMT expressions: (1) an expression ι for the result of the instruction, (2) an expression δL indicating whether the instruction is defined, and (3) an expression ρ indicating whether the result is free of poison. The first has a type corresponding to the return type of the instruction. The others are Boolean predicates. All 3 may contain free variables, corresponding to the uninterpreted input variables and symbolic constants in the optimization.
Typically, an instruction's result is encoded by applying the corresponding bitvector operation to the encoding of its arguments. Its definedness and poison-free conditions are the conjunction of the definedness and poison-free conditions, respectively, of its arguments along with any specific requirements for that instruction.
For example, consider the instruction udiv exact %a, %b, which is encoded as follows,
where ÷u is unsigned bitvector division. The unsigned division requires the second argument to be non-zero, and the exact attribute requires %a to be divisible by %b.
Encoding undefvalues. Undefvalues represent sets of possible values. The VC Gen encodes them as fresh SMT variables, which are collected in a set
No entries found