README

   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.12)
  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". If PREFIX is not provided, the default directory used will
  60   be "/usr/local/bin/".
  61
  62  Usage
  63 -------
  64
  65 Usage: acc.native [options] file...
  66   -s      Choose the source language between:
  67           Clight, Cminor
  68           [default is C]
  69   -l      Choose the target language between:
  70           Clight, Cminor, RTLabs, RTL, ERTL, LTL, LIN, ASM
  71           [default is ASM]
  72   -a      Add cost annotations on the source code.
  73   -i      Interpret the compiled code.
  74   -d      Debugging mode.
  75   -dev    Playground for developers.
  76   -help   Display this list of options
  77   --help  Display this list of options
  78
  79  Test-suite
  80 ------------
  81
  82   You can optionnally check that compilation went well by confronting
  83   the freshly built compiler to our test-suite. At the root of the
  84   source tree, use:
  85
  86   % make check
  87
  88  mcu8051ide
  89 ------------
  90
  91   The object code can be simulated using the mcu8051ide[3] emulator. The code
  92   makes use of an external memory and that the usage of such memory is not the
  93   default option in mcu8051ide. In order to enable this option, click on the
  94   'Project' menu, and then on 'Edit project'. There is a box to enable 'External
  95   RAM (XDATA)' and a scrolling bar to specify its size (we suggest to use the
  96   maximum possible). Also, since the produced code might be too big for standard
  97   memory, it is recommended to enable 'External ROM/FLASH (XCODE)' to its
  98   maximum size.
  99
 100 [3] http://mcu8051ide.sourceforge.net/
 101
 102  Known bugs
 103 ------------
 104
 105   - shift operations between [int] and [unsigned int]
 106   - accessing an array initialized by a string