Denali: A practical algorithm for generating optimal code

Abstract

This article presents a design for the Denali-2 superoptimizer, which will generate minimum-instruction-length machine code for realistic machine architectures using automatic theorem-proving technology: specifically, using E-graph matching (a technique for pattern matching in the presence of equality information) and Boolean satisfiability solving.This article presents a precise definition of the underlying automatic programming problem solved by the Denali-2 superoptimizer. It sketches the E-graph matching phase and presents a detailed exposition and proof of soundness of the reduction of the automatic programming problem to the Boolean satisfiability problem.