1 | Description |
---|
2 | ------------- |
---|
3 | |
---|
4 | This is an experimental annotating C compiler that was built upon |
---|
5 | the CIL parser[1], Xavier Leroy's translation from C to Clight, and |
---|
6 | an existing back-end compiler for a register transfer language to a |
---|
7 | subset of the MIPS assembly language[2]. |
---|
8 | |
---|
9 | We wrote 3 compiler passes: one from Clight to Cminor, another from |
---|
10 | Cminor to an abstract register transfer language (RTLabs), and a |
---|
11 | last one from RTLabs to an RTL that uses MIPS instructions. We |
---|
12 | extended interpreters for the intermediate languages to output a |
---|
13 | list of labels which denote key control points of the program that |
---|
14 | have been crossed during the interpretation. These labels are the |
---|
15 | places where the code can be instrumented to obtain a precise cost |
---|
16 | annotation. Thus, in that experiment, the annotation function is the |
---|
17 | composition of a labelling function followed by an instrumentation |
---|
18 | function. |
---|
19 | |
---|
20 | The architecture of the compiler is described in full details in the |
---|
21 | documentation of this development, which can be found in this source |
---|
22 | tree at doc/html/index.html. |
---|
23 | |
---|
24 | [1] http://cil-parser.sourceforge.net/ |
---|
25 | [2] http://www.enseignement.polytechnique.fr/informatique/INF564/petit.tar.gz |
---|
26 | |
---|
27 | Licence |
---|
28 | --------- |
---|
29 | |
---|
30 | This piece of code must not be distributed. It is addressed to the |
---|
31 | CerCo partners only. |
---|
32 | |
---|
33 | Requirements |
---|
34 | -------------- |
---|
35 | |
---|
36 | - ocaml (>= 3.11) |
---|
37 | - menhir (>= 20090505) |
---|
38 | - CIL (included in the distribution) |
---|
39 | - GNU Make (>= 3.8) |
---|
40 | - gcc |
---|
41 | |
---|
42 | Compilation |
---|
43 | ------------- |
---|
44 | |
---|
45 | You can compile this compiler using the following command: |
---|
46 | |
---|
47 | % make |
---|
48 | |
---|
49 | (assuming that you are located at the root of the source tree) |
---|
50 | |
---|
51 | Installation |
---|
52 | -------------- |
---|
53 | |
---|
54 | To install the compiler in your favorite system hierarchy, use: |
---|
55 | |
---|
56 | % PREFIX=your-directory make install |
---|
57 | |
---|
58 | The executable "acc" will be installed in the subdirectory "bin/" of |
---|
59 | "your-directory". |
---|
60 | |
---|
61 | Usage |
---|
62 | ------- |
---|
63 | |
---|
64 | Usage: acc.native [options] file... |
---|
65 | -s Choose the source language between: |
---|
66 | Clight, Cminor |
---|
67 | [default is C] |
---|
68 | -l Choose the target language between: |
---|
69 | Clight, Cminor, RTLabs, RTL, ERTL, LTL, LIN, ASM |
---|
70 | [default is ASM] |
---|
71 | -a Add cost annotations on the source code. |
---|
72 | -i Interpret the compiled code. |
---|
73 | -d Debugging mode. |
---|
74 | -dev Playground for developers. |
---|
75 | -help Display this list of options |
---|
76 | --help Display this list of options |
---|
77 | |
---|
78 | Test-suite |
---|
79 | ------------ |
---|
80 | |
---|
81 | You can optionnally check that compilation went well by confronting |
---|
82 | the freshly built compiler to our test-suite. At the root of the |
---|
83 | source tree, use: |
---|
84 | |
---|
85 | % make check |
---|
86 | |
---|
87 | mcu8051ide |
---|
88 | ------------ |
---|
89 | |
---|
90 | The object code can be simulated using the mcu8051ide[3] emulator. The code |
---|
91 | makes use of an external memory and that the usage of such memory is not the |
---|
92 | default option in mcu8051ide. In order to enable this option, click on the |
---|
93 | 'Project' menu, and then on 'Edit project'. There is a box to enable 'External |
---|
94 | RAM (XDATA)' and a scrolling bar to specify its size (we suggest to use the |
---|
95 | maximum possible). Also, since the produced code might be too big for standard |
---|
96 | memory, it is recommended to enable 'External ROM/FLASH (XCODE)' to its |
---|
97 | maximum size. |
---|
98 | |
---|
99 | [3] http://mcu8051ide.sourceforge.net/ |
---|