1 | \BOOKMARK [1][]{section.1}{Introduction}{} |
---|
2 | \BOOKMARK [2][]{subsection.1.1}{Meaning of cost annotations}{section.1} |
---|
3 | \BOOKMARK [2][]{subsection.1.2}{Soundness and precision of cost annotations}{section.1} |
---|
4 | \BOOKMARK [2][]{subsection.1.3}{Compositionality}{section.1} |
---|
5 | \BOOKMARK [2][]{subsection.1.4}{Direct approach to cost annotations}{section.1} |
---|
6 | \BOOKMARK [2][]{subsection.1.5}{Labelling approach to cost annotations}{section.1} |
---|
7 | \BOOKMARK [2][]{subsection.1.6}{A toy compiler}{section.1} |
---|
8 | \BOOKMARK [2][]{subsection.1.7}{A C compiler}{section.1} |
---|
9 | \BOOKMARK [2][]{subsection.1.8}{Organisation}{section.1} |
---|
10 | \BOOKMARK [1][]{section.2}{A toy compiler}{} |
---|
11 | \BOOKMARK [2][]{subsection.2.1}{Imp: language and semantics}{section.2} |
---|
12 | \BOOKMARK [2][]{subsection.2.2}{Big-step semantics}{section.2} |
---|
13 | \BOOKMARK [2][]{subsection.2.3}{Small-step semantics}{section.2} |
---|
14 | \BOOKMARK [2][]{subsection.2.4}{Vm: language and semantics}{section.2} |
---|
15 | \BOOKMARK [2][]{subsection.2.5}{Compilation from Imp to Vm}{section.2} |
---|
16 | \BOOKMARK [2][]{subsection.2.6}{Soundness of compilation for the big-step semantics}{section.2} |
---|
17 | \BOOKMARK [2][]{subsection.2.7}{Soundness of compilation for the small-step semantics}{section.2} |
---|
18 | \BOOKMARK [2][]{subsection.2.8}{Compiled code is well-formed}{section.2} |
---|
19 | \BOOKMARK [2][]{subsection.2.9}{Mips: language and semantics}{section.2} |
---|
20 | \BOOKMARK [2][]{subsection.2.10}{Compilation from Vm to Mips}{section.2} |
---|
21 | \BOOKMARK [1][]{section.3}{Direct approach for the toy compiler}{} |
---|
22 | \BOOKMARK [2][]{subsection.3.1}{Mips and Vm cost annotations}{section.3} |
---|
23 | \BOOKMARK [2][]{subsection.3.2}{Imp cost annotation}{section.3} |
---|
24 | \BOOKMARK [2][]{subsection.3.3}{Composition}{section.3} |
---|
25 | \BOOKMARK [2][]{subsection.3.4}{Coq development}{section.3} |
---|
26 | \BOOKMARK [2][]{subsection.3.5}{Limitations of the direct approach}{section.3} |
---|
27 | \BOOKMARK [1][]{section.4}{Labelling approach for the toy compiler}{} |
---|
28 | \BOOKMARK [2][]{subsection.4.1}{Labelled Imp}{section.4} |
---|
29 | \BOOKMARK [2][]{subsection.4.2}{Labelled Vm}{section.4} |
---|
30 | \BOOKMARK [2][]{subsection.4.3}{Labelled Mips}{section.4} |
---|
31 | \BOOKMARK [2][]{subsection.4.4}{Labellings and instrumentations}{section.4} |
---|
32 | \BOOKMARK [2][]{subsection.4.5}{Sound and precise labellings}{section.4} |
---|
33 | \BOOKMARK [1][]{section.5}{A C compiler}{} |
---|
34 | \BOOKMARK [2][]{subsection.5.1}{Clight}{section.5} |
---|
35 | \BOOKMARK [2][]{subsection.5.2}{Cminor}{section.5} |
---|
36 | \BOOKMARK [2][]{subsection.5.3}{RTLAbs}{section.5} |
---|
37 | \BOOKMARK [2][]{subsection.5.4}{RTL}{section.5} |
---|
38 | \BOOKMARK [2][]{subsection.5.5}{ERTL}{section.5} |
---|
39 | \BOOKMARK [2][]{subsection.5.6}{LTL}{section.5} |
---|
40 | \BOOKMARK [2][]{subsection.5.7}{LIN}{section.5} |
---|
41 | \BOOKMARK [2][]{subsection.5.8}{Mips}{section.5} |
---|
42 | \BOOKMARK [1][]{section.6}{Labelling approach for the C compiler}{} |
---|
43 | \BOOKMARK [2][]{subsection.6.1}{Labelled Clight and labelled Cminor}{section.6} |
---|
44 | \BOOKMARK [2][]{subsection.6.2}{Labels in RTLAbs and the back-end languages}{section.6} |
---|
45 | \BOOKMARK [2][]{subsection.6.3}{Labelling of the source language}{section.6} |
---|
46 | \BOOKMARK [3][]{subsubsection.6.3.1}{Sequential instructions}{subsection.6.3} |
---|
47 | \BOOKMARK [3][]{subsubsection.6.3.2}{Ternary expressions}{subsection.6.3} |
---|
48 | \BOOKMARK [3][]{subsubsection.6.3.3}{Conditionals}{subsection.6.3} |
---|
49 | \BOOKMARK [3][]{subsubsection.6.3.4}{Loops}{subsection.6.3} |
---|
50 | \BOOKMARK [3][]{subsubsection.6.3.5}{Program Labels and Gotos}{subsection.6.3} |
---|
51 | \BOOKMARK [3][]{subsubsection.6.3.6}{Function calls}{subsection.6.3} |
---|
52 | \BOOKMARK [2][]{subsection.6.4}{Verifications on the object code}{section.6} |
---|
53 | \BOOKMARK [2][]{subsection.6.5}{Building the cost annotation}{section.6} |
---|
54 | \BOOKMARK [2][]{subsection.6.6}{Testing}{section.6} |
---|
55 | \BOOKMARK [1][]{section.7}{Conclusion and future work}{} |
---|
56 | \BOOKMARK [1][]{appendix.A}{Assessment of the deliverable within the CerCo project}{} |
---|
57 | \BOOKMARK [1][]{appendix.B}{Proofs}{} |
---|
58 | \BOOKMARK [2][]{subsection.B.1}{Notation}{appendix.B} |
---|
59 | \BOOKMARK [2][]{subsection.B.2}{Proof of proposition 4}{appendix.B} |
---|
60 | \BOOKMARK [2][]{subsection.B.3}{Proof of proposition 8}{appendix.B} |
---|
61 | \BOOKMARK [2][]{subsection.B.4}{Proof of proposition 10}{appendix.B} |
---|
62 | \BOOKMARK [2][]{subsection.B.5}{Proof of proposition 11}{appendix.B} |
---|
63 | \BOOKMARK [2][]{subsection.B.6}{Proof of proposition 13}{appendix.B} |
---|
64 | \BOOKMARK [2][]{subsection.B.7}{Proof of proposition 14}{appendix.B} |
---|
65 | \BOOKMARK [2][]{subsection.B.8}{Proof of proposition 16}{appendix.B} |
---|
66 | \BOOKMARK [2][]{subsection.B.9}{Proof of proposition 17}{appendix.B} |
---|
67 | \BOOKMARK [2][]{subsection.B.10}{Proof of proposition 20}{appendix.B} |
---|
68 | \BOOKMARK [2][]{subsection.B.11}{Proof of proposition 22}{appendix.B} |
---|
69 | \BOOKMARK [2][]{subsection.B.12}{Proof of proposition 23}{appendix.B} |
---|
70 | \BOOKMARK [2][]{subsection.B.13}{Proof of proposition 25}{appendix.B} |
---|