\select@language {english}
\contentsline {paragraph}{Abstract}{2}{section*.1}
\contentsline {section}{\numberline {1}Introduction}{5}{section.1}
\contentsline {paragraph}{Meaning of cost annotations}{5}{section*.3}
\contentsline {paragraph}{Soundness and precision of cost annotations}{6}{section*.4}
\contentsline {paragraph}{Compositionality}{6}{section*.5}
\contentsline {paragraph}{Labelling approach to cost annotations}{6}{section*.6}
\contentsline {paragraph}{A toy compiler}{7}{section*.7}
\contentsline {paragraph}{A C compiler}{8}{section*.8}
\contentsline {paragraph}{Organization}{8}{section*.9}
\contentsline {section}{\numberline {2}Labelling approach for the toy compiler}{8}{section.2}
\contentsline {subsection}{\numberline {2.1}Labelled ${\sf Imp}$}{9}{subsection.2.1}
\contentsline {subsection}{\numberline {2.2}Labelled ${\sf Vm}$}{9}{subsection.2.2}
\contentsline {subsection}{\numberline {2.3}Labelled ${\sf Mips}$}{10}{subsection.2.3}
\contentsline {subsection}{\numberline {2.4}Labellings and instrumentations}{10}{subsection.2.4}
\contentsline {subsection}{\numberline {2.5}Sound and precise labellings}{11}{subsection.2.5}
\contentsline {section}{\numberline {3}Labelling approach for the ${\sf C}$ compiler}{13}{section.3}
\contentsline {subsection}{\numberline {3.1}Labelled languages}{13}{subsection.3.1}
\contentsline {subsection}{\numberline {3.2}Labelling of the source language}{14}{subsection.3.2}
\contentsline {paragraph}{Sequential instructions}{14}{section*.10}
\contentsline {paragraph}{Ternary expressions and conditionals}{14}{section*.11}
\contentsline {paragraph}{Loops}{14}{section*.12}
\contentsline {paragraph}{Program Labels and Gotos}{14}{section*.13}
\contentsline {paragraph}{Function calls}{14}{section*.14}
\contentsline {subsection}{\numberline {3.3}Verifications on the object code}{15}{subsection.3.3}
\contentsline {subsection}{\numberline {3.4}Building the cost annotation}{16}{subsection.3.4}
\contentsline {subsection}{\numberline {3.5}Testing}{16}{subsection.3.5}
\contentsline {section}{\numberline {4}Conclusion and future work}{16}{section.4}
\contentsline {section}{\numberline {A}A toy compiler}{18}{appendix.A}
\contentsline {subsection}{\numberline {A.1}{\sf Imp}: language and semantics}{18}{subsection.A.1}
\contentsline {subsection}{\numberline {A.2}{\sf Vm}: language and semantics}{18}{subsection.A.2}
\contentsline {subsection}{\numberline {A.3}Compilation from ${\sf Imp}$ to ${\sf Vm}$}{19}{subsection.A.3}
\contentsline {subsection}{\numberline {A.4}${\sf Mips}$: language and semantics}{20}{subsection.A.4}
\contentsline {subsection}{\numberline {A.5}Compilation from ${\sf Vm}$ to ${\sf Mips}$}{21}{subsection.A.5}
\contentsline {section}{\numberline {B}Proofs}{23}{appendix.B}
\contentsline {subsection}{\numberline {B.1}Notation}{23}{subsection.B.1}
\contentsline {subsection}{\numberline {B.2}Proof of proposition \ref {labelled-sim-imp-vm}}{23}{subsection.B.2}
\contentsline {subsection}{\numberline {B.3}Proof of proposition \ref {sim-vm-mips-prop}}{23}{subsection.B.3}
\contentsline {subsection}{\numberline {B.4}Proof of proposition \ref {lab-instr-erasure-imp}}{23}{subsection.B.4}
\contentsline {subsection}{\numberline {B.5}Proof of proposition \ref {global-commutation-prop}}{24}{subsection.B.5}
\contentsline {subsection}{\numberline {B.6}Proof of proposition \ref {instrument-to-label-prop}}{24}{subsection.B.6}
\contentsline {subsection}{\numberline {B.7}Proof of proposition \ref {sound-label-prop}}{24}{subsection.B.7}
\contentsline {subsection}{\numberline {B.8}Proof of proposition \ref {precise-label-prop}}{24}{subsection.B.8}
\contentsline {subsection}{\numberline {B.9}Proof of proposition \ref {lab-sound}}{25}{subsection.B.9}
\contentsline {subsection}{\numberline {B.10}Proof of proposition \ref {ann-correct}}{25}{subsection.B.10}
\contentsline {subsection}{\numberline {B.11}Proof of proposition \ref {soundness-small-step}}{25}{subsection.B.11}
\contentsline {section}{\numberline {C}A ${\sf C}$ compiler}{27}{appendix.C}
\contentsline {subsection}{\numberline {C.1}${\sf Clight}$}{27}{subsection.C.1}
\contentsline {subsection}{\numberline {C.2}${\sf Cminor}$}{27}{subsection.C.2}
\contentsline {paragraph}{Translation of ${\sf Clight}$ to ${\sf Cminor}$}{27}{section*.16}
\contentsline {subsection}{\numberline {C.3}${\sf RTLAbs}$}{27}{subsection.C.3}
\contentsline {paragraph}{Syntax.}{30}{section*.17}
\contentsline {paragraph}{Translation of ${\sf Cminor}$ to ${\sf RTLAbs}$.}{30}{section*.18}
\contentsline {subsection}{\numberline {C.4}${\sf RTL}$}{31}{subsection.C.4}
\contentsline {paragraph}{Syntax.}{31}{section*.19}
\contentsline {paragraph}{Translation of ${\sf RTLAbs}$ to ${\sf RTL}$.}{31}{section*.20}
\contentsline {subsection}{\numberline {C.5}${\sf ERTL}$}{31}{subsection.C.5}
\contentsline {paragraph}{Syntax.}{32}{section*.21}
\contentsline {paragraph}{Translation of ${\sf RTL}$ to ${\sf ERTL}$.}{32}{section*.22}
\contentsline {paragraph}{Optimizations.}{33}{section*.23}
\contentsline {subsection}{\numberline {C.6}${\sf LTL}$}{33}{subsection.C.6}
\contentsline {paragraph}{Syntax.}{33}{section*.24}
\contentsline {paragraph}{Translation of ${\sf ERTL}$ to ${\sf LTL}$.}{33}{section*.25}
\contentsline {paragraph}{Optimizations.}{33}{section*.26}
\contentsline {subsection}{\numberline {C.7}${\sf LIN}$}{34}{subsection.C.7}
\contentsline {paragraph}{Syntax.}{34}{section*.27}
\contentsline {paragraph}{Translation of ${\sf LTL}$ to ${\sf LIN}$.}{34}{section*.28}
\contentsline {subsection}{\numberline {C.8}Assembly}{34}{subsection.C.8}
\contentsline {paragraph}{Translation of ${\sf LIN}$ to ${\sf Mips}$.}{34}{section*.29}
\contentsline {subsection}{\numberline {C.9}Benchmarks}{36}{subsection.C.9}
\contentsline {section}{\numberline {D}A direct approach}{37}{appendix.D}
\contentsline {subsection}{\numberline {D.1}${\sf Mips}$ and ${\sf Vm}$ cost annotations}{37}{subsection.D.1}
\contentsline {subsection}{\numberline {D.2}${\sf Imp}$ cost annotation}{38}{subsection.D.2}
\contentsline {subsection}{\numberline {D.3}Composition}{40}{subsection.D.3}
\contentsline {subsection}{\numberline {D.4}${\sf Coq}$ development}{40}{subsection.D.4}
\contentsline {subsection}{\numberline {D.5}Limitations of the direct approach}{40}{subsection.D.5}
\contentsline {section}{\numberline {E}Related approaches}{41}{appendix.E}
\contentsline {section}{\numberline {F}Assessment of the deliverable within the $CerCo$ project, with hindsight}{42}{appendix.F}