source: Deliverables/D2.1/text.tex @ 2585

\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 optimising 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 functionally correct 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}.

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 two methodologies addressing these three
questions and to consider their concrete application to 
a simple toy compiler and to a moderately optimising $\C$ compiler.


\subsection{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 $S$ amounts to
build an {\em annotated program} $\w{An}(S)$ which behaves as $S$
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}(S)$ to be functionally equivalent to $S$.  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. 


\subsection{Soundness and precision of cost annotations}
Suppose we have a functionally correct compiler $\cl{C}$ that
associates with a program $S$ in the source language a program
$\cl{C}(S)$ 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}(S)$ 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} 
if the {\em difference} between the predicted and real execution costs 
is bounded by a constant which depends on the program. 


\subsection{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 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.


\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.


\[
\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.



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

\newcolumntype{M}[1]{>{\raggedright}m{#1}}

\-

\begin{tabular}{M{10cm}||M{4cm}}
$$
\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}_{1} &= &\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 \w{cost} variable. Then an {\em annotation} $\w{An}_{1}$ of the 
source program can be derived simply as the composition of the labelling
and the instrumentation functions: $\w{An}_{1} = \cl{I}\comp \cl{L}$.

As for the direct approach, suppose $s$ is some adequate representation
of the state of a program. Let $S$ be a source program and suppose
that its annotation satisfies the following property:
\begin{equation}\label{STEP1}
(\w{An}_{1}(S),s[c/\w{cost}])  \eval s'[c+\delta/\w{cost}]
\end{equation}
where $\delta$ is some non-negative number.
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}(L(S)),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}(L(S)))$ is actually  equal to 
the compiled code $\cl{C}(S)$ we are interested in.
Given this, the following question arises: 

\begin{quote}
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? 
\end{quote}

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 pieces 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. 















\subsection{A toy compiler}\label{toy-intro}
As a first case study for the two approaches to cost
annotations we have sketched, we introduce a
{\em toy compiler} which is summarised by the
following diagram.

\[
\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
(cf. section \ref{comp-intro}).


\subsection{A C compiler}\label{Ccompiler-intro}
As a second, more complex, case study we consider a 
$\C$ compiler we have built in $\ocaml$ whose
structure is summarised by the following diagram:

{\footnotesize
\[
\begin{array}{cccccccccc}
&&\C &\arrow &\Clight &\arrow &\Cminor &\arrow &\RTLAbs &\qquad \mbox{(front end)}\\
                                              &&&&&&&&\downarrow \\
 \mips &\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.
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$ assembly language (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}.  The main optimisations it performs are common
subexpression elimination, liveness analysis and register allocation,
and graph compression.



\subsection{Organisation}
The rest of the paper is organised as follows.
Section \ref{toy-compiler-sec} describes the 3 languages and the 
2 compilation steps of the toy compiler. 
Section \ref{toy-direct-sec} describes the application of the
direct approach to the toy compiler and points
out its limitations. 
Section \ref{label-toy-sec} describes the application of
the labelling approach to the toy compiler.
Section \ref{C-compiler-sec} provides some details on the
structure of the $\C$ compiler we have implemented.
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.
Section \ref{paper-proofs} sketches the proofs that have not
been mechanically checked in $\coq$.



\section{A toy compiler}\label{toy-compiler-sec}
We formalise the toy compiler
introduced in section \ref{toy-intro}.

\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{Big-step semantics}
The big-step operational semantics of $\imp$ programs is 
defined by the following judgements:
\[
(e,s)\eval v  \quad (b,s) \eval v \qquad (S,s)\eval s'\quad (P,s)\eval s'
\]
and it is described in table \ref{semantics-imp}.
We assume that  the addition $v +_{\Z} v'$ is only defined if 
$v$ and $v'$ are integers and the comparison $v <_{\Z} v'$ produces
a value \s{true} or \s{false} only if $v$ and $v'$ are integers.
\begin{table}
{\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')} \\ \\ 

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

\qquad 

\infer{(e,s) \eval v}
{(x:=e,s) \eval s[v/x]} 

\qquad

\infer{(S_1,s)\eval s'\quad (S_2,s')\eval s''}
{(S_1;S_2,s)\eval s''} \\\\


\infer{(b,s)\eval \s{true} \quad (S,s)\eval s'}
{ (\s{if} \ b \ \s{then} \ S \ \s{else} \ S',s) \eval  s'}
\qquad
\infer{(b,s)\eval \s{false} \quad (S',s)\eval s'}
{ (\s{if} \ b \ \s{then} \ S \ \s{else} \ S',s) \eval  s'}
\\ \\ 

\infer{(b,s) \eval \s{false}}
{(\s{while} \ b \ \s{do} \  S ,s)\eval s}
\qquad

\infer{(b,s) \eval \s{true} \quad (S;\s{while} \ b \ \s{do} \  S,s) \eval s'}
{(\s{while} \ b \ \s{do} \  S ,s)\eval s'} \\ \\ 

\infer{(S,s)\eval s'}
{(\s{prog} \ S,s)\eval s'}

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


\subsection{Small-step semantics}
We also introduce an alternative small-step semantics of the
$\imp$ language.
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:
\[
\begin{array}{ll}
(S,s) \eval s'                   &\mbox{if }(S,\s{halt},s) \arrow \cdots \arrow (\s{skip},\s{halt},s') ~.
\end{array}
\]


\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. 
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 formalised 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.
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}
\Defitemf{(1)}
If $C:h$, $C\Gives (i,\sigma,s) \trarrow (j,\sigma',s')$, and 
$h(i)=|\sigma|$ then $h(j)=|\sigma'|$.

\Defitem{(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 for the big-step semantics}
We follow \cite{Leroy09-ln} for 
the proof of correctness of the compilation function with
respect to the big-step semantics (see also \cite{MP67} for a
much older reference).

\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}



\subsection{Soundness of compilation for the small-step semantics}
We prove soundness with respect to the small step semantics too.
To this end, 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}
\quad
&\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 intuition is that relative to the code $C$, 
the instruction $i$ can be regarded as having continuation $K$. 
Formally, the relation $R$ 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
&\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}
\]}


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 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$.
\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 formalised  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),
(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] = \left\{ \begin{array}{ll}
                    m(R_i) &\mbox{if }i<b \\
                    m(l_i) &\mbox{if }i\geq b
                    \end{array} \right.
\]
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)$.
\begin{table}
{\footnotesize
\[
\begin{array}{l|l}

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

\s{cnst}(n)  
& \left\{ \begin{array}{ll}
                   (\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}{ll}
                   (\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}{ll}
                     (\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}{ll}
                         (\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}{ll}
                     (\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) \mbox{ and} \\

&\quad 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}
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$ as in (\ref{p-function}), and finally the function $\cl{C'}$ as in table \ref{compil-vm-mips}.}
\begin{equation}\label{p-function}
p(i,C) = \Sigma_{0\leq j <i} d(i,C),
\end{equation}
where the function $d(i,C)$ is defined as follows:
\begin{equation}\label{d-function}
d(i,C) = |\cl{C'}(i,C)|~.
\end{equation}
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}



\section{Direct approach for the toy compiler}\label{toy-direct-sec}
We apply the direct approach discussed in section \ref{direct-intro}
to the toy compiler which 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 provide a `paper proof' in the appendix).  
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.




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

\-

\newcolumntype{M}[1]{>{\raggedright}m{#1}}
\begin{tabular}{M{9cm}||M{4cm}}
$$
\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}




\subsection{Labelled $\imp$}
We extend the syntax so that statements
and boolean conditions in \s{while} loops
can be labelled. 

{\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 $\ell:(\s{while} \ \ell' : (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.
The evaluation predicate $\eval$ on labelled boolean conditions is
extended as follows:

{\footnotesize
\begin{equation}
\infer{(b,s) \eval v}
{(\ell:b,s) \eval (v,\ell)}
\end{equation}}

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 follows.

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





(\s{while} \ \w{lb} \ \s{do} \ S ,K,s) &\act{\ell}
&\left\{
\begin{array}{ll}
(S,(\s{while} \ \w{lb} \ \s{do} \ S);K,s) &\mbox{if }(\w{lb},s)\eval (\s{true},\ell) \\
(\s{skip},K,s) &\mbox{if }(\w{lb},s)\eval (\s{false},\ell)
\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,
removes labels from labelled boolean conditions 
and is the identity on unlabelled ones, and traverses commands
removing all labels.
We derive a {\em labelled} big-step semantics as follows:

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

(S,s)\eval (s',\lambda)          &\mbox{if } (S,\s{halt},s) \act{\lambda_1} \cdots \act{\lambda_n}  
                                             (\s{skip},\s{halt},s')  \mbox{ and }\lambda =\lambda_1 \cdots \lambda_n~.

\end{array}
\]}







\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}
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}$.
The following proposition relates $\vm_\ell$ code and its compilation
and it is similar to proposition \ref{labelled-sim-imp-vm}.


\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.

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

\cl{I}(\ell:S) &= \w{inc}(\ell) ; \cl{I}(S) \\


\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 s[c/\w{cost}]$ then 
$(\cl{C'}(\cl{C}(\cl{L}(P))),m) \eval (m',\lambda)$, $m'\real 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 where the operator \w{new} is meant to return fresh
labels.

\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) &= \w{let} \ \ell=\w{new} \ \w{in}\ \quad \s{prog}\  \ell: \cl{L}_p(S) \\

\cl{L}_p(\s{skip})     &=\w{let} \ \ell=\w{new} \ \w{in} \ \quad \ell:(\s{skip}) \\

\cl{L}_p(x:=e)         &= \w{let} \ \ell=\w{new} \ \w{in} \ \quad \ell:(x:=e) \\

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


\cl{L}_p(\s{if} \ b \ \s{then} \ S_1 \ \s{else} \ S_2) &= \w{let} \ \ell=\w{new} \ \w{in} \quad\quad
\s{if} \ \ell:b \ \s{then} \ \cl{L}_p(S_1) \ \s{else} \ \cl{L}_p(S_2) \\ 


\cl{L}_p(\s{while} \ b \ \s{do} \ S) &= \w{let} \ \ell=\w{new} \ \w{in} \quad\quad 
\s{while} \ \ell:b \ \s{do} \ \cl{L}_p(S) 

\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
$(\s{while} \ \ell:(0<x) \ \s{do} \ x:=x+1)$.  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:
\[
\begin{array}{ll}

\w{An}_{\imp}(P) &= \cl{I}(L(P))~.

\end{array}
\]
\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 s[c/\w{cost}]$ entails that 
$(\cl{C'}(\cl{C}(P)),m) \eval m'$, $m'\real s'[c/\w{cost}]$ 
and the cost of the execution is bound (is exactly) $\delta$.
\end{proposition}


To summarise, 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, the 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 criteria to evaluate 
labellings is that they do not introduce too many unnecessary labels. 
We call this property {\em economy}.
There are two reasons for this requirement. On one hand we would like
to minimise the number of labels so that the source program 
is not cluttered by too many cost annotations and 
on the other hand we would like to maximise the length of the simple
paths because in a non-trivial processor the longer the sequence of
instructions we consider the more accurate is the estimation of
their execution cost (on a long sequence certain costs are 
amortized).
In practice, it seems that one can produce first a sound and 
possibly precise labelling and
then apply heuristics to eliminate unnecessary labels.



\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. 

\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.



\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$ assembly language.

\paragraph{Syntax.}
$\RTL$ is very close to $\RTLAbs$. It is based on CFGs and explicits the $\mips$
instructions corresponding to the $\RTLAbs$ instructions. Type information
disappears: everything is represented using 32 bits integers. 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
$\mips$ 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 $\mips$ instruction. There are a few
exceptions: some $\RTLAbs$ instructions are expanded in two or more $\mips$
instructions. When the translation of a $\RTLAbs$ instruction requires more than
a few simple $\mips$ 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.

\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{mips\_label:} & \quad \mbox{($\mips$ 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{$\mips$}

$\mips$ is a rather simple assembly language. 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.



%\newpage

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

This section informally describes the labelled extensions of the languages in 
the compilation chain, 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 $\mips$ 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
summarized in table \ref{annot-clight-summary} and is detailed in the following sections.

\begin{table}
{\footnotesize

1. Label the input $\Clight$ program.\\

2. Compile the labelled $\Clight$ program in the labelled world. This
  produces a labelled $\mips$ code. \\

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

4. 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.
}
\caption{Building the annotation of a $\Clight$ program in the labelling approach}\label{annot-clight-summary}
\end{table}




\subsection{Labelled $\Clight$ and labelled $\Cminor$} 

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 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 $\Cminor$ labelled statements and
expressions.

\subsection{Labels in $\RTLAbs$ and the back-end languages}
The labelled version of $\RTLAbs$ and the languages in the back-end language 
simply consists 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$ and $\mips$, it is $\s{emit}\ \w{label}$. The translation
of these label instructions is immediate.
In $\mips$, we also 
rely on a reserved label $\s{begin\_function}$  to pinpoint the
beginning of a function code (cf. section \ref{fun-call-sec}).



\subsection{Labelling of the source language}

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
$\mips$.

\subsubsection{Sequential instructions}

A sequence of $\Clight$ instructions that compile to sequential $\mips$ code,
such as a sequence of assignments, can be handled by a single 
label which covers the unique execution 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}

\subsubsection{Ternary expressions}

Most $\Clight$ expressions compile to sequential $\mips$ code. There is one
exception: {\em ternary expressions} that introduce a branching in the control
flow. 
Because of the precision condition, we must associate a label with each branch.


\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.}
The two $\Clight$ boolean operations \texttt{\&\&} and \texttt{||}
have a lazy semantics: depending on the evaluation of the first
argument, the second one might be evaluated or not.  There is an
obvious translation to ternary expressions.  For instance, the
expression \texttt{x \&\& y} is translated into the expression
\texttt{x?(y?1:0):0}.  Our compiler performs this translation
\emph{before} computing the labelling.



\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}

\subsubsection{Loops}

Loops in $\Clight$ are guarded by a condition. Following the arguments of 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 enough to guarantee that the loop in the compiled code goes through a label.


\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}

\subsubsection{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}

\subsubsection{Function calls}\label{fun-call-sec}

Function calls in $\mips$ are performed by indirect jumps, the address of the
callee being in a register. In the general case, this address cannot be inferred
statically. Even though the destination point of a function call is unknown,
when the considered $\mips$ 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 principles: 
(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.


\bigskip

Principle (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 $\mips$ 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.

\bigskip

Principle (2) is of course an over-approximation of the program
behaviour 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. 

\subsection{Verifications on the object code}

The labelling previously described has been designed so that the
compiled $\mips$ 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.

\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 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}



\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 initialised 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 $\mips$. 
To this end, each labelled language comes with an interpreter
that produces the trace of the labels encountered during the computation.
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 optimisations that may re-order computations, a weaker
condition could be considered which consists in abstracting the
traces as {\em multi-sets} of labels before comparing them.



\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 direct} and
{\em labelling} approaches and discussed their formal application to a
toy compiler. Based on this experience, we have argued that the second
approach has better scalability properties.  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 plan to test the current compiler on 
the kind of $\C$ code produced for embedded applications, 
a typical example being the $\C$ code produced by 
the compilation of synchronous languages such as $\lustre$ or $\esterel$.
Starting from the annotated $\C$ code, we expect to
produce automatically meaningful information on, say,
the reaction time of a given synchronous program.
%
Second, we plan to port the current compiler to commercial assembly
languages. In particular, it would be interesting to target
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.
%
Third,  we plan to formalise 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-compiler-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{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 hardware/software interface}, 
book by Hennessy and Patterson, 2005.


\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}, Germany, 2009. 


\bibitem{MP67}
J.~McCarthy and J.~Painter.
\newblock Correctness of a compiler for arithmetic expressions.
\newblock In {\em Mathematical aspects of computer science 1}, volume 19
of Symposia in Applied Mathematics, 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{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.

\end{thebibliography}}

\newpage
\appendix

%\section{Choice of target architecture and intermediate languages}

\section{Assessment of the deliverable within the $\cerco$ project}
%RA This section is supposed to be a kind of `executive summary' for
%the project reviewer. How about systematically adding a final appendix
%to the scientific deliverables with a title such as the one proposed above?

Following the extensive experiments described in the previous sections,
we now feel confident about the possibility of scaling our approach to
a realistic, mildly optimizing, complexity preserving\footnote{In the sense
of the project proposal.}  compiler 
% RA:
% Deliverable 2.1 makes no explicit reference to the notion of
% `complexity preservation' though this can be simply derived.
% If a program is soundly labelled and its execution generates a 
% sequence of labels lambda then the execution cost of the compiled code
% is proportional to the lenght of the sequence lambda.
for a target architecture of the kind described in the proposal. While we believe
that our approach should scale to a retargetable compiler, in the timeframe
of the European Project and according to the project work-plan we only commit
to the investigation of a compiler having a single target processor.

In particular, we will target the 8051 (also known as 8052 or MCS51) family
of processors. The 8051 is an 8 bit CISC microprocessor introduced in the 1980
by Intel, very popular and still manufactured by a host of companies,
many European. It is widely used in embedded systems and, thanks to its
predictable behaviour and execution cost, it will allow us to compute fully
accurate measurement of the actual computational complexity of $O(1)$
assembly program slices\footnote{In the sense of the project proposal.}, 
to be manifested at the C level.
% RA: 
% The terminology of `program slice' is used in the proposal but not in the
% deliverable. Note that some confusion is possible with the notion of 
% `program slicing' which is a technique we plan to use in Frama-C 

With respect to the test-cases previously described, in particular the
C compiler for MIPS, the main difficulty introduced by the 8051 is the
non uniform concrete memory model: the processor has different types of
memory (on-chip RAM, external RAM, on-chip and/or external ROM) that can
be accessed using different access modes and pointer types. 
Moreover, memory mapped I/O is heavily used in the design of the chip,
to the point that all registers (apart from the inaccessible program
counter) are seen as memory locations and have their own memory address.
To complete the picture, the different memories are
split into regions that may overlap, and the same accessing mode can
point to different regions (or even to memory mapped registers) according
to the value of the pointer. Finally, the amount of memory available is
quite limited, with a stack which is at most 80 bytes wide and different
speeds and opcode sizes to access different memory areas. For this
reasons, compilers that target 8051 processors usually abound in directives
to drive the tool in assigning memory locations to values.

Hence, because of the peculiar choice of target processor, in the next six
months of the $\cerco$ project and partly as an extension of the original work-plan we will:
% RA: Added partly

\begin{itemize} 

 \item Extend the memory model used so far (and taken from CompCert) to
       accurately describe the different memory types and regions of the 8051,
       as well as to obey to the \texttt{volatile} directive used to map
       memory mapped regions to program variables. This work will be done
       as part of Tasks~T2.3 and T4.1 and the outcome will be described in
       Deliverables~D2.2 and D4.1 where we will also provide a formalization in
       Matita of the executable semantics of the extended memory model.
       In case we decide to adopt the same memory model for all compilation
       phases, as it is done in CompCert, the memory model extension will
       also span over Task~T3.1, requiring close cooperation between
       the front-end formalization (lead by Edinburgh) and the back-end
       formalization (lead by Bologna).

 \item Devise language extensions (possibly inspired by the variable modifiers
       of the SDCC compiler) to let the user suggest or force the compiler to
       put data into particular memory regions. Similarly, we could refine the
       pointer types of ANSI C into classes of pointer types pointing to
       particular regions, in order to reflect the difference in sizes of
       pointers to different regions (8 bits to address internal RAM and
       memory mapped registers; 8 bits to address bits in the bit memory
       or in registers using an ad-hoc addressing mode;
       16 bits for code memory and external memory; 24 bits for generic
       pointers). All of these language extensions, if any, must be reflected
       all over the compilation chain, with modifications to the intermediate
       languages and/or memory model. This work will be done as part of
       Tasks~T2.3, T3.1 and T4.1 and the outcome will be described in
       Deliverables~D2.2, D3.1, D3.3, D4.1, D4.3 where we will provide
       executable semantics in Matita of the source, target and intermediate
       languages.

       In order to remain compatible with the project schedule, we will first
       focus on compiling standard Clight without floating points to the 8051,
       adding the language extensions in a second moment, within Task~T2.3.

%RA: If we want to follow the CompCert approach (one memory model for the
% whole verification chain) then these two points should be done in cooperation
% by Edinburgh (front-end formalisation) and  Bologna (back-end formalisation).


 \item Modify and extend the experimental compiler from Clight
(without floating point) to MIPS in order to target the 8051
architecture (Task~T2.3, Deliverable~D2.2).
%RA: In the 2 SVN (the one we used to prepare the proposal and the
%one we are using now) I cannot find the latest version of the proposal 
%with the correct numbering of the deliverables. Would it be possible
%to add it to the Contracts directory of the SVN?

%RA: We (Paris) are supposed to deliver the prototype annotating compiler end of January 
% which means that the bulk of the work must be done before Christmas (also remember
% that Nicolas will leave us end of February).
% However, we started talking about the specification of the memory model 
% and the extension of the source Clight language only a few days ago.
% This means that unless we get a solid specification in a couple of weeks, 
% the deliverable 2.2 will NOT necessarily cover all the `language extensions' which
% are mentioned above but will focus on compiling Clight with floating point to 8051.


\end{itemize}

But for the modifications required by the selection of the target processor (8051), 
we plan to rely as much as possible on the architecture and the 
the intermediate languages described in this deliverable D2.1.


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


\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.

\subsection{Proof of proposition \ref{soundness-small-step}} 

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$. 
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 
$(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}


\subsection{Proof of proposition \ref{labelled-simulation-vm-mips}}
We recall that the compiled code $\cl{C'}(C)$ does not read or write
the locations $l_{\w{cost}}$, $l_A$, and $l_B$.
Then we note the following properties.

{\footnotesize
\Defitem{(a)} If $\w{An}_{\vm}(C) \Gives (5 \cdot i, \sigma, s) \arrow^5 (5 \cdot j, \sigma', s')$
 then $C \Gives (i, \sigma, s) \arrow (j, \sigma', s'[s(\w{cost}) / \w{cost}])$.

\Defitem{(b)} If $M \Gives (i, m) \arrow (j, m')$ 
then $\w{An}_{\mips}(M) \Gives (9 \cdot i, m) \trarrow (9 \cdot j, m'[m(l_{\w{cost}}) + 1/ l_{\w{cost}}, m(A) / l_A, m(B) / l_B])$.
}

Using $(a)$ and the hypothesis, we derive:

{\footnotesize
\[
C \Gives (i, \sigma, s) \arrow (j, \sigma', s'[s(\w{cost}) / \w{cost}])
\]}
Then, by proposition~\ref{simulation-vm-mips} and the hypothesis on $m$ we derive:

{\footnotesize
\begin{equation}\label{step1}
\cl{C'}(C) \Gives (p(i,C),m) \trarrow (p(j,C),m') \mbox{ and } m' \real \sigma', s'[s(\w{cost}) / \w{cost}]
\end{equation}}
We perform a case analysis on the instruction $C[i]$ and $h(i)$ to derive: 


{\footnotesize
\[
\w{An}_{\mips}(\cl{C'}(C)) \Gives (9 \cdot p(i,C), m) \trarrow (9 \cdot p(j,C), m'[m(l_{\w{cost}}) + d(i,C) / l_{\w{cost}}, x / l_A, y / l_B])
\]}
where $x$ and $y$ are respectively the value of $l_A$ and $l_B$ in the
last intermediate configuration. 


\paragraph{The memory realisation.}
The final memory state is: $m'[m(l_{\w{cost}}) + d(i,C) / l_{\w{cost}}, x / l_A, y / l_B]$.
Then we have to verify:

{\footnotesize\[
(m'[m(l_{\w{cost}}) + d(i,C) / l_{\w{cost}}, x / l_A, y / l_B]) [s'(\w{cost}) / l_{\w{cost}}] \real \sigma', s'~.
\]}
This is  equivalent to:

{\footnotesize \[
m'[s'(\w{cost}) / l_{\w{cost}}, x / l_A, y / l_B] \real \sigma', s'~.
\]}
Since the realisation predicate does not depend on the locations $l_A$ and $l_B$,
we can conclude using the second part of (\ref{step1}).

\paragraph{The inequation.}
To conclude, we verify the inequation:

{\footnotesize
\[
m'[m(l_{\w{cost}}) + d(i,C) / l_{\w{cost}}, x / l_A, y / l_B](l_{\w{cost}}) - m(l_{\w{cost}}) \le s'(\w{cost}) - s(\w{cost})~.
\]}
\noindent By rewriting, we get: $d(i,C) \le s'(\w{cost}) - s(\w{cost})$.
This follows by case analysis of $C[i]$ and $h(i)$ since, by definition, $\w{An}_{\vm}$ uses the worst possible value of $d(i,C)$.
\qed


\subsection{Proof of proposition \ref{annot-composition}}
We have $P = \s{prog} \ S$ and by definition, $\w{An}_{\imp}(P) = \w{cost}:=\w{cost}+\kappa(S); \w{An}_{\imp}(S)$.
With our simulation hypothesis, we derive $(\w{An}_{\imp}(S), s[\kappa(S) /\w{cost}]) \eval s'[c'/\w{cost}]$.
Using the proposition~\ref{annot-imp-vm} with $C = C' = \epsilon$, $d = 0$ and $\sigma = \epsilon$, we have:

{\footnotesize
\[
\w{An}_{\vm}(\cl{C}(S)) \Gives (0,\epsilon, s[0/\w{cost}]) \trarrow (|\w{An}_{\vm}(\cl{C}(P))|,\epsilon,s'[d'/\w{cost}]) ~,
\]}
where $d' \leq (c' - \kappa(S)) +\kappa(S) = c'$.
%
By definition, $\cl{C}(P) = \cl{C}(S) \cdot \s{halt}$ and $|\w{An}_{\vm}(\cl{C}(P))| = 5 \cdot |\cl{C}(P)|$. We can rewrite the simulation:

{\footnotesize\[
\w{An}_{\vm}(\cl{C}(P)) \Gives (0,\epsilon, s[0/\w{cost}]) \trarrow (5 \cdot |\cl{C}(P)|,\epsilon,s'[d'/\w{cost}]) ~.
\]}
By proposition~\ref{well-formed-prop}, there is a decoration $h$ such that $\cl{C}(P) : h$ and $h(0) = 0$. 
By iterating proposition~\ref{labelled-simulation-vm-mips},
we derive:

{\footnotesize\[
\w{An}_{\mips}(\cl{C'}(\cl{C}(P))) \Gives (9 \cdot p(0,\cl{C}(P)), m) \trarrow (9 \cdot p(|\cl{C}(P)|, \cl{C}(P)), m')~,
\]}
with $m'[d'/l_{\w{cost}}] \real \epsilon, s'[d'/\w{cost}]$ and $m'(l_{\w{cost}}) \le d'$.
%
We know that the last instruction of $\cl{C}(P)$ is an $\s{halt}$, therefore the last instruction of $\cl{C'}(\cl{C}(P))$ is also an $\s{halt}$. By definition, $p(|\cl{C}(P)|, \cl{C}(P))$ is the position after this instruction. That gives us:

{\footnotesize\[
(\w{An}_{\mips}(\cl{C'}(\cl{C}(P))),m)
 \eval m' ~.
\]}
And by transitivity we have:
$m'(l_{\w{cost}}) \le d' \le c'$. \qed


\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}} 
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$. \qed


\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$ and \s{while} $lb$ \s{do} $S$ introduce loops in the
compiled code.  In the second case, the compilation ensures that a
label is placed in the loop.  In 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.

\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





\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