\newif\ifnoauthornotes\noauthornotesfalse

\newif\ifgenkill\genkillfalse  % have a section on gen and kill
\genkilltrue

\newif\ifseparateengine\separateenginetrue 
   % use engine.tex instead of what's here

\newif\ifnotesinmargin \notesinmargintrue 
\IfFileExists{notesinline.tex}{\notesinmarginfalse}{\relax}

\documentclass[blockstyle,preprint,nocopyrightspace]{sigplanconf}


\usepackage{alltt}
\usepackage{array}
\newcommand\lbr{\char`\{}
\newcommand\rbr{\char`\}}
 
\clubpenalty=10000
\widowpenalty=10000

\usepackage{verbatim} % allows to define \begin{smallcode}
\newenvironment{smallcode}{\small\verbatim}{\endverbatim}

\newcommand\arrow{\rightarrow}

\newcommand\join{\sqcup}
\newcommand\slotof[1]{\ensuremath{s_{#1}}}
\newcommand\tempof[1]{\ensuremath{t_{#1}}}

\makeatletter
\newcommand{\nrmono}[1]{%
  {\@tempdima = \fontdimen2\font\relax
   \texttt{\spaceskip = 1.1\@tempdima #1}}}
\makeatother

\usepackage{times}  % denser fonts
\renewcommand{\ttdefault}{aett} % \texttt that goes better with times fonts
\usepackage{enumerate}
\usepackage{url}
\usepackage{graphicx}
\usepackage{natbib}
\bibpunct();A{},
\let\cite\citep
\let\citeyearnopar=\citeyear
\let\citeyear=\citeyearpar

\usepackage[ps2pdf,bookmarksopen,breaklinks,pdftitle=dataflow-made-simple]{hyperref}

\newcommand\naive{na\"\i ve}

\usepackage{amsfonts}
\newcommand\naturals{\ensuremath{\mathbb{N}}}
\newcommand\true{\ensuremath{\mathbf{true}}}
\newcommand\implies{\supseteq}  % could use \Rightarrow?

\newcommand\PAL{\mbox{C{\texttt{-{}-}}}}
\newcommand\high[1]{\mbox{\fboxsep=1pt \smash{\fbox{\vrule height 6pt
   depth 0pt width 0pt \leavevmode \kern 1pt #1}}}}

% Put figures in boxes
\usepackage{float}
\floatstyle{boxed}
\restylefloat{figure}



% Set \noauthornotestrue to suppress notes
%\newcommand{\qed}{QED}
\ifnotesinmargin
  \long\def\authornote#1{%
          \leavevmode\unskip\raisebox{-3.5pt}{\rlap{$\scriptstyle\diamond$}}%
          \marginpar{\raggedright\hbadness=10000
         \def\baselinestretch{0.8}\tiny
         \it #1\par}}
\else
  % Simon: please set \notesinmargingfalse on the first line
  \newcommand{\authornote}[1]{{\em #1}}
\fi
\ifnoauthornotes
  \def\authornote#1{\unskip\relax}
\fi

\newcommand{\simon}[1]{\authornote{SLPJ: #1}}
\newcommand{\norman}[1]{\authornote{NR: #1}}
\let\remark\norman
\newcommand{\john}[1]{\authornote{JD: #1}}
\newcommand{\todo}[1]{\textbf{To~do:} \emph{#1}}

\newcommand\secref[1]{Section~\ref{sec:#1}}
\newcommand\seclabel[1]{\label{sec:#1}}

\newcommand\figref[1]{Figure~\ref{fig:#1}}
\newcommand\figlabel[1]{\label{fig:#1}}


\newcommand{\CPS}{\textbf{StkMan}}    % Not sure what to call it.


\usepackage{code}   % At-sign notation

\begin{document}
\title{Dataflow Optimization Made Simple}
%\subtitle{\today}

\authorinfo{Norman Ramsey}{Tufts University}{nr@cs.tufts.edu}
\authorinfo{Jo\~ao Dias}{Tufts University}{dias@cs.tufts.edu}
\authorinfo{Simon Peyton Jones}{Microsoft Research}{simonpj@microsoft.com}


\maketitle
 
\begin{abstract}
We present an interface that makes it easy for compiler writers
to implement program transformations based on dataflow analyses.
The compiler writer must identify (a)~a family of logical assertions
on which the transformation will be based;
(b)~an \emph{approximate} representation of such assertions, which
must be given a lattice structure such that every assertion can be increased at
most finitely many times;
(c)~transfer functions that approximate weakest preconditions or
strongest postconditions over the assertions; and
(d)~rewrite functions whose soundness is justified by the assertions.
To~guide the compiler writer,
we show how dataflow analyses are related to
seminal work on program 
correctness. 
Finally, we have implemented our interface using the
algorithm of 
\citet{lerner-grove-chambers:2002}, which enables the compiler writer to
compose very simple analyses and transformations in a way that achieves
the same precision as complex, handwritten
``super-analyses.''
Program transformations based on dataflow do most of the work of a new
back end for the Glasgow Haskell Compiler.
\end{abstract}

\makeatactive   %  Enable @foo@ notation

\section{Introduction}

Anyone writing a compiler for an imperative language gets the benefit
of over forty years' work on code improvement, also called
``optimization.''
But the way this work is typically presented annoys us: 
we see a large collection of apparently unrelated analyses and
transformations, each with its own name---who remembers the difference
between ``copy propagation'' and ``constant propagation,'' anyway?
The typical treatment obscures fundamental principles of
code improvement.

%The contribution of this paper is to elucidate a large body of work on code
%improvement; the body of work known as ``dataflow optimization.''
This paper makes two contributions:
\remark{Look up and see if ``dataflow optimization is a real term or
  if we want something else}
\begin{itemize}
\item
We show that the ad-hoc ``optimization zoo'' consists mostly of special
cases of reasoning techniques that have long been understood and used
by semanticists and functional programmers:
assertions about states, assertions about continuations, and
substitution of equals for equals (\secref{next-700}).
What distinguishes dataflow optimization from classic formal reasoning
about programs is that in dataflow optimization, the assertions are
computed automatically, and they are
\emph{approximated}. 
\item
We embody our ideas in an implementation that makes it not just
possible but \emph{easy} to adapt imperative, dataflow-based
code-improvement techniques to a purely functional compiler.
We~write analyses and transformations in such a way that
the code which is specific to a particular analysis is small, simple,
and easy to get right.
The complex part of dataflow optimization, which is difficult to get right, is
written once and is shared by all analyses and transformations.
\end{itemize}

We consider code improvements only over low-level
imperative codes, emcompassing both intermediate languages and machine
languages.
As \citet{benitez-davidson:portable-optimizer} have shown, all the
classical scalar and loop optimizations can be performed over such
codes.
Moreover, any functional program compiled to native code must
eventually translate to such a code.


We introduce the subject by analyzing and transforming example code in
\secref{example:xforms},
showing how we think about and justify classical optimizations using
Hoare logic and the substitution of equals for equals.
To~support our claim that we make dataflow optimization easy, 
we spend most of the paper explaining how
a compiler writer creates new dataflow analyses or transformations
(\secref{making-simple}) and showing complete implementations of significant
analyses (\secref{example-analyses}) and transformations
(\secref{example-rewrites}) from the Glasgow Haskell compiler.
We spend less space, in \secref{engine}, on the shared implementation.


\section{Dataflow analysis {\&} transformation by \rlap{example}}

\seclabel{example:transforms}
\seclabel{example:xforms}

In dataflow optimization, code-improving transformations are justified
by assertions about the program;
such assertions are typically computed using
strongest postconditions or weakest liberal preconditions.
The most typical transformations are
insertion of redundant assignments,
substitution of
equals for equals, 
and
removal of redundandant assignments,
all of which preserve semantics.
(Insertion and removal are often composed to achieve the effect called
``code motion,'' as done by \citet{knoop:lazy-code-motion}, for example.) 
The examples below express classical code
improvements by composing small analyses and transformations.



\newcommand\exampletransform{\subsection}


\exampletransform{Simple transformations}

\seclabel{constant-propagation}

Here is a sequence of three assignments separated by assertions.
We compute the assertions by starting with the weakest possible
assertion (@true@) and computing strongest postconditions.\footnote
{Variables do not alias.}
\begin{verbatim}
    { true }
  x = 7;
    { x == 7 }
  y = 8: 
    { x == 7 && y == 8 }
  z = x + y;
\end{verbatim}
In the assignment to~@z@, the assertion @x == 7@ justifies
substituting 7~for~@x@, leaving @z = 7 + y@.  
This transformation is traditionally called ``constant propagation.''
We may also substitute 8~for~@y@.
Finally, because @7 + 8 == 15@, we may again substitute equals for
equals, leaving the final assignment as
\begin{verbatim}
  z = 15;
\end{verbatim}
This transformation, although another instance of substituting equals
for equals, has a different name: ``constant folding.''

\exampletransform{A complex transformation}

\seclabel{induction-var-elim}

The loop optimization known as ``induction-variable elimination'' is
actually a collection of simple transformations.
We begin by showing a simple loop written in the style of FORTRAN,
although the code is~C code:
\begin{verbatim}
  struct pixel { double r, g, b; };
  double sum_r(struct pixel a[], int n) {
    double x = 0.0;
    int i;
    for (i = 0; i < n; i++)
      x += a[i].r;
    return x;
  }
\end{verbatim}
To explain the improvement we wish to make, we show the same
code at the machine level.
We write machine-level examples using our low-level compiler-target
language,~{\PAL} % tuning for line breaks
\cite{peyton-jones-ramsey:garbage-collection:inproceedings,peyton-jones-ramsey:exceptions}: 
\begin{verbatim}
  sum_r("address" bits32 a, bits32 n) {
       bits64 x; bits32 i;
       x = 0.0;
       i = 0;
   L1: if (i >= n) goto L2;
       x = %fadd(x, bits64[a+i*24]);
       i = i + 1;
       goto L1;
   L2: return x; 
  }
\end{verbatim}
The code improvement called ``induction-variable elimination''
replaces~@i@ with a new variable~@p@ so that we can avoid repeating
the computation @a+i*24@ on each iteration through the loop.
The new variable~@p@ is intended to satisfy the invariant
\begin{verbatim}
   { p == a + i * 24 }
\end{verbatim}
The variable @i@ is also used in the loop-termination test.
To rewrite that test, 
we introduce a new variable @lim@ satisfying
the invariant % line breaking
@lim == a + n * 24@,
so that @i >= n@ if and only if @p >= lim@.

We implement the code improvement as a sequence of transformations.
After each step, the observable behavior of the program is unchanged,
and it is possible to generate code (see discussion in \secref{vpoiso}).
%
Our first step is to declare @p@ and @lim@ and to insert suitable
assignments. 
New code is \high{boxed}\,.
\begin{alltt}
  sum_r("address" bits32 a, bits32 n) \lbr
       bits64 x; bits32 i; \high{bits32 p, lim;}
       x = 0.0;
       i = 0; \high{p = a; lim = a + n * 24;}
   L1: if (i >= n) goto L2;
       x = %fadd(x, bits64[a+i*24]);
       i = i + 1; \high{p = p + 24;}
       goto L1;
   L2: return x; 
  \rbr
\end{alltt}

As written, the assignments to @p@~and~@lim@ have no
effect on the program, but they enable the compiler to establish the assertions
@p == a + i * 24@ and @(i >= n) == (p >= lim)@.
On~the basis of these assertions, the compiler substitutes equals for
equals, resulting in the new code in boxes below:
\begin{alltt}
  sum_r("address" bits32 a, bits32 n) \lbr
       bits64 x; bits32 i; bits32 p, lim;
       x = 0.0;
       i = 0; p = a; lim = a + n * 24;
   L1: if (\high{p >= lim}) goto L2;
       x = %fadd(x, bits64[\kern1pt{}\high{p}\kern1pt{}]);
       i = i + 1; p = p + 24;
       goto L1;
   L2: return x; 
  \rbr
\end{alltt}

At this point, the compiler switches from reasoning about states to
reasoning about continuations.
In~particular, we reason about whether the value of a variable can be
used by a continuation; this reasoning is called ``liveness analysis.''
A~\naive\ analysis would show that although @i@~is not live at
label~@L2@, it is nevertheless live immediately after 
the assignment
@i = i + 1@ in the loop body,
because the value of~@i@ could be used by the next iteration of the
loop.
But we use the framework of
\citet{lerner-grove-chambers:2002} to \emph{interleave} liveness
analysis with 
``dead-assignment elimination.'' 
Dead-assignment elimination removes an assignment if the variable
assigned to is not live, that is, if it cannot be used by the
assignment's continuation.
As~explained in detail by Lerner, Grove, and Chambers, no sequential
composition of liveness analysis and dead-assignment elimination can
get rid of these assignments to~@i@, but interleaving analysis with
transformation does the trick.\footnote
{An experienced reader might be tempted to modify the
liveness analysis so that
@i = i + 1@ is not considered a ``use'' of~@i@ if @i@~is itself
dead.
This modification is tantamount to writing a single, combined dataflow
pass that understands \emph{both} liveness analysis and dead-code
elimination.
In~this particular example, writing a single, combined pass presents
few difficulties, but the approach does not scale:
most combined passes are more complicated than the examples shown here;
the cost of writing combined passes does not scale linearly with
the number of individual passes;
combined passes often cannot be composed;
and 
some combined passes require nonstandard, handwritten traversals of
the control-flow graph.
\citet{lerner-grove-chambers:2002} discuss these issues in detail;
\citet{click-cooper} present a handwritten combined pass of
significant complexity.}
\secref{dfengine} describes our implementation of their interleaving
method, which eliminates the boxed assignments to~@i@:
\begin{alltt}
sum_r("address" bits32 a, bits32 n) \lbr
     bits64 x; \high{bits32 i;} bits32 p, lim;
     x = 0.0;
     \high{i = 0;} p = a; lim = a + n * 24;
 L1: if ({p >= lim}) goto L2;
     x = %fadd(x, bits64[{p}]);
     \high{i = i + 1;} p = p + 24;
     goto L1;
 L2: return x; 
\rbr
\end{alltt}

After the insertion of assignments to @p@~and~@lim@, the substitution
of equals for equals, the removal of newly redundant assignments
to~@i@, we have ``eliminated the induction variable:''
\begin{alltt}
sum_r("address" bits32 a, bits32 n) \lbr
     bits64 x; bits32 p, lim;
     x = 0.0;
     p = a; lim = a + n * 24;
 L1: if ({p >= lim}) goto L2;
     x = %fadd(x, bits64[{p}]);
     p = p + 24;
     goto L1;
 L2: return x; 
\rbr
\end{alltt}

  
\section {Making dataflow simple}

\seclabel{making-simple}

\seclabel{create-analysis}

The goal of dataflow optimization is to compute valid
assertions, then use those assertions to justify code-improving
transformations.\remark{We want this whole \S\ on page~2}

% only Don Knuth knows why, but the paragraph break gets us three
% bullets on this page where a single paragraph gets only two!

Assertions are written in a restricted
language of \emph{dataflow facts}.
The connection between dataflow facts and traditional program logic is
elucidated in \secref{next-700}, but the most salient points are
these:
\begin{itemize}
\item
A dataflow fact is equivalent to an assertion about program state or
about a continuation.
For example, in \secref{constant-propagation}, @x == 7@ is a dataflow
fact. 
\item
Each analysis or transformation may use a different language of
dataflow facts.
\item
Each language of dataflow facts forms a lattice.
To ensure that analysis terminates,
it is enough if
no fact has more than finitely many distinct facts above it.
\end{itemize}


Assertions hold at program points, which we represent as edges in
a \emph{control-flow graph}.\footnote
{We discuss only intraprocedural optimization here;
interprocedural optimizations are the work of the GHC~inliner
\cite{peyton-jones:secrets-inliner}.} 
The edges connect nodes, each of which represents a label, an assignment, or
a control transfer.

To write a dataflow analysis, the compiler
writer must 
\begin{itemize}
\item
Choose a representation~$F$ of dataflow facts and a logical interpretation
thereof
\item
Implement lattice operations over~$F$
\item
Write \emph{transfer functions} that relate dataflow facts before and
after each type of node
\end{itemize}

To write a transformation based on an analysis, the compiler writer
must create a \emph{rewrite function}, which is presented with a
flow-graph node and with the dataflow facts on the edges coming
into that node.
The function either suggests that the node should be replaced with a
fresh subgraph, or it leaves the node alone.
The rewrite function uses incoming facts to guarantee that
any proposed replacement preserves semantics.
For example, in \secref{constant-propagation} the fact @x == 7@ is
used to justify replacing @z = x + y@ with @z = 7 + y@.

Given lattice operations and transfer functions, our
polymorphic, reusable \emph{dataflow engine} computes a
set of dataflow facts, one for each edge in the control-flow graph.
The set of facts is a fixed point of the transfer functions.
Given, in addition, a rewrite function for each type of node,
the dataflow engine implements a semantics-preserving transformation. 

\begin{figure}
\begin{code}
data ChangeFlag = NoChange | SomeChange
data TxRes a    = TxRes ChangeFlag a
data DataflowLattice a = DataflowLattice
 {fact_bot        :: a,
  fact_add_to     :: a -> a -> TxRes a,
  fact_name       :: String } -- for debugging
\end{code}
\caption{Representation of a dataflow lattice} \figlabel{lattice-type} \figlabel{lattice}
\end{figure}


\subsection{Dataflow lattices}


As an example lattice of dataflow facts, 
we present a representation for facts about constant propagation.
At any program point, a standard constant-propagation analysis
computes exactly one of the following three
assertions about a variable~$x$:
\begin{itemize}
\item
The analysis shows that
$x = k$, where $k$~is a compile-time constant.
\item
The analysis shows that $x$~is \emph{not} a compile-time constant.
We~notate this assertion as $x = \top$.
\item
The analysis shows nothing about~$x$, which we notate $x=\bot$.
\end{itemize}
The bottom element of the lattice is~$\bot$, and
the join operation corresponds to disjunction.
\emph{The logic implied by the
representation of dataflow facts cannot represent disjunction
exactly}; instead, a
disjunction of two inconsistent facts is represented by~$\top$.
\remark{At some point must talk about how the facts are
\emph{represented}, e.g., finite map from variable to @Maybe Const@}
Here are some examples:
\begin{itemize}
\item
$i = 7 \lor i=\bot \equiv i=7$ (no loss of information)
\item
$i = 7 \lor i= 7 \equiv  i=7$ (no loss of information)
\item
$i = 7 \lor i = 8 \equiv i = \top$ (loss of information)
\end{itemize}
The lattice  used by the analysis is the Cartesian product of the
lattices for all the local variables.
Because in any one program there are only finitely many variables,
only finitely many facts are computed at any program point, 
and any one fact can increase at most twice.
Together, these properties
guarantee that the dataflow engine will
reach a fixed point.



The dataflow engine uses the lattice join operation in a stylized way.
Joins occur at labels.
If~$f_{\mathit{id}}$ is the fact currently associated with the
label~$\mathit{id}$, 
and if a transfer function propagates a new fact~$f_{\mathit{new}}$
into the label~$\mathit{id}$, 
the dataflow engine replaces $f_{\mathit{id}}$ with
the join  $f_{\mathit{new}} \join f_{\mathit{id}}$.
Furthermore, the dataflow engine wants to know if
  $f_{\mathit{new}} \join f_{\mathit{id}} = f_{\mathit{id}}$,
because if not, it has not reached a fixed point.

When computing a join, 
it is typically very cheap to learn if the join
is equal to one of the arguments.
We therefore use the nonstandard representation of lattice operations
shown in \figref{lattice}.
The join operation~$\join$ and equality test~$=$ are represented by a
single function called @fact_add_to@.
The term $@fact_add_to@\;f_{\mathit{new}}\;f_{\mathit{id}}$ is equal to
$@TxRes NoChange@\; f_{\mathit{id}}$ if $f_{\mathit{new}} \join f_{\mathit{id}} = f_{\mathit{id}}$
and is equal to
$@TxRes SomeChange@\; (f_{\mathit{new}} \join f_{\mathit{id}})$ otherwise.
The @fact_bot@ value is the bottom element of the
lattice, 
and @fact_name@  is used for debugging.

\begin{figure}
\begin{code}
newtype LastOuts a = LastOuts [(BlockId, a)] 
data ForwardTransfers mid last a = ForwardTransfers
 {ft_first_out  :: BlockId -> a -> a,
  ft_middle_out :: mid     -> a -> a,
  ft_last_outs  :: last    -> a -> LastOuts a} 

data BackTransfers mid last a = BackTransfers
 {bt_first_in  :: BlockId -> a              -> a,
  bt_middle_in :: mid     -> a              -> a,
  bt_last_in   :: last    -> (BlockId -> a) -> a} 
\end{code}
\caption{Transfer functions for forward and backward analyses.}
\figlabel{transfers}
%
% elided: 
%    ft_exit_out   ::            a -> a
%
\end{figure}



\subsection{Transfer functions}

A~transfer function is presented with dataflow facts on edges coming
into a node, and it computes the dataflow facts on outgoing edges.
To~understand the types of transfer functions, we must first
understand how the nodes and edges of a control-flow graph are organized.

A~control-flow graph is a collection of labelled \emph{basic blocks}.
Each basic block is a sequence beginning with a \emph{first node},
containing zero or more \emph{middle nodes},
and ending in a \emph{last node}.
A~first node is always a label;
a~typical middle node assigns to a register or memory
location;
a~typical last node is a conditional, unconditional, or indirect branch.
\remark{Forward reference?}

Each type of node has its own invariant, which
constrains the number of predecessors and the number of successors of
that type of node in the control-flow graph.
A~first node has arbitrarily many predecessors and exactly one
successor;
a~middle node has exactly one predecessor and one successor;
and a last node has exactly one predecessor and arbitrarily many
successors. 

The constraints on the graph structure determine the signatures of
transfer functions, 
which are shown in \figref{transfers}.
For each type of node (first, middle, last) and for each kind of
analysis (forward, backward), there is a distinct transfer function.
Functions are grouped by kind of analysis, and each group is
parameterized over a dataflow fact of type~@a@ and over the types
@mid@ and @last@ of middle and last nodes.

The type @BlockId@ represents a label.
Because a fact in a forward analysis typically represents an assertion
about program state, and because passing a label does not change
program state, the transfer function @ft_first_out@ is typically 
@flip const@---a variation on
the
identity function.
\remark{Somewhere we should explain what a fact in a backward analysis
typically represents}
For a middle node, the transfer function @ft_middle_out@ is given a
node and a precondition and returns an approximation of the strongest
postcondition. 
For a last node, different postconditions may be propagated to
different successors; for example, the true and false successors of a
conditional branch may accumulate information implied by the truth or
falsehood of the condition.
A~collection of (successor, fact) pairs is represented by a value of
type @LastOuts a@.




In a forward analysis, the dataflow engine starts with the fact at the
beginning of a block and applies transfer functions to the nodes in
that block until eventually the transfer function for the last node
computes the facts that are propagated to the block's successors.
For example, in the basic block
\begin{verbatim}
  L1: x = 7;
      y = 8;
      z = x + y;
      goto L2;
\end{verbatim}
a forward analysis would propagate the fact 
$@x == 7@ \land @y == 8@$, which we will call $f_{\mathit{new}}$,
along the edge to~@L2@. 
\remark{Do we want an example that says 
$@ft\_middle\_out@\;f = f \land @x == 7@$?}
The dataflow engine then \emph{replaces} the current fact
at~@L2@~($f_{\mathtt{L2}}$) with the lattice join $f_{\mathit{new}}
\join f_{\mathtt{L2}}$. 
The dataflow engine iterates over the blocks repeatedly, creating new
facts~$f$ and joining them with facts $f_{\mathit{id}}$ until
\mbox{$f \join f_{\mathit{id}} = f_{\mathit{id}}$} at every label~$\mathit{id}$.
When the facts at labels stop changing, the dataflow
engine has reached a fixed point.
%\remark{Promissory note: compose this analysis with two
%transformations: constant propagation and constant folding}



\subsection{Running the dataflow engine}

\seclabel{zdfSolveFwd}

Given lattice operations of type @DataflowLattice a@
and transfer functions of type @ForwardTransfers m l a@,
the compiler writer can run the analysis by calling the
dataflow-engine function @zdfSolveFwd@:
\begin{code}
 zdfSolveFwd 
  :: LastNode l             -- Constrains last nodes
  => PassName               -- Name of this analysis
  -> DataflowLattice a      -- Lattice
  -> ForwardTransfers m l a -- Transfer functions
  -> a                      -- Input fact
  -> Graph m l              -- Control-flow graph
  -> ForwardFixedPoint m l a
\end{code}
The engine is polymorphic in the types of middle and last nodes
@m@~and~@l@ and in the type of the dataflow fact~@a@.
The first three arguments characterize the analysis.
The next argument is the dataflow fact that holds on entry to the
graph;
because the analysis may be run on a graph returned by a rewrite
function,\remark{forward ref, maybe}
this fact
is not always~$\bot$.
For example, if a rewrite function proposes to replace 
@z = x + y@ with @z = 7 + y@, an analysis will be run on the one-node
graph @z = 7 + y@ with input fact
$@x == 7@ \land @y == 8@$.
The last argument to @zdfSolveFwd@ is the graph, and the result is a 
fixed point.\footnote
{The type of @zdfSolveFwd@ has pedagogical lies;
truth is told in~\secref{engine-truth}.}\remark{One of the lies is
that I've deliberately conflated the three representations of graphs.}

The @ForwardFixedPoint@ data structure is a big bag
of information about the solution.
The most significant information includes
a finite map from each block label to the dataflow fact that holds at
the label, which is extracted using function @zdfFpFacts@;
and
a list of facts that hold on edges leaving the graph, which is  
 extracted using function @zdfFpLastOuts@.
\iffalse %%% WRONG -- it's the @goto@ that does this...
In the example above, when the subgraph
@z = 7 + y@ is analyzed, @zdfFpLastOuts@ will contain
the pair $(@L2@, @x == 7@ \land @y == 8@)$.
\fi






\iffalse
% never tell the whole truth!
\begin{code}
class DataflowSolverDirection
        transfers fixedpt where
  zdfSolveFrom :: (DebugNodes m l, Outputable a)
    => BlockEnv a        -- Init facts
    -> PassName          -- Analysis name
    -> DataflowLattice a -- Lattice
    -> transfers m l a   -- Transfers
    -> a                 -- Input fact
    -> Graph m l         -- CFG
    -> DFMonad (fixedpt m l a ())
\end{code}
\fi



%%  \subsection{Leftover junk}
%%  
%%  \begin{itemize} 
%%  \item
%%  
%%  \item
%%   for first, middle, and last nodes;
%%  if $F$~represents a logical assertion about program state, it is
%%  sufficient that the strongest postcondition imply the output of each
%%  transfer function.
%%  \item
%%  \item
%%  The main part of the implementation of the dataflow framework is the
%%  \emph{dataflow engine}.
%%  The dataflow engine may be used with a analysis pass,
%%  in which case it sets up the recursion equations implied by the
%%  transfer functions and finds a solution by iterating to a fixed point.
%%  The solution is represented by a finite map giving the dataflow fact
%%  at each label; other facts can be reconstructed using the transfer functions.
%%  
%%  The dataflow engine may also be used to \emph{interleave} analysis
%%  with transformation, in which case
%%  it not only solves the dataflow equations but may also rewrite the
%%  graph  \cite{lerner-grove-chambers:2002}. 
%%  %%%%\item
%%  %%%%The ease with which the framework can be used is determined by the
%%  %%%%\emph{interface} between the dataflow engine and the client passes.
%%  
%%  \item
%%  
%%  %\item
%%  Dataflow facts before and after nodes are related by \emph{transfer
%%  functions}.
%%  
%%  
%%  \end{itemize}
%%  The main contribution of this paper is to present an interface which
%%  enables many powerful program transformations based on dataflow
%%  analysis while keeping the individual dataflow passes as simple as
%%  possible.
%%  We keep the \emph{concepts} simple by relating dataflow facts and
%%  transfer functions to classic work in program correctness, as
%%  discussed in \secref{next-700}.
%%  We keep the \emph{implementations of dataflow passes} simple by pushing
%%  as much work as
%%  possible into the dataflow engine, which is implemented just once.
%%  We have also made the dataflow engine and its interface polymorphic in
%%  the types of 
%%  the nodes that appear in the control-flow graph \secref{polymorphic-framework}.
%%  Parametricity ensures separation of concerns between the dataflow
%%  engine and the individual dataflow passes.





\section{Example analysis passes}

\seclabel{example-analyses}


\newcommand\T{\rule{0pt}{0.6ex}}
\newcommand\B{\rule[-0.05ex]{0pt}{0pt}}
\newcolumntype{C}{>{\begin{minipage}{5.35in}}l<{\end{minipage}}} % code
\newcolumntype{L}{>{\Large\bfseries}m{1.3in}<{\centering}}       % label
\newenvironment{codetable}{\begin{tabular}{CL}}{\end{tabular}}

\begin{figure*}
\begin{codetable}
\T\begin{code}
data AvailVars = UniverseMinus VarSet
               | AvailVars     VarSet
extendAvail  :: AvailVars -> LocalVar  -> AvailVars
delFromAvail :: AvailVars -> LocalVar  -> AvailVars
elemAvail    :: AvailVars -> LocalVar  -> Bool
interAvail   :: AvailVars -> AvailVars -> AvailVars
smallerAvail :: AvailVars -> AvailVars -> Bool
\end{code}\B
& Dataflow fact and operations\\
\hline

\T\begin{code}
availVarsLattice :: DataflowLattice AvailVars
availVarsLattice = DataflowLattice "reloaded registers" empty add False
    where empty = UniverseMinus emptyVarSet
          add new old = let join = interAvail new old in
                        if join `smallerAvail` old then aTx join else noTx join
\end{code}\B
& Lattice\\
\hline

%%  \T\begin{code}
%%  agen  :: UserOfLocalVars    a => a -> AvailVars -> AvailVars
%%  akill :: DefinerOfLocalVars a => a -> AvailVars -> AvailVars
%%  agen  a avail = foldVarsUsed extendAvail  avail a
%%  akill a avail = foldVarsDefd delFromAvail avail a
%%  \end{code}\B
%%  & Gen/Kill \mbox{functions}\\
%%  \hline
%%  
\T\begin{code}
avail_reloads_transfer :: ForwardTransfers Middle Last AvailVars
avail_reloads_transfer = ForwardTransfers (flip const) middleAvail lastAvail

middleAvail :: Middle -> AvailVars -> AvailVars
middleAvail (MidAssign (CmmLocal x) (CmmLoad l) avail
                 | l `isStackSlotOf` x = extendAvail avail x
middleAvail (MidAssign lhs _expr) avail = 
  foldVarsDefd delFromAvail avail lhs  -- remove variables defined in 'lhs'
middleAvail (MidStore {})         avail = avail
middleAvail (MidComment {})       avail = avail

lastAvail :: Last -> AvailVars -> LastOuts AvailVars
lastAvail (LastCall _ (Just k) _ _) _ = LastOuts [(k, AvailVars emptyVarSet)]
lastAvail l avail = LastOuts $ map (\id -> (id, avail)) $ succs l
\end{code}\B
& Transfer \mbox{functions}\\
\hline

\T\begin{code}
cmmAvailableReloads :: Graph Middle Last -> BlockEnv AvailVars
cmmAvailableReloads g = zdfFpFacts soln
  where soln = zdfSolveFwd "available reloads" availVarsLattice 
               avail_reloads_transfer (fact_bot availVarsLattice) g
\end{code}\B
& Available-reloads analysis\\
%\hline

\end{codetable}
% \caption{Available-variable analysis}
\caption{Dataflow analysis pass to compute available variables}
\figlabel{avail-all}
\figlabel{avail}
\figlabel{avail-lattice}
\figlabel{avail-gen-kill}
\figlabel{avail-transfers}
\figlabel{avail-running}
\end{figure*}
% Old captions' text:
% The dataflow fact for the available-reload analysis describes
%   the set of registers for which a reload is available.
%   We list the types of the functions that manipuate sets of available registers,
%   as well as the definition of the lattice.
% The standard gen and kill functions for available expressions
% The transfer functions for the available-reloads analysis.
% Running the available-reloads analysis and extracting the results with \texttt{zdfFpFacts}
% The rewrite functions to insert redundant reloads immediately before uses

% Probably no space for the implementations:
% interAvail (UniverseMinus s) (UniverseMinus s') =
%   UniverseMinus (s `plusVarSet`  s')
% interAvail (AvailVars     s) (AvailVars     s') =
%   AvailVars (s `timesVarSet` s')
% interAvail (AvailVars     s) (UniverseMinus s') =
%   AvailVars (s  `minusVarSet` s')
% interAvail (UniverseMinus s) (AvailVars     s') =
%   AvailVars (s' `minusVarSet` s )
% 
% smallerAvail (AvailVars _) (UniverseMinus _) = True
% smallerAvail (UniverseMinus _) (AvailVars _) = False
% smallerAvail (AvailVars     s) (AvailVars    s')  =
%   sizeVarSet s < sizeVarSet s'
% smallerAvail (UniverseMinus s) (UniverseMinus s') =
%   sizeVarSet s > sizeVarSet s'
% 
% extendAvail (UniverseMinus s) r =
%   UniverseMinus (deleteFromVarSet s r)
% extendAvail (AvailVars     s) r =
%   AvailVars (extendVarSet s r)
% 
% delFromAvail (UniverseMinus s) r =
%   UniverseMinus (extendVarSet s r)
% delFromAvail (AvailVars     s) r =
%   AvailVars (deleteFromVarSet s r)
% 
% elemAvail (UniverseMinus s) r =
%   not $ elemVarSet r s
% elemAvail (AvailVars     s) r =
%   elemVarSet r s


Our big claim is that using our data structures, algorithms, and
interfaces makes it easy to write compiler passes based on dataflow.
In~this section we provide evidence for that claim by showing
implementations of two analyses;
related program transformations appear in \secref{example-rewrites}
below. 
These analyses help solve a real problem in the Glasgow Haskell
Compiler:
there are no callee-saves registers, so at each call site, all live
variables must be spilled to the stack.
In order to reduce register pressure,
such variables are spilled as early as possible and reloaded as late as possible.

To illustrate the results of the analyses and their associated transformations,
here is a contrived example program in the style of \secref{example:xforms}:
\begin{alltt}
f (bits32 a) \lbr
  bits32 x, y, z;  // local variables
  x = a * a;
  y = g(a + a);
  z = y + y;
  if (y > 0) \lbr
    return z;
  \rbr else \lbr
    return z + x;
  \rbr
\rbr
\end{alltt}
If @R1@ is the first argument register and @R0@ is the result
register, spills and reloads should be inserted as follows:%
\seclabel{spill-reload-example} % space is deliberate
\newcommand\bigstrut{%
  \leavevmode\vrule width 0pt height 11pt depth 6pt }
\begin{alltt}
f (bits32 a) \lbr
  bits32 x, y, z;  // local variables
  x = a * a;
  \high{SPILL x;}
  \bigstrut\high{R1 = a + a;} // no register pressure from x
  \high{y = g(R1);} // call instruction
  z = y + y;
  if (y > 0) \lbr
    return z;
  \rbr else \lbr
    \high{RELOAD x;}
    return z + x;
  \rbr
\rbr
\end{alltt}
Although the @SPILL@ and @RELOAD@ operations are introduced because of
the call to @g(a)@, they are moved as far from the call as possible:
the variable~@x@ is spilled immediately after being assigned @a * a@,
and @x@ is reloaded not
immediately after the call to~@g@, but just before its use in the
expression @z + x@.
 On the control-flow path to @return z@, @x@~needn't be reloaded
at all.

Getting spills and reloads in the right places requires the
composition of several dataflow passes:
\begin{enumerate}
\item
A backward transformation inserts reloads immediately after each call
site.
The same pass inserts spills not immediately before call sites, but
rather immediately after the appropriate reaching definitions.
\item
\label{reload-duplication}
A second pass inserts redundant reloads immediately before the
reloaded variables are used.
By keeping variables on the stack longer, this pass reduces register
pressure.
\item
\label{remove-dead-reloads}
A final pass, dead-assignment elimination, removes redundant reloads.
\end{enumerate}
The combined effect of passes
\ref{reload-duplication}~and~\ref{remove-dead-reloads} is to ``sink''
the reloads as far as possible from the call site.
In the next subsection we describe an analysis that supports
pass~\ref{reload-duplication}; 
pass~\ref{reload-duplication} itself is described in
\secref{sink-reloads}, and 
pass~\ref{remove-dead-reloads} is described in
\secref{dead-code-elimination}.


\subsection{Available variables: a forward analysis} 

\seclabel{avail}


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
%  desperately trying to get figures to emerge in a decent order
%
\begin{figure*}
\begin{codetable}
\T\begin{code}
type Live = VarSet
\end{code}\B
& Dataflow fact\\
\hline

\T\begin{code}
liveLattice :: DataflowLattice Live
liveLattice = DataflowLattice "live LocalReg's" emptyVarSet add False
  where add new old =
          let join = unionVarSets new old in
          (if sizeVarSet join > sizeVarSet old then aTx else noTx) join
\end{code}\B
& Lattice\\
\hline

%%  \T\begin{code}
%%  gen  :: UserOfLocalVars    a => a -> Live -> Live
%%  kill :: DefinerOfLocalVars a => a -> Live -> Live 
%%  gen  a live = foldVarsUsed extendVarSet  live a
%%  kill a live = foldVarsDefd delFromVarSet live a
%%  \end{code}\B
%%  & Gen/Kill \mbox{functions}\\
%%  \hline

\T\begin{code}
liveTransfers :: BackwardTransfers Middle Last Live
liveTransfers = BackwardTransfers (flip const) middleLiveness lastLiveness

middleLiveness :: Middle -> Live -> Live
lastLiveness   :: Last -> (BlockId -> Live) -> Live
middleLiveness l = addUsed l . remDefd l
lastLiveness   l = addUsed l . remDefd l . lastLiveOut l 

addUsed :: UserOfLocalVars    a => a -> Live -> Live
remDefd :: DefinerOfLocalVars a => a -> Live -> Live 
addUsed a live = foldVarsUsed extendVarSet  live a
remDefd a live = foldVarsDefd delFromVarSet live a

lastLiveOut :: Last -> (BlockId -> Live) -> Live
lastLiveOut l env = last l 
  where
    last (LastBranch id)        = env id 
    last (LastCondBranch _ t f) = unionVarSets (env t) (env f)
    last (LastSwitch _ tbl)     = unionManyVarSets $ map env (catMaybes tbl)
    last (LastCall { })         = emptyVarSet
\end{code}\B
& Transfer \mbox{functions}\\
\hline

\T\begin{code}
cmmLiveness :: Graph Middle Last -> BlockEnv Live
cmmLiveness g = zdfFpFacts soln
    where res = zdfSolveBwd "liveness analysis" liveLattice liveTransfers emptyVarSet g
\end{code}\B
& Liveness \mbox{analysis}\\
\end{codetable}
\caption{Liveness analysis}
\figlabel{liveness-all}
\figlabel{liveness}
\figlabel{live-lattice}
\figlabel{live-transfers}
\figlabel{live-running}
\end{figure*}
%
%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%



To~understand the analysis, you must know that for each variable~$x$,
there is a compiler pseudoregister~\tempof x and a stack slot~\slotof x, each of
which is used only to hold the value of~$x$.
%
\remark{Changing ``register'' to
``variable'' makes the example easier to understand and hides a
GHC-ism, but there's a slippery slope here\ldots}
%
If the stack slot is up to date, that is if $x = \slotof x$,
then it is safe to insert a reload without changing the observable
behavior of the program.
The logical assertion of interest therefore takes the form $x = \slotof x$.
The dataflow fact that corresponds to a conjunction of assertions of
this form is a set of variables~$X$ such that $\forall x \in X \mathrel
: x = \slotof x$.
The lattice-join operation is set intersection,\footnote
{A variable $x = \slotof x$ at a label~@L@ if and
only if $x = \slotof x$ on every control-flow edge coming into~@L@.}
and the bottom element
is the universal set containing all variables.
Because universal sets can be awkward to manipulate, we represent a
set using one of two alternatives
(see~\figref{avail-lattice}):
\begin{itemize}
\item \texttt{UniverseMinus~s}: All variables except those in the set~@s@
\item \texttt{AvailVars~~~~~s}: The variables in the set~@s@
\end{itemize}
The bottom element is @UniverseMinus emptyVarSet@.




%%  Among many other uses, an available-expressions analysis can be~used
%%  in code-motion optimizations.
%%  For example, when making a function call, we insert
%%  spills and reloads to save and restore the values of local variables
%%  around the call site.
%%  It is easy to insert the reloads at the function-call return site,
%%  but to avoid register pressure, it would be better to leave the variable
%%  where it was spilled on the stack.
%%  Rather than complicating the code that inserts the spills and
%%  reloads around call sites,
%%  we write an analysis to insert a redundant reload immediately
%%  before a reloaded variable is used.
%%  Then, we rely on a dead-code elimination to~remove
%%  the early reload.

To manipulate sets of variables, we provide these functions:
\begin{itemize}
\item \texttt{extendAvail~~s~x}: Add variable @x@ to the set~@s@
\item \texttt{delFromAvail~s~x}: Remove variable @x@ from the set~@s@
\item \texttt{elemAvail~~~~s~x}: Check if variable @x@ is in the set~@s@
\item \texttt{interAvail~~~s s'}: Intersect sets @s@ and @s'@
\item \texttt{smallerAvail~s s'}: Check if set~@s@ is smaller than @s'@
\end{itemize}
The implementations use analogous operations on @VarSet@s.

%%In~the lattice of available reloads (\figref{avail-lattice}),
%%the~join is computed by taking the intersection of two sets
%%of available reloads,
%%The join operation (@add@) returns a \emph{transaction} @aTx@
%%if the join has not yet reached a fixed point;
%%otherwise, it returns @noTx@ to indicate that the dataflow fact
%%did not change.
%%The bottom element of the lattice is the universe of all variables,
%%reflecting the initial assumption that all variables
%%have available reloads.
%%\john{Shouldn't it be @AvailRels@ instead of @AvailVars@?}



The most interesting part of the pass is the @middleAvail@ transfer
function in \figref{avail-transfers}.
\begin{itemize}
\item
The first case identifies an assignment that reloads local
variable~@x@ from its stack slot.\remark{I propose the compiler be
modified to use @isStackSlotOf@ as I've written. JD~approves.}
After such an assignment $@x@ = \slotof{\mathtt{x}}$, and no other variable
is affected, so @x@~is added to the set of available
variables.\remark{I'm not sure @agen@ and 
@akill@ are helping the exposition.}
\item
In the next case, an assignment to a local variable means that the
variable is no longer necessarily equal to the value in its stack
slot, so if @lhs@ is a local variable, it is removed from the set of
available variables.
Function @foldVarsDefd@ is an overloaded function which, in this
instance, calls @delFromAvail@ if @lhs@ is a local variable and does
nothing if @lhs@ is a hardware register.
\item 
In the other cases, comments and stores to memory don't affect the set
of available variables.
\footnote
{Although @MidStore@ may overwrite a stack slot \slotof x, GHC
carefully arranges that all stores to \slotof x have the form
$\slotof{\mathtt{x}}= @x@$.
These stores could be used to extend the set of available variables,
but it is not useful to do so.}
\remark{How do we know that @MidStore@ doesn't
destroy a stack slot??  I've put in a footnote but it will probably be
simpler to fix the code.}
\end{itemize}


The transfer function for a last node checks to see if the node is a
function call; if so, as for the foreign call, the set of
available variables is empty on every outgoing control-flow edge.
Other last nodes do not change values of variables or stack slots, 
so the set of available variables remains unchanged.
%
A~first node has no effect on program state, so its transfer function
is @flip const@.

%%Using the @agen@ and @akill@ functions, we define the transfer functions
%%for the available-reloads analysis (see~\figref{avail-transfers}):
%%\begin{itemize}
%%\item \emph{First nodes}:
%%  A first node cannot define a variable,
%%  so the set of available reloads is the same before and after a first node.
%%  We return the set unchanged using @flip const@.
%%\item \emph{Middle nodes}:
%%  If a middle node reloads a value from a register's slot on the stack (@RegSlot@),
%%  then we add the register the register to the set of available reloads.
%%  For any other assignment to a register, we remove the register from the
%%  set of available reloads.
%%  Similarly, because a function call can overwrite the value of any local variable,
%%  the set of available reloads is empty after a~function call.
%%  Any other middle node leaves the set of available reloads unchanged.
%%\item \emph{Last nodes}:
%%  If the last node is a function call, the outgoing set of available reloads
%%  is empty for every successor basic block.
%%  Otherwise, the last node cannot modify any variables,
%%  so the set of available reloads remains unchanged.
%%\end{itemize}

Given the lattice and the transfer functions,
we perform the available-reloads analysis by calling
the dataflow engine in the form of function @zdfSolveFwd@
(\figref{avail-running}).
The function @zdfFpFacts@ returns 
a finite map from basic-block IDs to the set of available reloads
at the beginning of each block.
Except for the implementations of the set operations on @AvailVars@,
\figref{avail} shows the \emph{entire} analysis.


\subsection{Liveness: a backward analysis} 

\seclabel{liveness}

The assertion computed by 
a backward dataflow analysis typically applies to a
\emph{continuation} at a program point, not to a state.
The classic example is liveness analysis;
the logical fact of interest is that at a particular program point,
the answer produced by the continuation does not depend on
the value of a particular variable~$x$.
If~so, $x$ is said to be \emph{dead} at that point.
If the answer produced by the continuation \emph{might} depend on the
value of~$x$, $x$~is \emph{live}.\footnote
{Liveness cannot be decided accurately; it reduces easily to the halting problem.
As usual, we approximate liveness by reachability.}

In a modern compiler, liveness analysis supports many program
transformations,
including
dead-assignment elimination,
which removes assigments to dead variables, 
and register allocation, which
ensures that if two variables are 
live at the same time, they are not assigned to the same register. 

The dataflow fact we use to represent liveness assertions is the set of
live variables.
The bottom element of the lattice is the empty set, and the join
operation is set union (\figref{live-lattice});
a~variable is deemed live if it is live on \emph{any} edge leaving a
node.

The transfer functions for liveness rely on two auxiliary functions
@addUsed@ and @remDefd@.
A~transfer function is given a set of variables live on the edges
going out of the node, and it removes from that set any variable
defined by the node, then adds to the set any variable used by the
node.
The~idea is that if a node has the assignment
\begin{verbatim}
  i = n - 1;
\end{verbatim}
then @i@ is not live just before the node, since if we start the
program just before the assignment @i = 0@, the answer cannot 
depend on the value of~@i@, which is about to be overwritten.
However, the answer might well depend on the value of~@n@, so
@n@~is considered live before the assignment.
If a variable appears on both left- and right-hand sides of an
assignment, as in
\begin{verbatim}
  i = i + 1;
\end{verbatim}
then the answer might well depend on~@i@, so @i@~is considered live
before the assignment.
For this reason the transfer functions in \figref{liveness} must
remove defined variables \emph{before} adding used variables.

For a last node, function @lastLiveOut@ consults the solution in
progress to find out what variables are live at the successors of a
last node. 
For an unconditional branch, we look up the live set at the label
branched to;
for a conditional branch, we look at both true and false edges, and
for a switch (computed goto), we consider every possible target of the
branch.
The~remaining case is a call, 
and since a call destroys the values of all local variables, the
only variables live just before a call are ones that might be used to
compute the address of the procedure being called, which are added by
@addUsed@ in @lastLiveness@.

Given the lattice and the transfer functions,
we perform the liveness analysis by calling
the dataflow engine in the form of function @zdfSolveBwd@
The function @zdfFpFacts@ returns 
a finite map from basic-block IDs to the set of live variables
at the beginning of each block.
\figref{avail} shows the \emph{entire} analysis.
(The overloaded functions
@foldVarsUsed@ and @foldVarsDefd@ are used throughout the back end and
should not be considered part of liveness analysis.)

%%  Each transfer function takes an instruction and
%%  the set of live registers in the instruction's continuation (the \liveout\ set);
%%  the result of the function is the set of live registers before the instruction.
%%  The standard procedure is to start with the set \liveout\,
%%  then remove each register defined by the instruction and
%%  add any register used by the instruction.
%%  In classic optimization literature, this procedure
%%  is~described in terms of @gen@ and @kill@ functions
%%  that add and remove registers from the live sets.
%%  
%%  Using the @gen@ and @kill@ functions, we define the 
%%  transfer functions for the liveness analysis as @liveTransfers@
%%  (see~\figref{live-transfers}):
%%  \begin{itemize}
%%  \item \emph{First nodes}:
%%    The set of live registers is the same before and after a first node,
%%    so we return the \liveout\ set unchanged using @flip const@.
%%  \item \emph{Middle nodes}:
%%    The set of live registers is determined by the @gen@ and @kill@
%%    functions, which are composed in @middleLiveness@.
%%  \item \emph{Last nodes}:
%%    Like a middle node, the set of live register is determined by
%%    the @gen@ and @kill@ sets, which are composed in @lastLiveness@.
%%    But because a last node may have multiple sucessors,
%%    we use the @lastLiveOut@ function to compute the set of registers that
%%    must be live in any continuation of the last node.
%%    For most last nodes, we take the union of the live sets from all of the successors.
%%    The exception is for call nodes: because a function call can overwrite any
%%    local register, there must not be any registers live out of a call site.
%%  \end{itemize}
%%  
%%  Finally, we can perform the liveness analysis by calling the dataflow framework's
%%  @zdfSolveFrom@ function with the lattice
%%  and transfer functions (see~\figref{live-running}).
%%  The function @zdfFpFacts@ returns the result of the analysis
%%  in the form of a map from basic-block IDs to the set of variables
%%  live at the beginning of each block.
%%  \john{Don't forget to go back and check consistency of names (e.g. s/CmmLive/Live/)}
%%  \john{I've dropped some sanity checking code.}


\ifgenkill
\section{Writing transfer functions using \texttt{gen} and \texttt{kill}}

\seclabel{gen-kill}

In the professional literature on optimization, it is common to specify
transfer functions by saying what dataflow facts are ``generated'' and
``killed'' by each node.
In~a forward analysis, for example an assignment might establish an
assertion (\texttt{gen}), or it might change state in such a way that an
assertion no longer holds (@kill@), or both.
If~you want to transliterate specifications that use @gen@ and @kill@,
it's easy.
In~fact the functions @addUsed@ and @remDefd@ in \figref{liveness}'s
liveness analysis correspond directly to the traditional @gen@ and
@kill@ functions.
In the available-variables analysis of \figref{avail}, @gen@ and
@kill@ can be defined as follows:
\begin{smallcode}
gen  :: UserOfLocalVars    a => a -> AvailVars -> AvailVars
kill :: DefinerOfLocalVars a => a -> AvailVars -> AvailVars
gen  a avail = foldVarsUsed extendAvail  avail a
kill a avail = foldVarsDefd delFromAvail avail a
\end{smallcode}
Using @gen@ and @kill@ entails no loss of efficiency;
for example, in @middleAvail@ in \figref{avail}, GHC~will identify and
inline the type-specific instance of @foldVarsUsed@, which for the
case of a local variable is the identity function, so @gen x avail@
reduces to @extendAvail avail x@.

\fi


\section{Using dataflow facts to rewrite graphs, with examples}

\seclabel{example-rewrites}

\begin{figure}
\begin{code}
type Rewrite mid last = Maybe (Graph mid last)
data ForwardRewrites mid last a = ForwardRewrites
 {fr_first  :: BlockId -> a -> Rewrite mid last,
  fr_middle :: mid     -> a -> Rewrite mid last,
  fr_last   :: last    -> a -> Rewrite mid last} 

data BackRewrites mid last a = BackRewrites
 {br_first  :: BlockId  -> a  -> Rewrite mid last,
  br_middle :: mid      -> a  -> Rewrite mid last,
  br_last   :: last ->
               (BlockId -> a) -> Rewrite mid last} 
\end{code}
\caption{Rewrite functions for forward and backward transformations.}
\figlabel{rewrites}
\end{figure}


\begin{figure*}
\begin{codetable}
\T\begin{code}
availRewrites :: ForwardRewrites Middle Last AvailVars
availRewrites = ForwardRewrites first middle last exit
  where first _ _ = Nothing
        middle m avail = maybe_reload_before avail m (mkMiddle m)
        last   l avail = maybe_reload_before avail l (mkLast l)
        exit _ = Nothing
        maybe_reload_before avail node tail =
            let used = filterVarsUsed (elemAvail avail) node
            in  if isEmptyVarSet used then Nothing
                else Just $ reloadTail used tail
        reloadTail vars t = foldl rel t $ varSetToList vars
          where rel t r = mkMiddle (reload r) <*> t
\end{code}\B
& Rewrite \mbox{functions}\\
\hline

\T\begin{code}
insertLateReloads :: (Graph Middle Last) -> DFMonad (Graph Middle Last)
insertLateReloads g = liftM zdfFpContents result
  where result = zdfRewriteFwd RewriteShallow "insert late reloads"
                               availVarsLattice avail_reloads_transfer
                               availRewrites (fact_bot availVarsLattice) g
\end{code}%
& Insert late reloads\\
\end{codetable}
\caption{Late-reload insertion, which relies on the analysis of \figref{avail}}
\figlabel{avail-rewrites}
\end{figure*}


We compute dataflow facts in order to enable code-improving
transformations.
When creating a transformation, the compiler writer uses
the assertions represented by dataflow facts to ensure that the
transformation preserves semantics.
We~write a transformation as a triple of
\emph{rewrite functions};
functions for both forward and backward transformations are shown in
\figref{rewrites}. 
%
A~rewrite function is given a dataflow fact and a node.
It~may choose to replace the node with a new graph~$g$, in which case it
returns $@Just@\;g$, or it may do nothing, in which case it returns @Nothing@.


To create a program transformation in our framework,
the compiler writer must 
\begin{itemize}
\item
Create a dataflow lattice and transfer functions for the supporting
analysis, as described in \secref{create-analysis}. 
\item
Create sound rewriting functions for first, middle, and last nodes;
it is sufficient that given the dataflow fact(s) coming into the node,
the behavior of 
any proposed replacement is not observably different from the original node.
\end{itemize}
Given the rewriting functions and the supporting analysis, the
compiler writer can then use the 
dataflow-engine function @zdfRewriteFwd@ to compute a solution:
\begin{code}
  zdfRewriteFwd 
    :: LastNode l             -- Can get successors
    => RewritingDepth         -- Rewrite recursively?
    -> PassName               -- Name of this pass
    -> DataflowLattice a      -- Lattice
    -> ForwardTransfers m l a -- Transfer functions
    -> ForwardRewrites m l a  -- Rewrite functions
    -> a                      -- Input fact
    -> Graph m l              -- Control-flow graph
    -> DFMonad (ForwardFixedPoint m l a (Graph m l))
\end{code}
%%  
%%  class DataflowSolverDirectiontransfers fixedpt =>
%%        DataflowDirection
%%          transfers fixedpt rewrites where
%%    zdfRewriteFrom :: (DebugNodes m l, Outputable a)
%%      => RewritingDepth    -- Recursive rewrites?
%%      -> BlockEnv a        -- Init facts
%%      -> PassName          -- Analysis name
%%      -> DataflowLattice a -- Lattice
%%      -> transfers m l a   -- Transfers
%%      -> rewrites m l a    -- Input fact
%%      -> a                 -- Input fact
%%      -> Graph m l         -- CFG
%%      -> DFMonad (fixedpt m l a (Graph m l))
%%
%%
The rewriting function is like the @zdfSolveFwd@ function in
\secref{zdfSolveFwd}, but it uses and produces extra
information.\seclabel{engine-truth} 
\begin{itemize}
\item
The @RewritingDepth@ parameter controls recursive rewriting;
if~a graph produced by a rewrite function cannot be further rewritten,
rewriting is \emph{shallow};
if~a graph produced by a rewrite function can be rewritten \emph{ad
infinitum}, rewriting is \emph{deep}.
Deep rewriting is essential to achieve the results of
\citet{lerner-grove-chambers:2002}, e.g., to remove the induction
variable from the loop in the example in \secref{induction-var-elim}.
\item
The rewriter requires rewriting functions as well as transfer
functions.
\item
The type constructor @ForwardFixedPoint@ has a fourth
type parameter,\footnote
{We lied to you earlier.}
which is a value contained in the fixed point.
The~value can be extracted using function @zdfFpContents@, which has
type @ForwardFixedPoint m l fact a -> a@.
Here the type parameter~@a@ is instantiated so that the fixed point
contains the rewritten graph;
in the solver, @a@~is instantiated with
the unit type~@()@.
\item
The computation is monadic in the \emph{dataflow monad}, written
@DFMonad@.
This monad provides a supply of fresh labels, and it
also helps implement the fault-isolation strategy invented by
\citet{whalley:isolation}.
Because they share substantial implementation in common, the truth
about the solver is that it also returns a value of monadic type.
\end{itemize}

In the rest of this section we present two transformations:
\secref{sink-reloads} shows how to insert a reload instruction just
before the first use of each spilled variable, and
\secref{dead-code-elim} shows how to eliminate dead assignments.
When these two transformations are run in sequence, the effect is to
sink reloads and produce programs like the example shown in
\secref{spill-reload-example}. 





%%  After defining the lattice, the transfer functions, and the rewrite functions,
%%  the client runs the analysis by invoking the dataflow framework
%%  (see~\figref{framework-fns}).
%%  The function @zdfSolveFrom@ performs an analysis on an input control-flow graph,
%%  using a dataflow lattice and a set of transfer functions.
%%  The additional arguments to the function provide
%%  the name of the analysis,
%%  the initial set of dataflow facts (usually empty),
%%  and the initial fact (usually bottom)
%%  that flows into either the entry or exit of the graph,
%%  depending on whether the transfers define a forward or backward analysis.
%%  The result of the function is the fixed point of the analysis,
%%  which stores the dataflow fact on entry to each basic block.
%%  \john{Maybe we should export a simple version of these functions to clients?
%%    Do they always do the obvious things with the initial facts and in-fact?
%%    Initial facts can reuse results of a previous analysis, but then you lose
%%    interleaving.}
%%  
%%  To combine an analysis and a transformation,
%%  the client calls the @zdfRewriteFrom@ function,
%%  which takes the same arguments as @zdfSolveFrom@,
%%  with the addition of the set of rewrite functions
%%  and a parameter (@RewritingDepth@) that decides whether the result
%%  of a rewrite function should be considered for further rewriting.
%%  The result of the function is not only the fixed point of the
%%  analysis interleaved with the transformation,
%%  but also the transformed control-flow graph.
%%  



\begin{figure*}
\begin{codetable}
\T\begin{code}
deadRewrites = BackwardRewrites nothing middleRemoveDeads nothing Nothing
  where nothing _ _ = Nothing

middleRemoveDeads :: Middle -> CmmLive -> Maybe (Graph Middle Last)
middleRemoveDeads (MidAssign (CmmLocal x) _) live
    | not (x `elemVarSet` live) = Just emptyGraph
middleRemoveDeads _ _ = Nothing
\end{code}\B
& Rewrite \mbox{functions}\\
\hline

\T\begin{code}
removeDeadAssignments :: (Graph Middle Last) -> DFMonad (Graph Middle Last)
removeDeadAssignments g = liftM zdfFpContents result
     where result = zdfRewriteBwd RewriteDeep "dead-assignment elim"
                                  liveLattice liveTransfers rewrites emptyVarSet g
\end{code}%
& \mbox{Dead-code} elimination\\
\end{codetable}
\caption{Dead-assignment elimination, which relies on the analysis of
\figref{liveness}} 
\figlabel{dead-elim}
\end{figure*}


\subsection{Sinking reloads: a forward transformation}

\seclabel{sink-reloads}

We can use the available-variables analysis of \secref{avail} to
insert reloads
immediately before uses of variables.
The transformation is implemented by the rewrite functions in the top
half of \figref{avail-rewrites}.
A~first node uses no variables and so is never rewritten.
For middle and last nodes, the @maybe_reload_before@ function
computes @used@, which is the set $\{ x \mid x = \slotof x\}$, i.e., 
the set of variables whose values are the same as the values in the
corresponding stack slots.
If that set is not empty, function
@reloadTail@ replaces @node@ with a new graph in which @node@ is
preceded by a (redundant) reload for each variable in the set~@used@.

To do the rewriting, the code uses several functions that create
graphs:
\begin{code}
mkMiddle ::               m -> Graph m l
mkLast   :: LastNode l => l -> Graph m l
(<*>)    :: Graph m l -> Graph m l -> Graph m l
\end{code}
The infix @<*>@ function is graph concatenation.

The transformation is implemented by the call to @zdfRewriteFwd@
shown at the bottom of \figref{avail-rewrites}.
Rewriting is shallow, which is to say that a graph returned by
@maybe_reload_before@ is not itself rewritten.
(If~it \emph{were} rewritten, an nonempty @used@ set would make the
compiler insert an infinite sequence of reloads before @node@.)
Once the reloads are inserted, the original reloads immediately
following the call site are dead, and they can be eliminated by our
next transformation, dead-assignment elimination.

\subsection{Dead-assignment elimination: a backward \rlap{transformation}}

\seclabel{dead-code-elimination}
\seclabel{dead-code-elim}

\seclabel{bwd-rewrite}


\def\liveout{$\mathit{live_{out}}$}

We use the liveness analysis of \secref{liveness} to identify
assignments which modify only variables that are not used.
Such \emph{dead assignments} can be removed without changing the
observable behavior of the program.
The removal is implemented by the rewrite functions in the top half of
\figref{dead-elim}. 
First and last nodes are not assignments and are therefore never
rewritten.
A~middle node is rewritten to the empty graph if and only if it is an
assignment to a dead variable.
In~the bottom half of \figref{dead-elim}, we call @zdfRewriteBwd@, and
that is all there is to it.
\john{Need to run this version of the code in anger.}
%
\remark{In this space we should have some guff about
composing transformations, which should refer to the example on
eliminating the induction variable.}


\ifseparateengine\else

\section{Implementing graphs}
\seclabel{graphs}

Our optimizer represents each procedure using a control-flow graph.
Our representation of control-flow graphs is
\begin{itemize}
\item
Purely applicative, which makes it exceptionally easy to compose
analyses and transformations as described in \secref{engine}
\item
Polymorphic, which enables us not only to reuse the graph for
different low-level intermediate languages, but which forces us to
distinguish generally useful dataflow algorithms from particular
realizations in~GHC
\item
Based on Huet's \citeyearpar{huet:zipper} \emph{zipper},
which makes it easy to adapt existing code improvements written in
imperative style
\end{itemize}
\citet{dias-ramsey:applicative-flow-graph} present our design in
detail, as well as discussing alternatives, advantages, and
disadvantages.
In~this paper we give a high-level view of the data structure, and we
emphasize a significant refinement: the introduction of polymorphism.

\subsection{Basic data structure}

A~basic block is a sequence beginning with a first node, continuing
with zero or more middle nodes, and ending in a last node.
A~first node contains only a unique identifier of type @BlockId@; the
types of middle and last nodes are parameters.
At~any given moment, the dataflow engine may \emph{focus} on a
particular edge, in which case 
it holds the source of that edge plus a
list of its predecessors all the way back to the first node,
and 
it holds the sink of that edge plus a
list of its successors all the way forward to the last node.
These values have types @ZHead m@ and @ZTail m l@, where @m@~and~@l@
are the types of middle and last nodes:
\begin{code}
data ZHead m   = ZFirst BlockId 
               | ZHead (ZHead m) m
data ZTail m l = ZLast (ZLast l) | ZTail m (ZTail m l)
\end{code}
The type @ZLast l@ extends~@l@ with an additional case, @LastExit@,
which represents a subgraph that ends not in a control transfer but by
``falling off the end.''

We~``modify'' a block by creating a new head and tail; to ``insert'',
``remove'', or ``mutate'' a node typically requires a couple of
allocations 
\cite{dias-ramsey:applicative-flow-graph}. 
With these operations it is easy to recast imperative graph-rewriting
code into a pure functional form.


When we are not focusing on a particular edge, we represent a basic
block by pairing its first node (a~@BlockId@ with a @ZTail@):
\begin{code}
data Block m l = Block BlockId (ZTail m l)
\end{code}
An entire graph is represented as a finite map from @BlockId@ to
block, together with the ID of the entry node:\footnote
{The representation of @BlockId@ is chosen so that not only is
  it efficient to create an infinite supply of @BlockId@s, but finite
  maps with @BlockId@ keys can be implemented using a Patricia tree,
  which is even more efficient than a balanced binary tree
  \cite{okasaki-gill:integer-map}.} 
\begin{code}
data Graph m l =
   Graph { g_entry  :: BlockId
         , g_blocks :: BlockEnv (Block m l) }
\end{code}
%%  
%%  A~graph has a single \emph{entry} and at most one \emph{default exit}.
%%  A~graph has a default exit, which we abbreviate just ``exit'', only if
%%  control can ``fall off the end.'' 
%%  A~graph has no exit if control leaves the graph only by an explicit
%%  procedure return or tail call;
%%  for example, the graph for a whole procedure  has no exit.
%%  The most common use of a single-entry, single-exit flow graph is as a
%%  replacement for a middle node during code improvement.

%%  Each control-flow graph is represented as a finite map from @BlockId@ to
%%  basic block, together with a distinguished @BlockId@ that marks the entry
%%  node.
%%  When a graph is ``being modified'',
%%  we \emph{focus} on one internal edge of one basic block.
%%  The focus is represented by a pair.
%%  One element of the pair points to the
%%  source of the edge, which is linked to its predecessor, and so on up
%%  to the block's first node.
%%  The other element of the pair points to the
%%  sink of the edge, which is linked to its successor, and so on down
%%  to the block's last node.

\subsection{Realization in GHC}

The two significant differences between the applicative flow graph
used in Quick~{\PAL} \cite{dias-ramsey:applicative-flow-graph} and the
refined version described in this paper are that the new version is
polymorphic, and the new version stores properties in separate finite
maps, not in mutable property lists.
%We use finite maps in order to avoid mutable reference cells, which
%require that computations be done in the @IO@~monad.
The change from propertly lists to finite maps is inconsequential,
affecting the algorithms in only minor ways and the structure of the
code not at all.
The change from a monomorphic to a polymorphic control-flow graph, by
contrast, has far-reaching implications.

Types related to control flow graph are polymorphic in two parameters:
the type of middle nodes and the type of last nodes.\footnote
{We considered abstracting over types associated with first nodes as
  well, but we preferred to restrict first nodes so that a first node
  carries a @BlockId@ and only a @BlockId@.
  This design gives us fewer type parameters and
  therefore fewer higher-order functions associated with those
  parameters.
  Because we can always use a finite map to associate data with
  each first node, we don't lose any expressive power.}
This design militates toward a modular implementation,
in which the implementation of the dataflow engine is 
decoupled from the representation of computations at individual nodes.
\begin{itemize}
\item
Module @ZipCfg@ exports data structures and algorithms that are
independent of the type of middle and last nodes.
However, in order to enable other algorithms to change the flow graph
without knowing the representation of a last node, @ZipCfg@ exports a
@LastNode@ type class which all last nodes must support.
Ths @LastNode@ type class expresses the minimum required of a type
that claims to repesent a control transfer:
it must be possible to
create a last node that branches unconditionally to a given @BlockId@ (goto);
to test to see if a last node is an unconditional branch, and if so, to
what target;
and to observe what @BlockIds@ designate possible successors of a last
node.
Operations that observe successors are extended to basic
blocks of type @Block m l@ and to values of type @ZTail m l@.

@ZipCfg@ exports a number of basic algorithms on graphs, including the
splicing algorithms described by
\citet{ramsey-dias:applicative-flow-graph}. 
The most important algorithm is postorder depth-first-search
traversal, which orders the basic blocks in a way such that iterative
dataflow analyses converge quickly.
As~a benevolent side effect, this traversal also prunes unreachable
code from the graph.
\item
Module @ZipCfgCmmRep@ depends on @ZipCfg@, but not the converse.
It~exports definitions of the middle- and last-node types needed to
represent GHC's low-level intermediate code, @Cmm@.
For convenience, it also exports instantiations of graph types,
and it exports instance declarations that make it easy to walk @Cmm@
nodes and find out what registers and stack slots are defined and
used.
\item
The \emph{representation} exported by
@ZipCfg@ and @ZipCfgCmmRep@ is useful primarily
for \emph{analyzing} flow graphs.
To~\emph{construct} a flow graph we use ``smart constructors'' which
produce monadic functions from graphs to graphs.
Using these constructors, GHC's front end creates large graphs by
composing smaller ones.

The smart constructors are inspired by Hughes's \citeyearpar{hughes:novel-lists}
representation of lists.
They are similar to the functions of type 
@zgraph -> zgraph@ described by
\citet{ramsey-dias:applicative-flow-graph}, 
but in our Haskell implementation, the function type is monadic and is
hidden from clients.
A~monadic type is necessary in order to plumb through an infinite supply
of @BlockId@ values.
When a client \emph{wants} to use a @BlockId@, for example, to translate
structured control flow into conditional and unconditional branches,
the graph-construction interface provides a constructor of type
analogous to $(\mathtt{BlockId} \arrow \mathit{graph}) \arrow \mathit{graph}$.
%% , as described in the companion paper.
%% \cite{dias-peyton:refactoring}. 
\end{itemize}
\fi


\ifseparateengine
\input{engine}
\else
\section{The Dataflow Engine}
\seclabel{engine}
\seclabel{dfengine}

The dataflow engine is implemented in two layers.
The lower layer is the \emph{dataflow monad}.
It~keeps track of the values of dataflow facts as the engine iterates.
The upper layer is divided into four parts:
a forward solver, a forward rewriter,
a backward solver, and a backward rewriter.

Despite the implicit claim in the title of this paper,
the dataflow engine is not simple.
The benefit of our design is that the \emph{interface} to the dataflow
engine (lattice, transfer functions, rewriting functions) is simple,
and as shown above, compiler passes written \emph{using} the engine
are very simple indeed.
But~the engine itself is complex.

Most of the complexity in the dataflow engine arises because we
implement the ambitious algorithm of
\citet{lerner-grove-chambers:2002}, who write
\begin{quote}
\emph{Previous efforts to exploit [the mutually beneficial
interactions of dataflow analyses] either (1)~iteratively performed
each individual analysis until no further improvements are discovered
or (2)~developed [handwritten] ``super-analyses'' that manually
combine conceptually separate analyses. We have devised a new approach
that allows analyses to be defined independently while still enabling
them to be combined automatically and profitably. Our approach avoids
the loss of precision associated with iterating individual analyses
and the implementation difficulties of manually writing a
super-analysis.}
\end{quote}
Adapting this work to a purely functional setting results in an
implementation that is significantly simpler than the original.
We~sketch that implementation below.


%%  Note that the dataflow engine is the only part of the system that is
%%  hard to get right---this is where all the hair is.
%%  Prime benefit of our system is that once this is right, everything is
%%  easy (and indeed is just logic, strongest postcondition, or weakest
%%  precondition). 
%%  



\subsection{The dataflow monad}

The primary purpose of the dataflow monad is to keep track of 
dataflow facts as the engine iterates.
Dataflow facts are found in three places:
\begin{itemize}
\item
There is a dataflow fact associated with every labelled basic block in
the current graph;
the dataflow monad maintains this association in a finite map.
The functions @getFact@ and @setFact@ query and update this map.
\item
The current graph may be a subgraph of a larger graph, in which case a
forward dataflow pass may produce dataflow facts that flow to labelled
blocks that are outside the current graph.
These facts must be retained and propagated even if the current graph
is abandoned; such facts are added with @addLastOutFact@ and recovered
with @bareLastOuts@.
\item
Finally, a foraward dataflow pass over a subgraph may propagate a fact forward by
``falling off the end;'' such a fact is set with @setExitFact@ and
recovered with @getExitFact@.
\end{itemize}
In addition to keeping track of facts, 
the dataflow monad provides a number of other facilities to manage
changes in state as graphs are rewritten and facts climb the dataflow
lattice:
\begin{itemize}
\item
The monad keeps track of whether any fact has changed.
\item
It provides a @subanalysis@ function which makes it possible to
 analyze a subgraph using the current set of facts, then discard any
 changes in state that may have resulted from the analysis of the
 subgraph.
\item
It provides a supply of fresh @BlockId@s, which are available for use
by rewrite functions.
\item
It tracks the supply of \emph{optimization fuel}.
As~shown below, when fuel runs out, the dataflow engine stops
calling rewriting functions, effectively halting optimization.
Binary search on the size of the fuel supply enables the compiler to
identify unsound rewrites quickly \cite{whalley:isolation}.
\end{itemize}


\subsection{The dataflow engine}

In implementing the dataflow engine, our primary tactic has been to
minimize the amount of duplicate or near-duplicate code.
To~that end, \emph{the dataflow engine implements only composed
analysis and transformation}.
Pure analysis is implemented as a special case in which no node is
ever rewritten.
As explained by \citet{lerner-grove-chambers:2002}, a~composed
analysis is implemented in two phases:
\begin{itemize}
\item
In the first phase, when a rewrite function proposes to replace a
node, the replacement graph is analyzed recursively, and the results
of that analysis are used as the new dataflow
fact(s) flowing out of the original node.
But \emph{the original node is not replaced}; indeed, the replacement
graph is abandoned, and only the facts remain.
If,~during iteration, the original node is analyzed again, perhaps
with a more conservative input fact, the rewrite function may propose
a different replacement or even no replacement at all.
This phase is called the \emph{solver}.
The solve computes a fixed point of the dataflow analysis
\emph{as if} nodes were replaced, while avoiding ever replacing a node
unsafely.
\item
Once the solver is complete, the resulting fixed point is sound,
and the facts in the fixed point are used by the second phase in which
each replacement proposed by a rewriting function is actually
performed.
This phase is called the \emph{rewriter}.
\end{itemize}

In \citeyear{ramsey-dias:applicative-flow-graph}, two of us
\citeauthor{ramsey-dias:applicative-flow-graph} presented
implementations in Objective Caml of a backward solver and rewriter.
Here, then, as a complement, we sketch implementations of the forward
solver and rewriter used in~GHC.


\begin{itemize}
\item
@fwd_pure_anal@ is @forward_sol@ passed the @squash@ function
@\ _ _ -> Nothing@.
It ignores its rewrite, depth, and fuel parameters.
\item
The internal @solve@ function is higher-order in the parameter
@finish@, which extracts from the dataflow monad either the unique
exit fact or the set of @LastOuts@, depending on context.
\item
The function @set_or_save@ calls @setFact@ for @BlockId@s located
within graph~@g@ and calls @addLastOutFact@ for @BlockId@s located
outside graph~@g@.
\end{itemize}

\fi



\section{The next 700 dataflow analyses}

\seclabel{next-700}


%%  \section{Logical view of optimization}
%%  
%%  Connection to Hoare logic:
%%   - facts derived by forward analysis as assertions on state
%%   - facts derived by backward analysis as assertions on continuation.
%%  
%%  Examples on board.

\seclabel{logic}


Dataflow analysis is closely related to the seminal work done by
\citet{floyd:assigning-meanings},
\citet{hoare:axiomatic-basis},
and
\citet{dijkstra:discipline}
on semantics of programming languages and
 formal methods of program construction.
%
We would like to elucidate the relationship between the formal methods a
person uses to 
\emph{construct} a new program with the formal methods a compiler uses
to \emph{analyze} a program that already exists.
Understanding the relationship is a bit tricky, because compilers and
people typically work in opposite directions.

The most highly developed
methodology for constructing a procedure (Dijkstra's) starts with a
postcondition~$Q$ that the procedure must establish and a
precondition~$P$ that the procedure may assume.
Using Dijkstra's method, a programmer 
works backwards, adding a statement, computing the weakest
precondition of that statement with respect to~$Q$,
and continuing with more statements until
eventually the weakest precondition of the procedure body is implied by~$P$.
A~compiler, by contrast, is given a procedure with no specification,
and the compiler typically reasons forward,  starting with the
weakest possible precondition, then using strongest postconditions to
compute assertions that hold at various points throughout the program.


Computing either strongest postconditions or weakest liberal
preconditions is a simple matter of calculation---except for loops.
Let's revisit the example of induction-variable elimination in
\secref{induction-var-elim}. 
If~a compiler wants to know what @i@~is, it can easily see that on the
first trip $@i@=0$, on the second trip $@i@=1$, and so on.
But it's all too easy for a compiler to get stuck trying to compute an
infinite disjunction like $\bigvee_{k=0}^{\infty} @i@=k$.
Compilers are no good at solving recursion
equations that require limits of infinite sequences.

People don't like infinite sequences either---instead they invent
\emph{loop invariants}. 
In the classic situation, using weakest preconditions, a loop
invariant~$I$ is an assertion that is \emph{stronger} than the weakest
precondition, is invariant under the loop, and when conjoined with
the loop's termination condition, implies the weakest precondition of
what follows the loop.
%%   and has these properties:
%%  \begin{itemize}
%%  \item
%%  Together with the loop-termination condition, the invariant~$I$ implies the weakest
%%  precondition of the code following the loop.
%%  \item
%%  The invariant~$I$ implies the weakest precondition of the loop body
%%  with respect to~$I$.
%%  In other words, $I$~is strong enought so that having $I$ hold at the
%%  beginning of the loop body is enough to
%%  imply that $I$~also holds at the end of the loop body.
%%  \end{itemize}
To be useful, a loop invariant must be neither too strong nor too
weak.
Much like finding a useful induction hypothesis for a proof, 
finding a loop invariant requires art and intuition.
In~all but the simplest cases, it is beyond the capabilities of any
compiler.

%%  Strongest postconditions also require a loop invariant, but with dual
%%  properties:
%%  \begin{itemize}
%%  \item
%%  The invariant~$I$ is weaker than the true strongest postcondition,
%%  but it is implied by the strongest postcondition of the code before
%%  the loop.
%%  \item
%%  Assuming invariant~$I$ holds on entry to the loop, the strongest
%%  postcondition of the loop body must imply~$I$.
%%  \item
%%  The strongest postcondition of the entire loop is deemed to be the
%%  conjunction of invariant~$I$ and the termination condition.
%%  \end{itemize}
%%  


So if we can't find loop invariants automatically, what's a poor
compiler writer to do?
The compiler writer wants assertions that justify interesting program
transformations. 
Such assertions can often be established by a dataflow analysis.
So to write a new dataflow analysis, a compiler writer
should \emph{invent a new logic} which is
\emph{expressive enough to justify interesting transformations}
but \emph{inexpressive enough that a fixed point
  is always reached in finitely many steps}.
With the logic in place, the transfer functions simply approximate
  weakest preconditions (for a backward analysis) or strongest
  postconditions (for a forward analysis) as best they can within the
  constraints of the logic.
Thus, the next 700 dataflow analyses will spring from 700 variations on
program logic, each of which is inexpressive in a different way.
\remark{Do we have examples or not?}

%%  Let's review the examples of \secref{example:xforms} in that light.
%%  \begin{itemize}
%%  \item
%%  Logic $\bigwedge_i x_i=k_i$.
%%  \begin{itemize}
%%  \item
%%  $i = 7 \join \true \equiv \true$ (no loss of information)
%%  \item
%%  $i = 7 \join i= 7 \equiv  i=7$ (no loss of information)
%%  \item
%%  $i = 7 \join i = 8 \implies \true$ (loss of information)
%%  \end{itemize}
%%  Because there are only finitely many variables, we can say only
%%  finitely many things at each program point, and we're guaranteed to
%%  reach a fixed point.
%%  \item
%%  Example: induction-variable elimination.
%%  \begin{itemize}
%%  \item
%%  What is the proposition?
%%  \item
%%  Key point: be able to express the intermediate state where the
%%  invariant is temporarily violated (first add 1 to @i@, then add 4
%%  to~@p@).
%%  \end{itemize}
%%  \end{itemize}


%\clearpage

\section{Conclusion}

Compiler textbooks make dataflow analysis and optimization appear
difficult and complicated.
We make dataflow simple not by using a single magic
ingredient, but by applying ideas that are well understood by functional
programmers and others who reason formally about programs.
These ideas
make it possible to think simple thoughts about classical code improvements.
\begin{itemize}
\item
We acknowledge only one program-analysis technique: the solution of
recursion equations.
Like our colleagues working in imperative languages, we solve
recursion equations by iterating to a fixed point.
Most equations relate
properties of program states; some relate properties of continuations.
\item
When looking at properties of program states, we consider only two
relations: weakest liberal precondition and strongest 
postcondition.
In the compiler literature, these relations correspond respectively to
``backward dataflow problems'' and ``forward dataflow problems.''
%%  \item
%%  In a language that admits loops, iterating weakest preconditions or
%%  strongest postconditions typically does not reach a fixed point in
%%  finitely many steps; hence the need for loop invariants
%%  \cite{hoare:axiomatic-basis,dijkstra:discipline,gries:science-programming}.
%%  In \secref{logic-reconciled}, we show that we can guarantee to reach a
%%  fixed point by limiting what we can express in the logic.\remark{needs
%%  a fix}
%%  We~show that many classical analyses can be explained this way;
%%  the great diversity of classical analyses corresponds to a great
%%  diversity of inexpressive logics.
%%  This view leads us to a unifying principle:
%%  \emph{To implement a code-improving transformation, find the least
%%    expressive logic that can justify the transformation, then use that
%%    logic to compute strongest postconditions, which justify the
%%    transformation locally.}
\item
We consider only three program transformation techniques:
substitution of equals for equals, 
insertion of assignments to unobserved variables, 
and removal of assignments to unobserved variables.
Substituting equals for equals may require reasoning about program
states; for example, if we have a program point at which variable~$x$
is always~7, we are justified in substituting~7 for~$x$.
\remark{We can also justify substitution of \emph{labels} in goto
  statements by reasoning about continuations.  The introduction is
  probably not the place to mention this fact.}
Inserting and removing assignments require reasoning about program
continuations; an assignment may be inserted or removed if its results
are not used by its continuation.

%%  Some compiler texts treat the removal of unreachable code as a
%%  code-improving transformation in its own right.
%%  In~our framework, unreachable code becomes unreachable in the
%%  garbage-collection sense, so no special effort is required to remove
%%  it.
\item
These simple program transformations may be composed to form more
complex tranformations.
For example, both ``code motion'' and ``induction-variable
elimination'' are implemented in three stages: insert new assignments;
substitute equals for equals; remove unneeded assignments
(\secref{induction-var-elim}). 

One virtue of implementing complex transformations by composing simple
transformations is that each simple transformation leaves the program
in a consistent state.
It~is therefore safe to use 
``optimization fuel'' to limit the number of \emph{simple}
transformations, which means that when we isolate a fault in the optimizer
(\secref{vpoiso}), we have the luxury of debugging a simple
 transformation, not a complex one.
\end{itemize}

We also blend proven implementation technqiues
in a way that
makes it possible to
write simple code
to implement classical code improvements.
\begin{itemize}
\item
To {analyze} programs, we use a purely applicative representation of
control-flow graphs, inspired by Huet's zipper
\cite{huet:zipper,ramsey-dias:applicative-flow-graph}. 
%
% important, but no longer mentioned in this paper:
%
%%  \item
%%  To \emph{construct} programs, we use a different representation of
%%  flow graphs, one which hides the complexity of the zipper and which
%%  provides a constant-time operation for joining flow graphs in
%%  sequence.
%%  It is inspired in part by Hughes's \citeyearpar{hughes:novel-lists}
%%  representation of lists, which supports a constant-time append operation.
\item
Improving on our own prior work, we make all flow-graph
types fully polymorphic in the representations of
assignments and control-flow operations.
%%  Although our polymorphic representations have been instantiated only
%%  with the low-level intermediate code used by the Glasgow Haskell
%%  Compiler, they are intended eventually to be instantiated with
%%  machine-dependent representations of target-machine instructions, as
%%  part of a larger project of refactoring GHC's back ends.
%
Making the control-flow graph polymorphic seems obvious in retrospect,
but we underestimated the degree to which polymorphism forces us to
separate concerns.
Even though at present the polymorphic types have but one instance
apiece, introducing polymorphism has made the code far simpler, easier
to understand, and easier to maintain.
%
% gen and kill are history
%
%%\item
%%Judicious use of Haskell type classes makes is possible to write
%%weakest precondition or strongest postcondition using the ``transfer
%%equations'' that are familiar from compiler textbooks.
%%If you like, you can even write overloaded @gen@ and @kill@ functions.
%%The benefit is that it is easy to compare the actual code with the
%%abstract treatments found in textbooks\ifgenkill \ (\secref{gen-kill})\fi.
\item
Finally, we use both polymorphism and type classes to implement a single,
polymorphic,
higher-order ``dataflow engine,'' which composes analyses and transformations
\cite{lerner-grove-chambers:2002}. 
By~putting the sophisticated algorithms in the dataflow engine, 
we make it very easy to create a new analysis or transformation:
create a lattice representation for the assertions that can be
expressed in the logic;
create transfer functions that approximate weakest preconditions or
strongest postconditions;
and 
create rewrite functions that use the assertions to justify
interesting program transformations.
\end{itemize}
These ideas and techniques form a powerful toolkit for
analyzing and transforming imperative programs.


\makeatother

\providecommand\includeftpref{\relax} %% total bafflement -- workaround
\IfFileExists{nrbib.tex}{\bibliography{cs,ramsey}}{\bibliography{cs,ramsey,simon,jd}}
\bibliographystyle{plainnatx}

\clearpage

\appendix

\section{Dataflow-engine functions}


\begin{figure*}
%%  forward_sol
%%          :: forall m l a . 
%%             (DebugNodes m l, LastNode l, Outputable a)
%%          => (forall a . Fuel -> Maybe a -> Maybe a)
%%  		-- Squashes proposed rewrites if there is
%%  		-- no more fuel; OR if we are doing a pure
%%  		-- analysis, so totally ignore the rewrite
%%  		-- ie. For pure-analysis the fn is (\_ _ -> Nothing)
%%          -> RewritingDepth	-- Shallow/deep
%%          -> PassName
%%          -> BlockEnv a		-- Initial set of facts
%%          -> ForwardTransfers m l a
%%          -> ForwardRewrites m l a
%%          -> a			-- Entry fact
%%          -> Graph m l
%%          -> Fuel
%%          -> DFM a (ForwardFixedPoint m l a (), Fuel)
\begin{code}
forward_sol squash rewrite name start_facts transfers rewrites = fixed_point
 where 
   fixed_point in_fact g fuel =
     do { setAllFacts start_facts
        ; (a, fuel) <- solve getExitFact in_fact g fuel
        ; facts <- getAllFacts
        ; let fp = ... facts ...
        ; return (fp, fuel)
        }

   solve :: DFM a b -> a -> Graph m l -> Fuel -> DFM a (b, Fuel)
   solve finish in_fact (Graph entry blockenv) fuel =
     let blocks = G.postorder_dfs_from blockenv entry
         set_or_save = mk_set_or_save (isJust . lookupBlockEnv blockenv)
         set_successor_facts (Block id _ tail) fuel =
           do { idfact <- getFact id
              ; (last_outs, fuel) <-
                  case squash fuel $ fr_first rewrites id idfact of
                    Nothing -> solve_tail (ft_first_out transfers id idfact) tail fuel
                    Just g -> do { g <- areturn g
                                 ; (a, fuel) <- subAnalysis' $
                                     case rewrite of
                                       RewriteDeep -> solve getExitFact idfact g (oneLessFuel fuel)
                                       RewriteShallow ->
                                         do { a <- anal_f getExitFact idfact g
                                            ; return (a, oneLessFuel fuel) }
                                  ; solve_tail a tail fuel }
              ; set_or_save last_outs
              ; return fuel }

     in do { (last_outs, fuel) <- solve_tail in_fact entry fuel
           ; set_or_save last_outs                                    
           ; fuel <- run "forward" name set_successor_facts blocks fuel
           ; b <- finish
           ; return (b, fuel)
           }

   solve_tail in' (G.ZTail m t) fuel =
     case squash fuel $ fr_middle rewrites m in' of
       Nothing -> solve_tail (ft_middle_out transfers m in') t fuel
       Just g -> do { g <- areturn g                                                  
                    ; (a, fuel) <- subAnalysis' $                                     
                         case rewrite of                                              
                           RewriteDeep -> solve getExitFact in' g (oneLessFuel fuel)  
                           RewriteShallow -> do { a <- anal_f getExitFact in' g       
                                                ; return (a, oneLessFuel fuel) }      
                    ; solve_tail a t fuel                                             
                    }

   solve_tail in' (G.ZLast l) fuel = 
     case squash fuel $ either_last rewrites in' l of
       Nothing -> case l of LastOther l -> return (ft_last_outs transfers l in', fuel)
                            LastExit -> do { setExitFact in' ; return (LastOuts [], fuel) }
       Just g -> do { g <- areturn g                                                  
                    ; (last_outs :: LastOuts a, fuel) <- subAnalysis' $           
                        case rewrite of                                               
                          RewriteDeep -> solve lastOutFacts in' g (oneLessFuel fuel)  
                          RewriteShallow -> do { los <- anal_f lastOutFacts in' g     
                                               ; return (los, fuel) }                 
                    ; return (last_outs, fuel)                                        
                    }

   anal_f :: DFM a b -> a -> Graph m l -> DFM a b
   anal_f finish in' g = do { fwd_pure_anal name emptyBlockEnv transfers in' g; finish }
   either_last rewrites in' (LastExit) = in'
   either_last rewrites in' (LastOther l) = fr_last rewrites l in'
\end{code}
\caption{The forward solver}
\end{figure*}

\begin{figure*}
%%  forward_rew
%%          :: forall m l a . 
%%             (DebugNodes m l, LastNode l, Outputable a)
%%          => (forall a . Fuel -> Maybe a -> Maybe a)
%%          -> RewritingDepth
%%          -> BlockEnv a
%%          -> PassName
%%          -> ForwardTransfers m l a
%%          -> ForwardRewrites m l a
%%          -> a
%%          -> Graph m l
%%          -> Fuel
%%          -> DFM a (ForwardFixedPoint m l a (Graph m l), Fuel)
\begin{code}
forward_rew squash depth xstart_facts name transfers rewrites in_factx gx fuelx = fixed_pt_and_fuel
  where
    fixed_pt_and_fuel =
        do { (a, g, fuel) <- rewrite xstart_facts getExitFact in_factx gx fuelx
           ; facts <- getAllFacts
           ; let fp = ... facts ... g ...
           ; return (fp, fuel)
           }
    solve = forward_sol squash
    rewrite :: BlockEnv a -> DFM a b -> a -> Graph m l -> Fuel -> DFM a (b, Graph m l, Fuel)
    rewrite start finish in_fact g fuel =
      let Graph entry blockenv = g
          blocks = G.postorder_dfs_from blockenv entry
      in do { solve depth name start transfers rewrites in_fact g fuel
            ; eid <- freshBlockId "temporary entry id"
            ; (rewritten, fuel) <- rew_tail (ZFirst eid emptyStackInfo) in_fact entry emptyBlockEnv fuel
            ; (rewritten, fuel) <- rewrite_blocks blocks rewritten fuel
            ; a <- finish
            ; return (a, lgraphToGraph (LGraph eid 0 rewritten), fuel)
            }
    don't_rewrite facts finish in_fact g fuel =
        do  { solve depth name facts transfers rewrites in_fact g fuel
            ; a <- finish
            ; return (a, g, fuel)
            }
    inner_rew :: DFM a f -> a -> Graph m l -> Fuel -> DFM a (f, Graph m l, Fuel)
    inner_rew f i g fu = getAllFacts >>= \facts -> inner_rew' facts f i g fu
        where inner_rew' = case depth of RewriteShallow -> don't_rewrite
                                         RewriteDeep    -> rewrite
    rewrite_blocks :: [Block m l] -> (BlockEnv (Block m l)) -> Fuel -> DFM a (BlockEnv (Block m l), Fuel)
    rewrite_blocks [] rewritten fuel = return (rewritten, fuel)
    rewrite_blocks (G.Block id off t : bs) rewritten fuel =
      do { let h = ZFirst id off
         ; a <- getFact id
         ; case squash fuel $ fr_first rewrites id a of
             Nothing -> do { (rewritten, fuel) <- rew_tail h (ft_first_out transfers id a) t rewritten fuel
                           ; rewrite_blocks bs rewritten fuel }
             Just g  -> do { markGraphRewritten
                           ; g <- areturn g
                           ; (outfact, g, fuel) <- inner_rew getExitFact a g fuel
                           ; let (blocks, h) = splice_head' h g
                           ; (rewritten, fuel) <- rew_tail h outfact t (blocks `plusBlockEnv` rewritten) fuel
                           ; rewrite_blocks bs rewritten fuel }
         }

    rew_tail head in' (G.ZTail m t) rewritten fuel =
      case squash fuel $ fr_middle rewrites m in' of
        Nothing -> rew_tail (G.ZHead head m) (ft_middle_out transfers m in') t rewritten fuel
        Just g -> do { markGraphRewritten
                     ; g <- areturn g
                     ; (a, g, fuel) <- inner_rew getExitFact in' g fuel
                     ; let (blocks, h) = G.splice_head' head g
                     ; rew_tail h a t (blocks `plusBlockEnv` rewritten) fuel }
    rew_tail h in' (G.ZLast l) rewritten fuel = 
      case squash fuel $ either_last rewrites in' l of
        Nothing -> return (insertBlock (zipht h (G.ZLast l)) rewritten, fuel)
        Just g -> do { markGraphRewritten
                     ; g <- areturn g
                     ; ((), g, fuel) <- inner_rew (return ()) in' g fuel
                     ; let g' = G.splice_head_only' h g
                     ; return (G.lg_blocks g' `plusBlockEnv` rewritten, fuel) }
    either_last rewrites in' (LastExit) = in'
    either_last rewrites in' (LastOther l) = fr_last rewrites l in'
\end{code}
\caption{The forward rewriter}
\end{figure*}






\end{document}
