Superoptimization of WebAssembly Process Graphs

Abstract

The time needed for program execution is rarely minimal. Often, a faster program exists that produces the same output. Our superoptimizer aims to reduce the execution time of WebAssembly programs significantly. We propagate symbolic information over control flow, partially evaluate expressions and branch conditions using the Z3 SMT solver, synthesize alternate fragments for some small loops, and apply small structural changes to loops with low bounds. In particular, our approach of propagating symbolic information over control flow and driving loops with symbolic information is novel for superoptimization. Loop driving and synthesis make small artificial programs several orders of magnitude faster. On large programs, only partial evaluation already requires multiple hours of optimization time while finding only marginal (~1%) improvements. While the complete approach shows some potential, its application to large programs is currently infeasible, as it may require months of superoptimization time.