Widening Operators for Powerset Domains^{⋆}

Roberto Bagnara^{1}, Patricia M. Hill^{2}, and Enea Zaffanella^{1}

1 Department of Mathematics, University of Parma, Italy

                     {bagnara,zaffanella}@cs.unipr.it

2 School of Computing, University of Leeds, UK

                          hill@comp.leeds.ac.uk

Abstract. The finite powerset construction upgrades an abstract domain by allowing for the representation of finite disjunctions of its elements. In this paper we define two generic widening operators for the finite powerset abstract domain. Both widenings are obtained by lifting any widening operator defined on the base-level abstract domain and are parametric with respect to the specification of a few additional operators. We illustrate the proposed techniques by instantiating our widenings on powersets of convex polyhedra, a domain for which no non-trivial widening operator was previously known.

1 Introduction

The design and implementation of effective, expressive and efficient abstract domains for data-flow analysis and model-checking is a very difficult task. For this reason, starting with [11], there continues to be strong interest in techniques that derive enhanced abstract domains by applying systematic constructions on simpler, existing domains. Disjunctive completion, direct product, reduced product and reduced power are the first and most famous constructions of this kind [11]; several variations of them as well as others constructions have been proposed in the literature.

Once the carrier of the enhanced abstract domain has been obtained by one of these systematic constructions, the abstract operations can be defined, as usual, as the optimal approximations of the concrete ones. While this completely solves the specification problem, it usually leaves the implementation problem with the designer and gives no guarantees about the efficiency (or even the computability) of the resulting operations. This motivates the importance of generic techniques whereby correct, even though not necessarily optimal, domain operations are derived automatically or semi-automatically from those of the domains the construction operates upon [8, 11, 18].

This paper focuses on the derivation of widening operators for a kind of disjunctive refinement we call finite powerset construction. As far as we know, this

⋆ This work has been partly supported by MURST projects “Aggregate- and Number-Reasoning for Computing: from Decision Algorithms to Constraint Programming with Multisets, Sets, and Maps” and “Constraint Based Verification of Reactive Systems.”

is the first time that the problem of deriving non-trivial, provably correct widening operators in a domain refinement is tackled successfully. We also present its specialization to finite powersets of convex polyhedra. Not only is this included to help the reader gain a better intuition regarding the underlying approach but also to provide a definitely non-toy instance that is practically useful for applications such as data-flow analysis and model checking. Sets of polyhedra are implemented in Polylib [24, 28] and its successor PolyLib [25], even though no widenings are provided. Sets of polyhedra, represented with Presburger formulas made available by the Omega library [23, 26], are used in the verifier described in [7]; there, an extrapolation operator (i.e., a widening without convergence guarantee) on sets of polyhedra is described. Another extrapolation operator is implemented in the automated verification tool described in [16], where sets of polyhedra are represented using the clp(q, r) constraint library [22].

The rest of the paper is structured as follows: Section 2 recalls the basic concepts and notations; Section 3 defines the finite powerset construction as a disjunctive refinement for any abstract domain that is a join-semilattice; Section 4 presents two distinct strategies for upgrading any widening for the baselevel domain into a widening for the finite powerset domain; Section 5 provides a technique for controlling the precision/efficiency trade-off of these widenings; Section 6 concludes. The proofs of all the stated results can be found in [5].

2 Preliminaries

For a set S, ℘(S) is the powerset of S, whereas ℘_{f}(S) is the set of all the finite subsets of S; the cardinality of S is denoted by # S. The first limit ordinal is denoted by ω. Let O be a set equipped with a well-founded ordering ‘≻’. If M and N are finite multisets over O, #(n, M) denotes the number of occurrences of n ∈ O in M and M ≫ N means that there exists j ∈ O such that #(j, M) > #(j, N) and, for each k ∈ O with k ≻ j, we have #(k, M) = #(k, N). The relation ‘≫’ is well-founded [17].

In this paper we will adopt the abstract interpretation framework proposed in [13, Section 7], where the correspondence between the concrete and the abstract domains is induced from a concrete approximation relation and a concretization function. Since we are not aiming at maximum generality, for the sole purpose of simplifying the presentation, we will consider a particular instance of the framework by assuming a few additional but non-essential domain properties.

The concrete domain is modeled as a complete lattice of semantic properties ⟨C, ⊑, ⊥, ⊤, ⊔, ⊓⟩; as usual, the concrete approximation relation c_{1} ⊑ c_{2} holds if c_{1} is a stronger property than c_{2} (i.e., c_{2} approximates c_{1}). The concrete semantics c ∈ C of a program is formalized as the least fixpoint of a continuous (concrete) semantic function F: C → C, which is iteratively computed starting from the bottom element, so that c = F^{ω}(⊥).

The abstract domain D̂ = ⟨D, ⊢, 0, ⊕⟩ is modeled as a join-semilattice (i.e., the least upper bound d_{1} ⊕ d_{2} exists for all d_{1}, d_{2} ∈ D). We will overload ‘⊕’ so that, for each S ∈ ℘_{f}(D), ⨁S denotes the least upper bound of S. The abstract domain D̂ is related to the concrete domain by a monotonic and injective concretization function γ: D → C. Monotonicity and injectivity mean that the abstract partial order ‘⊢’ is indeed the approximation relation induced on D by the concretization function γ. For all d_{1}, d_{2} ∈ D, we will use the notation d_{1} ⊩ d_{2} to mean that d_{1} ⊢ d_{2} and d_{1} ≠ d_{2}. We assume the existence of a monotonic abstract semantic function F^{♯}: D → D that is sound with respect to F: C → C:

∀c ∈ C : ∀d ∈ D : c ⊑ γ(d) ⟹ F(c) ⊑ γ(F^{♯}(d)).  (1)

This local correctness condition ensures that each concrete iterate can be safely approximated by computing the corresponding abstract iterate (starting from the bottom element 0 ∈ D). However, due to the weaker algebraic properties satisfied by the abstract domain, the abstract upward iteration sequence may not converge. Even when it converges, it may fail to do so in a finite number of steps, therefore being useless for the purposes of static analysis.

Widening operators [9, 10, 13, 14] provide a simple and general characterization for enforcing and accelerating convergence. We will adopt a minor variation of the classical definition of widening operator (see footnote 6 in [14, p. 275]).

Definition 1. (Widening.) Let ⟨D, ⊢, 0, ⊕⟩ be a join-semilattice. The partial operator ∇: D × D ↣ D is a widening if

1. d_{1} ⊢ d_{2} implies d_{2} ⊢ d_{1} ∇ d_{2} for each d_{1}, d_{2} ∈ D;

2. for each increasing chain d_{0} ⊢ d_{1} ⊢ ⋯, the increasing chain defined by d′_{0} := d_{0} and d′_{i+1} := d′_{i} ∇ (d′_{i} ⊕ d_{i+1}), for i ∈ ℕ, is not strictly increasing.

Any widening operator ‘∇’ induces a corresponding partial ordering ‘⊢_{∇}’ on the domain D; this is defined as the reflexive and transitive closure of the relation { (d_{1}, d) ∈ D × D | ∃d_{2} ∈ D . d_{1} ⊩ d_{2} ∧ d = d_{1} ∇ d_{2} }. The relation ‘⊢_{∇}’ satisfies the ascending chain condition. We write d_{1} ⊩_{∇} d_{2} to denote d_{1} ⊢_{∇} d_{2} ∧ d_{1} ≠ d_{2}.

It can be proved that the upward iteration sequence with widenings starting at the bottom element d_{0} := 0 and defined by

d_{i+1} := \begin{cases}d_{i}, & if F^{♯}(d_{i}) ⊢ d_{i}, \\ d_{i} ∇ (d_{i} ⊕ F^{♯}(d_{i})), & otherwise, \end{cases}

converges after a finite number j ∈ ℕ of iterations [14]. Note that the widening is always applied to arguments d = d_{i} and d′ = d_{i} ⊕ F^{♯}(d_{i}) satisfying d ⊩ d′. Also, when condition (1) holds, the post-fixpoint d_{j} ∈ D of F^{♯} is a correct approximation of the concrete semantics, i.e., F^{ω}(⊥) ⊑ γ(d_{j}).

2.1 The Abstract Domain of Polyhedra

We now instantiate the abstract interpretation framework sketched above by presenting the well-known abstract domain of closed convex polyhedra. This domain will be used throughout the paper to illustrate the generic widening techniques that will be defined.

Let ℝ^{n}, where n > 0, be the n-dimensional real vector space. The set P ⊆ ℝ^{n} is a closed and convex polyhedron (polyhedron, for short) if and only if P can be expressed as the intersection of a finite number of closed affine half-spaces of ℝ^{n}. The set ℂℙ_{n} of closed convex polyhedra on ℝ^{n}, when partially ordered by subset inclusion, is a lattice having the empty set and ℝ^{n} as the bottom and top elements, respectively; the binary meet operation is set-intersection, whereas the binary join operation, denoted by ‘⊎’, is called convex polyhedral hull (poly-hull, for short). Therefore, we have the abstract domain

ℂ̂ℙ_{n} := ⟨ℂℙ_{n}, ⊆, ∅, ℝ^{n}, ⊎, ∩⟩.

This domain can be related to several concrete domains, depending on the intended application. One example of a concrete domain is the complete lattice

Â_{n} := ⟨℘(ℝ^{n}), ⊆, ∅, ℝ^{n}, ∪, ∩⟩.

Note that ℂ̂ℙ_{n} is a meet-sublattice of Â_{n}, sharing the same bottom and top elements. Another example is the complete lattice B̂_{n} := ⟨℘_{c}(ℝ^{n}), ⊆, ∅, ℝ^{n}, ∪_{c}, ∩⟩, where ℘_{c}(ℝ^{n}) is the set of all topologically closed and convex subsets of ℝ^{n} and the join operation ‘∪_{c}’ returns the smallest topologically closed and convex set containing its arguments. As a final example of concrete domain for some analysis, consider the complete lattice Ĉ_{n} := ⟨℘(ℂℙ_{n}), ⊆, ∅, ℂℙ_{n}, ∪, ∩⟩.

The abstract domain ℂ̂ℙ_{n}, which is a join-semilattice, is related to the concrete domains shown above by the concretization functions γ^{A} : ℂℙ_{n} → ℘(ℝ^{n}), γ^{B} : ℂℙ_{n} → ℘_{c}(ℝ^{n}) and γ^{C} : ℂℙ_{n} → ℘(ℂℙ_{n}): for each P ∈ ℂℙ_{n}, we have both γ^{A}(P) := P and γ^{B}(P) := P, and γ^{C}(P) := ↓ P := { Q ∈ ℂℙ_{n} | Q ⊆ P }. All these concretization functions are trivially monotonic and injective.

For each choice of the concrete domain C ∈ {℘(ℝ^{n}), ℘_{c}(ℝ^{n}), ℘(ℂℙ_{n})}, the continuous semantic function F: C → C and the corresponding monotonic abstract semantic function F^{♯}: ℂℙ_{n} → ℂℙ_{n}, which is assumed to be correct, are deliberately left unspecified. The domain ℂ̂ℙ_{n} contains infinite ascending chains having no least upper bound in ℂℙ_{n}. Thus, the convergence of the abstract iteration sequence has to be guaranteed by the adoption of widening operators.

The first widening on polyhedra was introduced in [15] and refined in [19]. This operator, denoted by ‘∇_{s}’, has been termed standard widening and used almost universally. In [4], we presented a framework designed so that all its instances are widening operators on ℂℙ_{n}. The standard widening ‘∇_{s}’ is an instance of the framework and all the other instances, including the specific widening ‘ ˆ∇’ defined and experimentally evaluated in [4], are at least as precise as ‘∇_{s}’. For a formal definition of both ‘∇_{s}’ and ‘ ˆ∇’, we refer the reader to [4].

3 A Disjunctive Refinement

In this section, we present the finite powerset operator, which is a domain refinement similar to disjunctive completion [11] and is obtained by a variant of the down-set completion construction presented in [12]. The following notation and definitions are mainly borrowed from [2, Section 6].

Definition 2. (Non-redundancy.) Let D̂ = ⟨D, ⊢, 0, ⊕⟩ be a join-semilattice. The set S ∈ ℘(D) is called non-redundant with respect to ‘ ⊢’ if and only if 0 ∉ S and ∀d_{1}, d_{2} ∈ S : d_{1} ⊢ d_{2} ⟹ d_{1} = d_{2}. The set of finite non-redundant subsets of D (with respect to ‘ ⊢’) is denoted by ℘_{fn}(D, ⊢). The reduction function Ω_{D}^{⊢}: ℘_{f}(D) → ℘_{fn}(D, ⊢) mapping each finite set into its non-redundant counterpart is defined, for each S ∈ ℘_{f}(D), by

Ω_{D}^{⊢}(S) := S \ { d ∈ S | d = 0 ∨ ∃d′ ∈ S . d ⊩ d′ }.

The restriction to the finite subsets reflects the fact that here we are mainly interested in an abstract domain where disjunctions are implemented by explicit collections of elements of the base-level abstract domain.

Definition 3. (Finite powerset domain.) Let D̂ := ⟨D, ⊢, 0, ⊕⟩ be a joinsemilattice. The finite powerset domain over D̂ is the join-semilattice

D̂_{P} := ⟨℘_{fn}(D, ⊢), ⊢_{P}, 0_{P}, ⊕_{P}⟩,

where 0_{P} := ∅ and, for all S_{1}, S_{2} ∈ ℘_{fn}(D, ⊢), S_{1} ⊕_{P} S_{2} := Ω_{D}^{⊢}(S_{1} ∪ S_{2}).

The approximation ordering ‘⊢_{P}’ induced by ‘⊕_{P}’ is the Hoare powerdomain partial order [1], so that S_{1} ⊢_{P} S_{2} if and only if ∀d_{1} ∈ S_{1} : ∃d_{2} ∈ S_{2} . d_{1} ⊢ d_{2}. A sort of Egli-Milner partial order relation [1] will also be useful: S_{1} ⊢_{EM} S_{2} holds if and only if either S_{1} = 0_{P} or S_{1} ⊢_{P} S_{2} and ∀d_{2} ∈ S_{2} : ∃d_{1} ∈ S_{1} . d_{1} ⊢ d_{2}. An (Egli-Milner) connector for D̂_{P}, denoted by ‘ ⊞_{EM}’ is any upper bound operator for the Egli-Milner ordering on ℘_{fn}(D, ⊢). Note that although a least upper bound for ‘⊢_{EM}’ may not exist, a connector can always be defined; for instance, we can let S_{1} ⊞_{EM} S_{2} := {⨁(S_{1} ∪ S_{2})}.

Besides the requirement on finiteness, another difference with respect to the down-set completion of [12] is that we are dropping the assumption about the complete distributivity of the concrete domain. This is possible because our semantic domains are not necessarily related by Galois connections, so that this property does not have to be preserved.

The finite powerset domain is related to the concrete domain by means of the concretization function γ_{P} : ℘_{fn}(D, ⊢) → C defined by

γ_{P}(S) := ⨆{ γ(d) | d ∈ S }.

Note that γ_{P} is monotonic but not necessarily injective. For S_{1}, S_{2} ∈ ℘_{fn}(D, ⊢), we write S_{1} ≡_{γ_{P}} S_{2} to denote that the two abstract elements actually denote the same concrete element, i.e., when γ_{P}(S_{1}) = γ_{P}(S_{2}). It is easy to see that ‘≡_{γ_{P}}’ is a congruence relation on D̂_{P}. As noted in [12], non-redundancy only provides a partial, syntactic form of reduction. On the other hand, requiring the full, semantic form of reduction for a finite powerset domain can be computationally very expensive.

A correct abstract semantic function F ♯_{P} : ℘_{fn}(D, ⊢) → ℘_{fn}(D, ⊢) on the finite powerset domain may be provided by an ad-hoc definition. More often, if the concrete semantic function F: C → C satisfies suitable hypotheses, F ♯_{P} can be safely induced from the abstract semantic function F^{♯}: D → D. For instance, if F is additive, we can define F ♯_{P} as follows [11, 18]:

F ♯_{P}(S) := Ω_{D}^{⊢}({ F^{♯}(d) | d ∈ S }).

3.1 The Finite Powerset Domain of Polyhedra

The polyhedral domain (ℂ̂ℙ_{n})_{P}, having carrier ℘_{fn}(ℂℙ_{n}, ⊆), is the finite powerset domain over ℂ̂ℙ_{n}. The approximation ordering is ‘⊆_{P}’ where, for each S_{1}, S_{2} ∈ ℘_{fn}(ℂℙ_{n}, ⊆),

S_{1} ⊆_{P} S_{2} ⟺ ∀P_{1} ∈ S_{1} : ∃P_{2} ∈ S_{2} . P_{1} ⊆ P_{2}.

Let γ_{P}^{A}, γ_{P}^{B} and γ_{P}^{C} denote the (powerset) concretization functions induced by γ^{A}, γ^{B} and γ^{C}, respectively. Then, the relation ‘≡_{γ_{P}^{A}}’ makes two finite sets of polyhedra equivalent if and only if they have the same set-union. The general problem of deciding the semantic equivalence with respect to γ_{P}^{A} of two finite (non-redundant) collections of polyhedra is known to be computationally hard [27]. For γ_{P}^{B}, the relation ‘≡_{γ_{P}^{B}}’ makes two finite sets of polyhedra equivalent if and only if they have the same poly-hull, so that the powerset construction provides no benefit at all. Finally, γ_{P}^{C} is injective so that ‘≡_{γ_{P}^{C}}’ coincides with the identity congruence relation.

Example 1. For the polyhedral domain (ℂ̂ℙ_{1})_{P}, let^{3}

T_{0} := {{0 ≤ x ≤ 2}, {1 ≤ x ≤ 2}, {3 ≤ x ≤ 4}, {4 ≤ x ≤ 5}},
T_{1} := {{0 ≤ x ≤ 2}, {3 ≤ x ≤ 4}, {4 ≤ x ≤ 5}},
T_{2} := {{0 ≤ x ≤ 1}, {1 ≤ x ≤ 2}, {3 ≤ x ≤ 5}}.

Then T_{0} ∉ ℘_{fn}(ℂℙ_{1}, ⊆), but T_{1} = Ω_{ℂℙ_{1}}^{⊆}(T_{0}) ∈ ℘_{fn}(ℂℙ_{1}, ⊆). Also, T_{1} ≡_{γ_{P}^{A}} T_{2}.

4 Widening the Finite Powerset Domain

If the domain refinement of the previous section is meant to be used for static analysis, then a key ingredient that is still missing is a systematic way of ensuring the termination of the analysis. In this section, we describe two widening strategies that rely on the existence of a widening ∇: D × D ↣ D on the base-level abstract domain.^{4} We start by proposing a general specification of an extrapolation operator that lifts this ‘∇’ operator to the powerset domain.

3 In this and the following examples, a polyhedron P ∈ ℂℙ_{n} will be denoted by a

corresponding finite set of linear equality and non-strict inequality constraints. 4 If the base-level abstract domain D̂ is finite or Noetherian, so that it is not necessarily

endowed with an explicit widening operator, then a dummy widening can be obtained by considering the least upper bound operator ‘⊕’.

Definition 4. (The ∇-connected extrapolation heuristics.) A partial operator h∇_{P} : ℘_{fn}(D, ⊢)^{2} ↣ ℘_{fn}(D, ⊢) is a ∇-connected extrapolation heuristics for D̂_{P} if, for all S_{1}, S_{2} ∈ ℘_{fn}(D, ⊢) such that S_{1} ⊩_{P} S_{2}, h∇_{P}(S_{1}, S_{2}) is defined and satisfies the following conditions:

S_{2} ⊢_{EM} h∇_{P}(S_{1}, S_{2});  (2)
∀d ∈ h∇_{P}(S_{1}, S_{2}) \ S_{2} : ∃d_{1} ∈ S_{1} . d_{1} ⊩_{∇} d;  (3)
∀d ∈ h∇_{P}(S_{1}, S_{2}) ∩ S_{2} : ((∃d_{1} ∈ S_{1} . d_{1} ⊩ d) → (∃d′_{1} ∈ S_{1} . d′_{1} ⊩_{∇} d)). (4)

Informally, condition (2) ensures that the result is an upper approximation of S_{2} in which every element covers at least one element of S_{2} (i.e., the heuristics cannot add elements that are unrelated to S_{2}); conditions (3) and (4) ensure that in the resulting set, each element covering an element of S_{1} originates from an application of ‘∇’ to a (possibly different) element of S_{1}.

It is straightforward to construct an algorithm for computing a ∇-connected extrapolation heuristics for any given base-level widening ‘∇’.

Proposition 1. For all S_{1}, S_{2} ∈ ℘_{fn}(D, ⊢) such that S_{1} ⊢_{P} S_{2}, let

h∇_{P}(S_{1}, S_{2}) := S_{2} ⊕_{P} Ω_{D}^{⊢}({ d_{1} ∇ d_{2} ∈ D | d_{1} ∈ S_{1}, d_{2} ∈ S_{2}, d_{1} ⊩ d_{2} }).

Then ‘ h∇_{P}’ is a ∇-connected extrapolation heuristics for D̂_{P}.

For the finite powerset domain over ℂ̂ℙ_{n}, lines 10–15 of the algorithm specified in [7, Figure 8, page 773] provide an implementation of the heuristics ‘h∇_{P}’ defined in Proposition 1, instantiated with the standard widening, ‘∇_{s}’, on ℂ̂ℙ_{n}.

Example 2. To see that the ‘h∇_{P}’ defined in Proposition 1 is not a widening for (ℂ̂ℙ_{n})_{P}, consider the strictly increasing sequence T_{0} ⊆_{P} T_{1} ⊆_{P} ⋯ in ℂℙ_{1} defined by T_{j} := { P_{i} | 0 ≤ i ≤ j }, where P_{i} := {x = i}, for i ∈ ℕ. Then, no matter what the specification for ‘∇’ is, we obtain h∇_{P}(T_{j}, T_{j+1}) = T_{j+1}, for all j ∈ ℕ. Thus, the “widened” sequence is diverging.

4.1 Powerset Widenings Using Egli-Milner Connectors

Example 2 shows that, when computing h∇_{P}(S_{1}, S_{2}), divergence is caused by those elements of S_{2} that cover none of the elements occurring in S_{1}, i.e., when S_{1} ⊬_{EM} S_{2}. Thus, stabilization can be obtained by replacing S_{2} with S_{1} ⊞_{EM} S_{2}, where ‘ ⊞_{EM}’ is a connector for D̂_{P}. We therefore define a simple widening operator on the finite powerset domain that uses a connector to ensure termination.

Definition 5. (The ‘_{EM}∇_{P}’ widening.) Let ‘ h∇_{P}’ be a ∇-connected extrapolation heuristics and ‘ ⊞_{EM}’ be a connector for D̂_{P}. Let also S_{1}, S_{2} ∈ ℘_{fn}(D, ⊢), where S_{1} ⊩_{P} S_{2}. Then

S_{1} _{EM}∇_{P}S_{2} := h∇_{P}(S_{1}, S′_{2}), where S′_{2} := \begin{cases}S_{2}, & if S_{1} ⊢_{EM} S_{2}; \\ S_{1} ⊞_{EM} S_{2}, & otherwise. \end{cases}

Theorem 1. The ‘_{EM}∇_{P}’ operator is a widening on D̂_{P}.

Example 3. To illustrate the widening operator ‘_{EM}∇_{P}’ we consider the powerset domain (ℂ̂ℙ_{1})_{P}, with the standard widening ‘∇_{s}’ on ℂ̂ℙ_{1} and the trivial connector ‘⊎_{EM}’ returning the singleton poly-hull of its arguments. Consider the sequence T_{0} ⊆_{P} T_{1} ⊆_{P} ⋯ of Example 2 and the widened sequence U_{0} ⊆_{P} U_{1} ⊆_{P} ⋯ where U_{0} = T_{0} and U_{i} = U_{i−1} _{EM}∇_{P}(U_{i−1} ⊎_{P} T_{i}), for each i > 0. When computing U_{1}, the second argument of the widening is U_{0} ⊎_{P} T_{1} = T_{1}. Note that U_{0} ⊢_{EM} T_{1} does not hold so that the connector is needed. Thus, we obtain

U_{1} = h∇_{P}(U_{0}, U_{0} ⊎_{EM} T_{1}) = h∇_{P}(U_{0}, {{0 ≤ x ≤ 1}}) = {{0 ≤ x}}.

In the next iteration we obtain stabilization. Clearly, in general the precision of this widening will depend on the chosen connector operator.

For the polyhedral domain ℂ̂ℙ_{n}, the powerset widening ‘_{EM}∇_{P}’ using the ‘h∇_{P}’ heuristics defined in Proposition 1 is similar to but not quite the same as the operator sketched in [7]. As noted in that paper, the algorithm in [7, Figure 8, page 773] cannot ensure the termination of the analysis. To this end, instead of using a connector operator it is proposed that, when the cardinality of the abstract collection reaches a fixed threshold, a further poly-hull approximation be applied. However, there are examples indicating that such an approach cannot come with a termination guarantee when considering arbitrary increasing sequences [5].

4.2 Powerset Widenings Using Finite Convergence Certificates

We now present another widening operator (denoted here by ‘_{μ}∇_{P}’) for the finite powerset domain. This requires that the operator ‘∇’ defined on the base-level domain is provided with a (finitely computable) finite convergence certificate. Formally, a finite convergence certificate for ‘∇’ (on D̂) is a triple (O, ≻, μ) where (O, ≻) is a well-founded ordered set and μ: D → O, which is called level mapping, is such that, for all d_{1} ⊩ d_{2} ∈ D, μ(d_{1}) ≻ μ(d_{1} ∇ d_{2}). We will abuse notation by writing μ to denote the certificate (O, ≻, μ).

Example 4. For the polyhedral domain ℂ̂ℙ_{n} and the standard widening ‘∇_{s}’, we can define a certificate (O_{s}, ≻_{s}, μ_{s}) where O_{s} is the pair (ℕ, ℕ), ‘≻_{s}’ the lexicographic ordering of the pair using > for the individual ordering of the components and μ_{s}: ℂℙ_{n} → O_{s} the level mapping μ_{s}(P) = (n − dim(P), k), where dim(P) is the dimension of P and k the minimal number of half-spaces needed to define P. Similarly, a certificate for the widening ‘ ˆ∇’ on ℂ̂ℙ_{n} proposed in [4] can be obtained by considering the level mapping μ_{b}: ℂℙ_{n} → O_{b} induced by the limited growth ordering relation ‘↷’ defined in [4], so that we have μ_{b}(P_{1}) ≻_{b} μ_{b}(P_{2}) if and only if P_{1} ↷ P_{2}. For lack of space, we refer the reader to [4].

Given a certificate for ‘∇’, we can define a suitable limited growth ordering relation ‘↷_{P}’ for the finite powerset domain D̂_{P} that satisfies the ascending chain condition.

Definition 6. (The ‘↷_{P}’ relation.) The relation ↷_{P} ⊆ ℘_{fn}(D, ⊢) × ℘_{fn}(D, ⊢) induced by the certificate μ for ‘ ∇’ is such that, for each S_{1}, S_{2} ∈ ℘_{fn}(D, ⊢), S_{1} ↷_{P} S_{2} if and only if either one of the following conditions holds:

μ(⨁S_{1}) ≻ μ(⨁S_{2});  (5)
μ(⨁S_{1}) = μ(⨁S_{2}) ∧ # S_{1} > 1 ∧ # S_{2} = 1;  (6)
μ(⨁S_{1}) = μ(⨁S_{2}) ∧ # S_{1} > 1 ∧ # S_{2} > 1 ∧ μ̃(S_{1}) ≫ μ̃(S_{2})  (7)

where, for each S ∈ ℘_{fn}(D, ⊢), μ̃(S) denotes the multiset over O obtained by applying μ to each abstract element in S.

Proposition 2. The ‘ ↷_{P}’ relation satisfies the ascending chain condition.

Intuitively, the relation ‘↷_{P}’ will induce a certificate μ_{P} : D̂_{P} → O_{P} for the new widening. Namely, by defining μ_{P}(S_{1}) ≻_{P} μ_{P}(S_{2}) if and only if S_{1} ↷_{P} S_{2}, we will obtain μ_{P}(S_{1}) ≻_{P} μ_{P}(S_{1} _{μ}∇_{P}S_{2}).

The specification of our “certificate-based widening” assumes the existence of a subtract operation for the base-level domain. It is expected that a specific subtraction would be provided for each domain; here we just indicate a minimal specification.

Definition 7. (Subtraction.) The partial operator ⊖: D × D ↣ D is a subtraction for D̂ if, for all d_{1}, d_{2} ∈ D such that d_{2} ⊢ d_{1}, we have d_{1} ⊖ d_{2} ⊢ d_{1} and d_{1} = (d_{1} ⊖ d_{2}) ⊕ d_{2}.

A trivial subtraction operator can always be defined as d_{1} ⊖ d_{2} := d_{1}.

Example 5. In ℂ̂ℙ_{n}, the function diff : ℂℙ_{n} × ℂℙ_{n} → ℂℙ_{n} is defined so that, for any P, Q ∈ ℂℙ_{n}, diff(P, Q) denotes the smallest closed and convex polyhedron containing the set difference P \ Q. Then, if Q ⊆ P, we have diff(P, Q) ⊆ P and

P = (P \ Q) ∪ Q = diff(P, Q) ∪ Q = diff(P, Q) ⊎ Q,

so that ‘diff’ is a subtraction.

We can now define the certificate-based widening ‘_{μ}∇_{P}’.

Definition 8. (The ‘_{μ}∇_{P}’ widening.) Let ‘ ↷_{P}’ be the limited growth ordering induced by the certificate μ for ‘ ∇’ and let ‘ ⊞_{P}’ be any upper bound operator on D̂_{P}. Let S_{1}, S_{2} ∈ ℘_{fn}(D, ⊢) be such that S_{1} ⊩_{P} S_{2}. Also, if ⨁S_{1} ⊩ ⨁(S_{1} ⊞_{P} S_{2}), let d ∈ D be defined as d := (⨁S_{1} ∇ ⨁(S_{1} ⊞_{P} S_{2})) ⊖ (⨁(S_{1} ⊞_{P} S_{2})). Then

S_{1} _{μ}∇_{P}S_{2} := \begin{cases}S_{1} ⊞_{P} S_{2}, & if S_{1} ↷_{P} S_{1} ⊞_{P} S_{2}; \\ (S_{1} ⊞_{P} S_{2}) ⊕_{P} \{d\}, & if ⨁S_{1} ⊩ ⨁(S_{1} ⊞_{P} S_{2}); \\ \{⨁S_{2}\}, & otherwise. \end{cases}

In the first case, we simply return the upper bound S_{1} ⊞_{P} S_{2}, since this is enough to ensure a strict decrease in the level mapping. In the second case, the join of S_{1} is strictly more precise than the join of S_{1} ⊞_{P} S_{2}, so that we apply ‘∇’ to them and then, using the subtraction operator, improve the obtained result, since S_{1} ↷_{P} (S_{1} ⊞_{P} S_{2}) ⊕_{P} {d} holds. In the last case, since the join of S_{1} ⊞_{P} S_{2} is invariant, we return the singleton consisting of the join itself, as originally proposed in [11, Section 9].

Theorem 2. The ‘_{μ}∇_{P}’ operator is a widening on D̂_{P}.

Example 6. To illustrate the last two cases of Definition 8, consider the domain (ℂ̂ℙ_{1})_{P} with the standard widening ‘∇_{s}’ for ℂ̂ℙ_{1} certified by the level mapping μ_{s} defined in Example 4 and the upper bound operator ‘⊞_{P}’ defined as ‘⊕_{P}’ so that S_{1} ⊞_{P} S_{2} = S_{2} always holds.

Let T_{1} = {{0 ≤ x ≤ 1}} and T_{2} = {{0 ≤ x ≤ 1}, {2 ≤ x ≤ 3}}. Then T_{1} ↷̸_{P} T_{2}, so that the condition for the first case in Definition 8 does not hold. The poly-hulls of T_{1} and T_{2} are {0 ≤ x ≤ 1} and {0 ≤ x ≤ 3}, respectively, so that the condition for the second case holds. Since ⨄ T_{1} ∇_{s} ⨄ T_{2} = {0 ≤ x}, then by letting the polyhedron P be the element d as specified in Definition 8, we obtain P = diff({0 ≤ x}, {0 ≤ x ≤ 3}) = {3 ≤ x}, so that

T_{1} _{μ}∇_{P}T_{2} = T_{2} ⊎_{P} {P} = {{0 ≤ x ≤ 1}, {2 ≤ x ≤ 3}, {3 ≤ x}}.

Now let T_{3} = {{x = 1}, {x = 3}} and T_{4} = {{x = 1}, {x = 2}, {x = 3}}. Then T_{3} ↷̸_{P} T_{4}, so that the condition for the first case in Definition 8 does not hold. Moreover, ⨄ T_{3} = ⨄ T_{4} = {1 ≤ x ≤ 3}, so that neither the second case applies. Thus, T_{3} _{μ}∇_{P}T_{4} = {{1 ≤ x ≤ 3}}.

As shown in the example above, Definition 8 does not require that the upper bound operator ‘⊞_{P}’ is based on the base-level widening ‘∇’. Moreover, the scheme of Definition 8 can be easily extended to any finite set of heuristically chosen upper bound operators on D̂_{P}, still obtaining a proper widening operator. The simplest heuristics, already used in the example above, is the one taking ⊞_{P} := ⊕_{P}. If this fails to ensure a decrease in the level mapping, another possibility is the adoption of a ∇-connected extrapolation heuristics ‘h∇_{P}’ for D̂_{P}. Anyway, many variations could be defined, depending on the required precision/efficiency trade-off. In the following section, we investigate one of these possibilities, which originates as a generalization of an idea proposed in [7].

5 Merging Elements According to a Congruence Relation

When computing a powerset widening S_{1} ∇_{P} S_{2}, no matter if it is based on an Egli-Milner connector or a finite convergence certificate, some of the elements occurring in the second argument S_{2} can be merged together (i.e., joined) without affecting the finite convergence guarantee. This merging operation can be guided by a congruence relation on the finite powerset domain D̂_{P}, the idea being that a well-chosen relation will benefit the precision/efficiency trade-off of the widening.

One option is to use semantics preserving congruence relations, i.e., refinements of the congruence relation ‘≡_{γ_{P}}’. The availability of relatively efficient but incomplete tests for semantic equivalence can thus be exploited to improve the efficiency and/or the precision of the analysis. As the purpose of this paper is to provide generic widening procedures for powersets that are independent of the underlying domains and hence, of any intended concretizations, here we define these congruences in a way that is independent of the particular concrete domain adopted. Two such relations are the identity congruence relation, where no nontrivial equivalence is assumed, and the ⊕-congruence relation, where sets that have the same join are equivalent. However, the identity congruence will have no influence on the convergence of the iteration sequence, while the ⊕-congruence is usually the basis of the default, roughest heuristics for ensuring termination. We now define a new congruence relation that lies between these extremes.

Definition 9. (‘◁’ and ‘▷◁’.) The content relation ◁ ⊆ ℘_{fn}(D, ⊢) × ℘_{fn}(D, ⊢) is such that S_{1} ◁ S_{2} holds if and only if for all S′_{1} ∈ ℘_{fn}(D, ⊢) where S′_{1} ⊢_{P} S_{1} there exists S′′_{1} ∈ ℘_{fn}(D, ⊢) such that ⨁S′_{1} = ⨁S′′_{1} and S′′_{1} ⊢_{P} S_{2}. The same-content relation ▷◁ ⊆ ℘_{fn}(D, ⊢) × ℘_{fn}(D, ⊢) is such that S_{1} ▷◁ S_{2} holds if and only if S_{1} ◁ S_{2} and S_{2} ◁ S_{1}.

Observe that the identity congruence relation can be obtained by strengthening the conditions in the definition of ‘◁’, replacing ⨁S′_{1} = ⨁S′′_{1} with S′_{1} = S′′_{1}; and the ⊕-congruence can be obtained by weakening the conditions, replacing S′′_{1} ⊢_{P} S_{2} with ⨁S′′_{1} ⊢ ⨁S_{2}. Thus the same-content relation is a compromise between keeping all the information provided by the explicit set structure, as done by the identity congruence, and losing all of this information, as occurs with the ⊕-congruence.

For the finite powerset domain of polyhedra (ℂ̂ℙ_{n})_{P}, the content relation ‘◁’ corresponds to the condition that all the points in polyhedra in the first set are contained by polyhedra in the second set; and hence, the same-content congruence relation ‘▷◁’ coincides with the induced congruence relation ‘≡_{γ_{P}^{A}}’.

Proposition 3. For all S_{1}, S_{2} ∈ ℘_{fn}(ℂℙ_{n}, ⊆), S_{1} ▷◁ S_{2} if and only if S_{1} ≡_{γ_{P}^{A}} S_{2}.

Example 7. For T_{1}, T_{2} ∈ ℘_{fn}(ℂℙ_{1}, ⊆) as defined in Example 1, we have T_{1} ▷◁ T_{2}. Consider also T_{3}, T_{4} ∈ ℘_{fn}(ℂℙ_{1}, ⊆) where

T_{3} := {{0 ≤ x ≤ 3}, {1 ≤ x ≤ 5}},  T_{4} := {{0 ≤ x ≤ 5}}.

Then T_{3} ▷◁ T_{4} and also T_{2} ◁ T_{4} although the converse does not hold. To see this, let S_{1}, S_{2}, and S′_{2} in Definition 9 be T_{2}, T_{4}, and T′_{4} := {{x = 2.5}}, respectively. Then, if T′′_{4} is such that ⨄ T′′_{4} = ⨄ T′_{4} and T′′_{4} ⊆_{P} T′_{4}, we must have T′′_{4} = T′_{4} ⊈_{P} T_{2}; hence, although T_{4} = {⨄ T_{2}}, we have T_{4} ⋪ T_{2}.

We now define an operation merger that is parametric with respect to the congruence relation and replaces selected subsets by congruent singleton sets.

O  T P_{2} P_{1}  P_{3}  ^{O  T ′ Q_{5} Q_{1} Q_{2} Q_{3} Q_{4}}

Fig. 1. Merging polyhedra according to ‘▷◁’.

Definition 10. (Merge and mergers.) Let R be a congruence relation on D̂_{P}. Then the merge relation merge_{R} ⊆ ℘_{fn}(D, ⊢) × ℘_{fn}(D, ⊢) for R is such that merge_{R}(S_{1}, S_{2}) holds if and only if S_{1} ⊢_{P} S_{2} and

∀d_{2} ∈ S_{2} : ∃S′_{1} ⊆ S_{1} . d_{2} = ⨁S′_{1} ∧ {d_{2}} R S′_{1}.

A set S ∈ ℘_{fn}(D, ⊢) is fully-merged for R, if merge_{R}(S, S′) implies S = S′; S is pairwise-merged for R if, for all d_{1}, d_{2} ∈ S, we have that {d_{1}, d_{2}} is fully-merged. An operator ↑_{R}: ℘_{fn}(D, ⊢) → ℘_{fn}(D, ⊢) is a merger for R if merge_{R}(S, ↑_{R} S) holds.

Note that, for all S ∈ ℘_{fn}(D, ⊢) and congruence relations R, we have S ⊢_{EM} ↑_{R} S.

For the finite powerset domain over ℂ̂ℙ_{n}, lines 1–9 of the algorithm specified in [7, Figure 8, page 773] define a merger operator ‘↑_{▷◁}’ such that, for each finite set S of polyhedra, ↑_{▷◁} S is pairwise-merged.

Example 8. Figure 1 shows two examples of sets of polyhedra. In the left-hand diagram, the set T = {P_{1}, P_{2}, P_{3}} of three squares is not pairwise-merged for ‘▷◁’ since P_{1} ∪ P_{2} and P_{2} ∪ P_{3} are convex polyhedra. Both T_{1} = {P_{1} ∪ P_{2}, P_{3}} and T_{2} = {P_{1}, P_{2} ∪ P_{3}} are fully-merged and hence pairwise-merged for ‘▷◁’, and merge_{▷◁}(T , T_{i}) holds for i = 1, 2. In the right-hand diagram, the set T′ = {Q_{1}, Q_{2}, Q_{3}, Q_{4}, Q_{5}} is pairwise-merged but not fully-merged for ‘▷◁’. Since Q′ := ⋃ T′ is a convex polyhedron, the singleton set {Q′} is fully-merged and hence pairwise-merged for ‘▷◁’ and merge_{▷◁}(T′, {Q′}) holds.

6 Conclusion

We have studied the problem of endowing any abstract domain obtained by means of the finite powerset construction with a provably correct widening operator. We have proposed two generic widening operators and we have instantiated our techniques, which are completely general, on powersets of convex polyhedra, an abstract domain that is being used for static analysis and abstract modelchecking and for which no non-trivial widening operator was previously known.

We have extended the Parma Polyhedra Library (PPL) [3, 6], a modern C^{++} library for the manipulation of convex polyhedra, with a prototype implementation of the widenings and their variants employing the ‘widening up to’ technique [20, 21]. The experimental work has just started, but the initial results obtained are very encouraging as our new widenings compare favorably, both in terms of precision and efficiency, with the extrapolation operator of [7].

References

1. S. Abramsky and A. Jung. Domain theory. In S. Abramsky, D. M. Gabbay, and T. S. E. Maibaum, editors, Handbook of Logic in Computer Science, volume 3, chapter 1, pages 1–168. Clarendon Press, Oxford, UK, 1994.

2. R. Bagnara. A hierarchy of constraint systems for data-flow analysis of constraint logic-based languages. Science of Computer Programming, 30(1–2):119–155, 1998.

3. R. Bagnara, P. M. Hill, E. Ricci, and E. Zaffanella. The Parma Polyhedra Library User’s Manual. Department of Mathematics, University of Parma, Parma, Italy, release 0.5 edition, April 2003. Available at http://www.cs.unipr.it/ppl/.

4. R. Bagnara, P. M. Hill, E. Ricci, and E. Zaffanella. Precise widening operators for convex polyhedra. In R. Cousot, editor, Static Analysis: Proceedings of the 10th International Symposium, volume 2694 of Lecture Notes in Computer Science, pages 337–354, San Diego, California, USA, 2003. Springer-Verlag, Berlin.

5. R. Bagnara, P. M. Hill, and E. Zaffanella. Widening operators for powerset domains. Quaderno, Dipartimento di Matematica, Università di Parma, Italy, 2003. To appear.

6. R. Bagnara, E. Ricci, E. Zaffanella, and P. M. Hill. Possibly not closed convex polyhedra and the Parma Polyhedra Library. In M. V. Hermenegildo and G. Puebla, editors, Static Analysis: Proceedings of the 9th International Symposium, volume 2477 of Lecture Notes in Computer Science, pages 213–229, Madrid, Spain, 2002. Springer-Verlag, Berlin.

7. T. Bultan, R. Gerber, and W. Pugh. Model-checking concurrent systems with unbounded integer variables: Symbolic representations, approximations, and experimental results. ACM Transactions on Programming Languages and Systems, 21(4):747–789, 1999.

8. A. Cortesi, B. Le Charlier, and P. Van Hentenryck. Combinations of abstract domains for logic programming: Open product and generic pattern construction. Science of Computer Programming, 38(1–3):27–71, 2000.

9. P. Cousot and R. Cousot. Static determination of dynamic properties of programs. In B. Robinet, editor, Proceedings of the Second International Symposium on Programming, pages 106–130. Dunod, Paris, France, 1976.

10. P. Cousot and R. Cousot. Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Proceedings of the Fourth Annual ACM Symposium on Principles of Programming Languages, pages 238–252, New York, 1977. ACM Press.

11. P. Cousot and R. Cousot. Systematic design of program analysis frameworks. In Proceedings of the Sixth Annual ACM Symposium on Principles of Programming Languages, pages 269–282, New York, 1979. ACM Press.

12. P. Cousot and R. Cousot. Abstract interpretation and applications to logic programs. Journal of Logic Programming, 13(2&3):103–179, 1992.

13. P. Cousot and R. Cousot. Abstract interpretation frameworks. Journal of Logic and Computation, 2(4):511–547, 1992.

14. P. Cousot and R. Cousot. Comparing the Galois connection and widening/narrowing approaches to abstract interpretation. In M. Bruynooghe and M. Wirsing, editors, Proceedings of the 4th International Symposium on Programming Language Implementation and Logic Programming, volume 631 of Lecture Notes in Computer Science, pages 269–295, Leuven, Belgium, 1992. Springer-Verlag, Berlin.

15. P. Cousot and N. Halbwachs. Automatic discovery of linear restraints among variables of a program. In Conference Record of the Fifth Annual ACM Symposium on Principles of Programming Languages, pages 84–96, Tucson, Arizona, 1978. ACM Press.

16. G. Delzanno and A. Podelski. Model checking in CLP. In R. Cleaveland, editor, Tools and Algorithms for Construction and Analysis of Systems, 5th International Conference, TACAS ’99, volume 1579 of Lecture Notes in Computer Science, pages 223–239, Amsterdam, The Netherlands, 1999. Springer-Verlag, Berlin.

17. N. Dershowitz and Z. Manna. Proving termination with multiset orderings. Communications of the ACM, 22(8):465–476, 1979.

18. G. Filé and F. Ranzato. The powerset operator on abstract interpretations. Theoretical Computer Science, 222:77–111, 1999.

19. N. Halbwachs. Détermination Automatique de Relations Linéaires Vérifiées par les Variables d’un Programme. Thèse de 3^{ème} cycle d’informatique, Université scientifique et médicale de Grenoble, Grenoble, France, March 1979.

20. N. Halbwachs. Delay analysis in synchronous programs. In C. Courcoubetis, editor, Computer Aided Verification: Proceedings of the 5th International Conference, volume 697 of Lecture Notes in Computer Science, pages 333–346, Elounda, Greece, 1993. Springer-Verlag, Berlin.

21. N. Halbwachs, Y.-E. Proy, and P. Roumanoff. Verification of real-time systems using linear relation analysis. Formal Methods in System Design, 11(2):157–185, 1997.

22. C. Holzbaur. OFAI clp(q,r) manual, edition 1.3.3. Technical Report TR-95-09, Austrian Research Institute for Artificial Intelligence, Vienna, 1995.

23. W. Kelly, V Maslov, W. Pugh, E. Rosser, T. Shpeisman, and D. Wonnacott. The Omega library interface guide. Technical Report CS-TR-3445, Department of Computer Science, University of Maryland, College Park, MD, USA, 1995.

24. H. Le Verge. A note on Chernikova’s algorithm. Publication interne 635, IRISA, Campus de Beaulieu, Rennes, France, 1992.

25. V. Loechner. PolyLib: A library for manipulating parameterized polyhedra. Avail-

able at http://icps.u-strasbg.fr/~loechner/polylib/, March 1999. Declares

itself to be a continuation of [28].

26. W. Pugh. A practical algorithm for exact array dependence analysis. Communications of the ACM, 35(8):102–114, 1992.

27. D. Srivastava. Subsumption and indexing in constraint query languages with linear arithmetic constraints. Annals of Mathematics and Artificial Intelligence, 8(3– 4):315–343, 1993.

28. D. K. Wilde. A library for doing polyhedral operations. Master’s thesis, Oregon State University, Corvallis, Oregon, December 1993. Also published as IRISA Publication interne 785, Rennes, France, 1993.