Efficient Structural Information Analysis for Real CLP Languages^{⋆}

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, U. K.

                    hill@comp.leeds.ac.uk

Abstract. We present the rational construction of a generic domain for structural information analysis of CLP languages called Pattern(D^{♯}), where the parameter D^{♯} is an abstract domain satisfying certain properties. Our domain builds on the parameterized domain for the analysis of logic programs Pat(ℜ), which is due to Cortesi et al. However, the formalization of our CLP abstract domain is independent from specific implementation techniques: Pat(ℜ) (suitably extended in order to deal with CLP systems omitting the occur-check) is one of the possible implementations. Reasoning at a higher level of abstraction we are able to appeal to familiar notions of unification theory. This higher level of abstraction also gives considerable more latitude for the implementer. Indeed, as demonstrated by the results summarized here, an analyzer that incorporates structural information analysis based on our approach can be highly competitive both from the precision and, contrary to popular belief, from the efficiency point of view.

1 Introduction

Most interesting CLP languages [16] offer a constraint domain that is an amalgamation of a domain of syntactic trees — like the classical domain of finite trees (also called the Herbrand domain) or the domain of rational trees [9] — with a set of “non-syntactic” domains, like finite domains, the domain of rational numbers and so forth. The inclusion of uninterpreted functors is essential for preserving Prolog programming techniques. Moreover, the availability of syntactic constraints greatly contributes to the expressive power of the overall language. When syntactic structures can be used to build aggregates of interpreted terms one can express, for instance, “records” or “unbounded containers” of numerical quantities.

From the experience gained with the first prototype version of the China data-flow analyzer [1] it was clear that, in order to attain a significant precision

⋆ This work has been partly supported by MURST project “Certificazione automatica di programmi mediante interpretazione astratta.” Some of this work was done during a visit of the first and third authors to Leeds, funded by EPSRC under grant M05645.

in the analysis of numerical constraints in CLP languages, one must keep at least part of the uninterpreted terms in concrete form. Note that almost any analysis is more precise when this kind of structural information is retained to some extent: in the case mentioned here the precision loss was just particularly acute. Of course, structural information is very valuable in itself. When exploited for optimized compilation it allows for enhanced clause indexing and simplified unification. Moreover, several program verification techniques are highly dependent on this kind of information.

Cortesi et al. [10, 11], after the work of Musumbu [21], put forward a very nice proposal for dealing with structural information in the analysis of logic programs. Using their terminology, they defined a generic abstract domain Pat(ℜ) that automatically upgrades a domain ℜ (which must support a certain set of elementary operations) with structural information.

As far as the overall approach is concerned, we extend the work described in [11] by allowing for the analysis of any CLP language [16]. Most importantly, we do not assume that the analyzed language performs the occur-check in the unification procedure. This is an important contribution, since the vast majority of real (i.e., implemented) CLP languages (in particular, almost all Prolog systems) do omit the occur-check, either as a mere efficiency measure or because they are based upon a theory of extended rational trees [9]. We describe a generic construction for structural analysis of CLP languages. Given an abstract domain D^{♯} satisfying a small set of very reasonable and weak properties, the structural abstract domain Pattern(D^{♯}) is obtained automatically by means of this construction. In contrast to [11], where the authors define a specific implementation of the generic structural domain (e.g., of the representation of term-tuples), the formalization of Pattern(·) is implementation-independent: Pat(ℜ) (suitably extended in order to deal with CLP languages and with the occur-check problem) is a possible base for the implementation. Reasoning at a higher level of abstraction we are able to appeal to familiar notions of unification theory [18]. One advantage is that we can identify an important parameter (a common anti-instance function) that gives some control over the precision and computational cost of the resulting structural domain. In addition, we believe our implementation-independent treatment can be more easily adapted to different analysis frameworks/systems.

One of the merits of Pat(ℜ) is to define a generic implementation that works on any domain ℜ that provides a certain set of elementary, fine-grained operations. Because of the simplicity of these operations it is particularly easy to extend an existing domain in order to accommodate them. However, this simplicity has a high cost in terms of efficiency: the execution of many isolated small operations over the underlying domain is much more expensive than performing few macro-operations where global effects can be taken into account. The operations that the underlying domain must provide are thus more complicated in our approach. However, this extra complication and the higher level of abstraction give considerable more latitude for the implementer. Indeed, as demonstrated by the results summarized here, an analyzer that incorporates structural information analysis based on our approach can be highly competitive both from the precision and the efficiency point of view. One of the contributions of this paper is that it disproves the common belief (now reinforced by [8]) whereby abstract domains enhanced with structural information are inherently inefficient.

The paper is structured as follows: Section 2 introduces some basic concepts and the notation that will be used in the paper; Section 3 presents the main ideas behind the tracking of explicit structural information for the analysis of CLP languages; Section 4 introduces the D^{♯} and Pattern(D^{♯}) domains and explains how an abstract semantics based on D^{♯} can systematically be upgraded to one on Pattern(D^{♯}); Section 5 summarizes the extensive experimental evaluation that has been conducted to validate the ideas presented in this paper; Section 6 presents a brief discussion of related work and, finally, Section 7 concludes with some final remarks.

2 Preliminaries

Let U be a set. The cardinality of U is denoted by |U|. We will denote by U^{n} the set of n-tuples of elements drawn from U, whereas U^{∗} denotes ⋃_{n∈ℕ} U^{n}. Elements of U^{∗} will be referred to as tuples or as sequences. The empty sequence, i.e., the only element of U^{0}, is denoted by ε. Throughout the paper all variables denoting sequences will be written with a “bar accent” like in s̄. For s̄ ∈ U^{∗}, the length of s̄ will be denoted by |s̄|. The concatenation of the sequences s̄_{1}, s̄_{2} ∈ U^{∗} is denoted by s̄_{1} ::s̄_{2}. For each s̄ ∈ U^{⋆} and each set X ∈ ℘_{f}(U), the sequence s̄\X is obtained by removing from s̄ all the elements that appear in X. The projection mappings π_{i}: U^{n} → U are defined, for i = 1, …, n, by π_{i}((e_{1}, …, e_{n})) = e_{i}. We will also use the liftings π_{i}: ℘(U^{n}) → ℘(U) given by π_{i}(S) = { π_{i}(s̄) | s̄ ∈ S }. If a sequence s̄ is such that |s̄| ≥ i, we let prefix_{i}(s̄) denote the sequence of the first i elements of s̄.

Let Vars denote a denumerable and totally ordered set of variable symbols. We assume that Vars contains (among others) two infinite, disjoint subsets: z and z′. Since Vars is totally ordered, z and z′ are as well. Thus we assume z = (Z_{1}, Z_{2}, Z_{3}, … and z′ = (Z′_{1}, Z′_{2}, Z′_{3}, . . .. If W ⊆ Vars we will denote by T_{W} the set of terms with variables in W. For any term or a tuple of terms t we will denote the set of variables occurring in t by vars(t). We will also denote by vseq(t) the sequence of first occurrences of variables that are found on a depth-first, leftto-right traversal of t. For instance, vseq((f(g(X), Y), h(X))) = (X, Y).

We implement the “renaming apart” mechanism by making use of two strong normal forms for tuples of terms. Specifically, the set of n-tuples in z-form is given by T_{z}^{n} = { t̄ ∈ T_{Vars}^{n} | vseq(t̄) = (Z_{1}, Z_{2}, …, Z_{|vars(t̄)|}) }. The set of all the tuples in z-form is denoted by T_{z}^{∗}. The definitions for T_{z′}^{n} and T_{z′}^{∗} are obtained in a similar way, by replacing z with z′. There is a useful device for toggling between z- and z′-forms. Let t̄ ∈ T_{z}^{n} ∪ T_{z′}^{n} and |vars(t̄)| = m. Then t̄′ = t̄[Z′_{1}/Z_{1}, …, Z′_{m}/Z_{m}], if t̄ ∈ T_{z}^{n}, and t̄[Z_{1}/Z′_{1}, …, Z_{m}/Z′_{m}], if t̄ ∈ T_{z′}^{n}. Notice that t̄′′ = (t̄′)′ = t̄.

When V̄ ∈ Vars^{m} and t̄ ∈ T_{Vars}^{m} we use [t̄/V̄] as a shorthand for the substitution [π_{1}(t̄)/π_{1}(V̄), …, π_{m}(t̄)/π_{m}(V̄)], if m > 0, and to denote the empty substitution if m = 0. If vars(t̄) ∩ V̄ = ∅, then [t̄/V̄] is idempotent. Suppose that s̄ = (s_{1}, …, s_{m}) ∈ T_{Vars}^{m} and t̄ = (t_{1}, …, t_{m}) ∈ T_{Vars}^{m}, then, s̄ = t̄ denotes (s_{1} = t_{1}, …, s_{m} = t_{m}). It is also useful to sometimes regard a substitution [t̄/V̄] as the finite set of equations V̄ = t̄. A couple of observations are useful for what follows. If s̄ ∈ T_{z}^{∗} and ū ∈ T_{z}^{|vars(s̄)|}, then s̄′[ū/vseq(s̄′)] ∈ T_{z}^{∗}. Moreover vseq(s̄′[ū/vseq(s̄′)]) = vseq(ū).

The logical theory underlying a CLP constraint system [16] is denoted by 𝔗. To simplify the notation, we drop the outermost universal quantifiers from (closed) formulas so that if F is a formula with free variables Z̄, then we write 𝔗 ⊧ F to denote the expression 𝔗 ⊧ ∀Z̄ : F.

The notation f: A ↣ B signifies that f is a partial function from A to B.

3 Making the Herbrand Information Explicit

A quite general picture for the analysis of a CLP language is as follows. We want to describe a (possibly infinite) set of constraint stores over a tuple of variables of interest V̄ = (V_{1}, …, V_{k}). Each constraint store can be represented, at some level of abstraction, by a formula of the kind ∃_{Δ} . ((V̄ = t̄) ∧ C), where (V̄ = t̄), with t̄ ∈ T_{Vars}^{k}, is a system of Herbrand equations in solved form, C ∈ C^{♭} is a constraint on the concrete constraint domain C^{♭}, and the set Δ = vars(C) ∪ vars(t̄) is such that Δ ∩ V̄ = ∅. Roughly speaking, C limits the values that the quantified variables occurring in t̄ can take. Notice that this treatment does not exclude the possibility of dealing with domains of rational trees: the non-Herbrand constraints will simply live in the constraint component. For example, the constraint store resulting from execution of the SICStus goal ‘?- X = f(a, X)’ may be captured by ∃X . ({V_{1} = X} ∧ X = f(a, X)) but also by ∃X . ({V_{1} = f(a, X)} ∧ X = f(a, X)).

Once variables V̄ have been fixed, the Herbrand part of the constraint store can be represented as a k-tuple of terms. We are thus assuming a concrete domain where the Herbrand information is explicit and other kinds of information are captured by some given constraint domain C^{♭}. For instance, if the target language of the analysis is CLP(R) [17], C^{♭} may encode conjunctions of equations and inequations over arithmetic expressions, the mechanisms for delaying non-linear constraints, and other peculiarities of the arithmetic part of the language. We assume constraints are modeled by logical formulas, so that it makes sense to talk about the free variables of C^{♭} ∈ C^{♭}, denoted by FV (C^{♭}). These are the variables that the constraint solver makes visible to the Herbrand engine, all the other variables being restricted in scope to the solver itself. Since we want to characterize any set of constraint stores, our concrete domain is

D^{♭} = ⋃_{n∈ℕ} ℘({ (s̄, C^{♭}) | s̄ ∈ T_{z}^{n}, C^{♭} ∈ C^{♭}, FV (C^{♭}) ⊆ vars(s̄) })

partially ordered by subset inclusion.

\xymatrix{℘(T_{z}^{∗} × C^{♭}) \ar[r]^{α} \ar[d]_{Φ_{ϕ}} & D^{♯} \\ T_{z}^{∗} × ℘(T_{z}^{∗} × C^{♭}) \ar[r]_{(id,α)} \ar[u]_{Φ_{ϕ}^{−1}} & T_{z}^{∗} × D^{♯} \ar@{.>}[u]_{α′}}

Fig. 1. Upgrading a domain with structural information.

An abstract interpretation [12] of D^{♭} can be specified by choosing an abstract domain D^{♯} and a suitable abstraction function α: D^{♭} → D^{♯}. If D^{♯} is not able to encode enough structural information from C^{♭} so as to achieve the desired precision, it is possible to improve the situation by keeping some Herbrand information explicit. One way of doing that is to perform a change of representation for D^{♭} and use the new representation as the basis for abstraction. The new representation is obtained by factoring out some common Herbrand information. The meaning of ‘some’ is encoded by a function.

Definition 1. (Common anti-instance function.) For each n ∈ ℕ, a function ϕ: ℘(T_{z}^{n}) → T_{z′}^{n} is called a common anti-instance function if and only if the following holds: whenever T ∈ ℘(T_{z}^{n}), if ϕ(T) = r̄′ and |vars(r̄)| = m with m ≥ 0, then ∀t̄ ∈ T : ∃ū ∈ T_{z}^{m} . r̄′[ū/vseq(r̄′)] = t̄. In words, ϕ(T) is an anti-instance [18], in z′-form, of each t̄∈ T.

Any choice of ϕ induces a function Φ_{ϕ}: D^{♭} → T_{z}^{∗} × D^{♭}, which is given, for each E^{♭} ∈ D^{♭}, by Φ_{ϕ}(E^{♭}) = (s̄, { (ū, G^{♭}) | (t̄, G^{♭}) ∈ E^{♭}, s̄′[ū/vseq(s̄′)] = t̄}), where s̄′ = ϕ(π_{1}(E^{♭})). The corestriction to the image of Φ_{ϕ}, that is the function Φ_{ϕ}: D^{♭} → Φ_{ϕ}(D^{♭}), is an isomorphism, the inverse being given, for each F^{♭} ∈ D^{♭}, by Φ_{ϕ}^{−1}((s̄, F^{♭})) = { (s̄′[ū/vseq(s̄′)], G^{♭}) | (ū, G^{♭}) ∈ F^{♭} }.

So far, we have just chosen a different representation for D^{♭}, that is Φ_{ϕ}(D^{♭}). The idea behind structural information analysis is to leave the first component of the new representation (the pattern component) untouched, while abstracting the second component by means of α, as illustrated in Figure 1. The dotted arrow indicates a residual abstraction function α′. As we will see in Section 4.2, such a function is implicitly required in order to define an important operation over the new abstract domain T_{z}^{∗} ×D^{♯}. Notice that, in general, α′ does not make the diagram of Figure 1 commute.

This approach has several advantages. First, factoring out common structural information improves the analysis precision, since part of the approximated ktuples of terms is recorded, in concrete form, into the first component of T_{z}^{∗}×D^{♯}. Secondly, the above construction is adjustable by means of the parameter ϕ. The most precise choice consists in taking ϕ to be a least common anti-instance (lca) function. For example, the set E^{♭} = {⟨(s(0), Z_{1}), C_{1}⟩, ⟨(s(s(0)), Z_{1}), C_{2}⟩}, is mapped onto Φ_{lca}(E^{♭}) = ((s(Z_{1}), Z_{2}), {⟨(0, Z_{1}), C_{1}⟩, ⟨(s(0), Z_{1}), C_{2}⟩}), where C_{1}, C_{2} ∈ C^{♭}. At the other end of the spectrum is the possibility of choosing ϕ so that it returns a k-tuple of distinct variables for each set of k-tuples of terms. This corresponds to a framework where structural information is simply discarded. With this choice, E^{♭} would be mapped onto ((Z_{1}, Z_{2}), E^{♭}). In-between these two extremes there are a number of possibilities that help to manage the complexity/precision tradeoff. The tuples returned by ϕ can be limited in depth, for instance. Another possibility is to limit them in size, that is, limiting the number of occurrences of symbols or the number of variables. This flexibility enables the analysis’ domains to be designed without considering the structural information: the problem for the domain designers is to approximate the elements of ℘(T_{z}^{k} × C^{♭}) with respect to the property of interest. It does not really matter whether k is fixed by the arity of a predicate or k is the number of variables occurring in a pattern.

4 Parametric Structural Information Analysis

In this section we describe how a complete abstract semantics — which includes an abstract domain plus all the operations needed to approximate the concrete semantics — can be turned into one keeping track of structural information.

We first need some assumptions on the domain C^{♭}, which represents the non-Herbrand part of constraint stores. Following [14], it is not at all restrictive to assume that, in order to define the concrete semantics of programs, four operations over C^{♭} need to be characterized. These model the constraint accumulation process, parameter passing, projection, and renaming apart (see also [1, 2] on this subject).

Constraint accumulation is modeled by the binary operator ‘⊗’: C^{♭}×C^{♭} → C^{♭} and the unsatisfiability condition in the constraint solver is modeled by the special value ⊥^{♭} ∈ C^{♭}. Notice that, while ‘⊗’ may be reasonably expected to satisfy certain properties, such as ∀C^{♭} ∈ C^{♭} : ⊥^{♭} ⊗ C^{♭} = ⊥^{♭}, these are not really required for what follows. The same applies to all the other operators we will introduce: only properties that are actually used will be singled out.

Parameter passing requires, roughly speaking, the ability of adding equality constraints to a constraint store. Notice that we assume C^{♭} and its operations encode both the proper constraint solver and the so called interface between the Herbrand engine and the solver [16]. In particular, the interface is responsible for type-checking of the equations it receives. For example in CLP(R) the interface is responsible for the fact that X = a cannot be consistently added to a constraint store where X was previously classified as numeric.

Another ingredient for defining the concrete semantics of any CLP system is the projection of a satisfiable constraint store onto a set of variables. This is modeled by the family of operators { ¶_{Δ}^{♭}: C^{♭} → C^{♭} | Δ ∈ ℘_{f}(Vars) }. If Δ is a finite set of variables and C^{♭} ∈ C^{♭} represents a satisfiable constraint store (i.e., C^{♭} ≠ ⊥^{♭}), then ¶_{Δ}^{♭} C^{♭} represents the projection of C^{♭} onto the variables in Δ.

For each s̄, t̄ ∈ T_{z}^{∗}, we write ϱs̄(t̄) (read “rename t̄ away from s̄”) to denote t̄[Z_{n+1}/Z_{1}, …, Z_{n+m}/Z_{m}], where n = |vars(s̄)| and m = |vars(t̄)|. The ϱ operator is useful for concatenating normalized term-tuples, still obtaining a normalized term-tuple, since we have s̄:: ϱs̄(t̄) ∈ T_{z}^{∗}. The renaming apart has to be extended to elements of D^{♭}. Let C^{♭} ∈ C^{♭} such that FV (C^{♭}) ⊆ vars(t̄). Then ϱs̄((t̄, C^{♭})) denotes the pair (ϱs̄(t̄), C_{1}^{♭}), where C_{1}^{♭} ∈ C^{♭} is obtained from C^{♭} by applying the same renaming applied to t̄ in order to obtain ϱs̄(t̄).

Term tuples are normalized by a normalization function η: T_{Vars}^{∗} → T_{z}^{∗} such that, for each ū ∈ T_{Vars}^{∗}, the resulting tuple η(ū) ∈ T_{z}^{∗} is a variant of ū. As for ϱ, the normalization function has to be extended to elements of D^{♭}. Suppose that G^{♭} ∈ C^{♭} where FV (G^{♭}) ⊆ vars(ū). then η((ū, G^{♭})) denotes (η(ū), G_{1}^{♭}) ∈ D^{♭} where it is assumed that G_{1}^{♭} can be obtained from G^{♭} by applying the same renaming applied to ū in order to obtain η(ū).

We will now show how any abstract domain can be upgraded so as to capture structural information by means of the Pattern(·) construction. Then we will focus our attention on the abstract semantic operators.

4.1 From D^{♯} to Pattern(D^{♯})

Since one of the driving aims of this work is maximum generality, we refer to a very weak abstract interpretation framework [12]. To start with, we assume very little on abstract domains.

Definition 2. (Abstract domain for D^{♭}.) An abstract domain for D^{♭} is a set P^{♯} equipped with a preorder relation ‘⪯’ ⊆ P^{♯} ×P^{♯}, an order preserving function γ: P^{♯} → D^{♭}, and a least element ⊥^{♯} such that γ(⊥^{♯}) = ∅. Moreover, γ is such that if (p̄_{1}, C^{♭}) ∈ γ(E^{♯}), and 𝔗 ⊧ C^{♭} → p̄_{1} = p̄_{2}, then η((p̄_{2}, C^{♭})) ∈ γ(E^{♯}).

Informally, P^{♯} is a set of abstract properties on which the notion of “relative precision” is captured by the preorder ‘⪯’. Moreover, P^{♯} is related to the concrete domain D^{♭} by means of a concretization function γ that specifies the soundness correspondence between D^{♭} and P^{♯}. The distinguished element ⊥^{♯} models an impossible state of affairs. In this framework, d^{♯} ∈ P^{♯} is a safe approximation of d^{♭} ∈ D^{♭} if and only if d^{♭} ⊆ γ(d^{♯}).

Suppose we are given an abstract domain complying with Definition 2. Here is how it can be upgraded with explicit structural information.

Definition 3. (The Pattern(·) construction.) Let D^{♯} be an abstract domain for D^{♭} and let γ be its concretization function. Then

Pattern(D^{♯}) = {⊥_{p}^{♯}} ∪ { (s̄, E^{♯}) ∈ T_{z}^{∗} × D^{♯} | γ(E^{♯}) ⊆ T_{z}^{|vars(s̄)|} × C^{♭} }.

The meaning of each element (s̄, E^{♯}) ∈ Pattern(D^{♯}) is given by the concretization function γ_{p}: Pattern(D^{♯}) → D^{♭} such that γ_{p}(⊥_{p}^{♯}) = ∅ and

γ_{p}((s̄, E^{♯})) = \{ η((r̄, C^{♭})) | \begin{matrix}(ū, C^{♭}) ∈ γ(E^{♯}) \\ 𝔗 ⊧ C^{♭} → r̄ = s̄′[ū/vseq(s̄′)] \end{matrix} \}.

We also define the binary relation ‘⪯_{p}’ ⊆ Pattern(D^{♯}) × Pattern(D^{♯}) given, for each d_{1}^{♯}, d_{2}^{♯} ∈ Pattern(D^{♯}), by d_{1}^{♯} ⪯_{p} d_{2}^{♯} ⟺ γ_{p}(d_{1}^{♯}) ⊆ γ_{p}(d_{2}^{♯}).

It can be seen that Pattern(D^{♯}) is an abstract domain in the sense of Definition 2 provided D^{♯} is. Thus Pattern(D^{♯}) can constitute the basis for designing an abstract semantics for CLP. This will usually require selecting an abstract semantic function on Pattern(D^{♯}), an effective convergence criterion for the abstract iteration sequence (notice that the ‘⪯’ and ‘⪯_{p}’ relations are not required to be computable), and perhaps a convergence acceleration method ensuring rapid termination of the abstract interpreter [12]. The last ingredient to complete the recipe is a computable way to associate an abstract description d^{♯} ∈ Pattern(D^{♯}) to each concrete property d^{♭} ∈ D^{♭}. For this purpose, the existence of a computable function α_{p}: D^{♭} → Pattern(D^{♯}) such that, for each d^{♭} ∈ D^{♭}, d^{♭} ⊆ γ_{p}(α_{p}(d^{♭})) is assumed.

While one option is to design an abstract semantics based on Pattern(D^{♯}) from scratch, it is more interesting to start with an abstract semantics centered around D^{♯}. In this case, it is possible to systematically lift the semantic construction to Pattern(D^{♯}).

4.2 Operations over D^{♯} and Pattern(D^{♯})

We now present the abstract operations we assume on D^{♯} and the derived operations over Pattern(D^{♯}). Each operator on D^{♯} is introduced by means of safety conditions that ensure the safety of the derived operators over Pattern(D^{♯}).

Given the abstract domain, there are still many degrees of freedom for the design of a constructive abstract semantics. Thus, choices have to be made in order to give a precise characterization. In what follows we continue to strive for maximum generality. Where this is not possible we detail the design choices we have made in the development of the China analyzer [1]. While some things may need adjustments for other analysis frameworks, the general principles should be clear enough for anyone to make the necessary changes.

Meet with Renaming Apart We call meet with renaming apart (denoted by ‘▷’) the operation of taking two descriptions in D^{♯} and, roughly speaking, juxtaposing them. This is needed when “solving” a clause body with respect to the current interpretation and corresponds, at the concrete level, to a renaming followed by an application of the ‘⊗’ operator. Its counterpart on Pattern(D^{♯}) is denoted by ‘rmeet’ and defined as follows.

Definition 4. (‘▷’ and ‘rmeet’) Let ‘▷’: D^{♯} × D^{♯} → D^{♯} be such that, for each E_{1}^{♯}, E_{2}^{♯} ∈ D^{♯},

γ(E_{1}^{♯} ▷ E_{2}^{♯}) = \{ η((r̄, C_{1}^{♭} ⊗ G_{2}^{♭})) | \begin{matrix}(r̄_{1}, C_{1}^{♭}) ∈ γ(E_{1}^{♯}) \\ (r̄_{2}, C_{2}^{♭}) ∈ γ(E_{2}^{♯}) \\ (w̄_{2}, G_{2}^{♭}) = ϱr̄_{1}((r̄_{2}, C_{2}^{♭})) \\ 𝔗 ⊧ (C_{1}^{♭} ⊗ G_{2}^{♭}) → r̄ = r̄_{1} :: w̄_{2} \end{matrix} \}.

Then, we define rmeet((s̄_{1}, E_{1}^{♯}), (s̄_{2}, E_{2}^{♯})) = (s̄_{1} :: ϱs̄_{1}(s̄_{2}), E_{1}^{♯} ▷ E_{2}^{♯}), for each (s̄_{1}, E_{1}^{♯}), (s̄_{2}, E_{2}^{♯}) ∈ Pattern(D^{♯}).

A consequence of this definition is that there is no precision loss in ‘rmeet’ [3].

Parameter Passing Concrete parameter passing is realized by an extended unification procedure. Unification is extended because it must involve the constraint solver(s). Remember that our notion of “constraint solver” includes also the interface between the Herbrand engine and the proper solver [16]. The interface needs to be notified about all the bindings performed by the Herbrand engine in order to maintain consistency between the solver and the Herbrand part. We also assume that CLP programs are normalized in such a way that interpreted function symbols only occur in explicit constraints (note that this is either required by the language syntax itself, as in the case of the clp(Q, R) libraries of SICStus Prolog, or is performed automatically by the CLP system).

At the abstract level we do not prescribe the use of any particular algorithm. This is to keep our approach as general as possible. For instance, an implementor is not forced to use any particular representation for term-tuples (as in [11]). Similarly, one can choose any sound unification procedure that works well with the selected representation. Of particular interest is the possibility of choosing a representation and procedure that closely match the ones employed in the concrete language being analyzed. In this case, all the easy steps typical of any unification procedure (functor name/arity checks, peeling, and so on) will be handled, at the abstract level, exactly as they are at the concrete level. The only crucial operation in abstract parameter passing over Pattern(D^{♯}) is the binding of an abstract variable to an abstract term. This is performed by first applying a non-cyclic approximation of the binding to the pattern component and then notifying the original (possibly cyclic) binding to the abstract constraint component. The correctness of this approach can be proved [3] by assuming the existence of a bind operator on the underlying abstract constraint system satisfying the following condition.

Definition 5. (bind) Let E^{♯} ∈ D^{♯} be a description such that γ(E^{♯}) ⊆ T_{z}^{m} × C^{♭}. Let Z̄ = (Z_{1}, …, Z_{m}), u ∈ TZ̄, vseq(u) = (Z_{j_{1}}, …, Z_{j_{l}}) and let 1 ≤ h ≤ m. Then, define (k_{1}, …, k_{m_{1}}) = ((1, …, h − 1) :: ((j_{1}, …, j_{l}) \ {1, …, h − 1}) :: ((h + 1, …, m) \ {j_{1}, …, j_{l}})). If E_{1}^{♯} = bind(E^{♯}, u, Z_{h}), then,

γ(E_{1}^{♯}) ⊇ \{ η((q̄θ, C_{1}^{♭})) | \begin{matrix}(p̄, C^{♭}) ∈ γ(E^{♯}) \\ p̄ = (p_{1}, …, p_{m}) \\ q̄ = (p_{k_{1}}, …, p_{k_{m_{1}}} ) \\ θ is an idempotent substitution \\ FV (C_{1}^{♭}) ⊆ vars(q̄θ) \\ 𝔗 ⊧ θ ← (Z′_{h} = u′)[p̄/Z̄′] \\ 𝔗 ⊧ C_{1}^{♭} ↔ ((Z′_{h} = u′)[p̄/Z̄′] ∧ C^{♭})θ \end{matrix} \}.

Note that m_{1} = m − 1 if Z_{h} ∉ vars(u), and m_{1} = m, otherwise.

To motivate and explain the above condition on E_{1}^{♯} = bind(E^{♯}, u, Z_{h}), suppose that p̄ is the pattern component and C^{♭} the constraint component of an element in the concretization of E^{♯}. Now, the pattern components of elements of the abstract domain Pattern(D^{♯}) are always in normal form and thus, after applying the binding [u′/Z′_{h}] to an element of E^{♯}, we must apply the normalization function so that the result is also in Pattern(D^{♯}). This will first remove the h-th term Z_{h} in the case that Z_{h} does not occur in u and then permute the remaining elements of Z̄. A corresponding operation is applied to the pattern p̄. That is, q̄ is constructed from p̄ first by removing the h-th term p_{h} in the case that Z_{h} does not occur in u and then by applying the same permutation as before on the remaining elements of p̄. As a most general solution ϕ to (Z′_{h} = u′)[p̄/Z̄′] may be cyclic, only an approximation of ϕ, the idempotent substitution θ, is applied to q̄. The actual solution ϕ together with C^{♭}θ is captured by the constraint C_{1}^{♭}. Finally, note that the new pattern component q̄θ may not be in normal form, so that in the condition for bind it is the normalized variant of (q̄θ, C_{1}^{♭}) that must be in the concretization of E_{1}^{♯}.

We refer the reader to [3] for a description of how any correct unification algorithm can be transformed into a correct (abstract) unification algorithm for Pattern(D^{♯}) using the bind operator and the normalization function η.

Projection When all the goals in a clause body have been solved, projection is used to restrict the abstract description to the tuple of arguments of the clause’s head. The projection operations on D^{♭} consist simply in dropping a suffix of the term-tuple component, with the consequent projection on the underlying constraint domain.

Definition 6. (‘project_{k}^{♭}’) { project_{k}^{♭}: D^{♭} → D^{♭} | k ∈ ℕ } is a family of operations such that, for each k ∈ ℕ and each (ū, C^{♭}) ∈ D^{♭} with |ū| ≥ k, if we define Δ = vars(prefix_{k}(ū)), then project_{k}^{♭}((ū, C^{♭})) = (prefix_{k}(ū), ¶_{Δ}^{♭} C^{♭}).

We now introduce the corresponding projection operations on Pattern(D^{♯}) and, in order to establish their correctness, we impose a safety condition on the projection operations of D^{♯}.

Definition 7. (¶_{k}^{♯} and project_{k}^{♯}) Assume we are given a family of operations { ¶_{k}^{♯}: D^{♯} → D^{♯} | k ∈ ℕ } such that, for each E^{♯} ∈ D^{♯} with γ(E^{♯}) ⊆ T_{z}^{m} × C^{♭} and each k ≤ m, γ(¶_{k}^{♯} E^{♯}) ⊇ { project_{k}^{♭}((ū, C^{♭})) | (ū, C^{♭}) ∈ γ(E^{♯}) }. Then, for each (s̄, E^{♯}) ∈ Pattern(D^{♯}) such that s̄ ∈ T_{z}^{m} and each k ≤ m, we define project_{k}^{♯}((s̄, E^{♯})) = (prefix_{k}(s̄), ¶_{j}^{♯} E^{♯}), where j = |vars(prefix_{k}(s̄))|.

With these definitions ‘project_{k}^{♯}’ is correct with respect to ‘project_{k}^{♭}’ [3].

Remapping The operation of remapping is used to adapt a description in Pattern(D^{♯}) to a different, less precise, pattern component. Remapping is essential to the definition of various join and widening operators. Consider a description (s̄, E♯ ; s̄) ∈ Pattern(D^{♯}) and a pattern r̄′ ∈ T_{z′}^{∗} such that r̄′ is an anti-instance of s̄. We want to obtain E♯ ; r̄ ∈ D^{♯} such that γ_{p}((r̄, E♯ ; r̄)) ⊇ γ_{p}((s̄, E♯ ; s̄)). This is what we call remapping (s̄, E♯ ; s̄) to r̄′.

Definition 8. (‘remap’) Let (s̄, E♯ ; s̄) ∈ Pattern(D^{♯}) be a description with s̄ ∈ T_{z}^{k} and let r̄′ ∈ T_{z′}^{k} be an anti-instance of s̄. Assume also |vars(r̄)| = m and let ū ∈ T_{z}^{m} be the unique tuple such that r̄′[ū/vseq(r̄′)] = s̄. Then the operation remap(s̄, E♯ ; s̄, r̄′) yields E♯ ; r̄ such that γ(E♯ ; r̄) ⊇ γ_{p}((ū, E♯ ; s̄)).

Observe that the remap function is closely related to the residual abstraction function α′ of Figure 1.^{1} With this definition, the specification of ‘remap’ meets our original requirement [3].

Upper Bound Operators A concrete (collecting) semantics for CLP will typically use set union to gather results coming from different computation paths. We assume that our base domain D^{♯} captures this operation by means of an upper bound operator ‘⊕’. Namely, for each E_{1}^{♯}, E_{2}^{♯} ∈ D^{♯} and each i = 1, 2, we have that E_{i}^{♯} ⪯ E_{1}^{♯} ⊕ E_{2}^{♯}. This is used to merge descriptions arising from the different computation paths explored during the analysis.

The operation of merging two descriptions in Pattern(D^{♯}) is defined in terms of ‘remap’. Let (s̄_{1}, E_{1}^{♯}) and (s̄_{2}, E_{2}^{♯}) be two descriptions with s̄_{1}, s̄_{2} ∈ T_{z}^{k}. The resulting description is (r̄, E_{1}^{♯} ⊕E_{2}^{♯}), where r̄′ ∈ T_{z′}^{k} is an anti-instance of both s̄_{1} and s̄_{2}, and E_{i}^{♯} = remap(s̄_{i}, E_{i}^{♯}, r̄′), for i = 1, 2. We note again that r̄′ might be the least common anti-instance of s̄_{1} and s̄_{2}, or it can be a further approximation of lca(s̄_{1}, s̄_{2}): this is one of the degrees of freedom of the framework. Thus, the family of operations we are about to present is parameterized with respect to a common anti-instance function and the analyzer may dynamically choose which anti-instance function is used at each step.

Definition 9. (‘join_{ϕ}’) Let ϕ be any common anti-instance function. The operation (partial function) join_{ϕ}: ℘_{f}(Pattern(D^{♯})) ↣ Pattern(D^{♯}) is defined as follows. For each k ∈ ℕ and each finite family F = {(s̄_{i}, E_{i}^{♯}) | i ∈ I } of elements of Pattern(D^{♯}) such that s̄_{i} ∈ T_{z}^{k} for each i ∈ I, join_{ϕ}(F) = (r̄, E^{♯}), where r̄′ = ϕ({ s̄_{i} | i ∈ I }) and E^{♯} = ⨁_{i∈I} remap(s̄_{i}, E_{i}^{♯}, r̄′).

If ϕ is any common anti-instance function then ‘join_{ϕ}’ is an upper bound operator [3].

Widenings It is possible to devise a (completely unnatural) abstract domain D^{♯} that enjoys the ascending chain condition^{2} still preventing Pattern(D^{♯}) from possessing the same property. This despite the fact that any element of T_{z}^{n} has a finite number of distinct anti-instances in T_{z′}^{n}. However, this problem is of no practical interest if the analysis applies ‘join_{ϕ}’ at each step of the iteration sequence. In this case, if we denote by (s̄_{j}, E_{j}^{♯}) ∈ Pattern(D^{♯}) the description at step j ∈ ℕ, we have (s̄_{i+1}, E_{i+1}^{♯}) = join_{ϕ}({(s̄_{i}, E_{i}^{♯}), … }), assuming no widening

1 Indeed, one can define α′ = λ(s̄, E^{♯}) ∈ T_{z}^{k} × D^{♯} . remap(s̄, E^{♯}, (Z′_{1}, …, Z′_{k})). 2 Namely, each strictly increasing chain is finite.

is employed. This implies that s̄′_{i+1} is an anti-instance of s̄_{i}. As any ascending chain in T_{z}^{n} is finite, the iteration sequence will eventually stabilize if D^{♯} enjoys the ascending chain condition.

In some cases, however, rapid termination of the analysis on D^{♯} can only be ensured by using one or more widening operators ∇: D^{♯} × D^{♯} → D^{♯} [13]. These can be lifted to work on Pattern(D^{♯}). As an example, we show the default lifting used by the China analyzer:

widen((s̄_{1}, E_{1}^{♯}), (s̄_{2}, E_{2}^{♯})) = \begin{cases}(s̄_{2}, E_{2}^{♯}), & if s̄_{1} ≠ s̄_{2}; \\ (s̄_{2}, E_{1}^{♯} ∇ E_{2}^{♯}), & if s̄_{1} = s̄_{2}. \end{cases}  (1)

This operator refrains from widening unless the pattern component has stabilized. A more drastic choice for a widening is given by

Widen((s̄_{1}, E_{1}^{♯}), (s̄_{2}, E_{2}^{♯})) = (s̄_{2}, remap(s̄_{1}, E_{1}^{♯}, s̄′_{2}) ∇ E_{2}^{♯}).  (2)

Widening operators only need to be evaluated over (s̄_{1}, E_{1}^{♯}) and (s̄_{2}, E_{2}^{♯}) when s̄′_{2} is an anti-instance of s̄_{1}. Thus, as T_{z}^{n} satisfies the ascending chain condition, ‘widen’ and ‘Widen’ are well-defined widening operators on Pattern(D^{♯}) [3].

Besides ensuring termination, widening operators are also used to accelerate convergence of the analysis. It is therefore important to be able to define widening operators on Pattern(D^{♯}) without relying on the existence of corresponding widenings on D^{♯}. There are many possibilities in this direction and some of them are currently under experimental evaluation. Just note that any upper bound operator ‘join_{ϕ}’ can be regarded as a widening as soon as the common anti-instance function ϕ is different from the lca. In order to ensure the convergence of the abstract computation, we will only consider widening operators on Pattern(D^{♯}) satisfying the following (very reasonable) condition: if (s̄, E^{♯}) is the result of the widening applied to (s̄_{1}, E_{1}^{♯}) and (s̄_{2}, E_{2}^{♯}), where s̄′_{2} is an anti-instance of s̄_{1}, then s̄′ is an anti-instance of s̄_{2}. Both widen and Widen comply with this restriction.

Comparing Descriptions The comparison operation on Pattern(D^{♯}) is used by the analyzer in order to check whether a local fixpoint has been reached.

Definition 10. (‘compare’) Let ‘≾’ ⊆ D^{♯} × D^{♯} be a computable preorder that correctly approximates ‘⪯’, that is, for each E_{1}^{♯}, E_{2}^{♯} ∈ D^{♯}, we have E_{1}^{♯} ⪯ E_{2}^{♯} whenever E_{1}^{♯} ≾ E_{2}^{♯}. The approximated ordering relation over Pattern(D^{♯}), denoted by ‘compare’ ⊆ Pattern(D^{♯}) × Pattern(D^{♯}), is defined, for each (s̄_{1}, E_{1}^{♯}), (s̄_{2}, E_{2}^{♯}) ∈ Pattern(D^{♯}), by compare((s̄_{1}, E_{1}^{♯}), (s̄_{2}, E_{2}^{♯})) ⟺ (s̄_{1} = s̄_{2} ∧ E_{1}^{♯} ≾ E_{2}^{♯}).

It must be stressed that the above ordering is “approximate” since it does not take into account the peculiarities of D^{♯}. More refined orderings can be obtained in a domain-dependent way, namely, when D^{♯} has been fixed. It is easy to show that compare is a preorder over Pattern(D^{♯}) that correctly approximates the approximation ordering ‘⪯_{p}’ [3]. The ability of comparing descriptions only when they have the same pattern is not restrictive in our setting. Indeed, the definition of join_{ϕ} and the condition we imposed on widenings ensure that any two descriptions arising from consecutive steps of the iteration sequence are ordered by the anti-instance relation. When combined with the ascending chain condition of the pattern component, this allows to inherit termination from the underlying domain D^{♯}.

5 Experimental Evaluation

We have conducted an extensive experimentation on the analysis using the Pattern(·) construction: this allowed us to tune the implementation and gain insight on the implications of keeping track of explicit structural information. To put ourselves in a realistic situation, we assessed the impact of the Pattern(·) construction on Modes, a very precise and complex domain for mode analysis. This captures information on simple types, groundness, boundedness, pairsharing, freeness, and linearity. It is a combination of, among other things, two copies of the GER representation for Pos [5] — one for groundness and one for boundedness — and the non-redundant pair-sharing domain PSD [4] with widening as described in [22]. Each of these domains has been suitably extended to ensure correctness and precision of the analysis even for systems that omit the occur-check [1, 15]. Some details on how the domains are combined can be found in [6].

The benchmark suite used for the development and tuning of the China analyzer is probably the largest one ever employed for this purpose. The suite comprises all the programs we have access to (i.e., everything we could find by systematically dredging the Internet): 300 programs, 16 MB of code, 500 K lines, the largest program containing 10063 clauses in 45658 lines of code.

The comparison between Modes and Pattern(Modes) involves the two usual things: precision and efficiency. However, how are we going to compare the precision of the domain with explicit structural information with one without it? That is something that should be established in advance. Let us consider a simple but not trivial Prolog program: mastermind.pl.^{3} Consider also the only direct query for which it has been written, ‘?- play.’, and focus the attention on the procedure extend code/1. A standard goal-dependent analysis of the program with the Modes domain is only able to tell something like

extend_code(A) :- list(A).

This means: “during any execution of the program, whenever extend code/1 succeeds it will have its argument bound to a list cell (i.e., a term whose principal functor is either '.'/2 or []/0)”. Not much indeed. Especially because this can be established instantly by visual inspection: extend code/1 is always called with a list argument and this completes the proof. If we perform the analysis with Pattern(Modes) the situation changes radically. Here is what such a domain allows China to derive:^{4}

 3 Available at http://www.cs.unipr.it/China/Benchmarks/Prolog/mastermind.pl.

4 Some extra groundness information obtained by the analysis has been omitted.

x = %inc. indep ground linear  free bound
GI GD GI GD GI GD GI GD GI GD
x < 0  0 1 0 0 0 1 0 0 0 0
x = 0 222 211 228 223 213 205 244 245 230 220
0 < x ≤ 2 36 35 24 26 46 44 26 21 49 45
2 < x ≤ 5 22 27 17 17 17 18 11 13 9 15
5 < x ≤ 10 7 8 10 11 9 11 10 8 9 8
x ≥ 10 13 18 21 23 15 21 9 13 3 12

Table 1. A summary of the Modes precision gained using structural information.

extend_code([([A|B],C,D)|E]) :- list(B), list(E),
  (functor(C,_,1);integer(C)), (functor(D,_,1);integer(D)),
  ground([C,D]), may_share([[A,B,E]]).

Under the circumstances mentioned above, this means: “the argument of procedure extend code/1 will be bound to a term of the form [([A|B],C,D)|E], where B and E are bound to list cells; C is either bound to a functor of arity 1 or to an integer, and likewise for D; both C and D are ground, and (consequently) pair-sharing may only occur between A, B, and E”.

It is clear that the analysis with Pattern(Modes) yields much more information. However, it is not clear at all how to define a fair measure for this precision gain. The approach we have chosen is simple though unsatisfactory: throw away all the structural information at the end of the analysis and compare the usual numbers (i.e., number of ground variables, number of free variables and so on). With reference to the above example, this metric pretends that explicit structural information gives no precision improvements on the analysis of extend code/1 in mastermind.pl. In fact, once all the structural information has been discarded, the analysis with Pattern(Modes) only specifies that, upon success, the argument of extend code/1 will be a list cell. In other words, we are measuring how the explicit structural information present in Pattern(Modes) improves the precision on Modes itself, which is only a tiny part of the real gain in accuracy. The value of this extra precision can only be measured from the point of view of the target application of the analysis.

It is important to note that the experimental results we are about to report have been obtained without using any widening on the pattern component. The widening operations are only propagated to the underlying Modes domain by means of the ‘widen’ operator given in Eq. (1). Moreover, the merge operation employed is always ‘join_{lca}’. For space limitations, here we can only summarize the results of the experimentation. The interested reader can find all the details at http://www.cs.unipr.it/China. As far as precision is concerned, we measure five different quantities: the total number of independent argument pairs (indep); the total number of ground argument positions; the total number of linear argument positions; the total number of free argument positions; and the total number of bound (or nonvar) argument positions.

time difference in seconds # prog.  % prog.
GI GD GI  GD
degradation ≥ 1  9 20 100.0 100.0
0.5 ≤ degradation < 1  2 4 97.0 93.3
0.2 ≤ degradation < 0.5 15 18 96.3 92.0
degradation < 0.2 105 106 91.3 86.0
same time  90 77 56.3 50.7
improvement < 0.2 34 31 26.3 25.0
0.2 ≤ improvement < 0.5 11 11 15.0 14.7
0.5 ≤ improvement < 1  9 5 11.3 11.0
improvement ≥ 1 25 28 8.3 9.3

Table 2. A summary on efficiency: the distribution of analysis time differences.

Since we are completely disregarding the precision gains coming from structural information in itself, our results give a (very pessimistic) lower bound on the overall precision improvement. The results are summarized by partitioning the benchmark suite into six classes of programs, identified by the percentage increase in precision due to the Pattern(·) construction. Table 1 gives the cardinalities of these classes for both goal-independent (GI) and goal-dependent (GD) analyses. A precision increase, on at least one of the measured quantities, is observed on more than one third of the benchmarks. The only precision decrease is due to the interaction between the Pattern(·) construction and the widenings used in the Modes domain. It is also worth observing that, on average, goal-dependent analysis is more likely to benefit from the addition of structural information.

In order to evaluate the impact on efficiency of the Pattern(·) transformation we computed the fixpoint evaluation time for all the programs, both with the Modes and with the Pattern(Modes) domains. Results are summarized by partitioning the benchmark suite into a number of classes and giving the cardinality of each class. As a first parameter, we considered the absolute time difference observed for each program.^{5} Table 2 gives the cardinality of 9 classes, distinguishing between GI and GD analyses. The numbers show that the full range of possible behaviors is indeed observable. Quite surprisingly, it is not uncommon, although inherently more precise and complex, for the case with the Pattern(·) construction to result in significant time improvements. The reason for this is only partly due to the enhanced ability of the Pattern component to be able to detect and hence prune failed computation paths. Most importantly, the description of a set of tuples of terms in Pattern(Modes) is often much more efficient

5 As the benchmark suite comprises several real programs of very respectable size, we believe that absolute time comparison is what really matters to assess the feasibility of the Pattern(·) construction with respect to the underlying domain. A time difference less than one second is an approximation of “the user will not notice.” The experiments were conducted on a PC equipped with an AMD Athlon clocked at 700 MHz, 256 MB of RAM, and running Linux 2.2.16.

T = time in secs.  GI  GD
w/o SI w SI diff. w/o SI w SI diff.
T ≥ 10  15 11 −4  22 17 −5
5 ≤ T < 10  9 5 −4  10 11 +1
1 ≤ T < 5  32 35 +3  35 43 +8
0.5 ≤ T < 1  11 21 +10  20 23 +3
0.2 ≤ T < 0.5  27 38 +11  37 46 +9
0.1 ≤ T < 0.2  164 158 −6  155 146 −9
T < 0.1  42 32 −10  21 14 −7

Table 3. A summary on efficiency: the distribution of analysis times.

than the corresponding description in Modes. Percentages in the columns on the right show how many programs are at least as good as the corresponding class. For instance, more than 85% of the benchmarks either reduce the analysis time or increase it by at most 0.2 secs. Since the occasional bad-behaving cases can be dealt with by defining a suitable widening operator on the pattern component, these results disprove the common belief that structural information has a heavy impact on the efficiency of the analysis.

As a second criterion, Table 3 partitions the benchmark suite into 7 classes based on their total fixpoint computation time, again distinguishing between GI and GD analysis. The columns labeled ‘diff.’ show how each class grows or shrinks because of the addition of structural information. It can be seen that the Pattern(·) construction causes only a minor change to the distribution, decreasing the number of benchmarks in both the fastest and the slowest classes.

6 Related Work

The use of explicit structural information has also been studied in [7], where abstract equation systems are integrated into an analysis domain tracking setsharing, freeness, linearity and compoundness. While allowing for an implementation independent definition, this proposal still assumes the occur-check, therefore resulting in an unsound analysis for implemented CLP languages. An experimental evaluation on a small benchmark suite (19 programs) was reported by Mulkers et al. in [19, 20]. Here the investigation mainly focused on the comparison between different instances of the underlying domain, showing the positive impact of freeness and linearity information on both the precision and performance of the classical set-sharing analysis. The experiments on the integration of structural information, by means of a depth-k abstraction (replacing all subterms occurring at a depth greater or equal to k with fresh abstract variables) for values of k between 0 and 3, showed that the domain they employed was not suitable to the analysis of real programs and, in fact, even the analysis of a modest-sized program like ‘ann’ could only be carried out with depth-0 abstraction (i.e., with no structural information at all).

In [8], an alternative technique is proposed for augmenting a data-flow analysis with structural information. Instead of upgrading the analysis domain, this technique relies on program transformations. In this approach, called untupling, the data-flow analysis of a given program would be performed in four distinct phases. This new analysis technique is advocated for its simplicity and efficiency. Comparing their limited experimental evaluation to the one conducted in [11], the authors of [8] claim that the untupling approach is inherently more efficient than abstract domain enhancement. Our new performance results suggest that this conclusion may need reconsidering. On the other hand, the proposal in [8] may be simpler to implement despite the four phases required, especially if one has to start from scratch. However, the Pattern(·) construction, besides being more precise and particularly efficient, is already implemented and has been thoroughly tested on a large number of benchmarks using the very expressive abstract domain Modes. Furthermore, as the implementation is in the form of a C^{++} template, only a very limited effort is required to upgrade any other abstract domain with structural information.

7 Conclusion

We have presented the rational construction of a generic domain for structural analysis of real CLP languages: Pattern(D^{♯}), where the parameter D^{♯} is an abstract domain satisfying certain properties. We build on the parameterized Pat(ℜ) domain of Cortesi et al. [10, 11], which is restricted to logic programs and requires the occur-check to be performed. However, while Pat(ℜ) is presented as a specific implementation of a generic structural domain, our formalization is implementation-independent. Reasoning at a higher level of abstraction we are able to appeal to familiar notions of unification theory, while leaving considerable more latitude for the implementer. Indeed our results show that, contrary to popular belief, an analyzer incorporating structural information analysis based on our approach can be highly competitive even from the efficiency point of view.

References

1. R. Bagnara. Data-Flow Analysis for Constraint Logic-Based Languages. PhD thesis, Dipartimento di Informatica, Università di Pisa, Italy, March 1997.

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, and E. Zaffanella. Efficient structural information analysis for real CLP languages. Quaderno 229, Dipartimento di Matematica, Università

    di Parma, 2000. Available at http://www.cs.unipr.it/~bagnara.

4. R. Bagnara, P. M. Hill, and E. Zaffanella. Set-sharing is redundant for pair-sharing. Theoretical Computer Science, 2000. To appear.

5. R. Bagnara and P. Schachte. Factorizing equivalent variable pairs in ROBDD-based implementations of Pos. In A. M. Haeberer, editor, Proc. of the “7th Int’l Conf. on Algebraic Methodology and Software Technology”, vol. 1548 of Lecture Notes in Computer Science, pages 471–485, Amazonia, Brazil, 1999. Springer-Verlag, Berlin.

6. R. Bagnara, E. Zaffanella, and P. M. Hill. Enhancing Sharing for precision. In M. C. Meo and M. Vilares Ferro, editors, Proc. of the “AGP’99 Joint Conf. on Declarative Programming”, pages 213–227, L’Aquila, Italy, 1999.

7. M. Bruynooghe, M. Codish, and A. Mulkers. Abstract unification for a composite domain deriving sharing and freeness properties of program variables. In F. S. de Boer and M. Gabbrielli, editors, Verification and Analysis of Logic Languages, Proc. of the W2 Post-Conference Workshop, Int’l Conf. on Logic Programming, pages 213–230, Santa Margherita Ligure, Italy, 1994.

8. M. Codish, K. Marriott, and C. Taboch. Improving program analyses by structure untupling. Journal of Logic Programming, 43(3):251–263, 2000.

9. A. Colmerauer. Prolog and infinite trees. In K. L. Clark and S. Å. Tärnlund, editors, Logic Programming, APIC Studies in Data Processing, vol. 16, pages 231– 251. Academic Press, New York, 1982.

10. A. Cortesi, B. Le Charlier, and P. Van Hentenryck. Conceptual and software support for abstract domain design: Generic structural domain and open product. Technical Report CS-93-13, Brown University, Providence, RI, 1993.

11. 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), 2000.

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

13. P. Cousot and R. Cousot. Comparing the Galois connection and widening/narrowing approaches to abstract interpretation. In M. Bruynooghe and M. Wirsing, editors, Proc. of the 4th Int’l Symp. on Programming Language Implementation and Logic Programming, vol. 631 of Lecture Notes in Computer Science, pages 269–295, Leuven, Belgium, 1992. Springer-Verlag, Berlin.

14. R. Giacobazzi, S. K. Debray, and G. Levi. Generalized semantics and abstract interpretation for constraint logic programs. Journal of Logic Programming, 25(3):191– 247, 1995.

15. P. M. Hill, R. Bagnara, and E. Zaffanella. The correctness of set-sharing. In G. Levi, editor, Static Analysis: Proc. of the 5th Int’l Symp., vol. 1503 of Lecture Notes in Computer Science, pages 99–114, Pisa, Italy, 1998. Springer-Verlag, Berlin.

16. J. Jaffar and M. Maher. Constraint logic programming: A survey. Journal of Logic Programming, 19&20:503–582, 1994.

17. J. Jaffar, S. Michaylov, P. Stuckey, and R. Yap. The CLP(R) language and system. ACM Transactions on Programming Languages and Systems, 14(3):339–395, 1992.

18. J.-L. Lassez, M. J. Maher, and K. Marriott. Unification revisited. In J. Minker, editor, Foundations of Deductive Databases and Logic Programming, pages 587– 625. Morgan Kaufmann, Los Altos, Ca., 1988.

19. A. Mulkers, W. Simoens, G. Janssens, and M. Bruynooghe. On the practicality of abstract equation systems. Report CW 198, Department of Computer Science, K. U. Leuven, Belgium, 1994.

20. A. Mulkers, W. Simoens, G. Janssens, and M. Bruynooghe. On the practicality of abstract equation systems. In L. Sterling, editor, Logic Programming: Proc. of the 12th Int’l Conf. on Logic Programming, MIT Press Series in Logic Programming, pages 781–795, Kanagawa, Japan, 1995. The MIT Press.

21. K. Musumbu. Interprétation Abstraite des Programmes Prolog. PhD thesis, Institut d’Informatique, Facultés Univ. Notre-Dame de la Paix, Namur, Belgium, 1990.

22. E. Zaffanella, R. Bagnara, and P. M. Hill. Widening Sharing. In G. Nadathur, editor, Principles and Practice of Declarative Programming, vol. 1702 of Lecture Notes in Computer Science, pages 414–431, Paris, 1999. Springer-Verlag, Berlin.