# Changeset 3223 for Deliverables/D3.4/Report/report.tex

Ignore:
Timestamp:
Apr 30, 2013, 12:05:24 PM (7 years ago)
Message:

More revisions to 3.4.

File:
1 edited

### Legend:

Unmodified
 r3218 code. \todo{move of initialisation code?} Following D2.2, we previous generated code for global variable initialisation in \textsf{Cminor}, for which we reserved a cost label to represent the execution time for initialisation.  However, the back-end must also add an initial call to the main function, whose cost must also be accounted for, so we decided to move the initialisation code to the back-end and merge the costs. \subsection{Main goals} observable witness is preserved, so the program must behave correctly. \section{Intermediate goals for the front-end} \section{Goals for the front-end} \label{sec:fegoals} 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. extensions similar to CompCert's. For the simulation we decided to prove a sufficient amount to give us confidence in the definitions and approach, but curtail the proof because this pass does not contribute to the intensional correctness result.  We tackled several simple cases, that do not interact with the switch removal per se, to show that the definitions were usable, and part of the switch case to check that the approach is reasonable. 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 both the implementation and the proof more complex, even though more comprehensive checks are made in the next stage. \todo{Make this a particular case of the more general statement on baking more invariants in the Clight language} %\todo{Make this a particular case of the more general statement on baking more invariants in the Clight language} \subsubsection{Clight to Cminor} 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 Compcert's \textsf{C\#minor} language: we translate directly to a CompCert's \textsf{C\#minor} language: we translate directly to a variant of \textsf{Cminor}. This presents the advantage of not requiring the special loop constructs, nor the explicit block 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 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 overly relaxed conditions on pointer validity (fixed during development). \paragraph{Simulation proof.} The correctness proof for this transformation was not completed. 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 would be expected, 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} We proved the simulation result for expressions and a representative selection of statements.  In particular we tackled \lstinline[language=C]'while' statements to ensure that we correctly translate loops because our approach differs from CompCert by converting directly to \textsf{Cminor} \lstinline[language=C]'goto's rather than maintaining a notion of loops.  We also have a partial proof for function entry, covering the setup of the memory injection, but not function exit.  Exits, and the remaining statements, have been axiomatised. Careful management of the proof state was required due to the proof terms that are embedded in \textsf{Cminor} code to show that some invariants are respected.  These proof terms can be large and awkward, and while generalising them away is usually sufficient, it can be difficult when they appear under a binder. %The correctness proof for this transformation was not completed. 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 would be expected, 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} \subsubsection{Cminor to RTLabs}