License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/OASIcs.FMBC.2020.3
URN: urn:nbn:de:0030-drops-134169
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2020/13416/
Go to the corresponding OASIcs Volume Portal

Schett, Maria A. ; Nagele, Julian

Populating the Peephole Optimizer of a Smart Contract Compiler

pdf-format:
OASIcs-FMBC-2020-3.pdf (0.6 MB)

Abstract

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.

BibTeX - Entry

@InProceedings{schett_et_al:OASIcs:2020:13416,
  author =	{Maria A. Schett and Julian Nagele},
  title =	{{Populating the Peephole Optimizer of a Smart Contract Compiler}},
  booktitle =	{2nd Workshop on Formal Methods for Blockchains (FMBC 2020)},
  pages =	{3:1--3:15},
  series =	{OpenAccess Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-169-6},
  ISSN =	{2190-6807},
  year =	{2020},
  volume =	{84},
  editor =	{Bruno Bernardo and Diego Marmsoler},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2020/13416},
  URN =		{urn:nbn:de:0030-drops-134169},
  doi =		{10.4230/OASIcs.FMBC.2020.3},
  annote =	{Keywords: Compiler Optimizations, Constraint Solving, Ethereum Bytecode}
}

Keywords: Compiler Optimizations, Constraint Solving, Ethereum Bytecode
Collection: 2nd Workshop on Formal Methods for Blockchains (FMBC 2020)
Issue Date: 2020
Date of publication: 11.12.2020
Supplementary Material: https://github.com/mariaschett/ppltr

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI