Combining Abstract Interpreters
Abstract
We present a methodology for automatically combining abstract
interpreters over given lattices to construct an abstract interpreter
for the combination of those lattices. This lends modularity to the
process of design and implementation of abstract interpreters.
We define the notion of logical product of lattices. This kind of
combination is more precise than the reduced product combination.
We give algorithms to obtain the join operator and the
existential quantification operator for the combined lattice from the
corresponding operators of the individual lattices. We also give a
bound on the number of steps required to reach a fixed point across
loops during analysis over the combined lattice in terms of the
corresponding bounds for the individual lattices.
We prove that our combination methodology
yields the most precise abstract interpretation operators over the
logical product of lattices when the individual lattices are over
theories that are convex, stably infinite, and disjoint.
We also present an interesting
application of logical product wherein some lattices can be reduced to
combination of simpler (unrelated) lattices.