A Transformational Approach to Binary Translation of Delayed Branches

NORMAN RAMSEY Division of Engineering and Applied Sciences Harvard University, Cambridge, MA 01238 USA

nr@eecs.harvard.edu

and CRISTINA CIFUENTES Department of Computer Science and Electrical Engineering University of Queensland, Brisbane, QLD 4072 Australia

cristina@csee.uq.edu.au

A binary translator examines binary code for a source machine, builds an intermediate representation, and generates code for a target machine. Understanding what to do with delayed branches in binary code can involve tricky case analyses, e.g., if there is a branch instruction in a delay slot. This paper 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 supports such common architectures as SPARC, MIPS, and PA-RISC, and it should apply to any tool that analyzes machine instructions.

We begin by writing a very simple interpreter for the source machine’s code. 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 sourcemachine 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 reasoning about corresponding states on source and target machines.

Categories and Subject Descriptors: D.3.4 [Programming Languages]: Processors; I.1.4 [Computing Methodologies]: Symbolic and Algebraic Manipulation—Applications

General Terms: Experimentation, Languages

Additional Key Words and Phrases: Binary translation, program analysis, program transformation

C. Cifuentes’s current address: Sun Microsystems, Inc., cristina.cifuentes@eng.sun.com.

2 · N. Ramsey and C. Cifuentes

1. INTRODUCTION

Binary translation makes it possible to run code compiled for source platform S on target platform T. Unlike interpreted or emulated code, binary-translated code approaches the speed of native code on machine T. Hardware vendors can use binary translation to provide a tempting array of software along with new machines [Bergh et al. 1987; May 1987; Andrews and Sand 1992; Sites et al. 1993; Ebcioğlu and Altman 1997]. Hardware buyers can use binary translation to run old code on new machines. This ability is particularly valuable when the old code is available only in binary form, e.g., when it has been purchased from a third party or its source code has been lost. Finally, binary translation is also an enabling technology for efficient simulation [Cmelik and Keppel 1994; Witchel and Rosenblum 1996].

The fundamental steps in binary translation are to distinguish code from data, to map data locations from the source to the target machine, and to translate instructions. Data must be translated differently from code, pointers must be translated differently from non-pointers, and code pointers (e.g., for indirect branches) must be translated differently from data pointers [Sites et al. 1993; Larus and Ball 1994]. This paper focuses on translation; the problem of distinguishing code from data is difficult, but solutions are well known.

When a mapping from source locations to target locations has been established, translating instructions is mostly straightforward. Finding the target instructions needed to achieve a particular effect is simply code generation. It is not always obvious, however, what is the effect of a delayed-branch instruction, especially when a branch or call instruction appears in a delay slot. The contribution of this paper is a disciplined method for understanding the effects of delayed branches, even in tricky, rarely used combinations. This method identifies cases that are problematic for translation, shows the translations for the non-problematic cases, and gives confidence that all cases are considered. We have applied the results of the method to the University of Queensland binary translator [Cifuentes et al. 1999; Cifuentes and Van Emmerik 2000], and these results could profitably be applied not only to other binary translators [Zheng and Thompson 2000] but also to any tools that analyze machine instructions, including optimizers [Srivastava and Wall 1993; Bala et al. 2000], code instrumentors [Wall 1992; Larus and Ball 1994; Larus and Schnarr 1995], fault isolators [Wahbe et al. 1993], and decompilers [Cifuentes and Gough 1995; Hoffman 1997; Cifuentes et al. 1998].

Our method uses register-transfer lists (RTLs) as a semantic framework in which to reason about instructions on both the source and target machines [Ramsey and Davidson 1998]. We divide a machine’s semantics into two parts. We specify semantics common to most instructions (e.g., the advancement of the program counter) as part of a simple imperative program representing the execution loop of a machine. We specify the unique effect of each instruction as a register-transfer list. The effect of executing a program is represented as the effect of running the execution loop on a sequence of instructions, or more precisely, on a sequence of register-transfer lists representing the semantics of the instructions.

A Transformational Approach to Binary Translation of Delayed Branches · 3

We build a binary translator by considering semantics for two machines. Each has an execution loop and a set of instructions. We begin by transforming the source machine’s execution loop into the target machine’s execution loop. To maintain the proper semantics for a program, we simultaneously transform the sequence of source-machine instructions into a sequence of target-machine instructions. This transformation of the sequence of instructions becomes our algorithm for binary translation.

A quick reading of this paper 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, except when the instruction in the delay slot is itself a delayed branch, call, or other transfer of control. 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 [SPARC International 1992, §B.26].

The building blocks of this paper are not new. Register-transfer languages have been used to describe instructions for years [Bell and Newell 1971; Barbacci and Siewiorek 1982]. Our program transformations draw from standard techniques in compiler optimization [Aho et al. 1986] and partial evaluation [Jones et al. 1993]. The contribution of this paper is the idea of applying these well-known techniques to a new problem domain, where they have been used to build a SPARC front end for the University of Queensland binary translator [Cifuentes et al. 1999; Cifuentes and Van Emmerik 2000]. Although the delayed branch is an architectural idea whose time has come and gone, the method is significant to anyone who must write tools that deal with legacy binaries. For example, translators using this method could run PA-RISC code on the new IA-64 architecture. They might also enable architects to eliminate delayed branches from future versions of the SPARC architecture.

2. 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.

We write R for the set of all possible RTLs. We assume that the effect of any machine instruction can be described by a suitable r ∈ R, as appears to be the case for many real microprocessors. This paper describes a translation between subsets L_{s} ⊂ R and L_{t} ⊂ R. The source-machine language, L_{s}, has delayed branches; the target-machine language, L_{t}, does not.

2.1 Register transfer lists

Our RTL formalism is designed for use in tools and component generators, and it makes machine-dependent computation explicit [Ramsey and Davidson 1998]. For this paper, we use a simplified version specified using the following syntax:

rtl ⇒ [effect {| effect}] Multiple assignment

effect ⇒ [exp →] location := exp Guarded assignment
exp ⇒ constant  Constant
| location  Fetch from a location
| exp binop exp  Binary RTL operator
| operator ( explist ) RTL operator

A register transfer list is a list of guarded effects. Each effect represents the transfer of a value into a storage location,^{1} i.e., a store operation. The transfer takes place only if the guard (an expression) evaluates to true. Effects in a list take place simultaneously, as in Dijkstra’s multiple-assignment statement; an RTL represents a single change of state. Appendix A makes this notion precise by giving a denotation function R[[rtl]] : Σ → Σ.

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 RTL operators to lists of expressions. RTL operators are pure functions on values. Expressions have their own denotation function E[[e]] : Σ → V, where V is the domain of values.

In this paper, we assume that locations are single cells in a mutable store, although the full RTL formalism supports a more general view that makes byte order explicit.

As an example of a typical RTL, consider a SPARC load instruction using the displacement addressing mode, written in the SPARC assembly language as

  ld [%sp-12], %i0

This load instruction computes an address by adding −12 to the stack pointer (register 14), then loads a word from that address into register %i0 (register 24). The effect of the instruction might be written ⟨RTL for sample instruction⟩≡

$r[24] := $m[$r[14] + sx(−12)] The notation $space[address] specifies a cell in a mutable store. The sx operator sign-extends the 13-bit immediate constant −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.

2.2 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 I that causes a delayed branch to a location target, the processor first executes I’s successor, then executes the instruction located at target. The location holding I’s successor is called I’s “delay slot.” On some machines, like the SPARC, the

1Storage locations represent not only memory but also registers and other processor state.

instruction I can “annul” its successor, in which case the successor is not executed; instead the processor stalls for a cycle before transferring control to target.

To model delayed branches with annuls, we use three pieces of processor state:

PC is the program counter, which identifies the instruction about to be executed. nPC is the “next program counter,” which identifies the instruction to be executed

after the current instruction. annul is the “annul status,” which determines whether the processor executes the

instruction at PC or ignores it.^{2}

In this model, a delayed control transfer is represented by an assignment to nPC . For example, a SPARC call instruction simultaneously assigns the target address to nPC and the current PC to register 15: ⟨RTL for call⟩≡

nPC := target | $r[15] := PC The target address in the RTL is distinct from the 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 target field on the right with zeroes.

A call transfers control unconditionally; we represent a conditional branch by a guarded assignment to nPC . The BNE (branch not equal) instruction tests the Z (zero) bit in the condition codes: ⟨rtl for conditional branch BNE ⟩≡

¬Z → nPC := target Again we abstract the computation of the target address relative to the location of the instruction.

2.3 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: ⟨RTL for generic instruction I ⟩≡

b_{I} → nPC := target_{I} | annul := a_{I} | I_{c} We interpret this form as follows:

b_{I} is a Boolean-valued expression that tells whether I branches. It is an expression, not a constant or a field of the instruction. For non-branching instructions, b_{I} is false. For calls and unconditional branches, b_{I} is true. For conditional branches, 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).

2Readers who are familiar with the SPARC architecture must distinguish the annul status, which is part of the processor state, from the a bit found in the binary representations of most branch instructions. The interpretation of the annul status is trivial: it tells whether to execute an instruction. The interpretation of the a bit is more involved, because there are special rules for some instructions. We abstract away from these special rules by associating with each instruction I a Boolean expression a_{I} (not necessarily a single bit) that tells the processor whether to annul the instruction’s successor.

target_{I} is an expression that identifies the target address to which I may branch. (If b_{I} is false, target_{I} is arbitrary.) For calls and PC-relative branches, target_{I} is a constant that statically identifies a target address. For indirect branches, target_{I} may be a more complex expression, e.g., one that fetches an address stored in a register.

a_{I} is a Boolean-valued expression that tells whether I annuls its successor. Like b_{I}, it is an expression; it is not the value of the a bit in an instruction’s representation. For most instructions, a_{I} is false. For conditional branches, a_{I} may be more complicated. For example, the SPARC BNE instruction annuls its successor if the a bit is set and if the branch is not taken, so a_{I} is a ≠ 0 ∧ Z.

I_{c} is an RTL that represents I’s “computational effect.” I_{c} may be empty, or it may contain guarded assignments that do not change annul, nPC , or PC . Typical RISC instructions change control flow or perform computation, but not both, so I_{c} tends to be non-empty only when b_{I} and a_{I} are false. On CISC architectures, however, an instruction like “decrement and skip if zero” might have both non-empty I_{c} (the decrement) and a nontrivial b_{I} (the test for zero).

An instruction can be expressed in this canonical form if, when executed, it branches to at most one target.^{3} This is true of all instructions on all architectures with which we are familiar, including indirect-branch instructions (although the value of target may be different on different executions of an indirect branch). We therefore define L_{s} as follows:

L_{s} =^{def} {I ∈ R | ∃b_{I}, target_{I}, a_{I}, I_{c} : R[[b_{I} → nPC := target_{I} | annul := a_{I} | I_{c}]] = R[[I]]}.

Here are a few example RTLs in canonical form; SPARC assembly language appears on the left, RTLs on the right. The mnemonic ba,a stands for “branch always, annul;” skip is the empty RTL.

   add rs1, rs2, rd

false → nPC := any | annul := false | $r[rd] := $r[rs1] + $r[rs2]

ba,a addr true → nPC := addr | annul := true | skip
call addr true → nPC := addr | annul := false | $r[15] := PC

3And of course if the machine uses delayed branches.

2.4 Instruction decoding and execution on two platforms

Given this canonical form for instructions, we represent instruction decoding using a let-binding notation: ⟨instruction decoding⟩≡

let (b_{I} → nPC := target_{I} | annul := a_{I} | I_{c}) ≡ src[PC ]

in …

end The let construct binds b_{I}, target_{I}, a_{I}, and I_{c}, which together determine the semantics of the instruction I found in the source memory src. Perhaps unusually, these identifiers are bound to syntax (either expressions or RTLs), not to values. The let-binding represents not only the process of using the binary representation to identify the instruction and its operands, but also the mapping from that representation into a register-transfer list. This mapping can be done statically, at binary-translation time; it can even be automated based on a combination of machine descriptions [Ramsey and Fernández 1997; Ramsey and Davidson 1998].

We have chosen a formalism in which an RTL alone is not sufficient to specify the behavior of a machine when it executes an instruction; we also require an execution loop. The source-machine execution loop decodes an instruction and executes it as follows: ⟨sparc execution loop⟩≡

fun loop() ≡

let (b_{I} → nPC := target_{I} | annul := a_{I} | I_{c}) ≡ src[PC ] in if annul then

[[PC := nPC | nPC := succ_{s}(nPC ) | annul := false]] else if [[b_{I}]] then

[[PC := nPC | nPC := target_{I} | I_{c} | annul := a_{I}]] else

[[PC := nPC | nPC := succ_{s}(nPC ) | I_{c} | annul := a_{I}]] fi ; loop()

end 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.

The execution loop is written using a simple imperative metalanguage, the semantics of which are given in Appendix A. In the body of the paper, we use several notational shortcuts. The most important of these are the brackets [[·]], which represent evaluation of syntax; for example, [[b_{I}]] is short for eval_{e}(b_{I}), which produces the value of the branch condition (true or false), given the current state of the machine. The notation [[r]] is short for eval_{r}(r), which changes the state of the machine as specified by R[[r]].

The function succ_{s} abstracts over the details of identifying the successor instruction on the source machine; succ_{t} finds the successor on the target machine. In both cases, succ is computed as part of instruction decoding.

Our example target, the Pentium, has neither delayed branches nor annulling, so it has a simpler canonical form and a simpler execution loop. We define the target language L_{t} by its canonical form:

L_{t} =^{def} {I ∈ R | ∃b_{I}, target_{I}, I_{c} : R[[b_{I} → PC := target_{I} | I_{c}]] = R[[I]]}.

This is the target execution loop: ⟨Pentium execution loop⟩≡

fun simple() ≡

let (b_{I} → PC := target_{I} | I_{c}) ≡ tgt[PC ] in if [[b_{I}]] then

[[PC := target_{I} | I_{c}]] else [[PC := succ_{t}(PC ) | I_{c}]] fi ; simple()

end

2.5 Strategy for translating delayed branches

The problem we are trying to solve is to take a source-machine program whose instructions are in L_{s}, and to translate it into a target-machine program whose instructions are in L_{t}, such that when the two programs are executed by their respective execution loops, the target program simulates the source program in a way made precise below.

Both our formalism and the SPARC architecture manual give a clear semantics of delayed branches in terms of PC , nPC , and annul. It would therefore suffice to create a translation that represented the source PC , nPC , and annul explicitly on the target machine, but such a translation would be very inefficient. For example, the representation of nPC would have to be updated in software after every execution of a translated instruction. A better idea is to make the values of the source PC , nPC , and annul implicit in the value of the target 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 loop, eliminating nPC and annul wherever possible, so that (almost all of) loop can be expressed using only the PC . This transformation leads to suitable changes in the sequence of instructions executed, thus guiding a transformation from src to tgt. This latter transformation is an algorithm for binary translation of delayed-branch instructions.

3. TRANSFORMING THE EXECUTION LOOP

We wish to develop a translation function that we can point at a location src[pc_{s}] and that will produce suitable instructions at a corresponding target location tgt[pc_{t}]. We cannot simply have pc_{t} = 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 codemap, a map that relates program counters on the two machines, so pc_{t} = codemap(pc_{s}).

We assume that when the source processor starts executing code at src[pc_{s}], it is not “in the middle” of a delayed or annulled branch, or formally,

annul = false ∧ nPC = succ_{s}(PC ).

We call a state stable if it satisfies this predicate. The processor ABI (application binary interface) guarantees that the processor will be in a stable state at a program’s start location [Prentice Hall 1993], and procedure calling conventions guarantee that the processor will be in a stable state at procedure entry points.

We begin our transformation by defining a function stable that can be substituted for loop whenever annul = false ∧ nPC = succ_{s}(PC ). ⟨stable execution loop⟩≡

fun stable() ≡

[[annul := false | nPC := succ_{s}(PC )]];

let (b_{I} → nPC := target_{I} | annul := a_{I} | I_{c}) ≡ src[PC ] in if annul then

[[PC := nPC | nPC := succ_{s}(nPC ) | annul := false]] else if [[b_{I}]] then

[[PC := nPC | nPC := target_{I} | I_{c} | annul := a_{I}]] else

[[PC := nPC | nPC := succ_{s}(nPC ) | I_{c} | annul := a_{I}]] fi ; loop()

end Appendix B lists the transformations used to get from this definition to something much like simple.

We do not show every step in the transformation of stable. The first transformations move the initial assignments inside the let, propagate (by forward substitution) the assignments to annul and nPC , move loop() inside the if, replace loop() with stable() where possible, and drop the (now dead) assignments. The result is:

⟨stable execution loop⟩+≡

fun stable() ≡

let (b_{I} → nPC := target_{I} | annul := a_{I} | I_{c}) ≡ src[PC ] in if [[b_{I}]] then

[[PC := succ_{s}(PC ) | nPC := target_{I} | I_{c} | annul := a_{I}]]

; loop() else if [[a_{I}]] then

[[PC := succ_{s}(PC ) | nPC := succ_{s}(succ_{s}(PC )) | I_{c} | annul := true]] ; loop()

else [[PC := succ_{s}(PC ) | I_{c}]] ; stable()

fi end

The last arm of the if shows the execution of an instruction that never branches or annuls. It corresponds to the execution of a similar instruction on the simple target.

The next step is to unfold loop in the first and second arms of the if statement. In the second arm, annul is true, so the call to loop() can be replaced by PC := nPC ; nPC := succ_{s}(nPC ); stable(). The definition of stable reduces to

⟨stable execution loop⟩+≡

fun stable() ≡ let (b_{I} → nPC := target_{I} | annul := a_{I} | I_{c}) ≡ src[PC ] in if [[b_{I}]] then

⟨case where I branches⟩ else if [[a_{I}]] then

[[PC := succ_{s}(succ_{s}(PC )) | I_{c}]] ; stable()

else [[PC := succ_{s}(PC ) | I_{c}]] ; stable()

fi end

where the interesting case is ⟨case where I branches⟩≡

[[PC := succ_{s}(PC ) | nPC := target_{I} | I_{c} | annul := a_{I}]]; let (b_{I′} → nPC := target_{I′} | annul := a_{I′} | I′_{c}) ≡ src[PC ] in if annul then

[[PC := nPC | nPC := succ_{s}(nPC ) | annul := false]] else if [[b_{I′}]] then

[[PC := nPC | nPC := target_{I′} | I′_{c} | annul := a_{I′}]] else

[[PC := nPC | nPC := succ_{s}(nPC ) | I′_{c} | annul := a_{I′}]] fi ; loop()

end

Transformation proceeds by combining these two fragments, moving the lets together, and flattening the nested if statements. We then use “The Trick” from partial evaluation [Danvy et al. 1996]: whenever [[a_{I}]] is free in a statement S, we replace S with if [[a_{I}]] then S else S fi. The Trick enables us to replace several calls to loop with calls to stable. The result is

⟨stable execution loop⟩+≡

fun stable() ≡ let (b_{I} → nPC := target_{I} | annul := a_{I} | I_{c}) ≡ src[PC ]

(b_{I′} → nPC := target_{I′} | annul := a_{I′} | I′_{c}) ≡ src[succ_{s}(PC )] in if [[b_{I}]] ∧ [[a_{I}]] then

[[I_{c}]]; [[PC := target_{I}]] ; stable()

else if [[b_{I}]] ∧ ¬[[a_{I}]] ∧ [[b_{I′}]] ∧ [[a_{I′}]] then [[I_{c}]]; [[I′_{c}]]; [[PC := target_{I′}]] ; stable()

else if [[b_{I}]] ∧ ¬[[a_{I}]] ∧ [[b_{I′}]] ∧ ¬[[a_{I′}]] then [[I_{c}]]; [[PC := target_{I} | nPC := target_{I′} | I′_{c} | annul := false]] ; loop()

else if [[b_{I}]] ∧ ¬[[a_{I}]] ∧ ¬[[b_{I′}]] ∧ [[a_{I′}]] then [[I_{c}]]; [[I′_{c}]]; [[PC := succ_{s}(target_{I})]] ; stable()

else if [[b_{I}]] ∧ ¬[[a_{I}]] ∧ ¬[[b_{I′}]] ∧ ¬[[a_{I′}]] then [[I_{c}]]; [[PC := target_{I} | I′_{c}]] ; stable()

else if ¬[[b_{I}]] ∧ [[a_{I}]] then [[PC := succ_{s}(succ_{s}(PC )) | I_{c}]] ; stable()

else if ¬[[b_{I}]] ∧ ¬[[a_{I}]] then [[PC := succ_{s}(PC ) | I_{c}]] ; stable()

fi end

This version of stable suffices to guide the construction of a translator. Considering the cases in order,

—A branch that annuls the instruction in its delay slot acts just like an ordinary

branch on a machine without delayed branches. —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.

—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 stable for loop. Interestingly, the MIPS architecture manual specifies that the machine’s behavior in this case is undefined [Kane 1988, Appendix A]. This case requires potentially unbounded unfolding of loop, which we discuss in Section 6.

—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, BN,A.)

—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. —An annuling non-branch skips over its successor. —A non-annuling non-branch (i.e., an ordinary computational instruction) simply

executes and advances the program counter to its successor.

4. APPLICATION TO THE SPARC INSTRUCTION SET

To this point, the development of our idea is abstract; it could apply to any machines with and without delayed branches. The value of our work, however, is that it can be applied to real translators for real instruction sets. This section applies our formal analysis to the SPARC instruction set, and it sketches the derivation of a translator. We used this derivation to build the SPARC front end of the University of Queensland binary translator [Cifuentes et al. 1999; Cifuentes and Van Emmerik 2000].

4.1 Classification of SPARC instructions

The three properties of instructions that govern the translation of control flow are b_{I} (must branch, may branch, may not branch), a_{I} (must annul, may annul, may not annul), and target_{I} (static target, dynamic target, no target). There are 15 reasonable combinations of these three properties. On the SPARC, only 9 combinations are used:

Instruction b_{I}  a_{I}  target_{I} I_{c}  Class
BA  true  false  static  skip  SD
BN  false  false  N/A  skip  NCT
Bcc  test_{cc}(icc) false  static  skip  SCD
BA,A  true  true  static  skip  SU
BN,A  false  true  N/A  skip  SKIP
Bcc,A  test_{cc}(icc) ¬test_{cc}(icc) static  skip  SCDA
CALL  true  false  static  $r[15] := PC SD
JMPL  true  false  dynamic $r[rd] := PC DD
RETT  true  false  dynamic ⟨restore state⟩ DD
TN  false  false  N/A  skip  NCT
Ticc  test_{cc}(icc) test_{cc}(icc) dynamic ⟨save state⟩  TRAP
TA  true  true  dynamic ⟨save state⟩  TRAP′
NCT  false  false  N/A  varies  NCT

These combinations enable us to classify instructions. We name 8 of the 9 classes as follows:

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

Our treatment of trap instructions may be surprising, since the architecture manual presents them as instructions that set both PC and nPC . Because nPC is always set to PC + 4 [SPARC International 1992, §C.8], we can model this behavior as setting nPC to the address of the trap handler and setting annul to 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 (TRAP′) in the same class as the conditional traps (TRAP). We can’t do this with the branch instructions because of BA,A’s anomalous treatment of the a bit.

The table exposes a useful property of the SPARC instruction set; a_{I} is not arbitrary, but is always given by one of these four possibilities:

a_{I} ≡ false Never annul.
a_{I} ≡ true Always annul.
a_{I} ≡ b_{I}  Annul if branch taken.
a_{I} ≡ ¬b_{I} Annul if branch not taken.

Whenever processor designers use this scheme, a_{I} can be eliminated at binarytranslation time. A more general a_{I} would require a second test in the translated code.

4.2 Derivation of a translator

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. Recall that if a machine is in a state σ, we write E[[e]]σ for the value of expression e in state σ; if executing instruction I causes a machine to make a transition from a state σ to a new state σ′, we write σ′ = R[[I]]σ.

A translation is correct if execution on the target machine simulates execution on the source machine. The translator builds a map \overline{·} from source-machine states to target-machine states.^{4} In a way made precise below, this map respects the operation of the machine. In our design, \overline{·} is partial—it is not defined when the source machine is “about to” execute a delayed branch or annulled instruction. To be precise, \overline{σ} is defined if E[[¬annul ∧ nPC = succ_{s}(PC )]]σ.

When referring to states, we use a left superscript of s or t to designate a state on the source or target machine. We use subscripts to number states in sequence.

We say the target machine simulates the source machine if the following condition holds: if we start the source machine in a state ^{s}σ_{0}, and the loop function takes it through a sequence of states ^{s}σ_{0},^{s}σ_{1}, …, then there is a subsequence of such states sσ_{k_{0}},^{s}σ_{k_{1}}, … such that \overline{^{s}σ_{k_{0}}}, \overline{^{s}σ_{k_{1}}}, … is a subsequence of the states that the target machine goes through when started in state ^{t}σ_{0} = \overline{^{s}σ_{0}}. 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.^{5} We sketch a proof in Section 5.

4Technically, the translator establishes not a map but a relation, because more than one targetmachine state can be used to simulate a particular source-machine state. We nevertheless use the function \overline{·} notation for its readability. When we write \overline{^{s}σ}, we really mean “any state ^{t}σ such that tσ and ^{s}σ stand in a weak bisimulation relation.” Writing the existential quantifiers and relations explicitly would obscure the ideas. 5In the terminology of Milner [1990], the transitions to these intermediate states are “silent.”

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 naïve translator, \overline{·} can mostly map locations to locations, without changing values. The exception is the program counter; its translation must use codemap, so we require E[[PC ]]\overline{σ} = codemap(E[[PC ]]σ). Given a map \overline{·} on locations, we can easily extend it to expressions like a_{I}, b_{I}, and target_{I}. If e is an expression, then E[[\overline{e}]]\overline{σ} = E[[e]]σ.

We assume that translations can be found for the computational effects I_{c}, which do not affect PC , nPC , or annul. Given an effect I_{c}, we write its translation \overline{I_{c}}; in general, \overline{I_{c}} is a sequence of RTLs, not exactly one RTL. Any translation is acceptable as long as for any σ, R[[\overline{I_{c}}]]\overline{σ} = \overline{R[[I_{c}]]σ}.^{6} We also assume that, given any condition b and address target, we can construct an instruction sequence implementing b → PC := target on the target machine.

Under these assumptions, we analyze source branch conditions b_{I}, annulment conditions a_{I}, and target addresses target_{I}, and we show how to construct branch conditions and target addresses for the target machine. In the process, we build the codemap function that takes source program counters to target program counters.

Structure of the translator. Our translator works with one basic block at a time. 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. The translator maintains a work queue of untranslated blocks, each of which is represented by a (pc_{s}, pc_{t}) pair. pc_{s} is the address of some code on the source machine. 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, pc_{t} might be a pointer to a basic block in a control-flow graph.) codemap contains pairs that have already been translated. We use the following auxiliary procedures:

queueForTranslation(pc_{s}, pc_{t}) Add a pair to the work queue.

codemap(pc_{s}) If a pair (pc_{s}, pc_{t}) is in codemap, return pc_{t}. Otherwise, let pc_{t} be a fresh placeholder, add (pc_{s}, pc_{t}) to codemap, and return pc_{t}. (We use codemap both as a function and as a collection of ordered pairs, but these usages are equivalent.)

emit(pc_{t}, I) Emit target-machine instructions I at pc_{t}, returning a pointer to the location following the instructions. If I is a sequence of n instructions, emit(pc_{t}, I) returns the result of applying succ_{t} to pc_{t}, n times.

newBlock()  Return a pointer to a fresh placeholder.

Placeholders created with codemap correspond to basic blocks in the source program. Placeholders created with newBlock are artifacts of translation.

The translator loops, removing pairs from the work queue, and calling trans if those pairs have not already been translated. trans translates individual basic blocks. If an instruction branches, trans calls queueForTranslation with the target addresses (from source and target machines). If an instruction flows through to its successor, trans calls itself tail-recursively.^{7} The outline of trans is

6We extend R to sequences of RTLs using the standard rule for sequential composition: R[[r_{1}; r_{2}]] = R[[r_{2}]] ∘ R[[r_{1}]]. 7Recursive calls to trans could be replaced by calls to queueForTranslation. The converse is not true, because trans would recur forever on loops.

⟨translator⟩≡ fun trans(pc_{s}, pc_{t}) ≡ ⟨put (pc_{s}, pc_{t}) in codemap if they are not there already⟩ let I as (b_{I} → nPC := target_{I} | annul := a_{I} | I_{c}) ≡ src[pc_{s}] in case class(I) of

⟨cases for translation of I ⟩ end

Translations of SPARC instructions. Deriving a translation function is tedious but straightforward. For each class of instructions, we use a_{I} and b_{I} to simplify stable. If necessary, we also consider a_{I′} and b_{I′}, where I′ is the instruction in the delay slot. We transform the simplified stable as needed until it suggests an obvious translation, and finally we emit target-machine instructions. We show only a few representative cases. Table I shows example SPARC and Pentium assembly language for each. These examples are shown unoptimized; in some cases, such as be followed by mov, it is possible to put I′ before I, eliminating significant overhead. This restructuring is not possible in the general case, however, and particular cases may be best left to a general-purpose optimizer.

The easiest cases are ones in which a’s and b’s are known statically. For noncontrol-transfer instructions, b_{I} ≡ false and a_{I} ≡ false, which corresponds to the last arm of stable, and the translation is ⟨cases for translation of I ⟩≡

| NCT ⟹ pc_{t} := emit(pc_{t}, \overline{I_{c}}); trans(succ_{s}(pc_{s}), pc_{t})

The static unconditional branch with annul is just like an ordinary branch. b_{I} ≡ true and a_{I} ≡ true, which corresponds to the first arm of stable, and the translation is

⟨cases for translation of I ⟩+≡

| SU ⟹ pc_{t} := emit(pc_{t}, PC := codemap(target_{I}));

queueForTranslation(target_{I}, codemap(target_{I})); The next simplest cases are the static delayed (SD) class, with b_{I} ≡ true and

a_{I} ≡ false. These instructions include unconditional branches and calls, and the translation depends on what sort of instruction I′ is found in the delay slot.

⟨cases for translation of I ⟩+≡

| SD ⟹

let (b_{I′} → nPC := target_{I′} | annul := a_{I′} | I′_{c}) ≡ src[succ_{s}(pc_{s})] in case class(I′) of

⟨translation cases for class(I′), where class(I) = SD⟩ end

class(I) class(I′)  SPARC instructions  Pentium instructions

NCT any

add %i1, %i2, %i3

mov eax, SPARCI1
add eax, SPARCI2
mov SPARCI3, eax

SU  any  ba,a L                        jmp L

SD NCT

ba L
add %i1, %i2, %i3

nop
mov eax, SPARCI1
add eax, SPARCI2
mov SPARCI3, eax
jmp L

SCD NCT

be L
mov %o1, %o2

⋮

nop
je BB
mov eax, SPARCO1
mov SPARCO2, eax

⋮

BB: mov eax, SPARCO1
mov SPARCO2, eax
jmp L

SCDA NCT

be,a L
mov %o1, %o2

⋮

nop
je BB

⋮

BB: mov eax, SPARCO1
mov SPARCO2, eax
jmp L

SD SD

ba L1
ba L2
mov 3, %o0

⋮

L1: mov 2, %o0

⋮

L2: . . .

nop nop mov eax, 2 jmp L2

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 SPARCI1 = \overline{%i1}, SPARCI2 = \overline{%i2}, etc. The examples where class(I) is SCD and SCDA show the same be instruction with and without the ,a suffix (annul when branch not taken).

Table I. Example translations from SPARC to Pentium

In the common case, we have a non-control-transfer instruction in the delay slot, with b_{I′} ≡ false and a_{I′} ≡ false. This corresponds to the fifth arm of stable, which executes [[I_{c}]]; [[PC := target_{I} | I′_{c}]]. Since target_{I} is a constant, we can rewrite this as [[I_{c}]]; [[I′_{c}]]; [[PC := target_{I}]]. The translation is then ⟨translation cases for class(I′), where class(I) = SD⟩≡

| NCT ⟹ pc_{t} := emit(pc_{t}, \overline{I_{c}}); pc_{t} := emit(pc_{t}, \overline{I′_{c}}); pc_{t} := emit(pc_{t}, PC := codemap(target_{I})); queueForTranslation(target_{I}, codemap(target_{I}));

This translation is not sufficient for call instructions, because a called procedure may use the program counter captured by 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 I is a call instruction, convention says that translation should resume with trans(succ_{s}(succ_{s}(pc_{s})), pc_{t}), or if the call returns a structure, with trans(succ_{s}(succ_{s}(succ_{s}(pc_{s}))), pc_{t}).

The treatment of class DD (dynamic delayed) branches is similar to that of class SD, except that the target addresses are computed dynamically. This means that it is not possible to use codemap at translation time; the translated code might use codemap at run time, or it might call an interpreter or a dynamic translator.

The most common class involving dynamic conditions is the SCD (static conditional delayed) class, in which b_{I} is dynamic and a_{I} is false. Again, the translation depends on what is in the delay slot.

⟨cases for translation of I ⟩+≡

| SCD ⟹

let (b_{I′} → nPC := target_{I′} | annul := a_{I′} | I′_{c}) ≡ src[succ_{s}(pc_{s})] in case class(I′) of

⟨translation cases for class(I′), where class(I) = SCD⟩ end The most common delay instruction is a non-control-transfer instruction (class

NCT ), where b_{I′} = false and a_{I′} = false. In this case, stable reduces to

⟨specialization of stable for SCD with NCT in the delay slot⟩≡ if [[b_{I}]] then [[I_{c}]]; [[PC := target_{I} | I′_{c}]]; stable() else [[I_{c} | PC := succ_{s}(PC )]]; stable() fi

Because I_{c} does not affect PC , we transform stable as follows:^{8}

⟨transformed specialization of stable for SCD with NCT in the delay slot⟩≡ [[I_{c}]]; if [[b_{I}]] then [[PC := target_{I} | I′_{c}]] else PC := succ_{s}(PC ); fi ; stable()

8We have the alternative of unfolding the call to stable in the else branch and moving both I_{c} and I′_{c} ahead of the if. This transformation leads to a translation in which I′_{c} moves ahead of the branch, and I′_{c}’s successor follows the branch. Epoxie and Noxie use this translation [Wall 1992]. The problem is that, if the branch condition b_{I} tests condition codes, and 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 I′_{c} into a new block, which the optimizer can sometimes eliminate.

In general, no single target instruction implements [[PC := target_{I} | I′_{c}]], so we rewrite it into the sequence [[I′_{c}]]; [[PC := target_{I}]], and we put this sequence into a new “trampoline” basic block bb. stable becomes

⟨final specialization of stable for SCD with NCT in the delay slot⟩≡ [[I_{c}]]; if [[b_{I}]] then PC := bb; else PC := succ_{s}(PC ); fi ; stable()

which we translate using an ordinary branch instruction: ⟨translation cases for class(I′), where class(I) = SCD⟩≡

| NCT ⟹ local bb := newBlock(); pc_{t} := emit(pc_{t}, \overline{I_{c}}); pc_{t} := emit(pc_{t}, \overline{b_{I}} → PC := bb); bb := emit(bb, \overline{I′_{c}}); bb := emit(bb, PC := codemap(target_{I})); queueForTranslation(target_{I}, codemap(target_{I})); trans(succ_{s}(pc_{s})), pc_{t});

The cases for class SCDA (static delayed branches that annul when not taken) are similar to those of class SCD. For example, when SCDA is followed by NCT , b_{I} is dynamic, a_{I} ≡ ¬b_{I}, and b_{I′} ≡ a_{I′} ≡ false. stable reduces to:

⟨specialization of stable for SCDA with NCT in the delay slot⟩≡ [[I_{c}]]; if [[b_{I}]] then [[I′_{c}]]; [[PC := target_{I}]] else PC := succ_{s}(succ_{s}(PC )); fi ; stable()

The translation is like that of class SCD, creating a new basic block, but the recursive call is trans(succ_{s}(succ_{s}(pc_{s})), pc_{t}), so translation resumes after the delay slot instead of at the delay slot.

The most difficult cases arise when the instruction in the delay slot of a branch I is another delayed-branch instruction I′. These cases multiply like rabbits. We show just one, but it is almost useful; putting an unconditional SD branch in the delay slot of another unconditional SD branch makes it possible to execute a single non-branching NCT instruction “out of line.” (To make the case truly useful, the target of the first branch should be computed dynamically, but this change would complicate the exposition significantly.)

When SD is in SD’s delay slot, b_{I′} = true and a_{I′} = false, and stable reduces to the following code.

⟨specialization of stable for SD with SD in the delay slot⟩≡ [[I_{c}]]; [[PC := target_{I} | nPC := target_{I′} | I′_{c} | annul := false]] ; loop()

We unfold the call to loop and substitute forward for PC , nPC , and annul. Removing dead assignments leaves

⟨transformed specialization of stable for SD with SD in the delay slot⟩≡ [[I_{c}]]; [[I′_{c}]]; let (b_{I′′} → nPC := target_{I′′} | annul := a_{I′′} | I′′_{c}) ≡ src[[[target_{I}]]] in if [[b_{I′′}]] then

[[PC := target_{I′} | nPC := target_{I′′} | I′′_{c} | annul := a_{I′′}]] else [[PC := target_{I′} | nPC := succ_{s}(target_{I′}) | I′′_{c} | annul := a_{I′′}]] fi ; loop()

end

We can now move loop() inside the conditional, convert it to stable() in one branch, unfold, etc. We wind up with 4 cases based on the values of [[a_{I′′}]] and [[b_{I′′}]]. Because I is a static branch, the value of [[target_{I}]] is independent of the state of the machine, so we can find I′′ and the expressions [[a_{I′′}]] and [[b_{I′′}]] statically. The simplest case is one in which I′′ never branches (NCT ), i.e., where b_{I′′} = false and a_{I′′} = false. This case reduces to

⟨further specialization of stable for SD with SD in the delay slot (class(I”)=NCT)⟩≡ [[I_{c}]]; [[I′_{c}]]; [[PC := target_{I′} | I′′_{c}]] ; stable()

As before, because I′ is static, we can rewrite [[PC := target_{I′} | I′′_{c}]] as the sequence [[I′′_{c}]]; [[PC := target_{I′}]], and we read off the following translation: ⟨translation cases for class(I′′), where class(I) = SD and class(I’) = SD⟩≡

| NCT ⟹ pc_{t} := emit(pc_{t}, \overline{I_{c}}); pc_{t} := emit(pc_{t}, \overline{I′_{c}}); pc_{t} := emit(pc_{t}, \overline{I′′_{c}}); pc_{t} := emit(pc_{t}, PC := codemap(target_{I′})); queueForTranslation(target_{I′}, codemap(target_{I′}));

Since on the SPARC, I_{c} and I′_{c} are no-ops, the translation executes the effect of I′′, then branches to target_{I′}, as shown in the last example in Table I. The instruction in the delay slot of I′ (mov 3, %o0 in Table I) is not executed.

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.

a_{I} ≡ b_{I}  Push the delay instruction to the fall-through address.
a_{I} ≡ ¬b_{I} Push the delay instruction to the destination address.
a_{I} ≡ false Push the delay instruction to both addresses.
a_{I} ≡ true Discard the delay instruction.

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 third, fourth, and fifth examples in Table I show how this strategy is applied to the unconditional (SD), conditional (SCD), and conditional annuled (SCDA) branches on the SPARC. On the MIPS, programmers may not put branches in delay slots [Kane 1988, Appendix A], and a_{I} ≡ false always, so a single instance of this strategy applies to every branch instruction [Srivastava and Wall 1993].

5. PROVING CORRECTNESS

We prove correctness of translation by reasoning about transitions from states to states. As noted in Section 4.2, we want to show that running the translated code results in an execution on the target machine that simulates the original execution on the source machine. Formally, if we start the source machine in a state ^{s}σ_{0}, and the loop function takes it through a sequence of states ^{s}σ_{0},^{s}σ_{1}, …, then there is a subsequence of such states ^{s}σ_{k_{0}},^{s}σ_{k_{1}}, … such that \overline{^{s}σ_{k_{0}}}, \overline{^{s}σ_{k_{1}}}, … is a subsequence of the states that the target machine goes through when started in state ^{t}σ_{0} = \overline{^{s}σ_{0}}.

The result desired follows directly from this transition theorem: If ^{s}σ_{m} is a source-machine state such that

(1) E[[annul = false ∧ nPC = succ_{s}(PC )]]^{s}σ_{m},

(2) there is a corresponding target-machine state ^{t}σ_{n} = \overline{^{s}σ_{m}}, and

(3) trans has been called with arguments (E[[P C]]^{s}σ_{m}, E[[P C]]^{t}σ_{n}),

then there is an i such that in i steps, the source machine reaches a state ^{s}σ_{m+i} that also satisfies E[[annul = false ∧ nPC = succ_{s}(PC )]]^{s}σ_{m+i}. Also, there is a j such that in j steps, the target machine reaches a state ^{t}σ_{n+j} = \overline{^{s}σ_{m+i}}, and furthermore (a) i > 0 or j > 0 and (b) trans has been called with arguments (E[[P C]]^{s}σ_{m+i}, E[[P C]]^{t}σ_{n+j}).

We prove the transition theorem by case analysis on the classes of the instructions located at src[PC ]. We assume that the translations of expressions and computational effects, whatever they are, satisfy the following identities:

E[[\overline{e}]]\overline{σ} = E[[e]]σ \overline{R[[I_{c}]]σ} = R[[\overline{I_{c}}]]\overline{σ}

Because of condition 1, we can substitute stable for loop, so we can apply our transformed version of stable, which assigns directly to PC . We assume that all mappings \overline{·} use codemap to map the source program counter to the target program counter. To translate a branch, we therefore write R[[PC := target]]σ

= \overline{subst_{PC}^{target}σ}
= substcodemap(target) \overline{PC}\overline{σ}
= subst_{PC}^{codemap(target)}\overline{σ}

= R[[PC := codemap(target)]]\overline{σ} (∗)

The simplest case in the proof of the transition theorem is a non-control-transfer instruction (NCT ). The canonical form of such an instruction is

false → nPC := any | annul := false | I_{c}.

The action of stable on this form is R[[PC := succ_{s}(PC ) | I_{c}]]. I_{c} leaves the program counter unchanged, so we rewrite this as R[[I_{c}; PC := succ_{s}(PC )]]. The binary translation has the form \overline{I_{c}}, which may be a sequence of j instructions. Therefore j applications of simple, or equivalently, j state transitions on the target machine, have the effect of R[[\overline{I_{c}}; PC := succ_{t}^{(j)}(PC )]]. Given ^{s}σ_{m} and ^{t}σ_{n} satisfying the hypotheses of the transition theorem, after one step, the source machine reaches the state

sσ_{m+1} = R[[PC := succ_{s}(PC )]](R[[I_{c}]]^{s}σ_{m}).

After j steps, the target machine reaches a state

tσ_{n+j} = R[[PC := succ_{t}^{(j)}(PC )]](R[[\overline{I_{c}}]]^{t}σ_{n})
= R[[PC := succ_{t}^{(j)}(PC )]](R[[\overline{I_{c}}]]\overline{^{s}σ_{m}})
= R[[PC := succ_{t}^{(j)}(PC )]](\overline{R[[I_{c}]]^{s}σ_{m}})

From trans, codemap(succ_{s}(pc_{s})) = succ_{t}^{(j)}(pc_{t}), so by (∗)

tσ_{n+j}

=

R[[PC := succ_{s}(PC )]](R[[I_{c}]]^{s}σ_{m})

= \overline{^{s}σ_{m+1}}

Thus, after one step on the source and 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 SCD with an instruction of class NCT in the delay slot. If the source machine begins in state ^{s}σ, after 1 or 2 steps it reaches state ^{s}σ′, where

sσ′ = if E[[b_{I}]](R[[I_{c}]]^{s}σ) then (R[[PC := target_{I}]] ∘ R[[I′_{c}]] ∘ R[[I_{c}]])^{s}σ
else (R[[PC := succ_{s}(PC )]] ∘ R[[I_{c}]])^{s}σ fi

If the target machine begins in state ^{t}σ = \overline{^{s}σ}, it reaches state ^{t}σ′, where

tσ′ = if E[[\overline{b_{I}}]](R[[\overline{I_{c}}]]\overline{^{s}σ}) then

(R[[PC := codemap(target_{I})]] ∘ R[[\overline{I′_{c}}]] ∘ R[[PC := bb]] ∘ R[[\overline{I_{c}}]])\overline{^{s}σ} else

(R[[PC := succ_{t}(PC )]] ∘ R[[\overline{I_{c}}]])\overline{^{s}σ} fi

Because R[[PC := t_{1}]] ∘ R[[PC := t_{2}]] = R[[PC := t_{1}]], and because R[[\overline{I′_{c}}]] commutes with assignments to PC , it is easy to show that ^{t}σ′ = \overline{^{s}σ′}.

The other cases for translation can be proved correct in similar fashion.

6. EXPERIENCE

We have used translators for delayed branches in two tools: a binary translator [Cifuentes et al. 1999; Cifuentes and Van Emmerik 2000] and a decompiler [Cifuentes et al. 1998]. In both tools, we translate machine instructions into a low-level, machine-independent intermediate form 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.

Many problems of binary translation are beyond the scope of this paper.

—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.

—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.

—Different machines use different representations of condition codes, and a naïve translation would emulate 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.

—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.

Our first attempt at translating delayed branches 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 replaced our first attempt with a new implementation 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.

All the transformations discussed in this paper were done by hand. We investigated tools that might have helped us transform stable, but we were left with the impression that this is still a research problem [Shankar 1996], and it was easy enough to transform stable by hand. By contrast, it would be very useful to automate the derivation of the translator from stable and the discovery of the translations of the a_{I}’s, b_{I}’s, and 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 nop instructions shown in Table I when I_{c} is skip. There are also many cases in which further transformation of 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. We also executed test cases on both source and target machines, to make sure the proper effects were executed in both source and target codes.

As presented in this paper, a branch in a delay slot requires a recursive call to loop, not to stable. Most cases, including all those shown in the SPARC manual, can be handled by an additional unfolding of loop, which we have done in our implementation. The unfolding game can go on indefinitely; no matter how many times we unfold loop, a single recursive call to 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 do not unfold 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 nPC and PC are parameters.

ACKNOWLEDGMENT

We thank Jack Davidson for helpful discussions, Mike Van Emmerik for the implementation of the translator, and Mitch Wand for help with semantics. 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.

REFERENCES Aho, A. V., Sethi, R., and Ullman, J. D. 1986. Compilers: Principles, Techniques, and Tools.

Addison-Wesley. Andrews, K. and Sand, D. 1992. Migrating a CISC computer family onto RISC via object code

translation. Proceedings of the Fifth International Conference on Architectural Support for Programming Languages and Operating Systems, in SIGPLAN Notices 27, 9 (Oct.), 213–222.

Bala, V., Duesterwald, E., and Banerjia, S. 2000. Dynamo: A transparent dynamic optimization system. Proceedings of the ACM SIGPLAN ’00 Conference on Programming Language Design and Implementation, in SIGPLAN Notices 35, 5 (May), 1–12.

Barbacci, M. R. and Siewiorek, D. P. 1982. The Design and Analysis of Instruction Set

Processors. McGraw-Hill, New York, NY. Bell, C. G. and Newell, A. 1971. Computer Structures: Readings and Examples. McGraw-Hill,

New York. Bergh, A., Keilman, K., Magenheimer, D., and Miller, J. 1987. HP3000 emulation on HP

Precision Architecture computers. Hewlett-Packward Journal, 87 – 89.

Cifuentes, C. and Gough, K. J. 1995. Decompilation of binary programs. Software—Practice

& Experience 25, 7 (July), 811–829. Cifuentes, C., Simon, D., and Fraboulet, A. 1998. Assembly to high-level language translation.

In Proceedings of the International Conference on Software Maintenance. IEEE-CS Press, 228– 237.

Cifuentes, C. and Van Emmerik, M. 2000. UQBT: Adaptable binary translation at low cost.

IEEE Computer 33, 3 (Mar.), 60–66. Cifuentes, C., van Emmerik, M., and Ramsey, N. 1999. The design of a resourceable and retar-

getable binary translator. In Proceedings of the Working Conference on Reverse Engineering (WCRE’99). IEEE CS Press, 280–291.

Cmelik, B. and Keppel, D. 1994. Shade: A fast instruction-set simulator for execution profiling. In Proceedings of the 1994 ACM SIGMETRICS Conference on Measurement and Modeling of Computer Systems. 128–137.

Danvy, O., Malmkjær, K., and Palsberg, J. 1996. Eta-expansion does The Trick. ACM

Transactions on Programming Languages and Systems 18, 6 (Nov.), 730–751. Ebcioğlu, K. and Altman, E. R. 1997. DAISY: Dynamic compilation for 100% architectural

compatibility. In 24th Annual International Symposium on Computer Architecture. 26–37. Hoffman, T. 1997. Recovery firm hot on heels of missing source code. Computer World. Jones, N. D., Gomard, C. K., and Sestoft, P. 1993. Partial Evaluation and Automatic Pro-

gram Generation. Prentice Hall International, International Series in Computer Science. ISBN number 0-13-020249-5 (pbk).

Kane, G. 1988. MIPS RISC Architecture. Prentice Hall, Englewood Cliffs, NJ. Larus, J. R. and Ball, T. 1994. Rewriting executable files to measure program behavior.

Software—Practice & Experience 24, 2 (Feb.), 197–218. Larus, J. R. and Schnarr, E. 1995. EEL: machine-independent executable editing. Proceedings

of the ACM SIGPLAN ’95 Conference on Programming Language Design and Implementation, in SIGPLAN Notices 30, 6 (June), 291–300.

May, C. 1987. MIMIC: A fast System/370 simulator. Proceedings of the ACM SIGPLAN ’87 Symposium on Interpreters and Interpretive Techniques, in SIGPLAN Notices 22, 7 (June), 1–13.

Milner, R. 1990. Operational and algebraic semantics of concurrent processes. In Handbook of Theoretical Computer Science, J. van Leewen, Ed. Vol. B: Formal Models and Semantics. The MIT Press, New York, N.Y., Chapter 19, 1201–1242.

Prentice Hall 1993. System V Application Binary Interface, SPARC Architecture Processor Sup-

plement, Third ed. Prentice Hall, Englewood Cliffs, NJ. Unix Press. Ramsey, N. and Davidson, J. W. 1998. Machine descriptions to build tools for embedded

systems. In ACM SIGPLAN Workshop on Languages, Compilers, and Tools for Embedded Systems (LCTES’98). LNCS, vol. 1474. Springer Verlag, 172–188.

Ramsey, N. and Fernández, M. F. 1997. Specifying representations of machine instructions.

ACM Transactions on Programming Languages and Systems 19, 3 (May), 492–524. Shankar, N. 1996. Steps towards mechanizing program transformations using PVS. Science of

Computer Programming 26, 1–3 (May), 33–57. Sites, R. L., Chernoff, A., Kirk, M. B., Marks, M. P., and Robinson, S. G. 1993. Binary

translation. Communications of the ACM 36, 2 (Feb.), 69–81. SPARC International 1992. The SPARC Architecture Manual, Version 8. SPARC International,

Englewood Cliffs, NJ. Srivastava, A. and Wall, D. W. 1993. A practical system for intermodule code optimization.

Journal of Programming Languages 1, 1–18. Also available as WRL Research Report 92/6, December 1992.

Wahbe, R., Lucco, S., Anderson, T. E., and Graham, S. L. 1993. Efficient software-based fault isolation. In Proceedings of the Fourteenth ACM Symposium on Operating System Principles. 203–216.

Wall, D. W. 1992. Systems for late code modification. In Code Generation - Concepts, Tools, Techniques, R. Giegerich and S. L. Graham, Eds. Springer-Verlag, 275–293.

Witchel, E. and Rosenblum, M. 1996. Embra: Fast and flexible machine simulation. In Proceedings of the ACM SIGMETRICS International Conference on Measurement and Modeling of Computer Systems. ACM SIGMETRICS Performance Evaluation Review, vol. 24,1. ACM Press, New York, 68–79.

Zheng, C. and Thompson, C. 2000. PA-RISC to IA-64: Transparent execution, no recompilation. Computer 33, 3 (Mar.), 47–52.

A. FORMAL MODELS

This appendix provides formal semantics for the RTLs and the metalanguage used in the body of the paper. We use a “core” metalanguage that is simpler than what is used in the body. Here is its grammar; the “{braces}” are EBNF meta-notation for sequences.

program ⇒ {fun function-name () ≡ statement}
statement ⇒ statement; statement
| eval_{r}(rtl)
| if meta-exp then statement else statement fi
| let (rtl) ≡ memory[exp] in statement end
| function-name()
meta-exp ⇒ eval_{e}(exp)
| ¬ meta-exp
| meta-exp ∧ meta-exp

The program fragments used in the paper should be rewritten into the simpler core using the following rules:

—The expression [[e]] is short for eval_{e}(e). —The statement [[r]] is short for eval_{r}(r). —An if statement using elseif is short for nested if statements. —A let binding multiple RTLs is short for nested let bindings (as in ML).

We present the semantic rules in three layers: expressions, which map states to values; RTLs, which map states to states, and statements, which map continuations to continuations. To simplify the semantic equations, we use a revised grammar for RTLs.

rtl  ⇒ exp_{g} → location := exp_{r} | rtl
rtl  ⇒ location := exp_{r} | rtl
rtl  ⇒
rtl  ⇒ name
exp ⇒ constant
| location
| exp operator exp
| operator ( explist )
| name
explist ⇒ exp , explist
|

In the right-hand sides for rtl, the vertical bar | is the RTL parallel-composition operator; elsewhere, it is the EBNF metasymbol for alternatives.

To define denotations, we begin with domains Bits (bit vectors), Bool (Booleans), and an unspecified domain L of locations. We construct domains for values and states.

V = Bits + Bool  (values)
L  (locations)
σ : Σ = L → V  (states)

The let construct in our metalanguage binds names to RTLs and expressions. The body of the paper does not say how to give meanings to such names; this appendix uses environments. Making environments explicit adds precision but also detail; the detail would be distracting in the body of the paper.

ρ : Env_{r} = name → exp + rtl  (RTL environments)

The environment ρ is unusual because the denotations of names are syntax, not values.

We assume that the denotations of constants, operators, and locations are given by functions N, O, and L. We provide semantic equations for expressions. We use “cons” and “nil,” written “::” and “[]”, to construct lists. The denotation functions have the following types:

N : constant → V
O : operator → V list → V
L : location → Env_{r} → Σ → L
E : exp → Env_{r} → Σ → V
EL : exp list → Env_{r} → Σ → V list

Here are the semantic equations defining E on expressions and EL on lists of expressions.

E[[constant]]ρσ  = N [[constant]]
E[[location]]ρσ  = σ(L[[location]]ρσ)
E[[exp_{1} operator exp_{2}]]ρσ = O[[operator]](E[[exp_{1}]]ρσ :: E[[exp_{2}]]ρσ :: [])
E[[operator(explist)]]ρσ = O[[operator]](EL[[explist]]ρσ)
E[[name]]ρσ  = E(ρ(name))ρσ
EL[[exp, explist]]ρσ  = E[[exp]]ρσ :: EL[[explist]]ρσ
EL[[ ]]ρσ  = []

As noted above, names denote syntax, which is unusual.

The semantics of RTLs are slightly more complicated than one might expect, because an RTL represents a multiple, simultaneous assignment. The key is the auxiliary function U (“update”), which computes the values of all the guards, locations and right-hand sides. U returns a function, which performs those assignments that are called for by the values of the guards. The denotation function R uses U to compute this function, then applies the function to the current state σ. We use “upds” to update a state and polymorphic “if” to choose between states. Here are the types of the relevant functions.

R : rtl → Env_{r} → Σ → Σ
U : rtl → Env_{r} → Σ → Σ → Σ
upds : Σ → L → V → Σ
if : ∀α.V → Σ → α → α

The following definition of U ignores a subtlety; properly speaking, an RTL should not have a denotation if the same location appears on more than one left-hand side. In our definition, the leftmost assignment takes priority. This simplification is warranted because it enables us to avoid putting error values in our domains, but readers should take care not to use transformations whose correctness depends on the order in which “simultaneous” assignments take place!

U[[location := exp | rtl]]ρσ = λσ′.upds(U[[rtl]]ρσσ′)(L[[location]]ρσ)(E[[exp]]ρσ)

U[[exp_{g} → location := exp_{r} | rtl]]ρσ = if(E[[exp_{g}]]ρσ)(λσ′.upds(U[[rtl]]ρσσ′)(L[[location]]ρσ)(E[[exp_{r}]]ρσ))(U[[rtl]]ρσ)

U[[ ]]ρσ  = λσ′.σ′
U[[name]]ρσ  = U(ρ(name))ρσ
R[[rtl]]ρσ  = U[[rtl]]ρσσ

Next, we present the semantics of statements. We use a continuation semantics in which the answers are sequences of states; these are the sequences used in Section 5. Statements also require an additional environment ρ_{f}, which is used to give meanings to function calls. Our functions are parameterless, and the denotation of a function is the same as the denotation of a statement: a function from continuations to continuations.

C = Σ → A  (continuations)
A = Σ list  (answers)
ρ_{f} : Env_{f} = name → C → C  (function environments)
S : statement → Env_{f} → Env_{r} → C → C

The most important semantic equation is the one for eval_{r}; evaluating an RTL adds a state to the answer. Since our interpreters don’t halt, it doesn’t really matter if we add the pre-state or the post-state; we’ve chosen the pre-state because it is simpler. The other semantic equations are more or less standard.

S[[eval_{r}(rtl)]]ρ_{f}ρ_{r}θ  = λσ.σ :: θ(R[[rtl]]ρ_{r}σ)
S[[statement_{1}; statement_{2}]]ρ_{f}ρ_{r}θ = S[[statement_{1}]]ρ_{f}ρ_{r}(S[[statement_{2}]]ρ_{f}ρ_{r}θ)

S[[if exp then statement_{1} else statement_{2} fi]]ρθ = λσ.if(E[[exp]]ρ_{r}σ)(S[[statement_{1}]]ρ_{f}ρ_{r}θσ)(S[[statement_{2}]]ρ_{f}ρ_{r}θσ)

S[[let (rtl) ≡ memory[exp] in statement end]]ρ_{f}ρ_{r}θ = λσ.S[[statement]]ρ_{f}(decode(E[[exp]]ρ_{r}σ)σrtl ρ_{r})θσ

S[[function-name()]]ρ_{f}ρ_{r}θ  = ρ_{f}function-name θ

The decode function in the rule for let binding hides substantial work. When applied as in

decode addr σ rtl ρ_{r},

the decode function performs the following computations:

(1) It examines the machine state σ, looking at the contents of memory at address addr in that state. Using the machine-dependent rules for binary representations of machine instructions, and the machine-dependent meanings of those instructions, it computes I : Σ → Σ, a representation of the semantics of the machine instruction located at address addr.

(2) It identifies the free variables of rtl, and it chooses bindings for those variables such that given those bindings, the denotation of rtl is I.

(3) Finally, it adds those bindings to environment ρ_{r}, and returns the new environment.

The only remaining semantic equation is the equation for function definitions. A function definition adds another function to the environment ρ_{f}. This equation requires a fixed-point computation to compute the new environment ρ′, because functions may call themselves recursively.

D[[fun name() ≡ statement]]ρ_{f} = ρ′
where ρ′ = upde(ρ_{f}, name, S[[statement]]ρ′(λx.⊥))

Here, (λx.⊥) is the empty RTL environment, and upde adds a binding to an environment.

Given a machine state σ_{0}, which determines a binary program and a program counter, the sequence of states produced by the execution of that program is ρ_{f} i (λσ.⊥)σ_{0}, where i is the name of the interpreter (loop or simple), and ρ_{f} is the environment produced by processing the definitions of the interpreters. If the interpreter runs forever without halting, the usual least-fixed-point calculation produces an infinite list of states.

B. TRANSFORMATIONS

This appendix lists the transformations used in the body of the paper. This list should make it easier for readers to verify the soundness of our transformations. It may also help readers judge how difficult it would be to automate the transformations. Because our purpose is to build readers’ intuitions, not to prove anything, we do not attempt to be completely precise and formal.

—Commutativity of simultaneous composition.

S | T ≡ T | S,

provided S and T have disjoint locations on their left-hand sides. This should be the case for all RTLs of interest.

—Associativity of sequential composition.

S; (T; V) ≡ (S; T); V ≡ S; T; V

—Converting simultaneous composition to sequential composition.

S | T ≡ S; T ,

provided no location on any left-hand side of S appears in a guard or a righthand-side of T. In other words, if the locations changed by S don’t affect the values computed by T, S and T can be performed in sequence, rather than in parallel. This transformation changes the answer produced by a program; it introduces a new intermediate state. Introducing a finite number of such states is harmless, as it doesn’t prevent us from proving the transition lemma. Introducing such new states may be necessary when the target machine’s instruction set does not contain the source machine’s instruction set; this is the rule that enables us to use a sequence of target-machine instructions to translate a single source-machine instruction.

—Distribution of sequential composition over conditional.

if P then S_{1} else S_{2} fi; S_{3} ≡ if P then S_{1}; S_{3} else S_{2}; S_{3} fi

We can move a trailing statement inside a conditional, provided we replicate it on both branches. There is a slightly more restrictive rule for moving leading statements inside conditionals.

S_{1}; if P then S_{2} else S_{3} fi ≡ if P then S_{1}; S_{2} else S_{1}; S_{3} fi,

provided no location modified by S_{1} is read by P. —Distribution of sequential composition over let. We can move a leading statement

inside let, provided there’s no clash of bound variables.

S_{1}; let B in S_{2} end ≡ let B in S_{1}; S_{2} end,

provided no name free in S_{1} is bound in B. There’s a similar rule for trailing statements.

—Alpha-conversion of let. Given let B in S end, we can rename bound variables in B and S.

—“The Trick” on Booleans.

S ≡ if P then S else S

—Constant folding. We partially evaluate with respect to constants as needed. For

example, if [[true]] then S_{1} else S_{2} fi ≡ S_{1}. —Dead-code elimination. Assignments to locations that are never read can be

eliminated. —Forward substitution (assignment). If exactly one write to a location reaches a

read of that location, we can substitute the expression written for the read from the location.

—Forward substitution (conditional). Given a statement if P then S_{1} else S_{2} fi, we may substitute [[true]] for P in S_{1}, and [[false]] for P in S_{2}, provided no conflicting change of state intervenes.

—Introduce assignment. If we know the value of a particular location at a particular program point, we can introduce a redundant assignment to that location. For example, we can introduce annul := annul.

—Function inlining.

name() ≡ S, provided ρ_{f}(name) = S

This rule, together with the preceding two rules, enables us to replace some calls to loop with calls to stable.

In deriving a translator, we introduce a case statement, to which we have applied the following transformation.

—Interchanging the order of tests in an if statement and a case statement. The order of tests of an if statement and a case statement that is nested within the if statement can be interchanged by distributing one over all of the arms of the other.

if P then case F of | E_{1} ⟹ S_{1} … | E_{n} ⟹ S_{n} end else S_{e} fi

≡

case F of

| E_{1} ⟹ if P then S_{1} else S_{e} fi … | E_{n} ⟹ if P then S_{n} else S_{e} fi end