{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,10]],"date-time":"2026-07-10T09:12:25Z","timestamp":1783674745480,"version":"3.55.0"},"reference-count":68,"publisher":"Association for Computing Machinery (ACM)","issue":"PLDI","license":[{"start":{"date-parts":[[2024,6,20]],"date-time":"2024-06-20T00:00:00Z","timestamp":1718841600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2024,6,20]]},"abstract":"<jats:p>\n            Given a loop-free sequence of instructions, superoptimization techniques use a constraint solver to search for an equivalent sequence that is\n            <jats:italic toggle=\"yes\">optimal<\/jats:italic>\n            for a desired objective. The complexity of the search grows exponentially with the\n            <jats:italic toggle=\"yes\">length of the solution<\/jats:italic>\n            being constructed and the problem becomes intractable for large sequences of instructions. This paper presents a new approach to superoptimizing stack-bytecode via three novel components: (1) a greedy algorithm to refine the bound on the length of the optimal solution; (2) a new representation of the optimization problem as a set of weighted soft clauses in MaxSAT; (3) a series of domain-specific dominance and redundant constraints to reduce the search space for optimal solutions. We have developed a tool, named S\n            <jats:sc>uper<\/jats:sc>\n            S\n            <jats:sc>tack<\/jats:sc>\n            , which can be used to find optimal code translations of modern stack-based bytecode, namely WebAssembly or Ethereum bytecode. Experimental evaluation on more than 500,000 sequences shows the proposed greedy, constraint-based and SAT combination is able to greatly increase optimization gains achieved by existing superoptimizers and reduce to at least a fourth the optimization time.\n          <\/jats:p>","DOI":"10.1145\/3656435","type":"journal-article","created":{"date-parts":[[2024,6,20]],"date-time":"2024-06-20T16:27:20Z","timestamp":1718900840000},"page":"1437-1462","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":9,"title":["SuperStack: Superoptimization of Stack-Bytecode via Greedy, Constraint-Based, and SAT Techniques"],"prefix":"10.1145","volume":"8","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-0048-0705","authenticated-orcid":false,"given":"Elvira","family":"Albert","sequence":"first","affiliation":[{"name":"Complutense University of Madrid, Madrid, Spain"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6666-514X","authenticated-orcid":false,"given":"Maria","family":"Garcia de la Banda","sequence":"additional","affiliation":[{"name":"Monash University, Melbourne, Australia"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2109-8863","authenticated-orcid":false,"given":"Alejandro","family":"Hern\u00e1ndez-Cerezo","sequence":"additional","affiliation":[{"name":"Complutense University of Madrid, Madrid, Spain"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4535-2902","authenticated-orcid":false,"given":"Alexey","family":"Ignatiev","sequence":"additional","affiliation":[{"name":"Monash University, Melbourne, Australia"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0501-9830","authenticated-orcid":false,"given":"Albert","family":"Rubio","sequence":"additional","affiliation":[{"name":"Complutense University of Madrid, Madrid, Spain"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2186-0459","authenticated-orcid":false,"given":"Peter J.","family":"Stuckey","sequence":"additional","affiliation":[{"name":"Monash University, Melbourne, Australia"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2024,6,20]]},"reference":[{"key":"e_1_3_1_2_1","doi-asserted-by":"publisher","unstructured":"AlbertElvira Garcia de la BandaMaria Hern\u00e1ndez-CerezoAlejandro IgnatievAlexey RubioAlbert and StuckeyPeter J.. 2024. Artifact for \u201cSuperStack: Superoptimization of Stack-Bytecode via Greedy Constraint-based and SAT Techniques\u201d. https:\/\/doi.org\/10.5281\/zenodo.10801691 10.5281\/zenodo.10801691","DOI":"10.5281\/zenodo.10801691"},{"key":"e_1_3_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-99524-9_11"},{"key":"e_1_3_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/3506800"},{"key":"e_1_3_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-53288-8_10"},{"key":"e_1_3_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10601-010-9105-0"},{"key":"e_1_3_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39071-5_23"},{"key":"e_1_3_1_8_1","doi-asserted-by":"publisher","DOI":"10.3233\/FAIA201008"},{"key":"e_1_3_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-45193-8_8"},{"key":"e_1_3_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/1168857.1168906"},{"key":"e_1_3_1_11_1","doi-asserted-by":"publisher","DOI":"10.3233\/FAIA201017"},{"key":"e_1_3_1_12_1","doi-asserted-by":"publisher","DOI":"10.1109\/TDSC.2022.3232813"},{"key":"e_1_3_1_13_1","first-page":"51","volume-title":"In SAT Competition","author":"Biere Armin","year":"2020","unstructured":"BiereArmin, FazekasKatalin, FleuryMathias, and HeisingerMaximilian. 2020. CaDiCaL, Kissat, Paracooba, Plingeling and Treengeling entering the SAT Competition 2020. In SAT Competition, 51\u201353."},{"key":"e_1_3_1_14_1","doi-asserted-by":"publisher","DOI":"10.1109\/Blockchain50366.2020.00042"},{"key":"e_1_3_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/321892.321901"},{"key":"e_1_3_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/3397537.3397567"},{"key":"e_1_3_1_17_1","doi-asserted-by":"publisher","DOI":"10.1609\/SOCS.V12I1.18567"},{"key":"e_1_3_1_18_1","doi-asserted-by":"publisher","DOI":"10.1109\/TETC.2020.2979019"},{"key":"e_1_3_1_19_1","doi-asserted-by":"publisher","DOI":"10.1109\/SANER.2017.7884650"},{"key":"e_1_3_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/3563308"},{"key":"e_1_3_1_21_1","doi-asserted-by":"publisher","DOI":"10.3233\/SAT190014"},{"key":"e_1_3_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/3306618.3314283"},{"key":"e_1_3_1_23_1","unstructured":"Google. 2023. BigQuery. https:\/\/cloud.google.com\/bigquery"},{"key":"e_1_3_1_24_1","unstructured":"WebAssembly Group. 2017. Binaryen Optimizations. https:\/\/github.com\/WebAssembly\/binaryen#binaryen-optimizations"},{"key":"e_1_3_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/3062341.3062363"},{"key":"e_1_3_1_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-15488-1_7"},{"key":"e_1_3_1_27_1","doi-asserted-by":"publisher","DOI":"10.1609\/AAAI.V35I5.16498"},{"key":"e_1_3_1_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-94144-8_26"},{"key":"e_1_3_1_29_1","doi-asserted-by":"publisher","DOI":"10.3233\/SAT190116"},{"key":"e_1_3_1_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-94205-6_41"},{"key":"e_1_3_1_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-24318-4_21"},{"issue":"3","key":"e_1_3_1_32_1","article-title":"Not So Fast: Analyzing the Performance of WebAssembly vs. Native Code","volume":"44","author":"Jangda Abhinav","year":"2019","unstructured":"JangdaAbhinav, PowersBobby, BergerEmery D., and GuhaArjun. 2019. Not So Fast: Analyzing the Performance of WebAssembly vs. Native Code. login Usenix Mag. 44, 3 (2019). https:\/\/www.usenix.org\/publications\/login\/fall2019\/jangda","journal-title":"login Usenix Mag."},{"key":"e_1_3_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/3133850.3133856"},{"key":"e_1_3_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/1186632.1186633"},{"key":"e_1_3_1_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/s11390-021-1674-4"},{"key":"e_1_3_1_36_1","unstructured":"KotsiasP.C.. 2020. pcko1\/etherscan-python. https:\/\/doi.org\/10.5281\/zenodo.4306855"},{"key":"e_1_3_1_37_1","unstructured":"LindholmTim and YellinFrank. 1997. The Java Virtual Machine Specification. Addison-Wesley"},{"key":"e_1_3_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/3597926.3598068"},{"key":"e_1_3_1_39_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFB0026432"},{"key":"e_1_3_1_40_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-98334-9_21"},{"key":"e_1_3_1_41_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39799-8_39"},{"key":"e_1_3_1_42_1","doi-asserted-by":"publisher","DOI":"10.3233\/FAIA200987"},{"key":"e_1_3_1_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/36206.36194"},{"key":"e_1_3_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/364995.365000"},{"key":"e_1_3_1_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/3428245"},{"key":"e_1_3_1_46_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPICS.SAT.2022.8"},{"key":"e_1_3_1_47_1","volume-title":"In Preproceedings of 29th International Symposium on Logic-based Program Synthesis and Transformation (LOPSTR 2019)","author":"Nagele Julian","year":"2019","unstructured":"NageleJulian, and SchettMaria A. 2019. Blockchain Superoptimizer. In Preproceedings of 29th International Symposium on Logic-based Program Synthesis and Transformation (LOPSTR 2019). https:\/\/arxiv.org\/abs\/2005.05912"},{"key":"e_1_3_1_48_1","unstructured":"NallaniSand. 2020. Issue in Solidity\u2019s repository reporting stack too deep errors. https:\/\/github.com\/ethereum\/solidity\/issues\/13158"},{"key":"e_1_3_1_49_1","doi-asserted-by":"publisher","DOI":"10.24963\/IJCAI.2018\/189"},{"key":"e_1_3_1_50_1","doi-asserted-by":"publisher","DOI":"10.1109\/BRAINS52497.2021.9569819"},{"key":"e_1_3_1_51_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICTAI.2013.13"},{"key":"e_1_3_1_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/2872362.2872387"},{"key":"e_1_3_1_53_1","doi-asserted-by":"publisher","DOI":"10.3233\/FAIA201003"},{"key":"e_1_3_1_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/3282510"},{"key":"e_1_3_1_55_1","doi-asserted-by":"publisher","DOI":"10.3233\/FAIA201012"},{"key":"e_1_3_1_56_1","unstructured":"SasnauskasRaimondas ChenYang CollingbournePeter KetemaJeroen TanejaJubi and RegehrJohn. 2017. Souper: A Synthesizing Superoptimizer. CoRR abs\/1711.04422 (2017). http:\/\/arxiv.org\/abs\/1711.04422"},{"key":"e_1_3_1_57_1","doi-asserted-by":"publisher","DOI":"10.1145\/2451116.2451150"},{"key":"e_1_3_1_58_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-30923-7_10"},{"key":"e_1_3_1_59_1","doi-asserted-by":"publisher","DOI":"10.1007\/11564751_73"},{"key":"e_1_3_1_60_1","doi-asserted-by":"publisher","DOI":"10.1613\/JAIR.4231"},{"key":"e_1_3_1_61_1","doi-asserted-by":"publisher","DOI":"10.3233\/978-1-61499-672-9-810"},{"key":"e_1_3_1_62_1","unstructured":"Etherscan team. 2018. Etherscan. https:\/\/etherscan.io. https:\/\/etherscan.io"},{"key":"e_1_3_1_63_1","unstructured":"Milk Road team. 2023. EthereumPrice. https:\/\/ethereumprice.org\/history\/?start=2019-02-28end=2023-05-10currency=USD. https:\/\/ethereumprice.org\/history\/?start=2019-02-28end=2023-05-10currency=USD"},{"key":"e_1_3_1_64_1","unstructured":"Solidity team. 2022. Solidity documentation. https:\/\/docs.soliditylang.org\/en\/v0.8.17\/. https:\/\/docs.soliditylang.org\/en\/v0.8.17\/"},{"key":"e_1_3_1_65_1","unstructured":"Solidity team. 2023. Optimizer of Solidity compiler. https:\/\/docs.soliditylang.org\/en\/latest\/internals\/optimizer.html"},{"key":"e_1_3_1_66_1","unstructured":"W3C. 2016. WebAssembly. https:\/\/webassembly.org\/"},{"key":"e_1_3_1_67_1","unstructured":"Gavin Wood . 2019. Ethereum: A secure decentralised generalised transaction ledger."},{"key":"e_1_3_1_68_1","doi-asserted-by":"publisher","DOI":"10.1613\/JAIR.1.12719"},{"key":"e_1_3_1_69_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSUSC.2022.3221444"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3656435","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3656435","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T20:39:10Z","timestamp":1751661550000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3656435"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,6,20]]},"references-count":68,"journal-issue":{"issue":"PLDI","published-print":{"date-parts":[[2024,6,20]]}},"alternative-id":["10.1145\/3656435"],"URL":"https:\/\/doi.org\/10.1145\/3656435","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,6,20]]},"assertion":[{"value":"2024-06-20","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}