source: Deliverables/D3.4/Report/report.tex @ 3191

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

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

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

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

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

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

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


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

\date{ }
\author{}

\begin{document}
\thispagestyle{empty}

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

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


\vspace*{0.5cm}
\begin{center}
\begin{LARGE}
\bf
Report n. D3.4\\
Front-end Correctness Proofs\\
\end{LARGE} 
\end{center}

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

\vspace*{0.5cm}
\begin{center}
\begin{large}
Authors:\\
Brian~Campbell, Ilias~Garnier, James~McKinna, Ian~Stark
\end{large}
\end{center}

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

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

\newpage

\vspace*{7cm}
\paragraph{Abstract}
We report on the correctness proofs for the front-end of the \cerco{}
cost lifting compiler.  First, we identify the core result we wish to
prove, which says that the we correctly predict the precise execution
time for particular parts of the execution called \emph{measurable}
subtraces.  Then we consider the three distinct parts of the task:
showing that the \emph{annotated source code} output by the compiler
has equivalent behaviour to the original input (up to the
annotations); showing that a measurable subtrace of the
annotated source code corresponds to an equivalent measurable subtrace
in the code produced by the front-end, including costs; and finally
showing that the enriched \emph{structured} execution traces required
for cost correctness in the back-end can be constructed from the
properties of the code produced by the front-end.

A key part of our work is that the intensional correctness results that show
that we get consistent cost measurements throughout the intermediate languages
of the compiler can be layered on top of normal forward simulation results,
if we split those results into local call-structure preserving simulations.

This deliverable shows correctness results about the formalised
compiler described in D3.2, using the source language semantics from
D3.1 and intermediate language semantics from D3.3.  It builds on
earlier work on a toy compiler built to test the labelling approach in
D2.1. Together with the companion deliverable about the correctness of
the back-end, D4.4, we obtain results about the whole formalised
compiler.

% TODO: mention the deliverable about the extracted compiler et al?

\newpage 

\tableofcontents

% CHECK: clear up any -ize vs -ise
% CHECK: clear up any "front end" vs "front-end"
% CHECK: clear up any mentions of languages that aren't textsf'd.
% CHECK: fix unicode in listings

\section{Introduction}

\todo{add stack space for more precise statement.  Also do some
translation validation on sound, precise labelling properties.}

The \cerco{} compiler compiles C code, targeting microcontrollers
implementing the Intel 8051 architecture.  It produces both the object
code and source code containing annotations describing the timing
behaviour of the object code.  There are two versions: first, an
initial prototype implemented in \ocaml{}~\cite{d2.2}, and a version
formalised in the \matita{} proof assistant~\cite{d3.2,d4.2} and then
extracted to \ocaml{} code to produce an executable compiler.  In this
document we present results formalised in \matita{} about the
front-end of the latter version of the compiler, and how that fits
into the verification of the whole compiler.

\todo{maybe mention stack space here?  other additions?  refer to
  "layering"?}  A key part of this work was to separate the proofs
about the compiled code's extensional behaviour (that is, the
functional correctness of the compiler) from the intensional
correctness that the costs given are correct.  Unfortunately, the
ambitious goal of completely verifying the entire compiler was not
feasible within the time available, but thanks to this separation of
extensional and intensional proofs we are able to axiomatize
simulation results similar to those in other compiler verification
projects and concentrate on the novel intensional proofs.  The proofs
were also made more tractable by introducing compile-time checks for
the `sound and precise' cost labelling properties rather than proving
that they are preserved throughout.

The overall statement of correctness says that the annotated program has the
same behaviour as the input, and that for any suitably well-structured part of
the execution (which we call \emph{measurable}), the object code will execute
the same behaviour taking precisely the time given by the cost annotations in
the annotated source program.

In the next section we recall the structure of the compiler and make the overall
statement more precise.  Following that, in Section~\ref{sec:fegoals} we
describe the statements we need to prove about the intermediate \textsf{RTLabs}
programs sufficient for the back-end proofs.  \todo{rest of document structure}

\section{The compiler and main goals}

The unformalised \ocaml{} \cerco{} compiler was originally described
in Deliverables 2.1 and 2.2.  Its design was replicated in the formal
\matita{} code, which was presented in Deliverables 3.2 and 4.2, for
the front-end and back-end respectively.

\begin{figure}
\begin{center}
\includegraphics{compiler-plain.pdf}
\end{center}
\caption{Languages in the \cerco{} compiler}
\label{fig:compilerlangs}
\end{figure}

The compiler uses a number of intermediate languages, as outlined the
middle two lines of Figure~\ref{fig:compilerlangs}.  The upper line
represents the front-end of the compiler, and the lower the back-end,
finishing with 8051 binary code.  Not all of the front-end passes
introduces a new language, and Figure~\ref{fig:summary} presents a
list of every pass involved.

\begin{figure}
\begin{center}
\begin{minipage}{.8\linewidth}
\begin{tabbing}
\quad \= $\downarrow$ \quad \= \kill
\textsf{C} (unformalized)\\
\> $\downarrow$ \> CIL parser (unformalized \ocaml)\\
\textsf{Clight}\\
%\> $\downarrow$ \> add runtime functions\\
\> $\downarrow$ \> \lstinline[language=C]'switch' removal\\
\> $\downarrow$ \> labelling\\
\> $\downarrow$ \> cast removal\\
\> $\downarrow$ \> stack variable allocation and control structure
 simplification\\
\textsf{Cminor}\\
%\> $\downarrow$ \> generate global variable initialization code\\
\> $\downarrow$ \> transform to RTL graph\\
\textsf{RTLabs}\\
\> $\downarrow$ \> check cost labelled properties of RTL graph\\
\> $\downarrow$ \> start of target specific back-end\\
\>\quad \vdots
\end{tabbing}
\end{minipage}
\end{center}
\caption{Front-end languages and compiler passes}
\label{fig:summary}
\end{figure}

\label{page:switchintro}
The annotated source code is taken after the cost labelling phase.
Note that there is a pass to replace C \lstinline[language=C]'switch'
statements before labelling --- we need to remove them because the
simple form of labelling used in the formalised compiler is not quite
capable of capturing their execution time costs, largely due to the
fall-through behaviour.

The cast removal phase which follows cost labelling simplifies
expressions to prevent unnecessary arithmetic promotion which is
specified by the C standard but costly for an 8-bit target.  The
transformation to \textsf{Cminor} and subsequently \textsf{RTLabs}
bear considerable resemblance to some passes of the CompCert
compiler\todo{cite}, although we use a simpler \textsf{Cminor} where
all loops use \lstinline[language=C]'goto' statements, and the
\textsf{RTLabs} language retains a target-independent flavour.  The
back-end takes \textsf{RTLabs} code as input.

The whole compilation function returns the following information on success:
\begin{lstlisting}[language=matita]
record compiler_output : Type[0] :=
 { c_labelled_object_code: labelled_object_code
 ; c_stack_cost: stack_cost_model
 ; c_max_stack: nat
 ; c_init_costlabel: costlabel
 ; c_labelled_clight: clight_program
 ; c_clight_cost_map: clight_cost_map
 }.
\end{lstlisting}
It consists of annotated 8051 object code, a mapping from function
identifiers to the function's stack space usage\footnote{The compiled
  code's only stack usage is to allocate a fixed-size frame on each
  function entry and discard it on exit.  No other dynamic allocation
  is provided by the compiler.}, the space available for the
stack after global variable allocation, a cost label covering the
execution time for the initialisation of global variables and the call
to the \lstinline[language=C]'main' function, the annotated source
code, and finally a mapping from cost labels to actual execution time
costs.

An \ocaml{} pretty printer is used to provide a concrete version of the output
code.  In the case of the annotated source code, it also inserts the actual
costs alongside the cost labels, and optionally adds a global cost variable
and instrumentation to support further reasoning.  \todo{Cross-ref case study
deliverables}

\subsection{Revisions to the prototype compiler}

Our focus on intensional properties prompted us to consider whether we
could incorporate stack space into the costs presented to the user.
We only allocate one fixed-size frame per function, so modelling this
was relatively simple.  It is the only form of dynamic memory
allocation provided by the compiler, so we were able to strengthen the
statement of the goal to guarantee successful execution whenever the
stack space obeys a bound calculated by subtracting the global
variable requirements from the total memory available.

The cost checks at the end of Figure~\ref{fig:summary} have been
introduced to reduce the proof burden, and are described in
Section~\ref{sec:costchecks}.

The use of dependent types to capture simple intermediate language
invariants makes every front-end pass except \textsf{Clight} to
\textsf{Cminor} and the cost checks total functions.  Hence various
well-formedness and type checks are dealt with once in that phase.
With the benefit of hindsight we would have included an initial
checking phase to produce a `well-formed' variant of \textsf{Clight},
conjecturing that this would simplify various parts of the proofs for
the \textsf{Clight} stages which deal with potentially ill-formed
code.

\todo{move of initialisation code?}

\subsection{Main goals}

TODO: need an example for this

Informally, our main intensional result links the time difference in a source
code execution to the time difference in the object code, expressing the time
for the source by summing the values for the cost labels in the trace, and the
time for the target by a clock built in to the 8051 executable semantics.

The availability of precise timing information for 8501
implementations and the design of the compiler allow it to give exact
time costs in terms of processor cycles, not just upper bounds.
However, these exact results are only available if the subtrace we
measure starts and ends at suitable points.  In particular, pure
computation with no observable effects may be reordered and moved past
cost labels, so we cannot measure time between arbitrary statements in
the program.

There is also a constraint on the subtraces that we
measure due to the requirements of the correctness proof for the
object code timing analysis.  To be sure that the timings are assigned
to the correct cost label, we need to know that each return from a
function call must go to the correct return address.  It is difficult
to observe this property locally in the object code because it relies
on much earlier stages in the compiler.  To convey this information to
the timing analysis extra structure is imposed on the subtraces, which
is described in Section~\ref{sec:fegoals}.

% Regarding the footnote, would there even be much point?
% TODO: this might be quite easy to add ('just' subtract the
% measurable subtrace from the second label to the end).  Could also
% measure other traces in this manner.
These restrictions are reflected in the subtraces that we give timing
guarantees on; they must start at a cost label and end at the return
of the enclosing function of the cost label\footnote{We expect that
  this would generalise to subtraces between cost labels in the same
  function, but could not justify the extra complexity that would be
  required to show this.}.  A typical example of such a subtrace is
the execution of an entire function from the cost label at the start
of the function until it returns.  We call such any such subtrace
\emph{measurable} if it (and the prefix of the trace from the start to
the subtrace) can also be executed within the available stack space.

Now we can give the main intensional statement for the compiler.
Given a \emph{measurable} subtrace for a labelled \textsf{Clight}
program, there is a subtrace of the 8051 object code program where the
time differences match.  Moreover, \emph{observable} parts of the
trace also match --- these are the appearance of cost labels and
function calls and returns.

More formally, the definition of this statement in \matita{} is
\begin{lstlisting}[language=matita]
definition simulates := 
  $\lambda$p: compiler_output.
  let initial_status := initialise_status $\dots$ (cm (c_labelled_object_code $\dots$ p)) in
  $\forall$m1,m2.
   measurable Clight_pcs (c_labelled_clight $\dots$ p) m1 m2
    (lookup_stack_cost (c_stack_cost $\dots$ p)) (c_max_stack $\dots$ p) $\rightarrow$
  $\forall$c1,c2.
   clock_after Clight_pcs (c_labelled_clight $\dots$ p) m1 (c_clight_cost_map $\dots$ p) = OK $\dots$ c1 $\rightarrow$
   clock_after Clight_pcs (c_labelled_clight $\dots$ p) (m1+m2) (c_clight_cost_map $\dots$ p) = OK $\dots$ c2 $\rightarrow$
  $\exists$n1,n2.
   observables Clight_pcs (c_labelled_clight $\dots$ p) m1 m2 =
   observables (OC_preclassified_system (c_labelled_object_code $\dots$ p))
    (c_labelled_object_code $\dots$ p) n1 n2
  $\wedge$
   c2 - c1 = clock $\dots$ (execute n2 ? initial_status) - clock $\dots$ (execute n1 ? initial_status).
\end{lstlisting}
where the \lstinline'measurable', \lstinline'clock_after' and
\lstinline'observables' definitions can be applied to multiple
languages; in this case the \lstinline'Clight_pcs' record applies them
to \textsf{Clight} programs.

There is a second part to the statement, which says that the initial
processing of the input program to produce the cost labelled version
does not affect the semantics of the program:
% Yes, I'm paraphrasing the result a tiny bit to remove the observe non-function
\begin{lstlisting}[language=matita]
  $\forall$input_program,output.
  compile input_program = return output $\rightarrow$
  not_wrong … (exec_inf … clight_fullexec input_program) $\rightarrow$
  sim_with_labels
   (exec_inf … clight_fullexec input_program)
   (exec_inf … clight_fullexec (c_labelled_clight … output))
\end{lstlisting}
That is, any successful compilation produces a labelled program that
has identical behaviour to the original, so long as there is no
`undefined behaviour'.

Note that this provides full functional correctness, including
preservation of (non-)termination.  The intensional result above does
not do this directly --- it does not guarantee the same result or same
termination.  There are two mitigating factors, however: first, to
prove the intensional property you need local simulation results that
can be pieced together to form full behavioural equivalence, only time
constraints have prevented us from doing so.  Second, if we wish to
confirm a result, termination, or non-termination we could add an
observable witness, such as a function that is only called if the
correct result is given.  The intensional result guarantees that the
observable witness is preserved, so the program must behave correctly.

\section{Intermediate goals for the front-end}
\label{sec:fegoals}

The essential parts of the intensional proof were outlined during work
on a toy
compiler~\cite{d2.1,springerlink:10.1007/978-3-642-32469-7_3}.  These
are
\begin{enumerate}
\item functional correctness, in particular preserving the trace of
  cost labels,
\item the \emph{soundness} and \emph{precision} of the cost labelling
  on the object code, and
\item the timing analysis on the object code produces a correct
  mapping from cost labels to time.
\end{enumerate}

However, that toy development did not include function calls.  For the
full \cerco{} compiler we also need to maintain the invariant that
functions return to the correct program location in the caller, as we
mentioned in the previous section.  During work on the back-end timing
analysis (describe in more detail in the companion deliverable, D4.4)
the notion of a \emph{structured trace} was developed to enforce this
return property, and also most of the cost labelling properties too.

\begin{figure}
\begin{center}
\includegraphics[width=0.5\linewidth]{compiler.pdf}
\end{center}
\caption{The compiler and proof outline}
\label{fig:compiler}
\end{figure}

Jointly, we generalised the structured traces to apply to any of the
intermediate languages with some idea of program counter.  This means
that they are introduced part way through the compiler, see
Figure~\ref{fig:compiler}.  Proving that a structured trace can be
constructed at \textsf{RTLabs} has several virtues:
\begin{itemize}
\item This is the first language where every operation has its own
  unique, easily addressable, statement.
\item Function calls and returns are still handled implicitly in the
  language and so the structural properties are ensured by the
  semantics.
\item Many of the back-end languages from \textsf{RTL} share a common
  core set of definitions, and using structured traces throughout
  increases this uniformity.
\end{itemize}

\begin{figure}
\begin{center}
\includegraphics[width=0.6\linewidth]{strtraces.pdf}
\end{center}
\caption{Nesting of functions in structured traces}
\label{fig:strtrace}
\end{figure}
A structured trace is a mutually inductive data type which 
contains the steps from a normal program trace, but arranged into a
nested structure which groups entire function calls together and
aggregates individual steps between cost labels (or between the final
cost label and the return from the function), see
Figure~\ref{fig:strtrace}.  This captures the idea that the cost labels
only represent costs \emph{within} a function --- calls to other
functions are accounted for in the nested trace for their execution, and we
can locally regard function calls as a single step.

These structured traces form the core part of the intermediate results
that we must prove so that the back-end can complete the main
intensional result stated above.  In full, we provide the back-end
with
\begin{enumerate}
\item A normal trace of the \textbf{prefix} of the program's execution
  before reaching the measurable subtrace.  (This needs to be
  preserved so that we know that the stack space consumed is correct,
  and to set up the simulation results.)
\item The \textbf{structured trace} corresponding to the measurable
  subtrace.
\item An additional property about the structured trace that no
  `program counter' is \textbf{repeated} between cost labels.  Together with
  the structure in the trace, this takes over from showing that
  cost labelling is sound and precise.
\item A proof that the \textbf{observables} have been preserved.
\item A proof that the \textbf{stack limit} is still observed by the prefix and
  the structure trace.  (This is largely a consequence of the
  preservation of observables.)
\end{enumerate}

Following the outline in Figure~\ref{fig:compiler}, we will first deal
with the transformations in \textsf{Clight} that produce the source
program with cost labels, then show that measurable traces can be
lifted to \textsf{RTLabs}, and finally that we can construct the
properties listed above ready for the back-end proofs.

\section{Input code to cost labelled program}

As explained on page~\pageref{page:switchintro}, the costs of complex
C \lstinline[language=C]'switch' statements cannot be represented with
the simple labelling.  Our first pass replaces these statements with
simpler C code, allowing our second pass to perform the cost
labelling.  We show that the behaviour of programs is unchanged by
these passes.

TODO: both give one-step-sim-by-many forward sim results; switch
removal tricky, uses aux var to keep result of expr, not central to
intensional correctness so curtailed proof effort once reasonable
level of confidence in code gained; labelling much simpler; don't care
what the labels are at this stage, just need to know when to go
through extra steps.  Rolled up into a single result with a cofixpoint
to obtain coinductive statement of equivalence (show).

\section{Finding corresponding measurable subtraces}

There follow the three main passes of the front-end:
\begin{enumerate}
\item simplification of casts in \textsf{Clight} code
\item \textsf{Clight} to \textsf{Cminor} translation, performing stack
  variable allocation and simplifying control structures
\item transformation to \textsf{RTLabs} control flow graph
\end{enumerate}
\todo{I keep mentioning forward sim results - I probably ought to say
  something about determinancy} We have taken a common approach to
each pass: first we build (or axiomatise) forward simulation results
that are similar to normal compiler proofs, but slightly more
fine-grained so that we can see that the call structure and relative
placement of cost labels is preserved.

Then we instantiate a general result which shows that we can find a
\emph{measurable} subtrace in the target of the pass that corresponds
to the measurable subtrace in the source.  By repeated application of
this result we can find a measurable subtrace of the execution of the
\textsf{RTLabs} code, suitable for the construction of a structured
trace (see Section~\ref{sec:structuredtrace}.  This is essentially an
extra layer on top of the simulation proofs that provides us with the
extra information required for our intensional correctness proof.

\subsection{Generic measurable subtrace lifting proof}

Our generic proof is parametrised on a record containing small-step
semantics for the source and target language, a classification of
states (the same form of classification is used when defining
structured traces), a simulation relation which loosely respects the
classification and cost labelling \todo{this isn't very helpful} and
four simulation results:
\begin{enumerate}
\item a step from a `normal' state (which is not classified as a call
  or return) which is not a cost label is simulated by zero or more
  `normal' steps;
\item a step from a `call' state followed by a cost label step is
  simulated by a step from a `call' state, a corresponding label step,
  then zero or more `normal' steps;
\item a step from a `call' state not followed by a cost label
  similarly (note that this case cannot occur in a well-labelled
  program, but we do not have enough information locally to exploit
  this); and
\item a cost label step is simulated by a cost label step.
\end{enumerate}
Finally, we need to know that a successfully translated program will
have an initial state in the simulation relation with the original
program's initial state.

\begin{figure}
\begin{center}
\includegraphics[width=0.5\linewidth]{meassim.pdf}
\end{center}
\caption{Tiling of simulation for a measurable subtrace}
\label{fig:tiling}
\end{figure}

To find the measurable subtrace in the target program's execution we
walk along the original program's execution trace applying the
appropriate simulation result by induction on the number of steps.
While the number of steps taken varies, the overall structure is
preserved, as illustrated in Figure~\ref{fig:tiling}.  By preserving
the structure we also maintain the same intensional observables.  One
delicate point is that the cost label following a call must remain
directly afterwards\footnote{The prototype compiler allowed some
  straight-line code to appear before the cost label until a later
  stage of the compiler, but we must move the requirement forward to
  fit with the structured traces.}
% Damn it, I should have just moved the cost label forwards in RTLabs,
% like the prototype does in RTL to ERTL; the result would have been
% simpler.  Or was there some reason not to do that?
(both in the program code and in the execution trace), even if we
introduce extra steps, for example to store parameters in memory in
\textsf{Cminor}.  Thus we have a version of the call simulation
that deals with both in one result.

In addition to the subtrace we are interested in measuring we must
also prove that the earlier part of the trace is also preserved in
order to use the simulation from the initial state.  It also
guarantees that we do not run out of stack space before the subtrace
we are interested in.  The lemmas for this prefix and the measurable
subtrace are similar, following the pattern above.  However, the
measurable subtrace also requires us to rebuild the termination
proof.  This is defined recursively:
\label{prog:terminationproof}
\begin{lstlisting}[language=matita]
let rec will_return_aux C (depth:nat)
                             (trace:list (cs_state … C × trace)) on trace : bool :=
match trace with
[ nil $\Rightarrow$ false
| cons h tl $\Rightarrow$
  let $\langle$s,tr$\rangle$ := h in
  match cs_classify C s with
  [ cl_call $\Rightarrow$ will_return_aux C (S depth) tl
  | cl_return $\Rightarrow$
      match depth with
      [ O $\Rightarrow$ match tl with [ nil $\Rightarrow$ true | _ $\Rightarrow$ false ]
      | S d $\Rightarrow$ will_return_aux C d tl
      ]
  | _ $\Rightarrow$ will_return_aux C depth tl
  ]
].
\end{lstlisting}
The \lstinline'depth' is the number of return states we need to see
before we have returned to the original function (initially zero) and
\lstinline'trace' the measurable subtrace obtained from the running
the semantics for the correct number of steps.  This definition
unfolds tail recursively for each step, and once the corresponding
simulation result has been applied a new one for the target can be
asserted by unfolding and applying the induction hypothesis on the
shorter trace.

This then gives us an overall result for any simulation fitting the
requirements above (contained in the \lstinline'meas_sim' record):
\begin{lstlisting}[language=matita]
theorem measured_subtrace_preserved :
  $\forall$MS:meas_sim.
  $\forall$p1,p2,m,n,stack_cost,max.
  ms_compiled MS p1 p2 $\rightarrow$
  measurable (ms_C1 MS) p1 m n stack_cost max $\rightarrow$
  $\exists$m',n'.
    measurable (ms_C2 MS) p2 m' n' stack_cost max $\wedge$
    observables (ms_C1 MS) p1 m n = observables (ms_C2 MS) p2 m' n'.
\end{lstlisting}
The stack space requirement that is embedded in \lstinline'measurable'
is a consequence of the preservation of observables.

TODO: how to deal with untidy edges wrt to sim rel; anything to
say about obs?

TODO: say something about termination measures; cost labels are
statements/exprs in these languages; split call/return gives simpler
simulations

\subsection{Simulation results for each pass}

\todo{don't use loop structures from CompCert, go straight to jumps}

\paragraph{Cast simplification.}

The parser used in Cerco introduces a lot of explicit type casts. 
If left as they are, these constructs can greatly hamper the 
quality of the generated code -- especially as the architecture 
we consider is an $8$ bit one. In \textsf{Clight}, casts are 
expressions. Hence, most of the work of this transformation 
proceeds on expressions. The tranformation proceeds by recursively 
trying to coerce an expression to a particular integer type, which 
is in practice smaller than the original one. This functionality 
is implemented by two mutually recursive functions whose signature 
is the following.

\begin{lstlisting}[language=matita]
let rec simplify_expr (e:expr) (target_sz:intsize) (target_sg:signedness) 
  : Σresult:bool×expr. 
    ∀ge,en,m. simplify_inv ge en m e (\snd result) target_sz target_sg (\fst result) ≝ $\ldots$

and simplify_inside (e:expr) : Σresult:expr. conservation e result ≝ $\ldots$
\end{lstlisting}

The \textsf{simplify\_inside} acts as a wrapper for 
\textsf{simplify\_expr}. Whenever \textsf{simplify\_inside} encounters 
a \textsf{Ecast} expression, it tries to coerce the sub-expression 
to the desired type using \textsf{simplify\_expr}, which tries to 
perform the actual coercion. In return, \textsf{simplify\_expr} calls 
back \textsf{simplify\_inside} in some particular positions, where we
decided to be conservative in order to simplify the proofs. However, 
the current design allows to incrementally revert to a more aggressive 
version, by replacing recursive calls to \textsf{simplify\_inside} by 
calls to \textsf{simplify\_expr} \emph{and} proving the corresponding 
invariants -- where possible. 

The \textsf{simplify\_inv} invariant encodes either the conservation 
of the semantics during the transformation corresponding to the failure 
of the transformation (\textsf{Inv\_eq} constructor), or the successful 
downcast of the considered expression to the target type 
(\textsf{Inv\_coerce\_ok}).

\begin{lstlisting}[language=matita]
inductive simplify_inv 
  (ge : genv) (en : env) (m : mem) 
  (e1 : expr) (e2 : expr) (target_sz : intsize) (target_sg : signedness) : bool → Prop ≝
| Inv_eq : ∀result_flag. $\ldots$
     simplify_inv ge en m e1 e2 target_sz target_sg result_flag
| Inv_coerce_ok : ∀src_sz,src_sg.
     (typeof e1) = (Tint src_sz src_sg) → (typeof e2) = (Tint target_sz target_sg) →     
     (smaller_integer_val src_sz target_sz src_sg (exec_expr ge en m e1) (exec_expr ge en m e2)) →
     simplify_inv ge en m e1 e2 target_sz target_sg true.
\end{lstlisting}

The \textsf{conservation} invariant simply states the conservation 
of the semantics, as in the \textsf{Inv\_eq} constructor of the previous 
invariant.

\begin{lstlisting}[language=matita]
definition conservation ≝ λe,result. ∀ge,en,m. 
          res_sim ? (exec_expr ge en m e) (exec_expr ge en m result)
         ∧ res_sim ? (exec_lvalue ge en m e) (exec_lvalue ge en m result)
         ∧ typeof e = typeof result.
\end{lstlisting}

This invariant is then easily lifted to statement evaluations.
The main problem encountered with this particular pass was dealing with 
inconsistently typed programs, a canonical case being a particular 
integer constant of a certain size typed with another size. This 
prompted the need to introduce numerous type checks, complexifying 
both the implementation and the proof.
\todo{Make this a particular case of the more general statement on baking more invariants in the Clight language}

\paragraph{Switch removal.}

The intermediate languages of the front-end have no jump tables. 
Hence, we have to compile the \lstinline[language=C]'switch' 
constructs away before going from \textsf{Clight} to \textsf{Cminor}. 
Note that this transformation does not necessarily deteriorate the 
efficiency of the generated code. For instance, compilers such as GCC 
introduce balanced trees of ``if-then-else'' constructs for small 
switches. However, our implementation strategy is much simpler. Let 
us consider the following input statement.

\begin{lstlisting}[language=C]
   switch(e) {
   case v1:
     stmt1;
   case v2:
     stmt2;
   default:
     stmt_default;
   }
\end{lstlisting}

Note that \textsf{stmt1}, \textsf{stmt2}, \ldots \textsf{stmt\_default}
may contain \lstinline[language=C]'break' statements, which have the 
effect of exiting the switch statement. In the absence of break, the 
execution falls through each case sequentially. In our current implementation, 
we produce an equivalent sequence of ``if-then'' chained by gotos:
\begin{lstlisting}[language=C]
   fresh = e;
   if(fresh == v1) {
     $\llbracket$stmt1$\rrbracket$; 
     goto lbl_case2;
   };
   if(fresh == v2) {
     lbl_case2:
     $\llbracket$stmt2;$\rrbracket$
     goto lbl_case2;
   };
   $\llbracket$stmt_default$\rrbracket$;
   exit_label:
\end{lstlisting}

The proof had to tackle the following points:
\begin{itemize}
\item the source and target memories are not the same (cf. fresh variable),
\item the flow of control is changed in a non-local way (e.g. \textbf{goto} 
  instead of \textbf{break}).
\end{itemize}

In order to tackle the first point, we implemented a version of memory 
extensions similar to Compcert's. What has been done is the simulation proof 
for all ``easy'' cases, that do not interact with the switch removal per se, 
plus a bit of the switch case. This comprises propagating the memory extension 
through  each statement (except switch), as well as various invariants that 
are needed for the switch case (in particular, freshness hypotheses). The 
details of the evaluation process for the source switch statement and its 
target counterpart can be found in the file \textbf{switchRemoval.ma},
along more details on the transformation itself. 

Proving the correctness of the second point would require reasoning on the 
semantics of \lstinline[language=C]'goto' statements. In the \textsf{Clight} 
semantics, this is implemented as a function-wide lookup of the target label. 
The invariant we would need is the fact that a global label lookup on a freshly 
created goto is equivalent to a local lookup. This would in turn require the 
propagation of some freshness hypotheses on labels. For reasons expressed above, 
we decided to omit this part of the correctness proof.

\paragraph{Clight to Cminor.}

This pass is the last one operating on the Clight intermediate language. 
Its input is a full \textsf{Clight} program, and its output is a \textsf{Cminor} 
program. Note that we do not use an equivalent of the C\#minor language: we 
translate directly to Cminor. This presents the advantage of not requiring the 
special loop constructs, nor the explicit block structure. Another salient 
point of our approach is that a significant part of the properties needed for 
the simulation proof were directly encoded in dependently typed translation 
functions. This concerns more precisely freshness conditions and well-typedness
conditions. The main effects of the transformation from \textsf{Clight} to 
\textsf{Cminor} are listed below.

\begin{itemize}
\item Variables are classified as being either globals, stack-allocated 
  locals or potentially register-allocated locals. The value of register-allocated 
  local variables is moved out of the modelled memory and stored in a 
  dedicated environment.
\item In Clight, each local variable has a dedicated memory block, whereas 
  stack-allocated locals are bundled together on a function-by-function basis.
\item Loops are converted to jumps.
\end{itemize}

The first two points require memory injections which are more flexible that those 
needed in the switch removal case. In the remainder of this section, we briefly 
discuss our implementation of memory injections, and then the simulation proof.

\subparagraph{Memory injections.}

Our memory injections are modelled after the work of Blazy \& Leroy. 
However, the corresponding paper is based on the first version of the 
Compcert memory model, whereas we use a much more concrete model, allowing byte-level
manipulations (as in the later version of Compcert's memory model). We proved 
roughly 80 \% of the required lemmas. Some difficulties encountered were notably 
due to some too relaxed conditions on pointer validity (problem fixed during development).
Some more conditions had to be added to take care of possible overflows when converting 
from \textbf{Z} block bounds to $16$ bit pointer offsets (in pratice, these overflows 
only occur in edge cases that are easily ruled out -- but this fact is not visible 
in memory injections). Concretely, some of the lemmas on the preservation of simulation of 
loads after writes were axiomatised, for lack of time.

\subparagraph{Simulation proof.}

The correction proof for this transformation was not terminated. We proved the 
simulation result for expressions and for some subset of the critical statement cases. 
Notably lacking are the function entry and exit, where the memory injection is
properly set up. As can be guessed, a significant amount of work has to be performed 
to show the conservation of all invariants at each simulation step.

\todo{list cases, explain while loop, explain labeling problem}

\section{Checking cost labelling properties}
\label{sec:costchecks}

Ideally, we would provide proofs that the cost labelling pass always
produced programs that are soundly and precisely labelled and that
each subsequent pass preserves these properties.  This would match our
use of dependent types to eliminate impossible sources of errors
during compilation, in particular retaining intermediate language type
information.

However, given the limited amount of time available we realised that
implementing a compile-time check for a sound and precise labelling of
the \textsf{RTLabs} intermediate code would reduce the proof burden
considerably.  This is similar in spirit to the use of translation
validation in certified compilation\todo{Cite some suitable work
  here}, which makes a similar trade-off between the potential for
compile-time failure and the volume of proof required.

The check cannot be pushed into a later stage of the compiler because
much of the information is embedded into the structured traces.
However, if an alternative method was used to show that function
returns in the compiled code are sufficiently well-behaved, then we
could consider pushing the cost property checks into the timing
analysis itself.  We leave this as a possible area for future work.

\subsection{Implementation and correctness}

For a cost labelling to be sound and precise we need a cost label at
the start of each function, after each branch and at least one in
every loop.  The first two parts are trivial to check by examining the
code.  In \textsf{RTLabs} the last part is specified by saying
that there is a bound on the number of successive instruction nodes in
the CFG that you can follow before you encounter a cost label, and
checking this is more difficult.

The implementation works through the set of nodes in the graph,
following successors until a cost label is found or a label-free cycle
is discovered (in which case the property does not hold and we stop).
This is made easier by the prior knowledge that any branch is followed
by cost labels, so we do not need to search each branch.  When a label
is found, we remove the chain from the set and continue from another
node in the set until it is empty, at which point we know that there
is a bound for every node in the graph.

Directly reasoning about the function that implements this would be
rather awkward, so an inductive specification of a single step of its
behaviour was written and proved to match the implementation.  This
was then used to prove the implementation sound and complete.

While we have not attempted to proof that the cost labelled properties
are established and preserved earlier in the compiler, we expect that
the effort for the \textsf{Cminor} to \textsf{RTLabs} would be similar
to the work outlined above, because it involves the change from
requiring a cost label at particular positions to requiring cost
labels to break loops in the CFG.  As there are another three passes
to consider (including the labelling itself), we believe that using
the check above is much simpler overall.

% TODO? Found some Clight to Cminor bugs quite quickly

\section{Existence of a structured trace}
\label{sec:structuredtrace}

\emph{Structured traces} enrich the execution trace of a program by
nesting function calls in a mixed-step style\todo{Can I find a
  justification for mixed-step} and embedding the cost properties of
the program.  It was originally designed to support the proof of
correctness for the timing analysis of the object code in the
back-end, then generalised to provide a common structure to use from
the end of the front-end to the object code.  See
Figure~\ref{fig:strtrace} on page~\pageref{fig:strtrace}
for an illustration of a structured trace.

To make the definition generic we abstract over the semantics of the
language,
\begin{lstlisting}[language=matita]
record abstract_status : Type[1] :=
  { as_status :> Type[0]
  ; as_execute : relation as_status
  ; as_pc : DeqSet
  ; as_pc_of : as_status $\rightarrow$ as_pc
  ; as_classify : as_status $\rightarrow$ status_class
  ; as_label_of_pc : as_pc $\rightarrow$ option costlabel
  ; as_after_return : ($\Sigma$s:as_status. as_classify s =  cl_call) $\rightarrow$ as_status $\rightarrow$ Prop
  ; as_result: as_status $\rightarrow$ option int
  ; as_call_ident : ($\Sigma$s:as_status.as_classify s = cl_call) $\rightarrow$ ident
  ; as_tailcall_ident : ($\Sigma$s:as_status.as_classify s = cl_tailcall) $\rightarrow$ ident
  }.
\end{lstlisting}
which gives a type of states, an execution relation, some notion of
program counters with decidable equality, the classification of states
and functions to extract the observable intensional information (cost
labels and the identity of functions that are called).  The
\lstinline'as_after_return' property links the state before a function
call with the state after return, providing the evidence that
execution returns to the correct place.  The precise form varies
between stages; in \textsf{RTLabs} it insists the CFG, the pointer to
the CFG node to execute next, and some call stack information is
preserved.

The structured traces are defined using three mutually inductive
types.  The core data structure is \lstinline'trace_any_label', which
captures some straight-line execution until the next cost label or
function return.  Each function call is embedded as a single step,
with its own trace nested inside and the before and after states
linked by \lstinline'as_after_return', and states classified as a
`jump' (in particular branches) must be followed by a cost label.

The second type, \lstinline'trace_label_label', is a
\lstinline'trace_any_label' where the initial state is cost labelled.
Thus a trace in this type identifies a series of steps whose cost is
entirely accounted for by the label at the start.

Finally, \lstinline'trace_label_return' is a sequence of
\lstinline'trace_label_label' values which end in the return from the
function.  These correspond to a measurable subtrace, and in
particular include executions of an entire function call (and so are
used for the nested calls in \lstinline'trace_any_label').

\subsection{Construction}

The core part of the construction of a fixed trace is to use the proof
of termination from the measurable trace (defined on
page~\pageref{prog:terminationproof}) to `fold up' the execution into
the nested form.

TODO: design, basic structure from termination proof, how cost
labelling props are baked in; unrepeating PCs, remainder of sound
labellings; coinductive version for whole programs, reason/relevance,
use of em (maybe a general comment about uses of classical reasoning
in development)

\section{Conclusion}

TODO

TODO: appendix on code layout?

\bibliographystyle{plain}
\bibliography{report}

\end{document}