source: Deliverables/D3.2/Report/report.tex @ 1235

\documentclass[11pt,epsf,a4wide]{article}
\usepackage[mathletters]{ucs}
\usepackage[utf8x]{inputenc}
\usepackage{listings}
\usepackage{../../style/cerco}
\newcommand{\ocaml}{OCaml}
\newcommand{\clight}{Clight}
\newcommand{\matita}{Matita}
\newcommand{\sdcc}{\texttt{sdcc}}

\newcommand{\textSigma}{\ensuremath{\Sigma}}

% LaTeX Companion, p 74
\newcommand{\todo}[1]{\marginpar{\raggedright - #1}}

\lstdefinelanguage{coq}
  {keywords={Definition,Lemma,Theorem,Remark,Qed,Save,Inductive,Record},
   morekeywords={[2]if,then,else},
  }

\lstdefinelanguage{matita}
  {keywords={definition,lemma,theorem,remark,inductive,record,qed,let,rec,match,with,Type,and,on},
   morekeywords={[2]whd,normalize,elim,cases,destruct},
   mathescape=true,
   morecomment=[n]{(*}{*)},
  }

\lstset{language=matita,basicstyle=\small\tt,columns=flexible,breaklines=false,
        keywordstyle=\color{red}\bfseries,
        keywordstyle=[2]\color{blue},
        commentstyle=\color{green},
        stringstyle=\color{blue},
        showspaces=false,showstringspaces=false}

\lstset{extendedchars=false}
\lstset{inputencoding=utf8x}
\DeclareUnicodeCharacter{8797}{:=}
\DeclareUnicodeCharacter{10746}{++}
\DeclareUnicodeCharacter{9001}{\ensuremath{\langle}}
\DeclareUnicodeCharacter{9002}{\ensuremath{\rangle}}


\title{
INFORMATION AND COMMUNICATION TECHNOLOGIES\\
(ICT)\\
PROGRAMME\\
\vspace*{1cm}Project FP7-ICT-2009-C-243881 \cerco{}}

\date{ }
\author{}

\begin{document}
\thispagestyle{empty}

\vspace*{-1cm}
\begin{center}
\includegraphics[width=0.6\textwidth]{../../style/cerco_logo.png}
\end{center}

\begin{minipage}{\textwidth}
\maketitle
\end{minipage}


\vspace*{0.5cm}
\begin{center}
\begin{LARGE}
\bf
Report n. D3.2\\
CIC encoding: Front-end\\
\end{LARGE} 
\end{center}

\vspace*{2cm}
\begin{center}
\begin{large}
Version 1.0
\end{large}
\end{center}

\vspace*{0.5cm}
\begin{center}
\begin{large}
Main Authors:\\
Brian~Campbell
\end{large}
\end{center}

\vspace*{\fill}
\noindent
Project Acronym: \cerco{}\\
Project full title: Certified Complexity\\
Proposal/Contract no.: FP7-ICT-2009-C-243881 \cerco{}\\

\clearpage \pagestyle{myheadings} \markright{\cerco{}, FP7-ICT-2009-C-243881}

\newpage

\vspace*{7cm}
\paragraph{Abstract}
We describe the translation of the front end of the \cerco{} compiler from the
\ocaml{} prototype to the Calculus of Inductive Constructions (CIC) in the
\matita{} proof assistant.  This transforms programs in the C-like
\textsf{Clight} language to the \textsf{RTLabs} language, which is reasonably
target-independent and in the form of a control flow graph.

We also report on progress enriching these transformations with dependent
types so as to establish key invariants in each intermediate language, which
will assist in future work proving correctness properties of the compiler.

\newpage 

\tableofcontents

% TODO: clear up any -ize vs -ise
% TODO: clear up any "front end" vs "front-end"
% TODO: clear up any mentions of languages that aren't textsf'd.
% TODO: fix unicode in listings
% TODO: make it clear that our correctness is intended to go beyond compcert's

\section{Introduction}

The \cerco{} compiler has been prototyped in \ocaml{}~\cite{d2.1,d2.2}, but
the certified compiler will be a program written in the Calculus of Inductive
Constructions (CIC), as realised by the \matita{} proof assistant.  This
deliverable reports on the translation of the front-end of the compiler into
CIC and the subsequent efforts to start exploiting dependent types to maintain
invariants and rule out potential sources of failure in the compiler.

The input language for the formalized compiler is the \textsf{Clight}
language.  This is a C-like language with side-effect free expressions that
was adapted from the CompCert project~\cite{compcertfm06}\footnote{We will
also use their CIL-based C parser to generate \textsf{Clight} abstract syntax
trees, but will not formalize this code.} and provided with an executable
semantics.  See~\cite{d3.1} for more details on the syntax and semantics.

\begin{figure}
\begin{tabbing}
\quad \= $\downarrow$ \quad \= \kill
\textsf{C} (unformalized)\\
\> $\downarrow$ \> CIL parser (unformalized \ocaml)\\
\textsf{Clight}\\
\> $\downarrow$ \> cast removal\\
\> $\downarrow$ \> add runtime functions\\
\> $\downarrow$ \> labelling\\
\> $\downarrow$ \> stack variable allocation and control structure
 simplification\\
\textsf{Cminor}\\
\> $\downarrow$ \> generate global variable initialisation code\\
\> $\downarrow$ \> transform to RTL graph\\
\textsf{RTLabs}\\
\> $\downarrow$ \> start of target specific backend\\
\ \  \dots
\end{tabbing}
\caption{Front-end languages and transformations}
\label{fig:summary}
\end{figure}

The front-end of the compiler is summarised in Figure~\ref{fig:summary}.  The
two intermediate languages involved are
\begin{description}
\item[\textsf{Cminor}] --- a C-like language where local variables are no
longer held explicitly in memory and control structures are simpler

\item[\textsf{RTLabs}] --- a language in the form of a control flow graph but
retaining the front end operations from \textsf{Cminor}
\end{description}
More details on the formalisation of the syntax and semantics of these
languages can be found in the accompanying deliverable 3.4.
Development of the formalized front-end was conducted in concert with the
development of these intermediate languages to facilitate testing.

\subsection{Revisions to the prototype compiler}

We have been tracking revisions to the prototype compiler during the
development of the formalized version.  These were usually minor, with the
exception of the following major revision to the compiler.

The original plan for the front-end featured a \textsf{Clight} to
\textsf{Clight8} phase near the start which replaced all of the integer
values and operations by 8 bit counterparts, while pointers were split into
bytes at a later stage.  Experimentation found that it would be difficult to
produce good code with this approach.  Instead, we now have:
\begin{itemize}
\item full size integers, pointers and operations until code selection (the
first part of the back-end after \textsf{RTLabs}), and
\item a cast removal stage which simplifies \textsf{Clight} expressions such
as
\begin{lstlisting}[language=C]
  (char)((int)x + (int)y)
\end{lstlisting}
which are produced by integer promotion built into the CIL parser into
equivalent operations on simpler types, \lstinline'x+y' in this case.
\end{itemize}

This document describes the formalized front end after these changes.

\section{Clight phases}

In addition to the conversion to \textsf{Cminor}, there are several
transformations that act directly on the \textsf{Clight} language.

\subsection{Cast simplification}

We noted above that the arithmetic promotion required by C (and implemented in
the CIL-based parser) adds numerous casts, causing arithmetic operations to be
performed on 32 bit integers.  If left alone, the resulting code will be
larger and slower.  This phase removes many of the casts so that the
operations can be performed more efficiently.

The prototype version worked by recognising fixed patterns in the
\textsf{Clight} abstract syntax tree such as 
\[ (t)((t_1)e_1 op (t_2)e_2) \]
subject to restrictions on the types, and replaces them with a simpler
version.  These deep pattern matches are slightly awkward in \matita{} and
they do not capture compositions of operations, such as
\begin{lstlisting}[language=C]
(char)((int)a + (int)b + (int)c)
\end{lstlisting}
where \lstinline'a', \lstinline'b' and \lstinline'c' are of type
\lstinline'char'.

The formalized version uses a different method, recursively examining each
expression constructor to see if the expression can be coerced to some
`desired' type.  For example, when processing the above expression it reaches
each \lstinline'int' cast with a desired type of \lstinline'char', notes that
the subexpression is of type \lstinline'char' and eliminates the cast.
Moreover, when the recursive processing is complete the \lstinline'char' cast
is also eliminated because its subexpression is now of the correct type.

This has been formalized in \matita.  We have also performed a few proofs that
the arithmetic behind these changes is correct to gain confidence in the
technique.  During task 3.4 we will extend these proofs to cover more
operations and show that the semantics of the expressions are equivalent, not
just the underlying arithmetic.

\subsection{Labelling}

This phase adds cost labels to the \textsf{Clight} program.  It is a fairly
simple recursive definition, and was straightforward to port to \matita.  The
generation of cost labels was handled by our generic identifiers code,
described in the accompanying deliverable 3.3 on intermediate languages.

\subsection{Runtime functions}
% TODO: this hasn't been implemented yet

\subsection{Conversion to Cminor}

The conversion to \textsf{Cminor} performs two essential tasks.  First, it
determines which local variables need to be stored in memory and generates
explicit memory accesses for them.  Second, it must translate the control
structures (\lstinline'for', \lstinline'while', \dots) into \textsf{Cminor}'s
more basic structures.

These are both performed by code similar to that in the prototype, although
the use of generic fold operations on statements and expressions has been
replaced by simpler recursive definitions.

There are two additional pieces of work that the formalized translation must
do.  The \textsf{Cminor} definition features some mild constraints of the
types of expressions, which we can enforce in the translation using some type
checking.  The error monad is used to dispose of ill-typed \textsf{Clight}
programs.

The other difficulty is that we need to generate fresh temporary variables to
store function results in before they are written to memory.  This is
necessary because \textsf{Clight} allows arbitrary \emph{lvalue} expressions
as the destination for the returned value, but \textsf{Cminor} only allows
local variables.  However, the variable names are supplied with the input
program, but without any method for generating fresh names.

Our identifiers are based on binary numbers, and generation of fresh names is
handled by keeping track of the highest allocated number.  Thus we create a
new name generator from the input program by finding the maximum number used.

\section{Cminor phases}

Only two phases deal with \textsf{Cminor} programs:

\subsection{Initialisation code}

This replaces the initialisation data with explicit code in the main function.
The only remarkable point in the formalization is that we have two slightly
different instantiations of the \textsf{Cminor} syntax: one with
initialisation data that this pass takes as input, and one with only size
information that is the output.  In addition to reflecting the purpose of this
pass in the types, it also ensures that it cannot be accidentally left out.

\subsection{Conversion to RTLabs}

This pass breaks down the structure of the \textsf{Cminor} program into a
control flow graph, but maintains the same set of operations.  The algorithm
is stateful in the sense that it builds up the \textsf{RTLabs} function body
incrementally, but all of the relevant state is already present in the
function record (including the fresh register and graph label name generators)
and the prototype passes this around.  Thus the formalized code is very
similar in nature.

One possible variation would be to explicitly define a state monad to carry
the function under construction around, but it is not yet clear if this will
make the correctness easier to prove.

\section{Adding and using invariants}

The compiler phases described above all use the error monad to deal with
inconsistencies in the program being transformed.  In particular, lookups in
environments may fail, control flow graphs may have missing statements and
various structural problems may be present.  We would like to show that these
failures are absent where possible by establishing that programs are well
formed early in the compilation process.

This work overlaps with deliverable 3.3 (where more details of the additions
to the syntax and semantics of the intermediate languages can be found) and
task 3.4 on the correctness of the compiler.  Thus this work is experimental
in nature, and will evolve during task 3.4.

Invariants on \textsf{Cminor} programs are defined using a higher order
predicate which applies a given predicate to a statement and recursively to
each of its substatements (and expressions and subexpressions, respectively).

Thus during the \textsf{Clight} to \textsf{Cminor} stage the values returned
are not just \textsf{Cminor} expressions and statements, but dependent pairs
that also return invariants to establish that only local variables appear in
the generated terms, and all labels appearing in \texttt{goto} statements are
defined in the result.  The latter is proved by showing two properties: first
by checking whether the labels are in the set defined by the original
\textsf{Clight} function body, and second that the translation preserves the
set of label statements.

These two properties are used at the end of translation to show the invariant
attached to \textsf{Cminor} \emph{functions}: that all \texttt{goto} labels
are defined in the body.  Similarly, the invariant for variables is slightly
different to the translation's: we go from the fact that every variable was
classified as local to the appearance of every variable in the locals or
parameters.  This is done using a lemma showing that the classification only
allows parameters and locals to be classed as `local'.

The next translation to \textsf{RTLabs}\dots

\section{Conclusion}

\bibliographystyle{plain}
\bibliography{report}

\end{document}