# source:Deliverables/D3.3/Report/report.tex@1235

Last change on this file since 1235 was 1235, checked in by campbell, 10 years ago

Some basic material for D3.2, but not yet finished.

File size: 18.2 KB
Line
1\documentclass[11pt,epsf,a4wide]{article}
2\usepackage[mathletters]{ucs}
3\usepackage[utf8x]{inputenc}
4\usepackage{listings}
5\usepackage{../../style/cerco}
6\newcommand{\ocaml}{OCaml}
7\newcommand{\clight}{Clight}
8\newcommand{\matita}{Matita}
9\newcommand{\sdcc}{\texttt{sdcc}}
10
11\newcommand{\textSigma}{\ensuremath{\Sigma}}
12
13% LaTeX Companion, p 74
14\newcommand{\todo}[1]{\marginpar{\raggedright - #1}}
15
16\lstdefinelanguage{coq}
17  {keywords={Definition,Lemma,Theorem,Remark,Qed,Save,Inductive,Record},
18   morekeywords={[2]if,then,else},
19  }
20
21\lstdefinelanguage{matita}
22  {keywords={definition,lemma,theorem,remark,inductive,record,qed,let,rec,match,with,Type,and,on},
23   morekeywords={[2]whd,normalize,elim,cases,destruct},
24   mathescape=true,
25   morecomment=[n]{(*}{*)},
26  }
27
28\lstset{language=matita,basicstyle=\small\tt,columns=flexible,breaklines=false,
29        keywordstyle=\color{red}\bfseries,
30        keywordstyle=[2]\color{blue},
32        stringstyle=\color{blue},
33        showspaces=false,showstringspaces=false}
34
35\lstset{extendedchars=false}
36\lstset{inputencoding=utf8x}
37\DeclareUnicodeCharacter{8797}{:=}
38\DeclareUnicodeCharacter{10746}{++}
39\DeclareUnicodeCharacter{9001}{\ensuremath{\langle}}
40\DeclareUnicodeCharacter{9002}{\ensuremath{\rangle}}
41
42
43\title{
44INFORMATION AND COMMUNICATION TECHNOLOGIES\\
45(ICT)\\
46PROGRAMME\\
47\vspace*{1cm}Project FP7-ICT-2009-C-243881 \cerco{}}
48
49\date{ }
50\author{}
51
52\begin{document}
53\thispagestyle{empty}
54
55\vspace*{-1cm}
56\begin{center}
57\includegraphics[width=0.6\textwidth]{../../style/cerco_logo.png}
58\end{center}
59
60\begin{minipage}{\textwidth}
61\maketitle
62\end{minipage}
63
64
65\vspace*{0.5cm}
66\begin{center}
67\begin{LARGE}
68\bf
69Report n. D3.3\\
70Executable Formal Semantics of front end intermediate languages\\
71\end{LARGE}
72\end{center}
73
74\vspace*{2cm}
75\begin{center}
76\begin{large}
77Version 1.0
78\end{large}
79\end{center}
80
81\vspace*{0.5cm}
82\begin{center}
83\begin{large}
84Main Authors:\\
85Brian~Campbell
86\end{large}
87\end{center}
88
89\vspace*{\fill}
90\noindent
91Project Acronym: \cerco{}\\
92Project full title: Certified Complexity\\
93Proposal/Contract no.: FP7-ICT-2009-C-243881 \cerco{}\\
94
96
97\newpage
98
99\vspace*{7cm}
100\paragraph{Abstract}
101We report on the formalization of the front end intermediate languages for the
102\cerco{} project's compiler using executable semantics in the \matita{} proof
103assistant.
104
105\newpage
106
107\tableofcontents
108
109% TODO: clear up any -ize vs -ise
110% TODO: clear up any "front end" vs "front-end"
111% TODO: clear up any mentions of languages that aren't textsf'd.
112% TODO: mention the restricted form of types after Clight
113% TODO: fix unicode in listings
114
115\section{Introduction}
116
117This work formalizes the front end intermediate languages from the \cerco{}
118prototype compiler, described in previous deliverables~\cite{d2.1,d2.2}.  The
119front end of the compiler is summarized in Figure~\ref{fig:summary}.  We
120have also refined parts of the formal development that are used for several of
121the languages in the compiler.
122
123We will also report on work to add several invariants to the languages.  This
124activity overlaps with task 3.4 on the correctness of the compiler front end.
125However, the use of dependent types mean that this work is tied closely to the
126definition of the languages and the transformations of the front end in task
1273.2.  By considering it now we can experiment with and judge its impact on the
128formal semantics, and how feasible retrofitting such invariants is.
129
130The input language to the formalized front end is the \textsf{Clight}
131language.  The executable semantics for this language were presented in a
132previous deliverable~\cite{d3.1}.  In the present work we will report on some
133minor changes to the semantics made to better align it with the whole
134development.
135
136\begin{figure}
137\begin{tabbing}
138\quad \= $\downarrow$ \quad \= \kill
139\textsf{C} (unformalized)\\
140\> $\downarrow$ \> CIL parser (unformalized \ocaml)\\
141\textsf{Clight}\\
142\> $\downarrow$ \> cast removal\\
143\> $\downarrow$ \> add runtime functions\\
144\> $\downarrow$ \> labelling\\
145\> $\downarrow$ \> stack variable allocation and control structure
146 simplification\\
147\textsf{Cminor}\\
148\> $\downarrow$ \> generate global variable initialisation code\\
149\> $\downarrow$ \> transform to RTL graph\\
150\textsf{RTLabs}\\
151\> $\downarrow$ \> start of target specific backend\\
152\ \  \dots
153\end{tabbing}
154\caption{Front end languages and transformations}
155\label{fig:summary}
156\end{figure}
157
158\subsection{Revisions to the prototype compiler}
159
160Ongoing work to maintain and improve the prototype compiler resulted in
161several changes.  Most importantly, the transformations to replace 16 and 32
162bit types have been moved from the \textsf{Clight} language to the
163target-specific stage between \textsf{RTLabs} and \textsf{RTL} to help
164generate better code, and the addition of a \textsf{Clight} cast removal
165transformation to reduce the number of 16 and 32 bit operations.
166
167The formalized semantics have tracked these changes, and in this report we
168describe them as they currently stand.
169
170\section{Definitions common to several languages}
171
172The semantics for many of the languages in the compiler share some core parts:
173the memory model, environments, runtime values, definitions of operations and
174a monad for encapsulating failure and I/O (using resumptions).  The executable
175memory model was ported from CompCert as part of the work on \textsf{Clight}
176and was reused for the front end languages\footnote{However, it is likely that
177we will revise the memory model to make it better suited for describing the
178back-end of our compiler.}.  The failure and I/O monad was introduced in the
179previous deliverable on \textsf{Clight}~\cite[\S4.2]{d3.1}.  The other parts
180are discussed below, with the only change to the runtime values being the
181representation of integers.
182
183\subsection{Identifiers}
184
185Each language features one or more kinds of names to represent variables,
186registers, \texttt{goto} labels and/or RTL graph labels.  We also need to
187describe various maps keyed on identifiers in the semantics and during
188compilation.
189
190Previous work on the executable semantics of the target machine
191code included bit vectors and bit vector tries to define various integers in
192the semantics, and give a low level view of memory~\cite{d4.1}.  To keep the
193size of the development down we have reused these data structures for
194identifiers and maps respectively.
195
196However, given the wide variety of identifiers used in the compiler we also
197wish to separate the different classes of identifier.  Thus we encapsulate the
198bit vector representing the identifier in a datatype that also carries a tag
199identifying which class of identifier we are using:
200\begin{lstlisting}
201inductive identifier (tag:String) : Type[0] ≝
202  an_identifier : Word → identifier tag.
203\end{lstlisting}
204The tries are also tagged in the same manner.
205
206One difficultly with using fixed size bit vectors for identifiers is that
207fresh name generation can fail if generate too many.  While we use an error
208monad to deal with failures, we wish to minimize its use in the compiler.
209Thus we add a flag to detect overflows, and check it after the phase of the
210compiler is complete to report exhaustion.  The rest of the phase can then be
211written as if name generation always succeeds.
212
213\subsection{Machine integers and arithmetic}
214
215The bit vectors in~\cite{d4.1} also came equipped with some basic arithmetic
216for the target semantics.  The front end required these operations to be
217generalized and extended.
218
219% TODO: expand, note need to sufficiently good performance for testing
220
221\subsection{Front end operations}
222
223The two front end intermediate languages, \textsf{Cminor} and \textsf{RTLabs},
224share the same set of operations on values.  They differ from
225\textsf{Clight}'s operations by incorporating casts and by having a separate
226operation for each type of data operated upon.  For example, subtraction of
227pointers is treated as a different operation from subtraction of integers.
228
229A common semantics is given for these operations, as simple functions on the
230operation and runtime values.
231
232\section{Clight}
233
234The \textsf{Clight} input language remained largely the same as in the
235previous deliverable~\cite{d3.1}.  The principal changes were to use the
236identifiers and arithmetic described above in place of the arbitrarily large
237integers used above.  For the identifiers, this relieved us of the burden of
238adding an efficient datatype for maps by reusing the bit vector tries instead.
239
240The arithmetic replaced a dependent pair of an arbitrary integer and proof
241that it was in range of 32 bit integers by the exact bit vector for each
242size of integer.  This direct approach is closer to the implementation and
243more obviously correct --- no extra precision can be left in by accident.
244
245\section{Cminor}
246
247The \textsf{Cminor} language does not store local variables in memory, and has
248simpler control structures than \textsf{Clight}.  The syntax is similar to the
249prototype, except that the types attached to expressions are restricted so
250that some corner cases are ruled out in the \textsf{Cminor} to \textsf{RTLabs}
251stage (see the accompanying deliverable 3.2 for details):
252\begin{lstlisting}
253inductive expr : typ → Type[0] ≝
254| Id : ∀t. ident → expr t
255| Cst : ∀t. constant → expr t
256| Op1 : ∀t,t'. unary_operation → expr t → expr t'
257| Op2 : ∀t1,t2,t'. binary_operation → expr t1 → expr t2 → expr t'
258| Mem : ∀t,r. memory_chunk → expr (ASTptr r) → expr t
259| Cond : ∀sz,sg,t. expr (ASTint sz sg) → expr t → expr t → expr t
260| Ecost : ∀t. costlabel → expr t → expr t.
261\end{lstlisting}
262In principle we could extend this to statically ensure that only well-typed
263\textsf{Cminor} expressions are considered, and we will consider this as part
264of the work on correctness in task 3.4.
265
266We also provide a variant of the syntax where the only initialization data is
267the size of each global variable, for use after the initialization code has
268been generated.
269
270The definition of the semantics is routine: a functional definition of a
271single small step of the machine is given, reusing the memory model,
272environments, arithmetic and operations mentioned above.
273
274\section{RTLabs}
275
276The \textsf{RTLabs} language provides a target independent Register Transfer
277Language, where programs are represented as control flow graphs.  We use the
278identifiers described above for the graph labels and the maps for the graph
279itself.  The tagging mechanism ensures that labels cannot be mixed up with
280other identifiers in the program (in particular, we cannot accidentally reuse
281a \texttt{goto} label from Cminor where a graph label should appear).
282
283Otherwise, the syntax and semantics of RTLabs mirrors that of the prototype
284compiler.  The same common elements are used as for \textsf{Cminor}, including
285the front end operations mentioned above.
286
287\section{Testing}
288
289To provide some assurance that the semantics were properly implemented, and to
290support the testing described in the accompanying deliverable 3.2, we have
291adapted the pretty printers in the prototype compiler to produce \matita{}
292terms in the syntax for each language described above.
293
294A few common definitions were added for animating the small step semantics
295definitions for any of the front end languages in \matita.  We then used a
296small selection of test cases to ensure basic functionality.  However, this is
297still a time consuming process, so more testing will carried out once the
298extraction to \ocaml{} programs is implemented in \matita.
299
300\section{Embedding invariants}
301
302Each phase of the prototype compiler can fail in a number of places if the
303input language permits programs that are badly structured in some sense: a
304missing label in a \texttt{goto} statement or CFG, an undefined variable name,
305a \texttt{break} statement outside of a loop or \texttt{switch}, and so on.
306We wish to restrict our intermediate languages using dependent types to remove
307as many `junk' programs as possible.  We also hope that such restrictions will
308help in other correctness proofs.
309
310This goal lies in the overlap between several tasks in the project: it
311involves manipulating the syntax and semantics of the intermediate languages
312(the present work), the encoding of the front-end compiler phases in \matita{}
313(task 3.2) and the correctness of the front-end (task 3.4).  Thus this work is
314rather experimental; it is being carried out on branches in our source code
315repository and the final form will be decided and merged in during task 3.4.
316
317So far we have tried adding two forms of invariant --- one by using dependent
318types to index statements in \textsf{Cminor} by their block depth, and the
319other asserts that variables and labels are present in the appropriate
320environments by adding a separate invariant to each function.  Note that these
321do not yet cover all of the properties that a program in these languages is
322expected to enjoy; for example, there are currently no checks that references
323to globals are well-defined.
324
325\subsection{Cminor block depth}
326
327The \textsf{Cminor} language simplifies loops with a single infinite loop
328construct and the switch statement does not contain the individual cases.
329Instead, statements are provided for infinite loops, non-looping blocks and
330exiting an arbitrary number of blocks (which is also what the switch statement
331does\footnote{We are considering replacing the \textsf{Cminor} switch
332statement with one that uses \texttt{goto}-like labels in both the prototype
333and the formalized compilers, but for now we stick with this CompCert-like
334arrangement.}.
335
336However, this means that there are badly-formed \textsf{Cminor} programs such
337as
338\begin{lstlisting}[language={}]
339  int main() {
340    block {
341      exit 5
342    }
343  }
344\end{lstlisting}
345where we attempt to exit more blocks than exist.  To rule these out (including
346demonstrating that the previous phase of the compiler does not generate them)
347we can index the statements of the language by the depth of the enclosing
348blocks.
349
350The adaption of the syntax adds the depth to every statement, and uses bounded
351integers in the exit and switch statements:
352\begin{lstlisting}[language=matita]
353inductive stmt : ∀blockdepth:nat. Type[0] ≝
354| St_skip : ∀n. stmt n
355...
356| St_loop : ∀n. stmt n → stmt n
357| St_block : ∀n. stmt (S n) → stmt n
358| St_exit : ∀n. Fin n → stmt n
359(* expr to switch on, table of <switch value, #blocks to exit>, default *)
360| St_switch : expr → ∀n. list (int × (Fin n)) → Fin n → stmt n
361...
362\end{lstlisting}
363where \texttt{stmt n} is a statement enclosed in \texttt{n} blocks or loops,
364and \texttt{Fin n} is a standard construction for a natural number which is at
365most \texttt{n}.
366
367In the semantics the number of blocks is also added to the continuations and
368state, and the function to find the continuation from an exit statement can be
370
371We note in passing that adding this parameter detected a small mistake in the
372semantics concerning continuations and tail calls, although the mistake itself
373was benign.
374
375\subsection{Identifier invariants}
376
377For showing that the variables and labels occurring in the body of a function
378are present in the relevant structures are add an additional invariant to the
379function records.
380
381For \textsf{Cminor} we add a higher-order predicate which recursively applies
382a predicate to all substatements:
383\begin{lstlisting}[language=matita]
384let rec stmt_P (P:stmt → Prop) (s:stmt) on s : Prop ≝
385match s with
386[ St_seq s1 s2 ⇒ P s ∧ stmt_P P s1 ∧ stmt_P P s2
387| St_ifthenelse _ _ _ s1 s2 ⇒ P s ∧ stmt_P P s1 ∧ stmt_P P s2
388| St_loop s' ⇒ P s ∧ stmt_P P s'
389| St_block s' ⇒ P s ∧ stmt_P P s'
390| St_label _ s' ⇒ P s ∧ stmt_P P s'
391| St_cost _ s' ⇒ P s ∧ stmt_P P s'
392| _ ⇒ P s
393].
394\end{lstlisting}
395Dependent pattern matching on statements thus allows \lstinline'stmt_P' to
396unfold to the predicate on the current statement as well as the predicate
397applied to all substatements.
398
399We use two properties in \textsf{Cminor}:
400\begin{enumerate}
401\item All variables are present in the list of parameters or the list of
402variables for the function (this also uses a similar recursive predicate on
403expressions).
404\item All labels in \texttt{goto} statements appear in a label statement.
405\end{enumerate}
406The function definition thus becomes:
407\begin{lstlisting}[language=matita]
408record internal_function : Type[0] ≝
409{ f_return    : option typ
410; f_params    : list (ident × typ)
411; f_vars      : list (ident × typ)
412; f_stacksize : nat
413; f_body      : stmt
414; f_inv       : stmt_P (λs.stmt_vars (λi.Exists ? (λx.\fst x = i) (f_params @ f_vars)) s ∧
415                           stmt_labels (λl.Exists ? (λl'.l' = l) (labels_of f_body)) s) f_body
416}.
417\end{lstlisting}
418where \lstinline'stmt_vars' and \lstinline'stmt_labels' return the
419variables and labels that appear directly in a statement (but not
420substatements), and
421\lstinline'labels_of' returns a list of all the labels defined in a
422statement.
423
424The \textsf{Clight} semantics can be amended to use these invariants, although
425the main benefit is for the compiler stages (see the accompanying deliverable
4263.2 for details).  The semantics require the invariants to be added to the
427state and continuations.  It was convenient to split the continuations between
428the local continuation representing the rest of the code to be executed within
429the function, and the stack of function calls.  The invariant for variables is
430slightly different --- we require that every variable appear in the local
431environment.  We use \lstinline'f_inv' from the function to establish this
432invariant when the environment is set up on function entry.
433
434It is unclear whether changing the semantics is really worthwhile.  It
435witnesses that the invariants are those we wanted, but makes no difference to
436the actual execution of the program, especially as the execution can still
437fail due to runtime errors.  Moreover, it is unclear what effect the presence
438of proof terms and more dependent pattern matching in the semantics will have
439on the complexity of future correctness proofs.  We plan to examine this issue
441
442We use a similar method to specify the invariant that the \textsf{RTLabs}
443graph is closed --- that is, any successor labels in a statement in the graph
444are present in the graph.  The definition is simpler in \textsf{RTLabs}
445because the flat representation of the graph does not require recursive
446definitions like \lstinline'stmt_P' above.
447
448\section{Conclusion}
449
450\bibliographystyle{plain}
451\bibliography{report}
452
453\end{document}
Note: See TracBrowser for help on using the repository browser.