Document Open Access Logo

Populating the Peephole Optimizer of a Smart Contract Compiler

Authors Maria A. Schett , Julian Nagele

Thumbnail PDF


  • Filesize: 0.57 MB
  • 15 pages

Document Identifiers

Author Details

Maria A. Schett
  • University College London, UK
Julian Nagele
  • London, UK

Cite AsGet BibTex

Maria A. Schett and Julian Nagele. Populating the Peephole Optimizer of a Smart Contract Compiler. In 2nd Workshop on Formal Methods for Blockchains (FMBC 2020). Open Access Series in Informatics (OASIcs), Volume 84, pp. 3:1-3:15, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2020)


Developing compiler optimizations, especially for new, rapidly evolving smart contract languages, can be onerous and error-prone, but is especially important for smart contracts, where deployment and execution directly translate to monetary cost and which cannot change once deployed. One common optimization technique is the use of peephole optimizations, replacement rules that are applied using pattern-matching. These rules are normally constructed using human expertise, which is both time-consuming and far from systematic in exploring opportunities for optimization. In this work we propose a pipeline to automatically populate the peephole optimizer of a smart contract compiler. We apply superoptimization to an existing code base to obtain sequences of instructions, which can be replaced by cheaper, observationally equivalent instructions. We then generate peephole optimization rules by extracting the underlying patterns of these optimizations. We provide a case study of our approach and a prototype implementation for bytecode of the Ethereum Virtual Machine, the tool ppltr, which combines the superoptimizer ebso and the rule generator sorg. Then we evaluate our approach by generating and applying nearly 1k peephole optimization rules extracted from 2k optimizations obtained from deployed bytecode.

Subject Classification

ACM Subject Classification
  • Software and its engineering → Formal methods
  • Software and its engineering → Compilers
  • Compiler Optimizations
  • Constraint Solving
  • Ethereum Bytecode


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads


  1. Wilhelm Ackermann. Solvable cases of the decision problem. Studies in logic and the foundations of mathematics. North-Holland Publishing Co., Amsterdam, 1954. Google Scholar
  2. Elvira Albert, Pablo Gordillo, Albert Rubio, and Maria A Schett. Synthesis of super-optimized smart contracts using Max-SMT. In Proc. 32nd CAV, volume 12224 of LNCS. Springer, 2020. URL:
  3. Sidney Amani, Myriam Bégel, Maksym Bortin, and Mark Staples. Towards verifying ethereum smart contract bytecode in Isabelle/HOL. In Proc. 7th CPP, pages 66-77. ACM, 2018. URL:
  4. Franz Baader and Tobias Nipkow. Term Rewriting and All That. Cambridge University Press, New York, NY, USA, 1998. Google Scholar
  5. Sorav Bansal and Alex Aiken. Automatic generation of peephole superoptimizers. In Proc. 12th ASPLOS, pages 394-403. ACM, 2006. URL:
  6. Sam Blackshear, Evan Cheng, David L Dill, Victor Gao, Ben Maurer, Todd Nowacki, Alistair Pott, Shaz Qadeer, Dario Russi, Stephane Sezer, Tim Zakian, and Runtian Zhou. Move: A language with programmable resources. URL:
  7. Ting Chen, Zihao Li, Hao Zhou, Jiachi Chen, Xiapu Luo, Xiaoqi Li, and Xiaosong Zhang. Towards saving money in using smart contracts. In Proc. 40th ICSE-NIER, pages 81-84. ACM, 2018. URL:
  8. Leonardo De Moura and Nikolaj Bjørner. Z3: An efficient SMT solver. In Proc. 14th TACAS, volume 4963 of LNCS, pages 337-340. Springer, 2008. URL:
  9. Everett Hildenbrandt, Manasvi Saxena, Xiaoran Zhu, Nishant Rodrigues, Philip Daian, Dwight Guth, Brandon Moore, Yi Zhang, Daejun Park, Andrei Ştefănescu, and Grigore Roşu. KEVM: A complete semantics of the ethereum virtual machine. In Proc. 31st CSF, pages 204-217. IEEE, 2018. URL:
  10. Yoichi Hirai. Defining the Ethereum virtual machine for interactive theorem provers. In Financial Cryptography and Data Security, volume 10323 of LNCS, pages 520-535. Springer, 2017. URL:
  11. Abhinav Jangda and Greta Yorsh. Unbounded superoptimization. In Proc. Onward! 2017, pages 78-88. ACM, 2017. URL:
  12. Cynthia Kop. Higher Order Termination. PhD thesis, Vrije Universiteit, Amsterdam, 2012. Google Scholar
  13. Cynthia Kop and Naoki Nishida. Constrained term rewriting tool. In Proc. 20th LPAR, volume 9450 of LNCS, pages 549-557, 2015. URL:
  14. Daniel Kroening and Ofer Strichman. Decision Procedures: An Algorithmic Point of View. Springer, Berlin, 2008. URL:
  15. Nomadic Labs. Michelson: the language of smart contracts in Tezos. URL:
  16. Nuno P. Lopes, David Menendez, Santosh Nagarakatte, and John Regehr. Practical verification of peephole optimizations with Alive. Commun. ACM, 61(2):84-91, 2018. URL:
  17. Dominic P. Mulligan, Scott Owens, Kathryn E. Gray, Tom Ridge, and Peter Sewell. Lem: Reusable engineering of real-world semantics. In Proc. 19th ICFP, pages 175-188. ACM, 2014. URL:
  18. Julian Nagele, Bertram Felgenhauer, and Aart Middeldorp. CSI: New evidence - A progress report. In Proc. CADE-26, volume 10395 of LNAI, pages 385-397, 2017. URL:
  19. Julian Nagele and Maria A. Schett. Blockchain superoptimizer. In Preproc. 29th LOPSTR, pages 166-180, 2019. URL:
  20. Grigore Roşu and Traian Florin Şerbănuţă. An overview of the K semantic framework. Journal of Logic and Algebraic Programming, 79(6):397-434, 2010. URL:
  21. Sarah Winkler and Aart Middeldorp. Completion for logically constrained rewriting. In Proc. 3rd FSCD, volume 108 of LIPIcs, pages 30:1-30:18, 2018. URL:
  22. Gavin Wood. Ethereum: A secure decentralised generalised transaction ledger, 2018. Byzantium Version e94ebda, URL:
Questions / Remarks / Feedback

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail