Decomposing Non-Redundant Sharing by Complementation

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

1 Servizio IX Automazione, Università degli Studi di Modena, Italy.

                   zaffanella.enea@unimo.it

2 School of Computer Studies, University of Leeds, Leeds, LS2 9JT, U. K.

                     hill@scs.leeds.ac.uk

3 Dipartimento di Matematica, Università degli Studi di Parma, Italy.

                     bagnara@cs.unipr.it

Abstract. Complementation, the inverse of the reduced product operation, is a relatively new technique for systematically finding minimal decompositions of abstract domains. Filé and Ranzato advanced the state of the art by introducing a simple method for computing a complement. As an application, they considered the extraction by complementation of the pair-sharing domain PS from the Jacobs and Langen’s set-sharing domain SH . However, since the result of this operation was still SH , they concluded that PS was too abstract for this. Here, we show that the source of this difficulty lies not with PS but with SH and, more precisely, with the redundant information contained in SH with respect to ground-dependencies and pair-sharing. In fact, the difficulties vanish if our non-redundant version of SH , SH^{ρ}, is substituted for SH . To establish the results for SH^{ρ}, we define a general schema for subdomains of SH that includes SH^{ρ} and Def as special cases. This sheds new light on the structure of SH^{ρ} and exposes a natural though unexpected connection between Def and SH^{ρ}. Moreover, we substantiate the claim that complementation alone is not sufficient to obtain truly minimal decompositions of domains. The right solution to this problem is to first remove redundancies by computing the quotient of the domain with respect to the observable behavior, and only then decompose it by complementation.

Keywords: Abstract Interpretation, Domain Decomposition, Complementation, Sharing Analysis.

1 Introduction

Complementation [5], which is the inverse of the well-known reduced product operation [7], can systematically obtain minimal decompositions of complex abstract domains. It was argued that these decompositions would be useful in finding space saving representations for domains and to simplify domain verification problems.

⋆ Part of this work was supported by EPSRC grant GR/M05645.

In [8], Filé and Ranzato presented a new method for computing the complement, which is simpler than the original proposal by Cortesi et al. [4, 5] because it has the advantage that, in order to compute the complement, only a relatively small number of elements (namely the meet-irreducible elements of the reference domain) need be considered. As an application of this method, the authors considered the Jacobs and Langen’s sharing domain [13], SH , for representing properties of variables such as groundness and sharing. This domain captures the property of set-sharing. However, it has been observed [1] that for most (if not all) applications, the property of interest is not set-sharing but pair-sharing. Filé and Ranzato illustrated their method by minimally decomposing SH into three components; using the words of the authors [8, Section 1]:

“each representing one of the elementary properties that coexist in the elements of Sharing, and that are as follows: (i) the ground-dependency information; (ii) the pair-sharing information, or equivalently variable independence; (iii) the set-sharing information, without variable independence and ground-dependency.”

However, this decomposition did not use the usual domain PS for pair-sharing. Filé and Ranzato observed that the complement of the pair-sharing domain PS with respect to SH is again SH and concluded that PS was too abstract to be extracted from SH by means of complementation. In order to overcome this difficulty, and to obtain this non-trivial decomposition of SH , they used a different (and somewhat unnatural) definition for an alternative pair-sharing domain that they called PS′. The nature of PS′ and its connection with PS is examined more carefully in Section 6.

We noticed that the difficulty Filé and Ranzato had was not in the definition of PS, which accurately represents the property of pair-sharing, but in the use of the set-sharing domain SH itself since it carries some redundant information. It was shown in [1] that, for groundness and pair-sharing, SH includes redundant information. By defining an upper closure operator ρ that removed this redundancy, a much smaller domain SH^{ρ} was found that captured pair-sharing with the same precision as SH . We show here that using the method given in [8], but with this domain instead of SH as the reference domain, the difficulties in the decomposition disappear. Moreover, we show that PS is exactly one of the components obtained by complementation of SH^{ρ}. Thus the problem exposed by Filé and Ranzato was, in fact, due to the “information preserving” property of complementation, as any factorization obtained in this way is such that the reduced product of the factors gives back the original domain. In particular, any factorization of SH has to encode the redundant information identified in [1]. We will show that such a problem disappears when SH^{ρ} is used as the reference domain.

Although the primary purpose of this work is to clarify the decomposition of the domain SH^{ρ}, the formulation is sufficiently general to apply to other properties that are captured by SH . The domain Pos of positive Boolean functions and its subdomain Def , the domain of definite Boolean functions, are normally used for capturing groundness. Each Boolean variable has the value true if the program variable it corresponds to is definitely bound to a ground term. However, the domain Pos is isomorphic to SH via the mapping from formulas in Pos to the set of complements of their models [3]. This means that any general results regarding the structure of SH are equally applicable to Pos and its subdomains.

To establish the results for SH^{ρ}, we define a general schema for subdomains of SH that includes SH^{ρ} and Def as special cases. This sheds new light on the structure of the domain SH^{ρ}, which is smaller but significantly more involved than SH .^{1} Of course, as we have used the more general schematic approach, we can immediately derive (where applicable) corresponding results for Def and Pos. Moreover, an interesting consequence of this work is the discovery of a natural connection between the abstract domains Def and SH^{ρ}. The results confirm that SH^{ρ} is, in fact, the “appropriate” domain to consider when pairsharing is the property of interest.

The paper is structured as follows: In Section 2 we briefly recall the required notions and notations, even though we assume general acquaintance with the topics of lattice theory, abstract interpretation, sharing analysis and groundness analysis. Section 3 introduces the SH domain and several abstractions of it. The meet-irreducible elements of an important family of abstractions of SH are identified in Section 4. This is required in order to apply, in Section 5, the method of Filé and Ranzato to this family. We conclude in Section 6 with some final remark where, in particular, we explain what is, in our opinion, the lesson to be learned from this and other related works.

2 Preliminaries

For any set S, ℘(S) denotes the power set of S and # S is the cardinality of S.

A preorder ⪯ over a set P is a binary relation that is reflexive and transitive. If ⪯ is also antisymmetric, then it is called partial order. A set P equipped with a partial order ⪯ is said to be partially ordered and sometimes written ⟨P, ⪯⟩. Partially ordered sets are also called posets.

Given a poset ⟨P, ⪯⟩ and S ⊆ P, y ∈ P is an upper bound for S if and only if x ⪯ y for each x ∈ S. An upper bound y for S is the least upper bound (or lub) of S if and only if, for every upper bound y′ for S, y ⪯ y′. The lub, when it exists, is unique. In this case we write y = lub S. Lower bounds and greatest lower bounds are defined dually.

A poset ⟨L, ⪯⟩ such that, for each x, y ∈ L, both lub{x, y} and glb{x, y} exist, is called a lattice. In this case, lub and glb are also called, respectively, the join and the meet operations of the lattice. A complete lattice is a lattice ⟨L, ⪯⟩ such that every subset of L has both a least upper bound and a greatest lower bound. The top element of a complete lattice L, denoted by ⊤, is such that ⊤ ∈ L and ∀x ∈ L : x ⪯ ⊤. The bottom element of L, denoted by ⊥, is defined dually.

1 For the well acquainted with the matter: SH is a powerset and hence it is dualatomistic; this is not the case for SH^{ρ}.

An algebra ⟨L, ∧, ∨⟩ is also called a lattice if ∧ and ∨ are two binary operations over L that are commutative, associative, idempotent, and satisfy the following absorption laws, for each x, y ∈ L: x ∧ (x ∨ y) = x and x ∨ (x ∧ y) = x. The two definitions of lattices are equivalent. This can be seen by setting up the isomorphism given by: x ⪯ y ⟺^{def} x ∧ y = x ⟺^{def} x ∨ y = y, glb{x, y} =^{def} x ∧ y, and lub{x, y} =^{def} x ∨ y. A complete lattice C is meet-continuous if for any chain Y ⊆ C and each x ∈ C, x ∧ (⋁ Y ) = ⋁_{y∈Y} (x ∧ y).

A monotone and idempotent self-map ρ: P → P over a poset ⟨P, ⪯⟩ is called a closure operator (or upper closure operator) if it is also extensive, namely ∀x ∈ P : x ⪯ ρ(x). If C is a complete lattice, then each upper closure operator ρ over C is uniquely determined by the set of its fixpoints, that is, by its image ρ(C) =^{def} { ρ(x) | x ∈ C }. The set of all upper closure operators over a complete lattice C, denoted by uco(C), form a complete lattice ordered as follows: if ρ_{1}, ρ_{2} ∈ uco(P), ρ_{1} ⊑ ρ_{2} if and only if ρ_{2}(C) ⊆ ρ_{1}(C). We will often denote upper closure operators by the sets of their fixpoints. The reader is referred to [11] for an extensive treatment of closure operators.

The reduced product of two elements ρ_{1}, ρ_{2} of uco(C) is: ρ_{1}⊓ρ_{2} =^{def} glb{ρ_{1}, ρ_{2}}. Suppose C is a meet-continuous lattice (which is the case for most domains for abstract interpretation [5], here included all the domains considered in this paper). Then the inverse of the reduced product operation, called complementation, is well defined and given as follows. If ρ ⊑ ρ_{1} then ρ ∼ ρ_{1} =^{def} lub{ ρ_{2} | ρ_{1} ⊓ ρ_{2} = ρ }. Given a meet-continuous lattice C and ρ ∈ uco(C), the pseudo-complement (or, by an abuse of terminology now customary in the field, simply complement) of ρ is denoted by id_{C} ∼ ρ, where id_{C} is the identity over C. Let C be a meet-continuous lattice and D_{i} =^{def} ρ_{D_{i}}(C) with ρ_{D_{i}} ∈ uco(C) for i = 1, …, n. Then { D_{i} | 1 ≤ i ≤ n } is a decomposition for C if C = D_{1} ⊓ ⋯ ⊓ D_{n}. The decomposition is also called minimal if, for each k ∈ ℕ with 1 ≤ k ≤ n and each E_{k} ∈ uco(C), D_{k} ⊏ E_{k} implies C ⊏ D_{1} ⊓ ⋯ ⊓ D_{k−1} ⊓ E_{k} ⊓ D_{k+1} ⊓ ⋯ ⊓ D_{n}. Let C be a complete lattice and X ⊆ C. Then Moore(X) denotes the Moore completion of X, namely, Moore(X) =^{def} { ⋀ Y | Y ⊆ X }. We say that C is meet-generated by X if C = Moore(X). An element x ∈ C is meet-irreducible if ∀y, z ∈ C : ((x = y ∧ z) ⟹ (x = y or x = z)). The set of meet-irreducible elements of a complete lattice C is denoted by MI(C). Note that ⊤ ∈ MI(C). An element x ∈ C is a dual-atom if x ≠ ⊤ and, for each y ∈ C, x ≤ y < ⊤ implies x = y. The set of dual-atoms is denoted by dAtoms(C). Note that dAtoms(C) ⊂ MI(C). The domain C is dual-atomistic if C = Moore(dAtoms(C)). Thus, if C is dualatomistic, MI(C) = {⊤} ∪ dAtoms(C).

The following result holds [8, Theorem 4.1].

Theorem 1. If C is meet-generated by MI(C) then uco(C) is pseudo-comple-mented and for any ρ ∈ uco(C)

id_{C} ∼ ρ = Moore(MI(C) \ ρ(C)).

Another useful result from lattice theory is the following.

Theorem 2. All continuous lattices are meet-generated by their meet-irreducible elements.

Hence we have the following corollary [8, Corollary 4.5].

Corollary 1. If C is dual-atomistic then uco(C) is pseudo-complemented and for any ρ ∈ uco(C)

id_{C} ∼ ρ = Moore(dAtoms(C) \ ρ(C)).

Domains such as SH are normally defined over a denumerable set of variables Vars and then a finite subset of Vars is used to define a subset of SH that is restricted to these variables. In this paper, we assume there is a fixed and finite set of variables of interest VI ⊂ Vars of cardinality n.

If t is a first-order term over VI , then vars(t) denotes the set of variables occurring in t. Bind denotes the set of equations of the form x = t (sometimes written x ↦ t) where x ∈ VI and t is a first-order term over VI . Note that we do not impose the occur-check condition x ∉ vars(t), since we have proved in [12] that this is not required to ensure correctness of the operations of SH and its derivatives. We also define Subst =^{def} ℘(Bind).

3 The Sharing Domains

3.1 The Set-sharing Domain SH

In this paper, since the set of relevant variables is fixed, it is assumed that SH , Def and PS are each restricted to the finite set of variables VI ⊂ Vars. Therefore, the domain elements for SH (and hence for all their subdomains such as PS and Def ) do not include the set of variables explicitly.

Definition 1. (The set-sharing domain SH .) The domain SH is given by SH =^{def} ℘(SG) where SG =^{def} { S ∈ ℘(VI ) | S ≠ ∅ }. SH is partially ordered by set inclusion so that the lub is given by set union and glb by set intersection.

Note that, as we are adopting the upper closure operator approach to abstract interpretation, all the domains we define here are ordered by subset inclusion. In the following examples, the elements of SH will be always written in a simplified notation, omitting the inner braces. For instance, the set {{x}, {x, y}, {x, z}, {x, y, z}} will be written simply as {x, xy, xz, xyz}.

For the purpose of this paper, we just need the following operations over SH . See [1] for a precise definition of all the operations used for an analysis.

Definition 2. (Some operations over SH .) The function bin: SH × SH → SH , called binary union, is given by

bin(sh_{1}, sh_{2}) =^{def} { S_{1} ∪ S_{2} | S_{1} ∈ sh_{1}, S_{2} ∈ sh_{2} }.

The star-union function (·)^{⋆}: SH → SH is given by

sh^{⋆} =^{def} { S ∈ SG | ∃sh′ ⊆ sh . S = ⋃ sh′ }.

For each j ≥ 1, the j-self-union function (·)^{j}: SH → SH is given by

sh^{j} =^{def} { S ∈ SG | ∃sh′ ⊆ sh . (# sh′ ≤ j, S = ⋃ sh′) }.

The extraction of the relevant component of an element of SH with respect to a subset of VI is encoded by the function rel: ℘_{f}(VI ) × SH → SH given by

rel(V, sh) =^{def} { S ∈ sh | S ∩ V ≠ ∅ }.

The function amgu captures the effects of a binding x ↦ t on an element of SH . Let v_{x} = {x}, v_{t} = vars(t) and v_{xt} = v_{x} ∪ v_{t}. Then

amgu(sh, x ↦ t) =^{def} (sh \ (rel(v_{xt}, sh)) ∪ bin(rel(v_{x}, sh)^{⋆}, rel(v_{t}, sh)^{⋆}).

We also define the extension amgu: SH × Subst → SH by

amgu(sh, ∅) =^{def} sh,
amgu(sh, {x ↦ t} ∪ σ) =^{def} amgu(amgu(sh, x ↦ t), σ \ {x ↦ t}).

The function proj: SH × ℘(VI ) → SH that projects an element of SH onto a subset V ⊆ VI of the variables of interest is given by

proj(sh, V) =^{def} { S ∩ V | S ∈ sh, S ∩ V ≠ ∅ }.

The j-self-union operator is new. We show later when it may be safely used to replace the star-union operator. Note, in particular that, letting j = 1, 2, and n, we have sh^{1} = sh, sh^{2} = bin(sh, sh), and, as # VI = n, sh^{n} = sh^{⋆}.

Since SH is a power set, SH is dual-atomistic and

dAtoms(SH ) = { SG \ {S} | S ∈ SG }.

Example 1. Suppose VI = {x, y, z}. Then the seven dual-atoms of SH are:

\begin{matrix}s_{1} & = \{ y, z, xy, xz, yz, xyz\}, \\ s_{2} & = \{x, z, xy, xz, yz, xyz\}, \\ s_{3} & = \{x, y, xy, xz, yz, xyz\}, \end{matrix} \}  these lack a singleton;

\begin{matrix}s_{4} & = \{x, y, z, xz, yz, xyz\}, \\ s_{5} & = \{x, y, z, xy, yz, xyz\}, \\ s_{6} & = \{x, y, z, xy, xz, xyz\}, \end{matrix} \}  these lack a pair;

s_{7} = {x, y, z, xy, xz, yz  },  this lacks VI .

Then the meet-irreducible elements of SH are s_{1}, …, s_{7} together with SG, the top element.

3.2 The Tuple-sharing Domains

To provide a general characterization of domains such as the groundness and pair-sharing domains in SH , we first identify the sets of elements that have the same cardinality.

Definition 3. (Tuples of cardinality k.) For each k ∈ ℕ with 1 ≤ k ≤ n, the overloaded functions tuples_{k}: SG → SH and tuples_{k}: SH → SH are defined as

tuples_{k}(S) =^{def} { T ∈ ℘(S) | # T = k },
tuples_{k}(sh) =^{def} ⋃{ tuples_{k}(S′) | S′ ∈ sh }.

In particular, if S ∈ SG, sh ∈ SH , let

pairs(S) =^{def} tuples_{2}(S),
pairs(sh) =^{def} tuples_{2}(sh).

The usual domains that represent groundness and pair-sharing information will be shown to be special cases of the following more general domain.

Definition 4. (The tuple-sharing domains TS_{k}.) For each k ∈ ℕ such that 1 ≤ k ≤ n, the function ρ_{_{TS}_{k}}: SH → SH is defined as

ρ_{_{TS}_{k}}(sh) =^{def} { S ∈ SG | tuples_{k}(S) ⊆ tuples_{k}(sh) }

and, as ρ_{_{TS}_{k}} ∈ uco(SH ), it induces the lattice

TS_{k} =^{def} ρ_{_{TS}_{k}}(SH ).

Note that ρ_{_{TS}_{k}}(tuples_{k}(sh)) = ρ_{_{TS}_{k}}(sh) and that there is a one to one correspondence between TS_{k} and ℘(tuples_{k}(VI )). The isomorphism is given by the functions tuples_{k}: TS_{k} → ℘(tuples_{k}(VI )) and ρ_{_{TS}_{k}}: ℘(tuples_{k}(VI )) → TS_{k}. Thus the domain TS_{k} is the smallest domain that can represent properties characterized by sets of variables of cardinality k. We now consider the tuple-sharing domains for the cases when k = 1, 2, and n.

Definition 5. (The groundness domain Con.) The upper closure operator ρ_{Con} : SH → SH and the corresponding domain Con are defined as ρ_{Con} =^{def} ρ_{_{TS}_{1}} and Con =^{def} TS_{1} = ρ_{Con}(SH ).

This domain, which represents groundness information, is isomorphic to the domain of conjunctions of Boolean variables. The isomorphism tuples_{1} maps each element of Con to the set of variables that are possibly non-ground. The usual domain (also normally called Con) for representing groundness can be obtained (as for Pos and Def ) by set complementation.

Definition 6. (The pair-sharing domain PS.) The upper closure operator ρ_{PS} : SH → SH and the corresponding domain PS are defined as ρ_{PS} =^{def} ρ_{_{TS}_{2}} and PS =^{def} TS_{2} = ρ_{PS}(SH ).

This domain represents pair-sharing information and the isomorphism tuples_{2} maps each element of PS to the set of pairs of variables that may be bound to terms that share a common variable. The domain for representing variable independence can be obtained by set complementation. Finally, in the case when k = n we have a domain consisting of just two elements:

TS_{n} = {SG, SG \ {VI }}.

Just as for SH , the domains TS_{k} are dual-atomistic and:

dAtoms(TS_{k}) = { (SG \ { U ∈ SG | T ⊆ U }) | T ∈ tuples_{k}(VI ) }.

Thus we have

dAtoms(Con) = { (SG \ { U ∈ SG | x ∈ U }) | x ∈ VI },
dAtoms(PS) = { (SG \ { U ∈ SG | x, y ∈ U }) | x ≠ y ∈ VI }.

Example 2. Consider Example 1. Then the dual atoms of Con are

{ y, z, yz},
{x, z, xz },
{x, y, xy },

and the dual atoms of PS are

{x, y, z, xz, yz},
{x, y, z, xy, yz},
{x, y, z, xy, xz }.

It can be seen from the dual atoms, that the precision of the information encoded by domains TS_{j} and TS_{k} is not comparable when j ≠ k. Also, we note that, if j < k, then ρ{TS \atop j}(TS_{k}) = \{SG\} and ρ_{_{TS}_{k}}(TS_{j}) = TS_{j}.

3.3 The Tuple-Sharing Dependency Domains

We now need to define domains that capture the propagation of groundness and pair-sharing; in particular, the dependency of these properties on the further instantiation of the variables. In the same way as with TS_{k} for Con and PS, we first define a general subdomain TSD_{k} of SH . This must be safe with respect to the tuple-sharing property represented by TS_{k} when performing the usual abstract operations. This was the motivation behind the introduction in [1] of the pair-sharing dependency domain SH^{ρ}. We now generalize this for tuplesharing.

Definition 7. The tuple-sharing dependency domain (TSD_{k}.) For each k where 1 ≤ k ≤ n, the function ρ_{_{TSD}_{k}}: SH → SH is defined as

ρ_{_{TSD}_{k}}(sh)

=^{def} { S ∈ SG | ∀T ⊆ S : # T < k ⟹ S = ⋃{ U ∈ sh | T ⊆ U ⊆ S } },

and, as ρ_{_{TSD}_{k}} ∈ uco(SH ), it induces the tuple-sharing dependency lattice

TSD_{k} =^{def} ρ_{_{TSD}_{k}}(SH ).

It follows from the definitions that the domains TSD_{k} form a strict chain.

Proposition 1. For j, k ∈ ℕ with 1 ≤ j < k ≤ n, we have TSD_{j} ⊂ TSD_{k}.

Moreover, TSD_{k} is not less precise than TS_{k}.

Proposition 2. For k ∈ ℕ with 1 ≤ k ≤ n, we have TS_{k} ⊆ TSD_{k}. Furthermore, if n > 1 then TS_{k} ⊂ TSD_{k}.

A consequence of Propositions 1 and 2 is that TSD_{k} is not less precise than TS_{1} ⊓ ⋯ ⊓ TS_{k}.

Corollary 2. For j, k ∈ ℕ with 1 ≤ j ≤ k ≤ n, we have TS_{j} ⊆ TSD_{k}.

It also follows from the definitions that, for the TSD_{k} domain, the star-union operator can be replaced by the k-self-union operator.

Proposition 3. For 1 ≤ k ≤ n, we have ρ_{_{TSD}_{k}}(sh^{k}) = sh^{⋆}.

We consider the tuple-sharing dependency domains for the cases when k = 1, 2, and n.

Definition 8. (The ground dependency domain Def .) The upper closure operator ρ_{Def} : SH → SH and the corresponding domain Def are defined as ρ_{Def} =^{def} ρ_{_{TSD}_{1}} and Def =^{def} TSD_{1} = ρ_{Def} (SH ).

By Proposition 3, we have for all sh ∈ SH , ρ_{_{TSD}_{1}}(sh) = sh^{⋆} so that TSD_{1} is a representation of the domain Def used for capturing groundness. It also confirms the well-known result that the star-union operator is redundant for elements in Def .

Definition 9. (The pair-sharing dependency domain PSD.) The upper closure operator ρ_{PSD} : SH → SH and the corresponding domain PSD are defined as ρ_{PSD} =^{def} ρ_{_{TSD}_{2}} and PSD =^{def} TSD_{2} = ρ_{PSD}(SH ).

Then, it follows from [1, Theorem 7] that PSD is in fact the domain, corresponding to SH^{ρ}, defined for capturing pair-sharing. By Proposition 3, we have for all sh ∈ SH , ρ_{PSD}(sh^{2}) = sh^{⋆}; thus confirming the result in [1] that for elements in PSD, the star-union operator sh^{⋆} can be replaced by the 2-self-union sh^{2} = bin(sh, sh) without any loss of precision. Furthermore, Corollary 2 confirms the result established in [1] that PSD also captures groundness. Finally, letting k = n, we observe that TSD_{n} = SH .

In [1], the PSD domain is shown to be as good as SH for both representing and propagating pair-sharing. It is also proved that any weaker domain does not satisfy these properties, so that PSD is the quotient [6] of SH with respect to the pair-sharing property PS. In the view of recent results on abstract domain completeness [9], this also means that PSD is the least fully-complete extension (lfce) of PS with respect to SH .

From a purely theoretical point of view, the quotient of an abstract interpretation with respect to a property of interest and the least fully-complete extension of an upper closure operator are not equivalent. It is known [6] that the quotient may not exist, while the lfce is always defined. However, it is also known [10] that when the quotient exists it is exactly the same as the lfce. Moreover, it should be noted that the quotient will exist as long as we consider a semantics where at least one of the domain operators is additive and this is almost always the case (just consider the merge-over-all-paths operator, usually implemented as the lub of the domain). Therefore, for the domains considered here, these two approaches to the completeness problem in abstract interpretation are equivalent.

We now generalize and strengthen the result in [1] and show that, for each k ∈ {1, …, n}, TSD_{k} is the quotient of SH with respect to the reduced product TS_{1} ⊓ ⋯ ⊓ TS_{k} (equivalently, the lfce of TS_{1} ⊓ ⋯ ⊓ TS_{k} with respect to SH ).

The following results can be obtained by generalizing the corresponding results in [1].

Theorem 3. Let sh_{1}, sh_{2} ∈ SH and 1 ≤ k ≤ n. If ρ_{_{TSD}_{k}}(sh_{1}) = ρ_{_{TSD}_{k}}(sh_{2}) then, for each σ ∈ Subst, each sh′ ∈ SH , and each V ∈ ℘_{f}(VI ),

ρ_{_{TSD}_{k}}(amgu(sh_{1}, σ)) = ρ_{_{TSD}_{k}}(amgu(sh_{2}, σ)),
ρ_{_{TSD}_{k}}(sh′ ∪ sh_{1}) = ρ_{_{TSD}_{k}}(sh′ ∪ sh_{2}),
ρ_{_{TSD}_{k}}(proj(sh_{1}, V)) = ρ_{_{TSD}_{k}}(proj(sh_{2}, V)).

Theorem 4. Let 1 ≤ k ≤ n For each sh_{1}, sh_{2} ∈ SH , ρ_{_{TSD}_{k}}(sh_{1}) ≠ ρ_{_{TSD}_{k}}(sh_{2}) implies

∃σ ∈ Subst, ∃j ∈ \{1, …, k\} . ρ{TS \atop j}(amgu(sh_{1}, σ)) ≠ ρ{TS \atop j}(amgu(sh_{2}, σ)).

4 The Meet-Irreducible Elements

In Section 5, we use the method of Filé and Ranzato [8] to decompose the dependency domains TSD_{k}. In preparation for this, in this section, we identify the meet-irreducible elements for the domains and state some general results.

We have already observed that TS_{k} and TSD_{n} = SH are dual-atomistic. However, TSD_{k}, for k < n, is not dual-atomistic and we need to identify the meet-irreducible elements. In fact, the set of dual-atoms for TSD_{k} is

dAtoms(TSD_{k}) = { SG \ {S} | S ∈ SG, # S ≤ k }.

Note that # dAtoms(TSD_{k}) = ∑_{j=1}^{k} \binom{n}{j}. Specializing this for k = 1 and k = 2, respectively, we have:

dAtoms(Def ) = { SG \ {{x}} | x ∈ VI },
dAtoms(PSD) = { SG \ {S} | S ∈ pairs(VI ) } ∪ dAtoms(Def ),

and that # dAtoms(Def ) = n and # dAtoms(PSD) = n(n + 1)/2. We present as an example of this the dual atoms for Def and PSD when n = 3.

Example 3. Consider Example 1. Then the 3 dual-atoms for Def are s_{1}, s_{2}, s_{3} and the 6 dual atoms for PSD are s_{1}, …, s_{6}. Note that these are not all the meetirreducible elements since sets that do not contain xyz such as ⊥ = ρ_{Def} (⊥) = ∅ and {x} cannot be obtained by the meet (which is set intersection) of a set of dual-atoms. Thus, unlike Con and PS, neither Def nor PSD are dual-atomistic.

Consider next the subset M_{k} of meet-irreducible elements of TSD_{k} that are neither the top element SG nor dual atoms. M_{k} has an element for each sharing group S ∈ SG such that # S > k and each tuple T ⊂ S with # T = k. Such an element is obtained from SG by removing all sharing groups U such that T ⊆ U ⊆ S. Formally,

M_{k} =^{def} { SG \ { U ∈ SG | T ⊆ U ⊆ S } | T, S ∈ SG, T ⊂ S, # T = k }.

Note that, as there are \binom{n}{k} possible choices for T and 2^{n−k} − 1 possible choices for S, we have # M_{k} = \binom{n}{k}(2^{n−k} − 1) and # MI(TSD_{k}) = ∑_{j=0}^{k−1} \binom{n}{j} + \binom{n}{k}2^{n−k}. Again, we illustrate this definition with the case when n = 3.

Example 4. Consider again Example 3. First, consider the domain Def . The meet-irreducible elements which are not dual-atoms, beside SG, are the following:

q_{1} = { y, z, xz, yz, xyz} ⊂ s_{1},
q_{2} = { y, z, xy, yz, xyz} ⊂ s_{1}, r_{1} = { y, z, yz} ⊂ q_{1} ∩ q_{2},
q_{3} = {x, z, xz, yz, xyz} ⊂ s_{2},
q_{4} = {x, z, xy, xz, xyz} ⊂ s_{2},  r_{2} = {x, z, xz } ⊂ q_{3} ∩ q_{4},
q_{5} = {x, y, xy, yz, xyz} ⊂ s_{3},
q_{6} = {x, y, xy, xz, xyz} ⊂ s_{3},  r_{3} = {x, y, xy  } ⊂ q_{5} ∩ q_{6}.

Next, consider the domain PSD. The only meet-irreducible elements that are not dual-atoms, beside SG, are the following:

m_{1} = {x, y, z, xz, yz  } ⊂ s_{4}
m_{2} = {x, y, z, xy, yz  } ⊂ s_{5}
m_{3} = {x, y, z, xy, xz  } ⊂ s_{6}.

Each of these lack a pair and none contains the sharing group xyz.

We now show that we have identified precisely all the meet-irreducible elements of TSD_{k}.

Theorem 5. If k ∈ ℕ with 1 ≤ k ≤ n, then

MI(TSD_{k}) = {SG} ∪ dAtoms(TSD_{k}) ∪ M_{k}.

As a consequence, we have the following result.

Corollary 3. Let k ∈ ℕ with 1 ≤ k ≤ n. Then

dAtoms(TS_{k}) = { sh ∈ MI(TSD_{k}) | VI ∉ sh }.

For the decomposition, we need to identify which meet-irreducible elements of TSD_{k} are in TS_{j}. Using Corollaries 2 and 3 we have the following result.

Corollary 4. If j, k ∈ ℕ with 1 ≤ j < k ≤ n, then MI(TSD_{k}) ∩ TS_{j} = {SG}.

By combining Proposition 1 with Theorem 5 we can identify the meet-irreducible elements of TSD_{k} that are in TSD_{j}, where j < k.

Corollary 5. If j, k ∈ ℕ with 1 ≤ j < k ≤ n, then

MI(TSD_{k}) ∩ TSD_{j} = dAtoms(TSD_{j}).

5 The Decomposition of the Domains

5.1 Removing the Tuple-Sharing Domains

We first consider the decomposition of TSD_{k} with respect to TS_{j}. It follows from Theorem 1 and Corollaries 2 and 4 that, for 1 ≤ j < k ≤ n, we have

TSD_{k} ∼ TS_{j} = TSD_{k}.  (1)

Since SH = TSD_{n}, we have, using Eq. (1) and setting k = n, that, if j < n,

SH ∼ TS_{j} = SH .  (2)

Thus, in general, TS_{j} is too abstract to be removed from SH by means of complementation. (Note that here it is required j < n, because we have SH ∼ TS_{n} ≠ SH .) In particular, letting j = 1, 2 (assuming n > 2) in Eq. (2), we have

SH ∼ PS = SH ∼ Con = SH ,  (3)

showing that Con and PS are too abstract to be removed from SH by means of complementation. Also, by Eq. (1), letting j = 1 and k = 2 it follows that the complement of Con in PSD is PSD.

Now consider decomposing TSD_{k} using TS_{k}. It follows from Theorem 1, Proposition 2 and Corollary 3 that, for 1 ≤ k ≤ n, we have

TSD_{k} ∼ TS_{k} = Moore(MI(TSD_{k}) \ ρ_{_{TS}_{k}}(TSD_{k}))
= { sh ∈ TSD_{k} | VI ∈ sh }.  (4)

Thus we have

TSD_{k} ∼ (TSD_{k} ∼ TS_{k}) = TS_{k}.  (5)

We have therefore extracted all the domain TS_{k} from TSD_{k}. So by letting k = 1, 2 in Eq. (5), we have found the complements of Con in Def and PS in PSD:

Def ∼ Con = { sh ∈ Def | VI ∈ sh },
PSD ∼ PS = { sh ∈ PSD | VI ∈ sh }.

Thus if we denote the domains induced by these complements as Def^{⊕} and PSD^{⊕}, respectively, we have the following result. Theorem 6.

Def ∼ Con = Def^{⊕},  Def ∼ Def^{⊕} = Con,
PSD ∼ PS = PSD^{⊕},  PSD ∼ PSD^{⊕} = PS.

Moreover, Con and Def^{⊕} form a minimal decomposition for Def and, similarly, PS and PSD^{⊕} form a minimal decomposition for PSD.

5.2 Removing the Dependency Domains

First we note that, by Theorem 5, Proposition 1 and Corollary 5 the complement of TSD_{j} in TSD_{k}, where 1 ≤ j < k ≤ n, is given as follows:

TSD_{k} ∼ TSD_{j} = Moore(MI(TSD_{k}) \ ρ_{_{TSD}_{j}}(TSD_{k}))
= { sh ∈ TSD_{k} | ∀S ∈ SG : # S ≤ j ⟹ S ∈ sh }. (6)

It therefore follows from Eq. (6) and setting k = n that the complement of ρ_{_{TSD}_{j}} in SH for j < n is:

SH ∼ TSD_{j} = { sh ∈ SH | ∀S ∈ SG : # S ≤ j ⟹ S ∈ sh }  (7)

=^{def} SH _{j}^{+}.

In particular, in Eq. (7) when j = 1, we have the following result for Def (also proved in [8, Lemma 5.4]):

SH ∼ Def = { sh ∈ SH | ∀x ∈ VI : {x} ∈ sh }.

This complement is denoted by SH +_{Def} . Also, in Eq. (7) when j = 2, we have the following result for PSD:

SH ∼ PSD = { sh ∈ SH | ∀S ∈ SG : # S ≤ 2 ⟹ S ∈ sh }.

This complement is denoted by SH +_{PSD}.

We next construct the complement of PSD with respect to Def . By Eq. (6),

PSD ∼ Def = { sh ∈ PSD | ∀x ∈ VI : {x} ∈ sh }

=^{def} PSD^{+}.

Then the complement factor Def^{−} =^{def} PSD ∼ PSD^{+} is exactly the same as SH ∼ SH +_{Def} and PSD and SH behave similarly for Def .

5.3 Completing the Decomposition

Just as for SH , the complement of SH +_{Def} using PS (or, more generally, TS_{j} where 1 < j < n) is SH +_{Def} . By Corollary 3 and Theorem 1, as PS is dual-atomistic, the complement of PS in PSD^{+} is given as follows.

Theorem 7.

PSD^{‡} =^{def} PSD^{+} ∼ PS
= { sh ∈ PSD | VI ∈ sh, ∀x ∈ VI : {x} ∈ sh },
PSD^{+} ∼ PSD^{‡} = PS.

So, we have extracted all the domain PS from PSD^{+} and we have the following result.

Corollary 6. Def^{−}, PS, and PSD^{‡} form a minimal decomposition for PSD.

6 Conclusion

In [1], we said that PSD ∼ PS ≠ PSD. This paper now clarifies that statement. We have provided a minimal decomposition for PSD whose components include Def^{−} and PS. Moreover, we have shown that PSD is not dual-atomistic. The meet-irreducible elements of PSD have been completely specified. As a consequence, it can be seen that the dual-atoms of PSD are precisely those elements which have the form SG \ {S} where # S ≤ 2.

By studying the sharing domain SH in a more general framework, we have been able to show that the domain PSD has natural place in a scheme of domains based on SH . Moreover, by means of this approach we have highlighted the close relationship between Def and PSD and the many properties they share.

Our starting point was the work of Filé and Ranzato. In [8], they noted, as we have, that SH +_{Def} ∼ PS = SH +_{Def} so that none of the domain PS could be extracted from SH +_{Def} . They noticed that ρ_{PS} maps all dual-atoms that contain VI to SG and thus lose all pair-sharing information. To avoid this, they replaced PS with the domain PS′ where, for all sh ∈ SH +_{Def} , ρ_{PS}′(sh) = ρ_{PS}(sh) \ ({VI } \ sh), and noted that SH +_{Def} ∼ PS′ = { sh ∈ SH +_{Def} | VI ∈ sh }. To understand the nature of this new domain PS′, we first observe that, PS′ is simply the reduced product of PS and TS_{n}. This is because TS_{n} = MI(TS_{n}) = {SG \ {VI }, SG}. In addition, SH +_{Def} ∼ TS_{n} = { sh ∈ SH +_{Def} | VI ∈ sh }, which is precisely the same as SH +_{Def} ∼ PS′. Thus, since SH +_{Def} ∼ PS = SH +_{Def} , it is not surprising that it is precisely the added component TS_{n} that is removed when we compute the complement for SH +_{Def} with respect to PS′.

We also note that, in [8], the fact that one of the components found by decomposition (here called TS_{n}) has only two elements is seemingly regarded as a positive thing, because [8, Section 1] “This shows that domain decomposition can lead to great gains in the size of the representation.” In our humble opinion, if one of the components is very small (e.g., only 2 elements in this case) this means that almost all the complexity remained elsewhere. If the objective is to decompose in order to find space saving representations for domains and to simplify domain verification problems, then “balanced” decompositions (that is, into parts of nearly equal complexity) should instead be regarded as the best one can hope for.

It should be stressed that the problems outlined above are not dependent on the particular domain chosen and, in our opinion, they are mainly related to the methodology for decomposing a domain. Indeed, we argue that complementation alone is not sufficient to obtain truly minimal decompositions of domains. The reason being that complementation only depends on the domain’s data (that is, the domain elements and the partial order relation modeling their intrinsic precision), while it is completely independent from the domain operators that manipulate that data. In particular, if the concrete domain contains elements that are redundant with respect to its operators (because the observable behavior of these elements is exactly the same in all possible program contexts) then any factorization of the domain obtained by complementation will encode this redundancy. However, the theoretical solution to this problem is well known [6, 9, 10] and it is straightforward to improve the methodology so as to obtain truly minimal decompositions: first remove all redundancies from the domain (this can be done by computing the quotient of a domain with respect to the observable behavior) and only then decompose it by complementation. This is exactly what is done here.

We conclude with some remarks on complementation. There are a number of reasons why we believe this is important. First of all, complementation is really an excellent concept to work with from a theoretical point of view: it allows the splitting of complex domains into simpler components, avoiding redundancies between them. However, as things stand at present, complementation has never been exploited. This may be because it is easier to implement a single complex domain than to implement several simpler domains and integrate them together. Note that complementation requires the implementation of a full-integration between components (i.e., the reduced product), otherwise precision would be lost and the theoretical results would not apply.

One notable example of domain decomposition that does enable significant memory and time savings with no precision loss is the GER decomposition of Pos [2], and this is not based on complementation. Observe that the complement of G with respect to Pos is Pos itself. This is because Pos is isomorphic to SH [3] and G ≡ Con =^{def} TS_{1} so that, by Eq. (3), Pos ∼ G = Pos. It is not difficult to observe that the same phenomenon happens if one considers the groundness equivalence component E, that is, Pos ∼ E = Pos. In fact, it can be shown that two variables x and y are ground-equivalent in sh ∈ SH ≡ Pos if and only if rel({x}, sh) = rel({y}, sh). In particular, this implies both {x} ∉ sh and {y} ∉ sh. Thus, it can be easily observed that in all the dual-atoms of Pos no variable is ground-equivalent to another variable (because each dual-atom lacks just a single sharing-group).

References

1. R. Bagnara, P. M. Hill, and E. Zaffanella. Set-sharing is redundant for pair-sharing. In P. Van Hentenryck, editor, Static Analysis: Proceedings of the 4th International Symposium, volume 1302 of Lecture Notes in Computer Science, pages 53–67, Paris, France, 1997. Springer-Verlag, Berlin.

2. R. Bagnara and P. Schachte. Factorizing equivalent variable pairs in ROBDD-based implementations of Pos. In A. M. Haeberer, editor, Proceedings of the “Seventh International Conference on Algebraic Methodology and Software Technology (A-MAST’98)”, volume 1548 of Lecture Notes in Computer Science, pages 471–485, Amazonia, Brazil, 1999. Springer-Verlag, Berlin.

3. M. Codish and H Søndergaard. The Boolean logic of set sharing analysis. In C. Palamidessi, H. Glaser, and K. Meinke, editors, Principles of Declarative Programming, volume 1490 of Lecture Notes in Computer Science, pages 89–100, Pisa, Italy, 1998. Springer-Verlag, Berlin.

4. A. Cortesi, G. Filé, R. Giacobazzi, C. Palamidessi, and F. Ranzato. Complementation in abstract interpretation. In A. Mycroft, editor, Static Analysis: Proceedings of the 2nd International Symposium, volume 983 of Lecture Notes in Computer Science, pages 100–117, Glasgow, UK, 1995. Springer-Verlag, Berlin.

5. A. Cortesi, G. Filé, R. Giacobazzi, C. Palamidessi, and F. Ranzato. Complementation in abstract interpretation. ACM Transactions on Programming Languages and Systems, 19(1):7–47, 1997.

6. A. Cortesi, G. Filé, and W. Winsborough. The quotient of an abstract interpretation for comparing static analyses. Theoretical Computer Science, 202(1&2):163– 192, 1998.

7. 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, 1979.

8. G. Filé and F. Ranzato. Complementation of abstract domains made easy. In M. Maher, editor, Logic Programming: Proceedings of the Joint International Conference and Symposium on Logic Programming, MIT Press Series in Logic Programming, pages 348–362, Bonn, Germany, 1996. The MIT Press.

9. R. Giacobazzi and F. Ranzato. Completeness in abstract interpretation: a domain perspective. In M. Johnson, editor, Proceedings of the 6th International Conference on Algebraic Methodology and Software Technology (AMAST’97), volume 1349 of Lecture Notes in Computer Science, pages 231–245, Sydney, Australia, 1997. Springer-Verlag, Berlin.

10. R. Giacobazzi, F. Ranzato, and F. Scozzari. Complete abstract interpretations made constructive. In J. Gruska and J. Zlatuska, editors, Proceedings of 23rd International Symposium on Mathematical Foundations of Computer Science (MFC-S’98), volume 1450 of Lecture Notes in Computer Science, pages 366–377. Springer-Verlag, Berlin, 1998.

11. G. Gierz, K. H. Hofmann, K. Keimel, J. D. Lawson, M. Mislove, and D. S. Scott. A Compendium of Continuous Lattices. Springer-Verlag, Berlin, 1980.

12. P. M. Hill, R. Bagnara, and E. Zaffanella. The correctness of set-sharing. In G. Levi, editor, Static Analysis: Proceedings of the 5th International Symposium, volume 1503 of Lecture Notes in Computer Science, pages 99–114, Pisa, Italy, 1998. Springer-Verlag, Berlin.

13. D. Jacobs and A. Langen. Static analysis of logic programs for independent AND parallelism. Journal of Logic Programming, 13(2&3):291–314, 1992.