Equality-based flow analysis versus recursive types.
Equality-based control-flow analysis has been studied by Henglein, Bondorf and Jrgensen, DeFouw, Grove, and Chambers, and others. It is faster than the subset-based-0-CFA, but also more approximate. Heintze asserted in 1995 that a program can be safety checked with an equality-based control-flow analysis if and only if it can be typed with recursive types. In this article we falsify Heintze's assertion, and we present a type system equivalent to equality-based control-flow analysis. The new type system contains both recursive types and an unusual notion of subtyping. We have s  t if s and t unfold to the same regular tree, and we have &bottom;t&top;    where t is a function type. In particular, there is no nontrivial subtyping between function types.
Introduction
Control-flow analysis is done to determine approximate sets of functions that may be called
from the call sites in a program. In this paper we address an instance of the question:
Question: How does flow analysis relate to type systems?
Our focus is on:
1. equality-based control-flow analysis which has been studied by Henglein [9], Bondorf
and J-rgensen [3], DeFouw, Grove, and Chambers [5], and others, and
2. recursive types which, for example, are present in a restricted form in Java [6], in the
form of recursive interfaces where equality and subtyping is based on names rather
than structure.
Equality-based control-flow analysis is a simplification of subset-based control-flow analysis
[16, 11, 8]. We will use the abbreviations:
subset-based control-flow analysis, and
equality-based control-flow analysis.
0-CFA' is also known as, simply, 0-CFA. We can illustrate the difference between 0-CFA'
and 0-CFA= by considering how they analyze a call site e 1 e 2 in a functional program.
Suppose -x:e is a function in that program. We want a flow analysis to express that:
if -x:e becomes the result of evaluating e 1 , then flow relations are established
between the actual argument e 2 and the formal argument x, and 2) between
the body e and the call site e 1 e 2 .
With a subset-based analysis, the flow relations are subset inclusions. This models that
values flow from the actual argument to the formal argument, and from the body of the
function back to the call site. With an equality-based analysis, the flow relations are
equations. Thus, the flow information for the actual and formal argument are forced to be
the same, and the flow information for the body and the call site are also forced to be the
same. Intuitively, the equations establish a bidirectional flow of information.
0-CFA= is more approximate than 0-CFA' . Both have been implemented many times
for various purposes. In general, for functional and object-oriented languages, 0-CFA'
can be executed in cubic time. For programs with finite types, 0-CFA' can be executed
in quadratic time [8], and specific flow-oriented questions such as "identify all functions
called from only one call site" can be answered in linear time [8]. For comparison, 0-
CFA= can always be executed in almost-linear time [9]. Which one of 0-CFA' and 0-
CFA= is the better choice in practice? For a language like ML [10] where functions have
finite polymorphic types and data may have recursive types, experiments by Heintze and
McAllester [8] indicate that it is a good choice to use 0-CFA' . They implemented a variant
of the quadratic-time algorithm for 0-CFA' which treated data in a much simplified way.
For the problem of pointer analysis, there are algorithms which are close cousins of 0-CFA'
and 0-CFA= [17]. For this problem, the condition of finite types does not hold in general.
Shapiro and Horwitz [15] presented an experimental comparison of the two algorithms,
and it confirms the theoretical conclusion that 0-CFA= is faster and more approximate
than 0-CFA' . For an object-oriented language like Java, the condition of finite types
is seldomly satisfied because of, for example, binary methods [4]. DeFouw, Grove, and
Chambers [5] experimentally compared a family of flow-analysis algorithms whose time
complexities are at most cubic time. Both 0-CFA= and some of its variants do well in
that comparison. Ashley [2] has also presented a flow analysis with time complexity less
than cubic time. It remains open how it relates to 0-CFA= . Bondorf and J-rgensen [3]
implemented both 0-CFA' and 0-CFA= for Scheme as part of the partial evaluator Similix.
For Scheme, the condition of finite types does not hold in general. They concluded that
the two analyses have comparable precision for their application, and that 0-CFA= is much
faster. In summary, 0-CFA= has in experiments proved to be a preferable alternative to
0-CFA' for many applications.
Flow analyses such as 0-CFA can be formulated using constraints, see for example
[11, 14]. This approach proceeds in two steps: 1) derive flow constraints from the program
text, and 2) compute the least solution of the constraints. The least solution is the desired
flow information. The precision of the analysis stems from the choice of constraints. For
example, one choice leads to 0-CFA' , and another choice leads to 0-CFA= . The kind of
flow constraints used in, for example, the paper [11] always admits a least solution.
We can turn a flow analysis into a predicate which accepts and rejects programs, by
extending it with safety constraints. For example, for a call site e 1 e 2 in a functional
program, a safety constraint might express: "does the flow information for e 1 denote only
Safety constraints do not always have a solution. They can be derived from
the program text, just like flow constraints. This means that we can do a flow-based safety
analysis of a program in two steps: 1) derive flow and safety constraints from the program
text, and 2) decide if the constraints are satisfiable. Such a safety analysis performs a task
akin to type inference, in the sense that "safe" is like "typable."
Palsberg and O'Keefe [12] showed that a program can be safety checked with 0-CFA'
if and only if it can be typed in Amadio and Cardelli's type system with subtyping and
recursive types [1]. The proof of this connection makes explicit the close relationship
between flow and subtyping.
Heintze asserted in 1995 [7] that a program can be safety checked with 0-CFA= if and
only if it can be typed with recursive types. This assertion is reasonable because it says
that, intuitively, if we replace subset inclusions by equalities, then the need for subtyping
disappears. Heintze's assertion is also consistent with the observation that both 0-CFA=
and type inference with recursive types can be executed in almost-linear time. Perhaps
surprisingly, Heintze's assertion is false. For example, consider the -term:
The variable f is applied to both the number 0 and the function -x:x. Thus, the -term
does not have a type in a type system with recursive types but no subtyping. Still, a
-based safety analysis accepts this program, by assigning both f and g the empty
flow set, see Section 2 for details.
For another example, consider the -term:
It reminds a bit of the previous example, but now f is applied to (-a:0) and (-b:-x:x).
Again, the -term e 2 does not have a type in a type system with recursive types but no
subtyping. For conservative flow analysis cannot assign the empty flow set to f
because that flow set should at least contain (-y:0). Still, a 0-CFA= -based safety analysis
accepts this program, by assigning y a flow set which contains both (-a:0) and (-b:-x:x).
Given that Heintze's assertion is false, we are left with two questions:
1. which type system corresponds to 0-CFA= ?, and
2. which control-flow analysis corresponds to recursive types?
Palsberg and O'Keefe's result [12] implies that E 1 and E 2 can be typed if we have both
recursive types and Amadio/Cardelli subtyping. Their result also seem to indicate that
adding both recursive types and all of the Amadio/Cardelli subtyping to match 0-CFA=
would be overkill. Thus, to answer the first question, it makes sense to ask: how much
subtyping is necessary and sufficient to match 0-CFA= ? To answer the second question we
must ask: what restrictions on 0-CFA= must we impose to match recursive types?
In this paper we answer the first question and we give a partial answer to the second
question. We show that a program can be safety checked with 0-CFA= if and only if it can
be typed with recursive types and an unusual restriction of Amadio/Cardelli subtyping.
We have s - t if s and t unfold to the same regular tree, and we have
is a function type. In particular, there is no non-trivial subtyping between function types.
To see why non-trivial subtyping between function types is not required to match 0-CFA= ,
consider the program (-x:e)e 0 . Let hxi be a flow variable for the binding occurrence of x,
and let [[(-x:e)e 0 ]], [[-x:e]], flow variables for the occurrences (-x:e)e 0 , -x:e, e,
e 0 , respectively. If ' is a map from flow variables to flow sets, which satisfies the 0-CFA=
constraints, then in particular it satisfies
We can also use hxi, variables, and for a type system
such as simple types where there is no non-trivial subtyping between function types, we
get, among others, the following constraints on type correctness:
Unification gives that a typing must satisfy the constraints:
Thus, we get the same form of relationships between the types as there are between the
flow sets. If we allow non-trivial subtyping between function types, then the constraints
on type correctness become [12]:
In particular, this opens the possibility for a non-trivial relationship:
and hence
These constraints are closely related to the flow constraints used in 0-CFA' [12].
We also show that if a program can be safety checked with a certain restriction of
0-CFA= , then it can be typed with recursive types. Our restriction of 0-CFA= is that all
flow sets must be nonempty and consistent. Consistency means that if two functions -x:e
and -y:e 0 occur in the same flow set, then the flow sets for x and y are equal, and also the
flow sets for e and e 0 are equal.
In slogan-form, our results read:
tiny drop of subtyping.
Recursive types '
The key to understanding the second result is that both empty flow sets and flow sets
with two or more inconsistent functions have no counterparts in a type system with just
recursive types. The restricted version of 0-CFA= does not fully match recursive types,
because a program may have a type for which no flow set exists.
In the next section, we present Heintze's definition of 0-CFA= , in Section 3 we present
the new type system, and in Section 4 and 5 we prove our results. Our example language
is a -calculus, defined by the grammar:
where succ denotes the successor function on integers.
Equality-Based Control-Flow Analysis
Given a -term P , assume that P has been ff-converted such that all bound variables are
distinct and different from the free variables. Let Var(P ) be the set of -bound variables
in P . Let X P be the set of variables consisting of one variable hxi for each x 2 Var(P ). Let
Y P be a set of variables disjoint from X P consisting of one variable each occurrence
of a subterm e of P . (The notation ambiguous because there may be more than one
occurrence of e in P . However, it will always be clear from context which occurrence is
meant.) The set Abs(P ) is the set of occurrences of subterms -x:e of P . The set CL(P ) is
Flow-based safety analysis of a -term P can be phrased in
terms of a constraint system over the variables range over CL(P
ffl For every occurrence in P of a subterm of the form 0, the constraint
ffl for every occurrence in P of a subterm of the form succ e, the two constraints
ffl for every occurrence in P of a subterm of the form -x:e, the constraint
ffl for every occurrence in P of a subterm of the form e 1 e 2 , the constraint
ffl for every occurrence in P of a -variable x, the constraint
ffl for every occurrence in P of a subterm of the form -x:e, and for every occurrence in
P of a subterm of the form e 1 e 2 , the constraints
The last two constraints create a connection between a call site e 1 e 2 and a potential callee
-x:e. Notice that two of the constraints are not equalities, but subset inclusions. This is
the key reason why subtyping is needed to match this safety analysis.
This constraint system mixes flow constraints and safety constraints. The safety constraints
are:
ffl for succ e: [[succ
ffl for e 1
and the rest are flow constraints. Notice that because Int and functions cannot occur in
the same flow set we have that a constraint such as has the same effect as
fIntg.
Denote by C(P ) the system of constraint generated from P in this fashion. Let Cmap(P )
be the set of total functions from
all constraints in C(P ). We say that P is 0-CFA= safe if C(P ) is
For example, consider again
where we have labeled the two occurrences of f as f 1 and f 2 , for notational convenience.
We have:
The constraint system C(E 1 ) has the point-wise '-least solution
Next, consider again:
where we have labeled the occurrences of f as f 1 and f 2 , for notational convenience. The
constraint system C(E 2 ) has the point-wise '-least solution
etc.
3 The Type System
We use v to range over type variables drawn from a countably infinite set Tv. Types are
defined by the grammar:
with the restriction that a type is not allowed to contain anything of the form
We identify types with their infinite unfoldings under the rule:
Such infinite unfolding eliminates all uses of - in types. It follows that types are a class of
regular trees over the alphabet
There is a subtype relation - on types:
It is straightforward to show that - is a partial order. Notice that ? is a lower bound and
? is an upper bound for only the function types but not Int. A more suggestive notation
might be ?! for ?, and ?! for ?.
A type environment is a partial function with finite domain which maps -variables to
types. We use A to range over type environments. We use the notation A[x : t] to denote
an environment which maps x to t, and maps y, where y 6= x, to A(y). A type judgment
has the form A ' e : t, and it means that in the type environment A, the expression e has
type t. Formally, this holds when it is derivable using the rules below.
Notice that there is no subsumption rule; instead subtyping can only be used in a
restricted way in rules 2 and 3. We say that e is RS-typable if A ' e : t is derivable
for some A; t. (RS stands for "restricted subtyping.") The type system has the subject
reduction property, that is, if A ' e : t is derivable, and e beta-reduces to e 0 , then A ' e
is derivable. This can be proved by straightforward induction on the structure of the
derivation of A ' e : t.
Here follow type derivations for the two -terms Section 1. The first type
derivation uses the abbreviation:
Notice the four uses of subtyping. Notice also that the only possible type for f is ?.
The second derivation uses the abbreviation: A
Notice that the only possible common type for both (-a:0) and (-b:-x:x) is ?.
The reason why there is no subsumption rule of the form
is that we want to disallow the use of subsumption immediately after a use of the rule for
variables. If we add a subsumption rule, then more -terms become typable. For example,
consider:
If we have a subsumption rule, then we can give -y:y the type ? ! ?, we can give both
-x:0 and the last occurrence of f the type ?, and it is then straightforward to complete
a type derivation for E 3 . Notice that the fragment of the type derivation for the last
occurrence of f is of the form:
Without a subsumption rule, this type derivation is not possible. Indeed, no type derivation
using rules (1)-(5) is possible. To see that, let s 1 be the type of -y:y, let s 2 be the type of
f . From -y:y we have is the type of x. Moreover, from (ff) we have
where u is the type of (ff ). We have
hence ff). Consider now
(f(-x:0)). The type of -x:0 is of the form s or ?. In both cases, it cannot be an
argument of a function of type -ff:(ff ! ff). We conclude that E 3 is not RS-typable.
4 The Equivalence Result
Theorem 4.1 A -term P is 0-CFA= safe if and only if P is RS-typable.
We prove this theorem in two steps. Lemma 4.3 shows that if P is 0-CFA= safe, then
P is RS-typable. To prove that lemma we use the technique from [13]. Lemma 4.4 shows
that if P is RS-typable, then P is 0-CFA= safe. To prove that lemma we use a technique
which is more direct than the one used to show a similar result, for 0-CFA' , in [12].
From Flows to Types
First we consider the mapping of flows to types. Given a program P , a map ' 2 Cmap(P ),
and S ' Abs(P ), we say that S is '-consistent if for all -x 1
Given a program P and ' 2 Cmap(P ), define
the equation system \Gamma(P; '):
ffl For each S 2 range('), let v S be a type variable, and
contains the equation
contains the equation
there are two cases: either S is '-
consistent and then \Gamma(P; ') contains the equation
otherwise \Gamma(P; ') contains the equation
Every equation system \Gamma(P; ') has a unique solution. To see this, notice that for every
type variable, there is exactly one equation with that variable as left-hand side. Thus,
intuitively, we obtain the solution by using each equation as an unfolding rule, possibly
infinitely often.
Lemma 4.2 If ' 2 Cmap(P is the unique solution of
Proof. Support first that '(w 1
Suppose then that '(w 1 ) is '-inconsistent. From '(w 1 ) ` '(w 2 ) we then have that
also
Suppose finally that '(w 1
consistent. There are two cases. If '(w 2 ) is '-inconsistent, then /(v '(w 1
Lemma 4.3 If ' satisfies C(P ), is the unique solution
of \Gamma(P; '), and e is a subterm of P , then we can derive A ` e : /(v '([[e]]) ).
Proof. We proceed by induction on the structure of e. In the base case, consider first
We have so we can derive A ` x : /(v '(hxi) ). This is the desired
derivation because
Consider then e j 0. We have and we can derive
In the induction step, consider first We have
so From the induction hypothesis we have that we can
derive A ' e and we can then also derive A ' succ e
Consider next e j -x:e 0 . We have f-x:e 0 g ' '([[-x:e 0 ]]), and from Lemma 4.2 we get
From the induction hypothesis, we have that we can derive
Thus, we can also derive A ' -x:e
Finally, consider e We have '([[e 1 ]]) ` Abs(P ), and for every -x:e 0 2 '([[e 1 ]])
we have '([[e 2 From the induction hypothesis, we
have that we can derive A ' There are two
cases. If '([[e 1 and we can
derive A ' e 1 then we use '([[e 1 ]]) ' Abs(P ) to conclude
that '([[e 1
]]) for all
is '-consistent. Thus, /(v '([[e 1 ]])
we can derive A ' e 1
For example, consider again the -term:
and recall the function ' 1 from Section 2 which satisfies C(E 1 ). The constraint system
When we plug this into the construction in the proof of Lemma 4.3, we get the type
derivation for shown in Section 3. We leave it to the reader to carry out the construction
It will lead to the type derivation for shown in Section 3.
From Types to Flows
Next we consider the mapping of types to flows. If \Delta is the type derivation A '
define f \Delta to map types to elements of CL(P
the set of occurrences -x:e of P where \Delta contains
a judgment of the form A
for an occurrence -x:e of P where \Delta contains
a judgment of the form A
for an occurrence e of P where \Delta contains
a judgment of the form A 0
Lemma 4.4 If \Delta is the type derivation A '
Proof. We consider in turn each of the constraints in C(P ). For an occurrence of 0 and
the constraint we have that \Delta contains a judgment of the form A 0
fIntg.
For an occurrence of succ e and the constraints
we have that \Delta contains judgments of the forms A
fIntg.
For an occurrence x and the constraint we have that \Delta contains a judgment
of the form A[x
For an occurrence -x:e and the constraint f-x:eg ' [[-x:e]], we have that \Delta contains
judgments of the forms A There are
two cases. If f-x:eg. If
For an occurrence e 1 e 2 and the constraint also the constraints, for
every occurrence -x:e in Abs(P ),
we have that \Delta contains judgments of the forms A 0 '
where There are two cases. If
and the other constraints are vacuously satisfied. If
From the definition of f
Concluding Remarks
If we remove from Section 3 the types ?, ? and the notion of subtyping, then we get a
traditional system of recursive types. Given a program P and a map ' 2 Cmap(P ), we
say that ' is consistent if for all S 2 range(') we have that S is '-consistent. If we add
to Section 2 the conditions:
does not contain ;, and
does not contain inconsistent maps,
then we get a notion of flow-based safety analysis which we here will refer to as restricted-
0-CFA= safety. It is easy to modify the proof of Lemma 4.3 to show the following result.
Theorem 5.1 If a -term P is restricted-0-CFA = safe, then P is typable with recursive
types.
Intuitively, the theorem says that if we want a flow analysis weaker than recursive types,
then we can start with 0-CFA= , outlaw ;, and insist on internal consistency in all flow sets.
The converse of Theorem 5.1 is false. For example, if we attempt to modify the proof of
Lemma 4.4, then we run into trouble in the case e 1 e 2 , because there is no guarantee that
is the type of e 1 . Such a situation arises with the program
With recursive types but not subtyping, there is just one type derivation for E 4 , using the
abbreviation
We have
It it straightforward to show that '([[x]]) 6= fIntg
and '([[x]]) 6= f-x:succ(x0)g, so
E 4 is therefore a counterexample to the converse of Theorem 5.1.
We leave it as an open problem to find a flow analysis equivalent to recursive types.
An unusual aspect of Heintze's definition of 0-CFA= is that Int and functions cannot
occur in the same flow set. To allow that we might define
and change the constraints from Section 2 such that the constraints for 0 and succ e become:
There is a systematic way of obtaining this modified flow analysis: begin with the constraints
for 0-CFA' [12] and
ffl change
to
All other constraints remain the same.
The type system that matches the modified flow analysis can be obtained by changing
the type system from Section 3 such that - is the smallest reflexive and transitive relation
on types where ? - t, and such that the type rules for 0 and succ e
become:
Notice that in this modified type system, ? is the least type and ? is the greatest type.



--R

Subtyping recursive types.
A practical and flexible flow analysis for higher-order languages
Efficient analyses for realistic off-line partial evaluation
On binary methods.
Fast interprocedural class analysis.
The Java Language Specification.


Dynamic typing.
The Definition of Standard ML.
Closure analysis in constraint form.
A type system equivalent to flow analysis.
From polyvariant flow information to intersection and union types.

Fast and accurate flow-insensitive points-to analysis


--TR
The definition of Standard ML
Control-flow analysis of higher-order languages of taming lambda
Dynamic typing
Subtyping recursive types
Object-oriented type systems
Closure analysis in constraint form
A type system equivalent to flow analysis
On binary methods
Points-to analysis in almost linear time
A practical and flexible flow analysis for higher-order languages
Linear-time subtransitive control flow analysis
Fast and accurate flow-insensitive points-to analysis
From polyvariant flow information to intersection and union types
Fast interprocedural class analysis
The Java Language Specification
Control-Flow Analysis and Type Systems

--CTR
Jens Palsberg , Mitchell Wand, CPS transformation of flow information, Journal of Functional Programming, v.13 n.5, p.905-923, September
Naoki Kobayashi, Type-based useless variable elimination, ACM SIGPLAN Notices, v.34 n.11, p.84-93, Nov. 1999
Naoki Kobayashi, Type-Based Useless-Variable Elimination, Higher-Order and Symbolic Computation, v.14 n.2-3, p.221-260, September 2001
Neal Glew , Jens Palsberg, Type-safe method inlining, Science of Computer Programming, v.52 n.1-3, p.281-306, August 2004
Jens Palsberg , Christina Pavlopoulou, From Polyvariant flow information to intersection and union types, Journal of Functional Programming, v.11 n.3, p.263-317, May 2001
Michael Hind, Pointer analysis: haven't we solved this problem yet?, Proceedings of the 2001 ACM SIGPLAN-SIGSOFT workshop on Program analysis for software tools and engineering, p.54-61, June 2001, Snowbird, Utah, United States
flow analysis;type systems