Content area
Peephole optimizations are a key component of optimizing compilers. The process of adding a new peephole optimization is manual and time-consuming. The focus of this dissertation is employing formal methods to aid developers in this process. This dissertation presents two techniques to improve the scalability of Souper, a superoptimizer for finding peephole optimizations for LLVM Intermediate Representation (IR). Finding optimization opportunities is merely a start—an optimization still needs to be generalized for it to be useful in a compiler. A superoptimizer does not help with this. The second part of this dissertation presents Hydra, a tool that uses synthesis to generalize peephole optimizations.
Souper’s core algorithm is a lazy enumerative search to find optimizations and it uses Alive2—a translation validation tool for LLVM—to verify the optimizations. This dissertation presents a technique to improve the scalability of Souper by using dataflow analysis to prune the search space. This technique reduces the number of solver calls by 65% and makes Souper 2.32x faster for optimizing standard benchmarks.
Enumeration—even with pruning—is hard to scale. This dissertation presents Iago— a drop in replacement for Souper that uses a Large Language Model (LLM), and complements it with formal verification to mitigate the risk of incorrect optimizations. Moreover, LLM results are often almost-valid, and Iago uses sketching to fix these results. Iago avoids direct enumeration, and thus, finds larger and more complex optimizations consisting of two or more instructions.
The optimizations found manually, or with a superoptimizer, are often too specific to be implemented in a compiler. Hydra uses program synthesis techniques to generalize concrete constants to symbolic constants, find preconditions, and then ensure the optimization is independent of bitwidth whenever possible. Hydra was able to generalize 75% of the peephole optimizations posted to the LLVM project’s issue tracker.