Xuanyu Peng | Searcharxiv

arXiv2025

Nice to Meet You: Synthesizing Practical MLIR Abstract Transformers

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.

cs.PL↗

arXiv2025

LOUD: Synthesizing Strongest and Weakest Specifications

This paper tackles the problem of synthesizing specifications for nondeterministic programs. For such programs, useful specifications can capture demonic properties, which hold for every nondeterministic execution, but also angelic properties, which hold for some nondeterministic execution. We build on top of a recently proposed a framework by Park et al. in which given (i) a quantifier-free query posed about a set of function definitions (i.e., the behavior for which we want to generate a specification), and (ii) a language L in which each extracted property is to be expressed (we call properties in the language L-properties), the goal is to synthesize a conjunction of L-properties such that each of the conjunct is a strongest L-consequence for the query: each property is an over-approximation of the query and there is no other L-property that over-approximates the query and is strictly more precise than each property. This framework does not apply to nondeterministic programs for two reasons: it does not support existential quantifiers in queries (which are necessary to expressing nondeterminism) and it can only compute L-consequences, i.e., it is unsuitable for capturing both angelic and demonic properties. This paper addresses these two limitations and presents a framework, LOUD, for synthesizing both strongest L-consequences and weakest L-implicants (i.e., under-approximations of the query) for queries that can involve existential quantifiers. We implement a solver, ASPIRE, for problems expressed in LOUD which can be used to describe and identify sources of bugs in both deterministic and nondeterministic programs, extract properties from concurrent programs, and synthesize winning strategies in two-player games.

cs.PL↗