Complete Abstract Interpretations made Constructive

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

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

                      {giaco,scozzari}@di.unipi.it

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

                           franz@math.unipd.it

Abstract. Completeness is a desirable, although uncommon, property of abstract interpretations, formalizing the intuition that, relatively to the underlying abstract domains, the abstract semantics is as precise as possible. We consider here the most general form of completeness, where concrete semantic functions can have different domains and ranges, a case particularly relevant in functional programming. In this setting, our main contributions are as follows. (i) Under the weak and reasonable hypothesis of dealing with continuous semantic functions, a constructive characterization of complete abstract interpretations is given. (ii) It turns out that completeness is an abstract domain property. By exploiting (i), we therefore provide explicit constructive characterizations for the least complete extension and the greatest complete restriction of abstract domains. This considerably extends previous work by the first two authors, who recently proved results of mere existence for more restricted forms of least complete extension and greatest complete restriction. (iii) Our results permit to generalize, from a natural perspective of completeness, the notion of quotient of abstract interpretations, a tool introduced by Cortesi et al. for comparing the expressive power of abstract interpretations. Fairly severe hypotheses are required for Cortesi et al.’s quotients to exist. We prove instead that continuity of the semantic functions guarantees the existence of our generalized quotients.

1 Introduction and Motivation

Within the classical and widely adopted Cousot and Cousot framework for approximating generic semantic definitions [7, 8], it is well known that completeness for an abstract interpretation is a much richer property than plain mandatory soundness. In fact, roughly speaking, a complete abstract interpretation turns out to be as precise as possible, relatively to its underlying abstract domains where approximate computations are encoded. This simple intuition explains why, although being a rather uncommon property in practice, notably in static program analysis, completeness is a highly desirable feature for an abstract interpretation, especially in abstract model checking (indeed, some authors arguably term it “optimality”). Examples of complete abstract interpretations can be found, e.g., when comparing algebraic polynomial systems [10] and program semantics [9].

In recent years, there has been a number of papers dealing with various theoretical issues related to completeness in abstract interpretation (cf. [6, 12, 16, 17, 18, 20]). Among them, Giacobazzi and Ranzato’s paper [12] points out that completeness for an abstract interpretation only depends on the underlying abstract domain, and therefore is an abstract domain property. In view of this basic observation, the following problem is then considered: Given an abstract interpretation with underlying abstract domain A, do there exist the least extension and the greatest restriction of A making the whole abstract interpretation complete? Giacobazzi and Ranzato [12] give an affirmative answer, by showing that greatest complete restrictions (called complete kernels) always exist, and, for continuous concrete semantic operations, least complete extensions exist as well. According to [11], these two operators on abstract domains are, resp., instances of generic abstract domain simplifications and refinements. Following the standard notation, let us denote resp. by α_{X,Y} and γ_{Y,X} the abstraction and concretization maps for a concrete domain X and an abstract domain Y. In [12], given a semantic operation f : C^{n} → C, an abstract interpretation I = ⟨A, f^{♯}⟩, with f^{♯} : A^{n} → A, is complete w.r.t. ⟨C, f⟩ when α_{C,A} ∘ f = f^{♯} ∘ α_{C^{n},A^{n}}. Thus, functions of generic type C → D, occurring frequently in denotational semantics for functional programming, cannot be handled. Moreover, Giacobazzi and Ranzato’s results, in general, only prove the existence of least complete extensions and complete kernels, and give a constructive iterative methodology for obtaining least complete extensions only when the semantic operations are additive. However, additivity is a fairly restrictive hypothesis to be widely applicable in practice. By contrast, the present work deals with the most general formulation of completeness for abstract interpretations – no hypothesis on the type of semantic functions is assumed – and fully solves the limitations of Giacobazzi and Ranzato’s approach, in particular on the side of complete domain construction.

Let us explain more in detail the general approach pursued in this paper. Firstly, given any concrete domain C, we denote by L_{C} the so-called lattice of abstract interpretations of C [7, 8]. Let f : C → D be any concrete semantic function occurring in some complex semantic specification, and assume that an abstract semantics is given by f^{♯} : A → B, where A ∈ L_{C} and B ∈ L_{D}. The concept of soundness is standard and well-known: ⟨A, B, f^{♯}⟩ is a sound abstract interpretation – or f^{♯} is a correct approximation of f relatively to A and B – when α_{D,B} ∘ f ⊑ f^{♯} ∘ α_{C,A} (⊑ denotes pointwise ordering). On the other hand, ⟨A, B, f^{♯}⟩ is complete when equality holds, i.e. α_{D,B} ∘ f = f^{♯} ∘ α_{C,A}. Since α_{D,B} ∘ f ⊑ f^{♯} ∘ α_{C,A} ⇔ α_{D,B} ∘ f ∘ γ_{A,C} ⊑ f^{♯}, the canonical best correct approximation f^{b_{A,B}} : A → B of f relatively to the abstract domains A and B is defined by f^{b_{A,B}} =^{def} α_{D,B} ∘ f ∘ γ_{A,C}. In this scenario, the following observation still holds: Given A and B, there exists f^{♯} such that ⟨A, B, f^{♯}⟩ is complete iff ⟨A, B, f^{b_{A,B}} ⟩ is complete. This means that, even in this general context, completeness is an abstract domain property, and gives rise to the question whether abstract domains can be minimally refined and/or simplified so that completeness is achieved. Let us give a simple example concerning Mycroft’s strictness analysis for functional programs [3, 15]. Consider the following function F of type Nat × Nat → Bool:

F (⟨x, y⟩) =^{def} if (x = 3 and y = 3) then true else ⊥

Following Burn et al. [3], from F one gets in the most natural way its denotational “collecting” semantics f : P(ℕ_{⊥} × ℕ_{⊥}) → P(Bool_{⊥}), where P is the Hoare powerdomain operator and ⊥ denotes undefinedness (i.e., both nontermination and error). Let S = {0 < 1} be the basic strictness domain, abstracting both P(ℕ_{⊥}) and P(Bool_{⊥}), and such that S × S abstracts P(ℕ_{⊥} × ℕ_{⊥}). Concretization and abstraction maps are the usual ones, e.g. γ(⟨0, 0⟩) = {⟨⊥, ⊥⟩} and γ(⟨0, 1⟩) = {⟨⊥, x⟩ | x ∈ ℕ_{⊥}}. Then, the best correct approximation f^{b} : S × S → S of f is as follows: f^{b} = {⟨0, 0⟩ ↦ 0, ⟨0, 1⟩ ↦ 0, ⟨1, 0⟩ ↦ 0, ⟨1, 1⟩ ↦ 1}. Clearly, f^{b} is not complete: For instance, α(f({⟨⊥, ⊥⟩, ⟨4, 5⟩})) = α({⊥}) = 0, whilst f^{b}(α({⟨⊥, ⊥⟩, ⟨4, 5⟩})) = f^{b}(⟨1, 1⟩) = 1. These phenomena of incompleteness in strictness analysis are analyzed in depth in [17, 18], which, however, do not investigate the issue of achieving completeness by minimally modifying the abstract domains. Moreover, because the range and domain of f are different, the method of [12] is not applicable here. Instead, the methodology proposed here allows to constructively derive the least extension E(S×S) of S×S which induces a complete abstract interpretation. It should be clear that by adding a point to S × S which is able to represent the information that the first and second components are surely not simultaneously equal to 3 ∈ ℕ_{⊥}, one gets a domain inducing a complete abstract interpretation. Indeed, our methodology allows to constructively derive that E(S × S) = (S × S) ∪ {⟨≠, ≠⟩}, where γ(⟨≠, ≠⟩) = (ℕ_{⊥} × ℕ_{⊥}) \ {⟨3, 3⟩}. In this way, one gets a best correct approximation f^{b}^{∗} : E(S × S) → S such that f^{b}^{∗}(⟨≠, ≠⟩) = 0, and therefore completeness has been achieved.

Let us illustrate the main contributions of the paper. In Section 3, the concept of completeness is formalized by resorting to the Cousot and Cousot closure operator approach to abstract interpretation [5, 8]. This allows us to be independent from specific representations of abstract domain’s objects. It is shown that completeness is an abstract domain property, which gives rise to a mathematically compact equation between closures, studied in later sections. Moreover, we observe that if an abstract interpretation f^{♯} : A → B is complete, and therefore f^{♯} = f^{b_{A,B}}, then for all the abstract domains A′ more concrete than A and B′ more abstract than B, it turns out that f^{b_{A′,B′}} : A′ → B′ is still complete. This implies that it is not meaningful to search for the complete kernel of A and the least complete extension of B, because, e.g., if the complete kernel of A would exist then A itself would already be complete. Instead, one should try to solve the converse problems. Under the working hypothesis of dealing with continuous semantic functions, a key constructive characterization of the domains inducing complete abstract interpretations is given in Section 4. More precisely, given a continuous semantic function f : C → D, we show that f^{b_{A,B}} : A → B is complete iff A is more concrete than a certain domain R_{f} (B) depending on B iff B is more abstract than a certain domain L_{f} (A) depending on A. Thus, the mappings L_{f} : L_{C} → L_{D} and R_{f} : L_{D} → L_{C} form an adjunction. By exploiting these results, we are able to characterize: (1) the least complete extension of A relative to B as the least domain which contains both A and R_{f} (B), and (2) the complete kernel of B relative to A as the greatest domain contained in both B and L_{f} (A). As a further consequence, we subsume the more restrictive notions of least complete extension and greatest complete restriction studied in [12] and the corresponding results of existence as well as the constructive characterization given for additive semantic functions. In Section 5, we investigate the relationship between completeness and the concept of quotient of an abstract interpretation, recently introduced by Cortesi et al. [4] for comparing the precision of abstract interpretations in computing a given property. Informally, the quotient of a complex abstract domain A w.r.t. a property P of A (i.e., a further abstraction of A) represents which part of A contributes in computing the property P. We show that, in general, Cortesi et al.’s quotients do not always exist: In particular, the basic assumption of continuity of the semantic functions does not ensure their existence. However, we observe that quotients, when they exist, turn out to be certain least complete extensions, which naturally formalize the intuition behind the notion of quotient. Thus, a simple and natural generalization of the notion of quotient is proposed, which retains the advantage of being always well-defined, under the hypothesis of continuity of the semantic functions.

2 Preliminaries

Basic Notation. If S is any set, P a poset, and f, g : S → P then we write f ⊑ g if for

all x ∈ S, f(x) ≤_{P} g(x). If S ⊆ P then max(S) =^{def} {s ∈ S | ∀t ∈ S. s ≤ t ⇒ s = t}.

Given two posets C and D, C ⟶^{m}D, C ⟶^{c}D, and C ⟶^{a}D denote, resp., the set of all monotone, continuous (i.e. preserving lub’s of chains), and (completely) additive (i.e. preserving all lub’s, empty set included) functions from C to D. ω denotes the first infinite ordinal. For a complete lattice C, given f : C → C, for any i ∈ ℕ, the i-th power f^{i} : C → C of f is inductively defined, for any x ∈ C, as x if i = 0, and as f(f^{i−1}(x)) if i is a successor.

The Lattice of Abstract Interpretations. In standard Cousot and Cousot’s abstract interpretation theory, abstract domains can be equivalently specified either by Galois connections, i.e. adjunctions, or by closure operators (see [5, 8]). In the first case, the concrete domain C and the abstract domain A are related by an adjunction (α, C, A, γ). It is generally assumed that (α, C, A, γ) is a Galois insertion (GI), i.e. α is onto or, equivalently, γ is 1-1. In the second case instead, an abstract domain is specified as an (upper) closure operator (shortly uco or closure) on the concrete domain C, i.e., a monotone, idempotent and extensive operator on C. These two approaches are equivalent, modulo isomorphic representations of domain’s objects. In the following, ⟨uco(C), ⊑⟩ denotes the poset of all uco’s on C. Let us recall that each ρ ∈ uco(C) is uniquely determined by the set of its fixpoints, which is its image, i.e. ρ(C) = {x ∈ C | ρ(x) = x}, and that ρ ⊑ η iff η(C) ⊆ ρ(C). Also, when ⟨C, ≤, ∨, ∧, ⊤, ⊥⟩ is a complete lattice, ⟨uco(C), ⊑, ⊔, ⊓, λx.⊤, λx.x⟩ is a complete lattice, and X ⊆ C is the set of fixpoints of a uco iff X is meet-closed, i.e. X = M(X) =^{def} {∧Y | Y ⊆ X} (where ∧∅ = ⊤ ∈ X). Moreover, given ρ ∈ uco(C), ⟨ρ(C), ≤⟩ is a complete meet subsemilattice of C. Hence, for a concrete domain C which is a complete lattice, we will identify uco(C) with the lattice L_{C} of abstract interpretations of C, i.e. the complete lattice of all possible abstract domains of C. Often, we will find convenient to identify closures with their sets of fixpoints. This does not give rise to 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} (i.e., A_{1} is more concrete than A_{2} or A_{2} is more abstract than A_{1}) iff A_{1} ⊑ A_{2} in uco(C). Lub and glb of uco(C) have therefore the following reading as operators on abstract domains. Let {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 (w.r.t. ⊑) common abstraction; (ii) ⊓_{i∈I}A_{i} is the most abstract among the domains (abstracting C) which are more concrete than every A_{i}; this domain is known as reduced product of all the A_{i}’s.

3 Completeness by Closures

Let f : C ⟶^{m}D be any monotone semantic function, where C and D are complete lattices playing the rôle of concrete semantic domains. Let an abstract interpretation ⟨A, B, f^{♯}⟩ of ⟨C, D, f⟩ be specified by the GIs (α_{C,A}, C, A, γ_{A,C}) and (α_{D,B}, D, B, γ_{B,D}), and by an abstract function f^{♯} : A⟶^{m}B. It is known [8] that f^{♯} is a correct approximation of f, i.e. α_{D,B} ∘ f ⊑ f^{♯} ∘ α_{C,A}, if and only if α_{D,B} ∘ f ∘ γ_{A,C} ⊑ f^{♯}. Thus, f^{b_{A,B}} =^{def} α_{D,B} ∘ f ∘ γ_{A,C} : A → B is called the canonical best correct approximation of f relatively to the abstract domains A and B. ⟨A, B, f^{♯}⟩ is called complete when α_{D,B} ∘ f = f^{♯} ∘ α_{C,A}. In this case, f^{♯} = f^{♯} ∘ α_{C,A} ∘ γ_{A,C} = α_{D,B} ∘ f ∘ γ_{A,C} = f^{b_{A,B}}, i.e. f^{♯} indeed is the best correct approximation f^{b_{A,B}}. This means that, given two abstract domains A and B, there exists f^{♯} such that ⟨A, B, f^{♯}⟩ is complete iff ⟨A, B, f^{b_{A,B}} ⟩ is complete. Since f^{b_{A,B}} only depends on A and B, we get that completeness is an abstract domain property. Thus, given A and B, we refer to completeness of A and B in order to refer to completeness of the whole abstract interpretation ⟨A, B, f^{b_{A,B}} ⟩. By using closure operators, if ρ = γ_{A,C} ∘α_{C,A} ∈ uco(C) and η = γ_{B,D} ∘α_{D,B} ∈ uco(D) are the uco’s associated, resp., with A and B, one can extend an analogous result in [12] by showing that A and B are complete iff η ∘ f = η ∘ f ∘ ρ. This justifies the following general definition of completeness.

Definition 3.1 Let C and D be complete lattices, f : C ⟶^{m}D, ρ ∈ uco(C), and η ∈ uco(D). Then, the pair ⟨ρ, η⟩ is complete for f if η ∘ f = η ∘ f ∘ ρ. Also, if F ⊆ C ⟶^{m}D then ⟨ρ, η⟩ is complete for F whenever ∀f ∈ F. η ∘ f = η ∘ f ∘ ρ. □

First, let us notice that, equivalently, one can define ⟨ρ, η⟩ complete for f when f ∘ ρ ⊑ η ∘ f. Further, it is worth remarking that our definition encompasses the case where f : C → C and one is interested in two different abstractions of input and output, i.e. ρ, η ∈ uco(C) with ρ ≠ η. Whenever f : C → C and ρ = η, the above definition of completeness boils down to the equation ρ ∘ f = ρ ∘ f ∘ ρ considered in [7, 12]. Also, it would not be too difficult (although notationally heavy) to develop the whole theory by considering semantic functions of type C^{n} → D^{m}.

For any given set of functions F ⊆ C ⟶^{m}D, we will use the following helpful nota-

tion: Γ(C, D, F) =^{def} {⟨ρ, η⟩ ∈ uco(C) × uco(D) | ∀f ∈ F. η ∘ f = η ∘ f ∘ ρ}. Whenever

F = {f}, we simply write Γ(C, D, f). The following result lists some interesting properties of completeness, where points (i)–(iii) generalize an analogous result given in [12].

Proposition 3.2

(i) ⟨λx.x, η⟩, ⟨ρ, λx.⊤_{D}⟩ ∈ Γ(C, D, F). (ii) ∀d ∈ D. Γ(C, D, λx.d) = uco(C) × uco(D). (iii) If ⟨ρ, η⟩ ∈ Γ(C, D, f) and ⟨η, μ⟩ ∈ Γ(D, E, g) then ⟨ρ, μ⟩ ∈ Γ(C, E, g ∘ f). (iv) If ⟨ρ, η⟩ ∈ Γ(C, D, F), δ ⊑ ρ and β ⊒ η, then ⟨δ, β⟩ ∈ Γ(C, D, F).

Given F ⊆ C ⟶^{m}D and η ∈ uco(D), let us now introduce the following operators transforming abstract domains of C (as usual, we follow the standard conventions ⊓∅ = ⊤_{uco(C)} and ⊔∅ = ⊥_{uco(C)}).

– K_{F}^{η} (ρ) =^{def} ⊓ {φ ∈ uco(C) | ρ ⊑ φ, ⟨φ, η⟩ ∈ Γ(C, D, F)};

– E_{F}^{η} (ρ) =^{def} ⊔ {φ ∈ uco(C) | φ ⊑ ρ, ⟨φ, η⟩ ∈ Γ(C, D, F)}.

Also, given ρ ∈ uco(C), analogous operators K_{F}^{ρ} and E_{F}^{ρ} of type uco(D) → uco(D) are introduced. Thus, e.g., E_{F}^{η} (ρ) is the least common abstraction of all the domains φ more concrete than ρ and such that ⟨φ, η⟩ is complete for F. As a consequence of Proposition 3.2 (iv), one can draw the following two important remarks: (i) If ⟨K_{F}^{η} (ρ), η⟩ ∈ Γ(C, D, F) then K_{F}^{η} (ρ) = ρ; (ii) If ⟨ρ, E_{F}^{ρ} (η)⟩ ∈ Γ(C, D, F) then E_{F}^{ρ} (η) = η. This means that it does not make sense to search for the greatest restriction ρ^{g} of ρ ∈ uco(C) such that ⟨ρ^{g}, η⟩ is complete, and, dually, the least extension η^{l} of η ∈ uco(D) such that ⟨ρ, η^{l}⟩ is complete, because either they coincide with their arguments or they do not exist. That is why we introduce just the following notions.

Definition 3.3 If ⟨ρ, K_{F}^{ρ} (η)⟩ ∈ Γ(C, D, F) then K_{F}^{ρ} (η) is called the complete kernel of η relative to ρ. Dually, if ⟨E_{F}^{η} (ρ), η⟩ ∈ Γ(C, D, F) then E_{F}^{η} (ρ) is called the least complete extension of ρ relative to η. □

As far as complete kernels are concerned, it is an easy task to show that they always exist, although no explicit characterization can be given.

Proposition 3.4 Let F ⊆ C ⟶^{m}D, ρ ∈ uco(C) and η ∈ uco(D). There exists the complete kernel of η relative to ρ.

Let us now consider the case where C = D and ρ = η. It is important to remark that if ⟨E_{F}^{ρ} (ρ), ρ⟩ ∈ Γ(C, C, F), then E_{F}^{ρ} (ρ) is the most abstract among the domains φ ⊑ ρ such that ρ ∘ f = ρ ∘ f ∘ φ. Thus, we stress that ρ thought of as output abstraction is considered fixed. We will see in Section 5 how this concept can be usefully exploited. Moreover, let us recall that in Giacobazzi and Ranzato’s approach [12], the least complete extension of ρ, when it exists, is instead defined as the most abstract among the domains φ ⊑ ρ such that φ ∘ f = φ ∘ f ∘ φ. Hence, by defining E_{F} (ρ) =^{def} ⊔{φ ∈ uco(C) | φ ⊑ ρ, ⟨φ, φ⟩ ∈ Γ(C, C, F)}, this latter least complete extension exists whenever ⟨E_{F} (ρ), E_{F} (ρ)⟩ ∈ Γ(C, C, F). Therefore, in this case, ρ considered as output abstraction is not fixed. Thus, we remark that this latter concept of least complete extension is different from that introduced in Definition 3.3. In the next section, we will study both these interesting notions. In order to distinguish them, when ⟨E_{F} (ρ), E_{F} (ρ)⟩ ∈ Γ(C, C, F), we will call E_{F} (ρ) the absolute least complete extension of ρ. Moreover, analogous dual considerations hold for complete kernels: We will call them absolute complete kernels.

4 Constructive Characterization of Completeness

The following key result characterizes complete abstract interpretations in a “constructive” way: In fact, it shows that a completeness equation η ∘ f = η ∘ f ∘ ρ holds iff ρ contains a certain set of points depending on η, and, in a dual fashion, iff η is contained in a certain set of points which depends on ρ. The proof makes use of a variant of the axiom of choice, known as Hausdorff’s Maximal Principle [2, pag. 192]. We will exploit largely the following compact notation: For any f : C → D and y ∈ D,

H_{y}^{f} =^{def} {x ∈ C | f(x) ≤ y}.

Theorem 4.1 Let F ⊆ C ⟶^{c}D, ρ ∈ uco(C) and η ∈ uco(D). Then,

⟨ρ, η⟩ ∈ Γ(C, D, F) ⇔ η ⊆ {y ∈ D | ∪_{f∈F} max(H_{y}^{f}) ⊆ ρ} ⇔ ∪_{f∈F,y∈η}max(H_{y}^{f}) ⊆ ρ. Moreover, {y ∈ D | ∪_{f∈F} max(H_{y}^{f}) ⊆ ρ} ∈ uco(D).

It is then useful to observe that, for any arbitrary set of points S and any uco ρ, the following equivalence holds: S ⊆ ρ ⇔ ρ ⊑ M(S). Thus, as the above theorem suggests, given any set of continuous functions F ⊆ C ⟶^{c}D, we define two mappings L_{F} : uco(C) → uco(D) and R_{F} : uco(D) → uco(C) as follows:

L_{F} (ρ) =^{def} {y ∈ D | ∪_{f∈F} max(H_{y}^{f}) ⊆ ρ}; R_{F} (η) =^{def} M(∪_{f∈F,y∈η}max(H_{y}^{f})).

In this way, Theorem 4.1 can be restated as follows:

⟨ρ, η⟩ ∈ Γ(C, D, F) ⇔ L_{F} (ρ) ⊑ η ⇔ ρ ⊑ R_{F} (η).

In particular, (L_{F} , uco(C), uco(D), R_{F}) is an adjunction. Consequently, for any ρ ∈ uco(C) and η ∈ uco(D), one gets the following characterizations for the operators K_{F}^{ρ} and E_{F}^{η}:

– K_{F}^{ρ} (β) = ⊓{μ ∈ uco(D) | β, L_{F} (ρ) ⊑ μ} = β ⊔ L_{F} (ρ);

– E_{F}^{η} (δ) = ⊔{φ ∈ uco(C) | φ ⊑ δ, R_{F} (η)} = δ ⊓ R_{F} (η).

Hence, since L_{F} (ρ) ⊑ β ⊔ L_{F} (ρ) and δ ⊓ R_{F} (η) ⊑ R_{F} (η), by Theorem 4.1, we obtain that ⟨ρ, β ⊔ L_{F} (ρ)⟩, ⟨δ ⊓ R_{F} (η), η⟩ ∈ Γ(C, D, F), and therefore, according to Definition 3.3, we can draw the following consequences:

– The complete kernel of η rel. to ρ is the least common abstraction of η and L_{F} (ρ);

– The least complete extension of ρ rel. to η is the reduced product of ρ and R_{F} (η).

For any ρ ∈ uco(C) and η ∈ uco(D), it is helpful to define two dual mappings F_{F}^{ρ} : uco(D) → uco(C) and G_{F}^{η} : uco(C) → uco(D) as follows:

F_{F}^{ρ} (μ) =^{def} ρ ⊓ R_{F} (μ); G_{F}^{η} (φ) =^{def} η ⊔ L_{F} (φ).

Summing up, we have shown the following result, which explicitly states what one must add to ρ in order to get its least complete extension relative to η and, dually, what one must subtract from η in order to get its complete kernel relative to ρ.

Theorem 4.2 Let F ⊆ C ⟶^{c}D, ρ ∈ uco(C) and η ∈ uco(D).

– F_{F}^{ρ} (η) = M(ρ ∪ (∪_{f∈F,y∈η}max(H_{y}^{f}))) is the least complete extension of ρ rel. to η;

– G_{F}^{η} (ρ) = η ∩ {y ∈ D | ∪_{f∈F} max(H_{y}^{f}) ⊆ ρ} is the complete kernel of η rel. to ρ.

Example 4.3 Consider the example sketched in Section 1. Let ρ ∈ uco(P(ℕ_{⊥} × ℕ_{⊥})) be the uco associated to the input abstract domain S × S, and η ∈ uco(P(Bool_{⊥})) be the uco associated to the output abstract domain S. Therefore, ρ = {{⟨⊥, ⊥⟩}, {⊥} × ℕ_{⊥}, ℕ_{⊥} × {⊥}, ℕ_{⊥} × ℕ_{⊥}} and η = {{⊥}, Bool_{⊥}}. The semantic function f is obviously continuous and hence, by Theorem 4.2, the least complete extension of ρ for f relative to η does exist, and it is given by the reduced product F_{f}^{ρ}(η) = ρ ⊓ R_{f} (η). Thus, for y ∈ η, let us compute max(H_{y}^{f}). We have that:

– max(H_{Bool_{⊥}}^{f}) = {ℕ_{⊥} × ℕ_{⊥}};

– max(H_{{⊥}}^{f}) = max({Z ∈ P(ℕ_{⊥} × ℕ_{⊥}) | f(Z) ⊆ {⊥}}) = max({Z ∈ P(ℕ_{⊥} × ℕ_{⊥}) | ⟨3, 3⟩ ∉ Z} = {(ℕ_{⊥} × ℕ_{⊥}) \ {⟨3, 3⟩}}.

Hence, F_{F}^{ρ} (η) = M(ρ ∪ {(ℕ_{⊥} × ℕ_{⊥}) \ {⟨3, 3⟩}}) = ρ ∪ {(ℕ_{⊥} × ℕ_{⊥}) \ {⟨3, 3⟩}}. Thus, as announced in Section 1, and as one naturally expects, this shows that the least complete extension of S × S can be obtained by adding a point ⟨≠, ≠⟩ with concrete meaning (ℕ_{⊥} ×ℕ_{⊥})\{⟨3, 3⟩}, i.e. denoting that first and second components are surely not simultaneously equal to the value 3. It should be clear that this refined input abstract domain induces now a complete abstract interpretation. □

Let us now turn to absolute complete kernels and absolute least complete extensions, as formally introduced at the end of Section 3. What follows generalizes the results in [12, Section 6], where the hypothesis consisted of dealing with additive semantic functions. Assume that C = D, i.e. F ⊆ C ⟶^{c}C, and let ρ ∈ uco(C). By Theorem 4.1, for any φ ∈ uco(C), we have that:

– φ ⊑ F_{F}^{ρ} (φ) ⇔ φ ⊑ ρ and ⟨φ, φ⟩ ∈ Γ(C, C, F);

– G_{F}^{ρ} (φ) ⊑ φ ⇔ ρ ⊑ φ and ⟨φ, φ⟩ ∈ Γ(C, C, F).

Therefore, for the operator E_{F} introduced at the end of Section 3, we obtain that E_{F} (ρ) = ⊔{φ ∈ uco(C) | φ ⊑ F_{F}^{ρ} (φ)}. Then, since F_{F}^{ρ} : uco(C) → uco(C) is clearly monotone for any ρ, and hence admits the greatest fixpoint, we get E_{F} (ρ) = gfp(F_{F}^{ρ}). Moreover, by Theorem 4.2, ⟨gfp(F_{F}^{ρ}), gfp(F_{F}^{ρ})⟩ ∈ Γ(C, C, F). This means that the absolute least complete extension of ρ exists, and it is gfp(F_{F}^{ρ}). Dual considerations hold for complete kernels. Thus, we get the following constructive characterization for absolute completeness.

Theorem 4.4 Let F ⊆ C ⟶^{c}C and ρ ∈ uco(C). Then, gfp(F_{F}^{ρ}) and lfp(G_{F}^{ρ}) are, resp., the absolute least complete extension and absolute complete kernel of ρ.

5 Generalized Quotients of Abstract Interpretations

The concept of quotient of an abstract interpretation has been recently introduced by Cortesi et al. [4] in order to formalize the least amount of information of a complex abstract domain A that is useful for computing some property that A is able to represent. Cortesi et al. [4] show how to exploit this notion for comparing the precision of two abstract interpretations in computing a given common property. Notably, they compare the well-known Jacobs and Langen Sharing [13] and Marriott and Søndergaard Pos [14] Prolog abstract interpretations, by demonstrating that Pos is strictly more precise than Sharing for computing variable groundness information. Further, Bagnara et al.

[1] show, also experimentally, that in order to compute pair-sharing information, the use of the quotient of Sharing w.r.t. the pair-sharing Søndergaard domain [19] leads to remarkable gains of efficiency, when compared with the full domain Sharing.

Let us recall from [4] the definition of quotient. Let A be any complete lattice, f : A⟶^{m}A be a monotone semantic function on A, and ρ ∈ uco(A) be an abstraction of A. Here, ⟨A, f⟩ models any abstract interpretation of some reference semantic definition, while ρ plays the rôle of the property (i.e. the abstraction of A) one is interested in. The equivalence relation r_{ρ} ⊆ A × A is defined as follows:^{1}

⟨a_{1}, a_{2}⟩ ∈ r_{ρ} iff ∀i ∈ ω. ρ(f^{i}(a_{1})) = ρ(f^{i}(a_{2})).

Roughly speaking, ⟨a_{1}, a_{2}⟩ ∈ r_{ρ} when A views a_{1} and a_{2} as “equivalent” w.r.t. the computation of the property ρ. Thus, according to this intuition, the quotient Q_{ρ}(A) of A w.r.t. ρ is defined (cf. [4, Definition 3.5]) as the subset of A of the lub’s of all equivalence classes of r_{ρ}: That is, if [a] denotes a generic equivalence class for r_{ρ}, then Q_{ρ}(A) =^{def} {∨[a] | a ∈ A}, and the ordering is that inherited from A. Cortesi et al. [4, Theorem 3.6] show that if the equivalence r_{ρ} is additive, i.e. ∀i ∈ I. ⟨a_{i}, b_{i}⟩ ∈ r_{ρ} ⇒ ⟨∨_{i∈I}a_{i}, ∨_{i∈I}b_{i}⟩ ∈ r_{ρ}, then Q_{ρ}(A) is well-defined, namely it is in turn an abstraction of A, i.e. the set of fixpoints of a uco on A, and ρ is an abstraction of Q_{ρ}(A).

Cortesi et al.’s results can be sharpened as follows. Firstly, it is useful to recall (see [8, Section 6.3]) that, in general, given an equivalence relation R on a complete lattice L, R is additive iff λx. ∨_{L} [x]_{R} ∈ uco(L). Thus, the hypothesis that the equivalence relation r_{ρ} is additive is indeed equivalent to the fact that λa.∨[a] ∈ uco(A), i.e. that the quotient Q_{ρ}(A) is well-defined. In this case, that Q_{ρ}(A) ⊑ ρ (i.e. [4, Theorem 3.6 (ii)]) is an immediate consequence: In fact, if a = ρ(a) and b ∈ [a] then a = ρ(a) = ρ(f^{0}(a)) = ρ(f^{0}(b)) = ρ(b), and hence b ≤ a, i.e. ∨[a] = a.

En passant, we observe that the additivity of f is an obvious sufficient condition guaranteeing that the quotient exists. Actually, the quotients presented in [1, 4] exist just because the involved semantic functions are additive.

Lemma 5.1 If f : A⟶^{a}A and ρ ∈ uco(A) then Q_{ρ}(A) ∈ uco(A).

1 This definition considers the case of the first limit ordinal ω for practical purposes – a generalization to any (possibly transfinite) ordinal would be straightforward.

It turns out that the quotient abstract domain satisfies the following remarkable property of “minimality”: When a quotient Q_{ρ}(A) exists, if ϕ_{ρ} = λa. ∨ [a] ∈ uco(A) is the uco associated to Q_{ρ}(A), then ϕ_{ρ} is the most abstract solution in uco(A) of the system of equations {ρ ∘ f^{i} = ρ ∘ f^{i} ∘ ψ | i ∈ ω}.

Lemma 5.2 Let ρ ∈ uco(A) such that Q_{ρ}(A) ∈ uco(A). Then, ∀i ∈ ω. ρ ∘ f^{i} = ρ ∘ f^{i} ∘ Q_{ρ}(A), and for any ψ ∈ uco(A), ∀i ∈ ω. ρ ∘ f^{i} = ρ ∘ f^{i} ∘ ψ implies ψ ⊑ Q_{ρ}(A).

Since the system of equations {ρ ∘ f^{i} = ρ ∘ f^{i} ∘ ψ | i ∈ ω} is clearly equivalent to the system {ψ ⊑ ρ} ∪ {ρ ∘ f^{i} = ρ ∘ f^{i} ∘ ψ | i > 0}, the above lemma says that, when a quotient Q_{ρ}(A) exists (i.e. Q_{ρ}(A) ∈ uco(A)), it is characterized as follows:

Q_{ρ}(A) = ⊔{ψ ∈ uco(A) | ψ ⊑ ρ, ∀i > 0. ρ ∘ f^{i} = ρ ∘ f^{i} ∘ ψ}.

Of course, in the terminology of this paper, this means that when it exists, Q_{ρ}(A) is the least complete extension of ρ for the set of functions {f^{i}}_{i>0} relative to ρ itself. However, it may well happen that, for some A, f and ρ, such least complete extension exists, whilst the quotient Q_{ρ}(A) does not exist, as the following simple example shows.

Example 5.3 Let A be the lattice depicted in the figure. Also, let f : A → A be defined as f = {a ↦ a, b ↦ a, c ↦ e, d ↦ e, e ↦ e}, and let ρ ∈ uco(A) such that

[figure: •; •; •; •; •; a; c; d; e; b]

ρ(A) = {a, b, e}. Trivially, f is monotone (and therefore continuous) but not additive. Moreover, f is idempotent, and therefore, for any i ≥ 1, f^{i} = f. It turns out that, for any i ≥ 1, ρ ∘ f^{i} = f. As a consequence, r_{ρ} is not an additive equivalence relation. In fact, for any i ≥ 0, ρ(f^{i}(c)) = ρ(f^{i}(d)): If i = 0 then, ρ(c) = ρ(d) = b; if i ≥ 1 then, ρ(f^{i}(c)) = f(c) = e = f(d) = ρ(f^{i}(d)). But, ρ(f(c ∨ d)) = ρ(f(b)) = f(b) = a. Hence, this means that

the quotient Q_{ρ}(A) does not exist. Instead, as each f^{i} is monotone, by Theorem 4.2, the least complete extension of ρ for {f^{i}}_{i>0} relative to ρ does exist. Moreover, this is given by the following reduced product: ρ ⊓ (∪_{i>0, y∈ρ}max(H_{y}^{f^{i}})). It is then a routine task to check that this is the domain A itself, i.e. the identity uco λx.x. □

Then, Lemma 5.2 and Example 5.3 hint to generalize the notion of quotient as the least complete extension of ρ for {f^{i}}_{i>0} relative to ρ, whenever this exists.

Definition 5.4 Given a complete lattice A, f : A⟶^{m}A, and ρ ∈ uco(A), the generalized quotient of A w.r.t. ρ is well-defined when there exists the least complete extension Φ_{ρ}(A) of ρ for {f^{i}}_{i>0} relative to ρ; in such a case, the generalized quotient is defined to be Φ_{ρ}(A). □

It is here worth noting that the above definition naturally extends the intuitive meaning of the concept of quotient: In fact, the abstract domain Φ_{ρ}(A) is the most abstract domain which is more concrete than the property ρ and which is as good as A for propagating the information through the semantic function f. In other words, Φ_{ρ}(A) encodes exactly the least amount of information of A that is useful for computing the property ρ. Thus, this exactly formalizes the clear intuition behind the concept of quotient. As an immediate consequence of Theorem 4.2, we are then able to give the following theorem ensuring that, when the semantic function f is continuous, generalized quotients always exist.

Theorem 5.5 If f : A⟶^{c}A then, for any ρ ∈ uco(A), the generalized quotient Φ_{ρ}(A) exists.

Acknowledgments. We wish to thank Enea Zaffanella for his helpful remarks on quotients of abstract interpretations and an anonymous referee for his/her useful comments. The work of Francesco Ranzato has been supported by an individual grant no. 202.12199 from Comitato 12 “Scienza e Tecnologie dell’Informazione” of Italian CNR.

References

1. R. Bagnara, P.M. Hill, and E. Zaffanella. Set-sharing is redundant for pair-sharing. In Proc. 4th Int. Static Analysis Symp., LNCS 1302:53–67, 1997.

2. G. Birkhoff. Lattice Theory. AMS Colloq. Publications vol. XXV, 3rd ed., 1967.

3. G.L. Burn, C. Hankin, and S. Abramsky. Strictness analysis for higher-order functions. Sci. Comput. Program., 7:249–278, 1986.

4. A. Cortesi, G. Filé, and W. Winsborough. The quotient of an abstract interpretation. Theor. Comput. Sci., 202(1-2):163–192, 1998.

5. P. Cousot. Méthodes itératives de construction et d’approximation de points fixes d’opérateurs monotones sur un treillis, analyse sémantique des programmes. PhD thesis, Université Scientifique et Médicale de Grenoble, 1978.

6. P. Cousot. Completeness in abstract interpretation (Invited Lecture). In Proc. 1995 Joint Italian-Spanish Conference on Declarative Programming, pp. 37–38, 1995.

7. P. Cousot and R. Cousot. Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Proc. 4th ACM POPL, pp. 238–252, 1977.

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

9. P. Cousot and R. Cousot. Inductive definitions, semantics and abstract interpretation. In Proc. 19th ACM POPL, pp. 83–94, 1992.

10. P. Cousot and R. Cousot. Abstract interpretation of algebraic polynomial systems. In Proc. 6th AMAST Conf., LNCS 1349:138–154, 1997.

11. R. Giacobazzi and F. Ranzato. Refining and compressing abstract domains. In Proc. 24th ICALP, LNCS 1256:771–781, 1997.

12. R. Giacobazzi and F. Ranzato. Completeness in abstract interpretation: a domain perspective. In Proc. 6th AMAST Conf., LNCS 1349:231–245, 1997.

13. D. Jacobs and A. Langen. Static analysis of logic programs for independent ANDparallelism. J. Logic Program., 13(2-3):154–165, 1992.

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

15. A. Mycroft. Abstract interpretation and optimising transformations for applicative programs. PhD thesis, CST-15-81, Univ. of Edinburgh, 1981.

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

17. U.S. Reddy and S.N. Kamin. On the power of abstract interpretation. Computer Languages, 19(2):79–89, 1993.

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

19. H. Søndergaard. An application of abstract interpretation of logic programs: occur check reduction. In Proc. ESOP ’86, LNCS 213:327–338, 1986.

20. B. Steffen. Optimal data flow analysis via observational equivalence. In Proc. 14th MFCS Symp., LNCS 379:492–502, 1989.