# Changeset 3415 for src

Ignore:
Timestamp:
Jan 14, 2014, 3:09:15 PM (7 years ago)
Message:
• changes for proceedings of TACAS 2014
Location:
src/ASM/TACAS2013-policy
Files:
3 edited

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

 r3393 return a smaller or equal solution. Experiments on the gcc 2.3.3 test suite of C programs have shown that on average, about 25 percent of jumps are encoded as short or absolute jumps by the algorithm. As not all instructions are jumps, this does not make for a large reduction in size, but it can make for a reduction in execution time: if jumps Experimenting with our algorithm on the test suite of C programs included with gcc 2.3.3 has shown that on average, about 25 percent of jumps are encoded as short or absolute jumps by the algorithm. As not all instructions are jumps, this does not make for a large reduction in size, but it can make for a reduction in execution time: if jumps are executed multiple times, for example in loops, the fact that short jumps take less cycles to execute than long jumps can have great effect. As for complexity, there are at most $2n$ iterations, with $n$ the number of As for complexity, there are at most $2n$ iterations, where $n$ is the number of branch instructions. Practical tests within the CerCo project on small to medium pieces of code have shown that in almost all cases, a fixed point is \If {$instr$ is a backward jump to $j$} \State $length \gets \mathrm{jump\_size}(pc,sigma_1(labels(j)))$ \Comment compute jump distance \ElsIf {$instr$ is a forward jump to $j$} \State $length \gets \mathrm{jump\_size}(pc,old\_sigma_1(labels(j))+added)$ \State $old\_length \gets \mathrm{old\_sigma_1}(ppc)$ \State $new\_length \gets \mathrm{max}(old\_length, length)$ \Comment length must never decrease \State $old\_size \gets \mathrm{old\_sigma_2}(ppc)$ \State $new\_size \gets \mathrm{instruction\_size}(instr,new\_length)$ \Comment compute size in bytes \State $new\_added \gets added+(new\_size-old\_size)$ \Comment keep track of total added bytes \State $new\_sigma \gets old\_sigma$ \State $new\_sigma_1(ppc+1) \gets pc+new\_size$ \State $new\_sigma_2(ppc) \gets new\_length$ \\ \State $new\_sigma_2(ppc) \gets new\_length$ \Comment update $\sigma$ \\ \Return $\langle new\_added, pc+new\_size, new\_sigma \rangle$ \EndFunction \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 \item $acc$, the fold accumulator, which contains $added$ (the number of bytes added to the program size with respect to the previous iteration), $pc$ (the highest memory address reached so far), and of course $sigma$, the $\sigma$ function under construction. \end{itemize}
• ## src/ASM/TACAS2013-policy/main.tex

 r3361 \usepackage{amsmath} \usepackage[british]{babel} \usepackage{caption} \usepackage{hyperref} \usepackage[utf8]{inputenc}
• ## src/ASM/TACAS2013-policy/proof.tex

 r3393 &&&&& (pc + \mathtt{instruction\_size}\ sigma\ ppc\ instruction < 2^{16}\ \vee\notag\\ &&&&& (\forall ppc'.ppc' < |instr\_list| \rightarrow ppc < ppc' \rightarrow \notag\\ &&&&& \mathbf{let}\ instruction' \equiv \mathtt{fetch\_pseudo\_instruction}\ instr\_list\ ppc'\ ppc\_ok'\ \mathbf{in} \notag\\ &&&&& \mathbf{let}\ instruction' \equiv \mathtt{fetch\_pseudo\_instruction}\ instr\_list\ ppc'\ \mathbf{in} \notag\\ &&&&&\ \mathtt{instruction\_size}\ sigma\ ppc'\ instruction' = 0)\ \wedge \notag\\ &&&&& pc + \mathtt{instruction\_size}\ sigma\ ppc\ instruction = 2^{16})
Note: See TracChangeset for help on using the changeset viewer.