{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,9,10]],"date-time":"2026-09-10T10:07:43Z","timestamp":1789034863962,"version":"build-2803163510"},"reference-count":22,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA","license":[{"start":{"date-parts":[[2018,10,24]],"date-time":"2018-10-24T00:00:00Z","timestamp":1540339200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2018,10,24]]},"abstract":"<jats:p>LLVM miscompiles certain programs in C, C++, and Rust that use low-level language features such as raw pointers in Rust or conversion between integers and pointers in C or C++. The problem is that it is difficult for the compiler to implement aggressive, high-level memory optimizations while also respecting the guarantees made by the programming languages to low-level programs. A deeper problem is that the memory model for LLVM's intermediate representation (IR) is informal and the semantics of corner cases are not always clear to all compiler developers. We developed a novel memory model for LLVM IR and formalized it. The new model requires a handful of problematic IR-level optimizations to be removed, but it also supports the addition of new optimizations that were not previously legal. We have implemented the new model and shown that it fixes known memory-model-related miscompilations without impacting the quality of generated code.<\/jats:p>","DOI":"10.1145\/3276495","type":"journal-article","created":{"date-parts":[[2018,10,24]],"date-time":"2018-10-24T11:57:18Z","timestamp":1540382238000},"page":"1-28","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":23,"title":["Reconciling high-level optimizations and low-level code in LLVM"],"prefix":"10.1145","volume":"2","author":[{"given":"Juneyoung","family":"Lee","sequence":"first","affiliation":[{"name":"Seoul National University, South Korea"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Chung-Kil","family":"Hur","sequence":"additional","affiliation":[{"name":"Seoul National University, South Korea"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Ralf","family":"Jung","sequence":"additional","affiliation":[{"name":"MPI-SWS, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Zhengyang","family":"Liu","sequence":"additional","affiliation":[{"name":"University of Utah, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"John","family":"Regehr","sequence":"additional","affiliation":[{"name":"University of Utah, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Nuno P.","family":"Lopes","sequence":"additional","affiliation":[{"name":"Microsoft Research, UK"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2018,10,24]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"crossref","unstructured":"Fr\u00e9d\u00e9ric Besson Sandrine Blazy and Pierre Wilke. 2014. A Precise and Abstract Memory Model for C Using Symbolic Values. In APLAS.  Fr\u00e9d\u00e9ric Besson Sandrine Blazy and Pierre Wilke. 2014. A Precise and Abstract Memory Model for C Using Symbolic Values. In APLAS.","DOI":"10.1007\/978-3-319-12736-1_24"},{"key":"e_1_2_2_2_1","doi-asserted-by":"crossref","unstructured":"Fr\u00e9d\u00e9ric Besson Sandrine Blazy and Pierre Wilke. 2015. A Concrete Memory Model for CompCert. In ITP.  Fr\u00e9d\u00e9ric Besson Sandrine Blazy and Pierre Wilke. 2015. A Concrete Memory Model for CompCert. In ITP.","DOI":"10.1007\/978-3-319-22102-1_5"},{"key":"e_1_2_2_3_1","doi-asserted-by":"crossref","unstructured":"Fr\u00e9d\u00e9ric Besson Sandrine Blazy and Pierre Wilke. 2017a. CompCertS: A Memory-Aware Verified C Compiler Using Pointer as Integer Semantics. In ITP.  Fr\u00e9d\u00e9ric Besson Sandrine Blazy and Pierre Wilke. 2017a. CompCertS: A Memory-Aware Verified C Compiler Using Pointer as Integer Semantics. In ITP.","DOI":"10.1007\/978-3-319-66107-0_6"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-017-9439-z"},{"key":"e_1_2_2_5_1","volume-title":"Watson","author":"Chisnall David","year":"2016","unstructured":"David Chisnall , Justus Matthiesen , Kayvan Memarian , Peter Sewell , and Robert N. M . Watson . 2016 . C memory object and value semantics: the space of de facto and ISO standards. https:\/\/www.cl.cam.ac.uk\/~pes20\/cerberus\/notes30.pdf David Chisnall, Justus Matthiesen, Kayvan Memarian, Peter Sewell, and Robert N. M. Watson. 2016. C memory object and value semantics: the space of de facto and ISO standards. https:\/\/www.cl.cam.ac.uk\/~pes20\/cerberus\/notes30.pdf"},{"key":"e_1_2_2_6_1","volume-title":"Navas","author":"Gurfinkel Arie","year":"2017","unstructured":"Arie Gurfinkel and Jorge A . Navas . 2017 . A Context-Sensitive Memory Model for Verification of C\/C++ Programs. In SAS. Arie Gurfinkel and Jorge A. Navas. 2017. A Context-Sensitive Memory Model for Verification of C\/C++ Programs. In SAS."},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737979"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2738005"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-03545-1_4"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676724.2693571"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/3062341.3062343"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/1538788.1538814"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-008-9099-0"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737965"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908081"},{"key":"e_1_2_2_16_1","unstructured":"Kayvan Memarian and Peter Sewell. 2016a. Clarifying the C memory object model (revised version of WG14 N2012). https:\/\/www.cl.cam.ac.uk\/~pes20\/cerberus\/notes64- wg14.html  Kayvan Memarian and Peter Sewell. 2016a. Clarifying the C memory object model (revised version of WG14 N2012). https:\/\/www.cl.cam.ac.uk\/~pes20\/cerberus\/notes64- wg14.html"},{"key":"e_1_2_2_17_1","volume-title":"N2090: Clarifying Pointer Provenance (Draft Defect Report or Proposal for C2x). https:\/\/www.cl.cam.ac.uk\/~pes20\/cerberus\/n2090","author":"Memarian Kayvan","year":"2016","unstructured":"Kayvan Memarian and Peter Sewell . 2016 b. N2090: Clarifying Pointer Provenance (Draft Defect Report or Proposal for C2x). https:\/\/www.cl.cam.ac.uk\/~pes20\/cerberus\/n2090 .html Kayvan Memarian and Peter Sewell. 2016b. N2090: Clarifying Pointer Provenance (Draft Defect Report or Proposal for C2x). https:\/\/www.cl.cam.ac.uk\/~pes20\/cerberus\/n2090.html"},{"key":"e_1_2_2_18_1","unstructured":"The LLVM Project. 2018. LLVM Language Reference Manual. https:\/\/llvm.org\/docs\/LangRef.html  The LLVM Project. 2018. LLVM Language Reference Manual. https:\/\/llvm.org\/docs\/LangRef.html"},{"key":"e_1_2_2_19_1","volume-title":"Souper: A Synthesizing Superoptimizer. CoRR abs\/1711.04422","author":"Sasnauskas Raimondas","year":"2017","unstructured":"Raimondas Sasnauskas , Yang Chen , Peter Collingbourne , Jeroen Ketema , Jubi Taneja , and John Regehr . 2017 . Souper: A Synthesizing Superoptimizer. CoRR abs\/1711.04422 (2017). http:\/\/arxiv.org\/abs\/1711.04422 Raimondas Sasnauskas, Yang Chen, Peter Collingbourne, Jeroen Ketema, Jubi Taneja, and John Regehr. 2017. Souper: A Synthesizing Superoptimizer. CoRR abs\/1711.04422 (2017). http:\/\/arxiv.org\/abs\/1711.04422"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/2487241.2487248"},{"key":"e_1_2_2_21_1","doi-asserted-by":"crossref","unstructured":"Wei Wang Clark Barrett and Thomas Wies. 2017. Partitioned Memory Models for Program Analysis. In VMCAI.  Wei Wang Clark Barrett and Thomas Wies. 2017. Partitioned Memory Models for Program Analysis. In VMCAI.","DOI":"10.1007\/978-3-319-52234-0_29"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103656.2103709"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3276495","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3276495","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T01:01:59Z","timestamp":1750208519000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3276495"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,10,24]]},"references-count":22,"journal-issue":{"issue":"OOPSLA","published-print":{"date-parts":[[2018,10,24]]}},"alternative-id":["10.1145\/3276495"],"URL":"https:\/\/doi.org\/10.1145\/3276495","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018,10,24]]},"assertion":[{"value":"2018-10-24","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}