Nice to Meet You: Synthesizing Practical MLIR Abstract Transformers

TL;DR

This paper introduces NiceToMeetYou, a synthesis framework that automatically generates sound and precise abstract transformers for compiler static analysis, improving upon existing LLVM transformers without requiring manual sketches.

Contribution

It presents a novel, fully automated synthesis technique for abstract transformers in MLIR, enhancing soundness and precision in compiler static analysis.

Findings

17% of synthesized transformers are more precise than LLVM's.

Transformers are verified via SMT lowering.

No sketches are required for synthesis.

Abstract

Static analyses play a fundamental role during compilation: they discover facts that are true in all executions of the code being compiled, and then these facts are used to justify optimizations and diagnostics. Each static analysis is based on a collection of abstract transformers that provide abstract semantics for the concrete instructions that make up a program. It can be challenging to implement abstract transformers that are sound, precise, and efficient, and in fact both LLVM and GCC have suffered from miscompilations caused by unsound abstract transformers. Moreover, even after more than 20 years of development, LLVM lacks abstract transformers for hundreds of instructions in its intermediate representation (IR). We developed NiceToMeetYou, a program synthesis framework for abstract transformers that are aimed at the kinds of non-relational integer abstract domains that are heavily used by today's production compilers. It exploits a simple but novel technique for breaking the synthesis problem into parts: each of our transformers is the meet of a collection of simpler, sound transformers that are synthesized such that each new piece fills a gap in the precision of the final transformer. Our design point is bulk automation: no sketches are required. Transformers are verified by lowering to a previously created SMT dialect of MLIR. Each of our synthesized transformers is provably sound and some (17 percent) are more precise than those provided by LLVM.