CIL API Documentation.
val initCIL : unit -> unitCall this function to perform some initialization.
These are the CIL version numbers. A CIL version is a number of the form M.m.r (major, minor and release)
This module defines the abstract syntax of CIL. It also provides utility functions for traversing the CIL data structures, and pretty-printing them. The parser can be invoked as Frontc.parse: string -> unit -> file. This function must be given the name of a preprocessed C file and will return the top-level data structure that describes a whole source file. The parsing and elaboration into CIL is done as for GCC source.
The Abstract Syntax of CIL
The top-level representation of a CIL source file (and the result of the parsing and elaboration). Its main contents is the list of global declarations and definitions. You can iterate over the globals in a file using the following iterators: mapGlobals, iterGlobals and foldGlobals. You can also use the dummyFile when you need a file as a placeholder. For each global item CIL stores the source location where it appears (using the type location)
type file = {mutable fileName : string;mutable globals : global list;List of globals as they will appear in the printed file
mutable globinit : fundec option;An optional global initializer function. This is a function where you can put stuff that must be executed before the program is started. This function is conceptually at the end of the file, although it is not part of the globals list. Use getGlobInit to create/get one.
mutable globinitcalled : bool;Whether the global initialization function is called in main. This should always be false if there is no global initializer. When you create a global initialization CIL will try to insert code in main to call it. This will not happen if your file does not contain a function called "main"
}Top-level representation of a C source file
Globals. The main type for representing global declarations and definitions. A list of these form a CIL file. The order of globals in the file is generally important.
and global = | GType of typeinfo * locationA typedef. All uses of type names (through the TNamed constructor) must be preceded in the file by a definition of the name. The string is the defined name and always not-empty.
| GCompTag of compinfo * locationDefines a struct/union tag with some fields. There must be one of these for each struct/union tag that you use (through the TComp constructor) since this is the only context in which the fields are printed. Consequently nested structure tag definitions must be broken into individual definitions with the innermost structure defined first.
| GCompTagDecl of compinfo * locationDeclares a struct/union tag. Use as a forward declaration. This is printed without the fields.
| GEnumTag of enuminfo * locationDeclares an enumeration tag with some fields. There must be one of these for each enumeration tag that you use (through the TEnum constructor) since this is the only context in which the items are printed.
| GEnumTagDecl of enuminfo * locationDeclares an enumeration tag. Use as a forward declaration. This is printed without the items.
| GVarDecl of varinfo * locationA variable declaration (not a definition). If the variable has a function type then this is a prototype. There can be several declarations and at most one definition for a given variable. If both forms appear then they must share the same varinfo structure. A prototype shares the varinfo with the fundec of the definition. Either has storage Extern or there must be a definition in this file
| GVar of varinfo * initinfo * locationA variable definition. Can have an initializer. The initializer is updateable so that you can change it without requiring to recreate the list of globals. There can be at most one definition for a variable in an entire program. Cannot have storage Extern or function type. Note: the initializer field is kept for backwards compatibility, but it is now also available directly in the varinfo.
| GFun of fundec * location| GAsm of string * locationGlobal asm statement. These ones can contain only a template
| GPragma of attribute * locationPragmas at top level. Use the same syntax as attributes
| GText of stringSome text (printed verbatim) at top level. E.g., this way you can put comments in the output.
A global declaration or definition
Types. A C type is represented in CIL using the type typ. Among types we differentiate the integral types (with different kinds denoting the sign and precision), floating point types, enumeration types, array and pointer types, and function types. Every type is associated with a list of attributes, which are always kept in sorted order. Use addAttribute and addAttributes to construct list of attributes. If you want to inspect a type, you should use unrollType or unrollTypeDeep to see through the uses of named types.
CIL is configured at build-time with the sizes and alignments of the underlying compiler. CIL contains functions that can compute the size of a type (in bits) bitsSizeOf, the alignment of a type (in bytes) alignOf_int, and can convert an offset into a start and width (both in bits) using the function bitsOffset. At the moment these functions do not take into account the packed attributes and pragmas.
and typ = | TVoid of attributes| TInt of ikind * attributes| TFloat of fkind * attributesA floating-point type. The kind specifies the precision. You can also use the predefined constant doubleType.
| TPtr of typ * attributes| TArray of typ * exp option * attributesArray type. It indicates the base type and the array length.
| TFun of typ * (string * typ * attributes) list option * bool * attributesFunction type. Indicates the type of the result, the name, type and name attributes of the formal arguments (None if no arguments were specified, as in a function whose definition or prototype we have not seen; Some [] means void). Use argsToList to obtain a list of arguments. The boolean indicates if it is a variable-argument function. If this is the type of a varinfo for which we have a function declaration then the information for the formals must match that in the function's sformals. Use setFormals, or setFunctionType, or makeFormalVar for this purpose.
| TNamed of typeinfo * attributesThe use of a named type. Each such type name must be preceded in the file by a GType global. This is printed as just the type name. The actual referred type is not printed here and is carried only to simplify processing. To see through a sequence of named type references, use unrollType or unrollTypeDeep. The attributes are in addition to those given when the type name was defined.
| TComp of compinfo * attributesThe most delicate issue for C types is that recursion that is possible by using structures and pointers. To address this issue we have a more complex representation for structured types (struct and union). Each such type is represented using the compinfo type. For each composite type the compinfo structure must be declared at top level using GCompTag and all references to it must share the same copy of the structure. The attributes given are those pertaining to this use of the type and are in addition to the attributes that were given at the definition of the type and which are stored in the compinfo.
| TEnum of enuminfo * attributesA reference to an enumeration type. All such references must share the enuminfo among them and with a GEnumTag global that precedes all uses. The attributes refer to this use of the enumeration and are in addition to the attributes of the enumeration itself, which are stored inside the enuminfo
| TBuiltin_va_list of attributesThis is the same as the gcc's type with the same name
There are a number of functions for querying the kind of a type. These are isIntegralType, isArithmeticType, isPointerType, isScalarType, isFunctionType, isArrayType.
There are two easy ways to scan a type. First, you can use the 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 cilVisitor).
If you want to compare types (or to use them as hash-values) then you should use instead type signatures (represented as typsig). These contain the same information as types but canonicalized such that simple Ocaml structural equality will tell whether two types are equal. Use typeSig to compute the signature of a type. If you want to ignore certain type attributes then use typeSigWithAttrs.
and ikind = | IChar| ISChar| IUChar| IBool| IInt| IUInt| IShort| IUShort| ILong| IULong| ILongLonglong long (or _int64 on Microsoft Visual C)
| IULongLongunsigned long long (or unsigned _int64 on Microsoft Visual C)
| IInt128| IUInt128
Various kinds of integers
and fkind = | FFloat| FDouble| FLongDouble| FComplexFloat| FComplexDouble| FComplexLongDouble
Various kinds of floating-point numbers
Attributes.
and attribute = | Attr of string * attrparam listAn attribute has a name and some optional parameters. The name should not start or end with underscore. When CIL parses attribute names it will strip leading and ending underscores (to ensure that the multitude of GCC attributes such as const, __const and __const__ all mean the same thing.)
Attributes are lists sorted by the attribute name. Use the functions addAttribute and addAttributes to insert attributes in an attribute list and maintain the sortedness.
The type of parameters of attributes
Structures. The compinfo describes the definition of a structure or union type. Each such compinfo must be defined at the top-level using the GCompTag constructor and must be shared by all references to this type (using either the TComp type constructor or from the definition of the fields.
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 compinfo can be tricky since it must contain fields that might refer to the host compinfo and furthermore the type of the field might need to refer to the compinfo for recursive types. Use the mkCompInfo function to create a compinfo. You can easily fetch the fieldinfo for a given field in a structure with getCompField.
and compinfo = {mutable cstruct : bool;True if struct, False if union
mutable cname : string;The name. Always non-empty. Use 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 mkCompInfo using a global variable in the Cil module. Thus two identical structs in two different files might have different keys. Use 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.
}The definition of a structure or union type. Use mkCompInfo to make one and use copyCompInfo to copy one (this ensures that a new key is assigned and that the fields have the right pointers to parents.).
Structure fields. The fieldinfo structure is used to describe a structure or union field. Fields, just like variables, can have attributes associated with the field itself or associated with the type of the field (stored along with the type of the field).
and fieldinfo = {mutable fcomp : compinfo;The host structure that contains this field. There can be only one compinfo that contains the field.
mutable fname : string;The name of the field. Might be the value of missingFieldName in which case it must be a bitfield and is not printed and it does not participate in initialization
mutable ftype : typ;mutable fbitfield : int option;If a bitfield then ftype should be an integer type and the width of the bitfield must be 0 or a positive integer smaller or equal to the width of the integer type. A field of width 0 is used in C to control the alignment of fields.
mutable fattr : attributes;The attributes for this field (not for its type)
mutable floc : location;The location where this field is defined
}Information about a struct/union field
Enumerations. Information about an enumeration. This is shared by all references to an enumeration. Make sure you have a GEnumTag for each of of these.
and enuminfo = {mutable ename : string;The name. Always non-empty.
mutable eitems : (string * exp * location) list;Items with names and values. This list should be non-empty. The item values must be compile-time constants.
mutable eattr : attributes;The attributes that are defined at the same time as the enumeration type. These attributes can be supplemented individually at each reference to this enuminfo using the TEnum type constructor.
mutable ereferenced : bool;True if used. Initially set to false
mutable ekind : ikind;The integer kind used to represent this enum. Per ANSI-C, this should always be IInt, but gcc allows other integer kinds
}Information about an enumeration
and typeinfo = {mutable tname : string;The name. Can be empty only in a GType when introducing a composite or enumeration tag. If empty cannot be referred to from the file
mutable ttype : typ;The actual type. This includes the attributes that were present in the typedef
mutable treferenced : bool;True if used. Initially set to false
}Information about a defined type
Variables. Each local or global variable is represented by a unique varinfo structure. A global varinfo can be introduced with the GVarDecl or GVar or GFun globals. A local varinfo can be introduced as part of a function definition fundec.
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:
makeGlobalVar : to make a global variablemakeTempVar : to make a temporary local variable whose name will be generated so that to avoid conflict with other locals.makeLocalVar : like makeTempVar but you can specify the exact name to be used.copyVarinfo: make a shallow copy of a varinfo assigning a new name and a new unique identifier
A varinfo is also used in a function type to denote the list of formals.
and varinfo = {mutable vname : string;The name of the variable. Cannot be empty. It is primarily your responsibility to ensure the uniqueness of a variable name. For local variables makeTempVar helps you ensure that the name is unique.
mutable vtype : typ;The declared type of the variable.
mutable vattr : attributes;A list of attributes associated with the variable.
mutable vstorage : storage;mutable vglob : bool;True if this is a global variable
mutable vinline : bool;Whether this varinfo is for an inline function.
mutable vdecl : location;Location of variable declaration.
vinit : initinfo;Optional initializer. Only used for static and global variables. Initializers for other types of local variables are turned into assignments. Not mutable because the init field in initinfo is mutable already.
mutable vid : int;mutable vaddrof : bool;True if the address of this variable is taken. CIL will set these flags when it parses C, but you should make sure to set the flag whenever your transformation create AddrOf expression.
mutable vreferenced : bool;True if this variable is ever referenced. This is computed by Rmtmps.removeUnusedTemps. It is safe to just initialize this to False
mutable vdescr : Pretty.doc;For most temporary variables, a description of what the var holds. (e.g. for temporaries used for function call results, this string is a representation of the function call.)
mutable vdescrpure : bool;Indicates whether the vdescr above is a pure expression or call. Printing a non-pure vdescr more than once may yield incorrect results.
mutable vhasdeclinstruction : bool;Indicates whether a VarDecl instruction was generated for this variable. Only applies to local variables. Currently, this is relevant for when to print the declaration. If this is true, it might be incorrect to print the declaration at the beginning of the function, rather than where the VarDecl instruction is. This was introduced to handle VLAs.
}Information about a variable.
and storage = | NoStorageThe default storage. Nothing is printed
| Static| Register| Extern
Storage-class information
Expressions. The CIL expression language contains only the side-effect free expressions of C. They are represented as the type exp. There are several interesting aspects of CIL expressions:
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 kinteger, kinteger64 and integer to construct constant expressions. CIL predefines the constants zero, one and mone (for -1).
Use the function isConstant to test if an expression is a constant.
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 typeOf.
You can perform constant folding on expressions using the function constFold.
and exp = | Const of constant| Lval of lval| SizeOf of typsizeof(<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
| Real of exp| Imag of exp| SizeOfE of exp| SizeOfStr of stringsizeof(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 typThis corresponds to the GCC __alignof_. Has unsigned int type
| AlignOfE of exp| UnOp of unop * exp * typUnary operation. Includes the type of the result.
| BinOp of binop * exp * exp * typBinary operation. Includes the type of the result. The arithmetic conversions are made explicit for the arguments.
| Question of exp * exp * exp * typ(a ? b : c) operation. Includes the type of the result
| CastE of typ * exp| AddrOf of lvalAlways use mkAddrOf to construct one of these. Apply to an lvalue of type T yields an expression of type TPtr(T). Use mkAddrOrStartOf to make one of these if you are not sure which one to use.
| AddrOfLabel of stmt refThe address of a label, using GCC's label-as-value extension. If you want to use these, you must set useComputedGoto.
| StartOf of lvalConversion 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 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.
Expressions (Side-effect free)
Constants.
and wstring_type = | Wchar_t| Char16_t| Char32_t
and encoding = | No_encoding| Utf8
and constant = | CInt of Cilint.cilint * ikind * string optionInteger constant. Give the ikind (see ISO9899 6.1.3.2) and the textual representation, if available. (This allows us to print a constant as, for example, 0xF instead of 15.) Use integer or kinteger to create these.
| CStr of string * encodingString constant. The escape characters inside the string have been already interpreted. This constant has pointer to character type! The only case when you would like a string literal to have an array type is when it is an argument to sizeof. In that case you should use SizeOfStr.
| CWStr of int64 list * wstring_typeWide character string constant. Note that the local interpretation of such a literal depends on wcharType and wcharKind. Such a constant has type pointer to wcharType. The escape characters in the string have not been "interpreted" in the sense that L"A\xabcd" remains "A\xabcd" rather than being represented as the wide character list with two elements: 65 and 43981. That "interpretation" depends on the underlying wide character type.
| CChr of charCharacter constant. This has type int, so use charConstToInt to read the value in case sign-extension is needed.
| CReal of float * fkind * string optionFloating point constant. Give the fkind (see ISO 6.4.4.2) and also the textual representation, if available.
| CEnum of exp * string * enuminfoAn enumeration constant with the given value, name, from the given enuminfo. This is used only if lowerConstants is true (default). Use constFoldVisitor to replace these with integer constants.
and unop = | Neg| BNot| LNot
and binop = | PlusA| PlusPI| IndexPIpointer + integer but only when it arises from an expression e[i] when e is a pointer and not an array. This is semantically the same as PlusPI but CCured uses this as a hint that the integer is probably positive.
| MinusA| MinusPI| MinusPP| Mult| Div| Mod| Shiftlt| Shiftrt| Lt< (arithmetic comparison)
| Gt> (arithmetic comparison)
| Le<= (arithmetic comparison)
| Ge> (arithmetic comparison)
| Eq== (arithmetic comparison)
| Ne!= (arithmetic comparison)
| BAnd| BXor| BOr| LAndlogical and. Unlike other expressions this one does not always evaluate both operands. If you want to use these, you must set useLogicalOperators.
| LOrlogical or. Unlike other expressions this one does not always evaluate both operands. If you want to use these, you must set useLogicalOperators.
Lvalues. Lvalues are the sublanguage of expressions that can appear at the left of an assignment or as operand to the address-of operator. In C the syntax for lvalues is not always a good indication of the meaning of the lvalue. For example the C value
a[0][1][2]
might involve 1, 2 or 3 memory reads when used in an expression context, depending on the declared type of the variable a. If a has type int
[4][4][4] then we have one memory read from somewhere inside the area that stores the array a. On the other hand if a has type int *** then the expression really means * ( * ( * (a + 0) + 1) + 2), in which case it is clear that it involves three separate memory operations.
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 lval). The host object (represented as lhost) can be a local or global variable or can be the object pointed-to by a pointer expression. The offset (represented as 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:
The following equivalences hold
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
and lhost = | Var of varinfo| Mem of expThe host is an object of type T when the expression has pointer TPtr(T).
The host part of an lval.
and offset = | NoOffsetNo offset. Can be applied to any lvalue and does not change either the starting address or the type. This is used when the lval consists of just a host or as a terminator in a list of other kinds of offsets.
| Field of fieldinfo * offsetA field offset. Can be applied only to an lvalue that denotes a structure or a union that contains the mentioned field. This advances the offset to the beginning of the mentioned field and changes the type to the type of the mentioned field.
| Index of exp * offsetAn array index offset. Can be applied only to an lvalue that denotes an array. This advances the starting address of the lval to the beginning of the mentioned array element and changes the denoted type to be the type of the array element
The offset part of an lval. Each offset can be applied to certain kinds of lvalues and its effect is that it advances the starting address of the lvalue and changes the denoted type, essentially focusing to some smaller lvalue that is contained in the original one.
and init = | SingleInit of exp| CompoundInit of typ * (offset * init) listUsed only for initializers of structures, unions and arrays. The offsets are all of the form Field(f, NoOffset) or Index(i,
NoOffset) and specify the field or the index being initialized. For structures all fields must have an initializer (except the unnamed bitfields), in the proper order. This is necessary since the offsets are not printed. For unions there must be exactly one initializer. If the initializer is not for the first field then a field designator is printed. For arrays, however, we allow you to give only a prefix of the initializers. You can scan an initializer list with foldLeftCompound.
Initializers. A special kind of expressions are those that can appear as initializers for global variables (initialization of local variables is turned into assignments). The initializers are represented as type init. You can create initializers with makeZeroInit and you can conveniently scan compound initializers them with foldLeftCompound.
Initializers for global variables.
and initinfo = {mutable init : init option;
}We want to be able to update an initializer in a variable, so we define it as a mutable field
and 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 setFormals or setFunctionType or 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 makeLocalVar and makeTempVar. You can also use setMaxId to set it after you have added the formals and locals.
mutable sbody : block;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 computeCFGInfo.
mutable sallstmts : stmt list;After you call computeCFGInfo this field is set to contain all statements in the function
}Function definitions. A function definition is always introduced with a GFun constructor at the top level. All the information about the function is stored into a fundec. Some of the information (e.g. its name, type, storage, attributes) is stored as a varinfo that is a field of the fundec. To refer to the function from the expression language you must use the varinfo.
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 makeFormalVar and setFormals and makeFormalVar.
and block = {mutable battrs : attributes;mutable bstmts : stmt list;The statements comprising the block
}A block is a sequence of statements with the control falling through from one element to the next
and stmt = {mutable labels : label list;Whether the statement starts with some labels, case statements or default statements.
mutable skind : stmtkind;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.
mutable fallthrough : stmt option;The fallthrough successor statement computed from the context of this statement in computeCFGInfo. Useful for the syntactic successor of Goto and Loop.
}Statements. CIL statements are the structural elements that make the CFG. They are represented using the type stmt. Every statement has a (possibly empty) list of labels. The stmtkind field of a statement indicates what kind of statement it is.
Use 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 prepareCFG and computeCFGInfo to do it.
and label = | Label of string * location * boolA real label. If the bool is "true", the label is from the input source program. If the bool is "false", the label was created by CIL or some other transformation
| Case of exp * location * locationA case statement. This expression is lowered into a constant if lowerConstants is set to true. Second location is just for label.
| CaseRange of exp * exp * location * locationA case statement corresponding to a range of values (GCC's extension). Both expressions are lowered into constants if lowerConstants is set to true. If you want to use these, you must set useCaseRange. Second location is just for label.
| Default of location * locationA default statement. Second location is just for label.
and stmtkind = | Instr of instr listA group of instructions that do not contain control flow. Control implicitly falls through.
| Return of exp option * locationThe return statement. This is a leaf in the CFG.
| Goto of stmt ref * locationA goto statement. Appears from actual goto's in the code or from goto's that have been inserted during elaboration. The reference points to the statement that is the target of the Goto. This means that you have to update the reference whenever you replace the target statement. The target statement MUST have at least a label.
| ComputedGoto of exp * locationA computed goto using GCC's label-as-value extension. If you want to use these, you must set useComputedGoto.
| Break of locationA break to the end of the nearest enclosing Loop or Switch
| Continue of locationA continue to the start of the nearest enclosing Loop
| If of exp * block * block * location * locationA conditional. Two successors, the "then" and the "else" branches. Both branches fall-through to the successor of the If statement. Second location is just for expression.
| Switch of exp * block * stmt list * location * locationA switch statement. The statements that implement the cases can be reached through the provided list. For each such target you can find among its labels what cases it implements. The statements that implement the cases are somewhere within the provided block. Second location is just for expression.
| Loop of block * location * location * stmt option * stmt optionA while(1) loop. The termination test is implemented in the body of a loop using a Break statement. If prepareCFG has been called, the first stmt option will point to the stmt containing the continue label for this loop and the second will point to the stmt containing the break label for this loop. Second location is just for expression.
| Block of blockJust a block of statements. Use it as a way to keep some block attributes local
The various kinds of control-flow statements statements
Instructions. An instruction instr is a statement that has no local (intraprocedural) control flow. It can be either an assignment, function call, or an inline assembly instruction.
and instr = | Set of lval * exp * location * locationAn assignment. The type of the expression is guaranteed to be the same with that of the lvalue. Second location is just for expression when inside condition.
| VarDecl of varinfo * location"Instruction" in the location where a varinfo was declared. All varinfos for which such a VarDecl instruction exists have vhasdeclinstruction set to true. The motivation for the addition of this instruction was to support VLAs for which declerations can not be pulled up like CIL used to do.
| Call of lval option * exp * exp list * location * locationA function call with the (optional) result placed in an lval. It is possible that the returned type of the function is not identical to that of the lvalue. In that case a cast is printed. The type of the actual arguments are identical to those of the declared formals. The number of arguments is the same as that of the declared formals, except for vararg functions. This construct is also used to encode a call to "__builtin_va_arg". In this case the second argument (which should be a type T) is encoded SizeOf(T). Second location is just for expression when inside condition.
| Asm of attributes
* string list
* (string option * string * lval) list
* (string option * string * exp) list
* string list
* locationThere are for storing inline assembly. They follow the GCC specification:
asm [volatile] ("...template..." "..template.."
: "c1" (o1), "c2" (o2), ..., "cN" (oN)
: "d1" (i1), "d2" (i2), ..., "dM" (iM)
: "r1", "r2", ..., "nL" );where the parts are
volatile (optional): when present, the assembler instruction cannot be removed, moved, or otherwise optimized- template: a sequence of strings, with %0, %1, %2, etc. in the string to refer to the input and output expressions. I think they're numbered consecutively, but the docs don't specify. Each string is printed on a separate line.
- "ci" (oi): pairs of constraint-string and output-lval; the constraint specifies that the register used must have some property, like being a floating-point register; the constraint string for outputs also has "=" to indicate it is written, or "+" to indicate it is both read and written; 'oi' is the name of a C lvalue (probably a variable name) to be used as the output destination
- "dj" (ij): pairs of constraint and input expression; the constraint is similar to the "ci"s. the 'ij' is an arbitrary C expression to be loaded into the corresponding register
- "rk": registers to be regarded as "clobbered" by the instruction; "memory" may be specified for arbitrary memory effects
an example (from gcc manual):
asm volatile ("movc3 %0,%1,%2"
: /* no outputs */
: "g" (from), "g" (to), "g" (count)
: "r0", "r1", "r2", "r3", "r4", "r5");Starting with gcc 3.1, the operands may have names:
asm volatile ("movc3 %[in0],%1,%2"
: /* no outputs */
: [in0] "g" (from), "g" (to), "g" (count)
: "r0", "r1", "r2", "r3", "r4", "r5");
and location = {line : int;The line number. -1 means "do not know"
file : string;The name of the source file
byte : int;The byte position in the source file
column : int;endLine : int;End line number. Negative means unknown.
endByte : int;End byte position. Negative means unknown.
endColumn : int;End column number. Negative means unknown.
synthetic : bool;Synthetic location, doesn't necessarily precisely correspond to a location in original source code, e.g. due to CIL transformations.
}Describes a location in a source file.
Type signatures. Two types are identical iff they have identical signatures. These contain the same information as types but canonicalized. For example, two function types that are identical except for the name of the formal arguments are given the same signature. Also, TNamed constructors are unrolled.
Lowering Options
val lowerConstants : bool refDo lower constants (default true)
val removeBranchingOnConstants : bool refRemove branches of the form if(const) ... else ... (default true)
val insertImplicitCasts : bool refDo insert implicit casts (default true)
Comparison function for locations. Compares first by filename, then line, then byte
Values for manipulating globals
val emptyFunction : string -> fundecUpdate the formals of a fundec and make sure that the function type has the same information. Will copy the name as well into the type.
Set the types of arguments and results as given by the function type passed as the second argument. Will not copy the names from the function type to the formals
Set the type of the function and make formal arguments for them
Update the smaxid after you have populated with locals and formals (unless you constructed those using makeLocalVar or makeTempVar.
A dummy function declaration handy when you need one as a placeholder. It contains inside a dummy varinfo.
val saveBinaryFile : file -> string -> unitWrite a file in binary form to the filesystem. The file can be read back in later using loadBinaryFile, possibly saving parsing time. The second argument is the name of the file that should be created.
Write a file in binary form to the filesystem. The file can be read back in later using loadBinaryFile, possibly saving parsing time. Does not close the channel.
val loadBinaryFile : string -> fileRead a file in binary form from the filesystem. The first argument is the name of a file previously created by saveBinaryFile. Because this also reads some global state, this should be called before any other CIL code is parsed or generated.
val getGlobInit : ?main_name:string -> file -> fundecGet the global initializer and create one if it does not already exist. When it creates a global initializer it attempts to place a call to it in the main function named by the optional argument (default "main")
val iterGlobals : file -> (global -> unit) -> unitIterate over all globals, including the global initializer
val foldGlobals : file -> ('a -> global -> 'a) -> 'a -> 'aFold over all globals, including the global initializer
Map over all globals, including the global initializer and change things in place
Find a function or function prototype with the given name in the file. If it does not exist, create a prototype with the given type, and return the new varinfo. This is useful when you need to call a libc function whose prototype may or may not already exist in the file.
Because the new prototype is added to the start of the file, you shouldn't refer to any struct or union types in the function type.
val new_sid : unit -> intval prepareCFG : fundec -> unitPrepare a function for CFG information computation by computeCFGInfo. This function converts all Break, Switch, Default and Continue stmtkinds and labels into Ifs and Gotos, giving the function body a very CFG-like character. This function modifies its argument in place.
val computeCFGInfo : fundec -> bool -> unitCompute the CFG information for all statements in a fundec and return a list of the statements. The input fundec cannot have Break, Switch, Default, or Continue stmtkinds or labels. Use prepareCFG to transform them away. The second argument should be true if you wish a global statement number, false if you wish a local (per-function) statement numbering. The list of statements is set in the sallstmts field of a fundec.
NOTE: unless you want the simpler control-flow graph provided by prepareCFG, or you need the function's smaxstmtid and sallstmt fields filled in, we recommend you use Cfg.computeFileCFG instead of this function to compute control-flow information. Cfg.computeFileCFG is newer and will handle switch, break, and continue correctly.
Create a deep copy of a function. There should be no sharing between the copy and the original function
CIL keeps the types at the beginning of the file and the variables at the end of the file. This function will take a global and add it to the corresponding stack. Its operation is actually more complicated because if the global declares a type that contains references to variables (e.g. in sizeof in an array length) then it will also add declarations for the variables to the types stack
An empty statement. Used in pretty printing
A list of the built-in functions for the current compiler. Maps the name to the result and argument types, and whether it is vararg. Initialized by initCIL
This map replaces gccBuiltins and msvcBuiltins in previous versions of CIL.
This is used as the location of the prototypes of builtin functions.
Values for manipulating initializers
Make a initializer for zero-ing a data type
val foldLeftCompound :
implicit:bool ->
doinit:(offset -> init -> typ -> 'a -> 'a) ->
ct:typ ->
initl:(offset * init) list ->
acc:'a ->
'aFold over the list of initializers in a Compound (not also the nested ones). doinit is called on every present initializer, even if it is of compound type. The parameters of doinit are: the offset in the compound (this is Field(f,NoOffset) or Index(i,NoOffset)), the initializer value, expected type of the initializer value, accumulator. In the case of arrays there might be missing zero-initializers at the end of the list. These are scanned only if implicit is true. This is much like List.fold_left except we also pass the type of the initializer.
This is a good way to use it to scan even nested initializers :
let rec myInit (lv: lval) (i: init) (acc: 'a) : 'a =
match i with
SingleInit e -> ... do something with lv and e and acc ...
| CompoundInit (ct, initl) ->
foldLeftCompound ~implicit:false
~doinit:(fun off' i' t' acc ->
myInit (addOffsetLval lv off') i' acc)
~ct:ct
~initl:initl
~acc:accValues for manipulating types
val isVoidType : typ -> boolis the given type "void"?
val isVoidPtrType : typ -> boolis the given type "void *"?
val typeOfRealAndImagComponents : typ -> typfor numerical __complex types return type of corresponding real part and imaginary parts
for an fkind, return the corresponding complex fkind
val stringLiteralType : typwchar_t, char16_t and char32_t depend on architecture and are set when you call initCIL.
val charConstPtrType : typAn unsigned integer type that fits pointers. Is set when you call initCIL.
An signed integer type that fits pointer difference. Is set when you call initCIL.
An unsigned integer type that is the type of sizeof. Is set when you call initCIL.
val isSigned : ikind -> boolReturns true if and only if the given integer type is signed.
Creates a a (potentially recursive) composite type. The arguments are: (1) a boolean indicating whether it is a struct or a union, (2) the name (always non-empty), (3) a function that when given a representation of the structure type constructs the type of the fields recursive type (the first argument is only useful when some fields need to refer to the type of the structure itself), and (4) a list of attributes to be associated with the composite type. The resulting compinfo has the field "cdefined" only if the list of fields is non-empty.
Makes a shallow copy of a compinfo changing the name and the key.
val missingFieldName : stringThis is a constant used as the name of an unnamed bitfield. These fields do not participate in initialization and their name is not printed.
Get the full name of a comp
val isCompleteType : typ -> boolReturns true if this is a complete type. This means that sizeof(t) makes sense. Incomplete types are not yet defined structures and empty arrays.
Unroll a type until it exposes a non TNamed. Will collect all attributes appearing in TNamed!!!
val unrollTypeDeep : typ -> typUnroll all the TNamed in a type (even under type constructors such as TPtr, TFun or TArray. Does not unroll the types of fields in TComp types. Will collect all attributes
val isIntegralType : typ -> boolTrue if the argument is an integral type (i.e. integer or enum)
val isArithmeticType : typ -> boolTrue if the argument is an arithmetic type (i.e. integer, enum or floating point
val isPointerType : typ -> boolTrue if the argument is a pointer type
val isScalarType : typ -> boolTrue if the argument is a scalar type
val isFunctionType : typ -> boolTrue if the argument is a function type
Obtain the argument list ( if None)
val isArrayType : typ -> boolTrue if the argument is an array type
Raised when lenOfArray fails either because the length is None or because it is a non-constant expression
val lenOfArray : exp option -> intCall to compute the array length as present in the array type, to an integer. Raises LenOfArray if not able to compute the length, such as when there is no length or the length is not a constant.
Return a named fieldinfo in compinfo, or raise Not_found
type existsAction = | ExistsTrue| ExistsFalseStop processing this branch
| ExistsMaybeThis node is not what we are looking for but maybe its successors are
A datatype to be used in conjunction with existsType
Scans a type by applying the function on all elements. When the function returns ExistsTrue, the scan stops with true. When the function returns ExistsFalse then the current branch is not scanned anymore. Care is taken to apply the function only once on each composite type, thus avoiding circularity. When the function returns ExistsMaybe then the types that construct the current type are scanned (e.g. the base type for TPtr and TArray, the type of fields for a TComp, etc).
Given a function type split it into return type, arguments, is_vararg and attributes. An error is raised if the type is not a function type
Same as splitFunctionType but takes a varinfo. Prints a nicer error message if the varinfo is not for a function
Type signatures
Type signatures. Two types are identical iff they have identical signatures. These contain the same information as types but canonicalized. For example, two function types that are identical except for the name of the formal arguments are given the same signature. Also, TNamed constructors are unrolled.
Like typeSig but customize the incorporation of attributes. Use ~ignoreSign:true to convert all signed integer types to unsigned, so that signed and unsigned will compare the same.
Replace the attributes of a signature (only at top level)
Get the top-level attributes of a signature
Lvalues
Make a varinfo. Use this (rarely) to make a raw varinfo. Use other functions to make locals (makeLocalVar or makeFormalVar or makeTempVar) and globals (makeGlobalVar). Note that this function will assign a new identifier. The first argument specifies whether the varinfo is for a global.
Make a formal variable for a function. Insert it in both the sformals and the type of the function. You can optionally specify where to insert this one. If where = "^" then it is inserted first. If where = "$" then it is inserted last. Otherwise where must be the name of a formal after which to insert this. By default it is inserted at the end.
Make a local variable and add it to a function's slocals (only if insert = true, which is the default). Make sure you know what you are doing if you set insert=false.
Make a temporary variable and add it to a function's slocals. CIL will ensure that the name of the new variable is unique in this function, and will generate this name by appending a number to the specified string ("__cil_tmp" by default).
The variable will be added to the function's slocals unless you explicitly set insert=false. (Make sure you know what you are doing if you set insert=false.)
Optionally, you can give the variable a description of its contents that will be printed by descriptiveCilPrinter.
Make a global variable. Your responsibility to make sure that the name is unique
Make a shallow copy of a varinfo and assign a new identifier
Generate a new variable ID. This will be different than any variable ID that is generated by makeLocalVar and friends
Add an offset at the end of an lvalue. Make sure the type of the lvalue and the offset are compatible.
addOffset o1 o2 adds o1 to the end of o2.
Remove ONE offset from the end of an lvalue. Returns the lvalue with the trimmed offset and the final offset. If the final offset is NoOffset then the original lval did not have an offset.
Remove ONE offset from the end of an offset sequence. Returns the trimmed offset and the final offset. If the final offset is NoOffset then the original lval did not have an offset.
Compute the type of an lvalue
Compute the type of an offset from a base type
Values for manipulating expressions
Construct an integer of a given kind, from a cilint. If needed it will truncate the integer to be within the representable range for the given kind.
Construct an integer of a given kind, using OCaml's int64 type. If needed it will truncate the integer to be within the representable range for the given kind.
Construct an integer of a given kind. Converts the integer to int64 and then uses kinteger64. This might truncate the value if you use a kind that cannot represent the given integer. This can only happen for one of the Char or Short kinds
Construct an integer of kind IInt. On targets where C's 'int' is 16-bits, the integer may get truncated.
If the given expression is an integer constant or a CastE'd integer constant, return that constant's value. Otherwise return None.
val i64_to_int : int64 -> intConvert a 64-bit int to an OCaml int, or raise an exception if that can't be done.
Convert a cilint int to an OCaml int, or raise an exception if that can't be done.
val isConstant : exp -> boolTrue if the expression is a compile-time constant
val isConstantOffset : offset -> boolTrue if the given offset contains only field nanmes or constant indices.
True if the given expression is a (possibly cast'ed) integer or character constant with value zero
val isNullPtrConstant : exp -> boolTrue if the given expression is a null-pointer constant. As per 6.3.2.3 subsection 3
Given the character c in a (CChr c), sign-extend it to 32 bits. (This is the official way of interpreting character constants, according to ISO C 6.4.4.4.10, which says that character constants are chars cast to ints) Returns CInt(sign-extended c, IInt, None)
val constFold : bool -> exp -> expDo constant folding on an expression. If the first argument is true then will also compute compiler-dependent expressions such as sizeof. See also constFoldVisitor, which will run constFold on all expressions in a given AST node.
Do constant folding on a binary operation. The bulk of the work done by constFold is done here. If the first argument is true then will also compute compiler-dependent expressions such as sizeof
val increm : exp -> int -> expIncrement an expression. Can be arithmetic or pointer type
Makes an lvalue out of a given variable
Make an AddrOf. Given an lvalue of type T will give back an expression of type ptr(T). It optimizes somewhat expressions like "& v" and "& v0"
Like mkAddrOf except if the type of lval is an array then it uses StartOf. This is the right operation for getting a pointer to the start of the storage denoted by lval.
Make a Mem, while optimizing AddrOf. The type of the addr must be TPtr(t) and the type of the resulting lval is t. Note that in CIL the implicit conversion between an array and the pointer to the first element does not apply. You must do the conversion yourself using StartOf
val mkString : string -> expMake an expression that is a string constant (of pointer type)
Construct a cast when having the old type of the expression. If the new type is the same as the old type, then no cast is added.
Like mkCastT but uses typeOf to get oldt
Removes casts from this expression, but ignores casts within other expression constructs. So we delete the (A) and (B) casts from "(A)(B)(x + (C)y)", but leave the (C) cast.
Compute the type of an expression
val parseInt : string -> expConvert a string representing a C integer literal to an expression. Handles the prefixes 0x and 0 and the suffixes L, U, UL, LL, ULL
Values for manipulating statements
Construct a statement, given its kind. Initialize the sid field to -1, and labels, succs and preds to the empty list
Construct a block with no attributes, given a list of statements
Construct a statement consisting of just one instruction
val compactStmts : stmt list -> stmt listTry to compress statements so as to get maximal basic blocks. use this instead of List.@ because you get fewer basic blocks
val mkEmptyStmt : unit -> stmtReturns an empty statement (of kind Instr)
A instr to serve as a placeholder
A statement consisting of just dummyInstr
Make a while loop. Can contain Break or Continue
Make a for loop for(i=start; i<past; i += incr) { ... }. The body can contain Break but not Continue. Can be used with i a pointer or an integer. Start and done must have the same type but incr must be an integer
Make a for loop for(start; guard; next) { ... }. The body can contain Break but not Continue !!!
Values for manipulating attributes
type attributeClass = | AttrName| AttrFunTypeAttribute of a function type.
| AttrType
Various classes of attributes
This table contains the mapping of predefined attributes to classes. Extend this table with more attributes as you need. This table is used to determine how to associate attributes with names or types
Partition the attributes into classes:name attributes, function type, and type attributes
Add an attribute. Maintains the attributes in sorted order of the second argument
Add a list of attributes. Maintains the attributes in sorted order. The second argument must be sorted, but not necessarily the first
Remove all attributes with the given name. Maintains the attributes in sorted order.
Remove all attributes with names appearing in the string list. Maintains the attributes in sorted order
Retains attributes with the given name
True if the named attribute appears in the attribute list. The list of attributes must be sorted.
Returns all the attributes contained in a type. This requires a traversal of the type structure, in case of composite, enumeration and named types
typeAttrs, which doesn't add inner attributes.
Add some attributes to a type
val typeRemoveAttributes : string list -> typ -> typRemove all attributes with the given names from a type. Note that this does not remove attributes from typedef and tag definitions, just from their uses
Partition attributes into type qualifiers and non type qualifiers.
val removeOuterQualifierAttributes : typ -> typRemove top-level type qualifiers from type.
Convert an expression into an attrparam, if possible. Otherwise raise NotAnAttrParam with the offending subexpression
exception NotAnAttrParam of expThe visitor
type 'a visitAction = | SkipChildrenDo not visit the children. Return the node as it is.
| DoChildrenContinue with the children of this node. Rebuild the node on return if any of the children changes (use == test)
| ChangeTo of 'aReplace the expression with the given one
| ChangeDoChildrenPost of 'a * 'a -> 'aFirst consider that the entire exp is replaced by the first parameter. Then continue with the children. On return rebuild the node if any of the children has changed and then apply the function on the node
Different visiting actions. 'a will be instantiated with exp, instr, etc.
A visitor interface for traversing CIL trees. Create instantiations of this type by specializing the class nopCilVisitor. Each of the specialized visiting functions can also call the queueInstr to specify that some instructions should be inserted before the current instruction or statement. Use syntax like self#queueInstr to call a method associated with the current object.
Default Visitor. Traverses the CIL tree without modifying anything
Visit a file. This will will re-cons all globals TWICE (so that it is tail-recursive). Use visitCilFileSameGlobals if your visitor will not change the list of globals.
A visitor for the whole file that does not change the globals (but maybe changes things inside the globals). Use this function instead of visitCilFile whenever appropriate because it is more efficient for long files.
Visit a function definition
Visit an lvalue or recursive offset
Visit an initializer offset
Visit a variable declaration
Visit an initializer, pass also the variable to which this belongs and the offset.
Visit a list of attributes
Utility functions
Whether the pretty printer should print output for the MS VC compiler. Default is GCC. After you set this function you should call initCIL.
val makeStaticGlobal : bool refWhether to convert local static variables into global static variables
val useLogicalOperators : bool refWhether to use the logical operands LAnd and LOr. By default, do not use them because they are unlike other expressions and do not evaluate both of their operands
val useComputedGoto : bool refWhether to use GCC's computed gotos. By default, do not use them and replace them by a switch.
val useCaseRange : bool refWhether to expand ranges of values in case statements. By default, expand them and do not use the CaseRange constructor.
Fold every CaseRange in a list of labels into the corresponding list of Case labels. Raises Errormsg.Error if one of the ranges cannot be constant folded.
val oldstyleExternInline : bool refSet this to true to get old-style handling of gcc's extern inline C extension: old-style: the extern inline definition is used until the actual definition is seen (as long as optimization is enabled) new-style: the extern inline definition is used only if there is no actual definition (as long as optimization is enabled) Note that CIL assumes that optimization is always enabled ;-)
A visitor that does constant folding. Pass as argument whether you want machine specific simplifications to be done, or not.
type lineDirectiveStyle = | LinePreprocessorInputUse # nnn directives (in gcc mode)
| LinePreprocessorOutput
Styles of printing line directives
How to print line directives
Whether we print something that will only be used as input to our own parser. In that case we are a bit more liberal in what we print
val printCilAsIs : bool refWhether to print the CIL as they are, without trying to be smart and print nicer code. Normally this is false, in which case the pretty printer will turn the while(1) loops of CIL into nicer loops, will not print empty "else" blocks, etc. There is one case howewer in which if you turn this on you will get code that does not compile: if you use varargs the __builtin_va_arg function will be printed in its internal form.
The length used when wrapping output lines. Setting this variable to a large integer will prevent wrapping and make #line directives more accurate.
val forgcc : string -> stringReturn the string 's' if we're printing output for gcc, suppres it if we're printing for CIL to parse back in. the purpose is to hide things from gcc that it complains about, but still be able to do lossless transformations when CIL is the consumer
Debugging support
A reference to the current location. If you are careful to set this to the current location then you can use some built-in logging functions that will print the location.
A reference to the current expression location
A reference to the current global being visited
CIL has a fairly easy to use mechanism for printing error messages. This mechanism is built on top of the pretty-printer mechanism (see Pretty.doc) and the error-message modules (see Errormsg.error).
Here is a typical example for printing a log message:
ignore (Errormsg.log "Expression %a is not positive (at %s:%i)\n"
d_exp e loc.file loc.line)
and here is an example of how you print a fatal error message that stop the execution:
Errormsg.s (Errormsg.bug "Why am I here?")
Notice that you can use C format strings with some extension. The most useful extension is "%a" that means to consumer the next two argument from the argument list and to apply the first to unit and then to the second and to print the resulting Pretty.doc. For each major type in CIL there is a corresponding function that pretty-prints an element of that type:
Pretty-print an integer of a given kind
Pretty-print a floating-point kind
Pretty-print storage-class information
val comparativeLevel : intval getParenthLevel : exp -> intParentheses level. An expression "a op b" is printed parenthesized if its parentheses level is >= that that of its context. Identifiers have the lowest level and weakly binding operators (e.g. |) have the largest level. The correctness criterion is that a smaller level MUST correspond to a stronger precedence!
A printer interface for CIL trees. Create instantiations of this type by specializing the class defaultCilPrinterClass.
These are pretty-printers that will show you more details on the internal CIL representation, without trying hard to make it look like C
Like defaultCilPrinterClass, but instead of temporary variable names it prints the description that was provided when the temp was created. This is usually better for messages that are printed for end users, although you may want the temporary names for debugging.
zra: This is the pretty printer that Maincil will use. by default it is set to defaultCilPrinter
Print a type given a pretty printer
Print an expression given a pretty printer
Print an lvalue given a pretty printer
Print a global given a pretty printer
Print an attribute given a pretty printer
Print a set of attributes given a pretty printer
Print an instruction given a pretty printer
Print a statement given a pretty printer. This can take very long (or even overflow the stack) for huge statements. Use dumpStmt instead.
Print a block given a pretty printer. This can take very long (or even overflow the stack) for huge block. Use dumpBlock instead.
Dump a statement to a file using a given indentation. Use this instead of printStmt whenever possible.
Dump a block to a file using a given indentation. Use this instead of printBlock whenever possible.
Print an initializer given a pretty printer. This can take very long (or even overflow the stack) for huge initializers. Use dumpInit instead.
Dump an initializer to a file using a given indentation. Use this instead of printInit whenever possible.
Pretty-print an offset using defaultCilPrinter, given the pretty printing for the base.
Pretty-print an initializer using defaultCilPrinter. This can be extremely slow (or even overflow the stack) for huge initializers. Use dumpInit instead.
Pretty-print a binary operator
Pretty-print a unary operator
Pretty-print a statement using defaultCilPrinter. This can be extremely slow (or even overflow the stack) for huge statements. Use dumpStmt instead.
Pretty-print a block using defaultCilPrinter. This can be extremely slow (or even overflow the stack) for huge blocks. Use dumpBlock instead.
Pretty-print the internal representation of a global using defaultCilPrinter. This can be extremely slow (or even overflow the stack) for huge globals (such as arrays with lots of initializers). Use dumpGlobal instead.
Versions of the above pretty printers, that don't print #line directives
Pretty-print a short description of the global. This is useful for error messages
Pretty-print a global. Here you give the channel where the printout should be sent.
Pretty-print an entire file. Here you give the channel where the printout should be sent.
the following error message producing functions also print a location in the code. use Errormsg.bug and Errormsg.unimp if you do not want that
Like error except that it explicitly takes a location argument, instead of using the currentLoc
Like warn except that it explicitly takes a location argument, instead of using the currentLoc
Sometimes you do not want to see the syntactic sugar that the above pretty-printing functions add. In that case you can use the following pretty-printing functions. But note that the output of these functions is not valid C
Pretty-print the internal representation of an expression
Pretty-print the internal representation of an integer
Pretty-print the internal representation of an lvalue
Pretty-print the internal representation of an lvalue offset val d_plainoffset: unit -> offset -> Pretty.doc
Pretty-print the internal representation of a type
Pretty-print an expression while printing descriptions rather than names of temporaries.
Pretty-print an lvalue on the left side of an assignment. If there is an offset or memory dereference, temporaries will be replaced by descriptions as in dd_exp. If the lval is a temp var, that var will not be replaced by a description; use "dd_exp () (Lval lv)" if that's what you want.
ALPHA conversion has been moved to the Alpha module.
val uniqueVarNames : file -> unitAssign unique names to local variables. This might be necessary after you transformed the code and added or renamed some new variables. Names are not used by CIL internally, but once you print the file out the compiler downstream might be confused. You might have added a new global that happens to have the same name as a local in some function. Rename the local to ensure that there would never be confusion. Or, viceversa, you might have added a local with a name that conflicts with a global
Optimization Passes
A peephole optimizer that processes two adjacent instructions and possibly replaces them both. If some replacement happens, then the new instructions are themselves subject to optimization
Similar to peepHole2 except that the optimization window consists of one instruction, not two
Machine dependency
exception SizeOfError of string * typRaised when one of the bitsSizeOf functions cannot compute the size of a type. This can happen because the type contains array-length expressions that we don't know how to compute or because it is a type whose size is not defined (e.g. TFun or an undefined compinfo). The string is an explanation of the error
Give the unsigned kind corresponding to any integer kind
Give the signed kind corresponding to any integer kind
val intRank : ikind -> intReturn the integer conversion rank of an integer kind
Return the common integer kind of the two integer arguments, as defined in ISO C 6.3.1.8 ("Usual arithmetic conversions")
val intKindForSize : int -> bool -> ikindThe signed integer kind for a given size (unsigned if second argument is true). Raises Not_found if no such kind exists
val floatKindForSize : int -> fkindThe float kind for a given size. Raises Not_found if no such kind exists
val bytesSizeOfInt : ikind -> intThe size in bytes of the given int kind.
val bitsSizeOf : typ -> intThe size of a type, in bits. Trailing padding is added for structs and arrays. Raises SizeOfError when it cannot compute the size. This function is architecture dependent, so you should only call this after you call initCIL. Remember that on GCC sizeof(void) is 1!
Represents an integer as for a given kind. Returns a truncation flag saying that the value fit in the kind (NoTruncation), didn't fit but no "interesting" bits (all-0 or all-1) were lost (ValueTruncation) or that bits were lost (BitTruncation). Another way to look at the ValueTruncation result is that if you had used the kind of opposite signedness (e.g. IUInt rather than IInt), you would gave got NoTruncation...
True if the integer fits within the kind's range
Return the smallest kind that will hold the integer's value. The kind will be unsigned if the 2nd argument is true, signed otherwise. Note that if the value doesn't fit in any of the available types, you will get ILongLong (2nd argument false) or IULongLong (2nd argument true).
Construct a cilint from an integer kind and int64 value. Used for getting the actual constant value from a CInt(n, ik, _) constant.
The size of a type, in bytes. Returns a constant expression or a "sizeof" expression if it cannot compute the size. This function is architecture dependent, so you should only call this after you call initCIL.
val alignOf_int : typ -> intThe minimum alignment (in bytes) for a type. This function is architecture dependent, so you should only call this after you call initCIL.
Give a type of a base and an offset, returns the number of bits from the base address and the width (also expressed in bits) for the subobject denoted by the offset. Raises SizeOfError when it cannot compute the size. This function is architecture dependent, so you should only call this after you call initCIL.
val char_is_unsigned : bool refWhether "char" is unsigned. Set after you call initCIL
val little_endian : bool refWhether the machine is little endian. Set after you call initCIL
val underscore_name : bool refWhether the compiler generates assembly labels by prepending "_" to the identifier. That is, will function foo() have the label "foo", or "_foo"? Set after you call initCIL
Represents a location that cannot be determined
Return the location of an instruction
Return the location of a global, or locUnknown
Return the location of a statement, or locUnknown
Generate an exp to be used in case of errors.
Generate an instr to be used in case of errors.
Generate a global to be used in case of errors.
val mapNoCopy : ('a -> 'a) -> 'a list -> 'a listLike map but try not to make a copy of the list
val mapNoCopyList : ('a -> 'a list) -> 'a list -> 'a listLike map but each call can return a list. Try not to make a copy of the list
val startsWith : string -> string -> boolsm: return true if the first is a prefix of the second string
val endsWith : string -> string -> boolreturn true if the first is a suffix of the second string
val stripUnderscores : string -> stringIf string has leading and trailing __, strip them.
val freshLabel : string -> stringTo generate new labels which do not provoke collision, call populateLabelAlphaTable for the corresponding fundec before
val populateLabelAlphaTable : fundec -> unitClears the labelAlphaTable and populates it with all label names appearing in the fundec. Needs to be called before freshLabel
An Interpreter for constructing CIL constructs
The type of argument for the interpreter
Pretty-prints a format arg
val warnTruncate : bool refEmit warnings when truncating integer constants (default true)
Machine model specified via CIL_MACHINE environment variable