Module Cil

module Cil: sig .. end

val initCIL : unit -> unit

val cilVersion : string

val cilVersionMajor : int

val cilVersionMinor : int

val cilVersionRevision : int

type comment = location * string 

There are two easy ways to scan a type. First, you can use the Cil.existsType to return a boolean answer about a type. This function is controlled by a user-provided function that is queried for each type that is used to construct the current type. The function can specify whether to terminate the scan with a boolean result or to continue the scan for the nested types.

The other method for scanning types is provided by the visitor interface (see Cil.cilVisitor).

If you want to compare types (or to use them as hash-values) then you should use instead type signatures (represented as Cil.typsig). These contain the same information as types but canonicalized such that simple Ocaml structural equality will tell whether two types are equal. Use Cil.typeSig to compute the signature of a type. If you want to ignore certain type attributes then use Cil.typeSigWithAttrs.

type ikind =

|	IChar	(*	char	*)
|	ISChar	(*	signed char	*)
|	IUChar	(*	unsigned char	*)
|	IInt	(*	int	*)
|	IUInt	(*	unsigned int	*)
|	IShort	(*	short	*)
|	IUShort	(*	unsigned short	*)
|	ILong	(*	long	*)
|	IULong	(*	unsigned long	*)
|	ILongLong	(*	long long (or _int64 on Microsoft Visual C)	*)
|	IULongLong	(*	unsigned long long (or unsigned _int64 on Microsoft Visual C)	*)

type attributes = attribute list 

If all you need is to scan the definition of each composite type once, you can do that by scanning all top-level GCompTag.

Constructing a Cil.compinfo can be tricky since it must contain fields that might refer to the host Cil.compinfo and furthermore the type of the field might need to refer to the Cil.compinfo for recursive types. Use the Cil.mkCompInfo function to create a Cil.compinfo. You can easily fetch the Cil.fieldinfo for a given field in a structure with Cil.getCompField.

type compinfo = {

	mutable cstruct : bool;	(*	True if struct, False if union	*)
	mutable cname : string;	(*	The name. Always non-empty. Use Cil.compFullName to get the full name of a comp (along with the struct or union)	*)
	mutable ckey : int;	(*	A unique integer. This is assigned by Cil.mkCompInfo using a global variable in the Cil module. Thus two identical structs in two different files might have different keys. Use Cil.copyCompInfo to copy structures so that a new key is assigned.	*)
	mutable cfields : fieldinfo list;	(*	Information about the fields. Notice that each fieldinfo has a pointer back to the host compinfo. This means that you should not share fieldinfo's between two compinfo's	*)
	mutable cattr : attributes;	(*	The attributes that are defined at the same time as the composite type. These attributes can be supplemented individually at each reference to this compinfo using the TComp type constructor.	*)
	mutable cdefined : bool;	(*	This boolean flag can be used to distinguish between structures that have not been defined and those that have been defined but have no fields (such things are allowed in gcc).	*)
	mutable creferenced : bool;	(*	True if used. Initially set to false.	*)

}

All references to a given global or local variable must refer to the same copy of the varinfo. Each varinfo has a globally unique identifier that can be used to index maps and hashtables (the name can also be used for this purpose, except for locals from different functions). This identifier is constructor using a global counter.

It is very important that you construct varinfo structures using only one of the following functions:

• Cil.makeGlobalVar : to make a global variable
• Cil.makeTempVar : to make a temporary local variable whose name will be generated so that to avoid conflict with other locals.
• Cil.makeLocalVar : like Cil.makeTempVar but you can specify the exact name to be used.
• Cil.copyVarinfo: make a shallow copy of a varinfo assigning a new name and a new unique identifier

Integer and floating point constants can carry their textual representation. This way the integer 15 can be printed as 0xF if that is how it occurred in the source.

CIL uses 64 bits to represent the integer constants and also stores the width of the integer type. Care must be taken to ensure that the constant is representable with the given width. Use the functions Cil.kinteger, Cil.kinteger64 and Cil.integer to construct constant expressions. CIL predefines the constants Cil.zero, Cil.one and Cil.mone (for -1).

Use the functions Cil.isConstant and Cil.isInteger to test if an expression is a constant and a constant integer respectively.

CIL keeps the type of all unary and binary expressions. You can think of that type qualifying the operator. Furthermore there are different operators for arithmetic and comparisons on arithmetic types and on pointers.

Another unusual aspect of CIL is that the implicit conversion between an expression of array type and one of pointer type is made explicit, using the StartOf expression constructor (which is not printed). If you apply the AddrOf}constructor to an lvalue of type T then you will be getting an expression of type TPtr(T).

You can find the type of an expression with Cil.typeOf.

You can perform constant folding on expressions using the function Cil.constFold.

type exp =

|	Const of constant	(*	Constant	*)
|	Lval of lval	(*	Lvalue	*)
|	SizeOf of typ	(*	sizeof(<type>). Has unsigned int type (ISO 6.5.3.4). This is not turned into a constant because some transformations might want to change types	*)
|	SizeOfE of exp	(*	sizeof(<expression>)	*)
|	SizeOfStr of string	(*	sizeof(string_literal). We separate this case out because this is the only instance in which a string literal should not be treated as having type pointer to character.	*)
|	AlignOf of typ	(*	This corresponds to the GCC __alignof_. Has unsigned int type	*)
|	AlignOfE of exp
|	UnOp of unop * exp * typ	(*	Unary operation. Includes the type of the result.	*)
|	BinOp of binop * exp * exp * typ	(*	Binary operation. Includes the type of the result. The arithmetic conversions are made explicit for the arguments.	*)
|	CastE of typ * exp	(*	Use Cil.mkCast to make casts.	*)
|	AddrOf of lval	(*	Always use Cil.mkAddrOf to construct one of these. Apply to an lvalue of type T yields an expression of type TPtr(T). Use Cil.mkAddrOrStartOf to make one of these if you are not sure which one to use.	*)
|	StartOf of lval	(*	Conversion from an array to a pointer to the beginning of the array. Given an lval of type TArray(T) produces an expression of type TPtr(T). Use Cil.mkAddrOrStartOf to make one of these if you are not sure which one to use. In C this operation is implicit, the StartOf operator is not printed. We have it in CIL because it makes the typing rules simpler.	*)

 
a[0][1][2]

An lvalue denotes the contents of a range of memory addresses. This range is denoted as a host object along with an offset within the object. The host object can be of two kinds: a local or global variable, or an object whose address is in a pointer expression. We distinguish the two cases so that we can tell quickly whether we are accessing some component of a variable directly or we are accessing a memory location through a pointer. To make it easy to tell what an lvalue means CIL represents lvalues as a host object and an offset (see Cil.lval). The host object (represented as Cil.lhost) can be a local or global variable or can be the object pointed-to by a pointer expression. The offset (represented as Cil.offset) is a sequence of field or array index designators.

Both the typing rules and the meaning of an lvalue is very precisely specified in CIL.

The following are a few useful function for operating on lvalues:

• Cil.mkMem - makes an lvalue of Mem kind. Use this to ensure that certain equivalent forms of lvalues are canonized. For example, *&x = x.
• Cil.typeOfLval - the type of an lvalue
• Cil.typeOffset - the type of an offset, given the type of the host.
• Cil.addOffset and Cil.addOffsetLval - extend sequences of offsets.
• Cil.removeOffset and Cil.removeOffsetLval - shrink sequences of offsets.

Mem(AddrOf(Mem a, aoff)), off   = Mem a, aoff + off 
Mem(AddrOf(Var v, aoff)), off   = Var v, aoff + off 
AddrOf (Mem a, NoOffset)        = a                 

type lval = lhost * offset 

The function definition contains, in addition to the body, a list of all the local variables and separately a list of the formals. Both kind of variables can be referred to in the body of the function. The formals must also be shared with the formals that appear in the function type. For that reason, to manipulate formals you should use the provided functions Cil.makeFormalVar and Cil.setFormals and Cil.makeFormalVar.

type fundec = {

	mutable svar : varinfo;	(*	Holds the name and type as a variable, so we can refer to it easily from the program. All references to this function either in a function call or in a prototype must point to the same varinfo.	*)
	mutable sformals : varinfo list;	(*	Formals. These must be in the same order and with the same information as the formal information in the type of the function. Use Cil.setFormals or Cil.setFunctionType or Cil.makeFormalVar to set these formals and ensure that they are reflected in the function type. Do not make copies of these because the body refers to them.	*)
	mutable slocals : varinfo list;	(*	Locals. Does NOT include the sformals. Do not make copies of these because the body refers to them.	*)
	mutable smaxid : int;	(*	Max local id. Starts at 0. Used for creating the names of new temporary variables. Updated by Cil.makeLocalVar and Cil.makeTempVar. You can also use Cil.setMaxId to set it after you have added the formals and locals.	*)
	mutable sbody : block;	(*	The function body.	*)
	mutable smaxstmtid : int option;	(*	max id of a (reachable) statement in this function, if we have computed it. range = 0 ... (smaxstmtid-1). This is computed by Cil.computeCFGInfo.	*)
	mutable sallstmts : stmt list;	(*	After you call Cil.computeCFGInfo this field is set to contain all statements in the function	*)

}

Use Cil.mkStmt to make a statement and the fill-in the fields.

CIL also comes with support for control-flow graphs. The sid field in stmt can be used to give unique numbers to statements, and the succs and preds fields can be used to maintain a list of successors and predecessors for every statement. The CFG information is not computed by default. Instead you must explicitly use the functions Cil.prepareCFG and Cil.computeCFGInfo to do it.

type stmt = {

	mutable labels : label list;	(*	Whether the statement starts with some labels, case statements or default statements.	*)
	mutable skind : stmtkind;	(*	The kind of statement	*)
	mutable sid : int;	(*	A number (>= 0) that is unique in a function. Filled in only after the CFG is computed.	*)
	mutable succs : stmt list;	(*	The successor statements. They can always be computed from the skind and the context in which this statement appears. Filled in only after the CFG is computed.	*)
	mutable preds : stmt list;	(*	The inverse of the succs function.	*)

}