Index: /src/ASM/CPP2012policy/algorithm.tex
===================================================================
 /src/ASM/CPP2012policy/algorithm.tex (revision 2090)
+++ /src/ASM/CPP2012policy/algorithm.tex (revision 2091)
@@ 8,20 +8,20 @@
The SDCC compiler~\cite{SDCC2011}, which has the MCS51 among its target
instruction sets, simply encodes every jump as a long jump without taking the
distance into account. While certainly correct (the long jump can reach any
destination in memory) and rapid, it does result in a less than optimal
solution.
+instruction sets, simply encodes every branch instruction as a long jump
+without taking the distance into account. While certainly correct (the long
+jump can reach any destination in memory) and rapid, it does result in a less
+than optimal solution.
The {\tt gcc} compiler suite~\cite{GCC2012}, while compiling C on the x86
architecture, uses a greatest fix point algorithm. In other words, it starts
off with all jumps encoded as the largest jumps available, and then tries to
reduce jumps as much as possible.
+off with all branch instructions encoded as the largest jumps available, and
+then tries to reduce branch instructions as much as possible.
Such an algorithm has the advantage that any intermediate results it returns
are correct: the solution where every jump is encoded as a large jump is
always possible, and the algorithm only reduces those jumps where the
destination address is in range for a shorter jump instruction. The algorithm
can thus be stopped after a determined amount of steps without losing
correctness.
+Such an algorithm has the advantage that any intermediate result it returns
+is correct: the solution where every branch instruction is encoded as a large
+jump is always possible, and the algorithm only reduces those branch
+instructions whose destination address is in range for a shorter jump.
+The algorithm can thus be stopped after a determined amount of steps without
+losing correctness.
The result, however, is not necessarily optimal, even if the algorithm is run
@@ 38,33 +38,37 @@
previous section: if we only take short and long jumps into account, the jump
encoding can only switch from short to long, but never in the other direction.
When we add absolute jumps, however, it is theoretically possible for a jump to
switch from absolute to long and back, as explained in the previous section.
+When we add absolute jumps, however, it is theoretically possible for a branch
+instruction to switch from absolute to long and back, as shown in the previous
+section.
Proving termination then becomes difficult, because there is nothing that
precludes a jump from switching back and forth between absolute and long
indefinitely.
+precludes a branch instruction from switching back and forth between absolute
+and long indefinitely.
In order to keep the algorithm in the same complexity class and more easily
prove termination, we decided to explicitly enforce the `jumps must always
increase' requirement: if a jump is encoded as a long jump in one step, it will
also be encoded as a long jump in all the following steps. This means that any
jump can change at most two times: once from short to absolute (or long), and
once from absolute to long.
+prove termination, we decided to explicitly enforce the `branch instructions
+must always grow longer' requirement: if a branch instruction is encoded as a
+long jump in one iteration, it will also be encoded as a long jump in all the
+following iterations. This means that the encoding of any branch instruction
+can change at most two times: once from short to absolute (or long), and once
+from absolute to long.
There is one complicating factor: suppose that a jump is encoded in step $n$
as an absolute jump, but in step $n+1$ it is determined that (because of changes
elsewhere) it can now be encoded as a short jump. Due to the requirement that
jumps must always increase, this means that the jump will be encoded as an
absolute jump in step $n+1$ as well.
+There is one complicating factor: suppose that a branch instruction is encoded
+in step $n$ as an absolute jump, but in step $n+1$ it is determined that
+(because of changes elsewhere) it can now be encoded as a short jump. Due to
+the requirement that the branch instructions must always grow longer, this
+means that the branch encoding will be encoded as an absolute jump in step
+$n+1$ as well.
This is not necessarily correct, however: it is not the case that any short
jump can correctly be encoded as an absolute jump (a short jump can bridge
segments, whereas an absolute jump cannot). Therefore, in this situation
we decide to encode the jump as a long jump, which is always correct.
+This is not necessarily correct, however: a branch instruction that can be
+encoded as a short jump cannot always also be encoded as an absolute jump
+(a short jump can bridge segments, whereas an absolute jump cannot). Therefore,
+in this situation we decide to encode the branch instruction as a long jump,
+which is always correct.
The resulting algorithm, while not optimal, is at least as good as the ones
from SDCC and {\tt gcc}, and potentially better. Its complexity remains
the same (there are at most $2n$ iterations, where $n$ is the number of jumps
in the program).
+the same (there are at most $2n$ iterations, where $n$ is the number of branch
+instructions in the program).
\subsection{The algorithm in detail}
@@ 172,18 +176,19 @@
Note that the $\sigma$ function used for label lookup varies depending on
whether the label is behind our current position or ahead of it. For
backward jumps, where the label is behind our current position, we can use
+backward branches, where the label is behind our current position, we can use
$sigma$ for lookup, since its memory address is already known. However, for
forward jumps, the memory address of the address of the label is not yet
+forward branches, the memory address of the address of the label is not yet
known, so we must use $old\_sigma$.
We cannot use $old\_sigma$ without change: it might be the case that we have
already changed some jumps before, making the program longer. We must therefore
compensate for this by adding the size increase of the program to the label's
memory address according to $old\_sigma$, so that jump distances do not get
compromised.
+already increased the size some branch instructions before, making the program
+longer and moving every instruction forward. We must compensate for this by
+adding the size increase of the program to the label's memory address according
+to $old\_sigma$, so that branch instruction spans do not get compromised.
Note also that we add the pc to $sigma$ at location $ppc+1$, whereas we add the
jump length at location $ppc$. We do this so that $sigma(ppc)$ will always
return a couple with the start address of the instruction at $ppc$ and the
length of its jump; the end address of the program can be found at $sigma(n+1)$,
where $n$ is the number of instructions in the program.
+length of its branch instruction (if any); the end address of the program can
+be found at $sigma(n+1)$, where $n$ is the number of instructions in the
+program.
Index: /src/ASM/CPP2012policy/biblio.bib
===================================================================
 /src/ASM/CPP2012policy/biblio.bib (revision 2090)
+++ /src/ASM/CPP2012policy/biblio.bib (revision 2091)
@@ 59,5 +59,6 @@
title = {Small Device {C} Compiler 3.1.0},
howpublished = {\url{http://sdcc.sourceforge.net/}},
 year = {2011}
+ year = {2011},
+ key = {SDCC2011}
}
@@ 65,5 +66,6 @@
title = {GNU Compiler Collection 4.7.0},
howpublished = {\url{http://gcc.gnu.org/}},
 year = {2012}
+ year = {2012},
+ key = {GCC2012}
}
@@ 94,2 +96,26 @@
}
+@misc {Hyde2006,
+ title = {Branch displacement optimisation},
+ author = {Randall Hyde},
+ howpublished = {\url{http://groups.google.com/group/alt.lang.asm/msg/d31192d442accad3}},
+ year = {2006},
+}
+
+@misc{DC2012,
+ title={On the correctness of an optimising assembler for the Intel MCS51 microprocessor},
+ author = {Dominic P. Mulligan and Claudio {Sacerdoti Coen}},
+ year = {2012},
+ booktitle = {Certified Proofs and Programs {(CPP)}},
+ note = {Submitted}
+}
+
+@article{Asperti2007,
+ author = {Andrea Asperti and Claudio {Sacerdoti Coen} and Enrico Tassi and Stefano Zacchiroli},
+ title = {User interaction with the {Matita} proof assistant},
+ journal = {Automated Reasoning},
+ pages = {109139},
+ volume = {39},
+ issue = {2},
+ year = {2007}
+}
Index: /src/ASM/CPP2012policy/conclusion.tex
===================================================================
 /src/ASM/CPP2012policy/conclusion.tex (revision 2090)
+++ /src/ASM/CPP2012policy/conclusion.tex (revision 2091)
@@ 15,5 +15,5 @@
the complete formalisation and verification of a compiler. More information
on the formalisation of the assembler, of which the present work is a part,
can be found in a companion publication.
+can be found in a companion publication~\cite{DC2012}.
\subsection{Related work}
Index: /src/ASM/CPP2012policy/problem.tex
===================================================================
 /src/ASM/CPP2012policy/problem.tex (revision 2090)
+++ /src/ASM/CPP2012policy/problem.tex (revision 2091)
@@ 2,14 +2,16 @@
The problem of branch displacement optimisation, also known as jump encoding, is
a wellknown problem in assembler design. It is caused by the fact that in
many architecture sets, the encoding (and therefore size) of some instructions
depends on the distance to their operand (the instruction 'span'). The branch
displacement optimisation problem consists in encoding these spandependent
instructions in such a way that the resulting program is as small as possible.
+a wellknown problem in assembler design~\cite{Hyde2006}. It is caused by the
+fact that in many architecture sets, the encoding (and therefore size) of some
+instructions depends on the distance to their operand (the instruction 'span').
+The branch displacement optimisation problem consists in encoding these
+spandependent instructions in such a way that the resulting program is as
+small as possible.
This problem is the subject of the present paper. After introducing the problem
in more detail, we will discuss the solutions used by other compilers, present
the algorithm used by us in the CerCo assembler, and discuss its verification,
that is the proofs of termination and correctness.
+that is the proofs of termination and correctness using the Matita theorem
+prover~\cite{Asperti2007}.
The research presented in this paper has been executed within the CerCo project
@@ 21,13 +23,14 @@
With this optimisation, however, comes increased complexity and hence
increased possibility for error. We must make sure that the jumps are encoded
correctly, otherwise the assembled program will behave unpredictably.
+increased possibility for error. We must make sure that the branch instructions
+are encoded correctly, otherwise the assembled program will behave
+unpredictably.
\section{The branch displacement optimisation problem}
In most modern instruction sets, the only spandependent instructions are
branch instructions. Taking the ubiquitous x8664 instruction set as an
example, we find that it contains are eleven different forms of the
unconditional jump instruction, all with different ranges, instruction sizes
+In most modern instruction sets that have them, the only spandependent
+instructions are branch instructions. Taking the ubiquitous x8664 instruction
+set as an example, we find that it contains are eleven different forms of the
+unconditional branch instruction, all with different ranges, instruction sizes
and semantics (only six are valid in 64bit mode, for example). Some examples
are shown in figure~\ref{f:x86jumps}.
@@ 46,5 +49,5 @@
\end{tabular}
\end{center}
\caption{List of x86 jump instructions}
+\caption{List of x86 branch instructions}
\label{f:x86jumps}
\end{figure}
@@ 67,28 +70,30 @@
\end{tabular}
\end{center}
\caption{List of MCS51 jump instructions}
+\caption{List of MCS51 branch instructions}
\label{f:mcs51jumps}
\end{figure}
The conditional jump instruction is only available in short form, which
means that a conditional jump outside the short address range has to be
encoded using two jumps; the call instruction is only available in
absolute and long forms.
+Conditional branch instructions are only available in short form, which
+means that a conditional branch outside the short address range has to be
+encoded using three branch instructions (for instructions whose logical
+negation is available, it can be done with two branch instructions, but for
+some instructions, this opposite is not available); the call instruction is
+only available in absolute and long forms.
Note that even though the MCS51 architecture is much less advanced and more
simple than the x8664 architecture, the basic types of jump remain the same:
a short jump with a limited range, an intrasegment jump and a jump that can
reach the entire available memory.
+simple than the x8664 architecture, the basic types of branch instruction
+remain the same: a short jump with a limited range, an intrasegment jump and a
+jump that can reach the entire available memory.
Generally, in the code that is sent to the assembler as input, the only
difference made between jump instructions is by semantics, not by span. This
means that a distinction is made between the unconditional jump and the several
kinds of conditional jump, but not between their short, absolute or long
variants.

The algorithm used by the assembler to encode these jumps into the different
machine instructions is known as the {\tt branch displacement algorithm}. The
optimisation problem consists in using as small an encoding as possible, thus
minimising program length and execution time.
+difference made between branch instructions is by semantics, not by span. This
+means that a distinction is made between an unconditional branch and the
+several kinds of conditional branch, but not between their short, absolute or
+long variants.
+
+The algorithm used by the assembler to encode these branch instructions into
+the different machine instructions is known as the {\em branch displacement
+algorithm}. The optimisation problem consists in using as small an encoding as
+possible, thus minimising program length and execution time.
This problem is known to be NPcomplete~\cite{Robertson1979,Szymanski1978},
@@ 98,7 +103,7 @@
recently by Dickson~\cite{Dickson2008} for the x86 instruction set, is to use a
fixed point algorithm that starts out with the shortest possible encoding (all
jumps encoded as short jumps, which is very probably not a correct solution)
and then iterates over the program to reencode those jumps whose target is
outside their range.
+branch instruction encoded as short jumps, which is very probably not a correct
+solution) and then iterates over the program to reencode those branch
+instructions whose target is outside their range.
\subsection*{Adding absolute jumps}
@@ 109,13 +114,13 @@
Here, termination of the smallest fixed point algorithm is easy to prove. All
jumps start out encoded as short jumps, which means that the distance between
any jump and its target is as short as possible. If, in this situation, there
is a jump $j$ whose span is not within the range for a short jump, we can be
sure that we can never reach a situation where the span of $j$ is so small that
it can be encoded as a short jump. This reasoning holds throughout the
subsequent iterations of the algorithm: short jumps can change into long jumps,
but not vice versa (spans only increase). Hence, the algorithm either
terminates when a fixed point is reached or when all short jumps have been
changed into long jumps.
+branch instructions start out encoded as short jumps, which means that the
+distance between any branch instruction and its target is as short as possible.
+If, in this situation, there is a branch instruction $b$ whose span is not
+within the range for a short jump, we can be sure that we can never reach a
+situation where the span of $j$ is so small that it can be encoded as a short
+jump. This argument continues to hold throughout the subsequent iterations of
+the algorithm: short jumps can change into long jumps, but not vice versa
+(spans only increase). Hence, the algorithm either terminates when a fixed
+point is reached or when all short jumps have been changed into long jumps.
Also, we can be certain that we have reached an optimal solution: a short jump
@@ 125,30 +130,33 @@
the absolute jump.
The reason for this is that with absolute jumps, the encoding of a jump no
longer depends only on the distance between the jump and its target: in order
for an absolute jump to be possible, they need to be in the same segment (for
the MCS51, this means that the first 5 bytes of their addresses have to be
equal). It is therefore entirely possible for two jumps with the same span to
be encoded in different ways (absolute if the jump and its target are in the
same segment, long if this is not the case).

This invalidates the termination argument: a jump, once encoded as a long jump,
can be reencoded during a later iteration as an absolute jump. Consider the
program shown in figure~\ref{f:term_example}. At the start of the first
iteration, both the jump to {\tt X} and the jump to $\mathtt{L}_{0}$ are
encoded as small jumps. Let us assume that in this case, the placement of
$\mathtt{L}_{0}$ and the jump to it are such that $\mathtt{L}_{0}$ is just
outside the segment that contains this jump. Let us also assume that the
distance between $\mathtt{L}_{0}$ and the jump to it are too large for the jump
to be encoded as a short jump.

All this means that in the second iteration, the jump to $\mathtt{L}_{0}$ will
be encoded as a long jump. If we assume that the jump to {\tt X} is encoded as
a long jump as well, the size of the jump will increase and $\mathtt{L}_{0}$
will be `propelled' into the same segment as its jump. Hence, in the third
iteration, it can be encoded as an absolute jump. At first glance, there is
nothing that prevents us from making a construction where two jumps interact
in such a way as to keep switching between long and absolute encodings for
an indefinite amount of iterations.
+The reason for this is that with absolute jumps, the encoding of a branch
+instruction no longer depends only on the distance between the branch
+instruction and its target: in order for an absolute jump to be possible, they
+need to be in the same segment (for the MCS51, this means that the first 5
+bytes of their addresses have to be equal). It is therefore entirely possible
+for two branch instructions with the same span to be encoded in different ways
+(absolute if the branch instruction and its target are in the same segment,
+long if this is not the case).
+
+This invalidates the termination argument: a branch instruction, once encoded
+as a long jump, can be reencoded during a later iteration as an absolute jump.
+Consider the program shown in figure~\ref{f:term_example}. At the start of the
+first iteration, both the branch to {\tt X} and the branch to $\mathtt{L}_{0}$
+are encoded as small jumps. Let us assume that in this case, the placement of
+$\mathtt{L}_{0}$ and the branch to it are such that $\mathtt{L}_{0}$ is just
+outside the segment that contains this branch. Let us also assume that the
+distance between $\mathtt{L}_{0}$ and the branch to it are too large for the
+branch instruction to be encoded as a short jump.
+
+All this means that in the second iteration, the branch to $\mathtt{L}_{0}$ will
+be encoded as a long jump. If we assume that the branch to {\tt X} is encoded as
+a long jump as well, the size of the branch instruction will increase and
+$\mathtt{L}_{0}$ will be `propelled' into the same segment as its branch
+instruction, because every subsequent instruction will move one byte forward.
+Hence, in the third iteration, the branch to $\mathtt{L}_{0}$ can be encoded as
+an absolute jump. At first glance, there is nothing that prevents us from
+making a construction where two branch instructions interact in such a way as
+to keep switching between long and absolute encodings for an indefinite amount
+of iterations.
\begin{figure}[h]
@@ 168,9 +176,9 @@
problem is NPcomplete. In this explanation, a condition for NPcompleteness
is the fact that programs be allowed to contain {\em pathological} jumps.
These are jumps that can normally not be encoded as a short(er) jump, but gain
this property when some other jumps are encoded as a long(er) jump. This is
exactly what happens in figure~\ref{f:term_example}: by encoding the first
jump as a long jump, another jump switches from long to absolute
(which is shorter).
+These are branch instructions that can normally not be encoded as a short(er)
+jump, but gain this property when some other branch instructions are encoded as
+a long(er) jump. This is exactly what happens in figure~\ref{f:term_example}:
+by encoding the first branch instruction as a long jump, another branch
+instructions switches from long to absolute (which is shorter).
The optimality argument no longer holds either. Let us consider the program
@@ 178,13 +186,13 @@
$\mathtt{L}_{0}$ and $\mathtt{L}_{1}$ is such that if {\tt jmp X} is encoded
as a short jump, there is a segment border just after $\mathtt{L}_{1}$. Let
us also assume that the three jumps to $\mathtt{L}_{1}$ are all in the same
+us also assume that the three branches to $\mathtt{L}_{1}$ are all in the same
segment, but far enough away from $\mathtt{L}_{1}$ that they cannot be encoded
as short jumps.
Then, if {\tt jmp X} were to be encoded as a short jump, which is clearly
possible, all of the jumps to $\mathtt{L}_{1}$ would have to be encoded as
+possible, all of the branches to $\mathtt{L}_{1}$ would have to be encoded as
long jumps. However, if {\tt jmp X} were to be encoded as a long jump, and
therefore increase in size, $\mathtt{L}_{1}$ would be `propelled' across the
segment border, so that the three jumps to $\mathtt{L}_{1}$ could be encoded
+segment border, so that the three branches to $\mathtt{L}_{1}$ could be encoded
as absolute jumps. Depending on the relative sizes of long and absolute jumps,
this solution might actually be smaller than the one reached by the smallest
Index: /src/ASM/CPP2012policy/proof.tex
===================================================================
 /src/ASM/CPP2012policy/proof.tex (revision 2090)
+++ /src/ASM/CPP2012policy/proof.tex (revision 2091)
@@ 50,13 +50,15 @@
termination in order to prove correctness: if the algorithm is halted after
a number of steps without reaching a fixed point, the solution is not
guaranteed to be correct. More specifically, jumps might be encoded whose
displacement is too great for the instruction chosen.

Proof of termination rests on the fact that jumps can only increase, which
means that we must reach a fixed point after at most $2n$ iterations, with
$2n$ the number of jumps in the program. This worst case is reached if at every
iteration, we change the encoding of exactly one jump; since a jump can change
from short to absolute and from absolute to long, there can be at most $2n$
changes.
+guaranteed to be correct. More specifically, branch instructions might be
+encoded who do not coincide with the span between their location and their
+destination.
+
+Proof of termination rests on the fact that the encoding of branch
+instructions can only grow larger, which means that we must reach a fixed point
+after at most $2n$ iterations, with $n$ the number of branch instructions in
+the program. This worst case is reached if at every iteration, we change the
+encoding of exactly one branch instruction; since the encoding of any branch
+instructions can change first from short to absolute and then from absolute to
+long, there can be at most $2n$ changes.
This proof has been executed in the ``Russell'' style from~\cite{Sozeau2006}.
@@ 99,6 +101,6 @@
This invariant states that when we try to look up the jump length of a
pseudoaddress where there is no jump, we will get the default value, a short
jump.
+pseudoaddress where there is no branch instruction, we will get the default
+value, a short jump.
\begin{lstlisting}
@@ 138,9 +140,9 @@
({\tt sigma\_policy\_specification}); its main difference
with the final version is that it uses {\tt instruction\_size\_jmplen} to
compute the instruction size. This function uses $j$ to compute the size
of jumps (i.e. it uses the $\sigma$ function under construction), instead
of looking at the distance between source and destination. This is because
$\sigma$ is still under construction; later on we will prove that after the
final iteration, {\tt sigma\_compact\_unsafe} is equivalent to the main
+compute the instruction size. This function uses $j$ to compute the span
+of branch instructions (i.e. it uses the $\sigma$ function under construction),
+instead of looking at the distance between source and destination. This is
+because $\sigma$ is still under construction; later on we will prove that after
+the final iteration, {\tt sigma\_compact\_unsafe} is equivalent to the main
property.
@@ 172,11 +174,11 @@
\end{lstlisting}
This is a more direct safety property: it states that jump instructions are
encoded properly, and that no wrong jump instructions are chosen.
+This is a more direct safety property: it states that branch instructions are
+encoded properly, and that no wrong branch instructions are chosen.
Note that we compute the distance using the memory address of the instruction
plus its size: this is due to the behaviour of the MCS51 architecture, which
increases the program counter directly after fetching, and only then executes
the jump.
+the branch instruction (by changing the program counter again).
\begin{lstlisting}
@@ 199,10 +201,11 @@
iteration does not change with respect to the current one. $added$ is the
variable that keeps track of the number of bytes we have added to the program
size by changing jumps; if this is 0, the program has not changed and vice
versa.
+size by changing the encoding of branch instructions; if this is 0, the program
+has not changed and vice versa.
We need to use two different formulations, because the fact that $added$ is 0
does not guarantee that no jumps have changed: it is possible that we have
replaced a short jump with a absolute jump, which does not change the size.
+does not guarantee that no branch instructions have changed: it is possible
+that we have replaced a short jump with a absolute jump, which does not change
+the size of the branch instruction.
Therefore {\tt policy\_pc\_equal} states that $old\_sigma_1(x) = sigma_1(x)$,
@@ 237,6 +240,6 @@
This invariant is applied to $old\_sigma$; if our program becomes too large
for memory, the previous iteration cannot have every jump encoded as a long
jump. This is needed later on in the proof of termination.
+for memory, the previous iteration cannot have every branch instruction encoded
+as a long jump. This is needed later on in the proof of termination.
If the iteration returns $\mathtt{Some}\ \sigma$, the invariants
@@ 270,5 +273,5 @@
This is the same invariant as ${\tt sigma\_compact\_unsafe}$, but instead it
computes the sizes of jump instructions by looking at the distance between
+computes the sizes of branch instructions by looking at the distance between
position and destination using $\sigma$.
@@ 294,12 +297,13 @@
been smaller than 65 Kbytes.
Suppose that all the jumps in the previous iteration are long jumps. This means
that all jumps in this iteration are long jumps as well, and therefore that
both iterations are equal in jumps. Per the invariant, this means that
+Suppose that all the branch instructions in the previous iteration are
+encodes as long jumps. This means that all branch instructions in this
+iteration are long jumps as well, and therefore that both iterations are equal
+in the encoding of their branch instructions. Per the invariant, this means that
$added = 0$, and therefore that all addresses in both iterations are equal.
But if all addresses are equal, the program sizes must be equal too, which
means that the program size in the current iteration must be smaller than
65 Kbytes. This contradicts the earlier hypothesis, hence not all jumps in
the previous iteration are long jumps.
+65 Kbytes. This contradicts the earlier hypothesis, hence not all branch
+instructions in the previous iteration are encoded as long jumps.
The proof of {\tt sigma\_compact} follows from {\tt sigma\_compact\_unsafe} and
@@ 311,6 +315,8 @@
These are the invariants that hold after $2n$ iterations, where $n$ is the
program size. Here, we only need {\tt out\_of\_program\_none},
{\tt sigma\_compact} and the fact that $\sigma(0) = 0$.
+program size (we use the program size for convenience; we could also use the
+number of branch instructions, but this is more complicated). Here, we only
+need {\tt out\_of\_program\_none}, {\tt sigma\_compact} and the fact that
+$\sigma(0) = 0$.
Termination can now be proven through the fact that there is a $k \leq 2n$, with
@@ 319,4 +325,5 @@
property holds, or every iteration up to $2n$ is different. In the latter case,
since the only changes between the iterations can be from shorter jumps to
longer jumps, in iteration $2n$ every jump must be long. In this case,
iteration $2n$ is equal to iteration $2n+1$ and the fixpoint is reached.
+longer jumps, in iteration $2n$ every branch instruction must be encoded as
+a long jump. In this case, iteration $2n$ is equal to iteration $2n+1$ and the
+fixpoint is reached.