Completeness in Abstract Interpretation: A Domain Perspective

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. Completeness in abstract interpretation is an ideal and rare situation where the abstract semantics is able to take full advantage of the power of representation of the underlying abstract domain. In this paper, we develop an algebraic theory of completeness in abstract interpretation. We show that completeness is an abstract domain property and we prove that there always exist both the greatest complete restriction and the least complete extension of any abstract domain, with respect to continuous semantic functions. Under certain hypotheses, a constructive procedure for computing these complete domains is given. These methodologies provide advanced algebraic tools for manipulating abstract interpretations, which can be fruitfully used both in program analysis and in semantics design.

1 Introduction

Abstract interpretation [8, 9] is a widely established methodology for programming language semantics approximation, which is primarily used for specifying and then validating static program analyses. Given a so-called concrete semantics defined by a concrete domain C (a complete lattice) and a semantic function [[·]] : Program → C , an abstract interpretation is specified by an abstract domain A (a complete lattice) and an abstract semantic function [[·]]^{♯} : Program → A, where the relationship between concrete and abstract objects is formalized by a pair of adjoint maps α : C → A and γ : A → C such that α(c) ≤_{A} a means that a is a correct approximation of c. Then, a typical soundness theorem for an abstract interpretation goes as follows: For all programs P, α([[P]])) ≤_{A} [[P]]^{♯}. It is well-known [8] that for the non-restrictive case of least fixpoint based semantics, i.e. where [[P]] = lfp(T_{P} ) and [[P]]^{♯} = lfp(TP^{♯}) for some monotone operators T_{P} : C → C and TP^{♯} : A → A indexed over Program, soundness is implied by the following stronger, but nevertheless much easier to check, condition: α ∘ T_{P} ≤_{A} TP^{♯} ∘ α.

While soundness is the basic requirement for any abstract interpretation, the dual notion of completeness is instead an ideal and quite rare situation. Completeness arises when no loss of precision occurs by approximating α([[P]]) with [[P]]^{♯}, i.e. when α([[P]]) = [[P]]^{♯}. Roughly speaking, this means that the abstract semantics is able to take full advantage of the power of representation of the abstract domain A. In this sense, complete abstract interpretations can be rightfully considered as optimal. As before, for least fixpoint based semantics, completeness is implied by the following stronger condition called full completeness: α ∘ T_{P} = TP^{♯} ∘ α (cf. [9]). For instance, the classical naïve “rule of signs” abstract interpretation is fully complete. In fact, the sign of a concrete integer multiplication can be exactly retrieved by the rule of signs applied to its arguments, i.e., by leaving out the details, sign(n · m) = sign(n) ·^{♯} sign(m), where ·^{♯} is the obvious abstract multiplication between signs.

The problem of achieving the completeness for an abstract interpretation, by enhancing either the abstract domain or the abstract semantic operators, has been investigated by a number of authors (see Section 9). While this has been successfully solved for some specific abstract interpretations and analyses, the more general problem of making a generic abstract interpretation complete in the best possible way (i.e. involving the most simple abstract domains and operators), is still, to the best of our knowledge, open.

We attack this problem from a domain perspective, since we show that, fixed a concrete semantics, both completeness and fully completeness for an abstract interpretation only depend on the underlying abstract domain. Thus, we develop an algebraic theory of domain completeness within the classical abstract interpretation framework. We concentrate on the set of all the domains, in the lattice L_{C} of abstract interpretations of the fixed concrete domain C , which are complete and fully complete for a given family of semantic operators F , denoted resp. by Δ(C , F ) and Γ(C , F ). In Section 4, we prove that both Δ(C , F ) and Γ(C , F ) are always complete meet subsemilattices of L_{C} . Moreover, while we show that, in general, Δ(C , F ) is not a join subsemilattice of L_{C} , even under very restrictive hypotheses on C and F , by contrast we prove that, when the functions in F are (Scott-)continuous, Γ(C , F ) is a complete join subsemilattice of L_{C} , and therefore a complete sublattice. It should be remarked that this latter result is far from being trivial.

Based on these results, in Section 5, we introduce a family of operators acting on abstract domains, which transform non-complete domains into complete or fully complete ones. There are two possibilities for doing this: Either by refining domains, i.e. by enhancing their precision by adding new elements, or by simplifying them by taking out some information which may cause incompleteness. Thus, following the ideas on systematic abstract domain refinements and simplifications introduced in [14, 18], we define the complete and fully complete kernel operators IK and K, and the least fully complete extension operator E. The first two are abstract domain simplifications which, given a set of concrete monotone functions F and an input abstract domain A, give as output the most concrete domains IK(A) and K(A) which are more abstract than A and complete, resp. fully complete, for any f ∈ F . E is instead an abstract domain refinement which, given a set of concrete continuous functions F and A, returns the most abstract domain E (A) which is an extension (i.e. more precise) of A and fully complete for any f ∈ F . By the aforementioned negative findings on the structure of Δ(C , F ), an analogous least complete extension operator is not generally definable. These operators satisfy a number of relevant algebraic properties; in particular, we show that the least fully complete extension of a domain can be always achieved by decomposing the input domain into simpler factors and then by refining these simpler domains. In Section 6, we present a constructive method for designing least fully complete extensions and fully complete kernels of abstract domains, under the hypotheses that the concrete semantic functions in F are additive.

As a relevant example, we reconstruct the Cousot and Cousot [8] abstract domain of integer intervals as the least fully complete extension for integer addition of the rule of signs domain. Clearly, to be an abstract domain is a relative notion. Thus, our systematic operators can be also applied to refine or simplify domains for analysis relatively to other more precise – but still approximated – ones. In Section 8, we show how to apply our operators to devise an intelligent strategy for improving the precision of abstract domains, which takes into account the efficiency/precision trade-off in a systematic refinement step. We apply this idea to compare the expressive power of some well-known abstract domains for ground-dependency analysis of logic programs.

2 Basic Notions

The structure ⟨uco(C ), ⊑, ⊔, ⊓, λx.⊤, λx.x⟩ denotes the complete lattice of all upper closure operators (shortly closures) on a complete lattice ⟨C , ≤, ∨, ∧, ⊤, ⊥⟩ (i.e., monotone, idempotent and extensive operators on C ), where (i) ρ ⊑ η iff ∀x ∈ C . ρ(x) ≤ η(x), (ii) (⊔_{i∈I} ρ_{i})(x) = x ⇔ ∀i ∈ I . ρ_{i}(x) = x; (iii) (⊓_{i∈I} ρ_{i})(x) = ∧_{i∈I} ρ_{i}(x); (iv) λx.⊤ and λx.x are, respectively, the top and bottom. The complete lattice of all lower closure operators on C is denoted by lco(C ) and is dually isomorphic to uco(C ). Recall that each closure ρ ∈ 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 is meet-closed, i.e. X = M(X ) = {∧Y | Y ⊆ X } (note that ⊤ ∈ X ). ⟨ρ(C ), ≤⟩ is a complete meet subsemilattice of C , while it is a complete sublattice iff ρ is completely additive. Let us also recall that uco(C ) is dual-atomic, i.e., for any ρ ∈ uco(C ), ρ = ⊓_{x ∈ρ(C )\{⊤}}φ_{x} , where each closure φ_{x} = {⊤, x}, for x ∈ C \ {⊤}, is a dual-atom in uco(C ).

In the standard Cousot and Cousot abstract interpretation theory, abstract domains can be equivalently specified either by Galois connections (GCs) or by closure operators (see [9]). In the first case, the concrete domain C and the abstract domain A (both assumed to be complete lattices) are related by a pair of adjoint functions of a GC (α, C , A, γ). If (α, C , A, γ) is a Galois insertion (GI), each element in A is useful to represent the concrete domain C , being α onto. Any GC (α, C , A, γ) may be lifted to a GI by reduction of the abstract domain A, i.e. by identifying in an equivalence class those elements in A having the same concrete meaning. In the second case instead, an abstract domain is specified as (the set of fixpoints of) an upper closure on the concrete domain. These two approaches are completely equivalent: If ρ ∈ uco(C ) and A ≅ ρ(C ) (with ι : ρ(C ) → A and ι^{−1} : A → ρ(C ) being the isomorphism) then (ι ∘ ρ, C , A, ι^{−1}) is a GI; if (α, C , A, γ) is a GI then ρ_{A} = γ ∘ α ∈ uco(C ) is the closure associated with A such that ρ_{A}(C ) ≅ A; moreover, these two constructions are one the inverse of the other. Hence, we will identify uco(C ) with the so-called lattice of abstract interpretations of C , viz. the complete lattice of all abstract domains of the concrete domain C . Often, we will find convenient to identify closures with their sets of fixpoints, denoted as sets by capital Latin letters; instead, when viewing closures as functions, they will be denoted by Greek letters. We keep this soft ambiguity, since one can distinguish their use as functions or sets, according to the context. The ordering on uco(C ) corresponds precisely to the standard order used in abstract interpretation to compare abstract domains with regard to their precision: A_{1} is more precise than A_{2} iff A_{1} ⊑ A_{2} in uco(C ). The lub and glb on uco(C ) have therefore the following meaning as operators on domains. Suppose {A_{i}}_{i∈I} ⊆ uco(C ): (i) ⊔_{i∈I} A_{i} is the most concrete among the domains which are abstractions of all the A_{i}’s, i.e. it is their least common abstraction; (ii) ⊓_{i∈I} A_{i} is (isomorphic to) the well-known reduced product of all the A_{i}’s, and, equivalently, it is the most abstract among the domains (abstracting C ) which are more concrete than every A_{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. [17]). This property allowed to define the operation of complementation of abstract domains (cf. [6]), namely an operation which, starting from any two domains D ⊑ A, where D is meetcontinuous, gives as result the most abstract domain D ∼A, such that (D ∼A)⊓A = D. A (conjunctive) decomposition of an abstract domain A ∈ uco(C ) is any tuple of domains ⟨D_{i}⟩_{i∈I} ⊆ uco(C ) such that A = ⊓_{i∈I} D_{i}. Complementation is important for decomposing abstract domains: If D ⊑ A then ⟨D ∼A, A⟩ is a (binary) decomposition for C , and more general decompositions can be obtained by complementation (see [6]).

3 Completeness in Abstract Interpretation

Let Program denote the set of (syntactically well-formed) programs. The concrete standard semantics is in general specified by a semantic function [[·]] : Program → C , where C is a concrete semantic domain of denotations, which we assume to be a complete lattice. If an abstract interpretation is specified by a GI (α, C , A, γ) and by an abstract semantic function [[·]]^{♯} : Program → A, then [[·]]^{♯} is a sound abstract semantics, or (correctly) approximates [[·]], if, for any program P, α([[P]]) ≤_{A} [[P]]^{♯}, or, equivalently, [[P]] ≤_{C} γ([[P]]^{♯}). The pattern of definition of [[·]] obviously depends on the considered programming language and on the semantics style adopted. We follow here a customary least fixpoint semantic approach, which is general enough to subsume and include most kinds of semantic specifications (see [12]). In the following, for two complete lattices C and D, we denote by C ⟶^{m}D, C ⟶^{c}D, and C ⟶^{a}D, respectively, the set of all monotone, (Scott-)continuous and (completely) additive (i.e. preserving all lub’s) functions from C to D. A concrete semantics is therefore specified by a pair ⟨C , T ⟩, where C is a complete lattice and T : Program → (C ⟶^{m}C ). For P ∈ Program, we use T_{P} to denote more compactly T (P). The least fixpoint semantics of any program P is then given by [[P]] = lfp(T_{P} ) ∈ C . On the abstract side, for some T^{♯} : Program → (A⟶^{m}A), the abstract least fixpoint semantics is analogously defined by [[P]]^{♯} = lfp(TP^{♯}).

Given a concrete semantics S = ⟨C , T ⟩ and an abstract semantics S^{♯} = ⟨A, T^{♯}⟩, related by a GI (α, C , A, γ), S^{♯} is called a sound abstraction of S if for all P ∈ Program, α(lfp(T_{P} )) ≤_{A} lfp(TP^{♯}). This soundness condition can be more easily verified by checking whether for all P ∈ Program, α ∘ T_{P} ≤_{A} TP^{♯} ∘ α, or, equivalently, α ∘ T_{P} ∘ γ ≤_{C} TP^{♯}. We distinguish between these two forms of soundness and we say that S^{♯} is a fully sound abstraction of S if for all P ∈ Program, α ∘ T_{P} ≤_{A} TP^{♯} ∘ α.

In abstract interpretation, the term completeness is used dually to the above notion of soundness [9, 11, 22]. Again, one distinguishes between a weaker form of completeness, involving least fixpoints only, and a stronger one (but easier to verify) involving semantic functions. We say that S^{♯} is a (fully) complete abstraction of S if for all P ∈ Program, (TP^{♯} ∘ α ≤_{A} α ∘ T_{P} ) lfp(TP^{♯}) ≤_{A} α(lfp(T_{P} )). Because soundness is always required in abstract interpretation, in the following we abuse terminology and say that S^{♯} is (fully) complete for S if for all P ∈ Program, (α ∘ T_{P} = TP^{♯} ∘ α) α(lfp(T_{P} )) = lfp(TP^{♯}). We also use such notions of completeness and full completeness locally for a given pair of semantic functions TP^{♯} and T_{P} .

Completeness as a Domain Property. For a pair of semantic functions T_{P} :C → C and TP^{♯} : A → A, when α ∘ T_{P} ∘ γ ≤_{C} TP^{♯} holds, TP^{♯} is traditionally called a correct approximation of T_{P} [9]. It is also well-known since [9, Corollary 7.2.0.4], that the abstract domain A induces a best correct approximation of T_{P} given by T_{P}^{A} = α ∘ T_{P} ∘ γ. Consequently, A always induces an (automatically) fully sound abstract semantics ⟨A, λP. T_{P}^{A}⟩. By contrast, this is not true for completeness, i.e., for a given abstract domain A it may well happen that it is not possible to define a fully complete or merely complete abstract semantics based on A – on the contrary, this is the most frequent situation. Furthermore, if A admits a fully complete abstract semantic operator TP^{♯}, then T_{P}^{A} is fully complete as well, and T_{P}^{A} = TP^{♯}: TP^{♯} = TP^{♯} ∘ α ∘ γ = α ∘ T_{P} ∘ γ = T_{P}^{A}. Likewise, if TP^{♯} is complete then T_{P}^{A} is complete: α(lfp(T_{P} )) ≤_{A} lfp(T_{P}^{A}) ≤_{A} lfp(TP^{♯}) = α(lfp(T_{P} )). Thus, we get the following important characterization of completeness as a domain property:

It is possible to define a (fully) complete abstract semantic operator on an abstract domain A if and only if the best correct approximation induced by A is (fully) complete.

4 The Lattice of Complete Abstract Interpretations

We have seen that one can consider, without loss of generality, completeness and full completeness for best correct approximations only. Moreover, by the equivalence between the GI and closure operator approaches to abstract domain design, completeness and full completeness can be equivalently specified for closure operators: In fact, it turns out that for a GI (α, C , A, γ) and f : C ⟶^{m}C , the best correct approximation f^{A} is (fully) complete iff γ(α(lfp(f ))) = lfp(γ ∘ α ∘ f ) ((γ ∘ α) ∘ f = (γ ∘ α) ∘ f ∘ (γ ∘ α)). Thus, in the following, we will study completeness and full completeness relatively to closure operators and generic (monotone) functions from a purely algebraic point of view, and say that A is (fully) complete for f if f^{A} is (fully) complete. We generalize full completeness to cope with generic (possibly nonmonotone) n-ary functions. If o⃗ denotes a generic tuple of objects, then o⃗_{i} denotes its i-th component.

Definition 4.1 Let C be a complete lattice.

(i) Given f : C^{n} → C (n ≥ 1), ρ ∈ uco(C ) is fully complete for f if for any x⃗ ∈ C^{n}, ρ(f (x⃗)) = ρ(f (ρ(x⃗_{1}), ..., ρ(x⃗_{n}))).

(ii) Given f ∈ C ⟶^{m}C , ρ ∈ uco(C ) is complete for f if ρ(lfp(f )) = lfp(ρ ∘ f ). □

We denote the condition in (i) simply by ρ ∘ f = ρ ∘ f ∘ ρ. Note that (i) encompasses also functions of type C → (C → ⋯ (C → C ) ⋯), by “Curryfying” them; moreover, lfp(ρ ∘ f ) in (ii) could be equivalently replaced by lfp(ρ ∘ f ∘ ρ).

For f ∈ C^{n} → C , we define Γ(C , f ) ⊆ uco(C ) to be the set of fully complete closures on C for f : Γ(C , f ) = {ρ ∈ uco(C ) | ρ ∘ f = ρ ∘ f ∘ ρ}. If f : C ⟶^{m}C then we define Δ(C , f ) ⊆ uco(C ) as the set of complete closures on C for f : Δ(C , f ) = {ρ ∈ uco(C ) | ρ(lfp(f )) = lfp(ρ ∘ f )}. Also, if η ∈ uco(C ) then Γ^{↑η}(C , f ) and Δ^{↑η}(C , f ) are the set of closures on ⟨η(C ), ≤_{C} ⟩ that are, respectively, fully complete and complete (for f ); since ρ ∈ uco(η(C )) iff ρ ∈ uco(C ) and ρ ⊑ η, then, by denoting ↑ η the principal filter of uco(C ) generated by η, we have that Γ^{↑η}(C , f ) = Γ(C , f ) ∩ ↑η and Δ^{↑η}(C , f ) = Δ(C , f ) ∩ ↑η. If (α, C , A, γ) is a GI such that γ ∘ α = η, then Γ^{↑A}(C , f ) and Δ^{↑A}(C , f ) are alternative notations for Γ^{↑η}(C , f ) and Δ^{↑η}(C , f ) respectively. We can also define completeness and full completeness relatively to any set of concrete functions: If F ⊆ C^{n} → C and G ⊆ C ⟶^{m}C then Γ(C , F ) = ∩_{f ∈F} Γ(C , f ) and Δ(C , G) = ∩_{g∈G}Δ(C , g) (obviously, Γ(C , ∅) = Δ(C , ∅) = uco(C )). We can then restate the basic Cousot and Cousot [9] result on completeness using our notation as follows: If F ⊆ C ⟶^{m}C then Γ(C , F ) ⊆ Δ(C , F ).

Example 4.2 Consider the classical “rule of signs” domain Sign in Fig. 1, which is an abstraction of ⟨℘(ZZ), ⊆⟩ [8]. If ρ_{s} denotes the closure on ⟨℘(ZZ), ⊆⟩ corresponding to Sign, i.e. Sign ≅ ρ_{s}(℘(ZZ)), as noted by [22], it is easy to check that ρ_{s} is fully complete for the multiplication ∗ : ℘(ZZ)^{2} → ℘(ZZ) given by X ∗ Y = {n · m | n ∈ X , m ∈ Y }. Moreover, Sign (i.e. ρ_{s}) is not fully complete for integer addition ⊕ : ℘(ZZ)^{2} → ℘(ZZ): For instance, ρ_{s}(ρ_{s}({−3, −1} ⊕ ρ_{s}({4, 7})) = ρ_{s}(ZZ) = ZZ, whereas ρ_{s}({−3, −1} ⊕ {4, 7}) = ρ_{s}({1, 3, 4, 6}) = 0+. Also, consider the unary monotone function f that selects, e.g., even numbers, i.e. f = λX . X ∩ ZZ_{even}. While Sign is not fully complete for f (e.g., ρ_{s}(f ({−1, 2})) = 0+ ≠ ZZ = ρ_{s}(f (ρ_{s}({−1, 2})))), it is instead complete for f : ρ_{s}(lfp(f )) = ρ_{s}(∅) = ∅ = lfp(ρ_{s} ∘ f ). Consider now the lattice uco(Sign) in Fig. 1 of all possible abstractions of Sign, and the monotone unary square operation sq = λX . X ∗ X . It is a routine task to check that the sets of complete and fully complete abstractions of Sign for sq are as follows:

(i) Δ^{↑Sign}(℘(ZZ), sq) = uco(Sign) \ {ρ_{5}}: In fact, ρ_{5}(lfp(sq)) = ρ_{5}(∅) = −0, whilst lfp(ρ_{5} ∘ sq) = ZZ, and this holds for ρ_{5} only;

[figure: •; •; •; •; •; 0+; ZZ; −0; 0; ∅]

[figure: •; •; •; •; •; •; •; •; •; •; •; •; •; •; ρ_{1} = {ZZ}; ρ_{2}; ρ_{3}; ρ_{4}; ρ_{5}; ρ_{6}; ρ_{7}; ρ_{8}; ρ_{9}; ρ_{10}; ρ_{11}; ρ_{12}; ρ_{13}; ρ_{s} = Sign]

ρ_{2} = {ZZ, 0+}
ρ_{3} = {ZZ, 0}
ρ_{4} = {ZZ, ∅}
ρ_{5} = {ZZ, −0}
ρ_{6} = {ZZ, 0+, ∅}
ρ_{7} = {ZZ, 0+, 0}
ρ_{8} = {ZZ, 0, ∅}
ρ_{9} = {ZZ, −0, 0}
ρ_{10} = {ZZ, −0, ∅}
ρ_{11} = {ZZ, 0+, 0, ∅}
ρ_{12} = {ZZ, −0, 0+, 0}
ρ_{13} = {ZZ, −0, 0, ∅}

Fig. 1. The lattices Sign and uco(Sign).

(ii) Γ^{↑Sign}(℘(ZZ), sq) = uco(Sign) \ {ρ_{5}, ρ_{10}}: For ρ_{5} and ρ_{10}, just consider X = {0}. Observe that Δ(℘(ZZ), sq) is not a complete sublattice of uco(℘(ZZ)): In fact, ρ_{9}, ρ_{10} ∈ Δ(℘(ZZ), sq), whereas ρ_{9} ⊔ ρ_{10} = ρ_{5} ∉ Δ(℘(ZZ), sq). Similarly, it is not difficult to check that Γ^{↑Sign}(℘(ZZ), ∗) = uco(Sign) \ {ρ_{2}, ρ_{5}, ρ_{6}, ρ_{10}}. □

The following result summarizes some helpful basic properties of the set of complete and fully complete abstract domains.

Proposition 4.3 Let f : C^{n} → C , g : C → C , and h : C ⟶^{m}C .

(i) λx. ⊤_{C} , λx. x ∈ Γ(C , f ) ∩ Δ(C , h). (ii) For all c ∈ C , Γ(C , λx⃗. c) = uco(C ) = Δ(C , λx. c). (iii) Γ(C , λx⃗. ∨n_{i=1} x⃗_{i}) = uco(C ). (iv) ρ ∈ Γ(C , λx⃗. ∧n_{i=1} x⃗_{i}) ⇔ ∀X ⊆ C . | X | < ω ⇒ ρ(∧X ) = ∧ρ(X ).

(v) If ρ ∈ Γ(C , {f , g}) then ρ ∈ Γ(C , g ∘ f ). (vi) If ρ, η ∈ Γ(C , f ) and ρ ∘ η = η ∘ ρ then ρ ∘ η ∈ Γ(C , f ). (vii) For all i ∈ [1, n], Γ(C , f ) = Γ(C , {λx⃗ ∈ C^{n−1}. f (⟨x_{1}, ..., x_{i−1}, c, x_{i}, ..., x_{n−1}⟩)}_{c∈C} ).

For F ⊆ C^{n} ⟶^{m}C and G ⊆ C ⟶^{m}C , we now consider both Γ(C , F ) and Δ(C , G) equipped with the pointwise partial order ⊑ of relative precision of domains, inherited from the lattice of abstract interpretations uco(C ). Our first finding is that Γ(C , F ) and Δ(C , G) are always (the sets of fixpoints of) lower closures on uco(C ), i.e. complete meet subsemilattices of uco(C ). The fact that full completeness for monotone unary functions is preserved by glb was already observed in [6, Proposition 5.2.3].

Theorem 4.4 If F ⊆ C^{n} ⟶^{m}C , G ⊆ C ⟶^{m}C then Γ(C , F ), Δ(C , G) ∈ lco(uco(C )).

As far as the lub is concerned, in Example 4.2 we observed that, in general, a subset of complete closures Δ(C , f ) is not closed under lub’s.

Example 4.5 Let us consider the finite chain of five points C = {0 < 1 < 2 < 3 < 4} and the function f : C → C defined as f = {0 ↦ 0, 1 ↦ 0, 2 ↦ 0, 3 ↦ 4, 4 ↦ 4}. Note that f is monotone and hence it is both additive and co-additive, while lfp(f ) = 0. Next, consider the closures ρ_{1}, ρ_{2} ∈ uco(C ) given by ρ_{1} = {1, 3, 4} and ρ_{2} = {2, 3, 4}. It is not difficult to verify that ρ_{1}, ρ_{2} ∈ Δ(C , f ): ρ_{k} (lfp(f )) = k = lfp(ρ_{k} ∘ f ). It turns out that ρ_{1} ⊔ρ_{2} = {3, 4} does not belong to Δ(C , f ). In fact, (ρ_{1} ⊔ρ_{2})(lfp(f )) = 3, while (ρ_{1} ⊔ ρ_{2}) ∘ f = {0 ↦ 3, 1 ↦ 3, 2 ↦ 3, 3 ↦ 4, 4 ↦ 4}, and hence lfp((ρ_{1} ⊔ ρ_{2}) ∘ f ) = 4. □

In general, i.e. with no hypothesis on C and f , also Γ(C , f ) is not closed under lub’s, as the following example shows.

Example 4.6 Let the ω + 2 ordinal be C , and consider the upper closure f ∈ uco(C ) defined by f (C ) = {x | x < ω} ∪ {ω + 1} (thus, f is the identity on C \ {ω} whereas maps ω to the top ω + 1). Next, consider the closures ρ_{1}, ρ_{2} ∈ uco(C ) defined by ρ_{1} = {x < ω | x is even} ∪ {ω, ω + 1} and ρ_{2} = {x < ω | x is odd} ∪ {ω, ω + 1}. It is immediate to verify that ρ_{i} ∘f = f ∘ρ_{i} (i = 1, 2), and therefore, by Proposition 4.3 (vii), ρ_{1}, ρ_{2} ∈ Γ(C , f ). Moreover, for the lub ρ_{1} ⊔ρ_{2} = {ω, ω +1}, we have that (ρ_{1} ⊔ρ_{2})∘f = ρ_{1} ⊔ ρ_{2} whilst (ρ_{1} ⊔ ρ_{2}) ∘ f ∘ (ρ_{1} ⊔ ρ_{2}) = λx. ω + 1, and therefore ρ_{1} ⊔ ρ_{2} ∉ Γ(C , f ). □

Note that, in Example 4.6, f lacks of the continuity property. Indeed, the following key result shows that for continuous functions, lub’s of fully complete closures are still fully complete.^{1} We already stated this fact, for continuous unary functions, in [18].

Theorem 4.7 If F ⊆ C^{n} ⟶^{c}C then Γ(C , F ) ∈ uco(uco(C )).

Continuity is a well-known and sufficiently weak hypothesis, which makes the above result widely applicable in programming language semantics and analysis.

Corollary 4.8 If F ⊆ C^{n} ⟶^{c}C then Γ(C , F ) is a complete sublattice of uco(C ). Moreover, if uco(C ) is pseudocomplemented then Γ(C , F ) is pseudocomplemented.

In general, Γ(C , F ) is not a sub-pseudocomplemented lattice of uco(C ): In Example 4.2, the pseudocomplement of ρ_{7} in uco(Sign) is ρ_{10} while it is ρ_{13} in Γ(℘(ZZ), sq).

5 Completeness by Domain Transformers

The notion of abstract domain refinement has been studied in [14], and more recently in [18], as a formalization and generalization for most of the systematic operators enhancing the precision of abstract domains (e.g. reduced product and disjunctive completion). For a fixed concrete domain C , a (unary) abstract domain refinement is defined as a mapping ℜ : uco(C ) → uco(C ), such that ℜ is monotone, and, for any A ∈ uco(C ), ℜ(A) is more precise than A (i.e., ℜ is reductive: ℜ(A) ⊑ A). Moreover, most of the times, refinements are idempotent, i.e. they upgrade domains all at once. This last condition evidently defines idempotent refinements as lower closure operators on uco(C ), i.e. mappings in lco(uco(C )). A dual theory holds for abstract domain simplifications, that are defined as upper closures in uco(uco(C )) (cf. [18]). Following this framework and exploiting the results of Section 4, we introduce the complete and fully complete kernel simplifications, for a set F of monotone functions, and the least fully complete extension refinement, for a set F of continuous functions. The (fully) complete kernel of an abstract domain A is defined as the most concrete domain abstracting A which is (fully) complete for any f ∈ F , while the least fully complete extension of A is the most abstract domain which is more precise than A and fully complete for any f ∈ F ; by the negative observations of Section 4, a similar least complete extension refinement is not in general definable.

Complete Kernel Operators. Let us introduce the following basic definitions.

Definition 5.1 For F ⊆ C^{n} → C , G ⊆ C ⟶^{m}C , define K_{F}^{C} , IK_{G}^{C} : uco(C ) → uco(C ) such that K_{F}^{C} (X ) = ⊓{Y ∈ uco(C ) | X ⊑ Y , Y ∈ Γ(C , F )} and IK_{G}^{C}(X ) = ⊓{Y ∈ uco(C ) | X ⊑ Y , Y ∈ Δ(C , G)}. □

1 Amato and Levi [1] have independently made an observation similar to Example 4.5, and stated an analogous but weaker result to Theorem 4.7 for additive functions.

When F = {f }, we write K_{f}^{C} and IK_{f}^{C} . By definition, K_{F}^{C} , IK_{G}^{C} ∈ uco(uco(C )), i.e. both K_{F}^{C} and IK_{G}^{C} are idempotent abstract domain simplifications (cf. [18]). We say that K_{F}^{C} (IK_{G}^{C}) is safely defined when for any X ∈ uco(C ), K_{F}^{C} (X ) ∈ Γ(C , F ) (IK_{G}^{C}(X ) ∈ Δ(C , G)). In this case, we call K_{F}^{C} and IK_{G}^{C}, respectively, the fully complete kernel operator for F (in C ) and the complete kernel operator for G (in C ). By Theorem 4.4, IK_{G}^{C} is always safely defined, while monotonicity on F is enough for K_{F}^{C} .

Example 5.2 The domain {ZZ, −0, ∅} in Example 4.2 is not fully complete for sq and {ZZ, 0−} is not even complete for sq. By Theorem 4.4, there exist their (fully) complete kernels, and from the diagram of uco(Sign) in Fig. 1 we derive that Ksq^{℘(ZZ)}({ZZ, −0, ∅}) = {ZZ, ∅} and IKsq^{℘(ZZ)}({ZZ, −0}) = {ZZ}. Let us also consider the following abstract domain Sign^{+} depicted below, introduced by Mycroft in [22, Sect. 3.1]. With respect to Sign of Example 4.2, Sign^{+} comprises a new element denoting the integer interval [1, 9]. ρs^{+}

[figure: ∅; [1, 9]; 0; −0; 0+; ZZ; •; •; •; •; •; •]

denotes the closure associated with Sign^{+} (i.e. such that ρs^{+}(℘(ZZ)) ≅ Sign^{+}). It is not difficult to check that Sign^{+} is fully complete for λX . {n} ∗ X iff n ∉ [2, 9]: In fact, for any n ∈ [2, 9], there exists X ⊆ [1, 9] ⊂ ZZ such that ρs^{+}({n}∗X ) ⊂ ρs^{+}({n}∗ρs^{+}(X )) (if n = 2 then X = [1, 2], and if n = 9 then X = [1, 1]). Note that only by removing [1, 9] from Sign^{+} we get a fully complete domain for all

n ∈ ZZ, viz. Sign. This observation implies that Sign is the fully complete kernel of Sign^{+} for λX . {n} ∗ X when n ∈ [2, 9]. Obviously, by the above considerations, Sign^{+} is not fully complete for ∗, and indeed K∗^{℘(ZZ)}(Sign^{+}) = Sign. □

The Least Fully Complete Extension Operator. Dually to what done above, we give the following definition.

Definition 5.3 For F ⊆ C^{n} → C , G ⊆ C ⟶^{m}C , define E_{F}^{C} , IE_{G}^{C} : uco(C ) → uco(C ) as E_{F}^{C} (X ) = ⊔{Y ∈ uco(C ) | Y ⊑ X , Y ∈ Γ(C , F )} and IE_{G}^{C}(X ) = ⊔{Y ∈ uco(C ) | Y ⊑ X , Y ∈ Δ(C , G)}. □

As before, when F = {f } we write E_{f}^{C} and IE_{f}^{C} . By definition, both E_{F}^{C} and IE_{G}^{C} are abstract domain refinements in the sense of [14], i.e. E_{F}^{C} , IE_{G}^{C} ∈ uco(uco(C )). Similarly to what done above, we define E_{F}^{C} and IE_{G}^{C} to be safely defined when their ranges are subsets of Γ(C , F ) and Δ(C , G), respectively. In this case, E_{F}^{C} and IE_{G}^{C} are called, respectively, the least fully complete extension operator (for F ) and the least complete extension operator (for G).

Recall that, in Examples 4.2 and 4.5, we have shown that even when the concrete domain is either an atomic complete Boolean algebra ℘(X ), or a finite chain and the concrete function is both additive and co-additive, a lub of complete closures is not necessarily still complete. Hence, this key observation precludes us the possibility of finding some reasonable conditions on C and/or G in order that IE_{G}^{C} is safely defined. For instance, from the diagram of uco(Sign) in Fig. 1 we derive that the least complete extension for sq of {ZZ, −0} does not exist: In fact, {ZZ, −0} just admits {ZZ, −0, 0} and {ZZ, −0.∅} as minimal complete extensions, and therefore, wrongly, we would get IEsq^{℘(ZZ)}({ZZ, −0}) = {ZZ, −0}. By contrast, when F consists of continuous functions, by Theorem 4.7, for any X ∈ uco(C ), E_{F}^{C} (X ) is the least fully complete extension of X , i.e. in this case E_{F}^{C} is safely defined.

Example 5.4 Since sq in Example 4.2 is obviously continuous, by Theorem 4.7, every abstract domain of ℘(ZZ) admits the least fully complete extension for sq. For instance, Esq^{℘(ZZ)}({ZZ, −0}) = {ZZ, −0, 0} and E∗^{℘(ZZ)}({ZZ, 0+, ∅}) = {ZZ, 0+, 0, ∅}. □

Algebraic Properties. We study now the basic algebraic properties of the above operators K, E, IK, and IE with respect to the operations of reduced product and least common abstraction of domains. These results are particularly important in order to simplify the construction of complete domains.

Lemma 5.5 Let F ⊆ C^{n} → C and G ⊆ C ⟶^{m}C . Then, (K_{F}^{C} , uco(C ), uco(C ), E_{F}^{C} ) and (IK_{G}^{C}, uco(C ), uco(C ), IE_{G}^{C}) are Galois connections.

The following relevant algebraic properties are consequences of the above result.

Proposition 5.6 Let F ⊆ C^{n} → C , G ⊆ C ⟶^{m}C , X , Y ∈ uco(C ) such that X ⊑ Y .

(i) K_{F}^{C} and IK_{G}^{C} are additive, and E_{F}^{C} and IE_{G}^{C} are co-additive. (ii) If C is meet-continuous then E_{F}^{C} (X ) = E_{F}^{C} (X ∼ Y ) ⊓ E_{F}^{C} (Y ) and IE_{G}^{C}(X ) = IE_{G}^{C}(X ∼Y ) ⊓ IE_{G}^{C}(Y ).

By point (i), the least (fully) complete extension of a domain A can always be obtained by computing separately the least (fully) complete extensions of the factors in a decomposition of A. This decomposition can be obtained by complementation. For instance, by (ii), if C is meet-continuous then E_{F}^{C} (X ) = E_{F}^{C} (X ∼K_{F}^{C} (X )) ⊓ K_{F}^{C} (X ).

The concrete domain C is not always the best place where completeness and full completeness for a semantic operator can be verified, as it might be far too concrete for this task. We show that one can always refine or simplify a domain A abstracting C by our operators, with the same result, on any (fully) complete abstraction D of C which is more concrete than A. We know that, for A ∈ uco(C ) and f : C^{n} → C (when needed, we assume n = 1), the best correct approximation of f for A is f^{A} : A^{n} → A defined as f^{A} = ρ_{A} ∘ f , where ρ_{A} is the closure associated with A, and, on the right hand side, f is thought of being restricted to A^{n}. If F is a set of functions, then we denote by F^{A} the corresponding set of best correct approximations for A. The idea is that we can reason about completeness issues relatively to the concrete domain A and function f^{A}, instead of, resp., C and f . Note that when f is monotone then f^{A} is monotone as well. Thus, for F ⊆ C^{n} → C and G ⊆ C ⟶^{m}C , and for any A ∈ uco(C ), we can define the operators of Definitions 5.1 and 5.3 relatively to Γ(A, F^{A}) and Δ(A, G^{A}), denoted by K_{F}^{A}, IK_{G}^{A}, E_{F}^{A}, and IE_{G}^{A}, where the superscript is intended to mean that the best correct approximations are considered. By Theorem 4.4, IK_{G}^{A} is always a complete kernel operator, and, for F ⊆ C^{n} ⟶^{m}C , K_{G}^{A} is a fully complete kernel operator. Moreover, it is easy to prove that if f : C^{n} ⟶^{c}C and A ∈ Γ(C , f ), then f^{A} : A^{n} ⟶^{c}A. Thus, if F ⊆ C^{n} ⟶^{c}C and A ∈ Γ(C , f ) then also E_{F}^{A} is a safely defined least fully complete extension operator.

Theorem 5.7 Let F ⊆ C^{n} → C , G ⊆ C ⟶^{m}C , and A ∈ uco(C ).

(i) A ∈ Γ(C , F ) ⇔ ∀X ∈ ↑A. K_{F}^{C} (X ) = K_{F}^{A}(X ) ⇔ ∀X ∈ ↑A. E_{F}^{C} (X ) = E_{F}^{A}(X ). (ii) A ∈ Δ(C , G) ⇔ ∀X ∈ ↑A. IK_{G}^{C}(X ) = IK_{G}^{A}(X ) ⇔ ∀X ∈ ↑A. IE_{G}^{C}(X ) = IE_{G}^{A}(X ).

The following example shows how to practically exploit the properties in Proposition 5.6 and Theorem 5.7 to design the least fully complete extension of Mycroft’s domain Sign^{+} for integer multiplication.

Example 5.8 Consider the domain Sign^{+} in Example 5.2. We constructively define the least fully complete extension of Sign^{+} for integer multiplication. As we observed in Example 5.2, Sign^{+} is fully complete for f_{n} = λX . {n} ∗ X (which is obviously continuous) iff n ∉ [2, 9]. Let n ∈ [2, 9]. As we have shown in Example 5.2, Kfn^{℘(ZZ)}(Sign^{+}) =

[figure: •; •; •; •; •; •; •; •; •; 0−; ZZ; 0+; 0; ∅; [1, 9]; [1, 4]; [1, 2]; [1]]
E_{f_{2}}^{Int}(Sign^{+})

[figure: •; •; •; •; •; •; •; •; 0−; ZZ; 0+; 0; ∅; [1, 9]; [1, 3]; [1]]
E_{f_{3}}^{Int}(Sign^{+})

[figure: •; •; •; •; •; •; •; 0−; ZZ; 0+; 0; ∅; [1, 9]; [1]]
{E_{fn}^{Int}(Sign^{+})}_{n∈[5,9]}

[figure: •; •; •; •; •; •; •; •; •; •; 0−; ZZ; 0+; 0; ∅; [1, 9]; [1, 4]; [1, 3]; [1, 2]; [1]]

E∗^{℘(ZZ)}(Sign^{+})

Fig. 2. Least fully complete extensions of Sign^{+}.

Sign and Sign^{+} ∼ Sign = {ZZ, [1, 9]}. By Proposition 5.6 (ii), we get Efn^{℘(ZZ)}(Sign^{+}) = Efn^{℘(ZZ)}(Sign^{+} ∼ Kfn^{℘(ZZ)}(Sign^{+})) ⊓ Efn^{℘(ZZ)}(Kfn^{℘(ZZ)}(Sign^{+})) = Efn^{℘(ZZ)}({ZZ, [1, 9]}) ⊓ Sign. We compute the least fully complete extension Efn^{℘(ZZ)}({ZZ, [1, 9]}) of the atomic domain {ZZ, [1, 9]} by a recursive computation. Consider the Cousot and Cousot [8] domain of integer intervals Int ∈ uco(℘(ZZ)) defined by

Int = {[a, b]}_{a≤b} ∪ {(−∞, b]}_{b∈ZZ} ∪ {[a, +∞)}_{a∈ZZ} ∪ {(−∞, +∞)} ∪ {⊥}. It is easy to prove that Int ∈ Γ(℘(ZZ), ∗) and hence, for any n ∈ ZZ, Int ∈ Γ(℘(ZZ), f_{n}). Thus, by Theorem 5.7, for any n ∈ ZZ and A such that Int ⊑ A, Efn^{℘(ZZ)}(A) = E_{fn}^{Int}(A), and therefore we can consider the more abstract (and simple) domain Int as concrete domain of reference. The following proposition characterizes the least fully complete extension in Int of any atomic domain of the form {ZZ, [1, m]}. We assume that m ≥ 1 and n ∈ [2, m]. An analogous result holds for m ≤ −1, {ZZ, [m, 1]} and n ∈ [m, 2].

Proposition 5.9 E_{fn}^{Int}(\{ZZ, [1, m]\}) = \{ZZ, [1, m]\} ⊓ E_{fn}^{Int}(\{ZZ, [1, ⌊ \frac{m}{n} ⌋]\}).

The above recursive definition has a solution which can be obtained finitely for any n ≤ m. For Sign^{+}, i.e. m = 9, it provides the domains depicted in Fig. 2. In particular, if F = {f_{n} | n ∈ ZZ} then E∗^{℘(ZZ)}(Sign^{+}) = EF^{℘(ZZ)}(Sign^{+}) = EInt_{{f_{2},f_{3}}}(Sign^{+}). □

6 Systematic Construction of Complete Domains

In Example 5.8 we have shown how to constructively design the least fully complete extension for integer multiplication of a simple domain for sign analysis. In this section, we show that under some hypotheses on the semantic functions, a similar methodology can be always defined and applied to finite abstract domains in order to construct their least fully complete extensions and kernels.

Constructing Least Fully Complete Extensions. The following result gives a useful characterization of full completeness for additive functions.

Theorem 6.1 Let f : C ⟶^{a}C . Then, for all X ∈ uco(C ), X ∈ Γ(C , f ) ⇔ ∀x ∈ X . ∨ {y ∈ C | f (y) ≤ x} ∈ X .

Thus, when f is additive, it turns out that E_{f}^{C} (X ) is the least meet-closed set Y containing X such that x ∈ Y ⇒ ∨{y | f (y) ≤ x} ∈ Y . This domain can be constructively obtained as the greatest (viz. most abstract) solution in uco(C ), smaller or equal to X , of the recursive abstract domain equation Y = Y ⊓ F_{f} (Y ), where F_{f} = λX . M({∨{y ∈ C | f (y) ≤ x} | x ∈ X }). Note that F_{f} : uco(C ) → uco(C ) is monotone, and therefore E_{f}^{C} (X ) is the limit of the (possibly transfinite) iteration sequence Y^{0} = X , Y^{α+1} = Y^{α} ⊓ F_{f} (Y^{α}) if α is a successor ordinal, and Y^{α} = ⊓_{δ<α}Y^{δ} if α is a limit ordinal. Clearly, if C is finite, then this constructive method is terminating. It is not difficult to prove that if f is in addition extensive and X = {⊤, x}, with x ∈ C \ {⊤}, is an atomic domain, then each element Y^{α} of the above iteration sequence having E_{f}^{C} ({⊤, x}) as limit, is a chain. In this case, termination for an atomic domain {⊤, x} is ensured by assuming the weaker hypothesis that ⟨↓ x, ≤⟩ is a well-ordered sublattice (i.e. it does not contain infinite descending chains) of the (possibly infinite) concrete domain C . An analogous argument led us to the constructive characterization of Proposition 5.9. The interest in least fully complete extensions of atomic domains is justified by observing that, because uco(C ) is always dual-atomic, for any abstract domain there exists a canonical decomposition involving atomic domains only: If X ∈ uco(C ) then ⟨{⊤, x}⟩_{x ∈X \{⊤}} is such a decomposition of X . Then, by Proposition 5.6 (i), for any X ∈ uco(C ) and f : C ⟶^{c}C , E_{f}^{C} (X ) = ⊓_{x ∈X \{⊤}}E_{f}^{C} ({⊤, x}). The extension of the above constructive method to a set of additive functions F is straightforward. In fact, by Theorem 6.1, for any X ∈ uco(C ), X ∈ Γ(C , F ) ⇔ ∀x ∈ X .∀f ∈ F .∨{y ∈ C | f (y) ≤ x} ∈ X . Thus, E_{C}^{F} (X ) simply is the greatest fixpoint solution in uco(C ) of the equation Y = X ⊓ F_{F} (Y ), where C_{F} = λX . M({∨{y ∈ C | f (y) ≤ x} | x ∈ X , f ∈ F }).

Constructing Fully Complete Kernels. The systematic construction of fully complete kernels relies on the above procedure for least fully complete extensions. As before, we consider atomic decompositions of the input domain, and the following result characterizes the fully complete kernel of a domain X in terms of the least fully complete extensions of the factors in the atomic decomposition of X .

Theorem 6.2 If f : C ⟶^{c}C then K_{f}^{C} (X )=⊓{E_{f}^{C} ({⊤, x}) | x ∈ X , E_{f}^{C} ({⊤, x}) ⊆ X }.

Input : Finite domain X Output : Fully complete kernel K of X K := {⊤}; A := X ; while A ≠ {⊤} do

x := choose(A \ {⊤}); if E_{f}^{C} ({⊤, x}) ⊆ X then

K := K ⊓ E_{f}^{C} ({⊤, x})

endwhile The above result hints a systematic constructive method to design fully complete of abstract domains. The correctness of the algorithm on the left follows by Theorem 6.2. The function choose selects and removes an arbitrary element from its input domain. Clearly, when f is additive, the least fully complete extension of the atomic domains can be obtained by the constructive method above.

7 Reconstructing the Integer Interval Domain

We observed in Example 4.2 that Sign is not fully complete for integer addition ⊕. Instead, it is an easy task to prove that the Cousot and Cousot integer interval domain Int of Example 5.8 is fully complete for addition, i.e. Int ∈ Γ(℘(ZZ), ⊕). We can go beyond this expected result. Since ⊕ is additive, and therefore continuous, the least complete extension of Sign with respect to ⊕ does exist, and the following theorem actually proves that it coincides with Int.

Theorem 7.1 E⊕^{℘(ZZ)}(Sign) = Int.

Therefore, the domain Int for integer interval analysis can be reconstructed by a systematic domain refinement from the rule of signs domain Sign.

8 Intelligently Refining Domains: The Case of Groundness Analysis

We have seen that for a fixed concrete least fixpoint semantics S = ⟨C , f ⟩, any abstraction D ∈ uco(C ) and its corresponding best correct approximation f^{D} : D → D automatically induce a correct abstract semantics I^{D} = ⟨D, f^{D}⟩. Clearly, being abstract or concrete is a relative notion, and therefore if A ∈ uco(C ) is a domain abstracting D, viz. D ⊑ A, we can reason on the completeness relationships between A and D, where I^{D} plays the role of the relative concrete semantics for A. In such a scenario, we simply say that A is complete, resp. fully complete, for D when A ∈ Δ(D, f^{D}), resp. A ∈ Γ(D, f^{D}). In particular, this situation arises whenever ℜ : uco(C ) → uco(C ) is some (possibly nonidempotent) domain refinement, and therefore, for some abstract domain A, C ⊑ ℜ(A) ⊑ A. In this case, we take into consideration the possible completeness relations of A wrt the relative concrete semantics ⟨ℜ(A), f^{ℜ(A)}⟩. Following the notation at the end of Section 5, we denote by Ef^{ℜ(A)} the corresponding completeness transformer. This is a safely defined least fully complete extension operator under the weak hypothesis that the best correct approximation f^{ℜ(A)} : ℜ(A) → ℜ(A) is continuous. In general, we have that ℜ(A) ⊑ Ef^{ℜ(A)}(A) ⊑ A. We say that ℜ(A) is too refined when ℜ(A) ⊏ Ef^{ℜ(A)}(A) holds. The intuition behind this definition is as follows. When, in the above scenario, it happens that A is fully complete for D, then we can reasonably consider the abstract interpretation I^{A} = ⟨A, f^{A}⟩ as just thinly less precise than I^{D}. In other terms, the gap of precision between the abstract interpretations I^{A} and I^{D} is very narrow, and therefore an efficiency/precision trade-off would suggest to prefer I^{A} to the more costly I^{D}. In particular, whenever ℜ(A) ⊏ Ef^{ℜ(A)}(A), one should prefer the thinly less refined domain Ef^{ℜ(A)}(A) rather than the canonical refinement ℜ(A). Thus, under the weak hypothesis that each best correct approximation f^{ℜ(A)} is continuous, an intelligent “efficiency-oriented” version ℜ^{⋆} of a refinement ℜ can therefore be defined as ℜ^{⋆} = λA. Ef^{ℜ(A)}(A). In the following, we illustrate a practical example of this idea in the field of ground-dependency analysis for logic programs.

The Intelligent Disjunctive Completion of Def is Pos. Def and Pos are two well-known finite abstract domains of propositional formulae widely used for grounddependency analysis of logic programs [20]. We refer e.g. to [2] for the details of their definitions. These abstract domains can be viewed as abstractions of the standard concrete domain ⟨℘(Atom), ⊆⟩ used in a collecting bottom-up semantics for logic programs (as usual, the set of atoms Atom is considered up to renaming). It turns out that ℘(Atom) ⊏ Pos ⊏ Def . For instance, a pair ⟨p(x, y, z), x ∧ (y ↔ z)⟩ ∈ Def ⊂ Pos represents each atom p(t_{1}, t_{2}, t_{3}) such that for any its instance p(s_{1}, s_{2}, s_{3}): (i) s_{1} is ground; (ii) var(s_{2}) = var(s_{3}). In particular, p(a, b, c) and p(a, x, g(x)) satisfy this property (where, as usual, a, b, c, … denote ground terms).

The disjunctive completion [9] is a well known abstract domain refinement that enhances an abstract domain so that it becomes disjunctive, i.e. so that the corresponding concretization map is additive. When the concrete domain C is completely distributive, as any powerset ⟨℘(X ), ⊆⟩ is, the disjunctive completion IP(A) of an abstract domain A can be obtained by quotienting the powerset of A for the equivalence relation {⟨S, T ⟩ | S, T ⊆ ℘(A), ∨_{C} γ(S) = ∨_{C} γ(T )} (see [15] for more details). The concretization of an equivalence class [S] of the disjunctive completion IP(A) is obviously defined as ∨_{C} γ(S), while the abstraction of [S] in A is given by ∨_{A}S. It has been shown in [15, Theorem 5.3] that Pos is not disjunctive, i.e. IP(Pos) ⊏ Pos, while [19, Theorem 7.2] proved that IP(Def ) = IP(Pos). Thus, it turns out that IP(Def ) = IP(Pos) ⊏ Pos ⊏ Def . For example, by considering the following abstract predicates ⟨p(x, y), x⟩ and ⟨p(x, y), x → y⟩, one has γ_{Def} (⟨p(x, y), x⟩) ∪ γ_{Def} (⟨p(x, y), x → y⟩) ⊂ γ_{Def} (⟨p(x, y), x ∨ (x → y)⟩) = γ_{Def} (⟨p(x, y), true⟩) (it is enough to consider the atom p(v, w)), and this shows that Def and Pos are not disjunctive.

Following the standard bottom-up approach (e.g. [3]), we consider the well-known s-semantics S = ⟨℘(Atom), T_{P}^{s} ⟩ of [13] as the concrete least fixpoint semantics of reference, which is fully abstract for the observable given by the computed answer substitutions of a logic program. Then, the abstract domains Def , Pos and their common disjunctive completion IP(Def ) induce the abstract semantics Def^{s} = ⟨Def , T_{P}^{Def} ⟩, Pos^{s} = ⟨Pos, T_{P}^{Pos}⟩, IP(Def )^{s} = ⟨IP(Def ), T_{P}^{IP(Def )}⟩, where each abstract semantic operator is defined as the best correct approximation of T_{P}^{s} on the corresponding abstract domain. Let us turn to discuss the completeness issues between these abstract semantics. It is known [20] that Def is not complete (and therefore fully complete) for Pos and IP(Def ), i.e. Def ∉ Γ(Pos, {T_{P}^{Pos}}_{P∈Program}) ∪ Γ(IP(Def ), {T_{P}^{IP(Def )}}_{P∈Program}), while [15, Proposition 5.13] proved that Pos is fully complete (and hence complete) for IP(Def ), i.e. Pos ∈ Γ(IP(Def ), {T_{P}^{IP(Def )}}_{P∈Program}).

Example 8.1 Consider the programs P and Q below.

P : p(x, y) : − q(x, y), r(x, y).  Q : p(x, a) : − p(x, z), p(y, x).
q(a, x) : −  p(x, x) : −
q(x, a) : −  p(a, y) : −
r(x, x) : −

It is easy to see that ⟨p(x, y), x ↔ y⟩ ∈ lfp(T_{P}^{Def} ), whilst ⟨p(x, y), x ∧y⟩ ∈ lfp(T_{P}^{Pos}) = lfp(T_{P}^{IP(Def )}). Thus, in P, by either Pos or IP(Def ), we are able to infer that any computed answer substitution for the predicate p will ground both its arguments, while in Def we can only conclude that the first argument is ground iff the second is ground. Moreover, the Kleene iterations for T_{Q}^{Pos} and T_{Q}^{IP(Def )} are as follows: (T_{Q}^{Pos})^{0} = ⟨p(x, y), false⟩, (T_{Q}^{Pos})^{1} = ⟨p(x, y), y → x⟩, (T_{Q}^{Pos})^{2} = ⟨p(x, y), true⟩ (least fixpoint); (T_{Q}^{IP(Def )})^{0} = ⟨p(x, y), false⟩, (T_{Q}^{IP(Def )})^{1} = ⟨p(x, y), [x ↔ y, x]⟩, (T_{Q}^{IP(Def )})^{2} = ⟨p(x, y), [x ↔ y, x, y]⟩ (least fixpoint). Thus, in Q, by IP(Def ) we are able to infer that in each computer answer substitution for p, either its first argument is ground or its second argument is ground or they are equivalent. Instead, by using Pos we get no ground-dependency information. Nevertheless, by abstracting in Pos the final output ⟨p(x, y), [x ↔ y, x, y]⟩ of IP(Def ) we get exactly the output ⟨p(x, y), true⟩ of Pos. □

We sharp the aforementioned result of [15, Proposition 5.13], and we show that Pos is the least complete and fully complete extension of Def in IP(Def ), i.e., by letting F = {T_{P}^{IP(Pos)}}_{P∈Program}, the following theorem holds.

Theorem 8.2 E_{F}^{IP(Def )}(Def ) = IE_{F}^{IP(Def )}(Def ) = Pos.

To conclude, let us draw the practical consequences of Theorem 8.2, in view of the general observations made at the beginning of this section. If we want to systematically design an abstract domain for disjunctive ground-dependency analysis starting from the existing domain Def , then, according to the standard procedure of refining Def to its disjunctive completion, we should use the disjunctive domain IP(Def ). However, according to our definitions, IP(Def ) is too refined, since, by Theorem 8.2, E^{IP(Def )}(Def ) = Pos is a proper abstraction of IP(Def ). By contrast, following the “efficiency-oriented” strategy of refinement outlined above, the intelligent disjunctive completion is defined as P^{⋆} = λA.EF^{IP(A)}(A), and therefore we get P^{⋆}(Def ) = Pos. This still is a systematic step of refinement, and by doing this, it is important to remark that we dramatically gain in efficiency: While IP(Def ) has an exponential size wrt Def , i.e. |IP(Def )| = O(2^{|Def |}), by contrast, it is easy to verify that |Pos| = O(|Def |) yet maintaining a relationship of full completeness between Pos and IP(Def ).

9 Related Work

The notion of completeness in abstract interpretation has been first considered by Cousot and Cousot in [9], where the basic properties of complete abstractions in the approximation of fixpoint-based semantics have been proved. Completeness arises typically among (concrete) semantics of programming languages at different levels of abstraction. Cousot and Cousot proved in [10] that some classical semantics of programming languages are (fully) complete abstractions of a generalized SOS operational semantics, and Cousot [7] formalized the relationships between some well known type inference systems as complete (called exact) abstract interpretations. In logic program semantics, Giacobazzi [16] proved that fully complete abstractions relating semantics provide a corresponding hierarchy of models for positive logic programs, while Comini and Levi [5] based their taxonomy of observables (perfect, denotational, and semidenotational) on the notion of full completeness, applied to some basic operators for building SLD-trees. Recently, Amato and Levi [1] studied the lattice structure of these observables, which is basically the lattice of full complete abstractions of the above additive operators for building SLD-trees, and independently formulated an analogous but weaker result to our Theorem 4.7, for additive operators only. In program analysis, Sekar et al. [24] focussed on completeness of Mycroft’s [21] strictness analysis of functional programs. Their approach is rather different from ours: They identified the greatest class Cl of programs such that the strictness analysis of P is complete iff P ∈ Cl. In our terminology, they have found the greatest set of programs Cl such that Strictness ∈ Δ(C , {T_{P} }_{P∈Cl}), where C and T_{P} are, respectively, the concrete domain and the semantic transformer in the standard collecting denotational semantics of P. Reddy and Kamin [23] generalized [24] to first-order and typed higher-order functional languages. Steffen [25] is one of the first authors isolating completeness as a key property for analysis. His approach is “observation directed”, in the sense that the design of a fully abstract (complete) abstract interpretation is directed by a certain observation level. This differs from our approach, which is, as the standard Cousot and Cousot theory of abstract interpretation, “semantics directed”. A categorical generalization of Steffen’s work has been successively studied in [26]. Colby [4] isolated the phenomenon of accumulated imprecision in abstract interpretation, which is essentially the same as the lack of full completeness. To overcome these problems, Colby proposes to consider a new enhanced so-called transfer relations language to express the net behavior of finite control paths in the operational semantics of programming languages, and he shows that this allows to solve the problem in some relevant examples. Colby’s approach is therefore orthogonal to ours: The whole semantic metalanguage is changed to gain precision. Finally, the most related work is certainly that of Mycroft [22]. He considers a notion of completeness which is essentially equal to ours, except that he develops his theory using a predicate-based approach to abstract interpretation (a kind of logical view of classical abstract interpretation). Moreover, he argues that the wellknown state minimization algorithm for finite deterministic automata can be used to produce a canonical (fully) complete abstract interpretation by removing useless domain elements. Although the technical approach followed by Mycroft is quite different from ours, the idea of systematically defining a canonical simplest complete abstract interpretation is basically the same idea of our complete kernel operators. This relationship certainly deserves further investigation in order to see if these two systematic methodologies actually have the same behavior. On the other hand, Mycroft does not consider the dual problem analogous to our least (fully) complete extension operators.

Acknowledgments. We are grateful to Francesca Scozzari for her contribution to Theorem 4.7.

References

1. G. Amato and G. Levi. Properties of the lattice of observables in logic programming. In Proc. APPIA-GULP-PRODE’97, pp. 175–187, 1997.

2. T. Armstrong, K. Marriott, P. Schachte, and H. Søndergaard. Two classes of Boolean functions for dependency analysis. To appear in Sci. Comput. Program., 1997.

3. R. Barbuti, R. Giacobazzi, and G. Levi. A general framework for semantics-based bottom-up abstract interpretation of logic programs. ACM TOPLAS, 15(1):133–181, 1993.

4. C. Colby. Accumulated imprecision in abstract interpretation. In Proc. 1st ACM AAS’97, pp. 77–89, 1997.

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

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

7. P. Cousot. Types as abstract interpretations. In Proc. ACM POPL’97, pp. 316–331, 1997.

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

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

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

11. 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.

12. P. Cousot and R. Cousot. Compositional and inductive semantic definitions in fixpoint, equational, constraint, closure-condition, rule-based and game-theoretic form. In Proc. CAV’95, LNCS 939, pp. 293–308, 1995.

13. M. Falaschi, G. Levi, M. Martelli, and C. Palamidessi. Declarative modeling of the operational behavior of logic languages. Theor. Comput. Sci., 69(3):289–318, 1989.

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

15. G. Filé and F. Ranzato. The powerset operator on abstract interpretations. To appear in Theor. Comput. Sci., 1998.

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

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

18. R. Giacobazzi and F. Ranzato. Refining and compressing abstract domains. In Proc. ICALP’97, LNCS 1256, pp. 771–781, 1997.

19. R. Giacobazzi and F. Ranzato. Optimal domains for disjunctive abstract interpretation. To appear in Sci. Comput. Program., 1998.

20. K. Marriott and H. Søndergaard. Precise and efficient groundness analysis for logic programs. ACM Lett. Program. Lang. Syst., 2(1-4):181–196, 1993.

21. A. Mycroft. Abstract interpretation and optimising transformations for applicative programs. PhD thesis, Univ. of Edinburgh, 1981.

22. A. Mycroft. Completeness and predicate-based abstract interpretation. In Proc. ACM PEPM ’93, pp. 179–185, 1993.

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

24. R.C. Sekar, P. Mishra, and I.V. Ramakrishnan. On the power and limitation of strictness analysis. J. ACM , 44(3), 1997.

25. B. Steffen. Optimal data flow analysis via observational equivalence. In Proc. MFCS ’89, LNCS 379, 1989.

26. B. Steffen, C.B. Jay, and M. Mendler. Compositional characterization of observable program properties. AFCET, 26:403–424, 1992.

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