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. You will also need to remove any other commands that operate on the generated library (e.g. ranlib, lorder), as the .a file is no longer an actual binary library.

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):

• --gcc=command Tell cilly to use command to invoke gcc, e.g. --gcc=arm-elf-gcc to use a cross-compiler. See also the --envmachine option below that tells CIL to assume a different machine model.
• --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. Many of these flags also have corresponding “--no*” versions if you need to go back to the default, as in “--nowarnall”.

       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.
• --strictcheck Same as --check, but it treats consistency problems as errors instead of warnings.
• --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.
• --commPrintLnSparse Like --commPrintLn but print only new line numbers.
• --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 Stats.SoftwareTimer.

• --envmachine. Use machine model specified in CIL_MACHINE environment variable, rather than the one compiled into CIL. Note that you should not pass gcc’s 32/64-bit -m32 and -m64 options to cilly if you use --envmachine (they use --envmachine under the hood). See Section 7.4 for a description of CIL_MACHINE’s format.

  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.

7.3  Internal Options

All of the cilly.asm options described above can be set programmatically – see src/ciloptions.ml or the individual extensions to see how. Some options should be set before parsing to be effective.

Additionally, a few CIL options have no command-line flag and can only be set programmatically. These options may be useful for certain analyses:

• Cabs2cil.doCollapseCallCast:This is false by default. Set to true to replicate the behavior of CIL 1.3.5 and earlier.

  When false, all casts in the program are made explicit using the CastE expression. Accordingly, the destination of a Call instruction will always have the same type as the function’s return type.

  If true, the destination type of a Call may differ from the return type, so there is an implicit cast. This is useful for analyses involving malloc. Without this option, CIL converts “T* x = malloc(n);” into “void* tmp = malloc(n); T* x = (T*)tmp;”. If you don’t need all casts to be made explicit, you can set Cabs2cil.doCollapseCallCast to true so that CIL won’t insert a temporary and you can more easily determine the allocation type from calls to malloc.

7.4  Specifying a machine model

The --envmachine option tells CIL to get its machine model from the CIL_MACHINE environment variable, rather than use the model compiled in to CIL itself. This is necessary when using CIL as part of a cross-compilation setup, and to handle gcc’s -m32 and -m64 which select between a 32-bit and 64-bit machine model.

CIL_MACHINE is a space-separated list of key=value pairs. Unknown keys are ignored. The following keys must be defined:

Some notes:

• Values cannot contain spaces as spaces separate key/value pairs.
• The value of size_t is the text for the type defined as size_t, e.g. unsigned long. As spaces are not allowed in values, CIL will replace underscores by spaces: size_t=unsigned_long.
• sizeof(t) and alignof(t) are respectively the size and alignment of type t.
• The boolean-valued keys expect true for true, and false for false.
• The src/machdep-ml.c program will print a CIL_MACHINE value when run with the --env option.

As an example, here’s the CIL_MACHINE value for 64-bit targets on an x86-based Mac OS X machine:

  short=2,2 int=4,4 long=8,8 long_long=8,8 pointer=8,8 enum=4,4
  float=4,4 double=8,8 long_double=16,16 void=1 bool=1,1 fun=1,1
  alignof_string=1 max_alignment=16 size_t=unsigned_long 
  wchar_t=int char_signed=true const_string_literals=true 
  big_endian=false __thread_is_keyword=true 
  __builtin_va_list=true underscore_name=true