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 %) are more precise than those provided by LLVM.

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 spyro framework 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 ℒ in which each extracted property is to be expressed (we call properties in the language ℒ-properties), the goal is to synthesize a conjunction ∧ 𝑖 𝜑 𝑖 of ℒ-properties such that each of the 𝜑 𝑖 is a strongest ℒ -consequence for Ψ: 𝜑 𝑖 is an overapproximation of Ψ and there is no other ℒ-property that over-approximates Ψ and is strictly more precise than 𝜑 𝑖 . 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 ℒ-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 ℒ -consequences and weakest ℒ -implicants (i.e., under-approximations of the query Ψ) for queries that can involve existential quantifiers . We devise algorithms for handling the quantifiers appearing in loud queries and implement them in 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.

In this paper, we propose an automated approach to finding correct and efficient memoization algorithms from a given declarative specification. This problem has two major challenges: (i) a memoization algorithm is too large to be handled by conventional program synthesizers; (ii) we need to guarantee the efficiency of the memoization algorithm. To address this challenge, we structure the synthesis of memoization algorithms by introducing the local objective function and the memoization partition function and reduce the synthesis task to two smaller independent program synthesis tasks. Moreover, the number of distinct outputs of the function synthesized in the second synthesis task also decides the efficiency of the synthesized memoization algorithm, and we only need to minimize the number of different output values of the synthesized function. However, the generated synthesis task is still too complex for existing synthesizers. Thus, we propose a novel synthesis algorithm that combines the deductive and inductive methods to solve these tasks. To evaluate our algorithm, we collect 42 real-world benchmarks from Leetcode, the National Olympiad in Informatics in Provinces-Junior (a national-wide algorithmic programming contest in China), and previous approaches. Our approach successfully synhesizes 39/42 problems in a reasonable time, outperforming the baselines.