What is the project closure analysis?

Answer 1

Closure analysis determines statically which function de¯nitions reach which program

points. This information is used for many di®erent purposes; e.g., type inference for

object-oriented programming languages [PS91], globalization analysis of functional pro-

grams [Ses89], partial evaluation [Bon90], type recovery in Scheme [Shi90], and others.

The reason why closure analysis is such a fundamental analysis in di®erent applications is

that it is (sort of) the universal data °ow analysis problem for monomorphic (data °ow

oriented) analyses for higher-order (functional) languages. As such it may be viewed as

the analogue of path analysis, which is universal for (continuous) ¯rst-order (classical)

data °ow analysis problems [Tar81].

General closure analysis is, unlike its ¯rst-order counterpart, expensive in the worst

case: the best known algorithms take time £(n3) in the worst case [Hen91a,PS92]. Many

times it is su±cient, however, to get somewhat coarser information than the exact closure

information. Coarser here means that the results may indicate that more function def-

initions reach a point than a precise closure analysis would really yield; nonetheless the

information should in practice be only marginally di®erent from the exact analysis.

In this note we exhibit a simple, but very e±cient closure analysis based on the binding-

time analysis of [Gom90] and the algorithm [Hen91b] for it. (In fact the algorithm here

is substantially simpler than the one in [Hen91b].) The computed abstract value °ow

information1 is coarser than normal closure analysis exactly in the following sense: exact

closure analysis keeps track of uni-directional °ow of (abstract) values from one program

point to another whereas our simple closure analysis works with the assumption that °ows

are reversible; that is, that any abstract value that °ows from point p to point p0 can also

°ow (backwards!) from p0 to p.

In the practice of partial evaluation this loss of information appears to be insubstantial.

Since the simple closure analysis algorithm runs in almost-linear time [Hen91b] and is very

¤DIKU Semantics Report D-193

1We prefer to call the abstractions of values corresponding to expressions in a program abstract values

rather than (abstract) closures, since these values represent values other than (run-time) closures, including

pairs, integers, etc.

1

2 BASIC IDEA OF SIMPLE CLOSURE ANALYSIS2

e±cient in practice [Hen91c] this appears to be an attractive alternative to computing

complete closure information.

2 Basic idea of simple closure analysis

In the binding-time analysis of [Gom89], on which [Hen91b] is based, we begin by asso-

ciating a unique abstract value (also called a token, label or a type variable depending on

the intention of their use) with every (sub)expression in a program, and constraints are

extracted that capture the °ow of actual values represented by these abstract values in the

program. The °ow is, of course, a conservative approximation of the actual °ow of data.

It not only makes the standard assumptions that all expressions inside a function de¯ni-

tion are actually evaluated and that abstract values can °ow forwards and backwards, as

mentioned above, but also that the °ows of di®erent arguments of a function merge inside

the function | the latter is why we refer to this analysis as monomorphic.

In the second step, the critical one, these constraints are normalized by a (very small)

set of rewriting rules. In the process di®erent abstract values may be identi¯ed, which is

tantamount to saying that one abstract value could \°ow" to the other, in any direction.

At the end of this process a single abstract value represents a whole set of abstract values

that have been identi¯ed during normalization. Such a set may contain (abstract values

labeling) closures as well as other program points, notably application points such as the

actual parameters of function applications. This information can be interpreted by saying

that the closures in the set may reach any of the application points in the same set. The

analysis is conservative w.r.t. to exact closure analysis in the sense that no other closures

reach the application points, but that some of the reported closures may actually be shown

not to reach some application point in the same set by exact closure analysis. (Of course,

\exact" closure analysis is itself a conservative approximation of the actual dynamic °ow

of run-time values, including concrete closures.)

3 Simple closure analysis exempli¯ed

In this section we exemplify the steps above by considering a simple example.

Consider the following code (fragment), representing Turner's tautology checker and

two calls to it:

taut = fn f => fn n. if n = 0 then f else taut (f true) (n-1) and taut (f false) (n-1)

g = fn x => fn y => (x and not y) or (not x or y)

h = fn z => z

taut g 2 taut h 1

3.1 Constraint extraction

In the ¯rst step we associate a distinct abstract value with every occurrence of a subex-

pression occurring in this code; for simplicity's sake all occurrences of a variable have

the same abstract value. We shall refer to the abstract value of an (occurrence of an)

expression by the special variable ® indexed by the expression; e.g., the abstract values

of the three function de¯nitions are ®taut; ®g and ®h. On top of these abstract values

representing (abstract) closures we have the abstract values ®¸f and ®¸n corresponding to

3 SIMPLE CLOSURE ANALYSIS EXEMPLIFIED 3

the partial applications of taut to one, resp. two arguments. Finally, we have ®¸y corre-

sponding to the partial application of g to one argument. These are all the abstract values

representing (abstract) closures; of course, as mentioned before, every subexpression has

a corresponding (unique) abstract value.

In the constraint extraction phase of the binding-time analysis algorithm the con-

straints in Figure 1 are generated for the code above. Two kinds of constraints are gener-

ated.

² ® = ®0: Such an equation between abstract values expresses that one °ows to the

other, and vice versa (Remember our basic assumption of bidirectionality of °ow!);

e.g., ® could be the abstract value of an actual argument to a function, and ®0 the

abstract value of the function's corresponding formal parameter.

² ® ! ®0 · ®00 or integer · ®00, etc.: An inequation has an abstract value constructor

applied to n ¸ 0 abstract values on the left-hand side and an abstract value on the

right; such an inequality expresses that the right-hand side abstract value \can be"

the abstract value on the left (there may be more than one, but not with the same

constructor; see below).

3.2 Constraint normalization

In the constraint normalization phase we combine de¯nitional information (constraints of

the second form above) and form equivalence classes of abstract values (for the constraints

of the ¯rst form).

For simple closure analysis we need only 2 of the 11 rewriting rules in [Hen91b]. In

particular, there is no need for an occurs check rule since we don't have to interpret the

result as ¯nite type expressions; and there is no need for a special type Dynamic (or ¤)

representing either possible type errors or run-time computable expressions or both, since

we are interested neither in the former nor in the latter. In particular, the rewriting rules

manipulating Dynamic can be omitted. We end up with the rewriting rules in Figure 2.

As proved in [Hen91b] a rewriting system normalizing constraints with additional

rewriting rules can be implemented in time O(n®(n; n) where ®(n; n) < 5 for any value of

n smaller than the number of atoms in the universe. It is quite easy to see that this more

rudimentary rewriting system can be implemented in the same time. In fact, a slightly

modi¯ed uni¯cation closure algorithm will do the job.

3.3 Interpretation as closure sets

The normalization of the constraints results in a transition C ) C0 labeled with a sub-

stitution S. For closure analysis it is this substitution we are interested, not the normal

form constraints left over. Since the substitution maps abstract values to abstract values

the pre-images of every abstract value in its range form a partition of the original abstract

values in the program. For our example these sets are displayed in Figure 3.

Looking at the set Ef we can see that simple closure analysis reports that the functions

f; g, all their partial applications, and the abstract values corresponding to their bodies

may reach the formal parameter f of taut. In this case this happens to be precisely correct,

but in general there will be some overreporting of one abstract value reaching (the point

of) another.

3 SIMPLE CLOSURE ANALYSIS EXEMPLIFIED 4

®f ! ®¸n · ®taut

®n ! ®if · ®¸n

®f = ®if

®and = ®if

integer · ®n

integer · ®0

bool · ®n=0

integer · ®1

integer · ®n

integer · ®n¡1

bool · ®true

®true ! ®ftrue · ®f

®ftrue ! ®taut(ftrue) · ®taut

®n¡1 ! ®taut(ftrue)(n¡1) · ®taut(ftrue)

bool · ®false

®false ! ®ffalse · ®f

®ffalse ! ®taut(ffalse) · ®taut

®n¡1 ! ®taut(ffalse)(n¡1) · ®taut(ffalse)

bool · ®t(ftrue)(n¡1)

bool · ®t(ffalse)(n¡1)

bool · ®and

®x ! ®¸y · ®g

®y ! ®or · ®¸y

bool · ®or

. . .

®z ! ®z · ®h

integer · ®2

®g ! ®tautg · ®taut

®2 ! ®tautg2 · ®tautg

integer · ®01

®h ! ®tauth · ®taut

®01 ! ®tauth1 · ®tauth

Figure 1: Abstract value constraints for Turner's tautology checker

4 DAMAS-MILNER POLYMORPHISM 5

C [ f® ! ®0 · °; ¯ ! ¯0 · °g

)C

[ f® ! ®0 · °; ® = ¯; ®0 = ¯0g

C [ f® = ®0g S)

S (C)

where S = f® 7! ®0g

Figure 2: Constraint rewritings for simple closure analysis

Etaut = f®tautg

Ef = f®f ; ®g; ®h; ®if ; ®and; ®taut(ftrue)(n¡1); ®taut(ffalse)(n¡1);

®ftrue; ®ffalse; ®lambday; ®or; ®zg

E¸n = f®¸n; ®taut(f true); ®taut(ffalse)g

En = f®n; ®n¡1g

Figure 3: Equivalence classes of abstract values for Turner's tautology checker

4 Damas-Milner polymorphism

Simple closure analysis is easily and naturally extended to a polymorphic analysis since the

normalized constraints of an expression can be interpreted as an \abstract value scheme":

e.g, the normalized constraints of ¸x:xx are f® ! ¯ · ®; ® ! ¯ · °g where ° is

the abstract value of the whole expression. This then corresponds to the polymorphic

\type scheme" 8®¯° : ® ! ¯ · ®; ® ! ¯ · °:°. Such an abstract value scheme can

be instantiated by substituting new abstract values for the scheme variables at every

occurrence of the identi¯er let-bound to ¸x:xx.

5 Milner-Mycroft polymorphism

ML-style polymorphic (also called polyvariant) simple closure analysis as above does not

¯nd abstract value schemes for mutually recursive de¯nitions. One approach is to topsort

the strong components of a mutually recursive de¯nition and treat them as a nonrecur-

sive serious of groups of genuinely mutually recursive de¯nitions. The groups themselves

are analyzed by a monomorphic closure analysis. This solution has well-known disad-

vantages, especially in a setting where closure information has to be relayed back to a

user/programmer or where attributes of code generated from such analyses has to satisfy

certain robustness criteria, such as: if the de¯nition of function f is changed, and this has

nothing to do with the de¯nitions of functions g and h, then after these changes the code

for g and h should not be negatively a®ected.