{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,10]],"date-time":"2025-10-10T01:19:44Z","timestamp":1760059184557,"version":"build-2065373602"},"reference-count":27,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA2","content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2025,10,9]]},"abstract":"<jats:p>LLVM's backends translate its intermediate representation (IR) to  \nassembly or object code. Alongside register allocation and  \ninstruction selection, these backends contain many analogues of  \ncomponents traditionally associated with compiler middle ends:  \ndataflow analyses, common subexpression elimination, loop invariant  \ncode motion, and a first-class IR -- MIR, the \"machine IR.\" In  \neffect, this kind of compiler backend is a highly optimizing compiler  \nin its own right, with all of the correctness hazards entailed by a  \nmillion lines of intricate C++. As a step towards gaining confidence  \nin the correctness of work done by LLVM backends, we have created  \narm-tv, which formally verifies translations between LLVM IR and  \nAArch64 (64-bit ARM) code. Ours is not the first translation  \nvalidation work for LLVM, but we have advanced the state of the art  \nalong multiple fronts: arm-tv is a checking validator that enforces  \nnumerous ABI rules; we have extended Alive2 (which we reuse as a  \nverification backend) to deal with unstructured mixes of pointers and  \nintegers that are typical of assembly code; we investigate the  \ntradeoffs between hand-written AArch64 semantics and those derived  \nmechanically from ARM's published formal semantics; and, we have used  \narm-tv to discover 45 previously unknown miscompilation bugs in this  \nLLVM backend, most of which are now fixed in upstream LLVM.<\/jats:p>","DOI":"10.1145\/3763147","type":"journal-article","created":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T08:51:31Z","timestamp":1759999891000},"page":"2710-2735","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Translation Validation for LLVM\u2019s AArch64 Backend"],"prefix":"10.1145","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0009-0001-0355-2009","authenticated-orcid":false,"given":"Ryan","family":"Berger","sequence":"first","affiliation":[{"name":"NVIDIA, Santa Clara, USA"}]},{"ORCID":"https:\/\/orcid.org\/0009-0005-8252-8814","authenticated-orcid":false,"given":"Mitch","family":"Briles","sequence":"additional","affiliation":[{"name":"University of Utah, Salt Lake City, USA"}]},{"ORCID":"https:\/\/orcid.org\/0009-0009-5095-368X","authenticated-orcid":false,"given":"Nader","family":"Boushehrinejad Moradi","sequence":"additional","affiliation":[{"name":"University of Utah, Salt Lake City, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8758-0666","authenticated-orcid":false,"given":"Nicholas","family":"Coughlin","sequence":"additional","affiliation":[{"name":"Defence Science and Technology Group, Brisbane, Australia"},{"name":"University of Queensland, Brisbane, Australia"}]},{"ORCID":"https:\/\/orcid.org\/0009-0001-2599-2259","authenticated-orcid":false,"given":"Kait","family":"Lam","sequence":"additional","affiliation":[{"name":"Defence Science and Technology Group, Brisbane, Australia"},{"name":"University of Queensland, Brisbane, Australia"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3160-1672","authenticated-orcid":false,"given":"Nuno P.","family":"Lopes","sequence":"additional","affiliation":[{"name":"INESC-ID, Lisbon, Portugal"},{"name":"Instituto Superior T\u00e9cnico - University of Lisbon, Lisbon, Portugal"}]},{"ORCID":"https:\/\/orcid.org\/0009-0006-8473-3667","authenticated-orcid":false,"given":"Stefan","family":"Mada","sequence":"additional","affiliation":[{"name":"University of Utah, Salt Lake City, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0049-5045","authenticated-orcid":false,"given":"Tanmay","family":"Tirpankar","sequence":"additional","affiliation":[{"name":"University of Utah, Salt Lake City, USA"}]},{"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"}]}],"member":"320","published-online":{"date-parts":[[2025,10,9]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3385964"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","unstructured":"Yuyou Fan and John Regehr. 2024. High-Throughput Formal-Methods-Assisted Fuzzing for LLVM. In CGO. https:\/\/doi.org\/10.1109\/CGO57630.2024.10444854 10.1109\/CGO57630.2024.10444854","DOI":"10.1109\/CGO57630.2024.10444854"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/3729275"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","unstructured":"Seungwan Kwon Jaeseong Kwon Wooseok Kang Juneyoung Lee and Kihong Heo. 2024. Translation Validation for JIT Compiler in the V8 JavaScript Engine. In ICSE. https:\/\/doi.org\/10.1145\/3597503.3639189 10.1145\/3597503.3639189","DOI":"10.1145\/3597503.3639189"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.34727\/2023\/isbn.978-3-85448-060-0_36"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","unstructured":"Vu Le Mehrdad Afshari and Zhendong Su. 2014. Compiler validation via equivalence modulo inputs. In PLDI. https:\/\/doi.org\/10.1145\/2594291.2594334 10.1145\/2594291.2594334","DOI":"10.1145\/2594291.2594334"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/3276495"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-81688-9_35"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/3062341.3062343"},{"key":"e_1_2_2_10_1","unstructured":"Arm Limited. 2025. Arm A64 Instruction Set for A-profile architecture. https:\/\/www.arm.com\/architecture\/cpu\/a-profile"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP46214.2022.9833799"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/3428264"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","unstructured":"Nuno P. Lopes Juneyoung Lee Chung-Kil Hur Zhengyang Liu and John Regehr. 2021. Alive2: bounded translation validation for LLVM. In PLDI. https:\/\/doi.org\/10.1145\/3453483.3454030 10.1145\/3453483.3454030","DOI":"10.1145\/3453483.3454030"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","unstructured":"George C. Necula. 2000. Translation validation for an optimizing compiler. In PLDI. https:\/\/doi.org\/10.1145\/349299.349314 10.1145\/349299.349314","DOI":"10.1145\/349299.349314"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","unstructured":"Amir Pnueli Michael Siegel and Eli Singerman. 1998. Translation Validation. In TACAS. https:\/\/doi.org\/10.1007\/BFb0054170 10.1007\/BFb0054170","DOI":"10.1007\/BFb0054170"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","unstructured":"Fr\u00e9d\u00e9ric Recoules S\u00e9bastien Bardin Richard Bonichon Laurent Mounier and Marie-Laure Potet. 2020. Get rid of inline assembly through verification-oriented lifting. In ASE. https:\/\/doi.org\/10.1109\/ASE.2019.00060 10.1109\/ASE.2019.00060","DOI":"10.1109\/ASE.2019.00060"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","unstructured":"Alastair Reid. 2016. Trustworthy specifications of ARM\u00ae v8-A and v8-M system level architecture. In FMCAD. https:\/\/doi.org\/10.1109\/FMCAD.2016.7886675 10.1109\/FMCAD.2016.7886675","DOI":"10.1109\/FMCAD.2016.7886675"},{"key":"e_1_2_2_18_1","unstructured":"Yuyang Rong Zhanghan Yu Zhenkai Weng Stephen Neuendorffer and Hao Chen. 2024. IRFuzzer: Specialized Fuzzing for LLVM Backend Code Generation. arxiv:2402.05256."},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/3649863"},{"key":"e_1_2_2_20_1","unstructured":"Fabian Ruffy Tao Wang and Anirudh Sivaraman. 2020. Gauntlet: finding bugs in compilers for programmable packet processing. In OSDI. https:\/\/www.usenix.org\/conference\/osdi20\/presentation\/ruffy"},{"key":"e_1_2_2_21_1","volume-title":"Automatically proving the correctness of translations involving optimized code. Ph. D. Dissertation","author":"Samet Hanan","unstructured":"Hanan Samet. 1975. Automatically proving the correctness of translations involving optimized code. Ph. D. Dissertation. Stanford University."},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","unstructured":"Thomas Sewell Magnus Myreen and Gerwin Klein. 2013. Translation Validation for a Verified OS Kernel. In PLDI. https:\/\/doi.org\/10.1145\/2491956.2462183 10.1145\/2491956.2462183","DOI":"10.1145\/2491956.2462183"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","unstructured":"Jean-Baptiste Tristan Paul Govereau and Greg Morrisett. 2011. Evaluating value-graph translation validation for LLVM. In PLDI. https:\/\/doi.org\/10.1145\/1993498.1993533 10.1145\/1993498.1993533","DOI":"10.1145\/1993498.1993533"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","unstructured":"Freek Verbeek Joshua Bockenek Zhoulai Fu and Binoy Ravindran. 2022. Formally verified lifting of C-compiled x86-64 binaries. In PLDI. https:\/\/doi.org\/10.1145\/3519939.3523702 10.1145\/3519939.3523702","DOI":"10.1145\/3519939.3523702"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/3689755"},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","unstructured":"Xuejun Yang Yang Chen Eric Eide and John Regehr. 2011. Finding and understanding bugs in C compilers. In PLDI. https:\/\/doi.org\/10.1145\/1993498.1993532 10.1145\/1993498.1993532","DOI":"10.1145\/1993498.1993532"},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","unstructured":"Jianzhou Zhao Santosh Nagarakatte Milo M.K. Martin and Steve Zdancewic. 2013. Formal verification of SSA-based optimizations for LLVM. In PLDI. https:\/\/doi.org\/10.1145\/2491956.2462164 10.1145\/2491956.2462164","DOI":"10.1145\/2491956.2462164"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3763147","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T17:42:05Z","timestamp":1760031725000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3763147"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,10,9]]},"references-count":27,"journal-issue":{"issue":"OOPSLA2","published-print":{"date-parts":[[2025,10,9]]}},"alternative-id":["10.1145\/3763147"],"URL":"https:\/\/doi.org\/10.1145\/3763147","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,10,9]]},"assertion":[{"value":"2025-03-24","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-08-12","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-10-09","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}