+The CIL Driver +

From a5f03d96eee482cd84861fc8cefff9eb451c0cad Mon Sep 17 00:00:00 2001 From: xleroy Date: Sun, 29 Mar 2009 09:47:11 +0000 Subject: Cleaned up configure script. Distribution of CIL as an expanded source tree with changes applied (instead of original .tar.gz + patches to be applied at config time). git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1020 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- cil/doc/cil007.html | 279 ++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 279 insertions(+) create mode 100644 cil/doc/cil007.html (limited to 'cil/doc/cil007.html') diff --git a/cil/doc/cil007.html b/cil/doc/cil007.html new file mode 100644 index 00000000..7d6c0230 --- /dev/null +++ b/cil/doc/cil007.html @@ -0,0 +1,279 @@ + + + + + + + + + + + + + +The CIL Driver + + + +

+ +

7 The CIL Driver

+We have packaged CIL as an application cilly that contains certain +example modules, such as logwrites.ml (a module +that instruments code to print the addresses of memory locations being +written). Normally, you write another module like that, add command-line +options and an invocation of your module in src/main.ml. Once you compile +CIL you will obtain the file obj/cilly.asm.exe.
+
+We wrote a driver for this executable that makes it easy to invoke your +analysis on existing C code with very little manual intervention. This driver +is bin/cilly and is quite powerful. Note that the cilly script +is configured during installation with the path where CIL resides. This means +that you can move it to any place you want.
+
+A simple use of the driver is: +

+bin/cilly --save-temps -D HAPPY_MOOD -I myincludes hello.c -o hello
+

+--save-temps tells CIL to save the resulting output files in the +current directory. Otherwise, they'll be put in /tmp and deleted +automatically. Not that this is the only CIL-specific flag in the +list – the other flags use gcc's syntax.
+
+This performs the following actions: +

+preprocessing using the -D and -I arguments with the resulting + file left in hello.i, +
the invocation of the cilly.asm application which parses hello.i + converts it to CIL and the pretty-prints it to hello.cil.c +
another round of preprocessing with the result placed in hello.cil.i +
the true compilation with the result in hello.cil.o +
a linking phase with the result in hello +

+Note that cilly behaves like the gcc compiler. This makes it +easy to use it with existing Makefiles: +

+make CC="bin/cilly" LD="bin/cilly"
+

+ cilly can also behave as the Microsoft Visual C compiler, if the first + argument is --mode=MSVC: +

+bin/cilly --mode=MSVC /D HAPPY_MOOD /I myincludes hello.c /Fe hello.exe
+

+ (This in turn will pass a --MSVC flag to the underlying cilly.asm + process which will make it understand the Microsoft Visual C extensions)
+
+cilly can also behave as the archiver ar, if it is passed an +argument --mode=AR. Note that only the cr mode is supported (create a +new archive and replace all files in there). Therefore the previous version of +the archive is lost.
+
+Furthermore, cilly allows you to pass some arguments on to the +underlying cilly.asm process. As a general rule all arguments that start +with -- and that cilly itself does not process, are passed on. For +example, +

+bin/cilly --dologwrites -D HAPPY_MOOD -I myincludes hello.c -o hello.exe
+

+ will produce a file hello.cil.c that prints all the memory addresses +written by the application.
+
+The most powerful feature of cilly is that it can collect all the +sources in your project, merge them into one file and then apply CIL. This +makes it a breeze to do whole-program analysis and transformation. All you +have to do is to pass the --merge flag to cilly: +

+make CC="bin/cilly --save-temps --dologwrites --merge"
+

+ You can even leave some files untouched: +

+make CC="bin/cilly --save-temps --dologwrites --merge --leavealone=foo --leavealone=bar"
+

+ This will merge all the files except those with the basename foo and +bar. Those files will be compiled as usual and then linked in at the very +end.
+
+The sequence of actions performed by cilly depends on whether merging +is turned on or not: +

+If merging is off +
1. + For every file file.c to compile +
  1. + Preprocess the file with the given arguments to + produce file.i +
  2. Invoke cilly.asm to produce a file.cil.c +
  3. Preprocess to file.cil.i +
  4. Invoke the underlying compiler to produce file.cil.o +
  +
2. Link the resulting objects +
+
If merging is on +
1. + For every file file.c to compile +
  1. + Preprocess the file with the given arguments to + produce file.i +
  2. Save the preprocessed source as file.o +
  +
2. When linking executable hello.exe, look at every object + file that must be linked and see if it actually + contains preprocessed source. Pass all those files to a + special merging application (described in + Section 13) to produce hello.exe_comb.c +
3. Invoke cilly.asm to produce a hello.exe_comb.cil.c +
4. Preprocess to hello.exe_comb.cil.i +
5. Invoke the underlying compiler to produce hello.exe_comb.cil.o +
6. Invoke the actual linker to produce hello.exe +
+

+Note that files that you specify with --leavealone are not merged and +never presented to CIL. They are compiled as usual and then are linked in at +the end.
+
+And a final feature of cilly is that it can substitute copies of the +system's include files: +

+make CC="bin/cilly --includedir=myinclude"
+

+ This will force the preprocessor to use the file myinclude/xxx/stdio.h +(if it exists) whenever it encounters #include <stdio.h>. The xxx is +a string that identifies the compiler version you are using. This modified +include files should be produced with the patcher script (see +Section 14).
+
+ +

7.1 `cilly` Options

+Among the options for the cilly you can put anything that can normally +go in the command line of the compiler that cilly is impersonating. +cilly will do its best to pass those options along to the appropriate +subprocess. In addition, the following options are supported (a complete and +up-to-date list can always be obtained by running cilly --help): +

+--mode=mode This must be the first argument if present. It makes +cilly behave as a given compiled. The following modes are recognized: +
- + GNUCC - the GNU C Compiler. This is the default. +
- MSVC - the Microsoft Visual C compiler. Of course, you should + pass only MSVC valid options in this case. +
- AR - the archiver ar. Only the mode cr is supported and + the original version of the archive is lost. +
+
--help Prints a list of the options supported. +
--verbose Prints lots of messages about what is going on. +
--stages Less than --verbose but lets you see what cilly + is doing. +
--merge This tells cilly to first attempt to collect into one +source file all of the sources that make your application, and then to apply +cilly.asm on the resulting source. The sequence of actions in this case is +described above and the merger itself is described in Section 13.
+
+
--leavealone=xxx. Do not merge and do not present to CIL the files +whose basename is "xxx". These files are compiled as usual and linked in at +the end. +
--includedir=xxx. Override the include files with those in the given +directory. The given directory is the same name that was given an an argument +to the patcher (see Section 14). In particular this means that +that directory contains subdirectories named based on the current compiler +version. The patcher creates those directories. +
--usecabs. Do not CIL, but instead just parse the source and print +its AST out. This should looked like the preprocessed file. This is useful +when you suspect that the conversion to CIL phase changes the meaning of the +program. +
--save-temps=xxx. Temporary files are preserved in the xxx + directory. For example, the output of CIL will be put in a file + named *.cil.c. +
--save-temps. Temporay files are preserved in the current directory. +

+ +

7.2 `cilly.asm` Options

+ +All of the options that start with -- and are not understood by +cilly are passed on to cilly.asm. cilly also passes along to +cilly.asm flags such as --MSVC that both need to know +about. The following options are supported:
+
+ General Options: +

+ --version output version information and exit +
--verbose Print lots of random stuff. This is passed on from cilly +
--warnall Show all warnings. +
--debug=xxx turns on debugging flag xxx +
--nodebug=xxx turns off debugging flag xxx +
--flush Flush the output streams often (aids debugging). +
--check Run a consistency check over the CIL after every operation. +
--nocheck turns off consistency checking of CIL. +
--noPrintLn Don't output #line directives in the output. +
--commPrintLn Print #line directives in the output, but + put them in comments. +
--log=xxx Set the name of the log file. By default stderr is used +
--MSVC Enable MSVC compatibility. Default is GNU. +
--ignore-merge-conflicts ignore merging conflicts. +
--extrafiles=filename: the name of a file that contains + a list of additional files to process, separated by whitespace. +
--stats Print statistics about the running time of the + parser, conversion to CIL, etc. Also prints memory-usage + statistics. You can time parts of your own code as well. Calling + (Stats.time “label” func arg) will evaluate (func arg) + and remember how long this takes. If you call Stats.time + repeatedly with the same label, CIL will report the aggregate + time.
+
+If available, CIL uses the x86 performance counters for these + stats. This is very precise, but results in “wall-clock time.” + To report only user-mode time, find the call to Stats.reset in + main.ml, and change it to Stats.reset false.
+
+Lowering Options +
--noLowerConstants do not lower constant expressions. +
--noInsertImplicitCasts do not insert implicit casts. +
--forceRLArgEval Forces right to left evaluation of function arguments. +
--disallowDuplication Prevent small chunks of code from being duplicated. +
--keepunused Do not remove the unused variables and types. +
--rmUnusedInlines Delete any unused inline functions. This is the default in MSVC mode.
+
+Output Options: +
--printCilAsIs Do not try to simplify the CIL when + printing. Without this flag, CIL will attempt to produce prettier + output by e.g. changing while(1) into more meaningful loops. +
--noWrap do not wrap long lines when printing +
--out=xxx the name of the output CIL file. cilly + sets this for you. +
--mergedout=xxx specify the name of the merged file +
--cabsonly=xxx CABS output file name +
+
+ Selected features. See Section 8 for more information. +
--dologcalls. Insert code in the processed source to print the name of +functions as are called. Implemented in src/ext/logcalls.ml. +
--dologwrites. Insert code in the processed source to print the +address of all memory writes. Implemented in src/ext/logwrites.ml. +
--dooneRet. Make each function have at most one 'return'. +Implemented in src/ext/oneret.ml. +
--dostackGuard. Instrument function calls and returns to +maintain a separate stack for return addresses. Implemeted in +src/ext/heapify.ml. +
--domakeCFG. Make the program look more like a CFG. Implemented +in src/cil.ml. +
--dopartial. Do interprocedural partial evaluation and +constant folding. Implemented in src/ext/partial.ml. +
--dosimpleMem. Simplify all memory expressions. Implemented in +src/ext/simplemem.ml.
+
+For an up-to-date list of available options, run cilly.asm --help.

+ + -- cgit

7 The CIL Driver

7.1 cilly Options

7.2 cilly.asm Options

7.1 `cilly` Options

7.2 `cilly.asm` Options