Hydra: Generalizing Peephole Optimizations with Program Synthesis
Manasij Mukherjee, John Regehr
Abstract
Optimizing compilers rely on peephole optimizations to simplify combinations of instructions and remove redundant instructions. Typically, a new peephole optimization is added when a compiler developer notices an optimization opportunity---a collection of dependent instructions that can be improved---and manually derives a more general rewrite rule that optimizes not only the original code, but also other, similar collections of instructions. In this paper, we present Hydra, a tool that automates the process of generalizing peephole optimizations using a collection of techniques centered on program synthesis. One of the most important problems we have solved is finding a version of each optimization that is independent of the bitwidths of the optimization's inputs (when this version exists). We show that Hydra can generalize 75% of the ungeneralized missed peephole optimizations that LLVM developers have posted to the LLVM project's issue tracker. All of Hydra's generalized peephole optimizations have been formally verified, and furthermore we can automatically turn them into C++ code that is suitable for inclusion in an LLVM pass.
Ask about this paper
Your agent reads all of it.
Lune indexed this paper to the last equation, along with the top-tier papers that cite it. Ask a question and the answer quotes them.
Cited by top-tier papers5
- First-Class Verification Dialects for MLIRMathieu Fehr, Yuyou Fan, Hugo Pompougnac, John Regehr et al.PLDI 2025 · 5 citations
- Exploiting Undefined Behavior in C/C++ Programs for Optimization: A Study on the Performance ImpactLucian Popescu, Nuno P. LopesPLDI 2025 · 2 citations
- LPO: Discovering Missed Peephole Optimizations with Large Language ModelsZhenyang Xu, Hongxu Xu, Yongqiang Tian, Xintong Zhou et al.ASPLOS 2026 · 1 citation
- Optimism in Equality SaturationRussel Arbore, Alvin Cheung, Max WillseyPLDI 2026
- Scaling Instruction-Selection Verification against Authoritative ISA SemanticsMichael McLoughlin, Ashley Sheng, Chris Fallin, Bryan Parno et al.OOPSLA 2025
Builds on5
- Alive2: bounded translation validation for LLVMNuno P. Lopes, Juneyoung Lee, Chung-Kil Hur, Zhengyang Liu et al.PLDI 2021 · 109 citations
- Program synthesis by type-guided abstraction refinementZheng Guo, Michael James, David Justo, Jiaxiao Zhou et al.POPL 2020 · 45 citations
- FlashFill++: Scaling Programming by Example by Cutting to the ChaseJosé Cambronero, Sumit Gulwani, Vu Le, Daniel Perelman et al.POPL 2023 · 27 citations
- Synthesizing abstract transformersPankaj Kumar Kalita, Sujit Kumar Muduli, Loris D'Antoni, Thomas W. Reps et al.OOPSLA 2022 · 21 citations
- Dataflow-based pruning for speeding up superoptimizationManasij Mukherjee, Pranav Kant, Zhengyang Liu, John RegehrOOPSLA 2020 · 21 citations
Related papers
- Seeking Evidence of Further Optimization: Detecting Missed Optimizations through Compiler’s Native AnalysesYi Zhang, Yu Wang, Ke Wang, Linzhang WangOOPSLA 2026
- Finding missed optimizations through the lens of dead code eliminationTheodoros Theodoridis, Manuel Rigger, Zhendong SuASPLOS 2022 · 48 citations
- Certified Decision Procedures for Width-Independent Bitvector PredicatesSiddharth Bhat, Léo Stefanesco, Chris Hughes, Tobias GrosserOOPSLA 2025 · 2 citations
- Pattern-Based Peephole Optimizations with Java JIT TestsZhiqiang Zang, Aditya Thimmaiah, Milos GligoricISSTA 2023 · 2 citations
- FLUX: Finding Bugs with LLVM IR Based Unit Test CrossoversEric Liu, Shengjie Xu, David LieASE 2023 · 8 citations
