Lifting Abstract Interpreters to Quantified Logical Domains

Today, abstract interpretation is capable of inferring a wide variety of quantifier-free program invariants. In this paper, we describe a general technique for building powerful quantified abstract domains that leverage existing quantifier-free domains. For example, from a domain that abstracts facts like “a[1] = 0”, we automatically construct a domain that can represent universally quantified facts like “Forall i: (0 A[i]=0)”. The principal challenge in building such a domain is that, while most domains supply over-approximations of operations like join, meet, and variable elimination, working with the guards of quantified facts requires under-approximation. A crucial component of our approach is an automatic technique to convert the standard over-approximation operations provided with all domains into sound under-approximations. The correctness of our abstract interpreters is established by identifying two lattices–one that establishes the soundness of the abstract interpreter and another that defines its precision, or completeness. Despite the computational intractability of inferring quantified facts in general, we prove that the analyses we generate are complete relative to a very natural partial order. Using our generic construction, we build a number of abstract interpreters on top of domains for linear arithmetic, uninterpreted function symbols (used to model heap accesses), and pointer reachability. Our experiments on a variety of programs using arrays and pointers (including several sorting algorithms) demonstrate the feasibility of the approach on challenging examples.