# source:Papers/jar-cerco-2017/architecture.tex@3663

Last change on this file since 3663 was 3663, checked in by mulligan, 21 months ago

more work on compiler architecture section

File size: 24.0 KB
Line
1\newcommand{\Alt}{ \mid\!\!\mid  }
2
3% CerCo compiler architecture
4%   Description of languages
5%   Target hardware description
6
7\section{Compiler architecture}
8\label{sect.compiler.architecture}
9
10In this section we give an overview of the architecture of the CerCo verified C compiler.
11We discuss the compiler's intermediate languages, the optimisations and other transforms that occur at each intermediate language, and discuss the compiler's target hardware: the MCS-51 8-bit microprocessor.
12
13Many of the intermediate languages used in the CerCo verified C compiler are inspired by analogous languages in the CompCert verified C compiler, and a compiler written by Fran\s{c}ois Pottier---used for teaching compiler construction to undergraduates.
14Where appropriate, we make reference to the source documentation of these two compilers, to explain our intermediate languages.
15
16Note: though many of the compiler intermediate languages (especially in the front end) are shared with CompCert, the architecture of the CerCo compiler is different in quite a substantial way from that of CompCert.
17In particular, the CompCert compiler's backend linearises' its code much earlier, compared to our own.
18Indeed, as explained below, the CerCo compiler works with a control-flow graph based representation of the program almost until producing machine code, only linearising in the translation from LTL to LIN intermediate languages.
19This is merely a design variation in our two compilers, and is not motivated by any real technical issue pertinent to the proof of correctness, or due to the lifting of cost models.
20
21\subsection{Compiler front-end}
22
23The compiler front-end lowers a program written in C to a low-level language of control-flow graphs, ready for the entry-point of our compiler backend.
24In total, there are three intermediate languages in the front-end.
25
26The first translation step of the compiler lowers the full C language to a high-level intermediate language, Clight---this language will be explained further below.
27This translation phase is unverified, using the CIL C parsing utility~\cite{cil02} to handle the intricacies of parsing C.
28We produce a Clight AST directly from a C source file, using this tool.
29As this translation step is unverified we do not expand any further on it here, and only note its existence.
30
31\paragraph{Clight} is a large subset of the C language, developed by the CompCert team for use in the CompCert verified C compiler, that we adopt as the source language of our compiler.
32We refer to~\cite{compcert} for a formal definition of the Clight language.
33
34Briefly, Clight features most of the types and operators of C, and includes pointer arithmetic, pointers to functions, and \texttt{struct} and \texttt{union} types, as well as all of C's control structures.
35The language is classically structured with expressions, statements, functions, and whole programs.
36Clight expressions are side-effect free, which means that side-effect operators ($\texttt{=}$,$\texttt{+=}$,$\texttt{++}$, and so on) and function calls within expressions are not supported.
37This is the key difference between the full C programming language and Clight.
38
39In order to limit the implementation effort of verifying the CerCo compiler, our current compiler for Clight does {\em not} cover the operators relating to the floating point type {\tt float}.
40
41\paragraph{Cminor} is a simple, low-level imperative language, comparable to a stripped-down, typeless variant of C.
42The Cminor intermediate language again is taken directly from the CompCert verified C compiler, and we refer to the CompCert project for its formal definition.
43Like Clight, the Cminor language is structured into expressions, statements, functions, and whole programs.
44Control flow constructs are now presented in a simpler form, compared to Clight.
45In particular, Cminor provides only a single, generic loop' construct, into which the different looping constructs of Clight must be translated.
46Switch statements are also present, but in a semi-explicit jump-table form.
47
48In Cminor, stack operations are made explicit, and one must know which variables are stored on the stack when translating from Clight to Cminor.
49This information is produced by a static analysis that determines the variables whose address may be `taken'.
50When translating from Clight to Cminor, space is reserved for local arrays and structures.
51In a second step, the proper compilation of Clight programs into Cminor programs is performed: consisting mainly of the translation of Clight control structures to the more primitive control-flow constructs available in Cminor.
52
53\paragraph{RTLabs} is the last architecture independent language in the compilation process.
54It is a rather straightforward abstraction of the architecture-dependent RTL intermediate language used in the CompCert project.
55
56RTLabs is intended to ease retargeting of the compiler---should that be desired---by factorising some work common to the various target assembly languages, for example optimisations.
57In RTLAbs the structure of Cminor expressions is lost.
58This may have a negative impact on the instruction selection steps that follow in the compiler backend.
59However, the subtleties of instruction selection seem rather orthogonal to our goals, and we deem the possibility of retargeting easily the compiler more important than the efficiency of the generated code.
60
61In RTLAbs, programs are represented as \emph{control flow graphs}, or CFGs for short.
62We associate with the nodes of the graphs instructions reflecting commands of the Cminor language.
63As usual, commands that change the control flow of the program (e.g. loops, conditionals) are translated by inserting suitable branching instructions in the CFG.
64
65Local variables are now represented by \emph{pseudo registers}.
66The number of available pseudo registers is unbounded.
67Eventually these pseudo registers will be replaced by real (machine) registers or stack slots, in the compiler backend.
68
69Translating Cminor programs to RTLAbs consists of transforming Cminor commands into a CFG form.
70Most commands are sequential and have a rather straightforward linear translation.
71However, a conditional is translated into a branch instruction, whilst a loop is translated using a back-edge in the CFG.
72
73\subsection{Compiler back-end}
74
75\paragraph{RTL} is the first architecture-dependant intermediate language of our compiler, and the entry point of the compiler back end.
76RTL programs are structured as CFGs, like RTLabs.
77
78The syntax of RTL is very close to RTLAbs, but now MCS-51 instructions are made explicit.
79Type information completely disappears: everything is represented using 32-bit words.
80Moreover, each global variable of a program is associated to a fixed offset, as we begin to fix the eventual memory layout of the program in the processor's memory.
81The syntax of the RTL language is provided in Table~\ref{RTL:syntax}.
82Within the grammar $\textit{unop}$, $\textit{binop}$, $\textit{uncon}$, and $\textit{bincon}$, represent the sets of unary operations, binary operations, unary conditions and binary conditions of the MCS-51 machine code language, lifted into RTL, respectively.
83
84\begin{table}
85{\footnotesize
86$87\begin{array}{lllllll} 88\textit{size} & ::= & \textsf{Byte} \Alt \textsf{HalfWord} \Alt \textsf{Word} & \qquad 89\textit{fun\_ref} & ::= & \textit{fun\_name} \Alt \textit{psd\_reg} 90\end{array} 91$
92
93$94\begin{array}{llll} 95\textit{instruction} & ::= & \Alt \textsf{skip} \rightarrow \textit{node} & 96 \quad \mbox{(no instruction)}\\ 97 & & \Alt \textit{psd\_reg} := n 98 \rightarrow \textit{node} & \quad \mbox{(constant)}\\ 99 & & \Alt \textit{psd\_reg} := \textit{unop}(\textit{psd\_reg}) 100 \rightarrow \textit{node} & \quad \mbox{(unary operation)}\\ 101 & & \Alt \textit{psd\_reg} := 102 \textit{binop}(\textit{psd\_reg},\textit{psd\_reg}) 103 \rightarrow \textit{node} & \quad 104 \mbox{(binary operation)}\\ 105 & & \Alt \textit{psd\_reg} := \textsf{\&globals}[n] 106 \rightarrow \textit{node} & 107 \quad \mbox{(address of a global)}\\ 108 & & \Alt \textit{psd\_reg} := \textsf{\&locals}[n] 109 \rightarrow \textit{node} & 110 \quad \mbox{(address of a local)}\\ 111 & & \Alt \textit{psd\_reg} := \textit{fun\_name} 112 \rightarrow \textit{node} & 113 \quad \mbox{(address of a function)}\\ 114 & & \Alt \textit{psd\_reg} := 115 \textit{size}(\textit{psd\_reg}[n]) 116 \rightarrow \textit{node} & \quad \mbox{(memory load)}\\ 117 & & \Alt \textit{size}(\textit{psd\_reg}[n]) := 118 \textit{psd\_reg} 119 \rightarrow \textit{node} & \quad \mbox{(memory store)}\\ 120 & & \Alt \textit{psd\_reg} := \textit{fun\_ref}({\it psd\_reg^*}) 121 \rightarrow \textit{node} & 122 \quad \mbox{(function call)}\\ 123 & & \Alt \textit{fun\_ref}({\it psd\_reg^*}) 124 & \quad \mbox{(function tail call)}\\ 125 & & \Alt \textsf{test}\ \textit{uncon}(\textit{psd\_reg}) \rightarrow 126 \textit{node}, \textit{node} & \quad 127 \mbox{(branch unary condition)}\\ 128 & & \Alt \textsf{test}\ \textit{bincon}(\textit{psd\_reg},\textit{psd\_reg}) 129 \rightarrow \textit{node}, \textit{node} & \quad 130 \mbox{(branch binary condition)}\\ 131 & & \Alt \textsf{return}\ \textit{psd\_reg}? & \quad 132 \mbox{(return)} 133\end{array} 134$
135
136$137\begin{array}{lllllll} 138\textit{fun\_def} & ::= & \textit{fun\_name}(\textit{psd\_reg}^*) & \qquad 139\textit{program} & ::= & \textsf{globals}: n\\ 140 & & \textsf{result:} \textit{psd\_reg}? & \qquad 141 & & \textit{fun\_def}^*\\ 142 & & \textsf{locals:} \textit{psd\_reg}^*\\ 143 & & \textsf{stack:} n\\ 144 & & \textsf{entry:} \textit{node}\\ 145 & & \textsf{exit:} \textit{node}\\ 146 & & (\textit{node:} \textit{instruction})^* 147\end{array} 148$}
149\caption{Syntax of the RTL language}\label{RTL:syntax}
150\end{table}
151
152Translating from RTLabs into RTL is mostly straightforward.
153An RTLAbs instruction is often directly translated to a corresponding MCS-51 instruction.
154However, there are a few exceptions: some RTLAbs instructions are expanded into multiple MCS-51 instructions.
155When the translation of an RTLAbs instruction requires more than a few simple MCS-51 instructions, we generate a function implementing the RTLabs instruction, place it in the program's preamble before the entry point, and generate a call to the relevant function, instead of directly generating the instruction sequence.
156
157\paragraph{ERTL} programs are again structured as CFGs.
158In ERTL, calling conventions of the MCS-51 machine language are made explicit.
159We provide the syntax of the language in Table~\ref{ERTL:syntax}.
160
161The main difference between RTL and ERTL is the elimination of pseudo registers, and the use of hardware registers to pass arguments to functions.
162Parameters are now passed in fixed hardware registers, tied directly to our target hardware.
163If there are too many parameters, the remaining arguments to be passed are spilled, and are stored in the stack.
164
165Further, we now enforce a convention that certain other now-explicit hardware registers are used for certain tasks.
166We fix registers holding the result of a function, holding the base address of the program's global variables, holding the address of the top of the stack.
167We also make explicit that some registers must be saved and restored when entering or returning from a function, to avoid clobbering.
168
169ERTL function calls do not list their parameters anymore---they merely assert the number of arguments that are being passed.
170Two new instructions are provided to allocate and deallocate on the stack some space needed by a function to execute.
171Along with these two instructions come two instructions to fetch or assign a value in the parameter sections of the stack; these instructions cannot yet be translated using regular load and store instructions.
172This is because we do not know the final size of the stack area of each function at this point in the compilation chain.
173
174Note that the ERTL function return instruction has a boolean argument that indicates whether the result of the function may be used later or not.
175This is exploited in certain optimisations.
176
177\begin{table}
178{\footnotesize
179$180\begin{array}{lllllll} 181\textit{size} & ::= & \textsf{Byte} \Alt \textsf{HalfWord} \Alt \textsf{Word} & \qquad 182\textit{fun\_ref} & ::= & \textit{fun\_name} \Alt \textit{psd\_reg} 183\end{array} 184$
185
186$187\begin{array}{llll} 188\textit{instruction} & ::= & \Alt \textsf{skip} \rightarrow \textit{node} & 189 \quad \mbox{(no instruction)}\\ 190 & & \Alt \textsf{NewFrame} \rightarrow \textit{node} & 191 \quad \mbox{(frame creation)}\\ 192 & & \Alt \textsf{DelFrame} \rightarrow \textit{node} & 193 \quad \mbox{(frame deletion)}\\ 194 & & \Alt \textit{psd\_reg} := \textsf{stack}[\textit{slot}, n] 195 \rightarrow \textit{node} & 196 \quad \mbox{(stack load)}\\ 197 & & \Alt \textsf{stack}[\textit{slot}, n] := \textit{psd\_reg} 198 \rightarrow \textit{node} & 199 \quad \mbox{(stack store)}\\ 200 & & \Alt \textit{hdw\_reg} := \textit{psd\_reg} 201 \rightarrow \textit{node} & 202 \quad \mbox{(pseudo to hardware)}\\ 203 & & \Alt \textit{psd\_reg} := \textit{hdw\_reg} 204 \rightarrow \textit{node} & 205 \quad \mbox{(hardware to pseudo)}\\ 206 & & \Alt \textit{psd\_reg} := n 207 \rightarrow \textit{node} & \quad \mbox{(constant)}\\ 208 & & \Alt \textit{psd\_reg} := \textit{unop}(\textit{psd\_reg}) 209 \rightarrow \textit{node} & \quad \mbox{(unary operation)}\\ 210 & & \Alt \textit{psd\_reg} := 211 \textit{binop}(\textit{psd\_reg},\textit{psd\_reg}) 212 \rightarrow \textit{node} & \quad 213 \mbox{(binary operation)}\\ 214 & & \Alt \textit{psd\_reg} := \textit{fun\_name} 215 \rightarrow \textit{node} & 216 \quad \mbox{(address of a function)}\\ 217 & & \Alt \textit{psd\_reg} := 218 \textit{size}(\textit{psd\_reg}[n]) 219 \rightarrow \textit{node} & \quad \mbox{(memory load)}\\ 220 & & \Alt \textit{size}(\textit{psd\_reg}[n]) := 221 \textit{psd\_reg} 222 \rightarrow \textit{node} & \quad \mbox{(memory store)}\\ 223 & & \Alt \textit{fun\_ref}(n) \rightarrow \textit{node} & 224 \quad \mbox{(function call)}\\ 225 & & \Alt \textit{fun\_ref}(n) 226 & \quad \mbox{(function tail call)}\\ 227 & & \Alt \textsf{test}\ \textit{uncon}(\textit{psd\_reg}) \rightarrow 228 \textit{node}, \textit{node} & \quad 229 \mbox{(branch unary condition)}\\ 230 & & \Alt \textsf{test}\ \textit{bincon}(\textit{psd\_reg},\textit{psd\_reg}) 231 \rightarrow \textit{node}, \textit{node} & \quad 232 \mbox{(branch binary condition)}\\ 233 & & \Alt \textsf{return}\ b & \quad \mbox{(return)} 234\end{array} 235$
236
237$238\begin{array}{lllllll} 239\textit{fun\_def} & ::= & \textit{fun\_name}(n) & \qquad 240\textit{program} & ::= & \textsf{globals}: n\\ 241 & & \textsf{locals:} \textit{psd\_reg}^* & \qquad 242 & & \textit{fun\_def}^*\\ 243 & & \textsf{stack:} n\\ 244 & & \textsf{entry:} \textit{node}\\ 245 & & (\textit{node:} \textit{instruction})^* 246\end{array} 247$}
248\caption{Syntax of the ERTL language}\label{ERTL:syntax}
249\end{table}
250
251The majority of the work involved in translating from RTL to ERTL involves making the MCS-51 calling conventions explicit.
252These conventions appear when entering, calling and leaving a function, and when referencing a global variable or the address of a local variable.
253
254At this point, we also perform a \emph{liveness analysis} on ERTL to replace unused instructions by a $\textsf{skip}$, or dummy instruction with no effect on the program state.
255Our analysis declares an instruction as unused when it performs an assignment on a register that will not be read afterwards.
256The result of this liveness analysis is also exploited by the \emph{register allocation} algorithm whose result is to efficiently associate a physical location (a hardware register or an address in the stack) to each pseudo register of the input RTL program.
257
258\paragraph{LTL}
259
260\paragraph{LIN}
261
262\subsection{Target hardware}
263
264\subsubsection{LTL}
265
266As in ERTL, the structure of LTL programs is based on CFGs. Pseudo
267registers are not used anymore; instead, they are replaced by physical locations
268(a hardware register or an address in the stack).
269
270\paragraph{Syntax.}
271Except for a few exceptions, the instructions of the language are those of
272ERTL with hardware registers replacing pseudo registers. Calling and
273returning conventions were explicited in ERTL; thus, function calls and
274returns do not need parameters in LTL. The syntax is defined in table
275\ref{LTL:syntax}.
276
277\begin{table}
278{\footnotesize
279$280\begin{array}{lllllll} 281\textit{size} & ::= & \textsf{Byte} \Alt \textsf{HalfWord} \Alt \textsf{Word} & \qquad 282\textit{fun\_ref} & ::= & \textit{fun\_name} \Alt \textit{hdw\_reg} 283\end{array} 284$
285
286$287\begin{array}{llll} 288\textit{instruction} & ::= & \Alt \textsf{skip} \rightarrow \textit{node} & 289 \quad \mbox{(no instruction)}\\ 290 & & \Alt \textsf{NewFrame} \rightarrow \textit{node} & 291 \quad \mbox{(frame creation)}\\ 292 & & \Alt \textsf{DelFrame} \rightarrow \textit{node} & 293 \quad \mbox{(frame deletion)}\\ 294 & & \Alt \textit{hdw\_reg} := n 295 \rightarrow \textit{node} & \quad \mbox{(constant)}\\ 296 & & \Alt \textit{hdw\_reg} := \textit{unop}(\textit{hdw\_reg}) 297 \rightarrow \textit{node} & \quad \mbox{(unary operation)}\\ 298 & & \Alt \textit{hdw\_reg} := 299 \textit{binop}(\textit{hdw\_reg},\textit{hdw\_reg}) 300 \rightarrow \textit{node} & \quad 301 \mbox{(binary operation)}\\ 302 & & \Alt \textit{hdw\_reg} := \textit{fun\_name} 303 \rightarrow \textit{node} & 304 \quad \mbox{(address of a function)}\\ 305 & & \Alt \textit{hdw\_reg} := \textit{size}(\textit{hdw\_reg}[n]) 306 \rightarrow \textit{node} & \quad \mbox{(memory load)}\\ 307 & & \Alt \textit{size}(\textit{hdw\_reg}[n]) := \textit{hdw\_reg} 308 \rightarrow \textit{node} & \quad \mbox{(memory store)}\\ 309 & & \Alt \textit{fun\_ref}() \rightarrow \textit{node} & 310 \quad \mbox{(function call)}\\ 311 & & \Alt \textit{fun\_ref}() 312 & \quad \mbox{(function tail call)}\\ 313 & & \Alt \textsf{test}\ \textit{uncon}(\textit{hdw\_reg}) \rightarrow 314 \textit{node}, \textit{node} & \quad 315 \mbox{(branch unary condition)}\\ 316 & & \Alt \textsf{test}\ \textit{bincon}(\textit{hdw\_reg},\textit{hdw\_reg}) 317 \rightarrow \textit{node}, \textit{node} & \quad 318 \mbox{(branch binary condition)}\\ 319 & & \Alt \textsf{return} & \quad \mbox{(return)} 320\end{array} 321$
322
323$324\begin{array}{lllllll} 325\textit{fun\_def} & ::= & \textit{fun\_name}(n) & \qquad 326\textit{program} & ::= & \textsf{globals}: n\\ 327 & & \textsf{locals:} n & \qquad 328 & & \textit{fun\_def}^*\\ 329 & & \textsf{stack:} n\\ 330 & & \textsf{entry:} \textit{node}\\ 331 & & (\textit{node:} \textit{instruction})^* 332\end{array} 333$}
334\caption{Syntax of the LTL language}\label{LTL:syntax}
335\end{table}
336
337\paragraph{Translation of ERTL to LTL.} The translation relies on the
338results of the liveness analysis and of the register allocation. Unused
339instructions are eliminated and each pseudo register is replaced by a physical
340location. In LTL, the size of the stack frame of a function is known;
341instructions intended to load or store values in the stack are translated
342using regular load and store instructions.
343
344\paragraph{Optimizations.} A \emph{graph compression} algorithm removes empty
345instructions generated by previous compilation passes and by the liveness
346analysis.
347
348\subsubsection{LIN}
349
350In LIN, the structure of a program is no longer based on CFGs. Every function
351is represented as a sequence of instructions.
352
353\paragraph{Syntax.}
354The instructions of LIN are very close to those of LTL. \emph{Program
355  labels}, \emph{gotos} and branch instructions handle the changes in the
356control flow. The syntax of LIN programs is shown in table \ref{LIN:syntax}.
357
358\begin{table}
359{\footnotesize
360$361\begin{array}{lllllll} 362\textit{size} & ::= & \textsf{Byte} \Alt \textsf{HalfWord} \Alt \textsf{Word} & \qquad 363\textit{fun\_ref} & ::= & \textit{fun\_name} \Alt \textit{hdw\_reg} 364\end{array} 365$
366
367$368\begin{array}{llll} 369\textit{instruction} & ::= & \Alt \textsf{NewFrame} & 370 \quad \mbox{(frame creation)}\\ 371 & & \Alt \textsf{DelFrame} & 372 \quad \mbox{(frame deletion)}\\ 373 & & \Alt \textit{hdw\_reg} := n & \quad \mbox{(constant)}\\ 374 & & \Alt \textit{hdw\_reg} := \textit{unop}(\textit{hdw\_reg}) 375 & \quad \mbox{(unary operation)}\\ 376 & & \Alt \textit{hdw\_reg} := 377 \textit{binop}(\textit{hdw\_reg},\textit{hdw\_reg}) 378 & \quad \mbox{(binary operation)}\\ 379 & & \Alt \textit{hdw\_reg} := \textit{fun\_name} 380 & \quad \mbox{(address of a function)}\\ 381 & & \Alt \textit{hdw\_reg} := \textit{size}(\textit{hdw\_reg}[n]) 382 & \quad \mbox{(memory load)}\\ 383 & & \Alt \textit{size}(\textit{hdw\_reg}[n]) := \textit{hdw\_reg} 384 & \quad \mbox{(memory store)}\\ 385 & & \Alt \textsf{call}\ \textit{fun\_ref} 386 & \quad \mbox{(function call)}\\ 387 & & \Alt \textsf{tailcall}\ \textit{fun\_ref} 388 & \quad \mbox{(function tail call)}\\ 389 & & \Alt \textit{uncon}(\textit{hdw\_reg}) \rightarrow 390 \textit{node} & \quad 391 \mbox{(branch unary condition)}\\ 392 & & \Alt \textit{bincon}(\textit{hdw\_reg},\textit{hdw\_reg}) 393 \rightarrow \textit{node} & \quad 394 \mbox{(branch binary condition)}\\ 395 & & \Alt \textit{mips\_label:} & \quad \mbox{(MCS-51 label)}\\ 396 & & \Alt \textsf{goto}\ \textit{mips\_label} & \quad \mbox{(goto)}\\ 397 & & \Alt \textsf{return} & \quad \mbox{(return)} 398\end{array} 399$
400
401$402\begin{array}{lllllll} 403\textit{fun\_def} & ::= & \textit{fun\_name}(n) & \qquad 404\textit{program} & ::= & \textsf{globals}: n\\ 405 & & \textsf{locals:} n & \qquad 406 & & \textit{fun\_def}^*\\ 407 & & \textit{instruction}^* 408\end{array} 409$}
410\caption{Syntax of the LIN language}\label{LIN:syntax}
411\end{table}
412
413\paragraph{Translation of LTL to LIN.}
414This translation amounts to transform in an efficient way the graph structure of
415functions into a linear structure of sequential instructions.
416
417\subsubsection{ASM}
Note: See TracBrowser for help on using the repository browser.