Set-Based Program Analysis

(Extended Abstract)

Nevin Heintze^{∗} and Joxan Jaffar^{†}

1 January 1991

Summary

Program analysis involves approximating the semantics of programs. One important kind of approximation, that of ignoring intervariable dependencies, is widely used for reasons of decidability and efficiency. This paper addresses program analysis wherein ignoring intervariable dependencies is the only kind of approximation used.

Starting with the collecting semantics of a program, it is shown that there is a natural formalization of this approximation in which program variables are associated with sets of values. Further, this formalization is applicable to both the imperative and logic programming paradigms. An algorithm is then presented which inputs an imperative or logic program and constructs an explicit representation of its approximate semantics. It therefore provides the most accurate analysis possible, given that intervariables dependencies are ignored during analysis.

∗School of Computer Science, Carnegie Mellon University, Pittsburgh, PA 15213-3890.

†IBM Thomas J. Watson Research Center, PO Box 704, Yorktown Heights, NY 10598.

1 Introduction

In program analysis, the notion of program approximation is fundamental because it is typically infeasible or impossible to obtain exact information about a program. In general, an approximation has several components, the complexity and number of which determine the simplicity and accuracy of the analysis. For example, one component of an approximation may involve the underlying domain of computation (to reason about integers, one may reason about their signs but ignore their specific values). Another component may involve intervariable relationships, for example, intervariable dependencies may be ignored (to reason about two variables x and y, one may reason about the collection of values each variable may assume, but ignore the collection of tuples (x, y)). For decidability reasons, program analyzers must limit their reasoning about intervariable dependencies. For efficiency reasons, analyzers often completely omit reasoning about intervariable dependencies [11]. This is in addition to making other approximations. What has not been addressed is whether or not program analysis is decidable when ignoring intervariable dependencies is the only approximation used.

The starting point of this paper is the use of environment constraints to specify the exact collecting semantics of a program. Such a formalization is concise because it states just the needed relationships between program points, without resort to the intricate details within a particular operational model. It is then shown that the approximation of ignoring intervariable dependencies can be naturally formalized by a set-based interpretation of these constraints, that is, by interpreting variables over sets of values. More formally, it is shown that the approximate semantics of a program can be defined to be the least set-based model of its environment constraints.

The main result proves that incorporating just the notion of ignoring intervariable dependencies into program semantics results in a decidable approximation. This is presented in the form of an algorithm whose first part rewrites environment constraints into a simpler set-based calculus in such a way that set-based models are preserved. The second part solves the resulting constraints and outputs an explicit representation of the least model. Because this model characterizes the approximate semantics of the program at hand, the algorithm provides the most accurate analysis possible in the context of the approximation considered.

In what follows, both the imperative and logic programming paradigms are considered to emphasize the generality of the result.

1.1 Related Work

The early works [14], [10] and [12] use set formulas on imperative and functional programs to conservatively estimate variable values. In addition to the approximation of ignoring intervariable dependencies, these formulas omit other information (such as that contained in if-then conditions), and the algorithms do not accommodate the notion of intersection between set expressions. Consequently, it is not clear how to relate these formulas with an independent definition of approximate semantics. However, their algorithms are considerably simpler, though less accurate, than the one presented in this paper.

In logic programming, the notion of program approximation has been used to formalize types [13]. Here, superset approximations of a program’s least model were sought. In [7], where the focus was program analysis and not types, the notion of set-based models was introduced, and it was shown that the resulting program approximation was both more accurate and decidable. The logic programming aspect of the present paper advances this work significantly. In [7] program approximation was defined in terms of the immediate consequence operator, and hence was limited to the approximation of bottom-up program execution. It is, for example, not applicable for the analysis of procedure calls in a top-down execution. The present paper, in contrast, is based upon a general formalism for collecting semantics, and hence can also be used for top-down execution strategies. Consequently the present algorithm is more general.

In abstract interpretation [1] approximation is typically formalized by means of a semantic function describing single step approximate computation. The least fixpoint gives the approximate semantics (see, for example, [4] and [5]), and so program analysis reduces to iterative fixpoint computation. Such an approach is not applicable in this paper because the appropriate semantic function does not converge. For example, while the our algorithm reasons exactly on the class of monadic logic programs, no abstract interpretation algorithm can. Note that abstract interpretation approaches typically ignore intervariable dependencies, in addition to making other approximations, for efficiency reasons (see for example [2, 3]).

1.2 Preliminary Definitions

The domain of computation is a Herbrand Universe with functors Σ hereafter denoted by small letters, and Σ^{−1} containing the projections of Σ: {f_{(i)}^{−1} : f is an n-ary symbol from Σ, 1 ≤ i ≤ n}. Program variables V are hereafter denoted by W, X, Y, Z. A term is constructed from V, Σ and Σ^{−1}; a simple term is constructed from V and Σ only. A ground term or simple term contains no variables.

A logic program also uses predicate symbols Π, and it is defined to be a finite collection of rules of the form H ← B_{1}, ⋯, B_{n}, n ≥ 0, where H, B_{1}, ⋯, B_{n} are atoms built from simple terms and Π. H is called the head of the rule while each B_{i} is called a body atom. There are two further conditions: first, a program contains one special rule, called the initial goal, which has no head atom; second, no variable is common to two rules in a program. Let head_{P} and body_{P} respectively denote the head and body atoms in P.

An imperative program is a finite sequence Stat⋆ of statements Stat:

Stat ::= X := t | if cond then Stat⋆ | while cond do Stat⋆

where t is a term, and cond (a program condition) ranges over boolean combinations of two basic relations: (a) X = s where s is either a program variable or a ground simple term, and (b) match_{s}(X) where s a template for a set of terms, that is, s is constructed from Σ and a new class of template variables. The relation match_{s}(X) is true if there is a substitution θ on the template variables such that θ(s) is equal to the ground term bound to X. Intuitively, the basic operations of imperative programs are data construction and destruction, and the basic tests involve term matching.

An environment, hereafter denoted by ρ, is a mapping from V into ground simple terms. We write ρ[X↦t] to denote the environment which is identical to ρ except that it maps X to t. For example, if ρ maps X to a.b.nil^{1} and Y to c, then execution of the imperative program Z_{1} := Y.X; Z_{2} := cdr(X); Z_{3} := c.(car(X)).nil starting from ρ results in the environment ρ[Z_{1}↦c.a.b.nil][Z_{2}↦b.nil][Z_{3}↦c.a.nil]. In what follows, we use notation such as {(X↦t_{1}, Y ↦t_{2}), (X↦s_{1}, Y ↦s_{2})} as an abbreviation for the collection of environments {ρ : ρ(X) = t_{1} ∧ ρ(Y) = t_{2} or ρ(X) = s_{1} ∧ ρ(Y) = s_{2}}.

2 Collecting Semantics

The execution model of a programming language can be viewed as defining an execution graph for each program. Nodes in this graph represent execution states and edges represent transitions between states. A collecting semantics is obtained by finitely classifying the execution states, and then reasoning about the classes of states. Typically, each class of execution states corresponds to a unique part of the program syntax; hence the classes are called program points.

In imperative programs, program points can be defined by first labelling each statement occurrence S_{i} in the program, and then, for each such S_{i}, associating two program points ↑i and ↓i which indicate the execution states just before and just after S_{i} is executed. In logic programs, program points can be obtained by labelling each rule and each occurrence of a body atom. A rule label indicates the execution state just after the rule has finished executing^{2}; a body atom label indicates the state just before execution of the body atom^{3}. A collecting semantics for both imperative and logic programs associates to each program point a collection of environments.

In what follows we use positive integers for labels. For technical convenience, we assume that the first statement of an imperative program has label 1. For logic programs, we also assume that the first rule of a logic program is the initial goal and has label 1. Consider the following imperative program IP and logic program LP:

1a.b.nil, car and cdr are syntactic sugar for cons(a, cons(b, nil)), cons_{(1)}^{−1} and cons_{(2)}^{−1} respectively.

2That is, every body atom (and sub-goals thereof) has been solved.

3That is, just before the body atom is selected.

1. X := a.b.nil;
2. Y := c;
3. while (X ≠ nil) do
4.  Y := car(X);
5.  X := cdr(X);

1. ← loop(a.b.nil, Y_{1})^{◯_{4}} ._{2. loop(Y_{2}.nil, Y_{2}).}_{3. loop(Z.X, Y_{3}) ← loop(X, Y_{3})^{◯_{5}} .}

Note that the label 3 corresponds to the entire while-do statement in IP. There are 10 program points for IP and 5 for LP. (Sometimes we will write labels n as ◯_{n} to avoid confusion with footnotes.) During execution of IP we have the following (in which we omit mention of the program points ↑1, ↓1, ↑2 and ↓2 for brevity):

\begin{aligned}& before \\ ↑3 & \{(X↦a.b.nil, Y ↦c)\} \\ ↑4 & \{(X↦a.b.nil, Y ↦c), (X↦b.nil, Y ↦a)\} \\ ↑5 & \{(X↦a.b.nil, Y ↦a), (X↦b.nil, Y ↦b)\} \end{aligned}  \begin{aligned}& after \\ ↓3 & \{(X↦nil, Y ↦b)\} \\ ↓4 & \{(X↦a.b.nil, Y ↦a), (X↦b.nil, Y ↦b)\} \\ ↓5 & \{(X↦b.nil, Y ↦a), (X↦nil, Y ↦b)\} \end{aligned}

During execution of LP we have the following (in which we omit Z for brevity):

before (atom)

4  all environments
5 {(X↦b.nil), (X↦nil)}

after (rule)

1  {(Y_{1}↦b)}
2  {(Y_{2}↦b)}
3 {(X↦b.nil, Y_{3}↦b)}

Let M denote an interpreter for imperative programs P which executes P in the obvious sequential manner.

Definition 1 The \underline{collecting semantics}^{4} of an imperative program P is the mapping:

↑i into \{ρ : \begin{matrix}when M executes P starting with some environment, \\ the environment ρ is encountered just before S_{i} is executed \end{matrix} \} ,

↓i into \{ρ : \begin{matrix}when M executes P starting with some environment, \\ the environment ρ is encountered just after S_{i} is executed \end{matrix} \}

for all program points ↑i and ↓i in P.

Before defining the collecting semantics for logic programs, we use the terminology of CLP [9] and recall some basic definitions. A goal is of the form (C, G) where C is a satisfiable conjunction of term equations, and G is a finite sequence of atoms. There is a derivation step from (C, G) to (C′, G′) if (i) A is selected^{5} from G; (ii) H ← B_{1}, ⋯, B_{n} is a rule and σ is a renaming into new variables; (iii) G′ is the result of replacing A in G by its descendents σ(B_{1}), ⋯, σ(B_{n}), and (iv) C_{n+1} is C_{n} ∧ (A = σ(H)). A derivation is a sequence of goals such that there is a derivation step from any two successive goals in the sequence. An atom in a goal is solved in a derivation if it has no descendents or all its descendents are solved. In the following definition, the only important information contained in the environments of a program point μ pertains to the variables in the rule at hand.

4For technical convenience, execution of an imperative program is defined to start from any environment.

5According to the atom selection rule at hand.

Definition 2 The \underline{collecting semantics} of a logic program P, whose initial goal is G, is the following mapping: for each rule R^{μ} = H ← B_{1}^{μ_{1}}, ⋯, B_{n}^{μ_{n}}, we have

μ_{i} ↦ \{ρ ∘ σ : \begin{matrix}there is a derivation (true, G), ⋯, (C, G′) \\ such that the renaming σ(B_{i}^{μ_{i}}) of B_{i}^{μ_{i}} \\ is selected from G′ and ρ ⊧ C. \end{matrix} \} , 1 ≤ i ≤ n;

μ ↦ \{ρ ∘ σ : \begin{matrix}there is a derivation (true, G), ⋯, (C, G′) \\ in which the renamings σ(B_{1}^{μ_{1}}), ⋯, σ(B_{n}^{μ_{n}}) of B_{1}^{μ_{1}}, ⋯, B_{n}^{μ_{n}} \\ have just^{6} been solved and ρ ⊧ C. \end{matrix} \}

Note that a more general definition of the collecting semantics for logic programs is obtained by collecting the constraints C encountered during execution instead of the environments ρ ∘ σ above. However in this paper we deal only with the values that variables may assume, and so the present (ground) definition suffices.

We now introduce a more flexible representation of the collecting semantics of a program. This representation makes explicit the essential properties of a collecting semantics without resort to an underlying definition of the operational model. Intuitively the representation captures the minimal notion of when a collecting interpretation is consistent. That is, if an environment ρ is associated with a program point μ, and a single step of program execution results in an environment ρ′ at program point μ′, then ρ′ must be associated with program point μ′. The advantage of this representation is that, by varying the interpretation of the constraints, different approximations of the collecting semantics may be obtained, including approximations defined via abstract interpretation, and those defined in this paper.

An environment expression is either an environment variable, hereafter denoted by Ψ, or one of the following:

• Ψ[X ↦ t];

• Ψ[cond];

• [t_{1} ∈ S_{1}, …, t_{n} ∈ S_{n}], n ≥ 0 or

• the union of two environment expressions where X is a program variable, t, t_{1}, …, t_{n} are terms, and S_{1}, …, S_{n} are expressions for sets of terms and are each of the form s_{1}.Ψ_{1} ∪ s_{2}.Ψ_{2} ∪ … s_{m}.Ψ_{m} where s_{1}, …, s_{m} are terms. Intuitively, the first two expressions denote operations on a variable Ψ, while the third expression denotes the construction of a collection of environments. More formally, an interpretation I maps variables Ψ into collections of substitutions, maps expressions of the form s.Ψ into {ρ(s) : ρ ∈ I(Ψ)}, maps ∪ into set union, and finally, maps:

6Strict super-sequences satisfying this property are discounted.

• Ψ[X ↦ t] into {ρ[X↦ρ(t)] : ρ ∈ I(Ψ)};

• Ψ[cond] into {ρ ∈ I(Ψ) : ρ ⊧ cond};

• [t_{1} ∈ S_{1}, …, t_{n} ∈ S_{n}] into {ρ : ρ(t_{1}) ∈ I(S_{1}), …, ρ(t_{n}) ∈ I(S_{n})}^{7}.

An environment constraint is of the form Ψ ⊇ EE where Ψ is an environment variable and EE an environment expression. An interpretation I maps such a constraint into true iff I(Ψ) ⊇ I(EE).

Definition 3 The environment constraints EC_{P} for an imperative program P are:

• Ψ^{↑1} ⊇ [ ];

• Ψ^{↑j} ⊇ Ψ^{↓i}, for all sequences of statements S_{i}; S_{j} appearing in P;

• Ψ^{↓i} ⊇ Ψ^{↑i}[X↦t] for all S_{i} in P of the form X :=t;

•

\begin{matrix}Ψ^{↑j} ⊇ Ψ^{↑i}[cond] \\ Ψ^{↓i} ⊇ Ψ^{↑i}[¬cond] ∪ Ψ^{↓k} \end{matrix} \}

for all S_{i} in P of the form if cond then Stat_{j}; …; Stat_{k};

• \begin{matrix}Ψ^{↑j} ⊇ Ψ^{↑i}[cond] ∪ Ψ^{↓k}[cond] \\ Ψ^{↓i} ⊇ Ψ^{↑i}[¬cond] ∪ Ψ^{↓k}[¬cond] \end{matrix} \} for all S_{i} in P of the form while cond do Stat_{j}; …; Stat_{k};

The (top-down) environment constraints EC_{P} for a logic program P are:

• Ψ^{η} ⊇ [H ∈ Call]^{8} for each body atom B^{η} appearing in a rule H ← ⋯ B^{η} ⋯ in P;

• Ψ^{μ} ⊇ [H ∈ Call, B_{1} ∈ Ret, …, B_{n} ∈ Ret]^{9} for each rule H^{μ} ← B_{1}, …, B_{n} in P labelled with μ;

where Call denotes ( ⋃_{B^{η} ∈body_{P}} B^{η}.Ψ^{η}) and Ret denotes ( ⋃_{H^{μ} ∈head_{P}} H^{μ}.Ψ^{μ}).

The logic program constraints defined above correspond to a top-down parallel interpreter. They can be easily adapted to the case of bottom-up execution, or to top-down execution with a fixed atom selection rule.

7In case n = 0, this reduces to I([ ]) = {ρ : true}, the set of all environments.

8This reduces to [ ] in case the rule is the initial goal.

9This reduces to [B_{1} ∈ Ret, …, B_{n} ∈ Ret] in case the rule is the initial goal.

Recall the previous example imperative program IP and logic program LP; the environment constraints corresponding to these programs are respectively

Ψ^{↑1} ⊇ [ ]
Ψ^{↓1} ⊇ Ψ^{↑1}[X↦a.b.c.nil]
Ψ^{↑2} ⊇ Ψ^{↓1}
Ψ^{↓2} ⊇ Ψ^{↑2}[Y ↦c]
Ψ^{↑3} ⊇ Ψ^{↓2}
Ψ^{↑4} ⊇ Ψ^{↑3}[X ≠ nil] ∪ Ψ^{↓5}[X ≠ nil]
Ψ^{↓4} ⊇ Ψ^{↑4}[Y ↦cons_{(1)}^{−1}(X)]
Ψ^{↑5} ⊇ Ψ^{↓4}
Ψ^{↓5} ⊇ Ψ^{↑5}[X↦cons_{(2)}^{−1}(X)]
Ψ^{↓3} ⊇ Ψ^{↑3}[X = nil] ∪ Ψ^{↓5}[X = nil]

\begin{aligned}Ψ^{◯_{1}} & ⊇ & [loop(a.b.nil, Y_{1}) ∈ Ret] \\ Ψ^{◯_{2}} & ⊇ & [loop(Y_{2}.nil, Y_{2}) ∈ Call] \\ Ψ^{◯_{3}} & ⊇ & [loop(Z.X, Y_{3}) ∈ Call, loop(X, Y_{3}) ∈ Ret] \\ Ψ^{◯_{4}} & ⊇ & [ ] \\ Ψ^{◯_{5}} & ⊇ & [loop(Z.X, Y_{3}) ∈ Call] \end{aligned}

where Call is loop(a.b.nil, Y_{1}).Ψ^{◯_{4}} ∪ loop(X, Y_{3}).Ψ^{◯_{5}}

and Ret is loop(Y_{2}.nil, Y_{2}).Ψ^{◯_{2}} ∪ loop(Z.X, Y_{3}).Ψ^{◯_{3}}

Lemma 1 Let P be an imperative or logic program. Then EC_{P} has a least model which coincides with the collecting semantics of P.

3 Approximate Semantics

To formalize the notion of ignoring inter-variable dependencies, a collection of environments is approximated by a single mapping from V into sets. That is, a (possibly infinite) collection of tuples is approximated by a single sequence of (possibly infinite) sets. A set-based approximation of a collection of environments ρ, ρ′, ⋯ is the sequence of sets ({ρ(X), ρ′(X), ⋯}, {ρ(Y), ρ′(Y), ⋯}, ⋯), where X, Y, ⋯ is some listing of V. We call such a sequence a set substitution because it associates a set to each variable. We write α = A ({ρ, ρ′, ⋯}) to denote that the set substitution α is the set-based approximation of ρ, ρ′, · · ·.

A set substitution may be applied to expressions in a similar manner as in the case for a normal substitution. More formally,

α(t) = \{ \begin{matrix}α(X) & if t is a variable X; \\ \{f(x_{1}, ⋯, x_{n}) : x_{i} ∈ α(t_{i})\} & if t is of the form f(t_{1}, ⋯, t_{n}); \\ \{x_{i} : f(x_{1}, ⋯, x_{n}) ∈ α(t′)\} & if t is of the form f_{(i)}^{−1}(t′). \end{matrix}

We write α[X ↦ S] to denote the set substitution which is identical to α except that it maps X to the set S. We also write α ⊇ α′ to denote that α(X) ⊇ α′(X) for all X ∈ V.

Next, define that a set-based interpretation I of environment constraints is like a normal interpretation except for one fundamental change: I maps variables Ψ into set substitutions, as opposed to collections of environments. Accordingly, I now maps:

• expressions t.Ψ into the set α(t) where α is I(Ψ); • Ψ[X↦t] into α[X↦α(t)] where α is I(Ψ);

• Ψ[cond] into A (\{ρ : \begin{matrix}ρ ⊧ cond ∧ \\ ∀X (ρ(X) ∈ (I(Ψ))(X)) \end{matrix} \});

• [t_{1} ∈ S_{1}, …, t_{n} ∈ S_{n}] into A (\{ρ : \begin{matrix}ρ(t_{1}) & ∈ & I(S_{1}) \\ & ⋯ \\ ρ(t_{n}) & ∈ & I(S_{n}) \end{matrix} \});

• EE_{1} ∪ EE_{2} into α such that α(X) = I(EE_{1})(X) ∪ I(EE_{2})(X) for all X ∈ V;

• constraints Ψ ⊇ EE into true iff I(Ψ) ⊇ I(EE).

In the previous section, the exact semantics of a program was obtained via the least model of the environment constraints at hand. We now obtain

Definition 4 The \underline{approximate semantics} of an imperative or logic program P is the least^{10} set-based model of EC_{P}.

Consider the following logic program LP_{2} and its environment constraints:

\begin{matrix}1. & ← p(W, X)^{◯_{5}} . \\ 2. & p(a, a). \\ 3. & p(b, b). \\ 4. & p(Y, f(f(Z))) ← p(Y, Z)^{◯_{6}} . \end{matrix}  \begin{aligned}Ψ^{◯_{1}} & ⊇ & [p(W, X) ∈ Ret] \\ Ψ^{◯_{2}} & ⊇ & [p(a, a) ∈ Call] \\ Ψ^{◯_{3}} & ⊇ & [p(b, b) ∈ Call] \\ Ψ^{◯_{4}} & ⊇ & [p(Y, f(f(Z))) ∈ Call, p(Y, Z) ∈ Ret] \\ Ψ^{◯_{5}} & ⊇ & [ ] \\ Ψ^{◯_{6}} & ⊇ & [p(Y, f(f(Z))) ∈ Call] \end{aligned}

The following compares the value of Ψ^{◯_{4}} (the return bindings of the last rule above) in the least model and the least set-based model of the environment constraints. Note that the intervariable dependency between Y and Z exhibited in the least model is absent in the least set-based model.

Ψ^{◯_{4}} , exact semantics  Ψ^{◯_{4}} , approximate semantics

\begin{matrix}Y ↦ a & Z ↦ a \\ Y ↦ b & Z ↦ b \\ Y ↦ a & Z ↦ f^{2}(a) \\ Y ↦ b & Z ↦ f^{2}(b) \\ … & … \end{matrix}  \begin{matrix}Y & ↦ & \{a, b\} \\ Z & ↦ & \{a, b\} ∪ f^{2}(\{a, b\}) ∪ f^{4}(\{a, b\}) ∪ … \end{matrix}

The rest of this paper deals with the problem of how to compute the approximate semantics of a given program. Toward this end, we transform the problem of finding the least set-based model of environment constraints into finding the least model of a more explicit class of constraints, the set constraints. The following definitions of set expressions and constraints are made with respect to variables of a given program, say X_{1}, ⋯, X_{N}.

10I ≤ I′ if I(Ψ) ⊆ I′(Ψ) for all Ψ.

A simple set expression is a union and intersection of terms constructed using Σ and a new class of set variables, hereafter denoted by W, X , Y, Z. A quantified set expression is of the form

{X_{i} : ∃X_{1} … X_{i−1}X_{i+1} … X_{N} (F_{1} ∧ ⋯ ∧ F_{n})}

where F_{i} is either (a) of the form t ∈ sexp, where t is a term and sexp a simple set expression, or (b) of the form cond, where cond is an (imperative) program conditional. A set expression is a union of simple and quantified set expressions. Finally, a set constraint is of the form X ⊇ SE where X is a set variable and SE a set expression. An interpretation of such a constraint maps each set variable into a set of ground simple terms, and it maps the constraint into true and false in the obvious way.

We now define how to obtain set constraints SC_{P} corresponding to environment constraints EC_{P}. Intuitively, we will use the set variables X_{1}^{μ}, …, X_{N}^{μ} to represent the program variables X_{1}, ⋯, X_{N}, and accordingly, environment expressions will be rewritten using set variables in place of program variables. Let ω^{μ} be a renaming substitution which maps each program variable X_{i} into its set variable counterpart X_{i}^{μ} w.r.t μ. Also define that Ω maps each expressions t.Ψ^{μ} in EC_{P} into its set expression counterpart ω^{μ}(t). For example, Ω(f(X_{1}, X_{2}).Ψ^{μ} ∪ f(X_{2}, X_{2}).Ψ^{ν}) is f(X_{1}^{μ}, X_{2}^{μ}) ∪ f(X_{2}^{ν}, X_{2}^{ν}). Now, for each environment constraint in EC_{P} of the form:

• Ψ^{μ} ⊇ Ψ^{η}, obtain the set constraints ⋀_{1≤i≤N}X_{i}^{μ} ⊇ X_{i}^{η} ;

• Ψ^{μ} ⊇ Ψ^{η}[X_{i}↦t], obtain the set constraints

⋀_{1≤j≤N}X_{j}^{μ} ⊇ \{X_{j} : ∃X_{1} … X_{j−1}X_{j+1} … X_{N} ( \begin{matrix}X_{1} ∈ X_{1}^{η} \\ ⋯ \\ X_{i} ∈ ω^{η}(t) \\ ⋯ \\ X_{N} ∈ X_{N}^{η} \end{matrix} )\};

• Ψ^{μ} ⊇ Ψ^{η}[cond], obtain the set constraints

⋀_{1≤j≤N}X_{j}^{μ} ⊇ \{X_{j} : ∃X_{1} … X_{j−1}X_{j+1} … X_{N} ( \begin{matrix}X_{1} ∈ X_{1}^{η} \\ ⋯ \\ X_{N} ∈ X_{N}^{η} \\ cond \end{matrix} )\};

• Ψ^{μ} ⊇ [t_{1} ∈ S_{1}, …, t_{n} ∈ S_{n}], obtain the set constraints

⋀_{1≤j≤N}X_{j}^{μ} ⊇ \{X_{j} : ∃X_{1} … X_{j−1}X_{j+1} … X_{N} ( \begin{matrix}t_{1} ∈ Ω(S_{1}) \\ ⋯ \\ t_{N} ∈ Ω(S_{N}) \end{matrix} )\};

• Ψ ⊇ EE_{1} ∪ EE_{2}, continually reduce such a constraint into Ψ ⊇ EE_{1} and Ψ ⊇ EE_{2} until the resulting constraints fall into the above cases.

Definition 5 The set constraints SC_{P} corresponding to a imperative or logic program P is obtained from EC_{P} as described above.

Consider the previous example logic program LP_{2}. The constraints in SC_{P} corresponding to the program points 4, 5 and 6 are:

Y^{◯_{4}} ⊇ \{Y : ∃Z ( \begin{matrix}p(Y, f(f(Z))) & ∈ & p(W^{◯_{5}} , X^{◯_{5}} ) ∪ p(Y^{◯_{6}} , Z^{◯_{6}} ) \\ p(Y, Z) & ∈ & p(a, a) ∪ p(b, b) ∪ p(Y^{◯_{3}} , f(f(Z^{◯_{3}} ))) \end{matrix} )\}
Z^{◯_{4}} ⊇ \{Z : ∃Y ( \begin{matrix}p(Y, f(f(Z))) & ∈ & p(W^{◯_{5}} , X^{◯_{5}} ) ∪ p(Y^{◯_{6}} , Z^{◯_{6}} ) \\ p(Y, Z) & ∈ & p(a, a) ∪ p(b, b) ∪ p(Y^{◯_{3}} , f(f(Z^{◯_{3}} ))) \end{matrix} )\}
W^{◯_{5}} ⊇ {W : ∃X true}
X^{◯_{5}} ⊇ {X : ∃W true}
Y^{◯_{6}} ⊇ {Y : ∃Z ( p(Y, f(f(Z))) ∈ p(W^{◯_{5}} , X^{◯_{5}} ) ∪ p(Y^{◯_{6}} , Z^{◯_{6}} ) )}
Z^{◯_{6}} ⊇ {Z : ∃Y ( p(Y, f(f(Z))) ∈ p(W^{◯_{5}} , X^{◯_{5}} ) ∪ p(Y^{◯_{6}} , Z^{◯_{6}} ) )}

A model of SC_{P} defined in the obvious way. Note that each model I of SC_{P} defines a collecting interpretation for P because it associates to each program point μ the set of environments {ρ : ρ(X_{i}) ∈ I(X_{i}^{μ}), 1 ≤ i ≤ N}.

Lemma 2 The least model of SC_{P} defines the approximate semantics of P.

4 The Algorithm

Partition set constraints X ⊇ exp into the cases: (a) exp is a simple set expression, in which case the constraint is called explicit, and (b) exp is a quantified set expression. Let the notation explicit(SC) denote the conjunction of just the explicit constraints in a conjunction SC.

A simplified overview of the main algorithm is that it starts with constraints SC_{P} obtained from a program P, and by performing a series of transformations, incrementally converts the constraints into explicit form. In each transformation step SC ⟹ SC′, a condition on explicit(SC) must be satisfied before the step is applied. Thus some key subroutines of the algorithm are for reasoning about explicit constraints. These subroutines can be adapted from [8] which contained an algorithm to construct a representation^{11} of the least model of given explicit constraints.

Let SC denote the conjunction of set constraints at hand. Let X̃^{μ} ≠ ◯̸ abbreviate X_{1}^{μ} ≠ ◯̸∧⋯∧X_{N}^{μ} ≠ ◯̸ where X_{1}, ⋯, X_{N} are the program variables at hand. Let Ψ̃ ∈ Φ̃ abbreviate a conjunction of the form Ψ_{1} ∈ Φ_{1} ∧ ⋯ ∧ Ψ_{n} ∈ Φ_{n}, and in particular, let X̃ ∈ X̃^{μ} abbreviate X_{1} ∈ X_{1}^{μ} ∧⋯∧X_{N} ∈ X_{N}^{μ}. Further, let ˜∃\overline{i} abbreviate the sequence of quantifiers ∃X_{1} ⋯ X_{i−1}X_{i+1} ⋯ X_{N}. The following outlines some of the transformation steps applied to SC in the context of a conjunction of explicit constraints ESC:

• If ESC ⊧ X̃^{μ}≠◯̸ ∧ X_{j}^{μ} ∩ X_{k}^{μ} ≠ ◯̸ then replace any expression \{X_{i} : ˜∃\overline{i} (X̃ ∈ X̃^{μ} ∧ X_{j} = X_{k})\} in SC by X_{j}^{μ} ∩ X_{k}^{μ} if i is j or k, and X_{i}^{μ} otherwise.

• If ESC ⊧ X̃^{μ}≠◯̸ ∧ |X_{j}^{μ}| ≥ 2 ∧ |X_{k}^{μ}| ≥ 2 and j ≠ k then replace any expression \{X_{i} : ˜∃\overline{i} (X̃ ∈ X̃^{μ} ∧ X_{j} ≠ X_{k})\} in SC by X_{i}^{μ}.

• Replace any expression \{X_{i} : ˜∃\overline{i} (Ψ̃ ∈ Φ̃ ∧ s ∈ t_{1}∪t_{2})\} in SC by

\{X_{i} : ˜∃\overline{i} (Ψ̃ ∈ Φ̃ ∧ s ∈ t_{1})\} ∪ \{X_{i} : ˜∃\overline{i} (Ψ̃ ∈ Φ̃ ∧ s ∈ t_{2})\}

• Replace any expression \{X_{i} : ˜∃\overline{i} (Ψ̃ ∈ Φ̃ ∧ f(s̃) ∈ g(t̃))\} in SC by

\{X_{i} : ˜∃\overline{i} (Ψ̃ ∈ Φ̃ ∧ s̃ ∈ t̃)\} if f = g and by ◯̸ otherwise.

• If ESC ⊧ s_{j,1} ∩ ⋯ ∩ s_{j,m_{j}} ≠◯̸, 1 ≤ j ≤ N, then replace any expression

\{X_{i} : ˜∃\overline{i} ( \begin{matrix}X_{1} ∈ s_{1,1} \\ ⋯ \\ X_{1} ∈ s_{1,m_{1}} \end{matrix} ⋀ ⋯ ⋀ \begin{matrix}X_{N} ∈ s_{N,1} \\ ⋯ \\ X_{N} ∈ s_{N,m_{N}} \end{matrix} )\} in SC by s_{i,1} ∩ ⋯ ∩ s_{i,m_{i}}.

We first remark that there are in fact a considerable number of additional transformations; they are omitted because they require lengthy preliminary definitions. Further, the transformations can only be applied in certain orders. This is because the interactions between them is particularly problematic for the guarantee of termination. The details are considerable and are left to the full version of this paper.

Let REDUCE(SC, ESC) denote the result of exhaustively applying the above transformations to SC in the context of ESC. The main algorithm, whose simplified format is in figure 1, is essentially a repeated application of REDUCE. In each iteration, a collection ESC of explicit constraints is extracted from the current set constraints SC. REDUCE is then applied on SC and ESC to obtain new set constraints for the next iteration.

11This explicit representation consists of a regular set of terms [6] for each variable at hand.

input an imperative or logic program P; obtain the environment constraints EC_{P} of P; obtain the set constraints SC_{P} from EC_{P}; i := 0; SC_{0} := SC_{P}; repeat

ESC_{i+1} := explicit(SC_{i});

SC_{i+1} := REDUCE(SC_{i}, ESC_{i+1});

i := i + 1;

until (SC_{i} is syntactically the same as SC_{i−1}); output the least model of ESC_{i};

Figure 1: Main Algorithm

Theorem: The main algorithm, when input with an imperative or logic program P:

• terminates, and outputs some I;

• I is the approximate semantics of P.

Termination is proved by establishing a metric on the form of quantified set expressions that appear in SC_{i}. That the transformations are correct, in the sense that they preserve models, can be easily verified. The essence of the proof of global correctness is in showing that when the algorithm terminates, say with i = n, all information about the least model of SC_{0} is contained in the definite constraints of SC_{n}.

We finally remark that the initial set of environments for an imperative program, presently predefined as the set of all environments, can be any set Ψ_{0} which is definable by a mapping of each variable into a regular set of terms. All that is required is to replace the set constraints corresponding to Ψ^{↑1} ⊇ [ ] by set constraints corresponding to Ψ^{↑1} ⊇ Ψ_{0}, and then conjoining appropriate set constraints which characterize Ψ_{0}.

5 Conclusion

The problem considered was formalizing approximate program semantics which (a) most naturally captures the notion of ignoring intervariable dependencies, (b) is as accurate as possible, and (c) is decidable. The first step taken was to define the approximate semantics using environment constraints. The following alternative characterizations of the approximation at hand justify this constraint approach. In the case of both imperative and logic programs, our approximation essentially corresponds to an abstract interpretation in which arbitrary set substitutions are used as the descriptions of collections of environments. Note that such an abstract interpretation approach cannot be directly used to compute the approximation. Another view, for the case of imperative programs, uses a restricted Hoare-style proof system. Recall that the exact collecting semantics of a program P can be characterized as just those environments consistent with a (Hoare- )provable assertion at that point. Accordingly, our approximate semantics essentially corresponds to provability in the context of a restricted assertion language in which no intervariable dependencies may be expressed. An example language: conjunctions of the form Φ_{1}(X_{1}) ∧ … ∧ Φ_{N}(X_{N}) where each Φ_{i}(X_{i}) is some first-order formula in which the program variable X_{i} is the only free variable.

Next addressed was the computation of the approximate semantics. Toward this end, it was first shown that the approximate semantics of an imperative or logic program can be represented uniformly and concisely by a conjunction of set constraints. More specifically, the least model of these constraints characterized the approximate semantics of the program. Finally, an algorithm for constructing a representation of the least model of given set constraints was outlined.

What was thus presented was a precise analyzer for reasoning about programs in the light of the program approximation considered. Consequently, it is strictly more accurate than previous analysis techniques for imperative, functional and logic programming which ignore intervariable dependencies. An additional advantage of the present algorithm is that it is extendible to other kinds of analyses, for example, structure sharing and mode analysis for logic programs. This is essentially because the algorithm preserves certain runtime properties; for example, if X and Y do not share the same occurrence of a term, then X and Y cannot share structure.

Work remains to be done in addressing efficiency considerations. The algorithm, as outlined, emphasized clarity. An implementation in progress reorganizes the algorithm to maintain constraints in a minimal form which helps to substantially reduce redundant computations. Further work also includes considering other classes of programs, CLP (R) for example. Note that there are classes of programs where ignoring intervariable dependencies does not yield a recursive approximation. An example is where program conditions may be arbitrary integer arithmetic expressions. We finally remark that there are important kinds of analysis for which this work does not seem applicable, for example, that which deals with variable aliasing.

References

[1] S. Abramsky and C. Hankin (Eds.), Abstract Interpretation of Declarative Languages, Ellis Horwood, 1987.

[2] M. Bruynooghe and G. Janssens, “An Instance of Abstract Interpretation integrating Type and Mode Inference”, Proceedings 5^{th} Int. Conf. on Logic Programming, K.A. Bowen and R.A. Kowalski (eds), MIT Press, pp 669 - 683, August 1988.

[3] S.K. Debray, “Global Optimization of Logic Programs”, Ph.D. Thesis, Department of Computer Science, SUNY at Stony Brook, 233 pages, December 1986.

[4] P. Cousot and R. Cousot, “Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints”, Proceedings 4^{th} ACM Symposium on Principles of Programming Languages, 1977, pp 238 - 252.

[5] P. Cousot and R. Cousot, “Systematic Design of Program Analysis Frameworks”, Proceedings 6^{th} ACM Symposium on Principles of Programming Languages, 1979, pp 269 - 282.

[6] F. Gècseg and M. Steinby, “Tree Automata”, Akadèmiai Kiadò, Budapest, 1984.

[7] N.C. Heintze and J. Jaffar, “A Finite Presentation Theorem for Approximating Logic Programs”, Proceedings 17^{th} ACM Symposium on Principles of Programming Languages, 1990, pp 197 - 209.

[8] N.C. Heintze and J. Jaffar, “A Decision Procedure for a Class of Herbrand Set Constraints”, Proceedings 5^{th} IEEE Symposium on Logic in Computer Science, June 1990, pp 42 - 51.

[9] Jaffar, J. and Lassez, J-L. “Constraint Logic Programming”, Technical Report 86/73, Dept. of Computer Science, Monash University (June 1986). [An abstract appears in the Proceedings 14^{th} ACM Symposium on Principles of Programming Languages, Munich (January 1987), 111–119.]

[10] N.D. Jones and S.S. Muchnick, “Flow Analysis and Optimization of LISP-like Structures”, Proceedings 6^{th} ACM Symposium on Principles of Programming Languages, 1979, pp 244 - 256.

[11] N.D. Jones and S.S. Muchnick, “Complexity of Flow Analysis, Inductive Assertion Synthesis, and a Language due to Dijkstra”, Proceedings 21^{st} Conference on Foundations of Computer Science, 1980, pp 185 - 190, also in, Program Flow Analysis: Theory and Applications, N.D. Jones and S.S. Muchnick (eds), Prentice-Hall, 1981.

[12] N.D. Jones and S.S. Muchnick, “A Flexible Approach to Interprocedural Dataflow Analysis and Programs with Recursive Data Structures”, Proceedings 9^{th} ACM Symposium on Principles of Programming Languages, 1982, pp 244 - 256.

[13] F. Pfenning (Ed.), Types in Logic Programming, MIT Press Series in Logic Programming, 1991, forthcoming.

[14] J.C. Reynolds, “Automatic Computation of Data Set Definitions”, Information Processing 68, North-Holland, 1969, pp 456 - 461.