# Changeset 1741 for Deliverables

Ignore:
Timestamp:
Feb 24, 2012, 3:24:45 PM (9 years ago)
Message:

...

File:
1 edited

### Legend:

Unmodified
 r1740 \usepackage{skull} \usepackage{stmaryrd} \usepackage{wasysym} \lstdefinelanguage{matita-ocaml} { meeting we intend to move this transformation to the back-end}\\ \> $\downarrow$ \> cost labelling\\ \> $\downarrow$ \> loop optimizations\footnote{To be ported from the untrusted compiler and certified only in case of early completion of the certification of the other passes.} (an endo-transformation)\\ \> $\downarrow$ \> loop optimizations\footnote{\label{lab:opt2}To be ported from the untrusted compiler and certified only in case of early completion of the certification of the other passes.} (an endo-transformation)\\ \> $\downarrow$ \> partial redundancy elimination$^{\mbox{\scriptsize \ref{lab:opt2}}}$ (an endo-transformation)\\ \> $\downarrow$ \> stack variable allocation and control structure simplification\\ \> $\downarrow$ \> transform to RTL graph\\ \textsf{RTLabs}\\ \> $\downarrow$ \> start of target specific back-end\\ \>\quad \vdots \> $\downarrow$ \> \\ \>\,\vdots \end{tabbing} \end{minipage} \begin{minipage}{.8\linewidth} \begin{tabbing} \quad \= $\downarrow$ \quad \= \kill \quad \=\,\vdots\= \\ \> $\downarrow$ \>\\ \> $\downarrow$ \quad \= \kill \textsf{RTLabs}\\ \> $\downarrow$ \> copy propagation\footnote{\label{lab:opt}To be ported from the untrusted compiler and certified only in case of early completion of the certification of the other passes.} (an endo-transformation) \\ \> $\downarrow$ \> constant propagation$^{\mbox{\scriptsize \ref{lab:opt}}}$ (an endo-transformation) \\ \> $\downarrow$ \> calling convention made explicit \\ \> $\downarrow$ \> stack frame generation \\ \> $\downarrow$ \> layout of activation records \\ \textsf{ERTL}\\ \> $\downarrow$ \> register allocation and spilling\\ \textsf{ASM}\\ \> $\downarrow$ \> pseudoinstruction expansion\\ \textsf{Machine code}\\ \textsf{MCS-51 machine code}\\ \end{tabbing} \end{minipage} The ASM to MCS-51 machine code translation step, and the required statements of correctness, are found in an unpublished manuscript attached to this document. \section{Estimated effort} Based on the rough analysis performed so far we can now estimate the total effort for the certification of the compiler. We obtain the estimation by combining, for each pass: 1) the number of lines of code to be certified; 2) the ratio number of lines of proof on number of lines of code from CompCert project~\cite{compcert} for the CompCert pass that is closer to ours; 3) an estimation of the complexity of the pass according to the analysis above. \begin{tabular}{lrll} Pass origin & Code lines & CompCert ratio & Estimated effort \\ Clight & \\ Cminor & \\ RTLabs & 1252 & 1.17 \permil & 1.5 \\ RTL    &  469 & 2.90 \permil & 1.4 \\ ERTL   &  789 & 2.79 \permil & 2.2 \\ LTL    &      & \\ LIN    &  354 & 7.34 \permil & 2.6 \\ ASM    &      & \\ \end{tabular} \end{document}