module Cil2cfg: sig
.. end
Build a CFG of a function keeping some information of the initial structure.
abstract type of a cfg
val dkey : Log.category
val debug : ('a, Format.formatter, unit) Pervasives.format -> 'a
val debug2 : ('a, Format.formatter, unit) Pervasives.format -> 'a
Nodes
type
block_type =
Be careful that only Bstmt are real Block statements
Be careful that only Bstmt are real Block statements
type
call_type =
val pp_call_type : Format.formatter -> call_type -> unit
type
node_type =
type
node_info = {
}
type
node = node_info
abstract type of the cfg nodes
val node_type : node_info -> node_type
val bkind_stmt : block_type -> Cil_types.stmt option
val _bkind_sid : block_type -> int
type
node_id = int * int
val node_type_id : node_type -> node_id
gives a identifier to each CFG node in order to hash them
val node_id : node_info -> node_id
val pp_bkind : Format.formatter -> block_type -> unit
val pp_node_type : Format.formatter -> node_type -> unit
val same_node : node_info -> node_info -> bool
module VL: sig
.. end
the CFG nodes
val pp_node : Format.formatter -> node_info -> unit
val start_stmt_of_node : node_info -> Cil_types.stmt option
val node_stmt_opt : node_info -> Cil_types.stmt option
val node_stmt_exn : node_info -> Cil_types.stmt
Edge labels
type
edge_type =
| |
Enone |
| |
Ethen |
| |
Eelse |
| |
Eback |
| |
EbackThen |
| |
EbackElse |
| |
Ecase of Cil_types.exp list |
| |
Enext |
module EL: sig
.. end
the CFG edges
Graph
module PMAP: functor (
X
:
Graph.Sig.COMPARABLE
) ->
sig
.. end
module MyGraph: Graph.Blocks.Make
(
PMAP
)
the CFG is an ocamlgraph, but be careful to use it through the cfg function
because some edges don't have the same meaning as some others...
module CFG: sig
.. end
module Eset: FCSet.Make
(
CFG.E
)
Set of edges.
module Nset: FCSet.Make
(
CFG.V
)
Set of nodes.
module Ntbl: Hashtbl.Make
(
CFG.V
)
Hashtbl of node
type
t = {
}
The final CFG is composed of the graph, but also :
the function that it represents,
an hashtable to find a CFG node knowing its hashcode
abstract type of a cfg
val new_cfg_env : bool -> Cil_types.kernel_function -> t
val cfg_kf : t -> Cil_types.kernel_function
val cfg_graph : t -> CFG.t
val cfg_spec_only : t -> bool
returns true
is this CFG is degenerated (no code available)
val unreachable_nodes : t -> node_type list
Returns the nodes that are unreachable from the 'start' node.
These nodes have been removed from the cfg already.
CFG edges
type
edge = CFG.E.t
abstract type of the cfg edges
val edge_type : CFG.E.t -> edge_type
val edge_src : CFG.E.t -> CFG.E.vertex
node and edges relations
val edge_dst : CFG.E.t -> CFG.E.vertex
val pp_edge : Format.formatter -> CFG.E.t -> unit
val is_back_edge : CFG.E.t -> bool
val is_next_edge : CFG.E.t -> bool
val pred_e : t -> CFG.vertex -> CFG.E.t list
val succ_e : t -> CFG.vertex -> CFG.E.t list
type
edge_key = int * int * int * int
val edge_key : CFG.E.t -> edge_key
val same_edge : CFG.E.t -> CFG.E.t -> bool
Iterators
ignoring the Enext
edges
val iter_nodes : (CFG.vertex -> unit) -> t -> unit
val fold_nodes : (CFG.vertex -> 'a -> 'a) -> t -> 'a -> 'a
iterators
val iter_edges : (CFG.E.t -> unit) -> t -> unit
val iter_succ : (CFG.E.vertex -> unit) -> t -> CFG.vertex -> unit
val fold_succ : (CFG.E.vertex -> 'a -> 'a) ->
t -> CFG.vertex -> 'a -> 'a
val fold_pred : (CFG.E.vertex -> 'a -> 'a) ->
t -> CFG.vertex -> 'a -> 'a
val _iter_succ_e : (CFG.E.t -> unit) -> t -> CFG.vertex -> unit
val iter_pred_e : (CFG.E.t -> unit) -> t -> CFG.vertex -> unit
val fold_pred_e : (CFG.E.t -> 'a -> 'a) -> t -> CFG.vertex -> 'a -> 'a
val fold_succ_e : (CFG.E.t -> 'a -> 'a) -> t -> CFG.vertex -> 'a -> 'a
val cfg_start : t -> CFG.V.t
val start_edge : t -> CFG.E.t
get the starting edges
exception Found of node
val _find_stmt_node : t -> Cil_types.stmt -> node
val get_test_edges : t -> CFG.vertex -> CFG.E.t * CFG.E.t
Get the edges going out a test node with the then branch first
similar to succ_e g v
but tests the branch to return (then-edge, else-edge)
Raises Invalid_argument
if the node is not a test.
val get_switch_edges : t ->
CFG.vertex ->
(Cil_types.exp list * CFG.E.t) list * CFG.E.t
similar to succ_e g v
but give the switch cases and the default edge
val get_call_out_edges : t -> CFG.vertex -> CFG.E.t * CFG.E.t
similar to succ_e g v
but gives the edge to VcallOut first and the edge to Vexit second.
val get_edge_labels : CFG.E.t -> Clabels.c_label list
Returns the (normalized) labels at the program point of the edge.
val next_edge : t -> CFG.vertex -> CFG.E.t
val node_after : t -> CFG.vertex -> CFG.E.vertex
Find the node that follows the input node statement.
The statement postcondition can then be stored to the edges before that node.
Raises Not_found
when the node after has been removed (unreachable)
val get_pre_edges : t -> CFG.vertex -> CFG.E.t list
Find the edges where the precondition of the node statement have to be
checked.
val get_post_edges : t -> CFG.vertex -> CFG.E.t list
Find the edges where the postconditions of the node statement have to be
checked.
val get_exit_edges : t -> CFG.V.t -> CFG.E.t list
Find the edges e
that goes to the Vexit
node inside the statement
begining at node n
val add_edges_before : t ->
CFG.V.t -> Eset.t -> CFG.E.t -> Eset.t
val get_internal_edges : t -> CFG.vertex -> CFG.E.t list * Eset.t
Find the edges e
of the statement node n
postcondition
and the set of edges that are inside the statement (e
excluded).
For instance, for a single statement node, e
is succ_e n
,
and the set is empty. For a test node, e
are the last edges of the 2
branches, and the set contains all the edges between n
and the e
edges.
val get_edge_next_stmt : t -> CFG.E.t -> Cil_types.stmt option
Returns None when the edge leads to the end of the function.
val get_post_logic_label : t -> CFG.vertex -> Cil_types.logic_label option
Get the label to be used for the Post state of the node contract if any.
val blocks_closed_by_edge : t -> CFG.E.t -> Cil_types.block list
val has_exit : t -> bool
wether an exit edge exists or not
Generic table to store things on edges
module type HEsig = sig
.. end
signature of a mapping table from cfg edges to some information.
module HE: functor (
I
:
sig
end
) ->
sig
.. end
Building the CFG
val add_node : t -> node_type -> CFG.V.t
val change_node_kind : t -> CFG.vertex -> node_type -> CFG.V.t
val add_edge : t ->
CFG.E.vertex -> edge_type -> CFG.E.vertex -> unit
val remove_edge : t -> CFG.E.t -> unit
val insert_loop_node : t -> CFG.vertex -> node_type -> CFG.V.t
val init_cfg : bool ->
Cil_types.kernel_function -> t * CFG.V.t * CFG.V.t
val get_node : t -> node_type -> CFG.V.t
val setup_preconditions_proxies : Cil_types.exp -> unit
Setup the preconditions at all the call points of e_kf
, when possible
val get_call_type : Cil_types.exp -> call_type
val get_stmt_node : t -> Cil_types.stmt -> CFG.V.t
In some cases (goto for instance) we have to create a node before having
processed if through cfg_stmt
. It is important that the created node
is the same than while the 'normal' processing ! That is why
this pattern matching might seem redondant with the other one.
val cfg_stmts : t -> Cil_types.stmt list -> CFG.V.t -> CFG.V.t
build the nodes for the stmts
, connect the last one with next
,
and return the node of the first stmt.
val cfg_block : t ->
block_type ->
Cil_types.block -> CFG.E.vertex -> CFG.V.t
val cfg_switch : t ->
Cil_types.stmt ->
Cil_types.exp ->
Cil_types.block ->
Cil_types.stmt list -> CFG.E.vertex -> CFG.V.t
val cfg_stmt : t -> Cil_types.stmt -> CFG.V.t -> CFG.V.t
Cleaning
remove node and edges that are unreachable
val clean_graph : t -> t
About loops
Let's first remind some definitions about loops :
- back edge : edge n->h such that h dominates n.
- natural loop : defined by a back edge n->h
* h is called the loop header,
* the body of the loop is the set of nodes n that are "between" h and n,
ie all n predecessors until h.
Because h dominates n, every backward path from n go through h.
Notice that each node in the loop body is dominated by h.
A loop is not a natural loop if it has several entries (no loop header),
or if it has some irreducible region (no back edge).
Below, we use an algorithm from the paper :
"A New Algorithm for Identifying Loops in Decompilation"
of Tao Wei, Jian Mao, Wei Zou, and Yu Chen,
to gather information about the loops in the builted CFG.
module type WeiMaoZouChenInput = sig
.. end
module WeiMaoZouChen:
Implementation of
"A New Algorithm for Identifying Loops in Decompilation"
module LoopInfo: sig
.. end
To use WeiMaoZouChen algorithm,
we need to define how to interact with our CFG graph
module Mloop: WeiMaoZouChen
(
LoopInfo
)
module HEloop: HE
(
sig
end
)
val set_back_edge : CFG.E.t -> unit
val mark_loops : LoopInfo.graph -> t
val loop_nodes : t -> node list
val strange_loops : t -> node list
detect is there are non natural loops or natural loops where we didn't
manage to compute back edges (see mark_loops
). Must be empty in the mode
-wp-no-invariants
. (see also very_strange_loops
)
val very_strange_loops : t -> node list
detect is there are natural loops where we didn't manage to compute
back edges (see mark_loops
). At the moment, we are not able to handle those
loops.
Create CFG
val cfg_from_definition : Kernel_function.t -> Cil_types.fundec -> t
val cfg_from_proto : Cil_types.kernel_function -> t
Export dot graph
Printer for ocamlgraph
module Printer: functor (
PE
:
sig
val edge_txt : edge -> string
end
) ->
sig
.. end
Export to dot file
type
pp_edge_fun = Format.formatter -> edge -> unit
type of functions to print things related to edges
val export : file:string ->
?pp_edge_fun:(Format.formatter -> CFG.E.t -> unit) ->
t -> unit
CFG management
val create : Kernel_function.t -> t
module KfCfg: Kernel_function.Make_Table
(
Datatype.Make
(
sig
include Datatype.Undefined
type
tt = Cil2cfg.t
type
t = tt
val name : string
val mem_project : (Project_skeleton.t -> bool) -> 'a -> bool
val reprs : t list
val equal : t -> t -> bool
val hash : t -> int
val compare : t -> t -> int
end
)
)
(
sig
val name : string
val dependencies : State.t list
val size : int
end
)
val get : KfCfg.key -> KfCfg.data
Raises Log.FeatureRequest
for non natural loops and 'exception' stmts.
Returns the graph and the list of unreachable nodes.