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