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 Computer Studies, University of Leeds, U. K.

                     hill@scs.leeds.ac.uk

Abstract. We present the rational construction of a generic domain for structural information analysis of real 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 occurs-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 (a.k.a. Herbrand domain) or the domain of rational trees [8] — 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 [2] 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. [9, 10], 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 [10] by allowing for the analysis of any CLP language [16]. Most importantly, we do not assume that the analyzed language performs the occurs-check in the unification procedure. This is an important contribution, since the vast majority of implemented CLP languages (in particular, almost all Prolog systems) do omit the occurs-check, either as a mere efficiency measure or because they are based upon a theory of extended rational trees [8]. 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 [10], 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 occurs-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. 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 [7]) 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 discusses recent 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}. We define the operation · \ ·: U^{⋆} × ℘_{f}(U) → U^{⋆} as follows. 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. Formally,

ε \ X =^{def} ε;
((x) :: s̄) \ X =^{def} \begin{cases}s̄ \ X, & if x ∈ X; \\ (x) :: (s̄ \ X), & if x ∉ X. \end{cases}

The projection mappings π_{i}: U^{n} → U are defined, for i = 1, …, n, by

π_{i}((e_{1}, …, e_{n})) =^{def} e_{i}.

We will also use the liftings π_{i}: ℘(U^{n}) → ℘(U) given by

π_{i}(S) =^{def} { π_{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 =^{def} (Z_{1}, Z_{2}, Z_{3}, … and z′ =^{def} (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} =^{def} { 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̄′ =^{def} \begin{cases}t̄[Z′_{1}/Z_{1}, …, Z′_{m}/Z_{m}], & if t̄∈ T_{z}^{n}; \\ t̄[Z_{1}/Z′_{1}, …, Z_{m}/Z′_{m}], & if t̄∈ T_{z′}^{n}. \end{cases}

Notice that t̄′′ =^{def} (t̄′)′ = t̄.

We will make use of a normalization function η: T_{Vars}^{∗} → T_{z}^{∗} such that, for each t̄∈ T_{Vars}^{∗}, the resulting tuple η(t̄) ∈ T_{z}^{∗} is a variant of t̄.

For each s̄ ∈ T_{Vars}^{∗} and each syntactic object o such that FV (o) ⊂ z, we write ϱs̄(o) (read “rename o away from s̄”) to denote o[Z_{n+i_{1}}/Z_{i_{1}}, …, Z_{n+i_{m}}/Z_{i_{m}}], where n = |vars(s̄)| and {Z_{i_{1}}, …, Z_{i_{m}}} = vars(o). This device will be useful for concatenating normalized term-tuples, still obtaining a normalized term-tuple. In fact, for each s̄_{1}, s̄_{2} ∈ T_{z}^{∗} we have s̄_{1} :: ϱs̄_{1}(s̄_{2}) ∈ T_{z}^{∗}.

When V̄ ∈ Vars^{m} is a finite sequence of distinct variables 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. The substitution [t̄/V̄] is said idempotent if vars(t̄) ∩ V̄ = ∅. 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.

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 distinct variables of interest (V_{1}, …, V_{k}). Each constraint store can be represented, at some level of abstraction, by a formula of the kind

∃_{Δ} . ({V_{1} = t_{1}, …, V_{k} = t_{k}} ∧ C),  (1)

such that

{V_{1} = t_{1}, …, V_{k} = t_{k}}, with t_{1}, …, t_{k} ∈ T_{Vars},  (2)

is a system of Herbrand equations in solved form, C ∈ C^{♭} is a constraint, and Δ =^{def} vars(C) ∪ vars(t_{1}) ∪ ⋯ ∪ vars(t_{k}) is such that Δ ∩ {V_{1}, …, V_{k}} = ∅. Roughly speaking, C limits the values that the quantified variables occurring in t_{1}, …, t_{k} 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_{1}, …, V_{k} have been fixed, the Herbrand part of the constraint store (1), the system of equations (2), 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, in addition to the cyclic bindings due to the omission of the occurscheck, 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^{♭} =^{def} ⋃_{n∈ℕ} ℘({ (s̄, C^{♭}) | s̄ ∈ T_{z}^{n}, C^{♭} ∈ C^{♭}, FV (C^{♭}) ⊆ vars(s̄) })

partially ordered by subset inclusion.

An abstract interpretation [11] 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^{♭}) =^{def} (s̄, { (ū, G^{♭}) | (t̄, G^{♭}) ∈ E^{♭}, s̄′[ū/vseq(s̄′)] = t̄}) ,

where s̄′ =^{def} ϕ(π_{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^{♭})) =^{def} { (s̄′[ū/vseq(s̄′)], G^{♭}) | (ū, G^{♭}) ∈ F^{♭} }.

So far, we have just chosen a different representation for D^{♭}, that is Φ_{ϕ}(D^{♭}).

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

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^{♭} =^{def} {⟨(s(0), c(Z_{1}, nil)), C_{1}⟩, ⟨(s(s(0)), c(Z_{1}, c(Z_{2}, nil))), C_{2}⟩},

where C_{1}, C_{2} ∈ C^{♭}, is mapped by the Φ_{lca} function onto

Φ_{lca}(E^{♭}) = ((s(Z_{1}), c(Z_{2}, Z_{3})),

{⟨(0, Z_{1}, nil), C_{1}⟩, ⟨(s(0), Z_{1}, c(Z_{2}, nil)), C_{2}⟩}).

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 [20, 22], 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 always 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.

It must be stressed that the abstract interpretation framework we are outlining — the concrete semantics in particular — while providing an adequate basis for most data-flow analyses, is “too abstract” when the properties of interest concern the internal workings of the Herbrand constraint solver. An example is structure-sharing analysis [23], whose aim is to determine those structure cells (elementary objects used to represent terms) that are possibly shared by more than one term representation. For example, the system

{V_{1} = f(a), V_{2} = f(a)}  (3)

does not say anything about structure sharing: we might have a shared f/1 cell, or two distinct ones. In the second case we might have a shared a/0 cell, or two distinct ones. Thus, there are a total of 3 cases that cannot be distinguished by looking at (3), the obvious consequence being that we cannot base structuresharing analysis on a concrete domain made up of representations of the form (1). We thus assume that we are dealing with properties that are insensible to the internal representation of terms.

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 [13], 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 [2, 3] 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 Δ.

Let s̄, t̄, ū ∈ T_{z}^{∗} be normalized term tuples and C^{♭}, G^{♭} ∈ C^{♭} such that FV (C^{♭}) ⊆ vars(t̄). We use the notation (ū, G^{♭}) = ϱs̄((t̄, C^{♭})) meaning that ū = ϱs̄(t̄) and that G^{♭} has been obtained from C^{♭} by applying the same renaming applied to t̄ in order to obtain ū. This device is needed in order to ensure renaming apart. Similarly, we will write (ū, G^{♭}) = η((t̄, C^{♭})) meaning that ū = η(t̄) and that G^{♭} has been obtained from C^{♭} by applying the same renaming applied to t̄ in order to obtain ū.

It is often helpful to think of C^{♭} as made up of first-order formulas [3]: in this view, ‘· ⊗ ·’ is logical conjunction, parameter passing amounts to conjunction of a formula with an equality formula, and ‘¶_{Δ}^{♭} ·’ corresponds to existential quantification on the variables in Vars \ Δ. While this is exactly how the “intended semantics” of CLP languages is captured, more concrete, non-standard semantics are often useful for the purpose of data-flow analysis. For instance, if the analysis must be sensible to the order in which constraints are posted to the solver, ‘· ⊗ ·’ cannot be interpreted as logical conjunction (it will not even be commutative, for that matter) [13].

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 [11]. 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.^{1} 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^{♯}) =^{def} {⊥_{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}^{♯}) =^{def} ∅ and

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

The binary relation ‘⪯_{p}’ ⊆ Pattern(D^{♯})×Pattern(D^{♯}) is given, for each d_{1}^{♯}, d_{2}^{♯} ∈ Pattern(D^{♯}), by

d_{1}^{♯} ⪯_{p} d_{2}^{♯} ⟺^{def} γ_{p}(d_{1}^{♯}) ⊆ γ_{p}(d_{2}^{♯}),

It is easily seen that Pattern(D^{♯}) is an abstract domain in the sense of Definition 2 provided D^{♯} is so. The ordering on the underlying domain is preserved by the Pattern(D^{♯}) domain.

Proposition 1. If (s̄, E_{1}^{♯}), (s̄, E_{2}^{♯}) ∈ Pattern(D^{♯}), then

γ(E_{1}^{♯}) ⊆ γ(E_{2}^{♯}) ⟹ γ_{p}((s̄, E_{1}^{♯})) ⊆ γ_{p}((s̄, E_{2}^{♯})).

1 At this stage of the presentation, ⊥^{♯} is not really required and could be dispensed with. However, it is simplest to postulate its existence and properties now.

Proof. Suppose that γ(E_{1}^{♯}) ⊆ γ(E_{2}^{♯}). Then, by Definition 3, we have

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

⊆ \{ η((t̄, C^{♭})) | \begin{matrix}(ū, C^{♭}) ∈ γ(E_{2}^{♯}) \\ 𝔗 ⊧ C^{♭} → t̄= s̄′[ū/vseq(s̄′)] \end{matrix} \}

= γ_{p}((s̄, E_{2}^{♯})).

⊓ ⊔

Up to now we have obtained from D^{♯} a new abstract domain Pattern(D^{♯}) that 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 [11]. 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^{♭}.^{2} For this purpose, we assume the existence of a computable function α_{p}: D^{♭} → Pattern(D^{♯}) such that, for each d^{♭} ∈ D^{♭}, we have d^{♭} ⊆ γ_{p}(α_{p}(d^{♭})).

While one option is to design from scratch an abstract semantics based on Pattern(D^{♯}), 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 soundness 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 [2]. 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,

2 Strictly speaking, one could require computability of the method to hold only for a strict subset of D^{♭} (e.g., depending on the kind of abstract iteration sequence employed, only the elements of D^{♭} describing initial and/or final states need to be effectively associated with an abstract counterpart).

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, for each (s̄_{1}, E_{1}^{♯}), (s̄_{2}, E_{2}^{♯}) ∈ Pattern(D^{♯}),

rmeet((s̄_{1}, E_{1}^{♯}), (s̄_{2}, E_{2}^{♯})) =^{def} (s̄_{1} :: ϱs̄_{1}(s̄_{2}), E_{1}^{♯} ▷ E_{2}^{♯}).

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

Theorem 1. For each (s̄_{1}, E_{1}^{♯}), (s̄_{2}, E_{2}^{♯}) ∈ Pattern(D^{♯}),

γ_{p}(rmeet((s̄_{1}, E_{1}^{♯}), (s̄_{2}, E_{2}^{♯})))

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

Proof. To simplify the notation, let q̄_{2} = ϱs̄_{1}(s̄_{2}). Then

γ_{p}(rmeet((s̄_{1}, E_{1}^{♯}), (s̄_{2}, E_{2}^{♯})))

= γ_{p}((s̄_{1} :: q̄_{2}, E_{1}^{♯} ▷ E_{2}^{♯}))

[by Definition 4]

= \{ η((t̄, C^{♭})) | \begin{matrix}(ū, C^{♭}) ∈ γ(E_{1}^{♯} ▷ E_{2}^{♯}) \\ 𝔗 ⊧ C^{♭} → t̄= (s̄′_{1} :: q̄′_{2})[ū/vseq(s̄′_{1} :: q̄′_{2})] \end{matrix} \} (4)

[by Definition 3]

Now, by the definition of ▷, we have (ū, C^{♭}) ∈ γ(E_{1}^{♯} ▷ E_{2}^{♯}) if and only if all the following hold:

(r̄_{1}, C_{1}^{♭}) ∈ γ(E_{1}^{♯}),  (r̄_{2}, C_{2}^{♭}) ∈ γ(E_{2}^{♯}),
(w̄_{2}, G_{2}^{♭}) = ϱr̄_{1}((r̄_{2}, C_{2}^{♭})),  C^{♭} = C_{1}^{♭} ⊗ G_{2}^{♭},
𝔗 ⊧ C^{♭} → ū = r̄_{1} :: w̄_{2}.

By the definition of Pattern(D^{♯}) |r̄_{1}| = |vars(s̄_{1})| and |w̄_{2}| = |vars(q̄_{2})| = |vars(s̄_{2})|. Hence, the expression (4) can be rewritten as

\{ η((t̄, 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}^{♭} → t̄= s̄′_{1}[r̄_{1}/vseq(s̄′_{1})]:: q̄′_{2}[w̄_{2}/vseq(q̄′_{2})] \end{matrix} \}.

(5)

Suppose that, for some t̄_{1} ∈ T_{vars(r̄_{1})}, ū_{2} ∈ T_{vars(w̄_{2})},

𝔗 ⊧ C_{1}^{♭} → t̄_{1} = s̄′_{1}[r̄_{1}/vseq(s̄′_{1})]
𝔗 ⊧ G_{2}^{♭} → ū_{2} = q̄′_{2}[w̄_{2}/vseq(q̄′_{2})].

We note that, by the definition of the renaming function ϱ,

q̄′_{2}[w̄_{2}/vseq(q̄′_{2})] = s̄′_{2}[w̄_{2}/vseq(s̄′_{2})]

so that

𝔗 ⊧ G_{2}^{♭} → ū_{2} = s̄′_{2}[w̄_{2}/vseq(s̄′_{2})].

It therefore follows from the definition of (w̄_{2}, G_{2}^{♭}) that as vars(ū_{2}) = vars(w̄_{2}) and vars(t̄_{1}) = vars(r̄_{1}), there exists t̄_{2} ∈ T_{vars(r̄_{2})} such that

(ū_{2}, G_{2}^{♭}) = ϱt̄_{1}((t̄_{2}, C_{2}^{♭}))

and

𝔗 ⊧ C_{2}^{♭} → t̄_{2} = s̄′_{2}[r̄_{2}/vseq(s̄′_{2})].

Then, by Definition 3, the expression (5) is equal to

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

⊓ ⊔

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 not a restriction, since this kind of normalization is either required by the language syntax itself (for instance, this is the case of the clp(Q, R) libraries of SICStus Prolog) or is performed automatically by the CLP system (see, e.g.,

[19] for a description of how normalization can be achieved).

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 [10]). 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 the current version of the China analyzer we adopted a representation of terms similar to the one used in the Warren’s Abstract Machine and its variants [1] and a unification procedure derived from [14]. In this case, all the easy steps typical of any unification procedure (functor name/arity checks, peeling, and so on) are handled, at the abstract level, exactly as they are at the concrete level.^{3} 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, proved below, assumes 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}}) =^{def} ((1, …, h − 1)

:: ((j_{1}, …, j_{l}) \ {1, …, h − 1})
:: ((h + 1, …, m) \ {j_{1}, …, j_{l}})).

3 Thus greatly reducing the proof obligations. For instance, termination of the abstract unification procedure will be a consequence of termination of the concrete one.

If E_{1}^{♯} =^{def} 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.

Suppose we take any sound unification algorithm and modify it as follows:

1. add a new parameter consisting of a description in D^{♯};

2. replace the step that performs the binding Z_{h} ↦ u, by one that performs the binding Z_{h} ↦ u[Z_{new}/Z_{h}] (where Z_{new} is a fresh variable that avoids the creation of cyclic terms in the pattern component), and updates the description E^{♯} to bind(E^{♯}, u, Z_{h});

3. add an η-normalization step so that the final result is still a description in Pattern(D^{♯}).

With the above definition for bind the only difficult part of the proof of correctness of the abstract (modified) unification algorithm with respect to the concrete (original) algorithm is a corollary of the following result.

Theorem 2. Let (s̄, E^{♯}) ∈ Pattern(D^{♯}), (p̄, C^{♭}) ∈ γ(E^{♯}), Z̄ = (Z_{1}, …, Z_{m}) = vseq(s̄), Z_{h} ∈ Z̄, u ∈ TZ̄, vseq(u) = (Z_{j_{1}}, …, Z_{j_{l}}), and

(k_{1}, …, k_{m_{1}}) = ((1, …, h − 1)

:: ((j_{1}, …, j_{l}) \ {1, …, h − 1})
:: ((h + 1, …, m) \ {j_{1}, …, j_{l}})).

We define

p̄ =^{def} (p_{1}, …, p_{m}),
q̄ =^{def} (p_{k_{1}}, …, p_{k_{m_{1}}} ).

Suppose that, for some idempotent substitution θ with variables in z and constraint C_{1}^{♭} ∈ C^{♭} such that FV (C_{1}^{♭}) ⊆ vars(q̄θ),

E_{1}^{♯} = bind(E^{♯}, Z_{h}, u)
𝔗 ⊧ θ ← (Z′_{h} = u′)[p̄/Z̄′]
𝔗 ⊧ C_{1}^{♭} ↔ ((Z′_{h} = u′)[p̄/Z̄′] ∧ C^{♭})θ
w = u[Z_{m+1}/Z_{h}]

Then (η(s̄[w/Z_{h}]), E_{1}^{♯}) ∈ Pattern(D^{♯}) and

η((s̄′[p̄θ/Z̄′], C_{1}^{♭})) ∈ γ_{p}((η(s̄[w/Z_{h}]), E_{1}^{♯})).

Proof. The following terminology is used in the proof. A substitution [W̄ /V̄] is called a renaming substitution in z for V̄ if W̄ is a sequence of distinct variables in z (though not necessarily disjoint from V̄).

Note that, since Z_{m+1} ∉ vars(s̄) ∪ vars(u), w is a variant of u, and, hence, s̄[w/Z_{h}] is a variant of s̄[u/Z_{h}] so that η(s̄[w/Z_{h}]) = η(s̄[u/Z_{h}]). Therefore, we just need to show that

(η(s̄[u/Z_{h}]), E_{1}^{♯}) ∈ Pattern(D^{♯})

and

η((s̄′[p̄θ/Z̄′], C_{1}^{♭})) ∈ γ_{p}((η(s̄[u/Z_{h}]), E_{1}^{♯})).

Note that m_{1} = m − 1 if Z_{h} ∉ vars(u), and m_{1} = m, otherwise. Note also that Z_{h}[p̄/Z̄] = p_{h}.

Let ν be a renaming substitution in z for s̄[u/Z_{h}] such that

s̄[u/Z_{h}]ν = η(s̄[u/Z_{h}]).  (6)

Then, using the definition of (k_{1}, …, k_{m_{1}}), we have

(Z_{1}, …, Z_{m_{1}}) = (Z_{k_{1}}, …, Z_{k_{m_{1}}} )ν.

However, by definition of (k_{1}, …, k_{m_{1}}),

(Z_{k_{1}}, …, Z_{k_{m_{1}}} ) = vseq(s̄[u/Z_{h}])  (7)

so that

(Z_{1}, …, Z_{m_{1}}) = vseq(η(s̄[u/Z_{h}])).  (8)

Thus, we have the first of the required results that

(η(s̄[u/Z_{h}]), E_{1}^{♯}) ∈ Pattern(D^{♯}).

Let μ be a renaming substitution in z for vars(p̄) ∪ vars(θ) such that

q̄θμ = η(q̄θ).  (9)

Then, by the hypothesis, Eq. 9, and Definition 5,

(q̄θμ, C_{1}^{♭}μ) = η((q̄θ, C_{1}^{♭})) ∈ γ(E_{1}^{♯}).  (10)

Also, as vseq(s̄′) = Z̄′ and, by the hypothesis, FV (C_{1}^{♭}) ⊆ vars(p̄θ), we have

η((s̄′[p̄θ/Z̄′]μ, C_{1}^{♭}μ)) = η((s̄′[p̄θ/Z̄′], C_{1}^{♭})).  (11)

Observe that, by the hypothesis,

𝔗 ⊧ C_{1}^{♭} → ((Z′_{h} = u′)[p̄/Z̄′])θ,
𝔗 ⊧ C_{1}^{♭} → (p_{h} = u′[p̄/Z̄′])θ,
𝔗 ⊧ C_{1}^{♭} → p_{h}θ = u′[p̄/Z̄′]θ,

so that, as Z̄′ ⊇ vars(u′),

𝔗 ⊧ C_{1}^{♭} → p_{h}θ = u′[p̄θ/Z̄′].  (12)

Now, since [p̄θ/Z̄′] is idempotent, we have

s̄′[u′[p̄θ/Z̄′]/Z′_{h}][p̄θ/Z̄′] = s̄′[u′/Z′_{h}][p̄θ/Z̄′]  (13)

and also, as Z′_{h} ↦ p_{h}θ is a binding in [p̄θ/Z̄′],

s̄′[p̄θ/Z̄′] = s̄′[p_{h}θ/Z′_{h}][p̄θ/Z̄′].  (14)

Hence,

𝔗 ⊧ C_{1}^{♭} → s̄′[p̄θ/Z̄′] = s̄′[p_{h}θ/Z′_{h}][p̄θ/Z̄′]

[by (14)]

𝔗 ⊧ C_{1}^{♭} → s̄′[p̄θ/Z̄′] = s̄′[u′[p̄θ/Z̄′]/Z′_{h}][p̄θ/Z̄′]

[by (12)]

𝔗 ⊧ C_{1}^{♭} → s̄′[p̄θ/Z̄′] = s̄′[u′/Z′_{h}][p̄θ/Z̄′]

[by (13)]

𝔗 ⊧ C_{1}^{♭}μ → s̄′[p̄θ/Z̄′]μ = (s̄[u/Z_{h}])′[p̄θ/Z̄′]μ  (15)

[by applying μ].

However,

(s̄[u/Z_{h}])′[p̄θ/Z̄′]μ = (s̄[u/Z_{h}])′[p̄θμ/Z̄′]

[as μ is a renaming for vars(p̄) ∪ vars(θ) ⊆ z]

= (s̄[u/Z_{h}])′[q̄θμ/(Z_{k_{1}}, …, Z_{k_{m_{1}}} )′]

[by the definition of q̄ and (7)]

= (s̄[u/Z_{h}]ν)′[q̄θμ/(Z_{1}, …, Z_{m_{1}})′].

[by definition of ν]

Therefore, by (15),

𝔗 ⊧ C_{1}^{♭}μ → s̄′[p̄θ/Z̄′]μ = (s̄[u/Z_{h}]ν)′[q̄θμ/(Z_{1}, …, Z_{m_{1}})′].  (16)

It therefore follows from (8), (10), and (16) that we can apply Definition 3 and hence obtain

η((s̄′[p̄θ/Z̄′]μ, C_{1}^{♭}μ)) ∈ γ_{p}((η(s̄[u/Z_{h}]ν), E_{1}^{♯})).

Therefore, by (11) and (6), we have the required result

η((s̄′[p̄θ/Z̄′], C_{1}^{♭})) ∈ γ_{p}((η(s̄[u/Z_{h}]), E_{1}^{♯})).
⊓ ⊔

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,

project_{k}^{♭}((ū, C^{♭})) =^{def} (prefix_{k}(ū), ¶_{Δ}^{♭} C^{♭}),

where Δ =^{def} vars(prefix_{k}(ū)).

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^{♯})) =^{def} (prefix_{k}(s̄), ¶_{j}^{♯} E^{♯}),

where j =^{def} |vars(prefix_{k}(s̄))|.

With these definitions ‘project_{k}^{♯}’ is correct with respect to ‘project_{k}^{♭}’. Theorem 3. For each (s̄, E^{♯}) ∈ Pattern(D^{♯}) such that s̄ ∈ T_{z}^{m} and each k ≤ m,

γ_{p}(project_{k}^{♯}((s̄, E^{♯}))) ⊇ { project_{k}^{♭}((p̄, C^{♭})) | (p̄, C^{♭}) ∈ γ_{p}((s̄, E^{♯})) }. Proof. In the following we let s̄_{k} =^{def} prefix_{k}(s̄), j =^{def} |vars(s̄_{k})|, r̄_{j} =^{def} prefix_{j}(r̄). Then

γ_{p}(project_{k}^{♯}((s̄, E^{♯})))

= γ_{p}((s̄_{k}, ¶_{j}^{♯} E^{♯}))

[by Definition 7]

= \{ η((q̄, G^{♭})) | \begin{matrix}(ū, G^{♭}) ∈ γ(¶_{j}^{♯} E^{♯}) \\ 𝔗 ⊧ G^{♭} → q̄ = s̄′_{k}[ū/vseq(s̄′_{k})] \end{matrix} \}

[by Definition 3]

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

[by Definition 7]

= \{ η((q̄, ¶_{vars(r̄_{j})}^{♭} C^{♭})) | \begin{matrix}(r̄, C^{♭}) ∈ γ(E^{♯}) \\ 𝔗 ⊧ ¶_{vars(r̄_{j})}^{♭} C^{♭} → q̄ = s̄′_{k}[r̄_{j}/vseq(s̄′_{k})] \end{matrix} \}

[by Definition 6]

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

[by Definition 2]

= { (prefix_{k}(p̄), ¶_{vars(r̄_{j})}^{♭} C^{♭}) | (p̄, C^{♭}) ∈ γ_{p}((s̄, E^{♯})) }

[by Definition 3]

= { project_{k}^{♭}((p̄, C^{♭})) | (p̄, C^{♭}) ∈ γ_{p}((s̄, E^{♯})) }

[by Definition 6].

⊓ ⊔

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̄)).  (17)

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.^{4} With this definition, the specification of ‘remap’ meets our original requirement given by (17). Theorem 4. Let (s̄, E♯ ; s̄) be a description with s̄ ∈ T_{z}^{k}. Let also r̄′ ∈ T_{z′}^{k} be an anti-instance of s̄. If E♯ ; r̄ = remap(s̄, E♯ ; s̄, r̄′) then γ_{p}((r̄, E♯ ; r̄)) ⊇ γ_{p}((s̄, E♯ ; s̄)). Proof. Assume |vars(r̄′)| = m and let ū ∈ T_{z}^{m} be the unique tuple such that

r̄′[ū/vseq(r̄′)] = s̄.  (18)

Then,

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

[by Definition 3]

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

[since, by Definition 8, we have γ(E♯ ; r̄) ⊇ γ_{p}((ū, E♯ ; s̄))]

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

[by Definition 3]

= \{ η((q̄, C^{♭})) | \begin{matrix}(t̄, C^{♭}) ∈ γ(E♯ ; s̄) \\ 𝔗 ⊧ C^{♭} → q̄ = s̄′[t̄/vseq(s̄′)] \end{matrix} \}

[by (18), since s̄ = r̄′[ū/vseq(r̄′)] and hence, vseq(ū) = vseq(s̄)]

= γ_{p}((s̄, E♯ ; s̄))

[by Definition 3].

⊓ ⊔

4 Indeed, one can define α′ =^{def} λ(s̄, E^{♯}) ∈ T_{z}^{k} × D^{♯} . remap(s̄, E^{♯}, (Z′_{1}, …, Z′_{k})).

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 ‘⊕’.

Definition 9. A partial function ⊕: D^{♯} ×D^{♯} ↣ D^{♯} is an upper bound operator over D^{♯} if and only if, for each E_{1}^{♯}, E_{2}^{♯} ∈ D^{♯} such that E_{1}^{♯} ⊕ E_{2}^{♯} is defined, we have E_{1}^{♯} ⪯ E_{1}^{♯} ⊕ E_{2}^{♯} and E_{2}^{♯} ⪯ E_{1}^{♯} ⊕ E_{2}^{♯}.

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 10. (‘join_{ϕ}’) Let ϕ be any common anti-instance function and ‘⊕’ an upper bound operator over D^{♯}. The operation (partial function)

join_{ϕ}: ℘_{f}(Pattern(D^{♯})) ↣ Pattern(D^{♯})

is defined as follows. For each k, I ∈ ℕ and each finite family

F =^{def} {(s̄_{i}, E_{i}^{♯}) | i ∈ I, s̄_{i} ∈ T_{z}^{k} }

of elements of Pattern(D^{♯}), if ⨁_{i∈I} remap(s̄_{i}, E_{i}^{♯}, r̄′) is defined, then

join_{ϕ}(F) =^{def} (r̄, E^{♯}),

where

r̄′ =^{def} ϕ({ s̄_{i} | i ∈ I }),
E^{♯} =^{def} ⨁_{i∈I} remap(s̄_{i}, E_{i}^{♯}, r̄′).

If ϕ is any common anti-instance function then ‘join_{ϕ}’ is an upper bound operator on the domain Pattern(D^{♯}).

Theorem 5. For each k ∈ ℕ, let F =^{def} {(s̄_{i}, E_{i}^{♯})}_{i∈I} be a finite family of elements of Pattern(D^{♯}) such that s̄_{i} ∈ T_{z}^{k}, for each i ∈ I. For each common anti-instance function ϕ and each j ∈ I we have γ_{p}(join_{ϕ}(F)) ⊇ γ_{p}((s̄_{j}, E_{j}^{♯})).

Proof. Let j ∈ I, r̄′ =^{def} ϕ({s̄_{i}}_{i∈I}) and E^{♯} =^{def} ⨁_{i∈I} remap(s̄_{i}, E_{i}^{♯}, r̄′). Then r̄′ is

an anti-instance of s̄_{j} and, by Definition 9, E_{j}^{♯} ⪯ E^{♯}. Thus

γ_{p}(join_{ϕ}(F)) ⊇ γ_{p}((r̄, E^{♯}))

[by Definition 10]

⊇ γ_{p}((r̄, remap(s̄_{j}, E_{j}^{♯}, r̄′)))

[by Proposition 1]

⊇ γ_{p}((s̄_{j}, E_{j}^{♯}))

[by Theorem 4]

⊓ ⊔

Widenings It is possible to devise a (completely unnatural) abstract domain D^{♯} that enjoys the ascending chain condition^{5} 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 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^{♯} [12]. 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}^{♯})) =^{def} \begin{cases}(s̄_{2}, E_{2}^{♯}), & if s̄_{1} ≠ s̄_{2}; \\ (s̄_{2}, E_{1}^{♯} ∇ E_{2}^{♯}), & if s̄_{1} = s̄_{2}. \end{cases}  (19)

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}^{♯})) =^{def} (s̄_{2}, remap(s̄_{1}, E_{1}^{♯}, s̄′_{2}) ∇ E_{2}^{♯}).  (20)

Widenings 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^{♯}).

Theorem 6. For i = 1, 2, suppose (s̄_{i}, E_{i}^{♯}) ∈ Pattern(D^{♯}) where s̄′_{2} is an antiinstance of s̄_{1} and γ_{p}((s̄_{1}, E_{1}^{♯})) ⊆ γ_{p}((s̄_{2}, E_{2}^{♯})) holds. Then

5 Namely, each strictly increasing chain is finite.

1. γ_{p}((s̄_{2}, E_{2}^{♯})) ⊆ γ_{p}(widen((s̄_{1}, E_{1}^{♯}), (s̄_{2}, E_{2}^{♯})));

2. γ_{p}((s̄_{2}, E_{2}^{♯})) ⊆ γ_{p}(Widen((s̄_{1}, E_{1}^{♯}), (s̄_{2}, E_{2}^{♯}))).

Proof. (1) Suppose (s̄, E^{♯}) = widen((s̄_{1}, E_{1}^{♯}), (s̄_{2}, E_{2}^{♯})). By the definition of widen, if s̄_{1} ≠ s̄_{2}, then (s̄, E^{♯}) = (s̄_{2}, E_{2}^{♯}) and there is nothing left to prove. If s̄_{1} = s̄_{2}, then (s̄, E^{♯}) = (s̄_{2}, E_{1}^{♯} ∇ E_{2}^{♯}). As ∇ is a widening on the D^{♯} domain, we have E_{2}^{♯} ⪯ E_{1}^{♯} ∇ E_{2}^{♯}. By γ monotonicity, this implies γ(E_{2}^{♯}) ⊆ γ(E_{1}^{♯} ∇ E_{2}^{♯}) and the result follows from Proposition 1.

(2) Suppose (s̄, E^{♯}) = Widen((s̄_{1}, E_{1}^{♯}), (s̄_{2}, E_{2}^{♯})), so that we have s̄ = s̄_{2} and

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

As ∇ is a widening on the D^{♯} domain, we have E_{2}^{♯} ⪯ E^{♯}. Again, the result follows from γ monotonicity and Proposition 1. ⊓ ⊔

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 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 11. (‘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}^{♯})) ⟺^{def} (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^{♯}.^{6} 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}’

The following is a trivial consequence of Definition 2 and Proposition 1.

6 It is also important not to confuse this approximate ordering with the approximation ordering of Pattern(D^{♯}), denoted by ‘⪯_{p}’, given in Definition 3.

Theorem 7. If compare((s̄_{1}, E_{1}^{♯}), (s̄_{2}, E_{2}^{♯})) holds, then

γ_{p}((s̄_{1}, E_{1}^{♯})) ⊆ γ_{p}((s̄_{2}, E_{2}^{♯})).

Moreover, compare is a preorder over Pattern(D^{♯}).

Proof. If compare((s̄_{1}, E_{1}^{♯}), (s̄_{2}, E_{2}^{♯})) holds, then, by Definition 11, s̄_{1} = s̄_{2} and E_{1}^{♯} ≾ E_{2}^{♯}. Hence, since ‘≾’ is a correct approximation of ‘⪯’, we have E_{1}^{♯} ⪯ E_{2}^{♯} and, by Proposition 1, γ_{p}((s̄_{1}, E_{1}^{♯})) ⊆ γ_{p}((s̄_{2}, E_{2}^{♯})). Furthermore, as ≾ is defined as a preorder, compare is a preorder. ⊓ ⊔

Observe that the ability of comparing descriptions only when they have the same pattern is not restrictive in our setting. The analyzer, in fact, will only need to compare the descriptions arising from the iteration sequence at two consecutive steps. By the definition of join_{ϕ} and the condition we imposed on widenings, if (s̄_{i}, E_{i}^{♯}) and (s̄_{i+1}, E_{i+1}^{♯}) are the descriptions at steps i and i + 1, then s̄′_{i+1} is an anti-instance of s̄_{i}. Moreover, since ‘join_{ϕ}’ and the widening operators are all upper-bound operators on Pattern(D^{♯}), we have

γ_{p}((s̄_{i}, E_{i}^{♯})) ⊆ γ_{p}((s̄_{i+1}, E_{i+1}^{♯})).  (21)

If also the reverse inclusion holds in (21) then we have reached a local fixpoint. The analyzer uses the approximate ordering to check for this possibility. Namely, it asks whether

compare((s̄_{i+1}, E_{i+1}^{♯}), (s̄_{i}, E_{i}^{♯}))

holds. The approximate test, of course, can fail even when equality does hold in (21). But this will be a fault of the pattern component only a finite number of times, since s̄′_{i+1} is an anti-instance of s̄_{i} and T_{z}^{n}, ordered by the anti-instance relation, has finite height. Thus, there exists ℓ ∈ ℕ such that, for each i ≥ ℓ, s̄_{i} = s̄_{ℓ}. After the ℓ-th step the accuracy of the approximate ordering is in the hands of D^{♯}.

5 Experimental Evaluation

We have conducted an extensive experimentation on the analysis using the Pattern(·) construction: this allowed to tune the implementation and to gain insight on the implications of keeping track of explicit structural information. In order to put ourselves in a realistic situation, we have assessed the impact of the Pattern(·) construction on a very precise and complex domain for mode analysis that we call Modes.^{7} The Modes domain captures information on simple types, groundness, boundedness, pair-sharing, freeness, and linearity. It is a combination of, among other things, two copies of the GER representation for Pos [5] —

7 This is an important point: if one starts from an imprecise domain it is rather easy to show big precision improvements.

one for groundness, the other for boundedness — and the non-redundant pairsharing domain PSD [4] with widenings as described in [24]. Some details on how these domain are combined can be found in [6]. All the domains used have been suitably extended in order to ensure correctness and precision also for the analysis of real systems omitting the occurs-check [2, 15].

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): 286 programs, 15 MB of code, 500.000 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 tracking explicit structural information with a domain ignoring it? That is something that should be established in advance. Let us consider a simple but not trivial Prolog program: mastermind.pl.^{8} 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:^{9}

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

Under the circumstances mentioned above, this means that: “the argument of extend code/1 will be bound to a term of the form [([A|B],C,D)|E], where

8 A program implementing the game “Mastermind”, rewritten by H. Koenig and T. Hoppe after code by M. H. van Emden. Also in H. Coelho and J. C. Cotta, “Prolog by Example”, Symbolic Computation, Springer-Verlag, Berlin, 1988. Avail-

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

9 Some extra groundness information obtained by the analysis has been omitted for the sake of simplicity: this says that, if A and B turn out to be ground, then E will also be ground.

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. The value of this extra precision can only be measured from the point of view of the target application of the analysis (e.g., optimized compilation, abstract debugging and verification, etc.). In other words, it is not clear at all how to define a fair measure for the precision gain independently from the intended application. 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. We are thus 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.

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. (19). Moreover, the merge operation employed is always ‘join_{lca}’. This is a deliberate choice: as we are currently tuning the implementations of the Pattern(·) construction and of the Modes domains (including its widenings), we feel that the inclusion of ad-hoc widenings for the pattern component should be postponed. One of the contributions of this paper is to show that explicit structural information analysis is feasible even without such widenings.

Here we only summarize the results of the experimentation. The interested reader can find all the relevant details at the URI http://www.cs.unipr.it/ China. The precision comparison is performed by measuring five different quantities:

indep: the total number of independent argument pairs; ground: the total number of ground argument positions; linear: the total number of linear argument positions; free: the total number of free argument positions; bound: the total number of bound (or nonvar) argument positions.

Note that our results can be considered as a lower bound on the overall precision improvement. First of all, as already noted, we are completely disregarding the precision gains coming from structural information in itself. Moreover, we are not reporting some relational information computed by the analyses, like groundness dependencies and sharing dependencies; often considered as a mere by-product of the analysis, sometimes this information can be suitably exploited to improve precision, e.g., when performing modular analyses.

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 212 201 219 215 204 197 237 235 219 211
0 < x ≤ 2 33 31 20 21 40 38 22 18 46 41
2 < x ≤ 5 20 25 15 16 18 18 9 10 10 16
5 < x ≤ 10 7 9 9 9 6 8 9 9 6 6
x ≥ 10 14 19 23 25 18 24 9 14 5 12

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

The results are summarized by partitioning the benchmark suite into six classes of programs, identified by the per cent 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 (in 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.

Structural information has the potential of pruning some computation paths on the grounds that they cannot be followed by the program being analyzed. In some cases the analysis is able to prove that a certain predicate can never succeed and/or never be called. This phenomenon actually happens for a dozen of programs in our benchmark suite: the analysis with Pattern(Modes) declares some procedures dead, but the same procedures are fine for the analysis with Modes. This means that systematic failure and/or the impossibility of calling these procedures is not due to undefined predicates or explicit failures caused by fail/0 and similar built-in predicates, but rather because of unification failures. At a closer examination, the problem seems to be caused by bugs in the involved benchmark programs.^{10} We have allowed for this in the results in Figure 1 by normalizing the precision results for the Pattern(Modes) domain. That is, we added to the results for Pattern(Modes) the number of variables or pair sharings, as appropriate, that were lost due to the pruning, before calculating the percentages. This amounts to the logically sound view whereby a procedure that always fails will have, in the impossible case of success, all its variables independent, ground, linear, free, and bound at the same time.

In order to evaluate the impact on efficiency of the Pattern transformation we computed the fixpoint computation time for all the programs, both with the Modes and with the Pattern(Modes) domains. The benchmark suite is thus

10 Indeed, China has proved very valuable as a debugging tool in several occasions, even if it has not yet been integrated into a suitable programming environment.

Time diff. in seconds programs
GI GD
degradation ≥ 1  10 20
degradation < 1  105 120
same time  98 75
improvement < 1  51 48
improvement ≥ 1  22 23

Table 2. A summary of the impact of structural information on analysis time.

partitioned into five classes based on the absolute differences observed^{11} and Table 2 gives the cardinality of the classes, again distinguishing between GI and GD analyses. The numbers show that the full range of possible behaviors is indeed observable. In particular, quite surprisingly, it is not uncommon the case when the Pattern construction, even being inherently more precise and complex, does allow significant time improvements. This is only partly due to the enhanced ability of pruning failed computation paths. Most importantly, the description of a set of tuples of terms in Pattern(Modes) is often much more efficient than the corresponding description in Modes.

In order to control the computational cost even in the few badly-behaving cases, which turn out to be much less than the well-behaving ones, it is necessary to provide the Pattern(·) construction with one or more specific widening operators, whose definitions do not depend on a corresponding widening on the underlying abstract domain. As noted in the previous section, simple solutions are readily available and currently under experimental evaluation.

6 Related Work

In [7], an alternative technique is proposed for augmenting a data-flow analysis with structural information. Instead of upgrading the analysis domain with structural information, this technique relies on program transformations. In this approach, the data-flow analysis of a given program is performed in four steps:

1. A pure structural information analysis is performed on the original program so as to collect an approximation of the common patterns in its success-set.

2. This common information is used to produce a specialized version of the original program where the common structures identified in the first phase are exposed. Roughly speaking, if all the success patterns for a predicate p/n in the original program are instances of a given structure, the specialized program is such that all of its syntactic calls to p/n are instances of that

11 As the benchmark suite comprises several real programs of very respectable size, we believe absolute time is what matters to assess the feasibility of the approach. 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.14. Note, once again, that no widening was employed on the Pattern(·) construction.

structure. If the original program is a pure logic program, then the specialization phase presented in [7] preserves its success-patterns but not necessarily its call-patterns and termination behavior.^{12}

3. The specialized program is then further transformed by untupling. The untupling transformation produces a new program where the sub-structures of common structures are represented by different argument positions. For example, if the specialized program computed in step 2 is such that all the calls to p/1 are instances of p(f(X, Y, h(Z))), the untupling transformation will introduce a new predicate p'/3, so that an instance p(f(t_{1}, t_{2}, h(t_{3}))) in the specialized program becomes p′(t_{1}, t_{2}, t_{3}) in the untupled program. The untupling transformation also adds a new clause for each predicate in the specialized program in order to maintain the connection between the specialized program itself and its untupled version. Following our example, the untupled version of the program contains the clause

                 p(f(X, Y, h(Z))) :- p prime(X, Y, Z).

In [7] the untupling transformation is reported to preserve both successpatterns (of the predicates in the specialized program) and termination behavior.

4. Analysis is finally performed on the untupled program with the abstract domain of choice.

This new analysis technique is, as pointed out in [7], less precise, in general, than the one of Pat(ℜ) or Pattern(·). This happens because the transformational approach may miss pruning information and thus lead to the analysis of computation branches that cannot lead to success (this phenomenon also has an impact on the cost of the analysis). The technique is advocated in [7] for its simplicity and efficiency.

As far as efficiency is concerned, [7] assumes that structural information analysis with Pat(ℜ) (and, by extension, with Pattern(D^{♯})) is inherently inefficient. This claim is supported by the comparison of their performance evaluation to the one reported in [9] for the domain Pat(Pos). However, the pioneering work described in [9] refers to implementations of Pos and of the generic structural domain that are no longer representative of the current state-of-the-art. Indeed, the experimental results we obtain for the Pattern(·) construction show that in most cases the slow-down is very limited and that even consistent speed-ups (up to a factor 5) can be achieved on the analysis of real programs. Moreover, in [7] the comparison with Pat(Pos) is only conducted on the 11 (mainly small) programs evaluated in [9]. Our experience tells us that such a small benchmark suite is far too small to warrant any generalization of the results. It also seems that, for the comparison, in [7] only the cost of the analysis of the untupled program is computed. The computational costs of the other phases of the proposed

12 This property does not carry through to, say, Prolog programs, as it can be easily established by considering a program constituted by only two clauses: p(X) :- q(X)

  and q(X) :- var(X), X = a.

method (pattern analysis, specialization and untupling) are disregarded, even though specialization and untupling are said to have linear complexity in the size of the program.

As far as simplicity is concerned, one advantage of the approach described in [7] is that one can reuse existing data-flow analyzers without having to develop a generic structural domain. Therefore, despite the need to implement the transformers used to obtain the specialized and the untupled versions of the original program, this new proposal may be simpler to implement. However, an implementer willing to apply the Pat(ℜ) or the Pattern(·) constructions to a different abstract domain does not need to start from scratch. Since both these constructions are generic, they can be (and have been) implemented only once and for all. To be more precise, the Pattern(·) construction is implemented as a C^{++} template. If one has a class Base Domain implementing the domain D^{♯}, an implementation of the Pattern(D^{♯}) domain is provided by the class Pattern<Base Domain>.^{13} So, while it is true that a good deal of work was invested in designing, implementing, testing and tuning the Pattern(·) construction, this work needs not to be repeated and its use as a template is one of the most simple things one can imagine.

To complete the comparison, we observe that the transformational approach may lack the wide applicability of the Pattern(·) construction. For instance, it is not clear from the definitions given in [7] if their technique can be extended so as to correctly deal with any implemented (constraint) logic programming system (which may omit the occurs-check and provide built-ins such as var/1). This ability is, in turn, one of the strongest points of our proposal.

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. [9, 10], which is restricted to logic programs and requires the occurs-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.

13 The Pattern template has additional arguments, each with its own default value, that allow the user to select the parameters of the construction such as the widening functions.

References

1. H. Aït-Kaci. Warren’s Abstract Machine. A Tutorial Reconstruction. The MIT Press, 1991.

2. R. Bagnara. Data-Flow Analysis for Constraint Logic-Based Languages. PhD thesis, Dipartimento di Informatica, Università di Pisa, Corso Italia 40, I-56125 Pisa, Italy, March 1997. Printed as Report TD-1/97.

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

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 ROBDDbased implementations of Pos. In A. M. Haeberer, editor, Proceedings of the “Seventh International Conference on Algebraic Methodology and Software Technology (AMAST’98)”, volume 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. Enhanced sharing analysis techniques: A comprehensive evaluation. In M. Gabbrielli and F. Pfenning, editors, Proceedings of the ACM SIGPLAN 2nd International Conference on Principles and Practice of Declarative Programming, Lecture Notes in Computer Science, Montreal, Canada, 2000. Springer-Verlag, Berlin. To appear.

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

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

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

10. 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, 2000. To appear.

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

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

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

14. S. Haridi and D. Sahlin. Efficient implementation of unification of cyclic structures. In J. A. Campbell, editor, Implementations of Prolog, pages 234–249. Ellis Horwood/Halsted Press/Wiley, 1984.

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

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. P. Lim and J. Schimpf. A conservative approach to meta-programming in constraint logic programming. In M. Bruynooghe and J. Penjam, editors, Proceedings of the 5th International Symposium on Programming Language Implementation and Logic Programming, volume 714 of Lecture Notes in Computer Science, pages 44–59, Tallinn, Estonia, 1993. Springer-Verlag, Berlin. Also available as Technical Report ECRC-94-31, ECRC 1994.

20. K. Marriott and H. Søndergaard. On describing success patterns of logic programs. Technical Report 12, The University of Melbourne, 1988.

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

22. T. Sato and H. Tamaki. Enumeration of success patterns in logic programs. Theoretical Computer Science, 34:227–240, 1984.

23. G. Weyer and W. Winsborough. Annotated structure shape graphs for abstract analysis of Prolog. In H. Kuchen and S. D. Swierstra, editors, Programming Languages: Implementations, Logics and Programs, Proceedings of the Eighth International Symposium, volume 1140 of Lecture Notes in Computer Science, pages 92–106, Aachen, Germany, 1996. Springer-Verlag, Berlin.

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