Refining and Compressing Abstract Domains

Roberto Giacobazzi^{⋆} Francesco Ranzato^{⋆⋆}

⋆Dipartimento di Informatica, Università di Pisa Corso Italia 40, 56125 Pisa, Italy

                            giaco@di.unipi.it

⋆⋆Dipartimento di Matematica Pura ed Applicata, Università di Padova Via Belzoni 7, 35131 Padova, Italy

                           franz@math.unipd.it

Abstract. In the context of Cousot and Cousot’s abstract interpretation theory, we present a general framework to define, study and handle operators modifying abstract domains. In particular, we introduce the notions of operators of refinement and compression of abstract domains: A refinement enhances the precision of an abstract domain; a compression operator (compressor) can exist relatively to a given refinement, and it simplifies as much as possible a domain of input for that refinement. The adequateness of our framework is shown by the fact that most of the existing operators on abstract domains fall in it. A precise relationship of adjunction between refinements and compressors is also given, justifying why compressors can be understood as inverses of refinements.

1 Introduction

It is well known that abstract domains play a fundamental rôle in abstract interpretation [5, 6], since the precision of an abstract interpretation-based program analysis strongly depends on the expressive power of the chosen abstract domain. Much work has been therefore devoted to define systematic operators for enhancing the precision of representation of abstract domains. Relevant examples are Cousot and Cousot’s reduced product, disjunctive completion and reduced cardinal power [6], Nielson’s tensor product [18], Giacobazzi and Ranzato’s dependencies and dual-Moore-set completion [13], the open product and pattern completion of Cortesi et al. [4], to cite the most known ones. The basic idea is that richer abstract domains can be obtained by combining simpler ones or by lifting them by adding new information. These operators on abstract domains provide high level facilities to tune the analysis in accuracy and cost, and some of them have been included as tools for abstract domain design aid in modern systems for program analysis, like for instance in System Z [22] and in PLAI [1].

We carry on this idea of operators enhancing the precision of abstract domains and we present in Sect. 3 a general and precise framework to handle these operators, which encompasses and improves the ideas sketched in [9]. The central notion is that of abstract domain refinement, that intuitively is any operator performing an action of refinement on abstract domains, with respect to their standard ordering relation of precision. There exists a strong link between refinements and closure operators, and many lattice-theoretic properties of closures are inherited by refinements. We introduce a generic pattern of definition for domain refinements, which allows to recover most of the important refinements listed above. Moreover, as an instance of this scheme, we present a new refinement of completeness. Roughly speaking, an abstract domain D is complete for a semantic function f defined on the concrete domain when no loss of precision is introduced by approximating f in the best possible way (i.e. by considering its best correct approximation, cf. [5, 6]) with respect to D. Thus, for a domain D, our refinement of completeness provides the most abstract domain which is more precise than D and complete for a given continuous concrete semantic function.

Recently, also operators of simplification of abstract domains have been defined and studied, like the operations of complementation in [3] and least disjunctive basis in [14]. As well as refinements, we show in Sect. 4 that these operators can be expressed in a formal and precise way in our framework. Actually, these operators are instances of our notion of operator of compression (or compressor). Roughly speaking, for a given abstract domain refinement ℜ, its relative compressor simplifies a domain D of input for ℜ, by returning the domain (if this exists) which contains the least amount of information required as input by ℜ to reach the same enhancement obtainable from D. This is somehow similar to the operation of compression on files – hence our terminology. In more precise terms, if ℜ is a unary refinement and D is an abstract domain, then an abstract domain A is the optimal basis of D for ℜ, if A is the most abstract solution to the equation ℜ(X ) = ℜ(D). Obviously, if an optimal basis exists then it is necessarily unique. We say that ℜ is invertible on a given class of abstract domains if there exists the optimal basis of any domain D in the class. In this case, the compressor ℜ^{−} relative to ℜ (also called the inverse of ℜ) provides the optimal basis ℜ^{−}(D) of D for ℜ. The problem of inverting a refinement is often hard to solve in a satisfactory way, and, in general, not all domain refinements admit a corresponding compressor defined for a significant class of abstract domains. We show that complementation and least disjunctive basis give rise, respectively, to the compressors relative to reduced product and disjunctive completion refinements, and we give a generic scheme for defining invertible refinements. Moreover, we show that invertible refinements provide solutions to the problem of decomposing abstract domains into simpler factors. If ℜ is an n-ary refinement and D = ℜ(D_{1}, …, D_{n}), then the tuple ⟨D_{1}, …, D_{n}⟩ can be considered as a decomposition of D relative to ℜ. We then present a general iterative method which starting from any decomposition relative to an invertible refinement provides minimal decompositions, i.e. decompositions involving the most abstract factors.

It is important to note that our notion of inversion of a refinement does not correspond to the more customary inversion in the sense of adjunctions – on the contrary, we observe that, in general, this is not possible. However, we show in Sect. 5 that this asymmetry can be overcome by considering a modified ordering relation between abstract domains, that is induced in a natural way by the refinement itself. We prove that for this lifted order on abstract domains, an invertible refinement and its compressor do constitute an adjunction. This provides a firm mathematical relationship between refinements and compressors, and gives a more precise justification to the use of the term “inverse”.

2 Preliminaries The structure ⟨uco(C ), ⊑, ⊔, ⊓, λx.⊤, λx.x⟩ denotes the complete lattice of all upper closure operators (shortly closures) on a complete lattice ⟨C , ≤, ∨, ∧, ⊤, ⊥⟩, where ρ ⊑ η iff ∀x ∈ C . ρ(x) ≤ η(x). The complete lattice of all lower closure operators on C is denoted by lco(C ) and is dual-isomorphic to uco(C ). Recall that each closure operator ρ ∈ uco(C ) is uniquely determined by the set of its fixpoints, which is its image, i.e. ρ(C ) = {x ∈ C | ρ(x) = x}, that ρ ⊑ η iff η(C ) ⊆ ρ(C ), and that a subset X ⊆ C is the set of fixpoints of a closure iff X = {∧Y | Y ⊆ X } (note that ⊤ ∈ X ). ⟨ρ(C ), ≤⟩ is a complete meet subsemilattice of C but, in general, it is not a complete sublattice of C .

In the standard Cousot and Cousot abstract interpretation theory, abstract domains can be equivalently specified either by Galois connections or by closure operators [6]. In the first case, concrete and abstract domains are related by a pair of adjoint functions. This provides a way to relate domains containing objects having different representation. In the second case instead, an abstract domain is specified as (the set of fixpoints of) an upper closure on the concrete domain. Thus, the closure operator approach is particularly convenient when reasoning about properties of abstract domains independently from the representation of their objects, as in our case. Hence, we will identify uco(C ) with the complete lattice of all possible abstract domains of the concrete domain (i.e. any complete lattice) C . The ordering on uco(C ) corresponds precisely to the standard order used in abstract interpretation to compare abstract domains with regard to their precision: D_{1} is more precise than D_{2} iff D_{1} ⊑ D_{2} in uco(C ) (⊏ denotes strict ordering). The lub and glb on uco(C ) have therefore the following meaning as operators on domains. Suppose {D_{i}}_{i∈I} ⊆ uco(C ): (i) ⊔_{i∈I} D_{i} is the most concrete among the domains which are abstractions of all the D_{i}’s, i.e. it is their least common abstraction; (ii) ⊓_{i∈I} D_{i} is (isomorphic to) the well-known reduced product of all the D_{i}’s, and, equivalently, it is the most abstract among the domains (abstracting C ) which are more concrete than every D_{i}. Whenever C is a meet-continuous complete lattice (i.e., for any chain Y ⊆ C and x ∈ C : x ∧ (∨Y ) = ∨_{y∈Y} (x ∧ y)), uco(C ) enjoys the lattice-theoretic property of pseudocomplementedness (cf. [12]). This property allowed to define the operation of complementation of abstract domains (cf. [3]), namely an operation which, starting from any two domains C ⊑ D, where C is meet-continuous, gives as result the most abstract domain C ∼D, such that (C ∼D) ⊓ D = C .

3 Abstract Domain Refinements Intuitively, an abstract domain refinement is an operator that, for any tuple ⟨D_{i}⟩_{1≤i≤n} of domains of input (ranging on a given domain of definition), provides as output a domain more precise than each D_{i}. It is also very reasonable to expect that such an operator is monotone. These observations naturally lead to the definition below. In the following, a generic tuple of objects is denoted by O, π_{i}(O) denotes its i-th component, and O[X /i] denotes the tuple obtained from O by replacing π_{i}(O) with X . Also, C is a complete lattice acting as the concrete domain and U ⊆ uco(C )^{n}, n ≥ 1, is a given tuple of sets of domains abstracting C (for simplicity, we only consider refinements of finite arity – actually those having a practical meaning – although a generalization would be straightforward). When n = 1 we denote U as the set U ⊆ uco(C ). We extend on tuples the glb of uco(C ): For any tuple of domains D, ⊓D = ⊓_{1≤i≤n}π_{i}(D). Definition 3.1 A map ℜ : U → uco(C ) is a (n-ary abstract domain) refinement if: (i) ℜ is monotone; (ii) ℜ is reductive: ∀D ∈ U. ℜ(D) ⊑ ⊓D. □

The kernel of definition of any refinement ℜ : U → uco(C ) is given by IKU = ∩_{1≤i≤n}π_{i}(U). Often, refinements are defined on any tuple of abstract domains, i.e., ℜ : uco(C )^{n} → uco(C ), as in the case of reduced product and disjunctive completion, later considered. We will call them full refinements, in order to distinguish them from generic ones as allowed by Definition 3.1. Any n-ary refinement ℜ : U → uco(C ) induces a family of refinements of lower arity obtained by fixing some of the domains of input. For instance, by fixing n − 1 domains, we get the unary refinements λX .ℜ(D[X /i]) : π_{i}(U) → uco(C ). Also, ℜ induces the canonical unary self-refinement ℜ_{1l} : IKU → uco(C ) defined as ℜ_{1l}(D) = ℜ(D, ..., D). Conversely, any n-uple R = ⟨ℜ_{i}⟩_{1≤i≤n} of unary refinements ℜ_{i} : U_{i} → uco(C ) induces an n-ary refinement ℜR : U_{1}×...×U_{n} → uco(C ) defined as ℜR(D) = ⊓_{1≤i≤n}ℜ_{i}(π_{i}(D)), and called attribute independent.

It is important to remark that Definition 3.1 lacks of any requirement of idempotence. For instance, for a unary refinement ℜ : U → uco(C ) may well happen that a refined domain ℜ(D) ∈ U can still be object of further refinement, i.e. ℜ(ℜ(D)) ⊏ ℜ(D). Due to lack of space, in the paper we will only consider examples of idempotent refinements, although a relevant example of nonidempotent refinement can be given by the dependencies between abstract domains of [13]. However, it is worth noting that, by monotonicity, any refinement can be lifted to an idempotent one as the limit of a possibly transfinite Kleene fixpoint iteration sequence. It is therefore reasonable requiring idempotence for refinements, i.e. that a refinement upgrades abstract domains all at once. Definition 3.2 An n-ary refinement ℜ : U → uco(C ) is idempotent if for any i ∈ [1, n] and D ∈ U such that ℜ(D) ∈ IKU, ℜ(D) = ℜ(D[ℜ(D)/i]). □ Proposition 3.3 For any ℜ : U → uco(C ), the following are equivalent:

(a) ℜ is idempotent;

(b) For any D ∈ U such that ℜ(D) ∈ IKU, ℜ(D) = ℜ_{1l}(ℜ(D)). If IKU is a (finitely) meet subsemilattice of uco(C ) then (a) is equivalent to:

(c) ℜ_{1l} is idempotent and for any D∈U such that ℜ(D)∈IKU, ℜ(D) = ℜ_{1l}(⊓D). The following example yields a generic and useful pattern of definition for

full idempotent refinements. Example 3.4 Consider any property P of abstract domains, i.e. a subset of the lattice of abstract interpretations P ⊆ uco(C ). For any fixed n ∈ IN, define the operator ℜ_{P} : uco(C )^{n} → uco(C ) as ℜ_{P} = λD. ⊔ {A ∈ uco(C ) | A ∈ P, A ⊑ ⊓D}. Thus, ℜ_{P}(D) is the least common abstraction of all domains that satisfy P and are more concrete (viz. precise) than every π_{i}(D) for i ∈ [1, n]. It is immediate to observe that ℜ_{P} is monotone and reductive. Also, it is easily seen that ℜ_{P} satisfies the condition (c) of Proposition 3.3. Thus, ℜ_{P} always defines a full idempotent refinement. However, in general, ℜ_{P}(D) may not satisfy P. On the other hand, the following characterization holds.

Proposition 3.5 ∀D. ℜ_{P}(D) ∈ P ⇔ P ∈ lco(uco(C )) ⇒ ℜ_{P} = λD.P(⊓D).

Thus, for a property P which is a lower closure, ℜ_{P}(D) is the most abstract domain which satisfies P and is more concrete than every π_{i}(D), or, equivalently, ℜ_{P}(D) is the least extension of ⊓D that satisfies P. It is also worth noting that ℜ_{P}(D) is the greatest fixpoint of the equation X = P(X ) ⊓ (⊓D) in uco(C ). □

Note that any unary idempotent refinement ℜ : U → uco(C ) such that ℜ(U ) ⊆ U (we say in this case that ℜ is well-defined on U ) actually is a lower closure operator on the poset ⟨U , ⊑⟩, with the order inherited from uco(C ), i.e. ℜ ∈ lco(U ). In particular, any unary full idempotent refinement ℜ is a lower closure on uco(C ), i.e. ℜ ∈ lco(uco(C )), a case already considered in [9]. Also, for any n-ary full idempotent refinement ℜ : uco(C )^{n} → uco(C ), we have that any unary refinement λX .ℜ(D[X /i]) (i ∈ [1, n]) induced by ℜ is a lower closure operator on uco(C ), as well as the self-refinement ℜ_{1l}. It would be straightforward, although notationally tedious, to generalize this latter observation to generic n-ary (possibly nonfull) idempotent refinements that satisfy a suitably generalized condition of well-definedness. These observations are fairly important, since unary idempotent refinements inherit all the lattice-theoretic properties of lower closures (see [23] for a few of them). For instance, whenever the domain of definition ⟨U , ⊑⟩ is a complete lattice, we get that these refinements well-defined on U form a complete lattice ⟨lco(U ), ⊑⟩ (by a slight abuse of notation, we always use the ordering symbol ⊑ for any kind of closures), where ℜ_{1} ⊑ ℜ_{2} iff for any A ∈ U , ℜ_{1}(A) ⊑ ℜ_{2}(A) iff the set of abstract domains refined by ℜ_{1} is contained in the set of those refined by ℜ_{2}. Thus, analogously to the case of abstract domains, the complete ordering ⊑ between idempotent refinements can be interpreted as a relation of precision among refinement operators, where ℜ_{1} is more precise than ℜ_{2} iff ℜ_{1} ⊑ ℜ_{2}. Moreover, any unary idempotent refinement well-defined on a complete subsemilattice U of uco(C ) enjoys the following properties of compositionality w.r.t. the reduced product and least common abstraction.

Proposition 3.6 If U is a complete meet (join) subsemilattice of uco(C ), ℜ : U → U is an idempotent refinement, and {D_{i}}_{i∈I} ⊆ ℘(U ), then ℜ(⊓_{i∈I} D_{i}) = ℜ(⊓_{i∈I} ℜ(D_{i})) (ℜ(⊔_{i∈I} ℜ(D_{i})) = ⊔_{i∈I} ℜ(D_{i})).

Reduced Product Refinement. The simplest and probably most familiar example of abstract domain refinement is the reduced product [6], which is the glb in the lattice of abstractions. For simplicity, we consider it as a binary refinement. For any fixed concrete domain C (i.e., any complete lattice), reduced product is obviously an idempotent full refinement ℜ_{⊓} : uco(C )×uco(C ) → uco(C ). Thus, the unary refinement induced by ℜ_{⊓}, i.e. λX . A ⊓ X is a lower closure, and for it the properties discussed above hold. It is worth noting that ℜ_{⊓} is the simplest instance of the family of refinements defined in Example 3.4, since ℜ_{⊓} is ℜ_{P} for the trivial property P = uco(C ). Also, ℜ_{⊓} is the attribute independent combination of the trivial identity refinements. Reduced product has been successfully applied as a domain refinement in program analysis e.g. in [1, 16, 21]. Disjunctive Completion Refinement. The disjunctive completion [6] enhances an abstract domain so that its disjunction operation (i.e. lub) becomes precise (as that of the concrete domain). Abstract domains with a precise disjunction (also called disjunctive abstract domains) correspond to additive closure operators. Disjunctive completion can be given as an instance of the general scheme of Example 3.4, where the property P is given by additivity: P = uco^{a}(C ), the subset of uco(C ) of additive closures. Hence, the disjunctive completion ℜ_{∨} : uco(C ) → uco(C ) is defined as ℜ_{∨}(D) = ⊔{A ∈ uco^{a}(C ) | A ⊑ D}. Thus, ℜ_{∨} is an idempotent full refinement. It is easy to observe that uco^{a}(C ) defines a lower closure on uco(C ). Then, by Proposition 3.5, ℜ_{∨}(D) is the most abstract disjunctive domain that is more concrete than D. The disjunctive completion refinement has been applied in program analysis e.g. in [8, 15, 10].

Negative Completion Refinement. Assume the concrete domain C be a complete Boolean algebra. It is easy to verify that if ρ ∈ uco^{a}(C ) then ¬ρ = {¬x ∈ C | x ∈ ρ} ∈ uco^{a}(C ). The negative completion refinement is then defined on disjunctive abstract domains, ℜ_{¬} : uco^{a}(C ) → uco(C ), as follows: ℜ_{¬}(A) = A ⊓ ¬A. Thus, ℜ_{¬} lifts a given disjunctive abstract domain A to the reduced product of A with its negative abstract domain, namely to the most abstract domain containing both A and ¬A. It is now simple to check that ℜ_{¬} : uco^{a}(C ) → uco(C ) is an idempotent refinement. It is worth noting that, in general, ℜ_{¬}(A) may not be disjunctive (i.e., ℜ_{¬} is not well-defined on uco^{a}(C )).

The Refinement of Completeness. Abstract interpretation is intended to create sound approximations of the concrete semantics of programs. If the program semantics is specified as the least fixpoint of a monotone semantic operation f : C → C on a complete lattice C , then, in the closure operator approach, the soundness criterion for an abstract domain given by ρ ∈ uco(C ) and for an abstract monotone semantic operation f^{♯} : ρ(C ) → ρ(C ), is ∀c ∈ C . ρ(f (c)) ≤ f^{♯}(ρ(c)). This ensures the global soundness of the abstract semantics, i.e. ρ(lfp(f )) ≤ lfp(f^{♯}) (cf. [5]). Completeness is the dual relation ∀c ∈ C . f^{♯}(ρ(c)) ≤ ρ(f (c)). Because soundness is always required in abstract interpretation, in the following we abuse terminology and say that f^{♯} is complete for f if ρ ∘ f = f^{♯} ∘ ρ. In this case ρ(lfp(f )) = lfp(f^{♯}). Completeness in abstract interpretation is a quite rare ideal situation, where for a given abstract domain no loss of precision is introduced by abstract semantic operations. Completeness is especially recurrent between (concrete) semantics of programming languages (cf. [2, 7, 11]). Issues of completeness and related notions have also been studied in [17, 19, 20]. Completeness can be made a property of abstract domains, by making this notion independent on the choice for f^{♯}. Recall that the best correct approximation of f w.r.t. ρ is given by ρ ∘ f : ρ(C ) → ρ(C ). Thus, we consider completeness of the best correct approximation: ρ ∈ uco(C ) is complete for f if ρ ∘ f = ρ ∘ f ∘ ρ. For example, let us consider the canonical 4-point abstract domain Sign = {∅, ZZ_{<0}, ZZ_{>0}, ZZ}, which is an obvious abstraction of ⟨℘(ZZ), ⊆⟩. It is simple to show that Sign is complete for the monotone operation of integer multiplication λX .n ·X : ℘(ZZ) → ℘(ZZ) (where n ∈ ZZ and n ·X = {n ·m | m ∈ X }). On the other hand, ρ = {ZZ_{>0}, ZZ} (with Sign ⊑ ρ) is not complete for λX . n · X with n < 0: In fact, e.g., ρ(n · {−3}) = ZZ_{>0}, but, because ρ({−3}) = ZZ, ρ(n · ρ({−3})) = ρ(ZZ) = ZZ. The property of completeness for a semantic function f is therefore given by Γ(f ) = {ρ ∈ uco(C ) | ρ∘f = ρ∘f ∘ρ}. Following the scheme of Example 3.4, we can define an idempotent full refinement of completeness ℜ_{Γ(f )} : uco(C ) → uco(C ) as ℜ_{Γ(f )}(ρ) = ⊔{η ∈ uco(C ) | η ∈ Γ(f ), η ⊑ ρ}.

Theorem 3.7 If f is continuous then Γ(f ) ∈ lco(uco(C )).

Thus, by Proposition 3.5, we have that for a continuous f , ℜ_{Γ(f )}(D) actually is the (unique) most abstract domain which includes D and is complete for f . For instance, it is possible to check that for n < 0, ℜ_{Γ(λX .n·X )}({ZZ_{>0}, ZZ}) = Sign.

4 Abstract Domain Compressors

We have introduced the notion of abstract domain refinement as a formalization (and generalization) of many existing operators devoted to enhance the expressiveness of abstract domains. However, no operator performing a dual action of simplification on abstract domains has been proposed up till now. We now formalize the idea of a simplifying operator that gives as input to a fixed refinement the simplest domains (i.e. most abstract) which can be object of that refinement. Let ℜ : U → uco(C ) be a (possibly nonidempotent) refinement. Define ℜ_{k}^{−} : U → uco(C ), k ∈ [1, n], as ℜ_{k}^{−} = λD.⊔{A ∈ π_{k}(U) | ℜ(D[A/k]) = ℜ(D)}. For D ∈ U, ℜ_{k}^{−}(D) is the least common abstraction of all domains in π_{k}(U) that, when substituted to π_{k}(D) as k-th input for ℜ, do not change the output.

Definition 4.1 ℜ_{k}^{−}(D) is the k-th optimal basis of D ∈ U for ℜ if ℜ_{k}^{−}(D) ∈ π_{k}(U) and ℜ(D) = ℜ(D[ℜ_{k}^{−}(D)/k]). The refinement ℜ is k-invertible (or admits the k-th inverse) on V ⊆ π_{k}(U) if for all D ∈ U[V /k], ℜ_{k}^{−}(D) is the k-th optimal basis of D for ℜ. When ℜ is k-invertible, the map ℜ_{k}^{−} : U[V /k] → π_{k}(U) is called the k-th compressor for ℜ. □

Note that if the domain of definition V ⊆ π_{k}(U) of the k-th compressor ℜ_{k}^{−} is a complete join subsemilattice of uco(C ), then the condition ℜ_{k}^{−}(D) ∈ π_{k}(U) in the above definition can be omitted. For K ⊆ [1, n], we say that ℜ is K -invertible on a |K |-tuple V, where ∀i ∈ K . π_{i}(V) ⊆ π_{i}(U), if it is k-invertible on π_{k}(V), for any k ∈ K . In particular, ℜ is fully invertible on V ⊆ U if it is [1, n]- invertible on V. For the simpler case of a unary refinement ℜ : U → uco(C ), we have that ℜ^{−} : U → uco(C ) is defined as ℜ^{−}(D) = ⊔{A ∈ U | ℜ(A) = ℜ(D)}, and ℜ is invertible on V ⊆ U iff for any D ∈ V , ℜ(ℜ^{−}(D)) = ℜ(D). It is simple to observe that the above definition of k-invertibility can be formulated by using the unary refinements induced by a (n-ary) refinement. More precisely, if ℜ : U → uco(C ) is a refinement, then we have already seen that for any k ∈ [1, n] and π_{i}(D) ∈ π_{i}(U) (i ≠ k), λX .ℜ(D[X /k]) : π_{k}(U) → uco(C ) is a unary refinement. It is then easily seen that ℜ is k-invertible in V ⊆ π_{k}(U) iff λX .ℜ(D[X /k]) is (1-)invertible on V ⊆ π_{k}(U). In this case, for the compressor (λX .ℜ(D[X /k]))^{−} : V → π_{k}(U) and the k-th compressor ℜ_{k}^{−} of ℜ, the following mutual equality result holds: ∀D ∈ V . (λX .ℜ(D[X /k]))^{−}(D) = ℜ_{k}^{−}(D).

Not all domain refinements are invertible in a satisfactory way. An example is provided by the negative completion refinement ℜ_{¬} of Sect. 3. In fact, as observed in [9], the optimal basis of the domain Sign (in Sect. 3) for ℜ_{¬} does not exist.

Since Sign enjoys all most important lattice-theoretic properties, this means that ℜ_{¬} is not invertible on any really significant class of abstract domains.

As the following result says, compressors relative to idempotent refinements are extensive and idempotent. Proposition 4.2 If ℜ : U → uco(C ) is idempotent and k-invertible in V , then the compressor ℜ_{k}^{−} : U[V /k] → π_{k}(U) is extensive (i.e. π_{k}(D) ⊑ ℜ_{k}^{−}(D)) and idempotent (i.e. ℜ_{k}^{−}(D) ∈ V ⇒ ℜ_{k}^{−}(D[ℜ_{k}^{−}(D)/k]) = ℜ_{k}^{−}(D)).

In general, compressors are neither monotone nor antimonotone: [14] proves that the least disjunctive basis operator is neither monotone nor antimonotone, and later we will show that the least disjunctive basis is the compressor relative to the disjunctive completion refinement. On the other hand, as expected, a compressor applied to a refined domain performs no further simplification. Proposition 4.3 If ℜ : U → uco(C ) is idempotent and k-invertible in V then for any D ∈ U[V /k] such that ℜ(D) ∈ V , ℜ_{k}^{−}(D[ℜ(D)/k]) = ℜ_{k}^{−}(D).

An n-ary refinement ℜ : U → uco(C ) is commutative if for any permutation τ of {1, …, n}, ℜ(π_{τ(1)}(D), …, π_{τ(n)}(D)) = ℜ(D) holds. For instance, the reduced product refinement ℜ_{⊓} is obviously commutative as well as any attribute independent refinement. For commutative refinements, the following result holds (this result admits a straightforward, although notationally tedious, generalization for generic K -commutativity and invertibility). Proposition 4.4 If ℜ : U → uco(C ) is a (possibly nonidempotent) commutative refinement and k ∈ [1, n] then, ℜ is fully invertible on V ⊆ U iff ℜ is k-invertible on π_{k}(V) iff for all D ∈ V, λX .ℜ(D[X /k]) : π_{k}(U) → uco(C ) is (1-)invertible on π_{k}(V).

Not all refinements are commutative. Examples of noncommutative refinements are reduced power [6], dependencies [13], and tensor product [18]. Due to lack of space, we do not formalize these operators as refinements. In the following, we show how the results in [3, 12, 14] on complementation and least disjunctive basis of abstract domains, actually permit to define the compressors relative to reduced product and disjunctive completion respectively. These results also suggest a generalization towards a general pattern of invertible refinements. The Inverse of Reduced Product. Since ℜ_{⊓} is commutative, by Proposition 4.4, ℜ_{⊓} is fully invertible on some V × V ⊆ uco(C )^{2} iff for any D ∈ V , λX .(D ⊓ X ) is invertible on V . As recalled in Sect. 2, for any meet-continuous complete lattice C and D ∈ uco(C ), one can define the complement abstract domain C ∼D. Moreover, it is immediate to note that, for any complete lattice C , if D_{1}, D_{2} ∈ uco(C ) satisfy the ascending chain condition (to be ACC, for short; DCC is dual) then D_{1} ⊓ D_{2} is ACC as well, and hence meet-continuous. These observations directly imply that we can invert the reduced product on the ACC abstractions of any concrete domain C (i.e. a plain complete lattice). Let us define ACC (C ) = {D ∈ uco(C ) | D is ACC}, for any complete lattice C . Theorem 4.5 If D ∈ ACC (C ) then λX .D ⊓ X is invertible on ACC (C ), and the corresponding compressor (λX .D ⊓ X )^{−} : ACC (C ) → uco(C ) is defined as (λX .D ⊓ X )^{−}(E) = (D ⊓ E)∼D.

Thus, ℜ_{⊓} is fully invertible on ACC (C ) × ACC (C ). For instance, if D_{1}, D_{2} ∈ ACC (C ), we have that the first compressor is (ℜ_{⊓})_{1}^{−}(D_{1}, D_{2}) = (D_{1} ⊓ D_{2})∼D_{2}.

The Inverse of Disjunctive Completion. Giacobazzi and Ranzato defined and studied in [14] the operator of least disjunctive basis on abstract domains, that corresponds exactly to the compressor for the disjunctive completion refinement. Hence, the results in [14] can be reformulated as follows.

Theorem 4.6

(i) If C is co-algebraic completely distributive then ℜ_{∨} is invertible on all uco(C ). (ii) If C is distributive then ℜ_{∨} is invertible on {A ∈ uco(C ) | A is finite}.

Compressing Lower and Upper Refinements. Define an upper (lower) improvement on C as any map I : ℘(C ) → ℘(C ) such that ∀S ∈ ℘(C ).∀s ∈ S.∀s′ ∈ I(S). s ≤ s′ (s′ ≤ s). Glb and lub are obvious examples of lower and upper improvements. We prove that upper and lower improvements induce invertible refinements in a natural way. This provides a general pattern for defining new invertible refinements. For an upper (lower) improvement I on C , define the corresponding upper (lower) set-refinement ℜ^{I} : ℘(C ) → ℘(C ) as: ℜ^{I}(X ) = X ∪ (∪_{S⊆X} I(S)). It turns out that ℜ^{I} is a lower closure on ⟨℘(C ), ⊇⟩. However, in general, for a closure ρ ∈ uco(C ), ℜ^{I}(ρ) may not be in uco(C ). But, when a unary full idempotent refinement ℜ ∈ lco(uco(C )) is the restriction on uco(C ) of an upper (lower) set-refinement, i.e. there exists an upper (lower) improvement I on C such that ℜ = ℜ_{|uco(C )}^{I} (in this case, we call ℜ an upper (lower) refinement), the following general theorem of inversion for ℜ holds. Theorem 4.7 If C is a complete lattice satisfying the DCC (ACC), then any upper (lower) refinement ℜ ∈ lco(uco(C )) is invertible on all uco(C ). For instance, if C is distributive and I = ∨, we get for free the inversion of disjunctive completion of Theorem 4.6 (ii). By Proposition 4.4, the attribute independent refinement induced by a family of upper or lower refinements is invertible under suitable hypotheses derived by Theorem 4.7. By this last observation, it would be possible (but we omit the details) to derive as a consequence of Theorem 4.7 the result of inversion for the reduced product of Theorem 4.5. Minimal ℜ-decompositions. For a given refinement ℜ : U → uco(C ) of arity n > 1, we say that D ∈ U is a ℜ-decomposition of D ∈ uco(C ), if D = ℜ(D). If D, E ∈ U are two ℜ-decompositions of D then D is better than E if E ⊑ D componentwise.^{1} The intended meaning is that D is better than E because it is a less costly decomposition (in particular, ∑_{i=1}^{n} |π_{i}(D)| ≤ ∑_{i=1}^{n} |π_{i}(E)|). Obviously, this relation induces a partial ordering between ℜ-decompositions of D, but, in general, optimal (i.e. least) ℜ-decompositions for this order do not exist. For instance, ⟨D, {⊤}⟩ and ⟨{⊤}, D⟩ are uncomparable minimal ℜ_{⊓}- decompositions of D. It is easy to see that, if ℜ is idempotent and fully invertible on V ⊆ U and D is a ℜ-decomposition of D, then for any k ∈ [1, n] the tuple D[ℜ_{k}^{−}(D)/k] (∗) is still a ℜ-decomposition of D which is better than D, and

1 For commutative refinements, both this definition and the successive development would identify decompositions up to permutation – however, we omit the details.

that D is a minimal ℜ-decomposition of D iff ∀k ∈ [1, n]. π_{k}(D) = ℜ_{k}^{−}(D). Thus, each ℜ-decomposition can be improved by iterating the above step (∗) as shown in the following nondeterministic function ℜ-min, where choose selects an arbitrary element from its input set.

 fun ℜ-min (D:array[1, n] of domains)

J := {1, ..., n};

 repeat

k := choose(J ); J := J \ {k};

D := D[ℜk^{−}(D)/k]

 until J = ∅
 output D

Theorem 4.8 Let ℜ be an idempotent and fully invertible refinement on V. If, for any k ∈ [1, n], ℜ_{k}^{−} is anti-monotone then for any D ∈ V, ℜ-min(D) is a minimal ℜdecomposition of ℜ(D).

Note that, for a ℜ-decomposition D of D, we can get at most n! different minimal ℜ-decompositions of D.

For instance, if ℜ(D_{1}, D_{2}) = D then ⟨ℜ_{1}^{−}(D_{1}, ℜ_{2}^{−}(D_{1}, D_{2})), ℜ_{2}^{−}(D_{1}, D_{2})⟩ is a minimal ℜ-decomposition of D. Theorem 4.8 generalizes the results of [3, Sect. 4], since the compressor relative to reduced product is anti-monotone (cf. [3]).

5 A Relation of Adjunction between Refinements and Compressors Assume that ℜ is an idempotent n-ary refinement ℜ : U → uco(C ) that is k-invertible on V ⊆ π_{k}(U) ⊆ uco(C ), for some k ∈ [1, n]. We saw in Sect. 4 that any (k-th) unary refinement λX .ℜ(D[X /k]) : π_{k}(U) → uco(C ) induced by ℜ is invertible in V , and the corresponding compressor (of type V → π_{k}(U)) is defined as (λX .ℜ(D[X /k]))^{−} = λX ∈ V .ℜ_{k}^{−}(D[X /k]). In general, the refinement λX .ℜ(D[X /k]) and the relative compressor λX .ℜ_{k}^{−}(D[X /k]) do not constitute an adjunction on the poset of domains ⟨V , ⊑⟩ of invertibility, i.e. for all A ∈ π_{k}(U) and B ∈ V , ℜ(D[A/k]) ⊑ B ⇔ A ⊑ ℜ_{k}^{−}(D[B/k])) may not hold. This is due to the fact that compressors, in general, are not monotone, as observed after Proposition 4.2. Since, by Proposition 4.2, compressors are idempotent and extensive, this also implies that compressors λX .ℜ_{k}^{−}(D[X /k]), well-defined on V , are not upper closures on ⟨V , ⊑⟩, as instead we would expect by viewing compressors as inverses of refinements.

We solve this asymmetry between abstract domain refinements and compressors by modifying the standard ordering ⊑ of precision between domains, so as to keep into account the rôle of ℜ. We maintain the above scenario and also suppose that the refinement λX .ℜ(D[X /k]) is well-defined in π_{k}(U), namely for any D ∈ π_{k}(U), ℜ(D[D/k]) ∈ π_{k}(U), and that ⟨π_{k}(U), ⊑⟩ is a complete sublattice of ⟨uco(C ), ⊑⟩. These hypotheses imply that λX .ℜ(D[X /k]) is a lower closure on the complete lattice ⟨π_{k}(U), ⊑⟩. Then, we define the following relation ⊑^{ℜ} (that actually depends also on the fixed arguments π_{i}(D), i ≠ k) on π_{k}(U):

A ⊑^{ℜ} B iff ℜ(D[A/k]) ⊑ ℜ(D[B/k]) & (ℜ(D[B/k]) ⊑ ℜ(D[A/k]) ⇒ A ⊑ B).

Theorem 5.1 ⟨π_{k}(U), ⊑^{ℜ}⟩ is a complete lattice.

Note that A ⊑ B ⇒ A ⊑^{ℜ} B. Thus, we call ⊑^{ℜ} the lifting of ⊑ via ℜ. This lifted complete partial order reflects precisely the relative precision of domains with respect to the refinement λX .ℜ(D[X /k]): A is more precise than B in the lifted order if the refinement of A is more precise than the refinement of B in the standard sense and, when they are the same (i.e. (ℜ(D[B/k]) = ℜ(D[A/k])), then A contains more information. For this ordering ⊑^{ℜ}, we get back a relation of adjunction between the invertible refinement and its compressor. Theorem 5.2 ∀A ∈ π_{k}(U), B ∈ V . ℜ(D[A/k]) ⊑^{ℜ} B ⇔ A ⊑^{ℜ} ℜ_{k}^{−}(D[B/k])). As a consequence, λX . ℜ_{k}^{−}(D[X /k]) is an upper closure operator on ⟨V , ⊑^{ℜ}⟩ (provided it is well-defined on V ). For example, we get an adjunction between reduced product and complementation w.r.t. the lifted order. For any complete lattice C and D ∈ uco(C ), the lifted order on uco(C ) is defined as follows: For all A, B ∈ uco(C ), A ⊑^{⊓} B iff D ⊓ A ⊑ D ⊓ B & (D ⊓ B ⊑ D ⊓ A ⇒ A ⊑ B). Hence, the adjunction between refinement (reduced product) and compressor (complementation) is the following: For any A ∈ uco(C ) and B ∈ ACC (C ), D ⊓ A ⊑^{⊓} B ⇔ A ⊑^{⊓} (D ⊓ B)∼D. Acknowledgments. We are grateful to Francesca Scozzari for her contribution to Theorem 3.7 and to one anonymous referee for many helpful suggestions. References

1. M. Codish, A. Mulkers, M. Bruynooghe, M. García de la Banda, and M. Hermenegildo. Improving abstract interpretations by combining domains. ACM TOPLAS, 17(1):28–44, 1995.

2. M. Comini and G. Levi.An algebraic theory of observables.In Proc. ILPS’94 , pp. 172–186, 1994.

3. A. Cortesi, G. Filé, R. Giacobazzi, C. Palamidessi, and F. Ranzato. Complementation in abstract interpretation. ACM TOPLAS, 19(1):7–47, 1997.

4. A. Cortesi, B. Le Charlier, and P. Van Hentenryck. Combinations of abstract domains for logic programming. In Proc. POPL’94, pp. 227–239, 1994.

5. P. Cousot and R. Cousot. Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Proc. POPL’77, pp. 238-252, 1977.

6. P. Cousot and R. Cousot. Systematic design of program analysis frameworks. In Proc. POPL’79, pp. 269–282, 1979.

7. P. Cousot and R. Cousot. Inductive definitions, semantics and abstract interpretation. In Proc. POPL’92, pp. 83–94, 1992.

8. P. Cousot and R. Cousot. Higher-order abstract interpretation (and application to comportment analysis generalizing strictness, termination, projection and PER analysis of functional languages). In Proc. IEEE ICCL’94, pp. 95–112, 1994.

9. G. Filé, R. Giacobazzi, and F. Ranzato. A unifying view of abstract domain design. ACM Comput. Surv., 28(2):333–336, 1996.

10. G. Filé and F. Ranzato. Improving abstract interpretations by systematic lifting to the powerset. In Proc. ILPS’94, pp. 655–669, 1994.

11. R. Giacobazzi. “Optimal” collecting semantics for analysis in a hierarchy of logic program semantics. In Proc. STACS’96, LNCS 1046, pp. 503-514, 1996.

12. R. Giacobazzi, C. Palamidessi, and F. Ranzato. Weak relative pseudo-complements of closure operators. Algebra Universalis, 36(3):405-412, 1996.

13. R. Giacobazzi and F. Ranzato. Functional dependencies and Moore-set completions of abstract interpretations and semantics. In Proc. ILPS’95, pp. 321–335, 1995.

14. R. Giacobazzi and F. Ranzato. Optimal domains for disjunctive abstract interpretation. To appear in Sci. Comput. Program. Preliminary version in LNCS 1058, pp. 141–155, 1996.

15. T.P. Jensen. Disjunctive strictness analysis. In Proc. LICS’92, pp. 174–185. 1992.

16. K. Muthukumar and M. Hermenegildo. Combined determination of sharing and freeness of program variables through abstract interpretation. In Proc. ICLP’91, pp. 49–63, 1991.

17. A. Mycroft. Completeness and predicate-based abstract interpretation. In Proc. PEPM’93.

18. F. Nielson. Tensor products generalize the relational data flow analysis method. In Proc. 4th Hungarian Comput. Sci. Conf., pp. 211–225, 1985.

19. U. Reddy and S. Kamin.On the power of abstract interpretation.In Proc. IEEE ICCL’92, 1992.

20. R.C. Sekar, P. Mishra, and I.V. Ramakrishnan. On the power and limitation of strictness analysis. To appear in J. ACM. Preliminary version in Proc. POPL’91, pp. 37–48, 1991.

21. R. Sundararajan and J. Conery. An abstract interpretation scheme for groundness, freeness, and sharing analysis of logic programs. In Proc. FST&TCS’92, LNCS 652, pp. 203–216, 1992.

22. K. Yi and W.L. Harrison. Automatic generation and management of interprocedural program analyses. In Proc. POPL’93, pp. 246–259, 1993.

23. M. Ward. The closure operators of a lattice. Ann. Math., 43(2):191–196, 1942.