Structural Information Analysis for CLP Languages

Roberto Bagnara^{∗} School of Computer Studies University of Leeds Leeds, LS2 9JT, United Kingdom

                   bagnara@scs.leeds.ac.uk

Abstract

We present the rational construction of a generic domain for structural analysis of CLP languages: Pattern(D^{♯}), where the parameter D^{♯} is an abstract domain satisfying certain properties. Our domain builds on the parameterized domain for the analysis of Prolog programs Pat(ℜ), which is due to Cortesi et al. [6, 7]. However, the formalization of our CLP abstract domain is independent from specific implementation techniques: Pat(ℜ) (suitably extended) is one of the possible implementations. 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, missing in [6]) that gives some control over the precision and computational cost of the resulting generic structural domain.

1 Introduction

It is important to make a clear distinction between the language CLP(H, X), where the Herbrand component H is completely separated from the domain X, and the language CLP(H_{X}), where H and X are somewhat amalgamated. Of course, CLP(H, X) languages are simpler, though still useful. The simplicity come from the fact that interpreted terms are not allowed to occur as leaves of Herbrand terms. When interpreted terms are allowed to occur in Herbrand structures more complex programs can be built. For instance, one can express unbounded lists where interpreted terms occur. Independently of the need for “unbounded containers”, it is a common CLP idiom to embed interpreted terms into Herbrand terms.

From the experience gained with the first prototype version of China [2] it was clear that, in order to attain a significant precision in the analysis of numerical constraints in CLP(H_{N}) languages, one must keep at least part of the uninterpreted terms in concrete form. Note that almost any analysis is much more precise when this kind of structural information is retained to some extent: in our case the precision loss was just particularly acute.

Cortesi et al. [6, 7] have a nice proposal in this respect. 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. Their approach is limited to the analysis of logic programs. Most importantly, the presentation in [6] has several drawbacks. First of all, the authors define a specific implementation of the generic structural domain. The implementation is forcedly cluttered with details that make the general principles difficult to understand. Moreover, they describe an implementation of the pattern component (taking care of representing the terms in concrete form) that appears to be unnecessarily complicated. Their representation of terms and subterms, while responsible for some of the intricacies in the description, does not seem to have any advantage, from the implementation point of view, with respect to more standard representations of terms (such as those employed in the Warren’s Abstract Machine and its variants [1]). As a consequence, standard notions from unification theory, such as instance, anti-instance, and (least) common anti-instance [10], are never mentioned in [6], while being implicitly present.

∗This work has been partly supported by EPSRC under grant GR/L19515.

In this paper we present the rational construction of a generic domain for structural analysis of CLP(H_{X}) languages: Pattern(D_{H_{X}}^{♯}), where the parameter D_{H_{X}}^{♯} is an abstract domain satisfying certain properties. The formalization of the structural domain is independent from specific implementation techniques: Pat(ℜ) (suitably extended) is a possible implementation of the domain. 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, missing in [6]) that gives some control over the precision and computational cost of the resulting generic structural domain.

It must be stressed that the merit of Pat(ℜ) is to define a generic implementation that works on any domain ℜ providing a certain set of elementary, low-level operations. It is particularly easy to extend an existing domain in order to support the simple operations required. 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. This is not a limitation, if one considers that in the actual implementation even more complex operations are used. For instance, all the abstract bindings arising from a bunch of unifications are executed in one shot, instead of one-at-a-time [3].

2 Preliminaries

Let S be a set. We will denote by S^{n} the set of n-tuples of elements drawn from S, whereas S^{∗} denotes ⋃_{n∈ℕ} S^{n}. Let Vars be a denumerable set of variable symbols. We will denote by T_{Vars} the set of terms with variables in Vars. 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}, . . .. For any syntactic object o (a term or a tuple of terms) we will denote by vseq(o) the sequence of first occurrences of variables which are found on a depth-first, left-to-right traversal^{1} of o. For instance, vseq((f(g(X), Y), h(X))) = (X, Y).

In order to avoid the burden of talking “modulo renaming” we will make 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̄)|}) }.

1Any other fixed ordering would be as good for our purposes.

All the tuples in z-form are contained in 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{matrix}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{matrix}  (1)

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

Another renaming we will use is the following: for each s̄ ∈ T_{Vars}^{⋆} and each other syntactic object o such that FV (o) ⊂ z, we write ϱs̄(o) 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} and t̄ ∈ T_{Vars}^{m} we use [t̄/V̄] as a shorthand for the substitution [π_{1}(t̄)/π_{1}(V̄), …, π_{m}(t̄)/π_{m}(V̄)]. 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(ū).

3 Factoring Out Structural Information

A quite general picture for the analysis of a CLP(H_{X}) language is as follows. We want to describe a (possibly infinite) set of constraint stores over a tuple of variables of interest V_{1}, …, V_{k}. These variables represent the arguments of some program predicate. 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),  (2)

such that

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

is a system of Herbrand equations in solved form, C ∈ D_{X}^{♭} is a constraint on the domain X, and Δ =^{def} vars(C) ∪ vars(t_{1}) ∪ ⋯ ∪ vars(t_{k}) is such that Δ ∩ {V_{1}, …, V_{k}} = ∅. Roughly speaking, the purpose of C is to limit the values that the (quantified) variables occurring in t_{1}, …, t_{k} can take.

Once variables V_{1}, …, V_{k} have been fixed, the Herbrand part of the constraint store (2), the system of equations (3), can be represented as a k-tuple of terms. Since we want to characterize any set of constraint stores, our concrete domain is

D_{H_{X}}^{♭} =^{def} ⋃_{n∈ℕ}℘(T_{z}^{n} × D_{X}^{♭} ).  (4)

[figure: ℘(T_{z}^{⋆} × D_{X}^{♭} ); α; Φ_{ϕ}; D_{H_{X}}^{♯}; T_{z}^{⋆} × ℘(T_{z}^{⋆} × D_{X}^{♭} ); (id,α); Φ_{ϕ}^{−1}; T_{z}^{⋆} × D_{H_{X}}^{♯}; α′]

Figure 1: Upgrading a domain with structural information.

An abstract interpretation of D_{H_{X}}^{♭} can be specified by choosing an abstract domain D_{H_{X}}^{♯} and a suitable abstraction function

α: D_{H_{X}}^{♭} → D_{H_{X}}^{♯} .  (5)

If D_{H_{X}}^{♯} is able to encode enough structural (Herbrand) information from D_{H_{X}}^{♭} so as to achieve the desired precision, fine. If this is not the case, it is possible to improve the situation by keeping some structural information explicit.

One way of doing that is to perform a change of representation for D_{H_{X}}^{♭}, which is the basis for further abstractions. 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.) A function

ϕ: ⋃_{n∈ℕ}℘(T_{z}^{n}) → T_{z′}^{⋆}

is called a common anti-instance function if, for each n ∈ ℕ and each T̂ ∈ ℘(T_{z}^{n}):

1. ϕ(T̂) ∈ T_{z′}^{n};

2. 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, in z′-form, of each t̄∈ T̂.

Any choice of ϕ induces a function

Φ_{ϕ}: D_{H_{X}}^{♭} → T_{z}^{⋆} × ℘(T_{z}^{⋆} × D_{X}^{♭} ),  (6)

which is given, for each Ê^{♭} ∈ D_{H_{X}}^{♭} by

Φ_{ϕ}(Ê^{♭}) =^{def} (s̄′, { (ū, D^{♭}) | (t̄, D^{♭}) ∈ Ê^{♭}, s̄[ū/vseq(s̄)] = t̄}) ,  (7)

where s̄ =^{def} ϕ(π_{1}(Ê^{♭})). The corestriction to the image of Φ_{ϕ}, that is Φ_{ϕ}: D_{H_{X}}^{♭} → Φ_{ϕ}(D_{H_{X}}^{♭} ), is an isomorphism. So far, we have just chosen a different representation for D_{H_{X}}^{♭}, that is Φ_{ϕ}(D_{H_{X}}^{♭} ). 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 5.4, such a function is implicitly required in order to define an important operation over the new abstract domain T_{z}^{⋆} × D_{H_{X}}^{♯}.^{2}

This approach has several advantages. First of all, factoring out common structural information improves the analysis precision, since part of the approximated k-tuples of terms is recorded, in concrete form, into the first component of T_{z}^{⋆} × D_{H_{X}}^{♯}. 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

Ŝ =^{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} ∈ D_{X}^{♭}, is mapped by the Φ_{lca} function onto

Φ_{lca}(Ŝ) = ((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 side of the spectrum is the possibility of choosing ϕ so that it returns a k-tuple of distinct, new variables for each set of k-tuples of terms. This correspond to a framework where structural information is just discarded. With this choice, Ŝ would be mapped onto ((Z_{1}, Z_{2}), Ŝ). In-between these two extremes there are a number of possibilities that help managing the complexity/precision tradeoff. The k-tuples returned by ϕ can be limited in depth [13, 11], for instance. More useful is to limit them in width, that is, limiting the number of symbols’ occurrences. This flexibility allows to design the analysis’ domains without caring about structural information: the problem is always to approximate elements of ℘(T_{z}^{a} × D_{X}^{♭} ). Whether a is fixed by the arity of a predicate or a is the number of variables occurring in some pattern does not really matter.

4 Parametric Structural Analysis

In order to specify the abstract domain for the analysis, we need some assumptions on the concrete X domain D_{X}^{♭}, which represents the X -part of consistent constraint stores. One can think about D_{X}^{♭} as made up of first-order sentences [5]. In this view, the operator ⊗: D_{X}^{♭} × D_{X}^{♭} → D_{X}^{♭} corresponds to logical conjunction. Moreover, we assume that it makes sense to talk about the free variables of D^{♭} ∈ D_{X}^{♭}, denoted by FV (D^{♭}). Let s̄, t̄, ū ∈ T_{z}^{⋆} and D^{♭}, E^{♭} ∈ D_{X}^{♭} such that FV (D^{♭}) ⊆ vars(t̄). When we write (ū, E^{♭}) = ϱs̄((t̄, D^{♭})), we mean that ū = ϱs̄(t̄) and that E^{♭} has been obtained from D^{♭} by applying the same renaming applied to t̄ in order to obtain ū.

Another natural thing to do is projecting a satisfiable store: thus ∃V̄ D^{♭}, where V̄ is a tuple (or set) of variables, is assumed to be as defined.

The last thing we need is the ability of adding an equality constraint to a constraint store. Thus D^{♭}[t_{1} = t_{2}] is the store obtained from D^{♭} by injecting the equation t_{1} = t_{2}, provided that the resulting store is consistent, otherwise the operation is undefined. Notice that we assume D_{X}^{♭} and its operations encode both the proper X -solver and the so called interface between the Herbrand engine and the X -solver [8]. In particular, the interface is responsible for type-checking of the equations it receives. For example in CLP(R) [9] 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.

2Notice that α′ may or may not make the diagram of Figure 1 commute (although often α′ turns out to have this property).

We now turn our attention to the abstract domain which is the parameter of the generic structural domain. We will denote it simply by D^{♯}, instead of D_{H_{X}}^{♯}. Thus, assuming that X has been fixed, D_{X}^{♭} is indicated just by D^{♭}.

Since the aim here is maximum generality, we refer to a very weak abstract interpretation framework. Definition 2 (Abstract domain.) An abstract domain for H_{X} is a set D^{♯} equipped with a preorder relation ⊑, an order preserving function γ: D^{♯} → D^{♭}, an upper-bound operator ⊕: D^{♯} × D^{♯} → D^{♯}, and a least element ⊥^{♯} such that γ(⊥^{♯}) = ∅. Thus, for each D_{1}^{♯}, D_{2}^{♯} ∈ D^{♯}, we have both that D_{1}^{♯} ⊑ D_{2}^{♯} implies γ(D_{1}^{♯}) ⊆ γ(D_{2}^{♯}) and γ(D_{1}^{♯} ⊕ D_{2}^{♯}) ⊇ γ(D_{1}^{♯}) ∪ γ(D_{2}^{♯}).

The structural information construction upgrades any given abstract domain D^{♯} as follows. Definition 3 (The Pattern(·) construction.) Let D^{♯} be an abstract domain. Then

Pattern(D^{♯}) =^{def} { (s̄, D^{♯}) ∈ T_{z}^{⋆} × D^{♯} | γ(D^{♯}) ⊆ T_{z}^{|vars(s̄)|} × D^{♭} }.

The meaning of each element (s̄, D) ∈ Pattern(D^{♯}) is given by the concretization function γ: Pattern(D^{♯}) → ℘(T_{z}^{⋆} × D^{♭}):

γ((s̄, D^{♯})) =^{def} { (s̄′[ū/ vseq(s̄′)], D^{♭}) | (ū, D^{♭}) ∈ γ(D^{♯}) }.

5 Operations for the Analysis

In this section we define the operations over Pattern(D^{♯}) that are needed for the analysis in a bottom-up framework. In order of appearance into the analysis process:

• we need an operation that takes two descriptions and, roughly speaking, juxtaposes them. This operation, which we call meet with renaming apart, is needed when “solving” a clause body with respect to the current interpretation.

• Unification, that realizes “parameter passing”. The descriptions that were simply juxtaposed are thus made to communicate with each other.

• 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 operation of remapping is used to adapt a description to a different, less precise, pattern component. It is used in order to realize various join and widening operations.

• The join operation is parameterized with respect to a common anti-instance function. It is used to merge descriptions arising from the different sets of computation paths explored during the analysis.

• The comparison operation is employed by the analyzer in order to check whether a local (to a program clause or predicate) fixpoint has been reached.

The above operations over Pattern(D^{♯}) induce the need for other operations on the underlying domain D^{♯}. The latter are specified in the next sections so that the correctness of the analysis can be ensured.

5.1 Meet with Renaming Apart

This operation is very simple.

Definition 4 (The rmeet operation.) Let ▷: D^{♯} × D^{♯} → D^{♯} be such that, for each D_{1}^{♯}, D_{2}^{♯} ∈ D^{♯},

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

Then, for each (s̄_{1}, D_{1}^{♯}), (s̄_{2}, D_{2}^{♯}) ∈ Pattern(D^{♯}).

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

The following result is a direct consequence of the definition: there is no precision loss in rmeet.

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

γ(rmeet((s̄_{1}, D_{1}^{♯}), (s̄_{2}, D_{2}^{♯}))) = \{ (t̄_{1} :: ū_{2}, D_{1}^{♭} ⊗ E_{2}^{♭}) | \begin{matrix}(t̄_{1}, D_{1}^{♭}) ∈ γ((s̄_{1}, D_{1}^{♯})) \\ (t̄_{2}, D_{2}^{♭}) ∈ γ((s̄_{2}, D_{2}^{♯})) \\ (ū_{2}, E_{2}^{♭}) = ϱt̄_{1}((t̄_{2}, D_{2}^{♭})) \end{matrix} \}.

5.2 Unification with Occur-Check

In this section we assume that the execution mechanism of the language being analyzed performs unifications without omitting the occur-check. With this hypothesis (which, unfortunately, is seldom verified) we can easily complete the unification algorithm given in [6]. When the occur-check fails in the abstract unification we know that the computation path being analyzed can be safely pruned, because the concrete unification would have failed at this point. Notice that, for the purpose of the present discussion, the occur-check need not be implemented explicitly, that is by making the unification fail in the logic programming sense. Since our data-flow analyses provide information of the kind

if control gets to this point, then that will hold there,

a more drastic handling of the occur-check is acceptable. If we are guaranteed that the concrete system enters either an error state or an infinite loop whenever a cyclic binding is attempted, then the abstract unification procedure presented in this section can safely be used. See [4] for a discussion about what can be done for those systems where the occur-check is, by any means, omitted.

We start with a description (s̄, D^{♯}) ∈ Pattern(D^{♯}) and two terms to be unified, t and u, such that vars((t, u)) ⊆ vars(s̄). We then apply the procedure unify, given as Algorithm 1, to s̄, D^{♯}, t and u. In the macro-operation bind(s̄, D^{♯}, u, Z_{h}), s̄ is passed only in order to maintain the connection between the variables in (u, Z_{h}) and the description D^{♯}. We assume, without loss of generality, that whenever bind(s̄, D^{♯}, u, Z_{h}) is invoked we have |vars(s̄)| = m, with m ≥ 0. The result of the operation will be a description D_{1}^{♯} such that γ(D_{1}^{♯}) ⊆ T_{z}^{m−1} × D^{♭}. This is because, after the binding, Z_{h} will not be referenced anymore. What remains to be described is the operation of reflecting the binding of Z_{h} to u into D^{♯} so to obtain D_{1}^{♯}. We will denote this operation by D^{♯}[u/Z_{h}], and present its variants (depending on whether u is a constant or a number or a variable or a compound term) in the next sections.

procedure unify(s̄, D^{♯}, t, u) 1: if t ≠ u then 2: if t = f(t_{1}, …, t_{n}) and u = f(u_{1}, …, u_{n}) then 3: for all i = 1, …, n do 4: unify(s̄, D^{♯}, t_{i}, u_{i}) 5: else if t = Z_{h} then 6: if Z_{h} does not occur in u then 7: D^{♯} := bind(s̄, D^{♯}, u, Z_{h}) {invokes underlying domain} 8: Z_{h} := u {instantiates all the occurrences of Z_{h}} 9: s̄:= η(s̄) {normalization} 10: else 11: D^{♯} := ⊥^{♯} 12: else if u = Z_{k} then 13: unify(s̄, D^{♯}, u, t) 14: else 15: D^{♯} := ⊥^{♯}

Algorithm 1: Unification for the parametric structural domain.

5.2.1 Binding to a Constant or a Number

The result of D^{♯}[k/Z_{h}], where k is a symbolic constant or a number and h ∈ {1, …, m} is any D_{1}^{♯} ∈ D^{♯} such that

γ(D_{1}^{♯}) ⊇ { ((t_{1}, …, t_{h−1}, t_{h+1}, …, t_{m}), D^{♭}[t_{h} = k]) | ((t_{1}, …, t_{m}), D^{♭}) ∈ γ(D^{♯}) }.

Notice that vseq(s̄[k/Z_{h}]) = (Z_{1}, …, Z_{h−1}, Z_{h+1}, …, Z_{m}). Similar comments apply also to what follows.

5.2.2 Binding to an Alias

Here we must specify an admissible result, D_{1}^{♯}, for the operation D^{♯}[Z_{i}/Z_{h}] with i, h ∈ {1, …, m} and i ≠ h. In order to reduce the complexity of the definition we need some special notation for sequences. Let U be a set. Then ℘_{f}(U) denotes the set of all the finite subsets of U. We define the operation · \ ·: U^{⋆} × ℘_{f}(U) → U^{⋆} as follows. For each sequence L ∈ U^{⋆} and each set S ∈ ℘_{f}(U), the sequence L\U is obtained by removing from L all the elements that appear in U. Let us define τ(k): {1, …, m − 1} → {1, …, m} as

τ(k) =^{def} π_{k}((1, …, h − 1) :: ((i) \ {1, …, h − 1}):: ((h + 1, …, m) \ {i})).

The transformation τ is such that, for each k = 1, …, m − 1,

π_{k}(vseq(s̄[Z_{i}/Z_{h}])) = Z_{τ(k)}.

Now, D_{1}^{♯} must satisfy

γ(D_{1}^{♯}) ⊇ { ((π_{τ(1)}(t̄), …, π_{τ(m−1)}(t̄)), D^{♭}[π_{h}(t̄) = π_{i}(t̄)]) | (t̄, D^{♭}) ∈ γ(D^{♯}) }.

5.2.3 Binding to a Compound

Specifying the result of the operation D[u/Z_{h}] is only slightly more complicated. Suppose that vseq(u) = (Z_{j_{1}}, …, Z_{j_{l}}), so that Z_{h} ∉ {Z_{j_{1}}, …, Z_{j_{l}}} and the transformation τ is given by

τ(k) =^{def} π_{k}((1, …, h − 1) :: ((j_{1}, …, j_{l}) \ {1, …, h − 1})

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

Then D^{♯}[u/Z_{h}] is allowed to return any D_{1}^{♯} such that

γ(D_{1}^{♯}) ⊇ \{ ((π_{τ(k)}(t̄))_{k=1}^{m−1}, D_{1}^{♭}) | \begin{matrix}(t̄, D^{♭}) ∈ γ(D^{♯}) \\ θ = [u_{j_{1}}/Z_{j_{1}}, …, u_{j_{l}}/Z_{j_{l}}] \\ π_{h}(t̄) = uθ \\ D_{1}^{♭} = D^{♭}[π_{j_{1}}(t̄) = u_{j_{1}}, \\ …, π_{j_{l}}(t̄) = u_{j_{l}}] \end{matrix} \}.

As observed in [6], the proof of the overall correctness of Algorithm 1 can be obtained by systematic generalization of the proof given in Musumbu’s PhD thesis [12].

5.3 Projection

This operation consists simply in dropping a suffix of the pattern component, with the consequent projection on the underlying domain.

Definition 6 (The project operation.) Let ∃∃_{m}: D^{♯} → D^{♯} be a family of operations such that, for each D^{♯} ∈ D^{♯} with γ(D^{♯}) ⊆ T_{z}^{m} × D^{♭} and each j < m,

γ(¯∃ ; ¯∃_{j} D^{♯}) ⊇ \{ (r̄, E^{♭}) | \begin{matrix}(ū, D^{♭}) ∈ γ(D^{♯}) \\ r̄ = (π_{1}(ū), …, π_{j}(ū)) \\ Δ = \overline{vars(r̄)} \\ E^{♭} = ∃_{Δ}D^{♭} \end{matrix} \}.

Then, for each (s̄, D^{♯}) ∈ Pattern(D^{♯}) such that s̄ ∈ T_{z}^{n} and each k < n,

project_{k}((s̄, D^{♯})) =^{def} (\underbrace{(π_{1}(s̄), …, π_{k}(s̄))}_{t̄}, ¯∃ ; ¯∃_{j} D^{♯}),

where j =^{def} |vars(t̄)|.

It is easy to show that project is indeed correct with respect to the obvious concrete operation.

5.4 Remapping

Consider a description (s̄, D♯ ; s̄) ∈ Pattern(D^{♯}) and a pattern r̄ ∈ T_{z′}^{⋆} such that r̄ is an anti-instance of s̄. We want to obtain D♯ ; r̄ ∈ D^{♯} such that

γ((r̄′, D♯ ; r̄)) ⊇ γ((s̄, D♯ ; s̄)).  (9)

This is what we call remapping (s̄, D♯ ; s̄) to r̄.

Definition 7 (The remap operation.) Let (s̄, D♯ ; s̄) be a description with s̄ ∈ T_{z}^{k} and let r̄ ∈ T_{z′}^{k} be an anti-instance of s̄. Assume |vars(r̄)| = m and let ū ∈ T_{z}^{m} be the unique tuple such that

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

Then the operation remap(s̄, D♯ ; s̄, r̄) yields D♯ ; r̄ such that

γ(D♯ ; r̄) ⊇ { (ū′[t̄/ vseq(ū′)], D^{♭}) | (t̄, D^{♭}) ∈ γ(D♯ ; s̄) }.  (11)

Observe that the remap function is closely related to the residual abstraction function α′ of Figure 1. It can be proven [4] that the specification of remap meets our original requirement.

Theorem 8 Let (s̄, D♯ ; s̄) be a description with s̄ ∈ T_{z}^{k}. Let also r̄ ∈ T_{z′}^{k} be an antiinstance of s̄. If D♯ ; r̄ = remap(s̄, D♯ ; s̄, r̄) then γ((r̄′, D♯ ; r̄)) ⊇ γ((s̄, D♯ ; s̄)).

5.5 Join and Widenings

The operation of merging two descriptions turns out to be an easy one, once remapping has been defined.

Definition 9 (The join_{ϕ} operations.) 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 =^{def} {(s̄_{i}, D_{i}^{♯})}_{i∈I} of elements

of Pattern(D^{♯}) such that s̄_{i} ∈ T_{z}^{k} for each i ∈ I, we have r̄ =^{def} ϕ({s̄_{i}}_{i∈I}) and

join_{ϕ}(F) =^{def} (r̄′, ⨁_{i∈I} remap(s̄_{i}, D_{i}^{♯}, r̄)).

We note again that ϕ might be the least common anti-instance function or an approximation of it: this is one of the degrees of freedom of the framework.

Theorem 10 Let F be as in Definition 9. For each common anti-instance function ϕ and each (s̄_{j}, D_{j}^{♯}) ∈ F we have γ(join_{ϕ}(F)) ⊇ γ((s̄_{j}, D_{j}^{♯})).

As far as widening operators are concerned, there are several possibilities. First of all, we might want to distinguish between widening in the pattern component and widening on the underlying domain. The former can be defined as any join operation join_{ϕ} with ϕ different from lca. The latter consists in propagating the widening to the underlying domain. For instance, the following widening operator is the default one applied by China:

widen((s̄_{1}, D_{1}^{♯}), (s̄_{2}, D_{2}^{♯})) =^{def} \{ \begin{matrix}(s̄_{2}, D_{2}^{♯}), & if s̄_{1} ≠ s̄_{2}; \\ (s̄_{2}, D_{1}^{♯} ∇ D_{2}^{♯}), & if s̄_{1} = s̄_{2}. \end{matrix}  (12)

This operator refrains from widening unless the pattern component is stabilized (see the next section to see why it works). Other operators can be defined by using joins and remappings (see [4]).

5.6 Comparing Descriptions

The last operation that is needed in order to put Pattern(D^{♯}) at work is for comparing descriptions.

Definition 11 (Approximation ordering.) The approximation ordering of the domain Pattern(D^{♯}), denoted by ⊑, is defined as follows, for each (s̄_{1}, D_{1}^{♯}), (s̄_{2}, D_{2}^{♯}) ∈ Pattern(D^{♯}):

(s̄_{1}, D_{1}^{♯}) ⊑ (s̄_{2}, D_{2}^{♯}) ⟺^{def} s̄_{1} = s̄_{2} ∧ D_{1}^{♯} ⊑ D_{2}^{♯}.

It must be stressed that the above approximation ordering is also “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.

The following result is a trivial consequence of Definition 2.

Theorem 12 If (s̄_{1}, D_{1}^{♯}) ⊑ (s̄_{2}, D_{2}^{♯}) then γ((s̄_{1}, D_{1}^{♯})) ⊆ ((s̄_{2}, D_{2}^{♯})). Moreover, ⊑ is a preorder over Pattern(D^{♯}).

Observe that the ability of comparing descriptions only when they have the same pattern is not restrictive in a data-flow analysis setting. The analyzer, in fact, will only need to compare the descriptions arising from the iteration sequence at two consecutive steps. Moreover, if we denote by (s̄_{n}, D_{n}^{♯}) the description at step n, we have

(s̄_{i+1}, D_{i+1}^{♯}) = widen((s̄_{i}, D_{i}^{♯}), join_{ϕ}({(s̄_{i}, D_{i}^{♯}), … })),  (13)

where the widening is possibly omitted. Whether or not the widening has been applied, this implies that s̄′_{i+1} is an anti-instance of s̄_{i} and

γ((s̄_{i}, D_{i}^{♯})) ⊆ γ((s̄_{i+1}, D_{i+1}^{♯})).  (14)

If also the reverse inclusion holds in (14) then we have reached a local fixpoint. The analyzer uses the approximate ordering in order to check for this possibility. Namely, it asks whether (s̄_{i+1}, D_{i+1}^{♯}) ⊑ (s̄_{i}, D_{i}^{♯}). The approximate test, of course, can fail even when equality does hold in (14). 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}^{k}, 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^{♯}.

6 Conclusion

We have presented the rational construction of a generic domain for structural analysis of CLP(H_{X}) languages: Pattern(D_{H_{X}}^{♯}), where the parameter D_{H_{X}}^{♯} is an abstract domain satisfying certain properties, We build on the parameterized Pat(ℜ) domain of Cortesi et al. [6, 7], which is restricted to logic programs. However, while Pat(ℜ) is presented as a specific implementation of a generic structural domain, our formalization is independent from specific implementation techniques. Reasoning at a higher level of abstraction we have been able to fully justify the ideas behind the structural domain. In particular, appealing to familiar notions of unification theory, we have identified an important parameter (a common anti-instance function, missing in [6]) that gives some control over the precision and computational cost of the resulting generic structural domain.

References

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

[2] R. Bagnara. On the detection of implicit and redundant numeric constraints in CLP programs. In M. Alpuente, R. Barbuti, and I. Ramos, editors, Proceedings of the “1994 Joint Conference on Declarative Programming (GULP-PRODE ’94)”, pages 312–326, Peñíscola, Spain, September 1994.

[3] R. Bagnara. A reactive implementation of Pos using ROBDDs. 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 107–121, Aachen, Germany, 1996. Springer-Verlag, Berlin.

[4] 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.

[5] R. Bagnara. A hierarchy of constraint systems for data-flow analysis of constraint logicbased languages. To appear in Science of Computer Programming. Extended version available as TR-96-10, Dipartimento di Informatica, Università di Pisa, 1997.

[6] 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.

[7] A. Cortesi, B. Le Charlier, and P. Van Hentenryck. Combinations of abstract domains for logic programming. In Conference Record of POPL ’94: 21st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 227–239, Portland, Oregon, 1994.

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

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

[10] 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.

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

[12] 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.

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