Index: src/ASM/CPP2012-policy/algorithm.tex
===================================================================
--- src/ASM/CPP2012-policy/algorithm.tex (revision 2063)
+++ src/ASM/CPP2012-policy/algorithm.tex (revision 2064)
@@ -124,5 +124,21 @@
\begin{figure}
\begin{algorithmic}
-\Function{jump\_expansion\_step}{x}
+\Function{f}{$labels$,$old\_sigma$,$instr$,$ppc$,$acc$}
+ \State $\langle added, pc, sigma \rangle \gets acc$
+ \If {$instr$ is a backward jump to $j$}
+ \State $length \gets \mathrm{jump\_size}(pc,sigma_1(labels(j)))$
+ \ElsIf {$instr$ is a forward jump to $j$}
+ \State $length \gets \mathrm{jump\_size}(pc,old\_sigma_1(labels(j))+added)$
+ \Else
+ \State $length \gets \mathtt{short\_jump}$
+ \EndIf
+ \State $old\_length \gets \mathrm{old\_sigma_1}(ppc)$
+ \State $new\_length \gets \mathrm{max}(old\_length, length)$
+ \State $old\_size \gets \mathrm{old\_sigma_2}(ppc)$
+ \State $new\_size \gets \mathrm{instruction\_size}(instr,new\_length)$
+ \State $new\_added \gets added+(new\_size-old\_size)$
+ \State $new\_sigma_1(ppc+1) \gets pc+new\_size$
+ \State $new\_sigma_2(ppc) \gets new\_length$ \\
+ \Return $\langle new\_added, pc+new\_size, new\_sigma \rangle$
\EndFunction
\end{algorithmic}
@@ -130,2 +146,52 @@
\label{f:jump_expansion_step}
\end{figure}
+
+The algorithm, shown in figure~\ref{f:jump_expansion_step}, works by folding the
+function {\sc f} over the entire program, thus gradually constructing $sigma$.
+This constitutes one step in the fixed point calculation; successive steps
+repeat the fold until a fixed point is reached.
+
+Parameters of the function {\sc f} are:
+\begin{itemize}
+ \item a function $labels$ that associates a label to its pseudo-address;
+ \item $old\_sigma$, the $\sigma$ function returned by the previous
+ iteration of the fixed point calculcation;
+ \item $instr$, the instruction currently under consideration;
+ \item $ppc$, the pseudo-address of $instr$;
+ \item $acc$, the fold accumulator, which contains $pc$ (the highest memory
+ address reached so far), $added$ (the number of bytes added to the program
+ size with respect to the previous iteration), and of course $sigma$, the
+ $\sigma$ function under construction.
+\end{itemize}
+
+The first two are parameters that remain the same through one iteration, the
+last three are standard parameters for a fold function (including $ppc$,
+which is simply the number of instructions of the program already processed).
+
+The $\sigma$ functions used by {\sc f} are not of the same type as the final
+$\sigma$ function: they are of type
+$\sigma: \mathbb{N} \rightarrow \mathbb{N} \times \{\mathtt{short\_jump},
+\mathtt{medium\_jump},\mathtt{long\_jump}\}$; a function that associates a
+pseudo-address with an memory address and a jump length. We do this to be able
+to more easily compare the jump lengths between iterations. In the algorithm,
+we use the notation $sigma_1(x)$ to denote the memory address corresponding to
+$x$, and $sigma_2(x)$ to denote the jump length corresponding to $x$.
+
+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
+$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
+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.
+
+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.
Index: src/ASM/CPP2012-policy/biblio.bib
===================================================================
--- src/ASM/CPP2012-policy/biblio.bib (revision 2063)
+++ src/ASM/CPP2012-policy/biblio.bib (revision 2064)
@@ -47,2 +47,11 @@
bibsource = {DBLP, http://dblp.uni-trier.de}
}
+
+@inproceedings{Sozeau2006,
+ author = {Matthieu Sozeau},
+ title = {Subset Coercions in {Coq}},
+ booktitle = {{TYPES}},
+ pages = {237--252},
+ year = {2006}
+}
+
Index: src/ASM/CPP2012-policy/conclusion.tex
===================================================================
--- src/ASM/CPP2012-policy/conclusion.tex (revision 2064)
+++ src/ASM/CPP2012-policy/conclusion.tex (revision 2064)
@@ -0,0 +1,1 @@
+\section{Conclusion}
Index: src/ASM/CPP2012-policy/lst-grafite.tex
===================================================================
--- src/ASM/CPP2012-policy/lst-grafite.tex (revision 2064)
+++ src/ASM/CPP2012-policy/lst-grafite.tex (revision 2064)
@@ -0,0 +1,1 @@
+link ../CPP2012-asm/lst-grafite.tex
Index: src/ASM/CPP2012-policy/main.tex
===================================================================
--- src/ASM/CPP2012-policy/main.tex (revision 2063)
+++ src/ASM/CPP2012-policy/main.tex (revision 2064)
@@ -3,5 +3,11 @@
\usepackage{alltt}
\usepackage{amsfonts}
+\usepackage[british]{babel}
\usepackage[utf8]{inputenc}
+\usepackage{listings}
+
+\renewcommand{\verb}{\lstinline}
+\def\lstlanguagefiles{lst-grafite.tex}
+\lstset{language=Grafite}
\begin{document}
@@ -31,4 +37,6 @@
\input{problem}
\input{algorithm}
+\input{proof}
+\input{conclusion}
\bibliography{biblio}
Index: src/ASM/CPP2012-policy/problem.tex
===================================================================
--- src/ASM/CPP2012-policy/problem.tex (revision 2063)
+++ src/ASM/CPP2012-policy/problem.tex (revision 2064)
@@ -67,5 +67,5 @@
The canonical solution, as shown in~\cite{Szymanski1978} or more recently
-in~\cite{Dickson2008} for the x86 instruction set, is to use a fixpoint
+in~\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
@@ -79,5 +79,5 @@
can be used; above this value the jump must be encoded as a long jump.
-Here, termination of the smallest fixpoint algorithm is easy to prove. All
+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 we therefore need to encode
@@ -86,6 +86,6 @@
reasoning holds throughout the subsequent iterations of the algorithms: short
jumps can change into long jumps, but not vice versa. Hence, the algorithm
-either terminates when a fixpoint is reached or when all short jumps have been
-changed into long jumps.
+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
@@ -147,5 +147,5 @@
as medium jumps. Depending on the relative sizes of long and medium jumps, this
solution might actually be smaller than the one reached by the smallest
-fixpoint algorithm.
+fixed point algorithm.
\begin{figure}[h]
Index: src/ASM/CPP2012-policy/proof.tex
===================================================================
--- src/ASM/CPP2012-policy/proof.tex (revision 2064)
+++ src/ASM/CPP2012-policy/proof.tex (revision 2064)
@@ -0,0 +1,59 @@
+\section{The proof}
+
+In this section, we will present the correctness proof of the algorithm in more
+detail.
+
+Since our computation is a least fixed point computation, we must prove
+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 {\tt short} to {\tt medium} and from {\tt medium} to {\tt long}, there
+can be at most $2n$ changes.
+
+This proof has been executed in the ``Russell'' style from~\cite{Sozeau2006}.
+We have proven some invariants of the {\sc f} function from the previous
+section; these invariants are then used to prove properties that hold for every
+iteration of the fixed point computation; and finally, we can prove some
+properties of the fixed point.
+
+The main correctness statement, then, is as follows:
+
+\begin{lstlisting}
+definition jump_expansion':
+$\forall$program:preamble $\times$ ($\Sigma$l:list labelled_instruction.S (|l|) < 2^16).
+ option ($\Sigma$sigma:Word → Word $\times$ bool.
+ $\forall$ppc: Word.$\forall$ppc_ok.
+ let pc := \fst (sigma ppc) in
+ let labels := \fst (create_label_cost_map (\snd program)) in
+ let lookup_labels :=
+ $\lambda$x.bitvector_of_nat ? (lookup_def ?? labels x 0) in
+ let instruction :=
+ \fst (fetch_pseudo_instruction (\snd program) ppc ppc_ok) in
+ let next_pc := \fst (sigma (add ? ppc (bitvector_of_nat ? 1))) in
+ And (nat_of_bitvector $\ldots$ ppc $\leq$ |\snd program| →
+ next_pc = add ? pc (bitvector_of_nat $\ldots$
+ (instruction_size lookup_labels ($\lambda$x.\fst (sigma x))
+ ($\lambda$x.\snd (sigma x)) ppc instruction))
+ )
+ (Or (nat_of_bitvector $\ldots$ ppc < |\snd program| →
+ nat_of_bitvector $\ldots$ pc < nat_of_bitvector $\ldots$ next_pc)
+ (nat_of_bitvector $\ldots$ ppc = |\snd program| → next_pc = (zero $\ldots$))))
+\end{lstlisting}
+
+Informally, this means that when fetching a pseudo-instruction at $ppc$, the
+translation by $\sigma$ of $ppc+1$ is the same as $\sigma(ppc)$ plus the size
+of the instruction at $ppc$; i.e. an instruction is placed immediately
+after the previous one, and there are no overlaps.
+
+The other condition enforced is the fact that instructions are stocked in
+order: the memory address of the instruction at $ppc$ should be smaller than
+the memory address of the instruction at $ppc+1$. There is one exeception to
+this rule: the instruction at the very end of the program, whose successor
+address can be zero (this is the case where the program size is exactly equal
+to the amount of memory).