Programmable tool helps build and improve compiler rewrite rules
Equality saturation theory exploration `a la carte
Programming Languages
Summary
Making computers run programs faster or prove program properties often needs rules to rewrite code in smarter ways, but creating these rules is hard. The authors designed Enumo, a new language that helps users write and improve these rules step by step, combining automated help and human guidance. Enumo can handle more complex rules and bigger programming languages than older tools, even using large language models to assist. Their approach can produce rules as good as ones made by hand in some cases and works faster without checking code outcomes directly.
What this means in practice
- •For compiler developers: Generate and refine sets of rewrite rules to improve program optimization and verification automatically and incrementally.
- •For software verification engineers: Automatically infer transformation rules for symbolic programs to enhance correctness checking without manual rule crafting.
Authors
Anjali Pal, Brett Saiki, Ryan Tjoa, Cynthia Richey, Amy Zhu, Oliver Flatt, Max Willsey, Zachary Tatlock, Chandrakana Nandi
Abstract
Rewrite rules are critical in equality saturation, an increasingly popular technique in optimizing compilers, synthesizers, and verifiers. Unfortunately, developing high-quality rulesets is difficult and error-prone. Recent work to automatically infer rewrite rules does not scale to large terms or grammars. Users struggle to guide inference and incrementally construct rulesets because existing rule inference tools are monolithic and opaque. As a result, most equality saturation users still manually develop and maintain rulesets. This paper proposes Enumo, a new domain-specific language for programmable theory exploration. Enumo provides a small set of core operators that enable users to strategically guide rule inference and incrementally build rulesets. Short Enumo programs easily replicate results from state-of-the-art tools like Ruler, but Enumo programs can also scale to infer deeper rules from larger grammars than prior approaches. Enumo's composable operators even facilitate developing new strategies for ruleset inference. We introduce a new fast-forwarding strategy which does not require evaluating terms in the target language, and thus supports domains that were out of scope for prior work. Enumo is also easy to extend: two new operators suffice to incorporate large language models into rule inference, where they complement guided search. We evaluate Enumo and fast-forwarding across a variety of domains. Compared to state-of-the-art techniques, Enumo can synthesize better rulesets over a diverse set of domains, in some cases matching the effects of manually developed rulesets in systems driven by equality saturation.