Functional Compositions of Abstract Interpretations

In the context of standard abstract interpretation theory, we define and study a systematic operator of reduced relative power for composing functionally abstract domains. The reduced relative power of two abstract domains D1 (the exponent) and D2 (the base) consists in a suitably defined lattice of monotone functions from D1 to D2, called dependencies, and it is a generalization of the Cousot and Cousot operator of reduced (cardinal) power. The relationship between the reduced relative power and Nielson's tensor product is also investigated. The case of autodependencies (when base and exponent are the same domain) turns out to be particularly interesting: Under certain hypotheses, the domain of autodependencies corresponds to a suitable powerset-like completion of the base abstract domain, providing a compact lattice-theoretic representation for autodependencies. The usefulness of the reduced relative power is shown by a number of applications to abstract domains used both for program analysis and for semantics design. Notably, we prove that the domain Def for logic program ground-dependency analysis can be characterized as autodependencies of a standard more abstract domain representing plain groundness only, and we show how to exploit reduced relative power to systematically derive compositional logic program semantics.