\select@language {english}
\contentsline {paragraph}{Abstract}{2}{section*.1}
\contentsline {section}{\numberline {1}Introduction}{5}{section.1}
\contentsline {subsection}{\numberline {1.1}Meaning of cost annotations}{5}{subsection.1.1}
\contentsline {subsection}{\numberline {1.2}Soundness and precision of cost annotations}{6}{subsection.1.2}
\contentsline {subsection}{\numberline {1.3}Compositionality}{6}{subsection.1.3}
\contentsline {subsection}{\numberline {1.4}Direct approach to cost annotations}{6}{subsection.1.4}
\contentsline {subsection}{\numberline {1.5}Labelling approach to cost annotations}{7}{subsection.1.5}
\contentsline {subsection}{\numberline {1.6}A toy compiler}{8}{subsection.1.6}
\contentsline {subsection}{\numberline {1.7}A C compiler}{8}{subsection.1.7}
\contentsline {subsection}{\numberline {1.8}Organisation}{9}{subsection.1.8}
\contentsline {section}{\numberline {2}A toy compiler}{9}{section.2}
\contentsline {subsection}{\numberline {2.1}{\sf Imp}: language and semantics}{9}{subsection.2.1}
\contentsline {subsection}{\numberline {2.2}Big-step semantics}{9}{subsection.2.2}
\contentsline {subsection}{\numberline {2.3}Small-step semantics}{10}{subsection.2.3}
\contentsline {subsection}{\numberline {2.4}{\sf Vm}: language and semantics}{11}{subsection.2.4}
\contentsline {subsection}{\numberline {2.5}Compilation from ${\sf Imp}$ to ${\sf Vm}$}{12}{subsection.2.5}
\contentsline {subsection}{\numberline {2.6}Soundness of compilation for the big-step semantics}{12}{subsection.2.6}
\contentsline {subsection}{\numberline {2.7}Soundness of compilation for the small-step semantics}{12}{subsection.2.7}
\contentsline {subsection}{\numberline {2.8}Compiled code is well-formed}{13}{subsection.2.8}
\contentsline {subsection}{\numberline {2.9}${\sf Mips}$: language and semantics}{13}{subsection.2.9}
\contentsline {subsection}{\numberline {2.10}Compilation from ${\sf Vm}$ to ${\sf Mips}$}{14}{subsection.2.10}
\contentsline {section}{\numberline {3}Direct approach for the toy compiler}{14}{section.3}
\contentsline {subsection}{\numberline {3.1}${\sf Mips}$ and ${\sf Vm}$ cost annotations}{15}{subsection.3.1}
\contentsline {subsection}{\numberline {3.2}${\sf Imp}$ cost annotation}{16}{subsection.3.2}
\contentsline {subsection}{\numberline {3.3}Composition}{17}{subsection.3.3}
\contentsline {subsection}{\numberline {3.4}${\sf Coq}$ development}{18}{subsection.3.4}
\contentsline {subsection}{\numberline {3.5}Limitations of the direct approach}{18}{subsection.3.5}
\contentsline {section}{\numberline {4}Labelling approach for the toy compiler}{18}{section.4}
\contentsline {subsection}{\numberline {4.1}Labelled ${\sf Imp}$}{18}{subsection.4.1}
\contentsline {subsection}{\numberline {4.2}Labelled ${\sf Vm}$}{19}{subsection.4.2}
\contentsline {subsection}{\numberline {4.3}Labelled ${\sf Mips}$}{20}{subsection.4.3}
\contentsline {subsection}{\numberline {4.4}Labellings and instrumentations}{20}{subsection.4.4}
\contentsline {subsection}{\numberline {4.5}Sound and precise labellings}{21}{subsection.4.5}
\contentsline {section}{\numberline {5}A ${\sf C}$ compiler}{23}{section.5}
\contentsline {subsection}{\numberline {5.1}${\sf Clight}$}{23}{subsection.5.1}
\contentsline {subsection}{\numberline {5.2}${\sf Cminor}$}{23}{subsection.5.2}
\contentsline {paragraph}{Translation of ${\sf Clight}$ to ${\sf Cminor}$.}{23}{section*.3}
\contentsline {subsection}{\numberline {5.3}${\sf RTLAbs}$}{23}{subsection.5.3}
\contentsline {paragraph}{Syntax.}{26}{section*.4}
\contentsline {paragraph}{Translation of ${\sf Cminor}$ to ${\sf RTLAbs}$.}{26}{section*.5}
\contentsline {subsection}{\numberline {5.4}${\sf RTL}$}{27}{subsection.5.4}
\contentsline {paragraph}{Syntax.}{27}{section*.6}
\contentsline {paragraph}{Translation of ${\sf RTLAbs}$ to ${\sf RTL}$.}{27}{section*.7}
\contentsline {subsection}{\numberline {5.5}${\sf ERTL}$}{27}{subsection.5.5}
\contentsline {paragraph}{Syntax.}{28}{section*.8}
\contentsline {paragraph}{Translation of ${\sf RTL}$ to ${\sf ERTL}$.}{28}{section*.9}
\contentsline {paragraph}{Optimizations.}{28}{section*.10}
\contentsline {subsection}{\numberline {5.6}${\sf LTL}$}{29}{subsection.5.6}
\contentsline {paragraph}{Syntax.}{29}{section*.11}
\contentsline {paragraph}{Translation of ${\sf ERTL}$ to ${\sf LTL}$.}{29}{section*.12}
\contentsline {paragraph}{Optimizations.}{29}{section*.13}
\contentsline {subsection}{\numberline {5.7}${\sf LIN}$}{30}{subsection.5.7}
\contentsline {paragraph}{Syntax.}{30}{section*.14}
\contentsline {paragraph}{Translation of ${\sf LTL}$ to ${\sf LIN}$.}{30}{section*.15}
\contentsline {subsection}{\numberline {5.8}${\sf Mips}$}{30}{subsection.5.8}
\contentsline {paragraph}{Translation of ${\sf LIN}$ to ${\sf Mips}$.}{30}{section*.16}
\contentsline {section}{\numberline {6}Labelling approach for the ${\sf C}$ compiler}{31}{section.6}
\contentsline {subsection}{\numberline {6.1}Labelled ${\sf Clight}$ and labelled ${\sf Cminor}$}{31}{subsection.6.1}
\contentsline {subsection}{\numberline {6.2}Labels in ${\sf RTLAbs}$ and the back-end languages}{32}{subsection.6.2}
\contentsline {subsection}{\numberline {6.3}Labelling of the source language}{32}{subsection.6.3}
\contentsline {subsubsection}{\numberline {6.3.1}Sequential instructions}{32}{subsubsection.6.3.1}
\contentsline {subsubsection}{\numberline {6.3.2}Ternary expressions}{32}{subsubsection.6.3.2}
\contentsline {paragraph}{Related cases.}{33}{section*.17}
\contentsline {subsubsection}{\numberline {6.3.3}Conditionals}{33}{subsubsection.6.3.3}
\contentsline {subsubsection}{\numberline {6.3.4}Loops}{33}{subsubsection.6.3.4}
\contentsline {subsubsection}{\numberline {6.3.5}Program Labels and Gotos}{34}{subsubsection.6.3.5}
\contentsline {subsubsection}{\numberline {6.3.6}Function calls}{34}{subsubsection.6.3.6}
\contentsline {subsection}{\numberline {6.4}Verifications on the object code}{35}{subsection.6.4}
\contentsline {subsection}{\numberline {6.5}Building the cost annotation}{35}{subsection.6.5}
\contentsline {subsection}{\numberline {6.6}Testing}{36}{subsection.6.6}
\contentsline {section}{\numberline {7}Conclusion and future work}{36}{section.7}
\contentsline {section}{\numberline {A}Assessment of the deliverable within the $CerCo$ project}{38}{appendix.A}
\contentsline {section}{\numberline {B}Proofs}{40}{appendix.B}
\contentsline {subsection}{\numberline {B.1}Notation}{40}{subsection.B.1}
\contentsline {subsection}{\numberline {B.2}Proof of proposition \ref {soundness-small-step}}{40}{subsection.B.2}
\contentsline {subsection}{\numberline {B.3}Proof of proposition \ref {labelled-simulation-vm-mips}}{41}{subsection.B.3}
\contentsline {paragraph}{The memory realisation.}{41}{section*.19}
\contentsline {paragraph}{The inequation.}{41}{section*.20}
\contentsline {subsection}{\numberline {B.4}Proof of proposition \ref {annot-composition}}{41}{subsection.B.4}
\contentsline {subsection}{\numberline {B.5}Proof of proposition \ref {labelled-sim-imp-vm}}{42}{subsection.B.5}
\contentsline {subsection}{\numberline {B.6}Proof of proposition \ref {sim-vm-mips-prop}}{42}{subsection.B.6}
\contentsline {subsection}{\numberline {B.7}Proof of proposition \ref {lab-instr-erasure-imp}}{42}{subsection.B.7}
\contentsline {subsection}{\numberline {B.8}Proof of proposition \ref {global-commutation-prop}}{42}{subsection.B.8}
\contentsline {subsection}{\numberline {B.9}Proof of proposition \ref {instrument-to-label-prop}}{42}{subsection.B.9}
\contentsline {subsection}{\numberline {B.10}Proof of proposition \ref {sound-label-prop}}{43}{subsection.B.10}
\contentsline {subsection}{\numberline {B.11}Proof of proposition \ref {precise-label-prop}}{43}{subsection.B.11}
\contentsline {subsection}{\numberline {B.12}Proof of proposition \ref {lab-sound}}{43}{subsection.B.12}
\contentsline {subsection}{\numberline {B.13}Proof of proposition \ref {ann-correct}}{43}{subsection.B.13}