Bounds Analysis by Abstract Interpretation^{∗}

Xiaolei Qian  Allen Goldberg
Computer Science Laboratory  Kestrel Institute

SRI International

qian@csl.sri.com  goldberg@kestrel.edu

Abstract

Abstract interpretation is a framework that precisely relates programs to their formal models. A model of a program retains its control structure but computes in a data domain that is less detailed, i.e. more abstract. Symbolically evaluating programs over the abstract domain yields analysis results that have been traditionally used by compilers for optimization.

This paper presents an abstract interpretation for a program language with settheoretic data structures that automatically and efficiently obtains bounds and containment data that may be used to help select efficient representations for these abstract types. In this work an abstract context, i.e. model, consists of a deductively-closed collection of formulas in a simple logical theory. The technique is easily extensible to other high-level data abstractions, and readily incorporable into compilers for very-high-level languages.

1 Introduction

We develop a program analysis technique that derives the symbolic containment and membership assertions of set-theoretic data abstractions automatically and effectively. Abstract interpretation[3] is applied to construct a deductive semantics of programs. Concrete contexts are abstracted into sets of simple facts about program points called bound assertions, and the abstract interpretation serves as a specialized theorem prover or fact gatherer[11] which computes global bounds information. In this application of abstract interpretation, the abstract domain is a deductively-closed decidable theory. i.e. an abstract model of the program. For a syntactic construct s and a bound assertion p, the abstract interpretation derives a post-condition of p over s[6]. Based on the abstract interpretation, we show to perform bounds analysis that are of interest to data structure selection. The importance of inclusion and membership relationships to automatic data structure selection in very-high-level languages was first recognized in [12] and developed in [4, 5]. Techniques similar to data flow analysis were developed there for setl, which start from an initial set of plausible relationships and iteratively eliminate those that might be false. Compared with the approach in [12], our approach does not require that all plausible inclusion and membership assertions be generated, and intra-function analysis is syntax-directed rather than iteratively approximated. Abstract interpretation was originally proposed in [2, 3] as a general framework for semantically correct program analysis. It has been applied to applicative languages to perform a variety of analysis tasks, such as strictness analysis in functional programs and mode analysis in logic programs[9]. An example of abstract interpretation applied to imperative languages is [1], where induction variables and recurrence relations in loops can be automatically recognized.

∗Supported in part by the U.S. Air Force Rome Laboratory under contract F30602-86-C-0026.

The paper is organized as follows. The syntax and semantics of our programming language are given in Sections 2 and 3. Section 4 defines abstract contexts and shows their correctness. Abstract interpretation is presented in Sections 5 and 6 together with their properties that are useful for bounds analysis. We discuss various types of bounds analysis in Section 7. Finally, Section 8 gives some concluding remarks.

2 Syntax

We define a simple programming language to illustrate the analysis method. The programming language has of three primitive datatypes: integer, symbol, and boolean; and five type constructors: pair, set, sequence, map, and (binary) relation. The grammar for the language is:

program

fn =^{def} function id(id: dl, …, id: dl) = st return e

declaration

dl =^{def} integer | symbol | boolean | pair(dl, dl) | set(dl) | sequence(dl) | map(dl, dl) | relation(dl, dl)

statement st =^{def} id ← exp

| id(exp) ← exp

| if exp then st else st

| (st; …; st)

| while exp do st

| enumerate id over exp do st | let (id = exp, …, id = exp) st

The expressions are formed by standard operators on the primitive types and the operators for composite types given in figure 1.

In this paper we restrict out attention to an intraprocedural analysis of a single function. In [10] the generalization of our analysis method to interprocedural analysis is given, as well as full proofs and a description of applications.

A program is represented by a directed graph ⟨ Node , Arc ⟩ whose nodes correspond to syntactic constructs defined in the grammar, and whose arcs denote to control flow. Arcs are specified by predecessor and successor relationships, which are mappings over nodes. Every statement is represented by a (hyper) node with exactly one incoming arc and one outgoing arc, as shown in Figure 2. The incoming node and outgoing nodes of a function, are called the entry and exit nodes respectively. The unique arc from the entry node is called the entry arc, and the unique node to the exit node the is called the exit arc.

For an if, test, or choice node n, its two successor nodes are denoted by succ_{t}(n) and succ_{f}(n) respectively. For a test or choice node n, its two predecessor nodes are denoted by pred_{i}(n) and pred_{l}(n) respectively. For an endif node, its two predecessor nodes are denoted by pred_{t}(n) and pred_{f}(n) respectively. For any other kind of node n, succ(n) and pred(n) denote its successor and predecessor nodes respectively.

As an example, the program in Figure 3 computes a topological sort from a partial order R over a set of symbols S. Succ is a map from an element of S to its direct successors in the partial order. A total order consistent with the partial order is accumulated in the sequence result. NumPred is a map that maps an element of S to the number of elements of S not yet inserted into the total order result. MinEls is the set of elements of S whose predecessors are elements of result. The directed graph representation of the program is shown in Figure 4.

Type  Expression  Remark
Pair  x.1  The first component of pair x
x.2  The second component of pair x
⟨x, y⟩  The pair consisting of x and y
Set { } Constant denoting the empty set
arb(x)  Select an arbitrary element of set x

(partial and nondeterministic)

x with y  Add element y to set x
x less y  Remove element y from set x
notempty(x)  Test if set x is not empty
x ∈ y  Set membership
x ⊆ y  Set inclusion
x ∪ y  Set union
x ∩ y  Set intersection
power(x)  Powerset of set x
{f(x): x ∈ y ∧ p(x)}  Set comprehension
Sequence [ ]  Constant denoting the empty sequence
first(x)  The first element of sequence x (partial)
append(x, y)  Append element y to the end of sequence x
range_{seq}(x)  The set of elements in sequence x
x ∈_{seq} y  Sequence membership
[f(x): x ∈_{seq} y ∧ p(x)]  Sequence comprehension
Map {||} Constant denoting the empty map
x(y)  Pointwise selection of map x at point y (partial)
x ∘ (y → z)  Pointwise assignment changing the value of map

x at point y to z

domain(x)  The set of elements in the domain of map x
range(x)  The set of elements in the range of map x
{|f(x) → g(x): x ∈ y ∧ p(x)|} Map comprehension
Relation domain_{rel}(x)  Projection of binary relation x onto its first

component

range_{rel}(x)  Projection of binary relation x onto its second

component

Figure 1: Operators on Composite Data Types

let let st st exp while/enumerate st st block st  return return st st exp condition endif entry edge exit edge function exit entry assign assign

Figure 2: Program Graphs

function TopSort(S: set(symbol), R: relation(symbol,symbol)) = s_{0} (let (result = [ ],

Succ = {| v → { }: v ∈ S |},

NumPred = {| v → 0: v ∈ S |})

s_{1} (enumerate z over R do s_{2} (let (x = z.1, y = z.2) s_{3} (Succ(x) ← Succ(x) with y; s_{4} NumPred(y) ← NumPred(y) + 1);)) s_{5} let (MinEls = { }) s_{6} (enumerate v over S do s_{7} if NumPred(v) = 0 then MinEls ← MinEls with v; s_{8} while ¬(MinEls = { }) do s_{9} let (a = arb(MinEls)) s_{10} (MinEls ← MinEls less a; s_{11} result ← append(result, a); s_{12} enumerate w over Succ(a) do s_{13} (NumPred(w) ← NumPred(w) − 1; s_{14} if NumPred(w) = 0 then MinEls ← MinEls with w)))) s_{15} return result

Figure 3: Topological Sorting Program

exit

6  8  9  12

1 0

10  11  13

7 2 5 entry

Figure 4: Graph Representation of Topological Sorting Program

3 Semantics

Following the Cousots [3], we define the semantic domain Value as the collection of values that program variables can take on; the semantic domain Id as the collection of program variables; the semantic domain Exp as the collection of expressions over the identifiers and operations; the semantic domain Environment as the mappings from Id to Value; and the semantic domain State as the collection of flow-graph arc and environment pairs, called states.

Value  =^{def} Integer + Boolean + Symbol + ⋯

Environment =^{def} Id→ Value

State  =^{def} Arc× Environment

The semantic domain for representing the set-theoretic types are the hereditarily finite sets [7]. The meaning of an expression in an environment is defined by the evaluation function val: Exp→ (Environment→ P(Value)). Since there is a non-deterministic operator arb, val maps an expression and an environment to a set of values. For expression e and environment r, the meaning of e in r is denoted by val[[e]]r. For most expressions, val is straightforward. For example

val[[S with x]]r = {S_{v} ∪ {x_{v}}|S_{v} ∈ val[[S]]r ∧ x_{v} ∈ val[[x]]r}

and

val[[arbS]]r = ⋃ val[[S]]r

.

The semantics of programs is defined using a state transition function next: State→ P(State), which maps a state to a collection of states. For arc ⟨m, n⟩ and environment r, next(⟨m, n⟩, r) is defined as follows.

• If n is an assignment node representing the statement v ← e, then the next state is in {⟨⟨n, succ(n)⟩, r ∘ (v → x)⟩|x ∈ val[[e]]r)}. If n is an assignment node representing the statement v(d) ← e, then the next state is in {⟨⟨n, succ(n)⟩, r ∘ (v → val[[v]]r ∘ (x → y))⟩|x ∈ val[[d]]r ∧ y ∈ val[[e]]r}.

• If n is an if node representing the statement if q then s_{1} else s_{2}, then the collection of possible next states contains ⟨⟨n, succ_{t}(n)⟩, r⟩ if true ∈ val[[q]]r and ⟨⟨n, succ_{f}(n)⟩, r⟩ if false ∈ val[[q]]r.

• If n is an endif node, then the next state is ⟨⟨n, succ(n)⟩, r⟩.

• If n is a let node representing the statement let (v_{1} = e_{1}, ⋯, v_{l} = e_{l}) s, then the next state is in {⟨⟨n, succ(n)⟩, r ∘ (v_{i} → x_{i})_{i=1}^{l}⟩| ⋀_{i=1}^{l} x_{i} ∈ val[[e_{i}]]r}.

• If n is an endlet node representing the statement let (v_{1} = e_{1}, ⋯, v_{l} = e_{l}) s, then the next state is ⟨⟨n, succ(n)⟩, {v → r(v)|v ∈ domain(r) ∧ v ∉ {v_{1}, …, v_{l}}}⟩.

• If n is a test node representing the statement while q do s, then the collection of possible next states contains ⟨⟨n, succ_{t}(n)⟩, r⟩ if true ∈ val[[q]]r and ⟨⟨n, succ_{f}(n)⟩, r⟩ if false ∈ val[[q]]r.

• The semantics of the statement enumerate v over S do s is equivalent to that of the let statement

let (S_{new} = S)
while ¬(S_{new} = { }) do
let (v = arb(S_{new}))
(s;
S_{new} ← S_{new} less v).

The static semantics of programs utilizes the notion of (concrete) contexts, which are collections of environments, i.e. Context=^{def} P(Environment). Boolean expression e is true in concrete context c if val[[e]]r = {true} for every environment r in c. Every arc is associated with a concrete context by the function cont: Arc→ Context.

An input environment for a function h is a mapping from h’s formal parameters to values. The concrete context c_{in} associated with the (unique) input arc entry consists of a collection of input environments. The concrete context associated with an arc a, cont(a), is defined as the collection of environments on a that can be obtained by applying the state transition function next a finite number of times to the input environment:

{r|(∃i ≥ 0)(∃r ∈ c_{in})(⟨a, r⟩ ∈ next^{i}(entry, r))}.

Finally, given an input environment r, the concrete semantics of a function function declared as function h(v_{1}: T_{1}, …, v_{l}: T_{l}) = st return e is {val[[e]]r′|r′ ∈ cont(exit)}.

4 Abstract Contexts

Abstract contexts are collections of atomic formulas over program variables of specific syntactic forms called bound assertions, that are closed under logical entailment.

4.1 Bound Assertions

The language of bound assertions is a restriction of the boolean expression available in the full programming language. There is one constant { }. The bound terms, are formed from constants and variables using the following operations form the programming language:

x, x(y), x.1, x.2, range_{seq}(x), domain(x), range(x), domain_{rel}(x), range_{rel}(x), power(x)

for terms x and y of appropriate types. The bound assertions are atomic formulas of the form

notempty(t), t_{1} = t_{2}, t_{1} ∈ t_{2}, t_{1} ⊆ t_{2}

for bound terms t, t_{1}, and t_{2} of appropriate types. We use S_{V} to denote a collection of bound assertions whose variables are exactly those in V.

The ∗-closure of a collection of bound assertions S_{V} over program variables V, denoted by S_{V}^{∗}, is the collection of bound assertions over V that are logically-entailed from S_{V}. S_{V} is consistent if bound assertion notempty({ }) is not in S_{V}^{∗}. For a program whose program variables are contained in the set V the abstract contexts are the sets S_{V}^{∗}.

4.2 Correctness

Suppose that g is a program with program variables V. An abstract interpretation of g consists of a lattice of abstract contexts, ordered by set inclusion with bottom { }, and an interpretation function. It is correct if it approximates the static semantics or concrete interpretation of g. According to the Cousots [3], this amounts to the construction of two functions α and γ such that (α, γ) forms an adjoined pair of functions: α ∘ γ = identity and γ ∘ α ⊒ identity. The abstraction function α maps concrete contexts to abstract contexts. For every concrete context c, α(c) is the collection of bound assertions over V that are true in every environment contained in c.

The concretization function γ maps abstract contexts to concrete contexts. For every abstract context c, γ(c) is the collection of environments in which every bound assertion in c is true.

Theorem 1 For abstract context c, α(γ(c)) = c. For concrete context c, c ⊆ γ(α(c)).

Proof Suppose that c is an abstract context. For every bound assertion p ∈ c and every environment r ∈ γ(c), we have that r ⊧ p. Hence p ∈ α(γ(c)).

Let p ∈ α(γ(c)). Then we have that for every model in which every formula of c is true, p is also true. Thus c ⊧ p. But since an abstract context is closed under entailment, p ∈ c.

Suppose that c is a concrete context. For every environment r ∈ c and every bound assertion p ∈ α(c), we have that r ⊧ p. Hence r ∈ γ(α(c)). □

5 Abstraction Functions

To perform abstract interpretation, we need abstraction functions that map set-theoretic expressions and boolean expressions in our programming language to logically related bound terms and bound assertions respectively. These abstraction functions can be viewed as abstract interpretations of the corresponding expressions.

5.1 Canonicalization

The first step is to transform set-theoretic expressions and boolean expressions into logically equivalent canonicalized forms that are closer in syntax to bound terms and bound assertions. The canonicalization is achieved by applying the boolean simplification rules in, for example,

[8] and the following transformation rules repeatedly until no rules are applicable:

range_{seq}([ ]) ⟹ { } domain({| |}) ⟹ { } range({| |}) ⟹ { } notempty({ }) ⟹ false notempty(t_{1} with t_{2}) ⟹ true notempty(t_{1} ∪ t_{2}) ⟹ notempty(t_{1}) ∨ notempty(t_{2}) ¬(t = { }) ⟹ notempty(t) t_{1} ∈ t_{2} ⟹ t_{1} ∈ range_{seq}(t_{2}) t_{2} has type seq(δ) arb(t_{1}) ∈ t_{2} ⟹ notempty(t_{1}) ∧ t_{1} ⊆ t_{2} p[y(x)] ⟹ x ∈ domain(y) ∧ p(y(x)) y has type map(δ, σ) t_{1} ∈ power(t_{2}) ⟹ t_{1} ⊆ t_{2} (t_{1} ∪ t_{2}) ⊆ t_{3} ⟹ (t_{1} ⊆ t_{3}) ∧ (t_{2} ⊆ t_{3}) t_{1} ⊆ (t_{2} ∩ t_{3}) ⟹ (t_{1} ⊆ t_{2}) ∧ (t_{1} ⊆ t_{3}) t_{1} ∈ (t_{2} with t_{3}) ⟹ (t_{1} ∈ t_{2}) ∨ (t_{1} = t_{3}) t_{1} ∈ (t_{2} less t_{3}) ⟹ (t_{1} ∈ t_{2}) ∧ ¬(t_{1} = t_{3}) (t_{1} with t_{2}) ⊆ t_{3} ⟹ (t_{1} ⊆ t_{3}) ∧ (t_{2} ∈ t_{3}) t_{1} ⊆ (t_{2} less t_{3}) ⟹ (t_{1} ⊆ t_{2}) ∧ ¬(t_{3} ∈ t_{1}) range_{seq}(append(t_{1}, t_{2})) ⟹ range_{seq}(t_{1}) with t_{2}

{v: v ∈ t}  ⟹ t  t has type set(δ)
{v: v ∈ t}  ⟹ range_{seq}(t)  t has type seq(δ)

[v: v ∈ t] ⟹ t domain(m ∘ (v → e)) ⟹ domain(m) with v range(m ∘ (v → e)) ⟹ (range(m) less m(v)) with e domain({|d → r: d ∈ t|}) ⟹ t t has type set(δ) domain({|d → r: d ∈ t|}) ⟹ range_{seq}(t) t has type seq(δ)

t_{1} = t_{2}  ⟹ t_{1} ⊆ t_{2} ∧ t_{2} ⊆ t_{1}  t_{1}, t_{2} are sets

Most transformation rules are straightforward except the ones that involve partial operators arbitrary selection, and pointwise selection. The rules generate the necessary applicability assertions, and preserve logical equivalence for defined terms.

5.2 Closure

Abstract context are collections of bound assertions closed under logical entailment. To generate closed sets we introduce a deductive system and show it complete. The +-closure of a collection of bound assertions S_{V} over program variables V, denoted by S_{V}^{+}, is the collection of bound assertions over V that are inferred from S_{V} by following rules of inference:

Tautolgy

\overline{\{ \} ⊆ x}  \overline{x ⊆ x}

Empty Set

\frac{x ∈ y}{notempty(y)}  \frac{notempty(x), x ⊆ y}{notempty(y)}

Subset

\frac{x ⊆ y, y ⊆ x}{x = y}  \frac{x = y}{x ⊆ y, y ⊆ x}  \frac{x ⊆ y, y ⊆ z}{x ⊆ z}

Power Set

\frac{x ⊆ y}{power(x) ⊆ power(y)}  \frac{power(x) ⊆ power(y)}{x ⊆ y}
\frac{x ⊆ y}{x ∈ power(y)}  \frac{x ∈ power(y)}{x ⊆ y}

Binary Relation

\frac{x ∈ y}{x.1 ∈ domain_{rel}(y)}  \frac{x ∈ y}{x.2 ∈ range_{rel}(y)}

Map Range

\frac{x ∈ domain(y)}{y(x) ∈ range(y)}  \frac{y(x) ∈ range(y)}{x ∈ domain(y)}

Equality

\frac{x = y, y = z}{x = z}  \frac{x = y}{f(x) = f(y)} f any function in the language

These rules are a specialized theorem proving system for bound assertions. For any given

finite collection of program variables, by restricting the use of the axiom \frac{x ⊆ y}{power(x) ⊆ power(y)}

in the obvious way, only a finite number of bound terms and hence bound assertions can be formed. Therefore, inference in this system always terminates. It is also easy to verify that our axiom system is sound. Theorem 2 shows that it is complete with respect to bound assertions.

Theorem 2 If S_{V} is consistent, then S_{V}^{+} = S_{V}^{∗}.

Proof (proof outline.) Suppose that there is a bound assertion p ∈ S_{V}^{∗} but p ∉ S_{V}^{+}. We construct a model of S_{V}^{+} in which p is false. This is a contradiction because (S_{V}^{+})^{∗} = S_{V}^{∗}. To construct the model we build a graph whose nodes are bound terms and whose edges denote membership or subset relations, insuring that any relationship that is provable is explicitly represented.

□

5.3 Bound Term Abstraction

We define two abstraction functions that map set-theoretic expressions to logically-related bound terms. A_{b}(t) maps a set-valued expression t to a collection of bound terms that are subsets of t, while A_{p}(t) maps a set-valued expression t to a collection of bound terms that are supersets of t. In other words, for every t_{1} ∈ A_{b}(t) and t_{2} ∈ A_{p}(t), t_{1} ⊆ t and t ⊆ t_{2} are valid. If t is a bound term, then A_{b}(t) = A_{p}(t) = {t}. If t is not a bound term and is not in one of the forms covered by the rules below, then the abstraction functions return empty. Otherwise they are computed by the following rules, where A_{w} and A_{s} are the bound-assertion abstraction functions to be defined in the next section:

A_{b}(t_{1} with t_{2})  =^{def} A_{b}(t_{1})
A_{b}(t_{1} ∪ t_{2})  =^{def} A_{b}(t_{1}) ∪ A_{b}(t_{2})
A_{b}(t_{1} ∩ t_{2})  =^{def} A_{b}(t_{1}) ∩ A_{b}(t_{2})
A_{b}({v: p})  =^{def} {x|{v ∈ x} ∈ A_{s}(p)}
A_{b}(range_{seq}([v: p]))  =^{def} {x|{v ∈ x} ∈ A_{s}(p)}

A_{b}(domain({|d → r: p|})) =^{def} {x|{d ∈ x} ∈ A_{s}(p)}

A_{b}(range({|d → r: p|})) =^{def} {x|{r ∈ x} ∈ A_{s}(p)}

A_{p}(t_{1} less t_{2})  =^{def} A_{p}(t_{1})
A_{p}(t_{1} − t_{2})  =^{def} A_{p}(t_{1})
A_{p}(t_{1} ∪ t_{2})  =^{def} A_{p}(t_{1}) ∩ A_{p}(t_{2})
A_{p}(t_{1} ∩ t_{2})  =^{def} A_{p}(t_{1}) ∪ A_{p}(t_{2})
A_{p}({v: p})  =^{def} {x|(v ∈ x) ∈ A_{w}^{+}(p)}
A_{p}(range_{seq}([v: p]))  =^{def} {x|(v ∈ x) ∈ A_{w}^{+}(p)}

A_{p}(domain({|d → r: p|})) =^{def} {x|(d ∈ x) ∈ A_{w}^{+}(p)}

A_{p}(range({|d → r: p|})) =^{def} {x|(r ∈ x) ∈ A_{w}^{+}(p)}

5.4 Bound Assertion Abstraction

We define two abstraction functions that map boolean expressions to logically related bound assertions. A_{w}(p) maps a boolean expression p to a collection of bound assertions that are logically weaker than p. In other words, for every q ∈ A_{w}(p), p → q is valid. Likewise, A_{s}(p) maps a boolean expression p to a collection of collections of bound assertions that are logically stronger than p. In other words, for every S ∈ A_{s}(p), ⋀_{q∈S} q → p is valid. If p is a bound assertion, then A_{w}(p) = {p} and A_{s}(p) = {{p}}. If p is not a bound assertion and is not in one of the forms covered by the rules below, then the abstraction functions return empty. Otherwise they are computed by the following rules, where A_{b} and A_{p} are the bound-term abstraction functions defined in the previous section:

A_{w}(p ∧ q)  =^{def} A_{w}(p) ∪ A_{w}(q)
A_{w}(p ∨ q)  =^{def} A_{w}(p) ∩ A_{w}(q)

A_{w}(notempty(t)) =^{def} {notempty(x)|x ∈ A_{p}(t)}

A_{w}(x_{1} ∈ t_{2})  =^{def} {x_{1} ∈ x_{2}|x_{2} ∈ A_{p}(t_{2})}  x_{1} is a bound term
A_{w}(t_{1} ⊆ t_{2})  =^{def} {x_{1} ⊆ x_{2}|x_{1} ∈ A_{b}(t_{1}) ∧ x_{2} ∈ A_{p}(t_{2})}

A_{w}(t_{1} = arb(t_{2})) =^{def} A_{w}(notempty(t_{2}) ∧ t_{1} ∈ t_{2}) A_{w}(t_{1} = first(t_{2})) =^{def} A_{w}(notempty(range_{seq}(t_{2})) ∧ t_{1} ∈ range_{seq}(t_{2})) A_{w}(t_{1} = t_{2}(t_{3})) =^{def} A_{w}(t_{3} ∈ domain(t_{2}) ∧ t_{1} ∈ range(t_{2})) t_{2} has type map(δ, σ) A_{w}(t_{1} = t_{2}) =^{def} A_{w}(range_{seq}(t_{1}) ⊆ range_{seq}(t_{2}))

∪A_{w}(range_{seq}(t_{2}) ⊆ range_{seq}(t_{1})) sequence equality

A_{w}(t_{1} = t_{2}) =^{def} A_{w}(domain(t_{1}) ⊆ domain(t_{2}))

∪A_{w}(domain(t_{2}) ⊆ domain(t_{1}))

∪A_{w}(range(t_{1}) ⊆ range(t_{2}))
∪A_{w}(range(t_{2}) ⊆ range(t_{1})) map equality
A_{s}(p ∧ q)  =^{def} {x_{1} ∪ x_{2}|x_{1} ∈ A_{s}(p) ∧ x_{2} ∈ A_{s}(q)}
A_{s}(p ∨ q)  =^{def} A_{s}(p) ∪ A_{s}(q)

A_{s}(notempty(t)) =^{def} {{notempty(x)}|x ∈ A_{b}(t)}

A_{s}(x_{1} ∈ t_{2})  =^{def} {{x_{1} ∈ x_{2}}|x_{2} ∈ A_{b}(t_{2})}  x_{1} is a bound term
A_{s}(t_{1} ⊆ t_{2})  =^{def} {{x_{1} ⊆ x_{2}}|x_{1} ∈ A_{p}(t_{1}) ∧ x_{2} ∈ A_{b}(t_{2})}

5.5 Example

As an example from the topsort program of Figure 3, A_{w} applied to the canonicalized boolean expression Succ = {|v → { }: v ∈ S|} is the union of A_{w} applied to the four boolean expressions below (after canonicalization):

domain(Succ) ⊆ S S ⊆ domain(Succ) range(Succ) ⊆ range({|v → { }: v ∈ S|}) range({|v → { }: v ∈ S|}) ⊆ range(Succ)

The first two expressions are already in the form of bound assertions. A_{w} applied to the third expression results in the bound assertion range(Succ) ⊆ power(S), because bound assertion { } ∈ power(S) is in A_{w}^{+}(v ∈ S). Finally, no bound assertion is abstracted by A_{w} from the last expression.

5.6 Correctness

Theorem 3 For every bound term t_{2} ∈ A_{b}(t_{1}), t_{2} ⊆ t_{1} is valid. For every bound term t_{2} ∈ A_{p}(t_{1}), t_{1} ⊆ t_{2} is valid. For every bound assertion q ∈ A_{w}(p), p → q is valid. For every collection of bound assertions S ∈ A_{s}(p), ⋀_{q∈S} q → p is valid.

Proof We prove by induction on the structure of set-theoretic and boolean expressions. For bound term t ∈ A_{b}(t_{1} ∪ t_{2}), we have that either t ∈ A_{b}(t_{1}) or t ∈ A_{b}(t_{2}) by definition. But t ⊆ t_{1} or t ⊆ t_{2} is valid according to induction hypothesis on A_{b}. Hence t ⊆ t_{1} ∪ t_{2} is valid. For bound term t ∈ A_{b}({v: p}), we have that {v ∈ t} ∈ A_{s}(p) by definition, and v ∈ t → p is valid by induction hypothesis on A_{s}. So {v: v ∈ t} ⊆ {v: p} and hence t ⊆ {v: p} are valid. Other cases for A_{b} and A_{p} are similar.

For bound assertion q ∈ A_{w}(t_{1} ⊆ t_{2}), q must be of the form x_{1} ⊆ x_{2} by definition. Furthermore, x_{1} ⊆ t_{1} and t_{2} ⊆ x_{2} are valid by induction hypothesis on A_{b} and A_{p}. It follows that t_{1} ⊆ t_{2} → q is valid. For q ∈ A_{w}(t_{1} = arb(t_{2})), q ∈ A_{w}(notempty(t_{2})) or q ∈ A_{w}(t_{1} ∈ t_{2}) by definition. By induction hypothesis on A_{w}, notempty(t_{2}) → q or t_{1} ∈ t_{2} → q is valid. In other words, notempty(t_{2}) ∧ t_{1} ∈ t_{2} → q is valid. Hence t_{1} = arb(t_{2}) → q is valid since t_{1} = arb(t_{2}) → notempty(t_{2}) ∧ t_{1} ∈ t_{2} is valid. Other cases for A_{w} are similar.

For collection of bound assertions S ∈ A_{s}(p ∧ q), there exists S_{1} and S_{2} such that S = S_{1} ∪ S_{2}, S_{1} ∈ A_{s}(p), and S_{2} ∈ A_{s}(q). By induction hypothesis on A_{s}, ⋀_{r∈S_{1}} r → p and ⋀_{r∈S_{2}} r → q are valid. Hence ⋀_{r∈S} r → (p ∧ q) is valid. Other cases for A_{s} are similar. □

6 Interpretation Function

The abstract interpretation ℑ maps an abstract context c and a arc ⟨m, n⟩ to another abstract context c′. Intuitively, if c is true before executing m, then c′ is true after executing m on the arc ⟨m, n⟩. In other words, ℑ computes post-conditions of bound assertions over syntactic constructs. If c′ = ∅, then the post-condition is true. If node n has only one outgoing arc, then ℑ(c, n) stands for ℑ(c, ⟨n, succ(n)⟩). If node n represents statement s, then ℑ(c, s) stands for ℑ(c, n). For notational convenience, ℑ(S, n) denotes ℑ(S^{+}, n) for set of bound assertions S, and ℑ(p, n) denotes ℑ({p}, n) for bound assertion p. For expression e, e[e′/v] denotes the expression identical to e except that occurrences of v in e are replaced by e′.

6.1 Non-Looping Constructs

The abstract interpretation of non-looping constructs is specified by the rules below. The interpretation of those syntactic constructs not listed is taken to be the identical mapping.

In the third and fourth rules, n denotes an if node with boolean expression q.

ℑ(c, v ← e)  =^{def} (S ∪ {p|p ∈ c ∧ (∃c′)(c′ ⊆ c ∧ c′ ∈ A_{s}(p[e/v]))})^{+}

S = { } if v occurs in e S = A_{w}(v = e) otherwise

ℑ(c, v(d) ← e) =^{def} (S ∪ {p|p ∈ c ∧ (∃c′)(c′ ⊆ c ∧ c′ ∈ A_{s}(p[v ∘ (d → e)/v]))})^{+}

S = { } if v occurs in d or e S = A_{w}(v(d) = e) otherwise

ℑ(c, ⟨n, succ_{t}(n)⟩)  =^{def} (c ∪ A_{w}(q))^{+}
ℑ(c, ⟨n, succ_{f}(n)⟩)  =^{def} (c ∪ A_{w}(¬q))^{+}

ℑ(c, let v_{1} = e_{1}, ⋯, v_{l} = e_{l}) =^{def} (c ∪ A_{w}(v_{1} = e_{1} ∧ ⋯ ∧ v_{l} = e_{l}))^{+}

ℑ(c, if q then s_{1} else s_{2})  =^{def} ℑ((c ∪ A_{w}(q))^{+}, s_{1}) ∩ ℑ((c ∪ A_{w}(¬q))^{+}, s_{2})
ℑ(c, (s_{1}; …; s_{l}))  =^{def} ℑ(ℑ(c, s_{1}), (s_{2}; …; s_{l}))

ℑ(c, let (v_{1} = e_{1}, ⋯, v_{l} = e_{l}) s) =^{def} {p|p ∈ ℑ((c ∪ A_{w}(v_{1} = e_{1} ∧ ⋯ ∧ v_{l} = e_{l}))^{+}, s)

∧p is free of v_{1}, …, v_{l}}

The interpretation for assignment statements needs further explanation. According to Hoare Logic [6], p is true after v ← e if p[e/v] is true before the assignment. Assuming that p is true before the assignment, then it is true after the assignment if p → p[e/v] is true before the assignment. Given an abstract context c that is true before v ← e and p ∈ c, p is true after the assignment if there exists c′ ⊆ c such that c′ ∈ A_{s}(p[e/v]).

6.2 Looping Constructs

The basic idea of the rules for looping constructs is as follows. The only way that a bound assertion could be propagated through a looping construct is when it is an invariant of the loop. Therefore the rules propagate exactly those bound assertions true on entry to the loop that are verifiably loop invariants.

To verify that an abstract context c is an invariant of a loop with loop body s, we need to show that if c is true before s then it is true after s. By the definition of abstract interpretation, it is sufficient to show that ℑ(c, s) logically implies c.

An invariant of while statement while q do s is an abstract context Inv such that Inv ⊆ ℑ((Inv ∪ A_{w}(q))^{+}, s). Invariants of enumerate statements can be defined similarly.

The rules for abstract interpretation can be stated as follows. Let n be the test node of while statement while q do s. For abstract context c, let Inv be the largest invariant of the statement such that Inv ⊆ c:

ℑ(c, ⟨n, succ_{t}(n)⟩) =^{def} (Inv ∪ A_{w}(q))^{+} ℑ(c, while q do s) =^{def} (Inv ∪ A_{w}(¬q))^{+}

The first rule for enumerate statements of the form enumerate v over S do s is the same if we replace q by v ∈ S. The second rule is specified as follows, since v should not be visible outside the statement:

ℑ(c, enumerate v over S do s) =^{def} Inv

6.3 Example

For the topsort program of Figure 3, we compute the interpretation of a collection P of bound assertions:

p_{1}: domain(Succ) = S

p_{2}: range(Succ) ⊆ power(S)

p_{3}: domain_{rel}(R) ⊆ S p_{4}: range_{rel}(R) ⊆ S

through the first enumerate statement s_{1}:

s_{1}: enumerate z over R do s_{2}: let (x = z.1, y = z.2) s_{3}: (Succ(x) ← Succ(x) with y; s_{4}: NumPred(y) ← NumPred(y) + 1);

In addition to the bound assertions in P, P′ = (P ∪ A_{w}(z ∈ R))^{+} contains bound assertions z.1 ∈ S, z.2 ∈ S, Succ(z.1) ⊆ S, etc. Assuming that n is the let node of s_{2}, we have that ℑ(P′, n) = (P′ ∪ {x = z.1, y = z.2})^{+}. Notice that

A_{s}(p_{1}[Succ ∘ (x → Succ(x) with y)/Succ]) = A_{s}(domain(Succ) with x ⊆ S ∧ S ⊆ domain(Succ) with x) = {{domain(Succ) ⊆ S, x ∈ S} ∪ {S ⊆ domain(Succ)}} = {{p_{1}, x ∈ S}}

A_{s}(p_{2}[Succ ∘ (x → Succ(x) with y)/Succ]) = A_{s}(range(Succ) less Succ(x) ⊆ power(S) ∧ Succ(x) ⊆ S ∧ y ∈ S) = {{range(Succ) ⊆ power(S)} ∪ {Succ(x) ⊆ S, y ∈ S}} = {{p_{2}, Succ(x) ⊆ S, y ∈ S}}

both of which contain subcollections of ℑ(P′, n). Furthermore, p_{3}, p_{4} are not affected by s_{3}. Hence P can be propagated through s_{3} and therefore s_{2}. In other words, P ⊆ ℑ(P′, s_{2}). In conclusion, all bound assertions in P are loop invariants of the enumerate statement s_{1} and can be propagated through it: ℑ(P, s_{1}) = P.

6.4 Correctness

Lemma 4 For abstract context c and arc a = ⟨m, n⟩, ℑ(c, a) is an abstract context.

Proof (proof outline.) ℑ has been defined so that it either explicitly closes the set using the inference procedure, or it follows inductively from the fact that c is. □

Theorem 5 For abstract context c and arc a = ⟨m, n⟩, if c is true before executing m, then abstract context ℑ(c, a) is true after executing m on arc a.

Proof We show by induction on the structure of m. Most rules for non-looping constructs are self-explanatory. For the first assignment rule and every p in ℑ(c, v ← e), if p ∈ A_{w}(v = e) then p is true after the assignment because v = e is. Otherwise there exists c′ ⊆ c true before the assignment such that c′ ∈ A_{s}(p[e/v]). Thus p[e/v] is true before the assignment according to Theorem 3, and hence p is true after the assignment.

For looping constructs, we show the case with while statement s of the form while q do s′. The case with enumerate statements is similar. Suppose that c is true before executing s, and Inv is the largest invariant of s such that Inv ⊆ c. If Inv and q are true before executing s′, then ℑ((Inv ∪ A_{w}(q))^{+}, s′) is true after executing s′ by induction hypothesis, and hence Inv is true after executing s′ since Inv ⊆ ℑ((Inv ∪ A_{w}(q))^{+}, s′). Therefore ℑ(c, s) = Inv is true after executing s since c is true before executing s and Inv ⊆ c. □

7 Bounds Analysis

Bounds Analysis is the process of determining bound assertions over program variables that are true throughout the lifetime of the program variables involved, i.e., in all environments in which these program variables are defined. We demonstrate the process of bounds analysis using our topsort program. First we propagate bound assertions to the abstract contexts associated with all program arcs. Assuming that the input abstract context consists of two bound assertions:

domain_{rel}(R) ⊆ S
range_{rel}(R) ⊆ S

After propagating through the let node of s_{0}, the abstract context contains in addition the following bound assertions:

range_{seq}(result) ⊆ S domain(Succ) = S range(Succ) ⊆ power(S) domain(NumPred) = S The above collection of bound assertions can be propagated to the abstract context at the outgoing arc of the first statement of s_{1}, as demonstrated in Section 6.3. After propagating them through the let node of s_{5}, a new bound assertion MinEls ⊆ S is obtained. Lets denote these bound assertions by P. Similar to Section 6.3 we can push P through the first statement of s_{6}. Notice that A_{w}(¬(MinEls = { })) = {notempty(MinEls)}. In order to push P through s_{8}, we have to compute ℑ((P ∪ {notempty(MinEls)})^{+}, s_{9}). After pushing P ∪ {notempty(MinEls)} through the let node of s_{9}, we get new bound assertions a ∈ MinEls, a ∈ S, etc. Only P′ = P ∪ {a ∈ S} can be pushed through the first statement of s_{10}, which can then be pushed through s_{11}.

Notice that A_{w}(w ∈ Succ(a)) = {a ∈ domain(Succ), w ∈ Succ(a)}, and w ∈ S is in the closure of P′ ∪ {a ∈ domain(Succ), w ∈ Succ(a)}. Similar to Section 6.4, we can push P′ through s_{13}, hence ℑ(P′, s_{12}) = P′. Finally, P can be pushed through s_{9}, therefore ℑ(P, s_{8}) = P. All bound assertions in P not mentioning MinEls reach the outgoing arc of s_{5}, and hence the outgoing arc of the function. The abstract contexts associated with other arcs can be computed in the similar way.

From the abstract interpretation, we conclude that S is a containment bound for MinEls, a domain bound and an access bound for Succ and NumPred, and a range bound for result. In addition, power(S) is a range bound for Succ.

An efficient implementation of topsort requires that access to the maps NumPred and Succ take constant time. This can be achieved by a data structure in which each element of S is a heap-allocated record containing fields that hold the corresponding range values of NumPred, and Succ. Elements of S appearing in MinEls, range(Succ), R, and result are represented by a pointers to the record. This representation requires the assertions developed by our analysis.

8 Conclusion

Bounds analysis, which is the process of determining symbolic bounds on program variables that are true throughout their lifetime, is central to the successful compilation of programs in very-high-level languages into efficient low-level implementation. We developed a technique for the automatic analysis of bounds information for several important set-theoretic data abstractions. Abstract interpretation is applied to associate a collection of bound assertions with every program point, based on which a variety of bounds analysis can be performed that are of interest to data structure selection. The abstract interpretation is kept computationally tractable by restricting ourselves to reasoning with bound assertions. Compared with the approach in [12], our approach does not require that all plausible inclusion and membership assertions be generated, and intra-function analysis is syntax-directed rather than iteratively approximated. The technique is easily extensible to other high-level data abstractions, and readily incorporable into compilers for very-high-level languages.

Acknowledgment

We thank Lee Blaine for our collaboration on the DTRE program transformation system, which has been a source of inspiration for the ideas presented here.

References

[1] Ammarguellat, Z., Harrison III, W., “Automatic Recognition of Induction Variables and Recurrence Relations by Abstract Interpretation”; Proceedings of the ACM SIG-PLAN’90 Conference on Programming Language Design and Implementation, June 1990, 283-295.

[2] Cousot, P., “Semantic Foundations of Program Analysis”; Program Flow Analysis: Theory and Applications, S.S. Muchnick and N.D. Jones (editors), Prentice-Hall, 1981, 303-342.

[3] Cousot, P., Cousot, R., “Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction of Approximations of Fixpoints”; Proceedings of the Fourth ACM Symposium on Principles of Programming Languages, January 1977, 238-252.

[4] Goldberg, A., Kotik, G., “Knowledge-Based Programming: An Overview of Data Structure Selection and Control Structure Refinement”; Technical Report KES.U.83.7, Kestrel Institute, November 1983.

[5] Goldberg, A., Smith, D., “Towards a Performance Estimation Assistant”; Technical Report KES.U.86.10, Kestrel Institute, November 1986.

[6] Hoare, C., “An Axiomatic Basis for Computer Programming”; Communications of the ACM 12:10, 1969, 576-583.

[7] Krivine, J. Introduction to Axiomatic Set Theory, Reidel Publishing Co., Holland, 1971.

[8] Manna, Z., Waldinger, R., The Logical Basis for Computer Programming, Vol.2: Deductive Systems, Addison-Wesley, 1990.

[9] Abramsky, S., Hankin, C. (editors), Abstract Interpretation of Declarative Languages, Ellis Horwood Limited, 1987.

[10] Qian, X., Goldberg, A., “Bounds Analysis by Abstract Interpretation,” Kestrel Institute Report, 1994.

[11] Schwartz, J., “Optimization of Very High Level Languages—I: Value Transmission and Its Corollaries”; Computer Languages 1, 1975, 161-194.

[12] Schwartz, J., “Optimization of Very High Level Languages—II: Deducing Relationships of Inclusion and Membership”; Computer Languages 1, 1975, 197-218.