Nice to Meet You: Synthesizing Practical MLIR Abstract Transformers

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 some instructions in its intermediate representation (IR).

We developed NiceToMeetYou: a program synthesis framework for abstract transformers that are aimed at the kind 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, and formal semantics for IR instructions were previously created using an SMT dialect of MLIR. Each of our synthesized transformers is provably sound, and some of them are more precise than those provided by LLVM

Xuanyu Peng

I’m DOFY, a PhD student in computer science at UCSD