Changeset 3168


Ignore:
Timestamp:
Apr 19, 2013, 12:30:32 PM (4 years ago)
Author:
campbell
Message:

Add some text from Ilias.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D3.4/Report/report.tex

    r3167 r3168  
    22\usepackage[mathletters]{ucs}
    33\usepackage[utf8x]{inputenc}
     4\usepackage{stmaryrd}
    45\usepackage{listings}
    56\usepackage{../../style/cerco}
     
    579580\todo{don't use loop structures from CompCert, go straight to jumps}
    580581
     582\paragraph{Cast simplification}
     583
     584The parser used in Cerco introduces a lot of explicit type casts. If left
     585as they are, these casts can greatly hamper the quality of the generated
     586code -- especially as the architecture we consider is an $8$ bit one.
     587In \textsf{Clight}, casts are expressions. Hence, most of the work of
     588this transformation proceeds on expressions, and the one-step simulation
     589result one those is easily lifted to statement evaluations.
     590
     591\todo{introduce the explicit type signature of the functions below ?}
     592
     593The tranformation proceeds by recursively trying to coerce an expression to
     594a particular type, which is in practice a integer type smaller than the
     595original one. This functionality is implemented by two mutually recursive
     596functions: \textbf{simplify\_expr} and \textbf{simplify\_inside}. The latter
     597acts as a wrapper for the first one. Whenever \textbf{simplify\_inside}
     598encounters a \textbf{Ecast} expression, it tries to coerce the sub-expression
     599to the desired type using \textbf{simplify\_expr}, which tries to perform the
     600actual coercion. In return, \textbf{simplify\_expr} calls back
     601\textbf{simplify\_inside} in some particular positions, where we decided to
     602be conservative in order to simplify the proofs. However, the current design
     603allows to incrementally revert to a more aggressive version, by replacing
     604recursive calls to \textbf{simplify\_inside} by calls to \textbf{simplify\_expr}
     605\emph{and} proving the corresponding invariants -- where possible.
     606
     607The main problem encountered with this particular pass was dealing with inconsistently
     608typed programs, a canonical case being a particular integer constant of a certain
     609size typed with another size. This prompted the need to introduce numerous
     610type checks, complexifying both the implementation and the proof.
     611
     612\paragraph{Switch removal}
     613
     614Our intermediate languages have no jump tables. Hence, we have to compile the
     615\lstinline[language=C]'switch' constructs away before going from \textsf{Clight} to
     616\textsf{Cminor}. Note that this is not necessarily a bad decision performance-wise
     617for small switches. For instance, compilers such as GCC introduce balanced trees
     618of ``if-then-else'' constructs. However, our implementation strategy is much simpler.
     619Let us consider the following input statement.
     620
     621\begin{lstlisting}[language=C]
     622   switch(e) {
     623   case v1:
     624     stmt1;
     625   case v2:
     626     stmt2;
     627   default:
     628     stmt_default;
     629   }
     630\end{lstlisting}
     631
     632Note that stmt1, stmt2, \ldots stmt\_default may contain "break" statements,
     633which have the effect of exiting the switch statement. In the absence of break,
     634the execution falls through each case sequentially. In our current implementation,
     635we produce an equivalent sequence of ``if-then'' chained by gotos:
     636\begin{lstlisting}[language=C]
     637   fresh = e;
     638   if(fresh == v1) {
     639     $\llbracket$stmt1$\rrbracket$;
     640     goto lbl_case2;
     641   };
     642   if(fresh == v2) {
     643     lbl_case2:
     644     $\llbracket$stmt2;$\rrbracket$
     645     goto lbl_case2;
     646   };
     647   $\llbracket$stmt_default$\rrbracket$;
     648   exit_label:
     649\end{lstlisting}
     650
     651The proof had to tackle the following points:
     652\begin{itemize}
     653\item the source and target memories are not the same (cf. fresh variable),
     654\item the flow of control is changed in a non-local way (e.g. \textbf{goto}
     655  instead of \textbf{break}).
     656\end{itemize}
     657
     658In order to tackle the first point, we implemented a version of memory
     659extensions similar to Compcert's. What has been done is the simulation proof
     660for all ``easy'' cases, that do not interact with the switch removal per se,
     661plus a bit of the switch case. This comprises propagating the memory extension
     662through  each statement (except switch), as well as various invariants that
     663are needed for the switch case (in particular, freshness hypotheses). The
     664details of the evaluation process for the source switch statement and its
     665target counterpart can be found in the file \textbf{switchRemoval.ma},
     666along more details on the transformation itself.
     667
     668Proving the correctness of the second point would require reasoning on the
     669semantics of \lstinline[language=C]'goto' statements. In the \textsf{Clight}
     670semantics, this is implemented as a function-wide lookup of the target label.
     671The invariant we would need is the fact that a global label lookup on a freshly
     672created goto is equivalent to a local lookup. This would in turn require the
     673propagation of some freshness hypotheses on labels. For reasons expressed above,
     674we decided to omit this part of the correctness proof.
     675
     676\paragraph{Clight to Cminor}
     677
     678This pass is the last one operating on the Clight intermediate language.
     679Its input is a full \textsf{Clight} program, and its output is a \textsf{Cminor}
     680program. Note that we do not use an equivalent of the C\#minor language: we
     681translate directly to Cminor. This presents the advantage of not requiring the
     682special loop constructs, nor the explicit block structure. Another salient
     683point of our approach is that a significant part of the properties needed for
     684the simulation proof were directly encoded in dependently typed translation
     685functions. This concerns more precisely freshness conditions and well-typedness
     686conditions. The main effects of the transformation from \textsf{Clight} to
     687\textsf{Cminor} are listed below.
     688
     689\begin{itemize}
     690\item Variables are classified as being either globals, stack-allocated
     691  locals or potentially register-allocated locals. The value of register-allocated
     692  local variables is moved out of the modelled memory and stored in a
     693  dedicated environment.
     694\item In Clight, each local variable has a dedicated memory block, whereas
     695  stack-allocated locals are bundled together on a function-by-function basis.
     696\item Loops are converted to jumps.
     697\end{itemize}
     698
     699The first two points require memory injections which are more flexible that those
     700needed in the switch removal case. In the remainder of this section, we briefly
     701discuss our implementation of memory injections, and then the simulation proof.
     702
     703\subparagraph{Memory injections}
     704
     705Our memory injections are modelled after the work of Blazy \& Leroy.
     706However, the corresponding paper is based on the first version of the
     707Compcert memory model, whereas we use a much more concrete model, allowing byte-level
     708manipulations (as in the later version of Compcert's memory model). We proved
     709roughly 80 \% of the required lemmas. Some difficulties encountered were notably
     710due to some too relaxed conditions on pointer validity (problem fixed during development).
     711Some more conditions had to be added to take care of possible overflows when converting
     712from \textbf{Z} block bounds to $16$ bit pointer offsets (in pratice, these overflows
     713only occur in edge cases that are easily ruled out -- but this fact is not visible
     714in memory injections). Concretely, some of the lemmas on the preservation of simulation of
     715loads after writes were axiomatised, for lack of time.
     716
     717\subparagraph{Simulation proof}
     718
     719The correction proof for this transformation was not terminated. We proved the
     720simulation result for expressions and for some subset of the critical statement cases.
     721Notably lacking are the function entry and exit, where the memory injection is
     722properly set up. As can be guessed, a significant amount of work has to be performed
     723to show the conservation of all invariants at each simulation step.
     724
     725\todo{list cases, explain while loop, explain labeling problem}
     726
    581727\section{Checking cost labelling properties}
    582728
Note: See TracChangeset for help on using the changeset viewer.