{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T18:21:31Z","timestamp":1784830891820,"version":"3.55.0"},"reference-count":50,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA1","license":[{"start":{"date-parts":[[2024,4,29]],"date-time":"2024-04-29T00:00:00Z","timestamp":1714348800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"name":"National Science Foundation","award":["1955688"],"award-info":[{"award-number":["1955688"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2024,4,29]]},"abstract":"<jats:p>Optimizing compilers rely on peephole optimizations to simplify  \ncombinations of instructions and remove redundant instructions.  \nTypically, a new peephole optimization is added when a compiler  \ndeveloper notices an optimization opportunity---a collection of  \ndependent instructions that can be improved---and manually derives a  \nmore general rewrite rule that optimizes not only the original code,  \nbut also other, similar collections of instructions.  \nIn this paper, we present Hydra, a tool that automates the process of  \ngeneralizing peephole optimizations using a collection of techniques  \ncentered on program synthesis.  \nOne of the most important problems we have solved is finding a version  \nof each optimization that is independent of the bitwidths of the  \noptimization's inputs (when this version exists).  \nWe show that Hydra can generalize 75% of the ungeneralized missed  \npeephole optimizations that LLVM developers have posted to the LLVM  \nproject's issue tracker.  \nAll of Hydra's generalized peephole optimizations have been formally  \nverified, and furthermore we can automatically turn them into C++ code  \nthat is suitable for inclusion in an LLVM pass.<\/jats:p>","DOI":"10.1145\/3649837","type":"journal-article","created":{"date-parts":[[2024,4,29]],"date-time":"2024-04-29T17:53:50Z","timestamp":1714413230000},"page":"725-753","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":12,"title":["Hydra: Generalizing Peephole Optimizations with Program Synthesis"],"prefix":"10.1145","volume":"8","author":[{"ORCID":"https:\/\/orcid.org\/0009-0007-8460-6745","authenticated-orcid":false,"given":"Manasij","family":"Mukherjee","sequence":"first","affiliation":[{"name":"University of Utah, Salt Lake City, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7025-4610","authenticated-orcid":false,"given":"John","family":"Regehr","sequence":"additional","affiliation":[{"name":"University of Utah, Salt Lake City, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2024,4,29]]},"reference":[{"key":"e_1_2_1_1_1","volume-title":"International Conference on Computer Aided Verification. 270\u2013288","author":"Abate Alessandro","year":"2018","unstructured":"Alessandro Abate, Cristina David, Pascal Kesseli, Daniel Kroening, and Elizabeth Polgreen. 2018. Counterexample guided inductive synthesis modulo theories. In International Conference on Computer Aided Verification. 270\u2013288."},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","unstructured":"Rajeev Alur Rastislav Bodik Garvit Juniwal Milo M. K. Martin Mukund Raghothaman Sanjit A. Seshia Rishabh Singh Armando Solar-Lezama Emina Torlak and Abhishek Udupa. 2013. Syntax-guided synthesis. Formal Methods in Computer-Aided Design 1\u201317. https:\/\/doi.org\/10.1109\/FMCAD.2013.6679385 10.1109\/FMCAD.2013.6679385","DOI":"10.1109\/FMCAD.2013.6679385"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","unstructured":"Rajeev Alur Pavol \u010cern\u00fd and Arjun Radhakrishna. 2015. Synthesis Through Unification. In Computer Aided Verification Daniel Kroening and Corina S. P\u0103s\u0103reanu (Eds.). 163\u2013179. isbn:978-3-319-21668-3 https:\/\/doi.org\/10.1007\/978-3-319-21668-3_10 10.1007\/978-3-319-21668-3_10","DOI":"10.1007\/978-3-319-21668-3_10"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54577-5_18"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/1168918.1168906"},{"key":"e_1_2_1_6_1","volume-title":"CVC4","author":"Barrett Clark","unstructured":"Clark Barrett, Christopher L. Conway, Morgan Deters, Liana Hadarean, Dejan Jovanovi\u0107, Tim King, Andrew Reynolds, and Cesare Tinelli. 2011. CVC4. In Computer Aided Verification, Ganesh Gopalakrishnan and Shaz Qadeer (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg. 171\u2013177. isbn:978-3-642-22110-1"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837666"},{"key":"e_1_2_1_8_1","volume-title":"Optgen: A Generator for Local Optimizations. In 24th International Conference on Compiler Construction (CC","author":"Buchwald Sebastian","year":"2015","unstructured":"Sebastian Buchwald. 2015. Optgen: A Generator for Local Optimizations. In 24th International Conference on Compiler Construction (CC 2015), Bj\u00f6rn Franke (Ed.). London, UK. 171\u2013189."},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/3571226"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/502874.502885"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.5555\/1792734.1792766"},{"key":"e_1_2_1_12_1","volume-title":"Solving Exists\/Forall Problems With Yices. In 13th International Workshop on Satisfiability Modulo Theories (SMT","author":"Dutertre Bruno","year":"2015","unstructured":"Bruno Dutertre. 2015. Solving Exists\/Forall Problems With Yices. In 13th International Workshop on Satisfiability Modulo Theories (SMT 2015)."},{"key":"e_1_2_1_13_1","volume-title":"Frontiers of Combining Systems","author":"Ekici Burak","unstructured":"Burak Ekici, Arjun Viswanathan, Yoni Zohar, Cesare Tinelli, and Clark Barrett. 2023. Formal Verification of Bit-Vector Invertibility Conditions in Coq. In Frontiers of Combining Systems, Uli Sattler and Martin Suda (Eds.). Springer Nature Switzerland, Cham. 41\u201359. isbn:978-3-031-43369-6"},{"key":"e_1_2_1_14_1","doi-asserted-by":"crossref","unstructured":"Graeme Gange Jorge A. Navas Peter Schachte Harald S\u00f8ndergaard and Peter James Stuckey. 2013. Abstract Interpretation over Non-lattice Abstract Domains. In SAS.","DOI":"10.1007\/978-3-642-38856-9_3"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/3318162"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1080\/00207168908803778"},{"key":"e_1_2_1_17_1","doi-asserted-by":"crossref","unstructured":"Sumit Gulwani. 2011. Automating string processing in spreadsheets using input-output examples. In POPL \u201911.","DOI":"10.1145\/1926385.1926423"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371080"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00236-017-0294-5"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1109\/ASE.2019.00033"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/512529.512566"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/3563334"},{"key":"e_1_2_1_23_1","volume-title":"Automatic Abstraction for Congruences","author":"King Andy","unstructured":"Andy King and Harald S\u00f8ndergaard. 2010. Automatic Abstraction for Congruences. In Verification, Model Checking, and Abstract Interpretation, Gilles Barthe and Manuel Hermenegildo (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg. 197\u2013213. isbn:978-3-642-11319-2"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/3192366.3192410"},{"key":"e_1_2_1_25_1","unstructured":"LLVM-LangRef. 2023. LLVM Language Reference Manual. http:\/\/llvm.org\/docs\/LangRef.html Accessed: 9-1-2023"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/3106237.3106253"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454030"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737965"},{"key":"e_1_2_1_29_1","volume-title":"Lopes and Jos\u00e9 Monteiro","author":"Nuno","year":"2014","unstructured":"Nuno P. Lopes and Jos\u00e9 Monteiro. 2014. Weakest Precondition Synthesis for Compiler Optimizations. In Verification, Model Checking, and Abstract Interpretation, Kenneth L. McMillan and Xavier Rival (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg. 203\u2013221. isbn:978-3-642-54013-4"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/36177.36194"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/364995.365000"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/3140587.3062372"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993316.1993537"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/3428245"},{"key":"e_1_2_1_35_1","volume-title":"ECOOP 2013 \u2013 Object-Oriented Programming, Giuseppe Castagna (Ed.). Springer Berlin Heidelberg","author":"Negara Stas","year":"2013","unstructured":"Stas Negara, Nicholas Chen, Mohsen Vakilian, Ralph E. Johnson, and Danny Dig. 2013. A Comparative Study of Manual and Automated Refactorings. In ECOOP 2013 \u2013 Object-Oriented Programming, Giuseppe Castagna (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg. 552\u2013576. isbn:978-3-642-39038-8"},{"key":"e_1_2_1_36_1","volume-title":"Automated Deduction \u2013 CADE 27","author":"Niemetz Aina","unstructured":"Aina Niemetz, Mathias Preiner, Andrew Reynolds, Yoni Zohar, Clark Barrett, and Cesare Tinelli. 2019. Towards Bit-Width-Independent Proofs in SMT Solvers. In Automated Deduction \u2013 CADE 27, Pascal Fontaine (Ed.). Springer International Publishing, Cham. 366\u2013384. isbn:978-3-030-29436-6"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908099"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/2872362.2872387"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE.2017.44"},{"key":"e_1_2_1_40_1","volume-title":"Meeting","author":"Sands Duncan","year":"2011","unstructured":"Duncan Sands. 2011. Super-optimizing LLVM IR. http:\/\/llvm.org\/devmtg\/2011-11\/Sands_Super-optimizingLLVMIR.pdf Presentation at the 2011 LLVM Developers\u2019 Meeting"},{"key":"e_1_2_1_41_1","volume-title":"Souper: A Synthesizing Superoptimizer. arxiv:1711.04422.","author":"Sasnauskas Raimondas","year":"2017","unstructured":"Raimondas Sasnauskas, Yang Chen, Peter Collingbourne, Jeroen Ketema, Gratian Lup, Jubi Taneja, and John Regehr. 2017. Souper: A Synthesizing Superoptimizer. arxiv:1711.04422."},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/2451116.2451150"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290386"},{"key":"e_1_2_1_44_1","volume-title":"Program Synthesis by Sketching. Ph. D. Dissertation","author":"Solar-Lezama Armando","unstructured":"Armando Solar-Lezama. 2008. Program Synthesis by Sketching. Ph. D. Dissertation. Berkeley, CA, USA. isbn:978-1-109-09745-0 AAI3353225"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/2983990.2984006"},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/3368826.3377927"},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706345"},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/1480881.1480915"},{"key":"e_1_2_1_49_1","volume-title":"Automated Deduction - CADE-25, Amy P","author":"Tiwari Ashish","unstructured":"Ashish Tiwari, Adri\u00e0 Gasc\u00f3n, and Bruno Dutertre. 2015. Program Synthesis Using Dual Interpretation. In Automated Deduction - CADE-25, Amy P. Felty and Aart Middeldorp (Eds.). Springer International Publishing, Cham. 482\u2013497. isbn:978-3-319-21401-6"},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993316.1993532"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3649837","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3649837","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T22:54:06Z","timestamp":1750287246000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3649837"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,4,29]]},"references-count":50,"journal-issue":{"issue":"OOPSLA1","published-print":{"date-parts":[[2024,4,29]]}},"alternative-id":["10.1145\/3649837"],"URL":"https:\/\/doi.org\/10.1145\/3649837","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,4,29]]},"assertion":[{"value":"2024-04-29","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}