cil-template /

Filename Size Date modified Message
CMakeModules
bin
ciltut-include
ciltut-lib
lib
src
test
453 B
Switching over to CMake for the whole build. This commit may fail to build
3.0 KB
1.5 KB
Updated README and docs to reflect cmake build
6.3 KB
Updated scripts for Cilly change. Fixed README.
328 B
Fix for ciltutcc script, etc.
728.0 KB
Updated README and docs to reflect cmake build
This is a simple tutorial about how to use the CIL compiler frontend to do
static and dynamic program analysis.

Author: Zach Anderson (zanderso@acm.org)

1. Intro
2. Building and Installing
3. Files
4. Bugs and Feedback
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
front-end 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
  - There is a problem building against versions 1.7.{1,2}. 
    If you encounter errors while linking, try the tip of
    the CIL git repo, or an earlier version.
. ocamlgraph
  - Ubuntu package: libocamlgraph-ocaml-dev
. 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 -DBUILD_TUT11=true to cmake to include this example

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 -DBUILD_TUT15=true to cmake to include this example

Then, to obtain and build:

$ hg clone https://bitbucket.org/zanderso/cil-template
$ mkdir build
$ cd build
$ cmake [-DBUILD_TUT11=true] [-DBUILD_TUT15=true] ..
$ make
$ sudo make install

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

$ ciltutcc -o tut1 --enable-tut1 test/tut1.c
test/tut1.c:9: Deleted assignment: #line 9 "test/tut1.c"
deleted = 0;
$ ./tut1
r = 37

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

As above

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


3. Files:
---------

CMakeLists.txt - Add additional filenames to CILTUT_SRC on line 48 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. The files in src/tut*.c
go along with the corresponding .ml files. ciltut_libc.c has utility functions.
To add new code to the runtime, add file names to the CMakeLists.txt file under
the src/ directory in the obvious place.

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.


4. Bugs, and Feedback:
--------------

Please use the issue tracker on bitbucket to report bugs, make suggestions,
give feedback, etc..


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, January 2013. 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 = Jan,
  year = 2013,
  note = {\url{http://www.inf.ethz.ch/~azachary/}},
}