source: Deliverables/D2.1/Revision/text-report.tex @ 3194

\section{Introduction}\label{intro-sec}
The formal description and certification of software components is
reaching a certain level of maturity with impressing case studies
ranging from compilers to kernels of operating systems.  A
well-documented example is the proof of functional correctness of a
moderately optimizing compiler from a large subset of the $\C$ language
to a typical assembly language of the kind used in embedded systems 
\cite{Leroy09}.

In the framework of the {\em Certified Complexity} ($\cerco$) project~\cite{Cerco10}, we
aim to refine this line of work by focusing on the issue of the {\em
execution cost} of the compiled code.  Specifically, we aim to build a
formally verified $\C$ compiler that given a source program produces
automatically a functionally equivalent object code plus an annotation
of the source code which is a sound and precise description
of the execution cost of the object code.

We target in particular the kind of $\C$ programs produced for embedded
applications; these programs are eventually compiled to binaries
executable on specific processors.  The current state of the art in
commercial products such as $\scade$~\cite{SCADE,Fornari10} is that the {\em reaction
time} of the program is estimated by means of abstract interpretation
methods (such as those developed by $\absint$~\cite{AbsInt,AbsintScade}) that operate on the
binaries.  These methods rely on a specific knowledge of the
architecture of the processor and may require explicit annotations of
the binaries to determine the number of times a loop is iterated (see,
{\em e.g.},~\cite{W09} for a survey of the state of the art).

In this context, our aim is to produce a mechanically verified
compiler which can {\em lift} in a provably correct way the pieces of
information on the execution cost of the binary code to cost
annotations on the source $\C$ code.  Eventually, we plan to
manipulate the cost annotations with automatic tools such as
$\framac$~\cite{Frama-C} to infer more synthetic cost annotations.  In
order to carry on our project, we need a clear and flexible picture
of: (i) the meaning of cost annotations, (ii) the method to prove them
sound and precise, and (iii) the way such proofs can be composed.  Our
purpose here is to propose a methodology addressing these three
questions and to consider its concrete application to a simple toy
compiler and to a moderately optimizing untrusted $\C$ compiler.


\paragraph{Meaning of cost annotations}
The execution cost of the source programs we are interested in depends on
their control structure. Typically, the source programs are composed
of mutually recursive procedures and loops and their execution cost
depends, up to some multiplicative constant, on the number of times
procedure calls and loop iterations are performed.
Producing a {\em cost annotation} of a  source program  amounts to:
\begin{itemize}

\item enrich the program with a  collection of {\em global cost variables} 
to measure resource consumption (time, stack size, heap size,$\ldots$)

\item inject suitable code at some critical points (procedures, loops,$\ldots$) to keep track of the execution cost.  

\end{itemize}

Thus producing a cost-annotation of a source program $P$ amounts to
build an {\em annotated program} $\w{An}(P)$ which behaves as $P$
while self-monitoring its execution cost. In particular, if we do {\em
  not} observe the cost variables then we expect the annotated
program $\w{An}(P)$ to be functionally equivalent to $P$.  Notice that
in the proposed approach an annotated program is a program in the
source language. Therefore the meaning of the cost
  annotations is automatically defined by the semantics of the source
language and tools developed to reason on the source programs 
can be directly applied to the annotated programs too. 


\paragraph{Soundness and precision of cost annotations}
Suppose we have a functionally correct compiler $\cl{C}$ that
associates with a program $P$ in the source language a program
$\cl{C}(P)$ in the object language.  Further suppose we have some
obvious way of defining the execution cost of an object code. For
instance, we have a good estimate of the number of cycles needed for
the execution of each instruction of the object code.  Now the
annotation of the source program $\w{An}(P)$ is {\em sound} if its
prediction of the execution cost is an upper bound for the `real'
execution cost. Moreover, we say that the annotation is {\em precise}
with respect to the cost model if the {\em difference} between the
predicted and real execution costs is bounded by a constant which
depends on the program.


\paragraph{Compositionality}\label{comp-intro}
In order to master the complexity of the compilation process (and its
verification), the compilation function $\cl{C}$ must be regarded as 
the result of the composition of a certain number of program transformations
$\cl{C}=\cl{C}_{k} \comp \cdots \comp \cl{C}_{1}$. 
When building a system of
cost annotations on top of an existing compiler  
a certain number of problems arise.
First, the estimated cost of executing a piece of source code
is determined only at the {\em end} of the compilation process.
Thus while we are used to define the compilation 
functions $\cl{C}_i$ in increasing order (from left to right),
the annotation function $\w{An}$ is the result of 
a progressive abstraction from 
the object to the source code (from right to left).
Second, we must be able to foresee in the source language 
the looping and branching  points of the object code. 
Missing a loop may lead to unsound cost annotations
while missing a branching point may lead to rough cost
predictions. This means that we must have a rather good
idea of the way the source code will eventually be compiled
to object code.
Third, the definition of the annotation of the source 
code depends heavily on {\em contextual information}. For instance,
the cost of the compiled code associated with 
a simple expression such as $x+1$ will depend on the
place in the memory hierarchy where the variable $x$ is allocated.
A previous experience described 
%in~\cite{CercoDeliverable} 
in appendix \ref{direct-sec}
suggests that the process
of pushing `hidden parameters' in the definitions of cost annotations
and of manipulating directly numerical cost is error prone and 
produces complex proofs. For this reason, we advocate next a 
`labelling approach' where costs are handled at
an abstract level and numerical values are produced at the very end of the
construction.





%% \subsection{Direct approach to cost annotations}\label{direct-intro}
%% A first `direct' approach to the problem of building
%% cost annotations is summarised by the following diagram.

%% %% {\footnotesize
%% %% \[
%% %% \begin{array}{cccccc}

%% %%       &\cl{C}_{1}   &          &                &\cl{C}_{k}              \\

%% %% L_1   &\arrow        &L_2      &\cdots        &\arrow       &L_{k+1}        \\

%% %% \ \quad\downarrow \w{An}_1
%% %% &
%% %% &\ \quad\downarrow \w{An}_2
%% %% &
%% %% &
%% %% &\ \quad\downarrow \w{An}_{k+1} \\

%% %% L_1   &             &L_2       &      & &L_{k+1}        \\

%% %% \end{array}
%% %% \]}

%% \[
%% \xymatrix{
%% % Row 1
%%   L_1 \ar[d]^{An_1} \ar[r]^{\cl{C}_1} 
%% & L_2 \ar[d]^{An_1}  
%% & \ldots \hspace{0.3cm}\ar[r]^{\cl{C}_k} 
%% & L_{k+1} \ar[d]^{An_{k+1}}  \\
%% % Row 2
%%   L_1                                  
%% & L_2   
%% & & L_{k+1}
%% }
%% \]

%% With respect to our previous discussion,  $L_1$ is the source
%% language with the related annotation function $\w{An}_1$ while
%% $L_{k+1}$ is the object language with a related annotation
%% $\w{An}_{k+1}$. This annotation of the object code is supposed to be truly
%% straightforward and it is taken as an `axiomatic' definition of
%% the `real' execution cost of the program. 
%% The languages $L_i$, for $2\leq i \leq k$, are
%% intermediate languages which are also equipped with increasingly `realistic' 
%% annotation functions.
%% Suppose we denote with $S$ the source program,
%% with $\cl{C}(S)$ the compiled program, and 
%% that we write $(P,s)\eval s'$ to mean that
%% the (source or object) program $P$ in the state $s$
%% terminates successfully in the state $s'$.
%% The soundness proof of the compilation function
%% guarantees that if $(S,s)\eval s'$ then 
%% $(\cl{C}(S),s)\eval s'$.
%% In the direct approach, the {\em proof of soundness} of
%% the cost annotations amounts to lift the proof of functional
%% equivalence of the source program and the object code to a proof of
%% `quasi-equivalence' of the respective instrumented codes.
%% Suppose we write $s[c/\w{cost}]$ for a state that associates $c$
%% with the cost variable $\w{cost}$. Then what we want to show is 
%% that whenever $(\w{An}_{1}(S),s[c/\w{cost}])\eval s'[c'/\w{cost}]$ 
%% we have that $(\w{An}_{k+1}(\cl{C}(S)),s[d/\w{cost}])\eval s'[d'/\w{cost}]$
%% and $|d'-d|\leq |c'-c|+k$.
%% This means that the increment in the annotated source program bounds up to 
%% an additive constant the increment in the annotated object program.
%% We will also say that the cost annotation is precise if we can also prove that
%% $|c'-c|\leq |d'-d|$, {\em i.e.}, the `estimated' cost is not too far
%% away from the `real' one. 
%% We will see that while in theory one can build sound and precise
%% annotation functions, in practice definitions and proofs become
%% unwieldy.



\paragraph{Labelling approach to cost annotations}\label{label-intro}
The `labelling' approach to the problem of building
cost annotations is summarized in the following diagram.

%% {\footnotesize
%% \[
%% \begin{array}{c||l}

%% \begin{array}{cccccc}


%% L_1      &         &                     &                          &                & \\

%% \quad\uparrow {\cal I}      &\cl{C}_{1}   &  &      &\cl{C}_{k}         &     \\

%% L_{1,\ell}   &\arrow        &L_{2,\ell}         &\cdots       &\arrow       &L_{k+1,\ell}        \\

%% \quad \cl{L} \uparrow \ \downarrow \w{er}_{1}
%% &
%% &\ \quad\downarrow \w{er}_{2}
%% &&
%% &\ \quad\downarrow \w{er}_{k+1} \\ 

%% L_{1}   &\arrow             &L_{2}        &\cdots     &\arrow &L_{k+1}        \\

%%       &\cl{C}_{1}   &                     &     &\cl{C}_{k}              \\
%% \end{array}

%% &\begin{array}{ccc}

%% \w{er}_{i+1} \comp \cl{C}_{i} &= &\cl{C}_{i} \comp \w{er}_{i} \\

%% \w{er}_{1} \comp \cl{L} &= &\w{id}_{L_{1}} \\ 

%% \w{An}_{1} &= &\cl{I} \comp \cl{L}  


%% \end{array}
%% \end{array}
%% \]
%% }
\newcolumntype{M}[1]{>{\raggedright}m{#1}}
\-
{\footnotesize

\begin{tabular}{M{8cm}||M{3cm}}
$$
\xymatrix{
% Row 1
  L_1 \\
%
% Row 2
  L_{1,\ell} 
  \ar[u]^{\cl{I}}
  \ar@/^/[d]^{\w{er}_1} 
  \ar[r]^{\cl{C}_1} 
%
& L_{2,\ell} 
  \ar[d]^{\w{er}_2}  
%
& \ldots \hspace{0.3cm}\ar[r]^{\cl{C}_k} 
%
& L_{k+1, \ell} 
  \ar[d]^{\w{er}_{k+1}}  \\
%
% Row 3
  L_1                                  
  \ar@/^/[u]^{\cl{L}} 
  \ar[r]^{\cl{C}_1}
& L_2   
& \ldots\hspace{0.3cm}
  \ar[r]^{\cl{C}_{k}}
& L_{k+1}
}
$$
&
$$
\begin{array}{ccc}
\w{er}_{i+1} \comp \cl{C}_{i} &= &\cl{C}_{i} \comp \w{er}_{i} \\

\w{er}_{1} \comp \cl{L} &= &\w{id}_{L_{1}} \\ 

\w{An} &= &\cl{I} \comp \cl{L}  
\end{array}
$$
\end{tabular}
}
\-

For each language $L_i$ considered in the compilation process,
we define an extended {\em labelled} language $L_{i,\ell}$ and an
extended operational semantics. The labels are used to mark
certain points of the control. The semantics makes sure 
that whenever we cross a labelled control point a labelled and observable
transition is produced.

For each labelled language there is an obvious function $\w{er}_i$
erasing all labels and producing a program in the corresponding
unlabelled language.
The compilation functions $\cl{C}_i$ are extended from the unlabelled
to the labelled language so that they enjoy commutation 
with the erasure functions. Moreover, we lift the soundness properties of
the compilation functions from the unlabelled to the labelled languages
and transition systems.

A {\em labelling} $\cl{L}$  of the source language $L_1$ is just a function 
such that $\w{er}_{L_{1}} \comp \cl{L}$ is the identity function.
An {\em instrumentation} $\cl{I}$ of the source labelled language  $L_{1,\ell}$
is a function replacing the labels with suitable increments of, say, 
a fresh global \w{cost} variable. Then an {\em annotation} $\w{An}$ of the 
source program can be derived simply as the composition of the labelling
and the instrumentation functions: $\w{An} = \cl{I}\comp \cl{L}$.

Suppose $s$ is some adequate representation
of the state of a program. Let $P$ be a source program and suppose
that its annotation satisfies the following property:
\begin{equation}\label{STEP1}
(\w{An}(P),s[c/\w{cost}])  \eval s'[c+\delta/\w{cost}]
\end{equation}
where $c$ and $\delta$ are some non-negative numbers.
Then the definition of the instrumentation and the fact that
the soundness proofs of the compilation functions have been lifted
to the labelled languages allows to conclude that
\begin{equation}\label{step2}
(\cl{C}(\cl{L}(P)),s[c/\w{cost}])  \eval (s'[c/\w{cost}],\lambda)
\end{equation}
where $\cl{C} = \cl{C}_{k} \comp \cdots \comp \cl{C}_{1}$ and
$\lambda$ is a sequence (or a multi-set) of labels whose `cost'
corresponds to the number $\delta$ produced by the 
annotated program.
Then the commutation properties of erasure and compilation functions
allows to conclude that the {\em erasure} of the compiled
labelled code $\w{er}_{k+1}(\cl{C}(\cl{L}(P)))$ is actually  equal to 
the compiled code $\cl{C}(P)$ we are interested in.
Given this, the following question arises: 
under which conditions 
the sequence $\lambda$, {\em i.e.}, the increment $\delta$,
is a sound and possibly precise description of the
execution cost of the object code? 

To answer this question, we observe that the object code we are
interested in is some kind of assembly code and its control flow can
be easily represented as a control flow graph. The fact that we have
to prove the soundness of the compilation functions means that we have
plenty of information on the way the control flows in the compiled
code, in particular as far as procedure calls and returns are
concerned.  These pieces of information allow to build a rather
accurate representation of the control flow of the compiled code at
run time.

The idea is then to perform two simple checks on the control flow
graph. The first check is to verify that all loops go through a labelled node.
If this is the case then we can associate a finite cost with
every label and prove that the cost annotations are sound.
The second check amounts to verify that all paths starting from 
a label have the same cost. If this check is successful then we can
conclude that the cost annotations are precise. 

\paragraph{A toy compiler}\label{toy-intro}
As a first case study for the labelling approach to cost
annotations we have sketched, we introduce a
{\em toy compiler} which is summarized by the
following diagram.
%% {\footnotesize
%% \[
%% \begin{array}{ccccc}

%%       &\cl{C}          &                   &\cl{C'}              \\

%% \imp   &\arrow        &\vm                &\arrow       &\mips        

%% \end{array}
%% \]}

{\footnotesize\[
\xymatrix{
\imp 
\ar[r]^{\cl{C}}
& \vm 
\ar[r]^{\cl{C'}}
& \mips
}
\]}%

The three languages considered can be shortly described as follows:
$\imp$ is a very simple imperative language
with pure expressions, branching and looping commands,
$\vm$ is an assembly-like language enriched with a stack, and
$\mips$ is a $\mips$-like assembly language with
registers and main memory.
The first compilation function $\cl{C}$ relies on the stack 
of the $\vm$ language to implement expression evaluation while
the second compilation function $\cl{C'}$ allocates (statically)
the base of the stack in the registers and the rest in main memory.
This is of course a naive strategy but it suffices to expose
some of the problems that arise in defining a compositional approach.

\paragraph{A C compiler}\label{Ccompiler-intro}
As a second, more complex, case study we consider a $\C$
compiler. Even if the long-term agenda of the $\cerco$ project is to
build a mechanically verified compiler using a proof assistant, we
only developed an untrusted compiler prototype in $\ocaml$ in
order to first experiment with the scalability of our approach.  The
architecture of this prototype is summarized by the following
diagram:

{\footnotesize
\[
\begin{array}{cccccccccc}
&&\C &\arrow &\Clight &\arrow &\Cminor &\arrow &\RTLAbs &\qquad \mbox{(front end)}\\
                                              &&&&&&&&\downarrow \\
 \mips \text{ or } \intel &\leftarrow &\LIN &\leftarrow  &\LTL &\leftarrow  &\ERTL  &\leftarrow &\RTL &\qquad \mbox{(back-end)}
\end{array}
\]
}%

The structure follows rather closely the one of the $\compcert$
compiler~\cite{Leroy09}.  Notable differences are that some
compilation steps are fusioned, that the front-end goes till $\RTLAbs$
(rather than $\Cminor$) and that we target the $\mips$ and Intel~$\intel$
assembly languages (rather than $\powerpc$).  These differences are
contingent to the way we built the compiler.  The compilation from
$\C$ to $\Clight$ relies on the $\cil$ front-end~\cite{CIL02}. The one
from $\Clight$ to $\RTL$ has been programmed from scratch and it is
partly based on the $\coq$ definitions available in the $\compcert$
compiler.  Finally, the back-end from $\RTL$ to $\mips$ is based on a
compiler developed in $\ocaml$ for pedagogical
purposes~\cite{Pottier}.  We extended this back-end to also target the
Intel~$\intel$~\cite{intel94}, an 8bits micro-controller used in embedded systems.
\footnote{According to \cite{share}, in 2008  $\intel$ was the most diffused processor in the
microcontroller market with a 19\% market share.}
The main optimizations the back-end performs are
liveness analysis and register allocation  and graph compression. We
ran some benchmarks to ensure that our prototype implementation is
realistic. The results are given in
appendix~\ref{C-compiler-benchmarks} and the compiler is available
from the authors.

\paragraph{Organization}
The rest of the paper is organized as follows. 
Section~\ref{label-toy-sec} describes the application of
the labelling approach to the toy compiler.
Section~\ref{C-label-sec} reports our experience in implementing
and testing the labelling approach on the $\C$ compiler.
Section~\ref{conclusion-sec} summarizes our contribution and 
outlines some perspectives for future work.
Appendix~\ref{toy-compiler-sec} gives standard definitions that
are skipped in the presentation for the sake of conciseness. 
Appendix~\ref{paper-proofs} sketches the proofs that have not
been mechanically checked in $\coq$ and
appendix~\ref{C-compiler-sec}  provides some details on the
structure of the $\C$ compiler we have implemented.
Appendix~\ref{direct-sec} describes a {\em direct approach}
to cost annotations that in our experience fails to scale to 
a realistic compiler architecture and 
appendix~\ref{related-sec} discusses informally some related approaches.

\section{Labelling approach for the toy compiler}\label{label-toy-sec}

\begin{figure}
{\footnotesize
\newcolumntype{M}[1]{>{\raggedright}m{#1}}
\begin{tabular}{M{6cm}M{4cm}}
$$
{\footnotesize\begin{array}{rcl}
\multicolumn{3}{l}{\textrm{Syntax for }\imp}\\
\w{id}&::=& x\Alt y\Alt \ldots       \\ % &\mbox{(identifiers)} \\
\w{n} &::=& 0 \Alt -1 \Alt +1 \Alt \ldots \\ % &\mbox{(integers)} \\
v &::=& n \Alt \s{true} \Alt \s{false}  \\ %&\mbox{(values)} \\
e &::=& \w{id} \Alt n \Alt e+e  \\ %  &\mbox{(numerical expressions)} \\
b &::=& e<e  \\ % &\mbox{(boolean conditions)} \\
S &::=& \s{skip} \Alt \w{id}:=e \Alt S;S \\ 
  &\Alt& \s{if} \ b \ \s{then} \ S \ \s{else} \ S \\
  &\Alt& \s{while} \ b \ \s{do} \ S  \\ % &\mbox{(commands)} \\
P &::= & \s{prog} \ S    \\ %   &\mbox{(programs)}\\
\end{array}}
$$
&
$$
{\footnotesize
\begin{array}{rcl}
\multicolumn{3}{l}{\textrm{Syntax for }\vm}\\
instr_\vm &::=& {\tt cnst} (n) \Alt {\tt var}(n) \\ 
  &\Alt& {\tt setvar}(n) \Alt {\tt add} \\
  &\Alt& {\tt branch}(k) \Alt {\tt bge}(k) \Alt {\tt halt}\\
\\[0.1em]
\multicolumn{3}{l}{\textrm{Syntax for }\mips}\\
instr_\mips &::=& {\tt loadi }\, R, n \Alt {\tt load }\, R, l \\
  &\Alt& {\tt store }\, R, l \Alt {\tt add }\, R, R, R \\
  &\Alt& {\tt branch }\, k \Alt {\tt bge }\, R, R, k \Alt {\tt halt}
\end{array}}
$$
\end{tabular}
}
\caption{Syntax definitions.}
\label{fig:syntaxes}
\end{figure}

A first case study for the labelling approach is performed on a toy
compiler. The syntax of the source, intermediate and target languages
is given in the Figure~\ref{fig:syntaxes}. The semantics of $imp$ is
defined over configurations $(S,K,s)$ where $S$ is a statement, $K$ is
a continuation and $s$ is a state. A {\em continuation} $K$ is a list
of commands which terminates with a special symbol \s{halt}. The
semantics of $\vm$ is defined over stack-based machine configurations
$C \vdash (i, \sigma, s)$ where $C$ is a program, $i$ is a program
counter, $\sigma$ is a stack and $s$ is a state. The semantics of
$\mips$ is defined over register-based machine configurations
$C \vdash (i, m)$ where $C$ is a program, $i$ is a program counter and
$m$ is a machine memory (with registers and main memory). The
compilation functions $\cl{C}$ from $\imp$ to $\vm$ and $\cl{C'}$ from
$\vm$ to $\mips$ are standard and thus eluded.  (see
Appendix~\ref{toy-compiler-sec} for formal details about semantics and
the compilation chain.)

We apply the labelling approach introduced in section 
\ref{label-intro} to this toy compiler which results in the following
diagram.

{\footnotesize

\newcolumntype{M}[1]{>{\raggedright}m{#1}}
\begin{tabular}{M{7cm}||M{3cm}}
$$
\xymatrix{
% Row 1
  \imp \\
%
% Row 2
  \imp_\ell
  \ar[u]^{\cl{I}}
  \ar@/^/[d]^{\w{er}_\imp} 
  \ar[r]^{\cl{C}} 
%
& \vm_\ell
  \ar[d]^{\w{er}_\vm}  
  \ar[r]^{\cl{C}'} 
%
& \mips_\ell
  \ar[d]^{\w{er}_{\mips}}  \\
%
% Row 3
  \imp                
  \ar@/^/[u]^{\cl{L}} 
  \ar[r]^{\cl{C}}
& \vm   
  \ar[r]^{\cl{C}'}
& \mips
}
$$
&
$$
\begin{array}{ccc}
\w{er}_\vm \comp \cl{C} &= &\cl{C} \comp \w{er}_{\imp} \\

\w{er}_\mips \comp \cl{C'} &= &\cl{C'} \comp \w{er}_{\vm} \\

\w{er}_\imp \comp \cl{L} & = & id_{\imp} \\

\w{An}_\imp &= &\cl{I} \comp \cl{L}  
\end{array}
$$
\end{tabular}}


%% {\footnotesize
%% \[
%% \begin{array}{c||l}

%% \begin{array}{ccccc}


%% \imp      &         &                                               &                & \\

%% \quad\uparrow {\cal I}      &\cl{C}   &        &\cl{C'}         &     \\

%% \imp_{\ell}   &\arrow        &\vm_{\ell}                &\arrow       &\mips_{\ell}        \\

%% \quad \cl{L} \uparrow \ \downarrow \w{er}_{\imp}
%% &
%% &\ \quad\downarrow \w{er}_{\vm}
%% &
%% &\ \quad\downarrow \w{er}_{\mips} \\ 

%% \imp   &\arrow             &\vm             &\arrow &\mips        \\

%%       &\cl{C}   &                          &\cl{C'}              \\
%% \end{array}

%% &\begin{array}{ccc}

%% \w{er}_{\vm} \comp \cl{C} &= &\cl{C} \comp \w{er}_{\imp} \\

%% \w{er}_{\mips} \comp \cl{C'} &= &\cl{C'} \comp \w{er}_{\vm} \\

%% \w{er}_{\imp} \comp \cl{L} &= &\w{id}_{\imp} \\ 

%% \w{An}_{\imp} &= &\cl{I} \comp \cl{L}  


%% \end{array}
%% \end{array}
%% \]
%% }


\subsection{Labelled $\imp$}
We extend the syntax so that statements
%lab-bool and boolean conditions in \s{while} loops
can be labelled: $S::=  \ldots \Alt \ell:S$.
% 
% {\footnotesize
% \[
% \begin{array}{lll}
%
% \w{lb}  &::= \ell:b   &\mbox{(labelled boolean conditions)}\\
%S  &::= \ldots \Alt \ell:S \Alt \s{while} \ \w{lb} \ \s{do} \ S
%&\mbox{(labelled commands)}
%
%\end{array}
%\]}
%
For instance,
%lab-bool $\ell:(\s{while} \ \ell' : (n<x) \ \s{do} \ \ell:S )$
$\ell:(\s{while} \ (n<x) \ \s{do} \ \ell:S )$ is a labelled command.
% Also notice that the definition allows labels in commands to 
% be nested as in $\ell:(\ell':(x:=e))$, though this feature is not really used.
%lab-bool The evaluation predicate $\eval$ on labelled boolean conditions is extended as follows:
%lab-bool {\footnotesize \begin{equation} \infer{(b,s) \eval v} {(\ell:b,s) \eval (v,\ell)} \end{equation}}
%lab-bool So a labelled boolean condition evaluates into a pair  composed of a boolean value and a label.
The small step semantics of statements 
% defined in table \ref{small-step-imp}
is extended as described by the following rule.

{\footnotesize
\[
\begin{array}{lll}
(\ell:S,K,s) &\act{\ell} &(S,K,s) 

%lab-bool\\  \\
%% (\s{if} \ b \ \s{then} \ S \ \s{else} \ S',K,s) 
%% &\act{\ell} 
%% &\left\{
%% \begin{array}{ll}
%% (S,K,s) &\mbox{if }(b,s)\eval (\s{true},\ell) \\
%% (S',K,s) &\mbox{if }(b,s)\eval (\s{false},\ell)
%% \end{array}
%% \right. 
%% \\ \\


%\lab-bool (\s{while} \ \w{lb} \ \s{do} \ S ,K,s) &\act{\ell} &\left\{ \begin{array}{ll}
%\lab-bool (S,(\s{while} \ \w{lb} \ \s{do} \ S);K,s) &\mbox{if }(\w{lb},s)\eval (\s{true},\ell) \\
%\lab-bool (\s{skip},K,s) &\mbox{if }(\w{lb},s)\eval (\s{false},\ell)
%\lab-bool \end{array} \right. \\

\end{array}
\]}

We denote with $\lambda,\lambda',\ldots$
finite sequences of labels. In particular, we denote with $\epsilon$ the empty sequence
and identify an unlabelled transition with a transition labelled with $\epsilon$.
Then the small step reduction relation we have defined
on statements becomes a {\em labelled transition system}.
There is an obvious {\em erasure} function $\w{er}_{\imp}$ 
from the labelled language to the unlabelled one which is the identity on expressions
%lab-bool removes labels from labelled boolean conditions 
and boolean conditions, 
%lab-bool and is the identity on unlabelled ones, 
and traverses commands removing all labels.
We derive a {\em labelled} big-step semantics as follows:
$(S,s)\eval (s',\lambda)$ if $(S,\s{halt},s) \act{\lambda_1} \cdots \act{\lambda_n}  
                                             (\s{skip},\s{halt},s')$  and $\lambda =\lambda_1 \cdots \lambda_n$.




%(*** Stronger properties hold
%\Defitem{(1)}
%$(\w{er}(S),s) \eval s'$ iff $\xst{\lambda}{(S,s)\eval (s',\lambda)}$.
%\Defitem{(2)}
%$(\cl{I}(S),s[c/\w{cost}]) \eval s'[c+\delta/\w{cost}]$ iff 
%$\xst{\lambda}{\kappa(\lambda)=\delta \mbox{ and }(S,s[c/\w{cost}])\eval(s'[c/\w{cost}],\lambda)}$. ***)




\subsection{Labelled $\vm$}
We introduce a new instruction
$\s{nop}(\ell)$
whose semantics is defined as follows:

{\footnotesize
\[
C \Gives (i,\sigma,s) \act{\ell} (i+1,\sigma,s) \qquad \mbox{if }C[i]=\s{nop}(\ell)~.
\]}


The erasure function $\w{er}_{\vm}$ amounts to remove from a
$\vm$ code $C$ all the $\s{nop}(\ell)$ instructions and recompute jumps
accordingly. Specifically, let $n(C,i,j)$ be the number of \s{nop} instructions
in the interval $[i,j]$. Then, assuming $C[i]=\s{branch}(k)$ we replace the offset
$k$ with an offset $k'$ determined as follows:


{\footnotesize
\[
k' = 
\left\{
\begin{array}{ll}

k-n(C,i,i+k) &\mbox{if }k\geq 0 \\

k+n(C,i+1+k,i)   &\mbox{if }k<0

\end{array}
\right.
\]}
%
The compilation function $\cl{C}$ is extended to $\imp_\ell$ by defining:

{\footnotesize
\[
\begin{array}{llll}   
\cl{C}(\ell:b,k) &=(\s{nop}(\ell))\cdot \cl{C}(b,k) \qquad
&\cl{C}(\ell:S)   &=   (\s{nop}(\ell))\cdot \cl{C}(S)~.
\end{array}
\]}

\begin{proposition}\label{labelled-sim-imp-vm}
For all commands $S$ in $\imp_\ell$ we have that:

\Defitem{(1)} $\w{er}_{\vm}(\cl{C}(S)) = \cl{C}(\w{er}_{\imp}(S))$.

\Defitem{(2)} 
If $(S,s)\eval (s',\lambda)$ then $(\cl{C}(S),s)\eval(s',\lambda)$.
\end{proposition}


\begin{remark}
\label{rem:multi-set}
In the current formulation, 
a sequence of transitions $\lambda$ in the source code 
must be simulated by the same sequence of transitions
in the object code. However, in the actual computation
of the costs, the order of the labels occurring in the sequence is
immaterial. Therefore one may consider a more relaxed notion of simulation
where $\lambda$ is a multi-set of labels.
\end{remark}


\subsection{Labelled $\mips$}
The labelled extension of $\mips$ is similar to the one of $\vm$.
We add an instruction $\s{nop} \ \ell$ whose semantics is defined
as follows:
%

{\footnotesize
\[
\begin{array}{ll}
M\Gives (i,m) \act{\ell} (i+1,m)    &\mbox{if }M[i]=(\s{nop} \ \ell)~.
\end{array}
\]}
%
The {\em erasure function} $\w{er}_{\mips}$ is also similar to the one 
of $\vm$ as it amounts to remove from a $\mips$ code all the $(\s{nop} \ \ell)$ 
instructions and recompute jumps accordingly. 
The compilation function $\cl{C'}$ is extended to $\vm_\ell$ by 
simply translating $\s{nop}(\ell)$ as $(\s{nop} \ \ell)$:
%

{\footnotesize
\[
\begin{array}{ll}   
\cl{C'}(i,C) = (\s{nop} \ \ell)
&\mbox{if }C[i]=\s{nop}(\ell)
\end{array}
\]}
The evaluation predicate for labelled $\mips$ is defined as
$(M,m)\eval (m',\lambda)$
if 
$M\Gives (0,m) \act{\lambda_1} \cdots \act{\lambda_n}  (j,m')$, 
$\lambda =\lambda_1 \cdots \lambda_n$  and $M[j]=\s{halt}$.
%
%Assuming a function $\kappa$ which associates an integer number to 
%labels, and  distinct fresh locations $l_\w{cost},l_A,l_B$ not occurring in 
%the $\mips$ code $M$ under consideration,
%we define the instrumentation $\cl{I}_{\mips}(M)$ by replacing each instruction $(\s{nop}\ \ell)$ with
%the following sequence of instructions:
%{\footnotesize
%\[
%\begin{array}{l}
%(\s{store} \ A,l_{A}) \cdot
%(\s{store} \ B,l_{B}) \cdot
%(\s{loadi} \ A, \kappa(\ell)) \cdot
%(\s{load} \ B, l_{\w{cost}}) \cdot \\
%(\s{add} \ A, A, B) \cdot
%(\s{store} \ A,l_{\w{cost}}) \cdot
%(\s{load} \ A, l_{A}) \cdot
%(\s{load} \ B, l_{B})
%~,
%\end{array}
%\]}
%and adapting the offset of the branching instructions consequently.
%We write $m=_X m'$ if the memories $m$ and $m'$ coincide but for the
%locations in $X$.
%The following proposition is the analogous for $\mips$ code of proposition 
%\ref{lab-instr-erasure-imp} for $\imp$ commands.
%\begin{proposition}\label{lab-er-instr-mips}
%Let $M$ be a $\mips_\ell$ code. Then:
%\Defitem{(1)}
%$(\w{er}_{\mips}(M),m) \eval m'$ iff $\xst{\lambda}{(M,m)\eval (m',\lambda)}$.
%\Defitem{(2)}
%If  $(\cl{I}_{\mips}(M),m[c/l_{\w{cost}}]) \eval m'[c+\delta/l_{\w{cost}}]$ 
%then there is a $\lambda$ such that 
%$\kappa(\lambda)=\delta$ and a $m''$ such that 
%$(M,m)\eval(m'',\lambda)$ with 
%$m'=_{X}, m''$, and $X=\set{l_{\w{cost}},l_A,l_B}$.
%\Defitem{(3)}
%If $(M,m)\eval(m',\lambda)$ then 
%$(\cl{I}_{\mips}(M),m[c/l_{\w{cost}}]) \eval m''[c+\kappa(\lambda)/l_{\w{cost}}]$, 
%$m'=_{X} m''$, and $X=\set{l_{\w{cost}},l_A,l_B}$.
%\end{proposition}
%
The following proposition relates $\vm_\ell$ code and its compilation
and it is similar to proposition~\ref{labelled-sim-imp-vm}.
$m \real \sigma, s$ means ``the low-level
$\mips$ memory~$m$ realizes the $\vm$ stack~$\sigma$ and state $s$''.
%
\begin{proposition}\label{sim-vm-mips-prop}
Let $C$ be a $\vm_\ell$ code. Then:

\Defitem{(1)} $\w{er}_{\mips}(\cl{C'}(C)) = \cl{C'}(\w{er}_{\vm}(C))$.

\Defitem{(2)} 
If $(C,s) \eval (s',\lambda)$ and $m\real \epsilon,s$ then
($\cl{C'}(C),m) \eval (m',\lambda)$ and $m'\real \epsilon,s'$.
\end{proposition}




\subsection{Labellings and instrumentations}
Assuming a function $\kappa$ which associates an integer number with
labels and a distinct variable \w{cost} which does not occur in the program $P$ under consideration,
we abbreviate with $\w{inc}(\ell)$ the assignment $\w{cost}:=\w{cost}+\kappa(\ell)$.
Then we define the instrumentation $\cl{I}$ (relative to $\kappa$ and $\w{cost})$ 
as follows:
\[
\cl{I}(\ell:S) = \w{inc}(\ell) ; \cl{I}(S) ~.
\]
%% {\footnotesize
%% \[
%% \begin{array}{ll}

%% \cl{I}(\ell:S) &= \w{inc}(\ell) ; \cl{I}(S) 
%% %\\
%% %% \cl{I}_{\imp}(\s{if} \ \ell:b \ \s{then} \ S_1 \ \s{else} \ S_2)
%% %% &= \w{cost}:=\w{cost}+\kappa(\ell); \s{if} \ b \ \s{then} \ \cl{I}_{\imp}(S_1) \ \s{else} \ \cl{I}_{\imp}(S_2) \\ 

%% %lab-bool \cl{I}(\s{while} \ \ell:b \ \s{do} \ S ) &= \w{inc}(\ell); \s{while} \ b \ \s{do} \ (\cl{I}(S);\w{inc}(\ell))

%% \end{array}
%% \]}
The function $\cl{I}$ just distributes over the other operators of the language.
We extend the function $\kappa$ on labels to sequences of labels by defining
$\kappa(\ell_1,\ldots,\ell_n) = \kappa(\ell_1)+\cdots +\kappa(\ell_n)$.
The instrumented $\imp$ program relates to the labelled one has follows.
%
\begin{proposition}\label{lab-instr-erasure-imp}
Let $S$ be an $\imp_\ell$ command. If 
$(\cl{I}(S),s[c/\w{cost}]) \eval s'[c+\delta/\w{cost}]$
then 
$\xst{\lambda}{\kappa(\lambda)=\delta \mbox{ and }(S,s[c/\w{cost}])\eval(s'[c/\w{cost}],\lambda)}$.
\end{proposition}
%
\begin{definition}\label{labelling-def}
A {\em labelling} is a function $\cl{L}$ from an unlabelled language to 
the corresponding labelled one such that
$\w{er}_{\imp} \comp \cl{L}$ is the identity function on the 
$\imp$ language.
\end{definition}
%
\begin{proposition}\label{global-commutation-prop}
For any labelling function $\cl{L}$, and $\imp$ program $P$, the following holds:
\begin{equation}
\w{er}_{\mips}(\cl{C'}(\cl{C}(\cl{L}(P))) = \cl{C'}(\cl{C}(P))~.
\end{equation}
\end{proposition}
%
\begin{proposition}\label{instrument-to-label-prop}
Given a function $\kappa$ for the labels and a labelling function $\cl{L}$,
for all programs $P$ of the source language if 
$(\cl{I}(\cl{L}(P)),s[c/\w{cost}]) \eval s'[c+\delta/\w{cost}]$ 
and $m\real \epsilon,s[c/\w{cost}]$ then 
$(\cl{C'}(\cl{C}(\cl{L}(P))),m) \eval (m',\lambda)$, 
$m'\real \epsilon,s'[c/\w{cost}]$ and 
$\kappa(\lambda)=\delta$.
\end{proposition}

\subsection{Sound and precise labellings}\label{sound-label-sec}
With any $\mips_\ell$ code $M$ we can associate a directed and rooted 
(control flow) graph whose nodes are the instruction positions $\set{0,\ldots,|M|-1}$,
whose root is the node $0$,  and
whose directed edges correspond to the possible transitions between instructions.  
We say that a node is labelled if it corresponds to an instruction $\s{nop}
\ \ell$.  
%
\begin{definition}
A {\em simple path} in a $\mips_\ell$ code $M$ is a directed finite path in the graph associated with 
$M$ where the first node is labelled, the last node is the predecessor of either a labelled node or a leaf,
and all the other nodes are unlabelled.
\end{definition}
%
\begin{definition}
A $\mips_\ell$ code $M$ is {\em soundly labelled} if 
in the associated graph 
the root node $0$ is labelled 
and there are no loops that do not go through a labelled node.
\end{definition}
%
In a soundly labelled graph there are finitely many simple paths.
Thus, given a soundly labelled $\mips$ code $M$, we can associate 
with every label $\ell$ a number $\kappa(\ell)$ which is the
maximum (estimated) cost  of executing a simple 
path whose first node is labelled with $\ell$. 
We stress that in the following we assume that 
the cost of a simple path is proportional to the number of $\mips$
instructions that are crossed in the path.
%
\begin{proposition}\label{sound-label-prop}
If $M$ is soundly labelled and $(M,m) \eval (m',\lambda)$ then the cost
of the computation is bounded by $\kappa(\lambda)$.
\end{proposition}
%
Thus for a soundly labelled $\mips$ code the sequence of labels associated
with a computation is a significant information on the execution cost.
%
\begin{definition}
We say that a soundly labelled code is {\em precise}
if for every label $\ell$ in the code, the simple 
paths starting from a node labelled with $\ell$ have
the same cost.
\end{definition}
%
In particular, a code is precise if we can associate at most one simple
path with every label. 
%
\begin{proposition}\label{precise-label-prop}
If $M$ is precisely labelled and $(M,m) \eval (m',\lambda)$ then the cost
of the computation is $\kappa(\lambda)$.
\end{proposition}
%
The next point we have to check is that 
there are labelling functions (of the source code)
such that the compilation function does produce sound and possibly
precise labelled $\mips$ code.  To discuss this point, we introduce in table
\ref{labelling} two labelling functions $\cl{L}_s$ and $\cl{L}_p$ for the
$\imp$ language. The first labelling relies on just one label while
the second one relies on a function ``\w{new}'' which is meant to return fresh
labels and on an auxiliary function $\cl{L'}_p$ which returns a labelled command
and a binary directive $d\in \set{0,1}$. If $d=1$
then the command that follows (if any) must be labelled.
%
\begin{table}
{\footnotesize
\[
\begin{array}{ll}
\cl{L}_s(\s{prog} \ S) &=  \s{prog}\  \ell: \cl{L}_s(S) \\

\cl{L}_s(\s{skip})     &=\s{skip} \\

\cl{L}_s(x:=e)         &=x:=e \\

\cl{L}_s(S;S')         &= \cl{L}_s(S);\cl{L}_s(S') \\


\cl{L}_s(\s{if} \ b \ \s{then} \ S_1 \ \s{else} \ S_2) &= 

\s{if} \ b \ \s{then} \ \cl{L}_s(S_1) \ \s{else} \ \cl{L}_s(S_2) \\ 


\cl{L}_s(\s{while} \ b \ \s{do} \ S) &= \s{while} \ b \ \s{do} \ \ell:\cl{L}_s(S) \\  \\




\cl{L}_p(\s{prog} \ S) &= \s{prog}\   \cl{L}_p(S) \\

\cl{L}_p(S) &= \w{let} \ \ell=\w{new}, \ (S',d) =  \cl{L'}_p(S)  \ \w{in} \ \ell: S' \\

\cl{L'}_p(S)   &=(S,0)\quad \mbox{if }S=\s{skip}\mbox{ or }S=(x:=e) \\

\cl{L'}_p(\s{if} \ b \ \s{then} \ S_1 \ \s{else} \ S_2) 
&= (\s{if} \ b \ \s{then} \ \cl{L}_p(S_1) \ \s{else} \ \cl{L}_p(S_2), 1) \\ 

\cl{L'}_p(\s{while} \ b \ \s{do} \ S) 
&= (\s{while} \ b \ \s{do} \ \cl{L}_p(S), 1) \\


\cl{L'}_p(S_1;S_2)         &= \w{let} \ (S'_1,d_1)= \cl{L'}_p(S_1),  \ (S'_2,d_2)= \cl{L'}_p(S_2) \ \w{in} \ \\ 
                           &\qquad \w{case} \ d_1\\
                           &\qquad 0: (S'_1;S'_2,d_2) \\
                           &\qquad 1: \w{let} \ \ell= \w{new} \ \w{in} \ (S'_1;\ell:S'_2,d_2) 

\end{array}
\]}
\caption{Two labellings for the $\imp$ language} \label{labelling}
\end{table}
%
\begin{proposition}\label{lab-sound}
For all $\imp$ programs $P$: 

\Defitem{(1)} 
$\cl{C'}(\cl{C}(\cl{L}_s(P))$ 
is a soundly labelled $\mips$ code.

\Defitem{(2)}
$\cl{C'}(\cl{C}(\cl{L}_p(P))$ is a 
soundly and precisely  labelled $\mips$ code.
\end{proposition}
%
For an example of command which is not soundly labelled, consider
$\ell: \s{while} \ 0<x \ \s{do} \ x:=x+1$, which when compiled, produces
a loop that does not go through any label.  On the other hand, for an
example of a program which is not precisely labelled consider
$\ell:(\s{if} \ 0<x \ \s{then} \ x:=x+1 \ \s{else} \ \s{skip})$.  In the compiled code, we
find two simple paths associated with the label $\ell$ whose cost will
be quite different in general.

Once a sound and possibly precise labelling $\cl{L}$ has been
designed, we can determine the cost of each label and define an instrumentation
$\cl{I}$ whose composition with $\cl{L}$ will produce the desired
cost annotation.


\begin{definition}
Given a labelling function $\cl{L}$ for the source language $\imp$ 
and a program $P$  in the $\imp$ language,  we define an
annotation for the source program as follows:
\[
\w{An}_{\imp}(P) = \cl{I}(\cl{L}(P))~.
\]
\end{definition}




\begin{proposition}\label{ann-correct}
If $P$ is a program and $\cl{C'}(\cl{C}(\cl{L}(P)))$ is a sound (sound and precise)
labelling then $(\w{An}_{\imp}(P),s[c/\w{cost}]) \eval s'[c+\delta/\w{cost}]$
and $m\real \epsilon,s[c/\w{cost}]$ entails that 
$(\cl{C'}(\cl{C}(P)),m) \eval m'$, $m'\real \epsilon,s'[c/\w{cost}]$ 
and the cost of the execution is bound (is exactly) $\delta$.
\end{proposition}


To summarize, producing sound and precise labellings is mainly a
matter of designing the labelled source language so that 
the labelling is sufficiently {\em fine grained}. 
For instance, in the toy compiler, it is enough to label commands while it is not necessary to label
boolean conditions and expressions.
%lab-boolthe fact that boolean conditions are labelled is instrumental to precision while 
%the labelling of expressions turns out to be unnecessary.

Besides soundness and precision, a third criterion to evaluate
labellings is that they do not introduce too many unnecessary labels.
We call this property {\em economy}. In practice, it seems that one
can produce first a sound and possibly precise labelling and then
apply heuristics to eliminate unnecessary labels.

We stress that  our approach to labelling is based on the hypothesis that we can
obtain precise informations on the execution time of each instruction
of the generated binary code.  This hypothesis is indeed realised in
the processors of the $\intel$ family we are considering. On the other
hand, the execution time of instructions running on more complex
architectures including, {\em e.g.}, cache memory or pipelines are
much less predictable.  This lack of precision may somehow be
compensated by analysing the worst-case execution time of (long) sequences of
instructions. This point is further developed in appendix \ref{related-sec}.

%(on modern processors, on a long
%sequence certain costs are amortized, but this is not the case
%in \intel).  


%\newpage


\section{Labelling approach for the $\C$ compiler}\label{C-label-sec}

This section informally describes the labelled extensions of the languages in 
%\marginpar{Add backpointers to section 4}
the compilation chain (see Appendix~\ref{C-compiler-sec} for details),
the way the labels are propagated by the compilation functions, the
labelling of the source code, the hypotheses on the control flow of
the labelled assembly code and the verification that we
perform on it, the way we build the instrumentation, and finally the
way the labelling approach has been tested. The process of annotating
a $\Clight$ program using the labelling approach is detailed in the
following sections. It is summarized by the following steps.

{\begin{enumerate}\footnotesize
  \item 
  Label the input $\Clight$ program.

  \item
  Compile the labelled $\Clight$ program in the labelled world. This
  produces a labelled assembly code. 

  \item
  For each label of the labelled assembly code, compute the cost of the
  instructions under its scope and generate a \emph{label-cost mapping}. An
  unlabelled assembly code --- the result of the compilation --- is obtained by
  removing the labels from the labelled assembly code. 

  \item 
  Add a fresh \emph{cost variable} to the labelled $\Clight$ program and
  replace the labels by an increment of this cost variable according to the
  label-cost mapping. The result is an \emph{annotated} $\Clight$ program with no
  label.
\end{enumerate}}

\subsection{Labelled languages} 
Both the $\Clight$ and $\Cminor$ languages are extended in the same way
by labelling both statements and expressions (by comparison, in the
toy language $\imp$ we just labelled statements).
%lab-bool and boolean conditions).
The labelling of expressions aims to capture precisely their execution cost.
Indeed,  $\Clight$ and $\Cminor$ include expressions such 
as $a_1?a_2;a_3$ whose evaluation cost depends on the boolean value $a_1$.
As both languages are extended in the same way, the extended
compilation does nothing more than sending $\Clight$ labelled
statements and expressions to those of $\Cminor$.
% labelled statements and expressions.

%\subsection{Labels in $\RTLAbs$ and the back-end languages}
The labelled versions of $\RTLAbs$ and the languages in the back-end
simply consist in adding a new instruction whose semantics is to emit a label
without modifying the state. For the CFG based languages
($\RTLAbs$ to $\LTL$), this new instruction is $\s{emit}\ \w{label} \rightarrow
\w{node}$. For $\LIN$, $\mips$ and $\intel$, it is $\s{emit}\ \w{label}$. The translation
of these label instructions is immediate.
In $\mips$ and $\intel$, we also 
rely on a reserved label $\s{begin\_function}$  to pinpoint the
beginning of a function code (cf. section \ref{fun-call-sec}).

%% $\s{begin\_function}$. \marginpar{Is this really a new instruction or just a reserved label?}
%% Its semantics has no effect on the current environment,
%% it is only used as a syntactic marker to easily pinpoint the start of a function
%% in the $\mips$ code. We will explain the reason for such an instruction when
%% detailing the labelling of function calls.

\subsection{Labelling of the source language}
As for the toy compiler (cf. end of section \ref{label-toy-sec}), the goals of a labelling are
soundness, precision, and possibly economy.
%%
%% The goal here is to add labels in the source program that cover every reachable
%% instruction of the program and avoid unlabelled loops; this can be seen as a \emph{soundness}
%% property. Another important point is \emph{precision}, meaning that a label
%% might cover several paths to the next labels only if those paths have equal
%% costs. Several labellings might satisfy the soundness and precision conditions,
%% but from an engineering point of view, a labelling that makes obvious which
%% instruction is under the scope of which label would be better. There is a thin
%% line to find between too many labels --- which may obfuscate the code --- and
%% too few labels --- which makes it harder to see which instruction is under the
%% scope of which label. The balance leans a bit towards the \emph{economy} of
%% labels because the cost of executing an assembly instruction often depends on
%% its context (for instance by the status of the cache memory).
We explain our labelling by considering the constructions of $\Clight$ and their compilation to
assembly code.
%; a useful work hypothesis being that $\Clight$ expressions side-effect free.

\paragraph{Sequential instructions}
A sequence of $\Clight$ instructions that compile to sequential assembly code,
such as a sequence of assignments, can be handled by a single %preceding
label which covers the unique execution path.
%. Indeed, executing the first instruction of successive assignments will
%eventually lead to execute the following instructions in a unique path. 
%% The example below illustrates the labelling of `sequential' $\Clight$ instructions.
%% \begin{center}
%%   {\footnotesize
%%     \begin{tabular}{lllll}
%%       $\Clight$ & $\xrightarrow{Labelling}$ & Labelled $\Clight$ &
%%       $\xrightarrow{Compilation}$ & Labelled $\mips$\\\\
%%       \codeex{i = 0;} & & \textbf{\_cost:} & & \codeex{emit} \textbf{\_cost}\\
%%       \codeex{tab[i] = x;} & & \codeex{i = 0;} & & \codeex{li\ \ \ \$v0, 4}\\
%%       \codeex{x++;} & & \codeex{tab[i] = x;} & &
%%       \codeex{mul\ \ \$v0, \$zero, \$v0}\\
%%       & & \codeex{x++;} & & \codeex{add\ \ \$v0, \$a1, \$v0}\\
%%       & & & & \codeex{sw\ \ \ \$a0, 0(\$v0)}\\
%%       & & & & \codeex{li\ \ \ \$v0, 1}\\
%%       & & & & \codeex{add\ \ \$a0, \$a0, \$v0}
%%     \end{tabular}}
%% \end{center}

\paragraph{Ternary expressions and conditionals}
Most $\Clight$ expressions compile to sequential assembly code. 
{\em Ternary expressions}, that introduce a branching in the control
flow, are one exception. In this case, we achieve precision by associating a label with each branch.
This is similar to the treatment of the conditional we have already discussed
in section \ref{label-toy-sec}. As for the $\Clight$ operations \texttt{\&\&} and \texttt{||}
which have a lazy semantics, they are transformed to ternary expressions
\emph{before} computing the labelling.
%% \begin{center}
%%   {\footnotesize
%%     \begin{tabular}{lllll}
%%       $\Clight$ & $\xrightarrow{Labelling}$ & Labelled $\Clight$ &
%%       $\xrightarrow{Compilation}$ & Labelled $\mips$\\\\
%%       \codeex{b ? x+1 :} & &
%%       \codeex{b ?} \textbf{(\_cost1:} \codeex{x+1}\textbf{)} \codeex{:} & &
%%       \codeex{beq\ \ \$a0, \$zero, c\_false}\\
%%       \codeex{\ \ \ \ \ y} & &
%%       \codeex{\ \ \ \ }\textbf{(\_cost2:} \codeex{y}\textbf{)}
%%       & & \codeex{emit} \textbf{\_cost1}\\
%%       & & & & \codeex{li\ \ \ \$v0, 1}\\
%%       & & & & \codeex{add\ \ \$v0, \$a1, \$v0}\\
%%       & & & & \codeex{j\ \ \ \ exit}\\
%%       & & & & \codeex{c\_false:}\\
%%       & & & & \codeex{emit} \textbf{\_cost2}\\
%%       & & & & \codeex{move \$v0, \$a2}\\
%%       & & & & \codeex{exit:}
%%     \end{tabular}}
%% \end{center}
%% \paragraph{Related cases.}
%Of course these exThese operations have a very close
%behaviour to that of a ternary expression. In fact, they are compiled as such,
%which introduces implicit branches with constant values. For example, the
%$\Clight$ expression \texttt{x \&\& y} is translated into the $\Cminor$
%expression \texttt{x?(y?1:0):0}. To handle these two particular cases, the
%$\Clight$ \texttt{\&\&} and \texttt{||} operations are transformed in $\Clight$
%ternary expressions \emph{before} the labelling is processed.

%% \subsubsection{Conditionals}
%% Conditionals are another way to introduce a branching. As for ternary
%% expressions, the labelling of a conditional consists in adding a starting label
%% to the labelling of each branch.
%% \begin{center}
%%   {\footnotesize
%%     \begin{tabular}{lllll}
%%       $\Clight$ & $\xrightarrow{Labelling}$ & Labelled $\Clight$ &
%%       $\xrightarrow{Compilation}$ & Labelled $\mips$\\\\
%%       \codeex{if (b) \{} & & \codeex{if (b) \{} & &
%%       \codeex{beq\ \ \$a0, \$zero, c\_false}\\
%%       \codeex{\ \ x = 1;} & & \ \ \textbf{\_cost1:}
%%       & & \codeex{emit} \textbf{\_cost1}\\
%%       \codeex{\ \ ... \}} & & \codeex{\ \ x = 1;} & & \codeex{li\ \ \ \$v0, 1}\\
%%       \codeex{else \{} & & \codeex{\ \ ... \}} & & \codeex{...}\\
%%       \codeex{\ \ x = 2;} & & \codeex{else \{} & & \codeex{j\ \ \ \ exit}\\
%%       \codeex{\ \ ... \}} & & \ \ \textbf{\_cost2:} & & \codeex{c\_false:}\\
%%       & & \codeex{\ \ x = 2;} & & \codeex{emit} \textbf{\_cost2}\\
%%       & & \codeex{\ \ ... \}} & & \codeex{li\ \ \ \$v0, 2}\\
%%       & & & & \codeex{...}\\
%%       & & & & \codeex{exit:}
%%     \end{tabular}}
%% \end{center}

\paragraph{Loops}
Loops in $\Clight$ are guarded by a condition. Following the arguments for the
previous cases, we add two labels when encountering a loop construct: one label
to start the loop's body, and one label when exiting the loop. 
This is similar to the treatment of \s{while} loops discussed in section \ref{label-toy-sec} and it
is enough to guarantee that the loop in the compiled code goes through a label.
%The definition of the soundness of the labelling in the toy compiler (section
%\ref{sound-label-sec}) establishes that each loop's body must contain at least
%one label. Interestingly, this is thus trivially satisfied.
%% \begin{center}
%%   {\footnotesize
%%     \begin{tabular}{lllll}
%%       $\Clight$ & $\xrightarrow{Labelling}$ & Labelled $\Clight$ &
%%       $\xrightarrow{Compilation}$ & Labelled $\mips$\\\\
%%       \codeex{while (b) \{} & & \codeex{while (b) \{} & &
%%       \codeex{loop:}\\
%%       \codeex{\ \ i++;} & & \textbf{\ \ \_cost1:} & &
%%       \codeex{beq\ \ \$a0, \$zero, exit}\\
%%       \codeex{\ \ ... \}} & & \codeex{\ \ i++;} & &
%%       \codeex{emit} \textbf{\_cost1}\\
%%       \codeex{x = i;} & & \codeex{\ \ ... \}} & & \codeex{li\ \ \ \$v0, 1}\\
%%       & & \textbf{\_cost2:} & & \codeex{add\ \ \$a1, \$a1, \$v0}\\
%%       & & \codeex{x = i;} & & \codeex{...}\\
%%       & & & & \codeex{j\ \ \ \ loop}\\
%%       & & & & \codeex{exit:}\\
%%       & & & & \codeex{emit} \textbf{\_cost2}\\
%%       & & & & \codeex{move \$a2, \$a1}
%%     \end{tabular}}
%% \end{center}

\paragraph{Program Labels and Gotos}
In $\Clight$, program labels and gotos are intraprocedural. Their only effect on
the control flow of the resulting assembly code is to potentially introduce an
unguarded loop. This loop must contain at least one cost label in order to
satisfy the soundness condition, which we ensure by adding a cost label right
after a program label.

\begin{center}
  {\footnotesize
    \begin{tabular}{lllll}
      $\Clight$ & $\xrightarrow{Labelling}$ & Labelled $\Clight$ &
      $\xrightarrow{Compilation}$ & Labelled $\mips$\\\\
      \codeex{lbl:} & & \codeex{lbl:} & & \codeex{lbl:}\\
      \codeex{i++;} & & \textbf{\_cost:} & &
      \codeex{emit} \textbf{\_cost}\\
      \codeex{...} & & \codeex{i++;} & &
      \codeex{li\ \ \ \$v0, 1}\\
      \codeex{goto lbl;} & & \codeex{...} & &
      \codeex{add\ \ \$a0, \$a0, \$v0}\\
      & & \codeex{goto lbl;} & & \codeex{...}\\
      & & & & \codeex{j\ \ \ \ lbl}
    \end{tabular}}
\end{center}

\paragraph{Function calls}\label{fun-call-sec}
Function calls in assembly code are performed by indirect jumps, the
address of the callee being in the memory. In the general case, this
address cannot be inferred statically. Even though the destination
point of a function call is unknown, when the considered assembly code
has been produced by our compiler, we know for a fact that this
function ends with a return statement that transfers the control back
to the instruction following the function call in the caller. As a
result, we treat function calls according to the following global
invariants of the compilation: (1) the instructions of a function are
covered by the labels inside this function, (2) we assume a function
call always returns and runs the instruction following the call.
Invariant (1) entails in particular that each function must contain at
least one label. To ensure this, we simply add a starting label in
every function definition. The example below illustrates this point:

\begin{center}
  {\footnotesize
    \begin{tabular}{lllll}
      $\Clight$ & $\xrightarrow{Labelling}$ & Labelled $\Clight$ &
      $\xrightarrow{Compilation}$ & Labelled $\mips$\\\\
      \codeex{void f () \{} & & \codeex{void f () \{} & & \codeex{f\_start:}\\
      \codeex{\ \ f}\emph{'s body} & & \textbf{\ \ \_cost:} & &
      \emph{Frame Creation}\\
      \codeex{\}} & & \codeex{\ \ f}\emph{'s body} & & \emph{Initializations}\\
      & & \codeex{\}} & & \codeex{emit} \textbf{\_cost} \\
      & & & & \codeex{f}\emph{'s body}\\
      & & & & \emph{Frame Deletion}\\
      & & & & \codeex{return}
    \end{tabular}}
\end{center}

We notice that some instructions in assembly code will be
inserted \emph{before} the first label is emitted. These instructions
relate to the frame creation and/or variable initializations, and are
composed of sequential instructions (no branching). To deal with this
issue, we take the convention that the instructions that precede the
first label in a function code are actually under the scope of the
first label.  Invariant (2) is of course an over-approximation of the
program behavior as a function might fail to return because of an
infinite loop.  In this case, the proposed labelling remains correct:
it just assumes that the instructions following the function call will
be executed, and takes their cost into consideration. The final
computed cost is still an over-approximation of the actual cost.

% As for the imprecision that it may
% introduce, we consider it to be reasonable because instructions that follow a
% call to a non-returning function can only be regarded as a bug.
% RA: IT SEEMS TO ME THAT WE DO NOT CARE WHAT HAPPENS OF OUR COST PREDICTIONS IF THE PROGRAM LOOPS

\subsection{Verifications on the object code}

The labelling previously described has been designed so that the
compiled assembly code satisfies the soundness and precision
conditions. However, we do not need to prove this, instead we have to
devise an algorithm that checks the conditions on the compiled code.
The algorithm assumes a correct management of function calls in the
compiled code. In particular, when we call a function we always jump
to the first instruction of the corresponding code segment and when we
return we always jump to an an instruction that follows a call.  We
stress that this is a reasonable hypothesis that is essentially
subsumed by the proof that the object code {\em simulates} the source
code.

In our current implementation, we check the soundness and the
precision conditions while building at the same time the label-cost
mapping. To this end, the algorithm takes the following main steps.

{\footnotesize
\begin{itemize}
\item First, for each function a control flow graph is built.

\item For each graph, we check whether there is a unique
label that is reachable from the root by a unique path.
This unique path corresponds to the instructions generated by 
the calling conventions as discussed in section \ref{fun-call-sec}.
We shift the occurrence of the label to the root of the graph.

\item 
By a  strongly connected components algorithm,
we check whether every loop in the graphs goes through at least one label.

\item We perform a (depth-first) search of the graph. Whenever we reach a
  labelled node, we perform a second (depth-first) search that stops at labelled
  nodes and computes an upper bound on the cost of the occurrence of the label. Of
  course, when crossing a branching instruction, we take the maximum cost of the
  branches.  When the second search stops we update the current cost of the
  label-cost mapping (by taking a maximum) and we continue the first search.

\item Warning messages are emitted whenever the maximum is taken between two
different values as in this case  the precision condition may be violated.

\end{itemize}}

In the particular case of the $\intel$, which is a very basic
micro-controller, the number of cycles required by each instruction is
fully specified. Therefore, if the labelling is precise, the cost
associated to a label is the exact number of cycles necessary to
execute every simple execution path starting from that label.

%% \item Then, for each node $n$ (instruction) of each control flow graph 
%% we determine the set of labels the node is under the scope of.
%% This amounts to determine the set of labelled nodes in the graph for which there
%% is a directed path to $n$ that does not cross another labelled node. 
%% There is one exception though, we associate to the instructions that are at the beginning of 
%% a function the first label that follows them.
%% We implement this verification through a depth-first search. Along the way,
%% we also check that every instruction is in the   scope of a label which is part
%% of our soundness condition.

%% \item To check whether every loop goes through at least one label, we simply rely on a
%%   strongly connected components algorithm. Pass this point, the soundness
%%   condition is verified.

%% \item Finally, the label-cost mapping is computed by adding the cost of an
%%   instruction to the cost associated with the labels it is in the scope of 
%%  (this is a rough approximation if a label can occur several time, but this situation 
%%   does not seem to arise with our labelling).
%%   There is only one particular case: the branching instruction. When founding one, the
%%   cost to reach the next label is computed for each branch. If it is different,
%%   a message warns the user that the precision condition may be violated, and the
%%   maximum is considered in the resulting cost.
%% \end{itemize}

% \paragraph{Colouring algorithm.}
% Most of the work to check soundness and precision is done by an algorithm that\marginpar{To be made more abstract}
% colours each instruction of the $\mips$ code. Four colours are used:
% \begin{itemize}
% \item \emph{white} tags instructions that have not been processed yet. Initially
%   every instruction is white;
% \item the \emph{black} colour is used together with a label whose scope is
%   currently opened. An instruction may be in the scope of several labels; thus,
%   colouring an instruction $i$ in black with label $l$ adds $l$ to the set of
%   labels that $i$ is in the scope of;
% \item \emph{gray} is the colour of an instruction that has been processed with no
%   associated label scope. It is the starting colour of the algorithm;
% \item finally, \emph{yellow} is used for the particular case of the instructions
%   before the first label of a function. The beginning of a function is marked
%   with the instruction $\s{begin\_function}$.
% \end{itemize}
% The algorithm has the following arguments: the code to colour, a stack of lines
% in the code to process, and the current colour. Initially, all the instructions
% in the code are white, the stack of lines to process is formed with the first
% line only, and the current colour is gray. Processing an instruction consists in
% a case analysis over the current colour, the instruction, and its associated
% colour. The algorithm ends when the stack of lines to process is empty, or when
% reaching the following particular case: finding an instruction coloulred in black
% $L$ ($L$ is a set of labels), when the current colour is black $l$ and $l \in
% L$. Then the algorithm stops and an error is reported: the soundness condition
% may be violated because a loop with no $\s{emit}$ instruction has been found.

% \paragraph{Checking the soundness.}
% The presence of loops with no $\s{emit}$ instruction is checked during the
% colouring algorithm. The other part of the soundness condition is checked on the
% result of the algorithm: if an instruction is not black in the end, this means
% that it is under the scope of no label. Then, an error is raised.

% \paragraph{Building the label-cost mapping and checking the precision.} 
% Having determined which instruction is under the scope of which label, the label-cost
% mapping is computed simply by adding the cost of an instruction to the cost
% associated to the label(s) it is in the scope of. There is only one particular
% case: the branching instruction. When founding one, the cost to reach the next
% label is computed for each branch. If it is different, a message warns the user
% that the precision condition may be violated, and the maximum is considered in
% the resulting cost.

% There are a lot of cases, some examples are described below:
% \begin{itemize}
% \item when finding a $\s{begin\_function}$ instruction, it is coloured in yellow,
%   the current color is set to yellow, and the next line is added to the set of
%   lines to process;
% \item when finding a $\s{emit}\ l$ white instruction, the instruction is colored
%   in black $l$, every yellow instruction in the code is colored in black
%   $l$, the current color is set to black $l$, and the next line is added to the
%   set of lines to process;
% \item when finding an instruction colored in black $L$ ($L$ is a set of labels),
%   if the current color is black $l$ where $l \in L$, then the algorithm stops
%   and an error is reported: the soundness condition may be violated because a
%   loop with no $\s{emit}$ instruction may be found. If $l
%   \not\in L$, the instruction is simply colored in black $l$ -- which means that
%   $l$ is added to $L$ --- and the next line is added to the set of lines to
%   process;
% \end{itemize}

% The verification algorithm updates a label-cost mapping; it is initially
% empty. Moreover, the algorithm has a label argument whose scope is currently
% opened; the initial label is undefined. Each time an instruction of the $\mips$
% code is processed, its cost is added in the label-cost mapping to the cost
% associated to the current label. The algorithm starts with the first
% instruction, continues with the instructions below, follows unconditional direct
% jumps, and passes through function calls and indirect jumps.

\subsection{Building the cost annotation}

Once the label-cost mapping is computed, instrumenting the labelled source code is an easy task. A fresh global variable which we call
\emph{cost variable} is added to the source program with the  purpose of holding the cost value and it is initialized at the very beginning of the \codeex{main} program.
Then, every label is replaced by an increment of the 
cost variable according to the label-cost
mapping. 
Following this replacement, the cost labels disappear and the result is
a $\Clight$ program with annotations in the form of assignments.

There is one final problem: labels inside expressions. 
As we already mentioned,  $\Clight$ does not allow 
writing side-effect instructions --- such as  cost
increments --- inside expressions. To cope with this restriction, we produce
first an instrumented $\C$ program --- with side-effects in expressions 
--- that we translate back to $\Clight$ using $\cil$. 
This process is summarized below.

\begin{center}
  {\footnotesize
    \begin{tabular}{lllll}
      $\left . \begin{array}{l}
      \text{Labelled $\Clight$}\\
      \text{label-cost mapping}
    \end{array} \right \}$ & $\xrightarrow{\text{Instrumentation}}$ &
      Instrumented $\C$ & $\xrightarrow{\cil}$ & Instrumented $\Clight$
    \end{tabular}}
\end{center}

\subsection{Testing}
It is desirable to test the coherence of the labelling from $\Clight$
to assembly code.  To this end, each labelled language comes with an
interpreter that produces the trace of the labels encountered during
the computation. 

% Not only does it classically interpret programs,
% but also, an interpret produces the trace of labels encountered during
% interpretation.
Then, one naive approach is to test 
the equality of the traces 
produced by the program at the different stages of the compilation.
Our current implementation passes this kind of tests.
For some optimizations that may re-order computations, the weaker
condition mentioned in remark~\ref{rem:multi-set} could be considered.

Furthermore, in the case of the $\intel$ back-end, we can run our compiled
code into a dedicated simulator and we check that the statically computed
number of cycles for each simple path is the same as the real one.

%\marginpar{Input Nicolas}


%% \paragraph{Contrasting the approaches}~
%% \begin{description}
%% \item[PROS] Better compositionality, we do not need to handle concrete values 
%% in the simulation proof and we do not need to define the intermediate annotations.
%% \item[CONS] The simulation might need to be relaxed if we want to reorder pieces of
%% computation.  For some optimisations that allow to extract a piece of code from a loop,
%% it might be difficult to find a suitable notion of simulation that still
%% allows to have precision.
%% \end{description}


\section{Conclusion and future work}\label{conclusion-sec}
We have discussed the problem of building a compiler which can {\em
  lift} in a provably correct way pieces of information on the
execution cost of the object code to cost annotations on the source
code.  To this end, we have introduced the so called 
{\em labelling} approach and discussed its formal application to a
toy compiler. Based on this experience, we have argued that the 
approach has good scalability properties, and  to substantiate this
claim, we have reported on our successful experience in implementing
and testing the labelling approach on top of a prototype compiler
written in $\ocaml$ for a large fragment of the $\C$ language which
can be shortly described as $\Clight$ without floating point.

We discuss next a few directions for future work.
%
First, we are currently testing the current compiler on 
the kind of $\C$ code produced for embedded applications
by a $\lustre$ compiler.
Starting from the annotated $\C$ code, we are relying on 
the $\framac$ tool to produce automatically meaningful information on, say,
the reaction time of a given synchronous program.
%
%Second, we are porting the current compiler to other assembly
%languages. In particular, we are interested in targeting
%one of the assembly languages covered by the $\absint$ tool so as 
%to obtain more realistic estimations of
%the execution cost of sequences of instructions.
%
Second,  we plan to formalize and validate in the {\em Calculus of Inductive
Constructions} the prototype implementation of the labelling approach
for the $\C$ compiler described in section \ref{C-label-sec}.
This requires a major implementation effort which will be carried
on in collaboration with our partners of  the $\cerco$ project~\cite{Cerco10}.
%
%Fourth, we plan to study the applicability of the labelling 
%approach to other optimisation techniques in the realm of
%the $\C$ compilers technology such as {\em loop optimisations},
%and to other languages which rely on  
%rather distinct compilation technologies
%such as a language of the $\ml$ family.


{\footnotesize
\begin{thebibliography}{99}

\bibitem{AbsInt}
AbsInt Angewandte Informatik. {\tt http://www.absint.com/}.

%\bibitem{CercoDeliverable}
%R.M.~Amadio, N.~Ayache, K.~Memarian, R.~Saillard, Y.~R\'egis-Gianas.
%\newblock Compiler Design and Intermediate Languages.
%\newblock Deliverable 2.1 of~\cite{Cerco10}.

\bibitem{Cerco10}
Certified Complexity (Project description).
\newblock  ICT-2007.8.0 FET Open, Grant 243881. 
{\tt http://cerco.cs.unibo.it}.
%\newblock  Partners: Universities of Bologna, Edinburgh, and Paris Diderot, 2010.

\bibitem{SCADE}
Esterel Technologies. 
{\tt http://www.esterel-technologies.com}.

\bibitem{Frama-C}
$\framac$ software analysers.
{\tt http://frama-c.com/}.

\bibitem{AbsintScade}
C.~Ferdinand, R.~Heckmann, T.~ Le Sergent, D.~Lopes, B.~Martin, X.~Fornari, and F.~Martin.
\newblock Combining a high-level design tool for safety-critical
systems with a tool for {WCET} analysis of executables.
\newblock  In 
%Proc. of the 4th European Congress on
{\em Embedded Real Time Software (ERTS)}, 
%Toulouse, 
2008.

\bibitem{Fornari10}
X.~Fornari.
\newblock Understanding how {SCADE} suite {KCG} generates safe {C} code.
\newblock White paper, Esterel Technologies, 2010.

\bibitem{Larus05}
J.~Larus.
\newblock Assemblers, linkers, and the SPIM simulator.
\newblock Appendix of {\em Computer Organization and Design: the hw/sw interface}, 
by Hennessy and Patterson, 2005.

\bibitem{intel94}
\newblock MCS 51 Microcontroller Family User's Manual. 
\newblock Publication number 121517, 
by Intel Corporation, 1994, 

\bibitem{Leroy09}
X.~Leroy.
\newblock Formal verification of a realistic compiler.
\newblock {\em Commun. ACM}, 52(7):107-115, 2009.


\bibitem{Leroy09-ln}
X.~Leroy.
\newblock Mechanized semantics, with applications to program proof and compiler verification.
%(lecture notes and Coq development). 
\newblock {\em Marktoberdorf summer school}, 2009. 


%% \bibitem{MP67}
%% J.~McCarthy and J.~Painter.
%% \newblock Correctness of a compiler for arithmetic expressions.
%% \newblock In {\em Math. aspects of Comp. Sci. 1}, vol. 19
%% of Symp. in Appl. Math., AMS, 1967.

\bibitem{CIL02}
 G.~Necula, S.~McPeak, S.P.~Rahul, and W.~Weimer.
\newblock CIL: Intermediate Language and Tools for Analysis and Transformation of C Programs.
\newblock In {\em Proceedings of Conference on Compiler Construction}, 
Springer LNCS 2304:213--228, 2002.

\bibitem{Pottier}
F.~Pottier.
\newblock Compilation (INF 564), \'Ecole Polytechnique, 2009-2010. 
{\tt http://www.enseignement.polytechnique.fr/informatique/INF564/}. 


%\bibitem{Saillard}
%R.~Saillard.
%\newblock Complexit\'e Certifi\'ee.
%\newblock Rapport de Master Recherche, Universit\'e Paris-Diderot, 2010.

\bibitem{W09}
R.~Wilhelm et al.
\newblock The worst-case execution-time problem - overview of methods and survey of tools. 
\newblock {\em ACM Trans. Embedded Comput. Syst.}, 7(3), 2008.


\bibitem{share}
Microcontroller market and Technology. Analysis report 2008.
EMITT solutions.


\end{thebibliography}}

\newpage
\appendix

\section{A toy compiler}\label{toy-compiler-sec}
We formalize the toy compiler
introduced in section \ref{toy-intro}~\footnote{A mechanized proof in the 
$\coq$ proof assistant can be found in K.~Memarian's 
{\em Travail d'\'etude et de recherche}
entitled {\em Complexit\'e Certifi\'ee}
which can be downloaded at
\url{http://www.pps.jussieu.fr/~yrg/miniCerCo/}.}.

\subsection{\imp: language and semantics}\label{imp-sec}
The syntax of the $\imp$ language is described below.
This is a rather standard imperative language with 
\s{while} loops and \s{if-then-else}. 

{\footnotesize
\[
\begin{array}{lll}

\w{id}&::= x\Alt y\Alt \ldots       &\mbox{(identifiers)} \\
\w{n} &::= 0 \Alt -1 \Alt +1 \Alt \ldots &\mbox{(integers)} \\
v &::= n \Alt \s{true} \Alt \s{false}  &\mbox{(values)} \\
e &::= \w{id} \Alt n \Alt e+e    &\mbox{(numerical expressions)} \\
b &::= e<e  &\mbox{(boolean conditions)} \\
S &::= \s{skip} \Alt \w{id}:=e \Alt S;S \Alt 
  \s{if} \ b \ \s{then} \ S \ \s{else} \ S 
   \Alt \s{while} \ b \ \s{do} \ S  &\mbox{(commands)} \\
P &::= \s{prog} \ S      &\mbox{(programs)}

\end{array}
\]}

Let $s$ be a total function from identifiers to integers representing
the {\bf state}.  If $s$ is a state, $x$ an identifier, and $n$ an
integer then $s[n/x]$ is the `updated' state such that $s[n/x](x)=n$
and $s[n/x](y)=s(y)$ if $x\neq y$.
%
%\subsection{$\imp$: semantics}
The {\em big-step} operational semantics of $\imp$ 
expressions and boolean conditions is defined as follows:

{\footnotesize
\[
\begin{array}{c}

\infer{}
{(v,s)\eval v}

\qquad

\infer{}
{(x,s) \eval s(x)}

\qquad

\infer{(e,s)\eval v\quad (e',s)\eval v'}
{(e+e',s)\eval (v+_{\Z} v')} 

\qquad
\infer{(e,s)\eval v\quad (e',s)\eval v'}
{(e<e',s) \eval (v<_{\Z} v')} 
\end{array}\]}

A {\em continuation} $K$ is a list of commands which terminates with a special
symbol \s{halt}:
$K::= \s{halt} \Alt S \cdot K$.
Table \ref{small-step-imp} defines a small-step semantics of $\imp$ commands 
whose basic judgement has the shape:
$(S,K,s) \arrow  (S',K',s')$.
We define the semantics of a program $\s{prog} \ S$ as the semantics
of the command $S$ with continuation $\s{halt}$.
We derive a big step semantics from the small step one as follows:
$(S,s) \eval s'$  if $(S,\s{halt},s) \arrow \cdots \arrow (\s{skip},\s{halt},s')$.

\begin{table}
{\footnotesize
\[
\begin{array}{lll}
(x:=e,K,s) &\arrow &(\s{skip},K,s[v/x]) \qquad\mbox{if }(e,s)\eval v \\ \\

(S;S',K,s) &\arrow &(S,S'\cdot K,s) \\ \\

(\s{if} \ b \ \s{then} \ S \ \s{else} \ S',K,s) &\arrow 
&\left\{
\begin{array}{ll}
(S,K,s) &\mbox{if }(b,s)\eval \s{true} \\
(S',K,s) &\mbox{if }(b,s)\eval \s{false}
\end{array}
\right. \\ \\


(\s{while} \ b \ \s{do} \ S ,K,s) &\arrow 
&\left\{
\begin{array}{ll}
(S,(\s{while} \ b \ \s{do} \ S)\cdot K,s) &\mbox{if }(b,s)\eval \s{true} \\
(\s{skip},K,s) &\mbox{if }(b,s)\eval \s{false}
\end{array}
\right. \\ \\


(\s{skip},S\cdot K,s) &\arrow
&(S,K,s)



\end{array}
\]}
\caption{Small-step operational semantics of $\imp$ commands}\label{small-step-imp}
\end{table}




\subsection{\vm: language and semantics}\label{vm-sec}
Following~\cite{Leroy09-ln},
we define a virtual machine $\vm$ and its programming language.
The machine includes the following elements:
(1) a fixed code $C$ (a possibly empty sequence of instructions),
(2) a program counter \w{pc},
(3) a store $s$ (as for the source program),
(4) a stack of integers $\sigma$.

%% We will rely on the following instructions with the associated
%% informal semantics:

%% {\footnotesize
%% \[
%% \begin{array}{ll}
%% {\tt cnst(n)}        &\mbox{push on the stack} \\
%% {\tt var(x)}         &\mbox{push value }x   \\
%% {\tt setvar(x)}      &\mbox{pop value and assign it to }x \\
%% {\tt add}            &\mbox{pop 2 values and push their sum} \\
%% {\tt branch(k)}      &\mbox{jump with offset }k        \\
%% {\tt bge(k)}         &\mbox{pop 2 values and jump if greater or equal with offset }k \\
%% {\tt halt}           &\mbox{stop computation}
%% \end{array}
%% \]}

%% In the branching instructions, $k$ is an integer that has to be added
%% to the current program counter in order to determine the following
%% instruction to be executed. 
%In the following to increase readability
%we will often rely on labels in order to point symbolically to a
%certain instruction.
Given a sequence $C$, we denote with $|C|$ its length and 
with  $C[i]$ its $i^{\w{th}}$ element (the leftmost element
being the $0^{\w{th}}$ element).
The operational semantics of the instructions is formalized by rules of the shape
$C \Gives (i,\sigma,s) \arrow (j,\sigma',s')$
and it is fully described in table \ref{semantics-vm}.
Notice that $\imp$ and $\vm$ semantics share the same notion of store.
%A sequence of exactly $n$ transitions is written $A \arrow^n B$.
We write, {\em e.g.}, $n\cdot \sigma$ to stress that the top element 
of the stack exists and is $n$.
We will also write $(C,s)\eval s'$ if 
$C\Gives (0,\epsilon,s) \trarrow (i,\epsilon,s')$ and $C[i]=\s{halt}$.
\begin{table}
{\footnotesize
\[
\begin{array}{l|l}

\mbox{Rule}                                                 & C[i]= \\\hline

C \Gives (i, \sigma, s) \arrow (i+1, n\cdot \sigma,s)  & {\tt cnst}(n) \\ 
C \Gives (i, \sigma, s) \arrow (i+1,s(x)\cdot \sigma,s)  & {\tt var}(x) \\ 
C \Gives (i, n \cdot \sigma, s) \arrow (i+1,\sigma,s[n/x])  & {\tt setvar}(x) \\
C \Gives (i, n \cdot n' \cdot \sigma, s) \arrow (i+1, (n+_{\Z} n')\cdot \sigma,s)  & {\tt add} \\
C \Gives (i, \sigma, s) \arrow (i+k+1, \sigma,s)  & {\tt branch(k)} \\
C \Gives (i, n \cdot n' \cdot \sigma, s) \arrow (i+1, \sigma,s)  & {\tt bge(k)} \mbox{ and }n<_{\Z} n'\\
C \Gives (i, n \cdot n' \cdot \sigma, s) \arrow (i+k+1, \sigma,s)  & {\tt bge(k)} \mbox{ and }n\geq_{\Z} n'\\

\end{array}
\]}
\caption{Operational semantics $\vm$ programs}\label{semantics-vm}
\end{table}

Code coming from the compilation of $\imp$ programs has specific
properties that are used in the following compilation step when values
on the stack are allocated either in registers or in main memory.  In
particular, it turns out that for every instruction of the compiled
code it is possible to predict statically the {\em height of the stack}
whenever the instruction is executed.  We now proceed to define a simple notion
of {\em well-formed} code and show that it enjoys this property.  In
the following section, we will define the compilation function from
$\imp$ to $\vm$ and show that it produces well-formed code.


\begin{definition}
We say that a sequence of instructions $C$ is well formed if there
is a function $h:\set{0,\ldots,|C|} \arrow \Nat$ which satisfies the
conditions listed in table \ref{well-formed-instr} for $0\leq i \leq |C|-1$.
In this case we write $C:h$.
\end{definition}

\begin{table}
{\footnotesize
\[
\begin{array}{l|l}

C[i]=         & \mbox{Conditions for }C:h \\\hline

\s{cnst}(n)
\mbox{ or } \s{var}(x)
&h(i+1) = h(i)+1 \\

\s{add}            
& h(i)\geq 2, \quad h(i+1)=h(i)-1 \\

\s{setvar}(x)      
& h(i)=1, \quad h(i+1)=0 \\

\s{branch}(k)
& 0\leq i+k+1 \leq |C|, \quad h(i)=h(i+1)=h(i+k+1)=0 \\

\s{bge}(k)
& 0\leq i+k+1 \leq |C|, \quad h(i)=2, \quad h(i+1)=h(i+k+1)=0 \\

\s{halt}    
&i=|C|-1, \quad h(i)=h(i+1)=0

\end{array}
\]}
\caption{Conditions for well-formed code}\label{well-formed-instr}
\end{table}

The conditions defining the predicate $C:h$ are strong enough 
to entail that $h$ correctly predicts the stack height 
and to guarantee the uniqueness of $h$ up to the initial condition.

\begin{proposition}\label{unicity-height-prop}
(1) 
If $C:h$, $C\Gives (i,\sigma,s) \trarrow (j,\sigma',s')$, and 
$h(i)=|\sigma|$ then $h(j)=|\sigma'|$.
(2) If $C:h$, $C:h'$ and $h(0)=h'(0)$ then $h=h'$.
\end{proposition}


\subsection{Compilation from $\imp$ to $\vm$}\label{compil-imp-vm-sec}
In table \ref{compil-imp-vm}, 
we define compilation functions $\cl{C}$ from $\imp$ to $\vm$ which
operate on expressions, boolean conditions, statements, and programs.
We write $\w{sz}(e)$, $\w{sz}(b)$, $\w{sz}(S)$ for the number of instructions
the compilation function associates with the expression $e$, the boolean
condition $b$, and the statement $S$, respectively.


\begin{table}
{\footnotesize
\[
\begin{array}{c}

\cl{C}(x) = {\tt var}(x)   \qquad
\cl{C}(n)  ={\tt cnst}(n)   \qquad
\cl{C}(e+e') =\cl{C}(e) \cdot \cl{C}(e') \cdot {\tt add} \\ \\

\cl{C}(e<e',k) = \cl{C}(e') \cdot \cl{C}(e) \cdot {\tt bge(k)} \\ \\ 

\qquad  \cl{C}(x:=e) = \cl{C}(e) \cdot {\tt setvar(x)} 

\qquad \cl{C}(S;S') = \cl{C}(S) \cdot \cl{C}(S')\\ \\


\cl{C}(\s{if} \ b \ \s{then} \ S\  \s{else} \ S') = 
\cl{C}(b,k) \cdot \cl{C}(S) \cdot (\s{branch}(k')) \cdot \cl{C}(S')  \\
\mbox{where: } k= \w{sz}(S)+1, \quad k'=\w{sz}(S')

\\ \\

\cl{C}(\s{while} \ b \ \s{do} \  S )
= \cl{C}(b,k)  \cdot \cl{C}(S)  \cdot \s{branch}(k') \\
\mbox{where: } k=\w{sz}(S)+1, \quad k'=-(\w{sz}(b)+\w{sz}(S)+1)\\\\

\cl{C}(\s{prog} \ S) = 
\cl{C}(S) \cdot \s{halt}

\end{array}
\]}

\caption{Compilation from $\imp$ to $\vm$}\label{compil-imp-vm}
\end{table}


% \subsection{Soundness of compilation: from $\imp$ to $\vm$}
We follow~\cite{Leroy09-ln} for 
the proof of soundness of the compilation function for
expressions and boolean conditions.

\begin{proposition}\label{soundness-big-step-prop}
The following properties hold:

\Defitem{(1)}
If $(e,s)\eval v$ then 
$C \cdot \cl{C}(e) \cdot C' 
\Gives (i,\sigma,s) \trarrow (j,v\cdot \sigma,s)$
where $i=|C|$ and $j=|C \cdot \cl{C}(e)|$.


\Defitem{(2)}
If $(b,s)\eval \s{true}$ then 
$C \cdot \cl{C}(b,k) \cdot C' 
\Gives (i,\sigma,s) \trarrow (j+k,\sigma,s)$
where  $i=|C|$ and $j=|C \cdot \cl{C}(b,k)|$.

\Defitem{(3)}
If $(b,s)\eval \s{false}$
then $C \cdot \cl{C}(b,k) \cdot C' 
\Gives (i,\sigma,s) \trarrow (j,\sigma,s)$
where  $i=|C|$ and $j=|C \cdot \cl{C}(b,k)|$.

% \Defitem{(4)}
% If $(S,s)\eval s'$ then
% $C \cdot \cl{C}(S) \cdot C' 
% \Gives (i,\sigma,s) \trarrow (j,\sigma,s')$
% where  $i=|C|$ and $j=|C \cdot \cl{C}(e)|$.
\end{proposition}

Next we focus on the compilation of statements.
We introduce a ternary relation $R(C,i,K)$ which relates 
a $\vm$ code $C$, a number $i\in\set{0,\ldots,|C|-1}$ and a continuation
$K$. The intuition is that relative to the code $C$, 
the instruction $i$ can be regarded as having continuation $K$. 
(A formal definition is available in Appendix~\ref{soundness-small-step}.)
We can then state the correctness of the compilation function as follows.


\begin{proposition}\label{soundness-small-step}
If $(S,K,s) \arrow (S',K',s')$ and $R(C,i,S\cdot K)$ then 
$C\Gives (i,\sigma,s) \trarrow (j,\sigma,s')$ and
$R(C,j,S'\cdot K')$.
\end{proposition}



%\subsection{Compiled code is well-formed}
As announced, we can prove that the result of the compilation
is a well-formed code.

\begin{proposition}\label{well-formed-prop}
For any program $P$  there is a unique $h$ such that $\cl{C}(P):h$.
\end{proposition}



\subsection{$\mips$: language and semantics}\label{mips-sec}
We consider a $\mips$-like machine~\cite{Larus05} 
which includes the following elements:
(1) a fixed code $M$ (a sequence of instructions),
(2) a program counter \w{pc},
(3) a finite set of registers including the registers 
$A$, $B$, and $R_0,\ldots,R_{b-1}$, 
and (4)  an (infinite) main memory which maps 
locations to integers.

We denote with $R,R',\ldots$ registers, with $l,l',\ldots$ locations
and with $m,m',\ldots$ memories which  are total functions from
registers and locations to (unbounded) integers.
%
%% We will rely on the following instructions with the associated
%% informal semantics:
%
%% {\footnotesize
%% \[
%% \begin{array}{ll}
%% \s{loadi} \ R, n    &\mbox{store value }n\mbox{ in the register }R \\
%% \s{load} \ R,l   &\mbox{store contents of location }l \mbox{ in the register }R   \\
%% \s{store} \ R,l &\mbox{store contents of register }R \mbox{ in the location }l   \\
%% \s{add}\ R,R',R''  &\mbox{add contents of }R',R''\mbox{ and store it in }R \\
%% \s{branch}\ k      &\mbox{jump with offset }k        \\
%% \s{bge}\  R,R',k     &\mbox{jump with offset }k \mbox{ if contents }R \mbox{ greater or equal than contents }R' \\
%% \s{halt}           &\mbox{stop computation}
%% \end{array}
%% \]}
We denote with $M$ a list of instructions.
The operational semantics is formalized  in
table \ref{semantics-mips} by rules of the shape
$M \Gives (i,m) \arrow (j,m')$, 
where $M$ is a list of $\mips$ instructions, $i,j$ are natural numbers and $m,m'$ are memories.
We write $(M,m) \eval m'$ if 
$M\Gives (0,m) \trarrow (j,m')$ and $M[j]=\s{halt}$.


\begin{table}
{\footnotesize
\[
\begin{array}{l|l}

\mbox{Rule}                                                 & M[i]= \\\hline

M \Gives (i, m) \arrow (i+1, m[n/R])  & \s{loadi} \ R,n \\ 

M \Gives (i, m) \arrow (i+1,m[m(l)/R])  & \s{load} \ R,l \\ 

M \Gives (i, m ) \arrow (i+1,m[m(R)/l]))  & \s{store} \ R,l \\

M \Gives (i, m) 
\arrow (i+1, m[m(R')+m(R'')/R])  & \s{add}\ R,R',R'' \\

M \Gives (i, m) \arrow (i+k+1, m)  & \s{branch}\ k \\

M \Gives (i, m) \arrow (i+1, m)  & \s{bge}\ R,R',k \mbox{ and }m(R)<_{\Z} m(R')\\

M \Gives (i, m) \arrow (i+k+1, m)  & \s{bge}\ R,R',k \mbox{ and }m(R)\geq_{\Z} m(R')
\end{array}
\]}
\caption{Operational semantics $\mips$ programs}\label{semantics-mips}
\end{table}


\subsection{Compilation from $\vm$ to $\mips$}\label{compil-vm-mips-sec}
In order to compile $\vm$ programs to $\mips$ programs we make the following
hypotheses:
(1) for every $\vm$ program variable $x$ we reserve an address $l_x$, 
(2) for every natural number $h\geq b$, we reserve an address $l_h$ (the addresses $l_x,l_h,\ldots$ are all distinct), and
(3) we store the first $b$ elements of the stack $\sigma$ in the registers 
$R_0,\ldots,R_{b-1}$ and the remaining (if any) at the addresses
$l_b,l_{b+1},\ldots$. 

We say that the memory $m$ represents the stack $\sigma$ and 
the store $s$, and write $m\real \sigma,s$, 
if the following conditions are satisfied:
(1) $s(x) = m(l_x)$, and (2) if $0\leq i < |\sigma|$ then
$\sigma[i] = m(R_i)$ if $i<b$, and 
$\sigma[i] = m(l_i)$ if $i\geq b$.



\begin{table}
{\footnotesize
\[
\begin{array}{l|l}

C[i]=          &\cl{C'}(i,C)= 
\\\hline

\s{cnst}(n)  
& \left\{ \begin{array}{lr}
                   (\s{loadi} \ R_h,n)                                &\mbox{if } h=h(i)<b \\
                   (\s{loadi} \ A,n ) \cdot  (\s{store} \ A, l_h)     &\mbox{otherwise}
                   \end{array} \right. \\ 


\s{var}(x)
&  \left\{ \begin{array}{lr}
                   (\s{load} \ R_h,l_x)                           &\mbox{if } h=h(i)<b \\
                   (\s{load} \ A,l_x ) \cdot  (\s{store} \ A, l_h)  &\mbox{otherwise}
                   \end{array} \right. \\ 



\s{add}
& \left\{ \begin{array}{lr}
                     (\s{add} \ R_{h-2} , R_{h-2} , R_{h-1})   &\mbox{if }h=h(i)<(b-1)   \\
                     (\s{load} \ A,l_{h-1}) \cdot (\s{add} \ R_{h-2}, R_{h-2}, A)         &\mbox{if }h=h(i)=(b-1)  \\
                     

                           (\s{load} \ A, l_{h-1}) \cdot (\s{load} \ B,l_{h-2})  &\mbox{if }h=h(i)>(b-1) \\ 
                           (\s{add} \ A,B,A) \cdot (\s{store} \ A, l_{h-2})         
                        \end{array}\right. \\ 

\s{setvar}(x)            
& \left\{ \begin{array}{lr}
                         (\s{store} \ R_{h-1} \ l_x) &\mbox{if }h=h(i)<b\\
                         (\s{load} \ A,l_{h-1})\cdot (\s{store} \ A,l_{x}) &\mbox{if }h=h(i)\geq b
                         \end{array}\right. \\ 



\s{branch}(k)
& (\s{branch} \ k')  \quad \mbox{if }k'=p(i+k+1,C)-p(i+1,C)\\ 


\s{bge}(k)
&\left\{ \begin{array}{lr}
                     (\s{bge} \ R_{h-2} , R_{h-1} , k')                                &\mbox{if }h=h(i)<(b-1)   \\

                     (\s{load} \ A,l_{h-1}) \cdot (\s{bge} \ R_{h-2}, A, k')         &\mbox{if }h=h(i)=(b-1)  \\
                     

                           (\s{load} \ A, l_{h-2}) \cdot (\s{load} \ B,l_{h-1}) \cdot 
                           (\s{bge} \ A,B,k')         &\mbox{if }h=h(i)>(b-1), \  k'= \\

&p(i+k+1,C)-p(i+1,C)
          \end{array}\right. \\ 



\s{halt}
&\s{halt}

\end{array}
\]}
\caption{Compilation from $\vm$ to $\mips$}\label{compil-vm-mips}
\end{table}


The compilation function $\cl{C'}$ from 
$\vm$ to $\mips$ is described in table \ref{compil-vm-mips}.
It operates on a well-formed $\vm$ code $C$ whose last instruction
is $\s{halt}$. Hence, by proposition \ref{well-formed-prop}(3), 
there is a unique $h$ such that $C:h$.
We denote with $\cl{C'}(C)$ the concatenation $\cl{C'}(0,C)\cdots \cl{C'}(|C|-1,C)$.
Given a well formed $\vm$ code $C$ with $i<|C|$ we denote with 
$p(i,C)$ the position of the first instruction in $\cl{C'}(C)$ which
corresponds to the compilation of the instruction with position $i$ in $C$.
This is defined as\footnote{There is an obvious circularity in this definition that can be easily eliminated by defining first the function 
$d$ following the case
analysis in table \ref{compil-vm-mips}, then the function $p$, and finally the function $\cl{C'}$ as in table \ref{compil-vm-mips}.}
$p(i,C) = \Sigma_{0\leq j <i} d(i,C)$,
where the function $d(i,C)$ is defined as 
$d(i,C) = |\cl{C'}(i,C)|$.
Hence $d(i,C)$ is the number of $\mips$ instructions associated
with the $i^{\w{th}}$ instruction of the (well-formed) $C$ code.
The functional correctness of the compilation function can then be stated 
as follows.



\begin{proposition}\label{simulation-vm-mips}
Let $C : h$ be a well formed code.
If  $C \Gives (i,\sigma,s) \arrow (j,\sigma',s')$ with $h(i) = |\sigma|$ and  $m \real \sigma,s$
then 
$\cl{C'}(C) \Gives (p(i,C),m) \trarrow (p(j,C),m')$ and $m'\real \sigma',s'$.
\end{proposition}

\newpage

\section{Proofs}\label{paper-proofs}

We omit the proofs that have been mechanically checked by K. Memarian
and R. Saillard with the $\coq$ proof assistant~\footnote{
These proofs can be downloaded at \url{http://www.pps.jussieu.fr/~yrg/miniCerCo/}
and at \url{http://www.pps.jussieu.fr/~saillard}. 
}.


% THIS HAS BEEN CHECKED IN COQ
%% \subsection{Proof  of proposition \ref{unicity-height-prop}}
%% \Proofitemf{(1)} By induction on the reduction length and by case analysis
%% on the last instruction being executed. 

%% \Proofitem{(2)} If $h(i)=h'(i)$ for $i=0,\ldots,k$ and $k<|C|$ then,
%% by case analysis on the instruction $C[k]$, we check that 
%% the conditions in table \ref{well-formed-instr} force $h(k+1)=h'(k+1)$. \qed 

\subsection{Notation}
Let $\act{t}$ be a family of reduction relations where 
$t$ ranges over the set of labels and $\epsilon$. Then we 
define:
\[
\wact{t} = \left\{
\begin{array}{ll}
(\act{\epsilon})^* &\mbox{if }t=\epsilon \\
(\act{\epsilon})^* \comp \act{t} \comp (\act{\epsilon})^*  &\mbox{otherwise}
\end{array}
\right.
\]
where as usual $R^*$ denote the reflexive and transitive closure of the relation $R$ 
and $\comp$ denotes the composition of relations.

%%     \item[$(e_1<e_2) \eval \s{false}$] We set $j=c$. 
%%       \begin{itemize}
%%      \item The instance of $(1)$ is  $(S,K,s) \arrow (S_2,K,s)$.
%%      \item The reduction required in $(6)$ takes the form 
%% $C \Gives (i,\sigma,s) \trarrow (i',\sigma,s) \trarrow (c,\sigma,s')$, and it
%% follows from $(3')$, the fact that $(e_1<e_2) \eval \s{false}$, and proposition \ref{soundness-big-step-prop}(3).
%%      \item Property $(7)$ follows from fact $(5)$ and the following proof tree:

%% {\footnotesize         $$ \infer{j \access{C} j \quad R(C,i'',K) }{R(C,j,S_2 \cdot K)} ~.$$ }

%% ~\qed
%%       \end{itemize}
%%   \end{description}


%% \subsection{Proof of proposition \ref{well-formed-prop}}
%% \Proofitemf{(1)}
%% By induction on $e$. For the inductive step, suppose
%% we have $\cl{C}(e_1):h_1$ with $h_1(0)=n$ and 
%% $\cl{C}(e_2):h_2$ with $h_2(0)=n+1$. Then we can build
%% $h$ such that $\cl{C}(e_1+e_2):h$ and $h(0)=n$ 
%% by glueing $h_1$ and $h_2$.
%% \Proofitem{(2)}
%% By induction on $S$.
%% \Proofitem{(3)} Consequence of (2). \qed


%% \subsection{Proof of proposition \ref{well-formed-prop}}
%% We actually prove that for any expression $e$, statement $S$, and program $P$ the
%% following holds:

%% \Defitem{(1)} 
%% For any $n\in\Nat$ there is a unique $h$ such that 
%% $\cl{C}(e):h$, $h(0)=n$, and $h(|\cl{C}(e)|)=h(0)+1$.

%% \Defitem{(2)}
%% For any $S$, 
%% there is a unique $h$ such that $\cl{C}(S):h$, $h(0)=0$, and 
%% $h(|\cl{C}(e)|)=0$.

%% \Defitem{(3)}
%% There is a unique $h$ such that $\cl{C}(P):h$.



\subsection{Proof of proposition \ref{labelled-sim-imp-vm}} 

\Defitemf{(1)} By induction on the structure of the command $S$.

\Defitem{(2)} By iterating the following proposition.

\begin{proposition}
  If $(S,K,s) \stackrel{t}{\arrow} (S',K',s')$ and $R(C,i,S\cdot K)$ with $t=\ell$ or $t=\epsilon$ then 
  $C\Gives (i,\sigma,s) \wact{t} (j,\sigma,s')$ and
  $R(C,j,S'\cdot K')$.
\end{proposition}

This is an extension of proposition \ref{soundness-small-step} and it is proven in the same way with
an additional case for labelled commands. \qed

\subsection{Proof of proposition \ref{sim-vm-mips-prop}} 
\Proofitemf{(1)} The compilation of the $\vm$ instruction $\s{nop}(\ell)$ is the $\mips$ instruction $(\s{nop} \ \ell)$.

\Proofitem{(2)}                         
By iterating the following proposition.

\begin{proposition}
Let $C : h$ be a well formed code.
If  $C \Gives (i,\sigma,s) \stackrel{t}\arrow (j,\sigma',s')$ with $t=\ell$ or $t=\epsilon$, $h(i) = |\sigma|$ and  $m \real \sigma,s$
then 
$\cl{C'}(C) \Gives (p(i,C),m) \wact{t} (p(j,C),m')$ and $m'\real \sigma',s'$.
\end{proposition} 

%% This is an extension of proposition \ref{simulation-vm-mips} and it is proven in the same way
%% with an additional case for the \s{nop} instruction.\qed

\subsection{Proof of proposition \ref{lab-instr-erasure-imp}} 
We extend the instrumentation to the continuations by defining:
\[
\cl{I}(S\cdot K) = \cl{I}(S)\cdot \cl{I}(K) \qquad
\cl{I}(\s{halt}) = \s{halt}~.
\]
Then we examine the possible reductions of a configuration
$(\cl{I}(S),\cl{I}(K),s[c/\w{cost}])$.

\begin{itemize}

\item
If $S$ is an unlabelled statement such as $\s{while} \ b \ \s{do} \ S'$
then $\cl{I}(S) = \s{while} \ b \ \s{do} \ \cl{I}(S')$ and 
assuming $(b,s) \eval \s{true}$ the reduction step is:
\[
(\cl{I}(S),\cl{I}(K),s[c/\w{cost}]) \arrow
(\cl{I}(S'), \cl{I}(S)\cdot \cl{I}(K),s[c/\w{cost}])~.
\]
Noticing that $\cl{I}(S)\cdot \cl{I}(K) = \cl{I}(S\cdot K)$,
this step is matched in the labelled language as follows:
\[
(S,K,s[c/\w{cost}]) \arrow
(S', S\cdot K,s[c/\w{cost}])~.
\]

\item On the other hand, if $S=\ell:S'$ is a labelled statement 
then $\cl{I}(S)= \w{inc}(\ell);\cl{I}(S')$ 
and, by a sequence of reductions steps, we have:
\[
(\cl{I}(S),\cl{I}(K),s[c/\w{cost}]) \trarrow
(\cl{I}(S'), \cl{I}(K),s[c+\kappa(\ell)/\w{cost}])~.
\]
This step is matched by the labelled reduction:
\[
(S,K,s[c/\w{cost}]) \act{\ell}
(S', K,s[c/\w{cost}])~.
\]
~\qed
\end{itemize}
%This is a direct proof on the 
%In order to carry on the proof, one needs to develop a bit
%more the properties of the small-step operational semantics.
%In particular, one needs to show that a continuation such
%as $S\cdot (S'\cdot K)$ is `observationally equivalent' to the
%continuation  $(S;S')\cdot K$. \marginpar{This should be simplified now!}
% CAN INSERT HERE PROOF ONCE IT IS CHECKED \input{instrumentation-proof}
%\qed
%Let $S_A$ denote a command
%which cannot be decomposed as $S;S'$.
%
%\begin{definition}
%Given a continuation $K$, its flattening $\w{flat}(K)$ is defined
%as follows:
%\[
%\begin{array}{ll}
%
%\w{flat}(\s{halt})      &=\s{halt} \\
%\w{flat}((S;S')\cdot K) &=\w{flat}(S,S'\cdot K) \\
%\w{flat}(S_A \cdot K)     &=S_A \cdot \w{flat}(K)
%
%\end{array}
%\]
%\end{definition}
%
%We write $K\equiv K'$ if $\w{flat}(K)=\w{flat}(K')$.
%
%\begin{lemma}
%If $\w{flat}(S\cdot K) = S_A \cdot K'$ then
%$(S,K,s) \trarrow (S_A,K'',s)$ and 
%$K' \equiv K''$.
%\end{lemma}

%\begin{lemma}
%If $S_1\cdot K_1 \equiv S_2\cdot K_2$ and 
%$(S_1,K_1,s) \arrow (S'_1,K'_1,s')$ then
%$(S_2,K_2,s) \trarrow (S'_2,K'_2,s')$ and 
%$S'_1 \cdot K'_1 \equiv S'_2 \cdot K'_2$.
%\end{lemma}

%\begin{definition} 
%  The relation $\equiv$ between continuations of $\imp_\ell$ and $\imp$ is defined inductively by the following rules :
%  $$ 
%  \infer{}{\s{\s{halt}} \equiv \s{\s{halt}}}(R_0) \quad
%  \infer{K \equiv K' \quad S'=\cl{I}(S)}{S.K \equiv S'.K'}(R_1) \quad
%  \infer{K \equiv K' \quad (S';S'')=\cl{I}(S)}{S.K \equiv S'.S''.K'}(R_2)
%  $$
%  We write $S.K \equiv_{R_i} S'.K'$ ($i$ = 1 or 2) when the last rule used to infer $S.K\equiv S'.K'$ is $R_i$.
%\end{definition}

%\begin{lemma}\label{equiv-lem}\ $\\$
%  If $S\in \{\s{skip},(x:=e),\s{if} b \s{then} S_t \s{else} S_f,\s{while} b \s{do} S_w\}$ then $S.K\equiv S'.K' \Rightarrow S.K \equiv_{R_1} S'.K'$
%\end{lemma}
%This comes from the fact that to apply rule $R_2$, $\cl{I}(S)$ must have the form $S';S''$.
%
%\begin{definition} 
%  The predicate $\mathcal{T}$ associate states of $\imp_\ell$ with states of $\imp$.
%  $$ \mathcal{T}((S_1,K_1,s_1),(S_2,K_2,s_2)) := S_1.K_1\equiv S_2.K_2 \text{ and } s_2=s_1[cost \leftarrow c]$$
%\end{definition}
%
%We, now formulate the small-step version of the theorem of correction of instrumentation.
 

\subsection{Proof of proposition \ref{global-commutation-prop}}
By diagram chasing using propositions \ref{labelled-sim-imp-vm}(1),
\ref{sim-vm-mips-prop}(1), and the definition \ref{labelling-def} of labelling. \qed


\subsection{Proof of proposition \ref{instrument-to-label-prop}}
Suppose that:
$$ (\cl{I}(\cl{L}(P)),s[c/\w{cost}]) \eval s'[c+\delta/\w{cost}] \text{ and } m\real s[c/\w{cost}]~. $$
Then, by proposition  \ref{lab-instr-erasure-imp}, for some $\lambda$:
$$ (\cl{L}(P),s[c/\w{cost}])\eval (s'[c/\w{cost}],\lambda) \text{ and } \kappa(\lambda)=\delta~. $$ 
Finally, by propositions  \ref{labelled-sim-imp-vm}(2) and \ref{sim-vm-mips-prop}(2) : 
$$ (\cl{C'}(\cl{C}(\cl{L}(P))),m) \eval (m',\lambda) \text{ and } m'\real s'[c/\w{cost}]~.$$
\qed

\subsection{Proof of proposition \ref{sound-label-prop}}
 If $\lambda=\ell_1 \cdots \ell_n$ then the 
computation is the concatenation of simple paths 
labelled with $\ell_1,\ldots,\ell_n$. Since $\kappa(\ell_i)$
bounds the cost of a simple path labelled with $\ell_i$, the
cost of the overall computation is bounded by $\kappa(\lambda)=
\kappa(\ell_1)+\cdots \kappa(\ell_n)$. \qed 


\subsection{Proof of proposition \ref{precise-label-prop}}
Same proof as proposition \ref{sound-label-prop}, by replacing the word \emph{bounds} by \emph{is exactly} and the words \emph{bounded by} by \emph{exactly}. \qed

\subsection{Proof of proposition \ref{lab-sound}}  
In both labellings under consideration the root node is labelled.  An
obvious observation is that only commands of the shape \s{while} $b$
\s{do} $S$
%lab-bool and \s{while} $lb$ \s{do} $S$ 
introduce loops in the compiled code.  
%lab-bool In the second case, the compilation ensures that a label is placed in the loop.  
%\lab-boolIn the first case, 
We notice that both labelling introduce a label in the loop (though at different places).
Thus all loops go through a label and the compiled code is always sound.

To show the precision of the second labelling $\cl{L}_p$, we note the
following property. %\marginpar{This seems unchanged.}

\begin{lemma}\label{precise-lemma}
A soundly labelled graph is precise if each label occurs at most once in the graph and 
if the immediate successors of the \s{bge} nodes are either \s{halt} (no successor) or labelled nodes.
\end{lemma}

Indeed, in a such a graph starting from a labelled node we can follow a unique path
up to a leaf, another labelled node, or a $\s{bge}$ node. In the last case, the 
hypotheses in the lemma \ref{precise-lemma} guarantee that the two 
simple paths one can follow from the $\s{bge}$ node have
the same length/cost.  \qed



%% This comes from the fact that, in such a graph, each labelled node has an unique simple path. \qed
%% The preciseness of $\cl{L}$ comes from the fact that, for any program $P$, $\cl{C'}(\cl{C}(\cl{L}_p(P)))$ satisfies the condition of lemma \ref{precise-lemma}.
%% This can be proved by induction on the command, knowing that:
%% A \s{beq} node appears only, if a \s{if then else} command or a \s{while do} command is compiled.
%% In the \s{if then else} case, the \s{beq} node is followed by the first instruction of each branch, which are the first instruction of the compiled code of a labelled command: a \s{nop} instruction.
%% In the \s{while do} case, the \s{beq} node is followed by the first instruction of compiled code of the labelled body loop, which is a \s{nop} instruction, and, if any, by the first instruction of the compiled code of the labelled command following the loop, a \s{nop} instruction, or by a \s{halt} instruction which is a leaf.
%% \qed




\subsection{Proof of proposition \ref{ann-correct}} 
By applying consecutively proposition \ref{instrument-to-label-prop}
and propositions \ref{sound-label-prop} or \ref{precise-label-prop}. \qed

\subsection{Proof of proposition \ref{soundness-small-step}} 
Given a $\vm$ code $C$, we define an `accessibility relation' 
$\access{C}$ as the least binary relation on $\set{0,\ldots,|C|-1}$ such that:

{\footnotesize
\[
\begin{array}{ll}

\infer{}
{i\access{C} i}
\qquad \qquad
&\infer{C[i]=\s{branch}(k)\quad (i+k+1)\access{C} j}
{i\access{C} j}

\end{array}
\]}

We also introduce a ternary relation $R(C,i,K)$ which relates 
a $\vm$ code $C$, a number $i\in\set{0,\ldots,|C|-1}$ and a continuation
$K$. 
The relation is 
defined as the least one that satisfies the following conditions.

{\footnotesize
\[
\begin{array}{ll}

\infer{
\begin{array}{c}
\\
i\access{C} j\qquad C[j]=\s{halt}
\end{array}}
{R(C,i,\s{halt})}

\qquad \qquad
&\infer{
\begin{array}{c}
i\access{C} i'\quad C=C_1 \cdot \cl{C}(S) \cdot C_2\\ 
i'=|C_1|\quad j=|C_1\cdot \cl{C}(S)| \quad R(C,j,K)
\end{array}}
{R(C,i,S\cdot K)}~.

\end{array}
\]}

The following properties are useful.

\begin{lemma}\label{access-lemma}
\Defitemf{(1)} The relation $\access{C}$ is transitive.

\Defitem{(2)}  If $i\access{C} j$ and $R(C,j,K)$ then $R(C,i,K)$.
\end{lemma}
The first property can be proven by induction on the definition of $\access{C}$ and  the second by induction on the structure of $K$. 
%\begin{lemma}
%\begin{enumerate}
%\item If $i \access{C} j$ then $C\Gives (i,\sigma,s) \trarrow (j,\sigma,s)$.
%\item If $i\access{C} j$ and $j\access{C} k$ then $i\access{C} k$.
%\item If $i\access{C}j$ and $R(C,j,K)$ then $R(C,i,K)$.
%\item $R(C,i,K)$ iff $R(C,i,(\s{skip})\cdot K)$.
%\end{enumerate}
%\end{lemma}


Next we can focus on the proposition.
The notation $C \stackrel{i}{\cdot} C'$ means that $i=|C|$.
Suppose that:

{\footnotesize
\[
\begin{array}{lll}
(S,K,s) \arrow (S',K',s') \quad (1)  &\text{and}  &R(C,i,S\cdot K) \quad (2)~.
\end{array}
\]}
From $(2)$, we know that there exist $i'$ and $i''$ such that:

{\footnotesize\[
\begin{array}{llll}
i \access{C} i' \quad (3),
&C=C_1\stackrel{i'}{\cdot}\cl{C}(S)\stackrel{i''}{\cdot}C_2 \quad (4), 
&\text{and} 
&R(C,i'',K) \quad (5)
\end{array}
\]}
and from $(3)$ it follows that:

{\footnotesize
\[ C\Gives (i,\sigma,s) \trarrow (i',\sigma,s) \quad (3')~.
\]}
We are looking for $j$ such that:

{\footnotesize
\[
\begin{array}{lll}
C \Gives (i,\sigma,s) \trarrow (j,\sigma,s') \quad (6), 
&\text{and} 
&R(C,j,S'\cdot K') \quad (7) ~.
\end{array}
\]}
We proceed by case analysis on $S$. We just detail the case of the conditional command as the
the remaining cases have similar proofs.
If $S=\s{if}$ $e_1<e_2$ $\s{then}$ $S_1$ $\s{else}$ $S_2$ then $(4)$ is rewritten as follows:

{\footnotesize  $$ C=C_1\stackrel{i'}{\cdot}\cl{C}(e_1)\cdot \cl{C}(e_2).\s{bge}(k_1)\stackrel{a}{\cdot}\cl{C}(S_1)\stackrel{b}{\cdot}\s{branch}(k_2) 
\stackrel{c}{\cdot} \cl{C}(S_2)\stackrel{i''}{\cdot}C_2~ $$}
where $c = a+k_1$ and $i''=c+k_2$.
  We distinguish two cases according to the evaluation of the boolean condition.
We describe the case 
%  \begin{description}
%\item[
$(e_1<e_2) \eval \s{true}$. We set $j=a$.
\begin{itemize}
        \item The instance of $(1)$ is $(S,K,s) \arrow (S_1,K,s)$.
        \item The reduction required in (6) takes the form 
$C \Gives (i,\sigma,s) \trarrow (i',\sigma,s) \trarrow (a,\sigma,s')$,
and it follows from $(3')$, the fact that $(e_1<e_2) \eval \s{true}$, and 
proposition \ref{soundness-big-step-prop}(2).

        \item Property $(7)$, follows from lemma \ref{access-lemma}(2), fact $(5)$, and 
the following proof tree:

{\footnotesize    
$$ \infer{j\access{C} j \quad \infer{b \access{C} i'' \quad R(C,i'',K)}{R(C,b,K)}}{R(C,j,S_1\cdot K)} ~.$$ }
~\qed
\end{itemize}



\newpage


\section{A $\C$ compiler}\label{C-compiler-sec}

This section gives an informal overview of the compiler, in particular it
highlights the main features of the intermediate languages, the purpose of the
compilation steps, and the optimisations. 
%For practical reasons, the compiler does not support the \texttt{float} type.
%(*** We could have a running example. ***)

\subsection{$\Clight$} 
$\Clight$ is a large subset of the $\C$ language that we adopt as
the source language of our compiler. 
It features most of the types and operators
of $\C$. It includes pointer arithmetic, pointers to
functions, and \texttt{struct} and \texttt{union} types, as well as
all $\C$ control structures. The main difference with the $\C$
language is that $\Clight$ expressions are side-effect free, which
means that side-effect operators ($\codeex{=}$,$\codeex{+=}$,$\codeex{++}$,$\ldots$) and function calls
within expressions are not supported. 
Given a $\C$ program, we rely on the $\cil$ tool~\cite{CIL02} to deal 
with the idiosyncrasy of  $\C$ concrete syntax and to produce an
equivalent program in $\Clight$ abstract syntax.
We refer to  the $\compcert$ project~\cite{Leroy09} 
for a formal definition of the
$\Clight$ language. Here we just recall  in 
figure \ref{syntax-clight} its syntax which is 
classically structured in expressions, statements, functions, 
and whole programs. In order to limit the implementation effort,
our current compiler for $\Clight$ does {\em not} cover the operators
relating to the floating point type {\tt float}. So, in a nutshell,
the fragment of $\C$ we have implemented is $\Clight$ without
floating point.

There is a notable difficulty to compile the $\C$ language into
$\intel$ assembly code due to the fact that $\intel$'s machine word are
8bits long and $\C$ has 32bits primitive datatypes. To deal with the
dissimilarity in that case, we first translate the $\Clight$ input
program into a $\Clight$ input program that only uses 8bits primitive
datatypes. 

\begin{figure}
  \label{syntax-clight}
  \footnotesize{
  \begin{tabular}{l l l l}
    Expressions: & $a$ ::= & $id$               & variable identifier \\
    & & $|$ $n$                                 & integer constant \\
%    & & $|$ $f$                                & float constant \\
    & & $|$ \texttt{sizeof}($\tau$)             & size of a type \\
    & & $|$ $op_1$ $a$                          & unary arithmetic operation \\
    & & $|$ $a$ $op_2$ $a$                      & binary arithmetic operation \\
    & & $|$ $*a$                                & pointer dereferencing \\
    & & $|$ $a.id$                              & field access \\
    & & $|$ $\&a$                               & taking the address of \\
    & & $|$ $(\tau)a$                           & type cast \\
    & & $|$ $a ? a : a$                         & conditional expression \\[10pt]
    Statements: & $s$ ::= & \texttt{skip}       & empty statement \\
    & & $|$ $a=a$                               & assignment \\
    & & $|$ $a=a(a^*)$                          & function call \\
    & & $|$ $a(a^*)$                            & procedure call \\
    & & $|$ $s;s$                               & sequence \\
    & & $|$ \texttt{if} $a$ \texttt{then} $s$ \texttt{else} $s$ & conditional \\
    & & $|$ \texttt{switch} $a$ $sw$            & multi-way branch \\
    & & $|$ \texttt{while} $a$ \texttt{do} $s$  & ``while'' loop \\
    & & $|$ \texttt{do} $s$ \texttt{while} $a$  & ``do'' loop \\
    & & $|$ \texttt{for}($s$,$a$,$s$) $s$       & ``for'' loop\\
    & & $|$ \texttt{break}                      & exit from current loop \\
    & & $|$ \texttt{continue}                   & next iteration of the current loop \\
    & & $|$ \texttt{return} $a^?$               & return from current function \\
    & & $|$ \texttt{goto} $lbl$                 & branching \\
    & & $|$ $lbl$ : $s$                         & labelled statement \\[10pt]
    Switch cases: & $sw$ ::= & \texttt{default} : $s$           & default case \\
    & & $|$ \texttt{case } $n$ : $s;sw$                         & labelled case \\[10pt]
    Variable declarations: & $dcl$ ::= & $(\tau\quad id)^*$             & type and name\\[10pt]
    Functions: & $Fd$ ::= & $\tau$ $id(dcl)\{dcl;s\}$   & internal function \\
    & & $|$ \texttt{extern} $\tau$ $id(dcl)$                    & external function\\[10pt]
    Programs: & $P$ ::= & $dcl;Fd^*;\texttt{main}=id$           & global variables, functions, entry point
  \end{tabular}}
  \caption{Syntax of the $\Clight$ language}
\end{figure}


\subsection{$\Cminor$}

$\Cminor$ is a simple, low-level imperative language, comparable to a
stripped-down, typeless variant of $\C$. Again we refer 
to the $\compcert$ project for its formal definition 
and we just recall in figure \ref{syntax-cminor}
its syntax which as for $\Clight$ is structured in
expressions, statements, functions, and whole programs.

\begin{figure}
  \label{syntax-cminor}
  \footnotesize{
  \begin{tabular}{l l l l}
    Signatures: & $sig$ ::= & \texttt{sig} $\vec{\texttt{int}}$ $(\texttt{int}|\texttt{void})$ & arguments and result \\[10pt]
    Expressions: & $a$ ::= & $id$               & local variable \\
     & & $|$ $n$                                & integer constant \\
%     & & $|$ $f$                               & float constant \\
     & & $|$ \texttt{addrsymbol}($id$)          & address of global symbol \\
     & & $|$ \texttt{addrstack}($\delta$)       & address within stack data \\
     & & $|$ $op_1$ $a$                         & unary arithmetic operation \\
     & & $|$ $op_2$ $a$ $a$                     & binary arithmetic operation \\
     & & $|$ $\kappa[a]$                        & memory read\\
     & & $|$ $a?a:a$                    & conditional expression \\[10pt]
    Statements: & $s$ ::= & \texttt{skip}       & empty statement \\
    & & $|$ $id=a$                              & assignment \\
    & & $|$ $\kappa[a]=a$                       & memory write \\
    & & $|$ $id^?=a(\vec{a}):sig$               & function call \\
    & & $|$ \texttt{tailcall} $a(\vec{a}):sig$  & function tail call \\
    & & $|$ \texttt{return}$(a^?)$              & function return \\
    & & $|$ $s;s$                               & sequence \\
    & & $|$ \texttt{if} $a$ \texttt{then} $s$ \texttt{else} $s$         & conditional  \\
    & & $|$ \texttt{loop} $s$                   & infinite loop \\
    & & $|$ \texttt{block} $s$          & block delimiting \texttt{exit} constructs \\
    & & $|$ \texttt{exit} $n$                   & terminate the $(n+1)^{th}$ enclosing block \\
    & & $|$ \texttt{switch} $a$ $tbl$           & multi-way test and exit\\
    & & $|$ $lbl:s$                             & labelled statement \\
    & & $|$ \texttt{goto} $lbl$                 & jump to a label\\[10pt]
    Switch tables: & $tbl$ ::= & \texttt{default:exit}($n$) & \\
    & & $|$ \texttt{case} $i$: \texttt{exit}($n$);$tbl$ & \\[10pt]
    Functions: & $Fd$ ::= & \texttt{internal} $sig$ $\vec{id}$ $\vec{id}$ $n$ $s$ & internal function: signature, parameters, \\
    & & & local variables, stack size and body \\
    & & $|$ \texttt{external} $id$ $sig$ & external function \\[10pt]
    Programs: & $P$ ::= & \texttt{prog} $(id=data)^*$ $(id=Fd)^*$ $id$   & global variables, functions and entry point 
  \end{tabular}}
  \caption{Syntax of the $\Cminor$ language}
\end{figure}

\paragraph{Translation of $\Clight$ to $\Cminor$}
As in $\Cminor$ stack operations are made explicit, one has to know
which variables are stored in the stack. This 
information is produced by a static analysis that determines
the variables whose address may be `taken'. 
Also space is reserved for local arrays and structures. In a
second step, the proper compilation is performed: it consists mainly
in translating $\Clight$ control structures to the basic
ones available in $\Cminor$.

\subsection{$\RTLAbs$}

$\RTLAbs$ is the last architecture independent language in the
compilation process.  It is a rather straightforward {\em abstraction} of
the {\em architecture-dependent} $\RTL$ intermediate language
available in the $\compcert$ project and it is intended to factorize
some work common to the various target assembly languages
(e.g. optimizations) and thus to make retargeting of the compiler a
simpler matter.

We stress that in $\RTLAbs$ the structure of $\Cminor$ expressions
is lost and that this may have a negative impact on the following
instruction selection step. 
Still, 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.



\paragraph{Syntax.}
In $\RTLAbs$, programs are represented as \emph{control flow
  graphs} (CFGs for short). We associate with the nodes of the graphs 
instructions reflecting the $\Cminor$ commands. As usual, commands that change the control
flow of the program (e.g. loops, conditionals) are translated by inserting 
suitable branching instructions in the CFG.
The syntax of the language is depicted in table
\ref{RTLAbs:syntax}. Local variables are now represented by \emph{pseudo
  registers} that are available in unbounded number. The grammar rule $\w{op}$ that is
not detailed in table \ref{RTLAbs:syntax} defines usual arithmetic and boolean
operations (\codeex{+}, \codeex{xor}, \codeex{$\le$}, etc.) as well as constants
and conversions between sized integers.

\begin{table}
{\footnotesize
\[
\begin{array}{lllllll}
\w{return\_type} & ::= & \s{int} \Alt \s{void} & \qquad
\w{signature} & ::= & (\s{int} \rightarrow)^*\ \w{return\_type}\\
\end{array}
\]

\[
\begin{array}{lllllll}
\w{memq} & ::= & \s{int8s} \Alt \s{int8u} \Alt \s{int16s} \Alt \s{int16u}
                 \Alt \s{int32} & \qquad
\w{fun\_ref} & ::= & \w{fun\_name} \Alt \w{psd\_reg}
\end{array}
\]

\[
\begin{array}{llll}
\w{instruction} & ::= & \Alt \s{skip} \rightarrow \w{node} &
                        \quad \mbox{(no instruction)}\\
                &     & \Alt \w{psd\_reg} := \w{op}(\w{psd\_reg}^*)
                        \rightarrow \w{node} & \quad \mbox{(operation)}\\
                &     & \Alt \w{psd\_reg} := \s{\&}\w{var\_name}
                        \rightarrow \w{node} &
                        \quad \mbox{(address of a global)}\\
                &     & \Alt \w{psd\_reg} := \s{\&locals}[n]
                        \rightarrow \w{node} &
                        \quad \mbox{(address of a local)}\\
                &     & \Alt \w{psd\_reg} := \w{fun\_name}
                        \rightarrow \w{node} &
                        \quad \mbox{(address of a function)}\\
                &     & \Alt \w{psd\_reg} :=
                        \w{memq}(\w{psd\_reg}[\w{psd\_reg}])
                        \rightarrow \w{node} & \quad \mbox{(memory load)}\\
                &     & \Alt \w{memq}(\w{psd\_reg}[\w{psd\_reg}]) :=
                        \w{psd\_reg}
                        \rightarrow \w{node} & \quad \mbox{(memory store)}\\
                &     & \Alt \w{psd\_reg} := \w{fun\_ref}(\w{psd\_reg^*}) :
                        \w{signature} \rightarrow \w{node} &
                        \quad \mbox{(function call)}\\
                &     & \Alt \w{fun\_ref}(\w{psd\_reg^*}) : \w{signature}
                        & \quad \mbox{(function tail call)}\\
                &     & \Alt \s{test}\ \w{op}(\w{psd\_reg}^*) \rightarrow
                        \w{node}, \w{node} & \quad \mbox{(branch)}\\
                &     & \Alt \s{return}\ \w{psd\_reg}? & \quad \mbox{(return)}
\end{array}
\]

\[
\begin{array}{lll}
\w{fun\_def} & ::= & \w{fun\_name}(\w{psd\_reg}^*): \w{signature}\\
             &     & \s{result:} \w{psd\_reg}?\\
             &     & \s{locals:} \w{psd\_reg}^*\\
             &     & \s{stack:} n\\
             &     & \s{entry:} \w{node}\\
             &     & \s{exit:} \w{node}\\
             &     & (\w{node:} \w{instruction})^*
\end{array}
\]

\[
\begin{array}{lllllll}
\w{init\_datum} & ::= & \s{reserve}(n) \Alt \s{int8}(n) \Alt \s{int16}(n)
                       \Alt \s{int32}(n) & \qquad
\w{init\_data} & ::= & \w{init\_datum}^+
\end{array}
\]

\[
\begin{array}{lllllll}
\w{global\_decl} & ::= & \s{var}\ \w{var\_name} \w{\{init\_data\}} & \qquad
\w{fun\_decl} & ::= & \s{extern}\ \w{fun\_name} \w{(signature)} \Alt
                      \w{fun\_def}
\end{array}
\]

\[
\begin{array}{lll}
\w{program} & ::= & \w{global\_decl}^*\\
            &     & \w{fun\_decl}^*
\end{array}
\]}
\caption{Syntax of the $\RTLAbs$ language}\label{RTLAbs:syntax}
\end{table}

\paragraph{Translation of $\Cminor$ to $\RTLAbs$.}
Translating $\Cminor$ programs to $\RTLAbs$ programs mainly consists in
transforming $\Cminor$ commands in CFGs. Most commands are sequential and have a
rather straightforward linear translation. A conditional is translated in a
branch instruction; a loop is translated using a back edge in the CFG.



\subsection{$\RTL$}

As in $\RTLAbs$, the structure of $\RTL$ programs is based on
CFGs. $\RTL$ is the first architecture-dependant intermediate language
of our compiler which, in its current version, targets the $\mips$ and
$\intel$ assembly languages.

\paragraph{Syntax.}
$\RTL$ is very close to $\RTLAbs$. It is based on CFGs and explicits
the $\mips$ or the $\intel$ instructions corresponding to the
$\RTLAbs$ instructions. Type information disappears: everything is
represented using machine words. Moreover, each global of the
program is associated to an offset. The syntax of the language can be
found in table \ref{RTL:syntax}. The grammar rules $\w{unop}$,
$\w{binop}$, $\w{uncon}$, and $\w{bincon}$, respectively, represent
the sets of unary operations, binary operations, unary conditions and
binary conditions of the target assembly language.

\begin{table}
{\footnotesize
\[
\begin{array}{lllllll}
\w{size} & ::= & \s{Byte} \Alt \s{HalfWord} \Alt \s{Word}  & \qquad
\w{fun\_ref} & ::= & \w{fun\_name} \Alt \w{psd\_reg}
\end{array}
\]

\[
\begin{array}{llll}
\w{instruction} & ::= & \Alt \s{skip} \rightarrow \w{node} &
                        \quad \mbox{(no instruction)}\\
                &     & \Alt \w{psd\_reg} := n
                        \rightarrow \w{node} & \quad \mbox{(constant)}\\
                &     & \Alt \w{psd\_reg} := \w{unop}(\w{psd\_reg})
                        \rightarrow \w{node} & \quad \mbox{(unary operation)}\\
                &     & \Alt \w{psd\_reg} :=
                        \w{binop}(\w{psd\_reg},\w{psd\_reg})
                        \rightarrow \w{node} & \quad
                        \mbox{(binary operation)}\\
                &     & \Alt \w{psd\_reg} := \s{\&globals}[n]
                        \rightarrow \w{node} &
                        \quad \mbox{(address of a global)}\\
                &     & \Alt \w{psd\_reg} := \s{\&locals}[n]
                        \rightarrow \w{node} &
                        \quad \mbox{(address of a local)}\\
                &     & \Alt \w{psd\_reg} := \w{fun\_name}
                        \rightarrow \w{node} &
                        \quad \mbox{(address of a function)}\\
                &     & \Alt \w{psd\_reg} :=
                        \w{size}(\w{psd\_reg}[n])
                        \rightarrow \w{node} & \quad \mbox{(memory load)}\\
                &     & \Alt \w{size}(\w{psd\_reg}[n]) :=
                        \w{psd\_reg}
                        \rightarrow \w{node} & \quad \mbox{(memory store)}\\
                &     & \Alt \w{psd\_reg} := \w{fun\_ref}(\w{psd\_reg^*})
                        \rightarrow \w{node} &
                        \quad \mbox{(function call)}\\
                &     & \Alt \w{fun\_ref}(\w{psd\_reg^*})
                        & \quad \mbox{(function tail call)}\\
                &     & \Alt \s{test}\ \w{uncon}(\w{psd\_reg}) \rightarrow
                        \w{node}, \w{node} & \quad
                        \mbox{(branch unary condition)}\\
                &     & \Alt \s{test}\ \w{bincon}(\w{psd\_reg},\w{psd\_reg})
                        \rightarrow \w{node}, \w{node} & \quad
                        \mbox{(branch binary condition)}\\
                &     & \Alt \s{return}\ \w{psd\_reg}? & \quad
                        \mbox{(return)}
\end{array}
\]

\[
\begin{array}{lllllll}
\w{fun\_def} & ::= & \w{fun\_name}(\w{psd\_reg}^*) & \qquad
\w{program} & ::= & \s{globals}: n\\
             &     & \s{result:} \w{psd\_reg}? & \qquad
            &     & \w{fun\_def}^*\\
             &     & \s{locals:} \w{psd\_reg}^*\\
             &     & \s{stack:} n\\
             &     & \s{entry:} \w{node}\\
             &     & \s{exit:} \w{node}\\
             &     & (\w{node:} \w{instruction})^*
\end{array}
\]}
\caption{Syntax of the $\RTL$ language}\label{RTL:syntax}
\end{table}

\paragraph{Translation of $\RTLAbs$ to $\RTL$.}
This translation is mostly straightforward. A $\RTLAbs$ instruction is often
directly translated to a corresponding assembly instruction. There are a few
exceptions: some $\RTLAbs$ instructions are expanded in two or more assembly
instructions. When the translation of a $\RTLAbs$ instruction requires more than
a few simple assembly instruction, it is translated into a call to a function
defined in the preamble of the compilation result.

\subsection{$\ERTL$}

As in $\RTL$, the structure of $\ERTL$ programs is based on
CFGs. $\ERTL$ explicits the calling conventions of the $\mips$
assembly language. In the back-end for $\intel$, we defined our own
calling convention since there were none.

\paragraph{Syntax.}
The syntax of the language is given in table \ref{ERTL:syntax}. The main
difference between $\RTL$ and $\ERTL$ is the use of hardware registers.
Parameters are passed in specific hardware registers; if there are too many
parameters, the remaining are stored in the stack. Other conventionally specific
hardware registers are used: a register that holds the result of a function, a
register that holds the base address of the globals, a register that holds the
address of the top of the stack, and some registers that need to be saved when
entering a function and whose values are restored when leaving a
function. Following these conventions, function calls do not list their
parameters anymore; they only mention their number. Two new instructions appear
to allocate and deallocate on the stack some space needed by a function to
execute. Along 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 because we do not
know the final size of the stack area of each function. At last, the return
instruction has a boolean argument that tells whether the result of the function
may later be used or not (this is exploited for optimizations).

\begin{table}
{\footnotesize
\[
\begin{array}{lllllll}
\w{size} & ::= & \s{Byte} \Alt \s{HalfWord} \Alt \s{Word}  & \qquad
\w{fun\_ref} & ::= & \w{fun\_name} \Alt \w{psd\_reg}
\end{array}
\]

\[
\begin{array}{llll}
\w{instruction} & ::= & \Alt \s{skip} \rightarrow \w{node} &
                        \quad \mbox{(no instruction)}\\
                &     & \Alt \s{NewFrame} \rightarrow \w{node} &
                        \quad \mbox{(frame creation)}\\
                &     & \Alt \s{DelFrame} \rightarrow \w{node} &
                        \quad \mbox{(frame deletion)}\\
                &     & \Alt \w{psd\_reg} := \s{stack}[\w{slot}, n]
                        \rightarrow \w{node} &
                        \quad \mbox{(stack load)}\\
                &     & \Alt \s{stack}[\w{slot}, n] := \w{psd\_reg}
                        \rightarrow \w{node} &
                        \quad \mbox{(stack store)}\\
                &     & \Alt \w{hdw\_reg} := \w{psd\_reg}
                        \rightarrow \w{node} &
                        \quad \mbox{(pseudo to hardware)}\\
                &     & \Alt \w{psd\_reg} := \w{hdw\_reg}
                        \rightarrow \w{node} &
                        \quad \mbox{(hardware to pseudo)}\\
                &     & \Alt \w{psd\_reg} := n
                        \rightarrow \w{node} & \quad \mbox{(constant)}\\
                &     & \Alt \w{psd\_reg} := \w{unop}(\w{psd\_reg})
                        \rightarrow \w{node} & \quad \mbox{(unary operation)}\\
                &     & \Alt \w{psd\_reg} :=
                        \w{binop}(\w{psd\_reg},\w{psd\_reg})
                        \rightarrow \w{node} & \quad
                        \mbox{(binary operation)}\\
                &     & \Alt \w{psd\_reg} := \w{fun\_name}
                        \rightarrow \w{node} &
                        \quad \mbox{(address of a function)}\\
                &     & \Alt \w{psd\_reg} :=
                        \w{size}(\w{psd\_reg}[n])
                        \rightarrow \w{node} & \quad \mbox{(memory load)}\\
                &     & \Alt \w{size}(\w{psd\_reg}[n]) :=
                        \w{psd\_reg}
                        \rightarrow \w{node} & \quad \mbox{(memory store)}\\
                &     & \Alt \w{fun\_ref}(n) \rightarrow \w{node} &
                        \quad \mbox{(function call)}\\
                &     & \Alt \w{fun\_ref}(n)
                        & \quad \mbox{(function tail call)}\\
                &     & \Alt \s{test}\ \w{uncon}(\w{psd\_reg}) \rightarrow
                        \w{node}, \w{node} & \quad
                        \mbox{(branch unary condition)}\\
                &     & \Alt \s{test}\ \w{bincon}(\w{psd\_reg},\w{psd\_reg})
                        \rightarrow \w{node}, \w{node} & \quad
                        \mbox{(branch binary condition)}\\
                &     & \Alt \s{return}\ b & \quad \mbox{(return)}
\end{array}
\]

\[
\begin{array}{lllllll}
\w{fun\_def} & ::= & \w{fun\_name}(n) & \qquad
\w{program} & ::= & \s{globals}: n\\
             &     & \s{locals:} \w{psd\_reg}^* & \qquad
            &     & \w{fun\_def}^*\\
             &     & \s{stack:} n\\
             &     & \s{entry:} \w{node}\\
             &     & (\w{node:} \w{instruction})^*
\end{array}
\]}
\caption{Syntax of the $\ERTL$ language}\label{ERTL:syntax}
\end{table}

\paragraph{Translation of $\RTL$ to $\ERTL$.}
The work consists in expliciting the conventions previously mentioned. These
conventions appear when entering, calling and leaving a function, and when
referencing a global variable or the address of a local variable.

\paragraph{Optimizations.}
A \emph{liveness analysis} is performed on $\ERTL$ to replace unused
instructions by a $\s{skip}$. An instruction is tagged as unused when it
performs an assignment on a register that will not be read afterwards. Also, the
result of the liveness analysis is exploited by a \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
program.

\subsection{$\LTL$}

As in $\ERTL$, the structure of $\LTL$ programs is based on CFGs. Pseudo
registers are not used anymore; instead, they are replaced by physical locations
(a hardware register or an address in the stack).

\paragraph{Syntax.}
Except for a few exceptions, the instructions of the language are those of
$\ERTL$ with hardware registers replacing pseudo registers. Calling and
returning conventions were explicited in $\ERTL$; thus, function calls and
returns do not need parameters in $\LTL$. The syntax is defined in table
\ref{LTL:syntax}.

\begin{table}
{\footnotesize
\[
\begin{array}{lllllll}
\w{size} & ::= & \s{Byte} \Alt \s{HalfWord} \Alt \s{Word}  & \qquad
\w{fun\_ref} & ::= & \w{fun\_name} \Alt \w{hdw\_reg}
\end{array}
\]

\[
\begin{array}{llll}
\w{instruction} & ::= & \Alt \s{skip} \rightarrow \w{node} &
                        \quad \mbox{(no instruction)}\\
                &     & \Alt \s{NewFrame} \rightarrow \w{node} &
                        \quad \mbox{(frame creation)}\\
                &     & \Alt \s{DelFrame} \rightarrow \w{node} &
                        \quad \mbox{(frame deletion)}\\
                &     & \Alt \w{hdw\_reg} := n
                        \rightarrow \w{node} & \quad \mbox{(constant)}\\
                &     & \Alt \w{hdw\_reg} := \w{unop}(\w{hdw\_reg})
                        \rightarrow \w{node} & \quad \mbox{(unary operation)}\\
                &     & \Alt \w{hdw\_reg} :=
                        \w{binop}(\w{hdw\_reg},\w{hdw\_reg})
                        \rightarrow \w{node} & \quad
                        \mbox{(binary operation)}\\
                &     & \Alt \w{hdw\_reg} := \w{fun\_name}
                        \rightarrow \w{node} &
                        \quad \mbox{(address of a function)}\\
                &     & \Alt \w{hdw\_reg} := \w{size}(\w{hdw\_reg}[n])
                        \rightarrow \w{node} & \quad \mbox{(memory load)}\\
                &     & \Alt \w{size}(\w{hdw\_reg}[n]) := \w{hdw\_reg}
                        \rightarrow \w{node} & \quad \mbox{(memory store)}\\
                &     & \Alt \w{fun\_ref}() \rightarrow \w{node} &
                        \quad \mbox{(function call)}\\
                &     & \Alt \w{fun\_ref}()
                        & \quad \mbox{(function tail call)}\\
                &     & \Alt \s{test}\ \w{uncon}(\w{hdw\_reg}) \rightarrow
                        \w{node}, \w{node} & \quad
                        \mbox{(branch unary condition)}\\
                &     & \Alt \s{test}\ \w{bincon}(\w{hdw\_reg},\w{hdw\_reg})
                        \rightarrow \w{node}, \w{node} & \quad
                        \mbox{(branch binary condition)}\\
                &     & \Alt \s{return} & \quad \mbox{(return)}
\end{array}
\]

\[
\begin{array}{lllllll}
\w{fun\_def} & ::= & \w{fun\_name}(n) & \qquad
\w{program} & ::= & \s{globals}: n\\
             &     & \s{locals:} n & \qquad
            &     & \w{fun\_def}^*\\
             &     & \s{stack:} n\\
             &     & \s{entry:} \w{node}\\
             &     & (\w{node:} \w{instruction})^*
\end{array}
\]}
\caption{Syntax of the $\LTL$ language}\label{LTL:syntax}
\end{table}

\paragraph{Translation of $\ERTL$ to $\LTL$.} The translation relies on the
results of the liveness analysis and of the register allocation. Unused
instructions are eliminated and each pseudo register is replaced by a physical
location. In $\LTL$, the size of the stack frame of a function is known;
instructions intended to load or store values in the stack are translated
using regular load and store instructions.

\paragraph{Optimizations.} A \emph{graph compression} algorithm removes empty
instructions generated by previous compilation passes and by the liveness
analysis.

\subsection{$\LIN$}

In $\LIN$, the structure of a program is no longer based on CFGs. Every function
is represented as a sequence of instructions.

\paragraph{Syntax.}
The instructions of $\LIN$ are very close to those of $\LTL$. \emph{Program
  labels}, \emph{gotos} and branch instructions handle the changes in the
control flow. The syntax of $\LIN$ programs is shown in table \ref{LIN:syntax}.

\begin{table}
{\footnotesize
\[
\begin{array}{lllllll}
\w{size} & ::= & \s{Byte} \Alt \s{HalfWord} \Alt \s{Word}  & \qquad
\w{fun\_ref} & ::= & \w{fun\_name} \Alt \w{hdw\_reg}
\end{array}
\]

\[
\begin{array}{llll}
\w{instruction} & ::= & \Alt \s{NewFrame} &
                        \quad \mbox{(frame creation)}\\
                &     & \Alt \s{DelFrame} &
                        \quad \mbox{(frame deletion)}\\
                &     & \Alt \w{hdw\_reg} := n & \quad \mbox{(constant)}\\
                &     & \Alt \w{hdw\_reg} := \w{unop}(\w{hdw\_reg})
                        & \quad \mbox{(unary operation)}\\
                &     & \Alt \w{hdw\_reg} :=
                        \w{binop}(\w{hdw\_reg},\w{hdw\_reg})
                        & \quad \mbox{(binary operation)}\\
                &     & \Alt \w{hdw\_reg} := \w{fun\_name}
                        & \quad \mbox{(address of a function)}\\
                &     & \Alt \w{hdw\_reg} := \w{size}(\w{hdw\_reg}[n])
                        & \quad \mbox{(memory load)}\\
                &     & \Alt \w{size}(\w{hdw\_reg}[n]) := \w{hdw\_reg}
                        & \quad \mbox{(memory store)}\\
                &     & \Alt \s{call}\ \w{fun\_ref}
                        & \quad \mbox{(function call)}\\
                &     & \Alt \s{tailcall}\ \w{fun\_ref}
                        & \quad \mbox{(function tail call)}\\
                &     & \Alt \w{uncon}(\w{hdw\_reg}) \rightarrow
                        \w{node} & \quad
                        \mbox{(branch unary condition)}\\
                &     & \Alt \w{bincon}(\w{hdw\_reg},\w{hdw\_reg})
                        \rightarrow \w{node} & \quad
                        \mbox{(branch binary condition)}\\
                &     & \Alt \w{asm\_label:} & \quad \mbox{(assembly label)}\\
                &     & \Alt \s{goto}\ \w{mips\_label} & \quad \mbox{(goto)}\\
                &     & \Alt \s{return} & \quad \mbox{(return)}
\end{array}
\]

\[
\begin{array}{lllllll}
\w{fun\_def} & ::= & \w{fun\_name}(n) & \qquad
\w{program} & ::= & \s{globals}: n\\
             &     & \s{locals:} n & \qquad
            &     & \w{fun\_def}^*\\
             &     & \w{instruction}^*
\end{array}
\]}
\caption{Syntax of the $\LIN$ language}\label{LIN:syntax}
\end{table}

\paragraph{Translation of $\LTL$ to $\LIN$.}
This translation amounts to transform in an efficient way the graph structure of
functions into a linear structure of sequential instructions.

\subsection{Assembly}

$\mips$ is a rather simple assembly language whereas $\intel$'s is
rather complex~\cite{intel94}. We only describe $\mips$. As for other
assembly languages, a program in $\mips$ is a sequence of
instructions. The $\mips$ code produced by the compilation of a
$\Clight$ program starts with a preamble in which some useful and
non-primitive functions are predefined (e.g. conversion from 8 bits
unsigned integers to 32 bits integers). The subset of the $\mips$
assembly language that the compilation produces is defined in
table \ref{mips:syntax}.

\begin{table}
{\footnotesize
\[
\begin{array}{lllllllllll}
\w{load} & ::= & \s{lb} \Alt \s{lhw} \Alt \s{lw} & \qquad
\w{store} & ::= & \s{sb} \Alt \s{shw} \Alt \s{sw} & \qquad
\w{fun\_ref} & ::= & \w{fun\_name} \Alt \w{hdw\_reg}
\end{array}
\]

\[
\begin{array}{llll}
\w{instruction} & ::= & \Alt \s{nop} & \quad \mbox{(empty instruction)}\\
                &     & \Alt \s{li}\ \w{hdw\_reg}, n & \quad \mbox{(constant)}\\
                &     & \Alt \w{unop}\ \w{hdw\_reg}, \w{hdw\_reg}
                        & \quad \mbox{(unary operation)}\\
                &     & \Alt \w{binop}\
                        \w{hdw\_reg},\w{hdw\_reg},\w{hdw\_reg}
                        & \quad \mbox{(binary operation)}\\
                &     & \Alt \s{la}\ \w{hdw\_reg}, \w{fun\_name}
                        & \quad \mbox{(address of a function)}\\
                &     & \Alt \w{load}\ \w{hdw\_reg}, n(\w{hdw\_reg})
                        & \quad \mbox{(memory load)}\\
                &     & \Alt \w{store}\ \w{hdw\_reg}, n(\w{hdw\_reg})
                        & \quad \mbox{(memory store)}\\
                &     & \Alt \s{call}\ \w{fun\_ref}
                        & \quad \mbox{(function call)}\\
                &     & \Alt \w{uncon}\ \w{hdw\_reg}, \w{node} & \quad
                        \mbox{(branch unary condition)}\\
                &     & \Alt \w{bincon}\ \w{hdw\_reg},\w{hdw\_reg},\w{node}
                        & \quad \mbox{(branch binary condition)}\\
                &     & \Alt \w{mips\_label:} & \quad \mbox{($\mips$ label)}\\
                &     & \Alt \s{j}\ \w{mips\_label} & \quad \mbox{(goto)}\\
                &     & \Alt \s{return} & \quad \mbox{(return)}
\end{array}
\]

\[
\begin{array}{lll}
\w{program} & ::= & \s{globals}: n\\
            &     & \s{entry}: \w{mips\_label}^*\\
            &     & \w{instruction}^*
\end{array}
\]}
\caption{Syntax of the $\mips$ language}\label{mips:syntax}
\end{table}

\paragraph{Translation of $\LIN$ to $\mips$.} This final translation is simple
enough. Stack allocation and deallocation are explicited and the function
definitions are sequentialized.


\subsection{Benchmarks}
\label{C-compiler-benchmarks}
\begin{figure}

\begin{center}
\begin{tabular}{r|rrr}
& \texttt{gcc -O0} & \texttt{acc} & \texttt{gcc -O1} \\
\hline
badsort & 55.93 & 34.51 & 12.96 \\
fib & 76.24 & 34.28 & 45.68 \\
mat\_det & 163.42 & 156.20 & 54.76 \\ 
min & 12.21 & 16.25 & 3.95 \\
quicksort & 27.46 & 17.95 & 9.41 \\
search & 463.19 & 623.79 & 155.38 \\
\hline
\end{tabular}
\end{center}

\caption{Benchmarks results (execution time is given in seconds).}
\label{fig:benchmark-results}
\end{figure}

To ensure that our prototype compiler is realistic, we performed some
preliminary benchmarks on a 183MHz MIPS 4KEc processor, running a
linux based distribution. We compared the wall clock execution time of
several simple~\C\ programs compiled with our compiler against the ones
produced by {\sc Gcc} set up with optimization levels 0 and 1. As
shown by Figure~\ref{fig:benchmark-results}, our prototype compiler
produces executable programs that are on average faster than 
{\sc Gcc}'s without optimizations.


\newpage

\section{A direct approach}\label{direct-sec}
Our first attempt at building cost annotations followed
a `direct' approach which is summarised by the following diagram.


\[
\xymatrix{
% Row 1
  L_1 \ar[d]^{An_1} \ar[r]^{\cl{C}_1} 
& L_2 \ar[d]^{An_1}  
& \ldots \hspace{0.3cm}\ar[r]^{\cl{C}_k} 
& L_{k+1} \ar[d]^{An_{k+1}}  \\
% Row 2
  L_1                                  
& L_2   
& & L_{k+1}
}
\]

With respect to the introductive discussion in section \ref{intro-sec},  
$L_1$ is the source language with the related annotation function $\w{An}_1$ while
$L_{k+1}$ is the object language with a related annotation
$\w{An}_{k+1}$. This annotation of the object code is supposed to be truly
straightforward and it is taken as an `axiomatic' definition of
the `real' execution cost of the program. 
The languages $L_i$, for $2\leq i \leq k$, are
intermediate languages which are also equipped with increasingly `realistic' 
annotation functions.
Suppose we denote with $S$ the source program,
with $\cl{C}(S)$ the compiled program, and 
that we write $(P,s)\eval s'$ to mean that
the (source or object) program $P$ in the state $s$
terminates successfully in the state $s'$.
The soundness proof of the compilation function
guarantees that if $(S,s)\eval s'$ then 
$(\cl{C}(S),s)\eval s'$.
In the direct approach, the {\em proof of soundness} of
the cost annotations amounts to lift the proof of functional
equivalence of the source program and the object code to a proof of
`quasi-equivalence' of the respective instrumented codes.
Suppose we write $s[c/\w{cost}]$ for a state that associates $c$
with the cost variable $\w{cost}$. Then what we want to show is 
that whenever $(\w{An}_{1}(S),s[c/\w{cost}])\eval s'[c'/\w{cost}]$ 
we have that $(\w{An}_{k+1}(\cl{C}(S)),s[d/\w{cost}])\eval s'[d'/\w{cost}]$
and $|d'-d|\leq |c'-c|+k$.
This means that the increment in the annotated source program bounds up to 
an additive constant the increment in the annotated object program.
We will also say that the cost annotation is precise if we can also prove that
$|c'-c|\leq |d'-d|$, {\em i.e.}, the `estimated' cost is not too far
away from the `real' one. 
We will see that while in theory one can build sound and precise
annotation functions, in practice definitions and proofs become
unwieldy.





Applying the direct approach  to the toy compiler, 
results in the following diagram.


\[
\xymatrix{
\imp 
\ar[r]^{\cl{C}}
\ar[d]^{An_{\imp}}
& 
\vm
\ar[r]^{\cl{C'}}
\ar[d]^{An_{\vm}}
& 
\mips
\ar[d]^{An_{\mips}}
\\
\imp 
& 
\vm
& \mips\\
}
\]



\subsection{$\mips$ and $\vm$ cost annotations}
The definition of the cost annotation $\w{An}_{\mips}(M)$ for a $\mips$ code $M$ goes as follows assuming that all the $\mips$ instructions have cost $1$.

\begin{enumerate}

\item  We select fresh locations $l_{\w{cost}},l_A,l_B$ not used in $M$.

\item Before each instruction in $M$ we insert the following 
list of  $8$ instructions whose effect is to
increase by $1$ the contents of location $l_\w{cost}$:

{\footnotesize
\[
\begin{array}{l}

(\s{store} \ A,l_{A}) \cdot
(\s{store} \ B,l_{B}) \cdot
(\s{loadi} \ A, 1) \cdot
(\s{load} \ B, l_{\w{cost}}) \cdot \\
(\s{add} \ A, A, B) \cdot
(\s{store} \ A,l_{\w{cost}}) \cdot
(\s{load} \ A, l_{A}) \cdot
(\s{load} \ B, l_{B})~.
\end{array}
\]}


\item We update the offset of the branching instructions according to the map
$k \mapsto (9\cdot k)$.

\end{enumerate}


The definition of the cost annotation 
$\w{An}_{\vm}(C)$ for a well-formed $\vm$ code $C$ such that
$C:h$ goes as follows.

\begin{enumerate}

\item We select a fresh $\w{cost}$ variable not used in $C$.

\item   Before the instruction $i^{\w{th}}$ in $C$,
we insert the following list of 4 instructions whose
effect is to increase the $\w{cost}$ variable by the maximum number 
$\kappa(C[i])$ of instructions associated with $C[i]$ (as specified
in table \ref{cost-approx-instr}):

{\footnotesize\[
(\s{cnst}(\kappa(C[i]))) \cdot
(\s{var}(\w{cost})) \cdot
(\s{add}) \cdot
(\s{setvar}(\w{cost}))~.
\]}

\item We update the offset of the branching instructions according to the map
$k\mapsto (5 \cdot k)$.

\end{enumerate}


\begin{table}
{\footnotesize
\[
\begin{array}{c|cccccc}

C[i]=

&\s{cnst}(n) \mbox{ or } \s{var}(x)

&\s{add}

&\s{setvar}(x)

&\s{branch}(k)

&\s{bge}(k)

&\s{halt} \\ \hline


\kappa(C[i])=

&2 

& 4 

& 2 

& 1 

& 3 

& 1

\end{array}
\]}
\caption{Upper bounds on the cost of $\vm$ instructions}\label{cost-approx-instr}
\end{table}


To summarise, the situation is that the instruction $i$ of the $\vm$
code $C$ corresponds to: the instruction $5\cdot i +4$ of the
annotated $\vm$ code $\w{An}_{\vm}(C)$, the instruction $p(i,C)$ of
the $\mips$ code $\cl{C'}(C)$, and the instruction $9\cdot p(i,C)+8$
of the instrumented $\mips$ code $\w{An}_{\mips}(\cl{C'}(C))$.

The following lemma describes the effect of the injected sequences
of instructions.

\begin{lemma}\label{annot-vm-mips}
The following properties hold:

\Defitem{(1)} If $M$ is a $\mips$ instruction then $C_1 \cdot \w{An}_{\mips}(M) \cdot C_2 \Gives  (|C_1|,m[c/l_{\w{cost}}]) \trarrow (|C_1|+8,m[c+1/l_{\w{cost}},m(A)/l_A,m(B)/l_B])$.

\Defitem{(2)} If $C$ is a $\vm$ instruction then $C_1 \cdot \w{An}_{\vm}(C) \cdot C_2 \Gives (|C_1|,\sigma,s[c/\w{cost}]) \trarrow (|C_1|+4,\sigma,s[c + \kappa(C[i])/\w{cost}])$, where 
$i=|C_1|$.

\end{lemma}


The simulation proposition \ref{simulation-vm-mips} is extended to the
annotated codes as follows where we write $\arrow^k$ for the relation
obtained by composing $k$ times the reduction relation $\arrow$.


\begin{proposition}\label{labelled-simulation-vm-mips}
Let $C : h$ be a well-formed code. If $\w{An}_{\vm}(C) \Gives (5 \cdot
i, \sigma, s) \arrow^5 (5 \cdot j, \sigma', s')$, $m \real \sigma,
s$, and $h(i) = |\sigma|$ then $\w{An}_{\mips}(\cl{C'}(C)) \Gives (9
\cdot p(i,C),m) \trarrow (9\cdot p(j,C),m')$, with $m'[s'(\w{cost}) /
  l_{\w{cost}}] \real \sigma', s'$ and
\[
m'(l_{\w{cost}}) - m(l_{\w{cost}}) \le s'(\w{cost}) - s(\w{cost})~.
\]
\end{proposition}






\subsection{$\imp$ cost annotation}\label{imp-cost-annotation}
The definition of the cost annotation $\w{An}_{\imp}(P)$ for an $\imp$
program $P$ is defined in table \ref{annotation-imp} and it relies on
an auxiliary function $\kappa$ which provides an upper bound on the
cost of executing the various operators of the language.  
For the sake of simplicity, this
annotation introduces two main {\em approximations}:

\begin{itemize}

\item It over-approximates the cost of 
an $\s{if\_then\_else}$ by taking the maximum cost of the
cost of the two branches. 

\item  It always considers the worst case where 
the data in the stack resides in the main memory. 

\end{itemize}

We will discuss in section \ref{limitations-direct-sec} to what extent 
these approximations can be removed.

\begin{table}
{\footnotesize
\[
\begin{array}{ll}

\w{An}_{\imp}(\s{prog} \ S) &= \w{cost}:=\w{cost}+\kappa(S); \w{An}_{\imp}(S) \\
\w{An}_{\imp}(\s{skip})     &= \s{skip} \\
\w{An}_{\imp}(x:=e)         &= x:=e \\
\w{An}_{\imp}(S;S')         &= \w{An}_{\imp}(S);\w{An}_{\imp}(S') \\
\w{An}_{\imp}(\s{if} \ b \ \s{then} \ S \ \s{else} \ S') 
&=  (\s{if} \ b \ \s{then} \  \w{An}_{\imp}(S) \\
&\qquad\qquad  \s{else} \ \w{An}_{\imp}(S')) \\ 

\w{An}_{\imp}(\s{while} \ b \ \s{do} \ S) 
&= (\s{while} \ b \ 
\s{do} \ \w{cost}:=\w{cost}+\kappa(b)+\kappa(S)+1; \w{An}_{\imp}(S)  ) 

\end{array}
\]
\[
\begin{array}{ll}

\kappa(\s{skip})  =0 
&\kappa(x:=e)       =\kappa(e) + \kappa(\s{setvar}) \\

\kappa(S;S')       = \kappa(S)+\kappa(S') 

&\kappa(\s{if} \ b \ \s{then} \ S \ \s{else} \ S') 
                   =\kappa(b)+\w{max}(\kappa(S) + \kappa(\s{branch}),\kappa(S')) \\

\kappa(\s{while} \ b \ \s{do} \ S)
                   =\kappa(b)  \\

\kappa(e<e')      =\kappa(e)+\kappa(e')+ \kappa(\s{bge})

&\kappa(e+e')    = \kappa(e)+\kappa(e')+ \kappa(\s{add})  \\

\kappa(n)       = \kappa(\s{cnst})

&\kappa(x)       = \kappa(\s{var})

\end{array}
\]}
\caption{Annotation for $\imp$ programs}\label{annotation-imp}
\end{table}

Next we formulate the soundness of the $\imp$ annotation with respect 
to the $\vm$ annotation along the pattern of proposition 
\ref{soundness-big-step-prop}.



\begin{proposition}\label{annot-imp-vm}
The following properties hold.

\Defitem{(1)} If $(e,s)\eval v$ then 
\[
C \cdot \w{An}_{\vm}(\cl{C}(e)) \cdot C'
\Gives (i,\sigma,s[c/\w{cost}]) \trarrow 
(j,v \cdot \sigma,s[c+\kappa(e)/\w{cost}])
\]
where $i=|C|$, $j=|C\cdot  \w{An}_{\vm}(\cl{C}(e))|$.


\Defitem{(2)} If $(b,s)\eval \s{true}$ then
\[
C \cdot \w{An}_{\vm}(\cl{C}(b,k)) \cdot C'
\Gives (i,\sigma,s[c/\w{cost}]) \trarrow 
(5\cdot k +j, \sigma,s[c+\kappa(b)/\w{cost}])
\]
where $i=|C|$, $j=|C\cdot  \w{An}_{\vm}(\cl{C}(b,k))|$.

\Defitem{(3)} If 
$(b,s)\eval \s{false}$ then 
\[
C \cdot \w{An}_{\vm}(\cl{C}(b,k)) \cdot C'
\Gives (i,\sigma,s[c/\w{cost}]) \trarrow 
(j,\sigma,s[c+\kappa(b)/\w{cost}])
\]
where $i=|C|$, $j=|C\cdot  \w{An}_{\vm}(\cl{C}(b,k))|$.

\Defitem{(4)}
If $(\w{An}_{\imp}(S),s[c/\w{cost}])\eval s'[c'/\w{cost}]$ then 
\[
C \cdot \w{An}_{\vm}(\cl{C}(S)) \cdot C' 
\Gives (i,\sigma,s[d/\w{cost}]) \trarrow (j,\sigma,s'[d'/\w{cost}]) 
\]
where $i=|C|$, $j=|C\cdot  \w{An}_{\vm}(\cl{C}(S))|$,
and $(d'-d) \leq (c'-c)+\kappa(S)$.
\end{proposition}


\subsection{Composition}
The soundness of the cost annotations can be composed 
so as to obtain the soundness of the cost annotations of the source
program relatively to the one of the object code.

\begin{proposition}\label{annot-composition}
If $(\w{An}_{\imp}(P),s[0/\w{cost}])\eval s'[c'/\w{cost}]$ 
and $m\real \epsilon,s[0/l_{\w{cost}}]$ then 
\[
(\w{An}_{\mips}(\cl{C'}(\cl{C}(P))),m)
 \eval m'
\]
where $m'(l_{\w{cost}})\leq c'$ and $m'[c'/l_{\w{cost}}] \real \epsilon,s'[c'/\w{cost}]$.
\end{proposition}



\subsection{$\coq$ development}\label{coq-development-sec}
We have formalised and mechanically checked in {\sc Coq} the
application of the direct approach to the toy compiler (but for
propositions \ref{labelled-simulation-vm-mips} and
\ref{annot-composition} for which
we produced `paper proofs').  
By current standards, this is a small size
development including 1000 lines of specifications and 4000 lines of
proofs.  Still there are a couple of points that deserve to be
mentioned.  First, we did not find a way of re-using the soundness
proof of the compiler in a modular way.  As a matter of fact, the
soundness proof of the annotations is intertwined with the soundness
proof of the compiler.  Second, the manipulation of the cost variables
in the annotated programs entails a significant increase in the size
of the proofs.  In particular, the soundness proof for the compilation
function $\cl{C}$ from $\imp$ to $\vm$ available in \cite{Leroy09-ln}
is roughly $7$ times smaller than the soundness proof of the
annotation function of the $\imp$ code relatively to the one of the
$\vm$ code.


\subsection{Limitations of the direct approach}\label{limitations-direct-sec}
As mentioned in section \ref{imp-cost-annotation}, the annotation
function for the source language introduces some over-approximation
thus {\em failing to be precise}.  On one hand, it is easy to modify
the definitions in table \ref{annotation-imp} so that they compute the
cost of each branch of an {\tt if\_then\_else} separately rather than
taking the maximum cost of the two branches.  On the other hand, it is
rather difficult to refine the annotation function so that it accounts
for the memory hierarchy in the $\mips$ machine; one needs to pass to
the function $\kappa$ an `hidden parameter' which corresponds to the
stack height.  This process of pushing hidden parameters into the
definition of the annotation is error prone and it seems unlikely to
work in practice for a realistic compiler. We programmed sound (but
not precise) cost annotations for the $\C$ compiler introduced in
section \ref{Ccompiler-intro} and found that the approach is difficult
to test because an over-approximation of the cost at some point may
easily compensate an under-approximation somewhere else. By contrast,
in the labelling approach introduced in section \ref{label-intro}, we
manipulate costs at an abstract level as labels and produce numerical
values only at the very end of the construction.



\newpage


\section{Related approaches}\label{related-sec}
Our fine-grained approach to labelling is based on the hypothesis that we can
obtain precise information on the execution time of each instruction
of the generated binary code.  This hypothesis is indeed realised in
the processors of the $\intel$ family we are considering. On the other
hand, the execution time of instructions running on more complex
architectures including, {\em e.g.}, cache memory or pipelines are
much less predictable.  This lack of precision may somehow be
compensated by analysing the worst-case execution time of sequences of
instructions.  As mentioned in the introduction, tools such as those
developped by $\absint$ require explicit annotations of the binaries
to determine the number of times a loop is iterated and apply abstract
interpretation methods in order to provide an estimation of the
execution time of the code.  From the point of view of a {\em formal}
certification this approach rises at least two questions.

First, one needs a formal certification of the fact that the abstract
interpretation method does indeed produce correct results for a given
processor.  This in turn supposes a formal modelling of the processor
and a proof that the abstract interpretation method does indeed
abstract the processor's behaviour.  Taking a pragmatic (and
informal) approach, one could argue that the results of the tool could
be trusted, in the same way we trust the execution times given by the
manufacturers.


Second, one needs a formal certification of the fact that the
annotations on the loops are indeed correct.  For instance, suppose we
can identify in the source code {\em for-loops} that iterate a {\em
constant} number of times some sequence of statements.
%To make the discussion concrete,
%let us assume our toy $\imp$ language is enriched with an instruction
%$\s{loop} \ n \ S$ that executes $n$ times the command $S$. 
In our approach, we must insert a label in the body of 
the loop so as to avoid that the control flow graph associated
with the binary code contains a loop that does not cross any label.
Having determined the cost of one iteration of the body of the loop,
we can then reason at the level of the source code to obtain the cost
of several iterations.

In an alternative approach, we could try to propagate to the control flow graph
the information that the body of the loop is iterated a constant number of
times and then invoke tools such as those mentioned above to get
an estimation of the cost of running the whole iteration.
As mentioned above, the rationale for this approach is to get a more precise
estimation of the cost of executing the iteration on a complex architecture.
While the approach seems easily implementable, it is not clear how
one should proceed in order to formally certify its correctness.
Specifically, one needs to propagate enough information at the level
of the binary code to be able to verify automatically that the
predicted number of iterations of the body of the loop is indeed correct.
In turn, this means to be able to track down the initial value of a certain 
number of memory locations (registers and/or stack locations) 
and to guarantee that their contents is modified at each iteration leading
eventually to the exit of the loop. While this seems within the 
reach of a {\em proof-carrying code} approach, the challenge is to devise
a more lightweight approach which targets the specific properties of interest.


\newpage

\section{Assessment of the deliverable within the $\cerco$ project, with hindsight}\label{asmt-sec}


The port of the compiler to the $\intel$ processor has required
a major and rather unrewarding implementation effort which is 
described in deliverable D2.2. 

One problem that has emerged is that the compilation of general
purpose $\C$ programs with recursion and/or 16-32 integers bits
produces binaries whose size approaches quickly the limits of the
architecture (program memory is limited to 64Kbytes).

This is a problem for instance for the case study which is planned in
deliverable D5.3 (Case study: analysis of synchronous code) whose
purpose is to produce automatically cost annotations for the $\C$
programs generated by a compiler of a synchronous language such as
{\sc Lustre}.  The generated $\C$ programs are rather large
(though their control flow is simple) and assume 32 bits integers.

At the time being, two options are being considered as far as 
deliverable D5.3 is concerned.

\begin{enumerate}

\item Improve the efficiency of the compilation of 16/32 bits
integers for the $\intel$ compiler.

\item Conduct the case study relying on a compiler to a 32 bits
processor.

\end{enumerate}

If the second option is chosen, one possibility is to target the {\sc
Mips} processor for which a prototype compiler has already been
developed. 
More generally, one advantage of the second option is that it allows
to conduct realistic case studies on a larger class of programming constructs.
For instance, we are interested in studying the extension of the 
labelling approach to a compilation chain from
a functional language of the {\sc ML} family to $\C$.