Lifting Abstract Interpreters to Quantified Logical Domains
Abstract
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
universally 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 <= i < n) => 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.