Previous  Up  Next

Module Types

module Types: sig .. end
Types used during the analysis
type name_var = string
Name of variables, functions and labels
type loc =
| Loc_c of int
| Loc_a of int
Locations of statements in programs
type type_c =
| Int_c
| Ptr of type_c
Type of C variables
type boolOpBoolBin =
| And
| Or
Binary operators which are of type bool -> bool -> bool
type boolOpArithBin =
| Eq
| Neq
| Lt
| Gt
| Le
| Ge
Binary operators which are of type int -> int -> bool
type arithOpArithBin =
| Plus
| Minus
| Times
| Div
Binary operators which are of type int -> int -> int
type boolOpBoolUna =
| Not
Unary operators which are of type bool -> bool
type arithOpArithUna =
| MinusUna
| BitwiseNot
Unary operators which are of type int -> bool
type reg32 =
| EAX
| EBX
| ECX
| EDX
Registers actually implemented in the analyser
type asm_expr =
| AsmReg of reg32
| AsmPtr of asm_expr
| AsmVar of name_var
| AsmCst of Z.t
| AsmLbl of name_var
| AsmLblLoc of loc
ASM expression aka operands of ASM statements
type ptr_var =
| PtrVar of ptr_var
| LastPtrVar of string
Pointer induction to a variable name
type stat_c =
| Declare of type_c * name_var
| DeclareAssign of type_c * name_var * arith_expr
| Assign of name_var * arith_expr
| Return of arith_expr
| Branch of bool_expr * loc_stat_c * loc_stat_c
| BranchWithoutLoc of bool_expr * stat_c list * stat_c list
| Asm of loc_stat_a
| AsmWithoutLoc of stat_a list
| While of bool_expr * loc_stat_c
| WhileWithoutLoc of bool_expr * stat_c list
| CallAssignC of name_var * name_var * arith_expr list
| CallAssignAsm of name_var * loc * arith_expr list
| PtrAssign of ptr_var * arith_expr
C statements
type stat_a =
| Label of name_var
| Jmp of asm_expr
| Mov of (asm_expr * asm_expr)
| Ret
| Call of asm_expr
| Push of asm_expr
| Pop of asm_expr
ASM statements
type loc_stat_c = loc * (stat_c * loc) list
Located C block
type loc_stat_a = loc * (stat_a * loc) list
Located ASM block
type arith_expr =
| Var of name_var
| Deref of arith_expr
| Addr of name_var
| Cons of Z.t
| Interval of Z.t * Z.t
| ArithArithBinExpr of arith_expr * arithOpArithBin * arith_expr
| ArithArithUnaExpr of arithOpArithUna * arith_expr
| TernaryExpr of bool_expr * arith_expr * arith_expr
C arithmetic expression
type bool_expr =
| True
| False
| BoolBinExpr of bool_expr * boolOpBoolBin * bool_expr
| BoolUnaExpr of boolOpBoolUna * bool_expr
| BoolArithBinExpr of arith_expr * boolOpArithBin * arith_expr
C boolean expressions
type arguments = (type_c * name_var) list
Definition of the arguments of C functions
type global_statement =
| Function of (type_c * name_var * arguments * loc_stat_c)
| FunctionWithoutLoc of (type_c * name_var * arguments * stat_c list)
Statements which are globals. So far, functions.
type program = loc * (global_statement * loc) list
C program with inline assembly
type generic_stat_loc =
| StatC of (loc * stat_c * loc)
| StatA of (loc * stat_a * loc)
Statement with its location associated
module IdSet: Set.Make(sig
type t = int 
val compare : 'a -> 'a -> int
end)
Set wich contains ids of variables, used to represent abstact domain of pointers 
type abstrD =
| AbstrD of (Z.t * Z.t)
| AbstrPtr of IdSet.t
| AbstrLoc of loc
| AbstrBot
Abstract domain
type realD =
| RealD of Z.t list
| RealBot
Real domain
val abstrMin : Z.t
Minimum number
val abstrMax : Z.t
Maximum number
val abstrTop : abstrD
Top element of the abstract domains
module Context: Map.Make(String)
Map with variable names as key 
type abstrContext =
| AbstrContext of int Context.t
| GoForward of loc * abstrContext
| AbstrContextBot
Context
type memoryStack = abstrD list
Memory stack
module Environment: Map.Make(sig
type t = int 
val compare : 'a -> 'a -> int
end)
Map with id as keys 
type abstrEnvironment = abstrD Environment.t
Environment
module LocMap: Map.Make(sig
type t = Types.loc 
val compare : 'a -> 'a -> int
end)
type functionContext = (global_statement * abstrContext) LocMap.t
Map which associates locations to their C functions (and contexts) associated
type callStack = (bool * abstrD * abstrEnvironment Pervasives.ref *
        abstrContext * memoryStack)
       Stack.t
Call stack (which is really a stack)
exception ReturnRaised of abstrD * abstrEnvironment Pervasives.ref * abstrContext
        * memoryStack
A return/ret instruction has been encountered and the function/block of statements is returned with the abstract domain of the value returned, the context and the memory stack associated
exception GoBackward
Do we have to go back in the past to start again a branch with more anticipation of a jump
val labels : loc Context.t Pervasives.ref
Map which associates all the labels which have been encountered with their locations