Every compiler comes with a set of local optimization rules, such as
x + 0 → x
x & x → x
, that do not require any global analysis. These rules reflect the wisdom of the compiler developers about mathematical identities that hold for the operations of their intermediate representation. Unfortunately, these sets of hand-crafted rules guarantee neither correctness nor completeness.
solves this problem by generating
local optimizations up to a given cost limit. Since
verifies each rule using an SMT solver, it guarantees correctness and completeness of the generated rule set. Using
, we tested the latest versions of
and identified more than 50 missing local optimizations that involve only two operations.