
\chapter{Transformations of Delayed Transfers of Control}
\label{ch-delay}

{\small
\begin{flushright}
Design: Norman and Cristina [c.98]; Implementation: Mike [c.98-99]; Documentation: Norman, Cristina [Sep 99]
\end{flushright}
}

This chapter is an updated version of Technical Report 440, Department of 
Computer Science and Electrical Engineering, The University of 
Queensland, December 1998.  A more up to date version, including 
application of this algorithm to the removal of PA-RISC delayed branches
will be part of a Sun Microsytems Laboratories Technical Report series  
(expected, early 2002). 
 

% l2h ignore special {% ===> this file was generated automatically by noweave --- better not edit it

%\ifx\afour\undefined
%  \documentclass[letterpaper]{elsart}
%  \let\sizeinfo\relax
%\else 
%  \documentclass[a4paper]{elsart}
%  \special{papersize=210mm,297mm} % put dvips into a4 automagically
%  \def\sizeinfo{A4 }
%\fi

%\usepackage{nchicago}

% l2h substitution bullet *
% l2h substitution and and
% l2h ignore active


\makeatletter
\def\@citex[#1]#2{%
  \let\@citea\@empty
  \@cite{\@for\@citeb:=#2\do
        {\@citea\def\@citea{,\penalty\@m\ }%
         \edef\@citeb{\expandafter\@firstofone\@citeb}%
         \if@filesw\immediate\write\@auxout{\string\citation{\@citeb}}\fi
         \@ifundefined{b@\@citeb}{\mbox{\reset@font\bfseries ?}%
           \G@refundefinedtrue
           \@latex@warning
             {Citation `\@citeb' on page \thepage \space undefined}}%
           {\citebox{\csname b@\@citeb\endcsname}}}}{#1}}
\let\citebox\hbox
\makeatother

\renewcommand\gets{\mathrel{:=}}

\newcommand\opentab{\addtolength{\extrarowheight}}
% l2h ignore catcode ==
% l2h let gdef def

% l2h substitution hatform ^
% l2h ignore markboth {{

% l2h ignore opentab {

% l2h substitution presigmap sigma'
% l2h ignore productionglue
% l2h substitution qquad &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;

\newif\iffullpaper
\fullpapertrue


% l2h argblock calexp E[ ]
% l2h argblock cmd E[ ]


\newcommand\calexp[1]{{\mathcal E}[\![#1]\!]}
\newcommand\cmd[1]{{\mathcal C}[\![#1]\!]}
\newcommand\pc{\mathit{PC}}

%\usepackage{array,tabularx,grammar}

% l2h letenv production quote

\newif\iftr
\trfalse % this is not the tech report

\newcolumntype{Y}{>{\raggedright\arraybackslash}X}


%\usepackage{noweb}
\let\originalprime='
\def\setupcode{\catcode`\ =10 \catcode`\'=12 \mathcode`\'="8000 \regressprime}
{\catcode`\'=\active 
 \makeatletter
 \gdef\regressprime{\def'{^\bgroup\prim@s}}
}
\let\Tt\relax


% l2h substitution div div
% l2h substitution mod mod

\overfullrule=10pt

\noweboptions{shortxref}
\def\nwdocspar{\vskip0pt plus1.5in\penalty-400\vskip0pt plus -1.5in}
%\def\nwdocspar{\par\penalty-1000}
\def\nwendcode{\endtrivlist\endgroup} % ditches filbreak
%\def\nwendcode{\endtrivlist\endgroup\vskip\nwextraglue} % page tuning

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

\newcommand\sfilbreak[1]{\vskip 0pt plus#1\penalty-200\vskip 0pt plus -#1}

\setcounter{secnumdepth}{2}

\let\orghbox=\hbox
\newcommand\nohbox{\let\hbox=\orghbox\relax}



%% \pagestyle{myheadings}
%% \catcode`\$=10 % make $ a blank space
%% \catcode`\:=10 % make : a blank space
%% \newcommand\rcsrevision{$Revision: 1.4 $}
%% \catcode`\$=3 % dollar sign is math shift
%% \catcode`\:=12
%% \markboth{\rcsrevision: \sizeinfo Draft of \today}{\rcsrevision: \sizeinfo Draft of \today}
%% 
%% \pagestyle{plain}

\def\remark#1{\marginpar{\raggedright\hbadness=10000
        \def\baselinestretch{0.8}\scriptsize
        \it #1\par}}

\let\hatform\overline

\let\nwpphat=\hatform

The fundamental steps in binary translation are
distinguishing code from data, mapping data from source to
target, and translating instructions.
Translating instructions presents few problems, except
when the source instruction set 
has features not present in typical compiler intermediate codes.
The most common such feature is the delayed branch.

Standard code-generation technology can handle delayed branches in the
target language, but not in the source.
Translating delayed branches can involve tricky case
analyses to figure out what happens if there is a branch instruction in
a delay slot.
This chapter presents a disciplined method for deriving such case analyses.
The method identifies problematic cases,
shows the translations for the non-problematic cases, and gives
confidence that all cases are considered.
The method also applies to other tools that analyze machine instructions.

We begin by writing a very simple interpreter for the source machine.
It specifies, at the register-transfer level, how the source machine
executes instructions, including delayed branches. We then transform
the interpreter into an interpreter for a target machine without
delayed branches.
To maintain the semantics of the program being interpreted, we 
simultaneously transform the sequence of source-machine instructions
into a sequence of target-machine instructions.
The transformation of the instructions becomes our
algorithm for binary translation.

We show the translation is correct by using a correspondence between
source and target states, and showing if the source and target
machines begin execution in corresponding states, they reach new
corresponding states in a few instructions.


\renewcommand\opencite[1]{{\let\citebox=\relax\cite{#1}}}

A quick reading of this chapter might suggest that the problem we solve
is trivial.
To build a flow graph representing a binary program,
why not simply convert the delayed branch to a non-delayed branch and
push the instruction in the delay slot along zero, one, or both
sucessor edges?
(The set of successors that should get copies of the instruction in
the delay slot depends on whether the delayed branch
``annuls'' that instruction.)
This simple approach is in fact correct, \emph{except} when the
instruction in the delay slot is itself a delayed branch.
In that case, the ``pushing'' approach fails to execute the
instruction that is the target of the first branch.
The methods in this paper translate this case correctly.
In practice, such cases occur rarely in user code, but they are
recommended in kernel code as a way of returning from interrupts or
otherwise switching contexts \cite[\S B.26]{sparc:architecture}.


\section{Semantic framework}

Rather than translate source-machine instructions directly into target-machine
instructions, we translate source instructions into register transfer
lists (RTLs), transform the RTLs, optimize the RTLs, and translate the
RTLs into target-machine instructions.
RTLs provide a uniform framework that can express source instructions,
target instructions, and their interpretations by the source and
target processors.

\subsection{Register transfer lists}

Our RTL formalism is designed for use in tools and component
generators, and it makes machine-dependent
computation explicit \opencite{ramsey:embedded}.
For this paper, we use a simplified version specified using an imperative syntax:
\begin{production}{rtl}%figure
\optional{\nt{effect} \sequence{\lit\vbar\ \nt{effect}}}
&Multiple assignment
\end{production}
\productionglue
\begin{production}{effect}%figure
\optional{\nt{exp} {{\Tt{}\(\mathbin{\rightarrow}\)}}} \nt{location} := \nt{exp}&
Guarded assignment
\end{production}
\productionglue
\begin{production}{exp}%figure
\term{constant}&Constant
| \nt{location}&Fetch from a location
| \nt{exp} \nt{binop} \nt{exp}&Binary RTL operator
| \nt{operator} \lit( \nt{explist} \lit)&RTL operator
\end{production}
A register transfer list is a list of guarded effects.
Each effect represents the transfer of a value into a storage
location,\footnote{Storage locations represent not only memory but
also registers and other processor state.}
 i.e., a store
operation.
The transfer takes place only if the guard (an expression) evaluates
to \textbf{true}.
Effects in a list take place simultaneously, as in
Dijkstra's multiple-assignment statement; an RTL represents a single
change of state.
%%For example, one RTL can specify a swap instruction without
%%introducing bogus temporaries.

Values are computed by expressions without
side effects.
Eliminating side effects simplifies analysis and transformation.
Expressions may be integer constants, fetches from locations, or
applications of \emph{RTL operators} to lists of expressions.
RTL operators are pure functions on values.

For purposes of this paper, we assume that locations are single cells
in a mutable store, although the RTL formalism supports a more general
view that makes byte order explicit.
\iffalse
Locations may be single cells or aggregates of consecutive
cells within a storage space.
Aggregation generalizes the idea of byte order, specifying a bijection
between a contiguous sequence of $k$ $n$-bit values and a single
$w$-bit value, where $w = kn$.\footnote{$w$ and $n$ are mnemonic for
``wide'' and ``narrow.''}
\fi

\iffullpaper
As an example of a typical RTL, consider a SPARC load instruction
using the displacement 
addressing mode, written in the SPARC  assembly language as
\begin{verbatim}
  ld [%sp-12], %i0
\end{verbatim}
The effect of this load instruction might be written
\nwenddocs{}\nwbegincode{2}\moddef{RTL for sample instruction}\endmoddef\nwstartdeflinemarkup\nwenddeflinemarkup
\(\$r[24] \mathrel{:=} \$m[\$r[14]+{\mathit{sx}}(\mathord{-}12)]\)
\nwendcode{}\nwbegindocs{3}because the stack pointer is register~14 and register \texttt{\%i0} is
register~24.
The notation {\Tt{}\(\$\)}\emph{space}\texttt{[}\emph{address}\texttt{]}
specifies a cell in a mutable store.
The {\Tt{}\({\mathit{sx}}\)} operator sign-extends the 13-bit immediate constant {\Tt{}\(\mathord{-}12\)}
so it can be added to the 32-bit value fetched from register~14.

The load instruction not only loads a value into register~24; it also advances
the program counter to point to the next instruction.
Changing the program counter is intimately connected with branching;
we separate the effect on the
program counter in order to give it special treatment.
\else
\emph{The full paper shows and explains an example RTL.}
\fi

\subsection{Processor state for delayed branches}

A processor executing straight-line code executes one instruction
after another, in sequence.
A delayed-branch instruction causes the processor to depart from that
sequence, but not immediately.
When the processor executes an instruction~{\Tt{}\(I\)} that causes a delayed
branch to a location 
{\Tt{}\({\mathit{target}}\)}, the processor {first} executes {\Tt{}\(I\)}'s successor,
{then} executes the instruction located at {\Tt{}\({\mathit{target}}\)}.
The location holding {\Tt{}\(I\)}'s successor is called {\Tt{}\(I\)}'s ``delay
slot.''
On some machines, like the SPARC,
the instruction~{\Tt{}\(I\)} can
``annul'' its successor, in which case the successor is
\emph{not} executed, but instead the processor stalls for a cycle
before transferring control to {\Tt{}\({\mathit{target}}\)}.

To model delayed branches with annuls, we use
three pieces of processor state:
\begin{itemize}
\item[{}{\Tt{}\({\mathit{PC}}\)}{}] is the program counter, which identifies the
instruction about to be executed.
\item[{}{\Tt{}\({\mathit{nPC}}\)}{}] is the ``next program counter,'' which identifies the
instruction to be executed after the current instruction.
\item[{}{\Tt{}\({\mathit{annul}}\)}{}] is the ``annul status,'' which determines
whether the processor executes the instruction at~{\Tt{}\({\mathit{PC}}\)} or ignores
it.%
\footnote{\iffullpaper
It is crucial to distinguish the {\Tt{}\({\mathit{annul}}\)} status, which is
part of 
the processor state, from the \texttt{a}~bit found in the binary
representations of some branch instructions.
The interpretation of the {\Tt{}\({\mathit{annul}}\)} status is trivial: it tells
directly whether to execute an instruction.
The interpretation of the \texttt{a}~bit (when present) is more involved,
because there are special rules for some instructions.
We abstract away from these special rules by associating with each
instruction~{\Tt{}\(I\)} a predicate~{\Tt{}\(a_I\)} (not necessarily a single bit) that
tells the processor 
whether to annul the instruction's successor.
\else
\emph{The full paper notes the distinction between {\Tt{}\({\mathit{annul}}\)} and the
\texttt{a}~bit found in some branch instructions.}%
\fi
}
\end{itemize}
In this model, a delayed control transfer is represented by an
assignment to~{\Tt{}\({\mathit{nPC}}\)}.
For example, a SPARC call instruction simultaneously
assigns the target address to~{\Tt{}\({\mathit{nPC}}\)}
and the current {\Tt{}\({\mathit{PC}}\)} to register~15:
\nwenddocs{}\nwbegincode{4}\moddef{RTL for call}\endmoddef\nwstartdeflinemarkup\nwenddeflinemarkup
\({\mathit{nPC}} \mathrel{:=} {\mathit{target}} \mathrel{|} \$r[15] \mathrel{:=} {\mathit{PC}}\)
\nwendcode{}\nwbegindocs{5}The {\Tt{}\({\mathit{target}}\)} address in the semantics is
distinct from the \texttt{target} field in the binary representation of the
call instruction.
In the case of the SPARC, we abstract away from the rule that says the
target 
address is computed by extending the \texttt{target} field on the
right with zeroes.

A call transfers control unconditionally; we represent a conditional
branch by a guarded assignment to {\Tt{}\({\mathit{nPC}}\)}.
The \texttt{BNE} (branch not equal) instruction tests the {\Tt{}\(Z\)}~(zero)
bit in the condition codes:
\nwenddocs{}\nwbegincode{6}\moddef{rtl for conditional branch \texttt{BNE}}\endmoddef\nwstartdeflinemarkup\nwenddeflinemarkup
\(\lnot  Z \mathbin{\rightarrow} {\mathit{nPC}} \mathrel{:=} {\mathit{target}}\)
\nwendcode{}\nwbegindocs{7}Again we abstract the computation of the target address relative to
the location of the instruction.
\nwenddocs{}\nwbegindocs{8}\nwdocspar
\subsection{A canonical form of RTLs}
To isolate the part of instruction semantics that is relevant to
control flow, we put RTLs into the following canonical form:
\nwenddocs{}\nwbegincode{9}\moddef{RTL for generic instruction \code{}I\edoc{}}\endmoddef\nwstartdeflinemarkup\nwenddeflinemarkup
\(b_I \mathbin{\rightarrow} {\mathit{nPC}} \mathrel{:=} {\mathit{target}}_I \mathrel{|} {\mathit{annul}} \mathrel{:=} a_I \mathrel{|} I_c\)
\nwendcode{}\nwbegindocs{10}We interpret this form as follows:
\begin{itemize}
\item [{}{\Tt{}\(b_I\)}{}] is a predicate that tells whether {\Tt{}\(I\)}~branches.
It is an \emph{expression}, not a constant or a field of the
instruction.
For non-branching instructions, {\Tt{}\(b_I\)}~is {\Tt{}\(\textbf{false}\)}.
For calls and
unconditional branches, {\Tt{}\(b_I\)} is {\Tt{}\(\textbf{true}\)}.
For conditional branches, {\Tt{}\(b_I\)} is some other expression, the value of
which depends on the state of the machine (e.g., on the values of
the condition codes).
\item [{}{\Tt{}\({\mathit{target}}_I\)}{}] is an {expression} that identifies the
target address to which {\Tt{}\(I\)}~may branch.
(If {\Tt{}\(b_I\)} is {\Tt{}\(\textbf{false}\)}, {\Tt{}\({\mathit{target}}_I\)} is arbitrary.)
For calls and PC-relative branches, {\Tt{}\({\mathit{target}}_I\)} is a constant that
statically identifies a target address.
For indirect branches, {\Tt{}\({\mathit{target}}_I\)} may be a more complex expression,
e.g., one that fetches an address stored in a register.
\item [{}{\Tt{}\(a_I\)}{}] is a predicate that tells whether {\Tt{}\(I\)}~annuls its
successor. 
It is an expression, {not} the value of the \texttt{a}~bit in an
instruction's representation.
For most instructions, {\Tt{}\(a_I\)} is {\Tt{}\(\textbf{false}\)}.
For conditional branches, {\Tt{}\(a_I\)} may be more complicated.
For example,  the SPARC \texttt{BNE} instruction annuls its successor
if the \texttt{a} bit is set and if the branch is not taken, so {\Tt{}\(a_I\)} is
\mbox{{\Tt{}\(\mathtt{a} \ne  0 \land  Z\)}}.
\item [{}{\Tt{}\(I_c\)}{}] is an RTL that represents {\Tt{}\(I\)}'s ``computational
effect.''
{\Tt{}\(I_c\)} may be empty, or it may contain guarded assignments that do
not change {\Tt{}\({\mathit{annul}}\)}, {\Tt{}\({\mathit{nPC}}\)}, or {\Tt{}\({\mathit{PC}}\)}.
Typical RISC instructions change control flow or perform computation,
but not both, so {\Tt{}\(I_c\)} tends to be non-empty only when {\Tt{}\(b_I\)}
and {\Tt{}\(a_I\)} are {\Tt{}\(\textbf{false}\)}.
On CISC architectures, however, an instruction like ``decrement and
skip if zero'' might have both  non-empty {\Tt{}\(I_c\)} (the decrement) and
a nontrivial {\Tt{}\(b_I\)} (the test for zero).
\end{itemize}
An instruction can be expressed in this canonical form if, when
executed, it branches to
at most one {\Tt{}\({\mathit{target}}\)}.%
\footnote{And of course if the machine uses delayed branches.}
This is true of all instructions on all architectures with which we
are 
familiar, including indirect-branch instructions (although the value
 of {\Tt{}\({\mathit{target}}\)} may be different on different executions of an indirect
branch).

Here are a few example RTLs in canonical form;
SPARC assembly language appears on the left, RTLs on the right.
{\Tt{}\textbf{skip}} is the empty~RTL.
\begin{quote}%figure
\begin{tabular}{@{}ll@{}}
\multicolumn2{@{}l}{\texttt{add rs1, rs2, rd}}\\
\multicolumn2{@{}l}{\qquad  
{\Tt{}\(\textbf{false} \mathbin{\rightarrow} {\mathit{nPC}} \mathrel{:=} {\mathit{any}} \mathrel{|} {\mathit{annul}} \mathrel{:=} \textbf{false} \mathrel{|} \$r[\mathtt{rd}] \mathrel{:=} \$r[\mathtt{rs1}] + \$r[\mathtt{rs2}]\)}}\\
\texttt{ba,a addr}&{\Tt{}\(\textbf{true} \mathbin{\rightarrow} {\mathit{nPC}} \mathrel{:=} \mathtt{addr} \mathrel{|} {\mathit{annul}} \mathrel{:=} \textbf{true} \mathrel{|}\){\ }\textbf{skip}}\\
\texttt{call addr}&{\Tt{}\(\textbf{true} \mathbin{\rightarrow} {\mathit{nPC}} \mathrel{:=} \mathtt{addr} \mathrel{|} {\mathit{annul}} \mathrel{:=} \textbf{false} \mathrel{|} \$r[15] \mathrel{:=} {\mathit{PC}}\)}\\
\end{tabular}\kern-20pt
\end{quote}

\nwenddocs{}\nwbegindocs{11}\nwdocspar
\subsection{Instruction decoding and execution on two platforms}
Given this canonical form for instructions, we represent instruction
decoding using a {\Tt{}\textbf{let}}-binding notation:
\nwenddocs{}\nwbegincode{12}\moddef{instruction decoding}\endmoddef\nwstartdeflinemarkup\nwenddeflinemarkup
\textbf{let}{\ }\((b_I \mathbin{\rightarrow} {\mathit{nPC}} \mathrel{:=} {\mathit{target}}_I \mathrel{|} {\mathit{annul}} \mathrel{:=} a_I \mathrel{|} I_c) \equiv  {\mathit{src}}[{\mathit{PC}}]\)
\textbf{in}{\ }{\ }\(\ldots\)
\textbf{end}
\nwendcode{}\nwbegindocs{13}The {\Tt{}\textbf{let}} construct binds {\Tt{}\(b_I\)}, {\Tt{}\({\mathit{target}}_I\)},
{\Tt{}\(a_I\)}, and {\Tt{}\(I_c\)}, which together determine the
semantics of the instruction~{\Tt{}\(I\)} found in the source memory~{\Tt{}\({\mathit{src}}\)}.
\iffullpaper
This {\Tt{}\textbf{let}}-binding represents not only the process of using the
binary representation to identify the instruction and its operands,
but also the abstraction from that representation into the RTL semantics.
This abstraction from binary representation to semantics can be done
statically, at 
binary-translation time; it can even be automated based on a
combination of machine descriptions
\opencite{ramsey:specifying,ramsey:embedded}.
\fi
\nwenddocs{}\nwbegindocs{14}\nwdocspar
The source-machine execution loop
decodes an instruction and executes it as follows:
\nwenddocs{}\nwbegincode{15}\moddef{sparc execution loop}\endmoddef\nwstartdeflinemarkup\nwenddeflinemarkup
\textbf{fun}{\ }\({\mathit{loop}} () \equiv \)
{\ }{\ }\textbf{let}{\ }\((b_I \mathbin{\rightarrow} {\mathit{nPC}} \mathrel{:=} {\mathit{target}}_I \mathrel{|} {\mathit{annul}} \mathrel{:=} a_I \mathrel{|} I_c) \equiv  {\mathit{src}}[{\mathit{PC}}]\)
{\ }{\ }\textbf{in}{\ }{\ }\textbf{if}{\ }\({\mathit{annul}}\){\ }\textbf{then}
{\ }{\ }{\ }{\ }{\ }{\ }{\ }{\ }{\ }\({\mathit{PC}} \mathrel{:=} {\mathit{nPC}} \mathrel{|} {\mathit{nPC}} \mathrel{:=} {\mathit{succ}}_s({\mathit{nPC}}) \mathrel{|} {\mathit{annul}} \mathrel{:=} \textbf{false}\)
{\ }{\ }{\ }{\ }{\ }{\ }\textbf{else}{\ }\textbf{if}{\ }\([\![b_I]\!]\){\ }\textbf{then}
{\ }{\ }{\ }{\ }{\ }{\ }{\ }{\ }{\ }\({\mathit{PC}} \mathrel{:=} {\mathit{nPC}} \mathrel{|} {\mathit{nPC}} \mathrel{:=} [\![{\mathit{target}}_I]\!]  \mathrel{|} [\![I_c]\!] \mathrel{|} {\mathit{annul}} \mathrel{:=} [\![a_I]\!]\)
{\ }{\ }{\ }{\ }{\ }{\ }\textbf{else}
{\ }{\ }{\ }{\ }{\ }{\ }{\ }{\ }{\ }\({\mathit{PC}} \mathrel{:=} {\mathit{nPC}} \mathrel{|} {\mathit{nPC}} \mathrel{:=} {\mathit{succ}}_s({\mathit{nPC}}) \mathrel{|} [\![I_c]\!] \mathrel{|} {\mathit{annul}} \mathrel{:=} [\![a_I]\!]\)
{\ }{\ }{\ }{\ }{\ }{\ }\textbf{fi}
{\ }{\ }{\ }{\ }{\ }{\ }\(; {\mathit{loop}}()\)
{\ }{\ }\textbf{end}
\nwendcode{}\nwbegindocs{16}We specify the repeated execution of the processor loop as a tail
call, rather than as a loop, because that simplifies the
program transformations to follow.
\nwenddocs{}\nwbegindocs{17}\nwdocspar
The notation {\Tt{}\([\![\bullet ]\!]\)} represents execution; for example,
{\Tt{}\([\![b_I]\!]\)} is the value of the branch condition, given the current
state of the machine.
Executing the computational effect {\Tt{}\([\![I_c]\!]\)} changes the state of the machine.
\nwenddocs{}\nwbegindocs{18}\nwdocspar
The function {\Tt{}\({\mathit{succ}}_s\)} abstracts over the details of identifying
the successor instruction on the source machine; {\Tt{}\({\mathit{succ}}_t\)} finds the
successor on the target machine.
In both cases, {\Tt{}\({\mathit{succ}}\)} is computed as part of instruction decoding.
\nwenddocs{}\nwbegindocs{19}\nwdocspar
Our example target, the Pentium, has neither delayed branches nor
annulling, so it has a simpler canonical form and a simpler execution
loop:
\nwenddocs{}\nwbegincode{20}\moddef{Pentium execution loop}\endmoddef\nwstartdeflinemarkup\nwenddeflinemarkup
\textbf{fun}{\ }\({\mathit{simple}} () \equiv \)
{\ }{\ }\textbf{let}{\ }\((b_I \mathbin{\rightarrow} {\mathit{PC}} \mathrel{:=} {\mathit{target}}_I \mathrel{|} I_c) \equiv  {\mathit{tgt}}[{\mathit{PC}}]\)
{\ }{\ }\textbf{in}{\ }{\ }\textbf{if}{\ }\([\![b_I]\!]\){\ }\textbf{then}
{\ }{\ }{\ }{\ }{\ }{\ }{\ }{\ }\({\mathit{PC}} \mathrel{:=} [\![{\mathit{target}}_I]\!] \mathrel{|} [\![I_c]\!]\)
{\ }{\ }{\ }{\ }{\ }{\ }\textbf{else}
{\ }{\ }{\ }{\ }{\ }{\ }{\ }{\ }\({\mathit{PC}} \mathrel{:=} {\mathit{succ}}_t({\mathit{PC}}) \mathrel{|} [\![I_c]\!]\)
{\ }{\ }{\ }{\ }{\ }{\ }\textbf{fi}
{\ }{\ }{\ }{\ }{\ }{\ }\(; {\mathit{simple}}()\)
{\ }{\ }\textbf{end}
\nwendcode{}\nwbegindocs{21}\nwdocspar




\subsection{Strategy for translating delayed branches}

Both our formalism and
the SPARC architecture manual give a clear semantics of delayed
branches in terms of {\Tt{}\({\mathit{PC}}\)}, {\Tt{}\({\mathit{nPC}}\)}, and {\Tt{}\({\mathit{annul}}\)}.
To get an efficient target program, however, we wish \emph{not} to
represent the source {\Tt{}\({\mathit{PC}}\)}, {\Tt{}\({\mathit{nPC}}\)}, and {\Tt{}\({\mathit{annul}}\)} explicitly, but to
make all three \emph{implicit} in the value of the target~{\Tt{}\({\mathit{PC}}\)}.
How to do this based on the information in the architecture manual is
not immediately obvious, but our semantic framework enables a new technique.
We transform {\Tt{}\({\mathit{loop}}\)}, eliminating {\Tt{}\({\mathit{nPC}}\)} and {\Tt{}\({\mathit{annul}}\)} wherever
possible, so that (almost all of) {\Tt{}\({\mathit{loop}}\)} can be expressed using only
the~{\Tt{}\({\mathit{PC}}\)}.
%%This transformation leads to suitable changes in the sequence of
%%instructions executed, thus guiding a transformation from {\Tt{}\({\mathit{src}}\)} to {\Tt{}\({\mathit{tgt}}\)}.
%%This latter transformation is an algorithm for binary translation of
%%delayed-branch instructions.


% l2h substitution src s-sigma-
% l2h substitution tgt t-sigma-

\newcommand\presigma[1]{\mathord{{}^{#1}\sigma}}
\newcommand\presigmap[1]{\mathord{{}^{#1}\sigma'}}
\newcommand\src[1]{\presigma{s}_{#1}}
\newcommand\tgt[1]{\presigma{t}_{#1}}


\section{Transforming the execution loop}

We wish to develop a translation function that we can point at a
location {\Tt{}\({\mathit{src}}[{\mathit{pc}}_s]\)} and that will produce suitable instructions at a
corresponding target location {\Tt{}\({\mathit{tgt}}[{\mathit{pc}}_t]\)}.
We cannot simply have {\Tt{}\({\mathit{pc}}_t = {\mathit{pc}}_s\)}; source program counters
cannot be identical to target program counters, because 
source and target instruction sequences may be different sizes.
During translation, we build {\Tt{}\({\mathit{codemap}}\)}, a map that relates program
counters on the two machines, so {\Tt{}\({\mathit{pc}}_t = {\mathit{codemap}}({\mathit{pc}}_s)\)}.

We assume that
when the source processor starts executing code at {\Tt{}\({\mathit{src}}[{\mathit{pc}}_s]\)}, it
is not in the middle of a delayed
or annulled branch, or formally,
\begin{quote}
{\Tt{}\({\mathit{annul}} = \textbf{false} \land  {\mathit{nPC}} = {\mathit{succ}}_s({\mathit{PC}})\)}.
\end{quote}
Software conventions guarantee that
the processor will be in such a state at a program's start location
and at procedure entry points.
\nwenddocs{}\nwbegindocs{22}\nwdocspar
We begin our transformation by
defining a function {\Tt{}\({\mathit{stable}}\)} that can be substituted for {\Tt{}\({\mathit{loop}}\)}
whenever {\Tt{}\({\mathit{annul}} = \textbf{false} \land  {\mathit{nPC}} = {\mathit{succ}}_s({\mathit{PC}})\)}.
\nwenddocs{}\nwbegincode{23}\moddef{stable execution loop}\endmoddef\nwstartdeflinemarkup\nwenddeflinemarkup
\textbf{fun}{\ }\({\mathit{stable}} () \equiv \)
{\ }{\ }\({\mathit{annul}} \mathrel{:=} \textbf{false} \mathrel{|} {\mathit{nPC}} \mathrel{:=} {\mathit{succ}}_s({\mathit{PC}});\)
{\ }{\ }\textbf{let}{\ }\((b_I \mathbin{\rightarrow} {\mathit{nPC}} \mathrel{:=} {\mathit{target}}_I \mathrel{|} {\mathit{annul}} \mathrel{:=} a_I \mathrel{|} I_c) \equiv  {\mathit{src}}[{\mathit{PC}}]\)
{\ }{\ }\textbf{in}{\ }{\ }\textbf{if}{\ }\({\mathit{annul}}\){\ }\textbf{then}
{\ }{\ }{\ }{\ }{\ }{\ }{\ }{\ }{\ }\({\mathit{PC}} \mathrel{:=} {\mathit{nPC}} \mathrel{|} {\mathit{nPC}} \mathrel{:=} {\mathit{succ}}_s({\mathit{nPC}}) \mathrel{|} {\mathit{annul}} \mathrel{:=} \textbf{false}\)
{\ }{\ }{\ }{\ }{\ }{\ }\textbf{else}{\ }\textbf{if}{\ }\([\![b_I]\!]\){\ }\textbf{then}
{\ }{\ }{\ }{\ }{\ }{\ }{\ }{\ }{\ }\({\mathit{PC}} \mathrel{:=} {\mathit{nPC}} \mathrel{|} {\mathit{nPC}} \mathrel{:=} [\![{\mathit{target}}_I]\!]  \mathrel{|} [\![I_c]\!] \mathrel{|} {\mathit{annul}} \mathrel{:=} [\![a_I]\!]\)
{\ }{\ }{\ }{\ }{\ }{\ }\textbf{else}
{\ }{\ }{\ }{\ }{\ }{\ }{\ }{\ }{\ }\({\mathit{PC}} \mathrel{:=} {\mathit{nPC}} \mathrel{|} {\mathit{nPC}} \mathrel{:=} {\mathit{succ}}_s({\mathit{nPC}}) \mathrel{|} [\![I_c]\!] \mathrel{|} {\mathit{annul}} \mathrel{:=} [\![a_I]\!]\)
{\ }{\ }{\ }{\ }{\ }{\ }\textbf{fi}
{\ }{\ }{\ }{\ }{\ }{\ }\(; {\mathit{loop}}()\)
{\ }{\ }\textbf{end}
\nwendcode{}\nwbegindocs{24}\nwdocspar
\iftr
We move the initial assignment inside the {\Tt{}\textbf{let}}, and we distribute
the tail call to {\Tt{}\({\mathit{loop}}\)} over the arms of the {\Tt{}\textbf{if}}.
\nwenddocs{}%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
\nwbegindocs{26}\nwdocspar
We drop the first arm of the {\Tt{}\textbf{if}}, because {\Tt{}\({\mathit{annul}}\)} is always
false.
We expand the final arm by inserting a test on {\Tt{}\([\![a_I]\!]\)}.
\nwenddocs{}%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
\nwbegindocs{28}\nwdocspar
The last arm of the {\Tt{}\textbf{if}} shows the proper translation of an
instruction that neither branches nor annuls.
We can substitute {\Tt{}\({\mathit{stable}}\)} for {\Tt{}\({\mathit{loop}}\)}, then drop the assignments
to {\Tt{}\({\mathit{annul}}\)} and {\Tt{}\({\mathit{nPC}}\)}, because they don't reach any uses.
Finally, we propagate the initial definition of {\Tt{}\({\mathit{nPC}}\)} to its uses.
(This should be rewritten in a final TR.)
\nwenddocs{}%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
\nwbegindocs{30}\nwdocspar
The next steps are to drop the dead assignments to {\Tt{}\({\mathit{annul}}\)} and
{\Tt{}\({\mathit{nPC}}\)}, and
\fi
We do not show every step in the
transformation of {\Tt{}\({\mathit{stable}}\)}.
The first transformations move the initial
assignments inside the {\Tt{}\textbf{let}}, propagate (by forward substitution)
the assignments to {\Tt{}\({\mathit{annul}}\)} and {\Tt{}\({\mathit{nPC}}\)},
move {\Tt{}\({\mathit{loop}}\)} inside the {\Tt{}\textbf{if}},  replace {\Tt{}\({\mathit{loop}}\)}
with {\Tt{}\({\mathit{stable}}\)} where possible, and drop the (now dead)
assignments.
The result is:
\nwenddocs{}\nwbegincode{31}\moddef{stable execution loop}\plusendmoddef\nwstartdeflinemarkup\nwenddeflinemarkup
\textbf{fun}{\ }\({\mathit{stable}} () \equiv \)
{\ }{\ }\textbf{let}{\ }\((b_I \mathbin{\rightarrow} {\mathit{nPC}} \mathrel{:=} {\mathit{target}}_I \mathrel{|} {\mathit{annul}} \mathrel{:=} a_I \mathrel{|} I_c) \equiv  {\mathit{src}}[{\mathit{PC}}]\)
{\ }{\ }\textbf{in}{\ }{\ }\textbf{if}{\ }\([\![b_I]\!]\){\ }\textbf{then}
{\ }{\ }{\ }{\ }{\ }{\ }{\ }{\ }{\ }\({\mathit{PC}} \mathrel{:=} {\mathit{succ}}_s({\mathit{PC}}) \mathrel{|} {\mathit{nPC}} \mathrel{:=} [\![{\mathit{target}}_I]\!]  \mathrel{|} [\![I_c]\!] \mathrel{|} {\mathit{annul}} \mathrel{:=} [\![a_I]\!]\)
{\ }{\ }{\ }{\ }{\ }{\ }{\ }{\ }{\ }\(; {\mathit{loop}}()\)
{\ }{\ }{\ }{\ }{\ }{\ }\textbf{else}{\ }\textbf{if}{\ }\([\![a_I]\!]\){\ }\textbf{then}
{\ }{\ }{\ }{\ }{\ }{\ }{\ }{\ }{\ }\({\mathit{PC}} \mathrel{:=} {\mathit{succ}}_s({\mathit{PC}}) \mathrel{|} {\mathit{nPC}} \mathrel{:=} {\mathit{succ}}_s({\mathit{succ}}_s({\mathit{PC}})) \mathrel{|} [\![I_c]\!] \mathrel{|} {\mathit{annul}} \mathrel{:=} \textbf{true}\)
{\ }{\ }{\ }{\ }{\ }{\ }{\ }{\ }{\ }\(; {\mathit{loop}}()\)
{\ }{\ }{\ }{\ }{\ }{\ }\textbf{else}
{\ }{\ }{\ }{\ }{\ }{\ }{\ }{\ }{\ }\({\mathit{PC}} \mathrel{:=} {\mathit{succ}}_s({\mathit{PC}}) \mathrel{|} [\![I_c]\!]\)
{\ }{\ }{\ }{\ }{\ }{\ }{\ }{\ }{\ }\(; {\mathit{stable}}()\)
{\ }{\ }{\ }{\ }{\ }{\ }\textbf{fi}
{\ }{\ }\textbf{end}
\nwendcode{}\nwbegindocs{32}%
\iftr
\else 
The last arm of the {\Tt{}\textbf{if}} shows the execution of an
instruction that never branches or annuls.
It corresponds to
the execution of a similar instruction on the {\Tt{}\({\mathit{simple}}\)} target.
\fi
\nwenddocs{}\nwbegindocs{33}\nwdocspar

The next step is to unfold {\Tt{}\({\mathit{loop}}\)} in the first
and second arms of the {\Tt{}\textbf{if}} statement. 
In the second arm, {\Tt{}\({\mathit{annul}}\)} is {\Tt{}\(\textbf{true}\)}, so the call to {\Tt{}\({\mathit{loop}}()\)} can
be replaced by
{\Tt{}\({\mathit{PC}} \mathrel{:=} {\mathit{nPC}}; {\mathit{nPC}} \mathrel{:=} {\mathit{succ}}_s({\mathit{nPC}}); {\mathit{stable}}()\)}.
The definition of {\Tt{}\({\mathit{stable}}\)} reduces to
\iftr
\nwenddocs{}%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
\nwbegindocs{35}\nwdocspar
We now simplify {\Tt{}\({\mathit{stable}}\)} in two ways.
We encapsulate the first branch of the {\Tt{}\textbf{if}} in the chunk 
{\Tt{}\LA{}case where \code{}I\edoc{} branches\RA{}}, and we simplify the
second branch.
Reasonable care is required when substituting forward the value
({\Tt{}\({\mathit{succ}}_s({\mathit{succ}}_s({\mathit{PC}}))\)}) of {\Tt{}\({\mathit{nPC}}\)}, because the 
RTL that assigns to {\Tt{}\({\mathit{nPC}}\)} also assigns to {\Tt{}\({\mathit{PC}}\)}.
Moreover, because the values bound in the {\Tt{}\textbf{let}} don't reach any
uses, the entire {\Tt{}\textbf{let}} goes away.
Finally, the call to {\Tt{}\({\mathit{loop}}\)} can be replaced by a call to {\Tt{}\({\mathit{stable}}\)},
and the dead assignments to {\Tt{}\({\mathit{annul}}\)} and {\Tt{}\({\mathit{nPC}}\)} dropped.
\fi
\nwenddocs{}\nwbegincode{36}\moddef{stable execution loop}\plusendmoddef\nwstartdeflinemarkup\nwenddeflinemarkup
\textbf{fun}{\ }\({\mathit{stable}} () \equiv \)
{\ }{\ }\textbf{let}{\ }\((b_I \mathbin{\rightarrow} {\mathit{nPC}} \mathrel{:=} {\mathit{target}}_I \mathrel{|} {\mathit{annul}} \mathrel{:=} a_I \mathrel{|} I_c) \equiv  {\mathit{src}}[{\mathit{PC}}]\)
{\ }{\ }\textbf{in}{\ }{\ }\textbf{if}{\ }\([\![b_I]\!]\){\ }\textbf{then}
{\ }{\ }{\ }{\ }{\ }{\ }{\ }{\ }{\ }\LA{}case where \code{}I\edoc{} branches\RA{}
{\ }{\ }{\ }{\ }{\ }{\ }\textbf{else}{\ }\textbf{if}{\ }\([\![a_I]\!]\){\ }\textbf{then}
{\ }{\ }{\ }{\ }{\ }{\ }{\ }{\ }{\ }\({\mathit{PC}} \mathrel{:=} {\mathit{succ}}_s({\mathit{succ}}_s({\mathit{PC}})) \mathrel{|} [\![I_c]\!]\)
{\ }{\ }{\ }{\ }{\ }{\ }{\ }{\ }{\ }\(; {\mathit{stable}}()\)
{\ }{\ }{\ }{\ }{\ }{\ }\textbf{else}
{\ }{\ }{\ }{\ }{\ }{\ }{\ }{\ }{\ }\({\mathit{PC}} \mathrel{:=} {\mathit{succ}}_s({\mathit{PC}}) \mathrel{|} [\![I_c]\!]\)
{\ }{\ }{\ }{\ }{\ }{\ }{\ }{\ }{\ }\(; {\mathit{stable}}()\)
{\ }{\ }{\ }{\ }{\ }{\ }\textbf{fi}
{\ }{\ }\textbf{end}
\nwendcode{}\nwbegindocs{37}where the interesting case is
\nwenddocs{}\nwbegincode{38}\moddef{case where \code{}I\edoc{} branches}\endmoddef\nwstartdeflinemarkup\nwenddeflinemarkup
\({\mathit{PC}} \mathrel{:=} {\mathit{succ}}_s({\mathit{PC}}) \mathrel{|} {\mathit{nPC}} \mathrel{:=} [\![{\mathit{target}}_I]\!]  \mathrel{|} [\![I_c]\!] \mathrel{|} {\mathit{annul}} \mathrel{:=} [\![a_I]\!];\)
\textbf{let}{\ }\((b_{I'} \mathbin{\rightarrow} {\mathit{nPC}} \mathrel{:=} {\mathit{target}}_{I'} \mathrel{|} {\mathit{annul}} \mathrel{:=} a_{I'} \mathrel{|} {I'}_c) \equiv  {\mathit{src}}[{\mathit{PC}}]\)
\textbf{in}{\ }{\ }\textbf{if}{\ }\({\mathit{annul}}\){\ }\textbf{then}
{\ }{\ }{\ }{\ }{\ }{\ }{\ }\({\mathit{PC}} \mathrel{:=} {\mathit{nPC}} \mathrel{|} {\mathit{nPC}} \mathrel{:=} {\mathit{succ}}_s({\mathit{nPC}}) \mathrel{|} {\mathit{annul}} \mathrel{:=} \textbf{false}\)
{\ }{\ }{\ }{\ }\textbf{else}{\ }\textbf{if}{\ }\([\![b_{I'}]\!]\){\ }\textbf{then}
{\ }{\ }{\ }{\ }{\ }{\ }{\ }\({\mathit{PC}} \mathrel{:=} {\mathit{nPC}} \mathrel{|} {\mathit{nPC}} \mathrel{:=} [\![{\mathit{target}}_{I'}]\!]  \mathrel{|} [\![{I'}_c]\!] \mathrel{|} {\mathit{annul}} \mathrel{:=} [\![a_{I'}]\!]\)
{\ }{\ }{\ }{\ }\textbf{else}
{\ }{\ }{\ }{\ }{\ }{\ }{\ }\({\mathit{PC}} \mathrel{:=} {\mathit{nPC}} \mathrel{|} {\mathit{nPC}} \mathrel{:=} {\mathit{succ}}_s({\mathit{nPC}}) \mathrel{|} [\![{I'}_c]\!] \mathrel{|} {\mathit{annul}} \mathrel{:=} [\![a_{I'}]\!]\)
{\ }{\ }{\ }{\ }\textbf{fi}
{\ }{\ }{\ }{\ }\(; {\mathit{loop}}()\)
\textbf{end}
\nwendcode{}\nwbegindocs{39}\nwdocspar
Transformation proceeds by combining these two fragments, moving the
{\Tt{}\textbf{let}}s together, and flattening the nested {\Tt{}\textbf{if}} statements.
We then use ``The Trick'' from partial evaluation \opencite{danvy:eta}:
whenever  {\Tt{}\([\![a_I]\!]\)}~is free in a statement~{\Tt{}\(S\)}, we
replace~{\Tt{}\(S\)} with {\Tt{}\textbf{if}{\ }\([\![a_I]\!]\)}{\Tt{}{\ }\textbf{then}{\ }\(S\){\ }\textbf{else}{\ }\(S\){\ }\textbf{fi}}.
The Trick enables us to replace several calls to {\Tt{}\({\mathit{loop}}\)} with calls
to {\Tt{}\({\mathit{stable}}\)}.
\iftr
Move {\Tt{}\textbf{let}} outside, and propagate definitions to uses.
\nwenddocs{}%
%
%
%
%
%
%
%
%
%
%
%
\nwbegindocs{41}\nwdocspar
Eliminate dead code, and distribute {\Tt{}\({\mathit{loop}}\)} over the arms of the
{\Tt{}\textbf{if}}.
\nwenddocs{}%
%
%
%
%
%
%
%
%
%
%
%
%
%
\nwbegindocs{43}\nwdocspar
Put in {\Tt{}\({\mathit{stable}}\)}
\nwenddocs{}%
%
%
%
%
%
%
%
%
%
%
%
%
%
\nwbegindocs{45}\nwdocspar
\par\bigskip\hrule\bigskip
\def\nwdocspar{\vskip0pt plus2.5in\penalty-200\vskip0pt plus -2.5in}
Re-expand.
\nwenddocs{}%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
\nwbegindocs{47}\nwdocspar
Combine {\Tt{}\textbf{let}}s, and flatten {\Tt{}\textbf{if}}.
Also, make conditions more explicit.
\nwenddocs{}%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
\nwbegindocs{49}\nwdocspar
\nwenddocs{}\nwbegindocs{50}\nwdocspar
Insert tests on {\Tt{}\(a_{I'}\)}.
\nwenddocs{}%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
\nwbegindocs{52}\nwdocspar
This body has four calls to~{\Tt{}\({\mathit{loop}}\)}.
The fourth call satisfies the preconditions for using {\Tt{}\({\mathit{stable}}\)}.
The first and third are made when {\Tt{}\({\mathit{annul}}\)} is true, in which case
{\Tt{}\({\mathit{loop}}\)} can be unfolded once and turned into {\Tt{}\({\mathit{stable}}\)}.
Simplification therefore leaves a version of {\Tt{}\({\mathit{stable}}\)} in which only
one case requires a call to~{\Tt{}\({\mathit{loop}}\)}.
\fi
The result is
\nwenddocs{}\nwbegincode{53}\moddef{stable execution loop}\plusendmoddef\nwstartdeflinemarkup\nwenddeflinemarkup
\textbf{fun}{\ }\({\mathit{stable}} () \equiv \)
{\ }{\ }\textbf{let}{\ }\((b_I  \mathbin{\rightarrow} {\mathit{nPC}} \mathrel{:=} {\mathit{target}}_I  \mathrel{|} {\mathit{annul}} \mathrel{:=} a_I  \mathrel{|} I_c)  \equiv  {\mathit{src}}[{\mathit{PC}}]\)
{\ }{\ }{\ }{\ }{\ }{\ }\((b_{I'} \mathbin{\rightarrow} {\mathit{nPC}} \mathrel{:=} {\mathit{target}}_{I'} \mathrel{|} {\mathit{annul}} \mathrel{:=} a_{I'} \mathrel{|} {I'}_c) \equiv  {\mathit{src}}[{\mathit{succ}}_s({\mathit{PC}})]\)
{\ }{\ }\textbf{in}{\ }{\ }\textbf{if}{\ }\([\![b_I]\!] \land  [\![a_I]\!]\){\ }\textbf{then}
{\ }{\ }{\ }{\ }{\ }{\ }{\ }{\ }{\ }\([\![I_c]\!];\)
{\ }{\ }{\ }{\ }{\ }{\ }{\ }{\ }{\ }\({\mathit{PC}} \mathrel{:=} [\![{\mathit{target}}_I]\!]\)
{\ }{\ }{\ }{\ }{\ }{\ }{\ }{\ }{\ }\(; {\mathit{stable}}()\)
{\ }{\ }{\ }{\ }{\ }{\ }\textbf{else}{\ }\textbf{if}{\ }\([\![b_I]\!] \land  \lnot  [\![a_I]\!] \land  [\![b_{I'}]\!] \land  [\![a_{I'}]\!]\){\ }\textbf{then}
{\ }{\ }{\ }{\ }{\ }{\ }{\ }{\ }{\ }\([\![I_c]\!];\)
{\ }{\ }{\ }{\ }{\ }{\ }{\ }{\ }{\ }\([\![{I'}_c]\!];\)
{\ }{\ }{\ }{\ }{\ }{\ }{\ }{\ }{\ }\({\mathit{PC}} \mathrel{:=} [\![{\mathit{target}}_{I'}]\!]\)
{\ }{\ }{\ }{\ }{\ }{\ }{\ }{\ }{\ }\(; {\mathit{stable}}()\)
{\ }{\ }{\ }{\ }{\ }{\ }\textbf{else}{\ }\textbf{if}{\ }\([\![b_I]\!] \land  \lnot  [\![a_I]\!] \land  [\![b_{I'}]\!] \land  \lnot  [\![a_{I'}]\!]\){\ }\textbf{then}
{\ }{\ }{\ }{\ }{\ }{\ }{\ }{\ }{\ }\([\![I_c]\!];\)
{\ }{\ }{\ }{\ }{\ }{\ }{\ }{\ }{\ }\({\mathit{PC}} \mathrel{:=} [\![{\mathit{target}}_I]\!] \mathrel{|} {\mathit{nPC}} \mathrel{:=} [\![{\mathit{target}}_{I'}]\!]  \mathrel{|} [\![{I'}_c]\!] \mathrel{|} {\mathit{annul}} \mathrel{:=} \textbf{false}\)
{\ }{\ }{\ }{\ }{\ }{\ }{\ }{\ }{\ }\(; {\mathit{loop}}()\)
{\ }{\ }{\ }{\ }{\ }{\ }\textbf{else}{\ }\textbf{if}{\ }\([\![b_I]\!] \land  \lnot  [\![a_I]\!] \land  \lnot  [\![b_{I'}]\!] \land  [\![a_{I'}]\!]\){\ }\textbf{then}
{\ }{\ }{\ }{\ }{\ }{\ }{\ }{\ }{\ }\([\![I_c]\!];\)
{\ }{\ }{\ }{\ }{\ }{\ }{\ }{\ }{\ }\([\![{I'}_c]\!];\)
{\ }{\ }{\ }{\ }{\ }{\ }{\ }{\ }{\ }\({\mathit{PC}} \mathrel{:=} {\mathit{succ}}_s([\![{\mathit{target}}_I]\!])\)
{\ }{\ }{\ }{\ }{\ }{\ }{\ }{\ }{\ }\(; {\mathit{stable}}()\)
{\ }{\ }{\ }{\ }{\ }{\ }\textbf{else}{\ }\textbf{if}{\ }\([\![b_I]\!] \land  \lnot  [\![a_I]\!] \land  \lnot  [\![b_{I'}]\!] \land  \lnot  [\![a_{I'}]\!]\){\ }\textbf{then}
{\ }{\ }{\ }{\ }{\ }{\ }{\ }{\ }{\ }\([\![I_c]\!];\)
{\ }{\ }{\ }{\ }{\ }{\ }{\ }{\ }{\ }\({\mathit{PC}} \mathrel{:=} [\![{\mathit{target}}_I]\!] \mathrel{|} [\![{I'}_c]\!]\)
{\ }{\ }{\ }{\ }{\ }{\ }{\ }{\ }{\ }\(; {\mathit{stable}}()\)
{\ }{\ }{\ }{\ }{\ }{\ }\textbf{else}{\ }\textbf{if}{\ }\(\lnot  [\![b_I]\!] \land  [\![a_I]\!]\){\ }\textbf{then}
{\ }{\ }{\ }{\ }{\ }{\ }{\ }{\ }{\ }\({\mathit{PC}} \mathrel{:=} {\mathit{succ}}_s({\mathit{succ}}_s({\mathit{PC}})) \mathrel{|} [\![I_c]\!]\)
{\ }{\ }{\ }{\ }{\ }{\ }{\ }{\ }{\ }\(; {\mathit{stable}}()\)
{\ }{\ }{\ }{\ }{\ }{\ }\textbf{else}{\ }\textbf{if}{\ }\(\lnot  [\![b_I]\!] \land  \lnot  [\![a_I]\!]\){\ }\textbf{then}
{\ }{\ }{\ }{\ }{\ }{\ }{\ }{\ }{\ }\({\mathit{PC}} \mathrel{:=} {\mathit{succ}}_s({\mathit{PC}}) \mathrel{|} [\![I_c]\!]\)
{\ }{\ }{\ }{\ }{\ }{\ }{\ }{\ }{\ }\(; {\mathit{stable}}()\)
{\ }{\ }{\ }{\ }{\ }{\ }\textbf{fi}
{\ }{\ }\textbf{end}
\nwendcode{}\nwbegindocs{54}\nwdocspar
This version of {\Tt{}\({\mathit{stable}}\)} suffices to guide the construction of a
translator. 
Considering the cases in order,
\begin{itemize}
\item
A branch that annuls the instruction in its delay slot acts just like
an ordinary branch on a machine without delayed branches.
\item
A branch that does not annul, but that has an annuling branch in its
delay slot, acts as if the first branch never happened, and the second
is a non-delaying branch.
\item
A non-annuling branch with another non-annuling branch in its delay
slot is not trivial to translate; this is the one case in
which we cannot substitute {\Tt{}\({\mathit{stable}}\)} for {\Tt{}\({\mathit{loop}}\)}.
Interestingly, the  MIPS architecture manual specifies that the
machine's behavior in this case is undefined
\cite[Appendix~A]{kane:mips}.
This case requires potentially unbounded unfolding of~{\Tt{}\({\mathit{loop}}\)}, which
is discussed in Section~\ref{sec:limit-unfold}.
\item
A non-annuling branch with an annuling non-branch in its delay slot
acts as a branch to the successor of the target instruction.
(Note that the SPARC has an annulling non-branch, viz, \texttt{BN,A}.)
\item
A non-annuling branch with a non-annuling non-branch in its delay slot
has the effect of delaying the branch by one cycle.
This is the common case.
\item
An annuling non-branch skips over its successor.
\item
A non-annuling non-branch (i.e., an ordinary
computational instruction) simply executes and advances the program
counter to its successor.
\end{itemize}
We now apply this analysis to the SPARC.
\nwenddocs{}\nwbegindocs{55}\nwdocspar
\section{Application to the SPARC instruction set}



\subsection{Classification of SPARC instructions}

The three properties of instructions that govern the translation of
control flow are {\Tt{}\(b_I\)} (must branch, may branch, may not branch),
{\Tt{}\(a_I\)} (must annul, may annul, may not annul), and {\Tt{}\({\mathit{target}}_I\)}
(static target, dynamic target, no target).
There are 15~reasonable combinations of these three properties.
On the SPARC, only~9 are used:
\begin{quote}%figure
\rlap{%
\begin{tabular}{llllll}
\emph{Instruction}&{\Tt{}\(b_I\)}&{\Tt{}\(a_I\)}&{\Tt{}\({\mathit{target}}_I\)}&{\Tt{}\(I_c\)}&\emph{Class}\\
\texttt{BA}&{\Tt{}\(\textbf{true}\)}&{\Tt{}\(\textbf{false}\)}&static&{\Tt{}\textbf{skip}}&\emph{SD}\\
\texttt{BN}&{\Tt{}\(\textbf{false}\)}&{\Tt{}\(\textbf{false}\)}&N/A&{\Tt{}\textbf{skip}}&\emph{NCT}\\
\texttt{Bcc}&{\Tt{}\({\mathit{test}}_{\mathit{cc}}({\mathit{icc}})\)}&{\Tt{}\(\textbf{false}\)}&static&{\Tt{}\textbf{skip}}&\emph{SCD}\\
\texttt{BA,A}&{\Tt{}\(\textbf{true}\)}&{\Tt{}\(\textbf{true}\)}&static&{\Tt{}\textbf{skip}}&\emph{SU}\\
\texttt{BN,A}&{\Tt{}\(\textbf{false}\)}&{\Tt{}\(\textbf{true}\)}&N/A&{\Tt{}\textbf{skip}}&\emph{SKIP}\\
\texttt{Bcc,A}&{\Tt{}\({\mathit{test}}_{\mathit{cc}}({\mathit{icc}})\)}&{\Tt{}\(\lnot  {\mathit{test}}_{\mathit{cc}}({\mathit{icc}})\)}&static&{\Tt{}\textbf{skip}}&\emph{SCDA}\\
\texttt{CALL}&{\Tt{}\(\textbf{true}\)}&{\Tt{}\(\textbf{false}\)}&static&{\Tt{}\(\$r[15] \mathrel{:=} {\mathit{PC}}\)}&\emph{SD}\\
\texttt{JMPL}&{\Tt{}\(\textbf{true}\)}&{\Tt{}\(\textbf{false}\)}&dynamic&{\Tt{}\(\$r[{\mathit{rd}}] \mathrel{:=} {\mathit{PC}}\)}&\emph{DD}\\
\texttt{RETT}&{\Tt{}\(\textbf{true}\)}&{\Tt{}\(\textbf{false}\)}&dynamic&{\Tt{}\LA{}restore state\RA{}}&\emph{DD}\\
\texttt{TN}&{\Tt{}\(\textbf{false}\)}&{\Tt{}\(\textbf{false}\)}&N/A&{\Tt{}\textbf{skip}}&\emph{NCT}\\
\texttt{Ticc}&{\Tt{}\({\mathit{test}}_{\mathit{cc}}({\mathit{icc}})\)}&{\Tt{}\({\mathit{test}}_{\mathit{cc}}({\mathit{icc}})\)}&dynamic&{\Tt{}\LA{}save state\RA{}}&\emph{TRAP}\\
\texttt{TA}&{\Tt{}\(\textbf{true}\)}&{\Tt{}\(\textbf{true}\)}&dynamic&{\Tt{}\LA{}save state\RA{}}&{\Tt{}\({\mathit{TRAP'}}\)}\\
NCT&{\Tt{}\(\textbf{false}\)}&{\Tt{}\(\textbf{false}\)}&N/A&varies&\emph{NCT}\\
\end{tabular}}
\end{quote}
We name 8 of the 9~classes as follows:
\begin{quote}%figure
\begin{tabular}{>{\em}ll}
NCT&Non-control-transfer instructions (arithmetic, etc.)\\
DD&Dynamic delayed (unconditional)\\
SD&Static delayed (unconditional)\\
SCD&Static conditional delayed\\
SCDA&Static conditional delayed, annulling\\
SU&Static unconditional (not delayed)\\
SKIP&Skip successor (implement as static unconditional)\\
TRAP&Trap\\
\end{tabular}
\end{quote}
%%  Note we can't just omit translating the delay instruction of a
%%  \texttt{BN,A} (class \emph{SKIP}) unless a dataflow analysis shows
%%  that this instruction 
%%  cannot be the target of any branch.

Our treatment of trap instructions may be surprising, since the
architecture manual presents them as instructions that set both {\Tt{}\({\mathit{PC}}\)}
and {\Tt{}\({\mathit{nPC}}\)}.
Because {\Tt{}\({\mathit{nPC}}\)} is always set to {\Tt{}\({\mathit{PC}}+4\)}
\cite[\S C.8]{sparc:architecture}, we can model this behavior
as setting {\Tt{}\({\mathit{nPC}}\)} to the address of the trap handler and setting
{\Tt{}\({\mathit{annul}}\)} to {\Tt{}\(\textbf{true}\)}.
Our model introduces a stall before the trap is taken, but no
interesting state changes during a stall, so there is no problem.
For simplicity, we put the
unconditional trap ({\Tt{}\({\mathit{TRAP'}}\)}) in the same class as the conditional
traps ({\Tt{}\({\mathit{TRAP}}\)}).
We can't do this with the branch instructions 
because of \texttt{BA,A}'s anomalous treatment of the \texttt{a}~bit.
\nwenddocs{}\nwbegindocs{56}\nwdocspar


The table exposes a useful property of the SPARC instruction set;
{\Tt{}\(a_I\)} is not arbitrary, but is always given by one of these four possibilities:
\begin{quote}%figure
\begin{tabular}{ll}
{\Tt{}\(a_I \equiv  \textbf{false}\)}& Never annul.\\
{\Tt{}\(a_I \equiv  \textbf{true}\)}& Always annul.\\
{\Tt{}\(a_I \equiv      b_I\)}&  Annul if branch taken.\\
{\Tt{}\(a_I \equiv  \lnot  b_I\)}&  Annul if branch not taken.\\
\end{tabular}
\end{quote}
Whenever processor designers use this scheme,
{\Tt{}\(a_I\)}~can be eliminated at binary-translation time.
A~more general~{\Tt{}\(a_I\)} would require a second test in the translated code.
\nwenddocs{}\nwbegindocs{57}\nwdocspar

%% We can now consider the translations of the seven(?) classes above.
%% <sparc translator>=
%% fun sparcTrans(PC, ^PC) =
%%   case src[PC] of
%%   | BA tgt => <depends on successor>
%%   | BN tgt, NCT, etc => tgt[^PC] := I_c; sparcTrans(succ(PC), succ(^PC))
%%   | Bcc tgt =>
%%       if {\Tt{}\(b_I\)}


%%\begin{quote}
%%\begin{tabularx}{\linewidth}{llYl}
%%{\Tt{}\(I\)}&{\Tt{}\({\mathit{succ}}(I)\)}&\emph{Translation}&em{Next}\\
%%\texttt{BA}, \texttt{CALL}&?&?\\
%%\texttt{BN}, NCT, etc&any&{\Tt{}\(I_c\)}&{\Tt{}\({\mathit{succ}}({\mathit{PC}})\)}\\
%%\texttt{Bcc}&
%%\texttt{BA,A}&any&{\Tt{}\({\mathit{PC}} \mathrel{:=} {\mathit{target}}_I\)}&none\\
%%\texttt{BN,A}&any&{\Tt{}\({\mathit{PC}} \mathrel{:=} {\mathit{succ}}({\mathit{succ}}({\mathit{PC}}))\)}&{\Tt{}\({\mathit{succ}}({\mathit{PC}})\)}\\
%%\texttt{Bcc,A}&
%%\texttt{JMPL}, \texttt{RETT}&?&?\\

\nwenddocs{}\nwbegindocs{58}\nwdocspar
\iftr
\subsection{Specializing the {\Tt{}\({\mathit{stable}}\)} function}
OK, let's try one version for each class.
\nwenddocs{}%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
\nwbegindocs{61}\nwdocspar
For the remaining classes, {\Tt{}\(I_c\)} is {\Tt{}\textbf{skip}}, so it can be dropped.
\nwenddocs{}%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
\nwbegindocs{66}\nwdocspar
\fi
\nwenddocs{}\nwbegindocs{67}\nwdocspar
\subsection{Derivation of a translator}

\subsubsection{Correctness}

To say what it means to have a correct translation,
we reason about states, about values of
expressions in states, and about state transitions.
For notation,
if a machine is in a state~{\Tt{}\({\sigma}\)}, we write {\Tt{}\(\mathcal E[\![e]\!]{\sigma}\)} for
the value 
of expression~{\Tt{}\(e\)} in state~{\Tt{}\({\sigma}\)}; 
if executing instruction~$I$ causes a machine to make a transition
from a state~{\Tt{}\({\sigma}\)} to a new state {\Tt{}\(\sigma'\)}, we write
{\Tt{}\(\sigma' = \mathcal C[\![I]\!]{\sigma}\)}, 
so {\Tt{}\(\mathcal C[\![I]\!]\)} stands for the state-changing effect of~{\Tt{}\(I\)}.

A translation is correct if execution on the target machine simulates
execution on the source machine.
The translator builds a map $\hatform\bullet$ from
source-machine states to target-machine states.%
\footnote{Technically, the translator establishes not a map but a
relation, because 
more than one target-machine state can be used to simulate a particular
source-machine state. 
We nevertheless use the $\hatform\bullet$ notation because it seems more intuitive.
When we
write~{\Tt{}\(\nwpphat{\presigma{s}}\)}, we really mean ``any state {\Tt{}\(\presigma{t}\)} such that
{\Tt{}\(\presigma{t}\)} and {\Tt{}\(\presigma{s}\)} stand in a weak bisimulation relation.''}
In a way made precise below, this
map respects the operation of the machine.
In our design, 
 $\hatform\bullet$ is \emph{partial}---it is not defined
when the source machine is ``about to'' execute a delayed branch or
annulled instruction.
To be precise, {\Tt{}\(\nwpphat{{\sigma}}\)}~is defined if
 {\Tt{}\(\mathcal E[\![\lnot  {\mathit{annul}} \land  {\mathit{nPC}} = {\mathit{succ}}_s({\mathit{PC}})]\!]{\sigma}\)}.

\label{sec:informal-simulation}

The target machine is said to \emph{simulate} the source machine if the
following condition holds:
if we start the source machine
in a state~$\src1$, and the {\Tt{}\({\mathit{loop}}\)} function takes it through a sequence of
states $\src1, \src2, \ldots$, then there is a subsequence of such
states $\src{k_1}, \src{k_2}, \ldots$ such that $\hatform{\src{k_1}},
\hatform{\src{k_2}}, \ldots$  is a subsequence of the states that the
target machine goes through when started in state $\tgt1 = \hatform{\src1}$.
Informally,  although the target machine may go through
some intermediate states that don't correspond to any execution of the
source, and though the source machine may go through some intermediate
states that don't correspond to any execution of the target, when we
remove those intermediate states, what's left of the executions
correspond one to one.%
\footnote{In the terminology of \citeN{milner:operational}, the
transitions to these intermediate states are ``silent.''}
We sketch a proof in Section~\ref{sec:transition-lemma}.
\nwenddocs{}\nwbegindocs{68}\nwdocspar




\newcommand\PC{\mathit{PC}}
\newcommand\nPC{\mathit{nPC}}

\def\subst[#1/#2]{\mathrm{subst}^{#1}_{#2}}
 
\subsubsection{Translations of expressions and computational effects}

In the RTL framework, the state of the machine is the contents of all
the storage locations. 
In a \ifhtml naive \else na\"\i ve \fi translator, 
 $\hatform\bullet$ can mostly map
locations to locations, without  changing values.
The exception is the program counter; its translation must use
{\Tt{}\({\mathit{codemap}}\)}, so
{\Tt{}\(\mathcal E[\![{\mathit{PC}}]\!]\nwpphat{{\sigma}} = {\mathit{codemap}}(\mathcal E[\![{\mathit{PC}}]\!]{\sigma})\)}. 
Given a map $\hatform\bullet$ on locations, we can easily extend it to
expressions like~{\Tt{}\(a_I\)}, {\Tt{}\(b_I\)}, and {\Tt{}\({\mathit{target}}_I\)}.
If {\Tt{}\(e\)}~is an expression, then {\Tt{}\(\mathcal E[\![\nwpphat{e}]\!]\nwpphat{{\sigma}} = \mathcal E[\![e]\!]{\sigma}\)}.

We assume that translations can be found for the computational
effects~{\Tt{}\(I_c\)}, which do not affect {\Tt{}\({\mathit{PC}}\)}, {\Tt{}\({\mathit{nPC}}\)}, or {\Tt{}\({\mathit{annul}}\)}.
We require only that
{\Tt{}\(\mathcal C[\![ \hatform{I_c} ]\!] \hatform{{\sigma}} = \hatform{ \mathcal C[\![I_c]\!] {\sigma} }\)}.
In general, {\Tt{}\(\hatform{I_c}\)} will be a sequence of instructions,
not exactly one instruction.
We also assume that, given any condition {\Tt{}\(b\)} and  address
{\Tt{}\({\mathit{target}}\)}, we can construct an 
instruction sequence implementing {\Tt{}\(b \mathbin{\rightarrow} {\mathit{PC}} \mathrel{:=} {\mathit{target}}\)} on the target
machine.
\nwenddocs{}\nwbegindocs{69}\nwdocspar
Under these assumptions, we analyze source branch
conditions~{\Tt{}\(b_I\)}, annulment conditions {\Tt{}\(a_I\)}, and target addresses
{\Tt{}\({\mathit{target}}_I\)}, and we show how to construct branch conditions and target
addresses for the target machine.
In the process, we build the {\Tt{}\({\mathit{codemap}}\)} function that takes source
program counters to target program counters.
\nwenddocs{}\nwbegindocs{70}\nwdocspar

\subsubsection{Structure of the translator}

Our translator works with one basic block at a time.
{\Tt{}\({\mathit{codemap}}\)} must be built
incrementally, by the translator itself, because the only way to know
the size of the target basic blocks is to translate the source basic
blocks.
%%  A static translator typically translates as many basic blocks as
%%  possible, keeping track by means of a work queue.
%%  A dynamic translator may translate basic blocks only on demand.
%%  In that case, the code it uses to translate {\Tt{}\({\mathit{PC}} \mathrel{:=} {\mathit{target}}\)} will
%%  depend on whether {\Tt{}\({\mathit{target}}\)} has been translated.
The translator maintains a work queue of untranslated blocks, each of
which is represented by a {\Tt{}\(({\mathit{pc}}_s, {\mathit{pc}}_t)\)} pair.
{\Tt{}\({\mathit{pc}}_s\)} is the address of some code on the source machine.
{\Tt{}\({\mathit{pc}}_t\)} may be the corresponding target-machine address, or more
likely a placeholder 
for a target-machine address, to be filled in later.
(For example, {\Tt{}\({\mathit{pc}}_t\)} might be a pointer to a basic block in a
control-flow graph.)
{\Tt{}\({\mathit{codemap}}\)} contains pairs that have already been translated.
We use the following auxiliary procedures:
\begin{itemize}
\item[]%
\opentab{1.5pt}
\begin{tabularx}{\linewidth}{@{}lY@{}}
\rlap{{\Tt{}\({\mathit{queueForTranslation}}({\mathit{pc}}_s, {\mathit{pc}}_t)\)}\qquad Add a pair to the work queue.}&\\
{\Tt{}\({\mathit{codemap}}({\mathit{pc}}_s)\)}& 
If a pair {\Tt{}\(({\mathit{pc}}_s, {\mathit{pc}}_t)\)} is in {\Tt{}\({\mathit{codemap}}\)}, return {\Tt{}\({\mathit{pc}}_t\)}.
Otherwise, let {\Tt{}\({\mathit{pc}}_t\)} be a fresh placeholder, add {\Tt{}\(({\mathit{pc}}_s, {\mathit{pc}}_t)\)}
to {\Tt{}\({\mathit{codemap}}\)}, and return~{\Tt{}\({\mathit{pc}}_t\)}.
(We use {\Tt{}\({\mathit{codemap}}\)} both as a function and as a collection of ordered
pairs, but these usages are equivalent.)
\\
{\Tt{}\({\mathit{emit}}({\mathit{pc}}_t, I)\)}&
Emit target-machine instructions~{\Tt{}\(I\)} at~{\Tt{}\({\mathit{pc}}_t\)},
returning a 
pointer to the location following the instructions.
If {\Tt{}\(I\)} is a sequence of {\Tt{}\(n\)}~instructions, {\Tt{}\({\mathit{emit}}({\mathit{pc}}_t, I)\)}
returns the result of applying {\Tt{}\({\mathit{succ}}_t\)} to {\Tt{}\({\mathit{pc}}_t\)}, {\Tt{}\(n\)}~times.
\\
{\Tt{}\({\mathit{newBlock}}()\)}&
Return a pointer to a fresh placeholder.
\end{tabularx}
\end{itemize}
Placeholders created with {\Tt{}\({\mathit{codemap}}\)} correspond to basic blocks in
the source program.
Placeholders created with {\Tt{}\({\mathit{newBlock}}\)} are artifacts of translation.
\nwenddocs{}\nwbegindocs{71}\nwdocspar
The translator loops, removing pairs from the work queue, and calling
{\Tt{}\({\mathit{trans}}\)} if those pairs have not already been translated.
{\Tt{}\({\mathit{trans}}\)} translates individual basic blocks.
If an instruction branches, {\Tt{}\({\mathit{trans}}\)} calls {\Tt{}\({\mathit{queueForTranslation}}\)} with the
target addresses (from source and target machines).
If an instruction flows through to its successor, {\Tt{}\({\mathit{trans}}\)} calls
itself tail-recursively.%
\footnote{Recursive calls to {\Tt{}\({\mathit{trans}}\)} could be replaced by calls to
{\Tt{}\({\mathit{queueForTranslation}}\)}.
The converse is not true, because {\Tt{}\({\mathit{trans}}\)} would recurse forever on loops.}
The outline of {\Tt{}\({\mathit{trans}}\)} is 
\nwenddocs{}\nwbegincode{72}\moddef{translator}\endmoddef\nwstartdeflinemarkup\nwenddeflinemarkup
\textbf{fun}{\ }\({\mathit{trans}} ({\mathit{pc}}_s, {\mathit{pc}}_t) \equiv \)
{\ }{\ }\LA{}put $(\mathit{pc}_s, \mathit{pc}_t)$ in $\mathit{codemap}$ if they are not there already\RA{}
{\ }{\ }\textbf{let}{\ }\(I\){\ }\textbf{as}{\ }\((b_I  \mathbin{\rightarrow} {\mathit{nPC}} \mathrel{:=} {\mathit{target}}_I  \mathrel{|} {\mathit{annul}} \mathrel{:=} a_I  \mathrel{|} I_c)  \equiv  {\mathit{src}}[{\mathit{pc}}_s]\)
{\ }{\ }\textbf{in}{\ }{\ }\textbf{case}{\ }\({\mathit{class}}(I)\){\ }\textbf{of}
{\ }{\ }{\ }{\ }{\ }{\ }\LA{}cases for translation of \code{}I\edoc{}\RA{}
{\ }{\ }\textbf{end}
\nwendcode{}\nwbegindocs{73}\nwdocspar

\subsubsection{Translations of SPARC instructions}

Deriving a translation function is tedious but straightforward.
For each class of instructions, we use
{\Tt{}\(a_I\)}~and~{\Tt{}\(b_I\)} to simplify {\Tt{}\({\mathit{stable}}\)}.
If necessary, we also consider {\Tt{}\(a_{I'}\)}~and~{\Tt{}\(b_{I'}\)}, where {\Tt{}\({I'}\)}~is
the instruction in the delay slot.
We transform the simplified {\Tt{}\({\mathit{stable}}\)} as needed until it
suggests an obvious translation, and finally we emit target-machine
instructions.
Space limitations allow us to show only a
few representative cases.
Table~\ref{tab:example-trans} shows example SPARC and Pentium assembly
language for each.
\nwenddocs{}\nwbegindocs{74}\nwdocspar
\begin{table}
\setlength\extrarowheight{1.5pt}
% l2h substitution newline <br>
% l2h let hatform overline
\let\newline\\
\begin{center}
\begin{tabular}{|ll|p{1.4in}|@{}p{1.8in}@{}|}
\hline
{\Tt{}\({\mathit{class}}(I)\)}&{\Tt{}\({\mathit{class}}({I'})\)}&
\multicolumn1{c|}{SPARC instructions}&
\multicolumn1{c|}{Pentium instructions}\\
\hline\hline
{\Tt{}\({\mathit{NCT}}\)}&any&
\verb+add %i1, %i2, %i3+&
\leavevmode\verb+     mov eax, SPARCI1+\newline
\leavevmode\verb+     add eax, SPARCI2+\newline
\leavevmode\verb+     mov SPARCI3, eax+\\
\hline
{\Tt{}\({\mathit{SU}}\)}&any&
\verb+ba,a L+&
\verb+     jmp +${\mathtt L}$\\
\hline
{\Tt{}\({\mathit{SD}}\)}&{\Tt{}\({\mathit{NCT}}\)}&
\verb+ba L+\newline
\verb+add %i1, %i2, %i3+&
\verb+     nop+\newline
\verb+     mov eax, SPARCI1+\newline
\verb+     add eax, SPARCI2+\newline
\verb+     mov SPARCI3, eax+\newline
\verb+     jmp +${\mathtt L}$\\
\hline
{\Tt{}\({\mathit{SCD}}\)}&{\Tt{}\({\mathit{NCT}}\)}&
\texttt{be L}\newline
\verb+mov %o1, %o2+\newline
\verb+  +$\vdots$
&
\verb+     nop+\newline
\verb+     je BB+\newline
\verb+     mov eax, SPARCO1+\newline
\verb+     mov SPARCO2, eax+\newline
\verb+       +$\vdots$\par
\medskip
\hrule
\smallskip
\noindent
\verb+ BB: mov eax, SPARCO1+\newline
\verb+     mov SPARCO2, eax+\newline
\verb+     jmp +${\mathtt L}$\\
\hline
{\Tt{}\({\mathit{SCDA}}\)}&{\Tt{}\({\mathit{NCT}}\)}&
\verb+be,a L+\newline
\verb+mov %o1, %o2+\newline
\verb+  +$\vdots$
&
\verb+     nop+\newline
\verb+     je BB+\newline
\verb+       +$\vdots$\par
\medskip
\hrule
\smallskip
\noindent
\verb+ BB: mov eax, SPARCO1+\newline
\verb+     mov SPARCO2, eax+\newline
\verb+     jmp +${\mathtt L}$\\
\hline
\end{tabular}
\end{center}

\ifhtml\else
\begin{quote}
\newsavebox\percentbox
\setbox\percentbox=\hbox{\verb+%+}
\newcommand\percent{\usebox{\percentbox}}
% l2h substitution percent %
SPARC assembly language puts the destination on the right, but Intel
assembly language puts the destination on the left.
The SPARC has more registers than the Pentium, so we map onto them
memory locations $\mathtt{SPARCI1} = \hatform\mathtt{\percent i1}$, 
$\mathtt{SPARCI2} = \hatform\mathtt{\percent i2}$, etc.
The last two examples show the same \texttt{be} instruction with and without
the~\texttt{,a} 
suffix (annul when branch not taken).
\end{quote}
\fi

\caption{Example translations from SPARC to Pentium}
\label{tab:example-trans}
\end{table}

\nwenddocs{}\nwbegindocs{75}\nwdocspar
The easiest cases are ones in which {\Tt{}\(a\)}'s~and~{\Tt{}\(b\)}'s are known
statically.
For non-control-transfer instructions, {\Tt{}\(b_I \equiv  \textbf{false}\)} and {\Tt{}\(a_I \equiv  \textbf{false}\)}, 
which corresponds to the last arm of {\Tt{}\({\mathit{stable}}\)}, and the translation is
\nwenddocs{}\nwbegincode{76}\moddef{cases for translation of \code{}I\edoc{}}\endmoddef\nwstartdeflinemarkup\nwenddeflinemarkup
\(\mathrel{|} {\mathit{NCT}} \mathrel{\Longrightarrow} {\mathit{pc}}_t \mathrel{:=} {\mathit{emit}}({\mathit{pc}}_t, \nwpphat{I_c}); {\mathit{trans}}({\mathit{succ}}_s({\mathit{pc}}_s), {\mathit{pc}}_t)\)
\nwendcode{}\nwbegindocs{77}\nwdocspar
The static unconditional branch with annul is just like an ordinary
branch. {\Tt{}\(b_I \equiv  \textbf{true}\)} and {\Tt{}\(a_I \equiv  \textbf{true}\)}, which corresponds to the
first arm of {\Tt{}\({\mathit{stable}}\)}, and the translation is
\nwenddocs{}\nwbegincode{78}\moddef{cases for translation of \code{}I\edoc{}}\plusendmoddef\nwstartdeflinemarkup\nwenddeflinemarkup
\(\mathrel{|} {\mathit{SU}} \mathrel{\Longrightarrow} {\mathit{pc}}_t \mathrel{:=} {\mathit{emit}}({\mathit{pc}}_t, {\mathit{PC}} \mathrel{:=} {\mathit{codemap}}({\mathit{target}}_I));\)
{\ }{\ }{\ }{\ }{\ }{\ }{\ }{\ }{\ }{\ }{\ }\({\mathit{queueForTranslation}}({\mathit{target}}_I, {\mathit{codemap}}({\mathit{target}}_I));\)
\nwendcode{}\nwbegindocs{79}\nwdocspar
The next simplest cases are 
the static delayed ({\Tt{}\({\mathit{SD}}\)}) class, with {\Tt{}\(b_I \equiv  \textbf{true}\)} and {\Tt{}\(a_I \equiv  \textbf{false}\)}. 
These instructions include unconditional branches and calls, and the
translation depends on what sort of instruction~{\Tt{}\({I'}\)} is found in the
delay slot.
\nwenddocs{}\nwbegincode{80}\moddef{cases for translation of \code{}I\edoc{}}\plusendmoddef\nwstartdeflinemarkup\nwenddeflinemarkup
\(\mathrel{|} {\mathit{SD}} \mathrel{\Longrightarrow}\)
{\ }{\ }\textbf{let}{\ }\((b_{I'} \mathbin{\rightarrow} {\mathit{nPC}} \mathrel{:=} {\mathit{target}}_{I'} \mathrel{|} {\mathit{annul}} \mathrel{:=} a_{I'} \mathrel{|} {I'}_c) \equiv  {\mathit{src}}[{\mathit{succ}}_s({\mathit{pc}}_s)]\)
{\ }{\ }\textbf{in}{\ }{\ }\textbf{case}{\ }\({\mathit{class}}({I'})\){\ }\textbf{of}
{\ }{\ }{\ }{\ }{\ }{\ }\LA{}translation cases for $\mathit{class}(I')$, where \code{}class(I)\ =\ SD\edoc{}\RA{}
{\ }{\ }\textbf{end}
\nwendcode{}\nwbegindocs{81}\nwdocspar
In the common case, we have a non-control-transfer instruction in the
delay slot, with {\Tt{}\(b_{I'} \equiv  \textbf{false}\)} and {\Tt{}\(a_{I'} \equiv  \textbf{false}\)}.
This corresponds to the fifth arm of {\Tt{}\({\mathit{stable}}\)}, which executes
\mbox{{\Tt{}\([\![I_c]\!]; {\mathit{PC}} \mathrel{:=} {\mathit{target}}_I \mathrel{|} [\![{I'}_c]\!]\)}}.
Since {\Tt{}\({\mathit{target}}_I\)} is a constant, we can rewrite this as
\mbox{{\Tt{}\([\![I_c]\!]; [\![{I'}_c]\!]; {\mathit{PC}} \mathrel{:=} {\mathit{target}}_I\)}}.
The translation is then%
\nwenddocs{}\nwbegincode{82}\moddef{translation cases for $\mathit{class}(I')$, where \code{}class(I)\ =\ SD\edoc{}}\endmoddef\nwstartdeflinemarkup\nwenddeflinemarkup
\(\mathrel{|} {\mathit{NCT}} \mathrel{\Longrightarrow}\)
{\ }{\ }{\ }\({\mathit{pc}}_t \mathrel{:=} {\mathit{emit}}({\mathit{pc}}_t, \nwpphat{I_c});\)
{\ }{\ }{\ }\({\mathit{pc}}_t \mathrel{:=} {\mathit{emit}}({\mathit{pc}}_t, \nwpphat{{I'}_c});\)
{\ }{\ }{\ }\({\mathit{pc}}_t \mathrel{:=} {\mathit{emit}}({\mathit{pc}}_t, {\mathit{PC}} \mathrel{:=} {\mathit{codemap}}({\mathit{target}}_I));\)
{\ }{\ }{\ }\({\mathit{queueForTranslation}}({\mathit{target}}_I, {\mathit{codemap}}({\mathit{target}}_I));\)
\nwendcode{}\nwbegindocs{83}This translation is not sufficient for call instructions, because 
a called procedure may use the program counter
captured by~{\Tt{}\(I_c\)}, and its use of that program counter is determined
by software convention, not by the semantics of the hardware.
On the SPARC, if {\Tt{}\(I\)}~is a call instruction, translation
should resume with \mbox{{\Tt{}\({\mathit{trans}}({\mathit{succ}}_s({\mathit{succ}}_s({\mathit{pc}}_s)), {\mathit{pc}}_t)\)}}, or if
the call returns a structure, with
 \mbox{{\Tt{}\({\mathit{trans}}({\mathit{succ}}_s({\mathit{succ}}_s({\mathit{succ}}_s({\mathit{pc}}_s))), {\mathit{pc}}_t)\)}}.
\iftr
\nwenddocs{}%
%
%
%
%
%
%
%
%
\nwbegindocs{85}    
\nwenddocs{}%
%
%
%
%
%
%
%
%
\nwbegindocs{87}    
\nwenddocs{}%
%
%
%
%
%
%
%
\nwbegindocs{89}    
\nwenddocs{}%
%
%
%
%
%
%
\nwbegindocs{91}\nwdocspar
\nwenddocs{}%
%
%
%
%
%
%
\nwbegindocs{93}\nwdocspar
\fi
\nwenddocs{}\nwbegindocs{94}\nwdocspar
The treatment of class {\Tt{}\({\mathit{DD}}\)} (dynamic delayed) branches is similar to
that of class~{\Tt{}\({\mathit{SD}}\)},
except that the target addresses are computed dynamically.
This means that it is not possible to use {\Tt{}\({\mathit{codemap}}\)} at translation time;
the translated code might use {\Tt{}\({\mathit{codemap}}\)} at run time, or
it might call an interpreter or a dynamic translator.
\nwenddocs{}\nwbegindocs{95}\nwdocspar
The most common class involving dynamic conditions is the {\Tt{}\({\mathit{SCD}}\)}
(static conditional delayed) class, in which {\Tt{}\(b_I\)} is dynamic and
{\Tt{}\(a_I\)} is {\Tt{}\(\textbf{false}\)}.
Again, the translation depends on what is in the delay slot.
\nwenddocs{}\nwbegindocs{96}\nwdocspar
\nwenddocs{}\nwbegincode{97}\moddef{cases for translation of \code{}I\edoc{}}\plusendmoddef\nwstartdeflinemarkup\nwenddeflinemarkup
\(\mathrel{|} {\mathit{SCD}} \mathrel{\Longrightarrow}\)
{\ }{\ }\textbf{let}{\ }\((b_{I'} \mathbin{\rightarrow} {\mathit{nPC}} \mathrel{:=} {\mathit{target}}_{I'} \mathrel{|} {\mathit{annul}} \mathrel{:=} a_{I'} \mathrel{|} {I'}_c) \equiv  {\mathit{src}}[{\mathit{succ}}_s({\mathit{pc}}_s)]\)
{\ }{\ }\textbf{in}{\ }{\ }\textbf{case}{\ }\({\mathit{class}}({I'})\){\ }\textbf{of}
{\ }{\ }{\ }{\ }{\ }{\ }\LA{}translation cases for $\mathit{class}(I')$, where \code{}class(I)\ =\ SCD\edoc{}\RA{}
{\ }{\ }\textbf{end}
\nwendcode{}\nwbegindocs{98}\nwdocspar
The most common delay instruction is a
non-control-transfer instruction (class {\Tt{}\({\mathit{NCT}}\)}), where {\Tt{}\(b_{I'} = \textbf{false}\)}
and {\Tt{}\(a_{I'} = \textbf{false}\)}.
In this case, {\Tt{}\({\mathit{stable}}\)} reduces to
\begin{quote}
\nwenddocs{}\nwbegincode{99}\moddef{specialization of \code{}stable\edoc{} for \code{}SCD\edoc{} with \code{}NCT\edoc{} in the delay slot}\endmoddef\nwstartdeflinemarkup\nwenddeflinemarkup
\textbf{if}{\ }\([\![b_I]\!]\){\ }\textbf{then}
{\ }{\ }\([\![I_c]\!]; {\mathit{PC}} \mathrel{:=} [\![{\mathit{target}}_I]\!] \mathrel{|} [\![{I'}_c]\!]; {\mathit{stable}}()\)
\textbf{else}
{\ }{\ }\([\![I_c]\!] \mathrel{|} {\mathit{PC}} \mathrel{:=} {\mathit{succ}}_s({\mathit{PC}}); {\mathit{stable}}()\)
\textbf{fi}
\nwendcode{}\nwbegindocs{100}\nwdocspar
\end{quote}
Because {\Tt{}\(I_c\)} does not affect~{\Tt{}\({\mathit{PC}}\)}, we
transform {\Tt{}\({\mathit{stable}}\)} as follows:%
\footnote{%
We have the alternative of unfolding the call to {\Tt{}\({\mathit{stable}}\)} in the
{\Tt{}\textbf{else}} branch and moving both {\Tt{}\(I_c\)} and {\Tt{}\({I'}_c\)} ahead of
the~{\Tt{}\textbf{if}}.
This transformation leads to a translation in which {\Tt{}\({I'}_c\)} moves
ahead of the branch, and {\Tt{}\({I'}_c\)}'s successor follows the branch.
Epoxie and Noxie use this translation \cite{wall:systems}.
The problem is that, if the branch condition {\Tt{}\(b_I\)} tests condition
codes, and {\Tt{}\({I'}_c\)} sets condition codes, it will be necessary to save
and restore the condition codes in order to get the correct branch
instruction.
It is much simpler to move {\Tt{}\({I'}_c\)} into a new block, which
the optimizer can sometimes eliminate.}
\begin{quote}
\nwenddocs{}\nwbegincode{101}\moddef{transformed specialization of \code{}stable\edoc{} for \code{}SCD\edoc{} with \code{}NCT\edoc{} in the delay slot}\endmoddef\nwstartdeflinemarkup\nwenddeflinemarkup
\([\![I_c]\!];\)
\textbf{if}{\ }\([\![b_I]\!]\){\ }\textbf{then}
{\ }{\ }\({\mathit{PC}} \mathrel{:=} [\![{\mathit{target}}_I]\!] \mathrel{|} [\![{I'}_c]\!]\)
\textbf{else}
{\ }{\ }\({\mathit{PC}} \mathrel{:=} {\mathit{succ}}_s({\mathit{PC}});\)
\textbf{fi}
\(; {\mathit{stable}}()\)
\nwendcode{}\nwbegindocs{102}\nwdocspar
\end{quote}
In general,  no single target instruction implements
\mbox{{\Tt{}\({\mathit{PC}} \mathrel{:=} [\![{\mathit{target}}_I]\!] \mathrel{|} [\![{I'}_c]\!]\)}}, so we rewrite it into the
sequence \mbox{{\Tt{}\([\![{I'}_c]\!]; {\mathit{PC}} \mathrel{:=} [\![{\mathit{target}}_I]\!]\)}}, and we put this
sequence into a new ``trampoline'' basic block {\Tt{}\({\mathit{bb}}\)}.
{\Tt{}\({\mathit{stable}}\)} becomes
\begin{quote}
\nwenddocs{}\nwbegincode{103}\moddef{final specialization of \code{}stable\edoc{} for \code{}SCD\edoc{} with \code{}NCT\edoc{} in the delay slot}\endmoddef\nwstartdeflinemarkup\nwenddeflinemarkup
\([\![I_c]\!];\)
\textbf{if}{\ }\([\![b_I]\!]\){\ }\textbf{then}
{\ }{\ }\({\mathit{PC}} \mathrel{:=} {\mathit{bb}};\)
\textbf{else}
{\ }{\ }\({\mathit{PC}} \mathrel{:=} {\mathit{succ}}_s({\mathit{PC}});\)
\textbf{fi}
\(; {\mathit{stable}}()\)
\nwendcode{}\nwbegindocs{104}\nwdocspar
\end{quote}
which we translate using an ordinary branch instruction:
\nwenddocs{}\nwbegincode{105}\moddef{translation cases for $\mathit{class}(I')$, where \code{}class(I)\ =\ SCD\edoc{}}\endmoddef\nwstartdeflinemarkup\nwenddeflinemarkup
\(\mathrel{|} {\mathit{NCT}} \mathrel{\Longrightarrow}\)
{\ }{\ }{\ }\textbf{local}{\ }\({\mathit{bb}} \mathrel{:=} {\mathit{newBlock}}();\)
{\ }{\ }{\ }\({\mathit{pc}}_t \mathrel{:=} {\mathit{emit}} ({\mathit{pc}}_t, \nwpphat{I_c});\)
{\ }{\ }{\ }\({\mathit{pc}}_t \mathrel{:=} {\mathit{emit}} ({\mathit{pc}}_t, \hatform{b_I} \mathbin{\rightarrow} {\mathit{PC}} \mathrel{:=} {\mathit{bb}});\)
{\ }{\ }{\ }\({\mathit{bb}} \mathrel{:=} {\mathit{emit}} ({\mathit{bb}}, \nwpphat{{I'}_c});\)
{\ }{\ }{\ }\({\mathit{bb}} \mathrel{:=} {\mathit{emit}} ({\mathit{bb}}, {\mathit{PC}}\mathrel{:=}{\mathit{codemap}}({\mathit{target}}_I));\)
{\ }{\ }{\ }\({\mathit{queueForTranslation}} ({\mathit{target}}_I, {\mathit{codemap}}({\mathit{target}}_I));\)
{\ }{\ }{\ }\({\mathit{trans}}({\mathit{succ}}_s({\mathit{pc}}_s)), {\mathit{pc}}_t);\)
\nwendcode{}\nwbegindocs{106}\nwdocspar
The cases for class \emph{SCDA} (static delayed branches that annul
when not taken) are similar to those of class \emph{SCD}.
For example,
when {\Tt{}\({\mathit{SCDA}}\)} is followed by {\Tt{}\({\mathit{NCT}}\)}, {\Tt{}\(b_I\)}~is dynamic, {\Tt{}\(a_I \equiv  \lnot  b_I\)},
and {\Tt{}\(b_{I'} \equiv  a_{I'} \equiv  \textbf{false}\)}.
{\Tt{}\({\mathit{stable}}\)} reduces to:
\begin{quote}
\nwenddocs{}\nwbegincode{107}\moddef{specialization of \code{}stable\edoc{} for \code{}SCDA\edoc{} with \code{}NCT\edoc{} in the delay slot}\endmoddef\nwstartdeflinemarkup\nwenddeflinemarkup
\([\![I_c]\!];\)
\textbf{if}{\ }\([\![b_I]\!]\){\ }\textbf{then}
{\ }{\ }\([\![{I'}_c]\!];\)
{\ }{\ }\({\mathit{PC}} \mathrel{:=} [\![{\mathit{target}}_I]\!]\)
\textbf{else}
{\ }{\ }\({\mathit{PC}} \mathrel{:=} {\mathit{succ}}_s({\mathit{succ}}_s({\mathit{PC}}));\)
\textbf{fi}
\(; {\mathit{stable}}()\)
\nwendcode{}\nwbegindocs{108} 
\end{quote}
The translation is like that of class {\Tt{}\({\mathit{SCD}}\)}, creating a new basic
block, but the recursive call is 
{\Tt{}\({\mathit{trans}}({\mathit{succ}}_s({\mathit{succ}}_s({\mathit{pc}}_s)), {\mathit{pc}}_t)\)},
so
translation resumes \emph{after} the delay slot instead of \emph{at}
the delay slot.
\nwenddocs{}\nwbegindocs{109}\nwdocspar

\subsubsection{Simplified translation of many branch instructions}

When translating a branch with a non-branch in the delay slot, our
method can be reduced to a simple strategy:
rewrite the branch as a non-delayed branch, and 
push the delay instruction to the destination address, the
fall-through address, neither, or both, according to the table below.
\begin{quote}%figure
\opentab{1.5pt}
\begin{tabularx}{\linewidth}{@{}lX@{}}
{\Tt{}\(a_I \equiv      b_I\)}&  Push the delay instruction to the fall-through address.\\
{\Tt{}\(a_I \equiv  \lnot  b_I\)}&  Push the delay instruction to the destination address.\\
{\Tt{}\(a_I \equiv  \textbf{false}\)}& Push the delay instruction to both addresses.\\
{\Tt{}\(a_I \equiv  \textbf{true}\)}& Discard the delay instruction.\\
\end{tabularx}
\end{quote}
To push the delay instruction to the destination address,
we create a new ``trampoline'' basic block, which avoids problems in case
other branches also flow to the same address.

The last three entries in 
Table~\ref{tab:example-trans} show how this strategy is applied 
to the unconditional (\emph{SD}), conditional (\emph{SCD}), and conditional
annuled (\emph{SCDA}) branches on the SPARC.
On the MIPS, programmers may not put branches in delay slots
\cite[Appendix~A]{kane:mips}, and {\Tt{}\(a_I \equiv  \textbf{false}\)} always, so a
single instance of this strategy applies to every branch instruction
\cite{srivastava:practical}. 

\iftr
\section{The rough part}

\label{sec:bad-bb}

\nwenddocs{}\nwbegindocs{110}\nwdocspar
Let's consider the troublesome case:
\nwenddocs{}%
%
%
%
\nwbegindocs{112}\nwdocspar
Unfold {\Tt{}\({\mathit{loop}}\)}, renaming {\Tt{}\(I\)} to {\Tt{}\({I''}\)}.
\nwenddocs{}%
%
%
%
%
%
%
%
%
%
%
%
%
\nwbegindocs{114}\nwdocspar
Simplify.
\nwenddocs{}%
%
%
%
%
%
%
%
%
%
%
\nwbegindocs{116}\nwdocspar
Propagate {\Tt{}\({\mathit{loop}}\)} across arms of {\Tt{}\textbf{if}}, and unfold it.
\nwenddocs{}%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
\nwbegindocs{118}\nwdocspar
Re-roll into {\Tt{}\({\mathit{stable}}\)}?
\fi


\section{Proving Correctness}


\def\subst[#1/#2]{\mathrm{subst}^{#1}_{#2}}
 
\label{sec:transition-lemma}
\label{sec:proof}

We prove correctness of translation by reasoning about transitions
from states to states.
As noted in Section~\ref{sec:informal-simulation}, we want to show
that running the translated code results in an execution on the target
machine that simulates the original execution on the soure machine.
Formally,
if we start the source machine
in a state~$\src1$, and the {\Tt{}\({\mathit{loop}}\)} function takes it through a sequence of
states $\src1, \src2, \ldots$, then there is a subsequence of such
states $\src{k_1}, \src{k_2}, \ldots$ such that $\hatform{\src{k_1}},
\hatform{\src{k_2}}, \ldots$  is a subsequence of the states that the
target machine goes through when started in state $\tgt1 = \hatform{\src1}$.

The result desired follows directly from this \emph{transition theorem}:
If $\src m$ is a source-machine state such that
\begin{enumerate} 
\item
\label{stable-cond-a}
{\Tt{}\(\mathcal E[\![{\mathit{annul}} = \textbf{false} \land  {\mathit{nPC}} = {\mathit{succ}}_s({\mathit{PC}})]\!]\presigma{s}_m\)}, 
\item
there is a corresponding target-machine state $\tgt n =
\hatform{\src m}$, and
\item
\label{trans-called-a}
{\Tt{}\({\mathit{trans}}\)} has been called with arguments 
$(\calexp{PC}\src m, \calexp{PC}\tgt n)$,
\end{enumerate}
then there is an~$i$ such that in $i$~steps, the source machine
reaches a state~$\src{m+i}$ that also satisfies
{\Tt{}\(\mathcal E[\![{\mathit{annul}} = \textbf{false} \land  {\mathit{nPC}} = {\mathit{succ}}_s({\mathit{PC}})]\!]\src{m+i}\)}.
Also, there is a~$j$ such that in $j$~steps,
the target machine reaches
a state~$\tgt {n+j} = \hatform{\src{m+i}}$, and
furthermore (a) $i>0$ or $j>0$ and (b) {\Tt{}\({\mathit{trans}}\)} has been called with 
arguments $(\calexp{PC}\src {m+i}, \calexp{PC}\tgt {n+j})$.


We prove the transition theorem by case analysis on the
classes of the instructions located at {\Tt{}\({\mathit{src}}[{\mathit{PC}}]\)}.
We use the standard rule for sequential composition 
(\mbox{{\Tt{}\(\mathcal C[\![R_1; R_2]\!] = \mathcal C[\![R_2]\!] \circ  \mathcal C[\![R_1]\!]\)}})
as well as the identities for the translation of
expressions and computational effects:
\begin{quote}
{\Tt{}\(\mathcal E[\![\nwpphat{e}]\!]\nwpphat{{\sigma}} = \mathcal E[\![e]\!]{\sigma}\)}\\[2pt]
{\Tt{}\(\hatform{ \mathcal C[\![I_c]\!] {\sigma} } = \mathcal C[\![ \hatform{I_c} ]\!] \hatform{{\sigma}}\)}
\end{quote}

Because of condition~\ref{stable-cond-a}, we can substitute
{\Tt{}\({\mathit{stable}}\)} for {\Tt{}\({\mathit{loop}}\)}, so we can apply our transformed version of
{\Tt{}\({\mathit{stable}}\)}, which assigns directly to~{\Tt{}\({\mathit{PC}}\)}.
We assume that all mappings~$\hatform\bullet$ use \emph{codemap} to
map the source program counter to the target program counter.
To translate a branch, we therefore write
\begin{itemize}%figure
\item[]
\begin{tabularx}{\linewidth}{@{}lX}
{\Tt{}\(\hatform{ \mathcal C[\![ {\mathit{PC}} \mathrel{:=} {\mathit{target}} ]\!] {\sigma} }\)} &= {\Tt{}\(\hatform{\subst[{\mathit{target}}/{\mathit{PC}}]{\sigma}}\)}\\
&= {\Tt{}\(\subst[{\mathit{codemap}}({\mathit{target}}) / \hatform{{\mathit{PC}}}] \hatform{{\sigma}}\){\ }}\\
&= {\Tt{}\(\subst[{\mathit{codemap}}({\mathit{target}}) / {\mathit{PC}}] \hatform{{\sigma}}\){\ }}\\
&= {\Tt{}\(\mathcal C[\![ {\mathit{PC}} \mathrel{:=} {\mathit{codemap}}({\mathit{target}}) ]\!] \hatform{{\sigma}}\)}\hfill$(*)$\\
\end{tabularx}
\end{itemize}


The simplest case in the proof of the transition theorem is a
non-control-transfer instruction (\emph{NCT}).
The canonical form of such an instruction is
\begin{quote} 
{\Tt{}\(\textbf{false} \mathbin{\rightarrow} {\mathit{nPC}} \mathrel{:=} {\mathit{any}} \mathrel{|} {\mathit{annul}} \mathrel{:=} \textbf{false} \mathrel{|} I_c\)}.
\end{quote}
The action of {\Tt{}\({\mathit{stable}}\)} on this form is 
\mbox{{\Tt{}\(\mathcal C[\![{\mathit{PC}} \mathrel{:=} {\mathit{succ}}_s({\mathit{PC}}) \mathrel{|} I_c]\!]\)}}.
{\Tt{}\(I_c\)}~leaves the program counter unchanged, so we rewrite
this as \mbox{{\Tt{}\(\mathcal C[\![I_c; {\mathit{PC}} \mathrel{:=} {\mathit{succ}}_s({\mathit{PC}})]\!]\)}}.
The binary translation has the form {\Tt{}\(\nwpphat{I_c}\)}, which may be a sequence
of {\Tt{}\(j\)}~instructions.
Therefore {\Tt{}\(j\)}~applications of {\Tt{}\({\mathit{simple}}\)}, or equivalently,
{\Tt{}\(j\)}~state transitions on the target machine, have the effect of
\mbox{{\Tt{}\(\mathcal C[\![\nwpphat{I_c}; {\mathit{PC}} \mathrel{:=} \mathit{succ}_t^{(j)}({\mathit{PC}})]\!]\)}}.
Given {\Tt{}\(\presigma{s}_m\)}~and~{\Tt{}\(\presigma{t}_n\)} satisfying the hypotheses of the
transition theorem, after one step, the source machine reaches the
state
\[%figure
\src{m+1} = \cmd{\pc \gets \mathit{succ}_s(\pc)} (\cmd{I_c} \src m).
\]
After $j$~steps, the target machine reaches a state
%\[
\begin{eqnarray*}%figure
\tgt{n+j} &=& 
\cmd{\pc \gets \mathit{succ}_t^{(j)}(\pc)} (\cmd{\hatform{I_c}} \tgt n)\\
&=&
\cmd{\pc \gets \mathit{succ}_t^{(j)}(\pc)} (\cmd{\hatform{I_c}} \hatform{\src m})\\
&=&
\cmd{\pc \gets \mathit{succ}_t^{(j)}(\pc)} (\hatform{\cmd{I_c} {\src m}})
  \end{eqnarray*}
%\]
>From {\Tt{}\({\mathit{trans}}\)}, {\Tt{}\({\mathit{codemap}}({\mathit{succ}}_s({\mathit{pc}}_s)) = \mathit{succ}_t^{(j)}({\mathit{pc}}_t)\)}, so by~$(*)$ 
%\[
\begin{eqnarray*}%figure
\tgt{n+j} &=& 
\hatform{\cmd{\pc \gets \mathit{succ}_s(\pc)} (\cmd{I_c} {\src m})}\\
&=&\hatform{\src{m+1}}
  \end{eqnarray*}
%\]
Thus, after one step on the source and {\Tt{}\(j\)}~steps on the target, we
again reach a pair of states satisfying the conditions of the
transition theorem.


As another example, consider an instruction of
class~{\Tt{}\({\mathit{SCD}}\)} with an instruction of class~{\Tt{}\({\mathit{NCT}}\)} in the delay slot.
If the source machine begins in state~{\Tt{}\(\presigma{s}\)}, after 1~or~2 steps it reaches
state~$\presigmap s$, where
\begin{quote}%figure
\noindent\rlap{%
\begin{tabular}{@{}l@{}l}
$\presigmap s = \mbox{}$&
{\Tt{}\textbf{if}{\ }\(\mathcal E[\![b_I]\!](\mathcal C[\![I_c]\!]\presigma{s})\){\ }\textbf{then}{\ }\((\mathcal C[\![{\mathit{PC}} \mathrel{:=} {\mathit{target}}_I]\!] \circ  \mathcal C[\![{I'}_c]\!] \circ  \mathcal C[\![I_c]\!]) \presigma{s}\)}\\
&{\Tt{}\textbf{else}{\ }\((\mathcal C[\![{\mathit{PC}} \mathrel{:=} {\mathit{succ}}_s({\mathit{PC}})]\!] \circ  \mathcal C[\![I_c]\!]) \presigma{s}\){\ }\textbf{fi}}\\
\end{tabular}}
\end{quote}
If the target machine begins in state~{\Tt{}\(\presigma{t} = \nwpphat{\presigma{s}}\)}, it
reaches state~$\presigmap t$, where
\begin{quote}%figure
\noindent\rlap{%
\begin{tabular}{@{}l@{}l}
$\presigmap t = \mbox{}$&
{\Tt{}\textbf{if}{\ }\(\mathcal E[\![\nwpphat{b_I}]\!](\mathcal C[\![\nwpphat{I_c}]\!]\nwpphat{\presigma{s}})\){\ }\textbf{then}}\\
&\quad{\Tt{}\((\mathcal C[\![{\mathit{PC}} \mathrel{:=} {\mathit{codemap}}({\mathit{target}}_I)]\!]\circ \mathcal C[\![\nwpphat{{I'}_c}]\!]\circ \mathcal C[\![{\mathit{PC}} \mathrel{:=} {\mathit{bb}}]\!] \circ  \mathcal C[\![\nwpphat{I_c}]\!]) \nwpphat{\presigma{s}}\)}\\
&{\Tt{}\textbf{else}}\\
&\quad{\Tt{}\((\mathcal C[\![{\mathit{PC}} \mathrel{:=} {\mathit{succ}}_t({\mathit{PC}})]\!] \circ  \mathcal C[\![\nwpphat{I_c}]\!]) \nwpphat{\presigma{s}}\){\ }\textbf{fi}}\\
\end{tabular}}
\end{quote}
Because \mbox{{\Tt{}\(\mathcal C[\![{\mathit{PC}} \mathrel{:=} t_1]\!] \circ  \mathcal C[\![{\mathit{PC}} \mathrel{:=} t_2]\!] = \mathcal C[\![{\mathit{PC}} \mathrel{:=} t_1]\!]\)}}, and
because {\Tt{}\(\mathcal C[\![\nwpphat{{I'}_c}]\!]\)} commutes with assignments to~{\Tt{}\({\mathit{PC}}\)}, 
it is easy to show that $\presigmap t = \hatform{\presigmap s}$.
{\hfuzz=7pt\par}

The other cases for translation can be proved correct in similar fashion.
\nwenddocs{}\nwbegindocs{119}\nwdocspar


\section{Experience}
\label{sec:exp}

We have used translators for delayed branches in two tools:
a binary translator and a decompiler \opencite{cifuentes:assembly}.
In both tools, we translate machine instructions into a low-level,
machine-independent intermediate form \emph{without} delayed branches.
The binary translator uses this form to generate target code, applying
standard
optimization techniques.  
The decompiler analyzes the intermediate form to recover
high-level information like structured control flow.

There are many issues that are relevant to completely
general binary translation but which are beyond the scope of this
paper.
\begin{itemize}
\item
Our translator does not guarantee that the source and target codes
have  the same 
atomicity properties; providing atomic three-address operations on a
two-address machine would be prohibitively expensive.
\item
Self-modifying code and dynamic code generation can be handled either
by resorting to interpretation or by invoking the translator
dynamically; we intend to evaluate these alternatives experimentally.
\item
Different machines use different representations of condition
codes, and a na\"\i ve translation would emulate the source-machine
condition codes in a target-machine register.
This emulation may be necessary in some cases (e.g., when a Pentium
program depends on the value of the ``parity of the least-significant
byte'' bit), but in common cases, one definition of condition codes
reaches one use (in a conditional branch), and the source-machine
condition code can be eliminated by forward substitution.
\item 
The CPU model used in this paper models hardware exceptions as assignment to a
special ``exception location.''
This model is suitable only for a machine with precise exceptions.
It is an open question whether a similar formalism could help derive a
translation between machines with precise and imprecise exceptions.
\end{itemize}



Our original implementation was based on a case analysis of the
SPARC's architecture manual.
This analysis created an extra basic block for every delayed instruction 
that needed to be executed along any given path.  
More seriously, the analysis did not cover all cases, as there were many
combinations whose meaning was not clear from a direct reading of the
manual.
It was difficult even to characterize the set of binary codes that
could be analyzed.
These difficulties motivated the work presented here.

We have since replaced our original implementation with one based on
the method described in this paper.
The new implementation is used in both tools.
The advantages of the new method are three-fold: it can handle any
branch in a delay slot, even if the target is a branch;
it generates better intermediate code than before;
and we recover control-flow graphs with fewer basic blocks.  
%% We attribute these advantages to the case analysis based on different
%% combinations  of {\Tt{}\(a_I\)}~and~{\Tt{}\(b_I\)}.





All the transformations discussed in this paper were done 
by hand.  
We investigated tools that might have helped us transform {\Tt{}\({\mathit{stable}}\)},
but we were left with the impression that this is 
still a research problem \cite{shankar:mechanizing}, and
it was easy enough to transform {\Tt{}\({\mathit{stable}}\)} by hand.
By contrast, it would be very useful to automate
the derivation of the translator from {\Tt{}\({\mathit{stable}}\)} and the discovery of
the translations of the {\Tt{}\(a_I\)}'s, {\Tt{}\(b_I\)}'s, and~{\Tt{}\(I_c\)}'s.
This work is not intellectually demanding, but it is tedious because
there are many cases.

Our implementation includes simple optimizations not mentioned above.
For example, we do not create the
\texttt{nop} instructions shown in Table~\ref{tab:example-trans}
when {\Tt{}\(I_c\)} is {\Tt{}\textbf{skip}}.
There are also many cases in which further transformation
of~{\Tt{}\({\mathit{stable}}\)} can show that it is not necessary to create new basic
blocks. 


To test the correctness of our implementation, we developed a test
suite that includes not only standard programs but also artificial
programs with different kinds of branches in delay slots.
We checked by hand that
the intermediate forms and control-flow graphs derived from the
translation were
correct at each relevant basic block.  

\label{sec:limit-unfold}
As presented in this paper, a branch in a delay slot requires a
recursive call to~{\Tt{}\({\mathit{loop}}\)}, not to {\Tt{}\({\mathit{stable}}\)}.
Most cases, including all those shown in the SPARC manual, can be
handled by an additional unfolding of~{\Tt{}\({\mathit{loop}}\)}, 
which we have done in our implementation.
%This additional unfolding handles all cases of branches in delay
%slots, except when the target of the first branch is itself a branch.%
The unfolding game can go on indefinitely; no matter how many times we unfold
{\Tt{}\({\mathit{loop}}\)}, a single recursive call to {\Tt{}\({\mathit{loop}}\)} remains, and it is
always possible to write a program whose interpretation reaches this
recursive call. 
Because a program that does this indefinitely is not useful
(it does nothing but jump from one branch to another, never executing a
computational instruction), 
we have cut off the unfolding at one step
beyond what is shown in this paper.
This level of unfolding handles the case of two branch instructions
$I_1$~and~$I_2$, where $I_2$~is in $I_1$'s delay slot.
If the target of~$I_1$ is also a branch instruction, our system currently
rejects the code.
We have not decided whether it will eventually fall back on an
interpreter, or whether we will develop a fallback translation algorithm to
which both
{\Tt{}\({\mathit{nPC}}\)} and {\Tt{}\({\mathit{PC}}\)} are parameters.



%%Surprisingly, a limited case of branch-after-branch is actually used
%%in practice. 
%%To return from a trap, a SPARC interrupt handler executes the
%%two-instruction sequence
%%\begin{verbatim}
%%  jmpl %r17,%r0    ! restore PC
%%  rett %r18        ! restore nPC and the rest of the CPU state
%%\end{verbatim}
%%Various other games can be played, including restoring the state to
%%the instruction that \emph{dynamically} should follow the interrupted
%%instruction.
%%Our translator has not yet had to deal with such sequences, because we
%%are limiting our attention to the translation of user code, and
%%\texttt{rett} is a privileged instruction.


%\begin{ack}
%We thank Jack Davidson for helpful discussions and Mike van Emmerik 
%for the implementation of the algorithm. 
%This work has been supported by grant A49702762 from the Australian Research
%Council.
%The first author has additional support from  National Science
%Foundation grants ASC-9612756 and CCR-9733974
% and from DARPA contract MDA904-97-C-0247. 
%The second author has additional support from Sun Microsystems.
%\end{ack}



%\appendix



%\bibliographystyle{nchicago}
%\def\bibfont{\normalsize\raggedright}
%\bibliography{cs,ml,ramsey,web}
%\nwenddocs{}\nwbegindocs{120}\nwdocspar
%\end{document}



%\nwenddocs{}
