Componential Set-Based Analysis

Cormac Flanagan  Matthias Felleisen

cormac@cs.rice.edu    matthias@cs.rice.edu

Rice University^{∗}

Abstract

Set-based analysis is a constraint-based whole program analysis that is applicable to functional and objectoriented programming languages. Unfortunately, the analysis is useless for large programs, since it generates descriptions of data flow relationships that grow quadratically in the size of the program.

This paper presents componential set-based analysis, which is faster and handles larger programs without any loss of accuracy over set-based analysis. The design of the analysis exploits a number of theoretical results concerning constraint systems, including a completeness result and a decision algorithm concerning the observable equivalence of constraint systems. Experimental results validate the practicality of the analysis.

1 The Effectiveness of Set-Based Analysis

Rice’s Scheme program development environment provides a static debugger, MrSpidey, which analyzes a program and, using the results of this analysis, checks the soundness of all computational primitives [9]. If a primitive operation may fault due to a violation of its invariant, MrSpidey highlights the program operation so that the programmer can investigate the potential fault site before running the program. Using the graphical explanation facilities of MrSpidey, the programmer can determine whether this fault will really happen or whether the corresponding correctness proof is beyond the analysis’s capabilities.

MrSpidey’s program analysis is a constraint-based system similar to Heintze’s set-based analysis [11]. The analysis consists of two co-mingled phases: a derivation phase, during which MrSpidey derives constraints describing the data flow relationships of the analyzed program, and a solution phase, during which MrSpidey solves the constraints. The solution conservatively approximates the set of values that may be returned by each program expression.

In practice, MrSpidey has proven highly effective for pedagogic programming, which includes programs of several hundred to a couple of thousand lines of code. It becomes less useful, however, for debugging larger programs due to limitations in the underlying analysis, which has an O(n^{3}) worst-case time bound. The constant on the cubic element is small, but it becomes dominant for programs of several thousand lines.

The bottleneck is due to the excessive size of the constraint systems that describe a program’s data flow relationships. If we could simplify these constraint systems without affecting the data flow relationships that they denote, then we could reduce the analysis times. That is, by first simplifying the constraint system for each program component (e.g. module or package), we could solve the combined system of constraints in less time. Furthermore, if we saved each simplified constraint system in a constraint file, then we could exploit those saved constraints in future runs of the analysis to avoid reprocessing components that have not changed.

The simplification of constraint systems raises both interesting theoretical and practical questions. On the theoretical side, we need to ensure that simplification preserves the observable behavior of a constraint system. In this paper, we provide a complete characterization of observable behavior and, in the course of this development, establish a close connection between this observable equivalence of constraint systems and the equivalence of regular tree grammars (RTGs).^{1} Exploiting this connection, we develop a complete algorithm for deciding the equivalence of constraint systems. Unfortunately, the algorithm is PSPACE-hard.

Fortunately, a minimized constraint system is only optimal but not necessary for practical purposes. The practical question concerns finding approximate algorithms for simplifying constraint systems that would make MrSpidey more useful. To answer this question, we exploit the correspondence between the minimization problems for RTGs and constraint systems to adapt a variety of algorithms for simplifying RTGs to the problem of simplifying constraint systems. Based on these simplification algorithms, we develop a componential,^{2} or component-wise, variant of set-based analysis. Experimental results verify the effectiveness of the simplification algorithms and the corresponding flavors of the analysis. The simplified constraint systems are typically at least an order of magnitude smaller than the original systems, and these reductions in size result in significant gains in the speed of the analysis.

∗This work was partially supported by NSF grants CCR-9633746 and CCR-9619756, and a Lodieska Stockbridge Vaughan Fellowship.

1A number of researchers, including Reynolds [18], Jones and Muchnick [14], Heintze [11], Aiken [2], and Cousot and Cousot [3] previously exploited the relationship between RTGs and the least solution of a constraint system. We present an additional result, namely a connection between RTGs and the observable behavior (i.e., the entire solution space) of constraint systems.

We expect that some of our theoretical and practical results as well as the techniques will carry over to other constraint-based systems, such as the conditional type system of Aiken et al. [2], Eifrig et al.’s object-oriented type system [5], or Pottier’s or Smith et al.’s subtyping simplification algorithms [17, 21].

The presentation proceeds as follows. Section 2 describes an idealized source language. Sections 3 and 4 present the theoretical underpinnings of the new analysis. Section 5 introduces practical constraint simplification algorithms and Sections 6 and 7 discuss how these algorithms perform in a realistic program analysis system. Section 8 discusses related work, and Section 9 describes directions for future research.

2 The Source Language

For simplicity, we derive our analysis for a λ-calculus-like language with constants and labeled expressions. It is straightforward to extend the analysis to a realistic language including assignments, recursive data structures, objects and modules along the lines described in an earlier report [7].

Expressions in the language are either variables, values, function applications, let-expressions, or labeled expressions: see figure 1. We use labels to identify those program expressions whose values we wish to predict. Values include basic constants and functions. Functions have identifying tags so that MrSpidey can reconstruct a call-graph from the results of the analysis. We use let-expressions to introduce polymorphic bindings, and hence restrict these bindings to syntactic values [23]. We work with the usual conventions and terminology of the λ_{v}-calculus when discussing syntactic issues. In

Syntax:

M ∈ Λ = x | V | (M M) | M^{l} (Expressions)
| (let (x M) M)
V ∈ Value  = b | (λ^{t}x.M)  (Values)
x ∈ Vars  = {x, y, z, …}  (Variables)
b ∈ BConst  (Basic constants)
t ∈ Tag  (Function tags)
l ∈ Label  (Expression labels)

Evaluator:

eval : Λ^{0} ⟶ Value ∪ {⊥}
eval(M) = V  if M ⟼^{∗} V

Reduction Rules:

E[ ((λ^{t}x.M) V) ] ⟶ E[ M[x ↦ V] ]  (β_{v})
E[ (let (x V) M) ] ⟶ E[ M[x ↦ V] ]  (βlet )
E[ V^{l} ] ⟶ E[ V ]  (unlabel)

Evaluation Contexts:

E = [ ] | (E M) | (V E) | (let (x E) M) | E^{l}

Figure 1: The source language Λ: syntax and semantics

particular, the substitution operation M[x ← V] replaces all free occurrences of x within M by V, and Λ^{0} denotes the set of closed terms, also called programs. We specify the meaning of programs via the reduction semantics based on the rules described in figure 1. The reduction rules β_{v} and βlet are conventional, and the unlabel rule removes the label from an expression once its value is needed.

3 Set-Based Analysis

Conceptually, set-based analysis consists of two phases: a specification phase and a solution phase.^{3} During the specification phase, the analysis tool derives constraints on the sets of values that program expressions may assume. These constraints describe the data flow relationships of the analyzed program. During the solution phase, the analysis produces finite descriptions of the potentially infinite sets of values that satisfy these constraints. The result provides an approximate set of values for each labeled expression in the program.

3.1 The Constraint Language

To simplify the derivation of the constraint simplification algorithms, we formulate our constraint language in terms of type selectors, instead of the more usual type constructors:

2componential a. of or pertaining to components; spec. (Ling.)

designating the analysis of distinctive sound units or grammatical elements into phonetic or semantics components (New Shorter Oxford English Dictionary, Clarendon Press, 1993)

3Cousot and Cousot showed that set-based analysis can alternatively be formulated as an abstract interpretation computed by chaotic iteration [3].

τ ∈ SetExp = α | c | dom(τ) | rng(τ)
α, β, γ ∈ SetVar ⊃ Label
c ∈ Const = BConst ∪ Tag

A set expression τ is either a set variable; a constant; or one of the “selector” expressions dom(τ) or rng(τ). By using selector expressions, we can specify each “quantum” of the program’s data flow behavior independently; using constructors would combine several of these quanta into one constraint. The meta-variables α, β, γ range over set variables, and we include program labels in the collection of set variables. Constants include both basic constants and function tags. A constraint C is an inequality τ_{1} ≤ τ_{2} relating two set expressions.

Intuitively, each set expression denotes a set of runtime values, and a constraint [τ_{1} ≤ τ_{2}] indicates that the value set denoted by τ_{1} is contained in the value set denoted by τ_{2}. A constraint system S is a collection of constraints. A simple constraint system is a collection of simple constraints, which have the form:

c ≤ β |  α ≤ β | α ≤ dom(β)
| rng(α) ≤ β | dom(α) ≤ β | α ≤ rng(β)

In some cases, we are interested in constraints that only mention certain set variables. The restriction of a constraint system to a collection of set variables E is:

S |_{E} = {C ∈ S | C only mentions set variables in E}

3.2 Semantics of Constraints

A set expression denotes a collection of values, which is represented as a triple X = ⟨C, D, R⟩. The first component C ∈ P(Const)^{4} is a set of basic constants and function tags, and represents a set of run-time values (relative to a given program) according to the relation V in C:

b in C iff b ∈ C
(λ^{t}x.M) in C iff t ∈ C

The second and third components of X denote the possible argument values (dom) and result values (rng) of functions in X, respectively. Since these two components also denote value sets, the appropriate model for set expressions is the solution of the equation:^{5}

D = P(Const) × D × D We use the functions const : D ⟶ P(Const) and dom, rng : D ⟶ D to extract the respective components of an element of D.

We order the elements of D according to a relation that is contravariant in the argument component, since the information about argument values at an application needs to flow backward along data-flow paths to the formal parameter of the corresponding function definitions. Thus ⟨C_{1}, D_{1}, R_{1}⟩ ⊑ ⟨C_{2}, D_{2}, R_{2}⟩ if and only if C_{1} ⊆ C_{2}, D_{2} ⊑ D_{1}, and R_{1} ⊑ R_{2}. The set D forms a complete lattice under this ordering, with top and bottom elements being the solutions to the equations ⊤ = ⟨Const, ⊥, ⊤⟩ and ⊥ = ⟨∅, ⊤, ⊥⟩, respectively.

The semantics of set expressions is defined with respect to a set environment ρ, which maps each set variable to an element of D. We extend the domain of set environments from set variables to set expressions in the natural manner:

ρ : SetExp ⟶ D
ρ(c) = ⟨{c}, ⊤, ⊥⟩
ρ(dom(τ)) = dom (ρ(τ))
ρ(rng(τ)) = rng (ρ(τ))

An environment ρ satisfies a constraint C = [τ_{1} ≤ τ_{2}] (written ρ ⊧ C) if ρ(τ_{1}) ⊑ ρ(τ_{2}). Similarly, ρ satisfies S, or ρ is a solution of S (written ρ ⊧ S) if ρ ⊧ C for each C ∈ S. The solution space of a constraint system S is Soln(S) = {ρ | ρ ⊧ S}. A constraints set S_{1} entails S_{2} (written S_{1} ⊧ S_{2}) iff Soln(S_{1}) ⊆ Soln(S_{2}), and S_{1} is observably equivalent to S_{2} (written S_{1} ≅ S_{2}) iff S_{1} ⊧ S_{2} and S_{2} ⊧ S_{1}.

The restriction of a solution space to a collection of variables E is:

Soln(S) |_{E} = {ρ | ∃ρ′ ∈ Soln(S). ∀α ∈ E. ρ(α) = ρ′(α)}

We extend the notion of restriction to entailment and observable equivalence of constraint systems:

• If Soln(S_{1}) |_{E} ⊆ Soln(S_{2}) |_{E}, then S_{1} entails S_{2} with respect to E (written S_{1} ⊧_{E} S_{2}).

• If S_{1} ⊧_{E} S_{2} and S_{2} ⊧_{E} S_{1} then that S_{1} and S_{2} are observably equivalent with respect to E (written S_{1} ≅_{E} S_{2}) .

3.3 Deriving Constraints

The specification phase of set-based analysis derives constraints on the sets of values that program expressions may assume. Following Aiken et al. and Palsberg and O’Keefe, we formulate this derivation as a subtype system [2, 16].

The derivation proceeds in a syntax-directed manner according to the constraint derivation rules presented

4P denotes the power-set constructor.

5The set D is equivalent to the set of all infinite binary trees with each node labeled with an element of P(Const). This set can be formally defined as the set of total functions f : {dom, rng}^{∗} ⟶ P(Const), and the rest of the development can be adapted mutandis mutatis [16]. For clarity, we present our results using the more intuitive notation instead.

Γ ∪ {x : α} ⊢ x : α, ∅  (var)
Γ ⊢ b : α, {b ≤ α}  (const)
\frac{Γ ⊢ M : α, S}{Γ ⊢ M^{l} : α, S ∪ \{α ≤ l\}}  (label)

\frac{Γ ∪ \{x : α_{1}\} ⊢ M : α_{2}, S}{Γ ⊢ (λ^{t}x.M) : α, S ∪ \{t ≤ α, dom(α) ≤ α_{1}, α_{2} ≤ rng(α)\}} (abs)

\frac{Γ ⊢ M_{i} : β_{i}, S_{i}}{Γ ⊢ (M_{1} M_{2}) : α, S_{1} ∪ S_{2} ∪ \{β_{2} ≤ dom(β_{1}), rng(β_{1}) ≤ α\}} (app)

\frac{Γ ⊢ V : α, S_{V} A = Vars(S_{V} ) \ (F V [rng(Γ)] ∪ Label) Γ ∪ \{x : ∀A. (α, S_{V} )\} ⊢ M : β, S}{Γ ⊢ (let (x V) M) : β, S}  (let)

\frac{ψ is a substitution of fresh vars for A}{Γ ∪ \{x : ∀A. (α, S_{V} )\} ⊢ x : ψ(α), ψ(S_{V} )}  (inst)

Figure 2: Constraint derivation rules.

in figure 2. Each rule infers a judgement of the form Γ ⊢ M : α, S, where the set variable context Γ maps the free variables of M either to set variables or constraint schemas (see below); α names the value set of M; and the constraint system S describes the data flow relationships of M, using α.

The rules (var) and (const) are straightforward. The rule (label) records the value set of a labeled expression in the appropriate label. The rule (abs) for functions records the function’s tag, and also propagates values from the function’s domain into its formal parameter and from the function’s body into its range. The rule (app) for applications propagates values from the argument expression into the domain of the applied function and from the range of that function into the result of the application expression.

The rule (let) produces a constraint schema σ = ∀A. (α, S) for polymorphic, let-bound values [20, 2, 23]. The set variable α names the result of the expression, the constraint system S describes the data flow relationships of the expression, and the set A contains those internal set variables of the constraint system that must be duplicated at each reference to the let-bound variable via the rule (inst). We use F V [rng(Γ)] to denote the free set variables in the range of Γ. The free set variables of a schema σ = ∀A. (α, S) are those in S but not in A, and the free variables of a set variable is simply the set variable itself.

3.4 Set Based Analysis

Every constraint system admits the trivial solution ρ^{⊤} where ρ^{⊤}(α) = ⊤_{s} and ⊤_{s} = ⟨Const, ⊤_{s}, ⊤_{s}⟩. Since ⊤_{s} represents the set of all run-time values, this solution is highly approximate and utterly useless. Fortunately, constraint systems typically yield many additional solutions that more accurately characterize the value sets of program expressions.

For example, consider the program P = (λ^{t}x.x), which yields the constraint system:

{t ≤ α_{P} , dom(α_{P}) ≤ α_{x}, α_{x} ≤ rng(α_{P})}

In addition to the trivial solution described above, this constraint system admits a number of other solutions, including:

\begin{aligned}ρ_{1} & = & \{α_{P} ↦ ⟨\{t\}, ⊥, ⊥⟩, α_{x} ↦ ⊥\} \\ ρ_{2} & = & \{α_{P} ↦ ⟨\{t\}, ⊤, ⊤⟩, α_{x} ↦ ⊤\} \end{aligned}

The solution ρ_{1} more accurately describes the program’s run-time value sets than ρ_{2}. Yet these two solutions are incomparable under the ordering ⊑ (pointwise extended to environments), since it models the flow of values through a program, but does not rank environments according to their accuracy.

Therefore we introduce a second ordering ⊑_{s} on D that properly ranks environments according to their accuracy. This ordering is covariant in the domain position, i.e., ⟨C_{1}, D_{1}, R_{1}⟩ ⊑_{s} ⟨C_{2}, D_{2}, R_{2}⟩ if and only if C_{1} ⊆ C_{2}, D_{1} ⊑_{s} D_{2}, and R_{1} ⊑_{s} R_{2}.

Under this ordering, a constraint system S has both a maximal solution (ρ^{⊤} above) and a minimal solution. The minimal solution exists because the greatest lower bound ⊓_{s} with respect to ⊑_{s} of two solutions is also a solution [11]. We use LeastSoln(S) to denote this least solution, and define set-based analysis as the function that extracts the basic constants and function tags for each labeled expression from LeastSoln(S).

Definition 3.1. (sba) If ∅ ⊢ P : α, S, then:

sba(P)(l) = const(LeastSoln(S)(l))

The solution sba(P) conservatively approximates the value sets for each labeled expression.

Theorem 3.2 (Correctness of sba) If P ⟼^{∗} E[ V^{l} ] then V in sba(P)(l).

This result follows from a subject reduction proof along the lines of Wright and Felleisen [22] and Palsberg [15] and is contained in a related report [8].

3.5 Computing the Least Solution

To compute sba(P), we close the constraint system for P under the rules Θ described in figure 3. Intuitively,

\frac{c ≤ β  β ≤ γ}{c ≤ γ}  (s_{1})

\frac{α ≤ rng(β)  β ≤ γ}{α ≤ rng(γ)}  (s_{2})

\frac{dom(β) ≤ α  β ≤ γ}{dom(γ) ≤ α}  (s_{3})

\frac{α ≤ rng(β)  rng(β) ≤ γ}{α ≤ γ}  (s_{4})

\frac{α ≤ dom(β)  dom(β) ≤ γ}{α ≤ γ}  (s_{5})

Figure 3: The inference rule system Θ.

these rules infer all the data flow paths in the program, and propagate values along those paths. Specifically, the rules (s_{1}), (s_{2}), and (s_{3}) propagate information about constants, function domains and function ranges forward along the data flow paths of the program. These data flow paths are described by constraints of the form β ≤ γ. The rule (s_{4}) constructs the data flow paths from actual to formal parameters for each function call, and the rule (s_{5}) similarly constructs data flow paths from function bodies to corresponding call sites. We write S ⊢_{Θ} C if S proves C via the rules Θ, and use Θ(S) to denote the closure of S under Θ, i.e., the set {C | S ⊢_{Θ} C}.

MrSpidey uses a worklist algorithm to compute the closure of S under Θ efficiently. The worklist keeps track of all eligible inference rules whose antecedents are in S but whose consequent may not be in S. The algorithm repeatedly removes an inference rule from the worklist, adds its consequent to S, if necessary, and then adds to the worklist all inference rules that are made eligible by the addition of that consequent. The process iterates until the worklist is empty, at which point S is closed under Θ. The complete algorithm can be found in an earlier technical report [7].

This closure process propagates all information concerning the possible constants for labeled expressions into constraints of the form c ≤ l. Hence, we can infer sba(P) from Θ(S) according to the following theorem.

Theorem 3.3 If P ∈ Λ^{0} and ∅ ⊢ P : α, S then:

sba(P)(l) = {c | [c ≤ l] ∈ Θ(S)}

4 Observable Equivalence of Constraints

The traditional set-based analysis we have just described has proven highly effective for programs of up to a couple of thousand lines of code. Unfortunately, it is useless for larger programs due to its nature as a whole program analysis and due to the size of the constraint systems it produces, which are quadratic in the size of (large) programs. Storing these constraint systems in memory is beyond the capabilities of most machines.

To overcome this problem, we develop algorithms for simplifying constraints systems. Applying these simplification algorithms to each program component significantly reduces both the time and space required by the overall analysis.

The following subsection shows that constraint simplification does not affect the analysis results provided the simplified system is observably equivalent to the original system. Subsection 4.2 presents a complete proof-theoretic formulation of observable equivalence, and subsection 4.3 exploits this formulation to develop an algorithm for deciding the observable equivalence of constraint systems. The insights provided by this development lead to the practical constraint simplification algorithms of section 5.

4.1 Conditions on Constraint Simplification

Let us consider a program P containing a program component M. Suppose the constraint derivations for M concludes Γ ⊢ M : α, S_{1}, where S_{1} is the constraint system for M. Our goal is to replace S_{1} by a simpler constraint system without changing sba(P).

Since the constraint derivation process is compositional, the constraint derivation for the entire program concludes ∅ ⊢ P : β, S_{C} ∪S_{1}, where S_{C} is the constraint system for the context surrounding M. The combined constraint system S_{C} ∪ S_{1} describes the space of solutions for the entire program, which is the intersection of the two respective solution spaces:

Soln(S_{C} ∪ S_{1}) = Soln(S_{C}) ∩ Soln(S_{1})

and hence Soln(S_{1}) describes at least all the properties of S_{1} relevant to the analysis. However, Soln(S_{1}) may describe solutions for set variables that are not relevant to the analysis of P. In particular,

• sba(P) only references the solutions for labels; and

• the only interactions between S_{C} and S_{1} are due to the set variables {α} ∪ F V [rng(Γ)].

Thus the only properties of S_{1} relevant to the analysis is the solution space for its external set variables

E = Label ∪ {α} ∪ F V [rng(Γ)]

For our original problem, this means that we want a constraint system S_{2} whose solution space restricted to E is equivalent to that of S_{1} restricted to E:

Soln(S_{1}) |_{E} = Soln(S_{2}) |_{E};

or, with the notation from section 3, S_{1} and S_{2} are observably equivalent on E:

S_{1} ≅_{E} S_{2}

We can translate this compaction idea into an additional rule for the constraint derivation system:

\frac{Γ ⊢≅ M : α, S_{1} S_{1} ≅_{E} S_{2} where E = Label ∪ F V [rng(Γ)] ∪ \{α\}}{Γ ⊢≅ M : α, S_{2}} (≅)

This rule is admissible in that any derivation (denoted using ⊢≅) in the extended constraint derivation system produces information that is equivalent to the information produced by the original analysis.

Lemma 4.1 If ∅ ⊢≅ P : α, S, then:

sba(P)(l) = const(LeastSoln(S)(l))

4.2 Proof-Theoretic Characterization

Since the new derivation rule (≅) involves the semantic notion of observably equivalent constraint systems, it cannot be used directly. To make this rule useful, we must first reformulate the observable equivalence relation as a syntactic proof system.

The key properties of the observational equivalence relation are reflections of the properties of the ordering relation (⊑) and the functions dom and rng, respectively. We can reify these properties into a syntactic proof system via the following inference rules:

α ≤ α (reflex) \frac{τ_{1} ≤ τ τ ≤ τ_{2}}{τ_{1} ≤ τ_{2}} (trans′)

\frac{κ_{1} ≤ κ_{2}}{rng(κ_{1}) ≤ rng(κ_{2}) dom(κ_{2}) ≤ dom(κ_{1})} (compat)

where we restrict κ to non-constant set expressions to avoid inferring useless tautologies:

κ ::= α | dom(κ) | rng(κ)

Many of the inferred constraints lie outside of the original language of simple constraints. The extended language of compound constraints is:

C ::= c ≤ κ | κ ≤ κ

While this proof system obviously captures the properties of ⊑, it does not lend itself to an efficient imple-

\frac{α ≤ rng(β)  β ≤ κ}{α ≤ rng(κ)}  (compose_{1})

\frac{α ≤ dom(β)  β ≥ κ}{α ≤ dom(κ)}  (compose_{2})

\frac{α ≥ rng(β)  β ≥ κ}{α ≥ rng(κ)}  (compose_{3})

\frac{α ≥ dom(β)  β ≤ κ}{α ≥ dom(κ)}  (compose_{4})
α ≤ α  (reflex)

\frac{τ_{1} ≤ α  α ≤ τ_{2}}{τ_{1} ≤ τ_{2}}  (trans)

\frac{κ_{1} ≤ κ_{2}}{rng(κ_{1}) ≤ rng(κ_{2}) dom(κ_{2}) ≤ dom(κ_{1})}  (compat)

Figure 4: The inference rule system Ψ.

mentation. Specifically, checking if two potential antecedents of (trans′) contain the same set expression τ involves comparing two potentially large set expressions. Hence we use an alternative proof system that can easily be implemented, yet infers the same constraints as the above. The alternative system consists of the inference rules Ψ described in Figure 4, together with the rules Θ from Figure 3. The rules (compose_{1...4}) replace a reference to a set variable by an upper or lower (non-constant) bound for that variable, as appropriate. The rule (trans) of Ψ provides a weaker characterization of transitivity than the previous rule (trans′), but the additional rules compensate for this weakness.

The proof system Θ ∪ Ψ is sound and complete in that it infers all true compound constraints.

Lemma 4.2 (Soundness and Completeness of ΘΨ) For a simple constraint system S and compound constraint C, S ⊢_{ΨΘ} C if and only if S ⊧ C.

This lemma implies that ΨΘ(S), which denotes the closure of S with respect to Θ∪Ψ, contains exactly those (compound) constraints that hold in all environments in Soln(S). For a collection of external set variables E, ΨΘ(S) |_{E} contains all (compound) constraints that hold in all environments in Soln(S) |_{E}.

Lemma 4.3 S ≅_{E} ΨΘ(S) |_{E}.

We could use this result to define a proof-theoretic equivalent of restricted entailment as follows:

S_{1} ⊢_{ΨΘ}^{E} S_{2} iff ΨΘ(S_{1}) |_{E} ⊇ ΨΘ(S_{2}) |_{E}

and then show that S_{1} ⊢_{ΨΘ}^{E} S_{2} if and only if S_{1} ⊧_{E} S_{2}. However, a variant of the above definition yields a relation that is easier to compute. Specifically, suppose ΨΘ(S_{1}) |_{E} contains the constraint [rng(τ_{1}) ≤ rng(τ_{2})] inferred by (compat). Then, since Vars(τ_{1})∪Vars(τ_{2}) ⊆ E, the corresponding antecedent [τ_{1} ≤ τ_{2}] is also in ΨΘ(S) |_{E}, and therefore:

ΨΘ(S) |_{E} \ {rng(τ_{1}) ≤ rng(τ_{2})} ≅_{E} ΨΘ(S) |_{E}

Put differently, because (compat) does not eliminate any variables, any (compat)-consequent in ΨΘ(S) |_{E} is subsumed by its antecedent. If we define:

Π = Ψ \ {compat}

then this argument implies that ΨΘ(S) |_{E} ≅_{E} ΠΘ(S) |_{E}. Hence we get the following lemma.

Lemma 4.4 S ≅_{E} ΠΘ(S) |_{E}.

Together, lemmas 4.2 and 4.4 provide the basis to introduce proof-theoretic equivalents of restricted entailment and observable equivalence:

• S_{1} ⊢_{ΨΘ}^{E} S_{2} iff ΨΘ(S_{1}) |_{E} ⊇ ΠΘ(S_{2}) |_{E},

• S_{1} =_{ΨΘ}^{E} S_{2} iff S_{1} ⊢_{ΨΘ}^{E} S_{2} and S_{2} ⊢_{ΨΘ}^{E} S_{1}.

The two relations completely characterize restricted entailment and observable equivalence.

Theorem 4.5 (Soundness and Completeness)

1. S_{1} ⊢_{ΨΘ}^{E} S_{2} if and only if S_{1} ⊧_{E} S_{2}.

2. S_{1} =_{ΨΘ}^{E} S_{2} if and only if S_{1} ≅_{E} S_{2}.

4.3 Deciding Observable Equivalence

The relation =_{ΨΘ}^{E} completely characterizes the modeltheoretic observable equivalence relation ≅_{E}, but for an implementation of the extended constraint derivation system we need a decision algorithm for =_{ΨΘ}^{E}.

Given S_{1} and S_{2} closed under Θ, this algorithm needs to verify that Ψ(S_{1}) |_{E} = Ψ(S_{2}) |_{E}. The naive approach to enumerate and to compare the two constraint systems does not work, since they are infinite. For example, if S = {α ≤ rng(α)}, then Ψ(S) is the infinite set {α ≤ rng(α), α ≤ rng(rng(α)), …}.

Fortunately, the infinite constraint systems inferred by Ψ exhibit a regular structure, which we exploit to decide observable equivalence as follows. First, we generate regular grammars describing the upper and lower bounds for each set variable. Second, we extend these grammars to regular tree grammars (RTGs) describing all constraints in Π(S_{1}) |_{E} and Π(S_{2}) |_{E}, excluding those constraints inferred via compat, which we cannot describe in this manner. Third, we use these RTGs to decide entailment by checking if Ψ(S_{1}) |_{E} ⊇ Π(S_{2}) |_{E} via an adaptation of an RTG containment algorithm. To decide observable equivalence, we simply check entailment in both directions. These steps are described in more detail below.

Regular Grammars: Our first step is to describe the lower and upper non-constant bounds for each set variable. Technically, we want to describe the following two languages of types:

{κ | [κ ≤ α] ∈ Ψ(S) and Vars(κ) ⊆ E}
{κ | [α ≤ κ] ∈ Ψ(S) and Vars(κ) ⊆ E}

for each set variable α. Both languages are generated by a regular grammar G_{r}(S, E). The grammar contains the non-terminals α_{U} and α_{L}, for each α in S, which generate the above lower and upper bounds of α, respectively.

The productions of the grammar are determined by S and Ψ. To illustrate this idea, suppose S contains [α ≤ rng(β)]. Then, for each upper bound κ of β, the rule (compose_{1}) infers the upper bound rng(κ) of α. Since, by induction, β’s upper bounds are generated by β_{U}, the production α_{U} ↦ rng(β_{U}) generates the corresponding upper bounds of α. More generally, the collection of productions {α_{U} ↦ rng(β_{U}) | [α ≤ rng(β)] ∈ S} describes all bounds inferred via (compose_{1}). Bounds inferred via the remaining (compose) rules can be described in a similar manner.

Bounds inferred via the rule (reflex) imply the production rules α_{U} ↦ α, α_{L} ↦ α for α ∈ E. The rule (compat) cannot generate constraints of the form [κ ≤ α] or [α ≤ κ]. Finally, consider the rule (trans), and suppose this rule infers an upper bound τ on α. This bound must be inferred from an upper bound τ on β, based on the antecedent [α ≤ β]. Hence the productions {α_{U} ↦ β_{U} | [α ≤ β] ∈ S} generate all upper bounds inferred via (trans). In a similar fashion, the productions {β_{L} ↦ α_{L} | [α ≤ β] ∈ S} generate all lower bounds inferred via (trans).

Definition 4.6. (Regular Grammar G_{r}(S, E)) Let S be a simple constraint system and E a collection of set variables. The regular grammar G_{r}(S, E) consists of the non-terminals {α_{L}, α_{U} | α ∈ Vars(S)} and the following productions:

α_{U} ↦ α, α_{L} ↦ α  ∀ α ∈ E
α_{U} ↦ β_{U}, β_{L} ↦ α_{L}  ∀ [α ≤ β] ∈ S
α_{U} ↦ dom(β_{L})  ∀ [α ≤ dom(β)] ∈ S
α_{U} ↦ rng(β_{U})  ∀ [α ≤ rng(β)] ∈ S
β_{L} ↦ dom(α_{U})  ∀ [dom(α) ≤ β] ∈ S
β_{L} ↦ rng(α_{L})  ∀ [rng(α) ≤ β] ∈ S

The grammar G_{r}(S, E) describes two languages for each set variable: the upper and lower non-constant bounds. Specifically, if ↦_{G}^{∗} denotes a derivation in the grammar G, and L_{G}(x) denotes the language {τ | x ↦_{G}^{∗} τ} generated by a non-terminal x, then the following lemma holds.

Lemma 4.7 If G = G_{r}(S, E), then:

L_{G}(α_{L}) = {κ | [κ ≤ α] ∈ Ψ(S) and Vars(κ) ⊆ E}
L_{G}(α_{U}) = {κ | [α ≤ κ] ∈ Ψ(S) and Vars(κ) ⊆ E}

Proof: We prove each containment relation by induction on the appropriate derivation.

Regular Tree Grammars: The grammar G_{r}(S, E) does not describe all constraints in Π(S) |_{E}. In particular, it does not describe constraints of the form [c ≤ τ] and constraints inferred by (trans) or (compat). To represent the constraint system Π(S) |_{E}, we extend the grammar G_{r}(S, E) to a regular tree grammar G_{t}(S, E). It combines upper and lower bounds for set variables in the same fashion as the (trans) rule, and also generates constraints of the form [c ≤ τ] where appropriate.

Definition 4.8. (Regular Tree Grammar G_{t}(S, E)) The RTG G_{t}(S, E) extends the grammar G_{r}(S, E) with the root non-terminal R and the additional productions:

\begin{matrix}R ↦ [α_{L} ≤ α_{U}] & ∀ α ∈ Vars(S) \\ R ↦ [c ≤ α_{U}] & ∀ [c ≤ α] ∈ S \end{matrix}

where [· ≤ ·] is viewed as a binary constructor.

The grammar G_{t}(S, E) describes all constraints in Π(S) |_{E}.

Lemma 4.9 If G = G_{t}(S, E), then Π(S) |_{E} = L_{G}(R).

Before we can exploit the grammar representation of Π(S) |_{E}, we must still prove that the closure under Θ ∪ Π∪{compat} can be performed in a sequential manner. The following lemma justifies this staging of the closure algorithm.

Lemma 4.10 For any simple constraint system S:

ΨΘ(S) = Ψ(Θ(S)) = compat(Π(Θ(S)))

The Entailment Algorithm: We can check entailment based on lemmas 4.9 and 4.10 as follows. Given S_{1} and S_{2}, we close them under Θ and then have:

S_{2} ⊢_{ΨΘ}^{E} S_{1}
⟺ ΨΘ(S_{2}) |_{E} ⊇ ΠΘ(S_{1}) |_{E} by defn ⊢_{ΨΘ}^{E}
⟺ Ψ(Θ(S_{2})) |_{E} ⊇ Π(Θ(S_{1})) |_{E} by lemma 4.10
⟺ Ψ(S_{2}) |_{E} ⊇ Π(S_{1}) |_{E} as S_{i} = Θ(S_{i})
⟺ compat(Π(S_{2}) |_{E}) ⊇ Π(S_{1}) |_{E} by lemma 4.10
⟺ compat(L_{G_{2}}(R)) ⊇ L_{G_{1}}(R) by lemma 4.9
where G_{i} = G_{t}(S_{i}, E)

The Entailment Algorithm

In the following, P_{fin} denotes the finite power-set constructor.

Let:  \begin{aligned}G_{1} & = & G_{r}(S_{1}, E) \\ G_{2} & = & G_{t}(S_{2}, E) \end{aligned}  L_{i} = \{α_{L} | α ∈ Vars(S_{i})\} U_{i} = \{α_{U} | α ∈ Vars(S_{i})\}

Assume G_{1} and G_{2} are pre-processed to remove ϵ-transitions. For C ∈ P_{fin}(L_{2} × U_{2}), define:

L(C) = {[τ_{L} ≤ τ_{U}] | ⟨α_{L}, β_{U} ⟩ ∈ C, α_{L} ↦_{G_{2}} τ_{L}, β_{U} ↦_{G_{2}} τ_{U} }

The relation R_{S_{1},S_{2}}[·, ·, ·, ·] is defined as the largest relation on L_{1} × U_{1} × P_{fin}(L_{2} × U_{2}) × P_{fin}(L_{2} × U_{2}) such that if:

R_{S_{1},S_{2}}[α_{L}, β_{U} , C, D]  α_{L} ↦_{G_{1}} X  β_{U} ↦_{G_{1}} Y

then one of the following cases hold: 1. L([X ≤ Y]) ⊆ L(C ∪ D).

2. X = rng(α′_{L}), Y = rng(β′_{U}) and R_{S_{1},S_{2}}[α′_{L}, β′_{U} , C, D′], where:

D′ = \{⟨γ′_{L}, δ′_{U} ⟩ | \begin{matrix}⟨γ_{L}, δ_{U} ⟩ ∈ C ∪ D, \\ γ_{L} ↦_{G_{2}} rng(γ′_{L}), δ_{U} ↦_{G_{2}} rng(δ′_{U})\} \end{matrix}

3. X = dom(α′_{U}), Y = dom(β′_{L}) and R_{S_{1},S_{2}}[β′_{L}, α′_{U} , C, D′], where:

D′ = \{⟨δ′_{L}, γ′_{U} ⟩ | \begin{matrix}⟨γ_{L}, δ_{U} ⟩ ∈ C ∪ D, \\ γ_{L} ↦_{G_{2}} dom(γ′_{U}), δ_{U} ↦_{G_{2}} dom(δ′_{L})\} \end{matrix}

The computable entailment relation S_{2} ⊢_{alg}^{E} S_{1} holds if and only if ∀α ∈ Vars(S_{1}):

R_{S_{1},S_{2}}[α_{L}, α_{U} , {⟨γ_{L}, γ_{U} ⟩ | γ ∈ Vars(S_{2})}, ∅]

Figure 5: The computable entailment relation ⊢_{alg}^{E}

The containment question L_{G_{2}}(R) ⊇ L_{G_{1}}(R) can be decided via an RTG containment algorithm. To decide the more difficult question:

compat(L_{G_{2}}(R)) ⊇ L_{G_{1}}(R)

we adapt an RTG containment algorithm to allow for constraints inferred via (compat) on L_{G_{2}}(R).

The extended algorithm is presented in Figure 5. It first computes the largest relation R_{S_{1},S_{2}} such that R_{S_{1},S_{2}}[α_{L}, β_{U}, C, D] holds if and only if:

L([α_{L} ≤ β_{U}]) ⊆ compat(L(C)) ∪ L(D)

where α_{L}, β_{U} describe collections of types; C, D describe collections of constraints; and L([α_{L} ≤ β_{U}]) denotes the language {[τ_{L} ≤ τ_{U}] | α_{L} ↦^{∗} τ_{L}, β_{U} ↦^{∗} τ_{U}}. The first case in the definition of R uses an RTG containment algorithm to detect if L([α_{L} ≤ β_{U}]) ⊆ L(C) ∪ L(D). The two remaining cases handle constraints of the form [rng(α′_{L}) ≤ rng(β′_{U})] or [dom(α′_{U}) ≤ dom(β′_{L})], and allow for inferences via (compat). The relation R can be computed by starting with a maximal relation (true at every point), and then iteratively setting entries to false as required by figure 5, until the largest relation satisfying the definition is reached.

Based on this relation, the algorithm then defines a computable entailment relation ⊢_{alg}^{E} on constraint systems. This relation is equivalent to ⊢_{Ψ}^{E}.

Theorem 4.11 S_{2} ⊢_{Ψ}^{E} S_{1} if and only if S_{2} ⊢_{alg}^{E} S_{1}.

The entailment algorithm takes exponential time, since the size of R is exponential in the number of set variables in S_{2}. Although faster algorithms for the entailment may exist, these algorithms must all be in PSPACE, because the containment problem on NFA’s, which is PSPACE-complete [1], can be polynomially reduced to the entailment problem on constraint systems.

By using the entailment algorithm in both directions, we can now decide if two constraint systems are observable equivalent. Thus, given a constraint system, we can find a minimal, observably equivalent system by systematically generating all constraint systems in order of increasing size, until we find one observably equivalent to the original system. Of course, the process of computing the minimal equivalent system with this algorithm is far too expensive for use in practical program analysis systems.

5 Practical Constraint Simplification

Fortunately, to take advantage of the rule (≅) in a program analysis tool, we do not need a completely minimized constraint system. Any simplifications in a constraint system produces corresponding reductions in the overall analysis time.

For this purpose, we exploit the connection between constraint systems and RTGs. By Lemmas 4.4 and 4.9, any transformation on constraint systems that preserves the language:

L_{G_{t}(Θ(S),E)}(R)

also preserves the observable behavior of S with respect to E. Based on this observation, we transform a variety of existing algorithms for simplifying RTGs to algorithms for simplifying constraint systems. In the following subsections, we present the four most promising algorithms found so far. We use G to denote G_{t}(S, E), and we let X range over non-terminals and p over paths, which are sequences of the constructors dom and rng. Each algorithm assumes that the constraint system S is closed under Θ. Computing this closure corresponds to propagating data flow information locally within a program component. This step is relatively cheap, since program components are typically small (less than a few thousand lines of code).

5.1 Empty Constraint Simplification

A non-terminal X is empty if L_{G}(X) = ∅. Similarly, a production is empty if it refers to empty non-terminals, and a constraint is empty if it only induces empty productions. Since empty productions have no effect on the language generated by G, an empty constraint in S can be deleted without changing S’s observable behavior. To illustrate this idea, consider the program component P = (λ^{g}y.((λ^{f}x.1) y)), where f and g are function tags. Although this example is unrealistic, it illustrates the behavior of our simplification algorithms. Analyzing P according to the constraint derivation rules yields a system S containing ten constraints. Closing S under Θ yields an additional three constraints. Figure 6 displays the resulting constraint system Θ(S), together with the corresponding grammar G_{t}(Θ(S), {α^{P} }). An inspection of this grammar shows that the set of nonempty non-terminals is:

{α^{P}_{L}, α^{P}_{U}, α^{y}_{L}, α^{a}_{U}, α^{r}_{L}, α^{1}_{U}, α^{x}_{L}, R}

Five of the constraints in Θ(S) are empty, and are removed by this simplification algorithm, yielding a simplified system of eight non-empty constraints.

5.2 Unreachable Constraint Simplification

A non-terminal X is unreachable if there is no production R ↦ [Y ≤ Z] or R ↦ [Z ≤ Y] such that L_{G}(Y) ≠ ∅ and Z →_{G}^{∗} p(X). Similarly, a production is unreachable if it refers to unreachable non-terminals, and a constraint is unreachable if it only induces unreachable productions. Unreachable productions have no effect on the language L_{G}(R), and hence unreachable constraints in S can be deleted without changing the observable behavior of S.

In the above example, the reachable non-terminals are α^{1}_{U}, α^{a}_{U} and α^{g}_{U}. Three of the constraints are unreachable, and are removed by this algorithm, yielding a simplified system with five reachable constraints.

5.3 Removing ϵ-Constraints

A constraint of the form [α ≤ β] ∈ S is an ϵ-constraint. Suppose α ∉ E and the only upper bound on α in S is the ϵ-constraint [α ≤ β], i.e., there are no other constraints of the form α ≤ τ, rng(α) ≤ γ, or γ ≤ dom(α) in S. Then, for any solution ρ of S, the set environment

Constraints Production Rules Non-empty

Reachable

f ≤ α^{f}  R ↦ [f ≤ α^{f}_{U}]
dom(α^{f}) ≤ α^{x}  α^{x}_{L} ↦ dom(α^{f}_{U})
1 ≤ α^{1} R ↦ [1 ≤ α^{1}_{U}] 1 ≤ α^{1} 1 ≤ α^{1}
α^{1} ≤ rng(α^{f})  α^{1}_{U} ↦ rng(α^{f}_{U})
rng(α^{f}) ≤ α^{a}  α^{a}_{L} ↦ rng(α^{f}_{L})
α^{y} ≤ α^{r} α^{y}_{U} ↦ α^{r}_{U} α^{r}_{L} ↦ α^{y}_{L} α^{y} ≤ α^{r}
α^{r} ≤ dom(α^{f})  α^{r}_{U} ↦ dom(α^{f}_{L})
g ≤ α^{P}  R ↦ [g ≤ α^{P}_{U}]  g ≤ α^{P}  g ≤ α^{P}
dom(α^{P}) ≤ α^{y}  α^{y}_{L} ↦ dom(α^{P}_{U})  dom(α^{P}) ≤ α^{y}
α^{a} ≤ rng(α^{P})  α^{a}_{U} ↦ rng(α^{P}_{U})  α^{a} ≤ rng(α^{P}) α^{a} ≤ rng(α^{P})
α^{r} ≤ α^{x}  α^{r}_{U} ↦ α^{x}_{U}  α^{x}_{L} ↦ α^{r}_{L}  α^{r} ≤ α^{x}
α^{1} ≤ α^{a}  α^{1}_{U} ↦ α^{a}_{U}  α^{a}_{L} ↦ α^{1}_{L}  α^{1} ≤ α^{a}  α^{1} ≤ α^{a}
1 ≤ α^{a}  R ↦ [1 ≤ α^{a}_{U}]  1 ≤ α^{a}  1 ≤ α^{a}
α^{P}_{L} ↦ α^{P}  α^{P}_{U} ↦ α^{P}

Figure 6: The original constraint system, grammar and simplified constraint systems for P = (λ^{g}y.((λ^{f}x.1) y))

ρ′ defined by:

ρ′(δ) = \{ \begin{matrix}ρ(δ) & if δ ≢ α \\ ρ(β) & if δ ≡ α \end{matrix}

is also a solution of S. Therefore we can replace all occurrences of α in S by β while still preserving the observable behavior Soln(S) |_{E}. This substitution transforms the constraint [α ≤ β] to the tautology [β ≤ β], which can be deleted. Dually, if [α ≤ β] ∈ S with β ∉ E and β having no other lower bounds, then we can replace β by α, again eliminating the constraint [α ≤ β].

To illustrate this idea, consider the remaining constraints for P. In this system, the only upper bound for the set variable α^{1} is the ϵ-constraint [α^{1} ≤ α^{a}]. Hence this algorithm replaces all occurrences of α^{1} by α^{a}, which further simplifies this constraint system into:

{1 ≤ α^{a}, α^{a} ≤ rng(α^{P}), g ≤ α^{P} }

This system is the smallest simple constraint system observably equivalent to the original system Θ(S).

5.4 Hopcroft’s Algorithm

The previous algorithm merges set variables under certain circumstances, and only when they are related by an ϵ-constraint. We would like to identify more general circumstances under which set variables can be merged. To this end, we define a valid unifier for S to be an equivalence relation ∼ on the set variables of S such that we can merge the set variables in each equivalence class of ∼ without changing the observable behavior of S. Using a model-theoretic argument, we can show that an equivalence relation ∼ is a valid unifier for S if

1. Use a variant of Hopcroft’s algorithm [12] to compute an equivalence relation ∼ on the set variables of S that satisfies the following conditions:

(a) Each set variable in E is in an equivalence class by itself.

(b) If [α ≤ β] ∈ S then ∀α ∼ α′ ∃β ∼ β′ such that [α′ ≤ β′] ∈ S.

(c) If [α ≤ rng(β)] ∈ S then ∀α ∼ α′ ∃β ∼ β′ such that [α′ ≤ rng(β′)] ∈ S.

(d) If [rng(α) ≤ β] ∈ S then ∀α ∼ α′ ∃β ∼ β′ such that [rng(α′) ≤ β′] ∈ S.

(e) If [α ≤ dom(β)] ∈ S then ∀α ∼ α′ ∀β ∼ β′ such that [α′ ≤ dom(β′)] ∈ S.

2. Merge set variables according to their equivalence class.

Figure 7: The Hopcroft algorithm

for all solutions ρ ∈ Soln(S) there exists another solution ρ′ ∈ Soln(S) such that ρ′ agrees with ρ on E and ρ′(α) = ρ′(β) for all α ∼ β.

A natural strategy for generating ρ′ from ρ is to map each set variable to the least upper bound of the set variables in its equivalence class:

ρ′(α) = ⨆_{α′∼α} ρ(α′)

Figure 7 describes sufficient conditions to ensure that ρ′ is a solution of S, and hence that ∼ is a valid unifier for S. To produce an equivalence relation satisfying these conditions, we use a variant of Hopcroft’s O(n lg n) time algorithm [12] for computing an equivalence relation on states in a DFA and then merge set variables according to their equivalence class.^{6}

5.5 Simplification Benchmarks

To test the effectiveness of the simplification algorithms, we extended MrSpidey with the four algorithms that we have just described: empty, unreachable, ϵ-removal, and Hopcroft. Each algorithm also implements the preceding simplification strategies. The first three algorithms are linear in the number of non-empty constraints in the system, and Hopcroft is log-linear.

We tested the algorithms on the constraint systems for nine program components on a 167MHz Sparc Ultra 1 with 326M of memory, using the MzScheme byte code compiler [10]. The results are described in figure 8. The second column gives the number of lines in each program component, and the third column gives the number of constraints in the original (unsimplified) constraint system after closing it under the rules Θ. The remaining columns describe the behavior of each simplification algorithm, presenting the factor by which the number of constraints was reduced, and the time (in milliseconds) required for this simplification.

The results demonstrate the effectiveness and efficiency of our simplification algorithms. The resulting constraint systems are typically at least an order of magnitude smaller than the original system. The cost of these algorithms is reasonable, particularly considering that they were run on a byte code compiler. As expected, the more sophisticated algorithms are more effective, but are also more expensive.

6 Componential Set-Based Analysis

Equipped with the simplification algorithms, we return to our original problem of developing a componential set-based analysis. The new analysis tool processes programs in three steps.

1. For each component in the program, the analysis derives and simplifies the constraint system for that component and saves the simplified system in a constraint file, for use in later runs of the analysis. The simplification is performed with respect to the external variables of the component, excluding expression labels, in order to minimize the size of the simplified system. Thus, the simplified system only needs to describe how the component interacts with the rest of the program, and the simplification algorithm can discard constraints that are only necessary to infer local value set invariants. These discarded constraints are reconstructed later as needed. This step can be skipped for each program component that has not changed since the last run of the analysis, since its constraint file can be used instead.

2. The analysis combines the simplified constraint systems of the entire program and closes the combined collection of constraints under Θ, thus propagating data flow information between the constraint systems for the various program components.

3. Finally, to reconstruct the full analysis results for the program component that the programmer is focusing on, the analysis tool combines the constraint system from the second step with the unsimplified constraint system for that component. It closes the resulting system under Θ, which yields appropriate value set invariants for each labeled expression in the component.

The new analysis can easily process programs that consist of many components. For its first step, it eliminates all those constraints that have only local relevance, thus producing a small combined constraint system for the entire program. As a result, the analysis tool can solve the combined system more quickly and using less space than traditional set-based analysis [11]. Finally, it recreates as much precision as traditional setbased analysis as needed on a per-component basis.

The new analysis performs extremely in an interactive setting because it exploits the saved constraint files where possible and thus avoids re-processing many program components unnecessarily.

We implemented four variants of this analysis. Each analysis uses a particular simplification algorithm to simplify the constraint systems for the program components.

6.1 Benchmarks

We tested the componential analyses with five benchmark programs, ranging from 1,200 to 17,000 lines. For comparison purposes, we also analyzed each benchmark with the standard set-based analysis that performs no simplification. The analyses handled library functions in a context-sensitive, polymorphic manner according to the constraint derivation rules (let) and (inst) to avoid merging information between unrelated calls to these

6A similar development based on the definition ρ′(α) = ⊓{ρ(α′) | α ∼ α′} results in an alternative algorithm, which is less effective in practice.

empty  unreachable  ϵ-removal  Hopcroft
Definition  lines  size factor time factor time factor time factor time
map  5  221  3 <10  6  20  11  30  13  30
reverse  6  287  4 <10  8  20  20  10  20  30
substring  8  579  12  10  64  10  64  10  96  20
qsort  41 1387  15 <10  15  30  58  50  66  40
unify  89 2921  10  10  11  80  55 120  65 150
hopcroft  201 8429  25  10  42 100  118 100  124 200
check  237 21854  4  50  4 1150  26 370  168 510
escher-fish 493 30509  187  10  678  40  678  40  678  80
scanner  1209 59215  3 180  17 840  45 2450  57 2120

Figure 8: Behavior of the constraint simplification algorithms.

functions. The remaining functions were analyzed in a context-insensitive, monomorphic manner. The results are documented in figure 9.

The third column in the figure shows the maximum size of the constraint system generated by each analysis, and also shows this size as a percentage of the constraint system generated by the standard analysis. The analyses based on the simplification algorithms produce significantly smaller constraint systems, and can also analyze more programs, such as sba and poly, for which the standard analysis exhausted heap space.

The fourth column shows the time required to analyze each program from scratch, without using any existing constraint files.^{7} The analyses that exploit constraint simplification yield significant speed-ups over the standard analysis because they manipulate much smaller constraint systems. The results indicate that, for these benchmarks, the ϵ-removal algorithm yields the best trade-off between efficiency and effectiveness of the simplification algorithms. The additional simplification performed by the more expensive Hopcroft algorithm is out-weighed by the overhead of running the algorithm. The tradeoff may change as we analyze larger programs.

To test the responsiveness of the componential analyses in an interactive setting based on an analyze-debug-edit cycle, we re-analyzed each benchmark after changing a randomly chosen component in that benchmark. The re-analysis times are shown in the fifth column of figure 9. These times show an order-of-magnitude improvement in analysis times over the original, standard analysis, since the saved constraint files are used to avoid reanalyzing all of the unchanged program components. For example, the analysis of zodiac, which used to take over two minutes, now completes in under four seconds. Since practical debugging sessions using MrSpidey typically involve repeatedly analyzing the project each time the source code of one module is

Number  Analysis/  File
Program  of  Re-analysis size
(# lines) Analysis  constraints  time (s) (bytes)
scanner standard  61K  14.1 7.7 572K
(1253)  empty  24K (39%) 12.0 3.1 189K
unreachable 15K (25%)  9.7 2.0  39K
ϵ-removal  14K (23%)  9.5 1.7  28K
Hopcroft  14K (23%) 10.4 1.7  25K
zodiac standard 704K  133.4 110.6 1634K
(3419) empty 62K (9%) 34.1 8.1 328K
unreachable 21K (3%) 28.8 4.5 169K
ϵ-removal  13K (2%) 28.8 3.8 147K
Hopcroft  11K (2%) 31.4 3.8 136K
nucleic standard 333K  83.9 51.2 2882K
(3432) empty 90K (27%) 52.8 17.8 592K
unreachable 68K (20%) 48.4 14.6 386K
ϵ-removal  56K (17%) 48.3 13.1 330K
Hopcroft  56K (17%) 60.9 13.2 328K
sba standard >5M * * * *
(11560)  empty 1908K (<38%) 181.5 65.5 1351K
unreachable 105K (<2%) 149.5 43.3 920K
ϵ-removal  76K (<2%) 147.1 42.2 770K
Hopcroft  65K (<1%) 156.8 41.1 716K
poly  standard >5M  *      *     *      *
(17661)  empty  >5M  *      *     *      *
unreachable 201K (<4%) 259.6 26.9 1517K
ϵ-removal  68K (<1%) 239.6 13.3 1038K
Hopcroft  38K (<1%) 254.1 10.9 907K

* indicates the analysis exhausted heap space

Figure 9: Behavior of the componential analyses.

modified, e.g., when a bug is identified and eliminated, using separate analysis substantially improves the usability of MrSpidey.

The disk-space required to store the constraint files is shown in column six. Even though these files use a straight-forward, text-based representation, their size is typically within a factor of two or three of the corresponding source file.

7These times exclude scanning and parsing time.

copy  Relative time of smart polymorphic analyses  Mono.
Program lines analysis empty unreachable ϵ-removal Hopcroft analysis
lattice  215  4.2s  39%  36%  35%  38%  42%
browse  233  2.5s  76%  76%  76%  81%  75%
splay  265  7.9s  75%  73%  70%  72%  83%
check  281  50.1s  21%  23%  14%  14%  23%
graphs  621  2.8s  85%  85%  82%  87%  82%
boyer  624  4.3s  46%  46%  49%  50%  40%
matrix  744  7.5s  64%  57%  51%  52%  45%
maze  857  6.2s  64%  59%  58%  61%  54%
nbody  880  39.6s  57%  25%  25%  26%  28%
nucleic 3335  *    * 243s  * 42s  * 42s  * 44s  * 36s

* indicates the copy analysis exhausted heap space, and the table contains absolute times for the other analyses

Figure 10: Times for the smart polymorphic analyses, relative to the copy analysis.

7 Efficient Polymorphic Analysis

The constraint simplification algorithms also enables an efficient polymorphic, or context-sensitive, analysis. To avoid merging information between unrelated calls to functions that are used in a polymorphic fashion, a polymorphic analysis duplicates the function’s constraints at each call site. We extended MrSpidey with five polymorphic analyses. The first analysis is copy, which duplicates the constraint system for each polymorphic reference via a straightforward implementation of the rules (let) and (inst).^{8} The remaining four analyses are smart analyses that simplify the constraint system for each polymorphic definition.

We tested the analyses using a standard set of benchmarks [13]. The results of the test runs are documented in figure 10. The second column shows the number of lines in each benchmark; the third column presents the time for the copy analysis; and columns four to seven show the times for each smart polymorphic analysis, as a percentage of the copy analysis time. For comparison purposes, the last column shows the relative time of the original, but less accurate, monomorphic analysis.

The results again demonstrate the effectiveness of our constraint simplification algorithms. The smart analyses that exploit constraint simplification are always significantly faster and can analyze more programs than the copy analysis. For example, while copy exhausts heap space on the nucleic benchmark, all smart analyses successfully analyzed this benchmark.

Again, it appears that the ϵ-removal analysis yields the best trade-off between efficiency and effectiveness of the simplification algorithms. This analysis provides the additional accuracy of polymorphism without much additional cost over the coarse, monomorphic analysis. With the exception of the benchmarks browse, splay and graphs, which do not re-use many functions in a polymorphic fashion, this analysis is a factor of 2 to 4 times faster than the copy analysis, and it is also capable of analyzing larger programs.

8 Competitive Work

Fähndrich and Aiken [6] examine constraint simplification for an analysis based on a more complex constraint language. They develop a number of heuristic algorithms for constraint simplification, which they test on programs of up to 6000 lines. Their fastest approach yields a factor of 3 saving in both time and space, but is slow in absolute times compared to other analyses.

Pottier [17] studies an ML-style language with a subtype system based on constraints, and and presents an incomplete algorithm for deciding entailment on constraint systems. He proposes some ad hoc algorithms for simplifying constraints, but does not present results on the cost or effectiveness of these algorithms.

Eifrig, Smith and Trifonov [5, 21] describe a subtyping relation between constrained types that are similar to our constraint systems, and they present an incomplete decision algorithm for subtyping. They describe three algorithms for simplifying constraint systems, two of which which are similar to the empty and ϵ-removal algorithms, and the third is a special case of the Hopcroft algorithm. They do not present results on the cost or effectiveness of these algorithms.

Duesterwald et al [4] describe algorithms for simplifying data flow equations. These algorithms are similar to the ϵ-removal and Hopcroft algorithms. Their approach only preserves the greatest solution of the equation system and assumes that the control flow graph is already known. Hence it cannot be used to analyze programs in a componential manner or to analyze programs with advanced control-flow mechanisms such as first-class functions and virtual methods. The paper does not present results on the cost or effectiveness of these algorithms.

8We also implemented a polymorphic analysis that re-analyzes a definition at each reference, but found its performance to be comparable to, and sometimes worse than, the copy analysis.

9 Future Work

All our constraint simplification algorithms preserve the observable behavior of constraint systems, and thus do not affect the accuracy of the analysis. If we were willing to tolerate a less accurate analysis, we could choose a compressed constraint system that does not preserve the observable behavior of the original, but only entails that behavior. This approach allows the use of much smaller constraint systems, and hence yields a faster analysis.

A promising approach for deriving such approximate constraint systems is to rely on a programmer-provided signature describing the behavior of each program component, and to derive the new constraint system from that signature. After checking the entailment condition to verify that signature-based constraints correctly approximates the behavior of the module, we could use those constraints in the remainder of the analysis. Since the signature-based constraints are smaller than the derived ones, this approach could significantly reduce analysis times for large projects. We are investigating this approach for developing a typed module language on top of Scheme.

References

[1] Aho, A., J. Hopcroft and J. Ullman. The Design and Analysis of Computer Algorithms. Addison-Wesley, Reading, Mass., 1974.

[2] Aiken, A., Wimmers, E. L., and Lakshman, T. K. Soft typing with conditional types. In Proceedings of the ACM Sigplan Conference on Principles of Programming Languages (1994), pp. 163–173.

[3] Cousot, P., and Cousot, R. Formal language, grammar, and set-constraint-based program analysis by abstract interpretation. In Proceedings of the 1995 Conference on Functional Programming and Computer Architecture (1995), pp. 170–181.

[4] Duesterwald, E., Gupta, R., and Soffa, M. L. Reducing the cost of data flow analysis by congruence partitioning. In International Conference on Compiler Construction (April 1994).

[5] Eifrig, J., Smith, S., and Trifonov, V. Sound polymorphic type inference for objects. In Conference on Object-Oriented Programming Systems, Languages, and Applications (1995).

[6] Fähndrich, M., and Aiken, A. Making set-constraint based program analyses scale. Technical Report UCB/CSD-96-917, University of California at Berkeley, 1996.

[7] Flanagan, C., and Felleisen, M. Set-based analysis for full Scheme and its use in soft-typing. Technical Report TR95-254, Rice University, 1995.

[8] Flanagan, C., and Felleisen, M. Modular and polymorphic set-based analysis: Theory and practice. Technical Report TR-96-266, Rice University, 1996.

[9] Flanagan, C., Flatt, M., Krishnamurthi, S., Weirich, S., and Felleisen, M. Finding bugs in the web of program invariants. In Proceedings of the ACM Conference on Programming Language Design and Implementation (1996), pp. 23–32.

[10] Flatt, M. MzScheme Reference Manual. Rice University.

[11] Heintze, N. Set-based analysis of ML programs. In Proceedings of the ACM Conference on Lisp and Functional Programming (1994), pp. 306–317.

[12] Hopcroft, J. E. An n log n algorithm for minimizing the states of a finite automaton. The Theory of Machines and Computations (1971), 189–196.

[13] Jagannathan, S., and Wright, A. K. Effective flow analysis for avoiding run-time checks. In Proc. 2nd International Static Analysis Symposium, LNCS 983 (September 1995), Springer-Verlag, pp. 207–224.

[14] Jones, N., and Muchnick, S. A flexible approach to interprocedural data flow analysis and programs with recursive data structures. In Conference Record of the Ninth Annual ACM Symposium on Principles of Programming Languages (January 1982), pp. 66–74.

[15] Palsberg, J. Closure analysis in constraint form. Transactions on Programming Languages and Systems 17, 1 (1995), 47–62.

[16] Palsberg, J., and O’Keefe, P. A type system equivalent to flow analysis. In Proceedings of the ACM SIGPLAN ’95 Conference on Principles of Programming Languages (1995), pp. 367–378.

[17] Pottier, F. Simplifying subtyping constraints. In Proceedings of the 1996 ACM SIGPLAN International Conference on Functional Programming (1996), pp. 122–133.

[18] Reynolds, J. Automatic computation of data set defintions. Information Processing’68 (1969), 456–461.

[19] Shivers, O. Control-flow Analysis of Higher-Order Languages, or Taming Lambda. PhD thesis, Carnegie-Mellon University, 1991.

[20] Tofte, M. Type inference for polymorphic references. Information and Computation 89, 1 (November 1990), 1–34.

[21] Trifonov, V., and Smith, S. Subtyping constrained types. In Third International Static Analysis Symposium (LNCS 1145) (1996), pp. 349–365.

[22] Wright, A., and Felleisen, M. A syntactic approach to type soundness. Information and Computation 115, 1 (1994), 38–94.

[23] Wright, A. K. Simple imperative polymorphism. Lisp and Symbolic Computation 8, 4 (Dec. 1995), 343–356.