RT Conference Proceedings
T1 A Max-SMT Superoptimizer for EVM handling Memory and Storage
A1 Albert Albiol, Elvira María
A1 Gordillo Alguacil, Pablo
A1 Hernández-Cerezo, Alejandro
A1 Rubio, Albert
AB Superoptimization is a compilation technique that searches for the optimal sequence of instructions semantically equivalent to a given (loop-free) initial sequence. With the advent of SMT solvers, it has been successfully applied to LLVM code (to reduce the number of instructions) and to Ethereum EVM bytecode (to reduce its gas consumption). Both applications, when proven practical, have left out memory operations and thus missed important optimization opportunities. A main challenge to superoptimization today is handling memory operations while remaining scalable. We present GASOLv2 , a gas and bytes-size superoptimization tool for Ethereum smart contracts, that leverages a previous Max-SMT approach for only stack optimization to optimize also wrt. memory and storage. GASOLv2 can be used to optimize the size in bytes, aligned with the optimization criterion used by the Solidity compiler solc, and it can also be used to optimize gas consumption. Our experiments on 12,378 blocks from 30 randomly selected real contracts achieve gains of 16.42% in gas wrt. the previous version of the optimizer without memory handling.
SN 9783030995232
SN 9783030995249
SN 0302-9743
SN 1611-3349
YR 2022
FD 2022-03-30
LK https://hdl.handle.net/20.500.14352/96667
UL https://hdl.handle.net/20.500.14352/96667
LA eng
DS Docta Complutense
RD 7 abr 2025