cil-template / README

This is a simple tutorial about how to use the CIL compiler frontend to do
static and dynamic program analysis.

Author: Zach Anderson (zachary.anderson@inf.ethz.ch)

1. Intro
2. Building and Installing
3. Documentation
4. Files
5. Citation

1. Intro:
------

CIL is a frontend for C compilers. It takes C code as input, which can then be
analyzed or instrumented, and then spits out C code, which can be passed to
your favorite C compiler. This process can be automated such that your CIL-based
frontend can be made to look like gcc, or whatever, and used directly in your
build process. This tutorial creates such a frontend, and demonstrates, in
tutorial form, some nifty things that might be done with it.

2a. Building and Installing (Ubuntu):
------------------------

There are a few dependencies:
. Everything you need to build C programs
. OCaml
. cmake
  - Ubuntu packages: cmake cmake-data
. CIL
  - Build and install from http://cil.sf.net
. Please let me know if I've forgotten anything

Dependencies only for the theorem proving example (tut11.ml):
. why3
. theorem provers (e.g. alt-ergo)
. pass --disable-tut11 to the configure script to disable tut11

Dependencies only for the automated test generation example (tut15.ml):
. Yices SMT solver (http://yices.csl.sri.com/)
. ocamlyices (https://github.com/polazarus/ocamlyices)
. pass --disable-tut15 to the configure script to disable tut15

After obtaining the code, enter the directory and do the following:

$ ./configure [--disable-tut11] [--disable-tut15]
$ make
$ sudo make install

Then, enter the /test directory and build the program like so:

$ ciltutcc -o test1 test1.c
$ ./test1

The generated ciltutcc takes all of the usual gcc arguments, in addition to the
following:

--trace       - shows all of the commands run
--save-temps  - saves all of the intermediate files
--enable-tutN - enables the pass defined by tutN.ml

And others that you can define in src/ciltutoptions.ml

If you do:

$ ciltutcc --save-temps -o test1 test1.c

A file called test1.cil.c will be created showing the source file created by
the frontend before it is passed on to gcc.

  [Ocamlyices installation]

$ git clone git://github.com/polazarus/ocamlyices.git
$ cd ocamlyices
(Download yices for your platform from http://yices.csl.sri.com/download.shtml
 into the ocamlyices directory. If the version statically linked with gmp
 doesn't work, then try the dynamically linked version.)
$ sudo ./install-yices.sh [the tar.gz file you dl'd]
$ autoconf [if needed]
$ ./configure
$ make
$ sudo make install

  [Alt-Ergo installation]

$ wget http://alt-ergo.lri.fr/http/alt-ergo-0.94.tar.gz
$ tar zxf alt-ergo-0.94.tar.gz
$ cd alt-ergo-0.94
$ autoconf [if needed]
$ ./configure
$ make
$ sudo make install

  [Why3 Installation]

$ git clone https://gforge.inria.fr/git/why3/why3.git
$ cd why3
$ autoconf [if needed]
$ ./configure
$ make
$ make byte
$ sudo make install
$ sudo make install-lib
$ why3config

2b. Building and Installing (Mac OS X)
-------------

This project should build and install on 10.8 using the MacPorts OCaml install.
I have not yet tried to get tutorials 11 and 15 running on it yet, though.

(It appears that there is some problem with linking the calls from C -> OCaml
in tut15.c, but Why3, Alt-Ergo, and Ocamlyices *should* build without
problems---I just haven't tried it yet.)

Anyway, here's what you'll need to do:
1. install XCode and be sure to install the "Unix" or "Command line" tools.
2. install MacPorts from http://www.macports.org
3. Do:

$ sudo port install ocaml ocaml-findlib lablgl lablgtk lablgtk2 mercurial cmake
                    ocaml-ocamlgraph

4. Install CIL:

$ git clone git://cil.git.sourceforge.net/gitroot/cil/cil
$ cd cil
$ ./configure; make; sudo make install

5. Build cil-tutorial

$ hg clone https://bitbucket.org/zanderso/cil-template
$ cd cil-template
$ ./configure --disable-tut11 --disable-tut15
$ make; sudo make install

6. Let me know if I've missed any steps =)

3. Documentation
-------------
(This is to remind me how to build the docs in my private repo, and so they
don't apply to the code under this tree. The documentation of which this section
speaks will shortly be available at http://www.inf.ethz.ch/~azachary.)


Dependencies for the documentation:
. LaTeX
. ocamlweb
  - Ubuntu package: ocamlweb
. highlight
	- Ubuntu packages: highlight highlight-common
	- Version 2.16 can be obtained for Mac OSX at:
	  http://www.hmug.org/pub/MacOS_X/BSD/Applications/Text/highlight
. Again, please let me know if I've forgotten anything

Assuming you have installed these, doing:

$ make

will build docs/ciltut.pdf along with everything else.

Pass --disable-docs to the configure script to disable document building.

4. Files:
---------

Makefile.in - Edit the "MODULES =" line to add additional OCaml modules. Other
parts of the Makefile can probably remain unchanged unless you need to do
something weird.

src/main.ml - Reads in a source file, calls into the various tutorial modules,
spits out the result. Hopefully it is obvious where to add code to call into
any new modules that you write.

src/ciltutoptions.ml - Defines command line options.

src/tut*.ml - Tutorial modules explaining how to use CIL.

ciltut-include/ciltut.h - Various function and macro definitions needed for
building ciltut-lib and the things in test/.

ciltut-lib/ - The runtime library, build with CMake. The files in src/tut*.c
go along with the corresponding .ml files. ciltut_libc.c has utility functions.

lib/Ciltut.pm - A perl script that sits in front of the actual compiler
frontend. It is used for massaging the command line a bit. For example, it makes
sure that the final result links against the code in ciltut-lib/.

test/tut*.c - Test programs for the various tutorial modules.

LICENSE - All the code in this project is licensed under a standard 3-clause
BSD license.

5. Citation:
------------

If you use cil-template as a starting point for your project, please make the
following citation:

Zachary Anderson. A CIL Tutorial: Using CIL for Language Extensions and Program
  Analysis, <the date given on the document>. <http://the.download.url>.

At the time this README file was written, this evaluates to:

Zachary Anderson. A CIL Tutorial: Using CIL for Language Extensions and Program
  Analysis, February 2012. http://www.inf.ethz.ch/~azachary.

Or in bibtex format:

@misc{ciltut,
  title = {A {CIL} Tutorial: Using {CIL} for Language Extensions and Program Analysis},
  author = {Zachary Anderson},
  month = Sep,
  year = 2012,
  note = {\url{http://www.inf.ethz.ch/~azachary/}},
}
Tip: Filter by directory path e.g. /media app.js to search for public/media/app.js.
Tip: Use camelCasing e.g. ProjME to search for ProjectModifiedEvent.java.
Tip: Filter by extension type e.g. /repo .js to search for all .js files in the /repo directory.
Tip: Separate your search with spaces e.g. /ssh pom.xml to search for src/ssh/pom.xml.
Tip: Use ↑ and ↓ arrow keys to navigate and return to view the file.
Tip: You can also navigate files with Ctrl+j (next) and Ctrl+k (previous) and view the file with Ctrl+o.
Tip: You can also navigate files with Alt+j (next) and Alt+k (previous) and view the file with Alt+o.