# Changeset 2064 for src/ASM

Ignore:
Timestamp:
Jun 13, 2012, 5:29:11 PM (9 years ago)
Message:
• more progress
Location:
src/ASM/CPP2012-policy
Files:
4 edited

Unmodified
Removed
• ## src/ASM/CPP2012-policy/algorithm.tex

 r2054 \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} \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.
• ## src/ASM/CPP2012-policy/biblio.bib

 r1889 bibsource = {DBLP, http://dblp.uni-trier.de} } @inproceedings{Sozeau2006, author = {Matthieu Sozeau}, title = {Subset Coercions in {Coq}}, booktitle = {{TYPES}}, pages = {237--252}, year = {2006} }
• ## src/ASM/CPP2012-policy/main.tex

 r2054 \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} \input{problem} \input{algorithm} \input{proof} \input{conclusion} \bibliography{biblio}
• ## src/ASM/CPP2012-policy/problem.tex

 r2054 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 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 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 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]
Note: See TracChangeset for help on using the changeset viewer.