Previous  Up  Next

Module Cil2cfg

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 =
| Bstmt of Cil_types.stmt
| Bthen of Cil_types.stmt
| Belse of Cil_types.stmt
| Bloop of Cil_types.stmt
| Bfct
Be careful that only Bstmt are real Block statements

Be careful that only Bstmt are real Block statements

type call_type =
| Dynamic of Cil_types.exp
| Static of Cil_types.kernel_function 
val pp_call_type : Format.formatter -> call_type -> unit
type node_type =
| Vstart
| Vend
| Vexit
| VfctIn
| VfctOut
| VblkIn of block_type * Cil_types.block
| VblkOut of block_type * Cil_types.block
| Vstmt of Cil_types.stmt
| Vcall of Cil_types.stmt * Cil_types.lval option * call_type
* Cil_types.exp list
| Vtest of bool * Cil_types.stmt * Cil_types.exp (*
bool=true for In and false for Out
*)
| Vswitch of Cil_types.stmt * Cil_types.exp
| Vloop of bool option * Cil_types.stmt (*
boolean is is_natural. None means the node has not been detected as a loop

boolean is is_natural. None means the node has not been detected as a loop.

*)
| Vloop2 of bool * int 
type node_info = {
   kind : node_type;
   mutable reachable : bool;
} 
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 (*
normal edge
*)
| Ethen (*
then branch : edge source is a Vtest
*)
| Eelse (*
else branch : edge source is a Vtest
*)
| Eback (*
back edge to a loop : the edge destination is a Vloop
*)
| EbackThen (*
Eback + Ethen
*)
| EbackElse (*
Eback + Eelse
*)
| Ecase of Cil_types.exp list (*
switch branch : edge source is a Vswitch. Ecase [] for default case
*)
| Enext (*
not really a edge : gives the next node of a complex stmt
*) 
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 = {
   kernel_function : Cil_types.kernel_function;
   graph : CFG.t;
   spec_only : bool;
   stmt_node : (int * int, CFG.V.t) Hashtbl.t;
   unreachables : node_type list;
   loop_nodes : node list option;
   mutable loop_cpt : int;
}
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

Getting information


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


type t 



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 : 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: 
functor (G : WeiMaoZouChenInput) -> sig .. end
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


type t = Cil2cfg.Nset.t 



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.