source: Deliverables/D4.2-4.3/reports/D4-2.tex @ 1366

Last change on this file since 1366 was 1366, checked in by mulligan, 8 years ago

added connections with other languages to d4.3 report, also fixed mistaken attribution of d2.2 to d2.1

File size: 27.7 KB
Line 
1\documentclass[11pt, epsf, a4wide]{article}
2
3\usepackage{../../style/cerco}
4
5\usepackage{amsfonts}
6\usepackage{amsmath}
7\usepackage{amssymb} 
8\usepackage[english]{babel}
9\usepackage{graphicx}
10\usepackage[utf8x]{inputenc}
11\usepackage{listings}
12\usepackage{stmaryrd}
13\usepackage{url}
14
15\title{
16INFORMATION AND COMMUNICATION TECHNOLOGIES\\
17(ICT)\\
18PROGRAMME\\
19\vspace*{1cm}Project FP7-ICT-2009-C-243881 \cerco{}}
20
21\lstdefinelanguage{matita-ocaml}
22  {keywords={definition,coercion,lemma,theorem,remark,inductive,record,qed,let,in,rec,match,return,with,Type,try},
23   morekeywords={[2]whd,normalize,elim,cases,destruct},
24   morekeywords={[3]type,of},
25   mathescape=true,
26  }
27
28\lstset{language=matita-ocaml,basicstyle=\small\tt,columns=flexible,breaklines=false,
29        keywordstyle=\color{red}\bfseries,
30        keywordstyle=[2]\color{blue},
31        keywordstyle=[3]\color{blue}\bfseries,
32        commentstyle=\color{green},
33        stringstyle=\color{blue},
34        showspaces=false,showstringspaces=false}
35
36\lstset{extendedchars=false}
37\lstset{inputencoding=utf8x}
38\DeclareUnicodeCharacter{8797}{:=}
39\DeclareUnicodeCharacter{10746}{++}
40\DeclareUnicodeCharacter{9001}{\ensuremath{\langle}}
41\DeclareUnicodeCharacter{9002}{\ensuremath{\rangle}}
42
43\date{}
44\author{}
45
46\begin{document}
47
48\thispagestyle{empty}
49
50\vspace*{-1cm}
51\begin{center}
52\includegraphics[width=0.6\textwidth]{../../style/cerco_logo.png}
53\end{center}
54
55\begin{minipage}{\textwidth}
56\maketitle
57\end{minipage}
58
59\vspace*{0.5cm}
60\begin{center}
61\begin{LARGE}
62\textbf{
63Report n. D4.2\\
64Functional encoding in the Calculus of Constructions
65}
66\end{LARGE} 
67\end{center}
68
69\vspace*{2cm}
70\begin{center}
71\begin{large}
72Version 1.0
73\end{large}
74\end{center}
75
76\vspace*{0.5cm}
77\begin{center}
78\begin{large}
79Main Authors:\\
80Dominic P. Mulligan and Claudio Sacerdoti Coen
81\end{large}
82\end{center}
83
84\vspace*{\fill}
85
86\noindent
87Project Acronym: \cerco{}\\
88Project full title: Certified Complexity\\
89Proposal/Contract no.: FP7-ICT-2009-C-243881 \cerco{}\\
90
91\clearpage
92\pagestyle{myheadings}
93\markright{\cerco{}, FP7-ICT-2009-C-243881}
94
95\newpage
96
97\vspace*{7cm}
98\paragraph{Abstract}
99We describe the encoding, in the Calculus of Constructions, of the intermediate languages for the CerCo compiler.
100The CerCo backend consists of four distinct intermediate languages---RTL, ERTL, LTL and LIN, respectively---though we also handle the translations from the last frontend intermediate language, RTLabs, into RTL, and the translation of LIN into assembly language.
101Where feasible, we have made use of dependent types to enforce invariants and to make otherwise partial functions total.
102\newpage
103
104\tableofcontents
105
106\newpage
107
108%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
109% SECTION.                                                                    %
110%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
111\section{Task}
112\label{sect.task}
113
114The Grant Agreement states that Task T4.2, entitled `Functional encoding in the Calculus of Constructions' has associated Deliverable D4.2, consisting of the following:
115\begin{quotation}
116CIC encoding: Back-end: Functional Specification in the internal language of the Proof Assistant (the Calculus of Inductive Construction) of the back end of the compiler. This unit is meant to be composable with the front-end of deliverable D3.2, to obtain a full working compiler for Milestone M2. A first validation of the design principles and implementation choices for the Untrusted Cost-annotating OCaml Compiler D2.2 is achieved and reported in the deliverable, possibly triggering updates of the Untrusted Cost-annotating OCaml Compiler sources.
117\end{quotation}
118This report details our implementation of this deliverable.
119
120%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
121% SECTION.                                                                    %
122%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
123\subsection{Connections with other deliverables}
124\label{subsect.connections.with.other.deliverables}
125
126Deliverable D4.2 enjoys a close relationship with three other deliverables, namely deliverables D2.2, D4.3 and D4.4.
127
128Deliverable D2.2, the O'Caml implementation of a cost preserving compiler for a large subset of the C programming language, is the basis upon which we have implemented the current deliverable.
129In particular, the architecture of the compiler, its intermediate languages, and the overall implementation of the Matita encodings has been taken from the O'Caml compiler.
130Any variations from the O'Caml design are due to bugs identified in the prototype compiler during the Matita implementation, our identification of code that can be abstracted and made generic, or our use of Matita's much stronger type system to enforce invariants through the use of dependent types.
131
132Deliverable D4.3 can be seen as a `sister' deliverable to the deliverable reported on herein.
133In particular, where this deliverable reports on the encoding in the Calculus of Constructions of the backend translations, D4.3 is the encoding in the Calculus of Constructions of the semantics of those languages.
134As a result, a substantial amount of Matita code is shared between the two deliverables.
135
136Deliverable D4.4, the backend correctness proofs, is the immediate successor of this deliverable.
137
138%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
139% SECTION.                                                                    %
140%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
141\subsection{A brief overview of the backend compilation chain}
142\label{subsect.brief.overview.backend.compilation.chain}
143
144The compiler's backend consists of four distinct intermediate languages: RTL, ERTL, LTL and LIN.
145A fifth language, RTLabs, serves as the exit point of the backend and the entry point of the frontend.
146RTL, ERTL and LTL are `graph based' languages, whereas LIN is a linearised language, the final language before translation to assembly.
147
148We now briefly discuss the properties of the intermediate languages, and discuss the various transformations that take place during the translation process:
149
150\paragraph{RTLabs ((Abstract) Register Transfer Language)}
151As mentioned, this is the final language of the compiler's frontend and the entry point for the backend.
152This language uses pseudoregisters, not hardware registers.
153During the translation pass from RTLabs to RTL instruction selection is carried out.
154
155\paragraph{RTL (Register Transfer Language)}
156This language uses pseudoregisters, not hardware registers.
157Tailcall elimination is carried out during the translation from RTL to ERTL.
158
159\paragraph{ERTL (Extended Register Transfer Language)}
160In this language most instructions still operate on pseudoregisters, apart from instructions that move data to, and from, the accumulator.
161The ERTL to LTL pass performs the following transformations: liveness analysis, register colouring and register/stack slot allocation.
162
163\paragraph{LTL (Linearised Transfer Language)}
164The name is somewhat of a misnomer, as the language is \emph{not} linearised, and is in fact still graph based, but uses hardware registers instead of pseudoregisters.
165Tunnelling (branch compression) should be implemented here.
166
167\paragraph{LIN (Linearised)}
168This is a linearised form of the LTL language; function graphs have been linearised into lists of statements.
169All registers have been translated into hardware registers or stack addresses.
170This is the final stage of compilation before translating directly into assembly language.
171
172%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
173% SECTION.                                                                    %
174%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
175\section{The backend intermediate languages in Matita}
176\label{sect.backend.intermediate.languages.matita}
177
178We now discuss the encoding of the compiler backend languages in the Calculus of Constructions proper.
179We pay particular heed to changes that we made from the O'Caml prototype.
180In particular, many aspects of the backend languages have been unified into a single `joint' language.
181We have also made heavy use of dependent types to reduce `spurious partiality' and to encode invariants.
182
183%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
184% SECTION.                                                                    %
185%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
186\subsection{Abstracting related languages}
187\label{subsect.abstracting.related.languages}
188
189The O'Caml compiler is written in the following manner.
190Each intermediate language has its own dedicated syntax, notions of internal function, and so on.
191Translations map syntaxes to syntaxes, and internal functions to internal functions explicitly.
192
193This is a perfectly valid way to write a compiler, where everything is made explicit, but writing a \emph{verified} compiler poses new challenges.
194In particular, we must look ahead to see how our choice of encodings will affect the size and complexity of the forthcoming proofs of correctness.
195We now discuss some abstractions, introduced in the Matita code, which we hope will make our proofs shorter, amongst other benefits.
196
197\paragraph{Shared code, reduced proofs}
198Many features of individual backend intermediate languages are shared with other intermediate languages.
199For instance, RTLabs, RTL, ERTL and LTL are all graph based languages, where functions are represented as a graph of statements that form their bodies.
200Functions for adding statements to a graph, searching the graph, and so on, are remarkably similar across all languages, but are duplicated in the O'Caml code.
201
202As a result, we chose to abstract the representation of internal functions for the RTL, ERTL, LTL and LIN intermediate languages into a `joint' representation.
203This representation is parameterised by a record that dictates the layout of the function body for each intermediate language.
204For instance, in RTL, the layout is graph like, whereas in LIN, the layout is a linearised list of statements.
205Further, a generalised way of accessing the successor statement to the one currently under consideration is needed, and so forth.
206
207Our joint internal function record looks like so:
208\begin{lstlisting}
209record joint_internal_function (globals: list ident) (p:params globals) : Type[0] ≝
210{ 
211  ...
212  joint_if_params   : paramsT p;
213  joint_if_locals   : localsT p;
214  ...
215  joint_if_code     : codeT … p;
216  ...
217}.
218\end{lstlisting}
219In particular, everything that can vary between differing intermediate languages has been parameterised.
220Here, we see the number of parameters, the listing of local variables, and the internal code representation has been parameterised.
221Other particulars are also parameterised, though here omitted.
222
223Hopefully this abstraction process will reduce the number of proofs that need to be written, dealing with internal functions.
224We only need to prove once that fetching a statement's successor is `correct', and we inherit this property for free for every intermediate language.
225
226\paragraph{Changes between languages made explicit}
227Due to the bureaucracy inherent in explicating each intermediate language's syntax in the O'Caml compiler, it can often be hard to see exactly what changes between each successive intermediate language.
228By abstracting the syntax of the RTL, ERTL, LTL and LIN intermediate languages, we make these changes much clearer.
229
230Our abstraction takes the following form:
231\begin{lstlisting}
232inductive joint_instruction (p: params__) (globals: list ident): Type[0] :=
233  | COMMENT: String $\rightarrow$ joint_instruction p globals
234  | COST_LABEL: costlabel $\rightarrow$ joint_instruction p globals
235  | INT: generic_reg p $\rightarrow$ Byte $\rightarrow$ joint_instruction p globals
236  ...
237  | extension: extend_statements p $\rightarrow$ joint_instruction p globals.
238\end{lstlisting}
239We first note that for the majority of intermediate languages, many instructions are shared.
240However, these instructions expect different register types (either a pseudoregister or a hardware register) as arguments.
241We must therefore parameterise the joint syntax with a record of parameters that will be specialised to each intermediate language.
242In the type above, this parameterisation is realised wit the \texttt{params\_\_} record.
243
244Further, we note that some intermediate languages have language specific instructions (i.e. the instructions that change between languages).
245We therefore add a new constructor to the syntax, \texttt{extension}, which expects a value of type \texttt{extend\_statements p}.
246As \texttt{p} varies between intermediate languages, we can provide language specific extensions to the syntax of the joint language.
247For example, ERTL's extended syntax consists of the following extra statements:
248\begin{lstlisting}
249inductive ertl_statement_extension: Type[0] :=
250  | ertl_st_ext_new_frame: ertl_statement_extension
251  | ertl_st_ext_del_frame: ertl_statement_extension
252  | ertl_st_ext_frame_size: register $\rightarrow$ ertl_statement_extension.
253\end{lstlisting}
254These are further packaged into an ERTL specific instance of \texttt{params\_\_} as follows:
255\begin{lstlisting}
256definition ertl_params__: params__ :=
257  mk_params__ register register ... ertl_statement_extension.
258\end{lstlisting}
259
260\paragraph{Possible language commutations}
261The backend translation passes of the CerCo compiler differ quite a bit from the CompCert compiler.
262In the CompCert compiler, linearisation occurs much earlier in the compilation chain, and passes such as register colouring and allocation are carried out on a linearised form of program.
263Contrast this with our own approach, where the code is represented as a graph for much longer.
264
265However, by abstracting the representation of intermediate functions, we are now much more free to reorder translation passes as we see fit.
266The linearisation process, for instance, now no longer cares about the specific representation of code in the source and target languages.
267It just relies on a common interface.
268We are therefore, in theory, free to pick where we wish to linearise our representation.
269This adds an unusual flexibility into the compilation process, and allows us to freely experiment with different orderings of translation passes.
270
271%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
272% SECTION.                                                                    %
273%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
274\subsection{Use of dependent types}
275\label{subsect.use.of.dependent.types}
276
277We use dependent types in the backend for three reasons.
278
279First, we encode informal invariants, or uses of \texttt{assert false} in the O'Caml code, with dependent types, converting partial functions into total functions.
280There are numerous examples of this throughout the backend.
281For example, in the \texttt{RTLabs} to \texttt{RTL} transformation pass, many functions only `make sense' when lists of registers passed to them as arguments conform to some specific length.
282For instance, the \texttt{translate\_negint} function, which translates a negative integer constant:
283\begin{lstlisting}
284definition translate_negint ≝
285  $\lambda$globals: list ident.
286  $\lambda$destrs: list register.
287  $\lambda$srcrs: list register.
288  $\lambda$start_lbl: label.
289  $\lambda$dest_lbl: label.
290  $\lambda$def: rtl_internal_function globals.
291  $\lambda$prf: |destrs| = |srcrs|. (* assert here *)
292    ...
293\end{lstlisting}
294The last argument to the function, \texttt{prf}, is a proof that the lengths of the lists of source and destination registers are the same.
295This was an assertion in the O'Caml code.
296
297Secondly, we make use of dependent types to make the Matita code easier to read, and eventually the proofs of correctness for the compiler easier to write.
298For instance, many intermediate languages in the backend of the compiler, from RTLabs to LTL, are graph based languages.
299Here, function definitions consist of a graph (i.e. a map from labels to statements) and a pair of labels denoting the entry and exit points of this graph.
300Practically, we would always like to ensure that the entry and exit labels are present in the statement graph.
301We ensure that this is so with a dependent sum type in the \texttt{joint\_internal\_function} record, which all graph based languages specialise to obtain their own internal function representation:
302\begin{lstlisting}
303record joint_internal_function (globals: list ident) (p: params globals): Type[0] :=
304{
305  ...
306  joint_if_code     : codeT $\ldots$ p;
307  joint_if_entry    : $\Sigma$l: label. lookup $\ldots$ joint_if_code l $\neq$ None $\ldots$;
308  ...
309}.
310\end{lstlisting}
311Here, \texttt{codeT} is a parameterised type representing the `structure' of the function's body (a graph in graph based languages, and a list in the linearised LIN language).
312Specifically, the \texttt{joint\_if\_entry} is a dependent pair consisting of a label and a proof that the label in question is a vertex in the function's graph.
313A similar device exists for the exit label.
314
315Finally, we make use of dependent types for another reason: experimentation.
316Namely, CompCert makes little use of dependent types to encode invariants.
317In contrast, we wish to make as much use of dependent types as possible, both to experiment with different ways of encoding compilers in a proof assistant, but also as a way of `stress testing' Matita's support for dependent types.
318
319%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
320% SECTION.                                                                    %
321%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
322\subsection{What we do not implement}
323\label{subsect.what.we.do.not.implement}
324
325There are several classes of functionality that we have chosen not to implement in the backend languages:
326\begin{itemize}
327\item
328\textbf{Datatypes and functions over these datatypes that are not supported by the compiler.}
329In particular, the compiler does not support the floating point datatype, nor accompanying functions over that datatype.
330At the moment, frontend languages within the compiler possess constructors corresponding to floating point code.
331These are removed during instruction selection (in the RTLabs to RTL transformation) using a daemon.
332However, at some point, we would like the front end of the compiler to recognise programs that use floating point code and reject them as being invalid.
333\item
334\textbf{Functions and operations on datatypes that are implemented in the C runtime.}
335The compiler emits only a subset of the instructions available in the MCS-51's instruction architecture.
336In particular, integer modulus at the C source level is transformed into a call to a runtime function implementing the modulus operation during the translation to C-light.
337
338However, all datatypes corresponding to valid C operations over integers and floats mention integer modulus in the backend, and the translation of these operations is discharged using a daemon.
339We have plans to dispense with this `precooking' processs at the C-light level and move the translation of these operations into the RTLabs to RTL pass, where they can be translated properly.
340\item
341\textbf{Axiomatised components that will be implemented using external oracles.}
342Several large, complex pieces of compiler infrastructure, most noticably register colouring and fixed point calculation during liveness analysis have been axiomatised.
343This was already agreed upon before the start of the project, and is clearly marked in the project proposal, following comments by those involved with the CompCert project about the difficulty in formalising register colouring in that project.
344Instead, these components are axiomatised, along with the properties that they need to satisfy in order for the rest of the compilation chain to be correct.
345These axiomatised components are found in the ERTL to LTL pass.
346\item
347\textbf{A few non-computational proof obligations.}
348A few difficult-to-close, but non-computational (i.e. they do not prevent us from executing the compiler inside Matita), proof obligations have been closed using daemons in the backend.
349These proof obligations originate with our use of dependent types for expressing invariants in the compiler.
350\textbf{Branch compression (tunnelling).}
351This was a feature of the O'Caml compiler.
352It is not yet currently implemented in the Matita compiler.
353This feature is only an optimisation, and will not affect the correctness of the compiler.
354\textbf{`Real' tailcalls}
355For the time being, tailcalls in the backend are translated to `vanilla' function calls during the ERTL to LTL pass.
356This follows the O'Caml compiler, which did not implement tailcalls, and did this simplification step.
357`Real' tailcalls are being implemented in the O'Caml compiler, and when this implementation is complete, we aim to port this code to the Matita compiler.
358\end{itemize}
359
360%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
361% SECTION.                                                                    %
362%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
363\section{Future work}
364\label{sect.future.work}
365
366As mentioned in Section~\ref{subsect.what.we.do.not.implement}, there are several unimplemented features in the compiler, and several aspects of the Matita code that can be improved in order to make currently partial functions total.
367We summarise this future work here:
368\begin{itemize}
369\item
370We plan to make use of dependent types to identify `floating point' free programs and make all functions total over such programs.
371This will remove a swathe of uses of daemons.
372This should be routine.
373\item
374We plan to move expansion of integer modulus, and other related functions, into the instruction selection (RTLabs to RTL) phase.
375This will also help to remove a swathe of uses of daemons, as well as potentially introduce new opportunities for optimisations that we currently miss in expanding these instructions at the C-light level.
376\item
377We plan to close all existing proof obligations that are closed using daemons, arising from our use of dependent types in the backend.
378This should be routine.
379\item
380We plan to port the O'Caml compiler's implementation of tailcalls when this is completed, and eventually port the branch compression code currently in the O'Caml compiler to the Matita implementation.
381This should not cause any major problems.
382\item
383We plan to validate the backend translations, removing any obvious bugs, by executing the translation inside Matita on small C programs.
384\end{itemize}
385
386\newpage
387
388%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
389% SECTION.                                                                    %
390%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
391\section{Code listing}
392\label{sect.code.listing}
393
394%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
395% SECTION.                                                                    %
396%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
397\subsection{Listing of files}
398\label{subsect.listing.files}
399
400Translation specific files (files relating to language semantics have been omitted):
401\begin{center}
402\begin{tabular*}{0.9\textwidth}{p{5cm}p{8cm}}
403Title & Description \\
404\hline
405\texttt{RTLabs/syntax.ma} & The syntax of RTLabs \\
406\texttt{RTLabs/RTLabsToRTL.ma} & The translation from RTLabs to RTL \\
407\texttt{joint/Joint.ma} & Abstracted syntax for backend languages \\
408\texttt{joint/TranslateUtils.ma} & Generic translation utilities \\
409\texttt{RTL/RTL.ma} & The syntax of RTL \\
410\texttt{RTL/RTLToERTL.ma} & The translation from RTL to ERTL \\
411\texttt{RTL/RTLtailcall.ma} & Elimination of tailcalls \\
412\texttt{ERTL/ERTL.ma} & The syntax of ERTL \\
413\texttt{ERTL/ERTLToLTL.ma} & The translation from ERTL to LTL \\
414\texttt{ERTL/Interference.ma} & Axiomatised graph colouring component \\
415\texttt{ERTL/liveness.ma} & Liveness analysis \\
416\texttt{LTL/LTL.ma} & The syntax of LTL \\
417\texttt{LTL/LTLToLIN.ma} & The translation from LTL to LIN \\
418\texttt{LIN/LIN.ma} & The syntax of LIN \\
419\texttt{LIN/LINToASM.ma} & The translation from LIN to assembly language
420\end{tabular*}
421\end{center}
422
423%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
424% SECTION.                                                                    %
425%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
426\subsection{Listing of important functions and axioms}
427\label{subsect.listing.important.functions.and.axioms}
428
429We list some important functions in the backend compilation:
430
431\paragraph{From RTL/RTLabsToRTL.ma}
432\begin{center}
433\begin{tabular*}{0.9\textwidth}{p{5cm}p{8cm}}
434Title & Description \\
435\hline
436\texttt{translate\_stmt} & Translation of an RTLabs statement to an RTL statement \\
437\texttt{translate\_internal} & Translation of an RTLabs internal function to an RTL internal function \\
438\texttt{rtlabs\_to\_rtl} & Translation of an RTLabs program to an RTL program
439\end{tabular*}
440\end{center}
441
442\paragraph{From joint/TranslateUtils.ma}
443\begin{center}
444\begin{tabular*}{0.9\textwidth}{p{5cm}p{8cm}}
445Title & Description \\
446\hline
447\texttt{fresh\_regs} & Generic fresh pseudoregister generation, for any intermediate language \\
448\texttt{adds\_graph} & Generic means of adding a statement to a graph, for any intermediate language
449\end{tabular*}
450\end{center}
451
452\paragraph{From RTL/RTLTailcall.ma}
453\begin{center}
454\begin{tabular*}{0.9\textwidth}{p{5cm}p{8cm}}
455Title & Description \\
456\hline
457\texttt{simplify\_statement} & Remove a single tailcall \\
458\texttt{simplify\_graph} & Remove all tailcalls in the function graph \\
459\texttt{tailcall\_simplify} & Simplify an RTL program by removing tailcalls
460\end{tabular*}
461\end{center}
462
463\paragraph{From RTL/RTLToERTL.ma}
464\begin{center}
465\begin{tabular*}{0.9\textwidth}{p{5cm}p{8cm}}
466Title & Description \\
467\hline
468\texttt{translate\_stmt} & Translation of an RTL statement to an ERTL statement \\
469\texttt{translate\_funct\_internal} & Translation of an RTL internal function to an ERTL internal function \\
470\texttt{translate} & Translation of an RTL program to an ERTL program
471\end{tabular*}
472\end{center}
473
474\paragraph{From ERTL/liveness.ma}
475\begin{center}
476\begin{tabular*}{0.9\textwidth}{p{5cm}p{8cm}}
477Title & Description \\
478\hline
479\texttt{analyse} & Dead code analysis
480\end{tabular*}
481\end{center}
482
483\paragraph{From ERTL/Interference.ma}
484\begin{center}
485\begin{tabular*}{0.9\textwidth}{p{5cm}p{8cm}}
486Title & Description \\
487\hline
488\texttt{build} & The (axiomatised) graph colouring for register and stack slot allocation
489\end{tabular*}
490\end{center}
491
492\paragraph{From ERTL/ERTLToLTL.ma}
493\begin{center}
494\begin{tabular*}{0.9\textwidth}{p{5cm}p{8cm}}
495Title & Description \\
496\hline
497\texttt{translate\_statement} & Translation of an ERTL statement into multiple LTL statements \\
498\texttt{translate\_internal} & Translation of an ERTL internal function into an LTL internal function \\
499\texttt{ertl\_to\_ltl} & Translation of an ERTL program into an LTL program
500\end{tabular*}
501\end{center}
502
503\paragraph{From LTL/LTLToLIN.ma}
504\begin{center}
505\begin{tabular*}{0.9\textwidth}{p{5cm}p{8cm}}
506Title & Description \\
507\hline
508\texttt{visit} & Visits, in order, every node in the statement graph for linearisation \\
509\texttt{translate\_stmt} & Translation of an LTL statement to a LIN statement \\
510\texttt{branch\_compress} & Place holder (currently identity) function for branch compression \\
511\texttt{translate\_internal} & Translation of an LTL internal function into a LIN internal function \\
512\texttt{ltl\_to\_lin} & Translation of an LTL program to a LIN program
513\end{tabular*}
514\end{center}
515
516\paragraph{From LIN/LINToASM.ma}
517\begin{center}
518\begin{tabular*}{0.9\textwidth}{p{5cm}p{8cm}}
519Title & Description \\
520\hline
521\texttt{translate\_statements} & Translation of a LIN statement to mutliple assembly instructions \\
522\texttt{translate\_fun\_def} & Translation of a LIN internal function definition into assembly \\
523\texttt{translate} & Translation of a LIN program into assembly
524\end{tabular*}
525\end{center}
526
527\end{document}
Note: See TracBrowser for help on using the repository browser.