| [486] | 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 |
|---|
| [619] | 7 | subset of the MIPS assembly language[2]. |
|---|
| [486] | 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 |
|---|
| [619] | 11 | last one from RTLabs to an RTL that uses MIPS instructions. We |
|---|
| 12 | extended interpreters for the intermediate languages to output a |
|---|
| [486] | 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 | |
|---|
| [1099] | 36 | - ocaml (>= 3.12) |
|---|
| [486] | 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/ |
|---|
