Safe Haskell	None
Language	Haskell2010

Analysis.ControlFlow

Description

Synopsis

cfg_gen :: Context -> Int -> IO (Set (Instruction, Int), CFG)
cfg_to_dot :: Context -> CFG -> String
is_end_node :: CFG -> Int -> Bool
node_info_of :: Context -> CFG -> Int -> NodeInfo
stepA :: Context -> Int -> Int -> IO (Either (Set (Instruction, Int)) [(Int, Bool)])
post :: CFG -> Key -> IntSet
fetch_block :: CFG -> Int -> [Instruction]
resolve_jump_target :: Context -> Instruction -> [ResolvedJumpTarget]
get_internal_addresses :: ResolvedJumpTarget -> [Int]
jump_is_actually_a_call :: Context -> Instruction -> Bool
show_block :: CFG -> Int -> String
show_invariants :: CFG -> Invariants -> String
isTerminal :: CFG -> Key -> Bool

Documentation

cfg_gen Source #

Arguments

:: Context	The context
-> Int	The entry point of the function
-> IO (Set (Instruction, Int), CFG)

Produce a CFG

Given the entry point of the function, generate either a CFG, or a set of new entry points to be analyzed first. The set of new entry points are function entries called by the current function, but for which we do not know yet whether they terminate or not. If a CFG is returned, then all function calls in that CFG have already been analyzed.

cfg_to_dot Source #

Arguments

:: Context	The context
-> CFG	The CFG
-> String

Export a CFG to .dot file

Strongly connected components get the same color.

is_end_node Source #

Arguments

:: CFG	The CFG
-> Int	The blockID
-> Bool

Returns true if the given blockID is a leaf-node in the given CFG.

node_info_of Source #

Arguments

:: Context	The context
-> CFG
-> Int
-> NodeInfo

Returns the NodeInfo of a given blockID.

Assumes the given blockID corresponds to a leaf-node.

stepA Source #

Arguments

:: Context	The context
-> Int	The entry address
-> Int	The instruction address
-> IO (Either (Set (Instruction, Int)) [(Int, Bool)])

An abstract step function

Given the entry address of the function currently under investigation, and the instruction address of the current instruction, try to get the set of next instruction addresses.

This returns either: * a set of tuples (i,a) where i is an instruction and a its address. All these instructions are function calls that need to be analyzed before this current function entry can continue. * a list of tuples (a,b) where a is an instruction address that may follow the current instruction, and b is a Bool indicating whether that address belongs to a call

TODO the Lefts are ignored so need no to return them

post :: CFG -> Key -> IntSet Source #

The set of next blocks from the given block in a CFG

fetch_block Source #

Arguments

:: CFG	The CFG
-> Int	The blockID
-> [Instruction]

Fetching an instruction list given a block ID

resolve_jump_target Source #

Arguments

:: Context	The context
-> Instruction	The instruction
-> [ResolvedJumpTarget]

Resolves the first operand of a call or jump instruction. First tries to see if the instruction is an indirection, that has already been resolved. If not, try to statically resolve the first operand using operand_static_resolve. If that resolves to an immediate value, see if that immediate value corresponds to an external function or an internal function.

Returns a list of ResolvedJumpTarget, since an indirection may be resolved to multiple targets.

get_internal_addresses Source #

Arguments

:: ResolvedJumpTarget	A resolved jump target
-> [Int]

Given a resolved jump target, get a possibly empty list of internal addresses to which the jump target can jump.

jump_is_actually_a_call Source #

Arguments

:: Context	The context
-> Instruction	The instruction
-> Bool

Returns true iff the JUMP instruction is actually a CALL followed by implicit RET

show_block Source #

Arguments

:: CFG	The CFG
-> Int	The blockID
-> String

Shows the block associated to the givern blockID.

show_invariants Source #

Arguments

:: CFG	The CFG
-> Invariants	The invariants
-> String

Shows invariants.

isTerminal :: CFG -> Key -> Bool Source #