1 | \documentclass[a4paper, 10pt]{article} |
---|
2 | |
---|
3 | \usepackage{a4wide} |
---|
4 | \usepackage{amsfonts} |
---|
5 | \usepackage{amsmath} |
---|
6 | \usepackage{amssymb} |
---|
7 | \usepackage[english]{babel} |
---|
8 | \usepackage{color} |
---|
9 | \usepackage{diagrams} |
---|
10 | \usepackage{graphicx} |
---|
11 | \usepackage[colorlinks]{hyperref} |
---|
12 | \usepackage[utf8x]{inputenc} |
---|
13 | \usepackage{listings} |
---|
14 | \usepackage{microtype} |
---|
15 | \usepackage{skull} |
---|
16 | \usepackage{stmaryrd} |
---|
17 | \usepackage{wasysym} |
---|
18 | |
---|
19 | \lstdefinelanguage{matita-ocaml} { |
---|
20 | mathescape=true |
---|
21 | } |
---|
22 | \lstset{ |
---|
23 | language=matita-ocaml,basicstyle=\tt,columns=flexible,breaklines=false, |
---|
24 | showspaces=false, showstringspaces=false, extendedchars=false, |
---|
25 | inputencoding=utf8x, tabsize=2 |
---|
26 | } |
---|
27 | |
---|
28 | \title{Proof outline for the correctness of the CerCo compiler} |
---|
29 | \date{\today} |
---|
30 | \author{The CerCo team} |
---|
31 | |
---|
32 | \begin{document} |
---|
33 | |
---|
34 | \maketitle |
---|
35 | |
---|
36 | \section{Introduction} |
---|
37 | \label{sect.introduction} |
---|
38 | |
---|
39 | In the last project review of the CerCo project, the project reviewers expressed the opinion that it would be a good idea to attempt to write down some of the statements of the correctness theorems that we intend to prove about the complexity preserving compiler. |
---|
40 | This document provides a very high-level, pen-and-paper sketch of what we view as the best path to completing the correctness proof for the compiler. |
---|
41 | In particular, for every translation between two intermediate languages, in both the front- and back-ends, we identify the key translation steps, and identify some invariants that we view as being important for the correctness proof. |
---|
42 | |
---|
43 | \section{Front-end: Clight to RTLabs} |
---|
44 | |
---|
45 | The front-end of the CerCo compiler consists of several stages: |
---|
46 | |
---|
47 | \begin{center} |
---|
48 | \begin{minipage}{.8\linewidth} |
---|
49 | \begin{tabbing} |
---|
50 | \quad \= $\downarrow$ \quad \= \kill |
---|
51 | \textsf{Clight}\\ |
---|
52 | \> $\downarrow$ \> cast removal\\ |
---|
53 | \> $\downarrow$ \> add runtime functions\footnote{Following the last project |
---|
54 | meeting we intend to move this transformation to the back-end}\\ |
---|
55 | \> $\downarrow$ \> cost labelling\\ |
---|
56 | \> $\downarrow$ \> loop optimizations\footnote{\label{lab:opt2}To be ported from the untrusted compiler and certified only in case of early completion of the certification of the other passes.} (an endo-transformation)\\ |
---|
57 | \> $\downarrow$ \> partial redundancy elimination$^{\mbox{\scriptsize \ref{lab:opt2}}}$ (an endo-transformation)\\ |
---|
58 | \> $\downarrow$ \> stack variable allocation and control structure |
---|
59 | simplification\\ |
---|
60 | \textsf{Cminor}\\ |
---|
61 | \> $\downarrow$ \> generate global variable initialisation code\\ |
---|
62 | \> $\downarrow$ \> transform to RTL graph\\ |
---|
63 | \textsf{RTLabs}\\ |
---|
64 | \> $\downarrow$ \> \\ |
---|
65 | \>\,\vdots |
---|
66 | \end{tabbing} |
---|
67 | \end{minipage} |
---|
68 | \end{center} |
---|
69 | |
---|
70 | Here, by `endo-transformation', we mean a mapping from language back to itself: |
---|
71 | the loop optimization step maps the Clight language to itself. |
---|
72 | |
---|
73 | %Our overall statements of correctness with respect to costs will |
---|
74 | %require a correctly labelled program |
---|
75 | There are three layers in most of the proofs proposed: |
---|
76 | \begin{enumerate} |
---|
77 | \item invariants closely tied to the syntax and transformations using |
---|
78 | dependent types, |
---|
79 | \item a forward simulation proof, and |
---|
80 | \item syntactic proofs about the cost labelling. |
---|
81 | \end{enumerate} |
---|
82 | The first will support both function correctness and allow us to show |
---|
83 | the totality of some of the compiler stages (that is, these stages of |
---|
84 | the compiler cannot fail). The second provides the main functional |
---|
85 | correctness result, and the last will be crucial for applying |
---|
86 | correctness results about the costings from the back-end. |
---|
87 | |
---|
88 | We will also prove that a suitably labelled RTLabs trace can be turned |
---|
89 | into a \emph{structured trace} which splits the execution trace into |
---|
90 | cost-label-to-cost-label chunks with nested function calls. This |
---|
91 | structure was identified during work on the correctness of the |
---|
92 | back-end cost analysis as retaining important information about the |
---|
93 | structure of the execution that is difficult to reconstruct later in |
---|
94 | the compiler. |
---|
95 | |
---|
96 | \subsection{Clight Cast removal} |
---|
97 | |
---|
98 | This removes some casts inserted by the parser to make arithmetic |
---|
99 | promotion explicit when they are superfluous (such as |
---|
100 | \lstinline[language=C]'c = (short)((int)a + (int)b);'). |
---|
101 | |
---|
102 | The transformation only affects Clight expressions, recursively |
---|
103 | detecting casts that can be safely eliminated. The semantics provides |
---|
104 | a big-step definition for expression, so we should be able to show a |
---|
105 | lock-step forward simulation using a lemma showing that cast |
---|
106 | elimination does not change the evaluation of expressions. This lemma |
---|
107 | will follow from a structural induction on the source expression. We |
---|
108 | have already proved a few of the underlying arithmetic results |
---|
109 | necessary to validate the approach. |
---|
110 | |
---|
111 | \subsection{Clight cost labelling} |
---|
112 | |
---|
113 | This adds cost labels before and after selected statements and |
---|
114 | expressions, and the execution traces ought to be equivalent modulo |
---|
115 | cost labels. Hence it requires a simple forward simulation with a |
---|
116 | limited amount of stuttering whereever a new cost label is introduced. |
---|
117 | A bound can be given for the amount of stuttering allowed can be given |
---|
118 | based on the statement or continuation to be evaluated next. |
---|
119 | |
---|
120 | We also intend to show three syntactic properties about the cost |
---|
121 | labelling: |
---|
122 | \begin{itemize} |
---|
123 | \item every function starts with a cost label, |
---|
124 | \item every branching instruction is followed by a label (note that |
---|
125 | exiting a loop is treated as a branch), and |
---|
126 | \item the head of every loop (and any \lstinline'goto' destination) is |
---|
127 | a cost label. |
---|
128 | \end{itemize} |
---|
129 | These can be shown by structural induction on the source term. |
---|
130 | |
---|
131 | \subsection{Clight to Cminor translation} |
---|
132 | |
---|
133 | This translation is the first to introduce some invariants, with the |
---|
134 | proofs closely tied to the implementation by dependent typing. These |
---|
135 | are largely complete and show that the generated code enjoys: |
---|
136 | \begin{itemize} |
---|
137 | \item some minimal type safety shown by explicit checks on the |
---|
138 | Cminor types during the transformation (a little more work remains |
---|
139 | to be done here, but follows the same form); |
---|
140 | \item that variables named in the parameter and local variable |
---|
141 | environments are distinct from one another, again by an explicit |
---|
142 | check; |
---|
143 | \item that variables used in the generated code are present in the |
---|
144 | resulting environment (either by checking their presence in the |
---|
145 | source environment, or from a list of freshly temporary variables); |
---|
146 | and |
---|
147 | \item that all \lstinline[language=C]'goto' labels are present (by |
---|
148 | checking them against a list of source labels and proving that all |
---|
149 | source labels are preserved). |
---|
150 | \end{itemize} |
---|
151 | |
---|
152 | The simulation will be similar to the relevant stages of CompCert |
---|
153 | (Clight to Csharpminor and Csharpminor to Cminor --- in the event that |
---|
154 | the direct proof is unwieldy we could introduce a corresponding |
---|
155 | intermediate language). During early experimentation with porting |
---|
156 | CompCert definitions to the Matita proof assistant we found little |
---|
157 | difficulty reproving the results for the memory model, so we plan to |
---|
158 | port the memory injection properties and use them to relate Clight |
---|
159 | in-memory variables with either a local variable valuation or a stack |
---|
160 | slot, depending on how it was classified. |
---|
161 | |
---|
162 | This should be sufficient to show the equivalence of (big-step) |
---|
163 | expression evaluation. The simulation can then be shown by relating |
---|
164 | corresponding blocks of statement and continuations with their Cminor |
---|
165 | counterparts and proving that a few steps reaches the next matching |
---|
166 | state. |
---|
167 | |
---|
168 | The syntactic properties required for cost labels remain similar and a |
---|
169 | structural induction on the function bodies should be sufficient to |
---|
170 | show that they are preserved. |
---|
171 | |
---|
172 | \subsection{Cminor global initialisation code} |
---|
173 | |
---|
174 | This short phase replaces the global variable initialisation data with |
---|
175 | code that executes when the program starts. Each piece of |
---|
176 | initialisation data in the source is matched by a new statement |
---|
177 | storing that data. As each global variable is allocated a distinct |
---|
178 | memory block, the program state after the initialisation statements |
---|
179 | will be the same as the original program's state at the start of |
---|
180 | execution, and will proceed in the same manner afterwards. |
---|
181 | |
---|
182 | % Actually, the above is wrong... |
---|
183 | % ... this ought to be in a fresh main function with a fresh cost label |
---|
184 | |
---|
185 | \subsection{Cminor to RTLabs translation} |
---|
186 | |
---|
187 | In this part of the compiler we transform the program's functions into |
---|
188 | control flow graphs. It is closely related to CompCert's Cminorsel to |
---|
189 | RTL transformation, albeit with target-independent operations. |
---|
190 | |
---|
191 | We already enforce several invariants with dependent types: some type |
---|
192 | safety is enforced mostly using the type information from Cminor; and |
---|
193 | that the graph is closed (by showing that each successor was recently |
---|
194 | added, or corresponds to a \lstinline[language=C]'goto' label which |
---|
195 | are all added before the end). Note that this relies on a |
---|
196 | monotonicity property; CompCert maintains a similar property in a |
---|
197 | similar way while building RTL graphs. We will also add a result |
---|
198 | showing that all of the pseudo-register names are distinct for use by |
---|
199 | later stages using the same method as Cminor. |
---|
200 | |
---|
201 | The simulation will relate Cminor states to RTLabs states about to |
---|
202 | execute the corresponding code (with a corresponding continuation). |
---|
203 | Each Cminor statement becomes zero or more RTLabs statements, with a |
---|
204 | decreasing measure based on the statement and continuations similar to |
---|
205 | CompCert's. We may also follow CompCert in using a relational |
---|
206 | specification of this stage so as to abstract away from the functional |
---|
207 | (and highly dependently typed) definition. |
---|
208 | |
---|
209 | The first two labelling properties remain as before; we will show that |
---|
210 | cost labels are preserved, so the function entry point will be a cost |
---|
211 | label, and successors that are cost labels map still map to cost |
---|
212 | labels, preserving the condition on branches. We replace the property |
---|
213 | for loops with the notion that we will always reach a cost label or |
---|
214 | the end of the function by following a bounded number of successors. |
---|
215 | This can be easily seen in Cminor using the requirement for cost |
---|
216 | labels at the head of loops and after gotos. It remains to show that |
---|
217 | this is preserved by the translation to RTLabs. % how? |
---|
218 | |
---|
219 | \subsection{RTLabs structured trace generation} |
---|
220 | |
---|
221 | This proof-only step incorporates the function call structure and cost |
---|
222 | labelling properties into the execution trace. As the function calls |
---|
223 | are nested within the trace, we need to distinguish between |
---|
224 | terminating and non-terminating function calls. |
---|
225 | |
---|
226 | Thus we use the excluded middle (specialised to a function termination |
---|
227 | property) to do this. Terminating functions are built by following |
---|
228 | the trace, breaking it into chunks between cost labels and recursively |
---|
229 | processing function calls. The main difficulties here are the |
---|
230 | non-structurally recursive nature of the function (instead we use the |
---|
231 | size of the termination proof as a measure) and using the properties |
---|
232 | on RTLabs cost labelling to create the correct structure. We also |
---|
233 | show that the lower stack frames are preserved during function calls |
---|
234 | in order to prove that after returning from a function call we execute |
---|
235 | the correct code. This part of the work has already been constructed, |
---|
236 | but still requires a simple proof to show that flattening the structured |
---|
237 | trace recreates the original flat trace. |
---|
238 | |
---|
239 | The non-terminating case uses the excluded middle to decide whether to |
---|
240 | use the function described above to construct an inductive terminating |
---|
241 | structured trace, or a coinductive version for non-termination. It |
---|
242 | follows the trace like the terminating version to build up chunks of |
---|
243 | trace from cost-label to cost-label (which, by the finite distance to |
---|
244 | a cost label property shown before, can be represented by an inductive |
---|
245 | type), unless it encounters a non-terminating function in which case |
---|
246 | it corecursively processes that. This part of the trace |
---|
247 | transformation is currently under construction, and will also need a |
---|
248 | flattening result to show that it is correct. |
---|
249 | |
---|
250 | \section{Backend: RTLabs to machine code} |
---|
251 | \label{sect.backend.rtlabs.machine.code} |
---|
252 | |
---|
253 | The compiler backend consists of the following intermediate languages, and stages of translation: |
---|
254 | |
---|
255 | \begin{center} |
---|
256 | \begin{minipage}{.8\linewidth} |
---|
257 | \begin{tabbing} |
---|
258 | \quad \=\,\vdots\= \\ |
---|
259 | \> $\downarrow$ \>\\ |
---|
260 | \> $\downarrow$ \quad \= \kill |
---|
261 | \textsf{RTLabs}\\ |
---|
262 | \> $\downarrow$ \> copy propagation\footnote{\label{lab:opt}To be ported from the untrusted compiler and certified only in case of early completion of the certification of the other passes.} (an endo-transformation) \\ |
---|
263 | \> $\downarrow$ \> instruction selection\\ |
---|
264 | \textsf{RTL}\\ |
---|
265 | \> $\downarrow$ \> constant propagation$^{\mbox{\scriptsize \ref{lab:opt}}}$ (an endo-transformation) \\ |
---|
266 | \> $\downarrow$ \> calling convention made explicit \\ |
---|
267 | \> $\downarrow$ \> layout of activation records \\ |
---|
268 | \textsf{ERTL}\\ |
---|
269 | \> $\downarrow$ \> register allocation and spilling\\ |
---|
270 | \> $\downarrow$ \> dead code elimination\\ |
---|
271 | \textsf{LTL}\\ |
---|
272 | \> $\downarrow$ \> function linearisation\\ |
---|
273 | \> $\downarrow$ \> branch compression (an endo-transformation) \\ |
---|
274 | \textsf{LIN}\\ |
---|
275 | \> $\downarrow$ \> relabeling\\ |
---|
276 | \textsf{ASM}\\ |
---|
277 | \> $\downarrow$ \> pseudoinstruction expansion\\ |
---|
278 | \textsf{MCS-51 machine code}\\ |
---|
279 | \end{tabbing} |
---|
280 | \end{minipage} |
---|
281 | \end{center} |
---|
282 | |
---|
283 | \subsection{The RTLabs to RTL translation} |
---|
284 | \label{subsect.rtlabs.rtl.translation} |
---|
285 | |
---|
286 | % dpm: type system and casting load (???) |
---|
287 | We require a map, $\sigma$, between \texttt{Values} of the front-end memory model to lists of \texttt{BEValues} of the back-end memory model: |
---|
288 | |
---|
289 | \begin{displaymath} |
---|
290 | \mathtt{Value} ::= \bot \mid \mathtt{int(size)} \mid \mathtt{float} \mid \mathtt{null} \mid \mathtt{ptr} \quad\stackrel{\sigma}{\longrightarrow}\quad \mathtt{BEValue} ::= \bot \mid \mathtt{byte} \mid \mathtt{int}_i \mid \mathtt{ptr}_i |
---|
291 | \end{displaymath} |
---|
292 | |
---|
293 | We further require a map, $\sigma$, which maps the front-end \texttt{Memory} and the back-end's notion of \texttt{BEMemory}. |
---|
294 | |
---|
295 | \begin{displaymath} |
---|
296 | \mathtt{Mem}\ \alpha = \mathtt{Block} \rightarrow (\mathbb{Z} \rightarrow \alpha) |
---|
297 | \end{displaymath} |
---|
298 | |
---|
299 | where |
---|
300 | |
---|
301 | \begin{displaymath} |
---|
302 | \mathtt{Block} ::= \mathtt{Region} \cup \mathtt{ID} |
---|
303 | \end{displaymath} |
---|
304 | |
---|
305 | \begin{displaymath} |
---|
306 | \mathtt{BEMem} = \mathtt{Mem} \mathtt{Value} |
---|
307 | \end{displaymath} |
---|
308 | |
---|
309 | \begin{displaymath} |
---|
310 | \mathtt{Address} = \mathtt{BEValue} \times \mathtt{BEValue} \\ |
---|
311 | \end{displaymath} |
---|
312 | |
---|
313 | \begin{displaymath} |
---|
314 | \mathtt{Mem} = \mathtt{Block} \rightarrow (\mathbb{Z} \rightarrow \mathtt{Cont} \mid \mathtt{Value} \times \mathtt{Size} \mid \mathtt{null}) |
---|
315 | \end{displaymath} |
---|
316 | |
---|
317 | \begin{center} |
---|
318 | \begin{picture}(2, 2) |
---|
319 | \put(0,-20){\framebox(25,25)[c]{\texttt{v}}} |
---|
320 | \put(26,-20){\framebox(25,25)[c]{\texttt{4}}} |
---|
321 | \put(51,-20){\framebox(25,25)[c]{\texttt{cont}}} |
---|
322 | \put(76,-20){\framebox(25,25)[c]{\texttt{cont}}} |
---|
323 | \put(101,-20){\framebox(25,25)[c]{\texttt{cont}}} |
---|
324 | \end{picture} |
---|
325 | \end{center} |
---|
326 | |
---|
327 | \begin{displaymath} |
---|
328 | \mathtt{load}\ s\ a\ M = \mathtt{Some}\ v \rightarrow \forall i \leq s.\ \mathtt{load}\ s\ (a + i)\ \sigma(M) = \mathtt{Some}\ v_i |
---|
329 | \end{displaymath} |
---|
330 | |
---|
331 | \begin{displaymath} |
---|
332 | \sigma(\mathtt{store}\ v\ M) = \mathtt{store}\ \sigma(v)\ \sigma(M) |
---|
333 | \end{displaymath} |
---|
334 | |
---|
335 | \begin{displaymath} |
---|
336 | \begin{array}{rll} |
---|
337 | \mathtt{State} & ::= & (\mathtt{State} : \mathtt{Frame}^* \times \mathtt{Frame} \\ |
---|
338 | & \mid & \mathtt{Call} : \mathtt{Frame}^* \times \mathtt{Args} \times \mathtt{Return} \times \mathtt{Fun} \\ |
---|
339 | & \mid & \mathtt{Return} : \mathtt{Frame}^* \times \mathtt{Value} \times \mathtt{Return}) \times \mathtt{Mem} |
---|
340 | \end{array} |
---|
341 | \end{displaymath} |
---|
342 | |
---|
343 | \begin{displaymath} |
---|
344 | \mathtt{State} ::= \mathtt{Frame}^* \times \mathtt{PC} \times \mathtt{SP} \times \mathtt{ISP} \times \mathtt{CARRY} \times \mathtt{REGS} |
---|
345 | \end{displaymath} |
---|
346 | |
---|
347 | \begin{displaymath} |
---|
348 | \mathtt{State} \stackrel{\sigma}{\longrightarrow} \mathtt{State} |
---|
349 | \end{displaymath} |
---|
350 | |
---|
351 | \begin{displaymath} |
---|
352 | \sigma(\mathtt{State} (\mathtt{Frame}^* \times \mathtt{Frame})) \longrightarrow ((\sigma(\mathtt{Frame}^*), \sigma(\mathtt{PC}), \sigma(\mathtt{SP}), 0, 0, \sigma(\mathtt{REGS})), \sigma(\mathtt{Mem})) |
---|
353 | \end{displaymath} |
---|
354 | |
---|
355 | \begin{displaymath} |
---|
356 | \sigma(\mathtt{Return}(-)) \longrightarrow \sigma \circ \text{return one step} |
---|
357 | \end{displaymath} |
---|
358 | |
---|
359 | \begin{displaymath} |
---|
360 | \sigma(\mathtt{Call}(-)) \longrightarrow \sigma \circ \text{call one step} |
---|
361 | \end{displaymath} |
---|
362 | |
---|
363 | Return one step commuting diagram: |
---|
364 | |
---|
365 | \begin{displaymath} |
---|
366 | \begin{diagram} |
---|
367 | s & \rTo^{\text{one step of execution}} & s' \\ |
---|
368 | & \rdTo & \dTo \\ |
---|
369 | & & \llbracket s'' \rrbracket |
---|
370 | \end{diagram} |
---|
371 | \end{displaymath} |
---|
372 | |
---|
373 | Call one step commuting diagram: |
---|
374 | |
---|
375 | \begin{displaymath} |
---|
376 | \begin{diagram} |
---|
377 | s & \rTo^{\text{one step of execution}} & s' \\ |
---|
378 | & \rdTo & \dTo \\ |
---|
379 | & & \llbracket s'' \rrbracket |
---|
380 | \end{diagram} |
---|
381 | \end{displaymath} |
---|
382 | |
---|
383 | \begin{displaymath} |
---|
384 | \begin{diagram} |
---|
385 | \mathtt{CALL}(\mathtt{id},\ \mathtt{args},\ \mathtt{dst},\ \mathtt{pc}),\ \mathtt{State}(\mathtt{Frame},\ \mathtt{Frames}) & \rTo & \mathtt{Call}(FINISH ME) |
---|
386 | \end{diagram} |
---|
387 | \end{displaymath} |
---|
388 | |
---|
389 | \begin{displaymath} |
---|
390 | \begin{array}{rcl} |
---|
391 | \mathtt{CALL}(\mathtt{id}, \mathtt{args}, \mathtt{dst}, \mathtt{pc}) & \longrightarrow & \mathtt{CALL\_ID}(\mathtt{id}, \sigma'(\mathtt{args}), \sigma(\mathtt{dst}), \mathtt{pc}) \\ |
---|
392 | \mathtt{RETURN} & \longrightarrow & \mathtt{RETURN} \\ |
---|
393 | \end{array} |
---|
394 | \end{displaymath} |
---|
395 | |
---|
396 | \begin{displaymath} |
---|
397 | \begin{array}{rcl} |
---|
398 | \sigma & : & \mathtt{register} \rightarrow \mathtt{list\ register} \\ |
---|
399 | \sigma' & : & \mathtt{list\ register} \rightarrow \mathtt{list\ register} |
---|
400 | \end{array} |
---|
401 | \end{displaymath} |
---|
402 | |
---|
403 | \subsection{The RTL to ERTL translation} |
---|
404 | \label{subsect.rtl.ertl.translation} |
---|
405 | |
---|
406 | \begin{displaymath} |
---|
407 | \begin{diagram} |
---|
408 | & & \llbracket \mathtt{CALL\_ID}(\mathtt{id}, \mathtt{args}, \mathtt{dst}, \mathtt{pc})\rrbracket & & \\ |
---|
409 | & \ldTo^{\text{external}} & & \rdTo^{\text{internal}} & \\ |
---|
410 | \skull & & & & \mathtt{regs} = [\mathtt{params}/-] \\ |
---|
411 | & & & & \mathtt{sp} = \mathtt{ALLOC} \\ |
---|
412 | & & & & \mathtt{PUSH}(\mathtt{carry}, \mathtt{regs}, \mathtt{dst}, \mathtt{return\_addr}), \mathtt{pc}_{0}, \mathtt{regs}, \mathtt{sp} \\ |
---|
413 | \end{diagram} |
---|
414 | \end{displaymath} |
---|
415 | |
---|
416 | \begin{align*} |
---|
417 | \llbracket \mathtt{RETURN} \rrbracket \\ |
---|
418 | \mathtt{return\_addr} & := \mathtt{top}(\mathtt{stack}) \\ |
---|
419 | v* & := m(\mathtt{rv\_regs}) \\ |
---|
420 | \mathtt{dst}, \mathtt{sp}, \mathtt{carry}, \mathtt{regs} & := \mathtt{pop} \\ |
---|
421 | \mathtt{regs}[v* / \mathtt{dst}] \\ |
---|
422 | \end{align*} |
---|
423 | |
---|
424 | \begin{displaymath} |
---|
425 | \begin{diagram} |
---|
426 | s & \rTo^1 & s' & \rTo^1 & s'' \\ |
---|
427 | \dTo & & & \rdTo & \dTo \\ |
---|
428 | \llbracket s \rrbracket & \rTo(1,3)^1 & & & \llbracket s'' \rrbracket \\ |
---|
429 | \mathtt{CALL} \\ |
---|
430 | \end{diagram} |
---|
431 | \end{displaymath} |
---|
432 | |
---|
433 | \begin{displaymath} |
---|
434 | \begin{diagram} |
---|
435 | s & \rTo^1 & s' & \rTo^1 & s'' \\ |
---|
436 | \dTo & & & \rdTo & \dTo \\ |
---|
437 | \ & \rTo(1,3) & & & \ \\ |
---|
438 | \mathtt{RETURN} \\ |
---|
439 | \end{diagram} |
---|
440 | \end{displaymath} |
---|
441 | |
---|
442 | \begin{displaymath} |
---|
443 | \mathtt{b\_graph\_translate}: (\mathtt{label} \rightarrow \mathtt{blist'}) |
---|
444 | \rightarrow \mathtt{graph} \rightarrow \mathtt{graph} |
---|
445 | \end{displaymath} |
---|
446 | |
---|
447 | \begin{align*} |
---|
448 | \mathtt{theorem} &\ \mathtt{b\_graph\_translate\_ok}: \\ |
---|
449 | & \forall f.\forall G_{i}.\mathtt{let}\ G_{\sigma} := \mathtt{b\_graph\_translate}\ f\ G_{i}\ \mathtt{in} \\ |
---|
450 | & \forall l \in G_{i}.\mathtt{subgraph}\ (f\ l)\ l\ (\mathtt{next}\ l\ G_{i})\ G_{\sigma} |
---|
451 | \end{align*} |
---|
452 | |
---|
453 | \begin{align*} |
---|
454 | \mathtt{lemma} &\ \mathtt{execute\_1\_step\_ok}: \\ |
---|
455 | & \forall s. \mathtt{let}\ s' := s\ \sigma\ \mathtt{in} \\ |
---|
456 | & \mathtt{let}\ l := pc\ s\ \mathtt{in} \\ |
---|
457 | & s \stackrel{1}{\rightarrow} s^{*} \Rightarrow \exists n. s' \stackrel{n}{\rightarrow} s'^{*} \wedge s'^{*} = s'\ \sigma |
---|
458 | \end{align*} |
---|
459 | |
---|
460 | \begin{align*} |
---|
461 | \mathrm{RTL\ status} & \ \ \mathrm{ERTL\ status} \\ |
---|
462 | \mathtt{sp} & = \mathtt{spl} / \mathtt{sph} \\ |
---|
463 | \mathtt{graph} & \mapsto \mathtt{graph} + \mathtt{prologue}(s) + \mathtt{epilogue}(s) \\ |
---|
464 | & \mathrm{where}\ s = \mathrm{callee\ saved} + \nu \mathrm{RA} \\ |
---|
465 | \end{align*} |
---|
466 | |
---|
467 | \begin{displaymath} |
---|
468 | \begin{diagram} |
---|
469 | \mathtt{CALL} & \rTo^1 & \mathtt{inside\ function} \\ |
---|
470 | \dTo & & \dTo \\ |
---|
471 | \underbrace{\ldots}_{\llbracket \mathtt{CALL} \rrbracket} & \rTo & |
---|
472 | \underbrace{\ldots}_{\mathtt{prologue}} \\ |
---|
473 | \end{diagram} |
---|
474 | \end{displaymath} |
---|
475 | |
---|
476 | \begin{displaymath} |
---|
477 | \begin{diagram} |
---|
478 | \mathtt{RETURN} & \rTo^1 & \mathtt{.} \\ |
---|
479 | \dTo & & \dTo \\ |
---|
480 | \underbrace{\ldots}_{\mathtt{epilogue}} & \rTo & |
---|
481 | \underbrace{\ldots} \\ |
---|
482 | \end{diagram} |
---|
483 | \end{displaymath} |
---|
484 | |
---|
485 | \begin{align*} |
---|
486 | \mathtt{prologue}(s) = & \mathtt{create\_new\_frame}; \\ |
---|
487 | & \mathtt{pop\ ra}; \\ |
---|
488 | & \mathtt{save\ callee\_saved}; \\ |
---|
489 | & \mathtt{get\_params} \\ |
---|
490 | & \ \ \mathtt{reg\_params}: \mathtt{move} \\ |
---|
491 | & \ \ \mathtt{stack\_params}: \mathtt{push}/\mathtt{pop}/\mathtt{move} \\ |
---|
492 | \end{align*} |
---|
493 | |
---|
494 | \begin{align*} |
---|
495 | \mathtt{epilogue}(s) = & \mathtt{save\ return\ to\ tmp\ real\ regs}; \\ |
---|
496 | & \mathtt{restore\_registers}; \\ |
---|
497 | & \mathtt{push\ ra}; \\ |
---|
498 | & \mathtt{delete\_frame}; \\ |
---|
499 | & \mathtt{save return} \\ |
---|
500 | \end{align*} |
---|
501 | |
---|
502 | \begin{displaymath} |
---|
503 | \mathtt{CALL}\ id \mapsto \mathtt{set\_params};\ \mathtt{CALL}\ id;\ \mathtt{fetch\_result} |
---|
504 | \end{displaymath} |
---|
505 | |
---|
506 | \subsection{The ERTL to LTL translation} |
---|
507 | \label{subsect.ertl.ltl.translation} |
---|
508 | |
---|
509 | \subsection{The LTL to LIN translation} |
---|
510 | \label{subsect.ltl.lin.translation} |
---|
511 | |
---|
512 | We require a map, $\sigma$, from LTL statuses, where program counters are represented as labels in a graph data structure, to LIN statuses, where program counters are natural numbers: |
---|
513 | \begin{displaymath} |
---|
514 | \mathtt{pc : label} \stackrel{\sigma}{\longrightarrow} \mathbb{N} |
---|
515 | \end{displaymath} |
---|
516 | |
---|
517 | The LTL to LIN translation pass also linearises the graph data structure into a list of instructions. |
---|
518 | Pseudocode for the linearisation process is as follows: |
---|
519 | |
---|
520 | \begin{lstlisting} |
---|
521 | let rec linearise graph visited required generated todo := |
---|
522 | match todo with |
---|
523 | | l::todo -> |
---|
524 | if l $\in$ visited then |
---|
525 | let generated := generated $\cup\ \{$ Goto l $\}$ in |
---|
526 | let required := required $\cup$ l in |
---|
527 | linearise graph visited required generated todo |
---|
528 | else |
---|
529 | -- Get the instruction at label `l' in the graph |
---|
530 | let lookup := graph(l) in |
---|
531 | let generated := generated $\cup\ \{$ lookup $\}$ in |
---|
532 | -- Find the successor of the instruction at label `l' in the graph |
---|
533 | let successor := succ(l, graph) in |
---|
534 | let todo := successor::todo in |
---|
535 | linearise graph visited required generated todo |
---|
536 | | [] -> (required, generated) |
---|
537 | \end{lstlisting} |
---|
538 | |
---|
539 | It is easy to see that this linearisation process eventually terminates. |
---|
540 | In particular, the size of the visited label set is monotonically increasing, and is bounded above by the size of the graph that we are linearising. |
---|
541 | |
---|
542 | The initial call to \texttt{linearise} sees the \texttt{visited}, \texttt{required} and \texttt{generated} sets set to the empty set, and \texttt{todo} initialized with the singleton list consisting of the entry point of the graph. |
---|
543 | We envisage needing to prove the following invariants on the linearisation function above: |
---|
544 | |
---|
545 | \begin{enumerate} |
---|
546 | \item |
---|
547 | $\mathtt{visited} \approx \mathtt{generated}$, where $\approx$ is \emph{multiset} equality, as \texttt{generated} is a set of instructions where instructions may mention labels multiple times, and \texttt{visited} is a set of labels, |
---|
548 | \item |
---|
549 | $\forall \mathtt{l} \in \mathtt{generated}.\ \mathtt{succ(l,\ graph)} \subseteq \mathtt{required} \cup \mathtt{todo}$, |
---|
550 | \item |
---|
551 | $\mathtt{required} \subseteq \mathtt{visited}$, |
---|
552 | \item |
---|
553 | $\mathtt{visited} \cap \mathtt{todo} = \emptyset$. |
---|
554 | \end{enumerate} |
---|
555 | |
---|
556 | The invariants collectively imply the following properties, crucial to correctness, about the linearisation process: |
---|
557 | |
---|
558 | \begin{enumerate} |
---|
559 | \item |
---|
560 | Every graph node is visited at most once, |
---|
561 | \item |
---|
562 | Every instruction that is generated is generated due to some graph node being visited, |
---|
563 | \item |
---|
564 | The successor instruction of every instruction that has been visited already will eventually be visited too. |
---|
565 | \end{enumerate} |
---|
566 | |
---|
567 | Note, because the LTL to LIN transformation is the first time the program is linearised, we must discover a notion of `well formed program' suitable for linearised forms. |
---|
568 | In particular, we see the notion of well formedness (yet to be formally defined) resting on the following conditions: |
---|
569 | |
---|
570 | \begin{enumerate} |
---|
571 | \item |
---|
572 | For every jump to a label in a linearised program, the target label exists at some point in the program, |
---|
573 | \item |
---|
574 | Each label is unique, appearing only once in the program, |
---|
575 | \item |
---|
576 | The final instruction of a program must be a return. |
---|
577 | \end{enumerate} |
---|
578 | |
---|
579 | We assume that these properties will be easy consequences of the invariants on the linearisation function defined above. |
---|
580 | |
---|
581 | The final condition above is potentially a little opaque, so we explain further. |
---|
582 | First, the only instructions that can reasonably appear in final position at the end of a program are returns or backward jumps, as any other instruction would cause execution to `fall out' of the end of the program (for example, when a function invoked with \texttt{CALL} returns, it returns to the next instruction past the \texttt{CALL} that invoked it). |
---|
583 | However, in LIN, though each function's graph has been linearised, the entire program is not yet fully linearised into a list of instructions, but rather, a list of `functions', each consisting of a linearised body along with other data. |
---|
584 | Each well-formed function must end with a call to \texttt{RET}, and therefore the only correct instruction that can terminate a LIN program is a \texttt{RET} instruction. |
---|
585 | |
---|
586 | \subsection{The LIN to ASM and ASM to MCS-51 machine code translations} |
---|
587 | \label{subsect.lin.asm.translation} |
---|
588 | |
---|
589 | The LIN to ASM translation step is trivial, being almost the identity function. |
---|
590 | The only non-trivial feature of the LIN to ASM translation is that all labels are `named apart' so that there is no chance of freshly generated labels from different namespaces clashing with labels from another namespace. |
---|
591 | |
---|
592 | The ASM to MCS-51 machine code translation step, and the required statements of correctness, are found in an unpublished manuscript attached to this document. |
---|
593 | |
---|
594 | \section{Estimated effort} |
---|
595 | Based on the rough analysis performed so far we can now estimate the total |
---|
596 | effort for the certification of the compiler. We obtain the estimation by |
---|
597 | combining, for each pass: 1) the number of lines of code to be certified; |
---|
598 | 2) the ratio number of lines of proof on number of lines of code from |
---|
599 | CompCert project~\cite{compcert} for the CompCert pass that is closer to |
---|
600 | ours; 3) an estimation of the complexity of the pass according to the |
---|
601 | analysis above. |
---|
602 | |
---|
603 | \begin{tabular}{lrll} |
---|
604 | Pass origin & Code lines & CompCert ratio & Estimated effort \\ |
---|
605 | Clight & \\ |
---|
606 | Cminor & \\ |
---|
607 | RTLabs & 1252 & 1.17 \permil & 1.5 \\ |
---|
608 | RTL & 469 & 2.90 \permil & 1.4 \\ |
---|
609 | ERTL & 789 & 2.79 \permil & 2.2 \\ |
---|
610 | LTL & & \\ |
---|
611 | LIN & 354 & 7.34 \permil & 2.6 \\ |
---|
612 | ASM & & \\ |
---|
613 | \end{tabular} |
---|
614 | |
---|
615 | \end{document} |
---|