1 | \section{The proof} |
---|
2 | |
---|
3 | In this section, we present the correctness proof for the algorithm in more |
---|
4 | detail. The main correctness statement is shown, slightly simplified, in~Figure~\ref{statement}. |
---|
5 | % |
---|
6 | \begin{figure}[t] |
---|
7 | \small |
---|
8 | \begin{alignat*}{6} |
---|
9 | \mathtt{sigma}&\omit\rlap{$\mathtt{\_policy\_specification} \equiv |
---|
10 | \lambda program.\lambda sigma.$} \notag\\ |
---|
11 | & \omit\rlap{$sigma\ 0 = 0\ \wedge$} \notag\\ |
---|
12 | & \mathbf{let}\ & & \omit\rlap{$instr\_list \equiv code\ program\ \mathbf{in}$} \notag\\ |
---|
13 | &&& \omit\rlap{$\forall ppc.ppc < |instr\_list| \rightarrow$} \notag\\ |
---|
14 | &&& \mathbf{let}\ && pc \equiv sigma\ ppc\ \mathbf{in} \notag\\ |
---|
15 | &&& \mathbf{let}\ && instruction \equiv \mathtt{fetch\_pseudo\_instruction}\ instr\_list\ ppc\ \mathbf{in} \notag\\ |
---|
16 | &&& \mathbf{let}\ && next\_pc \equiv sigma\ (ppc+1)\ \mathbf{in}\notag\\ |
---|
17 | &&&&& next\_pc = pc + \mathtt{instruction\_size}\ sigma\ ppc\ instruction\ \wedge\notag\\ |
---|
18 | &&&&& (pc + \mathtt{instruction\_size}\ sigma\ ppc\ instruction < 2^{16}\ \vee\notag\\ |
---|
19 | &&&&& (\forall ppc'.ppc' < |instr\_list| \rightarrow ppc < ppc' \rightarrow \notag\\ |
---|
20 | &&&&& \mathbf{let}\ instruction' \equiv \mathtt{fetch\_pseudo\_instruction}\ instr\_list\ ppc'\ \mathbf{in} \notag\\ |
---|
21 | &&&&&\ \mathtt{instruction\_size}\ sigma\ ppc'\ instruction' = 0)\ \wedge \notag\\ |
---|
22 | &&&&& pc + \mathtt{instruction\_size}\ sigma\ ppc\ instruction = 2^{16}) |
---|
23 | \end{alignat*} |
---|
24 | \caption{Main correctness statement\label{statement}} |
---|
25 | \label{sigmapolspec} |
---|
26 | \end{figure} |
---|
27 | % |
---|
28 | Informally, this means that when fetching a pseudo-instruction at $ppc$, the |
---|
29 | translation by $\sigma$ of $ppc+1$ is the same as $\sigma(ppc)$ plus the size |
---|
30 | of the instruction at $ppc$. That is, an instruction is placed consecutively |
---|
31 | 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, |
---|
32 | 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). |
---|
33 | |
---|
34 | 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. |
---|
35 | |
---|
36 | Since our computation is a least fixed point computation, we must prove |
---|
37 | termination in order to prove correctness: if the algorithm is halted after |
---|
38 | a number of steps without reaching a fixed point, the solution is not |
---|
39 | guaranteed to be correct. More specifically, branch instructions might be |
---|
40 | encoded which do not coincide with the span between their location and their |
---|
41 | destination. |
---|
42 | |
---|
43 | Proof of termination rests on the fact that the encoding of branch |
---|
44 | instructions can only grow larger, which means that we must reach a fixed point |
---|
45 | after at most $2n$ iterations, with $n$ the number of branch instructions in |
---|
46 | the program. This worst case is reached if at every iteration, we change the |
---|
47 | encoding of exactly one branch instruction; since the encoding of any branch |
---|
48 | instruction can change first from short to absolute, and then to long, there |
---|
49 | can be at most $2n$ changes. |
---|
50 | |
---|
51 | %The proof has been carried out using the ``Russell'' style from~\cite{Sozeau2006}. |
---|
52 | %We have proven some invariants of the {\sc f} function from the previous |
---|
53 | %section; these invariants are then used to prove properties that hold for every |
---|
54 | %iteration of the fixed point computation; and finally, we can prove some |
---|
55 | %properties of the fixed point. |
---|
56 | |
---|
57 | \subsection{Fold invariants} |
---|
58 | |
---|
59 | In this section, we present the invariants that hold during the fold of {\sc f} |
---|
60 | over the program. These will be used later on to prove the properties of the |
---|
61 | iteration. During the fixed point computation, the $\sigma$ function is |
---|
62 | implemented as a trie for ease of access; computing $\sigma(x)$ is achieved by |
---|
63 | looking up the value of $x$ in the trie. Actually, during the fold, the value |
---|
64 | we pass along is a pair $\mathbb{N} \times \mathtt{ppc\_pc\_map}$. The first |
---|
65 | component is the number of bytes added to the program so far with respect to |
---|
66 | the previous iteration, and the second component, {\tt ppc\_pc\_map}, is the |
---|
67 | actual $\sigma$ trie (which we'll call $strie$ to avoid confusion). |
---|
68 | % |
---|
69 | {\small |
---|
70 | \begin{alignat*}{2} |
---|
71 | \mathtt{out} & \mathtt{\_of\_program\_none} \equiv \lambda prefix.\lambda strie. \notag\\ |
---|
72 | & \forall i.i < 2^{16} \rightarrow (i > |prefix| \leftrightarrow |
---|
73 | \mathtt{lookup\_opt}\ i\ (\mathtt{snd}\ strie) = \mathtt{None}) |
---|
74 | \end{alignat*}} |
---|
75 | % |
---|
76 | The first invariant states that any pseudo-address not yet examined is not |
---|
77 | present in the lookup trie. |
---|
78 | % |
---|
79 | {\small |
---|
80 | \begin{alignat*}{2} |
---|
81 | \mathtt{not} & \mathtt{\_jump\_default} \equiv \lambda prefix.\lambda strie.\forall i.i < |prefix| \rightarrow\notag\\ |
---|
82 | & \neg\mathtt{is\_jump}\ (\mathtt{nth}\ i\ prefix) \rightarrow \mathtt{lookup}\ i\ (\mathtt{snd}\ strie) = \mathtt{short\_jump} |
---|
83 | \end{alignat*}} |
---|
84 | % |
---|
85 | This invariant states that when we try to look up the jump length of a |
---|
86 | pseudo-address where there is no branch instruction, we will get the default |
---|
87 | value, a short jump. |
---|
88 | % |
---|
89 | {\small |
---|
90 | \begin{alignat*}{4} |
---|
91 | \mathtt{jump} & \mathtt{\_increase} \equiv \lambda pc.\lambda op.\lambda p.\forall i.i < |prefix| \rightarrow \notag\\ |
---|
92 | & \mathbf{let}\ oj \equiv \mathtt{lookup}\ i\ (\mathtt{snd}\ op)\ \mathbf{in} \notag\\ |
---|
93 | & \mathbf{let}\ j \equiv \mathtt{lookup}\ i\ (\mathtt{snd}\ p)\ \mathbf{in}\ \mathtt{jmpleq}\ oj\ j |
---|
94 | \end{alignat*}} |
---|
95 | % |
---|
96 | This invariant states that between iterations (with $op$ being the previous |
---|
97 | iteration, and $p$ the current one), jump lengths either remain equal or |
---|
98 | increase. It is needed for proving termination. |
---|
99 | % |
---|
100 | \begin{figure}[h] |
---|
101 | \small |
---|
102 | \begin{alignat*}{6} |
---|
103 | \mathtt{sigma} & \omit\rlap{$\mathtt{\_compact\_unsafe} \equiv \lambda prefix.\lambda strie.\forall n.n < |prefix| \rightarrow$}\notag\\ |
---|
104 | & \mathbf{match}\ && \omit\rlap{$\mathtt{lookup\_opt}\ n\ (\mathtt{snd}\ strie)\ \mathbf{with}$}\notag\\ |
---|
105 | &&& \omit\rlap{$\mathtt{None} \Rightarrow \mathrm{False}$} \notag\\ |
---|
106 | &&& \omit\rlap{$\mathtt{Some}\ \langle pc, j \rangle \Rightarrow$} \notag\\ |
---|
107 | &&& \mathbf{match}\ && \mathtt{lookup\_opt}\ (n+1)\ (\mathtt{snd}\ strie)\ \mathbf{with}\notag\\ |
---|
108 | &&&&& \mathtt{None} \Rightarrow \mathrm{False} \notag\\ |
---|
109 | &&&&& \mathtt{Some}\ \langle pc_1, j_1 \rangle \Rightarrow |
---|
110 | pc_1 = pc + \notag\\ |
---|
111 | &&&&& \ \ \mathtt{instruction\_size\_jmplen}\ j\ (\mathtt{nth}\ n\ prefix) |
---|
112 | \end{alignat*} |
---|
113 | \caption{Temporary safety property} |
---|
114 | \label{sigmacompactunsafe} |
---|
115 | \end{figure} |
---|
116 | % |
---|
117 | We now proceed with the safety lemmas. The lemma in |
---|
118 | Figure~\ref{sigmacompactunsafe} is a temporary formulation of the main |
---|
119 | property {\tt sigma\_policy\_specification}. Its main difference from the |
---|
120 | final version is that it uses {\tt instruction\_size\_jmplen} to compute the |
---|
121 | instruction size. This function uses $j$ to compute the span of branch |
---|
122 | instructions (i.e. it uses the $\sigma$ under construction), instead |
---|
123 | of looking at the distance between source and destination. This is because |
---|
124 | $\sigma$ is still under construction; we will prove below that after the |
---|
125 | final iteration, {\tt sigma\_compact\_unsafe} is equivalent to the main |
---|
126 | property in Figure~\ref{sigmasafe} which holds at the end of the computation. |
---|
127 | % |
---|
128 | \begin{figure}[h] |
---|
129 | \small |
---|
130 | \begin{alignat*}{6} |
---|
131 | \mathtt{sigma} & \omit\rlap{$\mathtt{\_safe} \equiv \lambda prefix.\lambda labels.\lambda old\_strie.\lambda strie.\forall i.i < |prefix| \rightarrow$} \notag\\ |
---|
132 | & \omit\rlap{$\forall dest\_label.\mathtt{is\_jump\_to\ (\mathtt{nth}\ i\ prefix})\ dest\_label \rightarrow$} \notag\\ |
---|
133 | & \mathbf{let} && \omit\rlap{$\ paddr \equiv \mathtt{lookup}\ labels\ dest\_label\ \mathbf{in}$} \notag\\ |
---|
134 | & \mathbf{let} && \omit\rlap{$\ \langle j, src, dest \rangle \equiv \mathbf{if} \ paddr\ \leq\ i\ \mathbf{then}$}\notag\\ |
---|
135 | &&&&& \mathbf{let}\ \langle \_, j \rangle \equiv \mathtt{lookup}\ i\ (\mathtt{snd}\ strie)\ \mathbf{in} \notag\\ |
---|
136 | &&&&& \mathbf{let}\ \langle pc\_plus\_jl, \_ \rangle \equiv \mathtt{lookup}\ (i+1)\ (\mathtt{snd}\ strie)\ \mathbf{in}\notag\\ |
---|
137 | &&&&& \mathbf{let}\ \langle addr, \_ \rangle \equiv \mathtt{lookup}\ paddr\ (\mathtt{snd}\ strie)\ \mathbf{in}\notag\\ |
---|
138 | &&&&& \langle j, pc\_plus\_jl, addr \rangle\notag\\ |
---|
139 | &&&\mathbf{else} \notag\\ |
---|
140 | &&&&&\mathbf{let}\ \langle \_, j \rangle \equiv \mathtt{lookup}\ i\ (\mathtt{snd}\ strie)\ \mathbf{in} \notag\\ |
---|
141 | &&&&&\mathbf{let}\ \langle pc\_plus\_jl, \_ \rangle \equiv \mathtt{lookup}\ (i+1)\ (\mathtt{snd}\ old\_strie)\ \mathbf{in}\notag\\ |
---|
142 | &&&&&\mathbf{let}\ \langle addr, \_ \rangle \equiv \mathtt{lookup}\ paddr\ (\mathtt{snd}\ old\_strie)\ \mathbf{in}\notag\\ |
---|
143 | &&&&&\langle j, pc\_plus\_jl, addr \rangle \mathbf{in}\ \notag\\ |
---|
144 | &&&\mathbf{match} && \ j\ \mathbf{with} \notag\\ |
---|
145 | &&&&&\mathrm{short\_jump} \Rightarrow \mathtt{short\_jump\_valid}\ src\ dest\notag\\ |
---|
146 | &&&&&\mathrm{absolute\_jump} \Rightarrow \mathtt{absolute\_jump\_valid}\ src\ dest\notag\\ |
---|
147 | &&&&&\mathrm{long\_jump} \Rightarrow \mathrm{True} |
---|
148 | \end{alignat*} |
---|
149 | \caption{Safety property} |
---|
150 | \label{sigmasafe} |
---|
151 | \end{figure} |
---|
152 | % |
---|
153 | We compute the distance using the memory address of the instruction |
---|
154 | plus its size. This follows the behaviour of the MCS-51 microprocessor, which |
---|
155 | increases the program counter directly after fetching, and only then executes |
---|
156 | the branch instruction (by changing the program counter again). |
---|
157 | |
---|
158 | There are also some simple, properties to make sure that our policy |
---|
159 | remains consistent, and to keep track of whether the fixed point has been |
---|
160 | 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 |
---|
161 | iteration does not change with respect to the current one. $added$ is a |
---|
162 | variable that keeps track of the number of bytes we have added to the program |
---|
163 | size by changing the encoding of branch instructions. If $added$ is 0, the program |
---|
164 | has not changed and vice versa. |
---|
165 | |
---|
166 | %{\small |
---|
167 | %\begin{align*} |
---|
168 | %& \mathtt{lookup}\ 0\ (\mathtt{snd}\ strie) = 0 \notag\\ |
---|
169 | %& \mathtt{lookup}\ |prefix|\ (\mathtt{snd}\ strie) = \mathtt{fst}\ strie |
---|
170 | %\end{align*}} |
---|
171 | |
---|
172 | |
---|
173 | %{\small |
---|
174 | %\begin{align*} |
---|
175 | %& added = 0\ \rightarrow\ \mathtt{policy\_pc\_equal}\ prefix\ old\_strie\ strie \notag\\ |
---|
176 | %& \mathtt{policy\_jump\_equal}\ prefix\ old\_strie\ strie\ \rightarrow\ added = 0 |
---|
177 | %\end{align*}} |
---|
178 | |
---|
179 | We need to use two different formulations, because the fact that $added$ is 0 |
---|
180 | does not guarantee that no branch instructions have changed. For instance, |
---|
181 | it is possible that we have replaced a short jump with an absolute jump, which |
---|
182 | 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. |
---|
183 | |
---|
184 | Proving these invariants is simple, usually by induction on the prefix length. |
---|
185 | |
---|
186 | \subsection{Iteration invariants} |
---|
187 | |
---|
188 | These are invariants that hold after the completion of an iteration. The main |
---|
189 | difference between these invariants and the fold invariants is that after the |
---|
190 | completion of the fold, we check whether the program size does not supersede |
---|
191 | 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 |
---|
192 | the program becomes larger than 64 Kb, or $\mathtt{Some}\ \sigma$ |
---|
193 | otherwise. We also no longer pass along the number of bytes added to the |
---|
194 | program size, but a boolean that indicates whether we have changed something |
---|
195 | during the iteration or not. |
---|
196 | |
---|
197 | 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 |
---|
198 | 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. |
---|
199 | |
---|
200 | Instead of using {\tt sigma\_compact\_unsafe}, we can now use the proper |
---|
201 | invariant: |
---|
202 | % |
---|
203 | {\small |
---|
204 | \begin{alignat*}{6} |
---|
205 | \mathtt{sigma} & \omit\rlap{$\mathtt{\_compact} \equiv \lambda program.\lambda sigma.$} \notag\\ |
---|
206 | & \omit\rlap{$\forall n.n < |program|\ \rightarrow$} \notag\\ |
---|
207 | & \mathbf{match}\ && \omit\rlap{$\mathtt{lookup\_opt}\ n\ (\mathtt{snd}\ sigma)\ \mathbf{with}$}\notag\\ |
---|
208 | &&& \omit\rlap{$\mathrm{None}\ \Rightarrow\ \mathrm{False}$}\notag\\ |
---|
209 | &&& \omit\rlap{$\mathrm{Some}\ \langle pc, j \rangle \Rightarrow$}\notag\\ |
---|
210 | &&& \mathbf{match}\ && \mathtt{lookup\_opt}\ (n+1)\ (\mathtt{snd}\ sigma)\ \mathbf{with}\notag\\ |
---|
211 | &&&&& \mathrm{None}\ \Rightarrow\ \mathrm{False}\notag\\ |
---|
212 | &&&&& \mathrm{Some} \langle pc1, j1 \rangle \Rightarrow\notag\\ |
---|
213 | &&&&& \ \ pc1 = pc + \mathtt{instruction\_size}\ n\ (\mathtt{nth}\ n\ program) |
---|
214 | \end{alignat*}} |
---|
215 | % |
---|
216 | This is almost the same invariant as ${\tt sigma\_compact\_unsafe}$, but differs in that it |
---|
217 | computes the sizes of branch instructions by looking at the distance between |
---|
218 | position and destination using $\sigma$. In actual use, the invariant is qualified: $\sigma$ is compact if there have |
---|
219 | been no changes (i.e. the boolean passed along is {\tt true}). This is to |
---|
220 | reflect the fact that we are doing a least fixed point computation: the result |
---|
221 | is only correct when we have reached the fixed point. |
---|
222 | |
---|
223 | There is another, trivial, invariant in case the iteration returns |
---|
224 | $\mathtt{Some}\ \sigma$: it must hold that $\mathtt{fst}\ sigma < 2^{16}$. |
---|
225 | We need this invariant to make sure that addresses do not overflow. |
---|
226 | |
---|
227 | The proof of {\tt nec\_plus\_ultra} goes as follows: if we return {\tt None}, |
---|
228 | then the program size must be greater than 64 Kb. However, since the |
---|
229 | previous iteration did not return {\tt None} (because otherwise we would |
---|
230 | terminate immediately), the program size in the previous iteration must have |
---|
231 | been smaller than 64 Kb. |
---|
232 | |
---|
233 | Suppose that all the branch instructions in the previous iteration are |
---|
234 | encoded as long jumps. This means that all branch instructions in this |
---|
235 | iteration are long jumps as well, and therefore that both iterations are equal |
---|
236 | in the encoding of their branch instructions. Per the invariant, this means that |
---|
237 | $added = 0$, and therefore that all addresses in both iterations are equal. |
---|
238 | But if all addresses are equal, the program sizes must be equal too, which |
---|
239 | means that the program size in the current iteration must be smaller than |
---|
240 | 64 Kb. This contradicts the earlier hypothesis, hence not all branch |
---|
241 | instructions in the previous iteration are encoded as long jumps. |
---|
242 | |
---|
243 | The proof of {\tt sigma\_compact} follows from {\tt sigma\_compact\_unsafe} and |
---|
244 | the fact that we have reached a fixed point, i.e. the previous iteration and |
---|
245 | the current iteration are the same. This means that the results of |
---|
246 | {\tt instruction\_size\_jmplen} and {\tt instruction\_size} are the same. |
---|
247 | |
---|
248 | \subsection{Final properties} |
---|
249 | |
---|
250 | These are the invariants that hold after $2n$ iterations, where $n$ is the |
---|
251 | program size (we use the program size for convenience; we could also use the |
---|
252 | number of branch instructions, but this is more complex). Here, we only |
---|
253 | need {\tt out\_of\_program\_none}, {\tt sigma\_compact} and the fact that |
---|
254 | $\sigma(0) = 0$. |
---|
255 | |
---|
256 | Termination can now be proved using the fact that there is a $k \leq 2n$, with |
---|
257 | $n$ the length of the program, such that iteration $k$ is equal to iteration |
---|
258 | $k+1$. There are two possibilities: either there is a $k < 2n$ such that this |
---|
259 | property holds, or every iteration up to $2n$ is different. In the latter case, |
---|
260 | since the only changes between the iterations can be from shorter jumps to |
---|
261 | longer jumps, in iteration $2n$ every branch instruction must be encoded as |
---|
262 | a long jump. In this case, iteration $2n$ is equal to iteration $2n+1$ and the |
---|
263 | fixed point is reached. |
---|