Module GenericAbstract

module GenericAbstract: sig .. end

Static interpretation methods which are not dependant to the abstraction domain chosen.

val var_id : int Pervasives.ref

The last id used in an environment

val areEnvironmentEqual : Types.abstrEnvironment Pervasives.ref ->
       Types.abstrEnvironment Pervasives.ref -> bool

Test equality of two environments

e1 The first environment
e2 The second environment

Returns Are e1 and e2 equal

val wideningOnEnvironments : Types.abstrEnvironment Pervasives.ref ->
       Types.abstrEnvironment Pervasives.ref ->
       Types.abstrEnvironment Pervasives.ref

Apply widening on two environments by applying the widening to all the abstract domains of their ids. Delete the variables which exist only in one environment.

e1 The first environment
e2 The second environment

Returns The environment made of the application of the widening on e1 and e2

val environmentJoin : Types.abstrEnvironment Pervasives.ref ->
       Types.abstrEnvironment Pervasives.ref ->
       Types.abstrEnvironment Pervasives.ref

Joins two environment by joining all the ids. Delete the variables which exist only in one environment.

e1 The first environment
e2 The second environment

Returns The environment made of the join of e1 and e2

val contextMerge : Types.abstrContext -> Types.abstrContext -> Types.abstrContext

Merge two contexts by returning the variables which are both represented by the same ids.

c1 The first context
c2 The second context

Returns The resulting context

val forgetNewVariables : lastContext:Types.abstrContext ->
       newContext:Types.abstrContext ->
       env:Types.abstrEnvironment Pervasives.ref -> unit

Remove from the environment the variables which have been added in the newContext.

lastContext The original context
newContext The new context with perhaps some variables which have been added or modified and which should be forgotten in the env
env The environment

Returns unit

val environmentMeet : Types.abstrEnvironment Pervasives.ref ->
       Types.abstrEnvironment Pervasives.ref ->
       Types.abstrEnvironment Pervasives.ref

Meet two environment by meeting all the ids. Delete the variables which exist only in one environment.

e1 The first environment
e2 The second environment

Returns The environment made of the meet of e1 and e2

val getVar : context:Types.abstrContext ->
       vn:Types.name_var ->
       env:Types.abstrEnvironment Pervasives.ref -> Types.abstrD

Return a variable at a location in an environment

context The context in which vn is
vn The name of the variable
env The environment in which the variable will be searched

Raises UNDEFINEDVAR if the variable is not declared at the location specified
Returns The abstract domain of the variable at the location specified

val lfp : env:Types.abstrEnvironment Pervasives.ref ->
       e1:(Types.abstrContext * Types.memoryStack ->
           Types.abstrContext * Types.memoryStack) ->
       Types.abstrContext * Types.memoryStack -> Types.memoryStack

Calculates the least fixpoint of env by the function e1

env The initial environment
e1 The function to apply on the environment until we have a fixpoint (or an over-approximation of it if we use a widening function)
context The initial context
lastStack The initial memory stack

Returns The memory stack when the least fixpoint (or the over-approximation of it) has been found

val addVarToContext : vn:Types.name_var ->
       value:Types.abstrD ->
       env:Types.abstrEnvironment Pervasives.ref ->
       Types.abstrContext -> Types.abstrContext

Adds an undefined variable to a context and returns the new context

vn The name of the variable
value The value of the variable that we want to set
env The environment
context The context

Raises ALREADYDEFINED if the variable already exists in context
Returns The new context in which the value of the variable has been added

val updateVarInContext : vn:Types.name_var ->
       value:Types.abstrD ->
       context:Types.abstrContext ->
       env:Types.abstrEnvironment Pervasives.ref -> unit

Update an existing variable in a context and returns the new context

vn The name of the variable
value The value of the variable that we want to set
context The context
env The environment

Raises UNDEFINEDVAR if the variable doesn't exist in context
Returns unit

val getAsmValue : ae:Types.asm_expr ->
       context:Types.abstrContext ->
       env:Types.abstrEnvironment Pervasives.ref -> Types.abstrD

Get the abstract interpretation of an ASM expression

ae The ASM expression
context The context
env The environment

Returns The abstract interpretation of the ae in the provided context and env

val getLastFunction : l:Types.loc ->
       f:Types.functionContext Pervasives.ref ->
       Types.global_statement * Types.abstrContext

Get the C function in which a location is

l The location
f The reference to the set of the C functions which are known

Returns The function as a global statement and the context associated to it

val joinMemoryStack : s1:Types.memoryStack -> s2:Types.memoryStack -> Types.memoryStack

Join the abstract values of two memory stacks

s1 The first memory stack
s2 The second memory stack

Raises WRONGSTACKOFFSET If the stacks don't have the same length
Returns The memory stack in which each element is the join of the initials memory stacks

val initFunction : cCall:bool -> callStack:Types.callStack Pervasives.ref -> unit

Initialize the call stack in order to prepare it before the call of a function

cCall Is it a call to a C function (respectively ASM function)
callStack A reference to the call stack

Returns unit

val postlude_asm : context:Types.abstrContext ->
       env:Types.abstrEnvironment Pervasives.ref -> Types.abstrContext

Remove the registers from a context and in the associated environment after an ASM block

context The context

Returns The new context without the registers' values

val raiseReturn : cCall:bool ->
       addReturnPossibility:bool ->
       returnCode:Types.abstrD ->
       returnContext:Types.abstrContext ->
       returnEnv:Types.abstrEnvironment Pervasives.ref ->
       callStack:Types.callStack Pervasives.ref -> stack:Types.memoryStack -> unit

Raise a return (called by return/ret statement), join the return code, the return context, the return environment and the memory stack with the last ones saved

cCall Is the statement which calls it a return (respectively ret)
addReturnPossibility Do we have to wait for another return/ret
returnCode The code that has been returned
returnContext The context that has been returned
returnEnv The environment that has been returned
callStack A reference to the actual call stack
stack The memory stack to return

Raises Failure If you try to return a C function in ASM and vice versa
Returns unit

val abexpBoolBin : Types.abstrEnvironment Pervasives.ref * bool ->
       Types.boolOpBoolBin ->
       Types.abstrEnvironment Pervasives.ref * bool ->
       Types.abstrEnvironment Pervasives.ref * bool

Generic abstract interpretation of binary boolean operators

env1 The possible environment in which the first operand is satisfied
context1IsBot Is the context associated to env1 bottom
op The binary boolean operator
env2 The possible environment in which the second operand is satisfied
context2IsBot Is the context associated to env2 bottom

Returns The environment in which the whole boolean operation is satisfied and a boolean which represents if the resulting environment is bottom

val faexp : a:Types.arith_expr ->
       context:Types.abstrContext ->
       env:Types.abstrEnvironment Pervasives.ref -> Types.abstrD

Forward abstract semantics of arithmetic expressions

a An arithmetic expression
context The context in which the arithmetic expression is performed
env The environment in which the arithmetic expression is performed, perhaps it will be modified

Raises

UNDEFINEDVAR If a variable is not defined in the provided context
PTRINTMATCH If an operation is performed between a pointer and an int

Returns The abstract domain of the evaluation of the arithmetic expression

val baexp : a:Types.arith_expr ->
       context:Types.abstrContext ->
       p:Types.abstrD -> env:Types.abstrEnvironment Pervasives.ref -> bool

Backward abstract semantics of arithmetic expressions

a An arithmetic expression
context The context in which the arithmetic expression is performed
p The domain in which the evaluation of the arithmetic expression has to be
env The environment in which the arithmetic expression is performed, perhaps it will be modified

Raises UNDEFINEDVAR If a variable is not defined in the provided context
Returns Does the resulting context have to be bottom

val abexp : b:Types.bool_expr ->
       context:Types.abstrContext ->
       env:Types.abstrEnvironment Pervasives.ref -> bool

Generic abstract interpretation of boolean expression

b The boolean expression
context The context
env The environment, perhaps it will be modified

Returns Does the resulting context have to be bottom

val matchCArgs : args_def:Types.arguments ->
       args:Types.arith_expr list ->
       contextToEnhance:Types.abstrContext ->
       context:Types.abstrContext ->
       env:Types.abstrEnvironment Pervasives.ref -> Types.abstrContext

Add the abstract interpretation of a list of variables by the definition of a C function

args_def The definition of the arguments of a C function
args The list of the arithmetic expressions provided
contextToEnhance The context to update
context The context in which the arithmetic expression will be evaluated
env The environment in which the arithmetic expression will be evaluated and which will be enhanced with the new variables

Raises Failure If args_def doesn't match args
Returns The new context made from contextToEnhance

val matchAsmArgs : context:Types.abstrContext ->
       args_def:Types.arguments ->
       stack:Types.memoryStack ->
       env:Types.abstrEnvironment Pervasives.ref ->
       Types.abstrContext * Types.memoryStack

Adds the arguments from a memory stack to a context by a C function's definition

context The context
args_def_reversed The definition of the arguments that the C function is waiting for
stack The memory stack
env The environment

Raises Failure If the memory stack is too tiny compared to the argument's list
Returns The pair made of the new context and of the new memory stack (without the arguments used)

val prelude_asm : context:Types.abstrContext ->
       env:Types.abstrEnvironment Pervasives.ref -> Types.abstrContext

Add registers to the context

context The context before the ASM block
env The environment which will be modified

Returns The new context with the registers set

val reset_registers : context:Types.abstrContext ->
       env:Types.abstrEnvironment Pervasives.ref -> eax_value:Types.abstrD -> unit

Reset the value of all registers except EAX which is replaced by a specified value

context The context
env The environment which will be modified
eax_value The new value of EAX

Returns unit

val setRegisters : realContext:Types.abstrContext ->
       contextWithRegs:Types.abstrContext ->
       env:Types.abstrEnvironment Pervasives.ref -> unit

Replace the registers of a context by the registers of another one

c1 The context in which the registers will be changed
c2 The context from which the registers will be get
env The environment which will be modified

Returns The new context made of c1 with registers of c2

val aPostAsm : Types.loc * Types.stat_a * Types.loc ->
       shouldGoBackOnJmp:bool ->
       f:Types.functionContext Pervasives.ref ->
       callStack:Types.callStack Pervasives.ref ->
       stack:Types.memoryStack ->
       env:Types.abstrEnvironment Pervasives.ref ->
       context:Types.abstrContext -> Types.abstrContext * Types.memoryStack

Generic forward non-relational abstract interpretation of ASM statements

stat The statement which is currently read
shouldGoBackOnJmp Is the statement read in a branch which has not been read before
f A reference to the set of the C functions
callStack The call stack
stack The memory stack
env The environment
context The context

Returns A pair made of the new context after the read of stat and of the new memory stack

val aPostAsmBlock : Types.loc * (Types.stat_a * Types.loc) list ->
       shouldGoBackOnJmp:bool ->
       f:Types.functionContext Pervasives.ref ->
       callStack:Types.callStack Pervasives.ref ->
       stack:Types.memoryStack ->
       env:Types.abstrEnvironment Pervasives.ref ->
       Types.abstrContext -> Types.abstrContext * Types.memoryStack

Generic forward non-relational abstract interpretation of ASM blocks

pre_loc The entry location of block
block The block of ASM statement to read
shouldGoBackOnJmp Is the statement read in a branch which has not been read before
f A reference to the set of C functions
callStack The call stack
stack The memory stack
env The environment
context The context

Returns A pair made of the new context and of the new memory stack

val aPostCBlock : Types.loc_stat_c ->
       shouldGoBackOnJmp:bool ->
       f:Types.functionContext Pervasives.ref ->
       callStack:Types.callStack Pervasives.ref ->
       lastAsmStack:Types.memoryStack ->
       env:Types.abstrEnvironment Pervasives.ref ->
       context:Types.abstrContext -> Types.abstrContext * Types.memoryStack

Generic forward non-relational abstract interpretation of C blocks

program The block of C statements
shouldGoBackOnJmp Is the statement read in a branch which has not been read before
f A reference to the C functions
callStack The call stack
lastAsmStack The stack state of the last ASM statement
env The environment
context The context

Returns The pair made of the new context after the execution of the block of C statements and the new memory stack

val aPostC : Types.loc * Types.stat_c * Types.loc ->
       shouldGoBackOnJmp:bool ->
       f:Types.functionContext Pervasives.ref ->
       callStack:Types.callStack Pervasives.ref ->
       lastAsmStack:Types.memoryStack ->
       env:Types.abstrEnvironment Pervasives.ref ->
       context:Types.abstrContext -> Types.abstrContext * Types.memoryStack

Generic forward non-relational abstract interpretation of C statements

stat The C statement
shouldGoBackOnJmp Is the statement read in a branch which has not been read before
f A reference to the C functions
callStack The call stack
lastAsmStack The stack state of the last ASM statement
env The environment
context The context

Returns The pair made of the new context after the excetion of the C statement and of the new memory stack

val aPostGlobalC : pre_loc:Types.loc ->
       stat:Types.global_statement ->
       post_loc:Types.loc ->
       f:Types.functionContext Pervasives.ref ->
       env:Types.abstrEnvironment Pervasives.ref ->
       Types.abstrContext -> Types.abstrContext

Generic forward non-relational abstract interpretation of global statement

pre_loc The location before the global statement
stat The global statement
post_loc The location after the global statement
f A reference to the set of C functions
env The environement
context The context

Returns The new context after the execution of the global statement

val aPostProgram : pre_loc:Types.loc ->
       program:(Types.global_statement * Types.loc) list ->
       f:Types.functionContext Pervasives.ref ->
       env:Types.abstrEnvironment Pervasives.ref ->
       Types.abstrContext -> Types.abstrContext

Generic foward non-relational abstract interpretation of a block of global statements

pre_loc The location before the first global statement of the block
program The block of global statements
f A reference to the set of C functions
env The environment
context The context

Returns The new context after the execution of the block of global statements