Type and ControlFlow Analysis

An Efficient Type and ControlFlow Analysis for System F
ifl14.pdf
(with Connor Adsit; Accepted to IFL'14 (postproceedings))
ifl14.orig.pdf
(with Connor Adsit; Presented at IFL'14; ifl14_talk.orig.pdf)
At IFL'12, we presented a novel monovariant flow analysis for
System F (with recursion) that yields both typeflow and
controlflow information. The typeflow information
approximates the type expressions that may instantiate type variables
and the controlflow information approximates the λ and
Λexpressions that may be bound to variables. Furthermore, the
two flows are mutually beneficial: control flow determines which
Λexpressions may be applied to which type expressions (and,
hence, which type expressions may instantiate which type variables),
while type flow filters the λ and Λexpressions that
may be bound to variables (by rejecting expressions with static types
that are incompatible with the static type of the variable under the
type flow).
Using a specificationbased formulation of the type and controlflow
analysis, we proved the analysis to be sound, decidable, and
computable. Unfortunately, naively implementing the analysis using a
standard least fixedpoint iteration yields an
O(n^{13}) algorithm.
In this work, we give an alternative flowgraphbased formulation of
the type and controlflow analysis. We prove that the
flowgraphbased formulation induces solutions satisfying the
specificationbased formulation and, hence, that the flowgraphbased
formulation of the analysis is sound. We give a direct algorithm
implementing the flowgraphbased formulation of the analysis and
demonstrate that it is O(n^{4}). By distinguishing
the size l of expressions in the program from the size
m of types in the program and performing an amortized
complexity analysis, we further demonstrate that the algorithm is
O(l^{3} + m^{4}).

An Efficient Type and ControlFlow Analysis for System F
gccisphd_talk.pdf
(Presented at Rochester Institute of Technology — GCCIS PhD Colloquium Series (201409260))
We present a monovariant flow analysis for System F (with
recursion). The flow analysis yields both controlflow
information, approximating the λ and Λexpressions that
may be bound to variables, and typeflow information,
approximating the type expressions that may instantiate type
variables. Moreover, the two flows are mutually beneficial: the
control flow determines which Λexpressions may be applied to
which type expressions (and,hence, which type expressions may
instantiate which type variables), while the type flow filters the
λ and Λexpressions that may be bound to variables (by
rejecting expressions with static types that are incompatible with the
static type of the variable under the type flow). We first give a
specificationbased formulation of the type and controlflow
analysis. Incompatibility of static types (with free type variables)
under a type flow is decided by interpreting the type flow as a
regulartree grammar and performing intersection and
emptiness operations. Unfortunately, naively implementing the
analysis using a standard least fixedpoint iteration technique yields
an O(n^{13}) algorithm, due to the cost of the
regulartree grammar operations in an inner loop. We next give an
alternative flowgraphbased formulation of the type and controlflow
analysis. We give a direct algorithm implementing the
flowgraphbased formulation of the analysis and demonstrate that it
is O(n^{4}). By distinguishing the size l
of terms in the program from the size m of types in the
program and performing an amortized complexity analysis, we further
demonstrate that the algorithm is O(l^{3} +
m^{4}).

A Type and ControlFlow Analysis for System F
pldg_talk.pdf
(Presented at Cornell University — Programming Language Discussion Group (20130220))

A Type and ControlFlow Analysis for System F
ifl12.pdf techrpt.pdf
(Accepted to IFL'12 (postproceedings))
ifl12.orig.pdf techrpt.orig.pdf
(Presented at IFL'12; ifl12_talk.orig.pdf; video)
We present a monovariant flow analysis for System F (with
recursion). The flow analysis yields both controlflow
information, approximating the λ and Λexpressions that
may be bound to variables, and typeflow information,
approximating the type expressions that may instantiate type
variables. Moreover, the two flows are mutually beneficial: the
control flow determines which Λexpressions may be applied to
which type expressions (and, hence, which type expressions may
instantiate which type variables), while the type flow filters the
λ and Λexpressions that may be bound to variables (by
rejecting expressions with static types that are incompatible with the
static type of the variable under the type flow). As is typical for a
monovariant controlflow analysis, controlflow information is
expressed as an abstract environment mapping variables to sets of
(syntactic) λ and Λexpressions that occur in the
program under analysis. Similarly, typeflow information is expressed
as an abstract environment mapping type variables to sets of
(syntactic) types that occur in the program under analysis.
Compatibility of static types (with free type variables) under a type
flow is decided by interpreting the abstract environment as
productions for a regulartree grammar and querying if the
languages generated by taking the types in question as starting terms
have a nonempty intersection.
The documents contained in these directories are included by the
contributing authors as a means to ensure timely dissemination of
scholarly and technical work on a noncommercial basis. Copyright and
all rights therein are maintained by the authors or by other copyright
holders, notwithstanding that they have offered their works here
electronically. It is understood that all persons copying this
information will adhere to the terms and constraints invoked by each
author's copyright. These works may not be reposted without the
explicit permission of the copyright holder.

