Constraint Systems for Pattern Analysis of Constraint Logic-Based Languages

Roberto Bagnara Dipartimento di Informatica Università di Pisa Corso Italia 40, 56125 Pisa

                         bagnara@di.unipi.it

Phone: 050/887267 Fax: 050/887226

Abstract

Pattern analysis consists in determining the shape of the set of solutions of the constraint store at some program points. Our basic claim is that pattern analyses can all be described within a unified framework of constraint domains. We show the basic blocks of such a framework as well as construction techniques which induce a hierarchy of domains. In particular, we propose a general methodology for domain combination with asynchronous interaction. The interaction among domains is asynchronous in that it can occur at any time: before, during, and after the product operation in a completely homogeneous way. That is achieved by regarding semantic domains as particular kinds of (ask-and-tell) constraint systems. These constraint systems allow to express communication among domains in a very simple way. The techniques we propose allow for smooth integration within an appropriate framework for the definition of non-standard semantics of constraint logic-based languages. The effectiveness of this methodology is being demonstrated by a prototype implementation of CHINA, a CLP(H, N) analyzer we have developed.

Keywords: Constraint Systems, Constraint-based Languages, Data-flow Analysis, Abstract Interpretation.

1 Introduction

Pattern analysis for constraint logic-based languages consists in determining the shape of the set of solutions of the constraint store at some program point. For usual applications (most prominently, program specialization) the interesting program points are procedure calls and procedure (successful) exits.

In the case of Prolog, pattern analysis has been extensively studied (see [9] for a summary of this work). In the case of CLP, besides the generalization to CLP(H) of the ideas and techniques used for Prolog, not much has been done. A key observation here is that the shape of solutions can be conveniently described by constraints. Thus the CLP framework is general enough to encompass (some of) its own data-flow analyses. Intuitively, this is done by replacing the standard constraint domain with one suitable for expressing the desired information. This fundamental aspect was brought to light in [5] and elaborated in [12].

For languages of the kind of CLP(N), where N is some numerical domains, the first steps towards pattern analysis were moved in [3, 4]. [2] describes some of the more important applications of such analyses. The work done in this field is being generalized to CLP(H, N) languages, integrating numerical and symbolic pattern analysis. This is done with a variety of techniques, including depth-k abstraction. A more restricted kind of integration has recently been described in [17]. Here, the numerical part is essentially the one proposed in [3].

Now, instead of directly describing the techniques employed in [3, 4, 2, 17], we concentrate on what is missing from them: a general notion of constraint domain which allows one to adequately describe both the “logical part” of concrete computations (e.g. answer constraints) and as much pattern analyses (e.g. the shape of those answer constraints) we can think about.

We believe that it is possible to describe every pattern analysis within a unified framework of constraint domains. In particular we wish the framework being able to accommodate approximate inference techniques whose importance relies on very practical considerations, such as representing good compromises between precision and computational efficiency. Some of these techniques will be sketched in the sequel.

Then, what will be needed is a generalized algebraic semantics for constraint logic programs, parameterized with respect to an underlying constraint domain. The main advantages of this approach [12] are that: (1) different instances of CLP can be used to define non-standard semantics for constraint logic programs; and (2) the abstract interpretation of CLP programs can be thus formalized inside the CLP paradigm.

Let us concentrate on constraint domains for pattern analysis. They are algebraic structures of the kind

D̄ = ⟨D, ⪯, ⊗, ⊕, {∃∃_{Δ}}, 0, 1, {dX̄Ȳ }⟩,  (1)

where^{1} D is the set of constraints expressing the properties of interest. D is partially ordered with respect to ⪯ which, intuitively, relates the information content of constraints: C_{1} ⪯ C_{2} means that “C_{1} is more precise than C_{2}”. ⊗ and ⊕ are binary operators modeling conjunction and (weak) disjunction. {∃∃_{Δ}} is a family of unary operators, indexed over finite subsets of variables, modeling projection of constraints onto designated sets of variables. 0 and 1 represent, intuitively, the class of unsatisfiable constraints and the class of non-constraints (i.e. those which do not provide any information), respectively. The family of distinguished elements {dX̄Ȳ }, indexed on pairs of n-tuple of variables, allows to model parameter passing.

In this setting, data-flow analysis is then performed (or at least justified) through abstract interpretation [8, 9], i.e., “mimicking” the program run-time behavior by “executing” it, in a finite way, on an approximated (abstract) constraint domain. We will thus have two constraint domains of the form (1): the “concrete” and the “abstract” one. Following a generalized semantic approach, the concrete and abstract semantics are more easily related, being instances (over two different constraint systems) of the same generalized semantics, which is entirely parametric on a constraint domain. Thus, to ensure correctness, it will be sufficient to exhibit an “abstraction function” α which is a semimorphism between the constraint domains [10].

In this paper we describe a hierarchy of constraint systems which capture all the pattern analyses we know of, as well as the “concrete” collecting semantics they abstract. The basis is constituted by a set of finite constraints, each expressing some partial information about a program execution’s state. Once this is given (simple constraint systems, Section 2), we provide standard ways of representing and composing finite constraints (determinate constraint systems, Section 3). Then we can have the notion of dependency built into the constraint system (ask-and-tell constraint systems Section 4). Another construction is the one which allows us to treat disjunction (powerset constraint systems, Section 5). Finally, in Section 6 we sketch how to achieve combination of domains by considering dependencies within product constraint systems. We feel that, indeed, this is one of more important contributions of this paper.

For the sake of simplicity we will present constraint systems omitting the distinguished elements modeling parameter passing. For most applications dX̄Ȳ is simply a constraint expressing some sort of equivalence between X and Y. We disregard them also because, differently from [12], we do not require them to satisfy any interesting algebraic property.

1For space reasons we omit many details.

2 Simple constraint systems

The basic blocks of our construction are simple constraint systems (or s.c.s.), very similar to those of [19], but with a totally uninformative token (⊤) as in [20].

Definition 2.1 (Simple constraint system.) A simple constraint system is a structure ⟨C, ⊢, ⊥, ⊤⟩, where C is a set of (not better specified) constraints, ⊥ ∈ C, ⊤ ∈ C, and ⊢ ⊆ ℘_{f}(C)×C is a compact entailment relation such that, for each C, C′ ∈ ℘_{f}(C) and c, c′ ∈ C:

\begin{matrix}E_{1}. & c ∈ C ⇒ C ⊢ c, \\ E_{2}. & C ⊢ ⊤, \end{matrix}  \begin{matrix}E_{3}. & (C ⊢ c) ∧ (∀c′ ∈ C : C′ ⊢ c′) ⇒ C′ ⊢ c, \\ E_{4}. & \{⊥\} ⊢ c \end{matrix}

We consider also the extension ⊢ ⊆ ℘(C) × ℘(C) such that, for each C, C′ ∈ ℘(C),

C ⊢ C′ ⇔ ∀c′ ∈ C′ : ∃C′′ ⊆_{f} C . C′′ ⊢ c′.

It is clear that condition E_{1} implies reflexivity of ⊢, while condition E_{3} amounts to transitivity. E_{2} qualifies ⊤ as the least informative token: it will be needed just as a “marker” when the product of simple constraint systems will be considered (see Section 6). E_{4} ensures that C is a finitely generable element.

In general, describing the “standard” semantics of a CLP(X) language is an easy matter. Let T be the theory which corresponds to the domain X [15]. Let D be an appropriate set of formulas in the vocabulary of T closed under conjunction and existential quantification. Define Γ ⊢ c iff Γ entails c in the logic, with non-logical axioms T. Then (D, ⊢) is the required simple constraint system. For CLP(H) (i.e. pure Prolog) one takes the Clark’s theory of equality. For CLP(ℝ) the theory RCF of real closed fields will do the job.

However, describing “standard” constraint domains is not the reason which motivated our work. Here are the original motivations.

2.1 Pattern analysis for numeric domains

The analysis described in [3, 4, 2] is based on constraint inference (a variant of constraint propagation) [11]. This technique, developed in the field of artificial intelligence, has been applied to temporal and spatial reasoning [1, 21].

Let us focus our attention to arithmetic domains, where the constraints are binary relations over expressions. Let E be the set of arithmetic expressions of interest and I the set of intervals over some computable set of numbers (e.g. rational or floating point numbers). Then our constraints are given by

C = { e_{1} ▷◁ e_{2} | ▷◁ ∈ {=, ≠, ≤ <, ≥, >}, e_{1}, e_{2} ∈ E } ∪ { e ◁ I | e ∈ E, I ∈ I }.

The meaning of the constraint e ◁ I is the obvious one: any value the expression e can take is contained in I. Thus C provides a mixture of qualitative (relationships) and quantitative (bounds) knowledge.

Now, the approximate inference techniques we are interested in can be encoded into a consequence relation ⊢ over C. Let us see some of them. The most trivial one is symmetric closure: {e_{1} ▷◁ e_{2}} ⊢ e_{2} ▷◁^{−1} e_{1}, where ▷◁^{−1} is the inverse of ▷◁ (e.g., < is the inverse of >, ≥ of ≤ and so on). A more interesting qualitative technique is transitive closure, allowing inferences like A < C from A ≤ B and B < C. It is formalized by axioms of the form {e_{1} ≤ e_{2}, e_{2} < e_{3}} ⊢ e_{1} < e_{3}. A classical quantitative technique is interval arithmetic which allows to infer the variation interval of an expression from the intervals of its sub-expressions. Let f(e_{1}, …, e_{k}) be any arithmetic expression having e_{1}, …, e_{k} as subexpressions. Then {f(e_{1}, …, e_{k}) ◁ I, e_{1} ◁ I_{1}, …, e_{k} ◁ I_{k}} ⊢ f(e_{1}, …, e_{k}) ◁ f̈(I_{1}, …, I_{k}), where f̈: I^{k} → I is such that for each x_{1} ∈ I_{1}, …, x_{k} ∈ I_{k}, f(x_{1}, …, x_{k}) ∈ f̈(I_{1}, …, I_{k}). An example inference is: A ◁ [3, 6) ∧ B ◁ [−1, 5] ⊢ A + B ◁ [2, 11).

Another technique is numeric constraint propagation, which consists in determining the relationship between two expressions when their associated intervals do not overlap, except possibly at their endpoints. The associated family of axioms is {e_{1} ◁ I_{1}, e_{2} ◁ I_{2}} ⊢ e_{1} ▷◁ e_{2}, with the side condition ∀x_{1} ∈ I_{1}, x_{2} ∈ I_{2} : x_{1} ▷◁ x_{2}. For example, if A ∈ (−∞, 2], B ∈ [2, +∞), and C ∈ [5, 10], we can infer that A ≤ B and A < C. It is also possible to go the other way around, i.e., knowing that U < V may allow to refine the intervals associated to U and V so that they do not overlap. We call this weak interval refinement: {e_{1} ▷◁ e_{2}, e_{1} ◁ I_{1}, e_{2} ◁ I_{2}} ⊢ e_{1} ◁ I′_{1}, where I′_{1} is obtained by shrinking I_{1} so to ensure that x_{1} ∈ I′_{1} iff x_{1} ∈ I_{1} ∧ ∃x_{2} ∈ I_{2} . x_{1} ▷◁ x_{2}.

In summary, by considering the transitive closure of ⊢ and with some minor technical additions we end up with a simple constraint system which characterizes precisely the combination of the above (and possibly other) techniques.

3 Determinate constraint systems

By axioms E_{1} and E_{3} of Definition 2.1 the entailment relation of a simple constraint system is a preorder. Now, instead of considering the quotient poset with respect to the induced equivalence relation, a particular choice of the equivalence classes’ representatives is made: closed sets with respect to entailment. This representation is a very convenient domain-independent strong normal form for constraints.

Definition 3.1 (Elements.) [19] The elements of an s.c.s. ⟨C, ⊢, ⊥, ⊤⟩ are the entailment-closed subsets of C, that is, those C ⊆ C such that ∃C′ ⊆_{f} C . C′ ⊢ c implies c ∈ C. The set of elements of ⟨C, ⊢⟩ is denoted by |C|.

The poset of elements is thus given by ⟨|C|, ⊇⟩. Notice that we deviate from [19] in that we order our constraint systems in the dual way.

Definition 3.2 (Inference map, finite elements.) Given a simple constraint system ⟨C, ⊢, ⊥, ⊤⟩, the inference map of ⟨C, ⊢, ⊥, ⊤⟩ is the function ρ: ℘(C) → ℘(C) given, for each C ⊆ C, by ρ(C) = { c | ∃C′ ⊆_{f} C . C′ ⊢ c }. It is well known that ρ is a kernel operator, over the complete lattice ⟨℘(C), ⊇⟩, whose image is |C|. The image of the restriction of ρ onto ℘_{f}(C) is denoted by |C|_{0}. Elements of |C|_{0} are called finitely generated constraints or simply finite constraints.

From here on we will only work with finitely generated constraints, since we are not concerned with infinite behavior of CLP programs. The next step in our construction is about determinate constraint systems (or d.c.s.).

Definition 3.3 (Determinate constraint system.) Let S = ⟨C, ⊢, ⊥, ⊤⟩ be a simple constraint system. Let 0, 1 ∈ |C|_{0}, ⊗: |C|_{0} × |C|_{0} → |C|_{0}, and ⊢ ⊆ |C|_{0} × |C|_{0} be given, for each C_{1}, C_{2} ∈ |C|_{0}, by

\begin{aligned}0 & = & C, \\ 1 & = & ρ(∅), \end{aligned}  \begin{aligned}C_{1} ⊗ C_{2} & = & ρ(C_{1} ∪ C_{2}), \\ C_{1} ⊢ C_{2} & ⇔ & C_{1} ⊗ C_{2} = C_{1}. \end{aligned}

The projection operators ∃∃_{Δ}: |C|_{0} → |C|_{0} are given, for each Δ ⊆_{f} Vars and each C ∈ ℘(C), by

∃∃_{Δ} C = ρ({ c ∈ C | FV (c) ⊆ Δ }).

Finally, let ⊕: |C|_{0} × |C|_{0} → |C|_{0} be an operator enjoying the following properties:

J_{1}. ⟨|C|_{0}, ⊕, 0⟩ is a commutative and idempotent monoid;

J_{2}. for each C_{1}, C_{2} ∈ |C|_{0}, C_{1} ⊢ C_{1} ⊕ C_{2} and C_{2} ⊢ C_{1} ⊕ C_{2}.

We will refer to the structure ⟨|C|_{0}, ⊢, ⊗, ⊕, {∃∃_{Δ}}, 0, 1⟩ as the determinate constraint system over S and ⊕. The relation ⊑ induced by ⊕ over |C|_{0} is given, for each C_{1}, C_{2} ∈ |C|_{0}, by C_{1} ⊑ C_{2} iff C_{1} ⊕ C_{2} = C_{2}. The relations ⊢ and ⊑ are referred to, respectively, as the approximation ordering and the computational ordering of the determinate constraint system.

Observe that the required conditions on ⊕ are quite reasonable. The purpose of ⊕ is that of “merging” the information originating from different paths in the semantic construction. In this view, axiom J_{1} is very natural: associativity and commutativity amount to say that we can merge paths in any order, idempotence means that we do not loose precision blindly, and 0 being the monoid unit accounts for the ability of discarding failed computation paths. Condition J_{2} states the correctness of the merge operation, characterizing it as a (not necessarily least) upper bound operator with respect to the approximation ordering.

Notice that the distinction between approximation ordering and computational ordering is important. We assume that our semantics are defined as (approximations of) least fixpoints of some operator^{2} ϕ. So, while the approximation ordering, in general abstract interpretation, specifies the relative precision of program properties (e.g. entailment of constraints in our particular case), the computational ordering holds among the iterates ϕ^{k}(⊥) during the fixpoint computation. The case where the two orderings coincide (e.g. in [12]) is thus to be considered a special one. In our treatment, keeping them distinct allows for more freedom in the choice of the merge operator.

Since the set of finite computation paths is, in general, denumerably infinite, we consider also the following strengthening of Definition 3.3.

Definition 3.4 (Closed d.c.s.) A d.c.s. ⟨|C|_{0}, ⊢, ⊗, ⊕, {∃∃_{Δ}}, 0, 1⟩ is said closed iff it satisfies

J_{3}. for each family {C_{i} ∈ |C|_{0}}_{i∈ℕ}, ⨁_{i∈ℕ} C_{i} = C_{1} ⊕ C_{2} ⊕ ⋯ exists and is unique in |C|_{0}; moreover, associativity, commutativity, and idempotence of ⊕ apply to denumerable as well as to finite families of operands.

So, the operation of merging together the information coming from all the computation paths always makes sense in a closed determinate constraint system. Notice however that property J_{3} is only necessary when the semantic construction requires it. This will never happen when considering “abstract” semantic constructions formalizing data-flow analyses (which are finite in nature). In these cases the idea of merging infinitely many pieces of information is a nonsense in itself.

Determinate constraint systems enjoy several properties. Here are some elementary ones: ⊑ is a partial order and C_{1} ⊑ C_{2} implies C_{1} ⊢ C_{2}; ⊗ and ⊕ are componentwise monotone with respect to ⊢ and ⊑, respectively; 0 is an annihilator for ⊗, while 1 is a unit for ⊗ and an annihilator for ⊕. Finally, for absorption laws we have C_{2} = (C_{1} ⊕ C_{2}) ⊗ C_{2} and C_{2} ⊢ (C_{1} ⊗ C_{2}) ⊕ C_{2}. At a higher level, here is the situation.

Theorem 3.1 Let D = ⟨|C|_{0}, ⊢, ⊗, ⊕, {∃∃_{Δ}}, 0, 1⟩ be a determinate constraint system. Then the structure ⟨|C|_{0}; ⊢, 0, 1, ⊗⟩ is a bounded meet-semilattice and ⟨|C|_{0}; ⊑, 0, 1, ⊕⟩ is a join-semilattice. Moreover, if D is complete, then ⟨|C|_{0}; ⊑, 0, 1, ⊕⟩ is a (join-) complete lattice.

Notice that ⟨|C|_{0}, ⊗, ⊕, 0, 1⟩, in general, is not a lattice. Both ⊗ and ⊕ are associative, commutative, and idempotent. But, as stated above, while one of the absorption laws holds, only one direction of the dual law is generally valid. In particular ⊗ is not required to be componentwise monotone with respect to ⊑, and ⊕ might be not componentwise monotone with respect to ⊢. Observe also that ⊕ does not distribute, in general, over ⊗, as this would imply the equivalence of the two absorption laws.

2For example, if we choose a bottom-up (backward) semantic construction for CLP, this will be an immediate consequence operator T_{P} parameterized on the underlying constraint system [12]. We disregard this issues here, as we concentrate on the construction of constraint domains.

4 Ask-and-tell constraint systems

We now consider constraint systems having additional structure. This additional structure allows to express, at the constraint system level, that the imposition of certain constraints must be delayed until some other constraints are imposed. In [18] similar constructions are called askand-tell constraint systems. In our construction, ask-and-tell constraint systems are built from determinate constraint systems by regarding some kernel operators as constraints. We follow [18] in considering cc as the language framework for expressing and computing with kernel operators. For this reason we will present kernel operators as cc agents. For our current purposes we only need a very simple fragment of the determinate cc language: the one of finite cc agents. This fragment is described in [19] by means of a declarative semantics. Here we give an operational characterization which is better suited to our needs.

Definition 4.1 (Finite cc agents: syntax.) A finite cc agent over a simple constraint system S = ⟨C, ⊢, ⊥, ⊤⟩ is any string generated by the following grammar:

Agent ::= tell(C) | ask(C) → Agent | Agent ∥ Agent

where C ∈ |C|_{0}. We will denote by A(S) the language of such strings. The following explicit definition is also given:

ask(C_{1}; …; C_{n}) → Agent ≡ ( ask(C_{1}) → Agent) ∥ ⋯ ∥( ask(C_{n}) → Agent).

When this will not cause confusion we will freely drop the syntactic sugar, writing C and C_{1} → C_{2} where tell(C) and ask(C_{1}) → tell(C_{2}) are intended.

The introduction of a syntactic normal form for finite cc agents allows to simplify to subsequent semantic treatment.

Definition 4.2 (Finite cc agents: syntactic normal form.) The transformation η over A(S) is defined, for each C^{a}, C_{1}^{a}, C_{2}^{a}, C^{t} ∈ |C|_{0} and A, A_{1}, A_{2} ∈ A(S), as follows:

η(C^{a} → C^{t}) = \{ \begin{matrix}1 → 1 & if C^{a} ⊢ C^{t}, \\ C^{a} → (C^{a} ⊗ C^{t}) & otherwise, \end{matrix}
η(C^{t}) = 1 → C^{t},
η(C_{1}^{a} → (C_{2}^{a} → A)) = η((C_{1}^{a} ⊗ C_{2}^{a}) → A),
η(C^{a} → (A_{1} ∥ A_{2})) = η((C^{a} → A_{1}) ∥ (C^{a} → A_{2})),
η(A_{1} ∥ A_{2}) = η(A_{1}) ∥ η(A_{2}).

The following fact is easily proved.

Proposition 4.1 The transformation η of Definition 4.2 is well defined. Furthermore, if A ∈ A(S) then η(A) is of the form (C_{1}^{a} → C_{1}^{t}) ∥ ⋯ ∥ (C_{n}^{a} → C_{n}^{t}).

Thus, by considering only agents of the form ∥_{i=1}^{n} C_{i}^{a} → C_{i}^{t} we do not loose any generality. We will call elementary agents of the kind C^{a} → C^{t} ask–tell pairs.

Now we express the operational semantics of finite cc agents by means of rewrite rules. An agent in normal form is rewritten by applying the logical rules of the calculus modulo a structural congruence. This congruence states, intuitively, that we can regard an agent as a set of (concurrent) ask–tell pairs.

Definition 4.3 (A calculus of finite cc agents.) Let 1_{A} = 1 → 1. The structural congruence of the calculus is the smallest congruence relation ≡_{s} such that ⟨A(S), ∥, 1_{A}⟩_{/≡_{s}} is a commutative and idempotent monoid. The reduction rules of the calculus are given in Figure 1. We also define the relation ρ_{A} ⊆ A(S) × A(S) given, for each A, A′ ∈ A(S), by

A ρ_{A} A′ ⇔ ∃n ∈ ℕ . A = A_{1} ∧ A_{n} = A′ ∧ A_{1} ↦ A_{2} ↦ ⋯ ↦ A_{n} ↛

Structure  {A_{1} ≡_{s} A′_{1} A′_{1} ⟼ A′_{2} A′_{2} ≡_{s} A_{2} \atop A_{1} ⟼ A_{2}}  {A_{1} ⟼ A′_{1} \atop A_{1} ∥ A_{2} ⟼ A′_{1} ∥ A_{2}}

Reduction  {C_{2}^{a} ⊢ C_{1}^{a}  C_{1}^{t} ⊢ C_{2}^{t} \atop (C_{1}^{a} → C_{1}^{t}) ∥ (C_{2}^{a} → C_{2}^{t}) ⟼ (C_{1}^{a} → C_{1}^{t})}

Deduction  C_{1}^{t} ⊢ C_{2}^{a} ; (C_{1}^{a} → C_{1}^{t}) ∥ (C_{2}^{a} → C_{2}^{t}) ⟼ (C_{1}^{a} → (C_{1}^{t} ⊗ C_{2}^{t})) ∥ (C_{2}^{a} → C_{2}^{t})

Absorption C_{1}^{a} ⊢ C_{2}^{a} ; (C_{1}^{a} → C_{1}^{t}) ∥ (C_{2}^{a} → C_{2}^{t}) ⟼ ((C_{1}^{a} ⊗ C_{2}^{t}) → (C_{1}^{t} ⊗ C_{2}^{t})) ∥ (C_{2}^{a} → C_{2}^{t})

Figure 1: Reduction rules for finite cc agents.

In the following we will systematically abuse the notation denoting A(S)_{/≡_{s}} simply by A(S). Consequently, every assertion concerning A(S) is to be intended modulo structural congruence.

Proposition 4.2 The term-rewriting system depicted in Figure 1 is strongly normalizing. Thus the relation ρ_{A} is indeed a function ρ_{A}: A(S) → A(S).

The situation here is almost identical to the one of Definition 3.2, in that we have a domainindependent strong normal form also for the present class of constraints (i.e. agents) incorporating the notion of dependency.

Definition 4.4 (Elements.) The elements of A(S) are those which are closed under (are the fixed points of) the inference map ρ_{A}. The set of elements of A(S) will be denoted by | A(S)|.

The strict analogy with determinate constraint systems continues with the following.

Definition 4.5 (Ask-and-tell constraint system.) Given a simple constraint system S = ⟨C, ⊢, ⊥, ⊤⟩, let A = | A(S)|. Then let 0_{A}, 1_{A} ∈ A, ⊗_{A}: A × A → A, and ⊢_{A} ⊆ A × A be given, for each A_{1}, A_{2} ∈ A, by

\begin{aligned}0_{A} & = & 1 → 0, \\ 1_{A} & = & 1 → 1, \end{aligned}  \begin{aligned}A_{1} ⊗_{A} A_{2} & = & ρ_{A}(A_{1} ∥ A_{2}), \\ A_{1} ⊢_{A} A_{2} & ⇔ & A_{1} ⊗_{A} A_{2} = A_{1}. \end{aligned}

The projection operators The projection operators ∃∃Δ^{A}: A → A are given, for each Δ ⊆_{f} Vars and A ∈ A, by

∃∃Δ^{A} A = ρ_{A}(A_{|_{Δ}}),

where

A_{|_{Δ}} = \{ (∃∃_{Δ} C^{a} → ∃∃_{Δ} C^{t}) | \begin{matrix}(C^{t} → C^{a}) ∈ A and \\ ((1 → ∃∃_{Δ} C^{a}) ⊗_{A} A) ⊢_{A} (1 → C^{a}) \end{matrix} \} .

Finally, let ⊕_{A}: A × A → A be an operator satisfying, for each A_{1}, A_{2} ∈ A, the following axioms:

J_{1}^{a}. ⟨A, ⊕_{A}, 0_{A}⟩ is a commutative and idempotent monoid;

J_{2}^{a}. for each A_{1}, A_{2} ∈ A, A_{1} ⊢_{A} A_{1} ⊕_{A} A_{2} and A_{2} ⊢_{A} A_{1} ⊕_{A} A_{2}.

Again, we will denote by ⊑_{A} the relation induced by ⊕_{A} over A: A_{1} ⊑_{A} A_{2} iff A_{1} ⊕_{A} A_{2} = A_{2}. We will refer to ⟨A, ⊢_{A}, ⊗_{A}, ⊕_{A}, {∃∃Δ^{A}}, 0_{A}, 1_{A}⟩ as the ask-and-tell constraint system over S and ⊕_{A}. We will call it closed iff it satisfies J_{3}^{a}. for each family {A_{i} ∈ A}_{i∈ℕ}, ⨁_{i∈ℕ}^{a} A_{i} = A_{1}⊕_{A}A_{2}⊕_{A}⋯ exists and is unique in A; moreover,

associativity, commutativity, and idempotence of ⊕_{A} apply to denumerable as well as to finite families of operands.

Once you have a determinate constraint system, you also have an ask-and-tell constraint system, whose merge operator is induced as follows.

Definition 4.6 Let S = ⟨C, ⊢, ⊥, ⊤⟩ be an s.c.s., and let D = ⟨|C|_{0}, ⊢, ⊗, ⊕, {∃∃_{Δ}}, 0, 1⟩ a d.c.s. over S. Let also A = | A(S)|, and let ˆ⊕_{A}: A × A → A be given by

( ∥_{i=1}^{n} A_{i}) ˆ⊕_{A} ( ∥_{j=1}^{m} B_{j}) = ρ_{A}( ∥_{i=1}^{n} ∥_{j=1}^{m}(A_{i} ˆ⊕_{A} B_{j})),

where, for any two ask-tell pairs C_{1}^{a} → C_{1}^{t} and C_{2}^{a} → C_{2}^{t}, we define

(C_{1}^{a} → C_{1}^{t}) ˆ⊕_{A} (C_{2}^{a} → C_{2}^{t}) = \{ \begin{matrix}1_{A} & if C^{a} ⊢ C^{t}, \\ C^{a} → (C^{a} ⊗ C^{t}) & otherwise, \end{matrix}

being C^{a} = C_{1}^{a} ⊗C_{2}^{a} and C^{t} = C_{1}^{t} ⊕C_{2}^{t}. We will refer to ˆ⊕_{A} as the merge operator over A induced by D.

Proposition 4.3 ⟨A, ⊢_{A}, ⊗_{A}, ˆ⊕_{A}, {∃∃Δ^{A}}, 0_{A}, 1_{A}⟩ is an ask-and-tell constraint system. Furthermore, it is closed iff D is so.

Notice that ask-and-tell constraint systems subsume the determinate ones, where only “tells” were considered. In fact we have η(C_{1}) ⊗_{A} η(C_{2}) = η(C_{1} ⊗ C_{2}) and η(C_{1}) ˆ⊕_{A} η(C_{2}) = η(C_{1} ⊕ C_{2}).

It is time to start showing why we are interested in this kind of constraint systems, even though for the more exciting things we have to wait until the next section, where combination of constraint domains are introduced. Ask-and-tell constraint system are needed to model approximate inference techniques which can be very useful for pattern analysis.

4.1 More pattern analysis for numeric domains

Following Section 2.1, there is another technique which is used for the analysis described in [3, 4, 2]: relational arithmetic [21]. This technique allows to infer constraints on the qualitative relationship of an expression to its arguments. If we take the ask-and-tell constraint system over the simple one of Section 2.1, we can describe it by a number of (concurrent) agents. Here are some of them (where ▷◁ ranges in {=, ≠, ≤ <, ≥, >}):

ask(x ▷◁ 0) → tell((x + y) ▷◁ y)
ask(x > 0 ∧ y > 0 ∧ x ▷◁ 1) → tell((x ∗ y) ▷◁ y)
ask(x ▷◁ y) → tell(e^{x} ▷◁ e^{y})

An example of inference is deducing X + 1 ≤ Y + 2X + 1 from X ≥ 0 ∧ Y ≥ 0. Notice that there is no restriction to linear constraints.

5 Powerset constraint systems

For the purpose of pattern analysis it is not necessary to represent the “real disjunction” of constraints collected through different computation paths, since we are interested in the common information only. To this end, a weaker notion of disjunction suffices. We define powerset constraint systems, which are instances of a well known construction, i.e., disjunctive completion^{3} [10]. When this is applied to a simple constraint system S it yields the following.

3Given a poset ⟨L, ⊥, ≤⟩, the relation ⪯ ⊆ ℘(L) × ℘(L) induced by ≤ is given, for each M_{1}, M_{2} ∈ ℘(L) by (M_{1} ⪯ M_{2}) ⇔ (∀m_{1} ∈ M_{1} : ∃m_{2} ∈ M_{2} . m_{1} ≤ m_{2}). A subset M ∈ ℘(L) is said non-redundant iff ⊥ ∉ M and ∀m_{1}, m_{2} ∈ M : m_{1} ≤ m_{2} ⇒ m_{1} = m_{2} The set of non-redundant subsets of L is denoted by ℘_{n}(L). The function Ω: ℘(L) → ℘_{n}(L) is given, for each M ∈ ℘(L), by Ω(M) = M \ { m ∈ M | m = ⊥ ∨ ∃m′ ∈ M . m < m′ }.

Definition 5.1 (Powerset constraint system.) Given an s.c.s. ⟨C, ⊢, ⊥, ⊤⟩, the powerset constraint system over ⟨C, ⊢⟩ is given by ⟨℘_{n}(|C|_{0}), ⊢_{P}, ⊗_{P}, ⊕_{P}, {∃∃Δ^{P}}, 0_{P}, 1_{P}⟩, where

\begin{aligned}0_{P} & = & ∅, \\ 1_{P} & = & \{1\}, \\ S_{1} ⊕_{P} S_{2} & = & Ω(S_{1} ∪ S_{2}), \end{aligned}  \begin{aligned}∃∃Δ^{P} S & = & Ω(\{ ∃∃_{Δ} C | C ∈ S \}), \\ S_{1} ⊢_{P} S_{2} & ⇔ & ∀C_{1} ∈ S_{1} : ∃C_{2} ∈ S_{2} . C_{1} ⊢ C_{2}, \\ S_{1} ⊗_{P} S_{2} & = & Ω(\{ C_{1} ⊗ C_{2} | C_{1} ∈ S_{1}, C_{2} ∈ S_{2} \}). \end{aligned}

With these definitions ⟨℘_{n}(|C|_{0}); ⊢_{P}, 0_{P}, 1_{P}, ⊗_{P}, ⊕_{P}⟩, is a join-complete, distributive bounded lattice. We can of course apply the powerset construction also to ask-and-tell constraint systems.

6 Combination of domains

It is well known that different data-flow analyses can be combined together. In the framework of abstract interpretation this can be achieved by means of standard constructions such as reduced product and down-set completion [8, 9]. The key point is that the combined analysis can be more precise than each of the component ones for they can mutually improve each other. However, the degree of cross-fertilization is highly dependent on the degree and quality of interaction taking place among the component domains.

We now propose a general methodology for domain combination with asynchronous interaction. The interaction among domains is asynchronous in that it can occur at any time: before, during, and after the “meet operation” in a completely homogeneous way.

This is achieved by considering ask-and-tell constraint systems built over product simple constraint systems. These constraint systems allow to express communication among domains in a very simple way. They also inherit all the semantic elegance of concurrent constraint programming languages, which provide the basis for their construction. Recently, a methodology for the combination of abstract domains has been proposed in [7], which is directly based onto low level actions such as tests and queries. While the approach in [7] is immediately applicable to an apparently wider range of analyses (this is one subject for further study), the approach we follow here for pattern analysis has the merit of being much more elegant.

We start with a set of simple constraint systems { ⟨C_{i}, ⊢_{i}, ⊥_{i}, ⊤_{i}⟩ | i = 1, …, n }, each expressing some properties of interest, and we wish to combine them so to: (1) perform all the analyses at the same time; and (2) have the domains cooperate to the intent of mutually improving each other. The first goal is achieved by considering the product of the simple constraint systems.

Definition 6.1 (Product of simple constraint systems.) Given a finite family of simple constraint systems S_{i} = ⟨C_{i}, ⊢_{i}, ⊥_{i}, ⊤_{i}⟩ for i = 1, …, n, the product of the family is the structure given by ∏_{i=1}^{n} S_{i} = ⟨C_{×}, ⊢_{×}, ⊥_{×}, ⊤_{×}⟩, where the product tokens are

C_{×} = { (c_{1}, ⊤_{2}, …, ⊤_{n}) | c_{1} ∈ C_{1} } ∪ ⋯ ∪ { (⊤_{1}, …, ⊤_{n−1}, c_{n}) | c_{n} ∈ C_{n} } ∪ {⊥_{×}},

the product entailment is defined, for each C ∈ ℘_{f}(C_{×}), by

C ⊢_{×} (c_{1}, ⊤_{2}, …, ⊤_{n})  ⇔  Π_{1}(C) ⊢_{1} c_{1},
⋮  ⋮  ⋮
C ⊢_{×} (⊤_{1}, …, ⊤_{n−1}, c_{n})  ⇔  Π_{n}(C) ⊢_{n} c_{n},

where, for each i = 1, …, n, Π_{i}: ℘(C_{×}) → C_{i} is the obvious projection mapping a set of n-tuples onto the set of i-th components. Finally, ⊥_{×} = (⊥_{1}, …, ⊥_{n}) and ⊤_{×} = (⊤_{1}, …, ⊤_{n}).

If you had a family of determinate constraint systems D_{i} built on top of the S_{i}’s, you can easily “recycle” the merge operators ⊕_{i} to obtain a merge operator ⊕_{×}: |C_{×}|_{0} × |C_{×}|_{0} → |C_{×}|_{0} which allows you to build a product d.c.s.

So, taking the product of constraint systems, we have realized the simplest form of domain combination. It corresponds to the direct product construction of [8], allowing for different analyses to be carried out at the same time. Notice that there is no communication at all among the domains.

However, as soon as we consider the ask-and-tell constraint system built over the product, we can express asynchronous communication among the domains in complete freedom. At the very least we would like to have the smash product among the component domains. This is realized by the agent ∥_{i=1}^{n}0_{i} → 0_{×}. To say it operationally, the smash agent globalizes the (local) failure on any component domain. This is the only domain-independent agent we have.

Things become much more interesting when instantiated over particular constraint domains. In the CLP(R) system [16] non-linear constraints (e.g. X = Y ∗Z) are delayed (i.e. not treated by the constraint solver) until they become linear (e.g. until either Y or Z are constrained to take a single value). In standard semantic treatments this is modeled in the operational semantics by carrying over, besides the sequence of goals yet to be solved, a set of delayed constraints. Constraints are taken out from this set (and incorporated into the constraint store) as soon as they become linear.

We believe that this can be viewed in an alternative way which is more elegant, as it easily allows for taking into account the delay mechanism also in the fixpoint semantics, and makes sense from an implementation point of view. The basic claim is the following: CLP(R) has three computation domains: Herbrand, ℝ (well, an approximation of it), and definiteness.

In other words, it also manipulates, besides the usual ones, constraints of the kind X = gnd^{♭} which is interpreted as the variable X being definitively bound to a unique value. We can express the semantics of CLP(R) (at a certain level of abstraction) with delay of non-linear constraints by considering the ask-and-tell constraint system over the product of the above three domains. In this view, a constraint of the form X = Y ∗ Z in a program actually corresponds to the agent

ask(Y = gnd^{♭}; Z = gnd^{♭}) → tell(X = Y ∗ Z).

In fact, any CLP(R) user must know that X = Y ∗ Z is just a shorthand for that agent! A similar treatment could be done for logic programs with delay declarations.

Obviously, this cannot be forgotten in abstract constraint systems intended to formalize correct data-flow analyses of CLP(R). Referring back to sections 2.1 and 4.1, when the abstract constraint system extracts information from non-linear constraints, i.e. ask(Y > 0 ∧ Z > 0 ∧ Y ▷◁ 1) → tell((Y ∗ Z) ▷◁ Z) by relational arithmetic, you cannot simply let X = Y ∗ Z stand by itself. By doing this you would incur the risk of overshooting the concrete constraint system (thus loosing soundness), which is unable to deduce anything from non-linear constraints. The right thing to do is to combine your abstract constraint system with one for definiteness (by the product and the ask-and-tell construction) and considering, for example, the following agent:

ask(Y = gnd^{♯}; Z = gnd^{♯}) → ask(Y > 0 ∧ Z > 0 ∧ Y ▷◁ 1)
→ tell((Y ∗ Z) ▷◁ Z)

Beware not to confuse X = gnd^{♭} with X = gnd^{♯}. The first is the concrete one: X is definite if and only if X = gnd^{♭} is entailed in the current store. In contrast, having X = gnd^{♯} entailed in the current abstract constraint store means that X is certainly bound to a unique value in the concrete computation, but this is only a sufficient condition, not a necessary one.

Let us see another example. The analysis described in [13] aims at the compile-time detection of those non-linear constraints that will become linear at run time. This analysis is important for remedying the limitation of CLP(R) to linear constraints by incorporating powerful (and computationally complex) methods from computer algebra as the ones employed in RISC-CLP(Real) [14]. With the results of the above analysis this extension can be done in a smooth way: non-linear constraints which are guaranteed to become linear will be simply delayed, while only the other non-linear constraints will be treated with the special solving techniques. Thus, programs not requiring the extra power of these techniques will be hopefully recognized as such, and will not pay any penalties. The analysis of [13] is a kind of definiteness. One of its difficulties shows up when considering the simplest non-linear constraint: X = Y ∗ Z. Clearly X is definite if Y and Z are such. But we cannot conclude that the definiteness of Y follows from the one of X and Z, as we need also the condition Z ≠ 0. Similarly, we would like to conclude that X is definite if Y or Z have a zero value. Thus we need approximations of the concrete values of variables (i.e. pattern analysis), something which is not captured by common definiteness analyses while being crucial when dealing with non-linear constraints. Then, just take the combination to obtain something like^{4}

ask(Y = gnd^{♯} ∧ Z = gnd^{♯}) → tell(X = gnd^{♯})
∥ ask(Y = 0; Z = 0) → tell(X = gnd^{♯})
∥ ask(X = gnd^{♯} ∧ Z = gnd^{♯} ∧ Z ≠ 0) → tell(Y = gnd^{♯})
∥ ask(X = gnd^{♯} ∧ Y = gnd^{♯} ∧ Y ≠ 0) → tell(Z = gnd^{♯})

7 Conclusion and future work

We have shown a hierarchy of constraint systems which, both theoretically and experimentally, have several nice features. One feature we did not mention before is that proving two members of the hierarchy being one a correct approximation of the other is often quite easy.

Almost all of the ideas in this paper have been satisfactorily implemented in the CHINA analyzer [2]. The experimental results obtained with the implementation represent a strong encouragement to proceed along these lines.

In particular, we have proposed a general methodology for domain combination with asynchronous interaction. The interaction among domains is asynchronous in that it can occur at any time: before, during, and after the domains’ operations in a completely homogeneous way. This is achieved by regarding semantic domains as particular kinds of (ask-and-tell) constraint systems. These constraint systems allow to express communication among domains in a very simple way. They also inherit all the semantic elegance of concurrent constraint programming languages, which provide the basis for their construction. Future work includes answering the following questions: are there variation of these ideas which are applicable also to analysis oriented towards “nonlogical” properties? That is, properties which are not preserved as the computation progresses? Can we turn this constructions capturing dependence, combination, and disjunction into an algebra of constraint domains?

References

[1] J. F. Allen. Maintaining Knowledge About Temporal Intervals. CACM, 26(11):832–843, 1983.

[2] R. Bagnara. On the detection of implicit and redundant numeric constraints in CLP programs. In Proc. GULP–PRODE’94, 1994.

[3] R. Bagnara, R. Giacobazzi, and G. Levi. Static Analysis of CLP Programs over Numeric Domains. In M. Billaud et al., editors, Actes WSA’92, volume 81–82 of Bigre, pages 43–50, 1992.

[4] R. Bagnara, R. Giacobazzi, and G. Levi. An Application of Constraint Propagation to Data-Flow Analysis. In Proc. IEEE CAIA’93, pages 270–276, 1993. IEEE Press.

[5] P. Codognet and G. Filè. Computations, Abstractions and Constraints. In Proc. Fourth IEEE Int’l Conference on Computer Languages. IEEE Press, 1992.

4Notice that this is much more precise than the Prop formula X ← Y ∧ Z [6].

[6] A. Cortesi, G. Filè, and W. Winsborough. Prop revisited: Propositional Formula as Abstract Domain for Groundness Analysis. In Proc. LICS’91, pages 322–327. IEEE Press, 1991.

[7] A. Cortesi, B. Le Charlier, and P. Van Hentenryck. Combinations of abstract domains for logic programming. In Proc. POPL’94, pages 227–239, 1994.

[8] P. Cousot and R. Cousot. Systematic Design of Program Analysis Frameworks. In Proc. POPL’79, pages 269–282, 1979.

[9] P. Cousot and R. Cousot. Abstract Interpretation and Applications to Logic Programs. Journal of Logic Programming, 13(2 & 3):103–179, 1992.

[10] P. Cousot and R. Cousot. Abstract Interpretation Frameworks. Journal of Logic and Computation, 2(4):511–549, 1992.

[11] E. Davis. Constraint Propagation with Interval Labels. Artificial Intelligence, 32:281–331, 1987.

[12] R. Giacobazzi, S. K. Debray, and G. Levi. A Generalized Semantics for Constraint Logic Programs. In Proc. FGCS’92, pages 581–591, 1992.

[13] M. Hanus. Analysis of nonlinear constraints in CLP(R). In D. S. Warren, editor, Proc. ICLP’93, pages 83–99. The MIT Press, 1993.

[14] H. Hong. RISC-CLP(Real): Logic Programming with Non-linear Constraints over the Reals. In F. Benhamou and A. Colmerauer, editors, Constraint Logic Programming: Selected Research. The MIT Press, 1993.

[15] J. Jaffar and J.-L. Lassez. Constraint Logic Programming. In Proc. POPL’87, pages 111–119. ACM, 1987.

[16] J. Jaffar, S. Michaylov, P. Stuckey, and R. Yap. The CLP(R) Language and System. ACM TOPLAS’92, 14(3):339–395, 1992.

[17] G. Janssens, M. Bruynooghe, and V. Englebert. Abstracting numerical values in CLP(H, N). In M. Hermenegildo and J. Penjam, editors, Proc. PLILP’94, volume 844 of LNCS, pages 400–414. Springer-Verlag, 1994.

[18] V. A. Saraswat. Concurrent Constraint Programming. The MIT Press, 1993.

[19] V. A. Saraswat, M. Rinard, and P. Panangaden. Semantic Foundation of Concurrent Constraint Programming. In Proc. POPL’91, pages 333–353. ACM, 1991.

[20] D. Scott. Domains for Denotational Semantics. In M. Nielsen and E. M. Schmidt, editors, Proc. ICALP’82, volume 140 of LNCS, pages 577–613. Springer-Verlag, 1982.

[21] R. Simmons. Commonsense Arithmetic Reasoning. In Proc. AAAI-86, pages 118–124, 1986.