Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Nice to Meet You: Synthesizing Practical MLIR Abstract Transformers

Xuanyu Peng, Dominic Kennedy, Yuyou Fan, Ben Greenman, John Regehr, Loris D'Antoni

TL;DR

The paper tackles the challenge of building sound, precise abstract transformers for compiler analyses by introducing NiceToMeetYou, a drop-in synthesis framework that automatically generates transformers for finite non-relational integer domains. It leverages MLIR/SMT-backed semantics, a meet-based composition of smaller transformers, and an MCMC-driven search that does not require sketches. Through a case study on urem in the KnownBits domain, it demonstrates recovery of LLVM heuristics and discovery of new, sound heuristics, with transformers that can outperform or complement hand-written LLVM ones when combined via meet. The evaluation shows broad applicability across KnownBits and ConstantRange, with parallelization and JIT acceleration enabling scalable synthesis, and highlights the practical impact of DSL choice and abductive refinement on precision. The work argues for a practical, automation-friendly path to expanding transformer coverage in real compilers, reducing manual engineering effort while improving analysis precision and reliability.

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.

Nice to Meet You: Synthesizing Practical MLIR Abstract Transformers

TL;DR

The paper tackles the challenge of building sound, precise abstract transformers for compiler analyses by introducing NiceToMeetYou, a drop-in synthesis framework that automatically generates transformers for finite non-relational integer domains. It leverages MLIR/SMT-backed semantics, a meet-based composition of smaller transformers, and an MCMC-driven search that does not require sketches. Through a case study on urem in the KnownBits domain, it demonstrates recovery of LLVM heuristics and discovery of new, sound heuristics, with transformers that can outperform or complement hand-written LLVM ones when combined via meet. The evaluation shows broad applicability across KnownBits and ConstantRange, with parallelization and JIT acceleration enabling scalable synthesis, and highlights the practical impact of DSL choice and abductive refinement on precision. The work argues for a practical, automation-friendly path to expanding transformer coverage in real compilers, reducing manual engineering effort while improving analysis precision and reliability.

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.

Paper Structure

This paper contains 56 sections, 2 theorems, 10 equations, 5 figures, 8 tables, 4 algorithms.

Table of Contents

  1. Introduction
  2. Pattern 1: Splitting the input space
  3. Pattern 2: Separate transformers for separate jobs
  4. Implementation in MLIR
  5. Evaluation
  6. Contributions
  7. Problem Definition and Overview of the Approach
  8. The Transformer Synthesis Problem
  9. Norms vs. Metrics
  10. Problem Definition
  11. Case Study: Synthesizing a Precise Transformer for urem
  12. Background: The KnownBits Domain and the urem Operator
  13. Reference Implementation: LLVM's Hand-Written Transformer
  14. Synthesized Transformer in MLIR: Matching and Extending LLVM
  15. An Ideal Algorithm for the Transformer Synthesis Problem
  16. ...and 41 more sections

Key Result

theorem 1

If SynthesizeTransformer synthesizes a single sound transformer that is a solution to eq:one-best-condition and there exists a finite solution to the transformer synthesis problem, then alg:idealized-algo returns a solution to the transformer synthesis problem.

Figures (5)

  • Figure 1: Input and output for the transformer synthesis problem on a toy example.
  • Figure 2: The KnownBits transformers for urem operator in LLVM
  • Figure 3: Our synthesized KnownBits transformers for urem, written in MLIR.
  • Figure 4: Implementation overview. The outer loop (above) checks the soundness of promising candidates. The inner loop (below) generates new candidates via mutation and evaluates candidates' soundness and precision.
  • Figure 5: Optimal transformers

Theorems & Definitions (5)

  • Definition 2.1: Meet of Transformers
  • Definition 2.2: Soundness of Transformers
  • Definition 2.3: Transformer Synthesis Problem
  • theorem 1: Soundness
  • corollary 1: Asymptotic Optimality of MCMC Search