<commit_before>\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{<NAME>}{Tufts University}{<EMAIL>}
\authorinfo{<NAME>}{Tufts University}{<EMAIL>}
\authorinfo{<NAME>}{Microsoft Research}{<EMAIL>}


\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<commit_msg>Comitting those of Simon's changes that we wish to keep.<commit_after>\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{<NAME>}{Tufts University}{<EMAIL>}
\authorinfo{Jo\~<NAME>}{Tufts University}{<EMAIL>}
\authorinfo{<NAME>}{Microsoft Research}{<EMAIL>}


\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 
(\secref{zdfSolveFwd}).
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$ \simon{I'm hazy about when you
want to say ``fact'' and when  you want to say ``assertion'', or indeed
if you intend to distinguish the two at all.}:
\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 client must choose how to represent these assertions. In this
case, remembering the the assertion at each edge is a conjunction of assertions
about each in-scope variable, an appropraite choice might be a finite mapping
\begin{code}
  type CPFact = Data.Map Var (Maybe Const)
\end{code}
If the variable $x$ is not in the domain of the map, then $x=\bot$;
if it maps to @Nothing@ then $x=\top$; if it maps to $(@Just@~k)$ then
$x=k$.

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} \seclabel{tffuns}

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?}

First nodes are the only targets of control transfers;
middle nodes never perform control transfers;
and last nodes always perform control transfers.
Hence, 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.  
\simon{Notice that although the
library fixes the \emph{structure} of the graph, it is the client that
specifies the \emph{content} of middle and last nodes.}
\norman{We are having trouble understanding SLPJ's obsession with distinguishing the ``client'' (an entity we wish not to name) from the ``library.''}


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.\norman{It is not @flip const@ when we do the proc-point
analysis, but I am not exactly sure how to work this information into
the text.}  
\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@$?}
\simon{I don't think so.  What is $f$?}
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
{'fraction_non_alphanumeric': 0.09151851343669758, 'fraction_numerical': 0.009487033733853421, 'mean_word_length': 4.3377275580665415, 'pattern_counts': {'":': 0, '<': 17, '<?xml version=': 0, '>': 75, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '5669257', 'n_tokens_mistral': 15573, 'n_tokens_neox': 14593, 'n_words': 6514}