Integrating the EVM super-optimizer gasol into real-world compilers

Smart contracts are programs deployed and executed on the blockchain for a monetary fee paid in gas and thus smart contract compilers have a clear optimization target: gas usage. Because smart contracts are a young, fast-moving _eld for which (manually) _ne-tuned compilers have not yet been developed, they highly bene_t from automated and adaptable approaches. Moreover, smart contracts are e_ectively immutable, and as-such need a high-level of assurance, which makes them an ideal domain for applying formal methods to them. Super-Optimization is a technique, proposed by the formal methods community, which attempts to _nd the best translation of a block of instructions by trying all posible sequences of instructions that produce the same result. This work presents a framework for super-optimizing smart contracts based on Max- SMT with two main ingredients: 1. the extraction of a stack functional speci_cation from the basic blocks of a Smart contract, which is simpli_ed using rules that capture the semantics of arithmetic, bit-wise, and relational operations, and 2. the synthesis of optimized blocks, which by means of an e_cient SMT encoding, _nds the bytecode blocks with minimal gas cost whose stack functional speci_cation is equal (modulo commutativity) to the extracted one. This framework was already implemented in a tool called syrup 1.0, which only considered the necessary encodings to perform super-optimization. This Master Thesis presents an improved version of that tool, called gasol (GAS Optimization tooLkit), which includes more advanced encodings of the problem to speed up the process of super-optimization. Large-scale experiments have been performed to determine realistic settings for including gasol in an EVM compiler and investigate trade-o_s between quality of optimizations and required optimization time. Besides, veri_cation techniques have been developed to ensure the process is indeed correct. Our experimental results indicate these new encodings are useful, and by limiting the timeout of the tool, it is feasible to include gasol into an EVM compiler. In fact, GASOL project has been funded by the Ethereum Foundation and they are considering integrating this approach into following versions of the solc compiler. The main results in this project have been included as part of the article submitted to the ACM Transactions on Software Engineering and Methodology (TOSEM) for its publication