5  How to Use CIL

There are two predominant ways to use CIL to write a program analysis or transformation. The first is to phrase your analysis as a module that is called by our existing driver. The second is to use CIL as a stand-alone library. We highly recommend that you use cilly, our driver.

5.1  Using cilly, the CIL driver

The most common way to use CIL is to write an Ocaml module containing your analysis and transformation, which you then link into our boilerplate driver application called cilly. cilly is a Perl script that processes and mimics GCC and MSVC command-line arguments and then calls cilly.byte.exe or cilly.asm.exe (CIL’s Ocaml executable).

An example of such module is logwrites.ml, a transformation that is distributed with CIL and whose purpose is to instrument code to print the addresses of memory locations being written. (We plan to release a C-language interface to CIL so that you can write your analyses in C instead of Ocaml.) See Section 8 for a survey of other example modules.

Assuming that you have written /home/necula/logwrites.ml, here is how you use it:

1. Modify logwrites.ml so that it includes a CIL “feature descriptor” like this:

   let feature : featureDescr = 
     { fd_name = "logwrites";              
       fd_enabled = ref false;
       fd_description = "generation of code to log memory writes";
       fd_extraopt = [];
       fd_doit = 
       (function (f: file) -> 
         let lwVisitor = new logWriteVisitor in
         visitCilFileSameGlobals lwVisitor f)
     } 
   

   The fd_name field names the feature and its associated command-line arguments. The fd_enabled field is a bool ref. “fd_doit” will be invoked if !fd_enabled is true after argument parsing, so initialize the ref cell to true if you want this feature to be enabled by default.

   When the user passes the --dologwrites command-line option to cilly, the variable associated with the fd_enabled flag is set and the fd_doit function is called on the Cil.file that represents the merger (see Section 13) of all C files listed as arguments.

2. Invoke configure with the arguments

   ./configure EXTRASRCDIRS=/home/necula EXTRAFEATURES=logwrites
   

   This step works if each feature is packaged into its own ML file, and the name of the entry point in the file is feature.

   An alternative way to specify the new features is to change the build files yourself, as explained below. You’ll need to use this method if a single feature is split across multiple files.

   1. Put logwrites.ml in the src or src/ext directory. This will make sure that make can find it. If you want to put it in some other directory, modify Makefile.in and add to SOURCEDIRS your directory. Alternately, you can create a symlink from src or src/ext to your file.
   2. Modify the Makefile.in and add your module to the CILLY_MODULES or CILLY_LIBRARY_MODULES variables. The order of the modules matters. Add your modules somewhere after cil and before main.
   3. If you have any helper files for your module, add those to the makefile in the same way. e.g.:

      CILLY_MODULES = $(CILLY_LIBRARY_MODULES) \
                      myutilities1 myutilities2 logwrites \
                      main
      

      Again, order is important: myutilities2.ml will be able to refer to Myutilities1 but not Logwrites. If you have any ocamllex or ocamlyacc files, add them to both CILLY_MODULES and either MLLS or MLYS.

   4. Modify main.ml so that your new feature descriptor appears in the global list of CIL features.

      let features : C.featureDescr list = 
        [ Logcalls.feature;
          Oneret.feature;    
          Heapify.feature1;  
          Heapify.feature2;
          makeCFGFeature; 
          Partial.feature;
          Simplemem.feature;
          Logwrites.feature;  (* add this line to include the logwrites feature! *)
        ] 
        @ Feature_config.features 
      

      Features are processed in the order they appear on this list. Put your feature last on the list if you plan to run any of CIL’s built-in features (such as makeCFGfeature) before your own.

   Standard code in cilly takes care of adding command-line arguments, printing the description, and calling your function automatically. Note: do not worry about introducing new bugs into CIL by adding a single line to the feature list.

3. Now you can invoke the cilly application on a preprocessed file, or instead use the cilly driver which provides a convenient compiler-like interface to cilly. See Section 7 for details using cilly. Remember to enable your analysis by passing the right argument (e.g., --dologwrites).

5.2  Using CIL as a library

CIL can also be built as a library that is called from your stand-alone application. Add cil/src, cil/src/frontc, cil/obj/x86_LINUX (or cil/obj/x86_WIN32) to your Ocaml project -I include paths. Building CIL will also build the library cil/obj/*/cil.cma (or cil/obj/*/cil.cmxa). You can then link your application against that library.

You can call the Frontc.parse: string -> unit -> Cil.file function with the name of a file containing the output of the C preprocessor. The Mergecil.merge: Cil.file list -> string -> Cil.file function merges multiple files. You can then invoke your analysis function on the resulting Cil.file data structure. You might want to call Rmtmps.removeUnusedTemps first to clean up the prototypes and variables that are not used. Then you can call the function Cil.dumpFile: cilPrinter -> out_channel -> Cil.file -> unit to print the file to a given output channel. A good cilPrinter to use is defaultCilPrinter.

Check out src/main.ml and bin/cilly for other good ideas about high-level file processing. Again, we highly recommend that you just our cilly driver so that you can avoid spending time re-inventing the wheel to provide drop-in support for standard makefiles.

Here is a concrete example of compiling and linking your project against CIL. Imagine that your program analysis or transformation is contained in the single file main.ml.

$ ocamlopt -c -I $(CIL)/obj/x86_LINUX/ main.ml
$ ocamlopt -ccopt -L$(CIL)/obj/x86_LINUX/ -o main unix.cmxa str.cmxa \ 
        $(CIL)/obj/x86_LINUX/cil.cmxa main.cmx

The first line compiles your analysis, the second line links it against CIL (as a library) and the Ocaml Unix library. For more information about compiling and linking Ocaml programs, see the Ocaml home page at http://caml.inria.fr/ocaml/.

In the next section we give an overview of the API that you can use to write your analysis and transformation.