# Changeset 3214

Ignore:
Timestamp:
Apr 29, 2013, 7:17:03 PM (4 years ago)
Message:

Some 3.4 revisions.

File:
1 edited

### Legend:

Unmodified
 r3212 properties of the code produced by the front-end. A key part of our work is that the intensional correctness results that show A key part of our work is that the intensional correctness results which show that we get consistent cost measurements throughout the intermediate languages of the compiler can be layered on top of normal forward simulation results, 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. earlier work on the correctness of 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? \section{Introduction} 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. The \cerco{} compiler produces a version of the source code containing annotations describing the timing behaviour of the object code, as well as the object code itself. It compiles C code, targeting microcontrollers implementing the Intel 8051 architecture.  There are two versions: first, an initial prototype was implemented in \ocaml{}~\cite{d2.2}, then a version was formalised in the \matita{} proof assistant~\cite{d3.2,d4.2} and 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. A key part of this work was to layer the intensional correctness results that show that the costs given are correct on top of the results that show that the costs produced are correct on top of the proofs about the compiled code's extensional behaviour (that is, the functional correctness of the compiler).  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 extensional and intensional proofs we are able to axiomatize some simulation results which are similar to those in other compiler verification projects and concentrate on the novel intensional proofs.  We were also able to add stack space costs to obtain a stronger result.  The 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. programs for the back-end proofs. Section~\ref{sec:inputtolabelling} covers the passes which produce the annotated source program and Section~\ref{sec:measurablelifting} the rest \begin{figure} \begin{center} \includegraphics{compiler-plain.pdf} \includegraphics[width=0.5\linewidth]{compiler-plain.pdf} \end{center} \caption{Languages in the \cerco{} compiler} 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. capable of capturing their execution time costs, largely due to C's fall-through' behaviour where execution from one branch continues in the next unless there is an explicit \lstinline[language=C]'break'. The cast removal phase which follows cost labelling simplifies expressions to prevent unnecessary arithmetic promotion which is 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} 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 }. 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 identifiers to the function's stack space usage, 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 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. An \ocaml{} pretty printer is used to provide a concrete version of the output code and annotated source 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. \subsection{Revisions to the prototype compiler} 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 stack space obeys the \lstinline'c_max_stack' bound calculated by subtracting the global variable requirements from the total memory available. The cost labelling 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}. 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. well-formedness and type safety checks are performed once between \textsf{Clight} and \textsf{Cminor}, and the invariants rule out any difficulties in the later stages. With the benefit of hindsight we would have included an initial checking phase to produce a well-formed' variant of \textsf{Clight},