+How to Use CIL +

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/cilly.html | 187 +++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 187 insertions(+) create mode 100644 cil/doc/cilly.html (limited to 'cil/doc/cilly.html') diff --git a/cil/doc/cilly.html b/cil/doc/cilly.html new file mode 100644 index 00000000..1a287581 --- /dev/null +++ b/cil/doc/cilly.html @@ -0,0 +1,187 @@ + + + + + + + + + + + + + +How to Use CIL + + + +

+ +

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

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.
+
+
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.
+
+
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.
+
+

+ + -- cgit

5 How to Use CIL

5.1 Using cilly, the CIL driver

5.2 Using CIL as a library

5.1 Using `cilly`, the CIL driver