-How to Use CIL -

From 93d89c2b5e8497365be152fb53cb6cd4c5764d34 Mon Sep 17 00:00:00 2001 From: xleroy Date: Wed, 3 Mar 2010 10:25:25 +0000 Subject: Getting rid of CIL git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1270 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- cil/doc/cilly.html | 187 ----------------------------------------------------- 1 file changed, 187 deletions(-) delete mode 100644 cil/doc/cilly.html (limited to 'cil/doc/cilly.html') diff --git a/cil/doc/cilly.html b/cil/doc/cilly.html deleted file mode 100644 index 1a287581..00000000 --- a/cil/doc/cilly.html +++ /dev/null @@ -1,187 +0,0 @@ - - - - - - - - - - - - - -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