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

Last change on this file since 1356 was 1356, checked in by mulligan, 9 years ago

deleted redundant directory. added outlines for both reports, and added a few sections to report for D4.2. more work on foldi_strong in rtlabs to rtl

File size: 12.6 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={ndefinition,ncoercion,nlemma,ntheorem,nremark,ninductive,nrecord,nqed,nlet,let,in,rec,match,return,with,Type,try},
23   morekeywords={[2]nwhd,nnormalize,nelim,ncases,ndestruct},
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,
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
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%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
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}
116Executable Formal Semantics of back-end intermediate languages: This prototype is the formal counterpart of deliverable D2.1 for the back end side of the compiler and validates it.
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.1, D4.3 and D4.4.
127
128Deliverable D2.1, 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 compilation chain}
142\label{subsect.brief.overview.compilation.chain}
143
144
145
146%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
147% SECTION.                                                                    %
148%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
149\section{The backend intermediate languages in Matita}
150\label{sect.backend.intermediate.languages.matita}
151
152%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
153% SECTION.                                                                    %
154%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
155\subsection{Use of dependent types}
156\label{subsect.use.of.dependent.types}
157
158%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
159% SECTION.                                                                    %
160%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
161\subsection{Abstracting related languages}
162\label{subsect.abstracting.related.languages}
163
164%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
165% SECTION.                                                                    %
166%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
167\subsection{What we do not implement}
168\label{subsect.what.we.do.not.implement}
169
170There are several classes of functionality that we have chosen not to implement in the backend languages:
171\begin{itemize}
172\item
173\textbf{Datatypes and functions over these datatypes that are not supported by the compiler.}
174In particular, the compiler does not support the floating point datatype, nor accompanying functions over that datatype.
175At the moment, frontend languages within the compiler possess constructors corresponding to floating point code.
176These are removed during instruction selection (in the RTLabs to RTL transformation) using a daemon.
177However, 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.
178\item
179\textbf{Functions and operations on datatypes that are implemented in the C runtime.}
180The compiler emits only a subset of the instructions available in the MCS-51's instruction architecture.
181In 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.
182
183However, 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.
184We 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.
185\item
186\textbf{Axiomatised components that will be implemented using external oracles.}
187Several large, complex pieces of compiler infrastructure, most noticably register colouring and fixed point calculation during liveness analysis have been axiomatised.
188This 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.
189Instead, 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.
190These axiomatised components are found in the ERTL to LTL pass.
191\item
192\textbf{A few non-computational proof obligations.}
193A 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.
194These proof obligations originate with our use of dependent types for expressing invariants in the compiler.
195\textbf{Real' tailcalls}
196For the time being, tailcalls in the backend are translated to vanilla' function calls during the ERTL to LTL pass.
197This follows the O'Caml compiler, which did not implement tailcalls, and did this simplification step.
198Real' 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.
199\end{itemize}
200
201%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
202% SECTION.                                                                    %
203%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
204\section{Future work}
205\label{sect.future.work}
206
207As 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.
208We summarise this future work here:
209\begin{itemize}
210\item
211We plan to make use of dependent types to identify `floating point' free programs and make all functions total over such programs.
212This will remove a swathe of uses of daemons.
213This should be routine.
214\item
215We plan to move expansion of integer modulus, and other related functions, into the instruction selection (RTLabs to RTL) phase.
216This 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.
217\item
218We plan to close all existing proof obligations that are closed using daemons, arising from our use of dependent types in the backend.
219This should be routine.
220\item
221We plan to port the O'Caml compiler's implementation of tailcalls when this is completed.
222This should not cause any major problems.
223\item
224We plan to validate the backend translations, removing any obvious bugs, by executing the translation inside Matita on small C programs.
225\end{itemize}
226
227\newpage
228
229%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
230% SECTION.                                                                    %
231%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
232\section{Code listing}
233\label{sect.code.listing}
234
235%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
236% SECTION.                                                                    %
237%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
238\subsection{Listing of files}
239\label{subsect.listing.files}
240
241Translation specific files (files relating to language semantics have been omitted):
242\begin{center}
243\begin{tabular*}{0.9\textwidth}{p{5cm}p{8cm}}
244Title & Description \\
245\hline
246\texttt{RTLabs/syntax.ma} & The syntax of RTLabs \\
247\texttt{RTLabs/RTLabsToRTL.ma} & The translation from RTLabs to RTL \\
248\texttt{joint/Joint.ma} & Abstracted syntax for backend languages \\
249\texttt{joint/TranslateUtils.ma} & Generic translation utilities \\
250\texttt{RTL/RTL.ma} & The syntax of RTL \\
251\texttt{RTL/RTLToERTL.ma} & The translation from RTL to ERTL \\
252\texttt{RTL/RTLtailcall.ma} & Elimination of tailcalls \\
253\texttt{ERTL/ERTL.ma} & The syntax of ERTL \\
254\texttt{ERTL/ERTLToLTL.ma} & The translation from ERTL to LTL \\
255\texttt{ERTL/Interference.ma} & Axiomatised graph colouring component \\
256\texttt{ERTL/liveness.ma} & Liveness analysis \\
257\texttt{LTL/LTL.ma} & The syntax of LTL \\
258\texttt{LTL/LTLToLIN.ma} & The translation from LTL to LIN \\
259\texttt{LIN/LIN.ma} & The syntax of LIN \\
260\texttt{LIN/LINToASM.ma} & The translation from LIN to assembly language
261\end{tabular*}
262\end{center}
263
264\end{document}
Note: See TracBrowser for help on using the repository browser.