# Changeset 3393

Ignore:
Timestamp:
Oct 11, 2013, 4:39:32 PM (6 years ago)
Message:
• TACAS stuff
Location:
src/ASM/TACAS2013-policy
Files:
5 edited

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

 r3370 execution time. On the other hand, the {\tt gcc} compiler suite~\cite{GCC2012}, while compiling On the other hand, the {\tt gcc} compiler suite, while compiling C on the x86 architecture, uses a greatest fix point algorithm. In other words, it starts with all branch instructions encoded as the largest jumps When we add absolute jumps, however, it is theoretically possible for a branch instruction to switch from absolute to long and back, as previously explained. Proving termination then becomes difficult, because there is nothing that precludes a branch instruction from oscillating back and forth between absolute 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 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 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 reached in 3 passes. Only in one case did the algorithm need 4. This is not surprising: after all, the difference between short/absolute and reached in 3 passes. Only in one case did the algorithm need 4. This is not surprising: after all, the difference between short/absolute and long jumps is only one byte (three for conditional jumps). For a change from short/absolute to long to have an effect on other jumps is therefore relatively pseudocode to assembler. More specifically, it is used by the function that translates pseudo-addresses (natural numbers indicating the position of the instruction in the program) to actual addresses in memory. instruction in the program) to actual addresses in memory. Note that in pseudocode, all instructions are of size 1. Our original intention was to have two different functions, one function intended encoding, and a function $\sigma: \mathbb{N} \rightarrow \mathtt{Word}$ to associate pseudo-addresses to machine addresses. $\sigma$ would use $\mathtt{policy}$ to determine the size of jump instructions. This turned out to be suboptimal from the algorithmic point of view and would use $\mathtt{policy}$ to determine the size of jump instructions. This turned out to be suboptimal from the algorithmic point of view and impossible to prove correct. \begin{figure}[t] \small \begin{algorithmic} \Function{f}{$labels$,$old\_sigma$,$instr$,$ppc$,$acc$} \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)$ 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. repeat the fold until a fixed point is reached. We have abstracted away the case where an instruction is not a jump, since the size of these instructions is constant. Parameters of the function {\sc f} are: $\sigma$ function under construction. \end{itemize} The first two are parameters that remain the same through one iteration, the final three are standard parameters for a fold function (including $ppc$, We cannot use $old\_sigma$ without change: it might be the case that we have already increased the size of 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 pair with the start address of the instruction at $ppc$ and the 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. already increased the size of 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 pair with the start address of the instruction at $ppc$ and the %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.
• ## src/ASM/TACAS2013-policy/biblio.bib

 r3370 year = {2011}, key = {SDCC2011} } @misc{GCC2012, title = {GNU Compiler Collection 4.7.0}, howpublished = {\url{http://gcc.gnu.org/}}, year = {2012}, key = {GCC2012} }
• ## src/ASM/TACAS2013-policy/conclusion.tex

 r3370 surely also interesting to formally prove that the assembler never rejects programs that should be accepted, i.e. that the algorithm itself is correct. This was the topic of the current paper. This is the topic of the current paper. \subsection{Related work} displacement optimisation algorithm is not needed. An offshoot of the CompCert project is the CompCertTSO project, which adds thread concurrency and synchronisation to the CompCert compiler~\cite{TSO2011}. This compiler also generates assembly code and therefore does not include a branch displacement algorithm. %An offshoot of the CompCert project is the CompCertTSO project, which adds %thread concurrency and synchronisation to the CompCert compiler~\cite{TSO2011}. %This compiler also generates assembly code and therefore does not include a %branch displacement algorithm. Finally, there is also the Piton stack~\cite{Moore1996}, which not only includes the formal verification of a compiler, but also of the machine architecture targeted by that compiler, a microprocessor called the FM9001. However, this architecture does not have different jump sizes (branching is simulated by assigning values to the program counter), so the branch displacement problem is irrelevant. %Finally, there is also the Piton stack~\cite{Moore1996}, which not only includes the %formal verification of a compiler, but also of the machine architecture %targeted by that compiler, a microprocessor called the FM9001. %However, this architecture does not have different %jump sizes (branching is simulated by assigning values to the program counter), %so the branch displacement problem is irrelevant. \subsection{Formal development} All Matita files related to this development can be found on the CerCo website, \url{http://cerco.cs.unibo.it}. The specific part that contains the branch displacement algorithm is in the {\tt ASM} subdirectory, in the files {\tt PolicyFront.ma}, {\tt PolicyStep.ma} and {\tt Policy.ma}.
• ## src/ASM/TACAS2013-policy/problem.tex

 r3364 contains span-dependent instructions. Furthermore, its maximum addressable memory size is very small (64 Kb), which makes it important to generate programs that are as small as possible. With this optimisation, however, comes increased complexity and hence increased possibility for error. We must make sure that the branch instructions are encoded correctly, otherwise the assembled program will behave unpredictably. programs that are as small as possible. With this optimisation, however, comes increased complexity and hence increased possibility for error. We must make sure that the branch instructions are encoded correctly, otherwise the assembled program will behave unpredictably. All Matita files related to this development can be found on the CerCo website, \url{http://cerco.cs.unibo.it}. The specific part that contains the branch displacement algorithm is in the {\tt ASM} subdirectory, in the files {\tt PolicyFront.ma}, {\tt PolicyStep.ma} and {\tt Policy.ma}. \section{The branch displacement optimisation problem} Here, termination of the smallest fixed point algorithm is easy to prove. All 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. distance between any branch instruction and its target is as short as possible (all the intervening jumps are short). 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 \begin{figure}[t] \begin{subfigure}[b]{.45\linewidth} \small \begin{alltt} jmp X \hfill \begin{subfigure}[b]{.45\linewidth} \small \begin{alltt} L$$\sb{0}$$: jmp X
• ## src/ASM/TACAS2013-policy/proof.tex

 r3370 In this section, we present the correctness proof for the algorithm in more detail. The main correctness statement is shown, slightly simplified, in~Figure~\ref{statement}. \label{sigmapolspec} % \begin{figure}[t] \small \begin{alignat*}{6} \mathtt{sigma}&\omit\rlap{$\mathtt{\_policy\_specification} \equiv \lambda program.\lambda sigma.\lambda policy.$} \notag\\ \lambda program.\lambda sigma.$} \notag\\ & \omit\rlap{$sigma\ 0 = 0\ \wedge$} \notag\\ & \mathbf{let}\ & & \omit\rlap{$instr\_list \equiv code\ program\ \mathbf{in}} \notag\\ &&& \mathbf{let}\ && instruction \equiv \mathtt{fetch\_pseudo\_instruction}\ instr\_list\ ppc\ \mathbf{in} \notag\\ &&& \mathbf{let}\ && next\_pc \equiv sigma\ (ppc+1)\ \mathbf{in}\notag\\ &&&&& next\_pc = pc + \mathtt{instruction\_size}\ sigma\ policy\ ppc\ instruction\ \wedge\notag\\ &&&&& (pc + \mathtt{instruction\_size}\ sigma\ policy\ ppc\ instruction < 2^{16}\ \vee\notag\\ &&&&& next\_pc = pc + \mathtt{instruction\_size}\ sigma\ ppc\ instruction\ \wedge\notag\\ &&&&& (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\\ &&&&&\ \mathtt{instruction\_size}\ sigma\ policy\ ppc'\ instruction' = 0)\ \wedge \notag\\ &&&&& pc + \mathtt{instruction\_size}\ sigma\ policy\ ppc\ instruction = 2^{16}) &&&&&\ \mathtt{instruction\_size}\ sigma\ ppc'\ instruction' = 0)\ \wedge \notag\\ &&&&& pc + \mathtt{instruction\_size}\ sigma\ ppc\ instruction = 2^{16}) \end{alignat*} \caption{Main correctness statement\label{statement}} \label{sigmapolspec} \end{figure} % Informally, this means that when fetching a pseudo-instruction atppc$, the translation by$\sigma$of$ppc+1$is the same as$\sigma(ppc)$plus the size of the instruction at$ppc$. That is, an instruction is placed consecutively after the previous one, and there are no overlaps. Instructions are also 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 exception 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). Finally, we enforce that the program starts at address 0, i.e.$\sigma(0) = 0$. after the previous one, and there are no overlaps. The rest of the statement deals with memory size: either the next instruction fits within memory ($next\_pc < 2^{16}$) or it ends exactly at the limit memory, in which case it must be the last translated instruction in the program (enforced by specfiying that the size of all subsequent instructions is 0: there may be comments or cost annotations that are not translated). Finally, we enforce that the program starts at address 0, i.e.$\sigma(0) = 0$. It may seem strange that we do not explicitly include a safety property stating that every jump instruction is of the right type with respect to its target (akin to the lemma from Figure~\ref{sigmasafe}), but this is not necessary. The distance is recalculated according to the instruction addresses from$\sigma$, which implicitly expresses safety. Since our computation is a least fixed point computation, we must prove can be at most$2n$changes. The proof has been carried out using 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 proof has been carried out using 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. \subsection{Fold invariants} In this section, we present the invariants that hold during the fold of {\sc f} over the program. These will be used later on to prove the properties of the iteration. Note that during the fixed point computation, the$\sigma$function is iteration. During the fixed point computation, the$\sigma$function is implemented as a trie for ease of access; computing$\sigma(x)$is achieved by looking up the value of$x$in the trie. Actually, during the fold, the value component is the number of bytes added to the program so far with respect to the previous iteration, and the second component, {\tt ppc\_pc\_map}, is the actual$\sigma$trie. actual$\sigma$trie (which we'll call$strieto avoid confusion). % {\small \begin{alignat*}{2} \mathtt{out} & \mathtt{\_of\_program\_none} \equiv \lambda prefix.\lambda sigma. \notag\\ \mathtt{out} & \mathtt{\_of\_program\_none} \equiv \lambda prefix.\lambda strie. \notag\\ & \forall i.i < 2^{16} \rightarrow (i > |prefix| \leftrightarrow \mathtt{lookup\_opt}\ i\ (\mathtt{snd}\ sigma) = \mathtt{None}) \end{alignat*} \mathtt{lookup\_opt}\ i\ (\mathtt{snd}\ strie) = \mathtt{None}) \end{alignat*}} % The first invariant states that any pseudo-address not yet examined is not present in the lookup trie. % {\small \begin{alignat*}{2} \mathtt{not} & \mathtt{\_jump\_default} \equiv \lambda prefix.\lambda sigma.\notag\\ & \forall i.i < |prefix| \rightarrow\notag\\ & \neg\mathtt{is\_jump}\ (\mathtt{nth}\ i\ prefix) \rightarrow\notag\\ & \mathtt{lookup}\ i\ (\mathtt{snd}\ sigma) = \mathtt{short\_jump} \end{alignat*} \mathtt{not} & \mathtt{\_jump\_default} \equiv \lambda prefix.\lambda strie.\forall i.i < |prefix| \rightarrow\notag\\ & \neg\mathtt{is\_jump}\ (\mathtt{nth}\ i\ prefix) \rightarrow \mathtt{lookup}\ i\ (\mathtt{snd}\ strie) = \mathtt{short\_jump} \end{alignat*}} % This invariant states that when we try to look up the jump length of a pseudo-address where there is no branch instruction, we will get the default value, a short jump. % {\small \begin{alignat*}{4} \mathtt{jump} & \omit\rlap{\mathtt{\_increase} \equiv \lambda pc.\lambda op.\lambda p.$} \notag\\ & \omit\rlap{$\forall i.i < |prefix| \rightarrow} \notag\\ & \mathbf{let}\ && oj \equiv \mathtt{lookup}\ i\ (\mathtt{snd}\ op)\ \mathbf{in} \notag\\ & \mathbf{let}\ && j \equiv \mathtt{lookup}\ i\ (\mathtt{snd}\ p)\ \mathbf{in} \notag\\ &&& \mathtt{jmpleq}\ oj\ j \end{alignat*} \mathtt{jump} & \mathtt{\_increase} \equiv \lambda pc.\lambda op.\lambda p.\forall i.i < |prefix| \rightarrow \notag\\ & \mathbf{let}\ oj \equiv \mathtt{lookup}\ i\ (\mathtt{snd}\ op)\ \mathbf{in} \notag\\ & \mathbf{let}\ j \equiv \mathtt{lookup}\ i\ (\mathtt{snd}\ p)\ \mathbf{in}\ \mathtt{jmpleq}\ oj\ j \end{alignat*}} % This invariant states that between iterations (withop$being the previous iteration, and$pthe current one), jump lengths either remain equal or increase. It is needed for proving termination. \begin{figure}[ht] \begin{alignat*}{6} \mathtt{sigma} & \omit\rlap{\mathtt{\_compact\_unsafe} \equiv \lambda prefix.\lambda sigma.$}\notag\\ & \omit\rlap{$\forall n.n < |prefix| \rightarrow$}\notag\\ & \mathbf{match}\ && \omit\rlap{$\mathtt{lookup\_opt}\ n\ (\mathtt{snd}\ sigma)\ \mathbf{with}}\notag\\ % \begin{figure}[h] \small \begin{alignat*}{6} \mathtt{sigma} & \omit\rlap{\mathtt{\_compact\_unsafe} \equiv \lambda prefix.\lambda strie.\forall n.n < |prefix| \rightarrow$}\notag\\ & \mathbf{match}\ && \omit\rlap{$\mathtt{lookup\_opt}\ n\ (\mathtt{snd}\ strie)\ \mathbf{with}$}\notag\\ &&& \omit\rlap{$\mathtt{None} \Rightarrow \mathrm{False}$} \notag\\ &&& \omit\rlap{$\mathtt{Some}\ \langle pc, j \rangle \Rightarrow$} \notag\\ &&& \mathbf{match}\ && \mathtt{lookup\_opt}\ (n+1)\ (\mathtt{snd}\ sigma)\ \mathbf{with}\notag\\ &&& \mathbf{match}\ && \mathtt{lookup\_opt}\ (n+1)\ (\mathtt{snd}\ strie)\ \mathbf{with}\notag\\ &&&&& \mathtt{None} \Rightarrow \mathrm{False} \notag\\ &&&&& \mathtt{Some}\ \langle pc_1, j_1 \rangle \Rightarrow \label{sigmacompactunsafe} \end{figure} % We now proceed with the safety lemmas. The lemma in Figure~\ref{sigmacompactunsafe} is a temporary formulation of the main$\sigmais still under construction; we will prove below that after the final iteration, {\tt sigma\_compact\_unsafe} is equivalent to the main property. \begin{figure}[ht] \begin{alignat*}{6} \mathtt{sigma} & \omit\rlap{\mathtt{\_safe} \equiv \lambda prefix.\lambda labels.\lambda old\_sigma.\lambda sigma$}\notag\\ & \omit\rlap{$\forall i.i < |prefix| \rightarrow} \notag\\ property in Figure~\ref{sigmasafe} which holds at the end of the computation. % \begin{figure}[h] \small \begin{alignat*}{6} \mathtt{sigma} & \omit\rlap{\mathtt{\_safe} \equiv \lambda prefix.\lambda labels.\lambda old\_strie.\lambda strie.\forall i.i < |prefix| \rightarrow$} \notag\\ & \omit\rlap{$\forall dest\_label.\mathtt{is\_jump\_to\ (\mathtt{nth}\ i\ prefix})\ dest\_label \rightarrow$} \notag\\ & \mathbf{let} && \omit\rlap{$\ paddr \equiv \mathtt{lookup}\ labels\ dest\_label\ \mathbf{in}$} \notag\\ & \mathbf{let} && \omit\rlap{$\ \langle j, src, dest \rangle \equiv$}\notag\\ &&& \omit\rlap{$\mathbf{if} \ paddr\ \leq\ i\ \mathbf{then}$}\notag\\ &&&&& \mathbf{let}\ \langle \_, j \rangle \equiv \mathtt{lookup}\ i\ (\mathtt{snd}\ sigma)\ \mathbf{in} \notag\\ &&&&& \mathbf{let}\ \langle pc\_plus\_jl, \_ \rangle \equiv \mathtt{lookup}\ (i+1)\ (\mathtt{snd}\ sigma)\ \mathbf{in}\notag\\ &&&&& \mathbf{let}\ \langle addr, \_ \rangle \equiv \mathtt{lookup}\ paddr\ (\mathtt{snd}\ sigma)\ \mathbf{in}\notag\\ & \mathbf{let} && \omit\rlap{$\ \langle j, src, dest \rangle \equiv \mathbf{if} \ paddr\ \leq\ i\ \mathbf{then}$}\notag\\ &&&&& \mathbf{let}\ \langle \_, j \rangle \equiv \mathtt{lookup}\ i\ (\mathtt{snd}\ strie)\ \mathbf{in} \notag\\ &&&&& \mathbf{let}\ \langle pc\_plus\_jl, \_ \rangle \equiv \mathtt{lookup}\ (i+1)\ (\mathtt{snd}\ strie)\ \mathbf{in}\notag\\ &&&&& \mathbf{let}\ \langle addr, \_ \rangle \equiv \mathtt{lookup}\ paddr\ (\mathtt{snd}\ strie)\ \mathbf{in}\notag\\ &&&&& \langle j, pc\_plus\_jl, addr \rangle\notag\\ &&&\mathbf{else} \notag\\ &&&&&\mathbf{let}\ \langle \_, j \rangle \equiv \mathtt{lookup}\ i\ (\mathtt{snd}\ sigma)\ \mathbf{in} \notag\\ &&&&&\mathbf{let}\ \langle pc\_plus\_jl, \_ \rangle \equiv \mathtt{lookup}\ (i+1)\ (\mathtt{snd}\ old\_sigma)\ \mathbf{in}\notag\\ &&&&&\mathbf{let}\ \langle addr, \_ \rangle \equiv \mathtt{lookup}\ paddr\ (\mathtt{snd}\ old\_sigma)\ \mathbf{in}\notag\\ &&&&&\langle j, pc\_plus\_jl, addr \rangle\notag\\ &&&\omit\rlap{$\mathbf{in}}\notag\\ &&&&&\mathbf{let}\ \langle \_, j \rangle \equiv \mathtt{lookup}\ i\ (\mathtt{snd}\ strie)\ \mathbf{in} \notag\\ &&&&&\mathbf{let}\ \langle pc\_plus\_jl, \_ \rangle \equiv \mathtt{lookup}\ (i+1)\ (\mathtt{snd}\ old\_strie)\ \mathbf{in}\notag\\ &&&&&\mathbf{let}\ \langle addr, \_ \rangle \equiv \mathtt{lookup}\ paddr\ (\mathtt{snd}\ old\_strie)\ \mathbf{in}\notag\\ &&&&&\langle j, pc\_plus\_jl, addr \rangle \mathbf{in}\ \notag\\ &&&\mathbf{match} && \ j\ \mathbf{with} \notag\\ &&&&&\mathrm{short\_jump} \Rightarrow \mathtt{short\_jump\_valid}\ src\ dest\notag\\ \label{sigmasafe} \end{figure} The lemma in figure~\ref{sigmasafe} is a 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 % We compute the distance using the memory address of the instruction plus its size. This follows the behaviour of the MCS-51 microprocessor, which increases the program counter directly after fetching, and only then executes the branch instruction (by changing the program counter again). We now encode some final, simple, properties to make sure that our policy There are also some simple, properties to make sure that our policy remains consistent, and to keep track of whether the fixed point has been reached. \begin{align*} & \mathtt{lookup}\ 0\ (\mathtt{snd}\ policy) = 0 \notag\\ & \mathtt{lookup}\ |prefix|\ (\mathtt{snd}\ policy) = \mathtt{fst}\ policy \end{align*} These two properties give the values of\sigma$for the start and end of the program;$\sigma(0) = 0$and$\sigma(n)$, where$nis the number of instructions up until now, is equal to the maximum memory address so far. \begin{align*} & added = 0\ \rightarrow\ \mathtt{policy\_pc\_equal}\ prefix\ old\_sigma\ policy \notag\\ & \mathtt{policy\_jump\_equal}\ prefix\ old\_sigma\ policy\ \rightarrow\ added = 0 \end{align*} And finally, two properties that deal with what happens when the previous reached. We do not include them here in detail. Two of these properties give the values of\sigma$for the start and end of the program;$\sigma(0) = 0$and$\sigma(n)$, where$n$is the number of instructions up until now, is equal to the maximum memory address so far. There are also two properties that deal with what happens when the previous iteration does not change with respect to the current one.$addedis a variable that keeps track of the number of bytes we have added to the program has not changed and vice versa. %{\small %\begin{align*} %& \mathtt{lookup}\ 0\ (\mathtt{snd}\ strie) = 0 \notag\\ %& \mathtt{lookup}\ |prefix|\ (\mathtt{snd}\ strie) = \mathtt{fst}\ strie %\end{align*}} %{\small %\begin{align*} %& added = 0\ \rightarrow\ \mathtt{policy\_pc\_equal}\ prefix\ old\_strie\ strie \notag\\ %& \mathtt{policy\_jump\_equal}\ prefix\ old\_strie\ strie\ \rightarrow\ added = 0 %\end{align*}} We need to use two different formulations, because the fact thatadded$is 0 does not guarantee that no branch instructions have changed. For instance, it is possible that we have replaced a short jump with an 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)$, whereas {\tt policy\_jump\_equal} states that$old\_sigma_2(x) = sigma_2(x)$. This formulation is sufficient to prove termination and compactness. does not change the size of the branch instruction. Therefore {\tt policy\_pc\_equal} states that$old\_sigma_1(x) = sigma_1(x)$, whereas {\tt policy\_jump\_equal} states that$old\_sigma_2(x) = sigma_2(x)$. This formulation is sufficient to prove termination and compactness. Proving these invariants is simple, usually by induction on the prefix length. difference between these invariants and the fold invariants is that after the completion of the fold, we check whether the program size does not supersede 64 Kb, the maximum memory size the MCS-51 can address. The type of an iteration therefore becomes an option type: {\tt None} in case 64 Kb, the maximum memory size the MCS-51 can address. The type of an iteration therefore becomes an option type: {\tt None} in case the program becomes larger than 64 Kb, or$\mathtt{Some}\ \sigmaotherwise. We also no longer pass along the number of bytes added to the program size, but a boolean that indicates whether we have changed something during the iteration or not. If an iteration returns {\tt None}, we have the following invariant: \begin{alignat*}{2} \mathtt{nec} & \mathtt{\_plus\_ultra} \equiv \lambda program.\lambda p. \notag\\ &\neg(\forall i.i < |program|\ \rightarrow \notag\\ & \mathtt{is\_jump}\ (\mathtt{nth}\ i\ program)\ \rightarrow \notag\\ & \mathtt{lookup}\ i\ (\mathtt{snd}\ p) = \mathrm{long\_jump}). \end{alignat*} This invariant is applied toold\_sigma$; if our program becomes too large for memory, the previous iteration cannot have every branch instruction encoded as a long jump. This is needed later in the proof of termination. If the iteration returns$\mathtt{Some}\ \sigma$, the invariants {\tt out\_of\_program\_none},\\ {\tt not\_jump\_default}, {\tt jump\_increase}, and the two invariants that deal with$\sigma(0)$and$\sigma(n)$are retained without change. during the iteration or not. If the iteration returns {\tt None}, which means that it has become too large for memory, there is an invariant that states that the previous iteration cannot have every branch instruction encoded as a long jump. This is needed later in the proof of termination. If the iteration returns$\mathtt{Some}\ \sigma, the fold invariants are retained without change. Instead of using {\tt sigma\_compact\_unsafe}, we can now use the proper invariant: % {\small \begin{alignat*}{6} \mathtt{sigma} & \omit\rlap{\mathtt{\_compact} \equiv \lambda program.\lambda sigma.} \notag\\ &&&&& \mathrm{Some} \langle pc1, j1 \rangle \Rightarrow\notag\\ &&&&& \ \ pc1 = pc + \mathtt{instruction\_size}\ n\ (\mathtt{nth}\ n\ program) \end{alignat*} \end{alignat*}} % This is almost the same invariant as{\tt sigma\_compact\_unsafe}$, but differs in that it computes the sizes of branch instructions by looking at the distance between position and destination using$\sigma$. In actual use, the invariant is qualified:$\sigma$is compact if there have position and destination using$\sigma$. In actual use, the invariant is qualified:$\sigma$is compact if there have been no changes (i.e. the boolean passed along is {\tt true}). This is to reflect the fact that we are doing a least fixed point computation: the result$\mathtt{Some}\ \sigma$: it must hold that$\mathtt{fst}\ sigma < 2^{16}\$. We need this invariant to make sure that addresses do not overflow. The invariants taken directly from the fold invariants are trivial to prove. The proof of {\tt nec\_plus\_ultra} goes as follows: if we return {\tt None},
Note: See TracChangeset for help on using the changeset viewer.